# HG changeset patch
# User wenzelm
# Date 1436213162 -7200
# Node ID 17ba2df56dee0eb041a05ca34cdf10fef97cc7fa
# Parent  7109b66ba151d9daae401ff5956a03ddd65f779b
tuned proofs;

diff -r 7109b66ba151 -r 17ba2df56dee src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Jul 06 21:36:52 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Jul 06 22:06:02 2015 +0200
@@ -92,7 +92,7 @@
 by (rule diff_preserves_multiset)
 
 instance
-  by default (transfer, simp add: fun_eq_iff)+
+  by (standard; transfer; simp add: fun_eq_iff)
 
 end
 
@@ -126,7 +126,7 @@
 begin
 
 instance
-  by default (transfer; simp add: fun_eq_iff)
+  by (standard; transfer; simp add: fun_eq_iff)
 
 end
 
@@ -247,7 +247,7 @@
   by (auto simp add: add_eq_conv_diff)
 
 lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
-  by (rule_tac x = "M - {#x#}" in exI, simp)
+  by (rule exI [where x = "M - {#x#}"]) simp
 
 lemma multiset_add_sub_el_shuffle:
   assumes "c \<in># B"
@@ -277,18 +277,20 @@
 notation (xsymbols) subset_mset (infix "\<subset>#" 50)
 
 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
-  by default (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
+  by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
 
 lemma mset_less_eqI: "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le># B"
   by (simp add: subseteq_mset_def)
 
 lemma mset_le_exists_conv: "(A::'a multiset) \<le># B \<longleftrightarrow> (\<exists>C. B = A + C)"
-apply (unfold subseteq_mset_def, rule iffI, rule_tac x = "B - A" in exI)
-apply (auto intro: multiset_eq_iff [THEN iffD2])
-done
+  unfolding subseteq_mset_def
+  apply (rule iffI)
+   apply (rule exI [where x = "B - A"])
+   apply (auto intro: multiset_eq_iff [THEN iffD2])
+  done
 
 interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" "op -" 0 "op \<le>#" "op <#"
-  by default (simp, fact mset_le_exists_conv)
+  by standard (simp, fact mset_le_exists_conv)
 
 lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B"
   by (fact subset_mset.add_le_cancel_right)
@@ -323,13 +325,13 @@
 
 lemma mset_lessD: "A <# B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
 apply (clarsimp simp: subset_mset_def subseteq_mset_def)
-apply (erule_tac x=x in allE)
+apply (erule allE [where x = x])
 apply auto
 done
 
 lemma mset_leD: "A \<le># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
 apply (clarsimp simp: subset_mset_def subseteq_mset_def)
-apply (erule_tac x = x in allE)
+apply (erule allE [where x = x])
 apply auto
 done
 
@@ -380,9 +382,10 @@
 
 interpretation subset_mset: semilattice_inf inf_subset_mset "op \<le>#" "op <#"
 proof -
-   have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
-   show "class.semilattice_inf op #\<inter> op \<le># op <#"
-     by default (auto simp add: multiset_inter_def subseteq_mset_def aux)
+  have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat
+    by arith
+  show "class.semilattice_inf op #\<inter> op \<le># op <#"
+    by standard (auto simp add: multiset_inter_def subseteq_mset_def)
 qed
 
 
@@ -427,14 +430,16 @@
 
 
 subsubsection \<open>Bounded union\<close>
-definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)  where
-  "sup_subset_mset A B = A + (B - A)"
+
+definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)
+  where "sup_subset_mset A B = A + (B - A)"
 
 interpretation subset_mset: semilattice_sup sup_subset_mset "op \<le>#" "op <#"
 proof -
-  have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" by arith
+  have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
+    by arith
   show "class.semilattice_sup op #\<union> op \<le># op <#"
-    by default (auto simp add: sup_subset_mset_def subseteq_mset_def aux)
+    by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
 qed
 
 lemma sup_subset_mset_count [simp]: "count (A #\<union> B) x = max (count A x) (count B x)"
@@ -969,13 +974,15 @@
 
 lemma distinct_count_atmost_1:
   "distinct x = (\<forall>a. count (mset x) a = (if a \<in> set x then 1 else 0))"
-apply (induct x, simp, rule iffI, simp_all)
-apply (rename_tac a b)
-apply (rule conjI)
-apply (simp_all add: set_mset_mset [THEN sym] del: set_mset_mset)
-apply (erule_tac x = a in allE, simp, clarify)
-apply (erule_tac x = aa in allE, simp)
-done
+  apply (induct x, simp, rule iffI, simp_all)
+  subgoal for a b
+    apply (rule conjI)
+    apply (simp_all add: set_mset_mset [symmetric] del: set_mset_mset)
+    apply (erule_tac x = a in allE, simp)
+    apply clarify
+    apply (erule_tac x = aa in allE, simp)
+    done
+  done
 
 lemma mset_eq_setD: "mset xs = mset ys \<Longrightarrow> set xs = set ys"
 by (rule) (auto simp add:multiset_eq_iff set_count_greater_0)
@@ -998,14 +1005,16 @@
   by (induct xs) (auto simp: ac_simps)
 
 lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
-apply (induct ls arbitrary: i)
- apply simp
-apply (case_tac i)
- apply auto
-done
+proof (induct ls arbitrary: i)
+  case Nil
+  then show ?case by simp
+next
+  case Cons
+  then show ?case by (cases i) auto
+qed
 
 lemma mset_remove1[simp]: "mset (remove1 a xs) = mset xs - {#a#}"
-by (induct xs) (auto simp add: multiset_eq_iff)
+  by (induct xs) (auto simp add: multiset_eq_iff)
 
 lemma mset_eq_length:
   assumes "mset xs = mset ys"
@@ -1023,15 +1032,20 @@
   shows "List.fold f xs = List.fold f ys"
   using f equiv [symmetric]
 proof (induct xs arbitrary: ys)
-  case Nil then show ?case by simp
+  case Nil
+  then show ?case by simp
 next
   case (Cons x xs)
-  then have *: "set ys = set (x # xs)" by (blast dest: mset_eq_setD)
+  then have *: "set ys = set (x # xs)"
+    by (blast dest: mset_eq_setD)
   have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
     by (rule Cons.prems(1)) (simp_all add: *)
-  moreover from * have "x \<in> set ys" by simp
-  ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
-  moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)" by (auto intro: Cons.hyps)
+  moreover from * have "x \<in> set ys"
+    by simp
+  ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x"
+    by (fact fold_remove1_split)
+  moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)"
+    by (auto intro: Cons.hyps)
   ultimately show ?case by simp
 qed
 
@@ -1049,8 +1063,10 @@
 where
   "folding.F (\<lambda>x M. {#x#} + M) {#} = mset_set"
 proof -
-  interpret comp_fun_commute "\<lambda>x M. {#x#} + M" by default (simp add: fun_eq_iff ac_simps)
-  show "folding (\<lambda>x M. {#x#} + M)" by default (fact comp_fun_commute)
+  interpret comp_fun_commute "\<lambda>x M. {#x#} + M"
+    by standard (simp add: fun_eq_iff ac_simps)
+  show "folding (\<lambda>x M. {#x#} + M)"
+    by standard (fact comp_fun_commute)
   from mset_set_def show "folding.F (\<lambda>x M. {#x#} + M) {#} = mset_set" ..
 qed
 
@@ -1138,25 +1154,25 @@
 lemma empty [simp]: "F {#} = 1"
   by (simp add: eq_fold)
 
-lemma singleton [simp]:
-  "F {#x#} = x"
+lemma singleton [simp]: "F {#x#} = x"
 proof -
   interpret comp_fun_commute
-    by default (simp add: fun_eq_iff left_commute)
+    by standard (simp add: fun_eq_iff left_commute)
   show ?thesis by (simp add: eq_fold)
 qed
 
 lemma union [simp]: "F (M + N) = F M * F N"
 proof -
   interpret comp_fun_commute f
-    by default (simp add: fun_eq_iff left_commute)
-  show ?thesis by (induct N) (simp_all add: left_commute eq_fold)
+    by standard (simp add: fun_eq_iff left_commute)
+  show ?thesis
+    by (induct N) (simp_all add: left_commute eq_fold)
 qed
 
 end
 
 lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + \<Colon> 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
-  by default (simp add: add_ac comp_def)
+  by standard (simp add: add_ac comp_def)
 
 declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp]
 
@@ -1364,11 +1380,12 @@
 proof (rule properties_for_sort_key)
   from multiset show "mset ys = mset xs" .
   from \<open>sorted ys\<close> show "sorted (map (\<lambda>x. x) ys)" by simp
-  from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)"
+  from multiset have "length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)" for k
     by (rule mset_eq_length_filter)
-  then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
+  then have "replicate (length (filter (\<lambda>y. k = y) ys)) k =
+    replicate (length (filter (\<lambda>x. k = x) xs)) k" for k
     by simp
-  then show "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
+  then show "k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs" for k
     by (simp add: replicate_length_filter)
 qed
 
@@ -1653,10 +1670,10 @@
 done
 
 lemma one_step_implies_mult_aux:
-  "trans r \<Longrightarrow>
-    \<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)
-      \<longrightarrow> (I + K, I + J) \<in> mult r"
-apply (induct_tac n, auto)
+  "\<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)
+    \<longrightarrow> (I + K, I + J) \<in> mult r"
+apply (induct n)
+ apply auto
 apply (frule size_eq_Suc_imp_eq_union, clarify)
 apply (rename_tac "J'", simp)
 apply (erule notE, auto)
@@ -1714,20 +1731,22 @@
       by (rule mult_implies_one_step)
     then obtain I J K where "M = I + J" and "M = I + K"
       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
-    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
+    then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
     have "finite (set_mset K)" by simp
-    moreover note aux2
+    moreover note **
     ultimately have "set_mset K = {}"
       by (induct rule: finite_induct) (auto intro: order_less_trans)
-    with aux1 show False by simp
+    with * show False by simp
   qed
-  have trans: "\<And>K M N :: 'a multiset. K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># N"
+  have trans: "K #\<subset># M \<Longrightarrow> M #\<subset># N \<Longrightarrow> K #\<subset># N" for K M N :: "'a multiset"
     unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
   show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
-    by default (auto simp add: le_multiset_def irrefl dest: trans)
+    by standard (auto simp add: le_multiset_def irrefl dest: trans)
 qed
 
-lemma mult_less_irrefl [elim!]: "M #\<subset># (M::'a::order multiset) \<Longrightarrow> R"
+lemma mult_less_irrefl [elim!]:
+  fixes M :: "'a::order multiset"
+  shows "M #\<subset># M \<Longrightarrow> R"
   by simp
 
 
@@ -1760,7 +1779,7 @@
   by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans)
 
 interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset
-  by default (auto simp add: le_multiset_def intro: union_less_mono2)
+  by standard (auto simp add: le_multiset_def intro: union_less_mono2)
 
 
 subsubsection \<open>Termination proofs with multiset orders\<close>
@@ -2119,7 +2138,8 @@
   using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
 
 instance
-  by default (simp add: equal_multiset_def)
+  by standard (simp add: equal_multiset_def)
+
 end
 
 lemma [code]: "msetsum (mset xs) = listsum xs"
@@ -2198,7 +2218,7 @@
   next
     case False
     then obtain k where k: "j = Suc k"
-      by (case_tac j) simp
+      by (cases j) simp
     hence "k \<le> length xs"
       using Cons.prems by auto
     hence "mset (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
@@ -2298,9 +2318,10 @@
   show "rel_mset R OO rel_mset S \<le> rel_mset (R OO S)" for R S
     unfolding rel_mset_def[abs_def] OO_def
     apply clarify
-    apply (rename_tac X Z Y xs ys' ys zs)
-    apply (drule_tac xs = ys' and ys = zs and xs' = ys in list_all2_reorder_left_invariance)
-    apply (auto intro: list_all2_trans)
+    subgoal for X Z Y xs ys' ys zs
+      apply (drule list_all2_reorder_left_invariance [where xs = ys' and ys = zs and xs' = ys])
+      apply (auto intro: list_all2_trans)
+      done
     done
   show "rel_mset R =
     (BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
@@ -2355,17 +2376,16 @@
 qed
 
 lemma rel_mset'_imp_rel_mset: "rel_mset' R M N \<Longrightarrow> rel_mset R M N"
-apply(induct rule: rel_mset'.induct)
-using rel_mset_Zero rel_mset_Plus by auto
+  by (induct rule: rel_mset'.induct) (auto simp: rel_mset_Zero rel_mset_Plus)
 
 lemma rel_mset_size: "rel_mset R M N \<Longrightarrow> size M = size N"
-unfolding multiset.rel_compp_Grp Grp_def by auto
+  unfolding multiset.rel_compp_Grp Grp_def by auto
 
 lemma multiset_induct2[case_names empty addL addR]:
-assumes empty: "P {#} {#}"
-and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
-and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
-shows "P M N"
+  assumes empty: "P {#} {#}"
+    and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
+    and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
+  shows "P M N"
 apply(induct N rule: multiset_induct)
   apply(induct M rule: multiset_induct, rule empty, erule addL)
   apply(induct M rule: multiset_induct, erule addR, erule addR)
@@ -2376,7 +2396,8 @@
     and empty: "P {#} {#}"
     and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
   shows "P M N"
-using c proof(induct M arbitrary: N rule: measure_induct_rule[of size])
+  using c
+proof (induct M arbitrary: N rule: measure_induct_rule[of size])
   case (less M)
   show ?case
   proof(cases "M = {#}")
@@ -2470,7 +2491,7 @@
 qed
 
 lemma rel_mset_rel_mset': "rel_mset R M N = rel_mset' R M N"
-using rel_mset_imp_rel_mset' rel_mset'_imp_rel_mset by auto
+  using rel_mset_imp_rel_mset' rel_mset'_imp_rel_mset by auto
 
 text \<open>The main end product for @{const rel_mset}: inductive characterization:\<close>
 theorems rel_mset_induct[case_names empty add, induct pred: rel_mset] =
@@ -2480,7 +2501,9 @@
 subsection \<open>Size setup\<close>
 
 lemma multiset_size_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
-  unfolding o_apply by (rule ext) (induct_tac, auto)
+  apply (rule ext)
+  subgoal for x by (induct x) auto
+  done
 
 setup \<open>
   BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}