Theory Recursion-Theory-I.PRecFun2

(*  Title:       Primitive recursive functions of one variable
    Author:      Michael Nedzelsky <MichaelNedzelsky at yandex.ru>, 2008
    Maintainer:  Michael Nedzelsky <MichaelNedzelsky at yandex.ru>
*)

section ‹Primitive recursive functions of one variable›

theory PRecFun2
imports PRecFun
begin

subsection ‹Alternative definition of primitive recursive functions of one variable›

definition
  UnaryRecOp :: "(nat ⇒ nat) ⇒ (nat ⇒ nat) ⇒ (nat ⇒ nat)" where
  "UnaryRecOp = (λ g h. pr_conv_2_to_1 (PrimRecOp g (pr_conv_1_to_3 h)))"

lemma unary_rec_into_pr: "⟦ g ∈ PrimRec1; h ∈ PrimRec1 ⟧ ⟹ UnaryRecOp g h ∈ PrimRec1" by (simp add: UnaryRecOp_def pr_conv_1_to_3_lm pr_conv_2_to_1_lm pr_rec)

definition
  c_f_pair :: "(nat ⇒ nat) ⇒ (nat ⇒ nat) ⇒ (nat ⇒ nat)" where
  "c_f_pair = (λ f g x. c_pair (f x) (g x))"

lemma c_f_pair_to_pr: "⟦ f ∈ PrimRec1; g ∈ PrimRec1 ⟧ ⟹ c_f_pair f g ∈ PrimRec1"
  unfolding c_f_pair_def by prec

inductive_set PrimRec1' :: "(nat ⇒ nat) set"
where
  zero: "(λ x. 0) ∈ PrimRec1'"
  | suc:  "Suc ∈ PrimRec1'"
  | fst:  "c_fst ∈ PrimRec1'"
  | snd:  "c_snd ∈ PrimRec1'"
  | comp: "⟦ f ∈ PrimRec1'; g ∈ PrimRec1' ⟧ ⟹ (λ x. f (g x)) ∈ PrimRec1'"
  | pair: "⟦ f ∈ PrimRec1'; g ∈ PrimRec1' ⟧ ⟹ c_f_pair f g ∈ PrimRec1'"
  | un_rec: "⟦ f ∈ PrimRec1'; g ∈ PrimRec1' ⟧ ⟹ UnaryRecOp f g ∈ PrimRec1'"

lemma primrec'_into_primrec: "f ∈ PrimRec1' ⟹ f ∈ PrimRec1"
proof (induct f rule: PrimRec1'.induct)
  case zero show ?case by (rule pr_zero)
next
  case suc show ?case by (rule pr_suc)
next
  case fst show ?case by (rule c_fst_is_pr)
next
  case snd show ?case by (rule c_snd_is_pr)
next
  case comp from comp show ?case by (simp add: pr_comp1_1)
next
  case pair from pair show ?case by (simp add: c_f_pair_to_pr)
next
  case un_rec from un_rec show ?case by (simp add: unary_rec_into_pr)
qed

lemma pr_id1_1': "(λ x. x) ∈ PrimRec1'"
proof -
  have "c_f_pair c_fst c_snd ∈ PrimRec1'" by (simp add: PrimRec1'.fst PrimRec1'.snd PrimRec1'.pair)
  moreover have "c_f_pair c_fst c_snd = (λ x. x)" by (simp add: c_f_pair_def)
  ultimately show ?thesis by simp
qed

lemma pr_id2_1': "pr_conv_2_to_1 (λ x y. x) ∈ PrimRec1'" by (simp add: pr_conv_2_to_1_def PrimRec1'.fst)

lemma pr_id2_2': "pr_conv_2_to_1 (λ x y. y) ∈ PrimRec1'" by (simp add: pr_conv_2_to_1_def PrimRec1'.snd)

lemma pr_id3_1': "pr_conv_3_to_1 (λ x y z. x) ∈ PrimRec1'"
proof -
  have "pr_conv_3_to_1 (λ x y z. x) = (λx. c_fst (c_fst x))" by (simp add: pr_conv_3_to_1_def)
  moreover from PrimRec1'.fst PrimRec1'.fst have "(λx. c_fst (c_fst x)) ∈ PrimRec1'" by (rule PrimRec1'.comp)
  ultimately show ?thesis by simp
qed

lemma pr_id3_2': "pr_conv_3_to_1 (λ x y z. y) ∈ PrimRec1'"
proof -
  have "pr_conv_3_to_1 (λ x y z. y) = (λx. c_snd (c_fst x))" by (simp add: pr_conv_3_to_1_def)
  moreover from PrimRec1'.snd PrimRec1'.fst have "(λx. c_snd (c_fst x)) ∈ PrimRec1'" by (rule PrimRec1'.comp)
  ultimately show ?thesis by simp
qed

lemma pr_id3_3': "pr_conv_3_to_1 (λ x y z. z) ∈ PrimRec1'"
proof -
  have "pr_conv_3_to_1 (λ x y z. z) = (λx. c_snd x)" by (simp add: pr_conv_3_to_1_def)
  thus ?thesis by (simp add: PrimRec1'.snd)
qed

lemma pr_comp2_1': "⟦ pr_conv_2_to_1 f ∈ PrimRec1'; g ∈ PrimRec1'; h ∈ PrimRec1' ⟧ ⟹ (λ x. f (g x) (h x)) ∈ PrimRec1'"
proof -
  assume A1: "pr_conv_2_to_1 f ∈ PrimRec1'"
  assume A2: "g ∈ PrimRec1'"
  assume A3: "h ∈ PrimRec1'"
  let ?f1 = "pr_conv_2_to_1 f"
  have S1: "(%x. ?f1 ((c_f_pair g h) x)) = (λ x. f (g x) (h x))" by (simp add: c_f_pair_def pr_conv_2_to_1_def)
  from A2 A3 have S2: "c_f_pair g h ∈ PrimRec1'" by (rule PrimRec1'.pair)
  from A1 S2 have S3: "(%x. ?f1 ((c_f_pair g h) x)) ∈ PrimRec1'" by (rule PrimRec1'.comp)
  with S1 show ?thesis by simp
qed

lemma pr_comp3_1': "⟦ pr_conv_3_to_1 f ∈ PrimRec1'; g ∈ PrimRec1'; h ∈ PrimRec1'; k ∈ PrimRec1' ⟧ ⟹ (λ x. f (g x) (h x) (k x)) ∈ PrimRec1'"
proof -
  assume A1: "pr_conv_3_to_1 f ∈ PrimRec1'"
  assume A2: "g ∈ PrimRec1'"
  assume A3: "h ∈ PrimRec1'"
  assume A4: "k ∈ PrimRec1'"
  from A2 A3 have "c_f_pair g h ∈ PrimRec1'" by (rule PrimRec1'.pair)
  from this A4 have "c_f_pair (c_f_pair g h) k ∈ PrimRec1'" by (rule PrimRec1'.pair)
  from A1 this have "(%x. (pr_conv_3_to_1 f) ((c_f_pair (c_f_pair g h) k) x)) ∈ PrimRec1'" by (rule PrimRec1'.comp)
  then show ?thesis by (simp add: c_f_pair_def pr_conv_3_to_1_def)
qed

lemma pr_comp1_2': "⟦ f ∈ PrimRec1'; pr_conv_2_to_1 g ∈ PrimRec1' ⟧ ⟹ pr_conv_2_to_1 (λ x y. f (g x y)) ∈ PrimRec1'"
proof -
  assume "f ∈ PrimRec1'"
  and "pr_conv_2_to_1 g ∈ PrimRec1'" (is "?g1 ∈ PrimRec1'")
  then have "(λ x. f (?g1 x)) ∈ PrimRec1'" by (rule PrimRec1'.comp)
  then show ?thesis by (simp add: pr_conv_2_to_1_def)
qed

lemma pr_comp1_3': "⟦ f ∈ PrimRec1'; pr_conv_3_to_1 g ∈ PrimRec1' ⟧ ⟹ pr_conv_3_to_1 (λ x y z. f (g x y z)) ∈ PrimRec1'"
proof -
  assume "f ∈ PrimRec1'"
  and "pr_conv_3_to_1 g ∈ PrimRec1'" (is "?g1 ∈ PrimRec1'")
  then have "(λ x. f (?g1 x)) ∈ PrimRec1'" by (rule PrimRec1'.comp)
  then show ?thesis by (simp add: pr_conv_3_to_1_def)
qed

lemma pr_comp2_2': "⟦ pr_conv_2_to_1 f ∈ PrimRec1'; pr_conv_2_to_1 g ∈ PrimRec1'; pr_conv_2_to_1 h ∈ PrimRec1' ⟧ ⟹ pr_conv_2_to_1 (λ x y. f (g x y) (h x y)) ∈ PrimRec1'"
proof -
  assume "pr_conv_2_to_1 f ∈ PrimRec1'"
  and "pr_conv_2_to_1 g ∈ PrimRec1'" (is "?g1 ∈ PrimRec1'")
  and "pr_conv_2_to_1 h ∈ PrimRec1'" (is "?h1 ∈ PrimRec1'")
  then have "(λ x. f (?g1 x) (?h1 x)) ∈ PrimRec1'" by (rule pr_comp2_1')
  then show ?thesis by (simp add: pr_conv_2_to_1_def)
qed

lemma pr_comp2_3': "⟦ pr_conv_2_to_1 f ∈ PrimRec1'; pr_conv_3_to_1 g ∈ PrimRec1'; pr_conv_3_to_1 h ∈ PrimRec1' ⟧ ⟹ pr_conv_3_to_1 (λ x y z. f (g x y z) (h x y z)) ∈ PrimRec1'"
proof -
  assume "pr_conv_2_to_1 f ∈ PrimRec1'"
  and "pr_conv_3_to_1 g ∈ PrimRec1'" (is "?g1 ∈ PrimRec1'")
  and "pr_conv_3_to_1 h ∈ PrimRec1'" (is "?h1 ∈ PrimRec1'")
  then have "(λ x. f (?g1 x) (?h1 x)) ∈ PrimRec1'" by (rule pr_comp2_1')
  then show ?thesis by (simp add: pr_conv_3_to_1_def)
qed

lemma pr_comp3_2': "⟦ pr_conv_3_to_1 f ∈ PrimRec1'; pr_conv_2_to_1 g ∈ PrimRec1'; pr_conv_2_to_1 h ∈ PrimRec1'; pr_conv_2_to_1 k ∈ PrimRec1' ⟧ ⟹ pr_conv_2_to_1 (λ x y. f (g x y) (h x y) (k x y)) ∈ PrimRec1'"
proof -
  assume "pr_conv_3_to_1 f ∈ PrimRec1'"
  and "pr_conv_2_to_1 g ∈ PrimRec1'" (is "?g1 ∈ PrimRec1'")
  and "pr_conv_2_to_1 h ∈ PrimRec1'" (is "?h1 ∈ PrimRec1'")
  and "pr_conv_2_to_1 k ∈ PrimRec1'" (is "?k1 ∈ PrimRec1'")
  then have "(λ x. f (?g1 x) (?h1 x) (?k1 x)) ∈ PrimRec1'" by (rule pr_comp3_1')
  then show ?thesis by (simp add: pr_conv_2_to_1_def)
qed

lemma pr_comp3_3': "⟦ pr_conv_3_to_1 f ∈ PrimRec1'; pr_conv_3_to_1 g ∈ PrimRec1'; pr_conv_3_to_1 h ∈ PrimRec1'; pr_conv_3_to_1 k ∈ PrimRec1' ⟧ ⟹ pr_conv_3_to_1 (λ x y z. f (g x y z) (h x y z) (k x y z)) ∈ PrimRec1'"
proof -
  assume "pr_conv_3_to_1 f ∈ PrimRec1'"
  and "pr_conv_3_to_1 g ∈ PrimRec1'" (is "?g1 ∈ PrimRec1'")
  and "pr_conv_3_to_1 h ∈ PrimRec1'" (is "?h1 ∈ PrimRec1'")
  and "pr_conv_3_to_1 k ∈ PrimRec1'" (is "?k1 ∈ PrimRec1'")
  then have "(λ x. f (?g1 x) (?h1 x) (?k1 x)) ∈ PrimRec1'" by (rule pr_comp3_1')
  then show ?thesis by (simp add: pr_conv_3_to_1_def)
qed

lemma lm': "(f1 ∈ PrimRec1 ⟶ f1 ∈ PrimRec1') ∧ (g1 ∈ PrimRec2 ⟶ pr_conv_2_to_1 g1 ∈ PrimRec1') ∧ (h1 ∈ PrimRec3 ⟶ pr_conv_3_to_1 h1 ∈ PrimRec1')"
proof (induct rule: PrimRec1_PrimRec2_PrimRec3.induct)
     case zero show ?case by (rule PrimRec1'.zero)
next case suc show ?case by (rule PrimRec1'.suc)
next case id1_1 show ?case by (rule pr_id1_1')
next case id2_1 show ?case by (rule pr_id2_1')
next case id2_2 show ?case by (rule pr_id2_2')
next case id3_1 show ?case by (rule pr_id3_1')
next case id3_2 show ?case by (rule pr_id3_2')
next case id3_3 show ?case by (rule pr_id3_3')
next case comp1_1 from comp1_1 show ?case by (simp add: PrimRec1'.comp)
next case comp1_2 from comp1_2 show ?case by (simp add: pr_comp1_2')
next case comp1_3 from comp1_3 show ?case by (simp add: pr_comp1_3')
next case comp2_1 from comp2_1 show ?case by (simp add: pr_comp2_1')
next case comp2_2 from comp2_2 show ?case by (simp add: pr_comp2_2')
next case comp2_3 from comp2_3 show ?case by (simp add: pr_comp2_3')
next case comp3_1 from comp3_1 show ?case by (simp add: pr_comp3_1')
next case comp3_2 from comp3_2 show ?case by (simp add: pr_comp3_2')
next case comp3_3 from comp3_3 show ?case by (simp add: pr_comp3_3')
next case prim_rec
  fix g h assume A1: "g ∈ PrimRec1'" and "pr_conv_3_to_1 h ∈ PrimRec1'"
  then have "UnaryRecOp g (pr_conv_3_to_1 h) ∈ PrimRec1'" by (rule PrimRec1'.un_rec)
  moreover have "UnaryRecOp g (pr_conv_3_to_1 h) = pr_conv_2_to_1 (PrimRecOp g h)" by (simp add: UnaryRecOp_def)
  ultimately show "pr_conv_2_to_1 (PrimRecOp g h) ∈ PrimRec1'" by simp
qed

theorem pr_1_eq_1': "PrimRec1 = PrimRec1'"
proof -
  have S1: "⋀ f. f ∈ PrimRec1 ⟶ f ∈ PrimRec1'" by (simp add: lm')
  have S2: "⋀ f. f ∈ PrimRec1' ⟶ f ∈ PrimRec1" by (simp add: primrec'_into_primrec)
  from S1 S2 show ?thesis by blast
qed

subsection ‹The scheme datatype›

datatype PrimScheme = Base_zero | Base_suc | Base_fst | Base_snd
                      | Comp_op PrimScheme PrimScheme
                      | Pair_op PrimScheme PrimScheme
                      | Rec_op PrimScheme PrimScheme

primrec
  sch_to_pr :: "PrimScheme ⇒ (nat ⇒ nat)"
where
  "sch_to_pr Base_zero = (λ x. 0)"
| "sch_to_pr Base_suc = Suc"
| "sch_to_pr Base_fst = c_fst"
| "sch_to_pr Base_snd = c_snd"
| "sch_to_pr (Comp_op t1 t2)  = (λ x. (sch_to_pr t1) ((sch_to_pr t2) x))"
| "sch_to_pr (Pair_op t1 t2)  = c_f_pair (sch_to_pr t1) (sch_to_pr t2)"
| "sch_to_pr (Rec_op t1 t2)  = UnaryRecOp (sch_to_pr t1) (sch_to_pr t2)"

lemma sch_to_pr_into_pr: "sch_to_pr sch ∈ PrimRec1" by (simp add: pr_1_eq_1', induct sch, simp_all add: PrimRec1'.intros)

lemma sch_to_pr_srj: "f ∈ PrimRec1 ⟹ (∃ sch. f = sch_to_pr sch)"
proof -
  assume "f ∈ PrimRec1" then have A1: "f ∈ PrimRec1'" by (simp add: pr_1_eq_1')
  from A1 show ?thesis
  proof (induct f rule: PrimRec1'.induct)
    have "(λ x. 0) = sch_to_pr Base_zero" by simp
    then show "∃sch. (λu. 0) = sch_to_pr sch" by (rule exI)
  next
    have "Suc = sch_to_pr Base_suc" by simp
    then show "∃sch. Suc = sch_to_pr sch" by (rule exI)
  next
    have "c_fst = sch_to_pr Base_fst" by simp
    then show "∃sch. c_fst = sch_to_pr sch" by (rule exI)
  next
    have "c_snd = sch_to_pr Base_snd" by simp
    then show "∃sch. c_snd = sch_to_pr sch" by (rule exI)
  next
    fix f1 f2 assume B1: "∃sch. f1 = sch_to_pr sch" and B2: "∃sch. f2 = sch_to_pr sch"
    from B1 obtain sch1 where S1: "f1 = sch_to_pr sch1" ..
    from B2 obtain sch2 where S2: "f2 = sch_to_pr sch2" ..
    from S1 S2 have "(λ x. f1 (f2 x)) = sch_to_pr (Comp_op sch1 sch2)" by simp
    then show "∃sch. (λx. f1 (f2 x)) = sch_to_pr sch" by (rule exI)
  next
    fix f1 f2 assume B1: "∃sch. f1 = sch_to_pr sch" and B2: "∃sch. f2 = sch_to_pr sch"
    from B1 obtain sch1 where S1: "f1 = sch_to_pr sch1" ..
    from B2 obtain sch2 where S2: "f2 = sch_to_pr sch2" ..
    from S1 S2 have "c_f_pair f1 f2 = sch_to_pr (Pair_op sch1 sch2)" by simp
    then show "∃sch. c_f_pair f1 f2 = sch_to_pr sch" by (rule exI)
  next
    fix f1 f2 assume B1: "∃sch. f1 = sch_to_pr sch" and B2: "∃sch. f2 = sch_to_pr sch"
    from B1 obtain sch1 where S1: "f1 = sch_to_pr sch1" ..
    from B2 obtain sch2 where S2: "f2 = sch_to_pr sch2" ..
    from S1 S2 have "UnaryRecOp f1 f2 = sch_to_pr (Rec_op sch1 sch2)" by simp
    then show "∃sch. UnaryRecOp f1 f2 = sch_to_pr sch" by (rule exI)
  qed
qed

definition
  loc_f :: "nat ⇒ PrimScheme ⇒ PrimScheme ⇒ PrimScheme" where
  "loc_f n sch1 sch2 =
    (if n=0 then Base_zero else
     if n=1 then Base_suc else
     if n=2 then Base_fst else
     if n=3 then Base_snd else
     if n=4 then (Comp_op sch1 sch2) else
     if n=5 then (Pair_op sch1 sch2) else
     if n=6 then (Rec_op sch1 sch2) else
     Base_zero)"

definition
  mod7 :: "nat ⇒ nat" where
  "mod7 = (λ x. x mod 7)"

lemma c_snd_snd_lt [termination_simp]: "c_snd (c_snd (Suc (Suc x))) < Suc (Suc x)"
proof -
  let ?y = "Suc (Suc x)"
  have "?y > 1" by simp
  then have "c_snd ?y < ?y" by (rule c_snd_less_arg)
  moreover have "c_snd (c_snd ?y) ≤ c_snd ?y" by (rule c_snd_le_arg)
  ultimately show ?thesis by simp
qed

lemma c_fst_snd_lt [termination_simp]: "c_fst (c_snd (Suc (Suc x))) < Suc (Suc x)"
proof -
  let ?y = "Suc (Suc x)"
  have "?y > 1" by simp
  then have "c_snd ?y < ?y" by (rule c_snd_less_arg)
  moreover have "c_fst (c_snd ?y) ≤ c_snd ?y" by (rule c_fst_le_arg)
  ultimately show ?thesis by simp
qed

fun nat_to_sch :: "nat ⇒ PrimScheme" where
  "nat_to_sch 0 = Base_zero"
| "nat_to_sch (Suc 0) = Base_zero"
| "nat_to_sch x = (let u=mod7 (c_fst x); v=c_snd x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)"

primrec sch_to_nat :: "PrimScheme ⇒ nat" where
  "sch_to_nat Base_zero = 0"
| "sch_to_nat Base_suc = c_pair 1 0"
| "sch_to_nat Base_fst = c_pair 2 0"
| "sch_to_nat Base_snd = c_pair 3 0"
| "sch_to_nat (Comp_op t1 t2) = c_pair 4 (c_pair (sch_to_nat t1) (sch_to_nat t2))"
| "sch_to_nat (Pair_op t1 t2) = c_pair 5 (c_pair (sch_to_nat t1) (sch_to_nat t2))"
| "sch_to_nat (Rec_op t1 t2)  = c_pair 6 (c_pair (sch_to_nat t1) (sch_to_nat t2))"

lemma loc_srj_lm_1: "nat_to_sch (Suc (Suc x)) = (let u=mod7 (c_fst (Suc (Suc x))); v=c_snd (Suc (Suc x)); v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by simp

lemma loc_srj_lm_2: "x > 1 ⟹ nat_to_sch x = (let u=mod7 (c_fst x); v=c_snd x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)"
proof -
  assume A1: "x > 1"
  let ?y = "x-(2::nat)"
  from A1 have S1: "x = Suc (Suc ?y)" by arith
  have S2: "nat_to_sch (Suc (Suc ?y)) = (let u=mod7 (c_fst (Suc (Suc ?y))); v=c_snd (Suc (Suc ?y)); v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by (rule loc_srj_lm_1)
  from S1 S2 show ?thesis by simp
qed

lemma loc_srj_0: "nat_to_sch (c_pair 1 0) = Base_suc"
proof -
  let ?x = "c_pair 1 0"
  have S1: "?x = 2" by (simp add: c_pair_def sf_def)
  then have S2: "?x = Suc (Suc 0)" by simp
  let ?y = "Suc (Suc 0)"
  have S3: "nat_to_sch ?y = (let u=mod7 (c_fst ?y); v=c_snd ?y; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" (is "_ = ?R") by (rule loc_srj_lm_1)
  have S4: "c_fst ?y = 1"
  proof -
    from S2 have "c_fst ?y = c_fst ?x" by simp
    then show ?thesis by simp
  qed
  have S5: "c_snd ?y = 0"
  proof -
    from S2 have "c_snd ?y = c_snd ?x" by simp
    then show ?thesis by simp
  qed
  from S4 have S6: "mod7 (c_fst ?y) = 1" by (simp add: mod7_def)
  from S3 S5 S6 have S9: "?R = loc_f 1 Base_zero Base_zero" by (simp add: Let_def c_fst_at_0 c_snd_at_0)
  then have S10: "?R = Base_suc" by (simp add: loc_f_def)
  with S3 have S11: "nat_to_sch ?y = Base_suc" by simp
  from S2 this show ?thesis by simp
qed

lemma nat_to_sch_at_2: "nat_to_sch 2 = Base_suc"
proof -
  have S1: "c_pair 1 0 = 2" by (simp add: c_pair_def sf_def)
  have S2: "nat_to_sch (c_pair 1 0) = Base_suc" by (rule loc_srj_0)
  from S1 S2 show ?thesis by simp
qed

lemma loc_srj_1: "nat_to_sch (c_pair 2 0) = Base_fst"
proof -
  let ?x = "c_pair 2 0"
  have S1: "?x = 5" by (simp add: c_pair_def sf_def)
  then have S2: "?x = Suc (Suc 3)" by simp
  let ?y = "Suc (Suc 3)"
  have S3: "nat_to_sch ?y = (let u=mod7 (c_fst ?y); v=c_snd ?y; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" (is "_ = ?R") by (rule loc_srj_lm_1)
  have S4: "c_fst ?y = 2"
  proof -
    from S2 have "c_fst ?y = c_fst ?x" by simp
    then show ?thesis by simp
  qed
  have S5: "c_snd ?y = 0"
  proof -
    from S2 have "c_snd ?y = c_snd ?x" by simp
    then show ?thesis by simp
  qed
  from S4 have S6: "mod7 (c_fst ?y) = 2" by (simp add: mod7_def)
  from S3 S5 S6 have S9: "?R = loc_f 2 Base_zero Base_zero" by (simp add: Let_def c_fst_at_0 c_snd_at_0)
  then have S10: "?R = Base_fst" by (simp add: loc_f_def)
  with S3 have S11: "nat_to_sch ?y = Base_fst" by simp
  from S2 this show ?thesis by simp
qed

lemma loc_srj_2: "nat_to_sch (c_pair 3 0) = Base_snd"
proof -
  let ?x = "c_pair 3 0"
  have S1: "?x > 1" by (simp add: c_pair_def sf_def)
  from S1 have S2: "nat_to_sch ?x = (let u=mod7 (c_fst ?x); v=c_snd ?x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" (is "_ = ?R") by (rule loc_srj_lm_2)
  have S3: "c_fst ?x = 3" by simp
  have S4: "c_snd ?x = 0" by simp
  from S3 have S6: "mod7 (c_fst ?x) = 3" by (simp add: mod7_def)
  from S3 S4 S6 have S7: "?R = loc_f 3 Base_zero Base_zero" by (simp add: Let_def c_fst_at_0 c_snd_at_0)
  then have S8: "?R = Base_snd" by (simp add: loc_f_def)
  with S2 have S10: "nat_to_sch ?x = Base_snd" by simp
  from S2 this show ?thesis by simp
qed

lemma loc_srj_3: "⟦nat_to_sch (sch_to_nat sch1) = sch1; nat_to_sch (sch_to_nat sch2) = sch2⟧
       ⟹ nat_to_sch (c_pair 4 (c_pair (sch_to_nat sch1) (sch_to_nat sch2))) = Comp_op sch1 sch2"
proof -
  assume A1: "nat_to_sch (sch_to_nat sch1) = sch1"
  assume A2: "nat_to_sch (sch_to_nat sch2) = sch2"
  let ?x = "c_pair 4 (c_pair (sch_to_nat sch1) (sch_to_nat sch2))"
  have S1: "?x > 1" by (simp add: c_pair_def sf_def)
  from S1 have S2: "nat_to_sch ?x = (let u=mod7 (c_fst ?x); v=c_snd ?x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" (is "_ = ?R") by (rule loc_srj_lm_2)
  have S3: "c_fst ?x = 4" by simp
  have S4: "c_snd ?x = c_pair (sch_to_nat sch1) (sch_to_nat sch2)" by simp
  from S3 have S5: "mod7 (c_fst ?x) = 4" by (simp add: mod7_def)
  from A1 A2 S4 S5 have "?R = Comp_op sch1 sch2" by (simp add: Let_def c_fst_at_0 c_snd_at_0 loc_f_def)
  with S2 show ?thesis by simp
qed

lemma loc_srj_3_1: "nat_to_sch (c_pair 4 (c_pair n1 n2)) = Comp_op (nat_to_sch n1) (nat_to_sch n2)"
proof -
  let ?x = "c_pair 4 (c_pair n1 n2)"
  have S1: "?x > 1" by (simp add: c_pair_def sf_def)
  from S1 have S2: "nat_to_sch ?x = (let u=mod7 (c_fst ?x); v=c_snd ?x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" (is "_ = ?R") by (rule loc_srj_lm_2)
  have S3: "c_fst ?x = 4" by simp
  have S4: "c_snd ?x = c_pair n1 n2" by simp
  from S3 have S5: "mod7 (c_fst ?x) = 4" by (simp add: mod7_def)
  from S4 S5 have "?R = Comp_op (nat_to_sch n1) (nat_to_sch n2)" by (simp add: Let_def c_fst_at_0 c_snd_at_0 loc_f_def)
  with S2 show ?thesis by simp
qed

lemma loc_srj_4: "⟦nat_to_sch (sch_to_nat sch1) = sch1; nat_to_sch (sch_to_nat sch2) = sch2⟧
       ⟹ nat_to_sch (c_pair 5 (c_pair (sch_to_nat sch1) (sch_to_nat sch2))) = Pair_op sch1 sch2"
proof -
  assume A1: "nat_to_sch (sch_to_nat sch1) = sch1"
  assume A2: "nat_to_sch (sch_to_nat sch2) = sch2"
  let ?x = "c_pair 5 (c_pair (sch_to_nat sch1) (sch_to_nat sch2))"
  have S1: "?x > 1" by (simp add: c_pair_def sf_def)
  from S1 have S2: "nat_to_sch ?x = (let u=mod7 (c_fst ?x); v=c_snd ?x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" (is "_ = ?R") by (rule loc_srj_lm_2)
  have S3: "c_fst ?x = 5" by simp
  have S4: "c_snd ?x = c_pair (sch_to_nat sch1) (sch_to_nat sch2)" by simp
  from S3 have S5: "mod7 (c_fst ?x) = 5" by (simp add: mod7_def)
  from A1 A2 S4 S5 have "?R = Pair_op sch1 sch2" by (simp add: Let_def c_fst_at_0 c_snd_at_0 loc_f_def)
  with S2 show ?thesis by simp
qed

lemma loc_srj_4_1: "nat_to_sch (c_pair 5 (c_pair n1 n2)) = Pair_op (nat_to_sch n1) (nat_to_sch n2)"
proof -
  let ?x = "c_pair 5 (c_pair n1 n2)"
  have S1: "?x > 1" by (simp add: c_pair_def sf_def)
  from S1 have S2: "nat_to_sch ?x = (let u=mod7 (c_fst ?x); v=c_snd ?x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" (is "_ = ?R") by (rule loc_srj_lm_2)
  have S3: "c_fst ?x = 5" by simp
  have S4: "c_snd ?x = c_pair n1 n2" by simp
  from S3 have S5: "mod7 (c_fst ?x) = 5" by (simp add: mod7_def)
  from S4 S5 have "?R = Pair_op (nat_to_sch n1) (nat_to_sch n2)" by (simp add: Let_def c_fst_at_0 c_snd_at_0 loc_f_def)
  with S2 show ?thesis by simp
qed

lemma loc_srj_5: "⟦nat_to_sch (sch_to_nat sch1) = sch1; nat_to_sch (sch_to_nat sch2) = sch2⟧
       ⟹ nat_to_sch (c_pair 6 (c_pair (sch_to_nat sch1) (sch_to_nat sch2))) = Rec_op sch1 sch2"
proof -
  assume A1: "nat_to_sch (sch_to_nat sch1) = sch1"
  assume A2: "nat_to_sch (sch_to_nat sch2) = sch2"
  let ?x = "c_pair 6 (c_pair (sch_to_nat sch1) (sch_to_nat sch2))"
  have S1: "?x > 1" by (simp add: c_pair_def sf_def)
  from S1 have S2: "nat_to_sch ?x = (let u=mod7 (c_fst ?x); v=c_snd ?x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" (is "_ = ?R") by (rule loc_srj_lm_2)
  have S3: "c_fst ?x = 6" by simp
  have S4: "c_snd ?x = c_pair (sch_to_nat sch1) (sch_to_nat sch2)" by simp
  from S3 have S5: "mod7 (c_fst ?x) = 6" by (simp add: mod7_def)
  from A1 A2 S4 S5 have "?R = Rec_op sch1 sch2" by (simp add: Let_def c_fst_at_0 c_snd_at_0 loc_f_def)
  with S2 show ?thesis by simp
qed

lemma loc_srj_5_1: "nat_to_sch (c_pair 6 (c_pair n1 n2)) = Rec_op (nat_to_sch n1) (nat_to_sch n2)"
proof -
  let ?x = "c_pair 6 (c_pair n1 n2)"
  have S1: "?x > 1" by (simp add: c_pair_def sf_def)
  from S1 have S2: "nat_to_sch ?x = (let u=mod7 (c_fst ?x); v=c_snd ?x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" (is "_ = ?R") by (rule loc_srj_lm_2)
  have S3: "c_fst ?x = 6" by simp
  have S4: "c_snd ?x = c_pair n1 n2" by simp
  from S3 have S5: "mod7 (c_fst ?x) = 6" by (simp add: mod7_def)
  from S4 S5 have "?R = Rec_op (nat_to_sch n1) (nat_to_sch n2)" by (simp add: Let_def c_fst_at_0 c_snd_at_0 loc_f_def)
  with S2 show ?thesis by simp
qed

theorem nat_to_sch_srj: "nat_to_sch (sch_to_nat sch) = sch"
apply(induct sch, auto simp add: loc_srj_0 loc_srj_1 loc_srj_2 loc_srj_3 loc_srj_4 loc_srj_5)
apply(insert loc_srj_0)
apply(simp)
done

subsection ‹Indexes of primitive recursive functions of one variables›

definition
  nat_to_pr :: "nat ⇒ (nat ⇒ nat)" where
  "nat_to_pr = (λ x. sch_to_pr (nat_to_sch x))"

theorem nat_to_pr_into_pr: "nat_to_pr n ∈ PrimRec1" by (simp add: nat_to_pr_def sch_to_pr_into_pr)

lemma nat_to_pr_srj: "f ∈ PrimRec1 ⟹ (∃ n. f = nat_to_pr n)"
proof -
  assume "f ∈ PrimRec1"
  then have S1: "(∃ t. f = sch_to_pr t)" by (rule sch_to_pr_srj)
  from S1 obtain t where S2: "f = sch_to_pr t" ..
  let ?n = "sch_to_nat t"
  have S3: "nat_to_pr ?n = sch_to_pr (nat_to_sch ?n)" by (simp add: nat_to_pr_def)
  have S4: "nat_to_sch ?n = t" by (rule nat_to_sch_srj)
  from S3 S4 have S5: "nat_to_pr ?n = sch_to_pr t" by simp
  from S2 S5 have "nat_to_pr ?n = f" by simp
  then have "f = nat_to_pr ?n" by simp
  then show ?thesis ..
qed

lemma nat_to_pr_at_0: "nat_to_pr 0 = (λ x. 0)" by (simp add: nat_to_pr_def)

definition
  index_of_pr :: "(nat ⇒ nat) ⇒ nat" where
  "index_of_pr f = (SOME n. f = nat_to_pr n)"

theorem index_of_pr_is_real: "f ∈ PrimRec1 ⟹ nat_to_pr (index_of_pr f) = f"
proof -
  assume "f ∈ PrimRec1"
  hence "∃ n. f = nat_to_pr n" by (rule nat_to_pr_srj)
  hence "f = nat_to_pr (SOME n. f = nat_to_pr n)" by (rule someI_ex)
  thus ?thesis by (simp add: index_of_pr_def)
qed

definition
  comp_by_index :: "nat ⇒ nat ⇒ nat" where
  "comp_by_index = (λ n1 n2. c_pair 4 (c_pair n1 n2))"

definition
  pair_by_index :: "nat ⇒ nat ⇒ nat" where
  "pair_by_index = (λ n1 n2. c_pair 5 (c_pair n1 n2))"

definition
  rec_by_index :: "nat ⇒ nat ⇒ nat" where
  "rec_by_index = (λ n1 n2. c_pair 6 (c_pair n1 n2))"

lemma comp_by_index_is_pr: "comp_by_index ∈ PrimRec2"
  unfolding comp_by_index_def
  using const_is_pr_2 [of 4] by prec

lemma comp_by_index_inj: "comp_by_index x1 y1 = comp_by_index x2 y2 ⟹ x1=x2 ∧ y1=y2"
proof -
  assume "comp_by_index x1 y1 = comp_by_index x2 y2"
  hence "c_pair 4 (c_pair x1 y1) = c_pair 4 (c_pair x2 y2)" by (unfold comp_by_index_def)
  hence "c_pair x1 y1 = c_pair x2 y2" by (rule c_pair_inj2)
  thus ?thesis by (rule c_pair_inj)
qed

lemma comp_by_index_inj1: "comp_by_index x1 y1 = comp_by_index x2 y2 ⟹ x1 = x2" by (frule comp_by_index_inj, drule conjunct1)

lemma comp_by_index_inj2: "comp_by_index x1 y1 = comp_by_index x2 y2 ⟹ y1 = y2" by (frule comp_by_index_inj, drule conjunct2)

lemma comp_by_index_main: "nat_to_pr (comp_by_index n1 n2) = (λ x. (nat_to_pr n1) ((nat_to_pr n2) x))" by (unfold comp_by_index_def, unfold nat_to_pr_def, simp add: loc_srj_3_1)

lemma pair_by_index_is_pr: "pair_by_index ∈ PrimRec2" by (unfold pair_by_index_def, insert const_is_pr_2 [where ?n="(5::nat)"], prec)

lemma pair_by_index_inj: "pair_by_index x1 y1 = pair_by_index x2 y2 ⟹ x1=x2 ∧ y1=y2"
proof -
  assume "pair_by_index x1 y1 = pair_by_index x2 y2"
  hence "c_pair 5 (c_pair x1 y1) = c_pair 5 (c_pair x2 y2)" by (unfold pair_by_index_def)
  hence "c_pair x1 y1 = c_pair x2 y2" by (rule c_pair_inj2)
  thus ?thesis by (rule c_pair_inj)
qed

lemma pair_by_index_inj1: "pair_by_index x1 y1 = pair_by_index x2 y2 ⟹ x1 = x2" by (frule pair_by_index_inj, drule conjunct1)

lemma pair_by_index_inj2: "pair_by_index x1 y1 = pair_by_index x2 y2 ⟹ y1 = y2" by (frule pair_by_index_inj, drule conjunct2)

lemma pair_by_index_main: "nat_to_pr (pair_by_index n1 n2) = c_f_pair (nat_to_pr n1) (nat_to_pr n2)" by (unfold pair_by_index_def, unfold nat_to_pr_def, simp add: loc_srj_4_1)

lemma nat_to_sch_of_pair_by_index [simp]: "nat_to_sch (pair_by_index n1 n2) = Pair_op (nat_to_sch n1) (nat_to_sch n2)"
  by (simp add: pair_by_index_def loc_srj_4_1)

lemma rec_by_index_is_pr: "rec_by_index ∈ PrimRec2" by (unfold rec_by_index_def, insert const_is_pr_2 [where ?n="(6::nat)"], prec)

lemma rec_by_index_inj: "rec_by_index x1 y1 = rec_by_index x2 y2 ⟹ x1=x2 ∧ y1=y2"
proof -
  assume "rec_by_index x1 y1 = rec_by_index x2 y2"
  hence "c_pair 6 (c_pair x1 y1) = c_pair 6 (c_pair x2 y2)" by (unfold rec_by_index_def)
  hence "c_pair x1 y1 = c_pair x2 y2" by (rule c_pair_inj2)
  thus ?thesis by (rule c_pair_inj)
qed

lemma rec_by_index_inj1: "rec_by_index x1 y1 = rec_by_index x2 y2 ⟹ x1 = x2" by (frule rec_by_index_inj, drule conjunct1)

lemma rec_by_index_inj2: "rec_by_index x1 y1 = rec_by_index x2 y2 ⟹ y1 = y2" by (frule rec_by_index_inj, drule conjunct2)

lemma rec_by_index_main: "nat_to_pr (rec_by_index n1 n2) = UnaryRecOp (nat_to_pr n1) (nat_to_pr n2)" by (unfold rec_by_index_def, unfold nat_to_pr_def, simp add: loc_srj_5_1)

subsection ‹s-1-1 theorem for primitive recursive functions of one variable›

definition
  index_of_const :: "nat ⇒ nat" where
  "index_of_const = PrimRecOp1 0 (λ x y. c_pair 4 (c_pair 2 y))"

lemma index_of_const_is_pr: "index_of_const ∈ PrimRec1"
proof -
  have "(λ x y. c_pair (4::nat) (c_pair (2::nat) y)) ∈ PrimRec2" by (insert const_is_pr_2 [where ?n="(4::nat)"], prec)
  then show ?thesis by (simp add: index_of_const_def pr_rec1)
qed

lemma index_of_const_at_0: "index_of_const 0 = 0" by (simp add: index_of_const_def)

lemma index_of_const_at_suc: "index_of_const (Suc u) = c_pair 4 (c_pair 2 (index_of_const u))" by (unfold index_of_const_def, induct u, auto)

lemma index_of_const_main: "nat_to_pr (index_of_const n) = (λ x. n)" (is "?P n")
proof (induct n)
  show "?P 0" by (simp add: index_of_const_at_0 nat_to_pr_at_0)
next
  fix n assume "?P n"
  then show "?P (Suc n)" by ((simp add: index_of_const_at_suc nat_to_sch_at_2 nat_to_pr_def loc_srj_3_1))
qed

lemma index_of_const_lm_1: "(nat_to_pr (index_of_const n)) 0 = n" by (simp add: index_of_const_main)

lemma index_of_const_inj: "index_of_const n1 = index_of_const n2 ⟹ n1 = n2"
proof -
  assume "index_of_const n1 = index_of_const n2"
  then have "(nat_to_pr (index_of_const n1)) 0  = (nat_to_pr (index_of_const n2)) 0" by simp
  thus ?thesis by (simp add: index_of_const_lm_1)
qed

definition "index_of_zero = sch_to_nat Base_zero"
definition "index_of_suc = sch_to_nat Base_suc"
definition "index_of_c_fst = sch_to_nat Base_fst"
definition "index_of_c_snd = sch_to_nat Base_snd"
definition "index_of_id = pair_by_index index_of_c_fst index_of_c_snd"

lemma index_of_zero_main: "nat_to_pr index_of_zero = (λ x. 0)" by (simp add: index_of_zero_def nat_to_pr_def)

lemma index_of_suc_main: "nat_to_pr index_of_suc = Suc"
apply(simp add: index_of_suc_def nat_to_pr_def)
apply(insert loc_srj_0)
apply(simp)
done

lemma index_of_c_fst_main: "nat_to_pr index_of_c_fst = c_fst" by (simp add: index_of_c_fst_def nat_to_pr_def loc_srj_1)

lemma [simp]: "nat_to_sch index_of_c_fst = Base_fst" by (unfold index_of_c_fst_def, rule nat_to_sch_srj)

lemma index_of_c_snd_main: "nat_to_pr index_of_c_snd = c_snd" by (simp add: index_of_c_snd_def nat_to_pr_def loc_srj_2)

lemma [simp]: "nat_to_sch index_of_c_snd = Base_snd" by (unfold index_of_c_snd_def, rule nat_to_sch_srj)

lemma index_of_id_main: "nat_to_pr index_of_id = (λ x. x)" by (simp add: index_of_id_def nat_to_pr_def c_f_pair_def)

definition
  index_of_c_pair_n :: "nat ⇒ nat" where
  "index_of_c_pair_n = (λ n. pair_by_index (index_of_const n) index_of_id)"

lemma index_of_c_pair_n_is_pr: "index_of_c_pair_n ∈ PrimRec1"
proof -
  have "(λ x. index_of_id) ∈ PrimRec1" by (rule const_is_pr)
  with pair_by_index_is_pr index_of_const_is_pr have "(λ n. pair_by_index (index_of_const n) index_of_id) ∈ PrimRec1" by prec
  then show ?thesis by (fold index_of_c_pair_n_def)
qed

lemma index_of_c_pair_n_main: "nat_to_pr (index_of_c_pair_n n) = (λ x. c_pair n x)"
proof -
  have "nat_to_pr (index_of_c_pair_n n) = nat_to_pr (pair_by_index (index_of_const n) index_of_id)" by (simp add: index_of_c_pair_n_def)
  also have "… = c_f_pair (nat_to_pr (index_of_const n)) (nat_to_pr index_of_id)" by (simp add: pair_by_index_main)
  also have "… = c_f_pair (λ x. n) (λ x. x)" by (simp add: index_of_const_main index_of_id_main)
  finally show ?thesis by (simp add: c_f_pair_def)
qed

lemma index_of_c_pair_n_inj: "index_of_c_pair_n x1 = index_of_c_pair_n x2 ⟹ x1=x2"
proof -
  assume "index_of_c_pair_n x1 = index_of_c_pair_n x2"
  hence "pair_by_index (index_of_const x1) index_of_id = pair_by_index (index_of_const x2) index_of_id" by (unfold index_of_c_pair_n_def)
  hence "index_of_const x1 = index_of_const x2" by (rule pair_by_index_inj1)
  thus ?thesis by (rule index_of_const_inj)
qed

definition
  s1_1 :: "nat ⇒ nat ⇒ nat" where
  "s1_1 = (λ n x. comp_by_index n (index_of_c_pair_n x))"

lemma s1_1_is_pr: "s1_1 ∈ PrimRec2" by (unfold s1_1_def, insert comp_by_index_is_pr index_of_c_pair_n_is_pr, prec)

theorem s1_1_th: "(λ y. (nat_to_pr n) (c_pair x y)) = nat_to_pr (s1_1 n x)"
proof -
  have "nat_to_pr (s1_1 n x) = nat_to_pr (comp_by_index n (index_of_c_pair_n x))" by (simp add: s1_1_def)
  also have "… = (λ z. (nat_to_pr n) ((nat_to_pr (index_of_c_pair_n x)) z))" by (simp add: comp_by_index_main)
  also have "… = (λ z. (nat_to_pr n) ((λ u. c_pair x u) z))" by (simp add: index_of_c_pair_n_main)
  finally show ?thesis by simp
qed

lemma s1_1_inj: "s1_1 x1 y1 = s1_1 x2 y2 ⟹ x1=x2 ∧ y1=y2"
proof -
  assume "s1_1 x1 y1 = s1_1 x2 y2"
  then have "comp_by_index x1 (index_of_c_pair_n y1) = comp_by_index x2 (index_of_c_pair_n y2)" by (unfold s1_1_def)
  then have S1: "x1=x2 ∧ index_of_c_pair_n y1 = index_of_c_pair_n y2" by (rule comp_by_index_inj)
  then have S2: "x1=x2" ..
  from S1 have "index_of_c_pair_n y1 = index_of_c_pair_n y2" ..
  then have "y1 = y2" by (rule index_of_c_pair_n_inj)
  with S2 show ?thesis ..
qed

lemma s1_1_inj1: "s1_1 x1 y1 = s1_1 x2 y2 ⟹ x1=x2" by (frule s1_1_inj, drule conjunct1)

lemma s1_1_inj2: "s1_1 x1 y1 = s1_1 x2 y2 ⟹ y1=y2" by (frule s1_1_inj, drule conjunct2)

primrec
  pr_index_enumerator :: "nat ⇒ nat ⇒ nat"
where
  "pr_index_enumerator n 0 = n"
| "pr_index_enumerator n (Suc m) = comp_by_index index_of_id (pr_index_enumerator n m)"

theorem pr_index_enumerator_is_pr: "pr_index_enumerator ∈ PrimRec2"
proof -
  define g where "g x = x" for x :: nat
  have g_is_pr: "g ∈ PrimRec1" by (unfold g_def, rule pr_id1_1)
  define h where "h a b c = comp_by_index index_of_id b" for a b c :: nat
  from comp_by_index_is_pr have h_is_pr: "h ∈ PrimRec3" unfolding h_def by prec
  let ?f = "pr_index_enumerator"
  from g_def have f_at_0: "∀ x. ?f x 0 = g x" by auto
  from h_def have f_at_Suc: "∀ x y. ?f x (Suc y) = h x (?f x y) y" by auto
  from g_is_pr h_is_pr f_at_0 f_at_Suc show ?thesis by (rule pr_rec_last_scheme)
qed

lemma pr_index_enumerator_increase1: "pr_index_enumerator n m < pr_index_enumerator (n+1) m"
proof (induct m)
  show "pr_index_enumerator n 0 < pr_index_enumerator (n + 1) 0" by simp
  next fix na assume A: "pr_index_enumerator n na < pr_index_enumerator (n + 1) na"
  show "pr_index_enumerator n (Suc na) < pr_index_enumerator (n + 1) (Suc na)"
  proof -
    let ?a = "pr_index_enumerator n na"
    let ?b = "pr_index_enumerator (n+1) na"
    have S1: "pr_index_enumerator n (Suc na) = comp_by_index index_of_id ?a" by simp
    have L1: "pr_index_enumerator (n+1) (Suc na) = comp_by_index index_of_id ?b" by simp
    from A have "c_pair index_of_id ?a < c_pair index_of_id ?b" by (rule c_pair_strict_mono2)
    then have "c_pair 4 (c_pair index_of_id ?a) < c_pair 4 (c_pair index_of_id ?b)" by (rule c_pair_strict_mono2)
    then have "comp_by_index index_of_id ?a < c_pair 4 (c_pair index_of_id ?b)" by (simp add: comp_by_index_def)
    then have "comp_by_index index_of_id ?a < comp_by_index index_of_id ?b" by (simp add: comp_by_index_def)
    with S1 L1 show ?thesis by auto
  qed
qed

lemma pr_index_enumerator_increase2: "pr_index_enumerator n m < pr_index_enumerator n (m + 1)"
proof -
  let ?a = "pr_index_enumerator n m"
  have S1: "pr_index_enumerator n (m + 1) = comp_by_index index_of_id ?a" by simp
  have S2: "comp_by_index index_of_id ?a = c_pair 4 (c_pair index_of_id ?a)" by (simp add: comp_by_index_def)
  have S3: "4 + c_pair index_of_id ?a ≤ c_pair 4 (c_pair index_of_id ?a)" by (rule sum_le_c_pair)
  then have S4: "c_pair index_of_id ?a < c_pair 4 (c_pair index_of_id ?a)" by auto
  have S5: "?a ≤ c_pair index_of_id ?a" by (rule arg2_le_c_pair)
  from S4 S5 have S6: "?a < c_pair 4 (c_pair index_of_id ?a)" by auto
  with S1 S2 show ?thesis by auto
qed

lemma f_inc_mono: "(∀ (x::nat). (f::nat⇒nat) x < f (x+1)) ⟹ ∀ (x::nat) (y::nat). (x < y ⟶ f x < f y)"
proof (rule allI, rule allI)
  fix x y assume A: "∀ (x::nat). f x < f (x+1)" show " x < y ⟶ f x < f y"
  proof
    assume A1: "x < y"
    have L1: "⋀ u v. f u < f (u + (v+1))"
    proof -
      fix u v show "f u < f (u + (v+1))"
      proof (induct v)
        from A show "f u < f (u + (0 + 1))" by auto
      next
        fix v n
        assume A2: "f u < f (u + (n + 1))"
        from A have S1: "f (u + (n + 1)) < f (u + (Suc n + 1))" by auto
        from A2 S1 show " f u < f (u + (Suc n + 1))" by (rule less_trans)
      qed
    qed
  let ?v = "(y - x) - 1"
  from A1 have S2: "y = x + (?v + 1)" by auto
  have "f x < f (x + (?v + 1))" by (rule L1)
  with S2 show "f x < f y" by auto
  qed
qed

lemma pr_index_enumerator_mono1: "n1 < n2 ⟹ pr_index_enumerator n1 m < pr_index_enumerator n2 m"
proof -
  assume A: "n1 < n2"
  define f where "f x = pr_index_enumerator x m" for x
  have f_inc: "∀ x. f x < f (x+1)"
  proof
    fix x show "f x < f (x+1)" by (unfold f_def, rule pr_index_enumerator_increase1)
  qed
  from f_inc have "∀ x y. (x < y ⟶ f x < f y)" by (rule f_inc_mono)
  with A f_def show ?thesis by auto
qed

lemma pr_index_enumerator_mono2: "m1 < m2 ⟹ pr_index_enumerator n m1 < pr_index_enumerator n m2"
proof -
  assume A: "m1 < m2"
  define f where "f x = pr_index_enumerator n x" for x
  have f_inc: "∀ x. f x < f (x+1)"
  proof
    fix x show "f x < f (x+1)" by (unfold f_def, rule pr_index_enumerator_increase2)
  qed
  from f_inc have "∀ x y. (x < y ⟶ f x < f y)" by (rule f_inc_mono)
  with A f_def show ?thesis by auto
qed

lemma f_mono_inj: "∀ (x::nat) (y::nat). (x < y ⟶ (f::nat⇒nat) x < f y) ⟹ ∀ (x::nat) (y::nat). (f x = f y ⟶ x = y)"
proof (rule allI, rule allI)
  fix x y assume A: "∀x y. x < y ⟶ f x < f y" show "f x = f y ⟶ x = y"
  proof
    assume A1: "f x = f y" show "x = y"
    proof (rule ccontr)
      assume A2: "x ≠ y" show False
      proof cases
        assume A3: "x < y"
        from A A3 have "f x < f y" by auto
        with A1 show False by auto
      next
        assume "¬ x < y" with A2 have A4: "y < x" by auto
        from A A4 have "f y < f x" by auto
        with A1 show False by auto
      qed
    qed
  qed
qed

theorem pr_index_enumerator_inj1: "pr_index_enumerator n1 m = pr_index_enumerator n2 m ⟹ n1 = n2"
proof -
  assume A: "pr_index_enumerator n1 m = pr_index_enumerator n2 m"
  define f where "f x = pr_index_enumerator x m" for x
  have f_mono: "∀ x y. (x < y ⟶ f x < f y)"
  proof (rule allI, rule allI)
    fix x y show "x < y ⟶ f x < f y" by (unfold f_def, simp add: pr_index_enumerator_mono1)
  qed
  from f_mono have "∀ x y. (f x = f y ⟶ x = y)" by (rule f_mono_inj)
  with A f_def show ?thesis by auto
qed

theorem pr_index_enumerator_inj2: "pr_index_enumerator n m1 = pr_index_enumerator n m2 ⟹ m1 = m2"
proof -
  assume A: "pr_index_enumerator n m1 = pr_index_enumerator n m2"
  define f where "f x = pr_index_enumerator n x" for x
  have f_mono: "∀ x y. (x < y ⟶ f x < f y)"
  proof (rule allI, rule allI)
    fix x y show "x < y ⟶ f x < f y" by (unfold f_def, simp add: pr_index_enumerator_mono2)
  qed
  from f_mono have "∀ x y. (f x = f y ⟶ x = y)" by (rule f_mono_inj)
  with A f_def show ?thesis by auto
qed

theorem pr_index_enumerator_main: "nat_to_pr n = nat_to_pr (pr_index_enumerator n m)"
proof (induct m)
  show "nat_to_pr n = nat_to_pr (pr_index_enumerator n 0)" by simp
next
  fix na assume A: "nat_to_pr n = nat_to_pr (pr_index_enumerator n na)"
  show "nat_to_pr n = nat_to_pr (pr_index_enumerator n (Suc na))"
  proof -
    let ?a = "pr_index_enumerator n na"
    have S1: "pr_index_enumerator n (Suc na) = comp_by_index index_of_id ?a" by simp
    have "nat_to_pr (comp_by_index index_of_id ?a) = (λ x. (nat_to_pr index_of_id) (nat_to_pr ?a x))" by (rule comp_by_index_main)
    with index_of_id_main have "nat_to_pr (comp_by_index index_of_id ?a) = nat_to_pr ?a" by simp
    with A S1 show ?thesis by simp
  qed
qed

end