--- a/src/HOL/Conditionally_Complete_Lattices.thy Mon Feb 22 07:49:48 2021 +0000
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Mon Feb 22 07:49:51 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/Orderings.thy Mon Feb 22 07:49:48 2021 +0000
+++ b/src/HOL/Orderings.thy Mon Feb 22 07:49:51 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