# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1534259140 -3600
# Node ID 345ce5f262eafe85216a9c93f92d46fb895988b2
# Parent  64fb127e33f785f201b9c6cc3c893eca539301c5
Zorn's lemma for relations defined by predicates

diff -r 64fb127e33f7 -r 345ce5f262ea src/HOL/Cardinals/Wellorder_Extension.thy
--- 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
diff -r 64fb127e33f7 -r 345ce5f262ea src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy
--- 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" ..
diff -r 64fb127e33f7 -r 345ce5f262ea src/HOL/Order_Relation.thy
--- 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>
 
diff -r 64fb127e33f7 -r 345ce5f262ea src/HOL/Zorn.thy
--- 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"