Theory Wellorders

✐‹creator "Kevin Kappelmann"›
✐‹creator "Niklas Krofta"›
subsubsection ‹Well-Orders›
theory Wellorders
  imports
    Binary_Relations_Wellfounded
    Strict_Linear_Orders
begin

definition "wellorder_on ≡ strict_linear_order_on ⊓ wellfounded_on"

lemma wellorder_onI [intro]:
  assumes "strict_linear_order_on P R" "wellfounded_on P R"
  shows "wellorder_on P R"
  using assms unfolding wellorder_on_def by auto

lemma wellorder_onE [elim]:
  assumes "wellorder_on P R"
  obtains "strict_linear_order_on P R" "wellfounded_on P R"
  using assms unfolding wellorder_on_def by auto

lemma antimono_wellorder_on:
  "antimono (wellorder_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  using antimono_strict_linear_order_on wellfounded_on_if_le_pred_if_wellfounded_on
  by (intro antimonoI le_predI; elim wellorder_onE) (auto 5 0)

lemma wellorder_on_rel_map_if_injective_on_if_mono_wrt_pred_if_wellorder_on:
  fixes P :: "'a ⇒ bool"
  assumes "wellorder_on P R" "(Q ⇒ P) f" "injective_on Q f"
  shows "wellorder_on Q (rel_map f R)"
  using assms
    strict_linear_order_on_rel_map_if_injective_on_if_mono_wrt_pred_if_strict_linear_order_on
    wellfounded_on_rel_map_if_mono_wrt_pred_if_wellfounded_on
  by fastforce


consts wellorder :: "'a ⇒ bool"

overloading
  wellorder ≡ "wellorder :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "(wellorder :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ wellorder_on (⊤ :: 'a ⇒ bool)"
end

lemma wellorder_eq_wellorder_on:
  "(wellorder :: ('a ⇒ 'a ⇒ bool) ⇒ bool) = wellorder_on (⊤ :: 'a ⇒ bool)"
  unfolding wellorder_def ..

lemma wellorder_eq_wellorder_on_uhint [uhint]:
  assumes "P ≡ ⊤ :: 'a ⇒ bool"
  shows "(wellorder :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ wellorder_on P"
  using assms by (simp add: wellorder_eq_wellorder_on)

context
  fixes R :: "'a ⇒ 'a ⇒ bool"
begin

lemma wellorderI [intro]:
  assumes "strict_linear_order R"
  and "wellfounded R"
  shows "wellorder R"
  using assms by (urule wellorder_onI)

lemma wellorderE [elim]:
  assumes "wellorder R"
  obtains "strict_linear_order R" "wellfounded R"
  using assms by (urule (e) wellorder_onE)

lemma wellorder_on_if_wellorder:
  fixes P :: "'a ⇒ bool"
  assumes "wellorder R"
  shows "wellorder_on P R"
  using assms by (elim wellorderE)
  (intro wellorder_onI strict_linear_order_on_if_strict_linear_order wellfounded_on_if_wellfounded)

end


end