equal
deleted
inserted
replaced
118 apply (rule perm_append_swap [THEN perm.trans]) |
118 apply (rule perm_append_swap [THEN perm.trans]) |
119 -- \<open>the previous step helps this @{text blast} call succeed quickly\<close> |
119 -- \<open>the previous step helps this @{text blast} call succeed quickly\<close> |
120 apply (blast intro: perm_append_swap) |
120 apply (blast intro: perm_append_swap) |
121 done |
121 done |
122 |
122 |
123 lemma multiset_of_eq_perm: "multiset_of xs = multiset_of ys \<longleftrightarrow> xs <~~> ys" |
123 lemma mset_eq_perm: "mset xs = mset ys \<longleftrightarrow> xs <~~> ys" |
124 apply (rule iffI) |
124 apply (rule iffI) |
125 apply (erule_tac [2] perm.induct) |
125 apply (erule_tac [2] perm.induct) |
126 apply (simp_all add: union_ac) |
126 apply (simp_all add: union_ac) |
127 apply (erule rev_mp) |
127 apply (erule rev_mp) |
128 apply (rule_tac x=ys in spec) |
128 apply (rule_tac x=ys in spec) |
138 apply (erule perm_remove) |
138 apply (erule perm_remove) |
139 apply (drule_tac f=set_mset in arg_cong) |
139 apply (drule_tac f=set_mset in arg_cong) |
140 apply simp |
140 apply simp |
141 done |
141 done |
142 |
142 |
143 lemma multiset_of_le_perm_append: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" |
143 lemma mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" |
144 apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) |
144 apply (auto simp: mset_eq_perm[THEN sym] mset_le_exists_conv) |
145 apply (insert surj_multiset_of) |
145 apply (insert surj_mset) |
146 apply (drule surjD) |
146 apply (drule surjD) |
147 apply (blast intro: sym)+ |
147 apply (blast intro: sym)+ |
148 done |
148 done |
149 |
149 |
150 lemma perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys" |
150 lemma perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys" |
151 by (metis multiset_of_eq_perm multiset_of_eq_setD) |
151 by (metis mset_eq_perm mset_eq_setD) |
152 |
152 |
153 lemma perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys" |
153 lemma perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys" |
154 apply (induct pred: perm) |
154 apply (induct pred: perm) |
155 apply simp_all |
155 apply simp_all |
156 apply fastforce |
156 apply fastforce |