Theory HOL.Order_Relation

(*  Title:      HOL/Order_Relation.thy
    Author:     Tobias Nipkow
    Author:     Andrei Popescu, TU Muenchen
*)

section ‹Orders as Relations›

theory Order_Relation
imports Wfrec
begin

subsection ‹Orders on a set›

definition "preorder_on A r ≡ refl_on A r ∧ trans r"

definition "partial_order_on A r ≡ preorder_on A r ∧ antisym r"

definition "linear_order_on A r ≡ partial_order_on A r ∧ total_on A r"

definition "strict_linear_order_on A r ≡ trans r ∧ irrefl r ∧ total_on A r"

definition "well_order_on A r ≡ linear_order_on A r ∧ wf(r - Id)"

lemmas order_on_defs =
  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)

lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
  by (simp add: partial_order_on_def)

lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
  by (simp add: linear_order_on_def)

lemma well_order_on_empty[simp]: "well_order_on {} {}"
  by (simp add: well_order_on_def)


lemma preorder_on_converse[simp]: "preorder_on A (r¯) = preorder_on A r"
  by (simp add: preorder_on_def)

lemma partial_order_on_converse[simp]: "partial_order_on A (r¯) = partial_order_on A r"
  by (simp add: partial_order_on_def)

lemma linear_order_on_converse[simp]: "linear_order_on A (r¯) = linear_order_on A r"
  by (simp add: linear_order_on_def)


lemma partial_order_on_acyclic:
  "partial_order_on A r ⟹ acyclic (r - Id)"
  by (simp add: acyclic_irrefl partial_order_on_def preorder_on_def trans_diff_Id)

lemma partial_order_on_well_order_on:               
  "finite r ⟹ partial_order_on A r ⟹ wf (r - Id)" 
  by (simp add: finite_acyclic_wf partial_order_on_acyclic) 

lemma strict_linear_order_on_diff_Id: "linear_order_on A r ⟹ strict_linear_order_on A (r - Id)"
  by (simp add: order_on_defs trans_diff_Id)

lemma linear_order_on_singleton [simp]: "linear_order_on {x} {(x, x)}"
  by (simp add: order_on_defs)

lemma linear_order_on_acyclic:
  assumes "linear_order_on A r"
  shows "acyclic (r - Id)"
  using strict_linear_order_on_diff_Id[OF assms]
  by (auto simp add: acyclic_irrefl strict_linear_order_on_def)

lemma linear_order_on_well_order_on:
  assumes "finite r"
  shows "linear_order_on A r ⟷ well_order_on A r"
  unfolding well_order_on_def
  using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast


subsection ‹Orders on the field›

abbreviation "Refl r ≡ refl_on (Field r) r"

abbreviation "Preorder r ≡ preorder_on (Field r) r"

abbreviation "Partial_order r ≡ partial_order_on (Field r) r"

abbreviation "Total r ≡ total_on (Field r) r"

abbreviation "Linear_order r ≡ linear_order_on (Field r) r"

abbreviation "Well_order r ≡ well_order_on (Field r) r"


lemma subset_Image_Image_iff:
  "Preorder r ⟹ A ⊆ Field r ⟹ B ⊆ Field r ⟹
    r `` A ⊆ r `` B ⟷ (∀a∈A.∃b∈B. (b, a) ∈ r)"
  apply (simp add: preorder_on_def refl_on_def Image_def subset_eq)
  apply (simp only: trans_def)
  apply fast
  done

lemma subset_Image1_Image1_iff:
  "Preorder r ⟹ a ∈ Field r ⟹ b ∈ Field r ⟹ r `` {a} ⊆ r `` {b} ⟷ (b, a) ∈ r"
  by (simp add: subset_Image_Image_iff)

lemma Refl_antisym_eq_Image1_Image1_iff:
  assumes "Refl r"
    and as: "antisym r"
    and abf: "a ∈ Field r" "b ∈ Field r"
  shows "r `` {a} = r `` {b} ⟷ a = b"
    (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  then have *: "⋀x. (a, x) ∈ r ⟷ (b, x) ∈ r"
    by (simp add: set_eq_iff)
  have "(a, a) ∈ r" "(b, b) ∈ r" using ‹Refl r› abf by (simp_all add: refl_on_def)
  then have "(a, b) ∈ r" "(b, a) ∈ r" using *[of a] *[of b] by simp_all
  then show ?rhs
    using ‹antisym r›[unfolded antisym_def] by blast
next
  assume ?rhs
  then show ?lhs by fast
qed

lemma Partial_order_eq_Image1_Image1_iff:
  "Partial_order r ⟹ a ∈ Field r ⟹ b ∈ Field r ⟹ r `` {a} = r `` {b} ⟷ a = b"
  by (auto simp: order_on_defs Refl_antisym_eq_Image1_Image1_iff)

lemma Total_Id_Field:
  assumes "Total r"
    and not_Id: "¬ r ⊆ Id"
  shows "Field r = Field (r - Id)"
proof -
  have "Field r ⊆ Field (r - Id)"
  proof (rule subsetI)
    fix a assume *: "a ∈ Field r"
    from not_Id have "r ≠ {}" by fast
    with not_Id obtain b and c where "b ≠ c ∧ (b,c) ∈ r" by auto
    then have "b ≠ c ∧ {b, c} ⊆ Field r" by (auto simp: Field_def)
    with * obtain d where "d ∈ Field r" "d ≠ a" by auto
    with * ‹Total r› have "(a, d) ∈ r ∨ (d, a) ∈ r" by (simp add: total_on_def)
    with ‹d ≠ a› show "a ∈ Field (r - Id)" unfolding Field_def by blast
  qed
  then show ?thesis
    using mono_Field[of "r - Id" r] Diff_subset[of r Id] by auto
qed

subsection‹Relations given by a predicate and the field›

definition relation_of :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ ('a × 'a) set"
  where "relation_of P A ≡ { (a, b) ∈ A × 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: "⋀a. a ∈ A ⟹ P a a"
    and trans: "⋀a b c. ⟦ a ∈ A; b ∈ A; c ∈ A ⟧ ⟹ P a b ⟹ P b c ⟹ P a c"
    and antisym: "⋀a b. ⟦ a ∈ A; b ∈ A ⟧ ⟹ P a b ⟹ P b a ⟹ 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 ‹Orders on a type›

abbreviation "strict_linear_order ≡ strict_linear_order_on UNIV"

abbreviation "linear_order ≡ linear_order_on UNIV"

abbreviation "well_order ≡ well_order_on UNIV"


subsection ‹Order-like relations›

text ‹
  In this subsection, we develop basic concepts and results pertaining
  to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
  total relations. We also further define upper and lower bounds operators.
›


subsubsection ‹Auxiliaries›

lemma refl_on_domain: "refl_on A r ⟹ (a, b) ∈ r ⟹ a ∈ A ∧ b ∈ A"
  by (auto simp add: refl_on_def)

corollary well_order_on_domain: "well_order_on A r ⟹ (a, b) ∈ r ⟹ a ∈ A ∧ b ∈ A"
  by (auto simp add: refl_on_domain order_on_defs)

lemma well_order_on_Field: "well_order_on A r ⟹ A = Field r"
  by (auto simp add: refl_on_def Field_def order_on_defs)

lemma well_order_on_Well_order: "well_order_on A r ⟹ A = Field r ∧ Well_order r"
  using well_order_on_Field [of A] by auto

lemma Total_subset_Id:
  assumes "Total r"
    and "r ⊆ Id"
  shows "r = {} ∨ (∃a. r = {(a, a)})"
proof -
  have "∃a. r = {(a, a)}" if "r ≠ {}"
  proof -
    from that obtain a b where ab: "(a, b) ∈ r" by fast
    with ‹r ⊆ Id› have "a = b" by blast
    with ab have aa: "(a, a) ∈ r" by simp
    have "a = c ∧ a = d" if "(c, d) ∈ r" for c d
    proof -
      from that have "{a, c, d} ⊆ Field r"
        using ab unfolding Field_def by blast
      then have "((a, c) ∈ r ∨ (c, a) ∈ r ∨ a = c) ∧ ((a, d) ∈ r ∨ (d, a) ∈ r ∨ a = d)"
        using ‹Total r› unfolding total_on_def by blast
      with ‹r ⊆ Id› show ?thesis by blast
    qed
    then have "r ⊆ {(a, a)}" by auto
    with aa show ?thesis by blast
  qed
  then show ?thesis by blast
qed

lemma Linear_order_in_diff_Id:
  assumes "Linear_order r"
    and "a ∈ Field r"
    and "b ∈ Field r"
  shows "(a, b) ∈ r ⟷ (b, a) ∉ r - Id"
  using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force


subsubsection ‹The upper and lower bounds operators›

text ‹
  Here we define upper (``above") and lower (``below") bounds operators. We
  think of ‹r› as a ∗‹non-strict› relation. The suffix ‹S› at the names of
  some operators indicates that the bounds are strict -- e.g., ‹underS a› is
  the set of all strict lower bounds of ‹a› (w.r.t. ‹r›). Capitalization of
  the first letter in the name reminds that the operator acts on sets, rather
  than on individual elements.
›

definition under :: "'a rel ⇒ 'a ⇒ 'a set"
  where "under r a ≡ {b. (b, a) ∈ r}"

definition underS :: "'a rel ⇒ 'a ⇒ 'a set"
  where "underS r a ≡ {b. b ≠ a ∧ (b, a) ∈ r}"

definition Under :: "'a rel ⇒ 'a set ⇒ 'a set"
  where "Under r A ≡ {b ∈ Field r. ∀a ∈ A. (b, a) ∈ r}"

definition UnderS :: "'a rel ⇒ 'a set ⇒ 'a set"
  where "UnderS r A ≡ {b ∈ Field r. ∀a ∈ A. b ≠ a ∧ (b, a) ∈ r}"

definition above :: "'a rel ⇒ 'a ⇒ 'a set"
  where "above r a ≡ {b. (a, b) ∈ r}"

definition aboveS :: "'a rel ⇒ 'a ⇒ 'a set"
  where "aboveS r a ≡ {b. b ≠ a ∧ (a, b) ∈ r}"

definition Above :: "'a rel ⇒ 'a set ⇒ 'a set"
  where "Above r A ≡ {b ∈ Field r. ∀a ∈ A. (a, b) ∈ r}"

definition AboveS :: "'a rel ⇒ 'a set ⇒ 'a set"
  where "AboveS r A ≡ {b ∈ Field r. ∀a ∈ A. b ≠ a ∧ (a, b) ∈ r}"

definition ofilter :: "'a rel ⇒ 'a set ⇒ bool"
  where "ofilter r A ≡ A ⊆ Field r ∧ (∀a ∈ A. under r a ⊆ A)"

text ‹
  Note: In the definitions of ‹Above[S]› and ‹Under[S]›, we bounded
  comprehension by ‹Field r› in order to properly cover the case of ‹A› being
  empty.
›

lemma underS_subset_under: "underS r a ⊆ under r a"
  by (auto simp add: underS_def under_def)

lemma underS_notIn: "a ∉ underS r a"
  by (simp add: underS_def)

lemma Refl_under_in: "Refl r ⟹ a ∈ Field r ⟹ a ∈ under r a"
  by (simp add: refl_on_def under_def)

lemma AboveS_disjoint: "A ∩ (AboveS r A) = {}"
  by (auto simp add: AboveS_def)

lemma in_AboveS_underS: "a ∈ Field r ⟹ a ∈ AboveS r (underS r a)"
  by (auto simp add: AboveS_def underS_def)

lemma Refl_under_underS: "Refl r ⟹ a ∈ Field r ⟹ under r a = underS r a ∪ {a}"
  unfolding under_def underS_def
  using refl_on_def[of _ r] by fastforce

lemma underS_empty: "a ∉ Field r ⟹ underS r a = {}"
  by (auto simp: Field_def underS_def)

lemma under_Field: "under r a ⊆ Field r"
  by (auto simp: under_def Field_def)

lemma underS_Field: "underS r a ⊆ Field r"
  by (auto simp: underS_def Field_def)

lemma underS_Field2: "a ∈ Field r ⟹ underS r a ⊂ Field r"
  using underS_notIn underS_Field by fast

lemma underS_Field3: "Field r ≠ {} ⟹ underS r a ⊂ Field r"
  by (cases "a ∈ Field r") (auto simp: underS_Field2 underS_empty)

lemma AboveS_Field: "AboveS r A ⊆ Field r"
  by (auto simp: AboveS_def Field_def)

lemma under_incr:
  assumes "trans r"
    and "(a, b) ∈ r"
  shows "under r a ⊆ under r b"
  unfolding under_def
proof safe
  fix x assume "(x, a) ∈ r"
  with assms trans_def[of r] show "(x, b) ∈ r" by blast
qed

lemma underS_incr:
  assumes "trans r"
    and "antisym r"
    and ab: "(a, b) ∈ r"
  shows "underS r a ⊆ underS r b"
  unfolding underS_def
proof safe
  assume *: "b ≠ a" and **: "(b, a) ∈ r"
  with ‹antisym r› antisym_def[of r] ab show False
    by blast
next
  fix x assume "x ≠ a" "(x, a) ∈ r"
  with ab ‹trans r› trans_def[of r] show "(x, b) ∈ r"
    by blast
qed

lemma underS_incl_iff:
  assumes LO: "Linear_order r"
    and INa: "a ∈ Field r"
    and INb: "b ∈ Field r"
  shows "underS r a ⊆ underS r b ⟷ (a, b) ∈ r"
    (is "?lhs ⟷ ?rhs")
proof
  assume ?rhs
  with ‹Linear_order r› show ?lhs
    by (simp add: order_on_defs underS_incr)
next
  assume *: ?lhs
  have "(a, b) ∈ r" if "a = b"
    using assms that by (simp add: order_on_defs refl_on_def)
  moreover have False if "a ≠ b" "(b, a) ∈ r"
  proof -
    from that have "b ∈ underS r a" unfolding underS_def by blast
    with * have "b ∈ underS r b" by blast
    then show ?thesis by (simp add: underS_notIn)
  qed
  ultimately show "(a,b) ∈ r"
    using assms order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
qed

lemma finite_Partial_order_induct[consumes 3, case_names step]:
  assumes "Partial_order r"
    and "x ∈ Field r"
    and "finite r"
    and step: "⋀x. x ∈ Field r ⟹ (⋀y. y ∈ aboveS r x ⟹ P y) ⟹ P x"
  shows "P x"
  using assms(2)
proof (induct rule: wf_induct[of "r¯ - Id"])
  case 1
  from assms(1,3) show "wf (r¯ - Id)"
    using partial_order_on_well_order_on partial_order_on_converse by blast
next
  case prems: (2 x)
  show ?case
    by (rule step) (use prems in ‹auto simp: aboveS_def intro: FieldI2›)
qed

lemma finite_Linear_order_induct[consumes 3, case_names step]:
  assumes "Linear_order r"
    and "x ∈ Field r"
    and "finite r"
    and step: "⋀x. x ∈ Field r ⟹ (⋀y. y ∈ aboveS r x ⟹ P y) ⟹ P x"
  shows "P x"
  using assms(2)
proof (induct rule: wf_induct[of "r¯ - Id"])
  case 1
  from assms(1,3) show "wf (r¯ - Id)"
    using linear_order_on_well_order_on linear_order_on_converse
    unfolding well_order_on_def by blast
next
  case prems: (2 x)
  show ?case
    by (rule step) (use prems in ‹auto simp: aboveS_def intro: FieldI2›)
qed


subsection ‹Variations on Well-Founded Relations›

text ‹
  This subsection contains some variations of the results from \<^theory>‹HOL.Wellfounded›:
    ▪ means for slightly more direct definitions by well-founded recursion;
    ▪ variations of well-founded induction;
    ▪ means for proving a linear order to be a well-order.
›


subsubsection ‹Characterizations of well-foundedness›

text ‹
  A transitive relation is well-founded iff it is ``locally'' well-founded,
  i.e., iff its restriction to the lower bounds of of any element is
  well-founded.
›

lemma trans_wf_iff:
  assumes "trans r"
  shows "wf r ⟷ (∀a. wf (r ∩ (r¯``{a} × r¯``{a})))"
proof -
  define R where "R a = r ∩ (r¯``{a} × r¯``{a})" for a
  have "wf (R a)" if "wf r" for a
    using that R_def wf_subset[of r "R a"] by auto
  moreover
  have "wf r" if *: "∀a. wf(R a)"
    unfolding wf_def
  proof clarify
    fix phi a
    assume **: "∀a. (∀b. (b, a) ∈ r ⟶ phi b) ⟶ phi a"
    define chi where "chi b ⟷ (b, a) ∈ r ⟶ phi b" for b
    with * have "wf (R a)" by auto
    then have "(∀b. (∀c. (c, b) ∈ R a ⟶ chi c) ⟶ chi b) ⟶ (∀b. chi b)"
      unfolding wf_def by blast
    also have "∀b. (∀c. (c, b) ∈ R a ⟶ chi c) ⟶ chi b"
    proof safe
      fix b
      assume "∀c. (c, b) ∈ R a ⟶ chi c"
      moreover have "(b, a) ∈ r ⟹ ∀c. (c, b) ∈ r ∧ (c, a) ∈ r ⟶ phi c ⟹ phi b"
      proof -
        assume "(b, a) ∈ r" and "∀c. (c, b) ∈ r ∧ (c, a) ∈ r ⟶ phi c"
        then have "∀c. (c, b) ∈ r ⟶ phi c"
          using assms trans_def[of r] by blast
        with ** show "phi b" by blast
      qed
      ultimately show "chi b"
        by (auto simp add: chi_def R_def)
    qed
    finally have  "∀b. chi b" .
    with ** chi_def show "phi a" by blast
  qed
  ultimately show ?thesis unfolding R_def by blast
qed

text‹A transitive relation is well-founded if all initial segments are finite.›
corollary wf_finite_segments:
  assumes "irrefl r" and "trans r" and "⋀x. finite {y. (y, x) ∈ r}"
  shows "wf r"
proof -
  have "⋀a. acyclic (r ∩ {x. (x, a) ∈ r} × {x. (x, a) ∈ r})"
  proof -
    fix a
    have "trans (r ∩ ({x. (x, a) ∈ r} × {x. (x, a) ∈ r}))"
      using assms unfolding trans_def Field_def by blast
    then show "acyclic (r ∩ {x. (x, a) ∈ r} × {x. (x, a) ∈ r})"
      using assms acyclic_def assms irrefl_def by fastforce
  qed
  then show ?thesis
    by (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
qed

text ‹The next lemma is a variation of ‹wf_eq_minimal› from Wellfounded,
  allowing one to assume the set included in the field.›

lemma wf_eq_minimal2: "wf r ⟷ (∀A. A ⊆ Field r ∧ A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a', a) ∉ r))"
proof-
  let ?phi = "λA. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r)"
  have "wf r ⟷ (∀A. ?phi A)"
  proof
    assume "wf r"
    show  "∀A. ?phi A"
    proof clarify
      fix A:: "'a set"
      assume "A ≠ {}"
      then obtain x where "x ∈ A"
        by auto
      show "∃a∈A. ∀a'∈A. (a', a) ∉ r"
        apply (rule wfE_min[of r x A])
          apply fact+
        by blast
    qed
  next
    assume *: "∀A. ?phi A"
    then show "wf r"
      apply (clarsimp simp: ex_in_conv [THEN sym])
      apply (rule wfI_min)
      by fast
  qed
  also have "(∀A. ?phi A) ⟷ (∀B ⊆ Field r. ?phi B)"
  proof
    assume "∀A. ?phi A"
    then show "∀B ⊆ Field r. ?phi B" by simp
  next
    assume *: "∀B ⊆ Field r. ?phi B"
    show "∀A. ?phi A"
    proof clarify
      fix A :: "'a set"
      assume **: "A ≠ {}"
      define B where "B = A ∩ Field r"
      show "∃a ∈ A. ∀a' ∈ A. (a', a) ∉ r"
      proof (cases "B = {}")
        case True
        with ** obtain a where a: "a ∈ A" "a ∉ Field r"
          unfolding B_def by blast
        with a have "∀a' ∈ A. (a',a) ∉ r"
          unfolding Field_def by blast
        with a show ?thesis by blast
      next
        case False
        have "B ⊆ Field r" unfolding B_def by blast
        with False * obtain a where a: "a ∈ B" "∀a' ∈ B. (a', a) ∉ r"
          by blast
        have "(a', a) ∉ r" if "a' ∈ A" for a'
        proof
          assume a'a: "(a', a) ∈ r"
          with that have "a' ∈ B" unfolding B_def Field_def by blast
          with a a'a show False by blast
        qed
        with a show ?thesis unfolding B_def by blast
      qed
    qed
  qed
  finally show ?thesis by blast
qed


subsubsection ‹Characterizations of well-foundedness›

text ‹
  The next lemma and its corollary enable one to prove that a linear order is
  a well-order in a way which is more standard than via well-foundedness of
  the strict version of the relation.
›

lemma Linear_order_wf_diff_Id:
  assumes "Linear_order r"
  shows "wf (r - Id) ⟷ (∀A ⊆ Field r. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r))"
proof (cases "r ⊆ Id")
  case True
  then have *: "r - Id = {}" by blast
  have "wf (r - Id)" by (simp add: *)
  moreover have "∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r"
    if *: "A ⊆ Field r" and **: "A ≠ {}" for A
  proof -
    from ‹Linear_order r› True
    obtain a where a: "r = {} ∨ r = {(a, a)}"
      unfolding order_on_defs using Total_subset_Id [of r] by blast
    with * ** have "A = {a} ∧ r = {(a, a)}"
      unfolding Field_def by blast
    with a show ?thesis by blast
  qed
  ultimately show ?thesis by blast
next
  case False
  with ‹Linear_order r› have Field: "Field r = Field (r - Id)"
    unfolding order_on_defs using Total_Id_Field [of r] by blast
  show ?thesis
  proof
    assume *: "wf (r - Id)"
    show "∀A ⊆ Field r. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r)"
    proof clarify
      fix A
      assume **: "A ⊆ Field r" and ***: "A ≠ {}"
      then have "∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r - Id"
        using Field * unfolding wf_eq_minimal2 by simp
      moreover have "∀a ∈ A. ∀a' ∈ A. (a, a') ∈ r ⟷ (a', a) ∉ r - Id"
        using Linear_order_in_diff_Id [OF ‹Linear_order r›] ** by blast
      ultimately show "∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r" by blast
    qed
  next
    assume *: "∀A ⊆ Field r. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r)"
    show "wf (r - Id)"
      unfolding wf_eq_minimal2
    proof clarify
      fix A
      assume **: "A ⊆ Field(r - Id)" and ***: "A ≠ {}"
      then have "∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r"
        using Field * by simp
      moreover have "∀a ∈ A. ∀a' ∈ A. (a, a') ∈ r ⟷ (a', a) ∉ r - Id"
        using Linear_order_in_diff_Id [OF ‹Linear_order r›] ** mono_Field[of "r - Id" r] by blast
      ultimately show "∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r - Id"
        by blast
    qed
  qed
qed

corollary Linear_order_Well_order_iff:
  "Linear_order r ⟹
    Well_order r ⟷ (∀A ⊆ Field r. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a, a') ∈ r))"
  unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast

end