# Theory HOL-Cardinals.Wellfounded_More

```(*  Title:      HOL/Cardinals/Wellfounded_More.thy
Author:     Andrei Popescu, TU Muenchen

More on well-founded relations.
*)

section ‹More on Well-Founded Relations›

theory Wellfounded_More
imports Main Order_Relation_More
begin

subsection ‹Well-founded recursion via genuine fixpoints›

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)"],
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

(*2*)lemma wfrec_unique_fixpoint:
fixes r :: "('a * 'a) set" and
H :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" and
f :: "'a ⇒ 'b"
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
```