# HG changeset patch # User Christian Urban # Date 1368173223 -3600 # Node ID 415e3082ccbcfb86cc23bf6fc182e7bf1a9af5c5 # Parent ff54a3308fd66a0d78516d322faa422580f80b76 added first version of natbiject 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 \ 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 \ 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" + "even n \ oddfactor n = oddfactor (n div 2)" +by (simp_all add: oddfactor.simps) + + +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