tuned induct proofs;
authorwenzelm
Fri Nov 25 19:20:56 2005 +0100 (2005-11-25)
changeset 18258836491e9b7d5
parent 18257 2124b24454dd
child 18259 7b14579c58f2
tuned induct proofs;
src/HOL/Library/List_Prefix.thy
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Fri Nov 25 19:09:44 2005 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Fri Nov 25 19:20:56 2005 +0100
     1.3 @@ -242,12 +242,12 @@
     1.4    by(auto simp add: postfix_def)
     1.5  
     1.6  lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs"
     1.7 -  by (induct zs, auto)
     1.8 +  by (induct zs) auto
     1.9  lemma postfix_is_subset: "xs >>= ys \<Longrightarrow> set ys \<subseteq> set xs"
    1.10    by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma)
    1.11  
    1.12 -lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >>= ys"
    1.13 -  by (induct zs, auto intro!: postfix_appendI postfix_ConsI)
    1.14 +lemma postfix_ConsD2_lemma: "x#xs = zs @ y#ys \<Longrightarrow> xs >>= ys"
    1.15 +  by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)
    1.16  lemma postfix_ConsD2: "x#xs >>= y#ys \<Longrightarrow> xs >>= ys"
    1.17    by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma)
    1.18  
     2.1 --- a/src/HOL/Library/Multiset.thy	Fri Nov 25 19:09:44 2005 +0100
     2.2 +++ b/src/HOL/Library/Multiset.thy	Fri Nov 25 19:20:56 2005 +0100
     2.3 @@ -173,7 +173,7 @@
     2.4  
     2.5  lemma setsum_count_Int:
     2.6      "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
     2.7 -  apply (erule finite_induct)
     2.8 +  apply (induct rule: finite_induct)
     2.9     apply simp
    2.10    apply (simp add: Int_insert_left set_of_def)
    2.11    done
    2.12 @@ -285,7 +285,8 @@
    2.13  lemma setsum_decr:
    2.14    "finite F ==> (0::nat) < f a ==>
    2.15      setsum (f (a := f a - 1)) F = (if a\<in>F then setsum f F - 1 else setsum f F)"
    2.16 -  apply (erule finite_induct, auto)
    2.17 +  apply (induct rule: finite_induct)
    2.18 +   apply auto
    2.19    apply (drule_tac a = a in mk_disjoint_insert, auto)
    2.20    done
    2.21  
    2.22 @@ -333,22 +334,22 @@
    2.23      (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
    2.24    using rep_multiset_induct_aux by blast
    2.25  
    2.26 -theorem multiset_induct [induct type: multiset]:
    2.27 -  assumes prem1: "P {#}"
    2.28 -    and prem2: "!!M x. P M ==> P (M + {#x#})"
    2.29 +theorem multiset_induct [case_names empty add, induct type: multiset]:
    2.30 +  assumes empty: "P {#}"
    2.31 +    and add: "!!M x. P M ==> P (M + {#x#})"
    2.32    shows "P M"
    2.33  proof -
    2.34    note defns = union_def single_def Mempty_def
    2.35    show ?thesis
    2.36      apply (rule Rep_multiset_inverse [THEN subst])
    2.37      apply (rule Rep_multiset [THEN rep_multiset_induct])
    2.38 -     apply (rule prem1 [unfolded defns])
    2.39 +     apply (rule empty [unfolded defns])
    2.40      apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))")
    2.41       prefer 2
    2.42       apply (simp add: expand_fun_eq)
    2.43      apply (erule ssubst)
    2.44      apply (erule Abs_multiset_inverse [THEN subst])
    2.45 -    apply (erule prem2 [unfolded defns, simplified])
    2.46 +    apply (erule add [unfolded defns, simplified])
    2.47      done
    2.48  qed
    2.49  
    2.50 @@ -402,21 +403,21 @@
    2.51    let ?case1 = "?case1 {(N, M). ?R N M}"
    2.52  
    2.53    assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}"
    2.54 -  hence "\<exists>a' M0' K.
    2.55 +  then have "\<exists>a' M0' K.
    2.56        M0 + {#a#} = M0' + {#a'#} \<and> N = M0' + K \<and> ?r K a'" by simp
    2.57 -  thus "?case1 \<or> ?case2"
    2.58 +  then show "?case1 \<or> ?case2"
    2.59    proof (elim exE conjE)
    2.60      fix a' M0' K
    2.61      assume N: "N = M0' + K" and r: "?r K a'"
    2.62      assume "M0 + {#a#} = M0' + {#a'#}"
    2.63 -    hence "M0 = M0' \<and> a = a' \<or>
    2.64 +    then have "M0 = M0' \<and> a = a' \<or>
    2.65          (\<exists>K'. M0 = K' + {#a'#} \<and> M0' = K' + {#a#})"
    2.66        by (simp only: add_eq_conv_ex)
    2.67 -    thus ?thesis
    2.68 +    then show ?thesis
    2.69      proof (elim disjE conjE exE)
    2.70        assume "M0 = M0'" "a = a'"
    2.71        with N r have "?r K a \<and> N = M0 + K" by simp
    2.72 -      hence ?case2 .. thus ?thesis ..
    2.73 +      then have ?case2 .. then show ?thesis ..
    2.74      next
    2.75        fix K'
    2.76        assume "M0' = K' + {#a#}"
    2.77 @@ -424,7 +425,7 @@
    2.78  
    2.79        assume "M0 = K' + {#a'#}"
    2.80        with r have "?R (K' + K) M0" by blast
    2.81 -      with n have ?case1 by simp thus ?thesis ..
    2.82 +      with n have ?case1 by simp then show ?thesis ..
    2.83      qed
    2.84    qed
    2.85  qed
    2.86 @@ -442,38 +443,32 @@
    2.87      proof (rule accI [of "M0 + {#a#}"])
    2.88        fix N
    2.89        assume "(N, M0 + {#a#}) \<in> ?R"
    2.90 -      hence "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or>
    2.91 +      then have "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or>
    2.92            (\<exists>K. (\<forall>b. b :# K --> (b, a) \<in> r) \<and> N = M0 + K))"
    2.93          by (rule less_add)
    2.94 -      thus "N \<in> ?W"
    2.95 +      then show "N \<in> ?W"
    2.96        proof (elim exE disjE conjE)
    2.97          fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}"
    2.98          from acc_hyp have "(M, M0) \<in> ?R --> M + {#a#} \<in> ?W" ..
    2.99 -        hence "M + {#a#} \<in> ?W" ..
   2.100 -        thus "N \<in> ?W" by (simp only: N)
   2.101 +        then have "M + {#a#} \<in> ?W" ..
   2.102 +        then show "N \<in> ?W" by (simp only: N)
   2.103        next
   2.104          fix K
   2.105          assume N: "N = M0 + K"
   2.106          assume "\<forall>b. b :# K --> (b, a) \<in> r"
   2.107 -        have "?this --> M0 + K \<in> ?W" (is "?P K")
   2.108 +	then have "M0 + K \<in> ?W"
   2.109          proof (induct K)
   2.110 -          from M0 have "M0 + {#} \<in> ?W" by simp
   2.111 -          thus "?P {#}" ..
   2.112 -
   2.113 -          fix K x assume hyp: "?P K"
   2.114 -          show "?P (K + {#x#})"
   2.115 -          proof
   2.116 -            assume a: "\<forall>b. b :# (K + {#x#}) --> (b, a) \<in> r"
   2.117 -            hence "(x, a) \<in> r" by simp
   2.118 -            with wf_hyp have b: "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
   2.119 -
   2.120 -            from a hyp have "M0 + K \<in> ?W" by simp
   2.121 -            with b have "(M0 + K) + {#x#} \<in> ?W" ..
   2.122 -            thus "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc)
   2.123 -          qed
   2.124 +	  case empty
   2.125 +          from M0 show "M0 + {#} \<in> ?W" by simp
   2.126 +	next
   2.127 +	  case (add K x)
   2.128 +	  from add.prems have "(x, a) \<in> r" by simp
   2.129 +          with wf_hyp have "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
   2.130 +	  moreover from add have "M0 + K \<in> ?W" by simp
   2.131 +          ultimately have "(M0 + K) + {#x#} \<in> ?W" ..
   2.132 +          then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc)
   2.133          qed
   2.134 -        hence "M0 + K \<in> ?W" ..
   2.135 -        thus "N \<in> ?W" by (simp only: N)
   2.136 +	then show "N \<in> ?W" by (simp only: N)
   2.137        qed
   2.138      qed
   2.139    } note tedious_reasoning = this
   2.140 @@ -496,11 +491,11 @@
   2.141        show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
   2.142        proof
   2.143          fix M assume "M \<in> ?W"
   2.144 -        thus "M + {#a#} \<in> ?W"
   2.145 +        then show "M + {#a#} \<in> ?W"
   2.146            by (rule acc_induct) (rule tedious_reasoning)
   2.147        qed
   2.148      qed
   2.149 -    thus "M + {#a#} \<in> ?W" ..
   2.150 +    then show "M + {#a#} \<in> ?W" ..
   2.151    qed
   2.152  qed
   2.153  
   2.154 @@ -616,8 +611,8 @@
   2.155  *}
   2.156  
   2.157  lemma mult_irrefl_aux:
   2.158 -    "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) --> A = {}"
   2.159 -  apply (erule finite_induct)
   2.160 +    "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}"
   2.161 +  apply (induct rule: finite_induct)
   2.162     apply (auto intro: order_less_trans)
   2.163    done
   2.164  
   2.165 @@ -731,11 +726,11 @@
   2.166  lemma union_upper1: "A <= A + (B::'a::order multiset)"
   2.167  proof -
   2.168    have "A + {#} <= A + B" by (blast intro: union_le_mono)
   2.169 -  thus ?thesis by simp
   2.170 +  then show ?thesis by simp
   2.171  qed
   2.172  
   2.173  lemma union_upper2: "B <= A + (B::'a::order multiset)"
   2.174 -by (subst union_commute, rule union_upper1)
   2.175 +  by (subst union_commute) (rule union_upper1)
   2.176  
   2.177  
   2.178  subsection {* Link with lists *}
   2.179 @@ -747,21 +742,21 @@
   2.180    "multiset_of (a # x) = multiset_of x + {# a #}"
   2.181  
   2.182  lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
   2.183 -  by (induct_tac x, auto)
   2.184 +  by (induct x) auto
   2.185  
   2.186  lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
   2.187 -  by (induct_tac x, auto)
   2.188 +  by (induct x) auto
   2.189  
   2.190  lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
   2.191 -  by (induct_tac x, auto)
   2.192 +  by (induct x) auto
   2.193  
   2.194  lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
   2.195    by (induct xs) auto
   2.196  
   2.197 -lemma multiset_of_append[simp]:
   2.198 -  "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
   2.199 -  by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac)
   2.200 -
   2.201 +lemma multiset_of_append [simp]:
   2.202 +    "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
   2.203 +  by (induct xs fixing: ys) (auto simp: union_ac)
   2.204 +  
   2.205  lemma surj_multiset_of: "surj multiset_of"
   2.206    apply (unfold surj_def, rule allI)
   2.207    apply (rule_tac M=y in multiset_induct, auto)
   2.208 @@ -769,11 +764,11 @@
   2.209    done
   2.210  
   2.211  lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}"
   2.212 -  by (induct_tac x, auto)
   2.213 +  by (induct x) auto
   2.214  
   2.215  lemma distinct_count_atmost_1:
   2.216     "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
   2.217 -   apply ( induct_tac x, simp, rule iffI, simp_all)
   2.218 +   apply (induct x, simp, rule iffI, simp_all)
   2.219     apply (rule conjI)
   2.220     apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
   2.221     apply (erule_tac x=a in allE, simp, clarify)
   2.222 @@ -798,13 +793,13 @@
   2.223    apply simp
   2.224    done
   2.225  
   2.226 -lemma multiset_of_compl_union[simp]:
   2.227 - "multiset_of [x\<in>xs. P x] + multiset_of [x\<in>xs. \<not>P x] = multiset_of xs"
   2.228 +lemma multiset_of_compl_union [simp]:
   2.229 +    "multiset_of [x\<in>xs. P x] + multiset_of [x\<in>xs. \<not>P x] = multiset_of xs"
   2.230    by (induct xs) (auto simp: union_ac)
   2.231  
   2.232  lemma count_filter:
   2.233 -  "count (multiset_of xs) x = length [y \<in> xs. y = x]"
   2.234 -  by (induct xs, auto)
   2.235 +    "count (multiset_of xs) x = length [y \<in> xs. y = x]"
   2.236 +  by (induct xs) auto
   2.237  
   2.238  
   2.239  subsection {* Pointwise ordering induced by count *}