--- a/Admin/Isabelle_app/build Sun May 23 20:12:36 2021 +0200
+++ b/Admin/Isabelle_app/build Sun May 23 20:34:43 2021 +0200
@@ -2,6 +2,7 @@
set -e
+unset CDPATH
THIS="$(cd "$(dirname "$0")"; pwd)"
cd "$THIS"
--- a/Admin/bash_process/build Sun May 23 20:12:36 2021 +0200
+++ b/Admin/bash_process/build Sun May 23 20:34:43 2021 +0200
@@ -2,6 +2,7 @@
#
# Multi-platform build script
+unset CDPATH
THIS="$(cd "$(dirname "$0")"; pwd)"
PRG="$(basename "$0")"
--- a/Admin/build Sun May 23 20:12:36 2021 +0200
+++ b/Admin/build Sun May 23 20:34:43 2021 +0200
@@ -5,6 +5,7 @@
## directory layout
if [ -z "$ISABELLE_HOME" ]; then
+ unset CDPATH
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
fi
--- a/Admin/build_history Sun May 23 20:12:36 2021 +0200
+++ b/Admin/build_history Sun May 23 20:34:43 2021 +0200
@@ -2,6 +2,7 @@
#
# DESCRIPTION: build history versions from another repository clone
+unset CDPATH
THIS="$(cd "$(dirname "$0")"; pwd)"
"$THIS/build" jars > /dev/null || exit $?
--- a/Admin/build_release Sun May 23 20:12:36 2021 +0200
+++ b/Admin/build_release Sun May 23 20:34:43 2021 +0200
@@ -2,6 +2,7 @@
#
# DESCRIPTION: build full Isabelle distribution from repository
+unset CDPATH
THIS="$(cd "$(dirname "$0")"; pwd)"
"$THIS/build" jars || exit $?
--- a/Admin/cronjob/main Sun May 23 20:12:36 2021 +0200
+++ b/Admin/cronjob/main Sun May 23 20:34:43 2021 +0200
@@ -2,6 +2,7 @@
#
# DESCRIPTION: start the main Isabelle cronjob
+unset CDPATH
THIS="$(cd "$(dirname "$0")"; pwd)"
source "$HOME/.bashrc"
--- a/Admin/init Sun May 23 20:12:36 2021 +0200
+++ b/Admin/init Sun May 23 20:34:43 2021 +0200
@@ -7,6 +7,7 @@
## environment
+unset CDPATH
export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
ISABELLE_REPOS="https://isabelle.sketis.net/repos/isabelle"
--- a/bin/isabelle Sun May 23 20:12:36 2021 +0200
+++ b/bin/isabelle Sun May 23 20:34:43 2021 +0200
@@ -4,6 +4,8 @@
#
# Isabelle tool wrapper.
+unset CDPATH
+
if [ -L "$0" ]; then
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
--- a/bin/isabelle_java Sun May 23 20:12:36 2021 +0200
+++ b/bin/isabelle_java Sun May 23 20:34:43 2021 +0200
@@ -4,6 +4,8 @@
#
# Isabelle/Java cold start -- without settings environment
+unset CDPATH
+
if [ -L "$0" ]; then
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
--- a/bin/isabelle_scala_script Sun May 23 20:12:36 2021 +0200
+++ b/bin/isabelle_scala_script Sun May 23 20:34:43 2021 +0200
@@ -4,6 +4,8 @@
#
# Isabelle/Scala script wrapper.
+unset CDPATH
+
if [ -L "$0" ]; then
TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
--- a/src/HOL/Algebra/Divisibility.thy Sun May 23 20:12:36 2021 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Sun May 23 20:34:43 2021 +0200
@@ -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 Sun May 23 20:12:36 2021 +0200
+++ b/src/HOL/Combinatorics/List_Permutation.thy Sun May 23 20:34:43 2021 +0200
@@ -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 Sun May 23 20:12:36 2021 +0200
+++ b/src/HOL/Combinatorics/Permutations.thy Sun May 23 20:34:43 2021 +0200
@@ -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 Sun May 23 20:12:36 2021 +0200
+++ b/src/HOL/Library/Multiset.thy Sun May 23 20:34:43 2021 +0200
@@ -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"
--- a/src/HOL/Library/RBT_Set.thy Sun May 23 20:12:36 2021 +0200
+++ b/src/HOL/Library/RBT_Set.thy Sun May 23 20:34:43 2021 +0200
@@ -790,7 +790,7 @@
then show "x \<le> y"
using Cons[symmetric]
by(auto simp add: set_keys Cons_eq_filter_iff)
- (metis sorted.simps(2) sorted_append sorted_keys)
+ (metis sorted_wrt.simps(2) sorted_append sorted_keys)
qed
thus ?thesis using Cons by (simp add: Bleast_def)
qed
--- a/src/HOL/Library/Ramsey.thy Sun May 23 20:12:36 2021 +0200
+++ b/src/HOL/Library/Ramsey.thy Sun May 23 20:34:43 2021 +0200
@@ -10,6 +10,9 @@
subsection \<open>Preliminary definitions\<close>
+abbreviation strict_sorted :: "'a::linorder list \<Rightarrow> bool" where
+ "strict_sorted \<equiv> sorted_wrt (<)"
+
subsubsection \<open>The $n$-element subsets of a set $A$\<close>
definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" ("([_]\<^bsup>_\<^esup>)" [0,999] 999)
@@ -992,7 +995,7 @@
then show "(s ?j, s ?i) \<in> T k" by (simp add: k transition_idx_in ij)
qed
then have "\<not> wf (T k)"
- by (meson wf_iff_no_infinite_down_chain)
+ unfolding wf_iff_no_infinite_down_chain by iprover
with wfT \<open>k < n\<close> show False by blast
qed
--- a/src/HOL/List.thy Sun May 23 20:12:36 2021 +0200
+++ b/src/HOL/List.thy Sun May 23 20:34:43 2021 +0200
@@ -370,18 +370,14 @@
context linorder
begin
-fun sorted :: "'a list \<Rightarrow> bool" where
-"sorted [] = True" |
-"sorted (x # ys) = ((\<forall>y \<in> set ys. x \<le> y) \<and> sorted ys)"
-
-abbreviation strict_sorted :: "'a list \<Rightarrow> bool" where
- "strict_sorted \<equiv> sorted_wrt (<)"
-
-lemma sorted_sorted_wrt: "sorted = sorted_wrt (\<le>)"
-proof (rule ext)
- fix xs show "sorted xs = sorted_wrt (\<le>) xs"
- by(induction xs rule: sorted.induct) auto
-qed
+abbreviation sorted :: "'a list \<Rightarrow> bool" where
+ "sorted \<equiv> sorted_wrt (\<le>)"
+
+lemma sorted_simps: "sorted [] = True" "sorted (x # ys) = ((\<forall>y \<in> set ys. x\<le>y) \<and> sorted ys)"
+ by auto
+
+lemma strict_sorted_simps: "sorted_wrt (<) [] = True" "sorted_wrt (<) (x # ys) = ((\<forall>y \<in> set ys. x<y) \<and> sorted_wrt (<) ys)"
+ by auto
primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
"insort_key f x [] = [x]" |
@@ -403,10 +399,10 @@
"stable_sort_key sk =
(\<forall>f xs k. filter (\<lambda>y. f y = k) (sk f xs) = filter (\<lambda>y. f y = k) xs)"
-lemma strict_sorted_iff: "strict_sorted l \<longleftrightarrow> sorted l \<and> distinct l"
+lemma strict_sorted_iff: "sorted_wrt (<) l \<longleftrightarrow> sorted l \<and> distinct l"
by (induction l) (auto iff: antisym_conv1)
-lemma strict_sorted_imp_sorted: "strict_sorted xs \<Longrightarrow> sorted xs"
+lemma strict_sorted_imp_sorted: "sorted_wrt (<) xs \<Longrightarrow> sorted xs"
by (auto simp: strict_sorted_iff)
end
@@ -5506,52 +5502,55 @@
should be removed and \<open>sorted2_simps\<close> should be added instead.
Executable code is one such use case.\<close>
+lemma sorted0: "sorted [] = True"
+ by simp
+
lemma sorted1: "sorted [x] = True"
-by simp
+ by simp
lemma sorted2: "sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))"
-by(induction zs) auto
+ by(induction zs) auto
lemmas sorted2_simps = sorted1 sorted2
-lemmas [code] = sorted.simps(1) sorted2_simps
+lemmas [code] = sorted0 sorted2_simps
lemma sorted_append:
"sorted (xs@ys) = (sorted xs \<and> sorted ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
-by (simp add: sorted_sorted_wrt sorted_wrt_append)
+by (simp add: sorted_wrt_append)
lemma sorted_map:
"sorted (map f xs) = sorted_wrt (\<lambda>x y. f x \<le> f y) xs"
-by (simp add: sorted_sorted_wrt sorted_wrt_map)
+ by (simp add: sorted_wrt_map)
lemma sorted01: "length xs \<le> 1 \<Longrightarrow> sorted xs"
-by (simp add: sorted_sorted_wrt sorted_wrt01)
+ by (simp add: sorted_wrt01)
lemma sorted_tl:
"sorted xs \<Longrightarrow> sorted (tl xs)"
-by (cases xs) (simp_all)
+ by (cases xs) (simp_all)
lemma sorted_iff_nth_mono_less:
"sorted xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> xs ! i \<le> xs ! j)"
-by (simp add: sorted_sorted_wrt sorted_wrt_iff_nth_less)
+ by (simp add: sorted_wrt_iff_nth_less)
lemma sorted_iff_nth_mono:
"sorted xs = (\<forall>i j. i \<le> j \<longrightarrow> j < length xs \<longrightarrow> xs ! i \<le> xs ! j)"
-by (auto simp: sorted_iff_nth_mono_less nat_less_le)
+ by (auto simp: sorted_iff_nth_mono_less nat_less_le)
lemma sorted_nth_mono:
"sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
-by (auto simp: sorted_iff_nth_mono)
+ by (auto simp: sorted_iff_nth_mono)
lemma sorted_iff_nth_Suc:
"sorted xs \<longleftrightarrow> (\<forall>i. Suc i < length xs \<longrightarrow> xs!i \<le> xs!(Suc i))"
-by(simp add: sorted_sorted_wrt sorted_wrt_iff_nth_Suc_transp)
+ by(simp add: sorted_wrt_iff_nth_Suc_transp)
lemma sorted_rev_nth_mono:
"sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
-using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
- rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
-by auto
+ using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
+ rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
+ by auto
lemma sorted_rev_iff_nth_mono:
"sorted (rev xs) \<longleftrightarrow> (\<forall> i j. i \<le> j \<longrightarrow> j < length xs \<longrightarrow> xs!j \<le> xs!i)" (is "?L = ?R")
@@ -5713,10 +5712,10 @@
end
lemma sorted_upt[simp]: "sorted [m..<n]"
-by(simp add: sorted_sorted_wrt sorted_wrt_mono_rel[OF _ sorted_wrt_upt])
+ by(simp add: sorted_wrt_mono_rel[OF _ sorted_wrt_upt])
lemma sorted_upto[simp]: "sorted [m..n]"
-by(simp add: sorted_sorted_wrt sorted_wrt_mono_rel[OF _ sorted_wrt_upto])
+ by(simp add: sorted_wrt_mono_rel[OF _ sorted_wrt_upto])
subsubsection \<open>Sorting functions\<close>
@@ -6167,17 +6166,17 @@
with assms show ?thesis by simp
qed
-lemma strict_sorted_list_of_set [simp]: "strict_sorted (sorted_list_of_set A)"
+lemma strict_sorted_list_of_set [simp]: "sorted_wrt (<) (sorted_list_of_set A)"
by (simp add: strict_sorted_iff)
lemma finite_set_strict_sorted:
assumes "finite A"
- obtains l where "strict_sorted l" "set l = A" "length l = card A"
+ obtains l where "sorted_wrt (<) l" "set l = A" "length l = card A"
by (metis assms distinct_card distinct_sorted_list_of_set set_sorted_list_of_set strict_sorted_list_of_set)
lemma strict_sorted_equal:
- assumes "strict_sorted xs"
- and "strict_sorted ys"
+ assumes "sorted_wrt (<) xs"
+ and "sorted_wrt (<) ys"
and "set ys = set xs"
shows "ys = xs"
using assms
@@ -6199,7 +6198,7 @@
qed
qed auto
-lemma strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. strict_sorted xs \<and> set xs = A"
+lemma strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. sorted_wrt (<) xs \<and> set xs = A"
by (simp add: Uniq_def strict_sorted_equal)
lemma sorted_list_of_set_inject:
@@ -6209,7 +6208,7 @@
lemma sorted_list_of_set_unique:
assumes "finite A"
- shows "strict_sorted l \<and> set l = A \<and> length l = card A \<longleftrightarrow> sorted_list_of_set A = l"
+ shows "sorted_wrt (<) l \<and> set l = A \<and> length l = card A \<longleftrightarrow> sorted_list_of_set A = l"
using assms strict_sorted_equal by force
end
@@ -7590,7 +7589,7 @@
fix y assume "y \<in> set xs \<and> P y"
hence "y \<in> set (filter P xs)" by auto
thus "x \<le> y"
- by (metis Cons eq_iff filter_sort set_ConsD set_sort sorted.simps(2) sorted_sort)
+ by (metis Cons eq_iff filter_sort set_ConsD set_sort sorted_wrt.simps(2) sorted_sort)
qed
thus ?thesis using Cons by (simp add: Bleast_def)
qed
--- a/src/Tools/Metis/fix_metis_license Sun May 23 20:12:36 2021 +0200
+++ b/src/Tools/Metis/fix_metis_license Sun May 23 20:34:43 2021 +0200
@@ -1,4 +1,5 @@
#!/usr/bin/env bash
+unset CDPATH
THIS=$(cd "$(dirname "$0")"; echo $PWD)
(cd $THIS;
perl -p -i~ -w -e 's/MIT license/BSD License/g' Makefile src/*.s* scripts/mlpp)
--- a/src/Tools/Metis/make_metis Sun May 23 20:12:36 2021 +0200
+++ b/src/Tools/Metis/make_metis Sun May 23 20:34:43 2021 +0200
@@ -6,6 +6,7 @@
# A few other ad hoc transformations are performed to ensure that the sources
# compile within Isabelle on Poly/ML and SML/NJ.
+unset CDPATH
THIS=$(cd "$(dirname "$0")"; echo $PWD)
make -f Makefile.FILES refresh_FILES
FILES=$(cat "$THIS/FILES")