src/HOL/Order_Relation.thy

euclidean rings need no normalization

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

section \<open>Orders as Relations\<close>

theory Order_Relation
imports Wfrec
begin

subsection \<open>Orders on a set\<close>

definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"

definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"

definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"

definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"

definition "well_order_on A r \<equiv> linear_order_on A r \<and> 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 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\<inverse>) = preorder_on A r"
  by (simp add: preorder_on_def)

lemma partial_order_on_converse[simp]: "partial_order_on A (r\<inverse>) = partial_order_on A r"
  by (simp add: partial_order_on_def)

lemma linear_order_on_converse[simp]: "linear_order_on A (r\<inverse>) = linear_order_on A r"
  by (simp add: linear_order_on_def)


lemma strict_linear_order_on_diff_Id: "linear_order_on A r \<Longrightarrow> 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 \<longleftrightarrow> 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 \<open>Orders on the field\<close>

abbreviation "Refl r \<equiv> refl_on (Field r) r"

abbreviation "Preorder r \<equiv> preorder_on (Field r) r"

abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"

abbreviation "Total r \<equiv> total_on (Field r) r"

abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"

abbreviation "Well_order r \<equiv> well_order_on (Field r) r"


lemma subset_Image_Image_iff:
  "Preorder r \<Longrightarrow> A \<subseteq> Field r \<Longrightarrow> B \<subseteq> Field r \<Longrightarrow>
    r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b, a) \<in> 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 \<Longrightarrow> a \<in> Field r \<Longrightarrow> b \<in> Field r \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b, a) \<in> 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 \<in> Field r" "b \<in> Field r"
  shows "r `` {a} = r `` {b} \<longleftrightarrow> a = b"
    (is "?lhs \<longleftrightarrow> ?rhs")
proof
  assume ?lhs
  then have *: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r"
    by (simp add: set_eq_iff)
  have "(a, a) \<in> r" "(b, b) \<in> r" using \<open>Refl r\<close> abf by (simp_all add: refl_on_def)
  then have "(a, b) \<in> r" "(b, a) \<in> r" using *[of a] *[of b] by simp_all
  then show ?rhs
    using \<open>antisym r\<close>[unfolded antisym_def] by blast
next
  assume ?rhs
  then show ?lhs by fast
qed

lemma Partial_order_eq_Image1_Image1_iff:
  "Partial_order r \<Longrightarrow> a \<in> Field r \<Longrightarrow> b \<in> Field r \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a = b"
  by (auto simp: order_on_defs Refl_antisym_eq_Image1_Image1_iff)

lemma Total_Id_Field:
  assumes "Total r"
    and not_Id: "\<not> r \<subseteq> Id"
  shows "Field r = Field (r - Id)"
  using mono_Field[of "r - Id" r] Diff_subset[of r Id]
proof auto
  fix a assume *: "a \<in> Field r"
  from not_Id have "r \<noteq> {}" by fast
  with not_Id obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" by auto
  then have "b \<noteq> c \<and> {b, c} \<subseteq> Field r" by (auto simp: Field_def)
  with * obtain d where "d \<in> Field r" "d \<noteq> a" by auto
  with * \<open>Total r\<close> have "(a, d) \<in> r \<or> (d, a) \<in> r" by (simp add: total_on_def)
  with \<open>d \<noteq> a\<close> show "a \<in> Field (r - Id)" unfolding Field_def by blast
qed


subsection \<open>Orders on a type\<close>

abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"

abbreviation "linear_order \<equiv> linear_order_on UNIV"

abbreviation "well_order \<equiv> well_order_on UNIV"


subsection \<open>Order-like relations\<close>

text \<open>
  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.
\<close>


subsubsection \<open>Auxiliaries\<close>

lemma refl_on_domain: "refl_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
  by (auto simp add: refl_on_def)

corollary well_order_on_domain: "well_order_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
  by (auto simp add: refl_on_domain order_on_defs)

lemma well_order_on_Field: "well_order_on A r \<Longrightarrow> 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 \<Longrightarrow> A = Field r \<and> Well_order r"
  using well_order_on_Field [of A] by auto

lemma Total_subset_Id:
  assumes "Total r"
    and "r \<subseteq> Id"
  shows "r = {} \<or> (\<exists>a. r = {(a, a)})"
proof -
  have "\<exists>a. r = {(a, a)}" if "r \<noteq> {}"
  proof -
    from that obtain a b where ab: "(a, b) \<in> r" by fast
    with \<open>r \<subseteq> Id\<close> have "a = b" by blast
    with ab have aa: "(a, a) \<in> r" by simp
    have "a = c \<and> a = d" if "(c, d) \<in> r" for c d
    proof -
      from that have "{a, c, d} \<subseteq> Field r"
        using ab unfolding Field_def by blast
      then have "((a, c) \<in> r \<or> (c, a) \<in> r \<or> a = c) \<and> ((a, d) \<in> r \<or> (d, a) \<in> r \<or> a = d)"
        using \<open>Total r\<close> unfolding total_on_def by blast
      with \<open>r \<subseteq> Id\<close> show ?thesis by blast
    qed
    then have "r \<subseteq> {(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 \<in> Field r"
    and "b \<in> Field r"
  shows "(a, b) \<in> r \<longleftrightarrow> (b, a) \<notin> r - Id"
  using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force


subsubsection \<open>The upper and lower bounds operators\<close>

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

definition under :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
  where "under r a \<equiv> {b. (b, a) \<in> r}"

definition underS :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
  where "underS r a \<equiv> {b. b \<noteq> a \<and> (b, a) \<in> r}"

definition Under :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
  where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b, a) \<in> r}"

definition UnderS :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
  where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b, a) \<in> r}"

definition above :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
  where "above r a \<equiv> {b. (a, b) \<in> r}"

definition aboveS :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
  where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a, b) \<in> r}"

definition Above :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
  where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a, b) \<in> r}"

definition AboveS :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
  where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a, b) \<in> r}"

definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
  where "ofilter r A \<equiv> A \<subseteq> Field r \<and> (\<forall>a \<in> A. under r a \<subseteq> A)"

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

lemma underS_subset_under: "underS r a \<subseteq> under r a"
  by (auto simp add: underS_def under_def)

lemma underS_notIn: "a \<notin> underS r a"
  by (simp add: underS_def)

lemma Refl_under_in: "Refl r \<Longrightarrow> a \<in> Field r \<Longrightarrow> a \<in> under r a"
  by (simp add: refl_on_def under_def)

lemma AboveS_disjoint: "A \<inter> (AboveS r A) = {}"
  by (auto simp add: AboveS_def)

lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
  by (auto simp add: AboveS_def underS_def)

lemma Refl_under_underS: "Refl r \<Longrightarrow> a \<in> Field r \<Longrightarrow> under r a = underS r a \<union> {a}"
  unfolding under_def underS_def
  using refl_on_def[of _ r] by fastforce

lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
  by (auto simp: Field_def underS_def)

lemma under_Field: "under r a \<subseteq> Field r"
  by (auto simp: under_def Field_def)

lemma underS_Field: "underS r a \<subseteq> Field r"
  by (auto simp: underS_def Field_def)

lemma underS_Field2: "a \<in> Field r \<Longrightarrow> underS r a \<subset> Field r"
  using underS_notIn underS_Field by fast

lemma underS_Field3: "Field r \<noteq> {} \<Longrightarrow> underS r a \<subset> Field r"
  by (cases "a \<in> Field r") (auto simp: underS_Field2 underS_empty)

lemma AboveS_Field: "AboveS r A \<subseteq> Field r"
  by (auto simp: AboveS_def Field_def)

lemma under_incr:
  assumes "trans r"
    and "(a, b) \<in> r"
  shows "under r a \<subseteq> under r b"
  unfolding under_def
proof auto
  fix x assume "(x, a) \<in> r"
  with assms trans_def[of r] show "(x, b) \<in> r" by blast
qed

lemma underS_incr:
  assumes "trans r"
    and "antisym r"
    and ab: "(a, b) \<in> r"
  shows "underS r a \<subseteq> underS r b"
  unfolding underS_def
proof auto
  assume *: "b \<noteq> a" and **: "(b, a) \<in> r"
  with \<open>antisym r\<close> antisym_def[of r] ab show False
    by blast
next
  fix x assume "x \<noteq> a" "(x, a) \<in> r"
  with ab \<open>trans r\<close> trans_def[of r] show "(x, b) \<in> r"
    by blast
qed

lemma underS_incl_iff:
  assumes LO: "Linear_order r"
    and INa: "a \<in> Field r"
    and INb: "b \<in> Field r"
  shows "underS r a \<subseteq> underS r b \<longleftrightarrow> (a, b) \<in> r"
    (is "?lhs \<longleftrightarrow> ?rhs")
proof
  assume ?rhs
  with \<open>Linear_order r\<close> show ?lhs
    by (simp add: order_on_defs underS_incr)
next
  assume *: ?lhs
  have "(a, b) \<in> r" if "a = b"
    using assms that by (simp add: order_on_defs refl_on_def)
  moreover have False if "a \<noteq> b" "(b, a) \<in> r"
  proof -
    from that have "b \<in> underS r a" unfolding underS_def by blast
    with * have "b \<in> underS r b" by blast
    then show ?thesis by (simp add: underS_notIn)
  qed
  ultimately show "(a,b) \<in> r"
    using assms order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
qed

lemma finite_Linear_order_induct[consumes 3, case_names step]:
  assumes "Linear_order r"
    and "x \<in> Field r"
    and "finite r"
    and step: "\<And>x. x \<in> Field r \<Longrightarrow> (\<And>y. y \<in> aboveS r x \<Longrightarrow> P y) \<Longrightarrow> P x"
  shows "P x"
  using assms(2)
proof (induct rule: wf_induct[of "r\<inverse> - Id"])
  case 1
  from assms(1,3) show "wf (r\<inverse> - 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 \<open>auto simp: aboveS_def intro: FieldI2\<close>)
qed


subsection \<open>Variations on Well-Founded Relations\<close>

text \<open>
  This subsection contains some variations of the results from @{theory Wellfounded}:
    \<^item> means for slightly more direct definitions by well-founded recursion;
    \<^item> variations of well-founded induction;
    \<^item> means for proving a linear order to be a well-order.
\<close>


subsubsection \<open>Characterizations of well-foundedness\<close>

text \<open>
  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.
\<close>

lemma trans_wf_iff:
  assumes "trans r"
  shows "wf r \<longleftrightarrow> (\<forall>a. wf (r \<inter> (r\<inverse>``{a} \<times> r\<inverse>``{a})))"
proof -
  define R where "R a = r \<inter> (r\<inverse>``{a} \<times> r\<inverse>``{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 *: "\<forall>a. wf(R a)"
    unfolding wf_def
  proof clarify
    fix phi a
    assume **: "\<forall>a. (\<forall>b. (b, a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
    define chi where "chi b \<longleftrightarrow> (b, a) \<in> r \<longrightarrow> phi b" for b
    with * have "wf (R a)" by auto
    then have "(\<forall>b. (\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
      unfolding wf_def by blast
    also have "\<forall>b. (\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
    proof (auto simp add: chi_def R_def)
      fix b
      assume "(b, a) \<in> r" and "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
      then have "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
        using assms trans_def[of r] by blast
      with ** show "phi b" by blast
    qed
    finally have  "\<forall>b. chi b" .
    with ** chi_def show "phi a" by blast
  qed
  ultimately show ?thesis unfolding R_def by blast
qed

text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
corollary wf_finite_segments:
  assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
  shows "wf (r)"
proof (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
  fix a
  have "trans (r \<inter> ({x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r}))"
    using assms unfolding trans_def Field_def by blast
  then show "acyclic (r \<inter> {x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r})"
    using assms acyclic_def assms irrefl_def by fastforce
qed

text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
  allowing one to assume the set included in the field.\<close>

lemma wf_eq_minimal2: "wf r \<longleftrightarrow> (\<forall>A. A \<subseteq> Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a', a) \<notin> r))"
proof-
  let ?phi = "\<lambda>A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r)"
  have "wf r \<longleftrightarrow> (\<forall>A. ?phi A)"
    apply (auto simp: ex_in_conv [THEN sym])
     apply (erule wfE_min)
      apply assumption
     apply blast
    apply (rule wfI_min)
    apply fast
    done
  also have "(\<forall>A. ?phi A) \<longleftrightarrow> (\<forall>B \<subseteq> Field r. ?phi B)"
  proof
    assume "\<forall>A. ?phi A"
    then show "\<forall>B \<subseteq> Field r. ?phi B" by simp
  next
    assume *: "\<forall>B \<subseteq> Field r. ?phi B"
    show "\<forall>A. ?phi A"
    proof clarify
      fix A :: "'a set"
      assume **: "A \<noteq> {}"
      define B where "B = A \<inter> Field r"
      show "\<exists>a \<in> A. \<forall>a' \<in> A. (a', a) \<notin> r"
      proof (cases "B = {}")
        case True
        with ** obtain a where a: "a \<in> A" "a \<notin> Field r"
          unfolding B_def by blast
        with a have "\<forall>a' \<in> A. (a',a) \<notin> r"
          unfolding Field_def by blast
        with a show ?thesis by blast
      next
        case False
        have "B \<subseteq> Field r" unfolding B_def by blast
        with False * obtain a where a: "a \<in> B" "\<forall>a' \<in> B. (a', a) \<notin> r"
          by blast
        have "(a', a) \<notin> r" if "a' \<in> A" for a'
        proof
          assume a'a: "(a', a) \<in> r"
          with that have "a' \<in> 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 \<open>Characterizations of well-foundedness\<close>

text \<open>
  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.
\<close>

lemma Linear_order_wf_diff_Id:
  assumes "Linear_order r"
  shows "wf (r - Id) \<longleftrightarrow> (\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r))"
proof (cases "r \<subseteq> Id")
  case True
  then have *: "r - Id = {}" by blast
  have "wf (r - Id)" by (simp add: *)
  moreover have "\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r"
    if *: "A \<subseteq> Field r" and **: "A \<noteq> {}" for A
  proof -
    from \<open>Linear_order r\<close> True
    obtain a where a: "r = {} \<or> r = {(a, a)}"
      unfolding order_on_defs using Total_subset_Id [of r] by blast
    with * ** have "A = {a} \<and> r = {(a, a)}"
      unfolding Field_def by blast
    with a show ?thesis by blast
  qed
  ultimately show ?thesis by blast
next
  case False
  with \<open>Linear_order r\<close> 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 "\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r)"
    proof clarify
      fix A
      assume **: "A \<subseteq> Field r" and ***: "A \<noteq> {}"
      then have "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
        using Field * unfolding wf_eq_minimal2 by simp
      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r \<longleftrightarrow> (a', a) \<notin> r - Id"
        using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** by blast
      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r" by blast
    qed
  next
    assume *: "\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r)"
    show "wf (r - Id)"
      unfolding wf_eq_minimal2
    proof clarify
      fix A
      assume **: "A \<subseteq> Field(r - Id)" and ***: "A \<noteq> {}"
      then have "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
        using Field * by simp
      moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r \<longleftrightarrow> (a', a) \<notin> r - Id"
        using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** mono_Field[of "r - Id" r] by blast
      ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
        by blast
    qed
  qed
qed

corollary Linear_order_Well_order_iff:
  "Linear_order r \<Longrightarrow>
    Well_order r \<longleftrightarrow> (\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r))"
  unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast

end