--- a/src/HOL/Algebra/Divisibility.thy Mon May 17 13:57:19 2021 +1000
+++ b/src/HOL/Algebra/Divisibility.thy Mon May 17 09:07:30 2021 +0000
@@ -878,7 +878,7 @@
lemma perm_map [intro]:
assumes p: "a <~~> b"
shows "map f a <~~> map f b"
- using p by (simp add: perm_iff_eq_mset)
+ using p by simp
lemma perm_map_switch:
assumes m: "map f a = map f b" and p: "b <~~> c"
@@ -887,7 +887,7 @@
from m have \<open>length a = length b\<close>
by (rule map_eq_imp_length_eq)
from p have \<open>mset c = mset b\<close>
- by (simp add: perm_iff_eq_mset)
+ by simp
then obtain p where \<open>p permutes {..<length b}\<close> \<open>permute_list p b = c\<close>
by (rule mset_eq_permutation)
with \<open>length a = length b\<close> have \<open>p permutes {..<length a}\<close>
@@ -897,48 +897,27 @@
using m \<open>p permutes {..<length b}\<close> \<open>permute_list p b = c\<close>
by (auto simp flip: permute_list_map)
then show ?thesis
- by (auto simp add: perm_iff_eq_mset)
+ by auto
qed
lemma (in monoid) perm_assoc_switch:
assumes a:"as [\<sim>] bs" and p: "bs <~~> cs"
shows "\<exists>bs'. as <~~> bs' \<and> bs' [\<sim>] cs"
- using p a
-proof (induction bs cs arbitrary: as)
- case (swap y x l)
- then show ?case
- by (metis (no_types, hide_lams) list_all2_Cons2 perm.swap)
-next
-case (Cons xs ys z)
- then show ?case
- by (metis list_all2_Cons2 perm.Cons)
-next
- case (trans xs ys zs)
- then show ?case
- by (meson perm.trans)
-qed auto
+proof -
+ from p have \<open>mset cs = mset bs\<close>
+ by simp
+ then obtain p where \<open>p permutes {..<length bs}\<close> \<open>permute_list p bs = cs\<close>
+ by (rule mset_eq_permutation)
+ moreover define bs' where \<open>bs' = permute_list p as\<close>
+ ultimately have \<open>as <~~> bs'\<close> and \<open>bs' [\<sim>] cs\<close>
+ using a by (auto simp add: list_all2_permute_list_iff list_all2_lengthD)
+ then show ?thesis by blast
+qed
lemma (in monoid) perm_assoc_switch_r:
assumes p: "as <~~> bs" and a:"bs [\<sim>] cs"
shows "\<exists>bs'. as [\<sim>] bs' \<and> bs' <~~> cs"
- using p a
-proof (induction as bs arbitrary: cs)
- case Nil
- then show ?case
- by auto
-next
- case (swap y x l)
- then show ?case
- by (metis (no_types, hide_lams) list_all2_Cons1 perm.swap)
-next
- case (Cons xs ys z)
- then show ?case
- by (metis list_all2_Cons1 perm.Cons)
-next
- case (trans xs ys zs)
- then show ?case
- by (blast intro: elim: )
-qed
+ using a p by (rule list_all2_reorder_left_invariance)
declare perm_sym [sym]
@@ -946,14 +925,7 @@
assumes perm: "as <~~> bs"
and as: "P (set as)"
shows "P (set bs)"
-proof -
- from perm have "mset as = mset bs"
- by (simp add: mset_eq_perm)
- then have "set as = set bs"
- by (rule mset_eq_setD)
- with as show "P (set bs)"
- by simp
-qed
+ using assms by (metis set_mset_mset)
lemmas (in monoid) perm_closed = perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"]
@@ -1006,7 +978,7 @@
from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs"
by blast
assume "as <~~> abs"
- with p have pp: "as <~~> bs'" by fast
+ with p have pp: "as <~~> bs'" by simp
from pp ascarr have c1: "set bs' \<subseteq> carrier G" by (rule perm_closed)
from pb bscarr have c2: "set bcs \<subseteq> carrier G" by (rule perm_closed)
assume "bcs [\<sim>] cs"
@@ -1063,14 +1035,15 @@
assumes prm: "as <~~> bs"
and ascarr: "set as \<subseteq> carrier G"
shows "foldr (\<otimes>) as \<one> = foldr (\<otimes>) bs \<one>"
- using prm ascarr
-proof induction
- case (swap y x l) then show ?case
- by (simp add: m_lcomm)
-next
- case (trans xs ys zs) then show ?case
- using perm_closed by auto
-qed auto
+proof -
+ from prm have \<open>mset (rev as) = mset (rev bs)\<close>
+ by simp
+ moreover note one_closed
+ ultimately have \<open>fold (\<otimes>) (rev as) \<one> = fold (\<otimes>) (rev bs) \<one>\<close>
+ by (rule fold_permuted_eq) (use ascarr in \<open>auto intro: m_lcomm\<close>)
+ then show ?thesis
+ by (simp add: foldr_conv_fold)
+qed
lemma (in comm_monoid_cancel) multlist_ee_cong:
assumes "essentially_equal G fs fs'"
@@ -1197,12 +1170,13 @@
proof (elim essentially_equalE)
fix fs
assume prm: "as <~~> fs"
- with carr have fscarr: "set fs \<subseteq> carrier G" by (simp add: perm_closed)
+ with carr have fscarr: "set fs \<subseteq> carrier G"
+ using perm_closed by blast
note bfs
also assume [symmetric]: "fs [\<sim>] bs"
also (wfactors_listassoc_cong_l)
- note prm[symmetric]
+ have \<open>mset fs = mset as\<close> using prm by simp
finally (wfactors_perm_cong_l)
show "wfactors G as b" by (simp add: carr fscarr)
qed
@@ -1621,7 +1595,7 @@
lemma (in monoid) fmset_perm_cong:
assumes prm: "as <~~> bs"
shows "fmset G as = fmset G bs"
- using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast
+ using perm_map[OF prm] unfolding fmset_def by blast
lemma (in comm_monoid_cancel) eqc_listassoc_cong:
assumes "as [\<sim>] bs" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
@@ -1683,7 +1657,7 @@
by (simp_all add: permute_list_map)
moreover define as' where \<open>as' = permute_list p as\<close>
ultimately have tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs"
- by (simp_all add: perm_iff_eq_mset)
+ by simp_all
from tp show ?thesis
proof (rule essentially_equalI)
from tm tp ascarr have as'carr: "set as' \<subseteq> carrier G"
@@ -1941,7 +1915,7 @@
then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
by (fast elim: essentially_equalE)
then have "p \<in> set ds"
- by (simp add: perm_set_eq[symmetric])
+ by (metis \<open>mset (p # cs) = mset ds\<close> insert_iff list.set(2) perm_set_eq)
with dsassoc obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"
unfolding list_all2_conv_all_nth set_conv_nth by force
then consider "p' \<in> set as" | "p' \<in> set bs" by auto
@@ -2003,7 +1977,7 @@
then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
by (fast elim: essentially_equalE)
then have "p \<in> set ds"
- by (simp add: perm_set_eq[symmetric])
+ by (metis list.set_intros(1) set_mset_mset)
with dsassoc obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"
unfolding list_all2_conv_all_nth set_conv_nth by force
then consider "p' \<in> set as" | "p' \<in> set bs" by auto
@@ -2641,7 +2615,7 @@
proof (induct as arbitrary: a as')
case Nil
then have "a \<sim> \<one>"
- by (meson Units_one_closed one_closed perm.Nil perm_wfactorsD unit_wfactors)
+ by (simp add: perm_wfactorsD)
then have "as' = []"
using Nil.prems assoc_unit_l unit_wfactors_empty by blast
then show ?case
@@ -2728,8 +2702,12 @@
by (simp add: a'carr set_drop set_take)
from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')"
using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto
- with carr_ah have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
- by (auto simp: essentially_equal_def)
+ then obtain bs where \<open>mset as = mset bs\<close> \<open>bs [\<sim>] take i as' @ drop (Suc i) as'\<close>
+ by (auto simp add: essentially_equal_def)
+ with carr_ah have \<open>mset (ah # as) = mset (ah # bs)\<close> \<open>ah # bs [\<sim>] ah # take i as' @ drop (Suc i) as'\<close>
+ by simp_all
+ then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
+ unfolding essentially_equal_def by blast
have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
(as' ! i # take i as' @ drop (Suc i) as')"
proof (intro essentially_equalI)
--- a/src/HOL/Combinatorics/List_Permutation.thy Mon May 17 13:57:19 2021 +1000
+++ b/src/HOL/Combinatorics/List_Permutation.thy Mon May 17 09:07:30 2021 +0000
@@ -13,52 +13,10 @@
\<^text>\<open>Permutations\<close>; it should be seldom needed.
\<close>
-subsection \<open>An inductive definition \ldots\<close>
-
-inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr \<open><~~>\<close> 50)
-where
- Nil [intro!]: "[] <~~> []"
-| swap [intro!]: "y # x # l <~~> x # y # l"
-| Cons [intro!]: "xs <~~> ys \<Longrightarrow> z # xs <~~> z # ys"
-| trans [intro]: "xs <~~> ys \<Longrightarrow> ys <~~> zs \<Longrightarrow> xs <~~> zs"
-
-proposition perm_refl [iff]: "l <~~> l"
- by (induct l) auto
-
-text \<open>\ldots that is equivalent to an already existing notion:\<close>
+subsection \<open>An existing notion\<close>
-lemma perm_iff_eq_mset:
- \<open>xs <~~> ys \<longleftrightarrow> mset xs = mset ys\<close>
-proof
- assume \<open>mset xs = mset ys\<close>
- then show \<open>xs <~~> ys\<close>
- proof (induction xs arbitrary: ys)
- case Nil
- then show ?case
- by simp
- next
- case (Cons x xs)
- from Cons.prems [symmetric] have \<open>mset xs = mset (remove1 x ys)\<close>
- by simp
- then have \<open>xs <~~> remove1 x ys\<close>
- by (rule Cons.IH)
- then have \<open>x # xs <~~> x # remove1 x ys\<close>
- by (rule perm.Cons)
- moreover from Cons.prems have \<open>x \<in> set ys\<close>
- by (auto dest: union_single_eq_member)
- then have \<open>x # remove1 x ys <~~> ys\<close>
- by (induction ys) auto
- ultimately show \<open>x # xs <~~> ys\<close>
- by (rule perm.trans)
- qed
-next
- assume \<open>xs <~~> ys\<close>
- then show \<open>mset xs = mset ys\<close>
- by induction simp_all
-qed
-
-theorem mset_eq_perm: \<open>mset xs = mset ys \<longleftrightarrow> xs <~~> ys\<close>
- by (simp add: perm_iff_eq_mset)
+abbreviation (input) perm :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> (infixr \<open><~~>\<close> 50)
+ where \<open>xs <~~> ys \<equiv> mset xs = mset ys\<close>
subsection \<open>Nontrivial conclusions\<close>
@@ -66,29 +24,29 @@
proposition perm_swap:
\<open>xs[i := xs ! j, j := xs ! i] <~~> xs\<close>
if \<open>i < length xs\<close> \<open>j < length xs\<close>
- using that by (simp add: perm_iff_eq_mset mset_swap)
+ using that by (simp add: mset_swap)
proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
- by (auto simp add: perm_iff_eq_mset mset_subset_eq_exists_conv ex_mset dest: sym)
+ by (auto simp add: mset_subset_eq_exists_conv ex_mset dest: sym)
proposition perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys"
- by (rule mset_eq_setD) (simp add: perm_iff_eq_mset)
+ by (rule mset_eq_setD) simp
proposition perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs \<longleftrightarrow> distinct ys"
- by (rule mset_eq_imp_distinct_iff) (simp add: perm_iff_eq_mset)
+ by (rule mset_eq_imp_distinct_iff) simp
theorem eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys"
- by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq)
+ by (simp add: set_eq_iff_mset_remdups_eq)
proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y"
- by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq)
+ by (simp add: set_eq_iff_mset_remdups_eq)
theorem permutation_Ex_bij:
assumes "xs <~~> ys"
shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
proof -
from assms have \<open>mset xs = mset ys\<close> \<open>length xs = length ys\<close>
- by (auto simp add: perm_iff_eq_mset dest: mset_eq_length)
+ by (auto simp add: dest: mset_eq_length)
from \<open>mset xs = mset ys\<close> obtain p where \<open>p permutes {..<length ys}\<close> \<open>permute_list p ys = xs\<close>
by (rule mset_eq_permutation)
then have \<open>bij_betw p {..<length xs} {..<length ys}\<close>
@@ -101,84 +59,84 @@
qed
proposition perm_finite: "finite {B. B <~~> A}"
- using mset_eq_finite by (auto simp add: perm_iff_eq_mset)
+ using mset_eq_finite by auto
subsection \<open>Trivial conclusions:\<close>
proposition perm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []"
- by (simp add: perm_iff_eq_mset)
+ by simp
text \<open>\medskip This more general theorem is easier to understand!\<close>
proposition perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys"
- by (rule mset_eq_length) (simp add: perm_iff_eq_mset)
+ by (rule mset_eq_length) simp
proposition perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs"
- by (simp add: perm_iff_eq_mset)
+ by simp
text \<open>We can insert the head anywhere in the list.\<close>
proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_append_swap: "xs @ ys <~~> ys @ xs"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_append_single: "a # xs <~~> xs @ [a]"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_rev: "rev xs <~~> xs"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys"
- by (simp add: perm_iff_eq_mset)
+ by simp
text \<open>\medskip Congruence rule\<close>
proposition perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition remove_hd [simp]: "remove1 z (z # xs) = xs"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition cons_perm_eq [simp]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys"
- by (simp add: perm_iff_eq_mset)
+ by simp
proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys"
- by (simp add: perm_iff_eq_mset)
+ by simp
end
--- a/src/HOL/Combinatorics/Permutations.thy Mon May 17 13:57:19 2021 +1000
+++ b/src/HOL/Combinatorics/Permutations.thy Mon May 17 09:07:30 2021 +0000
@@ -1150,6 +1150,11 @@
by (induct xs) (auto simp: inv_f_f surj_f_inv_f)
qed
+lemma list_all2_permute_list_iff:
+ \<open>list_all2 P (permute_list p xs) (permute_list p ys) \<longleftrightarrow> list_all2 P xs ys\<close>
+ if \<open>p permutes {..<length xs}\<close>
+ using that by (auto simp add: list_all2_iff simp flip: permute_list_zip)
+
subsection \<open>More lemmas about permutations\<close>
--- a/src/HOL/Library/Multiset.thy Mon May 17 13:57:19 2021 +1000
+++ b/src/HOL/Library/Multiset.thy Mon May 17 09:07:30 2021 +0000
@@ -1923,26 +1923,55 @@
using assms by (metis count_mset)
lemma fold_multiset_equiv:
- assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
- and equiv: "mset xs = mset ys"
- shows "List.fold f xs = List.fold f ys"
- using f equiv [symmetric]
-proof (induct xs arbitrary: ys)
+ \<open>List.fold f xs = List.fold f ys\<close>
+ if f: \<open>\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x\<close>
+ and \<open>mset xs = mset ys\<close>
+using f \<open>mset xs = mset ys\<close> [symmetric] proof (induction xs arbitrary: ys)
case Nil
then show ?case by simp
next
case (Cons x xs)
- then have *: "set ys = set (x # xs)"
+ then have *: \<open>set ys = set (x # xs)\<close>
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"
+ have \<open>\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x\<close>
by (rule Cons.prems(1)) (simp_all add: *)
- moreover from * have "x \<in> set ys"
+ moreover from * have \<open>x \<in> set ys\<close>
+ by simp
+ ultimately have \<open>List.fold f ys = List.fold f (remove1 x ys) \<circ> f x\<close>
+ by (fact fold_remove1_split)
+ moreover from Cons.prems have \<open>List.fold f xs = List.fold f (remove1 x ys)\<close>
+ by (auto intro: Cons.IH)
+ ultimately show ?case
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
+
+lemma fold_permuted_eq:
+ \<open>List.fold (\<odot>) xs z = List.fold (\<odot>) ys z\<close>
+ if \<open>mset xs = mset ys\<close>
+ and \<open>P z\<close> and P: \<open>\<And>x z. x \<in> set xs \<Longrightarrow> P z \<Longrightarrow> P (x \<odot> z)\<close>
+ and f: \<open>\<And>x y z. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> P z \<Longrightarrow> x \<odot> (y \<odot> z) = y \<odot> (x \<odot> z)\<close>
+ for f (infixl \<open>\<odot>\<close> 70)
+using \<open>P z\<close> P f \<open>mset xs = mset ys\<close> [symmetric] proof (induction xs arbitrary: ys z)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons x xs)
+ then have *: \<open>set ys = set (x # xs)\<close>
+ by (blast dest: mset_eq_setD)
+ have \<open>P z\<close>
+ by (fact Cons.prems(1))
+ moreover have \<open>\<And>x z. x \<in> set ys \<Longrightarrow> P z \<Longrightarrow> P (x \<odot> z)\<close>
+ by (rule Cons.prems(2)) (simp_all add: *)
+ moreover have \<open>\<And>x y z. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> P z \<Longrightarrow> x \<odot> (y \<odot> z) = y \<odot> (x \<odot> z)\<close>
+ by (rule Cons.prems(3)) (simp_all add: *)
+ moreover from * have \<open>x \<in> set ys\<close>
+ by simp
+ ultimately have \<open>fold (\<odot>) ys z = fold (\<odot>) (remove1 x ys) (x \<odot> z)\<close>
+ by (induction ys arbitrary: z) auto
+ moreover from Cons.prems have \<open>fold (\<odot>) xs (x \<odot> z) = fold (\<odot>) (remove1 x ys) (x \<odot> z)\<close>
+ by (auto intro: Cons.IH)
+ ultimately show ?case
+ by simp
qed
lemma mset_shuffles: "zs \<in> shuffles xs ys \<Longrightarrow> mset zs = mset xs + mset ys"