# Theory WF

Up to index of Isabelle/ZF

theory WF
imports Trancl
begin

    (*  Title:      ZF/WF.thy
        ID:         $Id: WF.thy,v 1.25 2005/06/17 14:15:09 haftmann Exp $
        Author:     Tobias Nipkow and Lawrence C Paulson
        Copyright   1994  University of Cambridge

    Derived first for transitive relations, and finally for arbitrary WF relations
    via wf_trancl and trans_trancl.

    It is difficult to derive this general case directly, using r^+ instead of
    r.  In is_recfun, the two occurrences of the relation must have the same
    form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
    r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
    principle, but harder to use, especially to prove wfrec_eclose_eq in
    epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
    a mess.
    *)

    header{*Well-Founded Recursion*}

    theory WF imports Trancl begin

    constdefs
      wf           :: "i=>o"
        (*r is a well-founded relation*)
        "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"

      wf_on        :: "[i,i]=>o"                      ("wf[_]'(_')")
        (*r is well-founded on A*)
        "wf_on(A,r) == wf(r Int A*A)"

      is_recfun    :: "[i, i, [i,i]=>i, i] =>o"
        "is_recfun(r,a,H,f) == (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"

      the_recfun   :: "[i, i, [i,i]=>i] =>i"
        "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))"

      wftrec :: "[i, i, [i,i]=>i] =>i"
        "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"

      wfrec :: "[i, i, [i,i]=>i] =>i"
        (*public version.  Does not require r to be transitive*)
        "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"

      wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"       ("wfrec[_]'(_,_,_')")
        "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)"

    subsection{*Well-Founded Relations*}

    subsubsection{*Equivalences between @{term wf} and @{term wf_on}*}

    lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
    by (unfold wf_def wf_on_def, force)

    lemma wf_on_imp_wf: "[|wf[A](r); r <= A*A|] ==> wf(r)";
    by (simp add: wf_on_def subset_Int_iff)

    lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
    by (unfold wf_def wf_on_def, fast)

    lemma wf_iff_wf_on_field: "wf(r) <-> wf[field(r)](r)"
    by (blast intro: wf_imp_wf_on wf_on_field_imp_wf)

    lemma wf_on_subset_A: "[| wf[A](r);  B<=A |] ==> wf[B](r)"
    by (unfold wf_on_def wf_def, fast)

    lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)"
    by (unfold wf_on_def wf_def, fast)

    lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)"
    by (simp add: wf_def, fast)

    subsubsection{*Introduction Rules for @{term wf_on}*}

    text{*If every non-empty subset of @{term A} has an @{term r}-minimal element
       then we have @{term "wf[A](r)"}.*}
    lemma wf_onI:
     assumes prem: "!!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False"
     shows         "wf[A](r)"
    apply (unfold wf_on_def wf_def)
    apply (rule equals0I [THEN disjCI, THEN allI])
    apply (rule_tac Z = Z in prem, blast+)
    done

    text{*If @{term r} allows well-founded induction over @{term A}
       then we have @{term "wf[A](r)"}.   Premise is equivalent to
      @{term "!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B"} *}
    lemma wf_onI2:
     assumes prem: "!!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A |]
                           ==> y:B"
     shows         "wf[A](r)"
    apply (rule wf_onI)
    apply (rule_tac c=u in prem [THEN DiffE])
      prefer 3 apply blast
     apply fast+
    done

    subsubsection{*Well-founded Induction*}

    text{*Consider the least @{term z} in @{term "domain(r)"} such that
      @{term "P(z)"} does not hold...*}
    lemma wf_induct [induct set: wf]:
        "[| wf(r);
            !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) |]
         ==> P(a)"
    apply (unfold wf_def)
    apply (erule_tac x = "{z : domain(r). ~ P(z)}" in allE)
    apply blast
    done

    lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf]

    text{*The form of this rule is designed to match @{text wfI}*}
    lemma wf_induct2:
        "[| wf(r);  a:A;  field(r)<=A;
            !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) |]
         ==>  P(a)"
    apply (erule_tac P="a:A" in rev_mp)
    apply (erule_tac a=a in wf_induct, blast)
    done

    lemma field_Int_square: "field(r Int A*A) <= A"
    by blast

    lemma wf_on_induct [consumes 2, induct set: wf_on]:
        "[| wf[A](r);  a:A;
            !!x.[| x: A;  ALL y:A. <y,x>: r --> P(y) |] ==> P(x)
         |]  ==>  P(a)"
    apply (unfold wf_on_def)
    apply (erule wf_induct2, assumption)
    apply (rule field_Int_square, blast)
    done

    lemmas wf_on_induct_rule =
      wf_on_induct [rule_format, consumes 2, induct set: wf_on]

    text{*If @{term r} allows well-founded induction
       then we have @{term "wf(r)"}.*}
    lemma wfI:
        "[| field(r)<=A;
            !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;  y:A|]
                   ==> y:B |]
         ==>  wf(r)"
    apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf])
    apply (rule wf_onI2)
     prefer 2 apply blast
    apply blast
    done

    subsection{*Basic Properties of Well-Founded Relations*}

    lemma wf_not_refl: "wf(r) ==> <a,a> ~: r"
    by (erule_tac a=a in wf_induct, blast)

    lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. <a,x>:r --> <x,a> ~: r"
    by (erule_tac a=a in wf_induct, blast)

    (* [| wf(r);  <a,x> : r;  ~P ==> <x,a> : r |] ==> P *)
    lemmas wf_asym = wf_not_sym [THEN swap, standard]

    lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r"
    by (erule_tac a=a in wf_on_induct, assumption, blast)

    lemma wf_on_not_sym [rule_format]:
         "[| wf[A](r);  a:A |] ==> ALL b:A. <a,b>:r --> <b,a>~:r"
    apply (erule_tac a=a in wf_on_induct, assumption, blast)
    done

    lemma wf_on_asym:
         "[| wf[A](r);  ~Z ==> <a,b> : r;
             <b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z"
    by (blast dest: wf_on_not_sym)

    (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
      wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
    lemma wf_on_chain3:
         "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P"
    apply (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P",
           blast)
    apply (erule_tac a=a in wf_on_induct, assumption, blast)
    done

    text{*transitive closure of a WF relation is WF provided
      @{term A} is downward closed*}
    lemma wf_on_trancl:
        "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
    apply (rule wf_onI2)
    apply (frule bspec [THEN mp], assumption+)
    apply (erule_tac a = y in wf_on_induct, assumption)
    apply (blast elim: tranclE, blast)
    done

    lemma wf_trancl: "wf(r) ==> wf(r^+)"
    apply (simp add: wf_iff_wf_on_field)
    apply (rule wf_on_subset_A)
     apply (erule wf_on_trancl)
     apply blast
    apply (rule trancl_type [THEN field_rel_subset])
    done

    text{*@{term "r-``{a}"} is the set of everything under @{term a} in @{term r}*}

    lemmas underI = vimage_singleton_iff [THEN iffD2, standard]
    lemmas underD = vimage_singleton_iff [THEN iffD1, standard]

    subsection{*The Predicate @{term is_recfun}*}

    lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)"
    apply (unfold is_recfun_def)
    apply (erule ssubst)
    apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
    done

    lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function]

    lemma apply_recfun:
        "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
    apply (unfold is_recfun_def)
      txt{*replace f only on the left-hand side*}
    apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
    apply (simp add: underI)
    done

    lemma is_recfun_equal [rule_format]:
         "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |]
          ==> <x,a>:r --> <x,b>:r --> f`x=g`x"
    apply (frule_tac f = f in is_recfun_type)
    apply (frule_tac f = g in is_recfun_type)
    apply (simp add: is_recfun_def)
    apply (erule_tac a=x in wf_induct)
    apply (intro impI)
    apply (elim ssubst)
    apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
    apply (rule_tac t = "%z. H (?x,z) " in subst_context)
    apply (subgoal_tac "ALL y : r-``{x}. ALL z. <y,z>:f <-> <y,z>:g")
     apply (blast dest: transD)
    apply (simp add: apply_iff)
    apply (blast dest: transD intro: sym)
    done

    lemma is_recfun_cut:
         "[| wf(r);  trans(r);
             is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |]
          ==> restrict(f, r-``{b}) = g"
    apply (frule_tac f = f in is_recfun_type)
    apply (rule fun_extension)
      apply (blast dest: transD intro: restrict_type2)
     apply (erule is_recfun_type, simp)
    apply (blast dest: transD intro: is_recfun_equal)
    done

    subsection{*Recursion: Main Existence Lemma*}

    lemma is_recfun_functional:
         "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g"
    by (blast intro: fun_extension is_recfun_type is_recfun_equal)

    lemma the_recfun_eq:
        "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |] ==> the_recfun(r,a,H) = f"
    apply (unfold the_recfun_def)
    apply (blast intro: is_recfun_functional)
    done

    (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
    lemma is_the_recfun:
        "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]
         ==> is_recfun(r, a, H, the_recfun(r,a,H))"
    by (simp add: the_recfun_eq)

    lemma unfold_the_recfun:
         "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"
    apply (rule_tac a=a in wf_induct, assumption)
    apply (rename_tac a1)
    apply (rule_tac f = "lam y: r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
      apply typecheck
    apply (unfold is_recfun_def wftrec_def)
      --{*Applying the substitution: must keep the quantified assumption!*}
    apply (rule lam_cong [OF refl])
    apply (drule underD)
    apply (fold is_recfun_def)
    apply (rule_tac t = "%z. H(?x,z)" in subst_context)
    apply (rule fun_extension)
      apply (blast intro: is_recfun_type)
     apply (rule lam_type [THEN restrict_type2])
      apply blast
     apply (blast dest: transD)
    apply (frule spec [THEN mp], assumption)
    apply (subgoal_tac "<xa,a1> : r")
     apply (drule_tac x1 = xa in spec [THEN mp], assumption)
    apply (simp add: vimage_singleton_iff
                     apply_recfun is_recfun_cut)
    apply (blast dest: transD)
    done

    subsection{*Unfolding @{term "wftrec(r,a,H)"}*}

    lemma the_recfun_cut:
         "[| wf(r);  trans(r);  <b,a>:r |]
          ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
    by (blast intro: is_recfun_cut unfold_the_recfun)

    (*NOT SUITABLE FOR REWRITING: it is recursive!*)
    lemma wftrec:
        "[| wf(r);  trans(r) |] ==>
              wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))"
    apply (unfold wftrec_def)
    apply (subst unfold_the_recfun [unfolded is_recfun_def])
    apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
    done

    subsubsection{*Removal of the Premise @{term "trans(r)"}*}

    (*NOT SUITABLE FOR REWRITING: it is recursive!*)
    lemma wfrec:
        "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))"
    apply (unfold wfrec_def)
    apply (erule wf_trancl [THEN wftrec, THEN ssubst])
     apply (rule trans_trancl)
    apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context])
     apply (erule r_into_trancl)
    apply (rule subset_refl)
    done

    (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
    lemma def_wfrec:
        "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==>
         h(a) = H(a, lam x: r-``{a}. h(x))"
    apply simp
    apply (elim wfrec)
    done

    lemma wfrec_type:
        "[| wf(r);  a:A;  field(r)<=A;
            !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)
         |] ==> wfrec(r,a,H) : B(a)"
    apply (rule_tac a = a in wf_induct2, assumption+)
    apply (subst wfrec, assumption)
    apply (simp add: lam_type underD)
    done

    lemma wfrec_on:
     "[| wf[A](r);  a: A |] ==>
             wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))"
    apply (unfold wf_on_def wfrec_on_def)
    apply (erule wfrec [THEN trans])
    apply (simp add: vimage_Int_square cons_subset_iff)
    done

    text{*Minimal-element characterization of well-foundedness*}
    lemma wf_eq_minimal:
         "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q))"
    by (unfold wf_def, blast)

    ML
    {*
    val wf_def = thm "wf_def";
    val wf_on_def = thm "wf_on_def";

    val wf_imp_wf_on = thm "wf_imp_wf_on";
    val wf_on_field_imp_wf = thm "wf_on_field_imp_wf";
    val wf_iff_wf_on_field = thm "wf_iff_wf_on_field";
    val wf_on_subset_A = thm "wf_on_subset_A";
    val wf_on_subset_r = thm "wf_on_subset_r";
    val wf_onI = thm "wf_onI";
    val wf_onI2 = thm "wf_onI2";
    val wf_induct = thm "wf_induct";
    val wf_induct2 = thm "wf_induct2";
    val field_Int_square = thm "field_Int_square";
    val wf_on_induct = thm "wf_on_induct";
    val wfI = thm "wfI";
    val wf_not_refl = thm "wf_not_refl";
    val wf_not_sym = thm "wf_not_sym";
    val wf_asym = thm "wf_asym";
    val wf_on_not_refl = thm "wf_on_not_refl";
    val wf_on_not_sym = thm "wf_on_not_sym";
    val wf_on_asym = thm "wf_on_asym";
    val wf_on_chain3 = thm "wf_on_chain3";
    val wf_on_trancl = thm "wf_on_trancl";
    val wf_trancl = thm "wf_trancl";
    val underI = thm "underI";
    val underD = thm "underD";
    val is_recfun_type = thm "is_recfun_type";
    val apply_recfun = thm "apply_recfun";
    val is_recfun_equal = thm "is_recfun_equal";
    val is_recfun_cut = thm "is_recfun_cut";
    val is_recfun_functional = thm "is_recfun_functional";
    val is_the_recfun = thm "is_the_recfun";
    val unfold_the_recfun = thm "unfold_the_recfun";
    val the_recfun_cut = thm "the_recfun_cut";
    val wftrec = thm "wftrec";
    val wfrec = thm "wfrec";
    val def_wfrec = thm "def_wfrec";
    val wfrec_type = thm "wfrec_type";
    val wfrec_on = thm "wfrec_on";
    val wf_eq_minimal = thm "wf_eq_minimal";
    *}

    end

### Well-Founded Relations

#### Equivalences between @{term wf} and @{term wf_on}

lemma wf_imp_wf_on:

      wf(r) ==> wf[A](r)

lemma wf_on_imp_wf:

      [| wf[A](r); r ⊆ A × A |] ==> wf(r)

lemma wf_on_field_imp_wf:

      wf[field(r)](r) ==> wf(r)

lemma wf_iff_wf_on_field:

      wf(r) <-> wf[field(r)](r)

lemma wf_on_subset_A:

      [| wf[A](r); B ⊆ A |] ==> wf[B](r)

lemma wf_on_subset_r:

      [| wf[A](r); s ⊆ r |] ==> wf[A](s)

lemma wf_subset:

      [| wf(s); r ⊆ s |] ==> wf(r)

#### Introduction Rules for @{term wf_on}

lemma wf_onI:

      (!!Z u. [| Z ⊆ A; u ∈ Z; ∀x∈Z. ∃y∈Z. ⟨y, x⟩ ∈ r |] ==> False) ==> wf[A](r)

lemma wf_onI2:

      (!!y B. [| ∀x∈A. (∀y∈A. ⟨y, x⟩ ∈ r --> y ∈ B) --> x ∈ B; y ∈ A |] ==> y ∈ B)
      ==> wf[A](r)

#### Well-founded Induction

lemma wf_induct:

      [| wf(r); !!x. ∀y. ⟨y, x⟩ ∈ r --> P(y) ==> P(x) |] ==> P(a)

lemmas wf_induct_rule:

      [| wf(r); !!x. (!!y. ⟨y, x⟩ ∈ r ==> P(y)) ==> P(x) |] ==> P(a)

lemmas wf_induct_rule:

      [| wf(r); !!x. (!!y. ⟨y, x⟩ ∈ r ==> P(y)) ==> P(x) |] ==> P(a)

lemma wf_induct2:

      [| wf(r); a ∈ A; field(r) ⊆ A;
         !!x. [| x ∈ A; ∀y. ⟨y, x⟩ ∈ r --> P(y) |] ==> P(x) |]
      ==> P(a)

lemma field_Int_square:

      field(r ∩ A × A) ⊆ A

lemma wf_on_induct:

      [| wf[A](r); a ∈ A; !!x. [| x ∈ A; ∀y∈A. ⟨y, x⟩ ∈ r --> P(y) |] ==> P(x) |]
      ==> P(a)

lemmas wf_on_induct_rule:

      [| wf[A](r); a ∈ A;
         !!x. [| x ∈ A; !!y. [| y ∈ A; ⟨y, x⟩ ∈ r |] ==> P(y) |] ==> P(x) |]
      ==> P(a)

lemmas wf_on_induct_rule:

      [| wf[A](r); a ∈ A;
         !!x. [| x ∈ A; !!y. [| y ∈ A; ⟨y, x⟩ ∈ r |] ==> P(y) |] ==> P(x) |]
      ==> P(a)

lemma wfI:

      [| field(r) ⊆ A;
         !!y B. [| ∀x∈A. (∀y∈A. ⟨y, x⟩ ∈ r --> y ∈ B) --> x ∈ B; y ∈ A |] ==> y ∈ B |]
      ==> wf(r)

### Basic Properties of Well-Founded Relations

lemma wf_not_refl:

      wf(r) ==> ⟨a, a⟩ ∉ r

lemma wf_not_sym:

      [| wf(r); ⟨a, x⟩ ∈ r |] ==> ⟨x, a⟩ ∉ r

lemmas wf_asym:

      [| wf(r); ⟨a, x⟩ ∈ r; ¬ P ==> ⟨x, a⟩ ∈ r |] ==> P

lemmas wf_asym:

      [| wf(r); ⟨a, x⟩ ∈ r; ¬ P ==> ⟨x, a⟩ ∈ r |] ==> P

lemma wf_on_not_refl:

      [| wf[A](r); a ∈ A |] ==> ⟨a, a⟩ ∉ r

lemma wf_on_not_sym:

      [| wf[A](r); a ∈ A; b ∈ A; ⟨a, b⟩ ∈ r |] ==> ⟨b, a⟩ ∉ r

lemma wf_on_asym:

      [| wf[A](r); ¬ Z ==> ⟨a, b⟩ ∈ r; ⟨b, a⟩ ∉ r ==> Z; ¬ Z ==> a ∈ A;
         ¬ Z ==> b ∈ A |]
      ==> Z

lemma wf_on_chain3:

      [| wf[A](r); ⟨a, b⟩ ∈ r; ⟨b, c⟩ ∈ r; ⟨c, a⟩ ∈ r; a ∈ A; b ∈ A; c ∈ A |] ==> P

lemma wf_on_trancl:

      [| wf[A](r); r -`` A ⊆ A |] ==> wf[A](r^+)

lemma wf_trancl:

      wf(r) ==> wf(r^+)

lemmas underI:

      ⟨a, b⟩ ∈ r ==> a ∈ r -`` {b}

lemmas underI:

      ⟨a, b⟩ ∈ r ==> a ∈ r -`` {b}

lemmas underD:

      a ∈ r -`` {b} ==> ⟨a, b⟩ ∈ r

lemmas underD:

      a ∈ r -`` {b} ==> ⟨a, b⟩ ∈ r

### The Predicate @{term is_recfun}

lemma is_recfun_type:

      is_recfun(r, a, H, f) ==> f ∈ r -`` {a} -> range(f)

lemmas is_recfun_imp_function:

      is_recfun(r1, a1, H1, f) ==> function(f)

lemmas is_recfun_imp_function:

      is_recfun(r1, a1, H1, f) ==> function(f)

lemma apply_recfun:

      [| is_recfun(r, a, H, f); ⟨x, a⟩ ∈ r |] ==> f ` x = H(x, restrict(f, r -`` {x}))

lemma is_recfun_equal:

      [| wf(r); trans(r); is_recfun(r, a, H, f); is_recfun(r, b, H, g); ⟨x, a⟩ ∈ r;
         ⟨x, b⟩ ∈ r |]
      ==> f ` x = g ` x

lemma is_recfun_cut:

      [| wf(r); trans(r); is_recfun(r, a, H, f); is_recfun(r, b, H, g); ⟨b, a⟩ ∈ r |]
      ==> restrict(f, r -`` {b}) = g

### Recursion: Main Existence Lemma

lemma is_recfun_functional:

      [| wf(r); trans(r); is_recfun(r, a, H, f); is_recfun(r, a, H, g) |] ==> f = g

lemma the_recfun_eq:

      [| is_recfun(r, a, H, f); wf(r); trans(r) |] ==> the_recfun(r, a, H) = f

lemma is_the_recfun:

      [| is_recfun(r, a, H, f); wf(r); trans(r) |]
      ==> is_recfun(r, a, H, the_recfun(r, a, H))

lemma unfold_the_recfun:

      [| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r, a, H))

### Unfolding @{term "wftrec(r,a,H)"}

lemma the_recfun_cut:

      [| wf(r); trans(r); ⟨b, a⟩ ∈ r |]
      ==> restrict(the_recfun(r, a, H), r -`` {b}) = the_recfun(r, b, H)

lemma wftrec:

      [| wf(r); trans(r) |] ==> wftrec(r, a, H) = H(a, λx∈r -`` {a}. wftrec(r, x, H))

#### Removal of the Premise @{term "trans(r)"}

lemma wfrec:

      wf(r) ==> wfrec(r, a, H) = H(a, λx∈r -`` {a}. wfrec(r, x, H))

lemma def_wfrec:

      [| !!x. h(x) == wfrec(r, x, H); wf(r) |] ==> h(a) = H(a, λx∈r -`` {a}. h(x))

lemma wfrec_type:

      [| wf(r); a ∈ A; field(r) ⊆ A;
         !!x u. [| x ∈ A; u ∈ Pi(r -`` {x}, B) |] ==> H(x, u) ∈ B(x) |]
      ==> wfrec(r, a, H) ∈ B(a)

lemma wfrec_on:

      [| wf[A](r); a ∈ A |]
      ==> wfrec[A](r,a,H) = H(a, λx∈r -`` {a} ∩ A. wfrec[A](r,x,H))

lemma wf_eq_minimal:

      wf(r) <-> (∀Q x. x ∈ Q --> (∃z∈Q. ∀y. ⟨y, z⟩ ∈ r --> y ∉ Q))