# Theory CPair

(*  Title:       Defintion and basics facts about Cantor pairing function
Author:      Michael Nedzelsky <MichaelNedzelsky at yandex.ru>, 2008
Maintainer:  Michael Nedzelsky <MichaelNedzelsky at yandex.ru>
*)

section ‹Cantor pairing function›

theory CPair
imports Main
begin

text ‹
We introduce a particular coding ‹c_pair› from ordered pairs
of natural numbers to natural numbers.  See \cite{Rogers} and the
›

subsection ‹Pairing function›

definition
sf :: "nat ⇒ nat" where
sf_def: "sf x = x * (x+1) div 2"

definition
c_pair :: "nat ⇒ nat ⇒ nat" where
"c_pair x y = sf (x+y) + x"

lemma sf_at_0: "sf 0 = 0" by (simp add: sf_def)

lemma sf_at_1: "sf 1 = 1" by (simp add: sf_def)

lemma sf_at_Suc: "sf (x+1) = sf x + x + 1"
proof -
have S1: "sf(x+1) = ((x+1)*(x+2)) div 2" by (simp add: sf_def)
have S2: "(x+1)*(x+2) = x*(x+1) + 2*(x+1)" by (auto)
have S2_1: "⋀ x y. x=y ⟹ x div 2 = y div 2" by auto
from S2 have S3: "(x+1)*(x+2) div 2 = (x*(x+1) + 2*(x+1)) div 2" by (rule S2_1)
have S4: "(0::nat) < 2" by (auto)
from S4 have S5: "(x*(x+1) + 2*(x+1)) div 2 = (x+1) + x*(x+1) div 2" by simp
from S1 S3 S5 show ?thesis by (simp add: sf_def)
qed

lemma arg_le_sf: "x ≤ sf x"
proof -
have "x + x ≤ x*(x + 1)" by simp
hence "(x + x) div 2 ≤ x*(x+1) div 2" by (rule div_le_mono)
hence "x ≤ x*(x+1) div 2" by simp
thus ?thesis by (simp add: sf_def)
qed

lemma sf_mono: "x ≤ y ⟹ sf x ≤ sf y"
proof -
assume A1: "x ≤ y"
then have "x+1 ≤ y+1" by (auto)
with A1 have "x*(x+1) ≤ y*(y+1)" by (rule mult_le_mono)
then have "x*(x+1) div 2 ≤ y*(y+1) div 2" by (rule div_le_mono)
thus ?thesis by (simp add: sf_def)
qed

lemma sf_strict_mono: "x < y ⟹ sf x < sf y"
proof -
assume A1: "x < y"
from A1 have S1: "x+1 ≤ y" by simp
from S1 sf_mono have S2: "sf (x+1) ≤ sf y" by (auto)
from sf_at_Suc have S3: "sf x < sf (x+1)" by (auto)
from S2 S3 show ?thesis by (auto)
qed

lemma sf_posI: "x > 0 ⟹ sf(x) > 0"
proof -
assume A1: "x > 0"
then have "sf(0) < sf(x)" by (rule sf_strict_mono)
then show ?thesis by simp
qed

lemma arg_less_sf: "x > 1 ⟹ x < sf(x)"
proof -
assume A1: "x > 1"
let ?y = "x-(1::nat)"
from A1 have S1: "x = ?y+1" by simp
from A1 have "?y > 0" by simp
then have S2: "sf(?y) > 0" by (rule sf_posI)
have "sf(?y+1) = sf(?y) + ?y + 1" by (rule sf_at_Suc)
with S1 have "sf(x) = sf(?y) + x" by simp
with S2  show ?thesis by simp
qed

lemma sf_eq_arg: "sf x = x ⟹ x ≤ 1"
proof -
assume "sf(x) = x"
then have "¬ (x < sf(x))" by simp
then have "(¬ (x > 1))" by (auto simp add: arg_less_sf)
then show ?thesis by simp
qed

lemma sf_le_sfD: "sf x ≤ sf y ⟹ x ≤ y"
proof -
assume A1: "sf x ≤ sf y"
have S1: "y < x ⟹ sf y < sf x" by (rule sf_strict_mono)
have S2: "y < x ∨ x ≤ y" by (auto)
from A1 S1 S2 show ?thesis by (auto)
qed

lemma sf_less_sfD: "sf x < sf y ⟹ x < y"
proof -
assume A1: "sf x < sf y"
have S1: "y ≤ x ⟹ sf y ≤ sf x" by (rule sf_mono)
have S2: "y ≤ x ∨ x < y" by (auto)
from A1 S1 S2 show ?thesis by (auto)
qed

lemma sf_inj: "sf x = sf y ⟹ x = y"
proof -
assume A1: "sf x = sf y"
have S1: "sf x ≤ sf y ⟹ x ≤ y" by (rule sf_le_sfD)
have S2: "sf y ≤ sf x ⟹ y ≤ x" by (rule sf_le_sfD)
from A1 have S3: "sf x ≤ sf y ∧ sf y ≤ sf x" by (auto)
from S3 S1 S2 have S4: "x ≤ y ∧ y ≤ x" by (auto)
from S4 show ?thesis by (auto)
qed

text ‹Auxiliary lemmas›

lemma sf_aux1: "x + y < z ⟹ sf(x+y) + x < sf(z)"
proof -
assume A1: "x+y < z"
from A1 have S1: "x+y+1 ≤ z" by (auto)
from S1 have S2: "sf(x+y+1) ≤ sf(z)" by (rule sf_mono)
have S3: "sf(x+y+1) = sf(x+y) + (x+y)+1" by (rule sf_at_Suc)
from S3 S2 have S4: "sf(x+y) + (x+y) + 1 ≤ sf(z)" by (auto)
from S4 show ?thesis by (auto)
qed

lemma sf_aux2: "sf(z) ≤ sf(x+y) + x ⟹ z ≤ x+y"
proof -
assume A1: "sf(z) ≤ sf(x+y) + x"
from A1 have S1: "¬ sf(x+y) +x < sf(z)" by (auto)
from S1 sf_aux1 have S2: "¬ x+y < z" by (auto)
from S2 show ?thesis by (auto)
qed

lemma sf_aux3: "sf(z) + m < sf(z+1) ⟹ m ≤ z"
proof -
assume A1: "sf(z) + m < sf(z+1)"
have S1: "sf(z+1) = sf(z) + z + 1" by (rule sf_at_Suc)
from A1 S1 have S2: "sf(z) + m < sf(z) + z + 1" by (auto)
from S2 have S3: "m < z + 1" by (auto)
from S3 show ?thesis by (auto)
qed

lemma sf_aux4: "(s::nat) < t ⟹ (sf s) + s < sf t"
proof -
assume A1: "(s::nat) < t"
have "s*(s + 1) + 2*(s+1) ≤ t*(t+1)"
proof -
from A1 have S1: "(s::nat) + 1 ≤ t" by (auto)
from A1 have "(s::nat) + 2 ≤ t+1" by (auto)
with S1 have "((s::nat)+1)*(s+2) ≤ t*(t+1)" by (rule mult_le_mono)
thus ?thesis by (auto)
qed
then have S1: "(s*(s+1) + 2*(s+1)) div 2 ≤  t*(t+1) div 2" by (rule div_le_mono)
have "(0::nat) < 2" by (auto)
then have "(s*(s+1) + 2*(s+1)) div 2 = (s+1) + (s*(s+1)) div 2" by simp
with S1 have "(s*(s+1)) div 2 + (s+1) ≤ t*(t+1) div 2" by (auto)
then have "(s*(s+1)) div 2 + s < t*(t+1) div 2" by (auto)
thus ?thesis by (simp add: sf_def)
qed

text ‹Basic properties of c\_pair function›

lemma sum_le_c_pair: "x + y ≤ c_pair x y"
proof -
have "x+y ≤ sf(x+y)" by (rule arg_le_sf)
thus ?thesis by (simp add: c_pair_def)
qed

lemma arg1_le_c_pair: "x ≤ c_pair x y"
proof -
have "(x::nat) ≤ x + y" by (simp)
moreover have "x + y ≤ c_pair x y" by (rule sum_le_c_pair)
ultimately show ?thesis by (simp)
qed

lemma arg2_le_c_pair: "y ≤ c_pair x y"
proof -
have "(y::nat) ≤ x + y" by (simp)
moreover have "x + y ≤ c_pair x y" by (rule sum_le_c_pair)
ultimately show ?thesis by (simp)
qed

lemma c_pair_sum_mono: "(x1::nat) + y1 < x2 + y2 ⟹ c_pair x1 y1 < c_pair x2 y2"
proof -
assume "(x1::nat) + y1 < x2 + y2"
hence "sf (x1+y1) + (x1+y1) < sf(x2+y2)" by (rule sf_aux4)
hence "sf (x1+y1) + x1 < sf(x2+y2) + x2" by (auto)
thus ?thesis by (simp add: c_pair_def)
qed

lemma c_pair_sum_inj: "c_pair x1 y1 = c_pair x2 y2 ⟹ x1 + y1 = x2 + y2"
proof -
assume A1: "c_pair x1 y1 = c_pair x2 y2"
have S1: "(x1::nat) + y1 < x2 + y2 ⟹ c_pair x1 y1 ≠ c_pair x2 y2" by (rule less_not_refl3, rule c_pair_sum_mono, auto)
have S2: "(x2::nat) + y2 < x1 + y1 ⟹ c_pair x1 y1 ≠ c_pair x2 y2" by (rule less_not_refl2, rule c_pair_sum_mono, auto)
from S1 S2 have "(x1::nat) + y1 ≠ x2 + y2 ⟹ c_pair x1 y1 ≠ c_pair x2 y2" by (arith)
with A1 show ?thesis by (auto)
qed

lemma c_pair_inj: "c_pair x1 y1 = c_pair x2 y2 ⟹ x1 = x2 ∧ y1 = y2"
proof -
assume A1: "c_pair x1 y1 = c_pair x2 y2"
from A1 have S1: "x1 + y1 = x2 + y2" by (rule c_pair_sum_inj)
from A1 have S2: "sf (x1+y1) + x1 = sf (x2+y2) + x2" by (unfold c_pair_def)
from S1 S2 have S3: "x1 = x2" by (simp)
from S1 S3 have S4: "y1 = y2" by (simp)
from S3 S4 show ?thesis by (auto)
qed

lemma c_pair_inj1: "c_pair x1 y1 = c_pair x2 y2 ⟹ x1 = x2" by (frule c_pair_inj, drule conjunct1)

lemma c_pair_inj2: "c_pair x1 y1 = c_pair x2 y2 ⟹ y1 = y2" by (frule c_pair_inj, drule conjunct2)

lemma c_pair_strict_mono1: "x1 < x2 ⟹ c_pair x1 y < c_pair x2 y"
proof -
assume "x1 < x2"
then have "x1 + y < x2 + y" by simp
then show ?thesis by (rule c_pair_sum_mono)
qed

lemma c_pair_mono1: "x1 ≤ x2 ⟹ c_pair x1 y ≤ c_pair x2 y"
proof -
assume A1: "x1 ≤ x2"
show ?thesis
proof cases
assume "x1 < x2"
then have "c_pair x1 y < c_pair x2 y" by (rule c_pair_strict_mono1)
then show ?thesis by simp
next
assume "¬ x1 < x2"
with A1 have "x1 = x2" by simp
then show ?thesis by simp
qed
qed

lemma c_pair_strict_mono2: "y1 < y2 ⟹ c_pair x y1 < c_pair x y2"
proof -
assume A1: "y1 < y2"
from A1 have S1: "x + y1 < x + y2" by simp
then show ?thesis by (rule c_pair_sum_mono)
qed

lemma c_pair_mono2: "y1 ≤ y2 ⟹ c_pair x y1 ≤ c_pair x y2"
proof -
assume A1: "y1 ≤ y2"
show ?thesis
proof cases
assume "y1 < y2"
then have "c_pair x y1 < c_pair x y2" by (rule c_pair_strict_mono2)
then show ?thesis by simp
next
assume "¬ y1 < y2"
with A1 have "y1 = y2" by simp
then show ?thesis by simp
qed
qed

subsection ‹Inverse mapping›

text ‹
‹c_fst› and ‹c_snd› are the functions which yield
the inverse mapping to ‹c_pair›.
›

definition
c_sum :: "nat ⇒ nat" where
"c_sum u = (LEAST z. u < sf (z+1))"

definition
c_fst :: "nat ⇒ nat" where
"c_fst u = u - sf (c_sum u)"

definition
c_snd :: "nat ⇒ nat" where
"c_snd u = c_sum u - c_fst u"

lemma arg_less_sf_at_Suc_of_c_sum: "u < sf ((c_sum u) + 1)"
proof -
have "u+1 ≤ sf(u+1)" by (rule arg_le_sf)
hence "u < sf(u+1)" by simp
thus ?thesis by (unfold c_sum_def, rule LeastI)
qed

lemma arg_less_sf_imp_c_sum_less_arg: "u < sf(x) ⟹ c_sum u < x"
proof -
assume A1: "u < sf(x)"
then show ?thesis
proof (cases x)
assume "x=0"
with A1 show ?thesis by (simp add: sf_def)
next
fix y
assume A2: "x = Suc y"
show ?thesis
proof -
from A1 A2 have "u < sf(y+1)" by simp
hence "(Least (%z. u < sf (z+1))) ≤ y" by (rule Least_le)
hence "c_sum u ≤ y" by (fold c_sum_def)
with A2 show ?thesis by simp
qed
qed
qed

lemma sf_c_sum_le_arg: "u ≥ sf (c_sum u)"
proof -
let ?z = "c_sum u"
from arg_less_sf_at_Suc_of_c_sum have S1: "u < sf (?z+1)" by (auto)
have S2: "¬ c_sum u < c_sum u" by (auto)
from arg_less_sf_imp_c_sum_less_arg S2 have S3: "¬ u < sf (c_sum u) " by (auto)
from S3 show ?thesis by (auto)
qed

lemma c_sum_le_arg: "c_sum u ≤ u"
proof -
have "c_sum u ≤ sf (c_sum u)" by (rule arg_le_sf)
moreover have "sf(c_sum u) ≤ u" by (rule sf_c_sum_le_arg)
ultimately show ?thesis by simp
qed

lemma c_sum_of_c_pair [simp]: "c_sum (c_pair x y) = x + y"
proof -
let ?u = "c_pair x y"
let ?z = "c_sum ?u"
have S1: "?u < sf(?z+1)" by (rule arg_less_sf_at_Suc_of_c_sum)
have S2: "sf(?z) ≤ ?u" by (rule sf_c_sum_le_arg)
from S1 have S3: "sf(x+y)+x < sf(?z+1)" by (simp add: c_pair_def)
from S2 have S4: "sf(?z) ≤ sf(x+y) + x" by (simp add: c_pair_def)
from S3 have S5: "sf(x+y) < sf(?z+1)" by (auto)
from S5 have S6: "x+y < ?z+1" by (rule sf_less_sfD)
from S6 have S7: "x+y ≤ ?z" by (auto)
from S4 have S8: "?z ≤ x+y" by (rule sf_aux2)
from S7 S8 have S9: "?z = x+y" by (auto)
from S9 show ?thesis by (simp)
qed

lemma c_fst_of_c_pair[simp]: "c_fst (c_pair x y) = x"
proof -
let ?u = "c_pair x y"
have "c_sum ?u = x + y" by simp
hence "c_fst ?u = ?u - sf(x+y)" by (simp add: c_fst_def)
moreover have "?u = sf(x+y) + x" by (simp add: c_pair_def)
ultimately show ?thesis by (simp)
qed

lemma c_snd_of_c_pair[simp]: "c_snd (c_pair x y) = y"
proof -
let ?u = "c_pair x y"
have "c_sum ?u = x + y" by simp
moreover have "c_fst ?u = x" by simp
ultimately show ?thesis by (simp add: c_snd_def)
qed

lemma c_pair_at_0: "c_pair 0 0 = 0" by (simp add: sf_def c_pair_def)

lemma c_fst_at_0: "c_fst 0 = 0"
proof -
have "c_pair 0 0 = 0" by (rule c_pair_at_0)
hence "c_fst 0 = c_fst (c_pair 0 0)" by simp
thus ?thesis by simp
qed

lemma c_snd_at_0: "c_snd 0 = 0"
proof -
have "c_pair 0 0 = 0" by (rule c_pair_at_0)
hence "c_snd 0 = c_snd (c_pair 0 0)" by simp
thus ?thesis by simp
qed

lemma sf_c_sum_plus_c_fst: "sf(c_sum u) + c_fst u = u"
proof -
have S1: "sf(c_sum u) ≤ u" by (rule sf_c_sum_le_arg)
have S2: "c_fst u = u - sf(c_sum u)" by (simp add: c_fst_def)
from S1 S2 show ?thesis by (auto)
qed

lemma c_fst_le_c_sum: "c_fst u ≤ c_sum u"
proof -
have S1: "sf(c_sum u) + c_fst u = u" by (rule sf_c_sum_plus_c_fst)
have S2: "u < sf((c_sum u) + 1)" by (rule arg_less_sf_at_Suc_of_c_sum)
from S1 S2 sf_aux3 show ?thesis by (auto)
qed

lemma c_snd_le_c_sum: "c_snd u ≤ c_sum u" by (simp add: c_snd_def)

lemma c_fst_le_arg: "c_fst u ≤ u"
proof -
have "c_fst u ≤ c_sum u" by (rule c_fst_le_c_sum)
moreover have "c_sum u ≤ u" by (rule c_sum_le_arg)
ultimately show ?thesis by simp
qed

lemma c_snd_le_arg: "c_snd u ≤ u"
proof -
have "c_snd u ≤ c_sum u" by (rule c_snd_le_c_sum)
moreover have "c_sum u ≤ u" by (rule c_sum_le_arg)
ultimately show ?thesis by simp
qed

lemma c_sum_is_sum: "c_sum u = c_fst u + c_snd u" by (simp add: c_snd_def c_fst_le_c_sum)

lemma proj_eq_imp_arg_eq: "⟦ c_fst u = c_fst v; c_snd u = c_snd v⟧ ⟹ u = v"
proof -
assume A1: "c_fst u = c_fst v"
assume A2: "c_snd u = c_snd v"
from A1 A2 c_sum_is_sum have S1: "c_sum u = c_sum v" by (auto)
have S2: "sf(c_sum u) + c_fst u = u" by (rule sf_c_sum_plus_c_fst)
from A1 S1 S2 have S3: "sf(c_sum v) + c_fst v = u" by (auto)
from S3 sf_c_sum_plus_c_fst show ?thesis by (auto)
qed

lemma c_pair_of_c_fst_c_snd[simp]: "c_pair (c_fst u) (c_snd u) = u"
proof -
let ?x = "c_fst u"
let ?y = "c_snd u"
have S1: "c_pair ?x ?y = sf(?x + ?y) + ?x" by (simp add: c_pair_def)
have S2: "c_sum u = ?x + ?y" by (rule c_sum_is_sum)
from S1 S2 have "c_pair ?x ?y = sf(c_sum u) + c_fst u" by (auto)
thus ?thesis by (simp add: sf_c_sum_plus_c_fst)
qed

lemma c_sum_eq_arg: "c_sum x = x ⟹ x ≤ 1"
proof -
assume A1: "c_sum x = x"
have S1: "sf(c_sum x) + c_fst x = x" by (rule sf_c_sum_plus_c_fst)
from A1 S1 have S2: "sf x + c_fst x = x" by simp
have S3: "x ≤ sf x" by (rule arg_le_sf)
from S2 S3 have "sf(x)=x" by simp
thus ?thesis by (rule sf_eq_arg)
qed

lemma c_sum_eq_arg_2: "c_sum x = x ⟹ c_fst x = 0"
proof -
assume A1: "c_sum x = x"
have S1: "sf(c_sum x) + c_fst x = x" by (rule sf_c_sum_plus_c_fst)
from A1 S1 have S2: "sf x + c_fst x = x" by simp
have S3: "x ≤ sf x" by (rule arg_le_sf)
from S2 S3 show ?thesis by simp
qed

lemma c_fst_eq_arg: "c_fst x = x ⟹ x = 0"
proof -
assume A1: "c_fst x = x"
have S1: "c_fst x ≤ c_sum x" by (rule c_fst_le_c_sum)
have S2: "c_sum x ≤ x" by (rule c_sum_le_arg)
from A1 S1 S2 have "c_sum x = x" by simp
then have "c_fst x = 0" by (rule c_sum_eq_arg_2)
with A1 show ?thesis by simp
qed

lemma c_fst_less_arg: "x > 0 ⟹ c_fst x < x"
proof -
assume A1: "x > 0"
show ?thesis
proof cases
assume "c_fst x < x"
then show ?thesis by simp
next
assume "¬ c_fst x < x"
then have S1: "c_fst x ≥ x" by simp
have "c_fst x ≤ x" by (rule c_fst_le_arg)
with S1 have "c_fst x = x" by simp
then have "x = 0" by (rule c_fst_eq_arg)
with A1 show ?thesis by simp
qed
qed

lemma c_snd_eq_arg: "c_snd x = x ⟹ x ≤ 1"
proof -
assume A1: "c_snd x = x"
have S1: "c_snd x ≤ c_sum x" by (rule c_snd_le_c_sum)
have S2: "c_sum x ≤ x" by (rule c_sum_le_arg)
from A1 S1 S2 have "c_sum x = x" by simp
then show ?thesis by (rule c_sum_eq_arg)
qed

lemma c_snd_less_arg: "x > 1 ⟹ c_snd x < x"
proof -
assume A1: "x > 1"
show ?thesis
proof cases
assume "c_snd x < x"
then show ?thesis .
next
assume "¬ c_snd x < x"
then have S1: "c_snd x ≥ x" by auto
have "c_snd x ≤ x" by (rule c_snd_le_arg)
with S1 have "c_snd x = x" by simp
then have "x ≤ 1" by (rule c_snd_eq_arg)
with A1 show ?thesis by simp
qed
qed

end


# Theory PRecFun

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

section ‹Primitive recursive functions›

theory PRecFun imports CPair
begin

text ‹
This theory contains definition of the primitive recursive functions.
›

subsection ‹Basic definitions›

primrec
PrimRecOp :: "(nat ⇒ nat) ⇒ (nat ⇒ nat ⇒ nat ⇒ nat) ⇒ (nat ⇒ nat ⇒ nat)"
where
"PrimRecOp g h 0 x  = g x"
| "PrimRecOp g h (Suc y) x = h y (PrimRecOp g h y x) x"

primrec
PrimRecOp_last :: "(nat ⇒ nat) ⇒ (nat ⇒ nat ⇒ nat ⇒ nat) ⇒ (nat ⇒ nat ⇒ nat)"
where
"PrimRecOp_last g h x 0  = g x"
| "PrimRecOp_last g h x (Suc y)= h x (PrimRecOp_last g h x y) y"

primrec
PrimRecOp1 :: "nat ⇒ (nat ⇒ nat ⇒ nat) ⇒ (nat ⇒ nat)"
where
"PrimRecOp1 a h 0 = a"
| "PrimRecOp1 a h (Suc y) = h y (PrimRecOp1 a h y)"

inductive_set
PrimRec1 :: "(nat ⇒ nat) set" and
PrimRec2 :: "(nat ⇒ nat ⇒ nat) set" and
PrimRec3 :: "(nat ⇒ nat ⇒ nat ⇒ nat) set"
where
zero: "(λ x. 0) ∈ PrimRec1"
| suc:   "Suc ∈ PrimRec1"
| id1_1: "(λ x. x) ∈ PrimRec1"
| id2_1: "(λ x y. x) ∈ PrimRec2"
| id2_2: "(λ x y. y) ∈ PrimRec2"
| id3_1: "(λ x y z. x) ∈ PrimRec3"
| id3_2: "(λ x y z. y) ∈ PrimRec3"
| id3_3: "(λ x y z. z) ∈ PrimRec3"
| comp1_1: "⟦ f ∈ PrimRec1; g ∈ PrimRec1⟧ ⟹ (λ x. f (g x)) ∈ PrimRec1"
| comp1_2: "⟦ f ∈ PrimRec1; g ∈ PrimRec2⟧ ⟹ (λ x y. f (g x y)) ∈ PrimRec2"
| comp1_3: "⟦ f ∈ PrimRec1; g ∈ PrimRec3⟧ ⟹ (λ x y z. f (g x y z)) ∈ PrimRec3"
| comp2_1: "⟦ f ∈ PrimRec2; g ∈ PrimRec1; h ∈ PrimRec1⟧ ⟹ (λ x. f (g x) (h x)) ∈ PrimRec1"
| comp3_1: "⟦ f ∈ PrimRec3; g ∈ PrimRec1; h ∈ PrimRec1; k ∈ PrimRec1⟧ ⟹ (λ x. f (g x) (h x) (k x)) ∈ PrimRec1"
| comp2_2: "⟦ f ∈ PrimRec2; g ∈ PrimRec2; h ∈ PrimRec2⟧ ⟹ (λ x y. f (g x y) (h x y)) ∈ PrimRec2"
| comp2_3: "⟦ f ∈ PrimRec2; g ∈ PrimRec3; h ∈ PrimRec3⟧ ⟹ (λ x y z. f (g x y z) (h x y z)) ∈ PrimRec3"
| comp3_2: "⟦ f ∈ PrimRec3; g ∈ PrimRec2; h ∈ PrimRec2; k ∈ PrimRec2⟧ ⟹ (λ x y. f (g x y) (h x y) (k x y)) ∈ PrimRec2"
| comp3_3: "⟦ f ∈ PrimRec3; g ∈ PrimRec3; h ∈ PrimRec3; k ∈ PrimRec3⟧ ⟹ (λ x y z. f (g x y z) (h x y z) (k x y z)) ∈ PrimRec3"
| prim_rec: "⟦ g ∈ PrimRec1; h ∈ PrimRec3⟧ ⟹ PrimRecOp g h ∈ PrimRec2"

lemmas pr_zero = PrimRec1_PrimRec2_PrimRec3.zero
lemmas pr_suc = PrimRec1_PrimRec2_PrimRec3.suc
lemmas pr_id1_1 = PrimRec1_PrimRec2_PrimRec3.id1_1
lemmas pr_id2_1 = PrimRec1_PrimRec2_PrimRec3.id2_1
lemmas pr_id2_2 = PrimRec1_PrimRec2_PrimRec3.id2_2
lemmas pr_id3_1 = PrimRec1_PrimRec2_PrimRec3.id3_1
lemmas pr_id3_2 = PrimRec1_PrimRec2_PrimRec3.id3_2
lemmas pr_id3_3 = PrimRec1_PrimRec2_PrimRec3.id3_3
lemmas pr_comp1_1 = PrimRec1_PrimRec2_PrimRec3.comp1_1
lemmas pr_comp1_2 = PrimRec1_PrimRec2_PrimRec3.comp1_2
lemmas pr_comp1_3 = PrimRec1_PrimRec2_PrimRec3.comp1_3
lemmas pr_comp2_1 = PrimRec1_PrimRec2_PrimRec3.comp2_1
lemmas pr_comp2_2 = PrimRec1_PrimRec2_PrimRec3.comp2_2
lemmas pr_comp2_3 = PrimRec1_PrimRec2_PrimRec3.comp2_3
lemmas pr_comp3_1 = PrimRec1_PrimRec2_PrimRec3.comp3_1
lemmas pr_comp3_2 = PrimRec1_PrimRec2_PrimRec3.comp3_2
lemmas pr_comp3_3 = PrimRec1_PrimRec2_PrimRec3.comp3_3
lemmas pr_rec = PrimRec1_PrimRec2_PrimRec3.prim_rec

ML_file ‹Utils.ML›

named_theorems prec

method_setup prec0 = ‹
Attrib.thms >> (fn ths => fn ctxt => Method.METHOD (fn facts =>
HEADGOAL (prec0_tac ctxt (facts @ Named_Theorems.get ctxt @{named_theorems prec}))))
› "apply primitive recursive functions"

lemmas [prec] = pr_zero pr_suc pr_id1_1 pr_id2_1 pr_id2_2 pr_id3_1 pr_id3_2 pr_id3_3

lemma pr_swap: "f ∈ PrimRec2 ⟹ (λ x y. f y x) ∈ PrimRec2" by prec0

theorem pr_rec_scheme: "⟦ g ∈ PrimRec1; h ∈ PrimRec3; ∀ x. f 0 x = g x; ∀ x y. f (Suc y) x = h y (f y x) x ⟧ ⟹ f ∈ PrimRec2"
proof -
assume g_is_pr: "g ∈ PrimRec1"
assume h_is_pr: "h ∈ PrimRec3"
assume f_at_0: "∀ x. f 0 x = g x"
assume f_at_Suc: "∀ x y. f (Suc y) x = h y (f y x) x"
from f_at_0 f_at_Suc have "⋀ x y. f y x  = PrimRecOp g h y x" by (induct_tac y, simp_all)
then have "f = PrimRecOp g h" by (simp add: ext)
with g_is_pr h_is_pr show ?thesis by (simp add: pr_rec)
qed

lemma op_plus_is_pr [prec]: "(λ x y. x + y) ∈ PrimRec2"
proof (rule pr_swap)
show "(λ x y. y+x) ∈ PrimRec2"
proof -
have S1: "PrimRecOp (λ x. x) (λ x y z. Suc y) ∈ PrimRec2"
proof (rule pr_rec)
show "(λ x. x) ∈ PrimRec1" by (rule pr_id1_1)
next
show "(λ x y z. Suc y) ∈ PrimRec3" by prec0
qed
have "(λ x y. y+x) = PrimRecOp (λ x. x) (λ x y z. Suc y)" (is "_ = ?f")
proof -
have "⋀ x y. (?f y x = y + x)" by (induct_tac y, auto)
thus ?thesis by (simp add: ext)
qed
with S1 show ?thesis by simp
qed
qed

lemma op_mult_is_pr [prec]: "(λ x y. x*y) ∈ PrimRec2"
proof (rule pr_swap)
show "(λ x y. y*x) ∈ PrimRec2"
proof -
have S1: "PrimRecOp (λ x. 0) (λ x y z. y+z) ∈ PrimRec2"
proof (rule pr_rec)
show "(λ x. 0) ∈ PrimRec1" by (rule pr_zero)
next
show "(λ x y z. y+z) ∈ PrimRec3" by prec0
qed
have "(λ x y. y*x) = PrimRecOp (λ x. 0) (λ x y z. y+z)" (is "_ = ?f")
proof -
have "⋀ x y. (?f y x = y * x)" by (induct_tac y, auto)
thus ?thesis by (simp add: ext)
qed
with S1 show ?thesis by simp
qed
qed

lemma const_is_pr: "(λ x. (n::nat)) ∈ PrimRec1"
proof (induct n)
show "(λ x. 0) ∈ PrimRec1" by (rule pr_zero)
next
fix n assume "(λ x. n) ∈ PrimRec1"
then show "(λ x. Suc n) ∈ PrimRec1" by prec0
qed

lemma const_is_pr_2: "(λ x y. (n::nat)) ∈ PrimRec2"
proof (rule pr_comp1_2 [where ?f="%x.(n::nat)" and ?g="%x y. x"])
show "(λ x. n) ∈ PrimRec1" by (rule const_is_pr)
next
show "(λ x y. x) ∈ PrimRec2" by (rule pr_id2_1)
qed

lemma const_is_pr_3: "(λ x y z. (n::nat)) ∈ PrimRec3"
proof (rule pr_comp1_3 [where ?f="%x.(n::nat)" and ?g="%x y z. x"])
show "(λ x. n) ∈ PrimRec1" by (rule const_is_pr)
next
show "(λ x y z. x) ∈ PrimRec3" by (rule pr_id3_1)
qed

theorem pr_rec_last: "⟦g ∈ PrimRec1; h ∈ PrimRec3⟧ ⟹ PrimRecOp_last g h ∈ PrimRec2"
proof -
assume A1: "g ∈ PrimRec1"
assume A2: "h ∈ PrimRec3"
let ?h1 = "λ x y z. h z y x"
from A2 pr_id3_3 pr_id3_2 pr_id3_1 have h1_is_pr: "?h1 ∈ PrimRec3" by (rule pr_comp3_3)
let ?f1 = "PrimRecOp g ?h1"
from A1 h1_is_pr have f1_is_pr: "?f1 ∈ PrimRec2" by (rule pr_rec)
let ?f = "λ x y. ?f1 y x"
from f1_is_pr have f_is_pr: "?f ∈ PrimRec2" by (rule pr_swap)
have "⋀ x y. ?f x y = PrimRecOp_last g h x y" by (induct_tac y, simp_all)
then have "?f = PrimRecOp_last g h" by (simp add: ext)
with f_is_pr show ?thesis by simp
qed

theorem pr_rec1: "h ∈ PrimRec2 ⟹ PrimRecOp1 (a::nat) h ∈ PrimRec1"
proof -
assume A1: "h ∈ PrimRec2"
let ?g = "(λ x. a)"
have g_is_pr: "?g ∈ PrimRec1" by (rule const_is_pr)
let ?h1 = "(λ x y z. h x y)"
from A1 have h1_is_pr: "?h1 ∈ PrimRec3" by prec0
let ?f1 = "PrimRecOp ?g ?h1"
from g_is_pr h1_is_pr have f1_is_pr: "?f1 ∈ PrimRec2" by (rule pr_rec)
let ?f = "(λ x. ?f1 x 0)"
from f1_is_pr pr_id1_1 pr_zero have f_is_pr: "?f ∈ PrimRec1" by (rule pr_comp2_1)
have "⋀ y. ?f y = PrimRecOp1 a h y" by (induct_tac y, auto)
then have "?f = PrimRecOp1 a h" by (simp add: ext)
with f_is_pr show ?thesis by (auto)
qed

theorem pr_rec1_scheme: "⟦ h ∈ PrimRec2; f 0 = a; ∀ y. f (Suc y) = h y (f y) ⟧ ⟹ f ∈ PrimRec1"
proof -
assume h_is_pr: "h ∈ PrimRec2"
assume f_at_0: "f 0 = a"
assume f_at_Suc: "∀ y. f (Suc y) = h y (f y)"
from f_at_0 f_at_Suc have "⋀ y. f y  = PrimRecOp1 a h y" by (induct_tac y, simp_all)
then have "f = PrimRecOp1 a h" by (simp add: ext)
with h_is_pr show ?thesis by (simp add: pr_rec1)
qed

lemma pred_is_pr: "(λ x. x - (1::nat)) ∈ PrimRec1"
proof -
have S1: "PrimRecOp1 0 (λ x y. x) ∈ PrimRec1"
proof (rule pr_rec1)
show "(λ x y. x) ∈ PrimRec2" by (rule pr_id2_1)
qed
have "(λ x. x-(1::nat)) = PrimRecOp1 0 (λ x y. x)" (is "_ = ?f")
proof -
have "⋀ x. (?f x = x-(1::nat))" by (induct_tac x, auto)
thus ?thesis by (simp add: ext)
qed
with S1 show ?thesis by simp
qed

lemma op_sub_is_pr [prec]: "(λ x y. x-y) ∈ PrimRec2"
proof (rule pr_swap)
show "(λ x y. y - x) ∈ PrimRec2"
proof -
have S1: "PrimRecOp (λ x. x) (λ x y z.  y-(1::nat)) ∈ PrimRec2"
proof (rule pr_rec)
show "(λ x. x) ∈ PrimRec1" by (rule pr_id1_1)
next
from pred_is_pr pr_id3_2 show "(λ x y z. y-(1::nat)) ∈ PrimRec3" by (rule pr_comp1_3)
qed
have "(λ x y. y - x) = PrimRecOp (λ x. x) (λ x y z.  y-(1::nat))" (is "_ = ?f")
proof -
have "⋀ x y. (?f y x = x - y)" by (induct_tac y, auto)
thus ?thesis by (simp add: ext)
qed
with S1 show ?thesis by simp
qed
qed

lemmas [prec] =
const_is_pr [of 0] const_is_pr_2 [of 0] const_is_pr_3 [of 0]
const_is_pr [of 1] const_is_pr_2 [of 1] const_is_pr_3 [of 1]
const_is_pr [of 2] const_is_pr_2 [of 2] const_is_pr_3 [of 2]

definition
sgn1 :: "nat ⇒ nat" where
"sgn1 x = (case x of 0 ⇒ 0 | Suc y ⇒ 1)"

definition
sgn2 :: "nat ⇒ nat" where
"sgn2 x ≡ (case x of 0 ⇒ 1 | Suc y ⇒ 0)"

definition
abs_of_diff :: "nat ⇒ nat ⇒ nat" where
"abs_of_diff = (λ x y. (x - y) + (y - x))"

lemma [simp]: "sgn1 0 = 0" by (simp add: sgn1_def)
lemma [simp]: "sgn1 (Suc y) = 1" by (simp add: sgn1_def)
lemma [simp]: "sgn2 0 = 1" by (simp add: sgn2_def)
lemma [simp]: "sgn2 (Suc y) = 0" by (simp add: sgn2_def)
lemma [simp]: "x ≠ 0 ⟹ sgn1 x = 1" by (simp add: sgn1_def, cases x, auto)
lemma [simp]: "x ≠ 0 ⟹ sgn2 x = 0" by (simp add: sgn2_def, cases x, auto)

lemma sgn1_nz_impl_arg_pos: "sgn1 x ≠ 0 ⟹ x > 0" by (cases x) auto
lemma sgn1_zero_impl_arg_zero: "sgn1 x = 0 ⟹ x = 0" by (cases x) auto
lemma sgn2_nz_impl_arg_zero: "sgn2 x ≠ 0 ⟹ x = 0" by (cases x) auto
lemma sgn2_zero_impl_arg_pos: "sgn2 x = 0 ⟹ x > 0" by (cases x) auto

lemma sgn1_nz_eq_arg_pos: "(sgn1 x ≠ 0) = (x > 0)" by (cases x) auto
lemma sgn1_zero_eq_arg_zero: "(sgn1 x = 0) = (x = 0)" by (cases x) auto
lemma sgn2_nz_eq_arg_pos: "(sgn2 x ≠ 0) = (x = 0)" by (cases x) auto
lemma sgn2_zero_eq_arg_zero: "(sgn2 x = 0) = (x > 0)" by (cases x) auto

lemma sgn1_pos_eq_one: "sgn1 x > 0 ⟹ sgn1 x = 1" by (cases x) auto
lemma sgn2_pos_eq_one: "sgn2 x > 0 ⟹ sgn2 x = 1" by (cases x) auto

lemma sgn2_eq_1_sub_arg: "sgn2 = (λ x. 1 - x)"
proof (rule ext)
fix x show "sgn2 x = 1 - x" by (cases x) auto
qed

lemma sgn1_eq_1_sub_sgn2: "sgn1  = (λ x. 1 - (sgn2 x))"
proof
fix x show "sgn1 x = 1 - sgn2 x"
proof -
have "1- sgn2 x = 1 - (1 - x)" by (simp add: sgn2_eq_1_sub_arg)
then show ?thesis by (simp add: sgn1_def, cases x, auto)
qed
qed

lemma sgn2_is_pr [prec]: "sgn2 ∈ PrimRec1"
proof -
have "(λ x. 1 - x) ∈ PrimRec1" by prec0
thus ?thesis by (simp add: sgn2_eq_1_sub_arg)
qed

lemma sgn1_is_pr [prec]: "sgn1 ∈ PrimRec1"
proof -
from sgn2_is_pr have "(λ x. 1 - (sgn2 x)) ∈ PrimRec1" by prec0
thus ?thesis by (simp add: sgn1_eq_1_sub_sgn2)
qed

lemma abs_of_diff_is_pr [prec]: "abs_of_diff ∈ PrimRec2" unfolding abs_of_diff_def by prec0

lemma abs_of_diff_eq: "(abs_of_diff x y = 0) = (x = y)" by (simp add: abs_of_diff_def, arith)

lemma sf_is_pr [prec]: "sf ∈ PrimRec1"
proof -
have S1: "PrimRecOp1 0 (λ x y. y + x + 1) ∈ PrimRec1"
proof (rule pr_rec1)
show "(λ x y. y + x + 1) ∈ PrimRec2" by prec0
qed
have "(λ x. sf x) = PrimRecOp1 0 (λ x y. y + x + 1)" (is "_ = ?f")
proof -
have "⋀ x. (?f x = sf x)"
proof (induct_tac x)
show "?f 0 = sf 0" by (simp add: sf_at_0)
next
fix x assume "?f x = sf x"
with sf_at_Suc show "?f (Suc x) = sf (Suc x)"  by auto
qed
thus ?thesis by (simp add: ext)
qed
with S1 show ?thesis by simp
qed

lemma c_pair_is_pr [prec]: "c_pair ∈ PrimRec2"
proof -
have "c_pair = (λ x y. sf (x+y) + x)" by (simp add: c_pair_def ext)
moreover from sf_is_pr have "(λ x y. sf (x+y) + x) ∈ PrimRec2" by prec0
ultimately show ?thesis by (simp)
qed

lemma if_is_pr: "⟦ p ∈ PrimRec1; q1 ∈ PrimRec1; q2 ∈ PrimRec1⟧ ⟹ (λ x. if (p x = 0) then (q1 x) else (q2 x)) ∈ PrimRec1"
proof -
have if_as_pr: "(λ x. if (p x = 0) then (q1 x) else (q2 x)) = (λ x. (sgn2 (p x)) * (q1 x) + (sgn1 (p x)) * (q2 x))"
proof (rule ext)
fix x show "(if (p x = 0) then (q1 x) else (q2 x)) = (sgn2 (p x)) * (q1 x) + (sgn1 (p x)) * (q2 x)" (is "?left = ?right")
proof cases
assume A1: "p x = 0"
then have S1: "?left = q1 x" by simp
from A1 have S2: "?right = q1 x" by simp
from S1 S2 show ?thesis by simp
next
assume A2: "p x ≠ 0"
then have S3: "p x > 0" by simp
then show ?thesis by simp
qed
qed
assume "p ∈ PrimRec1" and "q1 ∈ PrimRec1" and "q2 ∈ PrimRec1"
then have "(λ x. (sgn2 (p x)) * (q1 x) + (sgn1 (p x)) * (q2 x)) ∈ PrimRec1" by prec0
with if_as_pr show ?thesis by simp
qed

lemma if_eq_is_pr [prec]: "⟦ p1 ∈ PrimRec1; p2 ∈ PrimRec1; q1 ∈ PrimRec1; q2 ∈ PrimRec1⟧ ⟹ (λ x. if (p1 x = p2 x) then (q1 x) else (q2 x)) ∈ PrimRec1"
proof -
have S1: "(λ x. if (p1 x = p2 x) then (q1 x) else (q2 x)) = (λ x. if (abs_of_diff (p1 x) (p2 x) = 0) then (q1 x) else (q2 x))" (is "?L = ?R") by (simp add: abs_of_diff_eq)
assume A1: "p1 ∈ PrimRec1" and A2: "p2 ∈ PrimRec1"
with abs_of_diff_is_pr have S2: "(λ x. abs_of_diff (p1 x) (p2 x)) ∈ PrimRec1" by prec0
assume "q1 ∈ PrimRec1" and "q2 ∈ PrimRec1"
with S2 have "?R ∈ PrimRec1" by (rule if_is_pr)
with S1 show ?thesis by simp
qed

lemma if_is_pr2 [prec]: "⟦ p ∈ PrimRec2; q1 ∈ PrimRec2; q2 ∈ PrimRec2⟧ ⟹ (λ x y. if (p x y = 0) then (q1 x y) else (q2 x y)) ∈ PrimRec2"
proof -
have if_as_pr: "(λ x y. if (p x y = 0) then (q1 x y) else (q2 x y)) = (λ x y. (sgn2 (p x y)) * (q1 x y) + (sgn1 (p x y)) * (q2 x y))"
proof (rule ext, rule ext)
fix x fix y show "(if (p x y = 0) then (q1 x y) else (q2 x y)) = (sgn2 (p x y)) * (q1 x y) + (sgn1 (p x y)) * (q2 x y)" (is "?left = ?right")
proof cases
assume A1: "p x y = 0"
then have S1: "?left = q1 x y" by simp
from A1 have S2: "?right = q1 x y" by simp
from S1 S2 show ?thesis by simp
next
assume A2: "p x y ≠ 0"
then have S3: "p x y > 0" by simp
then show ?thesis by simp
qed
qed
assume "p ∈ PrimRec2" and "q1 ∈ PrimRec2" and "q2 ∈ PrimRec2"
then have "(λ x y. (sgn2 (p x y)) * (q1 x y) + (sgn1 (p x y)) * (q2 x y)) ∈ PrimRec2" by prec0
with if_as_pr show ?thesis by simp
qed

lemma if_eq_is_pr2: "⟦ p1 ∈ PrimRec2; p2 ∈ PrimRec2; q1 ∈ PrimRec2; q2 ∈ PrimRec2⟧ ⟹ (λ x y. if (p1 x y = p2 x y) then (q1 x y) else (q2 x y)) ∈ PrimRec2"
proof -
have S1: "(λ x y. if (p1 x y = p2 x y) then (q1 x y) else (q2 x y)) = (λ x y. if (abs_of_diff (p1 x y) (p2 x y) = 0) then (q1 x y) else (q2 x y))" (is "?L = ?R") by (simp add: abs_of_diff_eq)
assume A1: "p1 ∈ PrimRec2" and A2: "p2 ∈ PrimRec2"
with abs_of_diff_is_pr have S2: "(λ x y. abs_of_diff (p1 x y) (p2 x y)) ∈ PrimRec2" by prec0
assume "q1 ∈ PrimRec2" and "q2 ∈ PrimRec2"
with S2 have "?R ∈ PrimRec2" by (rule if_is_pr2)
with S1 show ?thesis by simp
qed

lemma if_is_pr3 [prec]: "⟦ p ∈ PrimRec3; q1 ∈ PrimRec3; q2 ∈ PrimRec3⟧ ⟹ (λ x y z. if (p x y z = 0) then (q1 x y z) else (q2 x y z)) ∈ PrimRec3"
proof -
have if_as_pr: "(λ x y z. if (p x y z = 0) then (q1 x y z) else (q2 x y z)) = (λ x y z. (sgn2 (p x y z)) * (q1 x y z) + (sgn1 (p x y z)) * (q2 x y z))"
proof (rule ext, rule ext, rule ext)
fix x fix y fix z show "(if (p x y z = 0) then (q1 x y z) else (q2 x y z)) = (sgn2 (p x y z)) * (q1 x y z) + (sgn1 (p x y z)) * (q2 x y z)" (is "?left = ?right")
proof cases
assume A1: "p x y z = 0"
then have S1: "?left = q1 x y z" by simp
from A1 have S2: "?right = q1 x y z" by simp
from S1 S2 show ?thesis by simp
next
assume A2: "p x y z ≠ 0"
then have S3: "p x y z > 0" by simp
then show ?thesis by simp
qed
qed
assume "p ∈ PrimRec3" and "q1 ∈ PrimRec3" and "q2 ∈ PrimRec3"
then have "(λ x y z. (sgn2 (p x y z)) * (q1 x y z) + (sgn1 (p x y z)) * (q2 x y z)) ∈ PrimRec3"
by prec0
with if_as_pr show ?thesis by simp
qed

lemma if_eq_is_pr3: "⟦ p1 ∈ PrimRec3; p2 ∈ PrimRec3; q1 ∈ PrimRec3; q2 ∈ PrimRec3⟧ ⟹ (λ x y z. if (p1 x y z = p2 x y z) then (q1 x y z) else (q2 x y z)) ∈ PrimRec3"
proof -
have S1: "(λ x y z. if (p1 x y z = p2 x y z) then (q1 x y z) else (q2 x y z)) = (λ x y z. if (abs_of_diff (p1 x y z) (p2 x y z) = 0) then (q1 x y z) else (q2 x y z))" (is "?L = ?R") by (simp add: abs_of_diff_eq)
assume A1: "p1 ∈ PrimRec3" and A2: "p2 ∈ PrimRec3"
with abs_of_diff_is_pr have S2: "(λ x y z. abs_of_diff (p1 x y z) (p2 x y z)) ∈ PrimRec3"
by prec0
assume "q1 ∈ PrimRec3" and "q2 ∈ PrimRec3"
with S2 have "?R ∈ PrimRec3" by (rule if_is_pr3)
with S1 show ?thesis by simp
qed

ML ‹
fun get_if_by_index 1 = @{thm if_eq_is_pr}
| get_if_by_index 2 = @{thm if_eq_is_pr2}
| get_if_by_index 3 = @{thm if_eq_is_pr3}
| get_if_by_index _ = raise BadArgument

fun if_comp_tac ctxt = SUBGOAL (fn (t, i) =>
let
val t = extract_trueprop_arg (Logic.strip_imp_concl t)
val (t1, t2) = extract_set_args t
val n2 =
let
val Const(s, _) = t2
in
get_num_by_set s
end
val (name, _, n1) = extract_free_arg t1
in
if name = @{const_name If} then
resolve_tac ctxt [get_if_by_index n2] i
else
let
val comp = get_comp_by_indexes (n1, n2)
in
Rule_Insts.res_inst_tac ctxt
[((("f", 0), Position.none), Variable.revert_fixed ctxt name)] [] comp i
end
end

fun prec_tac ctxt facts i =
Method.insert_tac ctxt facts i THEN
REPEAT (resolve_tac ctxt [@{thm const_is_pr}, @{thm const_is_pr_2}, @{thm const_is_pr_3}] i ORELSE
assume_tac ctxt i ORELSE if_comp_tac ctxt i)
›

method_setup prec = ‹
Attrib.thms >> (fn ths => fn ctxt => Method.METHOD (fn facts =>
HEADGOAL (prec_tac ctxt (facts @ Named_Theorems.get ctxt @{named_theorems prec}))))
› "apply primitive recursive functions"

subsection ‹Bounded least operator›

definition
b_least :: "(nat ⇒ nat ⇒ nat) ⇒ (nat ⇒ nat)" where
"b_least f x ≡ (Least (%y. y = x ∨ (y < x ∧ (f x y) ≠ 0)))"

definition
b_least2 :: "(nat ⇒ nat ⇒ nat) ⇒ (nat ⇒ nat ⇒ nat)" where
"b_least2 f x y ≡ (Least (%z. z = y ∨ (z < y ∧ (f x z) ≠ 0)))"

lemma b_least_aux1: "b_least f x = x ∨ (b_least f x < x ∧ (f x (b_least f x)) ≠ 0)"
proof -
let ?P = "%y. y = x ∨ (y < x ∧ (f x y) ≠ 0)"
have "?P x" by simp
then have "?P (Least ?P)" by (rule LeastI)
thus ?thesis by (simp add: b_least_def)
qed

lemma b_least_le_arg: "b_least f x ≤ x"
proof -
have "b_least f x = x ∨ (b_least f x < x ∧ (f x (b_least f x)) ≠ 0)" by (rule b_least_aux1)
from this show ?thesis by (arith)
qed

lemma less_b_least_impl_zero: "y < b_least f x ⟹ f x y = 0"
proof -
assume A1: "y < b_least f x" (is "_ < ?b")
have "b_least f x ≤ x" by (rule b_least_le_arg)
with A1 have S1: "y < x" by simp
with A1 have " y < (Least (%y. y = x ∨ (y < x ∧ (f x y) ≠ 0)))" by (simp add: b_least_def)
then have "¬ (y = x ∨ (y < x ∧ (f x y) ≠ 0))" by (rule not_less_Least)
with S1 show ?thesis by simp
qed

lemma nz_impl_b_least_le: "(f x y) ≠ 0 ⟹ (b_least f x) ≤ y"
proof (rule ccontr)
assume A1: "f x y ≠ 0"
assume "¬ b_least f x ≤ y"
then have "y < b_least f x" by simp
with A1 show False by (simp add: less_b_least_impl_zero)
qed

lemma b_least_less_impl_nz: "b_least f x < x ⟹ f x (b_least f x) ≠ 0"
proof -
assume A1: "b_least f x < x"
have "b_least f x = x ∨ (b_least f x < x ∧ (f x (b_least f x)) ≠ 0)" by (rule b_least_aux1)
from A1 this show ?thesis by simp
qed

lemma b_least_less_impl_eq: "b_least f x < x ⟹ (b_least f x) = (Least (%y. (f x y) ≠ 0))"
proof -
assume A1: "b_least f x < x" (is "?b < _")
let ?B = "(Least (%y. (f x y) ≠ 0))"
from A1 have S1: "f x ?b ≠ 0" by (rule b_least_less_impl_nz)
from S1 have S2: "?B  ≤ ?b" by (rule Least_le)
from S1 have S3: "f x ?B ≠ 0" by (rule LeastI)
from S3 have S4: "?b ≤ ?B" by (rule nz_impl_b_least_le)
from S2 S4 show ?thesis by simp
qed

lemma less_b_least_impl_zero2: "⟦y < x; b_least f x = x⟧ ⟹ f x y = 0" by (simp add: less_b_least_impl_zero)

lemma nz_impl_b_least_less: "⟦y<x; (f x y) ≠ 0⟧ ⟹ (b_least f x) < x"
proof -
assume A1: "y < x"
assume "f x y ≠ 0"
then have "b_least f x ≤ y" by (rule nz_impl_b_least_le)
with A1 show ?thesis by simp
qed

lemma b_least_aux2: "⟦y<x; (f x y) ≠ 0⟧ ⟹ (b_least f x) = (Least (%y. (f x y) ≠ 0))"
proof -
assume A1: "y < x" and A2: "f x y ≠ 0"
from A1 A2 have S1: "b_least f x < x" by (rule nz_impl_b_least_less)
thus ?thesis by (rule b_least_less_impl_eq)
qed

lemma b_least2_aux1: "b_least2 f x y = y ∨ (b_least2 f x y < y ∧ (f x (b_least2 f x y)) ≠ 0)"
proof -
let ?P = "%z. z = y ∨ (z < y ∧ (f x z) ≠ 0)"
have "?P y" by simp
then have "?P (Least ?P)" by (rule LeastI)
thus ?thesis by (simp add: b_least2_def)
qed

lemma b_least2_le_arg: "b_least2 f x y ≤ y"
proof -
let ?B = "b_least2 f x y"
have "?B = y ∨ (?B < y ∧ (f x ?B) ≠ 0)" by (rule b_least2_aux1)
from this show ?thesis by (arith)
qed

lemma less_b_least2_impl_zero: "z < b_least2 f x y ⟹ f x z = 0"
proof -
assume A1: "z < b_least2 f x y" (is "_ < ?b")
have "b_least2 f x y ≤ y" by (rule b_least2_le_arg)
with A1 have S1: "z < y" by simp
with A1 have " z < (Least (%z. z = y ∨ (z < y ∧ (f x z) ≠ 0)))" by (simp add: b_least2_def)
then have "¬ (z = y ∨ (z < y ∧ (f x z) ≠ 0))" by (rule not_less_Least)
with S1 show ?thesis by simp
qed

lemma nz_impl_b_least2_le: "(f x z) ≠ 0 ⟹ (b_least2 f x y) ≤ z"
proof -
assume A1: "f x z ≠ 0"
have S1: "z < b_least2 f x y ⟹ f x z = 0" by (rule less_b_least2_impl_zero)
from A1 S1 show ?thesis by arith
qed

lemma b_least2_less_impl_nz: "b_least2 f x y < y ⟹ f x (b_least2 f x y) ≠ 0"
proof -
assume A1: "b_least2 f x y < y"
have "b_least2 f x y = y ∨ (b_least2 f x y < y ∧ (f x (b_least2 f x y)) ≠ 0)" by (rule b_least2_aux1)
with A1 show ?thesis by simp
qed

lemma b_least2_less_impl_eq: "b_least2 f x y < y ⟹ (b_least2 f x y) = (Least (%z. (f x z) ≠ 0))"
proof -
assume A1: "b_least2 f x y < y" (is "?b < _")
let ?B = "(Least (%z. (f x z) ≠ 0))"
from A1 have S1: "f x ?b ≠ 0" by (rule b_least2_less_impl_nz)
from S1 have S2: "?B  ≤ ?b" by (rule Least_le)
from S1 have S3: "f x ?B ≠ 0" by (rule LeastI)
from S3 have S4: "?b ≤ ?B" by (rule nz_impl_b_least2_le)
from S2 S4 show ?thesis by simp
qed

lemma less_b_least2_impl_zero2: "⟦z<y; b_least2 f x y = y⟧ ⟹ f x z = 0"
proof -
assume  "z < y" and "b_least2 f x y = y"
hence "z < b_least2 f x y" by simp
thus ?thesis by (rule less_b_least2_impl_zero)
qed

lemma nz_b_least2_impl_less: "⟦z<y; (f x z) ≠ 0⟧ ⟹ (b_least2 f x y) < y"
proof (rule ccontr)
assume A1: "z < y"
assume A2: "f x z ≠ 0"
assume "¬ (b_least2 f x y) < y" then have A3: "y ≤ (b_least2 f x y)" by simp
have "b_least2 f x y ≤ y" by (rule b_least2_le_arg)
with A3 have "b_least2 f x y = y" by simp
with A1 have "f x z = 0" by (rule less_b_least2_impl_zero2)
with A2 show False by simp
qed

lemma b_least2_less_impl_eq2: "⟦z < y; (f x z) ≠ 0⟧ ⟹ (b_least2 f x y) = (Least (%z. (f x z) ≠ 0))"
proof -
assume A1: "z < y" and A2: "f x z ≠ 0"
from A1 A2 have S1: "b_least2 f x y < y" by (rule nz_b_least2_impl_less)
thus ?thesis by (rule b_least2_less_impl_eq)
qed

lemma b_least2_aux2: "b_least2 f x y < y ⟹ b_least2 f x (Suc y) = b_least2 f x y"
proof -
let ?B = "b_least2 f x y"
assume A1: "?B < y"
from A1 have S1: "f x ?B ≠ 0" by (rule b_least2_less_impl_nz)
from S1 have S2: "b_least2 f x (Suc y) ≤ ?B" by (simp add: nz_impl_b_least2_le)
from A1 S2 have S3: "b_least2 f x (Suc y) < Suc y" by (simp)
from S3 have S4: "f x (b_least2 f x (Suc y)) ≠ 0" by (rule b_least2_less_impl_nz)
from S4 have S5: "?B ≤ b_least2 f x (Suc y)" by (rule nz_impl_b_least2_le)
from S2 S5 show ?thesis by simp
qed

lemma b_least2_aux3: "⟦ b_least2 f x y = y; f x y ≠ 0⟧ ⟹ b_least2 f x (Suc y) = y"
proof -
assume A1: "b_least2 f x y =y"
assume A2: "f x y ≠ 0"
from A2 have S1: "b_least2 f x (Suc y) ≤ y" by (rule nz_impl_b_least2_le)
have S2: "b_least2 f x (Suc y) < y ⟹ False"
proof -
assume A2_1: "b_least2 f x (Suc y) < y" (is "?z < _")
from A2_1 have S2_1: "?z < Suc y" by simp
from S2_1 have S2_2: "f x ?z ≠ 0" by (rule b_least2_less_impl_nz)
from A2_1 S2_2 have S2_3: "b_least2 f x y < y" by (rule nz_b_least2_impl_less)
from S2_3 A1 show ?thesis by simp
qed
from S2 have S3: "¬ (b_least2 f x (Suc y) < y)" by auto
from S1 S3 show ?thesis by simp
qed

lemma b_least2_mono: "y1 ≤ y2 ⟹ b_least2 f x y1 ≤ b_least2 f x y2"
proof (rule ccontr)
assume A1: "y1 ≤ y2"
let ?b1 = "b_least2 f x y1" and ?b2 = "b_least2 f x y2"
assume "¬ ?b1 ≤ ?b2" then have A2: "?b2 < ?b1" by simp
have S1: "?b1 ≤ y1" by (rule b_least2_le_arg)
have S2: "?b2 ≤ y2" by (rule b_least2_le_arg)
from A1 A2 S1 S2 have S3: "?b2 < y2" by simp
then have S4: "f x ?b2 ≠ 0" by (rule b_least2_less_impl_nz)
from A2 have S5: "f x ?b2 = 0" by (rule less_b_least2_impl_zero)
from S4 S5 show False by simp
qed

lemma b_least2_aux4: "⟦ b_least2 f x y = y; f x y = 0⟧ ⟹ b_least2 f x (Suc y) = Suc y"
proof -
assume A1: "b_least2 f x y = y"
assume A2: "f x y = 0"
have S1: "b_least2 f x (Suc y) ≤ Suc y" by (rule b_least2_le_arg)
have S2: "y ≤ b_least2 f x (Suc y)"
proof -
have "y ≤ Suc y" by simp
then have "b_least2 f x y ≤ b_least2 f x (Suc y)" by (rule b_least2_mono)
with A1 show ?thesis by simp
qed
from S1 S2  have "b_least2 f x (Suc y) =y ∨ b_least2 f x (Suc y) = Suc y" by arith
moreover
{
assume A3: "b_least2 f x (Suc y) = y"
have "f x y ≠ 0"
proof -
have "y < Suc y" by simp
with A3 have "b_least2 f x (Suc y) < Suc y" by simp
from this have "f x (b_least2 f x (Suc y)) ≠ 0" by (simp add: b_least2_less_impl_nz)
with A3 show "f x y ≠ 0" by simp
qed
with A2 have ?thesis by simp
}
moreover
{
assume "b_least2 f x (Suc y) = Suc y"
then have ?thesis by simp
}
ultimately show ?thesis by blast
qed

lemma b_least2_at_zero: "b_least2 f x 0 = 0"
proof -
have S1: "b_least2 f x 0 ≤ 0" by (rule b_least2_le_arg)
from S1 show ?thesis by auto
qed

theorem pr_b_least2: "f ∈ PrimRec2 ⟹ b_least2 f ∈ PrimRec2"
proof -
define loc_Op1 where "loc_Op1 = (λ (f::nat ⇒ nat ⇒ nat) x y z. (sgn1 (z - y)) * y + (sgn2 (z - y))*((sgn1 (f x z))*z + (sgn2 (f x z))*(Suc z)))"
define loc_Op2 where "loc_Op2 = (λ f. PrimRecOp_last (λ x. 0) (loc_Op1 f))"
have loc_op2_lm_1: "⋀ f x y. loc_Op2 f x y < y ⟹ loc_Op2 f x (Suc y) = loc_Op2 f x y"
proof -
fix f x y
let ?b = "loc_Op2 f x y"
have S1: "loc_Op2 f x (Suc y) = (loc_Op1 f) x ?b y" by (simp add: loc_Op2_def)
assume "?b < y"
then have "y - ?b > 0" by simp
then have "loc_Op1 f x ?b y = ?b" by (simp add: loc_Op1_def)
with S1 show "loc_Op2 f x y < y ⟹ loc_Op2 f x (Suc y) = loc_Op2 f x y" by simp
qed
have loc_op2_lm_2: "⋀ f x y. ⟦¬(loc_Op2 f x y < y); f x y ≠ 0⟧ ⟹ loc_Op2 f x (Suc y) = y"
proof -
fix f x y
let ?b = "loc_Op2 f x y" and ?h = "loc_Op1 f"
have S1: "loc_Op2 f x (Suc y) = ?h x ?b y" by (simp add: loc_Op2_def)
assume "¬(?b < y)"
then have S2: "y - ?b = 0" by simp
assume "f x y ≠ 0"
with S2 have "?h x ?b y = y" by (simp add: loc_Op1_def)
with S1 show "loc_Op2 f x (Suc y) = y" by simp
qed
have loc_op2_lm_3: "⋀ f x y. ⟦¬(loc_Op2 f x y < y); f x y = 0⟧ ⟹ loc_Op2 f x (Suc y) = Suc y"
proof -
fix f x y
let ?b = "loc_Op2 f x y" and ?h = "loc_Op1 f"
have S1: "loc_Op2 f x (Suc y) = ?h x ?b y" by (simp add: loc_Op2_def)
assume "¬(?b < y)"
then have S2: "y - ?b = 0" by simp
assume "f x y = 0"
with S2 have "?h x ?b y = Suc y" by (simp add: loc_Op1_def)
with S1 show "loc_Op2 f x (Suc y) = Suc y" by simp
qed
have Op2_eq_b_least2_at_point: "⋀ f x y. loc_Op2 f x y = b_least2 f x y"
proof - fix f x show "⋀ y. loc_Op2 f x y = b_least2 f x y"
proof (induct_tac y)
show "loc_Op2 f x 0 = b_least2 f x 0" by (simp add: loc_Op2_def b_least2_at_zero)
next
fix y
assume A1: "loc_Op2 f x y = b_least2 f x y"
then show "loc_Op2 f x (Suc y) = b_least2 f x (Suc y)"
proof cases
assume A2: "loc_Op2 f x y < y"
then have S1: "loc_Op2 f x (Suc y) = loc_Op2 f x y" by (rule loc_op2_lm_1)
from A1 A2 have "b_least2 f x y < y" by simp
then have S2: "b_least2 f x (Suc y) = b_least2 f x y" by (rule b_least2_aux2)
from A1 S1 S2 show ?thesis by simp
next
assume A3: "¬ loc_Op2 f x y < y"
have A3': "b_least2 f x y = y"
proof -
have "b_least2 f x y ≤ y" by (rule b_least2_le_arg)
from A1 A3 this show ?thesis by simp
qed
then show ?thesis
proof cases
assume A4: "f x y ≠ 0"
with A3 have S3: "loc_Op2 f x (Suc y) = y" by (rule loc_op2_lm_2)
from A3' A4 have S4: "b_least2 f x (Suc y) = y" by (rule b_least2_aux3)
from S3 S4 show ?thesis by simp
next
assume "¬ f x y ≠  0"
then have A5: "f x y = 0" by simp
with A3 have S5: "loc_Op2 f x (Suc y) = Suc y" by (rule loc_op2_lm_3)
from A3' A5 have S6: "b_least2 f x (Suc y) = Suc y" by (rule b_least2_aux4)
from S5 S6 show ?thesis by simp
qed
qed
qed
qed
have Op2_eq_b_least2: "loc_Op2 = b_least2" by (simp add: Op2_eq_b_least2_at_point ext)
assume A1: "f ∈ PrimRec2"
have pr_loc_Op2: "loc_Op2 f ∈ PrimRec2"
proof -
from A1 have S1: "loc_Op1 f ∈ PrimRec3" by (simp add: loc_Op1_def, prec)
from pr_zero S1 have S2: "PrimRecOp_last (λ x. 0) (loc_Op1 f) ∈ PrimRec2" by (rule pr_rec_last)
from this show ?thesis by (simp add: loc_Op2_def)
qed
from Op2_eq_b_least2 this show "b_least2 f ∈ PrimRec2" by simp
qed

lemma b_least_def1: "b_least f = (λ x. b_least2 f x x)" by (simp add: b_least2_def b_least_def ext)

theorem pr_b_least: "f ∈ PrimRec2 ⟹ b_least f ∈ PrimRec1"
proof -
assume "f ∈ PrimRec2"
then have "b_least2 f ∈ PrimRec2" by (rule pr_b_least2)
from this pr_id1_1 pr_id1_1 have "(λ x. b_least2 f x x) ∈ PrimRec1" by (rule pr_comp2_1)
then show ?thesis by (simp add: b_least_def1)
qed

subsection ‹Examples›

theorem c_sum_as_b_least: "c_sum = (λ u. b_least2 (λ u z. (sgn1 (sf(z+1) - u))) u (Suc u))"
proof (rule ext)
fix u show "c_sum u = b_least2 (λ u z. (sgn1 (sf(z+1) - u))) u (Suc u)"
proof -
have lm_1: "(λ x y. (sgn1 (sf(y+1) - x) ≠ 0)) = (λ x y. (x < sf(y+1)))"
proof (rule ext, rule ext)
fix x y show "(sgn1 (sf(y+1) - x) ≠ 0) = (x < sf(y+1))"
proof -
have "(sgn1 (sf(y+1) - x) ≠ 0) = (sf(y+1) - x > 0)" by (rule sgn1_nz_eq_arg_pos)
thus "(sgn1 (sf(y+1) - x) ≠ 0) = (x < sf(y+1))" by auto
qed
qed (* lm_1 *)
let ?f = "λ u z. (sgn1 (sf(z+1) - u))"
have S1: "?f u u ≠ 0"
proof -
have S1_1: "u+1 ≤ sf(u+1)" by (rule arg_le_sf)
have S1_2: "u < u+1" by simp
from S1_1 S1_2 have S1_3: "u < sf(u+1)" by simp
from S1_3 have S1_4: "sf(u+1) - u > 0" by simp
from S1_4 have S1_5: "sgn1 (sf(u+1)-u) = 1" by simp
from S1_5 show ?thesis by simp
qed
have S3: "u < Suc u" by simp
from S3 S1 have S4: "b_least2 ?f u (Suc u) = (Least (%z. (?f u z) ≠ 0))" by (rule b_least2_less_impl_eq2)
let ?P = "λ u z. ?f u z ≠ 0"
let ?Q = "λ u z. u < sf(z+1)"
from lm_1 have S6: "?P = ?Q" by simp
from S6 have S7: "(%z. ?P u z) = (%z. ?Q u z)" by (rule fun_cong)
from S7 have S8: "(Least (%z. ?P u z)) = (Least (%z. ?Q u z))" by auto
from S4 S8 have S9: "b_least2 ?f u (Suc u) = (Least (%z. u < sf(z+1)))" by (rule trans)
thus ?thesis by (simp add: c_sum_def)
qed
qed

theorem c_sum_is_pr: "c_sum ∈ PrimRec1"
proof -
let ?f = "λ u z. (sgn1 (sf(z+1) - u))"
have S1: "(λ u z. sgn1 ((sf(z+1) - u))) ∈ PrimRec2" by prec
define g where "g = b_least2 ?f"
from g_def S1 have "g ∈ PrimRec2" by (simp add: pr_b_least2)
then have S2: "(λ u. g u (Suc u)) ∈ PrimRec1" by prec
from g_def have "c_sum = (λ u. g u (Suc u))" by (simp add: c_sum_as_b_least ext)
with S2 show ?thesis by simp
qed

theorem c_fst_is_pr [prec]: "c_fst ∈ PrimRec1"
proof -
have S1: "(λ u. c_fst u) = (λ u. (u - sf (c_sum u)))" by (simp add: c_fst_def ext)
from c_sum_is_pr have "(λ u. (u - sf (c_sum u))) ∈ PrimRec1" by prec
with S1 show ?thesis by simp
qed

theorem c_snd_is_pr [prec]: "c_snd ∈ PrimRec1"
proof -
have S1: "c_snd = (λ u. (c_sum u) - (c_fst u))" by (simp add: c_snd_def ext)
from c_sum_is_pr c_fst_is_pr have S2: "(λ u. (c_sum u) - (c_fst u)) ∈ PrimRec1" by prec
from S1 this show ?thesis by simp
qed

theorem pr_1_to_2: "f ∈ PrimRec1 ⟹ (λ x y. f (c_pair x y)) ∈ PrimRec2" by prec

theorem pr_2_to_1: "f ∈ PrimRec2 ⟹ (λ z. f (c_fst z) (c_snd z)) ∈ PrimRec1" by prec

definition "pr_conv_1_to_2 = (λ f x y. f (c_pair x y))"
definition "pr_conv_1_to_3 = (λ f x y z. f (c_pair (c_pair x y) z))"
definition "pr_conv_2_to_1 = (λ f x. f (c_fst x) (c_snd x))"
definition "pr_conv_3_to_1 = (λ f x. f (c_fst (c_fst x)) (c_snd (c_fst x)) (c_snd x))"
definition "pr_conv_3_to_2 = (λ f. pr_conv_1_to_2 (pr_conv_3_to_1 f))"
definition "pr_conv_2_to_3 = (λ f. pr_conv_1_to_3 (pr_conv_2_to_1 f))"

lemma [simp]: "pr_conv_1_to_2 (pr_conv_2_to_1 f) = f" by(simp add: pr_conv_1_to_2_def pr_conv_2_to_1_def)
lemma [simp]: "pr_conv_2_to_1 (pr_conv_1_to_2 f) = f" by(simp add: pr_conv_1_to_2_def pr_conv_2_to_1_def)
lemma [simp]: "pr_conv_1_to_3 (pr_conv_3_to_1 f) = f" by(simp add: pr_conv_1_to_3_def pr_conv_3_to_1_def)
lemma [simp]: "pr_conv_3_to_1 (pr_conv_1_to_3 f) = f" by(simp add: pr_conv_1_to_3_def pr_conv_3_to_1_def)
lemma [simp]: "pr_conv_3_to_2 (pr_conv_2_to_3 f) = f" by(simp add: pr_conv_3_to_2_def pr_conv_2_to_3_def)
lemma [simp]: "pr_conv_2_to_3 (pr_conv_3_to_2 f) = f" by(simp add: pr_conv_3_to_2_def pr_conv_2_to_3_def)

lemma pr_conv_1_to_2_lm: "f ∈ PrimRec1 ⟹ pr_conv_1_to_2 f ∈ PrimRec2" by (simp add: pr_conv_1_to_2_def, prec)
lemma pr_conv_1_to_3_lm: "f ∈ PrimRec1 ⟹ pr_conv_1_to_3 f ∈ PrimRec3" by (simp add: pr_conv_1_to_3_def, prec)
lemma pr_conv_2_to_1_lm: "f ∈ PrimRec2 ⟹ pr_conv_2_to_1 f ∈ PrimRec1" by (simp add: pr_conv_2_to_1_def, prec)
lemma pr_conv_3_to_1_lm: "f ∈ PrimRec3 ⟹ pr_conv_3_to_1 f ∈ PrimRec1" by (simp add: pr_conv_3_to_1_def, prec)
lemma pr_conv_3_to_2_lm: "f ∈ PrimRec3 ⟹ pr_conv_3_to_2 f ∈ PrimRec2"
proof -
assume "f ∈ PrimRec3"
then have "pr_conv_3_to_1 f ∈ PrimRec1" by (rule pr_conv_3_to_1_lm)
thus ?thesis by (simp add: pr_conv_3_to_2_def pr_conv_1_to_2_lm)
qed
lemma pr_conv_2_to_3_lm: "f ∈ PrimRec2 ⟹ pr_conv_2_to_3 f ∈ PrimRec3"
proof -
assume "f ∈ PrimRec2"
then have "pr_conv_2_to_1 f ∈ PrimRec1" by (rule pr_conv_2_to_1_lm)
thus ?thesis by (simp add: pr_conv_2_to_3_def pr_conv_1_to_3_lm)
qed

theorem b_least2_scheme: "⟦ f ∈ PrimRec2; g ∈ PrimRec1; ∀ x. h x < g x; ∀ x. f x (h x) ≠ 0; ∀ z x. z < h x ⟶ f x z = 0 ⟧ ⟹
h ∈ PrimRec1"
proof -
assume f_is_pr: "f ∈ PrimRec2"
assume g_is_pr: "g ∈ PrimRec1"
assume h_lt_g: "∀ x. h x < g x"
assume f_at_h_nz: "∀ x. f x (h x) ≠ 0"
assume h_is_min: "∀ z x. z < h x ⟶ f x z = 0"
have h_def: "h = (λ x. b_least2 f x (g x))"
proof
fix x show "h x = b_least2 f x (g x)"
proof -
from f_at_h_nz have S1: "b_least2 f x (g x) ≤ h x" by (simp add: nz_impl_b_least2_le)
from h_lt_g have "h x < g x" by auto
with S1 have "b_least2 f x (g x) < g x" by simp
then have S2: "f x (b_least2 f x (g x)) ≠ 0" by (rule b_least2_less_impl_nz)
have S3: "h x ≤ b_least2 f x (g x)"
proof (rule ccontr)
assume "¬ h x ≤ b_least2 f x (g x)" then have "b_least2 f x (g x) < h x" by auto
with h_is_min have "f x (b_least2 f x (g x)) = 0" by simp
with S2 show False by auto
qed
from S1 S3 show ?thesis by auto
qed
qed
define f1 where "f1 = b_least2 f"
from f_is_pr f1_def have f1_is_pr: "f1 ∈ PrimRec2" by (simp add: pr_b_least2)
with g_is_pr have "(λ x. f1 x (g x)) ∈ PrimRec1" by prec
with h_def f1_def show "h ∈ PrimRec1" by auto
qed

theorem b_least2_scheme2: "⟦ f ∈ PrimRec3; g ∈ PrimRec2; ∀ x y. h x y < g x y; ∀ x y. f x y (h x y) ≠ 0;
∀ z x y. z < h x y ⟶ f x y z = 0 ⟧ ⟹
h ∈ PrimRec2"
proof -
assume f_is_pr: "f ∈ PrimRec3"
assume g_is_pr: "g ∈ PrimRec2"
assume h_lt_g: "∀ x y. h x y < g x y"
assume f_at_h_nz: "∀ x y. f x y (h x y) ≠ 0"
assume h_is_min: "∀ z x y. z < h x y ⟶ f x y z = 0"
define f1 where "f1 = pr_conv_3_to_2 f"
define g1 where "g1 = pr_conv_2_to_1 g"
define h1 where "h1 = pr_conv_2_to_1 h"
from f_is_pr f1_def have f1_is_pr: "f1 ∈ PrimRec2" by (simp add: pr_conv_3_to_2_lm)
from g_is_pr g1_def have g1_is_pr: "g1 ∈ PrimRec1" by (simp add: pr_conv_2_to_1_lm)
from h_lt_g h1_def g1_def have h1_lt_g1: "∀ x. h1 x < g1 x" by (simp add: pr_conv_2_to_1_def)
from f_at_h_nz f1_def h1_def have f1_at_h1_nz: "∀ x. f1 x (h1 x) ≠ 0" by (simp add: pr_conv_2_to_1_def pr_conv_3_to_2_def pr_conv_3_to_1_def pr_conv_1_to_2_def)
from h_is_min f1_def h1_def have h1_is_min: "∀ z x. z < h1 x ⟶ f1 x z = 0" by (simp add: pr_conv_2_to_1_def pr_conv_3_to_2_def pr_conv_3_to_1_def pr_conv_1_to_2_def)
from f1_is_pr g1_is_pr h1_lt_g1 f1_at_h1_nz h1_is_min have h1_is_pr: "h1 ∈ PrimRec1" by (rule b_least2_scheme)
from h1_def have "h = pr_conv_1_to_2 h1" by simp
with h1_is_pr show "h ∈ PrimRec2" by (simp add: pr_conv_1_to_2_lm)
qed

theorem div_is_pr: "(λ a b. a div b) ∈ PrimRec2"
proof -
define f where "f a b z = (sgn1 b) * (sgn1 (b*(z+1)-a)) + (sgn2 b)*(sgn2 z)" for a b z
have f_is_pr: "f ∈ PrimRec3" unfolding f_def by prec
define h where "h a b = a div b" for a b :: nat
define g where "g a b = a + 1" for a b :: nat
have g_is_pr: "g ∈ PrimRec2" unfolding g_def by prec
have h_lt_g: "∀ a b. h a b < g a b"
proof (rule allI, rule allI)
fix a b
from h_def have "h a b ≤ a" by simp
also from g_def have "a < g a b" by simp
ultimately show "h a b < g a b" by simp
qed
have f_at_h_nz: "∀ a b. f a b (h a b) ≠ 0"
proof (rule allI, rule allI)
fix a b show "f a b (h a b) ≠ 0"
proof cases
assume A: "b = 0"
with h_def have "h a b = 0" by simp
with f_def A show ?thesis by simp
next
assume A: "b ≠ 0"
then have S1: "b > 0" by auto
from A f_def have S2: "f a b (h a b) = sgn1 (b * (h a b + 1) - a)" by simp
then have "?thesis = (sgn1(b * (h a b + 1) - a) ≠ 0)" by auto
also have "… = (b * (h a b + 1) - a > 0)" by (rule sgn1_nz_eq_arg_pos)
also have "… = (a < b * (h a b + 1))" by auto
also have "… = (a < b * (h a b) + b)" by auto
also from h_def have "… = (a < b * (a div b) + b)" by simp
finally have S3: "?thesis = (a < b * (a div b) + b)" by auto
have S4: "a < b * (a div b) + b"
proof -
from S1 have S4_1: "a mod b < b" by (rule mod_less_divisor)
also have S4_2: "b * (a div b) + a mod b = a" by (rule mult_div_mod_eq)
from S4_1 have S4_3: "b * (a div b) + a mod b < b * (a div b) + b" by arith
from S4_2 S4_3 show ?thesis by auto
qed
from S3 S4 show ?thesis by auto
qed
qed
have h_is_min: "∀ z a b. z < h a b ⟶ f a b z = 0"
proof (rule allI, rule allI, rule allI, rule impI)
fix a b z assume A: "z < h a b" show "f a b z = 0"
proof -
from A h_def have S1: "z < a div b" by simp
then have S2: "a div b > 0" by simp
have S3: "b ≠ 0"
proof (rule ccontr)
assume "¬ b ≠ 0" then have "b = 0" by auto
then have "a div b = 0" by auto
with S2 show False by auto
qed
from S3 have b_pos: "0 < b" by auto
from S1 have S4: "z+1 ≤ a div b" by auto
from b_pos have "(b * (z+1) ≤ b * (a div b)) = (z+1 ≤ a div b)" by (rule nat_mult_le_cancel1)
with S4 have S5: "b*(z+1) ≤ b*(a div b)" by simp
moreover have "b*(a div b) ≤ a"
proof -
have "b*(a div b) + (a mod b) = a" by (rule mult_div_mod_eq)
moreover have "0 ≤ a mod b" by auto
ultimately show ?thesis by arith
qed
ultimately have S6: "b*(z+1) ≤ a"
then have "b*(z+1) - a = 0" by auto
with S3 f_def show ?thesis by simp
qed
qed
from f_is_pr g_is_pr h_lt_g f_at_h_nz h_is_min have h_is_pr: "h ∈ PrimRec2" by (rule b_least2_scheme2)
with h_def [abs_def] show ?thesis by simp
qed

theorem mod_is_pr: "(λ a b. a mod b) ∈ PrimRec2"
proof -
have "(λ (a::nat) (b::nat). a mod b) = (λ a b. a - (a div b) * b)"
proof (rule ext, rule ext)
fix a b show "(a::nat) mod b = a - (a div b) * b" by (rule minus_div_mult_eq_mod [symmetric])
qed
also from div_is_pr have "(λ a b. a - (a div b) * b) ∈ PrimRec2" by prec
ultimately show ?thesis by auto
qed

theorem pr_rec_last_scheme: "⟦ g ∈ PrimRec1; h ∈ PrimRec3; ∀ x. f x 0 = g x; ∀ x y. f x (Suc y) = h x (f x y) y ⟧ ⟹ f ∈ PrimRec2"
proof -
assume g_is_pr: "g ∈ PrimRec1"
assume h_is_pr: "h ∈ PrimRec3"
assume f_at_0: "∀ x. f x 0 = g x"
assume f_at_Suc: "∀ x y. f x (Suc y) = h x (f x y) y"
from f_at_0 f_at_Suc have "⋀ x y. f x y = PrimRecOp_last g h x y" by (induct_tac y, simp_all)
then have "f = PrimRecOp_last g h" by (simp add: ext)
with g_is_pr h_is_pr show ?thesis by (simp add: pr_rec_last)
qed

theorem power_is_pr: "(λ (x::nat) (n::nat). x ^ n) ∈ PrimRec2"
proof -
define g :: "nat ⇒ nat" where "g x = 1" for x
define h where "h a b c = a * b" for a b c :: nat
have g_is_pr: "g ∈ PrimRec1" unfolding g_def by prec
have h_is_pr: "h ∈ PrimRec3" unfolding h_def by prec
let ?f = "λ (x::nat) (n::nat). x ^ n"
have f_at_0: "∀ x. ?f x 0 = g x"
proof
fix x show "x ^ 0 = g x" by (simp add: g_def)
qed
have f_at_Suc: "∀ x y. ?f x (Suc y) = h x (?f x y) y"
proof (rule allI, rule allI)
fix x y show "?f x (Suc y) = h x (?f x y) y" by (simp add: h_def)
qed
from g_is_pr h_is_pr f_at_0 f_at_Suc show ?thesis by (rule pr_rec_last_scheme)
qed

end


# File ‹Utils.ML›

(*  Title:      Recursion-Theory-I/Utils.ML
Author:     Michael Nedzelsky, email: MichaelNedzelsky <at> yandex <dot> ru

Some utilities for work with primitive recursive functions.
*)

(******** Utility functions. ***************)

fun extract_prop_arg (Const (@{const_name Pure.prop}, _) $t) = t | extract_prop_arg _ = raise BadArgument fun extract_trueprop_arg (Const (@{const_name "Trueprop"}, _)$ t) = t
| extract_trueprop_arg  _ = raise BadArgument

fun extract_set_args (Const (@{const_name Set.member}, _) $t1$ t2)  = (t1, t2)
| extract_set_args  _ = raise BadArgument

fun get_num_by_set @{const_name PRecFun.PrimRec1} = 1
| get_num_by_set @{const_name PRecFun.PrimRec2} = 2
| get_num_by_set @{const_name PRecFun.PrimRec3} = 3
| get_num_by_set _ = raise BadArgument

fun remove_abs (Abs (_, _, t)) = remove_abs t
| remove_abs t = t

fun extract_free_from_app (t1 \$ t2) (n: int) = extract_free_from_app t1 (n + 1)
| extract_free_from_app (Free (s, tp)) n = (s, tp, n)
| extract_free_from_app (Const (s, tp)) n = (s, tp, n)
| extract_free_from_app _ n = raise BadArgument

fun extract_free_arg t = extract_free_from_app (remove_abs t) 0

fun get_comp_by_indexes (1, 1) = @{thm pr_comp1_1}
| get_comp_by_indexes (1, 2) = @{thm pr_comp1_2}
| get_comp_by_indexes (1, 3) = @{thm pr_comp1_3}
| get_comp_by_indexes (2, 1) = @{thm pr_comp2_1}
| get_comp_by_indexes (2, 2) = @{thm pr_comp2_2}
| get_comp_by_indexes (2, 3) = @{thm pr_comp2_3}
| get_comp_by_indexes (3, 1) = @{thm pr_comp3_1}
| get_comp_by_indexes (3, 2) = @{thm pr_comp3_2}
| get_comp_by_indexes (3, 3) = @{thm pr_comp3_3}
| get_comp_by_indexes _ = raise BadArgument

(************ Tactic. ***************)

fun pr_comp_tac ctxt = SUBGOAL (fn (t, i) =>
let
val t = extract_trueprop_arg (Logic.strip_imp_concl t)
val (t1, t2) = extract_set_args t
val n2 =
let
val Const (s, _) = t2
in
get_num_by_set s
end
val (name, _, n1) = extract_free_arg t1
val comp = get_comp_by_indexes (n1, n2)
in
Rule_Insts.res_inst_tac ctxt
[((("f", 0), Position.none), Variable.revert_fixed ctxt name)] [] comp i
end

fun prec0_tac ctxt facts i =
Method.insert_tac ctxt facts i THEN
REPEAT (assume_tac ctxt i ORELSE pr_comp_tac ctxt i)


# Theory PRecList

(*  Title:       Primitive recursive coding of lists of natural numbers
Author:      Michael Nedzelsky <MichaelNedzelsky at yandex.ru>, 2008
Maintainer:  Michael Nedzelsky <MichaelNedzelsky at yandex.ru>
*)

section ‹Primitive recursive coding of lists of natural numbers›

theory PRecList
imports PRecFun
begin

text ‹
We introduce a particular coding ‹list_to_nat› from lists of
natural numbers to natural numbers.
›

definition
c_len :: "nat ⇒ nat" where
"c_len = (λ (u::nat). (sgn1 u) * (c_fst(u-(1::nat))+1))"

lemma c_len_1: "c_len u = (case u of 0 ⇒ 0 | Suc v ⇒ c_fst(v)+1)" by (unfold c_len_def, cases u, auto)

lemma c_len_is_pr: "c_len ∈ PrimRec1" unfolding c_len_def by prec

lemma [simp]: "c_len 0 = 0" by (simp add: c_len_def)

lemma c_len_2: "u ≠ 0 ⟹ c_len u = c_fst(u-(1::nat))+1" by (simp add: c_len_def)

lemma c_len_3: "u>0 ⟹ c_len u > 0" by (simp add: c_len_2)

lemma c_len_4: "c_len u = 0 ⟹ u = 0"
proof cases
assume A1: "u = 0"
thus ?thesis by simp
next
assume A1: "c_len u = 0" and A2: "u ≠ 0"
from A2 have "c_len u > 0" by (simp add: c_len_3)
from A1 this show "u=0" by simp
qed

lemma c_len_5: "c_len u > 0 ⟹ u > 0"
proof cases
assume A1: "c_len u > 0" and A2: "u=0"
from A2 have "c_len u = 0" by simp
from A1 this show ?thesis by simp
next
assume A1: "u ≠ 0"
from A1 show "u>0" by simp
qed

fun c_fold :: "nat list ⇒ nat" where
"c_fold [] = 0"
| "c_fold [x] = x"
| "c_fold (x#ls) = c_pair x (c_fold ls)"

lemma c_fold_0: "ls ≠ [] ⟹ c_fold (x#ls) = c_pair x (c_fold ls)"
proof -
assume A1: "ls ≠ []"
then have S1: "ls = (hd ls)#(tl ls)" by simp
then have S2: "x#ls = x#(hd ls)#(tl ls)" by simp
have S3: "c_fold (x#(hd ls)#(tl ls)) = c_pair x (c_fold ((hd ls)#(tl ls)))" by simp
from S1 S2 S3 show ?thesis by simp
qed

primrec
c_unfold :: "nat ⇒ nat ⇒ nat list"
where
"c_unfold 0 u = []"
| "c_unfold (Suc k) u = (if k = 0 then [u] else ((c_fst u) # (c_unfold k (c_snd u))))"

lemma c_fold_1: "c_unfold 1 (c_fold [x]) = [x]" by simp

lemma c_fold_2: "c_fold (c_unfold 1 u) = u" by simp

lemma c_unfold_1: "c_unfold 1 u = [u]" by simp

lemma c_unfold_2: "c_unfold (Suc 1) u = (c_fst u) # (c_unfold 1 (c_snd u))" by simp

lemma c_unfold_3: "c_unfold (Suc 1) u = [c_fst u, c_snd u]" by simp

lemma c_unfold_4: "k > 0 ⟹ c_unfold (Suc k) u = (c_fst u) # (c_unfold k (c_snd u))" by simp

lemma c_unfold_4_1: "k > 0 ⟹ c_unfold (Suc k) u ≠ []" by (simp add: c_unfold_4)

lemma two: "(2::nat) = Suc 1" by simp

lemma c_unfold_5: "c_unfold 2 u = [c_fst u, c_snd u]" by (simp add: two)

lemma c_unfold_6: "k>0 ⟹ c_unfold k u ≠ []"
proof -
assume A1: "k>0"
let ?k1 = "k-(1::nat)"
from A1 have S1: "k = Suc ?k1" by simp
have S2: "?k1 = 0 ⟹ ?thesis"
proof -
assume A2_1: "?k1=0"
from A1 A2_1 have S2_1: "k=1" by simp
from S2_1 show ?thesis by (simp add: c_unfold_1)
qed
have S3: "?k1 > 0 ⟹ ?thesis"
proof -
assume A3_1: "?k1 > 0"
from A3_1 have S3_1: "c_unfold (Suc ?k1) u ≠ []" by (rule c_unfold_4_1)
from S1 S3_1 show ?thesis by simp
qed
from S2 S3 show ?thesis by arith
qed

lemma th_lm_1: "k=1 ⟹ (∀ u. c_fold (c_unfold k u) = u)" by (simp add: c_fold_2)

lemma th_lm_2: "⟦k>0; (∀ u. c_fold (c_unfold k u) = u)⟧ ⟹ (∀ u. c_fold (c_unfold (Suc k) u) = u)"
proof
assume A1: "k>0"
assume A2: "∀ u. c_fold (c_unfold k u) = u"
fix u
from A1 have S1: "c_unfold (Suc k) u = (c_fst u) # (c_unfold k (c_snd u))" by (rule c_unfold_4)
let ?ls = "c_unfold k (c_snd u)"
from A1 have S2: "?ls ≠ []" by (rule c_unfold_6)
from S2 have S3: "c_fold ( (c_fst u) # ?ls) = c_pair (c_fst u) (c_fold ?ls)" by (rule c_fold_0)
from A2 have S4: "c_fold ?ls = c_snd u" by simp
from S3 S4 have S5: "c_fold ( (c_fst u) # ?ls) = c_pair (c_fst u) (c_snd u)" by simp
from S5 have S6: "c_fold ( (c_fst u) # ?ls) = u" by simp
from S1 S6 have S7: "c_fold (c_unfold (Suc k) u) = u" by simp
thus "c_fold (c_unfold (Suc k) u) = u" .
qed

lemma th_lm_3: "(∀ u. c_fold (c_unfold (Suc k) u) = u)⟹ (∀ u. c_fold (c_unfold (Suc (Suc k)) u) = u)"
proof -
assume A1: "∀ u. c_fold (c_unfold (Suc k) u) = u"
let ?k1 = "Suc k"
have S1: "?k1 > 0" by simp
from S1 A1 have S2: "∀ u. c_fold (c_unfold (Suc ?k1) u) = u" by (rule th_lm_2)
thus ?thesis by simp
qed

theorem th_1: "∀ u. c_fold (c_unfold (Suc k) u) = u"
apply(induct k)
apply(rule th_lm_3)
apply(assumption)
done

theorem th_2: "k > 0 ⟹ (∀ u. c_fold (c_unfold k u) = u)"
proof -
assume A1: "k>0"
let ?k1 = "k-(1::nat)"
from A1 have S1: "Suc ?k1 = k" by simp
have S2: "∀ u. c_fold (c_unfold (Suc ?k1) u) = u" by (rule th_1)
from S1 S2 show ?thesis by simp
qed

lemma c_fold_3: "c_unfold 2 (c_fold [x, y]) = [x, y]" by (simp add: two)

theorem c_unfold_len: "ALL u. length (c_unfold k u) = k"
apply(induct k)
apply(simp)
apply(subgoal_tac "n=(0::nat) ∨ n>0")
apply(drule disjE)
prefer 3
apply(simp_all)
apply(auto)
done

lemma th_3_lm_0: "⟦c_unfold (length ls) (c_fold ls) = ls; ls = a # ls1; ls1 = aa # list⟧ ⟹ c_unfold (length (x # ls)) (c_fold (x # ls)) = x # ls"
proof -
assume A1: "c_unfold (length ls) (c_fold ls) = ls"
assume A2: "ls = a # ls1"
assume A3: "ls1 = aa # list"
from A2 have S1: "ls ≠ []" by simp
from S1 have S2: "c_fold (x#ls) = c_pair x (c_fold ls)" by (rule c_fold_0)
have S3: "length (x#ls) = Suc (length ls)" by simp
from S3 have S4: "c_unfold (length (x # ls)) (c_fold (x # ls)) = c_unfold (Suc (length ls)) (c_fold (x # ls))" by simp
from A2 have S5: "length ls > 0" by simp
from S5 have S6: "c_unfold (Suc (length ls)) (c_fold (x # ls)) = c_fst (c_fold (x # ls))#(c_unfold (length ls) (c_snd (c_fold (x#ls))))" by (rule c_unfold_4)
from S2 have S7: "c_fst (c_fold (x#ls)) = x" by simp
from S2 have S8: "c_snd (c_fold (x#ls)) = c_fold ls" by simp
from S6 S7 S8 have S9: "c_unfold (Suc (length ls)) (c_fold (x # ls)) = x # (c_unfold (length ls) (c_fold ls))" by simp
from A1 have S10: "x # (c_unfold (length ls) (c_fold ls)) = x # ls" by simp
from S9 S10 have S11: "c_unfold (Suc (length ls)) (c_fold (x # ls)) = (x # ls)" by simp
thus ?thesis by simp
qed

lemma th_3_lm_1: "⟦c_unfold (length ls) (c_fold ls) = ls; ls = a # ls1⟧ ⟹ c_unfold (length (x # ls)) (c_fold (x # ls)) = x # ls"
apply(cases ls1)
apply(simp)
done

lemma th_3_lm_2: "c_unfold (length ls) (c_fold ls) = ls ⟹ c_unfold (length (x # ls)) (c_fold (x # ls)) = x # ls"
apply(cases ls)
apply(rule th_3_lm_1)
apply(assumption+)
done

theorem th_3: "c_unfold (length ls) (c_fold ls) = ls"
apply(induct ls)
apply(simp)
apply(rule th_3_lm_2)
apply(assumption)
done

definition
list_to_nat :: "nat list ⇒ nat" where
"list_to_nat = (λ ls. if ls=[] then 0 else (c_pair ((length ls) - 1) (c_fold ls))+1)"

definition
nat_to_list :: "nat ⇒ nat list" where
"nat_to_list = (λ u. if u=0 then [] else (c_unfold (c_len u) (c_snd (u-(1::nat)))))"

lemma nat_to_list_of_pos: "u>0 ⟹ nat_to_list u = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (simp add: nat_to_list_def)

theorem list_to_nat_th [simp]: "list_to_nat (nat_to_list u) = u"
proof -
have S1: "u=0 ⟹ ?thesis" by (simp add: list_to_nat_def nat_to_list_def)
have S2: "u>0 ⟹ ?thesis"
proof -
assume A1: "u>0"
define ls where "ls = nat_to_list u"
from ls_def A1 have S2_1: "ls = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (simp add: nat_to_list_def)
let ?k = "c_len u"
from A1 have S2_2: "?k > 0" by (rule c_len_3)
from S2_1 have S2_3: "length ls = ?k" by (simp add: c_unfold_len)
from S2_2 S2_3 have S2_4: "length ls > 0" by simp
from S2_4 have S2_5: "ls ≠ []" by simp
from S2_5 have S2_6: "list_to_nat ls = c_pair ((length ls)-(1::nat)) (c_fold ls)+1" by (simp add: list_to_nat_def)
have S2_7: "c_fold ls = c_snd(u-(1::nat))"
proof -
from S2_1 have S2_7_1: "c_fold ls = c_fold (c_unfold (c_len u) (c_snd (u-(1::nat))))" by simp
from S2_2 S2_7_1 show ?thesis by (simp add: th_2)
qed
have S2_8: "(length ls)-(1::nat) = c_fst (u-(1::nat))"
proof -
from S2_3 have S2_8_1: "length ls = c_len u" by simp
from A1 S2_8_1 have S2_8_2: "length ls = c_fst(u-(1::nat)) + 1" by (simp add: c_len_2)
from S2_8_2 show ?thesis by simp
qed
from S2_7 S2_8 have S2_9: "c_pair ((length ls)-(1::nat)) (c_fold ls) = c_pair (c_fst (u-(1::nat))) (c_snd (u-(1::nat)))" by simp
from S2_9 have S2_10: "c_pair ((length ls)-(1::nat)) (c_fold ls) = u - (1::nat)" by simp
from S2_6 S2_10 have S2_11: "list_to_nat ls = (u - (1::nat))+1" by simp
from A1 have S2_12: "(u - (1::nat))+1 = u" by simp
from ls_def S2_11 S2_12 show ?thesis by simp
qed
from S1 S2 show ?thesis by arith
qed

theorem nat_to_list_th [simp]: "nat_to_list (list_to_nat ls) = ls"
proof -
have S1: "ls=[] ⟹ ?thesis" by (simp add: nat_to_list_def list_to_nat_def)
have S2: "ls ≠ [] ⟹ ?thesis"
proof -
assume A1: "ls ≠ []"
define u where "u = list_to_nat ls"
from u_def A1 have S2_1: "u = (c_pair ((length ls)-(1::nat)) (c_fold ls))+1" by (simp add: list_to_nat_def)
let ?k = "length ls"
from A1 have S2_2: "?k > 0" by simp
from S2_1 have S2_3: "u>0" by simp
from S2_3 have S2_4: "nat_to_list u = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (simp add: nat_to_list_def)
have S2_5: "c_len u = length ls"
proof -
from S2_1 have S2_5_1: "u-(1::nat) = c_pair ((length ls)-(1::nat)) (c_fold ls)" by simp
from S2_5_1 have S2_5_2: "c_fst (u-(1::nat)) = (length ls)-(1::nat)" by simp
from S2_2 S2_5_2 have "c_fst (u-(1::nat))+1 = length ls" by simp
from S2_3 this show ?thesis by (simp add: c_len_2)
qed
have S2_6: "c_snd (u-(1::nat)) = c_fold ls"
proof -
from S2_1 have S2_6_1: "u-(1::nat) = c_pair ((length ls)-(1::nat)) (c_fold ls)" by simp
from S2_6_1 show ?thesis by simp
qed
from S2_4 S2_5 S2_6 have S2_7:"nat_to_list u = c_unfold (length ls) (c_fold ls)" by simp
from S2_7 have "nat_to_list u = ls" by (simp add: th_3)
from u_def this show ?thesis by simp
qed
have S3: "ls = [] ∨ ls ≠ []" by simp
from S1 S2 S3 show ?thesis by auto
qed

lemma [simp]: "list_to_nat [] = 0" by (simp add: list_to_nat_def)

lemma [simp]: "nat_to_list 0 = []" by (simp add: nat_to_list_def)

theorem c_len_th_1: "c_len (list_to_nat ls) = length ls"
proof (cases)
assume "ls=[]"
from this show ?thesis by simp
next
assume S1: "ls ≠ []"
then have S2: "list_to_nat ls = c_pair ((length ls)-(1::nat)) (c_fold ls)+1" by (simp add: list_to_nat_def)
let ?u = "list_to_nat ls"
from S2 have u_not_zero: "?u > 0" by simp
from S2 have S3: "?u-(1::nat) = c_pair ((length ls)-(1::nat)) (c_fold ls)" by simp
then have S4: "c_fst(?u-(1::nat)) = (length ls)-(1::nat)" by simp
from S1 this have S5: "c_fst(?u-(1::nat))+1=length ls" by simp
from u_not_zero S5 have S6: "c_len (?u) = length ls" by (simp add: c_len_2)
from S1 S6 show ?thesis by simp
qed

theorem "length (nat_to_list u) = c_len u"
proof -
let ?ls = "nat_to_list u"
have S1: "u = list_to_nat ?ls" by (rule list_to_nat_th [THEN sym])
from c_len_th_1 have S2: "length ?ls = c_len (list_to_nat ?ls)" by (rule sym)
from S1 S2 show ?thesis by (rule ssubst)
qed

definition
c_hd :: "nat ⇒ nat" where
"c_hd = (λ u. if u=0 then 0 else hd (nat_to_list u))"

definition
c_tl :: "nat ⇒ nat" where
"c_tl = (λ u. list_to_nat (tl (nat_to_list u)))"

definition
c_cons :: "nat ⇒ nat ⇒ nat" where
"c_cons = (λ x u. list_to_nat (x # (nat_to_list u)))"

lemma [simp]: "c_hd 0 = 0" by (simp add: c_hd_def)

lemma c_hd_aux0: "c_len u = 1 ⟹ nat_to_list u = [c_snd (u-(1::nat))]" by (simp add: nat_to_list_def c_len_5)

lemma c_hd_aux1: "c_len u = 1 ⟹ c_hd u = c_snd (u-(1::nat))"
proof -
assume A1: "c_len u = 1"
then have S1: "nat_to_list u = [c_snd (u-(1::nat))]" by (simp add: nat_to_list_def c_len_5)
from A1 have "u > 0" by (simp add: c_len_5)
with S1 show ?thesis by (simp add: c_hd_def)
qed

lemma c_hd_aux2: "c_len u > 1 ⟹ c_hd u = c_fst (c_snd (u-(1::nat)))"
proof -
assume A1: "c_len u > 1"
let ?k = "(c_len u) - 1"
from A1 have S1: "c_len u = Suc ?k" by simp
from A1 have S2: "c_len u > 0" by simp
from S2 have S3: "u > 0" by (rule c_len_5)
from S3 have S4: "c_hd u = hd (nat_to_list u)" by (simp add: c_hd_def)
from S3 have S5: "nat_to_list u = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (rule nat_to_list_of_pos)
from S1 S5 have S6: "nat_to_list u = c_unfold (Suc ?k) (c_snd (u-(1::nat)))" by simp
from A1 have S7: "?k > 0" by simp
from S7 have S8: "c_unfold (Suc ?k) (c_snd (u-(1::nat))) = (c_fst (c_snd (u-(1::nat)))) # (c_unfold ?k (c_snd (c_snd (u-(1::nat)))))" by (rule c_unfold_4)
from S6 S8 have S9: "nat_to_list u = (c_fst (c_snd (u-(1::nat)))) # (c_unfold ?k (c_snd (c_snd (u-(1::nat)))))" by simp
from S9 have S10: "hd (nat_to_list u) = c_fst (c_snd (u-(1::nat)))" by simp
from S4 S10 show ?thesis by simp
qed

lemma c_hd_aux3: "u > 0 ⟹ c_hd u = (if (c_len u) = 1 then c_snd (u-(1::nat)) else c_fst (c_snd (u-(1::nat))))"
proof -
assume A1: "u > 0"
from A1 have "c_len u > 0" by (rule c_len_3)
then have S1: "c_len u = 1 ∨ c_len u > 1" by arith
let ?tmp = "if (c_len u) = 1 then c_snd (u-(1::nat)) else c_fst (c_snd (u-(1::nat)))"
have S2: "c_len u = 1 ⟹ ?thesis"
proof -
assume A2_1: "c_len u = 1"
then have S2_1: "c_hd u = c_snd (u-(1::nat))" by (rule c_hd_aux1)
from A2_1 have S2_2: "?tmp = c_snd(u-(1::nat))" by simp
from S2_1 this show ?thesis by simp
qed
have S3: "c_len u > 1 ⟹ ?thesis"
proof -
assume A3_1: "c_len u > 1"
from A3_1 have S3_1: "c_hd u = c_fst (c_snd (u-(1::nat)))" by (rule c_hd_aux2)
from A3_1 have S3_2: "?tmp = c_fst (c_snd (u-(1::nat)))" by simp
from S3_1 this show ?thesis by simp
qed
from S1 S2 S3 show ?thesis by auto
qed

lemma c_hd_aux4: "c_hd u = (if u=0 then 0 else (if (c_len u) = 1 then c_snd (u-(1::nat)) else c_fst (c_snd (u-(1::nat)))))"
proof cases
assume "u=0" then show ?thesis by simp
next
assume "u ≠ 0" then have A1: "u > 0" by simp
then show ?thesis by (simp add: c_hd_aux3)
qed

lemma c_hd_is_pr: "c_hd ∈ PrimRec1"
proof -
have "c_hd = (%u. (if u=0 then 0 else (if (c_len u) = 1 then c_snd (u-(1::nat)) else c_fst (c_snd (u-(1::nat))))))" (is "_ = ?R")  by (simp add: c_hd_aux4 ext)
moreover have "?R ∈ PrimRec1"
proof (rule if_is_pr)
show "(λ x. x) ∈ PrimRec1" by (rule pr_id1_1)
next show "(λ x. 0) ∈ PrimRec1" by (rule pr_zero)
next show "(λx. if c_len x = 1 then c_snd (x - 1) else c_fst (c_snd (x - 1))) ∈ PrimRec1"
proof (rule if_eq_is_pr)
show "c_len ∈ PrimRec1" by (rule c_len_is_pr)
next show "(λ x. 1) ∈ PrimRec1" by (rule const_is_pr)
next show "(λx. c_snd (x - 1)) ∈ PrimRec1" by prec
next show "(λx. c_fst (c_snd (x - 1))) ∈ PrimRec1" by prec
qed
qed
ultimately show ?thesis by simp
qed

lemma [simp]: "c_tl 0 = 0" by (simp add: c_tl_def)

lemma c_tl_eq_tl: "c_tl (list_to_nat ls) = list_to_nat (tl ls)" by (simp add: c_tl_def)

lemma tl_eq_c_tl: "tl (nat_to_list x) = nat_to_list (c_tl x)" by (simp add: c_tl_def)

lemma c_tl_aux1: "c_len u = 1 ⟹ c_tl u = 0" by (unfold c_tl_def, simp add: c_hd_aux0)

lemma c_tl_aux2: "c_len u > 1 ⟹ c_tl u = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1"
proof -
assume A1: "c_len u > 1"
let ?k = "(c_len u) - 1"
from A1 have S1: "c_len u = Suc ?k" by simp
from A1 have S2: "c_len u > 0" by simp
from S2 have S3: "u > 0" by (rule c_len_5)
from S3 have S4: "nat_to_list u = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (rule nat_to_list_of_pos)
from A1 have S5: "?k > 0" by simp
from S5 have S6: "c_unfold (Suc ?k) (c_snd (u-(1::nat))) = (c_fst (c_snd (u-(1::nat)))) # (c_unfold ?k (c_snd (c_snd (u-(1::nat)))))" by (rule c_unfold_4)
from S6 have S7: "tl (c_unfold (Suc ?k) (c_snd (u-(1::nat)))) = c_unfold ?k (c_snd (c_snd (u-(1::nat))))" by simp
from S2 S4 S7 have S8: "tl (nat_to_list u) = c_unfold ?k (c_snd (c_snd (u-(1::nat))))" by simp
define ls where "ls = tl (nat_to_list u)"
from ls_def S8 have S9: "length ls = ?k" by (simp add: c_unfold_len)
from ls_def have S10: "c_tl u = list_to_nat ls" by (simp add: c_tl_def)
from S5 S9 have S11: "length ls > 0" by simp
from S11 have S12: "ls ≠ []" by simp
from S12 have S13: "list_to_nat ls = (c_pair ((length ls) - 1) (c_fold ls))+1" by (simp add: list_to_nat_def)
from S10 S13 have S14: "c_tl u = (c_pair ((length ls) - 1) (c_fold ls))+1" by simp
from S9 have S15: "(length ls)-(1::nat) = ?k-(1::nat)" by simp
from A1 have S16: "?k-(1::nat) = c_len u - (2::nat)" by arith
from S15 S16 have S17: "(length ls)-(1::nat) = c_len u - (2::nat)" by simp
from ls_def S8 have S18: "ls = c_unfold ?k (c_snd (c_snd (u-(1::nat))))" by simp
from S5 have S19: "c_fold (c_unfold ?k (c_snd (c_snd (u-(1::nat))))) = c_snd (c_snd (u-(1::nat)))" by (simp add: th_2)
from S18 S19 have S20: "c_fold ls = c_snd (c_snd (u-(1::nat)))" by simp
from S14 S17 S20 show ?thesis by simp
qed

lemma c_tl_aux3: "c_tl u = (sgn1 ((c_len u) - 1))*((c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1)" (is "_ = ?R")
proof -
have S1: "u=0 ⟹ ?thesis" by simp
have S2: "u>0 ⟹ ?thesis"
proof -
assume A1: "u>0"
have S2_1: "c_len u = 1 ⟹ ?thesis" by (simp add: c_tl_aux1)
have S2_2: "c_len u ≠ 1 ⟹ ?thesis"
proof -
assume A2_2_1: "c_len u ≠ 1"
from A1 have S2_2_1: "c_len u > 0" by (rule c_len_3)
from A2_2_1 S2_2_1 have S2_2_2: "c_len u > 1" by arith
from this have S2_2_3: "c_len u - 1 > 0" by simp
from this have S2_2_4: "sgn1 (c_len u - 1)=1" by simp
from S2_2_4 have S2_2_5: "?R = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1" by simp
from S2_2_2 have S2_2_6: "c_tl u = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1" by (rule c_tl_aux2)
from S2_2_5 S2_2_6 show ?thesis by simp
qed
from S2_1 S2_2 show ?thesis by blast
qed
from S1 S2 show ?thesis by arith
qed

lemma c_tl_less: "u > 0 ⟹ c_tl u < u"
proof -
assume A1: "u > 0"
then have S1: "c_len u > 0" by (rule c_len_3)
then show ?thesis
proof cases
assume "c_len u = 1"
from this A1 show ?thesis by (simp add: c_tl_aux1)
next
assume "¬ c_len u = 1" with S1 have A2: "c_len u > 1" by simp
then have S2: "c_tl u = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1" by (rule c_tl_aux2)
from A1 have S3: "c_len u = c_fst(u-(1::nat))+1" by (simp add: c_len_def)
from A2 S3 have S4: "c_len u - (2::nat) < c_fst(u-(1::nat))" by simp
then have S5: "(c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) < (c_pair (c_fst(u-(1::nat))) (c_snd (c_snd (u-(1::nat)))))" by (rule c_pair_strict_mono1)
have S6: "c_snd (c_snd (u-(1::nat))) ≤ c_snd (u-(1::nat))" by (rule c_snd_le_arg)
then have S7: "(c_pair (c_fst(u-(1::nat))) (c_snd (c_snd (u-(1::nat))))) ≤ (c_pair (c_fst(u-(1::nat))) (c_snd (u-(1::nat))))" by (rule c_pair_mono2)
then have S8: "(c_pair (c_fst(u-(1::nat))) (c_snd (c_snd (u-(1::nat))))) ≤ u-(1::nat)" by simp
with S5 have "(c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) < u - (1::nat)" by simp
with S2 have "c_tl u < (u-(1::nat))+1" by simp
with A1 show ?thesis by simp
qed
qed

lemma c_tl_le: "c_tl u ≤ u"
proof (cases u)
assume "u=0"
then show ?thesis by simp
next
fix v assume A1: "u = Suc v"
then have S1: "u > 0" by simp
then have S2: "c_tl u < u" by (rule c_tl_less)
with A1 show "c_tl u ≤ u" by simp
qed

theorem c_tl_is_pr: "c_tl ∈ PrimRec1"
proof -
have "c_tl = (λ u. (sgn1 ((c_len u) - 1))*((c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1))" (is "_ = ?R") by (simp add: c_tl_aux3 ext)
moreover from c_len_is_pr c_pair_is_pr have "?R ∈ PrimRec1" by prec
ultimately show ?thesis by simp
qed

lemma c_cons_aux1: "c_cons x 0 = (c_pair 0 x) + 1"
apply(unfold c_cons_def)
apply(simp)
apply(unfold list_to_nat_def)
apply(simp)
done

lemma c_cons_aux2: "u > 0 ⟹ c_cons x u = (c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1"
proof -
assume A1: "u > 0"
from A1 have S1: "c_len u > 0" by (rule c_len_3)
from A1 have S2: "nat_to_list u = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (rule nat_to_list_of_pos)
define ls where "ls = nat_to_list u"
from ls_def S2 have S3: "ls = c_unfold (c_len u) (c_snd (u-(1::nat)))" by simp
from S3 have S4: "length ls = c_len u" by (simp add: c_unfold_len)
from S4 S1 have S5: "length ls > 0" by simp
from S5 have S6: "ls ≠ []" by simp
from ls_def have S7: "c_cons x u = list_to_nat (x # ls)" by (simp add: c_cons_def)
have S8: "list_to_nat (x # ls) = (c_pair ((length (x#ls))-(1::nat)) (c_fold (x#ls)))+1" by (simp add: list_to_nat_def)
have S9: "(length (x#ls))-(1::nat) = length ls" by simp
from S9 S4 S8 have S10: "list_to_nat (x # ls) = (c_pair (c_len u) (c_fold (x#ls)))+1" by simp
have S11: "c_fold (x#ls) = c_pair x (c_snd (u-(1::nat)))"
proof -
from S6 have S11_1: "c_fold (x#ls) = c_pair x (c_fold ls)" by (rule c_fold_0)
from S3 have S11_2: "c_fold ls = c_fold (c_unfold (c_len u) (c_snd (u-(1::nat))))" by simp
from S1 S11_2 have S11_3: "c_fold ls = c_snd (u-(1::nat))" by (simp add: th_2)
from S11_1 S11_3 show ?thesis by simp
qed
from S7 S10 S11 show ?thesis by simp
qed

lemma c_cons_aux3: "c_cons = (λ x u. (sgn2 u)*((c_pair 0 x)+1) + (sgn1 u)*((c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1))"
proof (rule ext, rule ext)
fix x u show "c_cons x u = (sgn2 u)*((c_pair 0 x)+1) + (sgn1 u)*((c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1)" (is "_ = ?R")
proof cases
assume A1: "u=0"
then have "?R = (c_pair 0 x)+1" by simp
moreover from A1 have "c_cons x u = (c_pair 0 x)+1" by (simp add: c_cons_aux1)
ultimately show ?thesis by simp
next
assume A1: "u≠0"
then have S1: "?R = (c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1" by simp
from A1 have S2: "c_cons x u = (c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1" by (simp add: c_cons_aux2)
from S1 S2 have "c_cons x u = ?R" by simp
then show ?thesis .
qed
qed

lemma c_cons_pos: "c_cons x u > 0"
proof cases
assume "u=0"
then show "c_cons x u > 0" by (simp add: c_cons_aux1)
next
assume "¬ u=0" then have "u>0" by simp
then show "c_cons x u > 0" by (simp add: c_cons_aux2)
qed

theorem c_cons_is_pr: "c_cons ∈ PrimRec2"
proof -
have "c_cons = (λ x u. (sgn2 u)*((c_pair 0 x)+1) + (sgn1 u)*((c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1))" (is "_ = ?R") by (simp add: c_cons_aux3)
moreover from c_pair_is_pr c_len_is_pr have "?R ∈ PrimRec2" by prec
ultimately show ?thesis by simp
qed

definition
c_drop :: "nat ⇒ nat ⇒ nat" where
"c_drop = PrimRecOp (λ x. x) (λ x y z. c_tl y)"

lemma c_drop_at_0 [simp]: "c_drop 0 x = x" by (simp add: c_drop_def)

lemma c_drop_at_Suc: "c_drop (Suc y) x = c_tl (c_drop y x)" by (simp add: c_drop_def)

theorem c_drop_is_pr: "c_drop ∈ PrimRec2"
proof -
have "(λ x. x) ∈ PrimRec1" by (rule pr_id1_1)
moreover from c_tl_is_pr have "(λ x y z. c_tl y) ∈ PrimRec3" by prec
ultimately show ?thesis by (simp add: c_drop_def pr_rec)
qed

lemma c_tl_c_drop: "c_tl (c_drop y x) = c_drop y (c_tl x)"
apply(induct y)
apply(simp)
done

lemma c_drop_at_Suc1: "c_drop (Suc y) x = c_drop y (c_tl x)"
done

lemma c_drop_df: "∀ ls. drop n ls = nat_to_list (c_drop n (list_to_nat ls))"
proof (induct n)
show "∀ ls. drop 0 ls = nat_to_list (c_drop 0 (list_to_nat ls))" by (simp add: c_drop_def)
next
fix n assume A1: "∀ ls. drop n ls = nat_to_list (c_drop n (list_to_nat ls))"
then show "∀ ls. drop (Suc n) ls = nat_to_list (c_drop (Suc n) (list_to_nat ls))"
proof -
{
fix ls::"nat list"
have S1: "drop (Suc n) ls = drop n (tl ls)" by (rule drop_Suc)
from A1 have S2: "drop n (tl ls) = nat_to_list (c_drop n (list_to_nat (tl ls)))" by simp
also have "… = nat_to_list (c_drop n (c_tl (list_to_nat ls)))" by  (simp add: c_tl_eq_tl)
also have "… = nat_to_list (c_drop (Suc n) (list_to_nat ls))" by  (simp add: c_drop_at_Suc1)
finally have "drop n (tl ls) = nat_to_list (c_drop (Suc n) (list_to_nat ls))" by simp
with S1 have "drop (Suc n) ls = nat_to_list (c_drop (Suc n) (list_to_nat ls))" by simp
}
then show ?thesis by blast
qed
qed

definition
c_nth :: "nat ⇒ nat ⇒ nat" where
"c_nth = (λ x n. c_hd (c_drop n x))"

lemma c_nth_is_pr: "c_nth ∈ PrimRec2"
proof (unfold c_nth_def)
from c_hd_is_pr c_drop_is_pr show "(λx n. c_hd (c_drop n x)) ∈ PrimRec2" by prec
qed

lemma c_nth_at_0: "c_nth x 0 = c_hd x" by (simp add: c_nth_def)

lemma c_hd_c_cons [simp]: "c_hd (c_cons x y) = x"
proof -
have "c_cons x y > 0" by (rule c_cons_pos)
then show ?thesis by (simp add: c_hd_def c_cons_def)
qed

lemma c_tl_c_cons [simp]: "c_tl (c_cons x y) = y" by (simp add: c_tl_def c_cons_def)

definition
c_f_list :: "(nat ⇒ nat ⇒ nat) ⇒ nat ⇒ nat ⇒ nat" where
"c_f_list = (λ f.
let g = (%x. c_cons (f 0 x) 0); h = (%a b c. c_cons (f (Suc a) c) b) in PrimRecOp g h)"

lemma c_f_list_at_0: "c_f_list f 0 x = c_cons (f 0 x) 0" by (simp add: c_f_list_def Let_def)

lemma c_f_list_at_Suc: "c_f_list f (Suc y) x = c_cons (f (Suc y) x) (c_f_list f y x)" by ((simp add: c_f_list_def Let_def))

lemma c_f_list_is_pr: "f ∈ PrimRec2 ⟹ c_f_list f ∈ PrimRec2"
proof -
assume A1: "f ∈ PrimRec2"
let ?g = "(%x. c_cons (f 0 x) 0)"
from A1 c_cons_is_pr have S1: "?g ∈ PrimRec1" by prec
let ?h = "(%a b c. c_cons (f (Suc a) c) b)"
from A1 c_cons_is_pr have S2: "?h ∈ PrimRec3" by prec
from S1 S2 show ?thesis by (simp add: pr_rec c_f_list_def Let_def)
qed

lemma c_f_list_to_f_0: "f y x = c_hd (c_f_list f y x)"
apply(induct y)
done

lemma c_f_list_to_f: "f = (λ y x. c_hd (c_f_list f y x))"
apply(rule ext, rule ext)
apply(rule c_f_list_to_f_0)
done

lemma c_f_list_f_is_pr: "c_f_list f ∈ PrimRec2 ⟹ f ∈ PrimRec2"
proof -
assume A1: "c_f_list f ∈ PrimRec2"
have S1: "f = (λ y x. c_hd (c_f_list f y x))" by (rule c_f_list_to_f)
from A1 c_hd_is_pr have S2: "(λ y x. c_hd (c_f_list f y x)) ∈ PrimRec2" by prec
with S1 show ?thesis by simp
qed

lemma c_f_list_lm_1: "c_nth (c_cons x y) (Suc z) = c_nth y z" by (simp add: c_nth_def c_drop_at_Suc1)

lemma c_f_list_lm_2: " z < Suc n ⟹ c_nth (c_f_list f (Suc n) x) (Suc n - z) = c_nth (c_f_list f n x) (n - z)"
proof -
assume "z < Suc n"
then have "Suc n - z = Suc (n-z)" by arith
then have "c_nth (c_f_list f (Suc n) x) (Suc n - z) = c_nth (c_f_list f (Suc n) x) (Suc (n - z))" by simp
also have "… = c_nth (c_cons (f (Suc n) x) (c_f_list f n x)) (Suc (n - z))" by (simp add: c_f_list_at_Suc)
also have "… = c_nth (c_f_list f n x) (n - z)" by (simp add: c_f_list_lm_1)
finally show ?thesis by simp
qed

lemma c_f_list_nth: "z ≤ y ⟶ c_nth (c_f_list f y x) (y-z) = f z x"
proof (induct y)
show "z ≤ 0 ⟶ c_nth (c_f_list f 0 x) (0 - z) = f z x"
proof
assume "z ≤ 0" then have A1: "z=0" by simp
then have "c_nth (c_f_list f 0 x) (0 - z) = c_nth (c_f_list f 0 x) 0" by simp
also have "… = c_hd (c_f_list f 0 x)" by (simp add: c_nth_at_0)
also have "… = c_hd (c_cons (f 0 x) 0)" by (simp add: c_f_list_at_0)
also have "… = f 0 x" by simp
finally show "c_nth (c_f_list f 0 x) (0 - z) = f z x" by (simp add: A1)
qed
next
fix n assume A2: " z ≤ n ⟶ c_nth (c_f_list f n x) (n - z) = f z x" show "z ≤ Suc n ⟶ c_nth (c_f_list f (Suc n) x) (Suc n - z) = f z x"
proof
assume A3: "z ≤ Suc n"
show " z ≤ Suc n ⟹ c_nth (c_f_list f (Suc n) x) (Suc n - z) = f z x"
proof cases
assume AA1: "z ≤ n"
then have AA2: "z < Suc n" by simp
from A2 this have S1: "c_nth (c_f_list f n x) (n - z) = f z x" by auto
from AA2 have "c_nth (c_f_list f (Suc n) x) (Suc n - z) = c_nth (c_f_list f n x) (n - z)" by (rule c_f_list_lm_2)
with S1 show "c_nth (c_f_list f (Suc n) x) (Suc n - z) = f z x" by simp
next
assume "¬ z ≤ n"
from A3 this have S1: "z = Suc n" by simp
then have S2: "Suc n - z = 0" by simp
then have "c_nth (c_f_list f (Suc n) x) (Suc n - z) = c_nth (c_f_list f (Suc n) x) 0" by simp
also have "… = c_hd (c_f_list f (Suc n) x)" by (simp add: c_nth_at_0)
also have "… = c_hd (c_cons (f (Suc n) x) (c_f_list f n x))" by (simp add: c_f_list_at_Suc)
also have "… = f (Suc n) x" by simp
finally show "c_nth (c_f_list f (Suc n) x) (Suc n - z) = f z x" by (simp add: S1)
qed
qed
qed

theorem th_pr_rec: "⟦ g ∈ PrimRec1; h ∈ PrimRec3; (∀ x. (f 0 x) = (g x)); (∀ x y. (f (Suc y) x) = h y (f y x) x) ⟧ ⟹ f ∈ PrimRec2"
proof -
assume g_is_pr: "g ∈ PrimRec1"
assume h_is_pr: "h ∈ PrimRec3"
assume f_0: "∀ x. f 0 x = g x"
assume f_1: "∀ x y. (f (Suc y) x) = h y (f y x) x"
let ?f = "PrimRecOp g h"
from g_is_pr h_is_pr have S1: "?f ∈ PrimRec2" by (rule pr_rec)
have f_2:"∀ x. ?f 0 x = g x" by simp
have f_3: "∀ x y. (?f (Suc y) x) = h y (?f y x) x" by simp
have S2: "f = ?f"
proof -
have "⋀ x y. f y x = ?f y x"
apply(induct_tac y)
apply(insert f_0 f_1)
apply(auto)
done
then show "f = ?f" by (simp add: ext)
qed
from S1 S2 show ?thesis by simp
qed

theorem th_rec: "⟦ g ∈ PrimRec1; α ∈ PrimRec2; h ∈ PrimRec3; (∀ x y. α y x ≤ y); (∀ x. (f 0 x) = (g x)); (∀ x y. (f (Suc y) x) = h y (f (α y x) x) x) ⟧ ⟹ f ∈ PrimRec2"
proof -
assume g_is_pr: "g ∈ PrimRec1"
assume a_is_pr: "α ∈ PrimRec2"
assume h_is_pr: "h ∈ PrimRec3"
assume a_le: "(∀ x y. α y x ≤ y)"
assume f_0: "∀ x. f 0 x = g x"
assume f_1: "∀ x y. (f (Suc y) x) = h y (f (α y x) x) x"
let ?g' = "λ x. c_cons (g x) 0"
let ?h' = "λ a b c. c_cons (h a (c_nth b (a - (α a c))) c) b"
let ?r = "c_f_list f"
from g_is_pr c_cons_is_pr have g'_is_pr: "?g' ∈ PrimRec1" by prec
from h_is_pr c_cons_is_pr c_nth_is_pr a_is_pr have h'_is_pr: "?h' ∈ PrimRec3" by prec
have S1: "∀ x. ?r 0 x = ?g' x"
proof
fix x have "?r 0 x = c_cons (f 0 x) 0" by (rule c_f_list_at_0)
with f_0 have "?r 0 x = c_cons (g x) 0" by simp
then show "?r 0 x = ?g' x" by simp
qed
have S2: "∀ x y. ?r (Suc y) x = ?h' y (?r y x) x"
proof (rule allI, rule allI)
fix x y show "?r (Suc y) x = ?h' y (?r y x) x"
proof -
have S2_1: "?r (Suc y) x = c_cons (f (Suc y) x) (?r y x)" by (rule c_f_list_at_Suc)
with f_1 have S2_2: "f (Suc y) x = h y (f (α y x) x) x" by simp
from a_le have S2_3: "α y x ≤ y" by simp
then have S2_4: "f (α y x) x = c_nth (?r y x) (y-(α y x))" by (simp add: c_f_list_nth)
from S2_1 S2_2 S2_4 show ?thesis by simp
qed
qed
from g'_is_pr h'_is_pr S1 S2 have S3: "?r ∈ PrimRec2" by (rule th_pr_rec)
then show "f ∈ PrimRec2" by (rule c_f_list_f_is_pr)
qed

declare c_tl_less [termination_simp]

fun c_assoc_have_key :: "nat ⇒ nat ⇒ nat" where
c_assoc_have_key_df [simp del]: "c_assoc_have_key y x = (if y = 0 then 1 else
(if c_fst (c_hd y) = x then 0 else c_assoc_have_key (c_tl y) x))"

lemma c_assoc_have_key_lm_1: "y ≠ 0 ⟹ c_assoc_have_key y x = (if c_fst (c_hd y) = x then 0 else c_assoc_have_key (c_tl y) x)" by (simp add: c_assoc_have_key_df)

theorem c_assoc_have_key_is_pr: "c_assoc_have_key ∈ PrimRec2"
proof -
let ?h = "λ a b c. if c_fst (c_hd (Suc a)) = c then 0 else b"
let ?a = "λ y x. c_tl (Suc y)"
let ?g = "λ x. (1::nat)"
have g_is_pr: "?g ∈ PrimRec1" by (rule const_is_pr)
from c_tl_is_pr have a_is_pr: "?a ∈ PrimRec2" by prec
have h_is_pr: "?h ∈ PrimRec3"
proof (rule if_eq_is_pr3)
from c_fst_is_pr c_hd_is_pr show "(λx y z. c_fst (c_hd (Suc x))) ∈ PrimRec3" by prec
next
show "(λx y z. z) ∈ PrimRec3" by (rule pr_id3_3)
next
show "(λx y z. 0) ∈ PrimRec3" by prec
next
show "(λx y z. y) ∈ PrimRec3" by (rule pr_id3_2)
qed
have a_le: "∀ x y. ?a y x ≤ y"
proof (rule allI, rule allI)
fix x y show "?a y x ≤ y"
proof -
have "Suc y > 0" by simp
then have "?a y x < Suc y" by (rule c_tl_less)
then show ?thesis by simp
qed
qed
have f_0: "∀ x. c_assoc_have_key 0 x = ?g x" by (simp add: c_assoc_have_key_df)
have f_1: "∀ x y. c_assoc_have_key (Suc y) x = ?h y (c_assoc_have_key (?a y x) x) x" by (simp add: c_assoc_have_key_df)
from g_is_pr a_is_pr h_is_pr a_le f_0 f_1 show ?thesis by (rule th_rec)
qed

fun c_assoc_value :: "nat ⇒ nat ⇒ nat" where
c_assoc_value_df [simp del]: "c_assoc_value y x = (if y = 0 then 0 else
(if c_fst (c_hd y) = x then c_snd (c_hd y) else c_assoc_value (c_tl y) x))"

lemma c_assoc_value_lm_1: "y ≠ 0 ⟹ c_assoc_value y x = (if c_fst (c_hd y) = x then c_snd (c_hd y) else c_assoc_value (c_tl y) x)" by (simp add: c_assoc_value_df)

theorem c_assoc_value_is_pr: "c_assoc_value ∈ PrimRec2"
proof -
let ?h = "λ a b c. if c_fst (c_hd (Suc a)) = c then c_snd (c_hd (Suc a)) else b"
let ?a = "λ y x. c_tl (Suc y)"
let ?g = "λ x. (0::nat)"
have g_is_pr: "?g ∈ PrimRec1" by (rule const_is_pr)
from c_tl_is_pr have a_is_pr: "?a ∈ PrimRec2" by prec
have h_is_pr: "?h ∈ PrimRec3"
proof (rule if_eq_is_pr3)
from c_fst_is_pr c_hd_is_pr show "(λx y z. c_fst (c_hd (Suc x))) ∈ PrimRec3" by prec
next
show "(λx y z. z) ∈ PrimRec3" by (rule pr_id3_3)
next
from c_snd_is_pr c_hd_is_pr show "(λx y z. c_snd (c_hd (Suc x))) ∈ PrimRec3" by prec
next
show "(λx y z. y) ∈ PrimRec3" by (rule pr_id3_2)
qed
have a_le: "∀ x y. ?a y x ≤ y"
proof (rule allI, rule allI)
fix x y show "?a y x ≤ y"
proof -
have "Suc y > 0" by simp
then have "?a y x < Suc y" by (rule c_tl_less)
then show ?thesis by simp
qed
qed
have f_0: "∀ x. c_assoc_value 0 x = ?g x" by (simp add: c_assoc_value_df)
have f_1: "∀ x y. c_assoc_value (Suc y) x = ?h y (c_assoc_value (?a y x) x) x" by (simp add: c_assoc_value_df)
from g_is_pr a_is_pr h_is_pr a_le f_0 f_1 show ?thesis by (rule th_rec)
qed

lemma c_assoc_lm_1: "c_assoc_have_key (c_cons (c_pair x y) z) x = 0"
done

lemma c_assoc_lm_2: "c_assoc_value (c_cons (c_pair x y) z) x = y"
apply(rule impI)
apply(insert c_cons_pos [where x="(c_pair x y)" and u="z"])
apply(auto)
done

lemma c_assoc_lm_3: "x1 ≠ x ⟹ c_assoc_have_key (c_cons (c_pair x y) z) x1 = c_assoc_have_key z x1"
proof -
assume A1: "x1 ≠ x"
let ?ls = "(c_cons (c_pair x y) z)"
have S1: "?ls ≠ 0" by (simp add: c_cons_pos)
then have S2: "c_assoc_have_key ?ls x1 = (if c_fst (c_hd ?ls) = x1 then 0 else c_assoc_have_key (c_tl ?ls) x1)" (is "_ = ?R")  by (rule c_assoc_have_key_lm_1)
have S3: "c_fst (c_hd ?ls) = x" by simp
with A1 have S4: "¬ (c_fst (c_hd ?ls) = x1)" by simp
from S4 have S5: "?R = c_assoc_have_key (c_tl ?ls) x1" by (rule if_not_P)
from S2 S5 show ?thesis by simp
qed

lemma c_assoc_lm_4: "x1 ≠ x ⟹ c_assoc_value (c_cons (c_pair x y) z) x1 = c_assoc_value z x1"
proof -
assume A1: "x1 ≠ x"
let ?ls = "(c_cons (c_pair x y) z)"
have S1: "?ls ≠ 0" by (simp add: c_cons_pos)
then have S2: "c_assoc_value ?ls x1 = (if c_fst (c_hd ?ls) = x1 then c_snd (c_hd ?ls) else c_assoc_value (c_tl ?ls) x1)" (is "_ = ?R")  by (rule c_assoc_value_lm_1)
have S3: "c_fst (c_hd ?ls) = x" by simp
with A1 have S4: "¬ (c_fst (c_hd ?ls) = x1)" by simp
from S4 have S5: "?R = c_assoc_value (c_tl ?ls) x1" by (rule if_not_P)
from S2 S5 show ?thesis by simp
qed

end


# Theory 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