# HG changeset patch # User Christian Urban # Date 1368455328 -3600 # Node ID 0546ae45274731e734a783ecb5ad17ca99fcd8e0 # Parent 0846c45cedbba3d934dca17a6bf8938c430917b8 added diff -r 0846c45cedbb -r 0546ae452747 thys/NatBijection.thy --- a/thys/NatBijection.thy Mon May 13 14:08:54 2013 +0100 +++ b/thys/NatBijection.thy Mon May 13 15:28:48 2013 +0100 @@ -6,18 +6,44 @@ 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)" + 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]: +lemma oddfactor [simp]: "oddfactor 0 = 0" - "odd n \ oddfactor n = n" + "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)" diff -r 0846c45cedbb -r 0546ae452747 thys/Recs.thy --- a/thys/Recs.thy Mon May 13 14:08:54 2013 +0100 +++ b/thys/Recs.thy Mon May 13 15:28:48 2013 +0100 @@ -1,9 +1,12 @@ theory Recs -imports Main +imports Main Fact "~~/src/HOL/Number_Theory/Primes" - Fact + "~~/src/HOL/Library/Nat_Bijection" + "~~/src/HOL/Library/Discrete" begin +declare One_nat_def[simp del] + (* some definitions from @@ -574,6 +577,10 @@ apply(simp add: le_Suc_eq) by metis +lemma BMax_rec_eq3: + "BMax_rec R x = Max (Set.filter (\z. R z) {..x} \ {0})" +by (simp add: BMax_rec_eq2 Set.filter_def) + definition "rec_max1 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])" @@ -590,289 +597,90 @@ section {* Encodings *} -fun log :: "nat \ nat" where - [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))" - -lemma log_zero [simp]: - "log 0 = 0" - by (simp add: log.simps) +fun prod_decode1 where + "prod_decode1 z = z - (triangle (BMax_rec (\k. triangle k \ z) z))" -lemma log_one [simp]: - "log 1 = 0" - by (simp add: log.simps) +fun prod_decode2 where + "prod_decode2 z = BMax_rec (\k. triangle k \ z) z - prod_decode1 z" -lemma log_suc [simp]: - "log (Suc 0) = 0" - by (simp add: log.simps) +section {* Encodings *} -lemma log_rec: - "n \ 2 \ log n = Suc (log (n div 2))" - by (simp add: log.simps) - -lemma log_twice [simp]: - "n \ 0 \ log (2 * n) = Suc (log n)" - by (simp add: log_rec) +lemma triangle_sum: + "triangle k = (\i \ k. i)" +by (induct k) (simp_all) -lemma log_half [simp]: - "log (n div 2) = log n - 1" -proof (cases "n < 2") - case True - then have "n = 0 \ n = 1" by arith - then show ?thesis by (auto simp del: One_nat_def) -next - case False then show ?thesis by (simp add: log_rec) +fun sqrt where + "sqrt z = BMax_rec (\x. x * x \ z) z" + +lemma sqrt_bounded_Max: + "Discrete.sqrt n = Max (Set.filter (\m. m\ \ n) {0..n})" +proof - + from power2_nat_le_imp_le [of _ n] have "{m. m \ n \ m\ \ n} = {m. m\ \ n}" by auto + then show ?thesis by (simp add: Discrete.sqrt_def Set.filter_def) qed -lemma log_exp [simp]: - "log (2 ^ n) = n" - by (induct n) simp_all - -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)" - -lemma oddfactor[simp]: - "oddfactor 0 = 0" - "odd n \ oddfactor n = n" - "even n \ oddfactor n = oddfactor (n div 2)" -apply(simp_all add: oddfactor.simps) -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") +lemma sqrt: "Discrete.sqrt z = sqrt z" +apply(simp add: BMax_rec_eq3 sqrt_bounded_Max Set.filter_def power2_eq_square) +apply(rule_tac f="Max" in arg_cong) 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 i where + "i z = (Discrete.sqrt (1 + 8 * z) - 1) div 2" -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 = log ((Suc z) div (oddfactor (Suc z)))" - -lemma k: - "odd n \ oddfactor (2 ^ m * n) = n" -apply(induct m) -apply(simp_all) +lemma "map prod_decode [0,1,2,3,4,5,6,7,8,9,10,11,12] = + [(0, 0), (0, 1), (1, 0), (0, 2), (1, 1), (2, 0), (0, 3), + (1, 2), (2, 1), (3, 0), (0, 4), (1, 3), (2, 2)]" +apply(simp add: prod_decode_def prod_decode_aux.simps) 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) +lemma "map triangle [0, 1, 2, 3, 4, 5, 6 ] = [0, 1, 3, 6, 10, 15, 21]" +by(simp add: numeral_eq_Suc One_nat_def) + +lemma "map (\z. (z - (i(z) * (1 + i(z))) div 2, (i(z) * (3 + i(z))) div 2 - z)) + [0,1,2,3,4,5,6,7,8,9,10,11,12] = + [(0, 0), (0, 1), (1, 0), (0, 2), (1, 1), (2, 0), (0, 3), + (1, 2), (2, 1), (3, 0), (0, 4), (1, 3), (2, 2)]" +apply(simp add: sqrt) +by eval + +fun + prod_decode_max :: "nat \ nat \ nat" +where + "prod_decode_max k m = + (if m \ k then k else prod_decode_max (Suc k) (m - Suc k))" + +lemma t: "triangle (prod_decode_max k m) \ triangle k + m" +apply (induct k m rule: prod_decode_max.induct) +apply (subst prod_decode_max.simps) +apply (simp) +done + +lemma "prod_decode_max 0 z = (GREAT k. triangle k \ z)" +apply(rule sym) +apply(rule Great_equality) +using t +apply -[1] +apply (smt triangle_0) +apply(induct z arbitrary: y rule: nat_less_induct) +apply (subst prod_decode_max.simps) +apply (auto simp del: prod_decode_max.simps) +apply(case_tac y) 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) + +apply (subst prod_decode_max.simps) +apply (auto simp del: prod_decode_max.simps) -lemma t: - "(Suc (Suc m)) div 2 = Suc (m div 2)" -by (induct m) (auto) - -lemma u: - "((Suc (Suc m)) mod 2 = 0) <-> m mod 2 = 0" -by (auto) - -lemma u2: - "0 < n ==> 2 * 2 ^ (n - 1) = (2::nat) ^ (n::nat)" -by (induct n) (simp_all) - -lemma test: "x = y \ 2 * x = 2 * y" -by simp +apply(blast) -lemma m: "0 < n ==> 2 ^ 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 (log (n div oddfactor n) - 1) = log (n div oddfactor n)") -prefer 2 -apply (smt Recs.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:) -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 ^ 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) -apply(subst k) -apply(auto) -done - -lemma y2: - "pdecode1 (pencode m n) = m" -using [[simp_trace]] -apply(simp) -apply(subst k) -apply(auto)[1] -using [[simp_trace_depth_limit=10]] -apply(simp) -done - -lemma yy: - "pencode (pdecode1 m) (pdecode2 m) = m" -apply(induct m rule: nat_less_induct) -apply(simp (no_asm)) -apply(case_tac "n = 0") +lemma "prod_decode z = (z - (i(z) * (1 + i(z))) div 2, (i(z) * (3 + i(z))) div 2 - z)" +apply(simp add: prod_decode_def) +apply(case_tac z) +apply(simp add: prod_decode_aux.simps) 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 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) -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 section {* Discrete Logarithms *}