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