
diff -r ff54a3308fd6 -r 415e3082ccbc thys/NatBijection.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/NatBijection.thy	Fri May 10 09:07:03 2013 +0100
@@ -0,0 +1,248 @@
+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
\ No newline at end of file




