tuned proofs;
authorwenzelm
Thu Nov 10 21:14:05 2005 +0100 (2005-11-10)
changeset 18153a084aa91f701
parent 18152 1d1cc715a9e5
child 18154 0c05abaf6244
tuned proofs;
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/Isar_examples/Fibonacci.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/NestedDatatype.thy
src/HOL/Library/Nested_Environment.thy
     1.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Thu Nov 10 20:57:22 2005 +0100
     1.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Thu Nov 10 21:14:05 2005 +0100
     1.3 @@ -112,29 +112,32 @@
     1.4  *}
     1.5  
     1.6  lemma exec_append:
     1.7 -  "ALL stack. exec (xs @ ys) stack env =
     1.8 -    exec ys (exec xs stack env) env" (is "?P xs")
     1.9 -proof (induct xs)
    1.10 -  show "?P []" by simp
    1.11 +  "exec (xs @ ys) stack env =
    1.12 +    exec ys (exec xs stack env) env"
    1.13 +proof (induct xs fixing: stack)
    1.14 +  case Nil
    1.15 +  show ?case by simp
    1.16  next
    1.17 -  fix x xs assume hyp: "?P xs"
    1.18 -  show "?P (x # xs)"
    1.19 +  case (Cons x xs)
    1.20 +  show ?case
    1.21    proof (induct x)
    1.22 -    from hyp show "!!val. ?P (Const val # xs)" by simp
    1.23 -    from hyp show "!!adr. ?P (Load adr # xs)" by simp
    1.24 -    from hyp show "!!fun. ?P (Apply fun # xs)" by simp
    1.25 +    case Const show ?case by simp
    1.26 +  next
    1.27 +    case Load show ?case by simp
    1.28 +  next
    1.29 +    case Apply show ?case by simp
    1.30    qed
    1.31  qed
    1.32  
    1.33  theorem correctness: "execute (compile e) env = eval e env"
    1.34  proof -
    1.35 -  have "ALL stack. exec (compile e) stack env =
    1.36 -    eval e env # stack" (is "?P e")
    1.37 +  have "!!stack. exec (compile e) stack env = eval e env # stack"
    1.38    proof (induct e)
    1.39 -    show "!!adr. ?P (Variable adr)" by simp
    1.40 -    show "!!val. ?P (Constant val)" by simp
    1.41 -    show "!!fun e1 e2. ?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2)"
    1.42 -      by (simp add: exec_append)
    1.43 +    case Variable show ?case by simp
    1.44 +  next
    1.45 +    case Constant show ?case by simp
    1.46 +  next
    1.47 +    case Binop then show ?case by (simp add: exec_append)
    1.48    qed
    1.49    thus ?thesis by (simp add: execute_def)
    1.50  qed
    1.51 @@ -149,98 +152,75 @@
    1.52  *}
    1.53  
    1.54  lemma exec_append':
    1.55 -  "ALL stack. exec (xs @ ys) stack env
    1.56 -    = exec ys (exec xs stack env) env" (is "?P xs")
    1.57 -proof (induct xs)
    1.58 -  show "?P []" (is "ALL s. ?Q s")
    1.59 -  proof
    1.60 -    fix s have "exec ([] @ ys) s env = exec ys s env" by simp
    1.61 -    also have "... = exec ys (exec [] s env) env" by simp
    1.62 -    finally show "?Q s" .
    1.63 -  qed
    1.64 -  fix x xs assume hyp: "?P xs"
    1.65 -  show "?P (x # xs)"
    1.66 +  "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
    1.67 +proof (induct xs fixing: stack)
    1.68 +  case (Nil s)
    1.69 +  have "exec ([] @ ys) s env = exec ys s env" by simp
    1.70 +  also have "... = exec ys (exec [] s env) env" by simp
    1.71 +  finally show ?case .
    1.72 +next
    1.73 +  case (Cons x xs s)
    1.74 +  show ?case
    1.75    proof (induct x)
    1.76 -    fix val
    1.77 -    show "?P (Const val # xs)" (is "ALL s. ?Q s")
    1.78 -    proof
    1.79 -      fix s
    1.80 -      have "exec ((Const val # xs) @ ys) s env =
    1.81 -          exec (Const val # xs @ ys) s env"
    1.82 -        by simp
    1.83 -      also have "... = exec (xs @ ys) (val # s) env" by simp
    1.84 -      also from hyp
    1.85 -        have "... = exec ys (exec xs (val # s) env) env" ..
    1.86 -      also have "... = exec ys (exec (Const val # xs) s env) env"
    1.87 -        by simp
    1.88 -      finally show "?Q s" .
    1.89 -    qed
    1.90 -  next
    1.91 -    fix adr from hyp show "?P (Load adr # xs)" by simp -- {* same as above *}
    1.92 +    case (Const val)
    1.93 +    have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"
    1.94 +      by simp
    1.95 +    also have "... = exec (xs @ ys) (val # s) env" by simp
    1.96 +    also from Cons have "... = exec ys (exec xs (val # s) env) env" .
    1.97 +    also have "... = exec ys (exec (Const val # xs) s env) env" by simp
    1.98 +    finally show ?case .
    1.99    next
   1.100 -    fix fun
   1.101 -    show "?P (Apply fun # xs)" (is "ALL s. ?Q s")
   1.102 -    proof
   1.103 -      fix s
   1.104 -      have "exec ((Apply fun # xs) @ ys) s env =
   1.105 -          exec (Apply fun # xs @ ys) s env"
   1.106 -        by simp
   1.107 -      also have "... =
   1.108 -          exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env"
   1.109 -        by simp
   1.110 -      also from hyp have "... =
   1.111 -        exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env"
   1.112 -        ..
   1.113 -      also have "... = exec ys (exec (Apply fun # xs) s env) env" by simp
   1.114 -      finally show "?Q s" .
   1.115 -    qed
   1.116 +    case (Load adr)
   1.117 +    from Cons show ?case by simp -- {* same as above *}
   1.118 +  next
   1.119 +    case (Apply fun)
   1.120 +    have "exec ((Apply fun # xs) @ ys) s env =
   1.121 +        exec (Apply fun # xs @ ys) s env" by simp
   1.122 +    also have "... =
   1.123 +        exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
   1.124 +    also from Cons have "... =
   1.125 +        exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env" .
   1.126 +    also have "... = exec ys (exec (Apply fun # xs) s env) env" by simp
   1.127 +    finally show ?case .
   1.128    qed
   1.129  qed
   1.130  
   1.131  theorem correctness': "execute (compile e) env = eval e env"
   1.132  proof -
   1.133    have exec_compile:
   1.134 -    "ALL stack. exec (compile e) stack env = eval e env # stack"
   1.135 -    (is "?P e")
   1.136 +    "!!stack. exec (compile e) stack env = eval e env # stack"
   1.137    proof (induct e)
   1.138 -    fix adr show "?P (Variable adr)" (is "ALL s. ?Q s")
   1.139 -    proof
   1.140 -      fix s
   1.141 -      have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
   1.142 -        by simp
   1.143 -      also have "... = env adr # s" by simp
   1.144 -      also have "env adr = eval (Variable adr) env" by simp
   1.145 -      finally show "?Q s" .
   1.146 -    qed
   1.147 +    case (Variable adr s)
   1.148 +    have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
   1.149 +      by simp
   1.150 +    also have "... = env adr # s" by simp
   1.151 +    also have "env adr = eval (Variable adr) env" by simp
   1.152 +    finally show ?case .
   1.153    next
   1.154 -    fix val show "?P (Constant val)" by simp -- {* same as above *}
   1.155 +    case (Constant val s)
   1.156 +    show ?case by simp -- {* same as above *}
   1.157    next
   1.158 -    fix fun e1 e2 assume hyp1: "?P e1" and hyp2: "?P e2"
   1.159 -    show "?P (Binop fun e1 e2)" (is "ALL s. ?Q s")
   1.160 -    proof
   1.161 -      fix s have "exec (compile (Binop fun e1 e2)) s env
   1.162 -        = exec (compile e2 @ compile e1 @ [Apply fun]) s env" by simp
   1.163 -      also have "... = exec [Apply fun]
   1.164 -          (exec (compile e1) (exec (compile e2) s env) env) env"
   1.165 -        by (simp only: exec_append)
   1.166 -      also from hyp2
   1.167 -        have "exec (compile e2) s env = eval e2 env # s" ..
   1.168 -      also from hyp1
   1.169 -        have "exec (compile e1) ... env = eval e1 env # ..." ..
   1.170 -      also have "exec [Apply fun] ... env =
   1.171 +    case (Binop fun e1 e2 s)
   1.172 +    have "exec (compile (Binop fun e1 e2)) s env =
   1.173 +        exec (compile e2 @ compile e1 @ [Apply fun]) s env" by simp
   1.174 +    also have "... = exec [Apply fun]
   1.175 +        (exec (compile e1) (exec (compile e2) s env) env) env"
   1.176 +      by (simp only: exec_append)
   1.177 +    also have "exec (compile e2) s env = eval e2 env # s" by fact
   1.178 +    also have "exec (compile e1) ... env = eval e1 env # ..." by fact
   1.179 +    also have "exec [Apply fun] ... env =
   1.180          fun (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
   1.181 -      also have "... = fun (eval e1 env) (eval e2 env) # s" by simp
   1.182 -      also have "fun (eval e1 env) (eval e2 env) =
   1.183 -          eval (Binop fun e1 e2) env"
   1.184 -        by simp
   1.185 -      finally show "?Q s" .
   1.186 -    qed
   1.187 +    also have "... = fun (eval e1 env) (eval e2 env) # s" by simp
   1.188 +    also have "fun (eval e1 env) (eval e2 env) =
   1.189 +        eval (Binop fun e1 e2) env"
   1.190 +      by simp
   1.191 +    finally show ?case .
   1.192    qed
   1.193  
   1.194    have "execute (compile e) env = hd (exec (compile e) [] env)"
   1.195      by (simp add: execute_def)
   1.196    also from exec_compile
   1.197 -    have "exec (compile e) [] env = [eval e env]" ..
   1.198 +    have "exec (compile e) [] env = [eval e env]" .
   1.199    also have "hd ... = eval e env" by simp
   1.200    finally show ?thesis .
   1.201  qed
     2.1 --- a/src/HOL/Isar_examples/Fibonacci.thy	Thu Nov 10 20:57:22 2005 +0100
     2.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy	Thu Nov 10 21:14:05 2005 +0100
     2.3 @@ -28,20 +28,19 @@
     2.4  
     2.5  consts fib :: "nat => nat"
     2.6  recdef fib less_than
     2.7 - "fib 0 = 0"
     2.8 - "fib (Suc 0) = 1"
     2.9 - "fib (Suc (Suc x)) = fib x + fib (Suc x)"
    2.10 +  "fib 0 = 0"
    2.11 +  "fib (Suc 0) = 1"
    2.12 +  "fib (Suc (Suc x)) = fib x + fib (Suc x)"
    2.13  
    2.14  lemma [simp]: "0 < fib (Suc n)"
    2.15 -  by (induct n rule: fib.induct) (simp+)
    2.16 +  by (induct n rule: fib.induct) simp_all
    2.17  
    2.18  
    2.19  text {* Alternative induction rule. *}
    2.20  
    2.21  theorem fib_induct:
    2.22      "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
    2.23 -  by (induct rule: fib.induct, simp+)
    2.24 -
    2.25 +  by (induct rule: fib.induct) simp_all
    2.26  
    2.27  
    2.28  subsection {* Fib and gcd commute *}
    2.29 @@ -88,19 +87,19 @@
    2.30  lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
    2.31  proof -
    2.32    assume "0 < n"
    2.33 -  hence "gcd (n * k + m, n) = gcd (n, m mod n)"
    2.34 +  then have "gcd (n * k + m, n) = gcd (n, m mod n)"
    2.35      by (simp add: gcd_non_0 add_commute)
    2.36 -  also have "... = gcd (m, n)" by (simp! add: gcd_non_0)
    2.37 +  also from `0 < n` have "... = gcd (m, n)" by (simp add: gcd_non_0)
    2.38    finally show ?thesis .
    2.39  qed
    2.40  
    2.41  lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
    2.42  proof (cases m)
    2.43 -  assume "m = 0"
    2.44 -  thus ?thesis by simp
    2.45 +  case 0
    2.46 +  then show ?thesis by simp
    2.47  next
    2.48 -  fix k assume "m = Suc k"
    2.49 -  hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
    2.50 +  case (Suc k)
    2.51 +  then have "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
    2.52      by (simp add: gcd_commute)
    2.53    also have "fib (n + k + 1)
    2.54      = fib (k + 1) * fib (n + 1) + fib k * fib n"
    2.55 @@ -110,49 +109,44 @@
    2.56    also have "... = gcd (fib n, fib (k + 1))"
    2.57      by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
    2.58    also have "... = gcd (fib m, fib n)"
    2.59 -    by (simp! add: gcd_commute)
    2.60 +    using Suc by (simp add: gcd_commute)
    2.61    finally show ?thesis .
    2.62  qed
    2.63  
    2.64  lemma gcd_fib_diff:
    2.65 -  "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
    2.66 +  assumes "m <= n"
    2.67 +  shows "gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
    2.68  proof -
    2.69 -  assume "m <= n"
    2.70    have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"
    2.71      by (simp add: gcd_fib_add)
    2.72 -  also have "n - m + m = n" by (simp!)
    2.73 +  also from `m <= n` have "n - m + m = n" by simp
    2.74    finally show ?thesis .
    2.75  qed
    2.76  
    2.77  lemma gcd_fib_mod:
    2.78 -  "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
    2.79 -proof -
    2.80 -  assume m: "0 < m"
    2.81 -  show ?thesis
    2.82 -  proof (induct n rule: nat_less_induct)
    2.83 -    fix n
    2.84 -    assume hyp: "ALL ma. ma < n
    2.85 -      --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
    2.86 -    show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
    2.87 -    proof -
    2.88 -      have "n mod m = (if n < m then n else (n - m) mod m)"
    2.89 -	by (rule mod_if)
    2.90 -      also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
    2.91 -      proof cases
    2.92 -	assume "n < m" thus ?thesis by simp
    2.93 -      next
    2.94 -	assume not_lt: "~ n < m" hence le: "m <= n" by simp
    2.95 -	have "n - m < n" by (simp!)
    2.96 -	with hyp have "gcd (fib m, fib ((n - m) mod m))
    2.97 -	  = gcd (fib m, fib (n - m))" by simp
    2.98 -	also from le have "... = gcd (fib m, fib n)"
    2.99 -	  by (rule gcd_fib_diff)
   2.100 -	finally have "gcd (fib m, fib ((n - m) mod m)) =
   2.101 -	  gcd (fib m, fib n)" .
   2.102 -	with not_lt show ?thesis by simp
   2.103 -      qed
   2.104 -      finally show ?thesis .
   2.105 +  assumes m: "0 < m"
   2.106 +  shows "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
   2.107 +proof (induct n rule: nat_less_induct)
   2.108 +  case (1 n) note hyp = this
   2.109 +  show ?case
   2.110 +  proof -
   2.111 +    have "n mod m = (if n < m then n else (n - m) mod m)"
   2.112 +      by (rule mod_if)
   2.113 +    also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
   2.114 +    proof (cases "n < m")
   2.115 +      case True then show ?thesis by simp
   2.116 +    next
   2.117 +      case False then have "m <= n" by simp
   2.118 +      from m and False have "n - m < n" by simp
   2.119 +      with hyp have "gcd (fib m, fib ((n - m) mod m))
   2.120 +        = gcd (fib m, fib (n - m))" by simp
   2.121 +      also have "... = gcd (fib m, fib n)"
   2.122 +        using `m <= n` by (rule gcd_fib_diff)
   2.123 +      finally have "gcd (fib m, fib ((n - m) mod m)) =
   2.124 +        gcd (fib m, fib n)" .
   2.125 +      with False show ?thesis by simp
   2.126      qed
   2.127 +    finally show ?thesis .
   2.128    qed
   2.129  qed
   2.130  
   2.131 @@ -161,7 +155,7 @@
   2.132  proof (induct m n rule: gcd_induct)
   2.133    fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
   2.134    fix n :: nat assume n: "0 < n"
   2.135 -  hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
   2.136 +  then have "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
   2.137    also assume hyp: "fib ... = gcd (fib n, fib (m mod n))"
   2.138    also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod)
   2.139    also have "... = gcd (fib m, fib n)" by (rule gcd_commute)
     3.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Nov 10 20:57:22 2005 +0100
     3.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Nov 10 21:14:05 2005 +0100
     3.3 @@ -29,16 +29,15 @@
     3.4  text "The union of two disjoint tilings is a tiling."
     3.5  
     3.6  lemma tiling_Un:
     3.7 -  "t : tiling A ==> u : tiling A ==> t Int u = {}
     3.8 -    ==> t Un u : tiling A"
     3.9 +  assumes "t : tiling A" and "u : tiling A" and "t Int u = {}"
    3.10 +  shows "t Un u : tiling A"
    3.11  proof -
    3.12    let ?T = "tiling A"
    3.13 -  assume u: "u : ?T"
    3.14 -  assume "t : ?T"
    3.15 -  thus "t Int u = {} ==> t Un u : ?T" (is "PROP ?P t")
    3.16 +  from `t : ?T` and `t Int u = {}`
    3.17 +  show "t Un u : ?T"
    3.18    proof (induct t)
    3.19      case empty
    3.20 -    with u show "{} Un u : ?T" by simp
    3.21 +    with `u : ?T` show "{} Un u : ?T" by simp
    3.22    next
    3.23      case (Un a t)
    3.24      show "(a Un t) Un u : ?T"
    3.25 @@ -46,11 +45,10 @@
    3.26        have "a Un (t Un u) : ?T"
    3.27        proof (rule tiling.Un)
    3.28          show "a : A" .
    3.29 -	have atu: "(a Un t) Int u = {}" .
    3.30 -	hence "t Int u = {}" by blast
    3.31 -        thus "t Un u: ?T" by (rule Un)
    3.32 -	have "a <= - t" .
    3.33 -	with atu show "a <= - (t Un u)" by blast
    3.34 +        from `(a Un t) Int u = {}` have "t Int u = {}" by blast
    3.35 +        then show "t Un u: ?T" by (rule Un)
    3.36 +        have "a <= - t" .
    3.37 +        with `(a Un t) Int u = {}` show "a <= - (t Un u)" by blast
    3.38        qed
    3.39        also have "a Un (t Un u) = (a Un t) Un u"
    3.40          by (simp only: Un_assoc)
    3.41 @@ -171,13 +169,13 @@
    3.42  qed
    3.43  
    3.44  lemma domino_singleton:
    3.45 -  "d : domino ==> b < 2 ==> EX i j. evnodd d b = {(i, j)}"
    3.46 +  assumes "d : domino" and "b < 2"
    3.47 +  shows "EX i j. evnodd d b = {(i, j)}"
    3.48  proof -
    3.49 -  assume b: "b < 2"
    3.50 -  assume "d : domino"
    3.51 -  thus ?thesis (is "?P d")
    3.52 +  from `d : domino`
    3.53 +  show ?thesis (is "?P d")
    3.54    proof induct
    3.55 -    from b have b_cases: "b = 0 | b = 1" by arith
    3.56 +    from `b < 2` have b_cases: "b = 0 | b = 1" by arith
    3.57      fix i j
    3.58      note [simp] = evnodd_empty evnodd_insert mod_Suc
    3.59      from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
    3.60 @@ -185,10 +183,12 @@
    3.61    qed
    3.62  qed
    3.63  
    3.64 -lemma domino_finite: "d: domino ==> finite d"
    3.65 +lemma domino_finite:
    3.66 +  assumes "d: domino"
    3.67 +  shows "finite d"
    3.68  proof -
    3.69 -  assume "d: domino"
    3.70 -  thus ?thesis
    3.71 +  from `d: domino`
    3.72 +  show ?thesis
    3.73    proof induct
    3.74      fix i j :: nat
    3.75      show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
    3.76 @@ -200,58 +200,53 @@
    3.77  subsection {* Tilings of dominoes *}
    3.78  
    3.79  lemma tiling_domino_finite:
    3.80 -  "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t")
    3.81 -proof -
    3.82 -  assume "t : ?T"
    3.83 -  thus "?F t"
    3.84 -  proof induct
    3.85 -    show "?F {}" by (rule Finites.emptyI)
    3.86 -    fix a t assume "?F t"
    3.87 -    assume "a : domino" hence "?F a" by (rule domino_finite)
    3.88 -    thus "?F (a Un t)" by (rule finite_UnI)
    3.89 -  qed
    3.90 +  assumes "t : tiling domino"  (is "t : ?T")
    3.91 +  shows "finite t"  (is "?F t")
    3.92 +  using `t : ?T`
    3.93 +proof induct
    3.94 +  show "?F {}" by (rule Finites.emptyI)
    3.95 +  fix a t assume "?F t"
    3.96 +  assume "a : domino" then have "?F a" by (rule domino_finite)
    3.97 +  then show "?F (a Un t)" by (rule finite_UnI)
    3.98  qed
    3.99  
   3.100  lemma tiling_domino_01:
   3.101 -  "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
   3.102 -  (is "t : ?T ==> _")
   3.103 -proof -
   3.104 -  assume "t : ?T"
   3.105 -  thus ?thesis
   3.106 -  proof induct
   3.107 -    case empty
   3.108 -    show ?case by (simp add: evnodd_def)
   3.109 -  next
   3.110 -    case (Un a t)
   3.111 -    let ?e = evnodd
   3.112 -    have hyp: "card (?e t 0) = card (?e t 1)" .
   3.113 -    have at: "a <= - t" .
   3.114 -    have card_suc:
   3.115 -      "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
   3.116 +  assumes "t : tiling domino"  (is "t : ?T")
   3.117 +  shows "card (evnodd t 0) = card (evnodd t 1)"
   3.118 +  using `t : ?T`
   3.119 +proof induct
   3.120 +  case empty
   3.121 +  show ?case by (simp add: evnodd_def)
   3.122 +next
   3.123 +  case (Un a t)
   3.124 +  let ?e = evnodd
   3.125 +  note hyp = `card (?e t 0) = card (?e t 1)`
   3.126 +    and at = `a <= - t`
   3.127 +  have card_suc:
   3.128 +    "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
   3.129 +  proof -
   3.130 +    fix b :: nat assume "b < 2"
   3.131 +    have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
   3.132 +    also obtain i j where e: "?e a b = {(i, j)}"
   3.133      proof -
   3.134 -      fix b :: nat assume "b < 2"
   3.135 -      have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
   3.136 -      also obtain i j where e: "?e a b = {(i, j)}"
   3.137 -      proof -
   3.138 -        have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
   3.139 -        thus ?thesis by (blast intro: that)
   3.140 -      qed
   3.141 -      also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
   3.142 -      also have "card ... = Suc (card (?e t b))"
   3.143 -      proof (rule card_insert_disjoint)
   3.144 -        show "finite (?e t b)"
   3.145 -          by (rule evnodd_finite, rule tiling_domino_finite)
   3.146 -        from e have "(i, j) : ?e a b" by simp
   3.147 -        with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
   3.148 -      qed
   3.149 -      finally show "?thesis b" .
   3.150 +      have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
   3.151 +      then show ?thesis by (blast intro: that)
   3.152      qed
   3.153 -    hence "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
   3.154 -    also from hyp have "card (?e t 0) = card (?e t 1)" .
   3.155 -    also from card_suc have "Suc ... = card (?e (a Un t) 1)"
   3.156 -      by simp
   3.157 -    finally show ?case .
   3.158 +    also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
   3.159 +    also have "card ... = Suc (card (?e t b))"
   3.160 +    proof (rule card_insert_disjoint)
   3.161 +      show "finite (?e t b)"
   3.162 +        by (rule evnodd_finite, rule tiling_domino_finite)
   3.163 +      from e have "(i, j) : ?e a b" by simp
   3.164 +      with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
   3.165 +    qed
   3.166 +    finally show "?thesis b" .
   3.167    qed
   3.168 +  then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
   3.169 +  also from hyp have "card (?e t 0) = card (?e t 1)" .
   3.170 +  also from card_suc have "Suc ... = card (?e (a Un t) 1)"
   3.171 +    by simp
   3.172 +  finally show ?case .
   3.173  qed
   3.174  
   3.175  
   3.176 @@ -289,21 +284,21 @@
   3.177            by (rule finite_subset) auto
   3.178          show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
   3.179        qed
   3.180 -      thus ?thesis by simp
   3.181 +      then show ?thesis by simp
   3.182      qed
   3.183      also have "... < card (?e ?t 0)"
   3.184      proof -
   3.185        have "(0, 0) : ?e ?t 0" by simp
   3.186        with fin have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"
   3.187          by (rule card_Diff1_less)
   3.188 -      thus ?thesis by simp
   3.189 +      then show ?thesis by simp
   3.190      qed
   3.191      also from t have "... = card (?e ?t 1)"
   3.192        by (rule tiling_domino_01)
   3.193      also have "?e ?t 1 = ?e ?t'' 1" by simp
   3.194      also from t'' have "card ... = card (?e ?t'' 0)"
   3.195        by (rule tiling_domino_01 [symmetric])
   3.196 -    finally have "... < ..." . thus False ..
   3.197 +    finally have "... < ..." . then show False ..
   3.198    qed
   3.199  qed
   3.200  
     4.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Thu Nov 10 20:57:22 2005 +0100
     4.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Thu Nov 10 21:14:05 2005 +0100
     4.3 @@ -1,3 +1,5 @@
     4.4 +
     4.5 +(* $Id$ *)
     4.6  
     4.7  header {* Nested datatypes *}
     4.8  
     4.9 @@ -56,34 +58,29 @@
    4.10  subsection {* Alternative induction *}
    4.11  
    4.12  theorem term_induct' [case_names Var App]:
    4.13 -  "(!!a. P (Var a)) ==>
    4.14 -   (!!b ts. list_all P ts ==> P (App b ts)) ==> P t"
    4.15 -proof -
    4.16 -  assume var: "!!a. P (Var a)"
    4.17 -  assume app: "!!b ts. list_all P ts ==> P (App b ts)"
    4.18 -  show ?thesis
    4.19 -  proof (induct t)
    4.20 -    fix a show "P (Var a)" by (rule var)
    4.21 -  next
    4.22 -    fix b t ts assume "list_all P ts"
    4.23 -    thus "P (App b ts)" by (rule app)
    4.24 -  next
    4.25 -    show "list_all P []" by simp
    4.26 -  next
    4.27 -    fix t ts assume "P t" "list_all P ts"
    4.28 -    thus "list_all P (t # ts)" by simp
    4.29 -  qed
    4.30 +  assumes var: "!!a. P (Var a)"
    4.31 +    and app: "!!b ts. list_all P ts ==> P (App b ts)"
    4.32 +  shows "P t"
    4.33 +proof (induct t)
    4.34 +  fix a show "P (Var a)" by (rule var)
    4.35 +next
    4.36 +  fix b t ts assume "list_all P ts"
    4.37 +  thus "P (App b ts)" by (rule app)
    4.38 +next
    4.39 +  show "list_all P []" by simp
    4.40 +next
    4.41 +  fix t ts assume "P t" "list_all P ts"
    4.42 +  thus "list_all P (t # ts)" by simp
    4.43  qed
    4.44  
    4.45  lemma
    4.46    "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
    4.47 -  (is "?P t")
    4.48  proof (induct t rule: term_induct')
    4.49    case (Var a)
    4.50 -  show "?P (Var a)" by (simp add: o_def)
    4.51 +  show ?case by (simp add: o_def)
    4.52  next
    4.53    case (App b ts)
    4.54 -  thus "?P (App b ts)" by (induct ts) simp_all
    4.55 +  thus ?case by (induct ts) simp_all
    4.56  qed
    4.57  
    4.58  end
     5.1 --- a/src/HOL/Library/Nested_Environment.thy	Thu Nov 10 20:57:22 2005 +0100
     5.2 +++ b/src/HOL/Library/Nested_Environment.thy	Thu Nov 10 21:14:05 2005 +0100
     5.3 @@ -101,87 +101,82 @@
     5.4  *}
     5.5  
     5.6  theorem lookup_append_none:
     5.7 -  "!!env. lookup env xs = None ==> lookup env (xs @ ys) = None"
     5.8 -  (is "PROP ?P xs")
     5.9 -proof (induct xs)
    5.10 -  fix env :: "('a, 'b, 'c) env"
    5.11 -  {
    5.12 -    assume "lookup env [] = None"
    5.13 -    hence False by simp
    5.14 -    thus "lookup env ([] @ ys) = None" ..
    5.15 +  assumes "lookup env xs = None"
    5.16 +  shows "lookup env (xs @ ys) = None"
    5.17 +  using prems
    5.18 +proof (induct xs fixing: env)
    5.19 +  case Nil
    5.20 +  then have False by simp
    5.21 +  then show ?case ..
    5.22 +next
    5.23 +  case (Cons x xs)
    5.24 +  show ?case
    5.25 +  proof (cases env)
    5.26 +    case Val
    5.27 +    then show ?thesis by simp
    5.28    next
    5.29 -    fix x xs
    5.30 -    assume hyp: "PROP ?P xs"
    5.31 -    assume asm: "lookup env (x # xs) = None"
    5.32 -    show "lookup env ((x # xs) @ ys) = None"
    5.33 -    proof (cases env)
    5.34 -      case Val
    5.35 -      thus ?thesis by simp
    5.36 +    case (Env b es)
    5.37 +    show ?thesis
    5.38 +    proof (cases "es x")
    5.39 +      case None
    5.40 +      with Env show ?thesis by simp
    5.41      next
    5.42 -      fix b es assume env: "env = Env b es"
    5.43 +      case (Some e)
    5.44 +      note es = `es x = Some e`
    5.45        show ?thesis
    5.46 -      proof (cases "es x")
    5.47 -        assume "es x = None"
    5.48 -        with env show ?thesis by simp
    5.49 +      proof (cases "lookup e xs")
    5.50 +        case None
    5.51 +        then have "lookup e (xs @ ys) = None" by (rule Cons.hyps)
    5.52 +        with Env Some show ?thesis by simp
    5.53        next
    5.54 -        fix e assume es: "es x = Some e"
    5.55 -        show ?thesis
    5.56 -        proof (cases "lookup e xs")
    5.57 -          case None
    5.58 -          hence "lookup e (xs @ ys) = None" by (rule hyp)
    5.59 -          with env es show ?thesis by simp
    5.60 -        next
    5.61 -          case Some
    5.62 -          with asm env es have False by simp
    5.63 -          thus ?thesis ..
    5.64 -        qed
    5.65 +        case Some
    5.66 +        with Env es have False using Cons.prems by simp
    5.67 +        then show ?thesis ..
    5.68        qed
    5.69      qed
    5.70 -  }
    5.71 +  qed
    5.72  qed
    5.73  
    5.74  theorem lookup_append_some:
    5.75 -  "!!env e. lookup env xs = Some e ==> lookup env (xs @ ys) = lookup e ys"
    5.76 -  (is "PROP ?P xs")
    5.77 -proof (induct xs)
    5.78 -  fix env e :: "('a, 'b, 'c) env"
    5.79 -  {
    5.80 -    assume "lookup env [] = Some e"
    5.81 -    hence "env = e" by simp
    5.82 -    thus "lookup env ([] @ ys) = lookup e ys" by simp
    5.83 +  assumes "lookup env xs = Some e"
    5.84 +  shows "lookup env (xs @ ys) = lookup e ys"
    5.85 +  using prems
    5.86 +proof (induct xs fixing: env e)
    5.87 +  case Nil
    5.88 +  then have "env = e" by simp
    5.89 +  then show "lookup env ([] @ ys) = lookup e ys" by simp
    5.90 +next
    5.91 +  case (Cons x xs)
    5.92 +  note asm = `lookup env (x # xs) = Some e`
    5.93 +  show "lookup env ((x # xs) @ ys) = lookup e ys"
    5.94 +  proof (cases env)
    5.95 +    case (Val a)
    5.96 +    with asm have False by simp
    5.97 +    then show ?thesis ..
    5.98    next
    5.99 -    fix x xs
   5.100 -    assume hyp: "PROP ?P xs"
   5.101 -    assume asm: "lookup env (x # xs) = Some e"
   5.102 -    show "lookup env ((x # xs) @ ys) = lookup e ys"
   5.103 -    proof (cases env)
   5.104 -      fix a assume "env = Val a"
   5.105 -      with asm have False by simp
   5.106 -      thus ?thesis ..
   5.107 +    case (Env b es)
   5.108 +    show ?thesis
   5.109 +    proof (cases "es x")
   5.110 +      case None
   5.111 +      with asm Env have False by simp
   5.112 +      then show ?thesis ..
   5.113      next
   5.114 -      fix b es assume env: "env = Env b es"
   5.115 +      case (Some e')
   5.116 +      note es = `es x = Some e'`
   5.117        show ?thesis
   5.118 -      proof (cases "es x")
   5.119 -        assume "es x = None"
   5.120 -        with asm env have False by simp
   5.121 -        thus ?thesis ..
   5.122 +      proof (cases "lookup e' xs")
   5.123 +        case None
   5.124 +        with asm Env es have False by simp
   5.125 +        then show ?thesis ..
   5.126        next
   5.127 -        fix e' assume es: "es x = Some e'"
   5.128 -        show ?thesis
   5.129 -        proof (cases "lookup e' xs")
   5.130 -          case None
   5.131 -          with asm env es have False by simp
   5.132 -          thus ?thesis ..
   5.133 -        next
   5.134 -          case Some
   5.135 -          with asm env es have "lookup e' xs = Some e"
   5.136 -            by simp
   5.137 -          hence "lookup e' (xs @ ys) = lookup e ys" by (rule hyp)
   5.138 -          with env es show ?thesis by simp
   5.139 -        qed
   5.140 +        case Some
   5.141 +        with asm Env es have "lookup e' xs = Some e"
   5.142 +          by simp
   5.143 +        then have "lookup e' (xs @ ys) = lookup e ys" by (rule Cons.hyps)
   5.144 +        with Env es show ?thesis by simp
   5.145        qed
   5.146      qed
   5.147 -  }
   5.148 +  qed
   5.149  qed
   5.150  
   5.151  text {*
   5.152 @@ -192,13 +187,13 @@
   5.153  *}
   5.154  
   5.155  theorem lookup_some_append:
   5.156 -  "lookup env (xs @ ys) = Some e ==> \<exists>e. lookup env xs = Some e"
   5.157 +  assumes "lookup env (xs @ ys) = Some e"
   5.158 +  shows "\<exists>e. lookup env xs = Some e"
   5.159  proof -
   5.160 -  assume "lookup env (xs @ ys) = Some e"
   5.161 -  hence "lookup env (xs @ ys) \<noteq> None" by simp
   5.162 -  hence "lookup env xs \<noteq> None"
   5.163 +  from prems have "lookup env (xs @ ys) \<noteq> None" by simp
   5.164 +  then have "lookup env xs \<noteq> None"
   5.165      by (rule contrapos_nn) (simp only: lookup_append_none)
   5.166 -  thus ?thesis by simp
   5.167 +  then show ?thesis by simp
   5.168  qed
   5.169  
   5.170  text {*
   5.171 @@ -207,43 +202,40 @@
   5.172    at any upper position.
   5.173  *}
   5.174  
   5.175 -theorem lookup_some_upper: "!!env e.
   5.176 -  lookup env (xs @ y # ys) = Some e ==>
   5.177 -    \<exists>b' es' env'.
   5.178 -      lookup env xs = Some (Env b' es') \<and>
   5.179 -      es' y = Some env' \<and>
   5.180 -      lookup env' ys = Some e"
   5.181 -  (is "PROP ?P xs" is "!!env e. ?A env e xs ==> ?C env e xs")
   5.182 -proof (induct xs)
   5.183 -  fix env e let ?A = "?A env e" and ?C = "?C env e"
   5.184 -  {
   5.185 -    assume "?A []"
   5.186 -    hence "lookup env (y # ys) = Some e" by simp
   5.187 -    then obtain b' es' env' where
   5.188 -        env: "env = Env b' es'" and
   5.189 -        es': "es' y = Some env'" and
   5.190 -        look': "lookup env' ys = Some e"
   5.191 -      by (auto simp add: lookup_eq split: option.splits env.splits)
   5.192 -    from env have "lookup env [] = Some (Env b' es')" by simp
   5.193 -    with es' look' show "?C []" by blast
   5.194 -  next
   5.195 -    fix x xs
   5.196 -    assume hyp: "PROP ?P xs"
   5.197 -    assume "?A (x # xs)"
   5.198 -    then obtain b' es' env' where
   5.199 -        env: "env = Env b' es'" and
   5.200 -        es': "es' x = Some env'" and
   5.201 -        look': "lookup env' (xs @ y # ys) = Some e"
   5.202 -      by (auto simp add: lookup_eq split: option.splits env.splits)
   5.203 -    from hyp [OF look'] obtain b'' es'' env'' where
   5.204 -        upper': "lookup env' xs = Some (Env b'' es'')" and
   5.205 -        es'': "es'' y = Some env''" and
   5.206 -        look'': "lookup env'' ys = Some e"
   5.207 -      by blast
   5.208 -    from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
   5.209 -      by simp
   5.210 -    with es'' look'' show "?C (x # xs)" by blast
   5.211 -  }
   5.212 +theorem lookup_some_upper:
   5.213 +  assumes "lookup env (xs @ y # ys) = Some e"
   5.214 +  shows "\<exists>b' es' env'.
   5.215 +    lookup env xs = Some (Env b' es') \<and>
   5.216 +    es' y = Some env' \<and>
   5.217 +    lookup env' ys = Some e"
   5.218 +  using prems
   5.219 +proof (induct xs fixing: env e)
   5.220 +  case Nil
   5.221 +  from Nil.prems have "lookup env (y # ys) = Some e"
   5.222 +    by simp
   5.223 +  then obtain b' es' env' where
   5.224 +      env: "env = Env b' es'" and
   5.225 +      es': "es' y = Some env'" and
   5.226 +      look': "lookup env' ys = Some e"
   5.227 +    by (auto simp add: lookup_eq split: option.splits env.splits)
   5.228 +  from env have "lookup env [] = Some (Env b' es')" by simp
   5.229 +  with es' look' show ?case by blast
   5.230 +next
   5.231 +  case (Cons x xs)
   5.232 +  from Cons.prems
   5.233 +  obtain b' es' env' where
   5.234 +      env: "env = Env b' es'" and
   5.235 +      es': "es' x = Some env'" and
   5.236 +      look': "lookup env' (xs @ y # ys) = Some e"
   5.237 +    by (auto simp add: lookup_eq split: option.splits env.splits)
   5.238 +  from Cons.hyps [OF look'] obtain b'' es'' env'' where
   5.239 +      upper': "lookup env' xs = Some (Env b'' es'')" and
   5.240 +      es'': "es'' y = Some env''" and
   5.241 +      look'': "lookup env'' ys = Some e"
   5.242 +    by blast
   5.243 +  from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
   5.244 +    by simp
   5.245 +  with es'' look'' show ?case by blast
   5.246  qed
   5.247  
   5.248  
   5.249 @@ -334,47 +326,44 @@
   5.250  *}
   5.251  
   5.252  theorem lookup_update_some:
   5.253 -  "!!env e. lookup env xs = Some e ==>
   5.254 -    lookup (update xs (Some env') env) xs = Some env'"
   5.255 -  (is "PROP ?P xs")
   5.256 -proof (induct xs)
   5.257 -  fix env e :: "('a, 'b, 'c) env"
   5.258 -  {
   5.259 -    assume "lookup env [] = Some e"
   5.260 -    hence "env = e" by simp
   5.261 -    thus "lookup (update [] (Some env') env) [] = Some env'"
   5.262 -      by simp
   5.263 +  assumes "lookup env xs = Some e"
   5.264 +  shows "lookup (update xs (Some env') env) xs = Some env'"
   5.265 +  using prems
   5.266 +proof (induct xs fixing: env e)
   5.267 +  case Nil
   5.268 +  then have "env = e" by simp
   5.269 +  then show ?case by simp
   5.270 +next
   5.271 +  case (Cons x xs)
   5.272 +  note hyp = Cons.hyps
   5.273 +    and asm = `lookup env (x # xs) = Some e`
   5.274 +  show ?case
   5.275 +  proof (cases env)
   5.276 +    case (Val a)
   5.277 +    with asm have False by simp
   5.278 +    then show ?thesis ..
   5.279    next
   5.280 -    fix x xs
   5.281 -    assume hyp: "PROP ?P xs"
   5.282 -    assume asm: "lookup env (x # xs) = Some e"
   5.283 -    show "lookup (update (x # xs) (Some env') env) (x # xs) = Some env'"
   5.284 -    proof (cases env)
   5.285 -      fix a assume "env = Val a"
   5.286 -      with asm have False by simp
   5.287 -      thus ?thesis ..
   5.288 +    case (Env b es)
   5.289 +    show ?thesis
   5.290 +    proof (cases "es x")
   5.291 +      case None
   5.292 +      with asm Env have False by simp
   5.293 +      then show ?thesis ..
   5.294      next
   5.295 -      fix b es assume env: "env = Env b es"
   5.296 +      case (Some e')
   5.297 +      note es = `es x = Some e'`
   5.298        show ?thesis
   5.299 -      proof (cases "es x")
   5.300 -        assume "es x = None"
   5.301 -        with asm env have False by simp
   5.302 -        thus ?thesis ..
   5.303 +      proof (cases xs)
   5.304 +        case Nil
   5.305 +        with Env show ?thesis by simp
   5.306        next
   5.307 -        fix e' assume es: "es x = Some e'"
   5.308 -        show ?thesis
   5.309 -        proof (cases xs)
   5.310 -          assume "xs = []"
   5.311 -          with env show ?thesis by simp
   5.312 -        next
   5.313 -          fix x' xs' assume xs: "xs = x' # xs'"
   5.314 -          from asm env es have "lookup e' xs = Some e" by simp
   5.315 -          hence "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
   5.316 -          with env es xs show ?thesis by simp
   5.317 -        qed
   5.318 +        case (Cons x' xs')
   5.319 +        from asm Env es have "lookup e' xs = Some e" by simp
   5.320 +        then have "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
   5.321 +        with Env es Cons show ?thesis by simp
   5.322        qed
   5.323      qed
   5.324 -  }
   5.325 +  qed
   5.326  qed
   5.327  
   5.328  text {*
   5.329 @@ -386,93 +375,90 @@
   5.330  *}
   5.331  
   5.332  theorem update_append_none:
   5.333 -  "!!env. lookup env xs = None ==> update (xs @ y # ys) opt env = env"
   5.334 -  (is "PROP ?P xs")
   5.335 -proof (induct xs)
   5.336 -  fix env :: "('a, 'b, 'c) env"
   5.337 -  {
   5.338 -    assume "lookup env [] = None"
   5.339 -    hence False by simp
   5.340 -    thus "update ([] @ y # ys) opt env = env" ..
   5.341 +  assumes "lookup env xs = None"
   5.342 +  shows "update (xs @ y # ys) opt env = env"
   5.343 +  using prems
   5.344 +proof (induct xs fixing: env)
   5.345 +  case Nil
   5.346 +  then have False by simp
   5.347 +  then show ?case ..
   5.348 +next
   5.349 +  case (Cons x xs)
   5.350 +  note hyp = Cons.hyps
   5.351 +    and asm = `lookup env (x # xs) = None`
   5.352 +  show "update ((x # xs) @ y # ys) opt env = env"
   5.353 +  proof (cases env)
   5.354 +    case (Val a)
   5.355 +    then show ?thesis by simp
   5.356    next
   5.357 -    fix x xs
   5.358 -    assume hyp: "PROP ?P xs"
   5.359 -    assume asm: "lookup env (x # xs) = None"
   5.360 -    show "update ((x # xs) @ y # ys) opt env = env"
   5.361 -    proof (cases env)
   5.362 -      fix a assume "env = Val a"
   5.363 -      thus ?thesis by simp
   5.364 -    next
   5.365 -      fix b es assume env: "env = Env b es"
   5.366 +    case (Env b es)
   5.367 +    show ?thesis
   5.368 +    proof (cases "es x")
   5.369 +      case None
   5.370 +      note es = `es x = None`
   5.371        show ?thesis
   5.372 -      proof (cases "es x")
   5.373 -        assume es: "es x = None"
   5.374 -        show ?thesis
   5.375 -          by (cases xs) (simp_all add: es env fun_upd_idem_iff)
   5.376 +        by (cases xs) (simp_all add: es Env fun_upd_idem_iff)
   5.377 +    next
   5.378 +      case (Some e)
   5.379 +      note es = `es x = Some e`
   5.380 +      show ?thesis
   5.381 +      proof (cases xs)
   5.382 +        case Nil
   5.383 +        with asm Env Some have False by simp
   5.384 +        then show ?thesis ..
   5.385        next
   5.386 -        fix e assume es: "es x = Some e"
   5.387 -        show ?thesis
   5.388 -        proof (cases xs)
   5.389 -          assume "xs = []"
   5.390 -          with asm env es have False by simp
   5.391 -          thus ?thesis ..
   5.392 -        next
   5.393 -          fix x' xs' assume xs: "xs = x' # xs'"
   5.394 -          from asm env es have "lookup e xs = None" by simp
   5.395 -          hence "update (xs @ y # ys) opt e = e" by (rule hyp)
   5.396 -          with env es xs show "update ((x # xs) @ y # ys) opt env = env"
   5.397 -            by (simp add: fun_upd_idem_iff)
   5.398 -        qed
   5.399 +        case (Cons x' xs')
   5.400 +        from asm Env es have "lookup e xs = None" by simp
   5.401 +        then have "update (xs @ y # ys) opt e = e" by (rule hyp)
   5.402 +        with Env es Cons show "update ((x # xs) @ y # ys) opt env = env"
   5.403 +          by (simp add: fun_upd_idem_iff)
   5.404        qed
   5.405      qed
   5.406 -  }
   5.407 +  qed
   5.408  qed
   5.409  
   5.410  theorem update_append_some:
   5.411 -  "!!env e. lookup env xs = Some e ==>
   5.412 -    lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
   5.413 -  (is "PROP ?P xs")
   5.414 -proof (induct xs)
   5.415 -  fix env e :: "('a, 'b, 'c) env"
   5.416 -  {
   5.417 -    assume "lookup env [] = Some e"
   5.418 -    hence "env = e" by simp
   5.419 -    thus "lookup (update ([] @ y # ys) opt env) [] = Some (update (y # ys) opt e)"
   5.420 -      by simp
   5.421 +  assumes "lookup env xs = Some e"
   5.422 +  shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
   5.423 +  using prems
   5.424 +proof (induct xs fixing: env e)
   5.425 +  case Nil
   5.426 +  then have "env = e" by simp
   5.427 +  then show ?case by simp
   5.428 +next
   5.429 +  case (Cons x xs)
   5.430 +  note hyp = Cons.hyps
   5.431 +    and asm = `lookup env (x # xs) = Some e`
   5.432 +  show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) =
   5.433 +      Some (update (y # ys) opt e)"
   5.434 +  proof (cases env)
   5.435 +    case (Val a)
   5.436 +    with asm have False by simp
   5.437 +    then show ?thesis ..
   5.438    next
   5.439 -    fix x xs
   5.440 -    assume hyp: "PROP ?P xs"
   5.441 -    assume asm: "lookup env (x # xs) = Some e"
   5.442 -    show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs)
   5.443 -      = Some (update (y # ys) opt e)"
   5.444 -    proof (cases env)
   5.445 -      fix a assume "env = Val a"
   5.446 -      with asm have False by simp
   5.447 -      thus ?thesis ..
   5.448 +    case (Env b es)
   5.449 +    show ?thesis
   5.450 +    proof (cases "es x")
   5.451 +      case None
   5.452 +      with asm Env have False by simp
   5.453 +      then show ?thesis ..
   5.454      next
   5.455 -      fix b es assume env: "env = Env b es"
   5.456 +      case (Some e')
   5.457 +      note es = `es x = Some e'`
   5.458        show ?thesis
   5.459 -      proof (cases "es x")
   5.460 -        assume "es x = None"
   5.461 -        with asm env have False by simp
   5.462 -        thus ?thesis ..
   5.463 +      proof (cases xs)
   5.464 +        case Nil
   5.465 +        with asm Env es have "e = e'" by simp
   5.466 +        with Env es Nil show ?thesis by simp
   5.467        next
   5.468 -        fix e' assume es: "es x = Some e'"
   5.469 -        show ?thesis
   5.470 -        proof (cases xs)
   5.471 -          assume xs: "xs = []"
   5.472 -          from asm env es xs have "e = e'" by simp
   5.473 -          with env es xs show ?thesis by simp
   5.474 -        next
   5.475 -          fix x' xs' assume xs: "xs = x' # xs'"
   5.476 -          from asm env es have "lookup e' xs = Some e" by simp
   5.477 -          hence "lookup (update (xs @ y # ys) opt e') xs =
   5.478 -            Some (update (y # ys) opt e)" by (rule hyp)
   5.479 -          with env es xs show ?thesis by simp
   5.480 -        qed
   5.481 +        case (Cons x' xs')
   5.482 +        from asm Env es have "lookup e' xs = Some e" by simp
   5.483 +        then have "lookup (update (xs @ y # ys) opt e') xs =
   5.484 +          Some (update (y # ys) opt e)" by (rule hyp)
   5.485 +        with Env es Cons show ?thesis by simp
   5.486        qed
   5.487      qed
   5.488 -  }
   5.489 +  qed
   5.490  qed
   5.491  
   5.492  text {*
   5.493 @@ -483,63 +469,58 @@
   5.494  *}
   5.495  
   5.496  theorem lookup_update_other:
   5.497 -  "!!env. y \<noteq> (z::'c) ==> lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
   5.498 +  assumes neq: "y \<noteq> (z::'c)"
   5.499 +  shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
   5.500      lookup env (xs @ y # ys)"
   5.501 -  (is "PROP ?P xs")
   5.502 -proof (induct xs)
   5.503 -  fix env :: "('a, 'b, 'c) env"
   5.504 -  assume neq: "y \<noteq> z"
   5.505 -  {
   5.506 -    show "lookup (update ([] @ z # zs) opt env) ([] @ y # ys) =
   5.507 -      lookup env ([] @ y # ys)"
   5.508 -    proof (cases env)
   5.509 -      case Val
   5.510 -      thus ?thesis by simp
   5.511 +proof (induct xs fixing: env)
   5.512 +  case Nil
   5.513 +  show ?case
   5.514 +  proof (cases env)
   5.515 +    case Val
   5.516 +    then show ?thesis by simp
   5.517 +  next
   5.518 +    case Env
   5.519 +    show ?thesis
   5.520 +    proof (cases zs)
   5.521 +      case Nil
   5.522 +      with neq Env show ?thesis by simp
   5.523      next
   5.524 -      case Env
   5.525 +      case Cons
   5.526 +      with neq Env show ?thesis by simp
   5.527 +    qed
   5.528 +  qed
   5.529 +next
   5.530 +  case (Cons x xs)
   5.531 +  note hyp = Cons.hyps
   5.532 +  show ?case
   5.533 +  proof (cases env)
   5.534 +    case Val
   5.535 +    then show ?thesis by simp
   5.536 +  next
   5.537 +    case (Env y es)
   5.538 +    show ?thesis
   5.539 +    proof (cases xs)
   5.540 +      case Nil
   5.541        show ?thesis
   5.542 -      proof (cases zs)
   5.543 -        case Nil
   5.544 -        with neq Env show ?thesis by simp
   5.545 +      proof (cases "es x")
   5.546 +        case None
   5.547 +        with Env Nil show ?thesis by simp
   5.548        next
   5.549 -        case Cons
   5.550 -        with neq Env show ?thesis by simp
   5.551 +        case Some
   5.552 +        with neq hyp and Env Nil show ?thesis by simp
   5.553 +      qed
   5.554 +    next
   5.555 +      case (Cons x' xs')
   5.556 +      show ?thesis
   5.557 +      proof (cases "es x")
   5.558 +        case None
   5.559 +        with Env Cons show ?thesis by simp
   5.560 +      next
   5.561 +        case Some
   5.562 +        with neq hyp and Env Cons show ?thesis by simp
   5.563        qed
   5.564      qed
   5.565 -  next
   5.566 -    fix x xs
   5.567 -    assume hyp: "PROP ?P xs"
   5.568 -    show "lookup (update ((x # xs) @ z # zs) opt env) ((x # xs) @ y # ys) =
   5.569 -      lookup env ((x # xs) @ y # ys)"
   5.570 -    proof (cases env)
   5.571 -      case Val
   5.572 -      thus ?thesis by simp
   5.573 -    next
   5.574 -      fix y es assume env: "env = Env y es"
   5.575 -      show ?thesis
   5.576 -      proof (cases xs)
   5.577 -        assume xs: "xs = []"
   5.578 -        show ?thesis
   5.579 -        proof (cases "es x")
   5.580 -          case None
   5.581 -          with env xs show ?thesis by simp
   5.582 -        next
   5.583 -          case Some
   5.584 -          with hyp env xs and neq show ?thesis by simp
   5.585 -        qed
   5.586 -      next
   5.587 -        fix x' xs' assume xs: "xs = x' # xs'"
   5.588 -        show ?thesis
   5.589 -        proof (cases "es x")
   5.590 -          case None
   5.591 -          with env xs show ?thesis by simp
   5.592 -        next
   5.593 -          case Some
   5.594 -          with hyp env xs neq show ?thesis by simp
   5.595 -        qed
   5.596 -      qed
   5.597 -    qed
   5.598 -  }
   5.599 +  qed
   5.600  qed
   5.601  
   5.602  end