# 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 Isabelle documentation for more information. › 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 handle BadArgument => no_tac) 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" by (simp add: minus_mod_eq_mult_div [symmetric]) 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. ***************) exception BadArgument 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 handle BadArgument => no_tac) 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(simp add: c_fold_2) 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 add: c_fold_1) 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(simp add: c_fold_1) 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) apply(simp add: c_drop_at_Suc) done lemma c_drop_at_Suc1: "c_drop (Suc y) x = c_drop y (c_tl x)" apply(simp add: c_drop_at_Suc c_tl_c_drop) 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) apply(simp add: c_f_list_at_0) apply(simp add: c_f_list_at_Suc) 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" apply(simp add: c_assoc_have_key_df) apply(simp add: c_cons_pos) done lemma c_assoc_lm_2: "c_assoc_value (c_cons (c_pair x y) z) x = y" apply(simp add: c_assoc_value_df) 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