Theory HOL.Wfrec

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

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)"
  by (simp add: fun_eq_iff cut_def)

lemma cut_apply: "(x, a)  R  cut f R a x = f x"
  by (simp add: cut_def)

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 (simp add: wfrec_def)
  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"
    and adm: "adm_wf R F"
  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"
    by (auto simp add: cut_apply)
  then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
    using adm adm_wf_def[of R F] by auto
  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 constwfrec 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"
  by (simp add: same_fst_def)

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