# Theory PRecFun2

Up to index of Isabelle/HOL/Recursion-Theory-I

theory PRecFun2
imports PRecFun
`(*  Title:       Primitive recursive functions of one variable    Author:      Michael Nedzelsky <MichaelNedzelsky at yandex.ru>, 2008    Maintainer:  Michael Nedzelsky <MichaelNedzelsky at yandex.ru>*)header {* Primitive recursive functions of one variable *}theory PRecFun2imports PRecFunbeginsubsection {* 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 precinductive_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)qedlemma 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 simpqedlemma 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 simpqedlemma 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 simpqedlemma 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)qedlemma 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 simpqedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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 simpqedtheorem 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 blastqedsubsection {* The scheme datatype *}datatype PrimScheme = Base_zero | Base_suc | Base_fst | Base_snd                      | Comp_op PrimScheme PrimScheme                      | Pair_op PrimScheme PrimScheme                      | Rec_op PrimScheme PrimSchemeprimrec  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)  qedqeddefinition  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 simpqedlemma 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 simpqedfun 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 simplemma 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 simpqedlemma 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 simpqedlemma 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 simpqedlemma 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 simpqedlemma 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 simpqedlemma 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 simpqedlemma 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 simpqedlemma 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 simpqedlemma 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 simpqedlemma 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 simpqedlemma 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 simpqedtheorem 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)donesubsection {* 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 ..qedlemma 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)qeddefinition  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 preclemma 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)qedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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))qedlemma 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)qeddefinition "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)donelemma 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)qedlemma 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)qedlemma 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)qeddefinition  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 simpqedlemma 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 ..qedlemma 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 -  def g_def: g ≡ "λ (x::nat). x"  have g_is_pr: "g ∈ PrimRec1" by (unfold g_def, rule pr_id1_1)  def h_def: h ≡ "λ (a::nat) b (c::nat). comp_by_index index_of_id b"  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)qedlemma 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  qedqedlemma 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 autoqedlemma 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  qedqedlemma pr_index_enumerator_mono1: "n1 < n2 ==> pr_index_enumerator n1 m < pr_index_enumerator n2 m"proof -  assume A: "n1 < n2"  def f_def: f ≡ "λ x. pr_index_enumerator x m"  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 autoqedlemma pr_index_enumerator_mono2: "m1 < m2 ==> pr_index_enumerator n m1 < pr_index_enumerator n m2"proof -  assume A: "m1 < m2"  def f_def: f ≡ "λ x. pr_index_enumerator n 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 autoqedlemma 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  qedqedtheorem 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"  def f_def: f ≡ "λ x. pr_index_enumerator x m"  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 autoqedtheorem 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"  def f_def: f ≡ "λ x. pr_index_enumerator n 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 autoqedtheorem 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 simpnext  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  qedqedend`