1.1 --- a/NEWS Wed May 12 22:33:10 2010 -0700
1.2 +++ b/NEWS Thu May 13 14:34:05 2010 +0200
1.3 @@ -298,8 +298,14 @@
1.4 generation;
1.5 - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
1.6 if needed.
1.7 +Renamed:
1.8 + multiset_eq_conv_count_eq -> multiset_ext_iff
1.9 + multi_count_ext -> multiset_ext
1.10 + diff_union_inverse2 -> diff_union_cancelR
1.11 INCOMPATIBILITY.
1.12
1.13 +* Theory Permutation: replaced local "remove" by List.remove1.
1.14 +
1.15 * Code generation: ML and OCaml code is decorated with signatures.
1.16
1.17 * Theory List: added transpose.
2.1 --- a/src/HOL/Algebra/Divisibility.thy Wed May 12 22:33:10 2010 -0700
2.2 +++ b/src/HOL/Algebra/Divisibility.thy Thu May 13 14:34:05 2010 +0200
2.3 @@ -2193,7 +2193,7 @@
2.4
2.5 from csmset msubset
2.6 have "fmset G bs = fmset G as + fmset G cs"
2.7 - by (simp add: multiset_eq_conv_count_eq mset_le_def)
2.8 + by (simp add: multiset_ext_iff mset_le_def)
2.9 hence basc: "b \<sim> a \<otimes> c"
2.10 by (rule fmset_wfactors_mult) fact+
2.11
3.1 --- a/src/HOL/Library/Multiset.thy Wed May 12 22:33:10 2010 -0700
3.2 +++ b/src/HOL/Library/Multiset.thy Thu May 13 14:34:05 2010 +0200
3.3 @@ -24,13 +24,13 @@
3.4 notation (xsymbols)
3.5 Melem (infix "\<in>#" 50)
3.6
3.7 -lemma multiset_eq_conv_count_eq:
3.8 +lemma multiset_ext_iff:
3.9 "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
3.10 by (simp only: count_inject [symmetric] expand_fun_eq)
3.11
3.12 -lemma multi_count_ext:
3.13 +lemma multiset_ext:
3.14 "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
3.15 - using multiset_eq_conv_count_eq by auto
3.16 + using multiset_ext_iff by auto
3.17
3.18 text {*
3.19 \medskip Preservation of the representing set @{term multiset}.
3.20 @@ -127,7 +127,7 @@
3.21 by (simp add: union_def in_multiset multiset_typedef)
3.22
3.23 instance multiset :: (type) cancel_comm_monoid_add proof
3.24 -qed (simp_all add: multiset_eq_conv_count_eq)
3.25 +qed (simp_all add: multiset_ext_iff)
3.26
3.27
3.28 subsubsection {* Difference *}
3.29 @@ -146,56 +146,62 @@
3.30 by (simp add: diff_def in_multiset multiset_typedef)
3.31
3.32 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
3.33 - by (simp add: Mempty_def diff_def in_multiset multiset_typedef)
3.34 +by(simp add: multiset_ext_iff)
3.35
3.36 -lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
3.37 - by (rule multi_count_ext)
3.38 - (auto simp del: count_single simp add: union_def diff_def in_multiset multiset_typedef)
3.39 +lemma diff_cancel[simp]: "A - A = {#}"
3.40 +by (rule multiset_ext) simp
3.41
3.42 -lemma diff_cancel: "A - A = {#}"
3.43 - by (rule multi_count_ext) simp
3.44 +lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
3.45 +by(simp add: multiset_ext_iff)
3.46 +
3.47 +lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
3.48 +by(simp add: multiset_ext_iff)
3.49
3.50 lemma insert_DiffM:
3.51 "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
3.52 - by (clarsimp simp: multiset_eq_conv_count_eq)
3.53 + by (clarsimp simp: multiset_ext_iff)
3.54
3.55 lemma insert_DiffM2 [simp]:
3.56 "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
3.57 - by (clarsimp simp: multiset_eq_conv_count_eq)
3.58 + by (clarsimp simp: multiset_ext_iff)
3.59
3.60 lemma diff_right_commute:
3.61 "(M::'a multiset) - N - Q = M - Q - N"
3.62 - by (auto simp add: multiset_eq_conv_count_eq)
3.63 + by (auto simp add: multiset_ext_iff)
3.64 +
3.65 +lemma diff_add:
3.66 + "(M::'a multiset) - (N + Q) = M - N - Q"
3.67 +by (simp add: multiset_ext_iff)
3.68
3.69 lemma diff_union_swap:
3.70 "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
3.71 - by (auto simp add: multiset_eq_conv_count_eq)
3.72 + by (auto simp add: multiset_ext_iff)
3.73
3.74 lemma diff_union_single_conv:
3.75 "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
3.76 - by (simp add: multiset_eq_conv_count_eq)
3.77 + by (simp add: multiset_ext_iff)
3.78
3.79
3.80 subsubsection {* Equality of multisets *}
3.81
3.82 lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
3.83 - by (simp add: multiset_eq_conv_count_eq)
3.84 + by (simp add: multiset_ext_iff)
3.85
3.86 lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
3.87 - by (auto simp add: multiset_eq_conv_count_eq)
3.88 + by (auto simp add: multiset_ext_iff)
3.89
3.90 lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
3.91 - by (auto simp add: multiset_eq_conv_count_eq)
3.92 + by (auto simp add: multiset_ext_iff)
3.93
3.94 lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
3.95 - by (auto simp add: multiset_eq_conv_count_eq)
3.96 + by (auto simp add: multiset_ext_iff)
3.97
3.98 lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False"
3.99 - by (auto simp add: multiset_eq_conv_count_eq)
3.100 + by (auto simp add: multiset_ext_iff)
3.101
3.102 lemma diff_single_trivial:
3.103 "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
3.104 - by (auto simp add: multiset_eq_conv_count_eq)
3.105 + by (auto simp add: multiset_ext_iff)
3.106
3.107 lemma diff_single_eq_union:
3.108 "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = N + {#x#}"
3.109 @@ -210,27 +216,11 @@
3.110 by auto
3.111
3.112 lemma union_is_single:
3.113 - "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")
3.114 -proof
3.115 + "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")proof
3.116 assume ?rhs then show ?lhs by auto
3.117 next
3.118 - assume ?lhs
3.119 - then have "\<And>b. count (M + N) b = (if b = a then 1 else 0)" by auto
3.120 - then have *: "\<And>b. count M b + count N b = (if b = a then 1 else 0)" by auto
3.121 - then have "count M a + count N a = 1" by auto
3.122 - then have **: "count M a = 1 \<and> count N a = 0 \<or> count M a = 0 \<and> count N a = 1"
3.123 - by auto
3.124 - from * have "\<And>b. b \<noteq> a \<Longrightarrow> count M b + count N b = 0" by auto
3.125 - then have ***: "\<And>b. b \<noteq> a \<Longrightarrow> count M b = 0 \<and> count N b = 0" by auto
3.126 - from ** and *** have
3.127 - "(\<forall>b. count M b = (if b = a then 1 else 0) \<and> count N b = 0) \<or>
3.128 - (\<forall>b. count M b = 0 \<and> count N b = (if b = a then 1 else 0))"
3.129 - by auto
3.130 - then have
3.131 - "(\<forall>b. count M b = (if b = a then 1 else 0)) \<and> (\<forall>b. count N b = 0) \<or>
3.132 - (\<forall>b. count M b = 0) \<and> (\<forall>b. count N b = (if b = a then 1 else 0))"
3.133 - by auto
3.134 - then show ?rhs by (auto simp add: multiset_eq_conv_count_eq)
3.135 + assume ?lhs thus ?rhs
3.136 + by(simp add: multiset_ext_iff split:if_splits) (metis add_is_1)
3.137 qed
3.138
3.139 lemma single_is_union:
3.140 @@ -239,6 +229,7 @@
3.141
3.142 lemma add_eq_conv_diff:
3.143 "M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}" (is "?lhs = ?rhs")
3.144 +(* shorter: by (simp add: multiset_ext_iff) fastsimp *)
3.145 proof
3.146 assume ?rhs then show ?lhs
3.147 by (auto simp add: add_assoc add_commute [of "{#b#}"])
3.148 @@ -287,7 +278,7 @@
3.149 mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
3.150
3.151 instance proof
3.152 -qed (auto simp add: mset_le_def mset_less_def multiset_eq_conv_count_eq intro: order_trans antisym)
3.153 +qed (auto simp add: mset_le_def mset_less_def multiset_ext_iff intro: order_trans antisym)
3.154
3.155 end
3.156
3.157 @@ -298,7 +289,7 @@
3.158 lemma mset_le_exists_conv:
3.159 "(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)"
3.160 apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
3.161 -apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
3.162 +apply (auto intro: multiset_ext_iff [THEN iffD2])
3.163 done
3.164
3.165 lemma mset_le_mono_add_right_cancel [simp]:
3.166 @@ -327,11 +318,11 @@
3.167
3.168 lemma multiset_diff_union_assoc:
3.169 "C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
3.170 - by (simp add: multiset_eq_conv_count_eq mset_le_def)
3.171 + by (simp add: multiset_ext_iff mset_le_def)
3.172
3.173 lemma mset_le_multiset_union_diff_commute:
3.174 "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
3.175 -by (simp add: multiset_eq_conv_count_eq mset_le_def)
3.176 +by (simp add: multiset_ext_iff mset_le_def)
3.177
3.178 lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
3.179 apply (clarsimp simp: mset_le_def mset_less_def)
3.180 @@ -361,7 +352,7 @@
3.181 done
3.182
3.183 lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
3.184 - by (auto simp add: mset_less_def mset_le_def multiset_eq_conv_count_eq)
3.185 + by (auto simp add: mset_less_def mset_le_def multiset_ext_iff)
3.186
3.187 lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
3.188 by (auto simp: mset_le_def mset_less_def)
3.189 @@ -379,7 +370,7 @@
3.190
3.191 lemma mset_less_diff_self:
3.192 "c \<in># B \<Longrightarrow> B - {#c#} < B"
3.193 - by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq)
3.194 + by (auto simp: mset_le_def mset_less_def multiset_ext_iff)
3.195
3.196
3.197 subsubsection {* Intersection *}
3.198 @@ -406,15 +397,15 @@
3.199 by (simp add: multiset_inter_def multiset_typedef)
3.200
3.201 lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
3.202 - by (rule multi_count_ext) (auto simp add: multiset_inter_count)
3.203 + by (rule multiset_ext) (auto simp add: multiset_inter_count)
3.204
3.205 lemma multiset_union_diff_commute:
3.206 assumes "B #\<inter> C = {#}"
3.207 shows "A + B - C = A - C + B"
3.208 -proof (rule multi_count_ext)
3.209 +proof (rule multiset_ext)
3.210 fix x
3.211 from assms have "min (count B x) (count C x) = 0"
3.212 - by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq)
3.213 + by (auto simp add: multiset_inter_count multiset_ext_iff)
3.214 then have "count B x = 0 \<or> count C x = 0"
3.215 by auto
3.216 then show "count (A + B - C) x = count (A - C + B) x"
3.217 @@ -429,15 +420,15 @@
3.218 by (simp add: MCollect_def in_multiset multiset_typedef)
3.219
3.220 lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
3.221 - by (rule multi_count_ext) simp
3.222 + by (rule multiset_ext) simp
3.223
3.224 lemma MCollect_single [simp]:
3.225 "MCollect {#x#} P = (if P x then {#x#} else {#})"
3.226 - by (rule multi_count_ext) simp
3.227 + by (rule multiset_ext) simp
3.228
3.229 lemma MCollect_union [simp]:
3.230 "MCollect (M + N) f = MCollect M f + MCollect N f"
3.231 - by (rule multi_count_ext) simp
3.232 + by (rule multiset_ext) simp
3.233
3.234
3.235 subsubsection {* Set of elements *}
3.236 @@ -455,7 +446,7 @@
3.237 by (auto simp add: set_of_def)
3.238
3.239 lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
3.240 -by (auto simp add: set_of_def multiset_eq_conv_count_eq)
3.241 +by (auto simp add: set_of_def multiset_ext_iff)
3.242
3.243 lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
3.244 by (auto simp add: set_of_def)
3.245 @@ -503,7 +494,7 @@
3.246 done
3.247
3.248 lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
3.249 -by (auto simp add: size_def multiset_eq_conv_count_eq)
3.250 +by (auto simp add: size_def multiset_ext_iff)
3.251
3.252 lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
3.253 by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
3.254 @@ -624,7 +615,7 @@
3.255 by (cases "B = {#}") (auto dest: multi_member_split)
3.256
3.257 lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
3.258 -apply (subst multiset_eq_conv_count_eq)
3.259 +apply (subst multiset_ext_iff)
3.260 apply auto
3.261 done
3.262
3.263 @@ -756,12 +747,12 @@
3.264
3.265 lemma multiset_of_eq_setD:
3.266 "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
3.267 -by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
3.268 +by (rule) (auto simp add:multiset_ext_iff set_count_greater_0)
3.269
3.270 lemma set_eq_iff_multiset_of_eq_distinct:
3.271 "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
3.272 (set x = set y) = (multiset_of x = multiset_of y)"
3.273 -by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
3.274 +by (auto simp: multiset_ext_iff distinct_count_atmost_1)
3.275
3.276 lemma set_eq_iff_multiset_of_remdups_eq:
3.277 "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
3.278 @@ -787,8 +778,9 @@
3.279 apply auto
3.280 done
3.281
3.282 -lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
3.283 -by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
3.284 +lemma multiset_of_remove1[simp]:
3.285 + "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
3.286 +by (induct xs) (auto simp add: multiset_ext_iff)
3.287
3.288 lemma multiset_of_eq_length:
3.289 assumes "multiset_of xs = multiset_of ys"
3.290 @@ -925,15 +917,15 @@
3.291
3.292 lemma Mempty_Bag [code]:
3.293 "{#} = Bag []"
3.294 - by (simp add: multiset_eq_conv_count_eq)
3.295 + by (simp add: multiset_ext_iff)
3.296
3.297 lemma single_Bag [code]:
3.298 "{#x#} = Bag [(x, 1)]"
3.299 - by (simp add: multiset_eq_conv_count_eq)
3.300 + by (simp add: multiset_ext_iff)
3.301
3.302 lemma MCollect_Bag [code]:
3.303 "MCollect (Bag xs) P = Bag (filter (P \<circ> fst) xs)"
3.304 - by (simp add: multiset_eq_conv_count_eq count_of_filter)
3.305 + by (simp add: multiset_ext_iff count_of_filter)
3.306
3.307 lemma mset_less_eq_Bag [code]:
3.308 "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
3.309 @@ -1140,10 +1132,10 @@
3.310 apply (rule_tac x = "J + {#a#}" in exI)
3.311 apply (rule_tac x = "K + Ka" in exI)
3.312 apply (rule conjI)
3.313 - apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
3.314 + apply (simp add: multiset_ext_iff split: nat_diff_split)
3.315 apply (rule conjI)
3.316 apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
3.317 - apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
3.318 + apply (simp add: multiset_ext_iff split: nat_diff_split)
3.319 apply (simp (no_asm_use) add: trans_def)
3.320 apply blast
3.321 apply (subgoal_tac "a :# (M0 + {#a#})")
3.322 @@ -1658,7 +1650,7 @@
3.323
3.324 subsection {* Legacy theorem bindings *}
3.325
3.326 -lemmas multi_count_eq = multiset_eq_conv_count_eq [symmetric]
3.327 +lemmas multi_count_eq = multiset_ext_iff [symmetric]
3.328
3.329 lemma union_commute: "M + N = N + (M::'a multiset)"
3.330 by (fact add_commute)
4.1 --- a/src/HOL/Library/Permutation.thy Wed May 12 22:33:10 2010 -0700
4.2 +++ b/src/HOL/Library/Permutation.thy Thu May 13 14:34:05 2010 +0200
4.3 @@ -93,29 +93,16 @@
4.4
4.5 subsection {* Removing elements *}
4.6
4.7 -primrec remove :: "'a => 'a list => 'a list" where
4.8 - "remove x [] = []"
4.9 - | "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
4.10 -
4.11 -lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
4.12 +lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove1 x ys"
4.13 by (induct ys) auto
4.14
4.15 -lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
4.16 - by (induct l) auto
4.17 -
4.18 -lemma multiset_of_remove [simp]:
4.19 - "multiset_of (remove a x) = multiset_of x - {#a#}"
4.20 - apply (induct x)
4.21 - apply (auto simp: multiset_eq_conv_count_eq)
4.22 - done
4.23 -
4.24
4.25 text {* \medskip Congruence rule *}
4.26
4.27 -lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
4.28 +lemma perm_remove_perm: "xs <~~> ys ==> remove1 z xs <~~> remove1 z ys"
4.29 by (induct pred: perm) auto
4.30
4.31 -lemma remove_hd [simp]: "remove z (z # xs) = xs"
4.32 +lemma remove_hd [simp]: "remove1 z (z # xs) = xs"
4.33 by auto
4.34
4.35 lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
4.36 @@ -146,7 +133,7 @@
4.37 apply (erule_tac [2] perm.induct, simp_all add: union_ac)
4.38 apply (erule rev_mp, rule_tac x=ys in spec)
4.39 apply (induct_tac xs, auto)
4.40 - apply (erule_tac x = "remove a x" in allE, drule sym, simp)
4.41 + apply (erule_tac x = "remove1 a x" in allE, drule sym, simp)
4.42 apply (subgoal_tac "a \<in> set x")
4.43 apply (drule_tac z=a in perm.Cons)
4.44 apply (erule perm.trans, rule perm_sym, erule perm_remove)
5.1 --- a/src/HOL/List.thy Wed May 12 22:33:10 2010 -0700
5.2 +++ b/src/HOL/List.thy Thu May 13 14:34:05 2010 +0200
5.3 @@ -2961,6 +2961,9 @@
5.4 (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
5.5 by (induct xs) auto
5.6
5.7 +lemma remove1_commute: "remove1 x (remove1 y zs) = remove1 y (remove1 x zs)"
5.8 +by (induct zs) auto
5.9 +
5.10 lemma in_set_remove1[simp]:
5.11 "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
5.12 apply (induct xs)
6.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed May 12 22:33:10 2010 -0700
6.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Thu May 13 14:34:05 2010 +0200
6.3 @@ -56,11 +56,6 @@
6.4 apply auto
6.5 done
6.6
6.7 -(* Should this go in Multiset.thy? *)
6.8 -(* TN: No longer an intro-rule; needed only once and might get in the way *)
6.9 -lemma multiset_eqI: "[| !!x. count M x = count N x |] ==> M = N"
6.10 - by (subst multiset_eq_conv_count_eq, blast)
6.11 -
6.12 (* Here is a version of set product for multisets. Is it worth moving
6.13 to multiset.thy? If so, one should similarly define msetsum for abelian
6.14 semirings, using of_nat. Also, is it worth developing bounded quantifiers
6.15 @@ -210,7 +205,7 @@
6.16 ultimately have "count M a = count N a"
6.17 by auto
6.18 }
6.19 - thus ?thesis by (simp add:multiset_eq_conv_count_eq)
6.20 + thus ?thesis by (simp add:multiset_ext_iff)
6.21 qed
6.22
6.23 definition multiset_prime_factorization :: "nat => nat multiset" where