diff -r 6e1c03614d36 -r 93db7414931d thys/NatBijection.thy --- 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 \ 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 \ 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 \ oddfactor n = (n - 1) div 2" - "even n \ oddfactor n = oddfactor (n div 2)" -by (simp_all add: oddfactor.simps) - -lemma evenfactor [simp]: - "evenfactor 0 = 0" - "odd n \ evenfactor n = 1" - "even n \ evenfactor n = 2 * evenfactor (n div 2)" -apply(simp_all add: evenfactor.simps) -apply(case_tac n) -apply(simp_all) -done - -fun penc :: "(nat \ nat) \ nat" where - "penc (m, n) = (2 ^ m) * (2 * n + 1) - 1" - -fun pdec :: "nat \ nat \ 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 \ 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 \ nat \ nat" where - "pencode m n = (2 ^ m) * (2 * n + 1) - 1" - -fun pdecode2 :: "nat \ nat" where - "pdecode2 z = (oddfactor (Suc z) - 1) div 2" - -fun pdecode1 :: "nat \ nat" where - "pdecode1 z = Discrete.log ((Suc z) div (oddfactor (Suc z)))" - -lemma k: - "odd n \ oddfactor (2 ^ m * n) = n" -apply(induct m) -apply(simp_all) -done - -lemma ww: "\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 \ 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 \ penc (a, 0)" -apply(induct a) -apply(simp) -apply(simp) -by (smt nat_one_le_power) - -lemma "penc(a, 0) \ 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 \ penc (a, b)" -apply(simp) -proof - - have f1: "(1\nat) + 1 = 2" - by (metis mult_2 nat_mult_1_right) - have f2: "\x\<^isub>1 x\<^isub>2. (x\<^isub>1\nat) \ x\<^isub>1 * x\<^isub>2 \ \ 1 \ x\<^isub>2" - by (metis mult_le_mono2 nat_mult_1_right) - have "1 + (b + b) \ 1 + b \ b \ (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 \ 1 + b \ b \ (1 + (b + b)) * (1 + 1) ^ a - 1" - using f2 by (metis le_add1 le_trans one_le_power) - hence "b \ 2 ^ a * (b + b + 1) - 1" - using f1 by (metis le_diff_conv nat_add_commute nat_le_linear nat_mult_commute) - thus "b \ 2 ^ a * (2 * b + 1) - 1" - by (metis mult_2) -qed - - -end \ No newline at end of file