author | haftmann |
Sat, 17 Dec 2016 15:22:13 +0100 | |
changeset 64587 | 8355a6e2df79 |
parent 63649 | e690d6f2185b |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
11054 | 1 |
(* Title: HOL/Library/Permutation.thy |
15005 | 2 |
Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker |
11054 | 3 |
*) |
4 |
||
60500 | 5 |
section \<open>Permutations\<close> |
11054 | 6 |
|
15131 | 7 |
theory Permutation |
51542 | 8 |
imports Multiset |
15131 | 9 |
begin |
11054 | 10 |
|
53238 | 11 |
inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ <~~> _" [50, 50] 50) (* FIXME proper infix, without ambiguity!? *) |
12 |
where |
|
13 |
Nil [intro!]: "[] <~~> []" |
|
14 |
| swap [intro!]: "y # x # l <~~> x # y # l" |
|
15 |
| Cons [intro!]: "xs <~~> ys \<Longrightarrow> z # xs <~~> z # ys" |
|
16 |
| trans [intro]: "xs <~~> ys \<Longrightarrow> ys <~~> zs \<Longrightarrow> xs <~~> zs" |
|
11054 | 17 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
18 |
proposition perm_refl [iff]: "l <~~> l" |
17200 | 19 |
by (induct l) auto |
11054 | 20 |
|
21 |
||
60500 | 22 |
subsection \<open>Some examples of rule induction on permutations\<close> |
11054 | 23 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
24 |
proposition xperm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []" |
56796 | 25 |
by (induct xs == "[] :: 'a list" ys pred: perm) simp_all |
11054 | 26 |
|
27 |
||
60500 | 28 |
text \<open>\medskip This more general theorem is easier to understand!\<close> |
11054 | 29 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
30 |
proposition perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys" |
25379 | 31 |
by (induct pred: perm) simp_all |
11054 | 32 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
33 |
proposition perm_empty_imp: "[] <~~> xs \<Longrightarrow> xs = []" |
17200 | 34 |
by (drule perm_length) auto |
11054 | 35 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
36 |
proposition perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs" |
25379 | 37 |
by (induct pred: perm) auto |
11054 | 38 |
|
39 |
||
60500 | 40 |
subsection \<open>Ways of making new permutations\<close> |
11054 | 41 |
|
60500 | 42 |
text \<open>We can insert the head anywhere in the list.\<close> |
11054 | 43 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
44 |
proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" |
17200 | 45 |
by (induct xs) auto |
11054 | 46 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
47 |
proposition perm_append_swap: "xs @ ys <~~> ys @ xs" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
48 |
by (induct xs) (auto intro: perm_append_Cons) |
11054 | 49 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
50 |
proposition perm_append_single: "a # xs <~~> xs @ [a]" |
17200 | 51 |
by (rule perm.trans [OF _ perm_append_swap]) simp |
11054 | 52 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
53 |
proposition perm_rev: "rev xs <~~> xs" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
54 |
by (induct xs) (auto intro!: perm_append_single intro: perm_sym) |
11054 | 55 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
56 |
proposition perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys" |
17200 | 57 |
by (induct l) auto |
11054 | 58 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
59 |
proposition perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l" |
17200 | 60 |
by (blast intro!: perm_append_swap perm_append1) |
11054 | 61 |
|
62 |
||
60500 | 63 |
subsection \<open>Further results\<close> |
11054 | 64 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
65 |
proposition perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []" |
17200 | 66 |
by (blast intro: perm_empty_imp) |
11054 | 67 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
68 |
proposition perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []" |
11054 | 69 |
apply auto |
70 |
apply (erule perm_sym [THEN perm_empty_imp]) |
|
71 |
done |
|
72 |
||
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
73 |
proposition perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]" |
25379 | 74 |
by (induct pred: perm) auto |
11054 | 75 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
76 |
proposition perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]" |
17200 | 77 |
by (blast intro: perm_sing_imp) |
11054 | 78 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
79 |
proposition perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]" |
17200 | 80 |
by (blast dest: perm_sym) |
11054 | 81 |
|
82 |
||
60500 | 83 |
subsection \<open>Removing elements\<close> |
11054 | 84 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
85 |
proposition perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys" |
17200 | 86 |
by (induct ys) auto |
11054 | 87 |
|
88 |
||
60500 | 89 |
text \<open>\medskip Congruence rule\<close> |
11054 | 90 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
91 |
proposition perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys" |
25379 | 92 |
by (induct pred: perm) auto |
11054 | 93 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
94 |
proposition remove_hd [simp]: "remove1 z (z # xs) = xs" |
15072 | 95 |
by auto |
11054 | 96 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
97 |
proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys" |
63649 | 98 |
by (drule perm_remove_perm [where z = z]) auto |
11054 | 99 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
100 |
proposition cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys" |
17200 | 101 |
by (blast intro: cons_perm_imp_perm) |
11054 | 102 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
103 |
proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys" |
53238 | 104 |
by (induct zs arbitrary: xs ys rule: rev_induct) auto |
11054 | 105 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
106 |
proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys" |
17200 | 107 |
by (blast intro: append_perm_imp_perm perm_append1) |
11054 | 108 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
109 |
proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys" |
11054 | 110 |
apply (safe intro!: perm_append2) |
111 |
apply (rule append_perm_imp_perm) |
|
112 |
apply (rule perm_append_swap [THEN perm.trans]) |
|
61585 | 113 |
\<comment> \<open>the previous step helps this \<open>blast\<close> call succeed quickly\<close> |
11054 | 114 |
apply (blast intro: perm_append_swap) |
115 |
done |
|
116 |
||
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
117 |
theorem mset_eq_perm: "mset xs = mset ys \<longleftrightarrow> xs <~~> ys" |
17200 | 118 |
apply (rule iffI) |
56796 | 119 |
apply (erule_tac [2] perm.induct) |
120 |
apply (simp_all add: union_ac) |
|
121 |
apply (erule rev_mp) |
|
122 |
apply (rule_tac x=ys in spec) |
|
123 |
apply (induct_tac xs) |
|
124 |
apply auto |
|
125 |
apply (erule_tac x = "remove1 a x" in allE) |
|
126 |
apply (drule sym) |
|
127 |
apply simp |
|
17200 | 128 |
apply (subgoal_tac "a \<in> set x") |
53238 | 129 |
apply (drule_tac z = a in perm.Cons) |
56796 | 130 |
apply (erule perm.trans) |
131 |
apply (rule perm_sym) |
|
132 |
apply (erule perm_remove) |
|
60495 | 133 |
apply (drule_tac f=set_mset in arg_cong) |
56796 | 134 |
apply simp |
15005 | 135 |
done |
136 |
||
64587 | 137 |
proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" |
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61699
diff
changeset
|
138 |
apply (auto simp: mset_eq_perm[THEN sym] mset_subset_eq_exists_conv) |
60515 | 139 |
apply (insert surj_mset) |
56796 | 140 |
apply (drule surjD) |
15072 | 141 |
apply (blast intro: sym)+ |
142 |
done |
|
15005 | 143 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
144 |
proposition perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys" |
60515 | 145 |
by (metis mset_eq_perm mset_eq_setD) |
25277 | 146 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
147 |
proposition perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys" |
25379 | 148 |
apply (induct pred: perm) |
149 |
apply simp_all |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
40122
diff
changeset
|
150 |
apply fastforce |
25379 | 151 |
apply (metis perm_set_eq) |
152 |
done |
|
25277 | 153 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
154 |
theorem eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys" |
25379 | 155 |
apply (induct xs arbitrary: ys rule: length_induct) |
53238 | 156 |
apply (case_tac "remdups xs") |
157 |
apply simp_all |
|
158 |
apply (subgoal_tac "a \<in> set (remdups ys)") |
|
57816
d8bbb97689d3
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
blanchet
parents:
56796
diff
changeset
|
159 |
prefer 2 apply (metis list.set(2) insert_iff set_remdups) |
56796 | 160 |
apply (drule split_list) apply (elim exE conjE) |
161 |
apply (drule_tac x = list in spec) apply (erule impE) prefer 2 |
|
162 |
apply (drule_tac x = "ysa @ zs" in spec) apply (erule impE) prefer 2 |
|
25379 | 163 |
apply simp |
53238 | 164 |
apply (subgoal_tac "a # list <~~> a # ysa @ zs") |
25379 | 165 |
apply (metis Cons_eq_appendI perm_append_Cons trans) |
40122
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
39916
diff
changeset
|
166 |
apply (metis Cons Cons_eq_appendI distinct.simps(2) |
25379 | 167 |
distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff) |
56796 | 168 |
apply (subgoal_tac "set (a # list) = |
169 |
set (ysa @ a # zs) \<and> distinct (a # list) \<and> distinct (ysa @ a # zs)") |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
40122
diff
changeset
|
170 |
apply (fastforce simp add: insert_ident) |
25379 | 171 |
apply (metis distinct_remdups set_remdups) |
30742 | 172 |
apply (subgoal_tac "length (remdups xs) < Suc (length xs)") |
173 |
apply simp |
|
174 |
apply (subgoal_tac "length (remdups xs) \<le> length xs") |
|
175 |
apply simp |
|
176 |
apply (rule length_remdups_leq) |
|
25379 | 177 |
done |
25287 | 178 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
179 |
proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y" |
25379 | 180 |
by (metis List.set_remdups perm_set_eq eq_set_perm_remdups) |
25287 | 181 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
182 |
theorem permutation_Ex_bij: |
39075 | 183 |
assumes "xs <~~> ys" |
184 |
shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))" |
|
56796 | 185 |
using assms |
186 |
proof induct |
|
53238 | 187 |
case Nil |
56796 | 188 |
then show ?case |
189 |
unfolding bij_betw_def by simp |
|
39075 | 190 |
next |
191 |
case (swap y x l) |
|
192 |
show ?case |
|
193 |
proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI) |
|
194 |
show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}" |
|
50037 | 195 |
by (auto simp: bij_betw_def) |
53238 | 196 |
fix i |
56796 | 197 |
assume "i < length (y # x # l)" |
39075 | 198 |
show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i" |
199 |
by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc) |
|
200 |
qed |
|
201 |
next |
|
202 |
case (Cons xs ys z) |
|
56796 | 203 |
then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" |
204 |
and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" |
|
205 |
by blast |
|
53238 | 206 |
let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0" |
39075 | 207 |
show ?case |
208 |
proof (intro exI[of _ ?f] allI conjI impI) |
|
209 |
have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}" |
|
210 |
"{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}" |
|
39078 | 211 |
by (simp_all add: lessThan_Suc_eq_insert_0) |
53238 | 212 |
show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" |
213 |
unfolding * |
|
39075 | 214 |
proof (rule bij_betw_combine) |
215 |
show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})" |
|
216 |
using bij unfolding bij_betw_def |
|
56154
f0a927235162
more complete set of lemmas wrt. image and composition
haftmann
parents:
55584
diff
changeset
|
217 |
by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def) |
39075 | 218 |
qed (auto simp: bij_betw_def) |
53238 | 219 |
fix i |
56796 | 220 |
assume "i < length (z # xs)" |
39075 | 221 |
then show "(z # xs) ! i = (z # ys) ! (?f i)" |
222 |
using perm by (cases i) auto |
|
223 |
qed |
|
224 |
next |
|
225 |
case (trans xs ys zs) |
|
56796 | 226 |
then obtain f g |
227 |
where bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" |
|
228 |
and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" |
|
229 |
by blast |
|
39075 | 230 |
show ?case |
53238 | 231 |
proof (intro exI[of _ "g \<circ> f"] conjI allI impI) |
39075 | 232 |
show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}" |
233 |
using bij by (rule bij_betw_trans) |
|
56796 | 234 |
fix i |
235 |
assume "i < length xs" |
|
236 |
with bij have "f i < length ys" |
|
237 |
unfolding bij_betw_def by force |
|
60500 | 238 |
with \<open>i < length xs\<close> show "xs ! i = zs ! (g \<circ> f) i" |
53238 | 239 |
using trans(1,3)[THEN perm_length] perm by auto |
39075 | 240 |
qed |
241 |
qed |
|
242 |
||
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
243 |
proposition perm_finite: "finite {B. B <~~> A}" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
244 |
proof (rule finite_subset[where B="{xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"]) |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
245 |
show "finite {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
246 |
apply (cases A, simp) |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
247 |
apply (rule card_ge_0_finite) |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
248 |
apply (auto simp: card_lists_length_le) |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
249 |
done |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
250 |
next |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
251 |
show "{B. B <~~> A} \<subseteq> {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
252 |
by (clarsimp simp add: perm_length perm_set_eq) |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
253 |
qed |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
254 |
|
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
255 |
proposition perm_swap: |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
256 |
assumes "i < length xs" "j < length xs" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
257 |
shows "xs[i := xs ! j, j := xs ! i] <~~> xs" |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
258 |
using assms by (simp add: mset_eq_perm[symmetric] mset_swap) |
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
259 |
|
11054 | 260 |
end |