--- a/src/HOL/Algebra/Pred_Zorn.thy Mon Apr 29 17:11:26 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-theory Pred_Zorn
- imports HOL.Zorn
-
-begin
-
-(* ========== *)
-lemma partial_order_onE:
- 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
-(* ========== *)
-
-abbreviation rel_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set"
- where "rel_of P A \<equiv> { (a, b) \<in> A \<times> A. P a b }"
-
-lemma Field_rel_of:
- assumes "refl_on A (rel_of P A)" shows "Field (rel_of P A) = A"
- using assms unfolding refl_on_def Field_def by auto
-
-(* ========== *)
-lemma Chains_rel_of:
- assumes "C \<in> Chains (rel_of P A)" shows "C \<subseteq> A"
- using assms unfolding Chains_def by auto
-(* ========== *)
-
-lemma partial_order_on_rel_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 (rel_of P A)"
-proof -
- from refl have "refl_on A (rel_of P A)"
- unfolding refl_on_def by auto
- moreover have "trans (rel_of P A)" and "antisym (rel_of P A)"
- 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_rel_ofI:
- assumes "partial_order_on A (rel_of P A)" shows "Partial_order (rel_of P A)"
- using assms unfolding Field_rel_of[OF partial_order_onE(1)[OF assms]] .
-
-lemma predicate_Zorn:
- assumes "partial_order_on A (rel_of P A)"
- and "\<forall>C \<in> Chains (rel_of P A). \<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 "a \<in> C" and "C \<in> Chains (rel_of P A)" for C a
- using that Chains_rel_of by auto
- moreover have "(a, u) \<in> rel_of P A" if "a \<in> A" and "u \<in> A" and "P a u" for a u
- using that by auto
- ultimately show ?thesis
- using Zorns_po_lemma[OF Partial_order_rel_ofI[OF assms(1)]] assms(2)
- unfolding Field_rel_of[OF partial_order_onE(1)[OF assms(1)]] by auto
-qed
-
-end
\ No newline at end of file