# HG changeset patch
# User wenzelm
# Date 944565189 -3600
# Node ID 5724bea1da530d0aba1e42ee1b1b7b43f863079c
# Parent  ad6440cd84beb7b78377121de8ed267dfedeabc0
tuned;

diff -r ad6440cd84be -r 5724bea1da53 src/HOL/Isar_examples/ExprCompiler.thy
--- 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;
diff -r ad6440cd84be -r 5724bea1da53 src/HOL/Isar_examples/Fibonacci.thy
--- /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;
diff -r ad6440cd84be -r 5724bea1da53 src/HOL/Isar_examples/ROOT.ML
--- 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";
diff -r ad6440cd84be -r 5724bea1da53 src/HOL/Isar_examples/document/root.bib
--- 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},
diff -r ad6440cd84be -r 5724bea1da53 src/HOL/Isar_examples/document/root.tex
--- 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}