author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 58424 cbbba613b6ab child 58426 cac802846ff1
simpler proof
```     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Sep 24 11:09:05 2014 +0200
1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Sep 24 15:45:55 2014 +0200
1.3 @@ -128,7 +128,7 @@
1.4
1.5  lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
1.6  by (rule diff_preserves_multiset)
1.7 -
1.8 +
1.9  instance
1.10  by default (transfer, simp add: fun_eq_iff)+
1.11
1.12 @@ -156,7 +156,7 @@
1.14    "(M::'a multiset) - (N + Q) = M - N - Q"
1.15    by (rule sym) (fact diff_diff_add)
1.16 -
1.17 +
1.18  lemma insert_DiffM:
1.19    "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
1.20    by (clarsimp simp: multiset_eq_iff)
1.21 @@ -242,7 +242,7 @@
1.22    qed
1.23  qed
1.24
1.25 -lemma insert_noteq_member:
1.26 +lemma insert_noteq_member:
1.27    assumes BC: "B + {#b#} = C + {#c#}"
1.28     and bnotc: "b \<noteq> c"
1.29    shows "c \<in># B"
1.30 @@ -262,14 +262,14 @@
1.31    "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
1.32    by (rule_tac x = "M - {#x#}" in exI, simp)
1.33
1.35 -  assumes "c \<in># B" and "b \<noteq> c"
1.37 +  assumes "c \<in># B" and "b \<noteq> c"
1.38    shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
1.39  proof -
1.40 -  from `c \<in># B` obtain A where B: "B = A + {#c#}"
1.41 +  from `c \<in># B` obtain A where B: "B = A + {#c#}"
1.42      by (blast dest: multi_member_split)
1.43    have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
1.44 -  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
1.45 +  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
1.46      by (simp add: ac_simps)
1.47    then show ?thesis using B by simp
1.48  qed
1.49 @@ -351,7 +351,7 @@
1.50  apply (erule_tac x = x in allE)
1.51  apply auto
1.52  done
1.53 -
1.54 +
1.55  lemma mset_less_insertD: "(A + {#x#} < B) \<Longrightarrow> (x \<in># B \<and> A < B)"
1.56  apply (rule conjI)
1.57   apply (simp add: mset_lessD)
1.58 @@ -590,7 +590,7 @@
1.59  lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
1.60    unfolding set_of_def[symmetric] by simp
1.61
1.62 -lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"
1.63 +lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"
1.64    by (metis mset_leD subsetI mem_set_of_iff)
1.65
1.66  subsubsection {* Size *}
1.67 @@ -705,7 +705,7 @@
1.68  proof (induct A arbitrary: B)
1.69    case (empty M)
1.70    then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
1.71 -  then obtain M' x where "M = M' + {#x#}"
1.72 +  then obtain M' x where "M = M' + {#x#}"
1.73      by (blast dest: multi_nonempty_split)
1.74    then show ?case by simp
1.75  next
1.76 @@ -713,9 +713,9 @@
1.77    have IH: "\<And>B. S < B \<Longrightarrow> size S < size B" by fact
1.78    have SxsubT: "S + {#x#} < T" by fact
1.79    then have "x \<in># T" and "S < T" by (auto dest: mset_less_insertD)
1.80 -  then obtain T' where T: "T = T' + {#x#}"
1.81 +  then obtain T' where T: "T = T' + {#x#}"
1.82      by (blast dest: multi_member_split)
1.83 -  then have "S < T'" using SxsubT
1.84 +  then have "S < T'" using SxsubT
1.85      by (blast intro: mset_less_add_bothsides)
1.86    then have "size S < size T'" using IH by simp
1.87    then show ?case using T by simp
1.88 @@ -1047,7 +1047,7 @@
1.89  next
1.90    case (Cons x xs)
1.91    then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
1.92 -  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.93 +  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.94      by (rule Cons.prems(1)) (simp_all add: *)
1.95    moreover from * have "x \<in> set ys" by simp
1.96    ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
1.97 @@ -1211,15 +1211,15 @@
1.98  end
1.99
1.100  syntax
1.101 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
1.102 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
1.103        ("(3SUM _:#_. _)" [0, 51, 10] 10)
1.104
1.105  syntax (xsymbols)
1.106 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
1.107 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
1.108        ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
1.109
1.110  syntax (HTML output)
1.111 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
1.112 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
1.113        ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
1.114
1.115  translations
1.116 @@ -1249,7 +1249,7 @@
1.117    by (fact msetprod.singleton)
1.118
1.119  lemma msetprod_Un:
1.120 -  "msetprod (A + B) = msetprod A * msetprod B"
1.121 +  "msetprod (A + B) = msetprod A * msetprod B"
1.122    by (fact msetprod.union)
1.123
1.124  lemma setprod_unfold_msetprod:
1.125 @@ -1263,15 +1263,15 @@
1.126  end
1.127
1.128  syntax
1.129 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
1.130 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
1.131        ("(3PROD _:#_. _)" [0, 51, 10] 10)
1.132
1.133  syntax (xsymbols)
1.134 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
1.135 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
1.136        ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
1.137
1.138  syntax (HTML output)
1.139 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
1.140 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
1.141        ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
1.142
1.143  translations
1.144 @@ -1349,7 +1349,7 @@
1.145  lemma multiset_of_insort [simp]:
1.146    "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs"
1.147    by (induct xs) (simp_all add: ac_simps)
1.148 -
1.149 +
1.150  lemma multiset_of_sort [simp]:
1.151    "multiset_of (sort_key k xs) = multiset_of xs"
1.152    by (induct xs) (simp_all add: ac_simps)
1.153 @@ -1469,7 +1469,7 @@
1.154      proof (cases zs)
1.155        case Nil with hyps show ?thesis by auto
1.156      next
1.157 -      case Cons
1.158 +      case Cons
1.159        from sort_key_by_quicksort [of f xs]
1.160        have "sort_key f xs = (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs
1.161          in sort_key f lts @ eqs @ sort_key f gts)"
1.162 @@ -1833,16 +1833,16 @@
1.163  next
1.164    case (pw_leq_step x y X Y)
1.165    then obtain A B Z where
1.166 -    [simp]: "X = A + Z" "Y = B + Z"
1.167 -      and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
1.168 +    [simp]: "X = A + Z" "Y = B + Z"
1.169 +      and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
1.170      by auto
1.171 -  from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less"
1.172 +  from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less"
1.173      unfolding pair_leq_def by auto
1.174    thus ?case
1.175    proof
1.176      assume [simp]: "x = y"
1.177      have
1.178 -      "{#x#} + X = A + ({#y#}+Z)
1.179 +      "{#x#} + X = A + ({#y#}+Z)
1.180        \<and> {#y#} + Y = B + ({#y#}+Z)
1.181        \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
1.182        by (auto simp: ac_simps)
1.183 @@ -1853,21 +1853,21 @@
1.184      have "{#x#} + X = ?A' + Z"
1.185        "{#y#} + Y = ?B' + Z"
1.186        by (auto simp add: ac_simps)
1.187 -    moreover have
1.188 +    moreover have
1.189        "(set_of ?A', set_of ?B') \<in> max_strict"
1.190 -      using 1 A unfolding max_strict_def
1.191 +      using 1 A unfolding max_strict_def
1.192        by (auto elim!: max_ext.cases)
1.193      ultimately show ?thesis by blast
1.194    qed
1.195  qed
1.196
1.197 -lemma
1.198 +lemma
1.199    assumes pwleq: "pw_leq Z Z'"
1.200    shows ms_strictI: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
1.201    and   ms_weakI1:  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
1.202    and   ms_weakI2:  "(Z + {#}, Z' + {#}) \<in> ms_weak"
1.203  proof -
1.204 -  from pw_leq_split[OF pwleq]
1.205 +  from pw_leq_split[OF pwleq]
1.206    obtain A' B' Z''
1.207      where [simp]: "Z = A' + Z''" "Z' = B' + Z''"
1.208      and mx_or_empty: "(set_of A', set_of B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
1.209 @@ -1880,7 +1880,7 @@
1.210        assume max': "(set_of A', set_of B') \<in> max_strict"
1.211        with max have "(set_of (A + A'), set_of (B + B')) \<in> max_strict"
1.212          by (auto simp: max_strict_def intro: max_ext_additive)
1.213 -      thus ?thesis by (rule smsI)
1.214 +      thus ?thesis by (rule smsI)
1.215      next
1.216        assume [simp]: "A' = {#} \<and> B' = {#}"
1.217        show ?thesis by (rule smsI) (auto intro: max)
1.218 @@ -1929,7 +1929,7 @@
1.219    val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union},
1.220                        @{thm Un_insert_left}, @{thm Un_empty_left}]
1.221  in
1.222 -  ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset
1.223 +  ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset
1.224    {
1.225      msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
1.226      mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
1.227 @@ -1989,7 +1989,7 @@
1.228  lemma mult_less_trans:
1.229    "K \<subset># M ==> M \<subset># N ==> K \<subset># (N::'a::order multiset)"
1.230    by (fact multiset_order.less_trans)
1.231 -
1.232 +
1.233  lemma mult_less_not_sym:
1.234    "M \<subset># N ==> \<not> N \<subset># (M::'a::order multiset)"
1.235    by (fact multiset_order.less_not_sym)
1.236 @@ -2114,9 +2114,9 @@
1.237    "mcard (multiset_of xs) = length xs"
1.238    by (simp add: mcard_multiset_of)
1.239
1.240 -fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
1.241 +fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
1.242    "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
1.243 -| "ms_lesseq_impl (Cons x xs) ys = (case List.extract (op = x) ys of
1.244 +| "ms_lesseq_impl (Cons x xs) ys = (case List.extract (op = x) ys of
1.245       None \<Rightarrow> None
1.246     | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
1.247
1.248 @@ -2148,7 +2148,7 @@
1.249      obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
1.250      note Some = Some[unfolded res]
1.251      from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
1.252 -    hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}"
1.253 +    hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}"
1.254        by (auto simp: ac_simps)
1.255      show ?thesis unfolding ms_lesseq_impl.simps
1.256        unfolding Some option.simps split
1.257 @@ -2267,13 +2267,13 @@
1.258        by (rule Cons.hyps(2))
1.259      thus ?thesis
1.260        unfolding k by (auto simp: add.commute union_lcomm)
1.261 -  qed
1.262 +  qed
1.263  qed
1.264
1.265  lemma ex_multiset_of_zip_left:
1.266    assumes "length xs = length ys" "multiset_of xs' = multiset_of xs"
1.267    shows "\<exists>ys'. length ys' = length xs' \<and> multiset_of (zip xs' ys') = multiset_of (zip xs ys)"
1.268 -using assms
1.269 +using assms
1.270  proof (induct xs ys arbitrary: xs' rule: list_induct2)
1.271    case Nil
1.272    thus ?case
1.273 @@ -2281,19 +2281,9 @@
1.274  next
1.275    case (Cons x xs y ys xs')
1.276    obtain j where j_len: "j < length xs'" and nth_j: "xs' ! j = x"
1.277 -  proof -
1.278 -    assume "\<And>j. \<lbrakk>j < length xs'; xs' ! j = x\<rbrakk> \<Longrightarrow> ?thesis"
1.279 -    moreover have "\<And>k m n. (m\<Colon>nat) + n < m + k \<or> \<not> n < k" by linarith
1.280 -    moreover have "\<And>n a as. n - n < length (a # as) \<or> n < n"
1.282 -        less_diff_conv not_add_less2)
1.283 -    moreover have "\<not> length xs' < length xs'" by blast
1.284 -    ultimately show ?thesis
1.285 -      by (metis (no_types) Cons.prems Nat.add_diff_inverse diff_add_inverse2 length_append
1.286 -        less_diff_conv list.set_intros(1) multiset_of_eq_setD nth_append_length split_list)
1.287 -  qed
1.288 -
1.289 -  def xsa \<equiv> "take j xs' @ drop (Suc j) xs'"
1.290 +    by (metis Cons.prems in_set_conv_nth list.set_intros(1) multiset_of_eq_setD)
1.291 +
1.292 +  def xsa \<equiv> "take j xs' @ drop (Suc j) xs'"
1.293    have "multiset_of xs' = {#x#} + multiset_of xsa"
1.294      unfolding xsa_def using j_len nth_j
1.295      by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
1.296 @@ -2345,7 +2335,7 @@
1.297
1.298  bnf "'a multiset"
1.299    map: image_mset
1.300 -  sets: set_of
1.301 +  sets: set_of
1.302    bd: natLeq
1.303    wits: "{#}"
1.304    rel: rel_mset
```