--- a/NEWS Wed Feb 24 14:49:16 2021 +0000
+++ b/NEWS Wed Feb 24 14:49:36 2021 +0000
@@ -9,12 +9,64 @@
*** HOL ***
+* Theory Multiset: dedicated predicate "multiset" is gone, use
+explict expression instead. Minor INCOMPATIBILITY.
+
* HOL-Analysis/HOL-Probability: indexed products of discrete
distributions, negative binomial distribution, Hoeffding's inequality,
Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some
more small lemmas. Some theorems that were stated awkwardly before were
corrected. Minor INCOMPATIBILITY.
+* Theory "Permutation" in HOL-Library has been renamed to the more
+specific "List_Permutation".
+
+
+*** ML ***
+
+* External bash processes are always managed by Isabelle/Scala, in
+contrast to Isabelle2021 where this was only done for macOS on Apple
+Silicon.
+
+The main Isabelle/ML interface is Isabelle_System.bash_process with
+result type Process_Result.T (resembling class Process_Result in Scala);
+derived operations Isabelle_System.bash and Isabelle_System.bash_output
+provide similar functionality as before. Rare INCOMPATIBILITY due to
+subtle semantic differences:
+
+ - Processes invoked from Isabelle/ML actually run in the context of
+ the Java VM of Isabelle/Scala. The settings environment and current
+ working directory are usually the same on both sides, but there can be
+ subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML).
+
+ - Output via stdout and stderr is line-oriented: Unix vs. Windows
+ line-endings are normalized towards Unix; presence or absence of a
+ final newline is irrelevant. The original lines are available as
+ Process_Result.out_lines/err_lines; the concatenated versions
+ Process_Result.out/err *omit* a trailing newline (using
+ Library.trim_line, which was occasional seen in applications before,
+ but is no longer necessary).
+
+ - Output needs to be plain text encoded in UTF-8: Isabelle/Scala
+ recodes it temporarily as UTF-16. This works for well-formed Unicode
+ text, but not for arbitrary byte strings. In such cases, the bash
+ script should write tempory files, managed by Isabelle/ML operations
+ like Isabelle_System.with_tmp_file to create a file name and
+ File.read to retrieve its content.
+
+ - Just like any other Scala function invoked from ML,
+ Isabelle_System.bash_process requires a proper PIDE session context.
+ This could be a regular batch session (e.g. "isabelle build"), a
+ PIDE editor session (e.g. "isabelle jedit"), or headless PIDE (e.g.
+ "isabelle dump" or "isabelle server"). Note that old "isabelle
+ console" or raw "isabelle process" don't have that.
+
+New Process_Result.timing works as in Isabelle/Scala, based on direct
+measurements of the bash_process wrapper in C: elapsed time is always
+available, CPU time is only available on Linux and macOS, GC time is
+unavailable.
+
+
New in Isabelle2021 (February 2021)
-----------------------------------
--- a/src/HOL/Algebra/Divisibility.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Algebra/Divisibility.thy Wed Feb 24 14:49:36 2021 +0000
@@ -6,7 +6,7 @@
section \<open>Divisibility in monoids and rings\<close>
theory Divisibility
- imports "HOL-Library.Permutation" Coset Group
+ imports "HOL-Library.List_Permutation" Coset Group
begin
section \<open>Factorial Monoids\<close>
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Wed Feb 24 14:49:36 2021 +0000
@@ -1507,7 +1507,7 @@
assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
using finite_number_of_roots[OF assms]
unfolding sym[OF alg_mult_gt_zero_iff_is_root[OF assms]]
- by (simp add: multiset_def roots_def)
+ by (simp add: roots_def)
lemma (in domain) roots_mem_iff_is_root:
assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Wed Feb 24 14:49:36 2021 +0000
@@ -1208,8 +1208,7 @@
lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is
"\<lambda>x p. if prime p then multiplicity p x else 0"
- unfolding multiset_def
-proof clarify
+proof -
fix x :: 'a
show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A")
proof (cases "x = 0")
@@ -2097,7 +2096,7 @@
from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
with S(2) have nz: "n \<noteq> 0" by auto
from S_eq \<open>finite S\<close> have count_A: "count A = f"
- unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
+ unfolding A_def by (subst multiset.Abs_multiset_inverse) simp_all
from S_eq count_A have set_mset_A: "set_mset A = S"
by (simp only: set_mset_def)
from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
--- a/src/HOL/Computational_Algebra/Primes.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Computational_Algebra/Primes.thy Wed Feb 24 14:49:36 2021 +0000
@@ -728,8 +728,8 @@
define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
define A where "A = Abs_multiset g"
have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
- from finite_subset[OF this assms(1)] have [simp]: "g \<in> multiset"
- by (simp add: multiset_def)
+ from finite_subset[OF this assms(1)] have [simp]: "finite {x. 0 < g x}"
+ by simp
from assms have count_A: "count A x = g x" for x unfolding A_def
by simp
have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
--- a/src/HOL/Conditionally_Complete_Lattices.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Wed Feb 24 14:49:36 2021 +0000
@@ -10,47 +10,93 @@
imports Finite_Set Lattices_Big Set_Interval
begin
+locale preordering_bdd = preordering
+begin
+
+definition bdd :: \<open>'a set \<Rightarrow> bool\<close>
+ where unfold: \<open>bdd A \<longleftrightarrow> (\<exists>M. \<forall>x \<in> A. x \<^bold>\<le> M)\<close>
+
+lemma empty [simp, intro]:
+ \<open>bdd {}\<close>
+ by (simp add: unfold)
+
+lemma I [intro]:
+ \<open>bdd A\<close> if \<open>\<And>x. x \<in> A \<Longrightarrow> x \<^bold>\<le> M\<close>
+ using that by (auto simp add: unfold)
+
+lemma E:
+ assumes \<open>bdd A\<close>
+ obtains M where \<open>\<And>x. x \<in> A \<Longrightarrow> x \<^bold>\<le> M\<close>
+ using assms that by (auto simp add: unfold)
+
+lemma I2:
+ \<open>bdd (f ` A)\<close> if \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<^bold>\<le> M\<close>
+ using that by (auto simp add: unfold)
+
+lemma mono:
+ \<open>bdd A\<close> if \<open>bdd B\<close> \<open>A \<subseteq> B\<close>
+ using that by (auto simp add: unfold)
+
+lemma Int1 [simp]:
+ \<open>bdd (A \<inter> B)\<close> if \<open>bdd A\<close>
+ using mono that by auto
+
+lemma Int2 [simp]:
+ \<open>bdd (A \<inter> B)\<close> if \<open>bdd B\<close>
+ using mono that by auto
+
+end
+
context preorder
begin
-definition "bdd_above A \<longleftrightarrow> (\<exists>M. \<forall>x \<in> A. x \<le> M)"
-definition "bdd_below A \<longleftrightarrow> (\<exists>m. \<forall>x \<in> A. m \<le> x)"
+sublocale bdd_above: preordering_bdd \<open>(\<le>)\<close> \<open>(<)\<close>
+ defines bdd_above_primitive_def: bdd_above = bdd_above.bdd ..
+
+sublocale bdd_below: preordering_bdd \<open>(\<ge>)\<close> \<open>(>)\<close>
+ defines bdd_below_primitive_def: bdd_below = bdd_below.bdd ..
+
+lemma bdd_above_def: \<open>bdd_above A \<longleftrightarrow> (\<exists>M. \<forall>x \<in> A. x \<le> M)\<close>
+ by (fact bdd_above.unfold)
-lemma bdd_aboveI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> x \<le> M) \<Longrightarrow> bdd_above A"
- by (auto simp: bdd_above_def)
+lemma bdd_below_def: \<open>bdd_below A \<longleftrightarrow> (\<exists>M. \<forall>x \<in> A. M \<le> x)\<close>
+ by (fact bdd_below.unfold)
-lemma bdd_belowI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A"
- by (auto simp: bdd_below_def)
+lemma bdd_aboveI: "(\<And>x. x \<in> A \<Longrightarrow> x \<le> M) \<Longrightarrow> bdd_above A"
+ by (fact bdd_above.I)
+
+lemma bdd_belowI: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A"
+ by (fact bdd_below.I)
lemma bdd_aboveI2: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> bdd_above (f`A)"
- by force
+ by (fact bdd_above.I2)
lemma bdd_belowI2: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> bdd_below (f`A)"
- by force
+ by (fact bdd_below.I2)
-lemma bdd_above_empty [simp, intro]: "bdd_above {}"
- unfolding bdd_above_def by auto
+lemma bdd_above_empty: "bdd_above {}"
+ by (fact bdd_above.empty)
-lemma bdd_below_empty [simp, intro]: "bdd_below {}"
- unfolding bdd_below_def by auto
+lemma bdd_below_empty: "bdd_below {}"
+ by (fact bdd_below.empty)
lemma bdd_above_mono: "bdd_above B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> bdd_above A"
- by (metis (full_types) bdd_above_def order_class.le_neq_trans psubsetD)
+ by (fact bdd_above.mono)
lemma bdd_below_mono: "bdd_below B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> bdd_below A"
- by (metis bdd_below_def order_class.le_neq_trans psubsetD)
+ by (fact bdd_below.mono)
-lemma bdd_above_Int1 [simp]: "bdd_above A \<Longrightarrow> bdd_above (A \<inter> B)"
- using bdd_above_mono by auto
+lemma bdd_above_Int1: "bdd_above A \<Longrightarrow> bdd_above (A \<inter> B)"
+ by (fact bdd_above.Int1)
-lemma bdd_above_Int2 [simp]: "bdd_above B \<Longrightarrow> bdd_above (A \<inter> B)"
- using bdd_above_mono by auto
+lemma bdd_above_Int2: "bdd_above B \<Longrightarrow> bdd_above (A \<inter> B)"
+ by (fact bdd_above.Int2)
-lemma bdd_below_Int1 [simp]: "bdd_below A \<Longrightarrow> bdd_below (A \<inter> B)"
- using bdd_below_mono by auto
+lemma bdd_below_Int1: "bdd_below A \<Longrightarrow> bdd_below (A \<inter> B)"
+ by (fact bdd_below.Int1)
-lemma bdd_below_Int2 [simp]: "bdd_below B \<Longrightarrow> bdd_below (A \<inter> B)"
- using bdd_below_mono by auto
+lemma bdd_below_Int2: "bdd_below B \<Longrightarrow> bdd_below (A \<inter> B)"
+ by (fact bdd_below.Int2)
lemma bdd_above_Ioo [simp, intro]: "bdd_above {a <..< b}"
by (auto simp add: bdd_above_def intro!: exI[of _ b] less_imp_le)
@@ -90,11 +136,21 @@
end
-lemma (in order_top) bdd_above_top[simp, intro!]: "bdd_above A"
- by (rule bdd_aboveI[of _ top]) simp
+context order_top
+begin
+
+lemma bdd_above_top [simp, intro!]: "bdd_above A"
+ by (rule bdd_aboveI [of _ top]) simp
+
+end
-lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A"
- by (rule bdd_belowI[of _ bot]) simp
+context order_bot
+begin
+
+lemma bdd_below_bot [simp, intro!]: "bdd_below A"
+ by (rule bdd_belowI [of _ bot]) simp
+
+end
lemma bdd_above_image_mono: "mono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_above (f`A)"
by (auto simp: bdd_above_def mono_def)
--- a/src/HOL/Lattices_Big.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Lattices_Big.thy Wed Feb 24 14:49:36 2021 +0000
@@ -675,17 +675,6 @@
shows "Max M \<le> Max N"
using assms by (fact Max.subset_imp)
-end
-
-lemma sum_le_card_Max: "finite A \<Longrightarrow> sum f A \<le> card A * Max (f ` A)"
-using sum_bounded_above[of A f "Max (f ` A)"] by simp
-
-lemma card_Min_le_sum: "finite A \<Longrightarrow> card A * Min (f ` A) \<le> sum f A"
-using sum_bounded_below[of A "Min (f ` A)" f] by simp
-
-context linorder (* FIXME *)
-begin
-
lemma mono_Min_commute:
assumes "mono f"
assumes "finite A" and "A \<noteq> {}"
@@ -810,6 +799,12 @@
end
+lemma sum_le_card_Max: "finite A \<Longrightarrow> sum f A \<le> card A * Max (f ` A)"
+using sum_bounded_above[of A f "Max (f ` A)"] by simp
+
+lemma card_Min_le_sum: "finite A \<Longrightarrow> card A * Min (f ` A) \<le> sum f A"
+using sum_bounded_below[of A "Min (f ` A)" f] by simp
+
context linordered_ab_semigroup_add
begin
--- a/src/HOL/Library/DAList_Multiset.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Library/DAList_Multiset.thy Wed Feb 24 14:49:36 2021 +0000
@@ -100,7 +100,7 @@
definition count_of :: "('a \<times> nat) list \<Rightarrow> 'a \<Rightarrow> nat"
where "count_of xs x = (case map_of xs x of None \<Rightarrow> 0 | Some n \<Rightarrow> n)"
-lemma count_of_multiset: "count_of xs \<in> multiset"
+lemma count_of_multiset: "finite {x. 0 < count_of xs x}"
proof -
let ?A = "{x::'a. 0 < (case map_of xs x of None \<Rightarrow> 0::nat | Some n \<Rightarrow> n)}"
have "?A \<subseteq> dom (map_of xs)"
@@ -117,7 +117,7 @@
with finite_dom_map_of [of xs] have "finite ?A"
by (auto intro: finite_subset)
then show ?thesis
- by (simp add: count_of_def fun_eq_iff multiset_def)
+ by (simp add: count_of_def fun_eq_iff)
qed
lemma count_simps [simp]:
@@ -291,7 +291,7 @@
let ?inv = "{xs :: ('a \<times> nat) list. (distinct \<circ> map fst) xs}"
note cs[simp del] = count_simps
have count[simp]: "\<And>x. count (Abs_multiset (count_of x)) = count_of x"
- by (rule Abs_multiset_inverse[OF count_of_multiset])
+ by (rule Abs_multiset_inverse) (simp add: count_of_multiset)
assume ys: "ys \<in> ?inv"
then show "fold_mset f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))"
unfolding Bag_def unfolding Alist_inverse[OF ys]
--- a/src/HOL/Library/Function_Algebras.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Library/Function_Algebras.thy Wed Feb 24 14:49:36 2021 +0000
@@ -132,6 +132,14 @@
instance "fun" :: (type, semiring_1) semiring_1 ..
+lemma numeral_fun: \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
+ \<open>numeral n = (\<lambda>x::'a. numeral n)\<close>
+ by (induction n) (simp_all only: numeral.simps plus_fun_def, simp_all)
+
+lemma numeral_fun_apply [simp]: \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
+ \<open>numeral n x = numeral n\<close>
+ by (simp add: numeral_fun)
+
lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
proof -
have comp: "comp = (\<lambda>f g x. f (g x))"
--- a/src/HOL/Library/Library.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Library/Library.thy Wed Feb 24 14:49:36 2021 +0000
@@ -50,6 +50,7 @@
Lattice_Constructions
Linear_Temporal_Logic_on_Streams
ListVector
+ List_Permutation
Lub_Glb
Mapping
Monad_Syntax
@@ -66,7 +67,6 @@
Pattern_Aliases
Periodic_Fun
Perm
- Permutation
Permutations
Poly_Mapping
Power_By_Squaring
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/List_Permutation.thy Wed Feb 24 14:49:36 2021 +0000
@@ -0,0 +1,230 @@
+(* Title: HOL/Library/List_Permutation.thy
+ Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker
+*)
+
+section \<open>Permuted Lists\<close>
+
+theory List_Permutation
+imports Multiset
+begin
+
+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
+
+
+subsection \<open>Some examples of rule induction on permutations\<close>
+
+proposition perm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []"
+ by (induction "[] :: 'a list" ys pred: perm) simp_all
+
+
+text \<open>\medskip This more general theorem is easier to understand!\<close>
+
+proposition perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys"
+ by (induct pred: perm) simp_all
+
+proposition perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs"
+ by (induct pred: perm) auto
+
+
+subsection \<open>Ways of making new permutations\<close>
+
+text \<open>We can insert the head anywhere in the list.\<close>
+
+proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
+ by (induct xs) auto
+
+proposition perm_append_swap: "xs @ ys <~~> ys @ xs"
+ by (induct xs) (auto intro: perm_append_Cons)
+
+proposition perm_append_single: "a # xs <~~> xs @ [a]"
+ by (rule perm.trans [OF _ perm_append_swap]) simp
+
+proposition perm_rev: "rev xs <~~> xs"
+ by (induct xs) (auto intro!: perm_append_single intro: perm_sym)
+
+proposition perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys"
+ by (induct l) auto
+
+proposition perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l"
+ by (blast intro!: perm_append_swap perm_append1)
+
+
+subsection \<open>Further results\<close>
+
+proposition perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []"
+ by (blast intro: perm_empty_imp)
+
+proposition perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []"
+ using perm_sym by auto
+
+proposition perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]"
+ by (induct pred: perm) auto
+
+proposition perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]"
+ by (blast intro: perm_sing_imp)
+
+proposition perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]"
+ by (blast dest: perm_sym)
+
+
+subsection \<open>Removing elements\<close>
+
+proposition perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys"
+ by (induct ys) auto
+
+
+text \<open>\medskip Congruence rule\<close>
+
+proposition perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys"
+ by (induct pred: perm) auto
+
+proposition remove_hd [simp]: "remove1 z (z # xs) = xs"
+ by auto
+
+proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
+ by (drule perm_remove_perm [where z = z]) auto
+
+proposition cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys"
+ by (meson cons_perm_imp_perm perm.Cons)
+
+proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys"
+ by (induct zs arbitrary: xs ys rule: rev_induct) auto
+
+proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys"
+ by (blast intro: append_perm_imp_perm perm_append1)
+
+proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys"
+ by (meson perm.trans perm_append1_eq perm_append_swap)
+
+theorem mset_eq_perm: "mset xs = mset ys \<longleftrightarrow> xs <~~> ys"
+proof
+ assume "mset xs = mset ys"
+ then show "xs <~~> ys"
+ proof (induction xs arbitrary: ys)
+ case (Cons x xs)
+ then have "x \<in> set ys"
+ using mset_eq_setD by fastforce
+ then show ?case
+ by (metis Cons.IH Cons.prems mset_remove1 perm.Cons perm.trans perm_remove perm_sym remove_hd)
+ qed auto
+next
+ assume "xs <~~> ys"
+ then show "mset xs = mset ys"
+ by induction (simp_all add: union_ac)
+qed
+
+proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
+ apply (rule iffI)
+ apply (metis mset_append mset_eq_perm mset_subset_eq_exists_conv surjD surj_mset)
+ by (metis mset_append mset_eq_perm mset_subset_eq_exists_conv)
+
+proposition perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys"
+ by (metis mset_eq_perm mset_eq_setD)
+
+proposition perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys"
+ by (metis card_distinct distinct_card perm_length perm_set_eq)
+
+theorem eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys"
+proof (induction xs arbitrary: ys rule: length_induct)
+ case (1 xs)
+ show ?case
+ proof (cases "remdups xs")
+ case Nil
+ with "1.prems" show ?thesis
+ using "1.prems" by auto
+ next
+ case (Cons x us)
+ then have "x \<in> set (remdups ys)"
+ using "1.prems" set_remdups by fastforce
+ then show ?thesis
+ using "1.prems" mset_eq_perm set_eq_iff_mset_remdups_eq by blast
+ qed
+qed
+
+proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y"
+ by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
+
+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))"
+ using assms
+proof induct
+ case Nil
+ then show ?case
+ unfolding bij_betw_def by simp
+next
+ case (swap y x l)
+ show ?case
+ proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
+ show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
+ by (auto simp: bij_betw_def)
+ fix i
+ assume "i < length (y # x # l)"
+ show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
+ by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
+ qed
+next
+ case (Cons xs ys z)
+ then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}"
+ and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)"
+ by blast
+ let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
+ show ?case
+ proof (intro exI[of _ ?f] allI conjI impI)
+ have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"
+ "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"
+ by (simp_all add: lessThan_Suc_eq_insert_0)
+ show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}"
+ unfolding *
+ proof (rule bij_betw_combine)
+ show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
+ using bij unfolding bij_betw_def
+ by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def)
+ qed (auto simp: bij_betw_def)
+ fix i
+ assume "i < length (z # xs)"
+ then show "(z # xs) ! i = (z # ys) ! (?f i)"
+ using perm by (cases i) auto
+ qed
+next
+ case (trans xs ys zs)
+ then obtain f g
+ where bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}"
+ and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)"
+ by blast
+ show ?case
+ proof (intro exI[of _ "g \<circ> f"] conjI allI impI)
+ show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
+ using bij by (rule bij_betw_trans)
+ fix i
+ assume "i < length xs"
+ with bij have "f i < length ys"
+ unfolding bij_betw_def by force
+ with \<open>i < length xs\<close> show "xs ! i = zs ! (g \<circ> f) i"
+ using trans(1,3)[THEN perm_length] perm by auto
+ qed
+qed
+
+proposition perm_finite: "finite {B. B <~~> A}"
+proof (rule finite_subset[where B="{xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"])
+ show "finite {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"
+ using finite_lists_length_le by blast
+next
+ show "{B. B <~~> A} \<subseteq> {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"
+ by (clarsimp simp add: perm_length perm_set_eq)
+qed
+
+proposition perm_swap:
+ assumes "i < length xs" "j < length xs"
+ shows "xs[i := xs ! j, j := xs ! i] <~~> xs"
+ using assms by (simp add: mset_eq_perm[symmetric] mset_swap)
+
+end
--- a/src/HOL/Library/Multiset.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Library/Multiset.thy Wed Feb 24 14:49:36 2021 +0000
@@ -14,17 +14,19 @@
subsection \<open>The type of multisets\<close>
-definition "multiset = {f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}"
-
-typedef 'a multiset = "multiset :: ('a \<Rightarrow> nat) set"
+typedef 'a multiset = \<open>{f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}\<close>
morphisms count Abs_multiset
- unfolding multiset_def
proof
- show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
+ show \<open>(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}\<close>
+ by simp
qed
setup_lifting type_definition_multiset
+lemma count_Abs_multiset:
+ \<open>count (Abs_multiset f) = f\<close> if \<open>finite {x. f x > 0}\<close>
+ by (rule Abs_multiset_inverse) (simp add: that)
+
lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
by (simp only: count_inject [symmetric] fun_eq_iff)
@@ -33,37 +35,15 @@
text \<open>Preservation of the representing set \<^term>\<open>multiset\<close>.\<close>
-lemma const0_in_multiset: "(\<lambda>a. 0) \<in> multiset"
- by (simp add: multiset_def)
-
-lemma only1_in_multiset: "(\<lambda>b. if b = a then n else 0) \<in> multiset"
- by (simp add: multiset_def)
-
-lemma union_preserves_multiset: "M \<in> multiset \<Longrightarrow> N \<in> multiset \<Longrightarrow> (\<lambda>a. M a + N a) \<in> multiset"
- by (simp add: multiset_def)
-
lemma diff_preserves_multiset:
- assumes "M \<in> multiset"
- shows "(\<lambda>a. M a - N a) \<in> multiset"
-proof -
- have "{x. N x < M x} \<subseteq> {x. 0 < M x}"
- by auto
- with assms show ?thesis
- by (auto simp add: multiset_def intro: finite_subset)
-qed
+ \<open>finite {x. 0 < M x - N x}\<close> if \<open>finite {x. 0 < M x}\<close> for M N :: \<open>'a \<Rightarrow> nat\<close>
+ using that by (rule rev_finite_subset) auto
lemma filter_preserves_multiset:
- assumes "M \<in> multiset"
- shows "(\<lambda>x. if P x then M x else 0) \<in> multiset"
-proof -
- have "{x. (P x \<longrightarrow> 0 < M x) \<and> P x} \<subseteq> {x. 0 < M x}"
- by auto
- with assms show ?thesis
- by (auto simp add: multiset_def intro: finite_subset)
-qed
-
-lemmas in_multiset = const0_in_multiset only1_in_multiset
- union_preserves_multiset diff_preserves_multiset filter_preserves_multiset
+ \<open>finite {x. 0 < (if P x then M x else 0)}\<close> if \<open>finite {x. 0 < M x}\<close> for M N :: \<open>'a \<Rightarrow> nat\<close>
+ using that by (rule rev_finite_subset) auto
+
+lemmas in_multiset = diff_preserves_multiset filter_preserves_multiset
subsection \<open>Representing multisets\<close>
@@ -74,19 +54,19 @@
begin
lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0"
-by (rule const0_in_multiset)
+ by simp
abbreviation Mempty :: "'a multiset" ("{#}") where
"Mempty \<equiv> 0"
lift_definition plus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)"
-by (rule union_preserves_multiset)
+ by simp
lift_definition minus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
-by (rule diff_preserves_multiset)
+ by (rule diff_preserves_multiset)
instance
- by (standard; transfer; simp add: fun_eq_iff)
+ by (standard; transfer) (simp_all add: fun_eq_iff)
end
@@ -99,9 +79,9 @@
end
lemma add_mset_in_multiset:
- assumes M: \<open>M \<in> multiset\<close>
- shows \<open>(\<lambda>b. if b = a then Suc (M b) else M b) \<in> multiset\<close>
- using assms by (simp add: multiset_def flip: insert_Collect)
+ \<open>finite {x. 0 < (if x = a then Suc (M x) else M x)}\<close>
+ if \<open>finite {x. 0 < M x}\<close>
+ using that by (simp add: flip: insert_Collect)
lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is
"\<lambda>a M b. if b = a then Suc (M b) else M b"
@@ -246,7 +226,7 @@
lemma finite_set_mset [iff]:
"finite (set_mset M)"
- using count [of M] by (simp add: multiset_def)
+ using count [of M] by simp
lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
by (auto simp flip: count_greater_eq_Suc_zero_iff split: if_splits)
@@ -1029,18 +1009,18 @@
lift_definition Inf_multiset :: "'a multiset set \<Rightarrow> 'a multiset" is
"\<lambda>A i. if A = {} then 0 else Inf ((\<lambda>f. f i) ` A)"
proof -
- fix A :: "('a \<Rightarrow> nat) set" assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<in> multiset"
- have "finite {i. (if A = {} then 0 else Inf ((\<lambda>f. f i) ` A)) > 0}" unfolding multiset_def
+ fix A :: "('a \<Rightarrow> nat) set"
+ assume *: "\<And>f. f \<in> A \<Longrightarrow> finite {x. 0 < f x}"
+ show \<open>finite {i. 0 < (if A = {} then 0 else INF f\<in>A. f i)}\<close>
proof (cases "A = {}")
case False
then obtain f where "f \<in> A" by blast
hence "{i. Inf ((\<lambda>f. f i) ` A) > 0} \<subseteq> {i. f i > 0}"
by (auto intro: less_le_trans[OF _ cInf_lower])
- moreover from \<open>f \<in> A\<close> * have "finite \<dots>" by (simp add: multiset_def)
+ moreover from \<open>f \<in> A\<close> * have "finite \<dots>" by simp
ultimately have "finite {i. Inf ((\<lambda>f. f i) ` A) > 0}" by (rule finite_subset)
with False show ?thesis by simp
qed simp_all
- thus "(\<lambda>i. if A = {} then 0 else INF f\<in>A. f i) \<in> multiset" by (simp add: multiset_def)
qed
instance ..
@@ -1098,10 +1078,9 @@
qed
lemma Sup_multiset_in_multiset:
- assumes "A \<noteq> {}" "subset_mset.bdd_above A"
- shows "(\<lambda>i. SUP X\<in>A. count X i) \<in> multiset"
- unfolding multiset_def
-proof
+ \<open>finite {i. 0 < (SUP M\<in>A. count M i)}\<close>
+ if \<open>A \<noteq> {}\<close> \<open>subset_mset.bdd_above A\<close>
+proof -
have "{i. Sup ((\<lambda>X. count X i) ` A) > 0} \<subseteq> (\<Union>X\<in>A. {i. 0 < count X i})"
proof safe
fix i assume pos: "(SUP X\<in>A. count X i) > 0"
@@ -1109,20 +1088,21 @@
proof (rule ccontr)
assume "i \<notin> (\<Union>X\<in>A. {i. 0 < count X i})"
hence "\<forall>X\<in>A. count X i \<le> 0" by (auto simp: count_eq_zero_iff)
- with assms have "(SUP X\<in>A. count X i) \<le> 0"
+ with that have "(SUP X\<in>A. count X i) \<le> 0"
by (intro cSup_least bdd_above_multiset_imp_bdd_above_count) auto
with pos show False by simp
qed
qed
- moreover from assms have "finite \<dots>" by (rule bdd_above_multiset_imp_finite_support)
- ultimately show "finite {i. Sup ((\<lambda>X. count X i) ` A) > 0}" by (rule finite_subset)
+ moreover from that have "finite \<dots>"
+ by (rule bdd_above_multiset_imp_finite_support)
+ ultimately show "finite {i. Sup ((\<lambda>X. count X i) ` A) > 0}"
+ by (rule finite_subset)
qed
lemma count_Sup_multiset_nonempty:
- assumes "A \<noteq> {}" "subset_mset.bdd_above A"
- shows "count (Sup A) x = (SUP X\<in>A. count X x)"
- using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset)
-
+ \<open>count (Sup A) x = (SUP X\<in>A. count X x)\<close>
+ if \<open>A \<noteq> {}\<close> \<open>subset_mset.bdd_above A\<close>
+ using that by (simp add: Sup_multiset_def Sup_multiset_in_multiset count_Abs_multiset)
interpretation subset_mset: conditionally_complete_lattice Inf Sup "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
proof
@@ -3700,7 +3680,7 @@
by (rule natLeq_cinfinite)
show "ordLeq3 (card_of (set_mset X)) natLeq" for X
by transfer
- (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
+ (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric])
show "rel_mset R OO rel_mset S \<le> rel_mset (R OO S)" for R S
unfolding rel_mset_def[abs_def] OO_def
apply clarify
@@ -3749,9 +3729,8 @@
unfolding rel_mset_def Grp_def by auto
declare multiset.count[simp]
-declare Abs_multiset_inverse[simp]
+declare count_Abs_multiset[simp]
declare multiset.count_inverse[simp]
-declare union_preserves_multiset[simp]
lemma rel_mset_Plus:
assumes ab: "R a b"
--- a/src/HOL/Library/Permutation.thy Wed Feb 24 14:49:16 2021 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,230 +0,0 @@
-(* Title: HOL/Library/Permutation.thy
- Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker
-*)
-
-section \<open>Permutations\<close>
-
-theory Permutation
-imports Multiset
-begin
-
-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
-
-
-subsection \<open>Some examples of rule induction on permutations\<close>
-
-proposition perm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []"
- by (induction "[] :: 'a list" ys pred: perm) simp_all
-
-
-text \<open>\medskip This more general theorem is easier to understand!\<close>
-
-proposition perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys"
- by (induct pred: perm) simp_all
-
-proposition perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs"
- by (induct pred: perm) auto
-
-
-subsection \<open>Ways of making new permutations\<close>
-
-text \<open>We can insert the head anywhere in the list.\<close>
-
-proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
- by (induct xs) auto
-
-proposition perm_append_swap: "xs @ ys <~~> ys @ xs"
- by (induct xs) (auto intro: perm_append_Cons)
-
-proposition perm_append_single: "a # xs <~~> xs @ [a]"
- by (rule perm.trans [OF _ perm_append_swap]) simp
-
-proposition perm_rev: "rev xs <~~> xs"
- by (induct xs) (auto intro!: perm_append_single intro: perm_sym)
-
-proposition perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys"
- by (induct l) auto
-
-proposition perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l"
- by (blast intro!: perm_append_swap perm_append1)
-
-
-subsection \<open>Further results\<close>
-
-proposition perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []"
- by (blast intro: perm_empty_imp)
-
-proposition perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []"
- using perm_sym by auto
-
-proposition perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]"
- by (induct pred: perm) auto
-
-proposition perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]"
- by (blast intro: perm_sing_imp)
-
-proposition perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]"
- by (blast dest: perm_sym)
-
-
-subsection \<open>Removing elements\<close>
-
-proposition perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys"
- by (induct ys) auto
-
-
-text \<open>\medskip Congruence rule\<close>
-
-proposition perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys"
- by (induct pred: perm) auto
-
-proposition remove_hd [simp]: "remove1 z (z # xs) = xs"
- by auto
-
-proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
- by (drule perm_remove_perm [where z = z]) auto
-
-proposition cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys"
- by (meson cons_perm_imp_perm perm.Cons)
-
-proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys"
- by (induct zs arbitrary: xs ys rule: rev_induct) auto
-
-proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys"
- by (blast intro: append_perm_imp_perm perm_append1)
-
-proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys"
- by (meson perm.trans perm_append1_eq perm_append_swap)
-
-theorem mset_eq_perm: "mset xs = mset ys \<longleftrightarrow> xs <~~> ys"
-proof
- assume "mset xs = mset ys"
- then show "xs <~~> ys"
- proof (induction xs arbitrary: ys)
- case (Cons x xs)
- then have "x \<in> set ys"
- using mset_eq_setD by fastforce
- then show ?case
- by (metis Cons.IH Cons.prems mset_remove1 perm.Cons perm.trans perm_remove perm_sym remove_hd)
- qed auto
-next
- assume "xs <~~> ys"
- then show "mset xs = mset ys"
- by induction (simp_all add: union_ac)
-qed
-
-proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
- apply (rule iffI)
- apply (metis mset_append mset_eq_perm mset_subset_eq_exists_conv surjD surj_mset)
- by (metis mset_append mset_eq_perm mset_subset_eq_exists_conv)
-
-proposition perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys"
- by (metis mset_eq_perm mset_eq_setD)
-
-proposition perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys"
- by (metis card_distinct distinct_card perm_length perm_set_eq)
-
-theorem eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys"
-proof (induction xs arbitrary: ys rule: length_induct)
- case (1 xs)
- show ?case
- proof (cases "remdups xs")
- case Nil
- with "1.prems" show ?thesis
- using "1.prems" by auto
- next
- case (Cons x us)
- then have "x \<in> set (remdups ys)"
- using "1.prems" set_remdups by fastforce
- then show ?thesis
- using "1.prems" mset_eq_perm set_eq_iff_mset_remdups_eq by blast
- qed
-qed
-
-proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y"
- by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
-
-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))"
- using assms
-proof induct
- case Nil
- then show ?case
- unfolding bij_betw_def by simp
-next
- case (swap y x l)
- show ?case
- proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
- show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
- by (auto simp: bij_betw_def)
- fix i
- assume "i < length (y # x # l)"
- show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
- by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
- qed
-next
- case (Cons xs ys z)
- then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}"
- and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)"
- by blast
- let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
- show ?case
- proof (intro exI[of _ ?f] allI conjI impI)
- have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"
- "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"
- by (simp_all add: lessThan_Suc_eq_insert_0)
- show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}"
- unfolding *
- proof (rule bij_betw_combine)
- show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
- using bij unfolding bij_betw_def
- by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def)
- qed (auto simp: bij_betw_def)
- fix i
- assume "i < length (z # xs)"
- then show "(z # xs) ! i = (z # ys) ! (?f i)"
- using perm by (cases i) auto
- qed
-next
- case (trans xs ys zs)
- then obtain f g
- where bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}"
- and perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)"
- by blast
- show ?case
- proof (intro exI[of _ "g \<circ> f"] conjI allI impI)
- show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
- using bij by (rule bij_betw_trans)
- fix i
- assume "i < length xs"
- with bij have "f i < length ys"
- unfolding bij_betw_def by force
- with \<open>i < length xs\<close> show "xs ! i = zs ! (g \<circ> f) i"
- using trans(1,3)[THEN perm_length] perm by auto
- qed
-qed
-
-proposition perm_finite: "finite {B. B <~~> A}"
-proof (rule finite_subset[where B="{xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"])
- show "finite {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"
- using finite_lists_length_le by blast
-next
- show "{B. B <~~> A} \<subseteq> {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"
- by (clarsimp simp add: perm_length perm_set_eq)
-qed
-
-proposition perm_swap:
- assumes "i < length xs" "j < length xs"
- shows "xs[i := xs ! j, j := xs ! i] <~~> xs"
- using assms by (simp add: mset_eq_perm[symmetric] mset_swap)
-
-end
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Wed Feb 24 14:49:36 2021 +0000
@@ -32,6 +32,7 @@
val theorems_of_sucessful_proof : Toplevel.state option -> thm list
val get_setting : (string * string) list -> string * string -> string
val get_int_setting : (string * string) list -> string * int -> int
+ val get_bool_setting : (string * string) list -> string * bool -> bool
val cpu_time : ('a -> 'b) -> 'a -> 'b * int
end
@@ -209,6 +210,12 @@
| SOME NONE => error ("bad option: " ^ key)
| NONE => default)
+fun get_bool_setting settings (key, default) =
+ (case Option.map Bool.fromString (AList.lookup (op =) settings key) of
+ SOME (SOME i) => i
+ | SOME NONE => error ("bad option: " ^ key)
+ | NONE => default)
+
fun cpu_time f x =
let val ({cpu, ...}, y) = Timing.timing f x
in (y, Time.toMilliseconds cpu) end
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Feb 24 14:49:36 2021 +0000
@@ -33,6 +33,7 @@
val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*)
val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*)
val strictK = "strict" (*=BOOL: run in strict mode*)
+val strideK = "stride" (*=NUM: run every nth goal*)
val term_orderK = "term_order" (*=STRING: term order (in E)*)
val type_encK = "type_enc" (*=STRING: type encoding scheme*)
val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*)
@@ -50,10 +51,11 @@
val fact_filter_default = "smart"
val type_enc_default = "smart"
val strict_default = "false"
+val stride_default = 1
val max_facts_default = "smart"
val slice_default = "true"
-val max_calls_default = "10000000"
-val trivial_default = "false"
+val max_calls_default = 10000000
+val check_trivial_default = false
(*If a key is present in args then augment a list with its pair*)
(*This is used to avoid fixing default values at the Mirabelle level, and
@@ -605,37 +607,49 @@
(* crude hack *)
val num_sledgehammer_calls = Unsynchronized.ref 0
+val remaining_stride = Unsynchronized.ref stride_default
-fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
- let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
- if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
- then () else
- let
- val max_calls =
- AList.lookup (op =) args max_callsK |> the_default max_calls_default
- |> Int.fromString |> the
- val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1;
- in
- if !num_sledgehammer_calls > max_calls then ()
- else
- let
- val meth = Unsynchronized.ref ""
- val named_thms =
- Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
- val trivial =
- if AList.lookup (op =) args check_trivialK |> the_default trivial_default
- |> Value.parse_bool then
- Try0.try0 (SOME try_timeout) ([], [], [], []) pre
- handle Timeout.TIMEOUT _ => false
- else false
- fun apply_method () =
- (Mirabelle.catch_result (proof_method_tag meth) false
- (run_proof_method trivial false name meth (these (!named_thms))) id st; ())
- in
- Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st;
- if is_some (!named_thms) then apply_method () else ()
- end
- end
+fun sledgehammer_action args =
+ let
+ val stride = Mirabelle.get_int_setting args (strideK, stride_default)
+ val max_calls = Mirabelle.get_int_setting args (max_callsK, max_calls_default)
+ val check_trivial = Mirabelle.get_bool_setting args (check_trivialK, check_trivial_default)
+ in
+ fn id => fn (st as {pre, name, log, ...}: Mirabelle.run_args) =>
+ let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
+ if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then
+ ()
+ else if !remaining_stride > 1 then
+ (* We still have some steps to do *)
+ (remaining_stride := !remaining_stride - 1;
+ log "Skipping because of stride")
+ else
+ (* This was the last step, now run the action *)
+ let
+ val _ = remaining_stride := stride
+ val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1
+ in
+ if !num_sledgehammer_calls > max_calls then
+ log "Skipping because max number of calls reached"
+ else
+ let
+ val meth = Unsynchronized.ref ""
+ val named_thms =
+ Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
+ val trivial =
+ if check_trivial then
+ Try0.try0 (SOME try_timeout) ([], [], [], []) pre
+ handle Timeout.TIMEOUT _ => false
+ else false
+ fun apply_method () =
+ (Mirabelle.catch_result (proof_method_tag meth) false
+ (run_proof_method trivial false name meth (these (!named_thms))) id st; ())
+ in
+ Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st;
+ if is_some (!named_thms) then apply_method () else ()
+ end
+ end
+ end
end
fun invoke args =
--- a/src/HOL/Orderings.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Orderings.thy Wed Feb 24 14:49:36 2021 +0000
@@ -13,114 +13,160 @@
subsection \<open>Abstract ordering\<close>
-locale ordering =
- fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50)
- and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50)
- assumes strict_iff_order: "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b"
- assumes refl: "a \<^bold>\<le> a" \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
- and antisym: "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>\<le> a \<Longrightarrow> a = b"
- and trans: "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>\<le> c \<Longrightarrow> a \<^bold>\<le> c"
+locale partial_preordering =
+ fixes less_eq :: \<open>'a \<Rightarrow> 'a \<Rightarrow> bool\<close> (infix \<open>\<^bold>\<le>\<close> 50)
+ assumes refl: \<open>a \<^bold>\<le> a\<close> \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
+ and trans: \<open>a \<^bold>\<le> b \<Longrightarrow> b \<^bold>\<le> c \<Longrightarrow> a \<^bold>\<le> c\<close>
+
+locale preordering = partial_preordering +
+ fixes less :: \<open>'a \<Rightarrow> 'a \<Rightarrow> bool\<close> (infix \<open>\<^bold><\<close> 50)
+ assumes strict_iff_not: \<open>a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> \<not> b \<^bold>\<le> a\<close>
begin
lemma strict_implies_order:
- "a \<^bold>< b \<Longrightarrow> a \<^bold>\<le> b"
- by (simp add: strict_iff_order)
+ \<open>a \<^bold>< b \<Longrightarrow> a \<^bold>\<le> b\<close>
+ by (simp add: strict_iff_not)
+
+lemma irrefl: \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
+ \<open>\<not> a \<^bold>< a\<close>
+ by (simp add: strict_iff_not)
+
+lemma asym:
+ \<open>a \<^bold>< b \<Longrightarrow> b \<^bold>< a \<Longrightarrow> False\<close>
+ by (auto simp add: strict_iff_not)
+
+lemma strict_trans1:
+ \<open>a \<^bold>\<le> b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c\<close>
+ by (auto simp add: strict_iff_not intro: trans)
+
+lemma strict_trans2:
+ \<open>a \<^bold>< b \<Longrightarrow> b \<^bold>\<le> c \<Longrightarrow> a \<^bold>< c\<close>
+ by (auto simp add: strict_iff_not intro: trans)
+
+lemma strict_trans:
+ \<open>a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c\<close>
+ by (auto intro: strict_trans1 strict_implies_order)
+
+end
+
+lemma preordering_strictI: \<comment> \<open>Alternative introduction rule with bias towards strict order\<close>
+ fixes less_eq (infix \<open>\<^bold>\<le>\<close> 50)
+ and less (infix \<open>\<^bold><\<close> 50)
+ assumes less_eq_less: \<open>\<And>a b. a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>< b \<or> a = b\<close>
+ assumes asym: \<open>\<And>a b. a \<^bold>< b \<Longrightarrow> \<not> b \<^bold>< a\<close>
+ assumes irrefl: \<open>\<And>a. \<not> a \<^bold>< a\<close>
+ assumes trans: \<open>\<And>a b c. a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c\<close>
+ shows \<open>preordering (\<^bold>\<le>) (\<^bold><)\<close>
+proof
+ fix a b
+ show \<open>a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> \<not> b \<^bold>\<le> a\<close>
+ by (auto simp add: less_eq_less asym irrefl)
+next
+ fix a
+ show \<open>a \<^bold>\<le> a\<close>
+ by (auto simp add: less_eq_less)
+next
+ fix a b c
+ assume \<open>a \<^bold>\<le> b\<close> and \<open>b \<^bold>\<le> c\<close> then show \<open>a \<^bold>\<le> c\<close>
+ by (auto simp add: less_eq_less intro: trans)
+qed
+
+lemma preordering_dualI:
+ fixes less_eq (infix \<open>\<^bold>\<le>\<close> 50)
+ and less (infix \<open>\<^bold><\<close> 50)
+ assumes \<open>preordering (\<lambda>a b. b \<^bold>\<le> a) (\<lambda>a b. b \<^bold>< a)\<close>
+ shows \<open>preordering (\<^bold>\<le>) (\<^bold><)\<close>
+proof -
+ from assms interpret preordering \<open>\<lambda>a b. b \<^bold>\<le> a\<close> \<open>\<lambda>a b. b \<^bold>< a\<close> .
+ show ?thesis
+ by standard (auto simp: strict_iff_not refl intro: trans)
+qed
+
+locale ordering = partial_preordering +
+ fixes less :: \<open>'a \<Rightarrow> 'a \<Rightarrow> bool\<close> (infix \<open>\<^bold><\<close> 50)
+ assumes strict_iff_order: \<open>a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b\<close>
+ assumes antisym: \<open>a \<^bold>\<le> b \<Longrightarrow> b \<^bold>\<le> a \<Longrightarrow> a = b\<close>
+begin
+
+sublocale preordering \<open>(\<^bold>\<le>)\<close> \<open>(\<^bold><)\<close>
+proof
+ show \<open>a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> \<not> b \<^bold>\<le> a\<close> for a b
+ by (auto simp add: strict_iff_order intro: antisym)
+qed
lemma strict_implies_not_eq:
- "a \<^bold>< b \<Longrightarrow> a \<noteq> b"
+ \<open>a \<^bold>< b \<Longrightarrow> a \<noteq> b\<close>
by (simp add: strict_iff_order)
lemma not_eq_order_implies_strict:
- "a \<noteq> b \<Longrightarrow> a \<^bold>\<le> b \<Longrightarrow> a \<^bold>< b"
+ \<open>a \<noteq> b \<Longrightarrow> a \<^bold>\<le> b \<Longrightarrow> a \<^bold>< b\<close>
by (simp add: strict_iff_order)
lemma order_iff_strict:
- "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>< b \<or> a = b"
+ \<open>a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>< b \<or> a = b\<close>
by (auto simp add: strict_iff_order refl)
-lemma irrefl: \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
- "\<not> a \<^bold>< a"
- by (simp add: strict_iff_order)
-
-lemma asym:
- "a \<^bold>< b \<Longrightarrow> b \<^bold>< a \<Longrightarrow> False"
- by (auto simp add: strict_iff_order intro: antisym)
-
-lemma strict_trans1:
- "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
- by (auto simp add: strict_iff_order intro: trans antisym)
-
-lemma strict_trans2:
- "a \<^bold>< b \<Longrightarrow> b \<^bold>\<le> c \<Longrightarrow> a \<^bold>< c"
- by (auto simp add: strict_iff_order intro: trans antisym)
-
-lemma strict_trans:
- "a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
- by (auto intro: strict_trans1 strict_implies_order)
-
-lemma eq_iff: "a = b \<longleftrightarrow> a \<^bold>\<le> b \<and> b \<^bold>\<le> a"
+lemma eq_iff: \<open>a = b \<longleftrightarrow> a \<^bold>\<le> b \<and> b \<^bold>\<le> a\<close>
by (auto simp add: refl intro: antisym)
end
-text \<open>Alternative introduction rule with bias towards strict order\<close>
-
-lemma ordering_strictI:
- fixes less_eq (infix "\<^bold>\<le>" 50)
- and less (infix "\<^bold><" 50)
- assumes less_eq_less: "\<And>a b. a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>< b \<or> a = b"
- assumes asym: "\<And>a b. a \<^bold>< b \<Longrightarrow> \<not> b \<^bold>< a"
- assumes irrefl: "\<And>a. \<not> a \<^bold>< a"
- assumes trans: "\<And>a b c. a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
- shows "ordering less_eq less"
+lemma ordering_strictI: \<comment> \<open>Alternative introduction rule with bias towards strict order\<close>
+ fixes less_eq (infix \<open>\<^bold>\<le>\<close> 50)
+ and less (infix \<open>\<^bold><\<close> 50)
+ assumes less_eq_less: \<open>\<And>a b. a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>< b \<or> a = b\<close>
+ assumes asym: \<open>\<And>a b. a \<^bold>< b \<Longrightarrow> \<not> b \<^bold>< a\<close>
+ assumes irrefl: \<open>\<And>a. \<not> a \<^bold>< a\<close>
+ assumes trans: \<open>\<And>a b c. a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c\<close>
+ shows \<open>ordering (\<^bold>\<le>) (\<^bold><)\<close>
proof
fix a b
- show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b"
+ show \<open>a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b\<close>
by (auto simp add: less_eq_less asym irrefl)
next
fix a
- show "a \<^bold>\<le> a"
+ show \<open>a \<^bold>\<le> a\<close>
by (auto simp add: less_eq_less)
next
fix a b c
- assume "a \<^bold>\<le> b" and "b \<^bold>\<le> c" then show "a \<^bold>\<le> c"
+ assume \<open>a \<^bold>\<le> b\<close> and \<open>b \<^bold>\<le> c\<close> then show \<open>a \<^bold>\<le> c\<close>
by (auto simp add: less_eq_less intro: trans)
next
fix a b
- assume "a \<^bold>\<le> b" and "b \<^bold>\<le> a" then show "a = b"
+ assume \<open>a \<^bold>\<le> b\<close> and \<open>b \<^bold>\<le> a\<close> then show \<open>a = b\<close>
by (auto simp add: less_eq_less asym)
qed
lemma ordering_dualI:
- fixes less_eq (infix "\<^bold>\<le>" 50)
- and less (infix "\<^bold><" 50)
- assumes "ordering (\<lambda>a b. b \<^bold>\<le> a) (\<lambda>a b. b \<^bold>< a)"
- shows "ordering less_eq less"
+ fixes less_eq (infix \<open>\<^bold>\<le>\<close> 50)
+ and less (infix \<open>\<^bold><\<close> 50)
+ assumes \<open>ordering (\<lambda>a b. b \<^bold>\<le> a) (\<lambda>a b. b \<^bold>< a)\<close>
+ shows \<open>ordering (\<^bold>\<le>) (\<^bold><)\<close>
proof -
- from assms interpret ordering "\<lambda>a b. b \<^bold>\<le> a" "\<lambda>a b. b \<^bold>< a" .
+ from assms interpret ordering \<open>\<lambda>a b. b \<^bold>\<le> a\<close> \<open>\<lambda>a b. b \<^bold>< a\<close> .
show ?thesis
by standard (auto simp: strict_iff_order refl intro: antisym trans)
qed
locale ordering_top = ordering +
- fixes top :: "'a" ("\<^bold>\<top>")
- assumes extremum [simp]: "a \<^bold>\<le> \<^bold>\<top>"
+ fixes top :: \<open>'a\<close> (\<open>\<^bold>\<top>\<close>)
+ assumes extremum [simp]: \<open>a \<^bold>\<le> \<^bold>\<top>\<close>
begin
lemma extremum_uniqueI:
- "\<^bold>\<top> \<^bold>\<le> a \<Longrightarrow> a = \<^bold>\<top>"
+ \<open>\<^bold>\<top> \<^bold>\<le> a \<Longrightarrow> a = \<^bold>\<top>\<close>
by (rule antisym) auto
lemma extremum_unique:
- "\<^bold>\<top> \<^bold>\<le> a \<longleftrightarrow> a = \<^bold>\<top>"
+ \<open>\<^bold>\<top> \<^bold>\<le> a \<longleftrightarrow> a = \<^bold>\<top>\<close>
by (auto intro: antisym)
lemma extremum_strict [simp]:
- "\<not> (\<^bold>\<top> \<^bold>< a)"
+ \<open>\<not> (\<^bold>\<top> \<^bold>< a)\<close>
using extremum [of a] by (auto simp add: order_iff_strict intro: asym irrefl)
lemma not_eq_extremum:
- "a \<noteq> \<^bold>\<top> \<longleftrightarrow> a \<^bold>< \<^bold>\<top>"
+ \<open>a \<noteq> \<^bold>\<top> \<longleftrightarrow> a \<^bold>< \<^bold>\<top>\<close>
by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum)
end
@@ -165,6 +211,16 @@
and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
begin
+sublocale order: preordering less_eq less + dual_order: preordering greater_eq greater
+proof -
+ interpret preordering less_eq less
+ by standard (auto intro: order_trans simp add: less_le_not_le)
+ show \<open>preordering less_eq less\<close>
+ by (fact preordering_axioms)
+ then show \<open>preordering greater_eq greater\<close>
+ by (rule preordering_dualI)
+qed
+
text \<open>Reflexivity.\<close>
lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
@@ -217,7 +273,7 @@
text \<open>Dual order\<close>
lemma dual_preorder:
- "class.preorder (\<ge>) (>)"
+ \<open>class.preorder (\<ge>) (>)\<close>
by standard (auto simp add: less_le_not_le intro: order_trans)
end
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Feb 24 14:49:36 2021 +0000
@@ -3,7 +3,7 @@
section \<open>Formalization of a Countermeasure by Koepf \& Duermuth 2009\<close>
theory Koepf_Duermuth_Countermeasure
- imports "HOL-Probability.Information" "HOL-Library.Permutation"
+ imports "HOL-Probability.Information" "HOL-Library.List_Permutation"
begin
lemma SIGMA_image_vimage:
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Wed Feb 24 14:49:36 2021 +0000
@@ -103,30 +103,33 @@
[bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()];
val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem;
val _ = File.write prob_path prob_str;
- val {out = output, err = error, rc = code, ...} = Isabelle_System.bash_process bash_cmd;
+ val res = Isabelle_System.bash_process bash_cmd;
+ val rc = Process_Result.rc res;
+ val out = Process_Result.out res;
+ val err = Process_Result.err res;
val backend =
- (case map_filter (try (unprefix "{backend:")) (split_lines output) of
+ (case map_filter (try (unprefix "{backend:")) (split_lines out) of
[s] => hd (space_explode "," s)
| _ => unknown_solver);
in
- if String.isPrefix "SAT" output then
- (if sound then Sat else Unknown o SOME) (backend, output, {tys = [], tms = []})
- else if String.isPrefix "UNSAT" output then
+ if String.isPrefix "SAT" out then
+ (if sound then Sat else Unknown o SOME) (backend, out, {tys = [], tms = []})
+ else if String.isPrefix "UNSAT" out then
if complete then Unsat backend else Unknown NONE
- else if String.isSubstring "TIMEOUT" output
+ else if String.isSubstring "TIMEOUT" out
(* FIXME: temporary *)
- orelse String.isSubstring "kodkod failed (errcode 152)" error then
+ orelse String.isSubstring "kodkod failed (errcode 152)" err then
Timeout
- else if String.isPrefix "UNKNOWN" output then
+ else if String.isPrefix "UNKNOWN" out then
Unknown NONE
- else if code = 126 then
+ else if rc = 126 then
Nunchaku_Cannot_Execute
- else if code = 127 then
+ else if rc = 127 then
Nunchaku_Not_Found
else
- Unknown_Error (code,
- simplify_spaces (elide_string 1000 (if error <> "" then error else output)))
+ Unknown_Error (rc,
+ simplify_spaces (elide_string 1000 (if err <> "" then err else out)))
end);
fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem =
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Feb 24 14:49:36 2021 +0000
@@ -818,11 +818,12 @@
if getenv env_var = "" then
(warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
else
- (case Isabelle_System.bash_output (cmd ^ File.bash_path file) of
- (out, 0) => out
- | (_, rc) =>
- error ("Error caused by prolog system " ^ env_var ^
- ": return code " ^ string_of_int rc))
+ let val res = Isabelle_System.bash_process (cmd ^ File.bash_path file) in
+ res |> Process_Result.check |> Process_Result.out
+ handle ERROR msg =>
+ cat_error ("Error caused by prolog system " ^ env_var ^
+ ": return code " ^ string_of_int (Process_Result.rc res)) msg
+ end
end
@@ -865,7 +866,7 @@
(l :: r :: []) => parse_term (unprefix " " r)
| _ => raise Fail "unexpected equation in prolog output")
fun parse_solution s = map dest_eq (space_explode ";" s)
- in map parse_solution (Library.trim_split_lines sol) end
+ in map parse_solution (split_lines sol) end
(* calling external interpreter and getting results *)
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Feb 24 14:49:36 2021 +0000
@@ -214,10 +214,6 @@
|> Exn.capture f
|> Exn.release
-fun elapsed_time description e =
- let val ({elapsed, ...}, result) = Timing.timing e ()
- in (result, (description, Time.toMilliseconds elapsed)) end
-
fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size))
ctxt cookie (code_modules, _) =
let
@@ -265,23 +261,29 @@
(map File.bash_platform_path
(map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
" -o " ^ File.bash_platform_path executable ^ ";"
- val (_, compilation_time) =
- elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
- val _ = Quickcheck.add_timing compilation_time current_result
+ val compilation_time =
+ Isabelle_System.bash_process cmd
+ |> Process_Result.check
+ |> Process_Result.timing_elapsed |> Time.toMilliseconds
+ handle ERROR msg => cat_error "Compilation with GHC failed" msg
+ val _ = Quickcheck.add_timing ("Haskell compilation", compilation_time) current_result
fun haskell_string_of_bool v = if v then "True" else "False"
- val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
fun with_size genuine_only k =
if k > size then (NONE, !current_result)
else
let
val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
val _ = current_size := k
- val ((response, _), timing) =
- elapsed_time ("execution of size " ^ string_of_int k)
- (fn () => Isabelle_System.bash_output
- (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^
- string_of_int k))
- val _ = Quickcheck.add_timing timing current_result
+ val res =
+ Isabelle_System.bash_process
+ (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^
+ string_of_int k)
+ |> Process_Result.check
+ val response = Process_Result.out res
+ val timing = res |> Process_Result.timing_elapsed |> Time.toMilliseconds;
+ val _ =
+ Quickcheck.add_timing
+ ("execution of size " ^ string_of_int k, timing) current_result
in
if response = "NONE" then with_size genuine_only (k + 1)
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Feb 24 14:49:36 2021 +0000
@@ -550,12 +550,12 @@
|> extra_options <> "" ? prefix (extra_options ^ " "),
proof_delims = tstp_proof_delims,
known_failures = known_szs_status_failures,
- prem_role = Conjecture,
+ prem_role = Hypothesis,
best_slices = fn _ =>
(* FUDGE *)
- [(0.333, (((128, "meshN"), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
+ [(0.333, (((128, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
(0.333, (((32, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
- (0.334, (((512, "meshN"), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
+ (0.334, (((512, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -574,7 +574,7 @@
(warning
(case extract_known_atp_failure known_perl_failures output of
SOME failure => string_of_atp_failure failure
- | NONE => trim_line output); []))) ()
+ | NONE => output); []))) ()
handle Timeout.TIMEOUT _ => []
fun find_remote_system name [] systems =
--- a/src/Pure/Admin/components.scala Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/Admin/components.scala Wed Feb 24 14:49:36 2021 +0000
@@ -279,9 +279,8 @@
}
yield {
progress.echo("Digesting remote " + entry.name)
- Library.trim_line(
- ssh.execute("cd " + ssh.bash_path(components_dir) +
- "; sha1sum " + Bash.string(entry.name)).check.out)
+ ssh.execute("cd " + ssh.bash_path(components_dir) +
+ "; sha1sum " + Bash.string(entry.name)).check.out
}
write_components_sha1(read_components_sha1(lines))
}
--- a/src/Pure/General/exn.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/General/exn.ML Wed Feb 24 14:49:36 2021 +0000
@@ -105,7 +105,7 @@
(* POSIX return code *)
fun return_code exn rc =
- if is_interrupt exn then (130: int) else rc;
+ if is_interrupt exn then 130 else rc;
fun capture_exit rc f x =
f x handle exn => exit (return_code exn rc);
--- a/src/Pure/ROOT.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/ROOT.ML Wed Feb 24 14:49:36 2021 +0000
@@ -294,6 +294,7 @@
(*Isabelle system*)
ML_file "PIDE/protocol_command.ML";
ML_file "System/scala.ML";
+ML_file "System/process_result.ML";
ML_file "System/isabelle_system.ML";
--- a/src/Pure/System/bash.scala Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/System/bash.scala Wed Feb 24 14:49:36 2021 +0000
@@ -223,8 +223,11 @@
case _ if is_interrupt => ""
case Exn.Exn(exn) => Exn.message(exn)
case Exn.Res(res) =>
- (res.rc.toString :: res.out_lines.length.toString ::
- res.out_lines ::: res.err_lines).mkString("\u0000")
+ (res.rc.toString ::
+ res.timing.elapsed.ms.toString ::
+ res.timing.cpu.ms.toString ::
+ res.out_lines.length.toString ::
+ res.out_lines ::: res.err_lines).mkString("\u0000")
}
}
}
--- a/src/Pure/System/isabelle_system.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/System/isabelle_system.ML Wed Feb 24 14:49:36 2021 +0000
@@ -6,10 +6,7 @@
signature ISABELLE_SYSTEM =
sig
- type process_result =
- {rc: int, out_lines: string list, err_lines: string list, out: string, err: string}
- val bash_process: string -> process_result
- val bash_output_check: string -> string
+ val bash_process: string -> Process_Result.T
val bash_output: string -> string * int
val bash: string -> int
val bash_functions: unit -> string list
@@ -31,45 +28,42 @@
(* bash *)
-type process_result =
- {rc: int, out_lines: string list, err_lines: string list, out: string, err: string};
-
-fun bash_process script : process_result =
+fun bash_process script =
Scala.function_thread "bash_process"
("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
|> space_explode "\000"
|> (fn [] => raise Exn.Interrupt
| [err] => error err
- | a :: b :: lines =>
+ | a :: b :: c :: d :: lines =>
let
val rc = Value.parse_int a;
- val ((out, err), (out_lines, err_lines)) =
- chop (Value.parse_int b) lines |> `(apply2 cat_lines);
- in {rc = rc, out_lines = out_lines, err_lines = err_lines, out = out, err = err} end);
+ val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c);
+ val (out_lines, err_lines) = chop (Value.parse_int d) lines;
+ in
+ Process_Result.make
+ {rc = rc,
+ out_lines = out_lines,
+ err_lines = err_lines,
+ timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
+ end
+ | _ => raise Fail "Malformed Isabelle/Scala result");
-fun bash_output_check s =
- (case bash_process s of
- {rc = 0, out, ...} => trim_line out
- | {err, ...} => error (trim_line err));
+val bash = bash_process #> Process_Result.print #> Process_Result.rc;
fun bash_output s =
let
- val {out, err, rc, ...} = bash_process s;
- val _ = warning (trim_line err);
- in (out, rc) end;
-
-fun bash s =
- let
- val (out, rc) = bash_output s;
- val _ = writeln (trim_line out);
- in rc end;
+ val res = bash_process s;
+ val _ = warning (Process_Result.err res);
+ in (Process_Result.out res, Process_Result.rc res) end;
(* bash functions *)
fun bash_functions () =
- bash_output_check "declare -Fx"
- |> split_lines |> map_filter (space_explode " " #> try List.last);
+ bash_process "declare -Fx"
+ |> Process_Result.check
+ |> Process_Result.out_lines
+ |> map_filter (space_explode " " #> try List.last);
fun check_bash_function ctxt arg =
Completion.check_entity Markup.bash_functionN
@@ -145,9 +139,12 @@
fun download url =
with_tmp_file "download" "" (fn path =>
- ("curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path)
- |> bash_process
- |> (fn {rc = 0, ...} => File.read path
- | {err, ...} => cat_error ("Failed to download " ^ quote url) err));
+ let
+ val s = "curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path;
+ val res = bash_process s;
+ in
+ if Process_Result.ok res then File.read path
+ else cat_error ("Failed to download " ^ quote url) (Process_Result.err res)
+ end);
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/process_result.ML Wed Feb 24 14:49:36 2021 +0000
@@ -0,0 +1,62 @@
+(* Title: Pure/System/process_result.scala
+ Author: Makarius
+
+Result of system process.
+*)
+
+signature PROCESS_RESULT =
+sig
+ type T
+ val make:
+ {rc: int,
+ out_lines: string list,
+ err_lines: string list,
+ timing: Timing.timing} -> T
+ val rc: T -> int
+ val out_lines: T -> string list
+ val err_lines: T -> string list
+ val timing: T -> Timing.timing
+ val timing_elapsed: T -> Time.time
+ val out: T -> string
+ val err: T -> string
+ val ok: T -> bool
+ val check: T -> T
+ val print: T -> T
+end;
+
+structure Process_Result: PROCESS_RESULT =
+struct
+
+abstype T =
+ Process_Result of
+ {rc: int,
+ out_lines: string list,
+ err_lines: string list,
+ timing: Timing.timing}
+with
+
+val make = Process_Result;
+fun rep (Process_Result args) = args;
+
+val rc = #rc o rep;
+val out_lines = #out_lines o rep;
+val err_lines = #err_lines o rep;
+
+val timing = #timing o rep;
+val timing_elapsed = #elapsed o timing;
+
+end;
+
+val out = trim_line o cat_lines o out_lines;
+val err = trim_line o cat_lines o err_lines;
+
+fun ok result = rc result = 0;
+
+fun check result = if ok result then result else error (err result);
+
+fun print result =
+ (warning (err result);
+ writeln (out result);
+ make {rc = rc result, out_lines = [], err_lines = [], timing = timing result});
+
+end;
--- a/src/Pure/System/process_result.scala Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/System/process_result.scala Wed Feb 24 14:49:36 2021 +0000
@@ -38,8 +38,8 @@
err_lines: List[String] = Nil,
timing: Timing = Timing.zero)
{
- def out: String = cat_lines(out_lines)
- def err: String = cat_lines(err_lines)
+ def out: String = Library.trim_line(cat_lines(out_lines))
+ def err: String = Library.trim_line(cat_lines(err_lines))
def output(outs: List[String]): Process_Result =
copy(out_lines = out_lines ::: outs.flatMap(split_lines))
--- a/src/Pure/Thy/presentation.scala Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/Thy/presentation.scala Wed Feb 24 14:49:36 2021 +0000
@@ -680,7 +680,7 @@
if (!result.ok) {
val message =
Exn.cat_message(
- Library.trim_line(result.err),
+ result.err,
cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
"Failed to build document " + quote(doc.name))
throw new Build_Error(log_lines, message)
--- a/src/Pure/Tools/doc.scala Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/Tools/doc.scala Wed Feb 24 14:49:36 2021 +0000
@@ -22,7 +22,7 @@
dir <- dirs()
catalog = dir + Path.basic("Contents")
if catalog.is_file
- line <- split_lines(Library.trim_line(File.read(catalog)))
+ line <- Library.trim_split_lines(File.read(catalog))
} yield (dir, line)
sealed abstract class Entry
--- a/src/Pure/Tools/generated_files.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/Tools/generated_files.ML Wed Feb 24 14:49:36 2021 +0000
@@ -332,7 +332,9 @@
(* execute compiler -- auxiliary *)
fun execute dir title compile =
- Isabelle_System.bash_output_check ("cd " ^ File.bash_path dir ^ " && " ^ compile)
+ Isabelle_System.bash_process ("cd " ^ File.bash_path dir ^ " && " ^ compile)
+ |> Process_Result.check
+ |> Process_Result.out
handle ERROR msg =>
let val (s, pos) = Input.source_content title
in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end;
--- a/src/Pure/Tools/ghc.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/Tools/ghc.ML Wed Feb 24 14:49:36 2021 +0000
@@ -84,9 +84,10 @@
val template_path = dir + (Path.basic name |> Path.ext "hsfiles");
val _ = File.write template_path (project_template {depends = depends, modules = modules});
val _ =
- Isabelle_System.bash_output_check
+ Isabelle_System.bash_process
("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^
- " --bare " ^ File.bash_platform_path template_path);
+ " --bare " ^ File.bash_platform_path template_path)
+ |> Process_Result.check;
in () end;
end;
--- a/src/Pure/Tools/jedit.ML Wed Feb 24 14:49:16 2021 +0000
+++ b/src/Pure/Tools/jedit.ML Wed Feb 24 14:49:36 2021 +0000
@@ -35,10 +35,13 @@
val xml_file = XML.parse o File.read;
fun xml_resource name =
- let val script = "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name in
- (case Isabelle_System.bash_output script of
- (txt, 0) => XML.parse txt
- | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc))
+ let
+ val res =
+ Isabelle_System.bash_process ("unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name);
+ val rc = Process_Result.rc res;
+ in
+ res |> Process_Result.check |> Process_Result.out |> XML.parse
+ handle ERROR _ => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)
end;