1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Tue Feb 12 09:58:59 2013 +0100
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Fri Feb 15 14:49:50 2013 +0100
1.3 @@ -136,58 +136,53 @@
1.4 value "primes_upto 10 = [2, 3, 5, 7, 11]"
1.5 value "primes_upto 11 = [2, 3, 5, 7, 11]"
1.6
1.7 -text {* FIXME next_prime_not_dvd loops with all the following:
1.8 -
1.9 -(* find a prime greater p not dividing the number n *)
1.10 +text {* FIXME Mail_3_Next_Prime.thy: next_prime_not_dvd loops with all the following:
1.11
1.12 function next_prime_not_dvd :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "next'_prime'_not'_dvd" 70) where
1.13 - "p next_prime_not_dvd n =
1.14 + "n1 next_prime_not_dvd n2 =
1.15 (let
1.16 - ps = primes_upto (p + 1);
1.17 + ps = primes_upto (n1 + 1);
1.18 nxt = List.nth ps (List.length ps - 1)
1.19 in
1.20 - if n mod nxt \<noteq> 0
1.21 + if n2 mod nxt \<noteq> 0
1.22 then nxt
1.23 - else 77)"
1.24 + else 77)" (*<<========================================== does not help*)
1.25 by pat_completeness (simp del: primes_upto.simps is_prime.simps)
1.26 termination sorry
1.27
1.28 +(* find a prime greater p not dividing the number n:
1.29 + next_prime_not_dvd :: int \<Rightarrow> int \<Rightarrow> int (infix)
1.30 + n1 next_prime_not_dvd n2 = p
1.31 + assumes True
1.32 + yields SOME p. p is_prime \<and> n1 < p \<and> \<not> p dvd n2 \<and>
1.33 + \<forall> pp. pp is_prime \<and> n1 < pp \<and> \<not> pp dvd n2 \<Rightarrow> p \<le> pp *)
1.34 function next_prime_not_dvd :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "next'_prime'_not'_dvd" 70) where
1.35 - "p next_prime_not_dvd n =
1.36 - (let
1.37 - ps = primes_upto (p + 1);
1.38 - nxt = List.nth ps (List.length ps - 1)
1.39 - in
1.40 - if n mod nxt \<noteq> 0
1.41 - then nxt
1.42 - else nxt next_prime_not_dvd n)"
1.43 -by pat_completeness (simp del: is_prime.simps make_primes.simps)
1.44 + "n1 next_prime_not_dvd n2 =
1.45 + (let
1.46 + ps = primes_upto (n1 + 1);
1.47 + nxt = List.nth ps (List.length ps - 1)
1.48 + in
1.49 + if n2 mod nxt \<noteq> 0
1.50 + then nxt
1.51 + else nxt next_prime_not_dvd n2)"
1.52 +by pat_completeness (simp del: primes_upto.simps)
1.53 termination sorry
1.54
1.55 ----
1.56 loops : by pat_completeness auto
1.57 loops : by pat_completeness simp
1.58 +loops : by pat_completeness (simp del: is_prime.simps)
1.59 Failed to finish proof : by pat_completeness (simp del: is_prime.simps make_primes.simps)
1.60 + see Mail_13_2loo-2by-del-is_prime-make_primes.trace: del: is_prime.simps IS SUPERFLUOUS !
1.61 Failed to finish proof : by pat_completeness (simp del: make_primes.simps)
1.62 +Failed to finish proof : by pat_completeness (simp del: primes_upto.simps)
1.63 +
1.64 +----
1.65 +declare [[simp_trace_depth_limit=9]]
1.66 +declare [[simp_trace=true]]
1.67 *}
1.68 -declare [[simp_trace_depth_limit=99]]
1.69 -declare [[simp_trace=true]]
1.70 -ML {*11111*}
1.71 -thm make_primes.simps
1.72 +(*---------------------------------------------------------------------------------------------*)
1.73
1.74 -function next_prime_not_dvd :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "next'_prime'_not'_dvd" 70) where
1.75 - "p next_prime_not_dvd n =
1.76 - (let
1.77 - ps = primes_upto (p + 1);
1.78 - nxt = List.nth ps (List.length ps - 1)
1.79 - in
1.80 - if n mod nxt \<noteq> 0
1.81 - then nxt
1.82 - else nxt next_prime_not_dvd n)"
1.83 -by pat_completeness (simp del: make_primes.simps)
1.84 -
1.85 -
1.86 -(*---------------------------------------------------------------------------------------------
1.87 subsection {* auxiliary functions for univariate polynomials *}
1.88
1.89 (* not in List.thy, copy from library.ML *)
1.90 @@ -207,7 +202,6 @@
1.91 by auto
1.92 termination sorry
1.93
1.94 -text {*"----------- fun lc -------------------------------------"*}
1.95 value "lc [3, 4, 5, 6] = 6"
1.96 value "lc [3, 4, 5, 6, 0] = 6"
1.97
1.98 @@ -221,7 +215,6 @@
1.99 termination sorry
1.100 (* TODO: ?let l = length uvp - 1? more efficient??? compare drop_lc0 !!! *)
1.101
1.102 -text {*"----------- fun deg ------------------------------------"*}
1.103 value "deg [3, 4, 5, 6] = 3"
1.104 value "deg [3, 4, 5, 6, 0] = 3"
1.105
1.106 @@ -235,7 +228,6 @@
1.107 then drop_lc0 (nth_drop l uvp)
1.108 else uvp)"
1.109
1.110 -text {*"----------- fun drop_lc0 -------------------------------";*}
1.111 value "drop_lc0 [0, 1, 2, 3, 4, 5, 0, 0] = [0, 1, 2, 3, 4, 5]"
1.112 value "drop_lc0 [0, 1, 2, 3, 4, 5] = [0, 1, 2, 3, 4, 5]"
1.113
1.114 @@ -258,7 +250,6 @@
1.115 in
1.116 if List.length p = 0 then p else norm p [] m lcp (List.length p - 1))"
1.117
1.118 -text {*"----------- fun normalise ------------------------------";*}
1.119 value "normalise [-18, -15, -20, 12, 20, -13, 2] 5 = [1, 0, 0, 1, 0, 1, 1]"
1.120 value "normalise [9, 6, 3] 10 = [3, 2, 1]"
1.121
1.122 @@ -314,6 +305,9 @@
1.123
1.124 thm dvd_up.simps
1.125 thm dvd_up.induct
1.126 +
1.127 +
1.128 +(*---------------------------------------------------------------------------------------------*)
1.129 (*
1.130 value "[2, 3] dvd_up [8, 22, 15] = True"
1.131 ... FIXME loops, incorrect: ALL SHOULD EVALUATE TO TRUE .......
1.132 @@ -326,7 +320,11 @@
1.133 (* centr is just local to poly_centr *)
1.134 definition centr :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
1.135 "centr m mid p_i = (if mid < p_i then p_i - m else p_i)"
1.136 -(* TODO *)
1.137 + (* normalise :: poly_centr \<Rightarrow> unipoly => int \<Rightarrow> unipoly
1.138 + normalise [p_0, .., p_k] m = [q_0, .., q_k]
1.139 + assumes
1.140 + yields. 0 \<le> i \<le> k \<Rightarrow> |^ ~m/2 ^| <= q_i <=|^ m/2 ^|
1.141 + where |^ x ^| means round x up to the next integer *)
1.142 definition poly_centr :: "unipoly \<Rightarrow> int \<Rightarrow> unipoly" where
1.143 "poly_centr p m =
1.144 (let
1.145 @@ -346,7 +344,10 @@
1.146 value "poly_centr [1, 2, 3, 4, 5] 10 = [1, 2, 3, 4, 5]"
1.147 value "poly_centr [1, 2, 3, 4, 5] 11 = [1, 2, 3, 4, 5]"
1.148
1.149 -(* TODO *)
1.150 +(* sum_lmb :: poly_centr \<Rightarrow> unipoly => int \<Rightarrow> int
1.151 + sum_lmb [p_0, .., p_k] e = s
1.152 + assumes exp >= 0
1.153 + yields. SOME s = p_0^e + p_1^e + ... + p_k^e *)
1.154 definition sum_lmb :: "unipoly \<Rightarrow> nat \<Rightarrow> int" where
1.155 "sum_lmb p exp = fold ((op +) o (swapf power exp)) p 0"
1.156
1.157 @@ -357,7 +358,11 @@
1.158 value "sum_lmb [-1, 2, -3, 4, -5] 5 = -2313"
1.159 value "sum_lmb [-1, 2, -3, 4, -5] 6 = 20515"
1.160
1.161 -(* TODO *)
1.162 +(* landau_mignotte_bound :: poly_centr \<Rightarrow> unipoly => unipoly \<Rightarrow> int
1.163 + landau_mignotte_bound [a_0, ..., a_m] [b_0, .., b_n] = lmb
1.164 + assumes True
1.165 + yields. lmb = 2^min(m,n) * gcd(a_m,b_n) *
1.166 + min( 1/|a_m| * root(sum_lmb [a_0,...a_m] 2 , 1/|b_n| * root(sum_lmb [b_0,...b_n] 2)*)
1.167 definition landau_mignotte_bound :: "unipoly \<Rightarrow> unipoly \<Rightarrow> nat" where
1.168 "landau_mignotte_bound p1 p2 =
1.169 ((power 2 (min (deg p1) (deg p2))) * (nat (gcd (lc p1) (lc p2))) *
1.170 @@ -380,7 +385,17 @@
1.171
1.172 subsection {* modulo calculations for polynomials *}
1.173
1.174 -(* pair is just local to chinese_remainder_poly *)
1.175 +(* pair is just local to chinese_remainder_poly, is "op ~~" in library.ML *)
1.176 +(*
1.177 +locale gcd_poly =
1.178 + fixes gcd_poly :: int poly -> int poly -> int poly
1.179 + assumes gcd_poly a b = c
1.180 + and not (a = [:0:])
1.181 + and not (b = [:0:])
1.182 + ==> c dvd a \<and> c dvd b
1.183 + and \<And> c'. (c' dvd a \<and> c’ dvd b) => c’ \<le> c
1.184 +*)
1.185 +
1.186 fun pair :: "unipoly \<Rightarrow> unipoly \<Rightarrow> ((int * int) list)" (infix "pair" 4) where
1.187 "([] pair []) = []"
1.188 | "([] pair ys) = []" (*raise ListPair.UnequalLengths*)
1.189 @@ -438,15 +453,22 @@
1.190 value "mod_poly_gcd [8, 28, 22, -11, -14, 1, 2] [2, 6, 0, 2, 6] 7 = [2, 6, 0, 2, 6]"
1.191 value "mod_poly_gcd [20, 15, 8, 6] [8, -2, -2, 3] 2 = [0, 1]"
1.192
1.193 -
1.194 -
1.195 -
1.196 (*----------------------------------------------------------------------------*)
1.197 value "xxx" -- "= "
1.198
1.199 print_configs
1.200 declare [[simp_trace_depth_limit=99]]
1.201 declare [[simp_trace=true]]
1.202 ----------------------------------------------------------------------------------------------*)
1.203 +(*---------------------------------------------------------------------------------------------*)
1.204 +
1.205 +(*
1.206 +locale gcd_poly =
1.207 + fixes gcd_poly :: int poly -> int poly -> int poly
1.208 + assumes gcd_poly a b = c
1.209 + and not (a = [:0:])
1.210 + and not (b = [:0:])
1.211 + ==> c dvd a \<and> c dvd b
1.212 + and \<And> c'. (c' dvd a \<and> c’ dvd b) => c’ \<le> c
1.213 +*)
1.214
1.215 end