# HG changeset patch
# User wenzelm
# Date 1131653645 -3600
# Node ID a084aa91f70175f5f6463761052c6fc4ec7e1f8f
# Parent  1d1cc715a9e54edc91e54ea9dcda8c5194e75ae5
tuned proofs;

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
diff -r 1d1cc715a9e5 -r a084aa91f701 src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Thu Nov 10 20:57:22 2005 +0100
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Thu Nov 10 21:14:05 2005 +0100
@@ -28,20 +28,19 @@
 
 consts fib :: "nat => nat"
 recdef fib less_than
- "fib 0 = 0"
- "fib (Suc 0) = 1"
- "fib (Suc (Suc x)) = fib x + fib (Suc x)"
+  "fib 0 = 0"
+  "fib (Suc 0) = 1"
+  "fib (Suc (Suc x)) = fib x + fib (Suc x)"
 
 lemma [simp]: "0 < fib (Suc n)"
-  by (induct n rule: fib.induct) (simp+)
+  by (induct n rule: fib.induct) simp_all
 
 
 text {* Alternative induction rule. *}
 
 theorem fib_induct:
     "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
-  by (induct rule: fib.induct, simp+)
-
+  by (induct rule: fib.induct) simp_all
 
 
 subsection {* Fib and gcd commute *}
@@ -88,19 +87,19 @@
 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)"
+  then have "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)
+  also from `0 < n` 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 (cases m)
-  assume "m = 0"
-  thus ?thesis by simp
+  case 0
+  then show ?thesis by simp
 next
-  fix k assume "m = Suc k"
-  hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
+  case (Suc k)
+  then have "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"
@@ -110,49 +109,44 @@
   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)
+    using Suc 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)"
+  assumes "m <= n"
+  shows "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!)
+  also from `m <= n` have "n - m + m = n" by simp
   finally show ?thesis .
 qed
 
 lemma gcd_fib_mod:
-  "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
-proof -
-  assume m: "0 < m"
-  show ?thesis
-  proof (induct n rule: nat_less_induct)
-    fix n
-    assume hyp: "ALL ma. ma < n
-      --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
-    show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
-    proof -
-      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 cases
-	assume "n < m" thus ?thesis by simp
-      next
-	assume not_lt: "~ n < m" hence le: "m <= n" by simp
-	have "n - m < n" by (simp!)
-	with hyp have "gcd (fib m, fib ((n - m) mod m))
-	  = gcd (fib m, fib (n - m))" by simp
-	also from le have "... = gcd (fib m, fib n)"
-	  by (rule gcd_fib_diff)
-	finally have "gcd (fib m, fib ((n - m) mod m)) =
-	  gcd (fib m, fib n)" .
-	with not_lt show ?thesis by simp
-      qed
-      finally show ?thesis .
+  assumes m: "0 < m"
+  shows "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
+proof (induct n rule: nat_less_induct)
+  case (1 n) note hyp = this
+  show ?case
+  proof -
+    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 (cases "n < m")
+      case True then show ?thesis by simp
+    next
+      case False then have "m <= n" by simp
+      from m and False have "n - m < n" by simp
+      with hyp have "gcd (fib m, fib ((n - m) mod m))
+        = gcd (fib m, fib (n - m))" by simp
+      also have "... = gcd (fib m, fib n)"
+        using `m <= n` by (rule gcd_fib_diff)
+      finally have "gcd (fib m, fib ((n - m) mod m)) =
+        gcd (fib m, fib n)" .
+      with False show ?thesis by simp
     qed
+    finally show ?thesis .
   qed
 qed
 
@@ -161,7 +155,7 @@
 proof (induct m n rule: gcd_induct)
   fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
   fix n :: nat assume n: "0 < n"
-  hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
+  then have "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)
diff -r 1d1cc715a9e5 -r a084aa91f701 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Nov 10 20:57:22 2005 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Nov 10 21:14:05 2005 +0100
@@ -29,16 +29,15 @@
 text "The union of two disjoint tilings is a tiling."
 
 lemma tiling_Un:
-  "t : tiling A ==> u : tiling A ==> t Int u = {}
-    ==> t Un u : tiling A"
+  assumes "t : tiling A" and "u : tiling A" and "t Int u = {}"
+  shows "t Un u : tiling A"
 proof -
   let ?T = "tiling A"
-  assume u: "u : ?T"
-  assume "t : ?T"
-  thus "t Int u = {} ==> t Un u : ?T" (is "PROP ?P t")
+  from `t : ?T` and `t Int u = {}`
+  show "t Un u : ?T"
   proof (induct t)
     case empty
-    with u show "{} Un u : ?T" by simp
+    with `u : ?T` show "{} Un u : ?T" by simp
   next
     case (Un a t)
     show "(a Un t) Un u : ?T"
@@ -46,11 +45,10 @@
       have "a Un (t Un u) : ?T"
       proof (rule tiling.Un)
         show "a : A" .
-	have atu: "(a Un t) Int u = {}" .
-	hence "t Int u = {}" by blast
-        thus "t Un u: ?T" by (rule Un)
-	have "a <= - t" .
-	with atu show "a <= - (t Un u)" by blast
+        from `(a Un t) Int u = {}` have "t Int u = {}" by blast
+        then show "t Un u: ?T" by (rule Un)
+        have "a <= - t" .
+        with `(a Un t) Int u = {}` show "a <= - (t Un u)" by blast
       qed
       also have "a Un (t Un u) = (a Un t) Un u"
         by (simp only: Un_assoc)
@@ -171,13 +169,13 @@
 qed
 
 lemma domino_singleton:
-  "d : domino ==> b < 2 ==> EX i j. evnodd d b = {(i, j)}"
+  assumes "d : domino" and "b < 2"
+  shows "EX i j. evnodd d b = {(i, j)}"
 proof -
-  assume b: "b < 2"
-  assume "d : domino"
-  thus ?thesis (is "?P d")
+  from `d : domino`
+  show ?thesis (is "?P d")
   proof induct
-    from b have b_cases: "b = 0 | b = 1" by arith
+    from `b < 2` have b_cases: "b = 0 | b = 1" by arith
     fix i j
     note [simp] = evnodd_empty evnodd_insert mod_Suc
     from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
@@ -185,10 +183,12 @@
   qed
 qed
 
-lemma domino_finite: "d: domino ==> finite d"
+lemma domino_finite:
+  assumes "d: domino"
+  shows "finite d"
 proof -
-  assume "d: domino"
-  thus ?thesis
+  from `d: domino`
+  show ?thesis
   proof induct
     fix i j :: nat
     show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
@@ -200,58 +200,53 @@
 subsection {* Tilings of dominoes *}
 
 lemma tiling_domino_finite:
-  "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t")
-proof -
-  assume "t : ?T"
-  thus "?F t"
-  proof induct
-    show "?F {}" by (rule Finites.emptyI)
-    fix a t assume "?F t"
-    assume "a : domino" hence "?F a" by (rule domino_finite)
-    thus "?F (a Un t)" by (rule finite_UnI)
-  qed
+  assumes "t : tiling domino"  (is "t : ?T")
+  shows "finite t"  (is "?F t")
+  using `t : ?T`
+proof induct
+  show "?F {}" by (rule Finites.emptyI)
+  fix a t assume "?F t"
+  assume "a : domino" then have "?F a" by (rule domino_finite)
+  then show "?F (a Un t)" by (rule finite_UnI)
 qed
 
 lemma tiling_domino_01:
-  "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
-  (is "t : ?T ==> _")
-proof -
-  assume "t : ?T"
-  thus ?thesis
-  proof induct
-    case empty
-    show ?case by (simp add: evnodd_def)
-  next
-    case (Un a t)
-    let ?e = evnodd
-    have hyp: "card (?e t 0) = card (?e t 1)" .
-    have at: "a <= - t" .
-    have card_suc:
-      "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
+  assumes "t : tiling domino"  (is "t : ?T")
+  shows "card (evnodd t 0) = card (evnodd t 1)"
+  using `t : ?T`
+proof induct
+  case empty
+  show ?case by (simp add: evnodd_def)
+next
+  case (Un a t)
+  let ?e = evnodd
+  note hyp = `card (?e t 0) = card (?e t 1)`
+    and at = `a <= - t`
+  have card_suc:
+    "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
+  proof -
+    fix b :: nat assume "b < 2"
+    have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
+    also obtain i j where e: "?e a b = {(i, j)}"
     proof -
-      fix b :: nat assume "b < 2"
-      have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
-      also obtain i j where e: "?e a b = {(i, j)}"
-      proof -
-        have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
-        thus ?thesis by (blast intro: that)
-      qed
-      also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
-      also have "card ... = Suc (card (?e t b))"
-      proof (rule card_insert_disjoint)
-        show "finite (?e t b)"
-          by (rule evnodd_finite, rule tiling_domino_finite)
-        from e have "(i, j) : ?e a b" by simp
-        with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
-      qed
-      finally show "?thesis b" .
+      have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
+      then show ?thesis by (blast intro: that)
     qed
-    hence "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
-    also from hyp have "card (?e t 0) = card (?e t 1)" .
-    also from card_suc have "Suc ... = card (?e (a Un t) 1)"
-      by simp
-    finally show ?case .
+    also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
+    also have "card ... = Suc (card (?e t b))"
+    proof (rule card_insert_disjoint)
+      show "finite (?e t b)"
+        by (rule evnodd_finite, rule tiling_domino_finite)
+      from e have "(i, j) : ?e a b" by simp
+      with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
+    qed
+    finally show "?thesis b" .
   qed
+  then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
+  also from hyp have "card (?e t 0) = card (?e t 1)" .
+  also from card_suc have "Suc ... = card (?e (a Un t) 1)"
+    by simp
+  finally show ?case .
 qed
 
 
@@ -289,21 +284,21 @@
           by (rule finite_subset) auto
         show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
       qed
-      thus ?thesis by simp
+      then show ?thesis by simp
     qed
     also have "... < card (?e ?t 0)"
     proof -
       have "(0, 0) : ?e ?t 0" by simp
       with fin have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"
         by (rule card_Diff1_less)
-      thus ?thesis by simp
+      then show ?thesis by simp
     qed
     also from t have "... = card (?e ?t 1)"
       by (rule tiling_domino_01)
     also have "?e ?t 1 = ?e ?t'' 1" by simp
     also from t'' have "card ... = card (?e ?t'' 0)"
       by (rule tiling_domino_01 [symmetric])
-    finally have "... < ..." . thus False ..
+    finally have "... < ..." . then show False ..
   qed
 qed
 
diff -r 1d1cc715a9e5 -r a084aa91f701 src/HOL/Isar_examples/NestedDatatype.thy
--- a/src/HOL/Isar_examples/NestedDatatype.thy	Thu Nov 10 20:57:22 2005 +0100
+++ b/src/HOL/Isar_examples/NestedDatatype.thy	Thu Nov 10 21:14:05 2005 +0100
@@ -1,3 +1,5 @@
+
+(* $Id$ *)
 
 header {* Nested datatypes *}
 
@@ -56,34 +58,29 @@
 subsection {* Alternative induction *}
 
 theorem term_induct' [case_names Var App]:
-  "(!!a. P (Var a)) ==>
-   (!!b ts. list_all P ts ==> P (App b ts)) ==> P t"
-proof -
-  assume var: "!!a. P (Var a)"
-  assume app: "!!b ts. list_all P ts ==> P (App b ts)"
-  show ?thesis
-  proof (induct t)
-    fix a show "P (Var a)" by (rule var)
-  next
-    fix b t ts assume "list_all P ts"
-    thus "P (App b ts)" by (rule app)
-  next
-    show "list_all P []" by simp
-  next
-    fix t ts assume "P t" "list_all P ts"
-    thus "list_all P (t # ts)" by simp
-  qed
+  assumes var: "!!a. P (Var a)"
+    and app: "!!b ts. list_all P ts ==> P (App b ts)"
+  shows "P t"
+proof (induct t)
+  fix a show "P (Var a)" by (rule var)
+next
+  fix b t ts assume "list_all P ts"
+  thus "P (App b ts)" by (rule app)
+next
+  show "list_all P []" by simp
+next
+  fix t ts assume "P t" "list_all P ts"
+  thus "list_all P (t # ts)" by simp
 qed
 
 lemma
   "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
-  (is "?P t")
 proof (induct t rule: term_induct')
   case (Var a)
-  show "?P (Var a)" by (simp add: o_def)
+  show ?case by (simp add: o_def)
 next
   case (App b ts)
-  thus "?P (App b ts)" by (induct ts) simp_all
+  thus ?case by (induct ts) simp_all
 qed
 
 end
diff -r 1d1cc715a9e5 -r a084aa91f701 src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Thu Nov 10 20:57:22 2005 +0100
+++ b/src/HOL/Library/Nested_Environment.thy	Thu Nov 10 21:14:05 2005 +0100
@@ -101,87 +101,82 @@
 *}
 
 theorem lookup_append_none:
-  "!!env. lookup env xs = None ==> lookup env (xs @ ys) = None"
-  (is "PROP ?P xs")
-proof (induct xs)
-  fix env :: "('a, 'b, 'c) env"
-  {
-    assume "lookup env [] = None"
-    hence False by simp
-    thus "lookup env ([] @ ys) = None" ..
+  assumes "lookup env xs = None"
+  shows "lookup env (xs @ ys) = None"
+  using prems
+proof (induct xs fixing: env)
+  case Nil
+  then have False by simp
+  then show ?case ..
+next
+  case (Cons x xs)
+  show ?case
+  proof (cases env)
+    case Val
+    then show ?thesis by simp
   next
-    fix x xs
-    assume hyp: "PROP ?P xs"
-    assume asm: "lookup env (x # xs) = None"
-    show "lookup env ((x # xs) @ ys) = None"
-    proof (cases env)
-      case Val
-      thus ?thesis by simp
+    case (Env b es)
+    show ?thesis
+    proof (cases "es x")
+      case None
+      with Env show ?thesis by simp
     next
-      fix b es assume env: "env = Env b es"
+      case (Some e)
+      note es = `es x = Some e`
       show ?thesis
-      proof (cases "es x")
-        assume "es x = None"
-        with env show ?thesis by simp
+      proof (cases "lookup e xs")
+        case None
+        then have "lookup e (xs @ ys) = None" by (rule Cons.hyps)
+        with Env Some show ?thesis by simp
       next
-        fix e assume es: "es x = Some e"
-        show ?thesis
-        proof (cases "lookup e xs")
-          case None
-          hence "lookup e (xs @ ys) = None" by (rule hyp)
-          with env es show ?thesis by simp
-        next
-          case Some
-          with asm env es have False by simp
-          thus ?thesis ..
-        qed
+        case Some
+        with Env es have False using Cons.prems by simp
+        then show ?thesis ..
       qed
     qed
-  }
+  qed
 qed
 
 theorem lookup_append_some:
-  "!!env e. lookup env xs = Some e ==> lookup env (xs @ ys) = lookup e ys"
-  (is "PROP ?P xs")
-proof (induct xs)
-  fix env e :: "('a, 'b, 'c) env"
-  {
-    assume "lookup env [] = Some e"
-    hence "env = e" by simp
-    thus "lookup env ([] @ ys) = lookup e ys" by simp
+  assumes "lookup env xs = Some e"
+  shows "lookup env (xs @ ys) = lookup e ys"
+  using prems
+proof (induct xs fixing: env e)
+  case Nil
+  then have "env = e" by simp
+  then show "lookup env ([] @ ys) = lookup e ys" by simp
+next
+  case (Cons x xs)
+  note asm = `lookup env (x # xs) = Some e`
+  show "lookup env ((x # xs) @ ys) = lookup e ys"
+  proof (cases env)
+    case (Val a)
+    with asm have False by simp
+    then show ?thesis ..
   next
-    fix x xs
-    assume hyp: "PROP ?P xs"
-    assume asm: "lookup env (x # xs) = Some e"
-    show "lookup env ((x # xs) @ ys) = lookup e ys"
-    proof (cases env)
-      fix a assume "env = Val a"
-      with asm have False by simp
-      thus ?thesis ..
+    case (Env b es)
+    show ?thesis
+    proof (cases "es x")
+      case None
+      with asm Env have False by simp
+      then show ?thesis ..
     next
-      fix b es assume env: "env = Env b es"
+      case (Some e')
+      note es = `es x = Some e'`
       show ?thesis
-      proof (cases "es x")
-        assume "es x = None"
-        with asm env have False by simp
-        thus ?thesis ..
+      proof (cases "lookup e' xs")
+        case None
+        with asm Env es have False by simp
+        then show ?thesis ..
       next
-        fix e' assume es: "es x = Some e'"
-        show ?thesis
-        proof (cases "lookup e' xs")
-          case None
-          with asm env es have False by simp
-          thus ?thesis ..
-        next
-          case Some
-          with asm env es have "lookup e' xs = Some e"
-            by simp
-          hence "lookup e' (xs @ ys) = lookup e ys" by (rule hyp)
-          with env es show ?thesis by simp
-        qed
+        case Some
+        with asm Env es have "lookup e' xs = Some e"
+          by simp
+        then have "lookup e' (xs @ ys) = lookup e ys" by (rule Cons.hyps)
+        with Env es show ?thesis by simp
       qed
     qed
-  }
+  qed
 qed
 
 text {*
@@ -192,13 +187,13 @@
 *}
 
 theorem lookup_some_append:
-  "lookup env (xs @ ys) = Some e ==> \<exists>e. lookup env xs = Some e"
+  assumes "lookup env (xs @ ys) = Some e"
+  shows "\<exists>e. lookup env xs = Some e"
 proof -
-  assume "lookup env (xs @ ys) = Some e"
-  hence "lookup env (xs @ ys) \<noteq> None" by simp
-  hence "lookup env xs \<noteq> None"
+  from prems have "lookup env (xs @ ys) \<noteq> None" by simp
+  then have "lookup env xs \<noteq> None"
     by (rule contrapos_nn) (simp only: lookup_append_none)
-  thus ?thesis by simp
+  then show ?thesis by simp
 qed
 
 text {*
@@ -207,43 +202,40 @@
   at any upper position.
 *}
 
-theorem lookup_some_upper: "!!env e.
-  lookup env (xs @ y # ys) = Some e ==>
-    \<exists>b' es' env'.
-      lookup env xs = Some (Env b' es') \<and>
-      es' y = Some env' \<and>
-      lookup env' ys = Some e"
-  (is "PROP ?P xs" is "!!env e. ?A env e xs ==> ?C env e xs")
-proof (induct xs)
-  fix env e let ?A = "?A env e" and ?C = "?C env e"
-  {
-    assume "?A []"
-    hence "lookup env (y # ys) = Some e" by simp
-    then obtain b' es' env' where
-        env: "env = Env b' es'" and
-        es': "es' y = Some env'" and
-        look': "lookup env' ys = Some e"
-      by (auto simp add: lookup_eq split: option.splits env.splits)
-    from env have "lookup env [] = Some (Env b' es')" by simp
-    with es' look' show "?C []" by blast
-  next
-    fix x xs
-    assume hyp: "PROP ?P xs"
-    assume "?A (x # xs)"
-    then obtain b' es' env' where
-        env: "env = Env b' es'" and
-        es': "es' x = Some env'" and
-        look': "lookup env' (xs @ y # ys) = Some e"
-      by (auto simp add: lookup_eq split: option.splits env.splits)
-    from hyp [OF look'] obtain b'' es'' env'' where
-        upper': "lookup env' xs = Some (Env b'' es'')" and
-        es'': "es'' y = Some env''" and
-        look'': "lookup env'' ys = Some e"
-      by blast
-    from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
-      by simp
-    with es'' look'' show "?C (x # xs)" by blast
-  }
+theorem lookup_some_upper:
+  assumes "lookup env (xs @ y # ys) = Some e"
+  shows "\<exists>b' es' env'.
+    lookup env xs = Some (Env b' es') \<and>
+    es' y = Some env' \<and>
+    lookup env' ys = Some e"
+  using prems
+proof (induct xs fixing: env e)
+  case Nil
+  from Nil.prems have "lookup env (y # ys) = Some e"
+    by simp
+  then obtain b' es' env' where
+      env: "env = Env b' es'" and
+      es': "es' y = Some env'" and
+      look': "lookup env' ys = Some e"
+    by (auto simp add: lookup_eq split: option.splits env.splits)
+  from env have "lookup env [] = Some (Env b' es')" by simp
+  with es' look' show ?case by blast
+next
+  case (Cons x xs)
+  from Cons.prems
+  obtain b' es' env' where
+      env: "env = Env b' es'" and
+      es': "es' x = Some env'" and
+      look': "lookup env' (xs @ y # ys) = Some e"
+    by (auto simp add: lookup_eq split: option.splits env.splits)
+  from Cons.hyps [OF look'] obtain b'' es'' env'' where
+      upper': "lookup env' xs = Some (Env b'' es'')" and
+      es'': "es'' y = Some env''" and
+      look'': "lookup env'' ys = Some e"
+    by blast
+  from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
+    by simp
+  with es'' look'' show ?case by blast
 qed
 
 
@@ -334,47 +326,44 @@
 *}
 
 theorem lookup_update_some:
-  "!!env e. lookup env xs = Some e ==>
-    lookup (update xs (Some env') env) xs = Some env'"
-  (is "PROP ?P xs")
-proof (induct xs)
-  fix env e :: "('a, 'b, 'c) env"
-  {
-    assume "lookup env [] = Some e"
-    hence "env = e" by simp
-    thus "lookup (update [] (Some env') env) [] = Some env'"
-      by simp
+  assumes "lookup env xs = Some e"
+  shows "lookup (update xs (Some env') env) xs = Some env'"
+  using prems
+proof (induct xs fixing: env e)
+  case Nil
+  then have "env = e" by simp
+  then show ?case by simp
+next
+  case (Cons x xs)
+  note hyp = Cons.hyps
+    and asm = `lookup env (x # xs) = Some e`
+  show ?case
+  proof (cases env)
+    case (Val a)
+    with asm have False by simp
+    then show ?thesis ..
   next
-    fix x xs
-    assume hyp: "PROP ?P xs"
-    assume asm: "lookup env (x # xs) = Some e"
-    show "lookup (update (x # xs) (Some env') env) (x # xs) = Some env'"
-    proof (cases env)
-      fix a assume "env = Val a"
-      with asm have False by simp
-      thus ?thesis ..
+    case (Env b es)
+    show ?thesis
+    proof (cases "es x")
+      case None
+      with asm Env have False by simp
+      then show ?thesis ..
     next
-      fix b es assume env: "env = Env b es"
+      case (Some e')
+      note es = `es x = Some e'`
       show ?thesis
-      proof (cases "es x")
-        assume "es x = None"
-        with asm env have False by simp
-        thus ?thesis ..
+      proof (cases xs)
+        case Nil
+        with Env show ?thesis by simp
       next
-        fix e' assume es: "es x = Some e'"
-        show ?thesis
-        proof (cases xs)
-          assume "xs = []"
-          with env show ?thesis by simp
-        next
-          fix x' xs' assume xs: "xs = x' # xs'"
-          from asm env es have "lookup e' xs = Some e" by simp
-          hence "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
-          with env es xs show ?thesis by simp
-        qed
+        case (Cons x' xs')
+        from asm Env es have "lookup e' xs = Some e" by simp
+        then have "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
+        with Env es Cons show ?thesis by simp
       qed
     qed
-  }
+  qed
 qed
 
 text {*
@@ -386,93 +375,90 @@
 *}
 
 theorem update_append_none:
-  "!!env. lookup env xs = None ==> update (xs @ y # ys) opt env = env"
-  (is "PROP ?P xs")
-proof (induct xs)
-  fix env :: "('a, 'b, 'c) env"
-  {
-    assume "lookup env [] = None"
-    hence False by simp
-    thus "update ([] @ y # ys) opt env = env" ..
+  assumes "lookup env xs = None"
+  shows "update (xs @ y # ys) opt env = env"
+  using prems
+proof (induct xs fixing: env)
+  case Nil
+  then have False by simp
+  then show ?case ..
+next
+  case (Cons x xs)
+  note hyp = Cons.hyps
+    and asm = `lookup env (x # xs) = None`
+  show "update ((x # xs) @ y # ys) opt env = env"
+  proof (cases env)
+    case (Val a)
+    then show ?thesis by simp
   next
-    fix x xs
-    assume hyp: "PROP ?P xs"
-    assume asm: "lookup env (x # xs) = None"
-    show "update ((x # xs) @ y # ys) opt env = env"
-    proof (cases env)
-      fix a assume "env = Val a"
-      thus ?thesis by simp
-    next
-      fix b es assume env: "env = Env b es"
+    case (Env b es)
+    show ?thesis
+    proof (cases "es x")
+      case None
+      note es = `es x = None`
       show ?thesis
-      proof (cases "es x")
-        assume es: "es x = None"
-        show ?thesis
-          by (cases xs) (simp_all add: es env fun_upd_idem_iff)
+        by (cases xs) (simp_all add: es Env fun_upd_idem_iff)
+    next
+      case (Some e)
+      note es = `es x = Some e`
+      show ?thesis
+      proof (cases xs)
+        case Nil
+        with asm Env Some have False by simp
+        then show ?thesis ..
       next
-        fix e assume es: "es x = Some e"
-        show ?thesis
-        proof (cases xs)
-          assume "xs = []"
-          with asm env es have False by simp
-          thus ?thesis ..
-        next
-          fix x' xs' assume xs: "xs = x' # xs'"
-          from asm env es have "lookup e xs = None" by simp
-          hence "update (xs @ y # ys) opt e = e" by (rule hyp)
-          with env es xs show "update ((x # xs) @ y # ys) opt env = env"
-            by (simp add: fun_upd_idem_iff)
-        qed
+        case (Cons x' xs')
+        from asm Env es have "lookup e xs = None" by simp
+        then have "update (xs @ y # ys) opt e = e" by (rule hyp)
+        with Env es Cons show "update ((x # xs) @ y # ys) opt env = env"
+          by (simp add: fun_upd_idem_iff)
       qed
     qed
-  }
+  qed
 qed
 
 theorem update_append_some:
-  "!!env e. lookup env xs = Some e ==>
-    lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
-  (is "PROP ?P xs")
-proof (induct xs)
-  fix env e :: "('a, 'b, 'c) env"
-  {
-    assume "lookup env [] = Some e"
-    hence "env = e" by simp
-    thus "lookup (update ([] @ y # ys) opt env) [] = Some (update (y # ys) opt e)"
-      by simp
+  assumes "lookup env xs = Some e"
+  shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
+  using prems
+proof (induct xs fixing: env e)
+  case Nil
+  then have "env = e" by simp
+  then show ?case by simp
+next
+  case (Cons x xs)
+  note hyp = Cons.hyps
+    and asm = `lookup env (x # xs) = Some e`
+  show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) =
+      Some (update (y # ys) opt e)"
+  proof (cases env)
+    case (Val a)
+    with asm have False by simp
+    then show ?thesis ..
   next
-    fix x xs
-    assume hyp: "PROP ?P xs"
-    assume asm: "lookup env (x # xs) = Some e"
-    show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs)
-      = Some (update (y # ys) opt e)"
-    proof (cases env)
-      fix a assume "env = Val a"
-      with asm have False by simp
-      thus ?thesis ..
+    case (Env b es)
+    show ?thesis
+    proof (cases "es x")
+      case None
+      with asm Env have False by simp
+      then show ?thesis ..
     next
-      fix b es assume env: "env = Env b es"
+      case (Some e')
+      note es = `es x = Some e'`
       show ?thesis
-      proof (cases "es x")
-        assume "es x = None"
-        with asm env have False by simp
-        thus ?thesis ..
+      proof (cases xs)
+        case Nil
+        with asm Env es have "e = e'" by simp
+        with Env es Nil show ?thesis by simp
       next
-        fix e' assume es: "es x = Some e'"
-        show ?thesis
-        proof (cases xs)
-          assume xs: "xs = []"
-          from asm env es xs have "e = e'" by simp
-          with env es xs show ?thesis by simp
-        next
-          fix x' xs' assume xs: "xs = x' # xs'"
-          from asm env es have "lookup e' xs = Some e" by simp
-          hence "lookup (update (xs @ y # ys) opt e') xs =
-            Some (update (y # ys) opt e)" by (rule hyp)
-          with env es xs show ?thesis by simp
-        qed
+        case (Cons x' xs')
+        from asm Env es have "lookup e' xs = Some e" by simp
+        then have "lookup (update (xs @ y # ys) opt e') xs =
+          Some (update (y # ys) opt e)" by (rule hyp)
+        with Env es Cons show ?thesis by simp
       qed
     qed
-  }
+  qed
 qed
 
 text {*
@@ -483,63 +469,58 @@
 *}
 
 theorem lookup_update_other:
-  "!!env. y \<noteq> (z::'c) ==> lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
+  assumes neq: "y \<noteq> (z::'c)"
+  shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
     lookup env (xs @ y # ys)"
-  (is "PROP ?P xs")
-proof (induct xs)
-  fix env :: "('a, 'b, 'c) env"
-  assume neq: "y \<noteq> z"
-  {
-    show "lookup (update ([] @ z # zs) opt env) ([] @ y # ys) =
-      lookup env ([] @ y # ys)"
-    proof (cases env)
-      case Val
-      thus ?thesis by simp
+proof (induct xs fixing: env)
+  case Nil
+  show ?case
+  proof (cases env)
+    case Val
+    then show ?thesis by simp
+  next
+    case Env
+    show ?thesis
+    proof (cases zs)
+      case Nil
+      with neq Env show ?thesis by simp
     next
-      case Env
+      case Cons
+      with neq Env show ?thesis by simp
+    qed
+  qed
+next
+  case (Cons x xs)
+  note hyp = Cons.hyps
+  show ?case
+  proof (cases env)
+    case Val
+    then show ?thesis by simp
+  next
+    case (Env y es)
+    show ?thesis
+    proof (cases xs)
+      case Nil
       show ?thesis
-      proof (cases zs)
-        case Nil
-        with neq Env show ?thesis by simp
+      proof (cases "es x")
+        case None
+        with Env Nil show ?thesis by simp
       next
-        case Cons
-        with neq Env show ?thesis by simp
+        case Some
+        with neq hyp and Env Nil show ?thesis by simp
+      qed
+    next
+      case (Cons x' xs')
+      show ?thesis
+      proof (cases "es x")
+        case None
+        with Env Cons show ?thesis by simp
+      next
+        case Some
+        with neq hyp and Env Cons show ?thesis by simp
       qed
     qed
-  next
-    fix x xs
-    assume hyp: "PROP ?P xs"
-    show "lookup (update ((x # xs) @ z # zs) opt env) ((x # xs) @ y # ys) =
-      lookup env ((x # xs) @ y # ys)"
-    proof (cases env)
-      case Val
-      thus ?thesis by simp
-    next
-      fix y es assume env: "env = Env y es"
-      show ?thesis
-      proof (cases xs)
-        assume xs: "xs = []"
-        show ?thesis
-        proof (cases "es x")
-          case None
-          with env xs show ?thesis by simp
-        next
-          case Some
-          with hyp env xs and neq show ?thesis by simp
-        qed
-      next
-        fix x' xs' assume xs: "xs = x' # xs'"
-        show ?thesis
-        proof (cases "es x")
-          case None
-          with env xs show ?thesis by simp
-        next
-          case Some
-          with hyp env xs neq show ?thesis by simp
-        qed
-      qed
-    qed
-  }
+  qed
 qed
 
 end