diff -r 6e7244ae43b8 -r 745547bdc1c7 thys/Recs.thy --- a/thys/Recs.thy Thu May 02 13:19:50 2013 +0100 +++ b/thys/Recs.thy Thu May 09 18:16:36 2013 +0100 @@ -1,5 +1,7 @@ theory Recs -imports Main Fact "~~/src/HOL/Number_Theory/Primes" +imports Main + "~~/src/HOL/Number_Theory/Primes" + Fact begin (* @@ -104,7 +106,8 @@ fixes f::"nat \<Rightarrow> nat" assumes "\<forall>i \<le> n. f i \<le> 1" shows "(\<Prod>i \<le> n. f i) \<le> 1" -using assms by (induct n) (auto intro: nat_mult_le_one) +using assms +by (induct n) (auto intro: nat_mult_le_one) lemma setprod_greater_zero: fixes f::"nat \<Rightarrow> nat" @@ -537,14 +540,14 @@ "rec_eval rec_prime [x] = (if prime x then 1 else 0)" by (auto simp add: rec_prime_def Let_def prime_alt_def) -section {* Bounded Min and Maximisation *} +section {* Bounded Maximisation *} fun BMax_rec where "BMax_rec R 0 = 0" | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)" definition BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat" - where "BMax_set R x = Max ({z | z. z \<le> x \<and> R z} \<union> {0})" + where "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})" definition (in ord) Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where @@ -555,8 +558,7 @@ assumes "P x" "\<And>y. P y \<Longrightarrow> y \<le> x" shows "Great P = x" unfolding Great_def -using assms -by(rule_tac the_equality) (auto intro: le_antisym) +using assms by(rule_tac the_equality) (auto intro: le_antisym) lemma BMax_rec_eq1: "BMax_rec R x = (GREAT z. (R z \<and> z \<le> x) \<or> z = 0)" @@ -566,28 +568,310 @@ by metis lemma BMax_rec_eq2: - "BMax_rec R x = Max ({z | z. z \<le> x \<and> R z} \<union> {0})" + "BMax_rec R x = Max ({z. z \<le> x \<and> R z} \<union> {0})" apply(induct x) apply(auto intro: Max_eqI Max_eqI[symmetric]) apply(simp add: le_Suc_eq) by metis 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])" + "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])" lemma max1_lemma [simp]: "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x" by (induct x) (simp_all add: rec_max1_def) definition - "rec_max2 f = PR (constn 0) - (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])" + "rec_max2 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])" lemma max2_lemma [simp]: "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x" by (induct x) (simp_all add: rec_max2_def) +section {* Encodings *} + +fun log :: "nat \<Rightarrow> 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) + +lemma log_one [simp]: + "log 1 = 0" + by (simp add: log.simps) + +lemma log_suc [simp]: + "log (Suc 0) = 0" + by (simp add: log.simps) + +lemma log_rec: + "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))" + by (simp add: log.simps) + +lemma log_twice [simp]: + "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)" + by (simp add: log_rec) + +lemma log_half [simp]: + "log (n div 2) = log n - 1" +proof (cases "n < 2") + case True + then have "n = 0 \<or> 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) +qed + +lemma log_exp [simp]: + "log (2 ^ n) = n" + by (induct n) simp_all + +fun divby2 :: "nat \<Rightarrow> nat" where + [simp del]: "divby2 n = (if n = 0 then 0 + else if even n then divby2 (n div 2) else n)" + +lemma divby2[simp]: + "divby2 0 = 0" + "odd n \<Longrightarrow> divby2 n = n" + "even n \<Longrightarrow> divby2 n = divby2 (n div 2)" +apply(simp_all add: divby2.simps) +done + +lemma divby2_odd: + "divby2 n = 0 \<or> odd (divby2 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: "divby2 (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 = (divby2 (Suc z) - 1) div 2" + +fun pdecode1 :: "nat \<Rightarrow> nat" where + "pdecode1 z = log ((Suc z) div (divby2 (Suc z)))" + +lemma k: + "odd n \<Longrightarrow> divby2 (2 ^ m * n) = n" +apply(induct m) +apply(simp_all) +done + +lemma ww: "\<exists>k. n = 2 ^ k * divby2 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 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 \<Longrightarrow> 2 * x = 2 * y" +by simp + +lemma m: "0 < n ==> 2 ^ log (n div (divby2 n)) = n div (divby2 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) divby2(3)[symmetric]) +apply(simp) +apply(subst (asm) divby2(3)[symmetric]) +apply(simp) +apply(subgoal_tac "n div 2 div divby2 n = n div (divby2 n) div 2") +prefer 2 +apply (metis div_mult2_eq nat_mult_commute) +apply(simp only: log_half) +apply(case_tac "n div divby2 n = 0") +apply(simp) +apply(simp del: divby2) +apply(drule test) +apply(subst (asm) power.simps(2)[symmetric]) +apply(subgoal_tac "Suc (log (n div divby2 n) - 1) = log (n div divby2 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 divby2_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 divby2 n * divby2 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 divby2(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww) + + +lemma m2: "0 < n ==> 2 ^ log (n div (divby2 n)) * (divby2 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" +apply(simp) +apply(subst k) +apply(auto)[1] +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") +apply(simp) +apply(subst dvd_mult_div_cancel) +using divby2_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 \<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 section {* Discrete Logarithms *} @@ -625,7 +909,7 @@ @{text "NextPrime x"} returns the first prime number after @{text "x"}; @{text "Pi i"} returns the i-th prime number. *} -fun NextPrime ::"nat \<Rightarrow> nat" +definition NextPrime ::"nat \<Rightarrow> nat" where "NextPrime x = (LEAST y. y \<le> Suc (fact x) \<and> x < y \<and> prime y)" @@ -639,14 +923,33 @@ lemma nextprime_lemma [simp]: "rec_eval rec_nextprime [x] = NextPrime x" -by (simp add: rec_nextprime_def Let_def) +by (simp add: rec_nextprime_def Let_def NextPrime_def) +lemma NextPrime_simps [simp]: + shows "NextPrime 2 = 3" + and "NextPrime 3 = 5" +apply(simp_all add: NextPrime_def) +apply(rule Least_equality) +apply(auto) +apply(eval) +apply(rule Least_equality) +apply(auto) +apply(eval) +apply(case_tac "y = 4") +apply(auto) +done fun Pi :: "nat \<Rightarrow> nat" where "Pi 0 = 2" | "Pi (Suc x) = NextPrime (Pi x)" +lemma Pi_simps [simp]: + shows "Pi 1 = 3" + and "Pi 2 = 5" +using NextPrime_simps +by(simp_all add: numeral_eq_Suc One_nat_def) + definition "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])"