src/HOL/Library/Multiset.thy
changeset 60678 17ba2df56dee
parent 60613 f11e9fd70b7d
child 60752 b48830b670a1
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Jul 06 21:36:52 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Jul 06 22:06:02 2015 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4  by (rule diff_preserves_multiset)
     1.5  
     1.6  instance
     1.7 -  by default (transfer, simp add: fun_eq_iff)+
     1.8 +  by (standard; transfer; simp add: fun_eq_iff)
     1.9  
    1.10  end
    1.11  
    1.12 @@ -126,7 +126,7 @@
    1.13  begin
    1.14  
    1.15  instance
    1.16 -  by default (transfer; simp add: fun_eq_iff)
    1.17 +  by (standard; transfer; simp add: fun_eq_iff)
    1.18  
    1.19  end
    1.20  
    1.21 @@ -247,7 +247,7 @@
    1.22    by (auto simp add: add_eq_conv_diff)
    1.23  
    1.24  lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
    1.25 -  by (rule_tac x = "M - {#x#}" in exI, simp)
    1.26 +  by (rule exI [where x = "M - {#x#}"]) simp
    1.27  
    1.28  lemma multiset_add_sub_el_shuffle:
    1.29    assumes "c \<in># B"
    1.30 @@ -277,18 +277,20 @@
    1.31  notation (xsymbols) subset_mset (infix "\<subset>#" 50)
    1.32  
    1.33  interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
    1.34 -  by default (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
    1.35 +  by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
    1.36  
    1.37  lemma mset_less_eqI: "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le># B"
    1.38    by (simp add: subseteq_mset_def)
    1.39  
    1.40  lemma mset_le_exists_conv: "(A::'a multiset) \<le># B \<longleftrightarrow> (\<exists>C. B = A + C)"
    1.41 -apply (unfold subseteq_mset_def, rule iffI, rule_tac x = "B - A" in exI)
    1.42 -apply (auto intro: multiset_eq_iff [THEN iffD2])
    1.43 -done
    1.44 +  unfolding subseteq_mset_def
    1.45 +  apply (rule iffI)
    1.46 +   apply (rule exI [where x = "B - A"])
    1.47 +   apply (auto intro: multiset_eq_iff [THEN iffD2])
    1.48 +  done
    1.49  
    1.50  interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" "op -" 0 "op \<le>#" "op <#"
    1.51 -  by default (simp, fact mset_le_exists_conv)
    1.52 +  by standard (simp, fact mset_le_exists_conv)
    1.53  
    1.54  lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B"
    1.55    by (fact subset_mset.add_le_cancel_right)
    1.56 @@ -323,13 +325,13 @@
    1.57  
    1.58  lemma mset_lessD: "A <# B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
    1.59  apply (clarsimp simp: subset_mset_def subseteq_mset_def)
    1.60 -apply (erule_tac x=x in allE)
    1.61 +apply (erule allE [where x = x])
    1.62  apply auto
    1.63  done
    1.64  
    1.65  lemma mset_leD: "A \<le># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
    1.66  apply (clarsimp simp: subset_mset_def subseteq_mset_def)
    1.67 -apply (erule_tac x = x in allE)
    1.68 +apply (erule allE [where x = x])
    1.69  apply auto
    1.70  done
    1.71  
    1.72 @@ -380,9 +382,10 @@
    1.73  
    1.74  interpretation subset_mset: semilattice_inf inf_subset_mset "op \<le>#" "op <#"
    1.75  proof -
    1.76 -   have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
    1.77 -   show "class.semilattice_inf op #\<inter> op \<le># op <#"
    1.78 -     by default (auto simp add: multiset_inter_def subseteq_mset_def aux)
    1.79 +  have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat
    1.80 +    by arith
    1.81 +  show "class.semilattice_inf op #\<inter> op \<le># op <#"
    1.82 +    by standard (auto simp add: multiset_inter_def subseteq_mset_def)
    1.83  qed
    1.84  
    1.85  
    1.86 @@ -427,14 +430,16 @@
    1.87  
    1.88  
    1.89  subsubsection \<open>Bounded union\<close>
    1.90 -definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)  where
    1.91 -  "sup_subset_mset A B = A + (B - A)"
    1.92 +
    1.93 +definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)
    1.94 +  where "sup_subset_mset A B = A + (B - A)"
    1.95  
    1.96  interpretation subset_mset: semilattice_sup sup_subset_mset "op \<le>#" "op <#"
    1.97  proof -
    1.98 -  have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" by arith
    1.99 +  have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
   1.100 +    by arith
   1.101    show "class.semilattice_sup op #\<union> op \<le># op <#"
   1.102 -    by default (auto simp add: sup_subset_mset_def subseteq_mset_def aux)
   1.103 +    by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
   1.104  qed
   1.105  
   1.106  lemma sup_subset_mset_count [simp]: "count (A #\<union> B) x = max (count A x) (count B x)"
   1.107 @@ -969,13 +974,15 @@
   1.108  
   1.109  lemma distinct_count_atmost_1:
   1.110    "distinct x = (\<forall>a. count (mset x) a = (if a \<in> set x then 1 else 0))"
   1.111 -apply (induct x, simp, rule iffI, simp_all)
   1.112 -apply (rename_tac a b)
   1.113 -apply (rule conjI)
   1.114 -apply (simp_all add: set_mset_mset [THEN sym] del: set_mset_mset)
   1.115 -apply (erule_tac x = a in allE, simp, clarify)
   1.116 -apply (erule_tac x = aa in allE, simp)
   1.117 -done
   1.118 +  apply (induct x, simp, rule iffI, simp_all)
   1.119 +  subgoal for a b
   1.120 +    apply (rule conjI)
   1.121 +    apply (simp_all add: set_mset_mset [symmetric] del: set_mset_mset)
   1.122 +    apply (erule_tac x = a in allE, simp)
   1.123 +    apply clarify
   1.124 +    apply (erule_tac x = aa in allE, simp)
   1.125 +    done
   1.126 +  done
   1.127  
   1.128  lemma mset_eq_setD: "mset xs = mset ys \<Longrightarrow> set xs = set ys"
   1.129  by (rule) (auto simp add:multiset_eq_iff set_count_greater_0)
   1.130 @@ -998,14 +1005,16 @@
   1.131    by (induct xs) (auto simp: ac_simps)
   1.132  
   1.133  lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
   1.134 -apply (induct ls arbitrary: i)
   1.135 - apply simp
   1.136 -apply (case_tac i)
   1.137 - apply auto
   1.138 -done
   1.139 +proof (induct ls arbitrary: i)
   1.140 +  case Nil
   1.141 +  then show ?case by simp
   1.142 +next
   1.143 +  case Cons
   1.144 +  then show ?case by (cases i) auto
   1.145 +qed
   1.146  
   1.147  lemma mset_remove1[simp]: "mset (remove1 a xs) = mset xs - {#a#}"
   1.148 -by (induct xs) (auto simp add: multiset_eq_iff)
   1.149 +  by (induct xs) (auto simp add: multiset_eq_iff)
   1.150  
   1.151  lemma mset_eq_length:
   1.152    assumes "mset xs = mset ys"
   1.153 @@ -1023,15 +1032,20 @@
   1.154    shows "List.fold f xs = List.fold f ys"
   1.155    using f equiv [symmetric]
   1.156  proof (induct xs arbitrary: ys)
   1.157 -  case Nil then show ?case by simp
   1.158 +  case Nil
   1.159 +  then show ?case by simp
   1.160  next
   1.161    case (Cons x xs)
   1.162 -  then have *: "set ys = set (x # xs)" by (blast dest: mset_eq_setD)
   1.163 +  then have *: "set ys = set (x # xs)"
   1.164 +    by (blast dest: mset_eq_setD)
   1.165    have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
   1.166      by (rule Cons.prems(1)) (simp_all add: *)
   1.167 -  moreover from * have "x \<in> set ys" by simp
   1.168 -  ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
   1.169 -  moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)" by (auto intro: Cons.hyps)
   1.170 +  moreover from * have "x \<in> set ys"
   1.171 +    by simp
   1.172 +  ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x"
   1.173 +    by (fact fold_remove1_split)
   1.174 +  moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)"
   1.175 +    by (auto intro: Cons.hyps)
   1.176    ultimately show ?case by simp
   1.177  qed
   1.178  
   1.179 @@ -1049,8 +1063,10 @@
   1.180  where
   1.181    "folding.F (\<lambda>x M. {#x#} + M) {#} = mset_set"
   1.182  proof -
   1.183 -  interpret comp_fun_commute "\<lambda>x M. {#x#} + M" by default (simp add: fun_eq_iff ac_simps)
   1.184 -  show "folding (\<lambda>x M. {#x#} + M)" by default (fact comp_fun_commute)
   1.185 +  interpret comp_fun_commute "\<lambda>x M. {#x#} + M"
   1.186 +    by standard (simp add: fun_eq_iff ac_simps)
   1.187 +  show "folding (\<lambda>x M. {#x#} + M)"
   1.188 +    by standard (fact comp_fun_commute)
   1.189    from mset_set_def show "folding.F (\<lambda>x M. {#x#} + M) {#} = mset_set" ..
   1.190  qed
   1.191  
   1.192 @@ -1138,25 +1154,25 @@
   1.193  lemma empty [simp]: "F {#} = 1"
   1.194    by (simp add: eq_fold)
   1.195  
   1.196 -lemma singleton [simp]:
   1.197 -  "F {#x#} = x"
   1.198 +lemma singleton [simp]: "F {#x#} = x"
   1.199  proof -
   1.200    interpret comp_fun_commute
   1.201 -    by default (simp add: fun_eq_iff left_commute)
   1.202 +    by standard (simp add: fun_eq_iff left_commute)
   1.203    show ?thesis by (simp add: eq_fold)
   1.204  qed
   1.205  
   1.206  lemma union [simp]: "F (M + N) = F M * F N"
   1.207  proof -
   1.208    interpret comp_fun_commute f
   1.209 -    by default (simp add: fun_eq_iff left_commute)
   1.210 -  show ?thesis by (induct N) (simp_all add: left_commute eq_fold)
   1.211 +    by standard (simp add: fun_eq_iff left_commute)
   1.212 +  show ?thesis
   1.213 +    by (induct N) (simp_all add: left_commute eq_fold)
   1.214  qed
   1.215  
   1.216  end
   1.217  
   1.218  lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + \<Colon> 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
   1.219 -  by default (simp add: add_ac comp_def)
   1.220 +  by standard (simp add: add_ac comp_def)
   1.221  
   1.222  declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp]
   1.223  
   1.224 @@ -1364,11 +1380,12 @@
   1.225  proof (rule properties_for_sort_key)
   1.226    from multiset show "mset ys = mset xs" .
   1.227    from \<open>sorted ys\<close> show "sorted (map (\<lambda>x. x) ys)" by simp
   1.228 -  from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)"
   1.229 +  from multiset have "length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)" for k
   1.230      by (rule mset_eq_length_filter)
   1.231 -  then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
   1.232 +  then have "replicate (length (filter (\<lambda>y. k = y) ys)) k =
   1.233 +    replicate (length (filter (\<lambda>x. k = x) xs)) k" for k
   1.234      by simp
   1.235 -  then show "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
   1.236 +  then show "k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs" for k
   1.237      by (simp add: replicate_length_filter)
   1.238  qed
   1.239  
   1.240 @@ -1653,10 +1670,10 @@
   1.241  done
   1.242  
   1.243  lemma one_step_implies_mult_aux:
   1.244 -  "trans r \<Longrightarrow>
   1.245 -    \<forall>I J K. size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)
   1.246 -      \<longrightarrow> (I + K, I + J) \<in> mult r"
   1.247 -apply (induct_tac n, auto)
   1.248 +  "\<forall>I J K. size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)
   1.249 +    \<longrightarrow> (I + K, I + J) \<in> mult r"
   1.250 +apply (induct n)
   1.251 + apply auto
   1.252  apply (frule size_eq_Suc_imp_eq_union, clarify)
   1.253  apply (rename_tac "J'", simp)
   1.254  apply (erule notE, auto)
   1.255 @@ -1714,20 +1731,22 @@
   1.256        by (rule mult_implies_one_step)
   1.257      then obtain I J K where "M = I + J" and "M = I + K"
   1.258        and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
   1.259 -    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
   1.260 +    then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
   1.261      have "finite (set_mset K)" by simp
   1.262 -    moreover note aux2
   1.263 +    moreover note **
   1.264      ultimately have "set_mset K = {}"
   1.265        by (induct rule: finite_induct) (auto intro: order_less_trans)
   1.266 -    with aux1 show False by simp
   1.267 +    with * show False by simp
   1.268    qed
   1.269 -  have trans: "\<And>K M N :: 'a multiset. K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># N"
   1.270 +  have trans: "K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># N" for K M N :: "'a multiset"
   1.271      unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
   1.272    show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
   1.273 -    by default (auto simp add: le_multiset_def irrefl dest: trans)
   1.274 +    by standard (auto simp add: le_multiset_def irrefl dest: trans)
   1.275  qed
   1.276  
   1.277 -lemma mult_less_irrefl [elim!]: "M #\<subset># (M::'a::order multiset) \<Longrightarrow> R"
   1.278 +lemma mult_less_irrefl [elim!]:
   1.279 +  fixes M :: "'a::order multiset"
   1.280 +  shows "M #\<subset># M \<Longrightarrow> R"
   1.281    by simp
   1.282  
   1.283  
   1.284 @@ -1760,7 +1779,7 @@
   1.285    by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans)
   1.286  
   1.287  interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset
   1.288 -  by default (auto simp add: le_multiset_def intro: union_less_mono2)
   1.289 +  by standard (auto simp add: le_multiset_def intro: union_less_mono2)
   1.290  
   1.291  
   1.292  subsubsection \<open>Termination proofs with multiset orders\<close>
   1.293 @@ -2119,7 +2138,8 @@
   1.294    using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   1.295  
   1.296  instance
   1.297 -  by default (simp add: equal_multiset_def)
   1.298 +  by standard (simp add: equal_multiset_def)
   1.299 +
   1.300  end
   1.301  
   1.302  lemma [code]: "msetsum (mset xs) = listsum xs"
   1.303 @@ -2198,7 +2218,7 @@
   1.304    next
   1.305      case False
   1.306      then obtain k where k: "j = Suc k"
   1.307 -      by (case_tac j) simp
   1.308 +      by (cases j) simp
   1.309      hence "k \<le> length xs"
   1.310        using Cons.prems by auto
   1.311      hence "mset (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
   1.312 @@ -2298,9 +2318,10 @@
   1.313    show "rel_mset R OO rel_mset S \<le> rel_mset (R OO S)" for R S
   1.314      unfolding rel_mset_def[abs_def] OO_def
   1.315      apply clarify
   1.316 -    apply (rename_tac X Z Y xs ys' ys zs)
   1.317 -    apply (drule_tac xs = ys' and ys = zs and xs' = ys in list_all2_reorder_left_invariance)
   1.318 -    apply (auto intro: list_all2_trans)
   1.319 +    subgoal for X Z Y xs ys' ys zs
   1.320 +      apply (drule list_all2_reorder_left_invariance [where xs = ys' and ys = zs and xs' = ys])
   1.321 +      apply (auto intro: list_all2_trans)
   1.322 +      done
   1.323      done
   1.324    show "rel_mset R =
   1.325      (BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
   1.326 @@ -2355,17 +2376,16 @@
   1.327  qed
   1.328  
   1.329  lemma rel_mset'_imp_rel_mset: "rel_mset' R M N \<Longrightarrow> rel_mset R M N"
   1.330 -apply(induct rule: rel_mset'.induct)
   1.331 -using rel_mset_Zero rel_mset_Plus by auto
   1.332 +  by (induct rule: rel_mset'.induct) (auto simp: rel_mset_Zero rel_mset_Plus)
   1.333  
   1.334  lemma rel_mset_size: "rel_mset R M N \<Longrightarrow> size M = size N"
   1.335 -unfolding multiset.rel_compp_Grp Grp_def by auto
   1.336 +  unfolding multiset.rel_compp_Grp Grp_def by auto
   1.337  
   1.338  lemma multiset_induct2[case_names empty addL addR]:
   1.339 -assumes empty: "P {#} {#}"
   1.340 -and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
   1.341 -and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
   1.342 -shows "P M N"
   1.343 +  assumes empty: "P {#} {#}"
   1.344 +    and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
   1.345 +    and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
   1.346 +  shows "P M N"
   1.347  apply(induct N rule: multiset_induct)
   1.348    apply(induct M rule: multiset_induct, rule empty, erule addL)
   1.349    apply(induct M rule: multiset_induct, erule addR, erule addR)
   1.350 @@ -2376,7 +2396,8 @@
   1.351      and empty: "P {#} {#}"
   1.352      and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
   1.353    shows "P M N"
   1.354 -using c proof(induct M arbitrary: N rule: measure_induct_rule[of size])
   1.355 +  using c
   1.356 +proof (induct M arbitrary: N rule: measure_induct_rule[of size])
   1.357    case (less M)
   1.358    show ?case
   1.359    proof(cases "M = {#}")
   1.360 @@ -2470,7 +2491,7 @@
   1.361  qed
   1.362  
   1.363  lemma rel_mset_rel_mset': "rel_mset R M N = rel_mset' R M N"
   1.364 -using rel_mset_imp_rel_mset' rel_mset'_imp_rel_mset by auto
   1.365 +  using rel_mset_imp_rel_mset' rel_mset'_imp_rel_mset by auto
   1.366  
   1.367  text \<open>The main end product for @{const rel_mset}: inductive characterization:\<close>
   1.368  theorems rel_mset_induct[case_names empty add, induct pred: rel_mset] =
   1.369 @@ -2480,7 +2501,9 @@
   1.370  subsection \<open>Size setup\<close>
   1.371  
   1.372  lemma multiset_size_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
   1.373 -  unfolding o_apply by (rule ext) (induct_tac, auto)
   1.374 +  apply (rule ext)
   1.375 +  subgoal for x by (induct x) auto
   1.376 +  done
   1.377  
   1.378  setup \<open>
   1.379    BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}