--- 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}