summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Mon, 17 May 2021 09:07:30 +0000 | |

changeset 73706 | 4b1386b2c23e |

parent 73705 | ac07f6be27ea |

child 73708 | 2e3a60ce5a9f |

mere abbreviation for logical alias

--- 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"