--- 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])"