Theory Binary_Relations_Wellfounded

✐‹creator "Kevin Kappelmann"›
✐‹creator "Niklas Krofta"›
subsubsection ‹Well-Founded Relations›
theory Binary_Relations_Wellfounded
  imports
    Functions_Monotone
begin

consts wellfounded_on :: "'a ⇒ 'b ⇒ bool"

overloading
  wellfounded_on_pred ≡ "wellfounded_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "wellfounded_on_pred (P :: 'a ⇒ bool) (R :: 'a ⇒ 'a ⇒ bool)
    ≡ ∀Q. (∃x : P. Q x) ⟶ (∃m : P. Q m ∧ (∀y : P. R y m ⟶ ¬(Q y)))"
end

lemma wellfounded_onI:
  assumes "⋀Q x. P x ⟹ Q x ⟹ ∃m : P. Q m ∧ (∀y : P. R y m ⟶ ¬(Q y))"
  shows "wellfounded_on P R"
  using assms unfolding wellfounded_on_pred_def by blast

lemma wellfounded_onE:
  assumes "wellfounded_on P R" "P x" "Q x"
  obtains m where "P m" "Q m" "⋀y. P y ⟹ R y m ⟹ ¬(Q y)"
proof -
  from assms obtain m where "P m" "Q m" "∀y : P. R y m ⟶ ¬(Q y)"
    unfolding wellfounded_on_pred_def by auto
  then show ?thesis using that by blast
qed

lemma wellfounded_on_induct [consumes 1, case_names step]:
  assumes "wellfounded_on P R" "P z"
  assumes step: "⋀x. P x ⟹ (⋀y. P y ⟹ R y x ⟹ Q y) ⟹ Q x"
  shows "Q z"
proof (rule ccontr)
  assume "¬(Q z)"
  then obtain m where "P m" "¬(Q m)" "⋀y. P y ⟹ R y m ⟹ Q y"
    using assms by (blast elim!: wellfounded_onE[where Q = "λx. ¬(Q x)"])
  then show "False" using step by auto
qed

lemma wellfounded_on_rel_map_if_mono_wrt_pred_if_wellfounded_on:
  fixes A :: "'a ⇒ bool" and B :: "'b ⇒ bool"
  assumes wf: "wellfounded_on A R"
  and "(B ⇒ A) f"
  shows "wellfounded_on B (rel_map f R)"
proof (intro wellfounded_onI)
  fix Q and x :: 'b assume "B x" "Q x"
  moreover define U where "U ≡ has_inverse_on (B ⊓ Q) f"
  ultimately have "A (f x)" "U (f x)" using ‹(B ⇒ A) f› by auto
  then obtain m⇩U where "A m⇩U" "U m⇩U" and min: "⋀a. A a ⟹ R a m⇩U ⟹ ¬(U a)"
    using wf by (blast elim!: wellfounded_onE)
  from ‹U m⇩U› obtain m⇩Q where "B m⇩Q" "f m⇩Q = m⇩U" "Q m⇩Q" unfolding U_def by blast
  have "¬(Q b)" if "B b" "rel_map f R b m⇩Q" for b
  proof -
    from that have "R (f b) m⇩U" using ‹f m⇩Q = m⇩U› by auto
    then have "¬(U (f b))" using ‹B b› ‹(B ⇒ A) f› min by blast
    then show ?thesis unfolding U_def using ‹B b› by blast
  qed
  then show "∃m : B. Q m ∧ (∀b : B. rel_map f R b m ⟶ ¬(Q b))" using ‹B m⇩Q› ‹Q m⇩Q› by blast
qed

corollary wellfounded_on_if_le_pred_if_wellfounded_on:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "wellfounded_on P R" "Q ≤ P"
  shows "wellfounded_on Q R"
proof -
  have "(Q ⇒ P) id" using ‹Q ≤ P› by force
  then have "wellfounded_on Q (rel_map id R)"
    using assms wellfounded_on_rel_map_if_mono_wrt_pred_if_wellfounded_on by blast
  then show ?thesis by simp
qed

lemma wellfounded_on_if_le_rel_if_wellfounded_on:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "wellfounded_on P R" "S ≤ R"
  shows "wellfounded_on P S"
proof (intro wellfounded_onI)
  fix Q and x :: 'a assume "P x" "Q x"
  then obtain m where "P m" "Q m" "⋀y. P y ⟹ R y m ⟹ ¬ Q y"
    using assms by (force elim!: wellfounded_onE)
  then show "∃m : P. Q m ∧ (∀y : P. S y m ⟶ ¬ Q y)" using ‹S ≤ R› by blast
qed

corollary antimono_wellfounded_on:
  "((≤) ⇒ (≤) ⇛ (≥)) (wellfounded_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  using wellfounded_on_if_le_pred_if_wellfounded_on wellfounded_on_if_le_rel_if_wellfounded_on
  by (intro mono_wrt_relI Fun_Rel_relI) blast


consts wellfounded :: "'a ⇒ bool"

overloading
  wellfounded ≡ "wellfounded :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "(wellfounded :: ('a ⇒ 'a ⇒ bool) ⇒ bool) ≡ wellfounded_on (⊤ :: 'a ⇒ bool)"
end

lemma wellfounded_eq_wellfounded_on:
  "(wellfounded :: ('a ⇒ 'a ⇒ bool) ⇒ _) = wellfounded_on (⊤ :: 'a ⇒ bool)"
  unfolding wellfounded_def ..

lemma wellfounded_eq_wellfounded_on_uhint [uhint]:
  "P ≡ (⊤ :: 'a ⇒ bool) ⟹ (wellfounded :: ('a ⇒ 'a ⇒ bool) ⇒ _) ≡ wellfounded_on P"
  by (simp add: wellfounded_eq_wellfounded_on)

lemma wellfoundedI [intro]:
  assumes "⋀Q x. Q x ⟹ (∃m : Q. ∀y. R y m ⟶ ¬(Q y))"
  shows "wellfounded R"
  by (urule wellfounded_onI) (use assms in fastforce)

lemma wellfoundedE:
  assumes "wellfounded R" "Q x"
  obtains m where "Q m" "⋀y. R y m ⟹ ¬(Q y)"
  by (urule wellfounded_onE) (urule assms | simp)+

lemma wellfounded_on_if_wellfounded:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "wellfounded R"
  shows "wellfounded_on P R"
  using assms by (urule wellfounded_on_if_le_pred_if_wellfounded_on) auto

lemma wellfounded_induct [consumes 1, case_names step]:
  assumes "wellfounded R"
  assumes "⋀x. (⋀y. R y x ⟹ Q y) ⟹ Q x"
  shows "Q x"
  using assms(1) by (urule wellfounded_on_induct) (use assms(2-) in auto)

lemma wellfounded_rel_restrict_if_wellfounded_on:
  assumes "wellfounded_on P R"
  shows "wellfounded R↑⇘P⇙"
proof (intro wellfoundedI)
  fix Q and x :: 'a assume "Q x"
  show "∃m : Q. ∀y. R↑⇘P⇙ y m ⟶ ¬(Q y)"
  proof (cases "∃s : P. Q s")
    case True
    then show ?thesis using assms by (fast elim!: wellfounded_onE)
  next
    case False
    then show ?thesis using ‹Q x› by blast
  qed
qed


end