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

author | wenzelm |

Mon, 06 Nov 2000 22:56:07 +0100 | |

changeset 10408 | d8b3613158b1 |

parent 10407 | 998778f8d63b |

child 10409 | 10a1b95ce642 |

improved: 'induct' handle non-atomic goals;

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