Theory Quasi_Order

theory Quasi_Order
imports Reduction_Pair Lattice_Syntax
(*
Author:  Akihisa Yamada (2017)
License: LGPL (see file COPYING.LESSER)
*)
theory Quasi_Order
  imports
    Reduction_Pair
    HOL.Complete_Lattices
    "HOL-Library.Lattice_Syntax"
begin

(*FIXME: move*)
section‹Convenient Relation-to-Set Conversion›

abbreviation rel_of where "rel_of f ≡ Collect (case_prod f)"

lemma mem_rel_ofI: "r1 x y ⟹ (x,y) ∈ rel_of r1" by simp
lemma rel_of:
  shows rel_of_OO: "⋀r1 r2. rel_of (r1 OO r2) = rel_of r1 O rel_of r2"
    and rel_of_sup: "⋀r1 r2. rel_of (r1 ⊔ r2) = rel_of r1 ∪ rel_of r2"
    and rel_of_inf: "⋀r1 r2. rel_of (r1 ⊓ r2) = rel_of r1 ∩ rel_of r2"
    and rel_of_tranclp: "⋀r. rel_of (r++) = (rel_of r)+"
    and rel_of_rtranclp: "⋀r. rel_of (r**) = (rel_of r)*"
    and rel_of_conversep: "⋀r. rel_of r¯¯ = (rel_of r)¯"
    and le_by_rel_of: "⋀r1 r2. r1 ≤ r2 ⟷ rel_of r1 ⊆ rel_of r2"
    and eq_by_rel_of: "⋀r1 r2. r1 = r2 ⟷ rel_of r1 = rel_of r2"
    and wfP_by_rel_of: "⋀r. wfP r ⟷ wf (rel_of r)"
  by (auto 0 4 simp add: trancl_def rtrancl_def wfP_def)

(* Maybe automation is useful *)
lemmas OO_mono1 = O_mono1[of "rel_of _" "rel_of _" "rel_of _", folded rel_of]
lemmas OO_mono2 = O_mono2[of "rel_of _" "rel_of _" "rel_of _", folded rel_of]
lemmas OO_assoc = O_assoc[of "rel_of _" "rel_of _" "rel_of _", folded rel_of]

lemma tranclp_mono: "r ≤ s ⟹ r++ ≤ s++"
  by (simp add: rel_of subrelI trancl_mono)

lemma wf_O_comm: "wf (R O S) ⟷ wf (S O R)"
  using SN_O_comm
  by (metis SN_iff_wf converse_converse converse_relcomp)

lemma wf_relto_relcomp: "wf (relto R S) ⟷ wf (R O S*)"
  using SN_on_relto_relcomp[of "S¯" "R¯" UNIV]
  by (simp add: rtrancl_converse converse_relcomp[symmetric] SN_iff_wf O_assoc)

context
  fixes S R
  assumes pull: "S O R ⊆ R* O S"
begin

qualified lemma push: "R¯ O S¯ ⊆ S¯ O (R¯)*"
  by (metis pull converse_mono converse_relcomp rtrancl_converse)

lemma O_rtrancl_pull: "S O R* ⊆ R* O S"
  using rtrancl_O_push[OF push]
  by (metis converse_mono converse_relcomp rtrancl_converse)

lemma rtrancl_U_pull: "(S ∪ R)* = R* O S*"
  using rtrancl_U_push[OF push]
  by (metis converse_Un converse_converse converse_relcomp rtrancl_converse sup_commute)

lemma wf_relto_pull: "wf (R* O S O R*) ⟷ wf S"
  apply (rule iffI)
  apply (rule wf_subset, force, force)
  unfolding wf_relto_relcomp
  using SN_on_O_push[OF push, of UNIV]
  by (subst wf_O_comm, auto simp: O_rtrancl_pull wf_relcomp_compatible)

end

lemma wf_trancl_iff[simp]: "wf (R+) ⟷ wf R"
  by (intro iffI[OF wf_subset[of "R+"] wf_trancl], auto)

context
  fixes R S :: "('a × 'a) set"
  assumes absorb: "R O S ⊆ R"
begin

lemma O_rtrancl_absorb_right: "R O S* = R"
proof-
  { fix x y z
    have "(y,z) ∈ S* ⟹ (x,y) ∈ R ⟹ (x,z) ∈ R"
      by (induct rule: rtrancl_induct, insert absorb, auto)
  }
  then show ?thesis by auto
qed

lemma rtrancl_U_absorb_right: "(S ∪ R)* = S* O R*"
  apply (subst Un_commute)
  apply (rule rtrancl_U_pull)
  using absorb by auto

lemma wf_relto_absorb_right: "wf (relto R S) ⟷ wf R"
  apply (rule wf_relto_pull) using absorb by auto

end

section ‹Quasi-Orderings›

context ord begin

text ‹Extending @{class ord} with some more notations.›

definition equiv (infix "∼" 50) where [simp]: "x ∼ y ≡ x ≤ y ∧ y ≤ x"

lemma equiv_sym[sym]: "x ∼ y ⟹ y ∼ x" by auto

definition equiv_class ("[_]") where "[x] ≡ { y. x ∼ y }"

lemma mem_equiv_class[simp]: "y ∈ [x] ⟷ x ∼ y" by (auto simp: equiv_class_def)

definition "Upper_Bounds X ≡ {b. ∀x ∈ X. b ≥ x}"

lemma mem_Upper_Bounds: "b ∈ Upper_Bounds X ⟷ (∀x ∈ X. b ≥ x)"
  by (auto simp: Upper_Bounds_def)

lemma Upper_BoundsI[intro]: "(⋀x. x ∈ X ⟹ b ≥ x) ⟹ b ∈ Upper_Bounds X"
  by (auto simp: Upper_Bounds_def)

lemma Upper_BoundsE[elim]: "b ∈ Upper_Bounds X ⟹ ((⋀x. x ∈ X ⟹ b ≥ x) ⟹ thesis) ⟹ thesis"
  by (auto simp: Upper_Bounds_def)

lemma Upper_Bounds_empty[simp]: "Upper_Bounds {} = UNIV" by auto
lemma Upper_Bounds_insert: "Upper_Bounds (insert x X) = {b. b ≥ x} ∩ Upper_Bounds X" by auto
lemma Upper_Bounds_singleton[simp]: "Upper_Bounds {x} = {b. b ≥ x}" by auto

lemma Upper_Bounds_cmono: assumes "X ⊆ Y" shows "Upper_Bounds X ⊇ Upper_Bounds Y"
  using assms by (auto simp: Upper_Bounds_def)

definition "Leasts X ≡ { b ∈ X. ∀c ∈ X. b ≤ c }"

lemma LeastsI[intro]: "b ∈ X ⟹ (⋀x. x ∈ X ⟹ b ≤ x) ⟹ b ∈ Leasts X"
  and LeastsD: "x ∈ Leasts X ⟹ y ∈ X ⟹ x ≤ y"
  and LeastsE[elim]: "b ∈ Leasts X ⟹ (b ∈ X ⟹ (⋀x. x ∈ X ⟹ b ≤ x) ⟹ thesis) ⟹ thesis"
  by (auto simp: Leasts_def)

lemma Least_Upper_Bounds_mono:
  assumes XY: "X ⊆ Y" and bX: "bX ∈ Leasts (Upper_Bounds X)" and bY: "bY ∈ Leasts (Upper_Bounds Y)"
  shows "bX ≤ bY"
proof-
  have "bY ∈ Upper_Bounds X" using XY bY by force
  with bX show ?thesis by auto
qed

lemma Leasts_equiv: "x ∈ Leasts X ⟹ y ∈ Leasts X ⟹ x ∼ y" by auto

end

text ‹This is a trick to make a class available also as a locale›

locale ord_syntax = ord less_eq less for less_eq less :: "'a ⇒ 'a ⇒ bool"
begin

notation less_eq (infix "⊑" 50)
notation less (infix "⊏" 50)
abbreviation(input) greater_eq_syntax (infix "⊒" 50) where "greater_eq_syntax ≡ ord.greater_eq less_eq"
abbreviation(input) greater_syntax (infix "⊐" 50) where "greater_syntax ≡ ord.greater less"

abbreviation equiv_syntax (infix "≃" 50) where "equiv_syntax ≡ ord.equiv less_eq"

abbreviation equiv_class_syntax ("[_]") where "equiv_class_syntax ≡ ord.equiv_class less_eq"

end

class quasi_order = ord +
  assumes order_refl[iff]: "x ≤ x"
      and order_trans[trans]: "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
      and le_less_trans[trans]: "x ≤ y ⟹ y < z ⟹ x < z"
      and less_le_trans[trans]: "x < y ⟹ y ≤ z ⟹ x < z"
      and less_imp_le: "x < y ⟹ x ≤ y"
begin

lemma eq_imp_le: "x = y ⟹ x ≤ y" by auto

lemma less_trans[trans]: "x < y ⟹ y < z ⟹ x < z"
  using le_less_trans[OF less_imp_le].

text ‹
 Class @{class quasi_order} is incomparable with HOL class @{class preorder}, as the latter
 fixes $<$ as the "strict part" (which is not nice, e.g., for comparing polynomials)
 while we already assume compatibility (@{thm le_less_trans}).
›

lemma equiv_trans[trans]:
  "x ∼ y ⟹ y ∼ z ⟹ x ∼ z"
  "x ∼ y ⟹ y ≤ z ⟹ x ≤ z"
  "x ≤ y ⟹ y ∼ z ⟹ x ≤ z"
  "x ∼ y ⟹ y < z ⟹ x < z"
  "x < y ⟹ y ∼ z ⟹ x < z"
  by (auto dest: order_trans le_less_trans less_le_trans)

lemma chainp_le_mono:
  assumes ch: "chainp (≤) seq" and ij: "i ≤ j" shows "seq i ≤ seq j"
  by (insert ij, induct rule: inc_induct, insert ch, auto dest: order_trans)

lemma chainp_less_mono: assumes ch: "chainp (<) seq" and ij: "i < j" shows "seq i < seq j"
  by (insert ij, induct rule:strict_inc_induct, insert ch, auto dest: less_trans)


lemma Leasts_singleton[simp]: "Leasts {a} = {a}"
  by auto

lemma Least_Upper_Bounds_singleton: "Leasts ({b. b ≥ x}) = [x]"
  by (auto intro!: LeastsI dest: order_trans)

lemma Least_Upper_Bounds_equiv_class:
  assumes bX: "b ∈ Leasts (Upper_Bounds X)" shows "Leasts (Upper_Bounds X) = [b]"
proof(intro equalityI subsetI, unfold mem_equiv_class)
  from bX have bX: "b ∈ Upper_Bounds X" and leastb: "⋀x. x ∈ Upper_Bounds X ⟹ b ≤ x" by auto
  { fix c assume "c ∈ Leasts (Upper_Bounds X)"
    then have cUpper_Bounds: "c ∈ Upper_Bounds X" and leastc: "⋀b. b ∈ Upper_Bounds X ⟹ c ≤ b" by auto
    from leastb[OF cUpper_Bounds] leastc[OF bX] show "b ∼ c" by auto
  }
  { fix c assume bc: "b ∼ c"
    show "c ∈ Leasts (Upper_Bounds X)"
    proof(intro LeastsI Upper_BoundsI)
      fix x assume "x ∈ X"
      with bX have "x ≤ b" by auto
      with bc show "x ≤ c" by (auto dest: order_trans)
    next
      fix x assume "x ∈ Upper_Bounds X"
      from leastb[OF this] bc show "c ≤ x" by (auto dest: order_trans)
    qed
  }
qed

sublocale order_pair "rel_of (>)" "rel_of (≥)"
  apply (unfold_locales, fold transp_trans)
  using le_less_trans less_le_trans
  by (auto intro: refl_onI transpI[OF less_trans] transpI[OF order_trans])

end

subsection ‹Weakly ordered domain: where antisymmetry holds›
class weak_order = quasi_order + assumes antisym[dest]: "a ≤ b ⟹ b ≤ a ⟹ a = b"
begin

lemma equiv_is_eq[simp]: "(∼) = (=)" by (intro ext, auto)

lemma equiv_class_singleton[simp]: "[a] = {a}" by auto

lemma Least_Upper_Bound_singleton[simp]: "Leasts (Upper_Bounds {a}) = {a}" by auto

end

declare equiv_def[simp del]

subclass(in order) weak_order by(unfold_locales, auto)


subsection ‹Well-founded quasi-ordered domain›

class wf_order = quasi_order +
  assumes less_induct[case_names less]: "⋀P a. (⋀x. (⋀y. y < x ⟹ P y) ⟹ P x) ⟹ P a"
begin

lemma wf: "wf (rel_of (<))" unfolding wf_def by(auto intro:less_induct)

sublocale SN_order_pair "rel_of (>)" "rel_of (≥)"
  by (unfold_locales, auto simp: SN_iff_wf converse_def conversep.simps intro: wf)

lemma chainp_ends_nonstrict:
  assumes 0: "chainp (≥) seq" shows "∃n. ∀i ≥ n. ¬ seq (Suc i) < seq i"
proof (rule ccontr, insert 0, induct "seq 0" arbitrary: seq rule: less_induct)
  case (less seq)
  from less.prems
  obtain n where 1: "seq n > seq (Suc n)" by auto
  define seq' where "⋀i. seq' i = seq (Suc n + i)"
  show False
  proof (rule less.hyps)
    from less.prems show "chainp (≥) seq'" by (auto simp: seq'_def)
    note 1
    also have "seq 0 ≥ seq n" using less.prems by (induct n, auto dest: order_trans)
    finally show "seq 0 > seq' 0" by (auto simp: seq'_def)
    show "∄n. ∀i≥n. ¬ seq' (Suc i) < seq' i"
    proof (unfold not_ex, intro allI notI)
      fix m
      assume 2: "∀i≥m. ¬ seq' (Suc i) < seq' i"
      from less.prems(1)[simplified, rule_format, of "m+n+1"]
      obtain i where "i ≥ m + n + 1" and "seq (Suc i) < seq i" by auto
      then have "i - n - 1 ≥ m" and "seq' (Suc (i-n-1)) < seq' (i-n-1)" by (auto simp: seq'_def)
      with 2 show False by auto
    qed
  qed
qed

end


text ‹@{class wellorder} is a @{class wf_order}.›

context wellorder begin

subclass wf_order by (unfold_locales; (fact less_induct | simp))

lemma chainp_ends_eq:
  assumes 1: "chainp (≥) seq" shows "∃n. ∀i≥n. seq i = seq n"
proof-
  from chainp_ends_nonstrict[OF 1] 1
  obtain n where 2: "⋀i. i ≥ n ⟹ seq (Suc i) = seq i" by (auto simp: not_less)
  show ?thesis
  proof (intro exI allI impI)
    show "n ≤ i ⟹ seq i = seq n" for i by (induct rule:dec_induct, auto simp: 2)
  qed
qed

end

text ‹@{type nat} is a @{class wf_order}.›
instance nat :: wf_order ..

text ‹The next one turns a well-founded relation into a well-founded order pair.›
locale wf_order_seed =
  fixes w s :: "'a ⇒ 'a ⇒ bool"
  assumes wf: "wfP s"
    and weak_compatp: "s OO w ≤ s++"
begin

definition less (infix "⊏" 50) where "less ≡ (w** OO s)++"

definition less_eq (infix "⊑" 50) where "less_eq ≡ (w ⊔ s)**"

lemma absorb: "s++ OO w ≤ s++"
proof-
  have "s++ x y ⟹ w y z ⟹ s++ x z" for x y z
    by (induct rule: tranclp_induct, insert weak_compatp, auto)
  then show ?thesis by auto
qed

sublocale wf_order where less_eq = less_eq and less = less
proof (unfold_locales)
  have [trans]: "⋀x y z. less x y ⟹ less y z ⟹ less x z" by (auto simp: less_def)
  have "less ≤ less_eq" by (unfold less_def less_eq_def rel_of, regexp)
  then show "⋀x y. x ⊏ y ⟹ x ⊑ y" by auto
  show [trans]: "⋀x y z. x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z" by (auto simp: less_eq_def)
  have 1: "less_eq OO less ≤ less" by (unfold rel_of less_eq_def less_def, regexp)
  then show "⋀x y z. x ⊑ y ⟹ y ⊏ z ⟹ x ⊏ z" by auto
  have "less OO w ≤ (w** OO s)** OO w** OO s++"
    apply (unfold less_def)
    apply (subst trancl_unfold_right[of "rel_of _", unfolded rel_of[symmetric]])
    using OO_mono1[OF weak_compatp, of "(w** OO s)** OO w**"]
    by (simp add: OO_assoc)
  also have "... ≤ less" by (unfold less_def rel_of, regexp)
  finally have "less OO w ≤ less".
  moreover have "less OO s ≤ less" by (unfold less_def rel_of, regexp)
  ultimately have "less OO (w ⊔ s) ≤ less" by auto
  then have 2: "less OO less_eq = less"
    by (simp add: less_eq_def rel_of O_rtrancl_absorb_right)
  from eq_imp_le[OF this] show "⋀x y z. x ⊏ y ⟹ y ⊑ z ⟹ x ⊏ z" by force
  have less: "less = (w** OO s++ OO w**)++"
    apply (subst 2[symmetric])
    apply (unfold less_eq_def less_def rel_of)
    apply regexp
    done
  have "wf (rel_of less)"
    apply (unfold less rel_of wf_trancl_iff)
    apply (subst wf_relto_absorb_right) using absorb wf
    by (auto simp: rel_of)
  then show "⋀P a. (⋀x. (⋀y. y ⊏ x ⟹ P y) ⟹ P x) ⟹ P a"
    by (auto simp: wf_def)
qed (auto simp: less_eq_def)

end

class quasi_order_sup = quasi_order + sup +
  assumes sup_ge1 [intro!]: "x ≤ x ⊔ y"
      and sup_ge2 [intro!]: "y ≤ x ⊔ y"
begin

lemma sup_trans1: assumes "x ≤ y" shows "x ≤ y ⊔ z"
proof-
  note assms also note sup_ge1 finally show ?thesis by auto
qed

lemma sup_trans2: assumes "x ≤ z" shows "x ≤ y ⊔ z"
proof-
  note assms also note sup_ge2 finally show ?thesis by auto
qed

lemma finite_set_has_Upper_Bounds: "finite X ⟹ ∃b. b ∈ Upper_Bounds X"
  by (unfold Upper_Bounds_def, induct X rule:finite_induct, auto dest: sup_trans1)

lemma finite_set_is_bounded:
  assumes "finite X" and "x ∈ X" shows "x ≤ (SOME b. b ∈ Upper_Bounds X)"
  using finite_set_has_Upper_Bounds[OF assms(1), folded some_eq_ex] assms(2) by auto

end

class quasi_semilattice_sup = quasi_order_sup +
  assumes sup_least: "y ≤ x ⟹ z ≤ x ⟹ y ⊔ z ≤ x"
begin

lemma finite_set_has_Least_Upper_Bounds: "finite X ⟹ X ≠ {} ⟹ ∃b. b ∈ Leasts (Upper_Bounds X)"
proof(induct X rule:finite_induct)
  case empty then show ?case by auto
next
  case IH: (insert x X)
  show ?case
  proof(cases "X = {}")
    case True
    with Least_Upper_Bounds_singleton have "Leasts (Upper_Bounds (insert x X)) = [x]" by auto
    then show ?thesis by auto
  next
    case False
    with IH have "Leasts (Upper_Bounds X) ≠ {}" by auto
    then obtain b where bX: "b ∈ Leasts (Upper_Bounds X)" by auto
    then have "sup x b ∈ Leasts (Upper_Bounds (insert x X))"
      by (auto intro: sup_trans2 sup_least intro!: LeastsI Upper_BoundsI simp: Upper_Bounds_insert)
    then show ?thesis by auto
  qed
qed

end

subclass (in semilattice_sup) quasi_semilattice_sup by (unfold_locales, auto)

class quasi_order_bot = quasi_order + bot +
  assumes bot_least: "⊥ ≤ a"

text ‹A class where the @{const Sup} operator is defined, which is valid only if it is definable.›

class quasi_order_Sup = quasi_order + Sup +
  assumes Sup_in_Least_Upper_Bounds: "Leasts (Upper_Bounds X) ≠ {} ⟹ ⨆X ∈ Leasts (Upper_Bounds X)"
begin

lemma Sup_upper: assumes LUB: "Leasts (Upper_Bounds X) ≠ {}" and xX: "x ∈ X" shows "x ≤ ⨆X"
  using Sup_in_Least_Upper_Bounds[OF LUB] xX by auto

lemma Sup_least: assumes LUB: "Leasts (Upper_Bounds X) ≠ {}" shows "(⋀x. x ∈ X ⟹ x ≤ y) ⟹ ⨆X ≤ y"
  using Sup_in_Least_Upper_Bounds[OF LUB] by (auto simp: Upper_Bounds_def)

lemma Sup_equiv_Least_Upper_Bounds: assumes bX: "b ∈ Leasts (Upper_Bounds X)" shows "⨆X ∼ b"
proof-
  have "Leasts (Upper_Bounds X) ≠ {}" using bX by auto
  from Sup_in_Least_Upper_Bounds[OF this] show ?thesis using bX by auto
qed

lemma Sup_singleton: "⨆{x} ∼ x" by (rule Sup_equiv_Least_Upper_Bounds, auto)

lemma Sup_mono:
  assumes X: "Leasts (Upper_Bounds X) ≠ {}" and Y: "Leasts (Upper_Bounds Y) ≠ {}" and XY: "X ⊆ Y"
  shows "⨆X ≤ ⨆Y"
  by (auto intro: Least_Upper_Bounds_mono[OF XY] Sup_in_Least_Upper_Bounds[OF X] Sup_in_Least_Upper_Bounds[OF Y])

end

text ‹Upward complete quasi-semilattices -- where @{const Sup} is always defined.›

class quasi_semilattice_Sup = quasi_order_Sup + sup + bot +
  assumes Least_Upper_Bounds: "Leasts (Upper_Bounds X) ≠ {}"
    and sup_Sup: "x ⊔ y = ⨆{x,y}"
    and bot_Sup: "⊥ = ⨆{}"
begin

lemmas Sup_in_Least_Upper_Bounds = Sup_in_Least_Upper_Bounds[OF Least_Upper_Bounds]
lemmas Sup_upper = Sup_upper[OF Least_Upper_Bounds]
lemmas Sup_least = Sup_least[OF Least_Upper_Bounds]
lemmas Sup_mono = Sup_mono[OF Least_Upper_Bounds]

subclass quasi_semilattice_sup
  by (unfold_locales, auto intro: Sup_upper Sup_least simp: sup_Sup)

subclass quasi_order_bot
proof(unfold_locales)
  fix x
  have "⊥ ≤ ⨆{x}" by (unfold bot_Sup, rule Sup_mono, auto)
  also have "… ∼ x" by (rule Sup_singleton)
  finally show "⊥ ≤ x".
qed

end


subsection ‹@{term inv_imagep}›

locale quasi_order_inv_imagep = base: quasi_order
begin

sublocale quasi_order "inv_imagep less_eq f" "inv_imagep less f"
  by (unfold_locales, unfold in_inv_imagep;
   fact base.order_refl base.order_trans base.less_trans base.less_le_trans base.le_less_trans base.less_imp_le)

end

locale wf_order_inv_imagep = base: wf_order
begin

interpretation quasi_order_inv_imagep..

sublocale wf_order "inv_imagep less_eq f" "inv_imagep less f"
  apply (unfold_locales)
  apply (unfold in_inv_imagep)
  using wf_inv_image[OF base.wf, unfolded wf_def] by auto

end

end