--- a/src/HOL/Isar_examples/Fibonacci.thy Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Isar_examples/Fibonacci.thy Mon Nov 06 22:56:07 2000 +0100
@@ -126,28 +126,34 @@
lemma gcd_fib_mod:
"0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
-proof (induct n rule: nat_less_induct)
- fix n
+proof -
assume m: "0 < m"
- and hyp: "ALL ma. ma < n
- --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
- 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! add: diff_less)
- 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
+ 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! add: diff_less)
+ 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 .
+ qed
qed
- finally show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" .
qed
--- a/src/HOL/Isar_examples/Hoare.thy Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy Mon Nov 06 22:56:07 2000 +0100
@@ -166,28 +166,26 @@
fix s s' assume s: "s : P"
assume "Sem (While b X c) s s'"
then obtain n where iter: "iter n b (Sem c) s s'" by auto
- show "s' : P Int -b"
- proof -
- have "ALL s s'. iter n b (Sem c) s s' --> s : P --> s' : P Int -b"
- (is "?P n")
- proof (induct (stripped) n)
- fix s s' assume s: "s : P"
- {
- assume "iter 0 b (Sem c) s s'"
- with s show "s' : P Int -b" by auto
- next
- fix n assume hyp: "?P n"
- assume "iter (Suc n) b (Sem c) s s'"
- then obtain s'' where b: "s : b" and sem: "Sem c s s''"
- and iter: "iter n b (Sem c) s'' s'"
- by auto
- from s b have "s : P Int b" by simp
- with body sem have "s'' : P" ..
- with hyp iter show "s' : P Int -b" by simp
- }
- qed
- with iter s show ?thesis by simp
+
+ have "!!s. iter n b (Sem c) s s' ==> s : P ==> s' : P Int -b"
+ (is "PROP ?P n")
+ proof (induct n)
+ fix s assume s: "s : P"
+ {
+ assume "iter 0 b (Sem c) s s'"
+ with s show "?thesis s" by auto
+ next
+ fix n assume hyp: "PROP ?P n"
+ assume "iter (Suc n) b (Sem c) s s'"
+ then obtain s'' where b: "s : b" and sem: "Sem c s s''"
+ and iter: "iter n b (Sem c) s'' s'"
+ by auto
+ from s b have "s : P Int b" by simp
+ with body sem have "s'' : P" ..
+ with iter show "?thesis s" by (rule hyp)
+ }
qed
+ from this iter s show "s' : P Int -b" .
qed
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Mon Nov 06 22:56:07 2000 +0100
@@ -23,31 +23,38 @@
inductive "tiling A"
intros
empty: "{} : tiling A"
- Un: "a : A ==> t : tiling A ==> a <= - t
- ==> a Un t : tiling A"
+ Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A"
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"
-proof
- assume "t : tiling A" (is "_ : ?T")
- thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t")
- proof (induct (stripped) t)
- assume "u : ?T" "{} Int u = {}"
- thus "{} Un u : ?T" by simp
+ "t : tiling A ==> u : tiling A ==> t Int u = {}
+ ==> 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")
+ proof (induct t)
+ from u show "{} Un u : ?T" by simp
next
fix a t
- assume "a : A" "t : ?T" "?P t" "a <= - t"
- assume "u : ?T" "(a Un t) Int u = {}"
- have hyp: "t Un u: ?T" by (blast!)
- have "a <= - (t Un u)" by (blast!)
- with _ hyp have "a Un (t Un u) : ?T" by (rule tiling.Un)
- also have "a Un (t Un u) = (a Un t) Un u"
- by (simp only: Un_assoc)
- finally show "... : ?T" .
+ assume "a : A" and hyp: "PROP ?P t"
+ and at: "a <= - t" and atu: "(a Un t) Int u = {}"
+ show "(a Un t) Un u : ?T"
+ proof -
+ have "a Un (t Un u) : ?T"
+ proof (rule tiling.Un)
+ show "a : A" .
+ from atu have "t Int u = {}" by blast
+ thus "t Un u: ?T" by (rule hyp)
+ from at atu 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)
+ finally show ?thesis .
+ qed
qed
qed
@@ -112,13 +119,13 @@
subsection {* Dominoes *}
-consts
+consts
domino :: "(nat * nat) set set"
inductive domino
intros
- horiz: "{(i, j), (i, j + 1)} : domino"
- vertl: "{(i, j), (i + 1, j)} : domino"
+ horiz: "{(i, j), (i, j + 1)} : domino"
+ vertl: "{(i, j), (i + 1, j)} : domino"
lemma dominoes_tile_row:
"{i} <*> below (2 * n) : tiling domino"
@@ -154,7 +161,7 @@
have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
also have "... : ?T"
- proof (rule tiling_Un [rule_format])
+ proof (rule tiling_Un)
show "?t : ?T" by (rule dominoes_tile_row)
from hyp show "?B m : ?T" .
show "?t Int ?B m = {}" by blast
@@ -178,10 +185,14 @@
qed
lemma domino_finite: "d: domino ==> finite d"
-proof (induct set: domino)
- fix i j :: nat
- show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
- show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros)
+proof -
+ assume "d: domino"
+ thus ?thesis
+ proof induct
+ fix i j :: nat
+ show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
+ show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros)
+ qed
qed
@@ -211,27 +222,27 @@
fix a t
let ?e = evnodd
- assume "a : domino" "t : ?T"
+ assume "a : domino" and "t : ?T"
and hyp: "card (?e t 0) = card (?e t 1)"
- and "a <= - t"
+ and at: "a <= - t"
have card_suc:
"!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
proof -
fix b 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 a b = {(i, j)}"
+ 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)
+ 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)"
+ show "finite (?e t b)"
by (rule evnodd_finite, rule tiling_domino_finite)
- have "(i, j) : ?e a b" by (simp!)
- thus "(i, j) ~: ?e t b" by (blast! dest: evnoddD)
+ 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
@@ -274,9 +285,9 @@
have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
< card (?e ?t' 0)"
proof (rule card_Diff1_less)
- from _ fin show "finite (?e ?t' 0)"
+ from _ fin show "finite (?e ?t' 0)"
by (rule finite_subset) auto
- show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
+ show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
qed
thus ?thesis by simp
qed
--- a/src/HOL/Isar_examples/W_correct.thy Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy Mon Nov 06 22:56:07 2000 +0100
@@ -27,7 +27,7 @@
has_type :: "(typ list * expr * typ) set"
syntax
- "_has_type" :: "[typ list, expr, typ] => bool"
+ "_has_type" :: "typ list => expr => typ => bool"
("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
translations
"a |- e :: t" == "(a, e, t) : has_type"
@@ -74,7 +74,7 @@
subsection {* Type inference algorithm W *}
consts
- W :: "[expr, typ list, nat] => (subst * typ * nat) maybe"
+ W :: "expr => typ list => nat => (subst * typ * nat) maybe"
primrec
"W (Var i) a n =
@@ -91,59 +91,52 @@
subsection {* Correctness theorem *}
-theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t"
-proof -
- assume W_ok: "W e a n = Ok (s, t, m)"
- have "ALL a s t m n. Ok (s, t, m) = W e a n --> $ s a |- e :: t"
- (is "?P e")
- proof (induct (stripped) e)
- fix a s t m n
- {
- fix i
- assume "Ok (s, t, m) = W (Var i) a n"
- thus "$ s a |- Var i :: t" by (simp split: if_splits)
- next
- fix e assume hyp: "?P e"
- assume "Ok (s, t, m) = W (Abs e) a n"
- then obtain t' where "t = s n -> t'"
- and "Ok (s, t', m) = W e (TVar n # a) (Suc n)"
- by (auto split: bind_splits)
- with hyp show "$ s a |- Abs e :: t"
- by (force intro: has_type.Abs)
- next
- fix e1 e2 assume hyp1: "?P e1" and hyp2: "?P e2"
- assume "Ok (s, t, m) = W (App e1 e2) a n"
- then obtain s1 t1 n1 s2 t2 n2 u where
+theorem W_correct: "!!a s t m n. Ok (s, t, m) = W e a n ==> $ s a |- e :: t"
+ (is "PROP ?P e")
+proof (induct e)
+ fix a s t m n
+ {
+ fix i
+ assume "Ok (s, t, m) = W (Var i) a n"
+ thus "$ s a |- Var i :: t" by (simp split: if_splits)
+ next
+ fix e assume hyp: "PROP ?P e"
+ assume "Ok (s, t, m) = W (Abs e) a n"
+ then obtain t' where "t = s n -> t'"
+ and "Ok (s, t', m) = W e (TVar n # a) (Suc n)"
+ by (auto split: bind_splits)
+ with hyp show "$ s a |- Abs e :: t"
+ by (force intro: has_type.Abs)
+ next
+ fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
+ assume "Ok (s, t, m) = W (App e1 e2) a n"
+ then obtain s1 t1 n1 s2 t2 n2 u where
s: "s = $ u o $ s2 o s1"
- and t: "t = u n2"
- and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
- and W1_ok: "W e1 a n = Ok (s1, t1, n1)"
- and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"
- by (auto split: bind_splits simp: that)
- show "$ s a |- App e1 e2 :: t"
- proof (rule has_type.App)
- from s have s': "$ u ($ s2 ($ s1 a)) = $s a"
- by (simp add: subst_comp_tel o_def)
- show "$s a |- e1 :: $ u t2 -> t"
- proof -
- from hyp1 W1_ok [symmetric] have "$ s1 a |- e1 :: t1"
- by blast
- hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"
- by (intro has_type_subst_closed)
- with s' t mgu_ok show ?thesis by simp
- qed
- show "$ s a |- e2 :: $ u t2"
- proof -
- from hyp2 W2_ok [symmetric]
- have "$ s2 ($ s1 a) |- e2 :: t2" by blast
- hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"
- by (rule has_type_subst_closed)
- with s' show ?thesis by simp
- qed
+ and t: "t = u n2"
+ and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
+ and W1_ok: "Ok (s1, t1, n1) = W e1 a n"
+ and W2_ok: "Ok (s2, t2, n2) = W e2 ($ s1 a) n1"
+ by (auto split: bind_splits simp: that)
+ show "$ s a |- App e1 e2 :: t"
+ proof (rule has_type.App)
+ from s have s': "$ u ($ s2 ($ s1 a)) = $s a"
+ by (simp add: subst_comp_tel o_def)
+ show "$s a |- e1 :: $ u t2 -> t"
+ proof -
+ from W1_ok have "$ s1 a |- e1 :: t1" by (rule hyp1)
+ hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)"
+ by (intro has_type_subst_closed)
+ with s' t mgu_ok show ?thesis by simp
qed
- }
- qed
- with W_ok [symmetric] show ?thesis by blast
+ show "$ s a |- e2 :: $ u t2"
+ proof -
+ from W2_ok have "$ s2 ($ s1 a) |- e2 :: t2" by (rule hyp2)
+ hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"
+ by (rule has_type_subst_closed)
+ with s' show ?thesis by simp
+ qed
+ qed
+ }
qed
end
--- a/src/HOL/Library/List_Prefix.thy Mon Nov 06 22:54:13 2000 +0100
+++ b/src/HOL/Library/List_Prefix.thy Mon Nov 06 22:56:07 2000 +0100
@@ -137,49 +137,44 @@
theorem parallel_decomp:
"xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
- (concl is "?E xs")
-proof -
- assume "xs \<parallel> ys"
- have "?this --> ?E xs" (is "?P xs")
- proof (induct (stripped) xs rule: rev_induct)
- assume "[] \<parallel> ys" hence False by auto
- thus "?E []" ..
- next
- fix x xs
- assume hyp: "?P xs"
- assume asm: "xs @ [x] \<parallel> ys"
- show "?E (xs @ [x])"
- proof (rule prefix_cases)
- assume le: "xs \<le> ys"
- then obtain ys' where ys: "ys = xs @ ys'" ..
- show ?thesis
- proof (cases ys')
- assume "ys' = []" with ys have "xs = ys" by simp
- with asm have "[x] \<parallel> []" by auto
- hence False by blast
- thus ?thesis ..
- next
- fix c cs assume ys': "ys' = c # cs"
- with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
- hence "x \<noteq> c" by auto
- moreover have "xs @ [x] = xs @ x # []" by simp
- moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
- ultimately show ?thesis by blast
- qed
- next
- assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
- with asm have False by blast
+ (is "PROP ?P xs" concl is "?E xs")
+proof (induct xs rule: rev_induct)
+ assume "[] \<parallel> ys" hence False by auto
+ thus "?E []" ..
+next
+ fix x xs
+ assume hyp: "PROP ?P xs"
+ assume asm: "xs @ [x] \<parallel> ys"
+ show "?E (xs @ [x])"
+ proof (rule prefix_cases)
+ assume le: "xs \<le> ys"
+ then obtain ys' where ys: "ys = xs @ ys'" ..
+ show ?thesis
+ proof (cases ys')
+ assume "ys' = []" with ys have "xs = ys" by simp
+ with asm have "[x] \<parallel> []" by auto
+ hence False by blast
thus ?thesis ..
next
- assume "xs \<parallel> ys"
- with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
- and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
- by blast
- from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
- with neq ys show ?thesis by blast
+ fix c cs assume ys': "ys' = c # cs"
+ with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
+ hence "x \<noteq> c" by auto
+ moreover have "xs @ [x] = xs @ x # []" by simp
+ moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
+ ultimately show ?thesis by blast
qed
+ next
+ assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
+ with asm have False by blast
+ thus ?thesis ..
+ next
+ assume "xs \<parallel> ys"
+ with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
+ and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
+ by blast
+ from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
+ with neq ys show ?thesis by blast
qed
- thus ?thesis ..
qed
end