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