# HG changeset patch
# User wenzelm
# Date 944583289 -3600
# Node ID 6ae3ca78a5582a6a18afc309d8b4966a4f27b33f
# Parent  5724bea1da530d0aba1e42ee1b1b7b43f863079c
tuned;

diff -r 5724bea1da53 -r 6ae3ca78a558 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Dec 07 12:13:09 1999 +0100
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Dec 07 17:14:49 1999 +0100
@@ -120,26 +120,21 @@
   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!);
-  next;
-    fix adr; show "?Q (Load adr)"; by (simp!);
-  next;
-    fix fun; show "?Q (Apply fun)"; by (simp!);
+    show "!!val. ?Q (Const val)"; by (simp!);
+    show "!!adr. ?Q (Load adr)"; by (simp!);
+    show "!!fun. ?Q (Apply fun)"; by (simp!);
   qed;
 qed;
 
-
 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);
+    show "!!adr. ?P (Variable adr)"; by simp;
+    show "!!val. ?P (Constant val)"; by simp;
+    show "!!fun e1 e2. (?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2))";
+      by (simp add: exec_append);
   qed;
   thus ?thesis; by (simp add: execute_def);
 qed;
@@ -154,7 +149,7 @@
 *};
 
 lemma exec_append:
-  "ALL stack. exec (xs @ ys) stack env 
+  "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");
@@ -166,30 +161,34 @@
   fix x xs; assume hyp: "?P xs";
   show "?P (x # xs)";
   proof (induct x);
-    fix val; 
+    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;
+      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;
+      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; 
+    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"; 
+      have "exec ((Apply fun # xs) @ ys) s env =
+          exec (Apply fun # xs @ ys) 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 (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;
@@ -198,13 +197,14 @@
 
 theorem correctness: "execute (compile e) env = eval e env";
 proof -;
-  have exec_compile: 
+  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;
+      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"; .;
@@ -215,23 +215,23 @@
     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 
+      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; 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 "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";  
+      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)"; 
+  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;
diff -r 5724bea1da53 -r 6ae3ca78a558 src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Tue Dec 07 12:13:09 1999 +0100
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Tue Dec 07 17:14:49 1999 +0100
@@ -19,7 +19,7 @@
 
 text_raw {*
  \footnote{Isar version by Gertrud Bauer.  Original tactic script by
- Lawrence C Paulson.  A few proofs of laws taken from
+ Larry Paulson.  A few proofs of laws taken from
  \cite{Concrete-Math}.}
 *};
 
@@ -53,8 +53,7 @@
 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} *};
+proof (rule fib_induct [of ?P n]) -- {* see \cite[page 280]{Concrete-Math} *};
   show "?P 0"; by simp;
   show "?P 1"; by simp;
   fix n;
diff -r 5724bea1da53 -r 6ae3ca78a558 src/HOL/Isar_examples/document/root.tex
--- a/src/HOL/Isar_examples/document/root.tex	Tue Dec 07 12:13:09 1999 +0100
+++ b/src/HOL/Isar_examples/document/root.tex	Tue Dec 07 17:14:49 1999 +0100
@@ -7,7 +7,7 @@
 
 \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
 \author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex]
-  With Contributions by Gertrud Bauer and Tobias Nipkow}
+  With contributions by Gertrud Bauer and Tobias Nipkow}
 \maketitle
 
 \begin{abstract}