Theory recursion

(*  Title:       Recursion theorem
    Author:      Georgy Dunaev <georgedunaev at gmail.com>, 2020
    Maintainer:  Georgy Dunaev <georgedunaev at gmail.com>
*)
section "Recursion Submission"

text ‹Recursion Theorem is proved in the following document.
It also contains the addition on natural numbers.
The development is done in the context of Zermelo-Fraenkel set theory.›

theory recursion
  imports ZF
begin

section ‹Basic Set Theory›
text ‹Useful lemmas about sets, functions and natural numbers›
lemma pisubsig : ‹Pi(A,P)⊆Pow(Sigma(A,P))›
proof
  fix x
  assume ‹x ∈ Pi(A,P)›
  hence ‹x ∈ {f∈Pow(Sigma(A,P)). A⊆domain(f) & function(f)}›
    by (unfold Pi_def)
  thus ‹x ∈ Pow(Sigma(A, P))›
    by (rule CollectD1)
qed

lemma apparg:
  fixes f A B
  assumes T0:‹f:A→B›
  assumes T1:‹f ` a = b›
  assumes T2:‹a ∈ A›
  shows ‹⟨a, b⟩ ∈ f›
proof(rule iffD2[OF func.apply_iff], rule T0)
  show T:‹a ∈ A ∧ f ` a = b›
    by (rule conjI[OF T2 T1])
qed

theorem nat_induct_bound :
  assumes H0:‹P(0)›
  assumes H1:‹!!x. x∈nat ⟹ P(x) ⟹ P(succ(x))›
  shows ‹∀n∈nat. P(n)›
proof(rule ballI)
  fix n
  assume H2:‹n∈nat›
  show ‹P(n)›
  proof(rule nat_induct[of n])
    from H2 show ‹n∈nat› by assumption
  next
    show ‹P(0)› by (rule H0)
  next
    fix x
    assume H3:‹x∈nat›
    assume H4:‹P(x)›
    show ‹P(succ(x))› by (rule H1[OF H3 H4])
  qed
qed

theorem nat_Tr : ‹∀n∈nat. m∈n ⟶ m∈nat›
proof(rule nat_induct_bound)
  show ‹m ∈ 0 ⟶ m ∈ nat› by auto
next
  fix x
  assume H0:‹x ∈ nat›
  assume H1:‹m ∈ x ⟶ m ∈ nat›
  show ‹m ∈ succ(x) ⟶ m ∈ nat›
  proof(rule impI)
    assume H2:‹m∈succ(x)›
    show ‹m ∈ nat›
    proof(rule succE[OF H2])
      assume H3:‹m = x›
      from H0 and H3 show ‹m ∈ nat›
        by auto
    next
      assume H4:‹m ∈ x›
      show ‹m ∈ nat›
        by(rule mp[OF H1 H4])
    qed
  qed
qed

(* Natural numbers are linearly ordered. *)
theorem zeroleq : ‹∀n∈nat. 0∈n ∨ 0=n›
proof(rule ballI)
  fix n
  assume H1:‹n∈nat›
  show ‹0∈n∨0=n›
  proof(rule nat_induct[of n])
    from H1 show ‹n ∈ nat› by assumption
  next
    show ‹0 ∈ 0 ∨ 0 = 0› by (rule disjI2, rule refl)
  next
    fix x
    assume H2:‹x∈nat›
    assume H3:‹ 0 ∈ x ∨ 0 = x›
    show ‹0 ∈ succ(x) ∨ 0 = succ(x)›
    proof(rule disjE[OF H3])
      assume H4:‹0∈x›
      show ‹0 ∈ succ(x) ∨ 0 = succ(x)›
      proof(rule disjI1)
        show ‹0 ∈ succ(x)›
          by (rule succI2[OF H4])
      qed
    next
      assume H4:‹0=x›
      show ‹0 ∈ succ(x) ∨ 0 = succ(x)›
      proof(rule disjI1)
        have q:‹x ∈ succ(x)› by auto
        from q and H4 show ‹0 ∈ succ(x)› by auto
      qed
    qed
  qed
qed

theorem JH2_1ii : ‹m∈succ(n) ⟹ m∈n∨m=n›
  by auto

theorem nat_transitive:‹∀n∈nat. ∀k. ∀m.  k ∈ m ∧ m ∈ n ⟶ k ∈ n›
proof(rule nat_induct_bound)
  show ‹∀k. ∀m. k ∈ m ∧ m ∈ 0 ⟶ k ∈ 0›
  proof(rule allI, rule allI, rule impI)
    fix k m
    assume H:‹k ∈ m ∧ m ∈ 0›
    then have H:‹m ∈ 0› by auto
    then show ‹k ∈ 0› by auto
  qed
next
  fix n
  assume H0:‹n ∈ nat›
  assume H1:‹∀k.
            ∀m.
               k ∈ m ∧ m ∈ n ⟶
               k ∈ n›
  show ‹∀k. ∀m.
               k ∈ m ∧
               m ∈ succ(n) ⟶
               k ∈ succ(n)›
  proof(rule allI, rule allI, rule impI)
    fix k m
    assume H4:‹k ∈ m ∧ m ∈ succ(n)›
    hence H4':‹m ∈ succ(n)› by (rule conjunct2)
    hence H4'':‹m∈n ∨ m=n› by (rule succE, auto)
    from H4 have Q:‹k ∈ m› by (rule conjunct1)
    have H1S:‹∀m. k ∈ m ∧ m ∈ n ⟶ k ∈ n›
      by (rule spec[OF H1])
    have H1S:‹k ∈ m ∧ m ∈ n ⟶ k ∈ n›
      by (rule spec[OF H1S])
    show ‹k ∈ succ(n)›
    proof(rule disjE[OF H4''])
      assume L:‹m∈n›
      from Q and L have QL:‹k ∈ m ∧ m ∈ n› by auto
      have G:‹k ∈ n› by (rule mp [OF H1S QL])
      show ‹k ∈ succ(n)›
        by (rule succI2[OF G])
    next
      assume L:‹m=n›
      from Q have F:‹k ∈ succ(m)› by auto
      from L and Q show ‹k ∈ succ(n)› by auto
    qed
  qed
qed

theorem nat_xninx : ‹∀n∈nat. ¬(n∈n)›
proof(rule nat_induct_bound)
  show ‹0∉0›
    by auto
next
  fix x
  assume H0:‹x∈nat›
  assume H1:‹x∉x›
  show ‹succ(x) ∉ succ(x)›
  proof(rule contrapos[OF H1])
    assume Q:‹succ(x) ∈ succ(x)›
    have D:‹succ(x)∈x ∨ succ(x)=x›
      by (rule JH2_1ii[OF Q])
    show ‹x∈x›
    proof(rule disjE[OF D])
      assume Y1:‹succ(x)∈x›
      have U:‹x∈succ(x)› by (rule succI1)
      have T:‹x ∈ succ(x) ∧ succ(x) ∈ x ⟶ x ∈ x›
        by (rule spec[OF spec[OF bspec[OF nat_transitive H0]]])
      have R:‹x ∈ succ(x) ∧ succ(x) ∈ x›
        by (rule conjI[OF U Y1])
      show ‹x∈x›
        by (rule mp[OF T R])
    next
      assume Y1:‹succ(x)=x›
      show ‹x∈x›
        by (rule subst[OF Y1], rule Q)
    qed
  qed
qed

theorem nat_asym : ‹∀n∈nat. ∀m. ¬(n∈m ∧ m∈n)›
proof(rule ballI, rule allI)
  fix n m
  assume H0:‹n ∈ nat›
  have Q:‹¬(n∈n)›
    by(rule bspec[OF nat_xninx H0])
  show ‹¬ (n ∈ m ∧ m ∈ n)›
  proof(rule contrapos[OF Q])
    assume W:‹(n ∈ m ∧ m ∈ n)›
    show ‹n∈n›
      by (rule mp[OF spec[OF spec[OF bspec[OF nat_transitive H0]]] W])
  qed
qed

theorem zerolesucc :‹∀n∈nat. 0 ∈ succ(n)›
proof(rule nat_induct_bound)
  show ‹0∈1›
    by auto
next
  fix x
  assume H0:‹x∈nat›
  assume H1:‹0∈succ(x)›
  show ‹0∈succ(succ(x))›
  proof
    assume J:‹0 ∉ succ(x)›
    show ‹0 = succ(x)›
      by(rule notE[OF J H1])
  qed
qed

theorem succ_le : ‹∀n∈nat. succ(m)∈succ(n) ⟶ m∈n›
proof(rule nat_induct_bound)
  show ‹ succ(m) ∈ 1 ⟶ m ∈ 0›
    by blast
next
  fix x
  assume H0:‹x ∈ nat›
  assume H1:‹succ(m) ∈ succ(x) ⟶ m ∈ x›
  show ‹ succ(m) ∈
             succ(succ(x)) ⟶
             m ∈ succ(x)›
  proof(rule impI)
    assume J0:‹succ(m) ∈ succ(succ(x))›
    show ‹m ∈ succ(x)›
    proof(rule succE[OF J0])
      assume R:‹succ(m) = succ(x)›
      hence R:‹m=x› by (rule upair.succ_inject)
      from R and succI1 show ‹m ∈ succ(x)› by auto
    next
      assume R:‹succ(m) ∈ succ(x)›
      have R:‹m∈x› by (rule mp[OF H1 R])
      then show ‹m ∈ succ(x)› by auto
    qed
  qed
qed

theorem succ_le2 : ‹∀n∈nat. ∀m. succ(m)∈succ(n) ⟶ m∈n›
proof
  fix n
  assume H:‹n∈nat›
  show ‹∀m. succ(m) ∈ succ(n) ⟶ m ∈ n›
  proof
    fix m
    from succ_le and H show ‹succ(m) ∈ succ(n) ⟶ m ∈ n› by auto
  qed
qed

theorem le_succ : ‹∀n∈nat. m∈n ⟶ succ(m)∈succ(n)›
proof(rule nat_induct_bound)
  show ‹m ∈ 0 ⟶ succ(m) ∈ 1›
    by auto
next
  fix x
  assume H0:‹x∈nat›
  assume H1:‹m ∈ x ⟶ succ(m) ∈ succ(x)›
  show ‹m ∈ succ(x) ⟶
            succ(m) ∈ succ(succ(x))›
  proof(rule impI)
    assume HR1:‹m∈succ(x)›
    show ‹succ(m) ∈ succ(succ(x))›
    proof(rule succE[OF HR1])
      assume Q:‹m = x›
      from Q show ‹succ(m) ∈ succ(succ(x))›
        by auto
    next
      assume Q:‹m ∈ x›
      have Q:‹succ(m) ∈ succ(x)›
        by (rule mp[OF H1 Q])
      from Q show ‹succ(m) ∈ succ(succ(x))›
        by (rule succI2)
    qed
  qed
qed

theorem nat_linord:‹∀n∈nat. ∀m∈nat. m∈n∨m=n∨n∈m›
proof(rule ballI)
  fix n
  assume H1:‹n∈nat›
  show ‹∀m∈nat. m ∈ n ∨ m = n ∨ n ∈ m›
  proof(rule nat_induct[of n])
    from H1 show ‹n∈nat› by assumption
  next
    show ‹∀m∈nat. m ∈ 0 ∨ m = 0 ∨ 0 ∈ m›
    proof
      fix m
      assume J:‹m∈nat›
      show ‹ m ∈ 0 ∨ m = 0 ∨ 0 ∈ m›
      proof(rule disjI2)
        have Q:‹0∈m∨0=m› by (rule bspec[OF zeroleq J])
        show ‹m = 0 ∨ 0 ∈ m›
          by (rule disjE[OF Q], auto)
      qed
    qed
  next
    fix x
    assume K:‹x∈nat›
    assume M:‹∀m∈nat. m ∈ x ∨ m = x ∨ x ∈ m›
    show ‹∀m∈nat.
            m ∈ succ(x) ∨
            m = succ(x) ∨
            succ(x) ∈ m›
    proof(rule nat_induct_bound)
      show ‹0 ∈ succ(x) ∨  0 = succ(x) ∨ succ(x) ∈ 0›
      proof(rule disjI1)
        show ‹0 ∈ succ(x)›
          by (rule bspec[OF zerolesucc K])
      qed
    next
      fix y
      assume H0:‹y ∈ nat›
      assume H1:‹y ∈ succ(x) ∨ y = succ(x) ∨ succ(x) ∈ y›
      show ‹succ(y) ∈ succ(x) ∨
            succ(y) = succ(x) ∨
            succ(x) ∈ succ(y)›
      proof(rule disjE[OF H1])
        assume W:‹y∈succ(x)›
        show ‹succ(y) ∈ succ(x) ∨
              succ(y) = succ(x) ∨
              succ(x) ∈ succ(y)›
        proof(rule succE[OF W])
          assume G:‹y=x›
          show ‹succ(y) ∈ succ(x) ∨
    succ(y) = succ(x) ∨
    succ(x) ∈ succ(y)›
            by (rule disjI2, rule disjI1, rule subst[OF G], rule refl)
        next
          assume G:‹y ∈ x›
          have R:‹succ(y) ∈ succ(x)›
            by (rule mp[OF bspec[OF le_succ K] G])
          show ‹succ(y) ∈ succ(x) ∨
           succ(y) = succ(x) ∨
           succ(x) ∈ succ(y)›
            by(rule disjI1, rule R)
        qed
      next
        assume W:‹y = succ(x) ∨ succ(x) ∈ y›
        show ‹succ(y) ∈ succ(x) ∨
              succ(y) = succ(x) ∨
              succ(x) ∈ succ(y)›
        proof(rule disjE[OF W])
          assume W:‹y=succ(x)›
          show ‹succ(y) ∈ succ(x) ∨
              succ(y) = succ(x) ∨
              succ(x) ∈ succ(y)›
            by (rule disjI2, rule disjI2, rule subst[OF W], rule succI1)
        next
          assume W:‹succ(x)∈y›
          show ‹succ(y) ∈ succ(x) ∨
              succ(y) = succ(x) ∨
              succ(x) ∈ succ(y)›
            by (rule disjI2, rule disjI2, rule succI2[OF W])
        qed
      qed
    qed
  qed
qed

lemma tgb:
  assumes knat: ‹k∈nat›
  assumes D: ‹t ∈ k → A›
  shows  ‹t ∈ Pow(nat × A)›
proof -
  from D
  have q:‹t∈{t∈Pow(Sigma(k,%_.A)). k⊆domain(t) & function(t)}›
    by(unfold Pi_def)
  have J:‹t ∈ Pow(k × A)›
    by (rule CollectD1[OF q])
  have G:‹k × A ⊆ nat × A›
  proof(rule func.Sigma_mono)
    from knat
    show ‹k⊆nat›
      by (rule QUniv.naturals_subset_nat)
  next
    show ‹⋀x. x ∈ k ⟹ A ⊆ A›
      by auto
  qed
  show ‹t ∈ Pow(nat × A)›
    by (rule subsetD, rule func.Pow_mono[OF G], rule J)
qed

section ‹Compatible set›
text ‹Union of compatible set of functions is a function.›

definition compat :: ‹[i,i]⇒o›
  where "compat(f1,f2) == ∀x.∀y1.∀y2.⟨x,y1⟩ ∈ f1 ∧ ⟨x,y2⟩ ∈ f2 ⟶ y1=y2"

lemma compatI [intro]:
  assumes H:‹⋀x y1 y2.⟦⟨x,y1⟩ ∈ f1; ⟨x,y2⟩ ∈ f2⟧⟹y1=y2›
  shows ‹compat(f1,f2)›
proof(unfold compat_def)
  show ‹∀x y1 y2. ⟨x, y1⟩ ∈ f1 ∧ ⟨x, y2⟩ ∈ f2 ⟶ y1 = y2›
  proof(rule allI | rule impI)+
    fix x y1 y2
    assume K:‹⟨x, y1⟩ ∈ f1 ∧ ⟨x, y2⟩ ∈ f2›
    have K1:‹⟨x, y1⟩ ∈ f1› by (rule conjunct1[OF K])
    have K2:‹⟨x, y2⟩ ∈ f2› by (rule conjunct2[OF K])
    show ‹y1 = y2› by (rule H[OF K1 K2])
  qed
qed

lemma compatD:
  assumes H: ‹compat(f1,f2)›
  shows ‹⋀x y1 y2.⟦⟨x,y1⟩ ∈ f1; ⟨x,y2⟩ ∈ f2⟧⟹y1=y2›
proof -
  fix x y1 y2
  assume Q1:‹⟨x, y1⟩ ∈ f1›
  assume Q2:‹⟨x, y2⟩ ∈ f2›
  from H have H:‹∀x y1 y2. ⟨x, y1⟩ ∈ f1 ∧ ⟨x, y2⟩ ∈ f2 ⟶ y1 = y2›
    by (unfold compat_def)
  show ‹y1=y2›
  proof(rule mp[OF spec[OF spec[OF spec[OF H]]]])
    show ‹⟨x, y1⟩ ∈ f1 ∧ ⟨x, y2⟩ ∈ f2›
      by(rule conjI[OF Q1 Q2])
  qed
qed

lemma compatE:
  assumes H: ‹compat(f1,f2)›
  and W:‹(⋀x y1 y2.⟦⟨x,y1⟩ ∈ f1; ⟨x,y2⟩ ∈ f2⟧⟹y1=y2) ⟹ E›
shows ‹E›
  by (rule W, rule compatD[OF H], assumption+)


definition compatset :: ‹i⇒o›
  where "compatset(S) == ∀f1∈S.∀f2∈S. compat(f1,f2)"

lemma compatsetI [intro] :
  assumes 1:‹⋀f1 f2. ⟦f1∈S;f2∈S⟧ ⟹ compat(f1,f2)›
  shows ‹compatset(S)›
  by (unfold compatset_def, rule ballI, rule ballI, rule 1, assumption+)

lemma compatsetD:
  assumes H: ‹compatset(S)›
  shows ‹⋀f1 f2.⟦f1∈S; f2∈S⟧⟹compat(f1,f2)›
proof -
  fix f1 f2
  assume H1:‹f1∈S›
  assume H2:‹f2∈S›
  from H have H:‹∀f1∈S.∀f2∈S. compat(f1,f2)›
    by (unfold compatset_def)
  show ‹compat(f1,f2)›
    by (rule bspec[OF bspec[OF H H1] H2])
qed

lemma compatsetE:
  assumes H: ‹compatset(S)›
  and W:‹(⋀f1 f2.⟦f1∈S; f2∈S⟧⟹compat(f1,f2)) ⟹ E›
shows ‹E›
  by (rule W, rule compatsetD[OF H], assumption+)

theorem upairI1 : ‹a ∈ {a, b}›
proof
  assume ‹a ∉ {b}›
  show ‹a = a› by (rule refl)
qed

theorem upairI2 : ‹b ∈ {a, b}›
proof
  assume H:‹b ∉ {b}›
  have Y:‹b ∈ {b}› by (rule upair.singletonI)
  show ‹b = a› by (rule notE[OF H Y])
qed

theorem sinup : ‹{x} ∈ ⟨x, xa⟩›
proof (unfold Pair_def)
  show ‹{x} ∈ {{x, x}, {x, xa}}›
  proof (rule IFOL.subst)
    show ‹{x} ∈ {{x},{x,xa}}›
      by (rule upairI1)
  next
    show ‹{{x}, {x, xa}} = {{x, x}, {x, xa}}›
      by blast
  qed
qed

theorem compatsetunionfun :
  fixes S
  assumes H0:‹compatset(S)›
  shows ‹function(⋃S)›
proof(unfold function_def)
  show ‹ ∀x y1. ⟨x, y1⟩ ∈ ⋃S ⟶
          (∀y2. ⟨x, y2⟩ ∈ ⋃S ⟶ y1 = y2)›
  proof(rule allI, rule allI, rule impI, rule allI, rule impI)
    fix x y1 y2
    assume F1:‹⟨x, y1⟩ ∈ ⋃S›
    assume F2:‹⟨x, y2⟩ ∈ ⋃S›
    show ‹y1=y2›
    proof(rule UnionE[OF F1], rule UnionE[OF F2])
      fix f1 f2
      assume J1:‹⟨x, y1⟩ ∈ f1›
      assume J2:‹⟨x, y2⟩ ∈ f2›
      assume K1:‹f1 ∈ S›
      assume K2:‹f2 ∈ S›
      have R:‹compat(f1,f2)›
        by (rule compatsetD[OF H0 K1 K2])
      show ‹y1=y2›
        by(rule compatD[OF R J1 J2])
    qed
  qed
qed

theorem mkel :
  assumes 1:‹A›
  assumes 2:‹A⟹B›
  shows ‹B›
  by (rule 2, rule 1)

theorem valofunion :
  fixes S
  assumes H0:‹compatset(S)›
  assumes W:‹f∈S›
  assumes Q:‹f:A→B›
  assumes T:‹a∈A›
  assumes P:‹f ` a = v›
  shows N:‹(⋃S)`a = v›
proof -
  have K:‹⟨a, v⟩ ∈ f›
    by (rule apparg[OF Q P T])
  show N:‹(⋃S)`a = v›
  proof(rule function_apply_equality)
    show ‹function(⋃S)›
      by(rule compatsetunionfun[OF H0])
  next
    show ‹⟨a, v⟩ ∈ ⋃S›
      by(rule UnionI[OF W K ])
  qed
qed

section "Partial computation"

definition satpc :: ‹[i,i,i] ⇒ o ›
  where ‹satpc(t,α,g) == ∀n ∈ α . t`succ(n) = g ` <t`n, n>›

text ‹$m$-step computation based on $a$ and $g$›
definition partcomp :: ‹[i,i,i,i,i]⇒o›
  where ‹partcomp(A,t,m,a,g) == (t:succ(m)→A) ∧ (t`0=a) ∧ satpc(t,m,g)›

lemma partcompI [intro]:
  assumes H1:‹(t:succ(m)→A)›
  assumes H2:‹(t`0=a)›
  assumes H3:‹satpc(t,m,g)›
  shows ‹partcomp(A,t,m,a,g)›
proof (unfold partcomp_def, auto)
  show ‹t ∈ succ(m) → A› by (rule H1)
  show ‹(t`0=a)› by (rule H2)
  show ‹satpc(t,m,g)› by (rule H3)
qed

lemma partcompD1: ‹partcomp(A,t,m,a,g) ⟹ t ∈ succ(m) → A›
  by (unfold partcomp_def, auto)

lemma partcompD2: ‹partcomp(A,t,m,a,g) ⟹ (t`0=a)›
 by (unfold partcomp_def, auto)

lemma partcompD3: ‹partcomp(A,t,m,a,g) ⟹ satpc(t,m,g)›
  by (unfold partcomp_def, auto)

lemma partcompE [elim] :
  assumes 1:‹partcomp(A,t,m,a,g)›
    and 2:‹⟦(t:succ(m)→A) ; (t`0=a) ; satpc(t,m,g)⟧ ⟹ E›
  shows ‹E›
  by (rule 2, rule partcompD1[OF 1], rule partcompD2[OF 1], rule partcompD3[OF 1])

text ‹If we add ordered pair in the middle of partial computation then
it will not change.›
lemma addmiddle:
(*  fixes  t m a g*)
  assumes mnat:‹m∈nat›
  assumes F:‹partcomp(A,t,m,a,g)›
  assumes xinm:‹x∈m›
  shows ‹cons(⟨succ(x), g ` ⟨t ` x, x⟩⟩, t) = t›
proof(rule partcompE[OF F])
  assume F1:‹t ∈ succ(m) → A›
  assume F2:‹t ` 0 = a›
  assume F3:‹satpc(t, m, g)›
  from F3
  have W:‹∀n∈m. t ` succ(n) = g ` ⟨t ` n, n⟩›
    by (unfold satpc_def)
  have U:‹t ` succ(x) = g ` ⟨t ` x, x⟩›
    by (rule bspec[OF W xinm])
  have E:‹⟨succ(x), (g ` ⟨t ` x, x⟩)⟩ ∈ t›
  proof(rule apparg[OF F1 U])
    show ‹succ(x) ∈ succ(m)›
      by(rule mp[OF bspec[OF le_succ mnat] xinm])
  qed
  show ?thesis
    by (rule equalities.cons_absorb[OF E])
qed


section ‹Set of functions ›
text ‹It is denoted as $F$ on page 48 in "Introduction to Set Theory".›
definition pcs :: ‹[i,i,i]⇒i›
  where ‹pcs(A,a,g) == {t∈Pow(nat*A). ∃m∈nat. partcomp(A,t,m,a,g)}›

lemma pcs_uniq :
  assumes F1:‹m1∈nat›
  assumes F2:‹m2∈nat›
  assumes H1: ‹partcomp(A,f1,m1,a,g)›
  assumes H2: ‹partcomp(A,f2,m2,a,g)›
  shows ‹∀n∈nat. n∈succ(m1) ∧ n∈succ(m2) ⟶ f1`n = f2`n›
proof(rule partcompE[OF H1], rule partcompE[OF H2])
  assume H11:‹f1 ∈ succ(m1) → A›
  assume H12:‹f1 ` 0 = a ›
  assume H13:‹satpc(f1, m1, g)›
  assume H21:‹f2 ∈ succ(m2) → A›
  assume H22:‹f2 ` 0 = a›
  assume H23:‹satpc(f2, m2, g)›
  show ‹∀n∈nat. n∈succ(m1) ∧ n∈succ(m2) ⟶ f1`n = f2`n›
proof(rule nat_induct_bound)
  from H12 and H22
  show ‹0∈succ(m1) ∧ 0∈succ(m2) ⟶ f1 ` 0 = f2 ` 0›
    by auto
next
  fix x
  assume J0:‹x∈nat›
  assume J1:‹x ∈ succ(m1) ∧ x ∈ succ(m2) ⟶ f1 ` x = f2 ` x›
  from H13 have G1:‹∀n ∈ m1 . f1`succ(n) = g ` <f1`n, n>›
    by (unfold satpc_def, auto)
  from H23 have G2:‹∀n ∈ m2 . f2`succ(n) = g ` <f2`n, n>›
    by (unfold satpc_def, auto)
  show ‹succ(x) ∈ succ(m1) ∧ succ(x) ∈ succ(m2) ⟶
        f1 ` succ(x) = f2 ` succ(x)›
  proof
    assume K:‹succ(x) ∈ succ(m1) ∧ succ(x) ∈ succ(m2)›
    from K have K1:‹succ(x) ∈ succ(m1)› by auto
    from K have K2:‹succ(x) ∈ succ(m2)› by auto
    have K1':‹x ∈ m1› by (rule mp[OF bspec[OF succ_le F1] K1])
    have K2':‹x ∈ m2› by (rule mp[OF bspec[OF succ_le F2] K2])
    have U1:‹x∈succ(m1)›
      by (rule Nat.succ_in_naturalD[OF K1 Nat.nat_succI[OF F1]])
    have U2:‹x∈succ(m2)›
      by (rule Nat.succ_in_naturalD[OF K2 Nat.nat_succI[OF F2]])
    have Y1:‹f1`succ(x) = g ` <f1`x, x>›
      by (rule bspec[OF G1 K1'])
    have Y2:‹f2`succ(x) = g ` <f2`x, x>›
      by (rule bspec[OF G2 K2'])
    have ‹f1 ` x = f2 ` x›
      by(rule mp[OF J1 conjI[OF U1 U2]])
    then have Y:‹g ` <f1`x, x> = g ` <f2`x, x>› by auto
    from Y1 and Y2 and Y
    show ‹f1 ` succ(x) = f2 ` succ(x)›
      by auto
  qed
qed
qed

lemma domainsubsetfunc :
  assumes Q:‹f1⊆f2›
  shows ‹domain(f1)⊆domain(f2)›
proof
  fix x
  assume H:‹x ∈ domain(f1)›
  show ‹x ∈ domain(f2)›
  proof(rule domainE[OF H])
    fix y
    assume W:‹⟨x, y⟩ ∈ f1›
    have ‹⟨x, y⟩ ∈ f2›
      by(rule subsetD[OF Q W])
    then show ‹x ∈ domain(f2)›
      by(rule domainI)
  qed
qed

lemma natdomfunc:
  assumes 1:‹q∈A›
  assumes J0:‹f1 ∈ Pow(nat × A)›
  assumes U:‹m1 ∈ domain(f1)›
  shows ‹m1∈nat›
proof -
  from J0 have J0 : ‹f1 ⊆ nat × A›
    by auto
  have J0:‹domain(f1) ⊆ domain(nat × A)›
    by(rule func.domain_mono[OF J0])
  have F:‹m1 ∈ domain(nat × A)›
    by(rule subsetD[OF J0 U])
  have R:‹domain(nat × A) = nat›
    by (rule equalities.domain_of_prod[OF 1])
  show ‹m1 ∈ nat›
    by(rule subst[OF R], rule F)
qed

lemma pcs_lem :
  assumes 1:‹q∈A›
  shows ‹compatset(pcs(A, a, g))›
proof (*(rule compatsetI)*)
  fix f1 f2
  assume H1:‹f1 ∈ pcs(A, a, g)›
  then have H1':‹f1 ∈ {t∈Pow(nat*A). ∃m∈nat. partcomp(A,t,m,a,g)}› by (unfold pcs_def)
  hence H1'A:‹f1 ∈ Pow(nat*A)› by auto
  hence H1'A:‹f1 ⊆ (nat*A)› by auto
  assume H2:‹f2 ∈ pcs(A, a, g)›
  then have H2':‹f2 ∈ {t∈Pow(nat*A). ∃m∈nat. partcomp(A,t,m,a,g)}› by (unfold pcs_def)
  show ‹compat(f1, f2)›
  proof(rule compatI)
    fix x y1 y2
    assume P1:‹⟨x, y1⟩ ∈ f1›
    assume P2:‹⟨x, y2⟩ ∈ f2›
    show ‹y1 = y2›
    proof(rule CollectE[OF H1'], rule CollectE[OF H2'])
      assume J0:‹f1 ∈ Pow(nat × A)›
      assume J1:‹f2 ∈ Pow(nat × A)›
      assume J2:‹∃m∈nat. partcomp(A, f1, m, a, g)›
      assume J3:‹∃m∈nat. partcomp(A, f2, m, a, g)›
      show ‹y1 = y2›
      proof(rule bexE[OF J2], rule bexE[OF J3])
        fix m1 m2
        assume K1:‹partcomp(A, f1, m1, a, g)›
        assume K2:‹partcomp(A, f2, m2, a, g)›
        hence K2':‹(f2:succ(m2)→A) ∧ (f2`0=a) ∧ satpc(f2,m2,g)›
          by (unfold partcomp_def)
        from K1 have K1'A:‹(f1:succ(m1)→A)› by (rule partcompD1)
        from K2' have K2'A:‹(f2:succ(m2)→A)› by auto
        from K1'A have K1'AD:‹domain(f1) = succ(m1)›
          by(rule domain_of_fun)
        from K2'A have K2'AD:‹domain(f2) = succ(m2)›
          by(rule domain_of_fun)
        have L1:‹f1`x=y1›
          by (rule func.apply_equality[OF P1], rule K1'A)
        have L2:‹f2`x=y2›
          by(rule func.apply_equality[OF P2], rule K2'A)
        have m1nat:‹m1∈nat›
        proof(rule natdomfunc[OF 1 J0])
          show ‹m1 ∈ domain(f1)›
            by (rule ssubst[OF K1'AD], auto)
        qed
        have m2nat:‹m2∈nat›
        proof(rule natdomfunc[OF 1 J1])
          show ‹m2 ∈ domain(f2)›
            by (rule ssubst[OF K2'AD], auto)
        qed
        have G1:‹⟨x, y1⟩ ∈ (nat*A)›
          by(rule subsetD[OF H1'A P1])
        have KK:‹x∈nat›
          by(rule SigmaE[OF G1], auto)
        (*x is in the domain of f1  i.e. succ(m1)
so we can have both  x ∈ ?m1.2 ∧ x ∈ ?m2.2
how to prove that m1 ∈ nat ? from J0 !  f1 is a subset of nat × A*)
        have W:‹f1`x=f2`x›
        proof(rule mp[OF bspec[OF pcs_uniq KK] ])
          show ‹m1 ∈ nat›
            by (rule m1nat)
        next
          show ‹m2 ∈ nat›
            by (rule m2nat)
        next
          show ‹partcomp(A, f1, m1, a, g)›
            by (rule K1)
        next
          show ‹partcomp(A, f2, m2, a, g)›
            by (rule K2)
        next
            (*  P1:‹⟨x, y1⟩ ∈ f1›
              K1'A:‹(f1:succ(m1)→A)›
            *)
          have U1:‹x ∈ succ(m1)›
            by (rule func.domain_type[OF P1 K1'A])
          have U2:‹x ∈ succ(m2)›
            by (rule func.domain_type[OF P2 K2'A])
          show ‹x ∈ succ(m1) ∧ x ∈ succ(m2)›
            by (rule conjI[OF U1 U2])
        qed
        from L1 and W and L2
        show ‹y1 = y2› by auto
      qed
    qed
  qed
qed

theorem fuissu : ‹f ∈ X -> Y ⟹ f ⊆ X×Y›
proof
  fix w
  assume H1 : ‹f ∈ X -> Y›
  then have J1:‹f ∈ {q∈Pow(Sigma(X,λ_.Y)). X⊆domain(q) & function(q)}›
    by (unfold Pi_def)
  then have J2:‹f ∈ Pow(Sigma(X,λ_.Y))›
    by auto
  then have J3:‹f ⊆ Sigma(X,λ_.Y)›
    by auto
  assume H2 : ‹w ∈ f›
  from J3 and H2 have ‹w∈Sigma(X,λ_.Y)›
    by auto
  then have J4:‹w ∈ (⋃x∈X. (⋃y∈Y. {⟨x,y⟩}))›
    by auto
  show ‹w ∈ X*Y›
  proof (rule UN_E[OF J4])
    fix x
    assume V1:‹x ∈ X›
    assume V2:‹w ∈ (⋃y∈Y. {⟨x, y⟩})›
    show ‹w ∈ X × Y›
    proof (rule UN_E[OF V2])
      fix y
      assume V3:‹y ∈ Y›
      assume V4:‹w ∈ {⟨x, y⟩}›
      then have V4:‹w = ⟨x, y⟩›
        by auto
      have v5:‹⟨x, y⟩ ∈ Sigma(X,λ_.Y)›
      proof(rule SigmaI)
        show ‹x ∈ X› by (rule V1)
      next
        show ‹y ∈ Y› by (rule V3)
      qed
      then have V5:‹⟨x, y⟩ ∈ X*Y›
        by auto
      from V4 and V5 show ‹w ∈ X × Y› by auto
    qed
  qed
qed

theorem recuniq :
  fixes f
  assumes H0:‹f ∈ nat -> A ∧ f ` 0 = a ∧ satpc(f, nat, g)›
  fixes t
  assumes H1:‹t ∈ nat -> A ∧ t ` 0 = a ∧ satpc(t, nat, g)›
  fixes x
  shows ‹f=t›
proof -
  from H0 have H02:‹∀n ∈ nat. f`succ(n) = g ` <(f`n), n>› by (unfold satpc_def, auto)
  from H0 have H01:‹f ` 0 = a› by auto
  from H0 have H00:‹f ∈ nat -> A› by auto
  from H1 have H12:‹∀n ∈ nat. t`succ(n) = g ` <(t`n), n>› by (unfold satpc_def, auto)
  from H1 have H11:‹t ` 0 = a› by auto
  from H1 have H10:‹t ∈ nat -> A› by auto
  show ‹f=t›
  proof (rule fun_extension[OF H00 H10])
    fix x
    assume K: ‹x ∈ nat›
    show ‹(f ` x) = (t ` x)›
    proof(rule nat_induct[of x])
      show ‹x ∈ nat› by (rule K)
    next
      from H01 and H11 show ‹f ` 0 = t ` 0›
        by auto
    next
      fix x
      assume A:‹x∈nat›
      assume B:‹f`x = t`x›
      show ‹f ` succ(x) = t ` succ(x)›
      proof -
        from H02 and A have H02':‹f`succ(x) = g ` <(f`x), x>›
          by (rule bspec)
        from H12 and A have H12':‹t`succ(x) = g ` <(t`x), x>›
          by (rule bspec)
        from B and H12' have H12'':‹t`succ(x) = g ` <(f`x), x>› by auto
        from H12'' and H02' show ‹f ` succ(x) = t ` succ(x)› by auto
      qed
    qed
  qed
qed

section ‹Lemmas for recursion theorem›

locale recthm =
  fixes A :: "i"
    and a :: "i"
    and g :: "i"
  assumes hyp1 : ‹a ∈ A›
    and hyp2 : ‹g : ((A*nat)→A)›
begin

lemma l3:‹function(⋃pcs(A, a, g))›
  by (rule compatsetunionfun, rule pcs_lem, rule hyp1)

lemma l1 : ‹⋃pcs(A, a, g) ⊆ nat × A›
proof
  fix x
  assume H:‹x ∈ ⋃pcs(A, a, g)›
  hence  H:‹x ∈ ⋃{t∈Pow(nat*A). ∃m∈nat. partcomp(A,t,m,a,g)}›
    by (unfold pcs_def)
  show ‹x ∈ nat × A›
  proof(rule UnionE[OF H])
    fix B
    assume J1:‹x∈B›
    assume J2:‹B ∈ {t ∈ Pow(nat × A) .
            ∃m∈nat. partcomp(A, t, m, a, g)}›
    hence J2:‹B ∈ Pow(nat × A)› by auto
    hence J2:‹B ⊆ nat × A› by auto
    from J1 and J2 show ‹x ∈ nat × A›
      by auto
  qed
qed

lemma le1:
  assumes H:‹x∈1›
  shows ‹x=0›
proof
  show ‹x ⊆ 0›
  proof
    fix z
    assume J:‹z∈x›
    show ‹z∈0›
    proof(rule succE[OF H])
      assume J:‹x∈0›
      show ‹z∈0›
        by (rule notE[OF not_mem_empty J])
    next
      assume K:‹x=0›
      from J and K show ‹z∈0›
        by auto
    qed
  qed
next
  show ‹0 ⊆ x› by auto
qed

lemma lsinglfun : ‹function({⟨0, a⟩})›
proof(unfold function_def)
  show ‹ ∀x y. ⟨x, y⟩ ∈ {⟨0, a⟩} ⟶
          (∀y'. ⟨x, y'⟩ ∈ {⟨0, a⟩} ⟶
                y = y')›
  proof(rule allI,rule allI,rule impI,rule allI,rule impI)
    fix x y y'
    assume H0:‹⟨x, y⟩ ∈ {⟨0, a⟩}›
    assume H1:‹⟨x, y'⟩ ∈ {⟨0, a⟩}›
    show ‹y = y'›
    proof(rule upair.singletonE[OF H0],rule upair.singletonE[OF H1])
      assume H0:‹⟨x, y⟩ = ⟨0, a⟩›
      assume H1:‹⟨x, y'⟩ = ⟨0, a⟩›
      from H0 and H1 have H:‹⟨x, y⟩ = ⟨x, y'⟩› by auto
      then show ‹y = y'› by auto
    qed
  qed
qed

lemma singlsatpc:‹satpc({⟨0, a⟩}, 0, g)›
proof(unfold satpc_def)
  show ‹∀n∈0. {⟨0, a⟩} ` succ(n) =
           g ` ⟨{⟨0, a⟩} ` n, n⟩›
    by auto
qed

lemma zerostep :
  shows ‹partcomp(A, {⟨0, a⟩}, 0, a, g)›
proof(unfold partcomp_def)
  show ‹{⟨0, a⟩} ∈ 1 -> A ∧ {⟨0, a⟩} ` 0 = a ∧ satpc({⟨0, a⟩}, 0, g)›
  proof
    show ‹{⟨0, a⟩} ∈ 1 -> A›
    proof (unfold Pi_def)
      show ‹{⟨0, a⟩} ∈ {f ∈ Pow(1 × A) . 1 ⊆ domain(f) ∧ function(f)}›
      proof
        show ‹{⟨0, a⟩} ∈ Pow(1 × A)›
        proof(rule PowI, rule equalities.singleton_subsetI)
          show ‹⟨0, a⟩ ∈ 1 × A›
          proof
            show ‹0 ∈ 1› by auto
          next
            show ‹a ∈ A› by (rule hyp1)
          qed
        qed
      next
        show ‹1 ⊆ domain({⟨0, a⟩}) ∧ function({⟨0, a⟩})›
        proof
          show ‹1 ⊆ domain({⟨0, a⟩})›
          proof
            fix x
            assume W:‹x∈1›
            from W have W:‹x=0› by (rule le1)
            have Y:‹0∈domain({⟨0, a⟩})›
              by auto
            from W and Y
            show ‹x∈domain({⟨0, a⟩})›
              by auto
          qed
        next
          show ‹function({⟨0, a⟩})›
            by (rule lsinglfun)
        qed
      qed
    qed
    show ‹{⟨0, a⟩} ` 0 = a ∧ satpc({⟨0, a⟩}, 0, g)›
    proof
      show ‹{⟨0, a⟩} ` 0 = a›
        by (rule func.singleton_apply)
    next
      show ‹satpc({⟨0, a⟩}, 0, g)›
        by (rule singlsatpc)
    qed
  qed
qed

lemma zainupcs : ‹⟨0, a⟩ ∈ ⋃pcs(A, a, g)›
proof
  show ‹⟨0, a⟩ ∈ {⟨0, a⟩}›
    by auto
next
  (* {⟨0, a⟩} is a 0-step computation *)
  show ‹{⟨0, a⟩} ∈ pcs(A, a, g)›
  proof(unfold pcs_def)
    show ‹{⟨0, a⟩} ∈ {t ∈ Pow(nat × A) . ∃m∈nat. partcomp(A, t, m, a, g)}›
    proof
      show ‹{⟨0, a⟩} ∈ Pow(nat × A)›
      proof(rule PowI, rule equalities.singleton_subsetI)
        show ‹⟨0, a⟩ ∈ nat × A›
        proof
          show ‹0 ∈ nat› by auto
        next
          show ‹a ∈ A› by (rule hyp1)
        qed
      qed
    next
      show ‹∃m∈nat. partcomp(A, {⟨0, a⟩}, m, a, g)›
      proof
        show ‹partcomp(A, {⟨0, a⟩}, 0, a, g)›
          by (rule zerostep)
      next
        show ‹0 ∈ nat› by auto
      qed
    qed
  qed
qed

lemma l2': ‹0 ∈ domain(⋃pcs(A, a, g))›
proof
  show ‹⟨0, a⟩ ∈ ⋃pcs(A, a, g)›
    by (rule zainupcs)
qed

text ‹Push an ordered pair to the end of partial computation t
and obtain another partial computation.›
lemma shortlem :
  assumes mnat:‹m∈nat›
  assumes F:‹partcomp(A,t,m,a,g)›
  shows ‹partcomp(A,cons(⟨succ(m), g ` <t`m, m>⟩, t),succ(m),a,g)›
proof(rule partcompE[OF F])
  assume F1:‹t ∈ succ(m) → A›
  assume F2:‹t ` 0 = a›
  assume F3:‹satpc(t, m, g)›
  show ?thesis (*‹partcomp(A,cons(⟨succ(m), g ` <t`m, m>⟩, t),succ(m),a,g)› *)
  proof
    have ljk:‹cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ∈ (cons(succ(m),succ(m)) → A)›
    proof(rule func.fun_extend3[OF F1])
      show ‹succ(m) ∉ succ(m)›
        by (rule  upair.mem_not_refl)
      have tmA:‹t ` m ∈ A›
        by (rule func.apply_funtype[OF F1], auto)
      show ‹g ` ⟨t ` m, m⟩ ∈ A›
        by(rule func.apply_funtype[OF hyp2], auto, rule tmA, rule mnat)
    qed
    have ‹cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ∈ (cons(succ(m),succ(m)) → A)›
      by (rule ljk)
    then have ‹cons(⟨cons(m, m), g ` ⟨t ` m, m⟩⟩, t) ∈ cons(cons(m, m), cons(m, m)) → A›
      by (unfold succ_def)
    then show ‹cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ∈ succ(succ(m)) → A›
      by (unfold succ_def, assumption)
    show ‹cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` 0 = a›
    proof(rule trans, rule func.fun_extend_apply[OF F1])
      show ‹succ(m) ∉ succ(m)› by (rule  upair.mem_not_refl)
      show ‹(if 0 = succ(m) then g ` ⟨t ` m, m⟩ else t ` 0) = a›
        by(rule trans, rule upair.if_not_P, auto, rule F2)
    qed
    show ‹satpc(cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t), succ(m), g)›
    proof(unfold satpc_def, rule ballI)
      fix n
      assume Q:‹n ∈ succ(m)›
      show ‹cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` succ(n)
= g ` ⟨cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` n, n⟩›
      proof(rule trans, rule func.fun_extend_apply[OF F1], rule upair.mem_not_refl)
        show ‹(if succ(n) = succ(m) then g ` ⟨t ` m, m⟩ else t ` succ(n)) =
    g ` ⟨cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` n, n⟩›
        proof(rule upair.succE[OF Q])
          assume Y:‹n=m›
          show ‹(if succ(n) = succ(m) then g ` ⟨t ` m, m⟩ else t ` succ(n)) =
    g ` ⟨cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` n, n⟩›
          proof(rule trans, rule upair.if_P)
            from Y show ‹succ(n) = succ(m)› by auto
          next
            have L1:‹t ` m = cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` n›
            proof(rule sym, rule trans, rule func.fun_extend_apply[OF F1], rule upair.mem_not_refl)
              show ‹ (if n = succ(m) then g ` ⟨t ` m, m⟩ else t ` n) = t ` m›
              proof(rule trans, rule upair.if_not_P)
                from Y show ‹t ` n = t ` m› by auto
                show ‹n ≠ succ(m)›
                proof(rule not_sym)
                  show ‹succ(m) ≠ n›
                    by(rule subst, rule sym, rule Y, rule upair.succ_neq_self)
                qed
              qed
            qed
            from Y
            have L2:‹m = n›
              by auto
            have L:‹ ⟨t ` m, m⟩ = ⟨cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` n, n⟩›
              by(rule subst_context2[OF L1 L2])
            show ‹ g ` ⟨t ` m, m⟩ = g ` ⟨cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` n, n⟩›
              by(rule subst_context[OF L])
          qed
        next
          assume Y:‹n ∈ m›
          show ‹(if succ(n) = succ(m) then g ` ⟨t ` m, m⟩ else t ` succ(n)) =
                g ` ⟨cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` n, n⟩›
          proof(rule trans, rule upair.if_not_P)
            show ‹succ(n) ≠ succ(m)›
              by(rule contrapos, rule upair.mem_imp_not_eq, rule Y, rule upair.succ_inject, assumption)
          next
            have X:‹cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` n = t ` n›
            proof(rule trans, rule func.fun_extend_apply[OF F1], rule upair.mem_not_refl)
              show ‹(if n = succ(m) then g ` ⟨t ` m, m⟩ else t ` n) = t ` n›
              proof(rule upair.if_not_P)
                show ‹n ≠ succ(m)›
                proof(rule contrapos)
                  assume q:"n=succ(m)"
                  from q and Y have M:‹succ(m)∈m›
                    by auto
                  show ‹m∈m›
                    by(rule Nat.succ_in_naturalD[OF M mnat])
                next
                  show ‹m ∉ m› by (rule  upair.mem_not_refl)
                qed
              qed
            qed
            from F3
            have W:‹∀n∈m. t ` succ(n) = g ` ⟨t ` n, n⟩›
              by (unfold satpc_def)
            have U:‹t ` succ(n) = g ` ⟨t ` n, n⟩›
              by (rule bspec[OF W Y])
            show ‹t ` succ(n) = g ` ⟨cons(⟨succ(m), g ` ⟨t ` m, m⟩⟩, t) ` n, n⟩›
              by (rule trans, rule U, rule sym, rule subst_context[OF X])
          qed
        qed
      qed
    qed
  qed
qed

lemma l2:‹nat ⊆ domain(⋃pcs(A, a, g))›
proof
  fix x
  assume G:‹x∈nat›
  show ‹x ∈ domain(⋃pcs(A, a, g))›
  proof(rule nat_induct[of x])
    show ‹x∈nat› by (rule G)
  next
    fix x
    assume Q1:‹x∈nat›
    assume Q2:‹x∈domain(⋃pcs(A, a, g))›
    show ‹succ(x)∈domain(⋃pcs(A, a, g))›
    proof(rule domainE[OF Q2])
      fix y
      assume W1:‹⟨x, y⟩ ∈ (⋃pcs(A, a, g))›
      show ‹succ(x)∈domain(⋃pcs(A, a, g))›
      proof(rule UnionE[OF W1])
        fix t
        assume E1:‹⟨x, y⟩ ∈ t›
        assume E2:‹t ∈ pcs(A, a, g)›
        hence E2:‹t∈{t∈Pow(nat*A). ∃m ∈ nat. partcomp(A,t,m,a,g)}›
          by(unfold pcs_def)
        have E21:‹t∈Pow(nat*A)›
          by(rule CollectD1[OF E2])
        have E22m:‹∃m∈nat. partcomp(A,t,m,a,g)›
          by(rule CollectD2[OF E2])
        show ‹succ(x)∈domain(⋃pcs(A, a, g))›
        proof(rule bexE[OF E22m])
          fix m
          assume mnat:‹m∈nat›
          assume E22P:‹partcomp(A,t,m,a,g)›
          hence E22:‹((t:succ(m)→A) ∧ (t`0=a)) ∧ satpc(t,m,g)›
            by(unfold partcomp_def, auto)
          hence E223:‹satpc(t,m,g)› by auto
          hence E223:‹∀n ∈ m . t`succ(n) = g ` <t`n, n>›
            by(unfold satpc_def, auto)
          from E22 have E221:‹(t:succ(m)→A)›
            by auto
          from E221 have domt:‹domain(t) = succ(m)›
            by (rule func.domain_of_fun)
          from E1 have xind:‹x ∈ domain(t)›
            by (rule equalities.domainI)
          from xind and domt have xinsm:‹x ∈ succ(m)›
            by auto
          show ‹succ(x)∈domain(⋃pcs(A, a, g))›
          proof
        (*proof(rule exE[OF E22])*)
            show ‹ ⟨succ(x), g ` <t`x, x>⟩ ∈ (⋃pcs(A, a, g))› (*?*)
            proof
             (*t∪{⟨succ(x), g ` <t`x, x>⟩}*)
              show ‹cons(⟨succ(x), g ` <t`x, x>⟩, t) ∈ pcs(A, a, g)›
              proof(unfold pcs_def, rule CollectI)
                from E21
                have L1:‹t ⊆ nat × A›
                  by auto
                from Q1 have J1:‹succ(x)∈nat›
                  by auto(*Nat.nat_succI*)
                have txA: ‹t ` x ∈ A›
                  by (rule func.apply_type[OF E221 xinsm])
                from txA and Q1 have txx:‹⟨t ` x, x⟩ ∈ A × nat›
                  by auto
                have secp: ‹g ` ⟨t ` x, x⟩ ∈ A›
                  by(rule func.apply_type[OF hyp2 txx])
                from J1 and secp
                have L2:‹⟨succ(x),g ` ⟨t ` x, x⟩⟩ ∈ nat × A›
                  by auto
                show ‹ cons(⟨succ(x),g ` ⟨t ` x, x⟩⟩,t) ∈ Pow(nat × A)›
                proof(rule PowI)
                  show ‹ cons(⟨succ(x), g ` ⟨t ` x, x⟩⟩, t) ⊆ nat × A›
                  proof
                    show ‹⟨succ(x), g ` ⟨t ` x, x⟩⟩ ∈ nat × A ∧ t ⊆ nat × A›
                      by (rule conjI[OF L2 L1])
                  qed
                qed
              next
                show ‹∃m ∈ nat. partcomp(A, cons(⟨succ(x), g ` ⟨t ` x, x⟩⟩, t), m, a, g)›
                proof(rule succE[OF xinsm])
                  assume xeqm:‹x=m›
                  show ‹∃m ∈ nat. partcomp(A, cons(⟨succ(x), g ` ⟨t ` x, x⟩⟩, t), m, a, g)›
                  proof
                    show ‹partcomp(A, cons(⟨succ(x), g ` ⟨t ` x, x⟩⟩, t), succ(x), a, g)›
                    proof(rule shortlem[OF Q1])
                      show ‹partcomp(A, t, x, a, g)›
                      proof(rule subst[of m x], rule sym, rule xeqm)
                        show ‹partcomp(A, t, m, a, g)›
                          by (rule E22P)
                      qed
                    qed
                  next
                    from Q1 show ‹succ(x) ∈ nat› by auto
                  qed
                next
                  assume xinm:‹x∈m›
                  have lmm:‹cons(⟨succ(x), g ` ⟨t ` x, x⟩⟩, t) = t›
                    by (rule addmiddle[OF mnat E22P xinm])
                  show ‹∃m∈nat. partcomp(A, cons(⟨succ(x), g ` ⟨t ` x, x⟩⟩, t), m, a, g)›
                    by(rule subst[of t], rule sym, rule lmm, rule E22m)
                qed
              qed
            next
              show ‹⟨succ(x), g ` ⟨t ` x, x⟩⟩ ∈ cons(⟨succ(x), g ` ⟨t ` x, x⟩⟩, t)›
                by auto
            qed
          qed
        qed
      qed
    qed
  next
    show ‹0 ∈ domain(⋃pcs(A, a, g))›
      by (rule l2')
  qed
qed

lemma useful : ‹∀m∈nat. ∃t. partcomp(A,t,m,a,g)›
proof(rule nat_induct_bound)
  show ‹∃t. partcomp(A, t, 0, a, g)›
  proof
    show ‹partcomp(A, {⟨0, a⟩}, 0, a, g)›
      by (rule zerostep)
  qed
next
  fix m
  assume mnat:‹m∈nat›
  assume G:‹∃t. partcomp(A,t,m,a,g)›
  show ‹∃t. partcomp(A,t,succ(m),a,g)›
  proof(rule exE[OF G])
    fix t
    assume G:‹partcomp(A,t,m,a,g)›
    show ‹∃t. partcomp(A,t,succ(m),a,g)›
    proof
      show ‹partcomp(A,cons(⟨succ(m), g ` <t`m, m>⟩, t),succ(m),a,g)›
        by(rule shortlem[OF mnat G])
    qed
  qed
qed

lemma l4 : ‹(⋃pcs(A,a,g)) ∈ nat -> A›
proof(unfold Pi_def)
  show ‹ ⋃pcs(A, a, g) ∈ {f ∈ Pow(nat × A) . nat ⊆ domain(f) ∧ function(f)}›
  proof
    show ‹⋃pcs(A, a, g) ∈ Pow(nat × A)›
    proof
      show ‹⋃pcs(A, a, g) ⊆ nat × A›
        by (rule l1)
    qed
  next
    show ‹nat ⊆ domain(⋃pcs(A, a, g)) ∧ function(⋃pcs(A, a, g))›
    proof
      show ‹nat ⊆ domain(⋃pcs(A, a, g))›
        by (rule l2)
    next
      show ‹function(⋃pcs(A, a, g))›
        by (rule l3)
    qed
  qed
qed

lemma l5: ‹(⋃pcs(A, a, g)) ` 0 = a›
proof(rule func.function_apply_equality)
  show ‹function(⋃pcs(A, a, g))›
    by (rule l3)
next
  show ‹⟨0, a⟩ ∈ ⋃pcs(A, a, g)›
    by (rule zainupcs)
qed

lemma ballE2:
  assumes ‹∀x∈AA. P(x)›
  assumes ‹x∈AA›
  assumes ‹P(x) ==> Q›
  shows Q
  by (rule assms(3), rule bspec, rule assms(1), rule assms(2))

text ‹ Recall that
  ‹satpc(t,α,g) == ∀n ∈ α . t`succ(n) = g ` <t`n, n>›
  ‹partcomp(A,t,m,a,g) == (t:succ(m)→A) ∧ (t`0=a) ∧ satpc(t,m,g)›
  ‹pcs(A,a,g) == {t∈Pow(nat*A). ∃m. partcomp(A,t,m,a,g)}›
›

lemma l6new: ‹satpc(⋃pcs(A, a, g), nat, g)›
proof (unfold satpc_def, rule ballI)
  fix n
  assume nnat:‹n∈nat›
  hence snnat:‹succ(n)∈nat› by auto
  (* l2:‹nat ⊆ domain(⋃pcs(A, a, g))› *)
  show ‹(⋃pcs(A, a, g)) ` succ(n) = g ` ⟨(⋃pcs(A, a, g)) ` n, n⟩›
  proof(rule ballE2[OF useful snnat], erule exE)
    fix t
    assume Y:‹partcomp(A, t, succ(n), a, g)›
    show ‹(⋃pcs(A, a, g)) ` succ(n) = g ` ⟨(⋃pcs(A, a, g)) ` n, n⟩›
    proof(rule partcompE[OF Y])
      assume Y1:‹t ∈ succ(succ(n)) → A›
      assume Y2:‹t ` 0 = a›
      assume Y3:‹satpc(t, succ(n), g)›
      hence Y3:‹∀x ∈ succ(n) . t`succ(x) = g ` <t`x, x>›
        by (unfold satpc_def)
      hence Y3:‹t`succ(n) = g ` <t`n, n>›
        by (rule bspec, auto)
      have e1:‹(⋃pcs(A, a, g)) ` succ(n) = t ` succ(n)›
      proof(rule valofunion, rule pcs_lem, rule hyp1)
        show ‹t ∈ pcs(A, a, g)›
        proof(unfold pcs_def, rule CollectI)
          show ‹t ∈ Pow(nat × A)›
            proof(rule tgb)
            show ‹t ∈ succ(succ(n)) → A› by (rule Y1)
          next
            from snnat
            show ‹succ(succ(n)) ∈ nat› by auto
          qed
        next
          show ‹∃m∈nat. partcomp(A, t, m, a, g)›
            by(rule bexI, rule Y, rule snnat)
        qed
      next
        show ‹t ∈ succ(succ(n)) → A› by (rule Y1)
      next
        show ‹succ(n) ∈ succ(succ(n))› by auto
      next
        show ‹t ` succ(n) = t ` succ(n)› by (rule refl)
      qed
      have e2:‹(⋃pcs(A, a, g)) ` n = t ` n›
      proof(rule valofunion, rule pcs_lem, rule hyp1)
        show ‹t ∈ pcs(A, a, g)›
        proof(unfold pcs_def, rule CollectI)
          show ‹t ∈ Pow(nat × A)›
          proof(rule tgb)
            show ‹t ∈ succ(succ(n)) → A› by (rule Y1)
          next
            from snnat
            show ‹succ(succ(n)) ∈ nat› by auto
          qed
        next
          show ‹∃m∈nat. partcomp(A, t, m, a, g)›
            by(rule bexI, rule Y, rule snnat)
        qed
      next
        show ‹t ∈ succ(succ(n)) → A› by (rule Y1)
      next
        show ‹n ∈ succ(succ(n))› by auto
      next
        show ‹t ` n = t ` n› by (rule refl)
      qed
      have e3:‹g ` ⟨(⋃pcs(A, a, g)) ` n, n⟩ = g ` ⟨t ` n, n⟩›
        by (rule subst[OF e2], rule refl)
      show ‹(⋃pcs(A, a, g)) ` succ(n) = g ` ⟨(⋃pcs(A, a, g)) ` n, n⟩›
        by (rule trans, rule e1,rule trans, rule Y3, rule sym, rule e3)
    qed
  qed
qed

section "Recursion theorem"

theorem recursionthm:
  shows ‹∃!f. ((f ∈ (nat→A)) ∧ ((f`0) = a) ∧ satpc(f,nat,g))›
(* where ‹satpc(t,α,g) == ∀n ∈ α . t`succ(n) = g ` <t`n, n>› *)
proof
  show ‹∃f. f ∈ nat -> A ∧ f ` 0 = a ∧ satpc(f, nat, g)›
  proof
    show ‹(⋃pcs(A,a,g)) ∈ nat -> A ∧ (⋃pcs(A,a,g)) ` 0 = a ∧ satpc(⋃pcs(A,a,g), nat, g)›
    proof
      show ‹⋃pcs(A, a, g) ∈ nat -> A›
        by (rule l4)
    next
      show ‹(⋃pcs(A, a, g)) ` 0 = a ∧ satpc(⋃pcs(A, a, g), nat, g)›
      proof
        show ‹(⋃pcs(A, a, g)) ` 0 = a›
          by (rule l5)
      next
        show ‹satpc(⋃pcs(A, a, g), nat, g)›
          by (rule l6new)
      qed
    qed
  qed
next
  show ‹⋀f y. f ∈ nat -> A ∧
           f ` 0 = a ∧
           satpc(f, nat, g) ⟹
           y ∈ nat -> A ∧
           y ` 0 = a ∧
           satpc(y, nat, g) ⟹
           f = y›
    by (rule recuniq)
qed

end

section "Lemmas for addition"

text ‹
Let's define function t(x) = (a+x).
Firstly we need to define a function ‹g:nat × nat → nat›, such that
‹g`⟨t`n, n⟩ = t`succ(n) = a + (n + 1) = (a + n) + 1 = (t`n) + 1›
So ‹g`⟨a, b⟩ = a + 1› and ‹g(p) = succ(pr1(p))›
and ‹satpc(t,α,g) ⟺ ∀n ∈ α . t`succ(n) = succ(t`n)›.
›

definition addg :: ‹i›
  where addg_def : ‹addg == λx∈(nat*nat). succ(fst(x))›

lemma addgfun: ‹function(addg)›
  by (unfold addg_def, rule func.function_lam)

lemma addgsubpow : ‹addg ∈ Pow((nat × nat) × nat)›
proof (unfold addg_def, rule subsetD)
  show ‹(λx∈nat × nat. succ(fst(x))) ∈ nat × nat → nat›
  proof(rule func.lam_type)
    fix x
    assume ‹x∈nat × nat›
    hence ‹fst(x)∈nat› by auto
    thus ‹succ(fst(x)) ∈ nat› by auto
  qed
next
  show ‹nat × nat → nat ⊆ Pow((nat × nat) × nat)›
    by (rule pisubsig)
qed

lemma addgdom : ‹nat × nat ⊆ domain(addg)›
proof(unfold addg_def)
  have e:‹domain(λx∈nat × nat. succ(fst(x))) = nat × nat›
    by (rule domain_lam)  (* "domain(Lambda(A,b)) = A" *)
  show ‹nat × nat ⊆
    domain(λx∈nat × nat. succ(fst(x)))›
    by (rule subst, rule sym, rule e, auto)
qed

lemma plussucc:
  assumes F:‹f ∈ (nat→nat)›
  assumes H:‹satpc(f,nat,addg)›
  shows ‹∀n ∈ nat . f`succ(n) = succ(f`n)›
proof
  fix n
  assume J:‹n∈nat›
  from H
  have H:‹∀n ∈ nat . f`succ(n) = (λx∈(nat*nat). succ(fst(x)))` <f`n, n>›
    by (unfold satpc_def, unfold addg_def)
  have H:‹f`succ(n) = (λx∈(nat*nat). succ(fst(x)))` <f`n, n>›
    by (rule bspec[OF H J])
  have Q:‹(λx∈(nat*nat). succ(fst(x)))` <f`n, n> = succ(fst(<f`n, n>))›
  proof(rule func.beta)
    show ‹⟨f ` n, n⟩ ∈ nat × nat›
    proof
      show ‹f ` n ∈ nat›
        by (rule func.apply_funtype[OF F J])
      show ‹n ∈ nat›
        by (rule J)
    qed
  qed
  have HQ:‹f`succ(n) = succ(fst(<f`n, n>))›
    by (rule trans[OF H Q])
  have K:‹fst(<f`n, n>) = f`n›
    by auto
  hence K:‹succ(fst(<f`n, n>)) = succ(f`n)›
    by (rule subst_context)
  show ‹f`succ(n) = succ(f`n)›
    by (rule trans[OF HQ K])
qed

section "Definition of addition"

text ‹Theorem that addition of natural numbers exists
and unique in some sense. Due to theorem 'plussucc' the term
 ‹satpc(f,nat,addg)›
  can be replaced here with
 ‹∀n ∈ nat . f`succ(n) = succ(f`n)›.›
theorem addition:
  assumes ‹a∈nat›
  shows
 ‹∃!f. ((f ∈ (nat→nat)) ∧ ((f`0) = a) ∧ satpc(f,nat,addg))›
proof(rule recthm.recursionthm, unfold recthm_def)
  show ‹a ∈ nat ∧ addg ∈ nat × nat → nat›
  proof
    show ‹a∈nat› by (rule assms(1))
  next
    show ‹addg ∈ nat × nat → nat›
    proof(unfold Pi_def, rule CollectI)
      show ‹addg ∈ Pow((nat × nat) × nat)›
        by (rule addgsubpow)
    next
      have A2: ‹nat × nat ⊆ domain(addg)›
        by(rule addgdom)
      have A3: ‹function(addg)›
        by (rule addgfun)
      show ‹nat × nat ⊆ domain(addg) ∧ function(addg)›
        by(rule conjI[OF A2 A3])
    qed
  qed
qed

end