Theory Wfrec

```(*  Title:      HOL/Wfrec.thy
Author:     Tobias Nipkow
Author:     Lawrence C Paulson
*)

section ‹Well-Founded Recursion Combinator›

theory Wfrec
imports Wellfounded
begin

inductive wfrec_rel :: "('a × 'a) set ⇒ (('a ⇒ 'b) ⇒ ('a ⇒ 'b)) ⇒ 'a ⇒ 'b ⇒ bool" for R F
where wfrecI: "(⋀z. (z, x) ∈ R ⟹ wfrec_rel R F z (g z)) ⟹ wfrec_rel R F x (F g x)"

definition cut :: "('a ⇒ 'b) ⇒ ('a × 'a) set ⇒ 'a ⇒ 'a ⇒ 'b"
where "cut f R x = (λy. if (y, x) ∈ R then f y else undefined)"

definition adm_wf :: "('a × 'a) set ⇒ (('a ⇒ 'b) ⇒ ('a ⇒ 'b)) ⇒ bool"
where "adm_wf R F ⟷ (∀f g x. (∀z. (z, x) ∈ R ⟶ f z = g z) ⟶ F f x = F g x)"

definition wfrec :: "('a × 'a) set ⇒ (('a ⇒ 'b) ⇒ ('a ⇒ 'b)) ⇒ ('a ⇒ 'b)"
where "wfrec R F = (λx. THE y. wfrec_rel R (λf x. F (cut f R x) x) x y)"

lemma cuts_eq: "(cut f R x = cut g R x) ⟷ (∀y. (y, x) ∈ R ⟶ f y = g y)"

lemma cut_apply: "(x, a) ∈ R ⟹ cut f R a x = f x"

text ‹
Inductive characterization of ‹wfrec› combinator; for details see:
John Harrison, "Inductive definitions: automation and application".
›

lemma theI_unique: "∃!x. P x ⟹ P x ⟷ x = The P"
by (auto intro: the_equality[symmetric] theI)

lemma wfrec_unique:
assumes "adm_wf R F" "wf R"
shows "∃!y. wfrec_rel R F x y"
using ‹wf R›
proof induct
define f where "f y = (THE z. wfrec_rel R F y z)" for y
case (less x)
then have "⋀y z. (y, x) ∈ R ⟹ wfrec_rel R F y z ⟷ z = f y"
unfolding f_def by (rule theI_unique)
with ‹adm_wf R F› show ?case
by (subst wfrec_rel.simps) (auto simp: adm_wf_def)
qed

lemma adm_lemma: "adm_wf R (λf x. F (cut f R x) x)"
by (auto simp: adm_wf_def intro!: arg_cong[where f="λx. F x y" for y] cuts_eq[THEN iffD2])

lemma wfrec: "wf R ⟹ wfrec R F a = F (cut (wfrec R F) R a) a"
apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality])
apply assumption
apply (rule wfrec_rel.wfrecI)
apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
done

text ‹This form avoids giant explosions in proofs.  NOTE USE OF ‹≡›.›
lemma def_wfrec: "f ≡ wfrec R F ⟹ wf R ⟹ f a = F (cut f R a) a"
by (auto intro: wfrec)

subsubsection ‹Well-founded recursion via genuine fixpoints›

lemma wfrec_fixpoint:
assumes wf: "wf R"
shows "wfrec R F = F (wfrec R F)"
proof (rule ext)
fix x
have "wfrec R F x = F (cut (wfrec R F) R x) x"
using wfrec[of R F] wf by simp
also
have "⋀y. (y, x) ∈ R ⟹ cut (wfrec R F) R x y = wfrec R F y"
then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
finally show "wfrec R F x = F (wfrec R F) x" .
qed

lemma wfrec_def_adm: "f ≡ wfrec R F ⟹ wf R ⟹ adm_wf R F ⟹ f = F f"
using wfrec_fixpoint by simp

subsection ‹Wellfoundedness of ‹same_fst››

definition same_fst :: "('a ⇒ bool) ⇒ ('a ⇒ ('b × 'b) set) ⇒ (('a × 'b) × ('a × 'b)) set"
where "same_fst P R = {((x', y'), (x, y)) . x' = x ∧ P x ∧ (y',y) ∈ R x}"
― ‹For \<^const>‹wfrec› declarations where the first n parameters
stay unchanged in the recursive call.›

lemma same_fstI [intro!]: "P x ⟹ (y', y) ∈ R x ⟹ ((x, y'), (x, y)) ∈ same_fst P R"

lemma wf_same_fst:
assumes "⋀x. P x ⟹ wf (R x)"
shows "wf (same_fst P R)"
proof -
have "⋀a b Q. ∀a b. (∀x. P a ∧ (x, b) ∈ R a ⟶ Q (a, x)) ⟶ Q (a, b) ⟹ Q (a, b)"
proof -
fix Q a b
assume *: "∀a b. (∀x. P a ∧ (x,b) ∈ R a ⟶ Q (a,x)) ⟶ Q (a,b)"
show "Q(a,b)"
proof (cases "wf (R a)")
case True
then show ?thesis
by (induction b rule: wf_induct_rule) (use * in blast)
qed (use * assms in blast)
qed
then show ?thesis
by (clarsimp simp add: wf_def same_fst_def)
qed

end
```