theory NatBijection

imports Main Parity "~~/src/HOL/Library/Discrete"

begin

declare One_nat_def[simp del]

fun oddfactor :: "nat \<Rightarrow> nat" where

  [simp del]: "oddfactor n = (if n = 0 then 0 

                              else if even n then oddfactor (n div 2) else n)"

fun evenfactor :: "nat \<Rightarrow> nat" where

  [simp del]: "evenfactor n = (if n = 0 then 0 

                               else if even n then 2 * evenfactor (n div 2) else 1)"

lemma oddfactor[simp]:

  "oddfactor 0 = 0"

  "odd n \<Longrightarrow> oddfactor n = n"

  "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)"

by (simp_all add: oddfactor.simps)

lemma oddfactor_odd:

  "oddfactor n = 0 \<or> odd (oddfactor n)" 

apply(induct n rule: nat_less_induct)

apply(case_tac "n = 0")

apply(simp)

apply(case_tac "odd n")

apply(auto)

done

lemma bigger: "oddfactor (Suc n) > 0"

apply(induct n rule: nat_less_induct)

apply(case_tac "n = 0")

apply(simp)

apply(case_tac "odd n")

apply(auto)

apply(drule_tac x="n div 2" in spec)

apply(drule mp)

apply(auto)

by (smt numeral_2_eq_2 odd_nat_plus_one_div_two)

fun pencode :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

  "pencode m n = (2 ^ m) * (2 * n + 1) - 1"

fun pdecode2 :: "nat \<Rightarrow> nat" where

  "pdecode2 z = (oddfactor (Suc z) - 1) div 2"

fun pdecode1 :: "nat \<Rightarrow> nat" where

  "pdecode1 z = Discrete.log ((Suc z) div (oddfactor (Suc z)))"

lemma k:

  "odd n \<Longrightarrow> oddfactor (2 ^ m * n) = n"

apply(induct m)

apply(simp_all)

done

lemma ww: "\<exists>k. n = 2 ^ k * oddfactor n"

apply(induct n rule: nat_less_induct)

apply(case_tac "n=0")

apply(simp)

apply(case_tac "odd n")

apply(simp)

apply(rule_tac x="0" in exI)

apply(simp)

apply(simp)

apply(drule_tac x="n div 2" in spec)

apply(erule impE)

apply(simp)

apply(erule exE)

apply(rule_tac x="Suc k" in exI)

apply(simp)

by (metis div_mult_self2_is_id even_mult_two_ex nat_mult_assoc nat_mult_commute zero_neq_numeral)

lemma test: "x = y \<Longrightarrow> 2 * x = 2 * y"

by simp

lemma m: "0 < n ==> 2 ^ Discrete.log (n div (oddfactor n)) = n div (oddfactor n)"

apply(induct n rule: nat_less_induct)

apply(case_tac "n=0")

apply(simp)

apply(case_tac "odd n")

apply(simp)

apply(drule_tac x="n div 2" in spec)

apply(drule mp)

apply(auto)[1]

apply(drule mp)

apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat)

apply(subst (asm) oddfactor(3)[symmetric])

apply(simp)

apply(subst (asm) oddfactor(3)[symmetric])

apply(simp)

apply(subgoal_tac "n div 2 div oddfactor n = n div (oddfactor n) div 2")

prefer 2

apply (metis div_mult2_eq nat_mult_commute)

apply(simp only: log_half)

apply(case_tac "n div oddfactor n = 0")

apply(simp)

apply(simp del: oddfactor)

apply(drule test)

apply(subst (asm) power.simps(2)[symmetric])

apply(subgoal_tac "Suc (Discrete.log (n div oddfactor n) - 1) = Discrete.log (n div oddfactor n)")

prefer 2

apply (smt log.simps Suc_1 div_less div_mult_self1_is_id log_half log_zero numeral_1_eq_Suc_0 numeral_One odd_1_nat odd_nat_plus_one_div_two one_less_numeral_iff power_one_right semiring_norm(76))

apply(simp only: One_nat_def)

apply(subst dvd_mult_div_cancel)

apply (smt Suc_1 div_by_0 div_mult_self2_is_id oddfactor_odd dvd_power even_Suc even_numeral_nat even_product_nat nat_even_iff_2_dvd power_0 ww)

apply(simp (no_asm))

done

lemma m1: "n div oddfactor n * oddfactor n = n"

apply(induct n rule: nat_less_induct)

apply(case_tac "n=0")

apply(simp)

apply(case_tac "odd n")

apply(simp)

apply(simp)

apply(drule_tac x="n div 2" in spec)

apply(drule mp)

apply(auto)[1]

by (metis add_eq_if diff_add_inverse oddfactor(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww)

lemma m2: "0 < n ==> 2 ^ Discrete.log (n div (oddfactor n)) * (oddfactor n) = n"

apply(subst m)

apply(simp)

apply(subst m1)

apply(simp)

done

lemma y1:

  "pdecode2 (pencode m n) = n"

apply(simp del: One_nat_def)

apply(subst k)

apply(auto)

done

lemma y2:

  "pdecode1 (pencode m n) = m"

apply(simp only: pdecode1.simps pencode.simps)

apply(subst Suc_diff_1)

apply(auto)[1]

apply(subst Suc_diff_1)

apply(auto)[1]

apply(subst k)

apply(auto)[1]

by (metis Suc_eq_plus1 Suc_neq_Zero comm_semiring_1_class.normalizing_semiring_rules(7) div_mult_self1_is_id log_exp)

lemma yy: 

  "pencode (pdecode1 m) (pdecode2 m) = m"

apply(induct m rule: nat_less_induct)

apply(simp (no_asm))

apply(case_tac "n = 0")

apply(simp)

apply(subst dvd_mult_div_cancel)

using oddfactor_odd

apply -

apply(drule_tac x="Suc n" in meta_spec)

apply(erule disjE)

apply(auto)[1]

apply (metis One_nat_def even_num_iff nat_even_iff_2_dvd odd_pos)

using bigger

apply -

apply(rotate_tac 3)

apply(drule_tac x="n" in meta_spec)

apply(simp del: pencode.simps pdecode2.simps pdecode1.simps One_nat_def add: One_nat_def[symmetric])

apply(subst m2)

apply(simp)

apply(simp)

done

fun penc where

 "penc (m, n) = pencode m n"

fun pdec where

 "pdec m = (pdecode1 m, pdecode2 m)"

lemma q1: "penc (pdec m) = m"

apply(simp only: penc.simps pdec.simps)

apply(rule yy)

done

lemma q2: "pdec (penc m) = m"

apply(simp only: penc.simps pdec.simps)

apply(case_tac m)

apply(simp only: penc.simps pdec.simps)

apply(subst y1)

apply(subst y2)

apply(simp)

done

lemma inj_penc: "inj_on penc A"

apply(rule inj_on_inverseI)

apply(rule q2)

done

lemma inj_pdec: "inj_on pdec A"

apply(rule inj_on_inverseI)

apply(rule q1)

done

lemma surj_penc: "surj penc"

apply(rule surjI)

apply(rule q1)

done

lemma surj_pdec: "surj pdec"

apply(rule surjI)

apply(rule q2)

done

lemma 

  "bij pdec"

by(simp add: bij_def surj_pdec inj_pdec)

lemma 

  "bij penc"

by(simp add: bij_def surj_penc inj_penc)

lemma "a \<le> penc (a, 0)"

apply(induct a)

apply(simp)

apply(simp)

by (smt nat_one_le_power)

lemma "penc(a, 0) \<le> penc (a, b)"

apply(simp)

by (metis diff_le_mono le_add1 mult_2_right mult_le_mono1 nat_add_commute nat_mult_1 nat_mult_commute)

lemma "b \<le> penc (a, b)"

apply(simp)

proof -

  have f1: "(1\<Colon>nat) + 1 = 2"

    by (metis mult_2 nat_mult_1_right)

  have f2: "\<And>x\<^isub>1 x\<^isub>2. (x\<^isub>1\<Colon>nat) \<le> x\<^isub>1 * x\<^isub>2 \<or> \<not> 1 \<le> x\<^isub>2"

    by (metis mult_le_mono2 nat_mult_1_right)

  have "1 + (b + b) \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1"

    by (metis le_add1 le_trans nat_add_left_cancel_le)

  hence "(1 + (b + b)) * (1 + 1) ^ a \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1"

    using f2 by (metis le_add1 le_trans one_le_power)

  hence "b \<le> 2 ^ a * (b + b + 1) - 1"

    using f1 by (metis le_diff_conv nat_add_commute nat_le_linear nat_mult_commute)

  thus "b \<le> 2 ^ a * (2 * b + 1) - 1"

    by (metis mult_2)

qed

end