author wenzelm Tue, 07 Dec 1999 12:13:09 +0100 changeset 8051 5724bea1da53 parent 8050 ad6440cd84be child 8052 6ae3ca78a558
tuned;
 src/HOL/Isar_examples/ExprCompiler.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Fibonacci.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/ROOT.ML file | annotate | diff | comparison | revisions src/HOL/Isar_examples/document/root.bib file | annotate | diff | comparison | revisions src/HOL/Isar_examples/document/root.tex file | annotate | diff | comparison | revisions
--- 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);
-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)";
+  proof (induct ?P e type: expr);
+  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)";
+  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;
+      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)";
+  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.
+*)
+
+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}. *};
+
+  "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)";
+  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))";
+  also; have "... = gcd (fib (n + 1), fib (n + 1 + 1))";
+  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)";
+  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))";
+  also; have "fib (n + k + 1)
+    = fib (k + 1) * fib (n + 1) + fib k * fib n";
+  also; have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))";
+  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)";
+  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))";
+  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},
+  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}