--- 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 (\<lambda>z. R z) {..x} \<union> {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 \<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)
+fun prod_decode1 where
+ "prod_decode1 z = z - (triangle (BMax_rec (\<lambda>k. triangle k \<le> z) z))"
-lemma log_one [simp]:
- "log 1 = 0"
- by (simp add: log.simps)
+fun prod_decode2 where
+ "prod_decode2 z = BMax_rec (\<lambda>k. triangle k \<le> z) z - prod_decode1 z"
-lemma log_suc [simp]:
- "log (Suc 0) = 0"
- by (simp add: log.simps)
+section {* Encodings *}
-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 triangle_sum:
+ "triangle k = (\<Sum>i \<le> 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 \<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)
+fun sqrt where
+ "sqrt z = BMax_rec (\<lambda>x. x * x \<le> z) z"
+
+lemma sqrt_bounded_Max:
+ "Discrete.sqrt n = Max (Set.filter (\<lambda>m. m\<twosuperior> \<le> n) {0..n})"
+proof -
+ from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<twosuperior> \<le> n} = {m. m\<twosuperior> \<le> 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 \<Rightarrow> 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 \<Longrightarrow> oddfactor n = n"
- "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)"
-apply(simp_all add: oddfactor.simps)
-done
-
-lemma oddfactor_odd:
- "oddfactor n = 0 \<or> 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 \<Rightarrow> nat \<Rightarrow> nat" where
- "pencode m n = (2 ^ m) * ((2 * n) + 1) - 1"
-
-fun pdecode2 :: "nat \<Rightarrow> nat" where
- "pdecode2 z = (oddfactor (Suc z) - 1) div 2"
-
-fun pdecode1 :: "nat \<Rightarrow> nat" where
- "pdecode1 z = log ((Suc z) div (oddfactor (Suc z)))"
-
-lemma k:
- "odd n \<Longrightarrow> 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: "\<exists>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 (\<lambda>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 \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "prod_decode_max k m =
+ (if m \<le> k then k else prod_decode_max (Suc k) (m - Suc k))"
+
+lemma t: "triangle (prod_decode_max k m) \<le> 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 \<le> 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 \<Longrightarrow> 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 \<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 *}