summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 10 Nov 2005 21:14:05 +0100 | |

changeset 18153 | a084aa91f701 |

parent 18152 | 1d1cc715a9e5 |

child 18154 | 0c05abaf6244 |

tuned proofs;

--- 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

--- 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)

--- 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

--- 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

--- 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