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