--- a/src/HOL/Cardinals/Wellorder_Extension.thy Sun Aug 12 14:31:46 2018 +0200
+++ b/src/HOL/Cardinals/Wellorder_Extension.thy Tue Aug 14 16:05:40 2018 +0100
@@ -110,7 +110,8 @@
using mono_Chains [OF I_init] and \<open>R \<in> Chains I\<close>
by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)
}
- then have 1: "\<forall>R\<in>Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast
+ then have 1: "\<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" if "R\<in>Chains I" for R
+ using that by (subst FI) blast
txt \<open>Zorn's Lemma yields a maximal wellorder m.\<close>
from Zorns_po_lemma [OF 0 1] obtain m :: "('a \<times> 'a) set"
where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and
--- a/src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy Sun Aug 12 14:31:46 2018 +0200
+++ b/src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy Tue Aug 14 16:05:40 2018 +0100
@@ -118,32 +118,26 @@
show "Partial_order ?R"
by (auto simp: partial_order_on_def preorder_on_def
antisym_def refl_on_def trans_def Field_def bot_unique)
- show "\<forall>C\<in>Chains ?R. \<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R"
- proof (safe intro!: bexI del: notI)
- fix c x
- assume c: "c \<in> Chains ?R"
-
- have Inf_c: "Inf c \<noteq> bot" "Inf c \<le> F" if "c \<noteq> {}"
+ show "\<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R" if C: "C \<in> Chains ?R" for C
+ proof (simp, intro exI conjI ballI)
+ have Inf_C: "Inf C \<noteq> bot" "Inf C \<le> F" if "C \<noteq> {}"
proof -
- from c that have "Inf c = bot \<longleftrightarrow> (\<exists>x\<in>c. x = bot)"
+ from C that have "Inf C = bot \<longleftrightarrow> (\<exists>x\<in>C. x = bot)"
unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def)
- with c show "Inf c \<noteq> bot"
+ with C show "Inf C \<noteq> bot"
by (simp add: bot_notin_R)
- from that obtain x where "x \<in> c" by auto
- with c show "Inf c \<le> F"
+ from that obtain x where "x \<in> C" by auto
+ with C show "Inf C \<le> F"
by (auto intro!: Inf_lower2[of x] simp: Chains_def)
qed
- then have [simp]: "inf F (Inf c) = (if c = {} then F else Inf c)"
- using c by (auto simp add: inf_absorb2)
-
- from c show "inf F (Inf c) \<noteq> bot"
- by (simp add: F Inf_c)
- from c show "inf F (Inf c) \<in> Field ?R"
- by (simp add: Chains_def Inf_c F)
-
- assume "x \<in> c"
- with c show "inf F (Inf c) \<le> x" "x \<le> F"
- by (auto intro: Inf_lower simp: Chains_def)
+ then have [simp]: "inf F (Inf C) = (if C = {} then F else Inf C)"
+ using C by (auto simp add: inf_absorb2)
+ from C show "inf F (Inf C) \<noteq> bot"
+ by (simp add: F Inf_C)
+ from C show "inf F (Inf C) \<le> F"
+ by (simp add: Chains_def Inf_C F)
+ with C show "inf F (Inf C) \<le> x" "x \<le> F" if "x \<in> C" for x
+ using that by (auto intro: Inf_lower simp: Chains_def)
qed
qed
then obtain U where U: "U \<in> ?A" "?B U" ..
--- a/src/HOL/Order_Relation.thy Sun Aug 12 14:31:46 2018 +0200
+++ b/src/HOL/Order_Relation.thy Tue Aug 14 16:05:40 2018 +0100
@@ -25,6 +25,9 @@
preorder_on_def partial_order_on_def linear_order_on_def
strict_linear_order_on_def well_order_on_def
+lemma partial_order_onD:
+ assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r"
+ using assms unfolding partial_order_on_def preorder_on_def by auto
lemma preorder_on_empty[simp]: "preorder_on {} {}"
by (simp add: preorder_on_def trans_def)
@@ -133,6 +136,34 @@
with \<open>d \<noteq> a\<close> show "a \<in> Field (r - Id)" unfolding Field_def by blast
qed
+subsection\<open>Relations given by a predicate and the field\<close>
+
+definition relation_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set"
+ where "relation_of P A \<equiv> { (a, b) \<in> A \<times> A. P a b }"
+
+lemma Field_relation_of:
+ assumes "refl_on A (relation_of P A)" shows "Field (relation_of P A) = A"
+ using assms unfolding refl_on_def Field_def by auto
+
+lemma partial_order_on_relation_ofI:
+ assumes refl: "\<And>a. a \<in> A \<Longrightarrow> P a a"
+ and trans: "\<And>a b c. \<lbrakk> a \<in> A; b \<in> A; c \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b c \<Longrightarrow> P a c"
+ and antisym: "\<And>a b. \<lbrakk> a \<in> A; b \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b a \<Longrightarrow> a = b"
+ shows "partial_order_on A (relation_of P A)"
+proof -
+ from refl have "refl_on A (relation_of P A)"
+ unfolding refl_on_def relation_of_def by auto
+ moreover have "trans (relation_of P A)" and "antisym (relation_of P A)"
+ unfolding relation_of_def
+ by (auto intro: transI dest: trans, auto intro: antisymI dest: antisym)
+ ultimately show ?thesis
+ unfolding partial_order_on_def preorder_on_def by simp
+qed
+
+lemma Partial_order_relation_ofI:
+ assumes "partial_order_on A (relation_of P A)" shows "Partial_order (relation_of P A)"
+ using Field_relation_of assms partial_order_on_def preorder_on_def by fastforce
+
subsection \<open>Orders on a type\<close>
--- a/src/HOL/Zorn.thy Sun Aug 12 14:31:46 2018 +0200
+++ b/src/HOL/Zorn.thy Tue Aug 14 16:05:40 2018 +0100
@@ -491,7 +491,7 @@
lemma Zorns_po_lemma:
assumes po: "Partial_order r"
- and u: "\<forall>C\<in>Chains r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r"
+ and u: "\<And>C. C \<in> Chains r \<Longrightarrow> \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r"
shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
proof -
have "Preorder r"
@@ -513,7 +513,8 @@
using \<open>Preorder r\<close> and \<open>a \<in> Field r\<close> and \<open>b \<in> Field r\<close>
by (simp add:subset_Image1_Image1_iff)
qed
- with u obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r" by auto
+ then obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r"
+ by (auto simp: dest: u)
have "?P u"
proof auto
fix a B assume aB: "B \<in> C" "a \<in> B"
@@ -539,6 +540,22 @@
using \<open>m \<in> Field r\<close> by blast
qed
+lemma predicate_Zorn:
+ assumes po: "partial_order_on A (relation_of P A)"
+ and ch: "\<And>C. C \<in> Chains (relation_of P A) \<Longrightarrow> \<exists>u \<in> A. \<forall>a \<in> C. P a u"
+ shows "\<exists>m \<in> A. \<forall>a \<in> A. P m a \<longrightarrow> a = m"
+proof -
+ have "a \<in> A" if "C \<in> Chains (relation_of P A)" and "a \<in> C" for C a
+ using that unfolding Chains_def relation_of_def by auto
+ moreover have "(a, u) \<in> relation_of P A" if "a \<in> A" and "u \<in> A" and "P a u" for a u
+ unfolding relation_of_def using that by auto
+ ultimately have "\<exists>m\<in>A. \<forall>a\<in>A. (m, a) \<in> relation_of P A \<longrightarrow> a = m"
+ using Zorns_po_lemma[OF Partial_order_relation_ofI[OF po], rule_format] ch
+ unfolding Field_relation_of[OF partial_order_onD(1)[OF po]] by blast
+ then show ?thesis
+ by (auto simp: relation_of_def)
+qed
+
subsection \<open>The Well Ordering Theorem\<close>
@@ -701,8 +718,8 @@
using mono_Chains [OF I_init] Chains_wo[of R] and \<open>R \<in> Chains I\<close>
unfolding I_def by blast
qed
- then have 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I"
- by (subst FI) blast
+ then have 1: "\<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" if "R \<in> Chains I" for R
+ using that by (subst FI) blast
\<comment> \<open>Zorn's Lemma yields a maximal well-order \<open>m\<close>:\<close>
then obtain m :: "'a rel"
where "Well_order m"