author | wenzelm |

Thu Nov 10 21:14:05 2005 +0100 (2005-11-10) | |

changeset 18153 | a084aa91f701 |

parent 18152 | 1d1cc715a9e5 |

child 18154 | 0c05abaf6244 |

tuned proofs;

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