diff -r 1d1cc715a9e5 -r a084aa91f701 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Thu Nov 10 20:57:22 2005 +0100
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Thu Nov 10 21:14:05 2005 +0100
@@ -112,29 +112,32 @@
 *}
 
 lemma exec_append:
-  "ALL stack. exec (xs @ ys) stack env =
-    exec ys (exec xs stack env) env" (is "?P xs")
-proof (induct xs)
-  show "?P []" by simp
+  "exec (xs @ ys) stack env =
+    exec ys (exec xs stack env) env"
+proof (induct xs fixing: stack)
+  case Nil
+  show ?case by simp
 next
-  fix x xs assume hyp: "?P xs"
-  show "?P (x # xs)"
+  case (Cons x xs)
+  show ?case
   proof (induct x)
-    from hyp show "!!val. ?P (Const val # xs)" by simp
-    from hyp show "!!adr. ?P (Load adr # xs)" by simp
-    from hyp show "!!fun. ?P (Apply fun # xs)" by simp
+    case Const show ?case by simp
+  next
+    case Load show ?case by simp
+  next
+    case Apply show ?case 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")
+  have "!!stack. exec (compile e) stack env = eval e env # stack"
   proof (induct e)
-    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)
+    case Variable show ?case by simp
+  next
+    case Constant show ?case by simp
+  next
+    case Binop then show ?case by (simp add: exec_append)
   qed
   thus ?thesis by (simp add: execute_def)
 qed
@@ -149,98 +152,75 @@
 *}
 
 lemma exec_append':
-  "ALL stack. exec (xs @ ys) stack env
-    = exec ys (exec xs stack env) env" (is "?P xs")
-proof (induct 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)"
+  "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
+proof (induct xs fixing: stack)
+  case (Nil s)
+  have "exec ([] @ ys) s env = exec ys s env" by simp
+  also have "... = exec ys (exec [] s env) env" by simp
+  finally show ?case .
+next
+  case (Cons x xs s)
+  show ?case
   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 *}
+    case (Const val)
+    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 Cons have "... = exec ys (exec xs (val # s) env) env" .
+    also have "... = exec ys (exec (Const val # xs) s env) env" by simp
+    finally show ?case .
   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
+    case (Load adr)
+    from Cons show ?case by simp -- {* same as above *}
+  next
+    case (Apply fun)
+    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 Cons 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 ?case .
   qed
 qed
 
 theorem correctness': "execute (compile e) env = eval e env"
 proof -
   have exec_compile:
-    "ALL stack. exec (compile e) stack env = eval e env # stack"
-    (is "?P e")
+    "!!stack. exec (compile e) stack env = eval e env # stack"
   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
+    case (Variable adr 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 ?case .
   next
-    fix val show "?P (Constant val)" by simp -- {* same as above *}
+    case (Constant val s)
+    show ?case 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 =
+    case (Binop fun e1 e2 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 (compile e2) s env = eval e2 env # s" by fact
+    also have "exec (compile e1) ... env = eval e1 env # ..." by fact
+    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
+    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 ?case .
   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]" ..
+    have "exec (compile e) [] env = [eval e env]" .
   also have "hd ... = eval e env" by simp
   finally show ?thesis .
 qed