Theory Recursion-Theory-I.CPair

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

section ‹Cantor pairing function›

theory CPair
imports Main
begin

text ‹
  We introduce a particular coding ‹c_pair› from ordered pairs
  of natural numbers to natural numbers.  See \<^cite>‹"Rogers"› and the
  Isabelle documentation for more information.
›

subsection ‹Pairing function›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

text ‹Auxiliary lemmas›

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

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

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

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

text ‹Basic properties of c\_pair function›

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Inverse mapping›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end