(*  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

(*  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