tuned induct proofs;
authorwenzelm
Tue Oct 30 17:37:25 2001 +0100 (2001-10-30)
changeset 11987bf31b35949ce
parent 11986 26b95a6f3f79
child 11988 8340fb172607
tuned induct proofs;
src/HOL/Isar_examples/Hoare.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
src/HOL/Isar_examples/W_correct.thy
src/HOL/Lambda/Type.thy
src/HOL/Library/List_Prefix.thy
src/HOL/MicroJava/J/TypeRel.thy
     1.1 --- a/src/HOL/Isar_examples/Hoare.thy	Tue Oct 30 17:33:56 2001 +0100
     1.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Tue Oct 30 17:37:25 2001 +0100
     1.3 @@ -166,24 +166,18 @@
     1.4    fix s s' assume s: "s : P"
     1.5    assume "Sem (While b X c) s s'"
     1.6    then obtain n where iter: "iter n b (Sem c) s s'" by auto
     1.7 -
     1.8    have "!!s. iter n b (Sem c) s s' ==> s : P ==> s' : P Int -b"
     1.9 -    (is "PROP ?P n")
    1.10    proof (induct n)
    1.11 -    fix s assume s: "s : P"
    1.12 -    {
    1.13 -      assume "iter 0 b (Sem c) s s'"
    1.14 -      with s show "?thesis s" by auto
    1.15 -    next
    1.16 -      fix n assume hyp: "PROP ?P n"
    1.17 -      assume "iter (Suc n) b (Sem c) s s'"
    1.18 -      then obtain s'' where b: "s : b" and sem: "Sem c s s''"
    1.19 -        and iter: "iter n b (Sem c) s'' s'"
    1.20 -        by auto
    1.21 -      from s b have "s : P Int b" by simp
    1.22 -      with body sem have "s'' : P" ..
    1.23 -      with iter show "?thesis s" by (rule hyp)
    1.24 -    }
    1.25 +    case (0 s)
    1.26 +    thus ?case by auto
    1.27 +  next
    1.28 +    case (Suc n s)
    1.29 +    then obtain s'' where b: "s : b" and sem: "Sem c s s''"
    1.30 +      and iter: "iter n b (Sem c) s'' s'"
    1.31 +      by auto
    1.32 +    from Suc and b have "s : P Int b" by simp
    1.33 +    with body sem have "s'' : P" ..
    1.34 +    with iter show ?case by (rule Suc)
    1.35    qed
    1.36    from this iter s show "s' : P Int -b" .
    1.37  qed
     2.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Oct 30 17:33:56 2001 +0100
     2.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Oct 30 17:37:25 2001 +0100
     2.3 @@ -37,19 +37,20 @@
     2.4    assume "t : ?T"
     2.5    thus "t Int u = {} ==> t Un u : ?T" (is "PROP ?P t")
     2.6    proof (induct t)
     2.7 -    from u show "{} Un u : ?T" by simp
     2.8 +    case empty
     2.9 +    with u show "{} Un u : ?T" by simp
    2.10    next
    2.11 -    fix a t
    2.12 -    assume "a : A" and hyp: "PROP ?P t"
    2.13 -      and at: "a <= - t" and atu: "(a Un t) Int u = {}"
    2.14 +    case (Un a t)
    2.15      show "(a Un t) Un u : ?T"
    2.16      proof -
    2.17        have "a Un (t Un u) : ?T"
    2.18        proof (rule tiling.Un)
    2.19          show "a : A" .
    2.20 -        from atu have "t Int u = {}" by blast
    2.21 -        thus "t Un u: ?T" by (rule hyp)
    2.22 -        from at atu show "a <= - (t Un u)" by blast
    2.23 +	have atu: "(a Un t) Int u = {}" .
    2.24 +	hence "t Int u = {}" by blast
    2.25 +        thus "t Un u: ?T" by (rule Un)
    2.26 +	have "a <= - t" .
    2.27 +	with atu show "a <= - (t Un u)" by blast
    2.28        qed
    2.29        also have "a Un (t Un u) = (a Un t) Un u"
    2.30          by (simp only: Un_assoc)
    2.31 @@ -129,13 +130,13 @@
    2.32  
    2.33  lemma dominoes_tile_row:
    2.34    "{i} <*> below (2 * n) : tiling domino"
    2.35 -  (is "?P n" is "?B n : ?T")
    2.36 +  (is "?B n : ?T")
    2.37  proof (induct n)
    2.38 -  show "?P 0" by (simp add: below_0 tiling.empty)
    2.39 -
    2.40 -  fix n assume hyp: "?P n"
    2.41 +  case 0
    2.42 +  show ?case by (simp add: below_0 tiling.empty)
    2.43 +next
    2.44 +  case (Suc n)
    2.45    let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
    2.46 -
    2.47    have "?B (Suc n) = ?a Un ?B n"
    2.48      by (auto simp add: Sigma_Suc Un_assoc)
    2.49    also have "... : ?T"
    2.50 @@ -144,29 +145,29 @@
    2.51        by (rule domino.horiz)
    2.52      also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
    2.53      finally show "... : domino" .
    2.54 -    from hyp show "?B n : ?T" .
    2.55 +    show "?B n : ?T" by (rule Suc)
    2.56      show "?a <= - ?B n" by blast
    2.57    qed
    2.58 -  finally show "?P (Suc n)" .
    2.59 +  finally show ?case .
    2.60  qed
    2.61  
    2.62  lemma dominoes_tile_matrix:
    2.63    "below m <*> below (2 * n) : tiling domino"
    2.64 -  (is "?P m" is "?B m : ?T")
    2.65 +  (is "?B m : ?T")
    2.66  proof (induct m)
    2.67 -  show "?P 0" by (simp add: below_0 tiling.empty)
    2.68 -
    2.69 -  fix m assume hyp: "?P m"
    2.70 +  case 0
    2.71 +  show ?case by (simp add: below_0 tiling.empty)
    2.72 +next
    2.73 +  case (Suc m)
    2.74    let ?t = "{m} <*> below (2 * n)"
    2.75 -
    2.76    have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
    2.77    also have "... : ?T"
    2.78    proof (rule tiling_Un)
    2.79      show "?t : ?T" by (rule dominoes_tile_row)
    2.80 -    from hyp show "?B m : ?T" .
    2.81 +    show "?B m : ?T" by (rule Suc)
    2.82      show "?t Int ?B m = {}" by blast
    2.83    qed
    2.84 -  finally show "?P (Suc m)" .
    2.85 +  finally show ?case .
    2.86  qed
    2.87  
    2.88  lemma domino_singleton:
    2.89 @@ -213,19 +214,18 @@
    2.90  
    2.91  lemma tiling_domino_01:
    2.92    "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
    2.93 -  (is "t : ?T ==> ?P t")
    2.94 +  (is "t : ?T ==> _")
    2.95  proof -
    2.96    assume "t : ?T"
    2.97 -  thus "?P t"
    2.98 +  thus ?thesis
    2.99    proof induct
   2.100 -    show "?P {}" by (simp add: evnodd_def)
   2.101 -
   2.102 -    fix a t
   2.103 +    case empty
   2.104 +    show ?case by (simp add: evnodd_def)
   2.105 +  next
   2.106 +    case (Un a t)
   2.107      let ?e = evnodd
   2.108 -    assume "a : domino" and "t : ?T"
   2.109 -      and hyp: "card (?e t 0) = card (?e t 1)"
   2.110 -      and at: "a <= - t"
   2.111 -
   2.112 +    have hyp: "card (?e t 0) = card (?e t 1)" .
   2.113 +    have at: "a <= - t" .
   2.114      have card_suc:
   2.115        "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
   2.116      proof -
   2.117 @@ -250,7 +250,7 @@
   2.118      also from hyp have "card (?e t 0) = card (?e t 1)" .
   2.119      also from card_suc have "Suc ... = card (?e (a Un t) 1)"
   2.120        by simp
   2.121 -    finally show "?P (a Un t)" .
   2.122 +    finally show ?case .
   2.123    qed
   2.124  qed
   2.125  
     3.1 --- a/src/HOL/Isar_examples/W_correct.thy	Tue Oct 30 17:33:56 2001 +0100
     3.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Tue Oct 30 17:37:25 2001 +0100
     3.3 @@ -46,8 +46,8 @@
     3.4  proof -
     3.5    assume "a |- e :: t"
     3.6    thus ?thesis (is "?P a e t")
     3.7 -  proof (induct (open) a e t)
     3.8 -    case Var
     3.9 +  proof induct
    3.10 +    case (Var a n)
    3.11      hence "n < length (map ($ s) a)" by simp
    3.12      hence "map ($ s) a |- Var n :: map ($ s) a ! n"
    3.13        by (rule has_type.Var)
    3.14 @@ -57,7 +57,7 @@
    3.15        by (simp only: app_subst_list)
    3.16      finally show "?P a (Var n) (a ! n)" .
    3.17    next
    3.18 -    case Abs
    3.19 +    case (Abs a e t1 t2)
    3.20      hence "$ s t1 # map ($ s) a |- e :: $ s t2"
    3.21        by (simp add: app_subst_list)
    3.22      hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
    3.23 @@ -66,7 +66,7 @@
    3.24        by (simp add: app_subst_list)
    3.25    next
    3.26      case App
    3.27 -    thus "?P a (App e1 e2) t1" by (simp add: has_type.App)
    3.28 +    thus ?case by (simp add: has_type.App)
    3.29    qed
    3.30  qed
    3.31  
     4.1 --- a/src/HOL/Lambda/Type.thy	Tue Oct 30 17:33:56 2001 +0100
     4.2 +++ b/src/HOL/Lambda/Type.thy	Tue Oct 30 17:37:25 2001 +0100
     4.3 @@ -95,11 +95,11 @@
     4.4  
     4.5  subsection {* n-ary function types *}
     4.6  
     4.7 -lemma list_app_typeD [rule_format]:
     4.8 -    "\<forall>t T. e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<longrightarrow> (\<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts)"
     4.9 -  apply (induct_tac ts)
    4.10 +lemma list_app_typeD:
    4.11 +    "\<And>t T. e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
    4.12 +  apply (induct ts)
    4.13     apply simp
    4.14 -  apply (intro strip)
    4.15 +  apply atomize
    4.16    apply simp
    4.17    apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
    4.18    apply (erule_tac x = T in allE)
    4.19 @@ -115,12 +115,11 @@
    4.20    "e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C"
    4.21    by (insert list_app_typeD) fast
    4.22  
    4.23 -lemma list_app_typeI [rule_format]:
    4.24 -    "\<forall>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<longrightarrow> e \<tturnstile> ts : Ts \<longrightarrow> e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T"
    4.25 -  apply (induct_tac ts)
    4.26 -   apply (intro strip)
    4.27 +lemma list_app_typeI:
    4.28 +    "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T"
    4.29 +  apply (induct ts)
    4.30     apply simp
    4.31 -  apply (intro strip)
    4.32 +  apply atomize
    4.33    apply (case_tac Ts)
    4.34     apply simp
    4.35    apply simp
    4.36 @@ -134,15 +133,13 @@
    4.37    apply blast
    4.38    done
    4.39  
    4.40 -lemma lists_typings [rule_format]:
    4.41 -    "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
    4.42 -  apply (induct_tac ts)
    4.43 -   apply (intro strip)
    4.44 +lemma lists_typings:
    4.45 +    "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
    4.46 +  apply (induct ts)
    4.47     apply (case_tac Ts)
    4.48       apply simp
    4.49       apply (rule lists.Nil)
    4.50      apply simp
    4.51 -  apply (intro strip)
    4.52    apply (case_tac Ts)
    4.53     apply simp
    4.54    apply simp
    4.55 @@ -192,11 +189,10 @@
    4.56      by induct auto
    4.57  qed
    4.58  
    4.59 -lemma lift_typings [rule_format]:
    4.60 -  "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
    4.61 -  apply (induct_tac ts)
    4.62 +lemma lift_typings:
    4.63 +  "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
    4.64 +  apply (induct ts)
    4.65     apply simp
    4.66 -  apply (intro strip)
    4.67    apply (case_tac Ts)
    4.68     apply auto
    4.69    done
     5.1 --- a/src/HOL/Library/List_Prefix.thy	Tue Oct 30 17:33:56 2001 +0100
     5.2 +++ b/src/HOL/Library/List_Prefix.thy	Tue Oct 30 17:37:25 2001 +0100
     5.3 @@ -151,27 +151,25 @@
     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 -  (is "PROP ?P xs" concl is "?E xs")
     5.8  proof (induct xs rule: rev_induct)
     5.9 -  assume "[] \<parallel> ys" hence False by auto
    5.10 -  thus "?E []" ..
    5.11 +  case Nil
    5.12 +  hence False by auto
    5.13 +  thus ?case ..
    5.14  next
    5.15 -  fix x xs
    5.16 -  assume hyp: "PROP ?P xs"
    5.17 -  assume asm: "xs @ [x] \<parallel> ys"
    5.18 -  show "?E (xs @ [x])"
    5.19 +  case (snoc x xs)
    5.20 +  show ?case
    5.21    proof (rule prefix_cases)
    5.22      assume le: "xs \<le> ys"
    5.23      then obtain ys' where ys: "ys = xs @ ys'" ..
    5.24      show ?thesis
    5.25      proof (cases ys')
    5.26        assume "ys' = []" with ys have "xs = ys" by simp
    5.27 -      with asm have "[x] \<parallel> []" by auto
    5.28 +      with snoc have "[x] \<parallel> []" by auto
    5.29        hence False by blast
    5.30        thus ?thesis ..
    5.31      next
    5.32        fix c cs assume ys': "ys' = c # cs"
    5.33 -      with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
    5.34 +      with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
    5.35        hence "x \<noteq> c" by auto
    5.36        moreover have "xs @ [x] = xs @ x # []" by simp
    5.37        moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
    5.38 @@ -179,11 +177,11 @@
    5.39      qed
    5.40    next
    5.41      assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
    5.42 -    with asm have False by blast
    5.43 +    with snoc have False by blast
    5.44      thus ?thesis ..
    5.45    next
    5.46      assume "xs \<parallel> ys"
    5.47 -    with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
    5.48 +    with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
    5.49        and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
    5.50        by blast
    5.51      from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
     6.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Oct 30 17:33:56 2001 +0100
     6.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Oct 30 17:37:25 2001 +0100
     6.3 @@ -193,11 +193,11 @@
     6.4  (*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
     6.5  proof -
     6.6    assume "G\<turnstile>S\<preceq>U"
     6.7 -  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
     6.8 -  proof (induct (*cases*) (open) (*?P S U*) rule: widen.induct [consumes 1])
     6.9 +  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" ( *(is "PROP ?P S U")* )
    6.10 +  proof (induct ( *cases* ) (open) ( *?P S U* ) rule: widen.induct [consumes 1])
    6.11      case refl
    6.12      fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
    6.13 -      (* fix T' show "PROP ?P T T".*)
    6.14 +      ( * fix T' show "PROP ?P T T".* )
    6.15    next
    6.16      case subcls
    6.17      fix T assume "G\<turnstile>Class D\<preceq>T"
    6.18 @@ -215,24 +215,19 @@
    6.19  theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
    6.20  proof -
    6.21    assume "G\<turnstile>S\<preceq>U"
    6.22 -  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
    6.23 -  proof (induct (*cases*) (open) (*?P S U*)) (* rule: widen.induct *)
    6.24 -    case refl
    6.25 -    fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
    6.26 -      (* fix T' show "PROP ?P T T".*)
    6.27 +  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
    6.28 +  proof induct
    6.29 +    case (refl T T')
    6.30 +    thus "G\<turnstile>T\<preceq>T'" .
    6.31    next
    6.32 -    case subcls
    6.33 -    fix T assume "G\<turnstile>Class D\<preceq>T"
    6.34 +    case (subcls C D T)
    6.35      then obtain E where "T = Class E" by (blast dest: widen_Class)
    6.36 -    from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
    6.37 +    with subcls show "G\<turnstile>Class C\<preceq>T" by (auto elim: rtrancl_trans)
    6.38    next
    6.39 -    case null
    6.40 -    fix RT assume "G\<turnstile>RefT R\<preceq>RT"
    6.41 +    case (null R RT)
    6.42      then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
    6.43      thus "G\<turnstile>NT\<preceq>RT" by auto
    6.44    qed
    6.45  qed
    6.46  
    6.47 -
    6.48 -
    6.49  end