blanchet@54552: (*  Title:      HOL/Order_Relation.thy
blanchet@54552:     Author:     Tobias Nipkow
blanchet@55026:     Author:     Andrei Popescu, TU Muenchen
blanchet@54552: *)
nipkow@26273: 
nipkow@26273: header {* Orders as Relations *}
nipkow@26273: 
nipkow@26273: theory Order_Relation
blanchet@55027: imports Wfrec
nipkow@26273: begin
nipkow@26273: 
nipkow@26295: subsection{* Orders on a set *}
nipkow@26295: 
nipkow@30198: definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
nipkow@26295: 
nipkow@26295: definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
nipkow@26273: 
nipkow@26295: definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
nipkow@26295: 
nipkow@26295: definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"
nipkow@26295: 
nipkow@26295: definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"
nipkow@26273: 
nipkow@26295: lemmas order_on_defs =
nipkow@26295:   preorder_on_def partial_order_on_def linear_order_on_def
nipkow@26295:   strict_linear_order_on_def well_order_on_def
nipkow@26295: 
nipkow@26273: 
nipkow@26295: lemma preorder_on_empty[simp]: "preorder_on {} {}"
nipkow@26295: by(simp add:preorder_on_def trans_def)
nipkow@26295: 
nipkow@26295: lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
nipkow@26295: by(simp add:partial_order_on_def)
nipkow@26273: 
nipkow@26295: lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
nipkow@26295: by(simp add:linear_order_on_def)
nipkow@26295: 
nipkow@26295: lemma well_order_on_empty[simp]: "well_order_on {} {}"
nipkow@26295: by(simp add:well_order_on_def)
nipkow@26295: 
nipkow@26273: 
nipkow@26295: lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
nipkow@26295: by (simp add:preorder_on_def)
nipkow@26295: 
nipkow@26295: lemma partial_order_on_converse[simp]:
nipkow@26295:   "partial_order_on A (r^-1) = partial_order_on A r"
nipkow@26295: by (simp add: partial_order_on_def)
nipkow@26273: 
nipkow@26295: lemma linear_order_on_converse[simp]:
nipkow@26295:   "linear_order_on A (r^-1) = linear_order_on A r"
nipkow@26295: by (simp add: linear_order_on_def)
nipkow@26295: 
nipkow@26273: 
nipkow@26295: lemma strict_linear_order_on_diff_Id:
nipkow@26295:   "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
nipkow@26295: by(simp add: order_on_defs trans_diff_Id)
nipkow@26295: 
nipkow@26295: 
nipkow@26295: subsection{* Orders on the field *}
nipkow@26273: 
nipkow@30198: abbreviation "Refl r \<equiv> refl_on (Field r) r"
nipkow@26295: 
nipkow@26295: abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
nipkow@26295: 
nipkow@26295: abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
nipkow@26273: 
nipkow@26295: abbreviation "Total r \<equiv> total_on (Field r) r"
nipkow@26295: 
nipkow@26295: abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
nipkow@26295: 
nipkow@26295: abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
nipkow@26295: 
nipkow@26273: 
nipkow@26273: lemma subset_Image_Image_iff:
nipkow@26273:   "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
nipkow@26273:    r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
blanchet@48750: unfolding preorder_on_def refl_on_def Image_def
blanchet@48750: apply (simp add: subset_eq)
blanchet@48750: unfolding trans_def by fast
nipkow@26273: 
nipkow@26273: lemma subset_Image1_Image1_iff:
nipkow@26273:   "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
nipkow@26273: by(simp add:subset_Image_Image_iff)
nipkow@26273: 
nipkow@26273: lemma Refl_antisym_eq_Image1_Image1_iff:
blanchet@54552:   assumes r: "Refl r" and as: "antisym r" and abf: "a \<in> Field r" "b \<in> Field r"
blanchet@54552:   shows "r `` {a} = r `` {b} \<longleftrightarrow> a = b"
blanchet@54552: proof
blanchet@54552:   assume "r `` {a} = r `` {b}"
blanchet@54552:   hence e: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r" by (simp add: set_eq_iff)
blanchet@54552:   have "(a, a) \<in> r" "(b, b) \<in> r" using r abf by (simp_all add: refl_on_def)
blanchet@54552:   hence "(a, b) \<in> r" "(b, a) \<in> r" using e[of a] e[of b] by simp_all
blanchet@54552:   thus "a = b" using as[unfolded antisym_def] by blast
blanchet@54552: qed fast
nipkow@26273: 
nipkow@26273: lemma Partial_order_eq_Image1_Image1_iff:
nipkow@26273:   "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
nipkow@26295: by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
nipkow@26295: 
popescua@52182: lemma Total_Id_Field:
popescua@52182: assumes TOT: "Total r" and NID: "\<not> (r <= Id)"
popescua@52182: shows "Field r = Field(r - Id)"
popescua@52182: using mono_Field[of "r - Id" r] Diff_subset[of r Id]
popescua@52182: proof(auto)
popescua@52182:   have "r \<noteq> {}" using NID by fast
blanchet@54482:   then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto
popescua@52182:   hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)
blanchet@54552: 
popescua@52182:   fix a assume *: "a \<in> Field r"
popescua@52182:   obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
popescua@52182:   using * 1 by auto
popescua@52182:   hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
popescua@52182:   by (simp add: total_on_def)
popescua@52182:   thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
popescua@52182: qed
popescua@52182: 
nipkow@26295: 
nipkow@26295: subsection{* Orders on a type *}
nipkow@26295: 
nipkow@26295: abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
nipkow@26295: 
nipkow@26295: abbreviation "linear_order \<equiv> linear_order_on UNIV"
nipkow@26295: 
blanchet@54551: abbreviation "well_order \<equiv> well_order_on UNIV"
nipkow@26273: 
blanchet@55026: 
blanchet@55026: subsection {* Order-like relations *}
blanchet@55026: 
blanchet@55026: text{* In this subsection, we develop basic concepts and results pertaining
blanchet@55026: to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
blanchet@55026: total relations. We also further define upper and lower bounds operators. *}
blanchet@55026: 
blanchet@55026: 
blanchet@55026: subsubsection {* Auxiliaries *}
blanchet@55026: 
blanchet@55026: lemma refl_on_domain:
blanchet@55026: "\<lbrakk>refl_on A r; (a,b) : r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
blanchet@55026: by(auto simp add: refl_on_def)
blanchet@55026: 
blanchet@55026: corollary well_order_on_domain:
blanchet@55026: "\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
blanchet@55026: by (auto simp add: refl_on_domain order_on_defs)
blanchet@55026: 
blanchet@55026: lemma well_order_on_Field:
blanchet@55026: "well_order_on A r \<Longrightarrow> A = Field r"
blanchet@55026: by(auto simp add: refl_on_def Field_def order_on_defs)
blanchet@55026: 
blanchet@55026: lemma well_order_on_Well_order:
blanchet@55026: "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
blanchet@55026: using well_order_on_Field by auto
blanchet@55026: 
blanchet@55026: lemma Total_subset_Id:
blanchet@55026: assumes TOT: "Total r" and SUB: "r \<le> Id"
blanchet@55026: shows "r = {} \<or> (\<exists>a. r = {(a,a)})"
blanchet@55026: proof-
blanchet@55026:   {assume "r \<noteq> {}"
blanchet@55026:    then obtain a b where 1: "(a,b) \<in> r" by fast
blanchet@55026:    hence "a = b" using SUB by blast
blanchet@55026:    hence 2: "(a,a) \<in> r" using 1 by simp
blanchet@55026:    {fix c d assume "(c,d) \<in> r"
blanchet@55026:     hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast
blanchet@55026:     hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and>
blanchet@55026:            ((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)"
blanchet@55026:     using TOT unfolding total_on_def by blast
blanchet@55026:     hence "a = c \<and> a = d" using SUB by blast
blanchet@55026:    }
blanchet@55026:    hence "r \<le> {(a,a)}" by auto
blanchet@55026:    with 2 have "\<exists>a. r = {(a,a)}" by blast
blanchet@55026:   }
blanchet@55026:   thus ?thesis by blast
blanchet@55026: qed
blanchet@55026: 
blanchet@55026: lemma Linear_order_in_diff_Id:
blanchet@55026: assumes LI: "Linear_order r" and
blanchet@55026:         IN1: "a \<in> Field r" and IN2: "b \<in> Field r"
blanchet@55026: shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)"
blanchet@55026: using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
blanchet@55026: 
blanchet@55026: 
blanchet@55026: subsubsection {* The upper and lower bounds operators  *}
blanchet@55026: 
blanchet@55026: text{* Here we define upper (``above") and lower (``below") bounds operators.
blanchet@55026: We think of @{text "r"} as a {\em non-strict} relation.  The suffix ``S"
blanchet@55026: at the names of some operators indicates that the bounds are strict -- e.g.,
blanchet@55026: @{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}).
blanchet@55026: Capitalization of the first letter in the name reminds that the operator acts on sets, rather
blanchet@55026: than on individual elements. *}
blanchet@55026: 
blanchet@55026: definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
blanchet@55026: where "under r a \<equiv> {b. (b,a) \<in> r}"
blanchet@55026: 
blanchet@55026: definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
blanchet@55026: where "underS r a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
blanchet@55026: 
blanchet@55026: definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
blanchet@55026: where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
blanchet@55026: 
blanchet@55026: definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
blanchet@55026: where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
blanchet@55026: 
blanchet@55026: definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
blanchet@55026: where "above r a \<equiv> {b. (a,b) \<in> r}"
blanchet@55026: 
blanchet@55026: definition aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
blanchet@55026: where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
blanchet@55026: 
blanchet@55026: definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
blanchet@55026: where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
blanchet@55026: 
blanchet@55026: definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
blanchet@55026: where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
blanchet@55026: 
traytel@55173: definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
traytel@55173: where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)"
traytel@55173: 
blanchet@55026: text{* Note:  In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
blanchet@55026:   we bounded comprehension by @{text "Field r"} in order to properly cover
blanchet@55026:   the case of @{text "A"} being empty. *}
blanchet@55026: 
blanchet@55026: lemma underS_subset_under: "underS r a \<le> under r a"
blanchet@55026: by(auto simp add: underS_def under_def)
blanchet@55026: 
blanchet@55026: lemma underS_notIn: "a \<notin> underS r a"
blanchet@55026: by(simp add: underS_def)
blanchet@55026: 
blanchet@55026: lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a"
blanchet@55026: by(simp add: refl_on_def under_def)
blanchet@55026: 
blanchet@55026: lemma AboveS_disjoint: "A Int (AboveS r A) = {}"
blanchet@55026: by(auto simp add: AboveS_def)
blanchet@55026: 
blanchet@55026: lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
blanchet@55026: by(auto simp add: AboveS_def underS_def)
blanchet@55026: 
blanchet@55026: lemma Refl_under_underS:
blanchet@55026:   assumes "Refl r" "a \<in> Field r"
blanchet@55026:   shows "under r a = underS r a \<union> {a}"
blanchet@55026: unfolding under_def underS_def
blanchet@55026: using assms refl_on_def[of _ r] by fastforce
blanchet@55026: 
blanchet@55026: lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
blanchet@55026: by (auto simp: Field_def underS_def)
blanchet@55026: 
blanchet@55026: lemma under_Field: "under r a \<le> Field r"
blanchet@55026: by(unfold under_def Field_def, auto)
blanchet@55026: 
blanchet@55026: lemma underS_Field: "underS r a \<le> Field r"
blanchet@55026: by(unfold underS_def Field_def, auto)
blanchet@55026: 
blanchet@55026: lemma underS_Field2:
blanchet@55026: "a \<in> Field r \<Longrightarrow> underS r a < Field r"
blanchet@55026: using underS_notIn underS_Field by fast
blanchet@55026: 
blanchet@55026: lemma underS_Field3:
blanchet@55026: "Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"
blanchet@55026: by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
blanchet@55026: 
blanchet@55026: lemma AboveS_Field: "AboveS r A \<le> Field r"
blanchet@55026: by(unfold AboveS_def Field_def, auto)
blanchet@55026: 
blanchet@55026: lemma under_incr:
blanchet@55026:   assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
blanchet@55026:   shows "under r a \<le> under r b"
blanchet@55026: proof(unfold under_def, auto)
blanchet@55026:   fix x assume "(x,a) \<in> r"
blanchet@55026:   with REL TRANS trans_def[of r]
blanchet@55026:   show "(x,b) \<in> r" by blast
blanchet@55026: qed
blanchet@55026: 
blanchet@55026: lemma underS_incr:
blanchet@55026: assumes TRANS: "trans r" and ANTISYM: "antisym r" and
blanchet@55026:         REL: "(a,b) \<in> r"
blanchet@55026: shows "underS r a \<le> underS r b"
blanchet@55026: proof(unfold underS_def, auto)
blanchet@55026:   assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
blanchet@55026:   with ANTISYM antisym_def[of r] REL
blanchet@55026:   show False by blast
blanchet@55026: next
blanchet@55026:   fix x assume "x \<noteq> a" "(x,a) \<in> r"
blanchet@55026:   with REL TRANS trans_def[of r]
blanchet@55026:   show "(x,b) \<in> r" by blast
blanchet@55026: qed
blanchet@55026: 
blanchet@55026: lemma underS_incl_iff:
blanchet@55026: assumes LO: "Linear_order r" and
blanchet@55026:         INa: "a \<in> Field r" and INb: "b \<in> Field r"
blanchet@55026: shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)"
blanchet@55026: proof
blanchet@55026:   assume "(a,b) \<in> r"
blanchet@55026:   thus "underS r a \<le> underS r b" using LO
blanchet@55026:   by (simp add: order_on_defs underS_incr)
blanchet@55026: next
blanchet@55026:   assume *: "underS r a \<le> underS r b"
blanchet@55026:   {assume "a = b"
blanchet@55026:    hence "(a,b) \<in> r" using assms
blanchet@55026:    by (simp add: order_on_defs refl_on_def)
blanchet@55026:   }
blanchet@55026:   moreover
blanchet@55026:   {assume "a \<noteq> b \<and> (b,a) \<in> r"
blanchet@55026:    hence "b \<in> underS r a" unfolding underS_def by blast
blanchet@55026:    hence "b \<in> underS r b" using * by blast
blanchet@55026:    hence False by (simp add: underS_notIn)
blanchet@55026:   }
blanchet@55026:   ultimately
blanchet@55026:   show "(a,b) \<in> r" using assms
blanchet@55026:   order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
blanchet@55026: qed
blanchet@55026: 
blanchet@55027: 
blanchet@55027: subsection {* Variations on Well-Founded Relations  *}
blanchet@55027: 
blanchet@55027: text {*
blanchet@55027: This subsection contains some variations of the results from @{theory Wellfounded}:
blanchet@55027: \begin{itemize}
blanchet@55027: \item means for slightly more direct definitions by well-founded recursion;
blanchet@55027: \item variations of well-founded induction;
blanchet@55027: \item means for proving a linear order to be a well-order.
blanchet@55027: \end{itemize}
blanchet@55027: *}
blanchet@55027: 
blanchet@55027: 
blanchet@55027: subsubsection {* Characterizations of well-foundedness *}
blanchet@55027: 
blanchet@55027: text {* A transitive relation is well-founded iff it is ``locally'' well-founded,
blanchet@55027: i.e., iff its restriction to the lower bounds of of any element is well-founded.  *}
blanchet@55027: 
blanchet@55027: lemma trans_wf_iff:
blanchet@55027: assumes "trans r"
blanchet@55027: shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
blanchet@55027: proof-
blanchet@55027:   obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
blanchet@55027:   {assume *: "wf r"
blanchet@55027:    {fix a
blanchet@55027:     have "wf(R a)"
blanchet@55027:     using * R_def wf_subset[of r "R a"] by auto
blanchet@55027:    }
blanchet@55027:   }
blanchet@55027:   (*  *)
blanchet@55027:   moreover
blanchet@55027:   {assume *: "\<forall>a. wf(R a)"
blanchet@55027:    have "wf r"
blanchet@55027:    proof(unfold wf_def, clarify)
blanchet@55027:      fix phi a
blanchet@55027:      assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
blanchet@55027:      obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
blanchet@55027:      with * have "wf (R a)" by auto
blanchet@55027:      hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
blanchet@55027:      unfolding wf_def by blast
blanchet@55027:      moreover
blanchet@55027:      have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
blanchet@55027:      proof(auto simp add: chi_def R_def)
blanchet@55027:        fix b
blanchet@55027:        assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
blanchet@55027:        hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
blanchet@55027:        using assms trans_def[of r] by blast
blanchet@55027:        thus "phi b" using ** by blast
blanchet@55027:      qed
blanchet@55027:      ultimately have  "\<forall>b. chi b" by (rule mp)
blanchet@55027:      with ** chi_def show "phi a" by blast
blanchet@55027:    qed
blanchet@55027:   }
blanchet@55027:   ultimately show ?thesis using R_def by blast
blanchet@55027: qed
blanchet@55027: 
blanchet@55027: text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,
blanchet@55027: allowing one to assume the set included in the field.  *}
blanchet@55027: 
blanchet@55027: lemma wf_eq_minimal2:
blanchet@55027: "wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))"
blanchet@55027: proof-
blanchet@55027:   let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
blanchet@55027:   have "wf r = (\<forall>A. ?phi A)"
blanchet@55027:   by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
blanchet@55027:      (rule wfI_min, fast)
blanchet@55027:   (*  *)
blanchet@55027:   also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
blanchet@55027:   proof
blanchet@55027:     assume "\<forall>A. ?phi A"
blanchet@55027:     thus "\<forall>B \<le> Field r. ?phi B" by simp
blanchet@55027:   next
blanchet@55027:     assume *: "\<forall>B \<le> Field r. ?phi B"
blanchet@55027:     show "\<forall>A. ?phi A"
blanchet@55027:     proof(clarify)
blanchet@55027:       fix A::"'a set" assume **: "A \<noteq> {}"
blanchet@55027:       obtain B where B_def: "B = A Int (Field r)" by blast
blanchet@55027:       show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
blanchet@55027:       proof(cases "B = {}")
blanchet@55027:         assume Case1: "B = {}"
blanchet@55027:         obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
blanchet@55027:         using ** Case1 unfolding B_def by blast
blanchet@55027:         hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
blanchet@55027:         thus ?thesis using 1 by blast
blanchet@55027:       next
blanchet@55027:         assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
blanchet@55027:         obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
blanchet@55027:         using Case2 1 * by blast
blanchet@55027:         have "\<forall>a' \<in> A. (a',a) \<notin> r"
blanchet@55027:         proof(clarify)
blanchet@55027:           fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
blanchet@55027:           hence "a' \<in> B" unfolding B_def Field_def by blast
blanchet@55027:           thus False using 2 ** by blast
blanchet@55027:         qed
blanchet@55027:         thus ?thesis using 2 unfolding B_def by blast
blanchet@55027:       qed
blanchet@55027:     qed
blanchet@55027:   qed
blanchet@55027:   finally show ?thesis by blast
blanchet@55027: qed
blanchet@55027: 
blanchet@55027: 
blanchet@55027: subsubsection {* Characterizations of well-foundedness *}
blanchet@55027: 
blanchet@55027: text {* The next lemma and its corollary enable one to prove that
blanchet@55027: a linear order is a well-order in a way which is more standard than
blanchet@55027: via well-foundedness of the strict version of the relation.  *}
blanchet@55027: 
blanchet@55027: lemma Linear_order_wf_diff_Id:
blanchet@55027: assumes LI: "Linear_order r"
blanchet@55027: shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
blanchet@55027: proof(cases "r \<le> Id")
blanchet@55027:   assume Case1: "r \<le> Id"
blanchet@55027:   hence temp: "r - Id = {}" by blast
blanchet@55027:   hence "wf(r - Id)" by (simp add: temp)
blanchet@55027:   moreover
blanchet@55027:   {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
blanchet@55027:    obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
blanchet@55027:    unfolding order_on_defs using Case1 Total_subset_Id by auto
blanchet@55027:    hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
blanchet@55027:    hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
blanchet@55027:   }
blanchet@55027:   ultimately show ?thesis by blast
blanchet@55027: next
blanchet@55027:   assume Case2: "\<not> r \<le> Id"
blanchet@55027:   hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
blanchet@55027:   unfolding order_on_defs by blast
blanchet@55027:   show ?thesis
blanchet@55027:   proof
blanchet@55027:     assume *: "wf(r - Id)"
blanchet@55027:     show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
blanchet@55027:     proof(clarify)
blanchet@55027:       fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
blanchet@55027:       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
blanchet@55027:       using 1 * unfolding wf_eq_minimal2 by simp
blanchet@55027:       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
blanchet@55027:       using Linear_order_in_diff_Id[of r] ** LI by blast
blanchet@55027:       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
blanchet@55027:     qed
blanchet@55027:   next
blanchet@55027:     assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
blanchet@55027:     show "wf(r - Id)"
blanchet@55027:     proof(unfold wf_eq_minimal2, clarify)
blanchet@55027:       fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
blanchet@55027:       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
blanchet@55027:       using 1 * by simp
blanchet@55027:       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
blanchet@55027:       using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
blanchet@55027:       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
blanchet@55027:     qed
blanchet@55027:   qed
blanchet@55027: qed
blanchet@55027: 
blanchet@55027: corollary Linear_order_Well_order_iff:
blanchet@55027: assumes "Linear_order r"
blanchet@55027: shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
blanchet@55027: using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
blanchet@55027: 
nipkow@26273: end