--- a/thys/NatBijection.thy Fri Dec 21 12:31:36 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,274 +0,0 @@
-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
\ No newline at end of file