author | wenzelm |

Mon Nov 06 22:56:07 2000 +0100 (2000-11-06) | |

changeset 10408 | d8b3613158b1 |

parent 10407 | 998778f8d63b |

child 10409 | 10a1b95ce642 |

improved: 'induct' handle non-atomic goals;

1.1 --- a/src/HOL/Isar_examples/Fibonacci.thy Mon Nov 06 22:54:13 2000 +0100 1.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy Mon Nov 06 22:56:07 2000 +0100 1.3 @@ -126,28 +126,34 @@ 1.4 1.5 lemma gcd_fib_mod: 1.6 "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" 1.7 -proof (induct n rule: nat_less_induct) 1.8 - fix n 1.9 +proof - 1.10 assume m: "0 < m" 1.11 - and hyp: "ALL ma. ma < n 1.12 - --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)" 1.13 - have "n mod m = (if n < m then n else (n - m) mod m)" 1.14 - by (rule mod_if) 1.15 - also have "gcd (fib m, fib ...) = gcd (fib m, fib n)" 1.16 - proof cases 1.17 - assume "n < m" thus ?thesis by simp 1.18 - next 1.19 - assume not_lt: "~ n < m" hence le: "m <= n" by simp 1.20 - have "n - m < n" by (simp! add: diff_less) 1.21 - with hyp have "gcd (fib m, fib ((n - m) mod m)) 1.22 - = gcd (fib m, fib (n - m))" by simp 1.23 - also from le have "... = gcd (fib m, fib n)" 1.24 - by (rule gcd_fib_diff) 1.25 - finally have "gcd (fib m, fib ((n - m) mod m)) = 1.26 - gcd (fib m, fib n)" . 1.27 - with not_lt show ?thesis by simp 1.28 + show ?thesis 1.29 + proof (induct n rule: nat_less_induct) 1.30 + fix n 1.31 + assume hyp: "ALL ma. ma < n 1.32 + --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)" 1.33 + show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" 1.34 + proof - 1.35 + have "n mod m = (if n < m then n else (n - m) mod m)" 1.36 + by (rule mod_if) 1.37 + also have "gcd (fib m, fib ...) = gcd (fib m, fib n)" 1.38 + proof cases 1.39 + assume "n < m" thus ?thesis by simp 1.40 + next 1.41 + assume not_lt: "~ n < m" hence le: "m <= n" by simp 1.42 + have "n - m < n" by (simp! add: diff_less) 1.43 + with hyp have "gcd (fib m, fib ((n - m) mod m)) 1.44 + = gcd (fib m, fib (n - m))" by simp 1.45 + also from le have "... = gcd (fib m, fib n)" 1.46 + by (rule gcd_fib_diff) 1.47 + finally have "gcd (fib m, fib ((n - m) mod m)) = 1.48 + gcd (fib m, fib n)" . 1.49 + with not_lt show ?thesis by simp 1.50 + qed 1.51 + finally show ?thesis . 1.52 + qed 1.53 qed 1.54 - finally show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" . 1.55 qed 1.56 1.57

2.1 --- a/src/HOL/Isar_examples/Hoare.thy Mon Nov 06 22:54:13 2000 +0100 2.2 +++ b/src/HOL/Isar_examples/Hoare.thy Mon Nov 06 22:56:07 2000 +0100 2.3 @@ -166,28 +166,26 @@ 2.4 fix s s' assume s: "s : P" 2.5 assume "Sem (While b X c) s s'" 2.6 then obtain n where iter: "iter n b (Sem c) s s'" by auto 2.7 - show "s' : P Int -b" 2.8 - proof - 2.9 - have "ALL s s'. iter n b (Sem c) s s' --> s : P --> s' : P Int -b" 2.10 - (is "?P n") 2.11 - proof (induct (stripped) n) 2.12 - fix s s' assume s: "s : P" 2.13 - { 2.14 - assume "iter 0 b (Sem c) s s'" 2.15 - with s show "s' : P Int -b" by auto 2.16 - next 2.17 - fix n assume hyp: "?P n" 2.18 - assume "iter (Suc n) b (Sem c) s s'" 2.19 - then obtain s'' where b: "s : b" and sem: "Sem c s s''" 2.20 - and iter: "iter n b (Sem c) s'' s'" 2.21 - by auto 2.22 - from s b have "s : P Int b" by simp 2.23 - with body sem have "s'' : P" .. 2.24 - with hyp iter show "s' : P Int -b" by simp 2.25 - } 2.26 - qed 2.27 - with iter s show ?thesis by simp 2.28 + 2.29 + have "!!s. iter n b (Sem c) s s' ==> s : P ==> s' : P Int -b" 2.30 + (is "PROP ?P n") 2.31 + proof (induct n) 2.32 + fix s assume s: "s : P" 2.33 + { 2.34 + assume "iter 0 b (Sem c) s s'" 2.35 + with s show "?thesis s" by auto 2.36 + next 2.37 + fix n assume hyp: "PROP ?P n" 2.38 + assume "iter (Suc n) b (Sem c) s s'" 2.39 + then obtain s'' where b: "s : b" and sem: "Sem c s s''" 2.40 + and iter: "iter n b (Sem c) s'' s'" 2.41 + by auto 2.42 + from s b have "s : P Int b" by simp 2.43 + with body sem have "s'' : P" .. 2.44 + with iter show "?thesis s" by (rule hyp) 2.45 + } 2.46 qed 2.47 + from this iter s show "s' : P Int -b" . 2.48 qed 2.49 2.50

3.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Mon Nov 06 22:54:13 2000 +0100 3.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Mon Nov 06 22:56:07 2000 +0100 3.3 @@ -23,31 +23,38 @@ 3.4 inductive "tiling A" 3.5 intros 3.6 empty: "{} : tiling A" 3.7 - Un: "a : A ==> t : tiling A ==> a <= - t 3.8 - ==> a Un t : tiling A" 3.9 + Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A" 3.10 3.11 3.12 text "The union of two disjoint tilings is a tiling." 3.13 3.14 lemma tiling_Un: 3.15 - "t : tiling A --> u : tiling A --> t Int u = {} 3.16 - --> t Un u : tiling A" 3.17 -proof 3.18 - assume "t : tiling A" (is "_ : ?T") 3.19 - thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t") 3.20 - proof (induct (stripped) t) 3.21 - assume "u : ?T" "{} Int u = {}" 3.22 - thus "{} Un u : ?T" by simp 3.23 + "t : tiling A ==> u : tiling A ==> t Int u = {} 3.24 + ==> t Un u : tiling A" 3.25 +proof - 3.26 + let ?T = "tiling A" 3.27 + assume u: "u : ?T" 3.28 + assume "t : ?T" 3.29 + thus "t Int u = {} ==> t Un u : ?T" (is "PROP ?P t") 3.30 + proof (induct t) 3.31 + from u show "{} Un u : ?T" by simp 3.32 next 3.33 fix a t 3.34 - assume "a : A" "t : ?T" "?P t" "a <= - t" 3.35 - assume "u : ?T" "(a Un t) Int u = {}" 3.36 - have hyp: "t Un u: ?T" by (blast!) 3.37 - have "a <= - (t Un u)" by (blast!) 3.38 - with _ hyp have "a Un (t Un u) : ?T" by (rule tiling.Un) 3.39 - also have "a Un (t Un u) = (a Un t) Un u" 3.40 - by (simp only: Un_assoc) 3.41 - finally show "... : ?T" . 3.42 + assume "a : A" and hyp: "PROP ?P t" 3.43 + and at: "a <= - t" and atu: "(a Un t) Int u = {}" 3.44 + show "(a Un t) Un u : ?T" 3.45 + proof - 3.46 + have "a Un (t Un u) : ?T" 3.47 + proof (rule tiling.Un) 3.48 + show "a : A" . 3.49 + from atu have "t Int u = {}" by blast 3.50 + thus "t Un u: ?T" by (rule hyp) 3.51 + from at atu show "a <= - (t Un u)" by blast 3.52 + qed 3.53 + also have "a Un (t Un u) = (a Un t) Un u" 3.54 + by (simp only: Un_assoc) 3.55 + finally show ?thesis . 3.56 + qed 3.57 qed 3.58 qed 3.59 3.60 @@ -112,13 +119,13 @@ 3.61 3.62 subsection {* Dominoes *} 3.63 3.64 -consts 3.65 +consts 3.66 domino :: "(nat * nat) set set" 3.67 3.68 inductive domino 3.69 intros 3.70 - horiz: "{(i, j), (i, j + 1)} : domino" 3.71 - vertl: "{(i, j), (i + 1, j)} : domino" 3.72 + horiz: "{(i, j), (i, j + 1)} : domino" 3.73 + vertl: "{(i, j), (i + 1, j)} : domino" 3.74 3.75 lemma dominoes_tile_row: 3.76 "{i} <*> below (2 * n) : tiling domino" 3.77 @@ -154,7 +161,7 @@ 3.78 3.79 have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc) 3.80 also have "... : ?T" 3.81 - proof (rule tiling_Un [rule_format]) 3.82 + proof (rule tiling_Un) 3.83 show "?t : ?T" by (rule dominoes_tile_row) 3.84 from hyp show "?B m : ?T" . 3.85 show "?t Int ?B m = {}" by blast 3.86 @@ -178,10 +185,14 @@ 3.87 qed 3.88 3.89 lemma domino_finite: "d: domino ==> finite d" 3.90 -proof (induct set: domino) 3.91 - fix i j :: nat 3.92 - show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros) 3.93 - show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros) 3.94 +proof - 3.95 + assume "d: domino" 3.96 + thus ?thesis 3.97 + proof induct 3.98 + fix i j :: nat 3.99 + show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros) 3.100 + show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros) 3.101 + qed 3.102 qed 3.103 3.104 3.105 @@ -211,27 +222,27 @@ 3.106 3.107 fix a t 3.108 let ?e = evnodd 3.109 - assume "a : domino" "t : ?T" 3.110 + assume "a : domino" and "t : ?T" 3.111 and hyp: "card (?e t 0) = card (?e t 1)" 3.112 - and "a <= - t" 3.113 + and at: "a <= - t" 3.114 3.115 have card_suc: 3.116 "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))" 3.117 proof - 3.118 fix b assume "b < 2" 3.119 have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un) 3.120 - also obtain i j where "?e a b = {(i, j)}" 3.121 + also obtain i j where e: "?e a b = {(i, j)}" 3.122 proof - 3.123 - have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton) 3.124 - thus ?thesis by (blast intro: that) 3.125 + have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton) 3.126 + thus ?thesis by (blast intro: that) 3.127 qed 3.128 also have "... Un ?e t b = insert (i, j) (?e t b)" by simp 3.129 also have "card ... = Suc (card (?e t b))" 3.130 proof (rule card_insert_disjoint) 3.131 - show "finite (?e t b)" 3.132 + show "finite (?e t b)" 3.133 by (rule evnodd_finite, rule tiling_domino_finite) 3.134 - have "(i, j) : ?e a b" by (simp!) 3.135 - thus "(i, j) ~: ?e t b" by (blast! dest: evnoddD) 3.136 + from e have "(i, j) : ?e a b" by simp 3.137 + with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD) 3.138 qed 3.139 finally show "?thesis b" . 3.140 qed 3.141 @@ -274,9 +285,9 @@ 3.142 have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) 3.143 < card (?e ?t' 0)" 3.144 proof (rule card_Diff1_less) 3.145 - from _ fin show "finite (?e ?t' 0)" 3.146 + from _ fin show "finite (?e ?t' 0)" 3.147 by (rule finite_subset) auto 3.148 - show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp 3.149 + show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp 3.150 qed 3.151 thus ?thesis by simp 3.152 qed

4.1 --- a/src/HOL/Isar_examples/W_correct.thy Mon Nov 06 22:54:13 2000 +0100 4.2 +++ b/src/HOL/Isar_examples/W_correct.thy Mon Nov 06 22:56:07 2000 +0100 4.3 @@ -27,7 +27,7 @@ 4.4 has_type :: "(typ list * expr * typ) set" 4.5 4.6 syntax 4.7 - "_has_type" :: "[typ list, expr, typ] => bool" 4.8 + "_has_type" :: "typ list => expr => typ => bool" 4.9 ("((_) |-/ (_) :: (_))" [60, 0, 60] 60) 4.10 translations 4.11 "a |- e :: t" == "(a, e, t) : has_type" 4.12 @@ -74,7 +74,7 @@ 4.13 subsection {* Type inference algorithm W *} 4.14 4.15 consts 4.16 - W :: "[expr, typ list, nat] => (subst * typ * nat) maybe" 4.17 + W :: "expr => typ list => nat => (subst * typ * nat) maybe" 4.18 4.19 primrec 4.20 "W (Var i) a n = 4.21 @@ -91,59 +91,52 @@ 4.22 4.23 subsection {* Correctness theorem *} 4.24 4.25 -theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t" 4.26 -proof - 4.27 - assume W_ok: "W e a n = Ok (s, t, m)" 4.28 - have "ALL a s t m n. Ok (s, t, m) = W e a n --> $ s a |- e :: t" 4.29 - (is "?P e") 4.30 - proof (induct (stripped) e) 4.31 - fix a s t m n 4.32 - { 4.33 - fix i 4.34 - assume "Ok (s, t, m) = W (Var i) a n" 4.35 - thus "$ s a |- Var i :: t" by (simp split: if_splits) 4.36 - next 4.37 - fix e assume hyp: "?P e" 4.38 - assume "Ok (s, t, m) = W (Abs e) a n" 4.39 - then obtain t' where "t = s n -> t'" 4.40 - and "Ok (s, t', m) = W e (TVar n # a) (Suc n)" 4.41 - by (auto split: bind_splits) 4.42 - with hyp show "$ s a |- Abs e :: t" 4.43 - by (force intro: has_type.Abs) 4.44 - next 4.45 - fix e1 e2 assume hyp1: "?P e1" and hyp2: "?P e2" 4.46 - assume "Ok (s, t, m) = W (App e1 e2) a n" 4.47 - then obtain s1 t1 n1 s2 t2 n2 u where 4.48 +theorem W_correct: "!!a s t m n. Ok (s, t, m) = W e a n ==> $ s a |- e :: t" 4.49 + (is "PROP ?P e") 4.50 +proof (induct e) 4.51 + fix a s t m n 4.52 + { 4.53 + fix i 4.54 + assume "Ok (s, t, m) = W (Var i) a n" 4.55 + thus "$ s a |- Var i :: t" by (simp split: if_splits) 4.56 + next 4.57 + fix e assume hyp: "PROP ?P e" 4.58 + assume "Ok (s, t, m) = W (Abs e) a n" 4.59 + then obtain t' where "t = s n -> t'" 4.60 + and "Ok (s, t', m) = W e (TVar n # a) (Suc n)" 4.61 + by (auto split: bind_splits) 4.62 + with hyp show "$ s a |- Abs e :: t" 4.63 + by (force intro: has_type.Abs) 4.64 + next 4.65 + fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2" 4.66 + assume "Ok (s, t, m) = W (App e1 e2) a n" 4.67 + then obtain s1 t1 n1 s2 t2 n2 u where 4.68 s: "s = $ u o $ s2 o s1" 4.69 - and t: "t = u n2" 4.70 - and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u" 4.71 - and W1_ok: "W e1 a n = Ok (s1, t1, n1)" 4.72 - and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)" 4.73 - by (auto split: bind_splits simp: that) 4.74 - show "$ s a |- App e1 e2 :: t" 4.75 - proof (rule has_type.App) 4.76 - from s have s': "$ u ($ s2 ($ s1 a)) = $s a" 4.77 - by (simp add: subst_comp_tel o_def) 4.78 - show "$s a |- e1 :: $ u t2 -> t" 4.79 - proof - 4.80 - from hyp1 W1_ok [symmetric] have "$ s1 a |- e1 :: t1" 4.81 - by blast 4.82 - hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)" 4.83 - by (intro has_type_subst_closed) 4.84 - with s' t mgu_ok show ?thesis by simp 4.85 - qed 4.86 - show "$ s a |- e2 :: $ u t2" 4.87 - proof - 4.88 - from hyp2 W2_ok [symmetric] 4.89 - have "$ s2 ($ s1 a) |- e2 :: t2" by blast 4.90 - hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2" 4.91 - by (rule has_type_subst_closed) 4.92 - with s' show ?thesis by simp 4.93 - qed 4.94 + and t: "t = u n2" 4.95 + and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u" 4.96 + and W1_ok: "Ok (s1, t1, n1) = W e1 a n" 4.97 + and W2_ok: "Ok (s2, t2, n2) = W e2 ($ s1 a) n1" 4.98 + by (auto split: bind_splits simp: that) 4.99 + show "$ s a |- App e1 e2 :: t" 4.100 + proof (rule has_type.App) 4.101 + from s have s': "$ u ($ s2 ($ s1 a)) = $s a" 4.102 + by (simp add: subst_comp_tel o_def) 4.103 + show "$s a |- e1 :: $ u t2 -> t" 4.104 + proof - 4.105 + from W1_ok have "$ s1 a |- e1 :: t1" by (rule hyp1) 4.106 + hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)" 4.107 + by (intro has_type_subst_closed) 4.108 + with s' t mgu_ok show ?thesis by simp 4.109 qed 4.110 - } 4.111 - qed 4.112 - with W_ok [symmetric] show ?thesis by blast 4.113 + show "$ s a |- e2 :: $ u t2" 4.114 + proof - 4.115 + from W2_ok have "$ s2 ($ s1 a) |- e2 :: t2" by (rule hyp2) 4.116 + hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2" 4.117 + by (rule has_type_subst_closed) 4.118 + with s' show ?thesis by simp 4.119 + qed 4.120 + qed 4.121 + } 4.122 qed 4.123 4.124 end

5.1 --- a/src/HOL/Library/List_Prefix.thy Mon Nov 06 22:54:13 2000 +0100 5.2 +++ b/src/HOL/Library/List_Prefix.thy Mon Nov 06 22:56:07 2000 +0100 5.3 @@ -137,49 +137,44 @@ 5.4 5.5 theorem parallel_decomp: 5.6 "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 5.7 - (concl is "?E xs") 5.8 -proof - 5.9 - assume "xs \<parallel> ys" 5.10 - have "?this --> ?E xs" (is "?P xs") 5.11 - proof (induct (stripped) xs rule: rev_induct) 5.12 - assume "[] \<parallel> ys" hence False by auto 5.13 - thus "?E []" .. 5.14 - next 5.15 - fix x xs 5.16 - assume hyp: "?P xs" 5.17 - assume asm: "xs @ [x] \<parallel> ys" 5.18 - show "?E (xs @ [x])" 5.19 - proof (rule prefix_cases) 5.20 - assume le: "xs \<le> ys" 5.21 - then obtain ys' where ys: "ys = xs @ ys'" .. 5.22 - show ?thesis 5.23 - proof (cases ys') 5.24 - assume "ys' = []" with ys have "xs = ys" by simp 5.25 - with asm have "[x] \<parallel> []" by auto 5.26 - hence False by blast 5.27 - thus ?thesis .. 5.28 - next 5.29 - fix c cs assume ys': "ys' = c # cs" 5.30 - with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) 5.31 - hence "x \<noteq> c" by auto 5.32 - moreover have "xs @ [x] = xs @ x # []" by simp 5.33 - moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) 5.34 - ultimately show ?thesis by blast 5.35 - qed 5.36 - next 5.37 - assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp 5.38 - with asm have False by blast 5.39 + (is "PROP ?P xs" concl is "?E xs") 5.40 +proof (induct xs rule: rev_induct) 5.41 + assume "[] \<parallel> ys" hence False by auto 5.42 + thus "?E []" .. 5.43 +next 5.44 + fix x xs 5.45 + assume hyp: "PROP ?P xs" 5.46 + assume asm: "xs @ [x] \<parallel> ys" 5.47 + show "?E (xs @ [x])" 5.48 + proof (rule prefix_cases) 5.49 + assume le: "xs \<le> ys" 5.50 + then obtain ys' where ys: "ys = xs @ ys'" .. 5.51 + show ?thesis 5.52 + proof (cases ys') 5.53 + assume "ys' = []" with ys have "xs = ys" by simp 5.54 + with asm have "[x] \<parallel> []" by auto 5.55 + hence False by blast 5.56 thus ?thesis .. 5.57 next 5.58 - assume "xs \<parallel> ys" 5.59 - with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c" 5.60 - and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" 5.61 - by blast 5.62 - from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp 5.63 - with neq ys show ?thesis by blast 5.64 + fix c cs assume ys': "ys' = c # cs" 5.65 + with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) 5.66 + hence "x \<noteq> c" by auto 5.67 + moreover have "xs @ [x] = xs @ x # []" by simp 5.68 + moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) 5.69 + ultimately show ?thesis by blast 5.70 qed 5.71 + next 5.72 + assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp 5.73 + with asm have False by blast 5.74 + thus ?thesis .. 5.75 + next 5.76 + assume "xs \<parallel> ys" 5.77 + with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c" 5.78 + and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" 5.79 + by blast 5.80 + from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp 5.81 + with neq ys show ?thesis by blast 5.82 qed 5.83 - thus ?thesis .. 5.84 qed 5.85 5.86 end