summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 07 Dec 1999 12:13:09 +0100 | |

changeset 8051 | 5724bea1da53 |

parent 8050 | ad6440cd84be |

child 8052 | 6ae3ca78a558 |

tuned;

--- a/src/HOL/Isar_examples/ExprCompiler.thy Tue Dec 07 12:12:54 1999 +0100 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Tue Dec 07 12:13:09 1999 +0100 @@ -106,8 +106,9 @@ text {* - The main result of this development is the correctness theorem for - $\idt{compile}$. We first establish some lemmas about $\idt{exec}$. + The main result of this development is the correctness theorem for + $\idt{compile}$. We first establish a lemma about $\idt{exec}$ and + list append. *}; lemma exec_append: @@ -116,8 +117,7 @@ proof (induct ?P xs type: list); show "?P []"; by simp; - fix x xs; - assume "?P xs"; + fix x xs; assume "?P xs"; show "?P (x # xs)" (is "?Q x"); proof (induct ?Q x type: instr); fix val; show "?Q (Const val)"; by (simp!); @@ -128,22 +128,114 @@ qed; qed; -lemma exec_compile: - "ALL stack. exec (compile e) stack env = + +theorem correctness: "execute (compile e) env = eval e env"; +proof -; + have "ALL stack. exec (compile e) stack env = eval e env # stack" (is "?P e"); -proof (induct ?P e type: expr); - fix adr; show "?P (Variable adr)"; by (simp!); -next; - fix val; show "?P (Constant val)"; by (simp!); -next; - fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)"; - by (simp! add: exec_append); + proof (induct ?P e type: expr); + fix adr; show "?P (Variable adr)"; by (simp!); + next; + fix val; show "?P (Constant val)"; by (simp!); + next; + fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)"; + by (simp! add: exec_append); + qed; + thus ?thesis; by (simp add: execute_def); qed; -text {* Main theorem ahead. *}; +text {* + \bigskip In the proofs above, the \name{simp} method does quite a lot + of work behind the scenes (mostly ``functional program execution''). + Subsequently, the same reasoning is elaborated in detail --- at most + one recursive function definition is used at a time. Thus we get a + better idea of what is actually going on. +*}; + +lemma exec_append: + "ALL stack. exec (xs @ ys) stack env + = exec ys (exec xs stack env) env" (is "?P xs"); +proof (induct ?P xs); + show "?P []" (is "ALL s. ?Q s"); + proof; + fix s; have "exec ([] @ ys) s env = exec ys s env"; by simp; + also; have "... = exec ys (exec [] s env) env"; by simp; + finally; show "?Q s"; .; + qed; + fix x xs; assume hyp: "?P xs"; + show "?P (x # xs)"; + proof (induct x); + fix val; + show "?P (Const val # xs)" (is "ALL s. ?Q s"); + proof; + fix s; + have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"; + by simp; + also; have "... = exec (xs @ ys) (val # s) env"; by simp; + also; from hyp; have "... = exec ys (exec xs (val # s) env) env"; ..; + also; have "... = exec ys (exec (Const val # xs) s env) env"; by simp; + finally; show "?Q s"; .; + qed; + next; + fix adr; from hyp; show "?P (Load adr # xs)"; by simp -- {* same as above *}; + next; + fix fun; + show "?P (Apply fun # xs)" (is "ALL s. ?Q s"); + proof; + fix s; + have "exec ((Apply fun # xs) @ ys) s env = exec (Apply fun # xs @ ys) s env"; + by simp; + also; have "... = exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env"; + by simp; + also; from hyp; have "... + = exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env"; ..; + also; have "... = exec ys (exec (Apply fun # xs) s env) env"; by simp; + finally; show "?Q s"; .; + qed; + qed; +qed; theorem correctness: "execute (compile e) env = eval e env"; - by (simp add: execute_def exec_compile); +proof -; + have exec_compile: + "ALL stack. exec (compile e) stack env = eval e env # stack" (is "?P e"); + proof (induct e); + fix adr; show "?P (Variable adr)" (is "ALL s. ?Q s"); + proof; + fix s; + have "exec (compile (Variable adr)) s env = exec [Load adr] s env"; by simp; + also; have "... = env adr # s"; by simp; + also; have "env adr = eval (Variable adr) env"; by simp; + finally; show "?Q s"; .; + qed; + next; + fix val; show "?P (Constant val)"; by simp -- {* same as above *}; + next; + fix fun e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2"; + show "?P (Binop fun e1 e2)" (is "ALL s. ?Q s"); + proof; + fix s; have "exec (compile (Binop fun e1 e2)) s env + = exec (compile e2 @ compile e1 @ [Apply fun]) s env"; by simp; + also; have "... + = exec [Apply fun] (exec (compile e1) (exec (compile e2) s env) env) env"; + by (simp only: exec_append); + also; from hyp2; have "exec (compile e2) s env = eval e2 env # s"; ..; + also; from hyp1; have "exec (compile e1) ... env = eval e1 env # ..."; ..; + also; have "exec [Apply fun] ... env + = fun (hd ...) (hd (tl ...)) # (tl (tl ...))"; by simp; + also; have "... = fun (eval e1 env) (eval e2 env) # s"; by simp; + also; have "fun (eval e1 env) (eval e2 env) = eval (Binop fun e1 e2) env"; + by simp; + finally; show "?Q s"; .; + qed; + qed; + + have "execute (compile e) env = hd (exec (compile e) [] env)"; + by (simp add: execute_def); + also; from exec_compile; have "exec (compile e) [] env = [eval e env]"; ..; + also; have "hd ... = eval e env"; by simp; + finally; show ?thesis; .; +qed; end;

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_examples/Fibonacci.thy Tue Dec 07 12:13:09 1999 +0100 @@ -0,0 +1,166 @@ +(* Title: HOL/Isar_examples/Fibonacci.thy + ID: $Id$ + Author: Gertrud Bauer + Copyright 1999 Technische Universitaet Muenchen + +The Fibonacci function. Demonstrates the use of recdef. Original +tactic script by Lawrence C Paulson. + +Fibonacci numbers: proofs of laws taken from + + R. L. Graham, D. E. Knuth, O. Patashnik. + Concrete Mathematics. + (Addison-Wesley, 1989) +*) + +header {* Fib and Gcd commute *}; + +theory Fibonacci = Primes:; + +text_raw {* + \footnote{Isar version by Gertrud Bauer. Original tactic script by + Lawrence C Paulson. A few proofs of laws taken from + \cite{Concrete-Math}.} +*}; + + +subsection {* Fibonacci numbers *}; + +consts fib :: "nat => nat"; +recdef fib less_than + "fib 0 = 0" + "fib 1 = 1" + "fib (Suc (Suc x)) = (fib x + fib (Suc x))"; + +lemmas [simp] = fib.rules; + +lemma [simp]: "0 < fib (Suc n)"; + by (induct n function: fib) (simp+); + + +text {* Alternative induction rule. *}; + +theorem fib_induct: +"[| P 0; P 1; !!n. [| P (n + 1); P n |] ==> P (n + 2) |] ==> P n"; + by (induct function: fib, simp+); + + + +subsection {* Fib and gcd commute *}; + +text {* A few laws taken from \cite{Concrete-Math}. *}; + +lemma fib_add: + "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" + (is "?P n"); +proof (rule fib_induct [of ?P n]); + txt_raw {* \cite[page 280]{Concrete-Math} *}; + show "?P 0"; by simp; + show "?P 1"; by simp; + fix n; + have "fib (n + 2 + k + 1) + = fib (n + k + 1) + fib (n + 1 + k + 1)"; by simp; + also; assume "fib (n + k + 1) + = fib (k + 1) * fib (n + 1) + fib k * fib n" + (is " _ = ?R1"); + also; assume "fib (n + 1 + k + 1) + = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)" + (is " _ = ?R2"); + also; have "?R1 + ?R2 + = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"; + by (simp add: add_mult_distrib2); + finally; show "?P (n + 2)"; .; +qed; + +lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n"); +proof (rule fib_induct [of ?P n]); + show "?P 0"; by simp; + show "?P 1"; by simp; + fix n; + have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"; + by simp; + also; have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"; + by (simp add: gcd_add2); + also; have "... = gcd (fib (n + 1), fib (n + 1 + 1))"; + by (simp add: gcd_commute); + also; assume "... = 1"; + finally; show "?P (n + 2)"; .; +qed; + +lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"; +proof -; + assume "0 < n"; + hence "gcd (n * k + m, n) = gcd (n, m mod n)"; + by (simp add: gcd_non_0 add_commute); + also; have "... = gcd (m, n)"; by (simp! add: gcd_non_0); + finally; show ?thesis; .; +qed; + +lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"; +proof (rule nat.exhaust [of m]); + assume "m = 0"; + thus "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"; by simp; +next; + fix k; assume "m = Suc k"; + hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"; + by (simp add: gcd_commute); + also; have "fib (n + k + 1) + = fib (k + 1) * fib (n + 1) + fib k * fib n"; + by (rule fib_add); + also; have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"; + by (simp add: gcd_mult_add); + also; have "... = gcd (fib n, fib (k + 1))"; + by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel); + also; have "... = gcd (fib m, fib n)"; + by (simp! add: gcd_commute); + finally; show ?thesis; .; +qed; + +lemma gcd_fib_diff: + "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"; +proof -; + assume "m <= n"; + have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"; + by (simp add: gcd_fib_add); + also; have "n - m + m = n"; by (simp!); + finally; show ?thesis; .; +qed; + +lemma if_cases: + "[| Q ==> P x; ~ Q ==> P y |] ==> P (if Q then x else y)"; by simp; + +lemma gcd_fib_mod: + "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; +proof (rule less_induct [of _ n]); + fix n; + assume m: "0 < m" + and hyp: "ALL ma. ma < n + --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"; + have "n mod m = (if n < m then n else (n - m) mod m)"; + by (rule mod_if); + also; have "gcd (fib m, fib ...) = gcd (fib m, fib n)"; + proof (rule if_cases); + assume "~ n < m"; hence m_le_n: "m <= n"; by simp; + have "n - m < n"; by (simp! add: diff_less); + with hyp; have "gcd (fib m, fib ((n - m) mod m)) + = gcd (fib m, fib (n - m))"; by simp; + also; from m_le_n; have "... = gcd (fib m, fib n)"; + by (rule gcd_fib_diff); + finally; show "gcd (fib m, fib ((n - m) mod m)) = gcd (fib m, fib n)"; .; + qed simp; + finally; show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; .; +qed; + + +theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n"); +proof (rule gcd_induct [of ?P m n]); + fix m; show "fib (gcd (m, 0)) = gcd (fib m, fib 0)"; by simp; + fix n; assume n: "0 < n"; + hence "gcd (m, n) = gcd (n, m mod n)"; by (rule gcd_non_0); + also; assume hyp: "fib ... = gcd (fib n, fib (m mod n))"; + also; from n; have "... = gcd (fib n, fib m)"; by (rule gcd_fib_mod); + also; have "... = gcd (fib m, fib n)"; by (rule gcd_commute); + finally; show "fib (gcd (m, n)) = gcd (fib m, fib n)"; .; +qed; + +end;

--- a/src/HOL/Isar_examples/ROOT.ML Tue Dec 07 12:12:54 1999 +0100 +++ b/src/HOL/Isar_examples/ROOT.ML Tue Dec 07 12:13:09 1999 +0100 @@ -15,5 +15,6 @@ time_use_thy "MutilatedCheckerboard"; with_path "../Induct" time_use_thy "MultisetOrder"; with_path "../W0" time_use_thy "W_correct"; +with_path "../ex" time_use_thy "Fibonacci"; time_use_thy "Puzzle"; time_use_thy "Minimal";

--- a/src/HOL/Isar_examples/document/root.bib Tue Dec 07 12:12:54 1999 +0100 +++ b/src/HOL/Isar_examples/document/root.bib Tue Dec 07 12:13:09 1999 +0100 @@ -5,6 +5,13 @@ @string{TUM="TU Munich"} +@Book{Concrete-Math, + author = {R. L. Graham and D. E. Knuth and O. Patashnik}, + title = {Concrete Mathematics}, + publisher = {Addison-Wesley}, + year = 1989 +} + @InProceedings{Wenzel:1999:TPHOL, author = {Markus Wenzel}, title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},

--- a/src/HOL/Isar_examples/document/root.tex Tue Dec 07 12:12:54 1999 +0100 +++ b/src/HOL/Isar_examples/document/root.tex Tue Dec 07 12:13:09 1999 +0100 @@ -6,7 +6,8 @@ \begin{document} \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic} -\author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/}} +\author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex] + With Contributions by Gertrud Bauer and Tobias Nipkow} \maketitle \begin{abstract}