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 - 1) div 2))"

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 - 1) div 2"
  "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)"
by (simp_all add: oddfactor.simps)

lemma evenfactor [simp]:
  "evenfactor 0 = 0"
  "odd n \<Longrightarrow> evenfactor n = 1"
  "even n \<Longrightarrow> evenfactor n = 2 * evenfactor (n div 2)"
apply(simp_all add: evenfactor.simps)
apply(case_tac n)
apply(simp_all)
done

fun penc :: "(nat \<times> nat) \<Rightarrow> nat" where
  "penc (m, n) = (2 ^ m) * (2 * n + 1) - 1"

fun pdec :: "nat \<Rightarrow> nat \<times> nat" where
  "pdec z = (Discrete.log (evenfactor (Suc z)), oddfactor (Suc z))"

lemma q2: "pdec (penc m) = m"
apply(case_tac m)
apply(simp)
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 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