# Theory HOL-Cardinals.Wellfounded_More

section ‹More on Well-Founded Relations›
theory Wellfounded_More
imports Main Order_Relation_More
begin
subsection ‹Well-founded recursion via genuine fixpoints›
lemma adm_wf_unique_fixpoint:
fixes r :: "('a * 'a) set" and
H :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" and
f :: "'a ⇒ 'b" and g :: "'a ⇒ 'b"
assumes WF: "wf r" and ADM: "adm_wf r H" and fFP: "f = H f" and gFP: "g = H g"
shows "f = g"
proof-
{fix x
have "f x = g x"
proof(rule wf_induct[of r "(λx. f x = g x)"],
auto simp add: WF)
fix x assume "∀y. (y, x) ∈ r ⟶ f y = g y"
hence "H f x = H g x" using ADM adm_wf_def[of r H] by auto
thus "f x = g x" using fFP and gFP by simp
qed
}
thus ?thesis by (simp add: ext)
qed
lemma wfrec_unique_fixpoint:
fixes r :: "('a * 'a) set" and
H :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" and
f :: "'a ⇒ 'b"
assumes WF: "wf r" and ADM: "adm_wf r H" and
fp: "f = H f"
shows "f = wfrec r H"
proof-
have "H (wfrec r H) = wfrec r H"
using assms wfrec_fixpoint[of r H] by simp
thus ?thesis
using assms adm_wf_unique_fixpoint[of r H "wfrec r H"] by simp
qed
end