--- a/NEWS Mon Feb 22 22:06:41 2021 +0100
+++ b/NEWS Mon Feb 22 22:41:50 2021 +0100
@@ -9,6 +9,9 @@
*** 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
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy Mon Feb 22 22:06:41 2021 +0100
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Mon Feb 22 22:41:50 2021 +0100
@@ -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 Mon Feb 22 22:06:41 2021 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Mon Feb 22 22:41:50 2021 +0100
@@ -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 Mon Feb 22 22:06:41 2021 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy Mon Feb 22 22:41:50 2021 +0100
@@ -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 Mon Feb 22 22:06:41 2021 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Mon Feb 22 22:41:50 2021 +0100
@@ -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/Library/DAList_Multiset.thy Mon Feb 22 22:06:41 2021 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy Mon Feb 22 22:41:50 2021 +0100
@@ -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/Multiset.thy Mon Feb 22 22:06:41 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Mon Feb 22 22:41:50 2021 +0100
@@ -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/Orderings.thy Mon Feb 22 22:06:41 2021 +0100
+++ b/src/HOL/Orderings.thy Mon Feb 22 22:41:50 2021 +0100
@@ -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