Theory HOL_Alignment_Orders

✐‹creator "Kevin Kappelmann"›
subsection ‹Alignment With Order Definitions from HOL›
theory HOL_Alignment_Orders
  imports
    "HOL-Library.Preorder"
    HOL_Alignment_Binary_Relations
    HOL_Syntax_Bundles_Orders
    Orders
begin

named_theorems HOL_order_alignment

paragraph ‹Functions›

definition "rel R x y ≡ (x, y) ∈ R"
lemma rel_of_eq [simp]: "rel = (λR x y. (x, y) ∈ R)" unfolding rel_def by simp
lemma rel_of_iff [iff]: "rel R x y ⟷ (x, y) ∈ R" by simp

subparagraph ‹Bi-Related›

overloading
  bi_related_set ≡ "bi_related :: 'a rel ⇒ 'a ⇒ 'a ⇒ bool"
begin
  definition "bi_related_set (S :: 'a rel) ≡ bi_related (rel S) :: 'a ⇒ 'a ⇒ bool"
end

lemma bi_related_set_eq_bi_related_pred [simp]:
  "((≡⇘S :: 'a rel⇙) :: 'a ⇒ 'a ⇒ bool) = (≡⇘rel S⇙)"
  unfolding bi_related_set_def by simp

lemma bi_related_set_eq_bi_related_pred_uhint [uhint]:
  assumes "R ≡ rel S"
  shows "(≡⇘S :: 'a rel⇙) :: 'a ⇒ 'a ⇒ bool ≡ (≡⇘R⇙)"
  using assms by simp

lemma bi_related_set_iff_bi_related_pred [iff]: "(x :: 'a) ≡⇘(S :: 'a rel)⇙ (y :: 'a) ⟷ x ≡⇘rel S⇙ y"
  by simp

lemma (in preorder_equiv) equiv_eq_bi_related [HOL_order_alignment]:
  "equiv = bi_related (≤)"
  by (intro ext) (auto intro: equiv_antisym dest: equivD1 equivD2)


subparagraph ‹Inflationary›

overloading
  inflationary_on_set ≡ "inflationary_on :: 'a set ⇒ ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool"
begin
  definition "inflationary_on_set (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool ≡
    inflationary_on (mem_of S)"
end

lemma inflationary_on_set_eq_inflationary_on_pred [simp]:
  "(inflationary_on (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool) =
    inflationary_on (mem_of S)"
  unfolding inflationary_on_set_def by simp

lemma inflationary_on_set_eq_inflationary_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "inflationary_on (S :: 'a set) :: ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool ≡ inflationary_on P"
  using assms by simp

lemma inflationary_on_set_iff_inflationary_on_pred [iff]:
  "inflationary_on (S :: 'a set) (R :: 'a ⇒ 'b ⇒ bool) (f :: 'a ⇒ 'b) ⟷
    inflationary_on (mem_of S) R f"
  by simp


subparagraph ‹Deflationary›

overloading
  deflationary_on_set ≡ "deflationary_on :: 'a set ⇒ ('b ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool"
begin
  definition "deflationary_on_set (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool ≡
    deflationary_on (mem_of S)"
end

lemma deflationary_on_set_eq_deflationary_on_pred [simp]:
  "(deflationary_on (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool) = deflationary_on (mem_of S)"
  unfolding deflationary_on_set_def by simp

lemma deflationary_on_set_eq_deflationary_on_pred_uhint [uhint]:
  assumes "P ≡ mem_of S"
  shows "deflationary_on (S :: 'a set) :: ('b ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool ≡ deflationary_on P"
  using assms by simp

lemma deflationary_on_set_iff_deflationary_on_pred [iff]:
  "deflationary_on (S :: 'a set) (R :: 'b ⇒ 'a ⇒ bool) (f :: 'a ⇒ 'b) ⟷ deflationary_on (mem_of S) R f"
  by simp


subparagraph ‹Idempotent›

overloading
  idempotent_on_set ≡ "idempotent_on :: 'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool"
begin
  definition "idempotent_on_set (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool ≡
    idempotent_on (mem_of S)"
end

lemma idempotent_on_set_eq_idempotent_on_pred [simp]:
  "(idempotent_on (S :: 'a set) :: ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool) = idempotent_on (mem_of S)"
  unfolding idempotent_on_set_def by simp

lemma idempotent_on_set_iff_idempotent_on_pred [iff]:
  "idempotent_on (S :: 'a set) (R :: 'a ⇒ 'a ⇒ bool) (f :: 'a ⇒ 'a) ⟷ idempotent_on (mem_of S) R f"
  by simp


paragraph ‹Properties›
subparagraph ‹Equivalence Relations›

lemma equiv_eq_equivalence_rel [HOL_order_alignment]: "equivp = equivalence_rel"
  by (intro ext) (fastforce intro: equivpI
    simp: HOL_bin_rel_alignment equivalence_rel_eq_equivalence_rel_on
    elim: equivpE)


subparagraph ‹Partial Equivalence Relations›

lemma part_equiv_eq_partial_equivalence_rel_if_rel [HOL_order_alignment]:
  assumes "R x y"
  shows "part_equivp R = partial_equivalence_rel R"
  using assms by (fastforce intro!: part_equivpI simp: HOL_bin_rel_alignment
    partial_equivalence_rel_eq_partial_equivalence_rel_on
    elim!: part_equivpE)


subparagraph ‹Partial Orders›

lemma (in order) partial_order [HOL_order_alignment]: "partial_order (≤)"
  using order_refl order_trans order_antisym by blast


subparagraph ‹Preorders›

lemma (in partial_preordering) preorder [HOL_order_alignment]: "preorder (❙≤)"
  using refl trans by blast

lemma partial_preordering_eq [HOL_order_alignment]:
  "partial_preordering = Preorders.preorder"
  by (intro ext) (auto intro: partial_preordering.intro
    dest: partial_preordering.trans partial_preordering.refl reflexiveD)

subparagraph ‹Linear Orders›

lemma (in linorder) linear_order: "linear_order (≤)"
  using linear partial_order by blast

subparagraph ‹Strict Parital Orders›

lemma (in preordering) linear_order: "strict_partial_order (❙<)"
  using strict_iff_not trans by blast

subparagraph ‹Strict Linear Orders›

lemma (in linorder) strict_linear_order: "strict_linear_order (<)"
  using preordering.linear_order local.order.linear_order
  by (intro strict_linear_orderI) auto

subparagraph ‹Well-Orders›

lemma (in wellorder) wellorder: "wellorder (<)"
  by (metis wellorderI local.strict_linear_order local.wfp_on_less wfp_eq_wellfounded)

end