1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly.thy Sun May 19 08:51:27 2013 +0200
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly.thy Tue May 21 10:38:16 2013 +0200
1.3 @@ -135,36 +135,8 @@
1.4 assumes True
1.5 yields r = r1 mod m1 \<and> r = r2 mod m2 *)
1.6 fun chinese_remainder (r1, m1) (r2, m2) =
1.7 -(writeln ("chinese_remainder" ^
1.8 -", r1 = " ^ PolyML.makestring r1 ^
1.9 -", m1 = " ^ PolyML.makestring m1 ^
1.10 -", r2 = " ^ PolyML.makestring r2 ^
1.11 -", m2 = " ^ PolyML.makestring m2 ^
1.12 -
1.13 -", r1 mod m1 = " ^ PolyML.makestring (r1 mod m1) ^
1.14 -", r2 - (r1 mod m1) mod m1 = " ^ PolyML.makestring (r2 - (r1 mod m1)) ^
1.15 -", (mod_inv m1 m2) = " ^ PolyML.makestring (mod_inv m1 m2) ^
1.16 -", ((r2 - (r1 mod m1)) * (mod_inv m1 m2)) = " ^ PolyML.makestring (((r2 - (r1 mod m1)) * (mod_inv m1 m2))) ^
1.17 -", ((...) mod m2) * m1 = " ^ PolyML.makestring (((r2 - (r1 mod m1)) * (mod_inv m1 m2) mod m2) * m1) ^
1.18 -
1.19 -", res = " ^ PolyML.makestring ((r1 mod m1) +
1.20 - ((r2 - (r1 mod m1)) * (mod_inv m1 m2) mod m2) * m1)
1.21 -);
1.22 -(*r1 = 4, m1 = 5, r2 = 3, m2 = 7*)
1.23 - (r1 mod m1) +
1.24 - (((r2 - (r1 mod m1)) * (mod_inv m1 m2)) mod m2) * m1
1.25 -(* r1 mod m1 = 4,
1.26 - r2 - (r1 mod m1)=~1,(mod_inv m1 m2) mod m2 = 3,
1.27 -res = 24 *)
1.28 -);
1.29 -*}
1.30 -
1.31 -ML {*
1.32 - fun chinese_remainder (r1, m1) (r2, m2) =
1.33 (r1 mod m1) +
1.34 (((r2 - (r1 mod m1)) * (mod_inv m1 m2)) mod m2) * m1;
1.35 -
1.36 - chinese_remainder (17, 9) (3, 4)
1.37 *}
1.38
1.39 subsection {* creation of lists of primes for efficiency *}
1.40 @@ -187,7 +159,7 @@
1.41 yields n \<le> maxs pps \<and> (\<forall>p. List.member pps p \<longrightarrow> Primes.prime p) \<and>
1.42 (\<forall>p. (p < maxs pps \<and> Primes.prime p) \<longrightarrow> List.member pps p)*)
1.43 fun make_primes ps last_p n =
1.44 - if n <= (nth ps (List.length ps - 1)) then ps else
1.45 + if n <= last_elem ps then ps else
1.46 if is_prime ps (last_p + 2)
1.47 then make_primes (ps @ [(last_p + 2)]) (last_p + 2) n
1.48 else make_primes ps (last_p + 2) n
1.49 @@ -335,8 +307,8 @@
1.50 infix mod_up
1.51 fun (p : unipoly) mod_up m =
1.52 let
1.53 - fun mod_pol m p = (curry op mod) p m
1.54 - in map (mod_pol m) p : unipoly end
1.55 + fun mod' m p = (curry op mod) p m
1.56 + in map (mod' m) p : unipoly end
1.57
1.58 (* euclidean algoritm in Z_p[x].
1.59 mod_up_gcd :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> unipoly
1.60 @@ -361,8 +333,9 @@
1.61 primitive_up p = pp
1.62 assumes True
1.63 yields \<forall>p1, p2. (List.member pp p1 \<and> List.member pp p2 \<and> p1 \<noteq> p2) \<longrightarrow> gcd p1 p2 = 1 *)
1.64 - fun primitive_up [c: int] = if c = 0 then [0] else [1]
1.65 - | primitive_up (p: unipoly) =
1.66 + fun primitive_up ([c] : unipoly) =
1.67 + if c = 0 then ([0] : unipoly) else ([1] : unipoly)
1.68 + | primitive_up p =
1.69 let
1.70 val d = abs (Integer.gcds p)
1.71 in
2.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Sun May 19 08:51:27 2013 +0200
2.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Tue May 21 10:38:16 2013 +0200
2.3 @@ -53,16 +53,7 @@
2.4 then rinv
2.5 else modi (rold * ((int rinv) + 1)) rold m (rinv + 1))"
2.6 by auto
2.7 -termination (*by lexicographic_order ...unfinished subgoals*)
2.8 - (*proof
2.9 - proof (state): step 1
2.10 - goal (2 subgoals):
2.11 - 1. wf ?R
2.12 - 2. \<And>r rold m rinv.
2.13 - \<not> m \<le> rinv \<Longrightarrow>
2.14 - r mod m \<noteq> 1 \<Longrightarrow> ((rold * (rinv + 1), rold, m, rinv + 1), r, rold, m, rinv) \<in> ?R*)
2.15 - apply auto
2.16 -sorry
2.17 +termination by (relation "measure (\<lambda>(r, rold, m, rinv). m - rinv)") auto
2.18
2.19 (* mod_inv :: int \<Rightarrow> nat \<Rightarrow> nat
2.20 mod_inv r m = s
2.21 @@ -91,17 +82,17 @@
2.22 "mod_div a b m = (nat a) * (mod_inv b m) mod m"
2.23
2.24 (* root1 is just local to approx_root *)
2.25 -function root1 :: "int \<Rightarrow> int \<Rightarrow> int" where
2.26 - "root1 a n = (if n * n < a then root1 a (n + 1) else n)"
2.27 +function root1 :: "int \<Rightarrow> nat \<Rightarrow> nat" where
2.28 + "root1 a n = (if (int (n * n)) < a then root1 a (n + 1) else n)"
2.29 by auto
2.30 -termination sorry (*by lexicographic_order unfinished subgoals*)
2.31 +termination by (relation "measure (\<lambda>(a, n). nat (a - (int (n * n))))") auto
2.32
2.33 (* required just for one approximation:
2.34 approx_root :: nat \<Rightarrow> nat
2.35 approx_root a = r
2.36 assumes True
2.37 yields r * r \<ge> a *)
2.38 -definition approx_root :: "int \<Rightarrow> int" where
2.39 +definition approx_root :: "int \<Rightarrow> nat" where
2.40 "approx_root a = root1 a 1"
2.41
2.42 (* chinese_remainder :: int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int
2.43 @@ -116,27 +107,6 @@
2.44 value "chinese_remainder 17 9 3 4 = 35"
2.45 value "chinese_remainder 7 2 6 11 = 17"
2.46
2.47 -declare[[show_types]]
2.48 -value "nat (17 mod (int 9))" --" = 8"
2.49 -value " (3 - (17 mod (int 9)))" --" = -5::int"
2.50 -value " (3 - (17 mod (int 9)))" --" = -5::int"
2.51 -value " (int (mod_inv 9 4))" --" = 1::int"
2.52 -value " ((3 - (17 mod (int 9))) * (int (mod_inv 9 4)))" --" = -5::int"
2.53 -value "( ((3 - (17 mod (int 9))) * (int (mod_inv 9 4))) mod 4)" --" = 3::int"
2.54 -value "( ((3 - (17 mod (int 9))) * (int (mod_inv 9 4))) mod 4) * 9" --" = 27::int"
2.55 -value "(nat (((3 - (17 mod (int 9))) * (int (mod_inv 9 4))) mod 4)) * 9" --" = 27::nat"
2.56 -(* |-----| |-----------|
2.57 - |--------------| |-----------------|
2.58 - |--------------------|
2.59 - |--------------------------------------------|
2.60 - |----------------------------------------------------|
2.61 - |----------------------------------------------------------|*)
2.62 -
2.63 -value "((nat (17 mod (int 9))) +
2.64 - (nat (((3 - (17 mod (int 9))) * (int (mod_inv 9 4))) mod 4)) * 9)"
2.65 -
2.66 -value "chinese_remainder 17 9 3 4"
2.67 -
2.68 subsection {* creation of lists of primes for efficiency *}
2.69
2.70 (* is_prime :: int list \<Rightarrow> int \<Rightarrow> bool
2.71 @@ -173,16 +143,33 @@
2.72 (\<forall>p. (p < maxs pps \<and> Primes.prime p) \<longrightarrow> List.member pps p)*)
2.73 function make_primes :: "nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list" where
2.74 "make_primes ps last_p n =
2.75 - (if (List.nth ps (List.length ps - 1)) < n
2.76 - then
2.77 + (if n <= last_elem ps then ps else
2.78 if is_prime ps (last_p + 2)
2.79 then make_primes (ps @ [(last_p + 2)]) (last_p + 2) n
2.80 - else make_primes ps (last_p + 2) n
2.81 - else ps)"
2.82 + else make_primes ps (last_p + 2) n)"
2.83 by pat_completeness auto --"simp del: is_prime.simps <-- declare"
2.84 -termination sorry (*by lexicographic_order unfinished subgoals*)
2.85 +(*Calls:
2.86 + a) (ps, last_p, n) ~> (ps @ [last_p + 2], last_p + 2, n)
2.87 + b) (ps, last_p, n) ~> (ps, last_p + 2, n)
2.88 +Measures:
2.89 + 1) \<lambda>p. size (snd (snd p)) --"n"
2.90 + 2) \<lambda>p. size (fst (snd p)) --"last_p"
2.91 + 3) \<lambda>p. size (snd p) --"(last_p, n)"
2.92 + 4) \<lambda>p. list_size size (fst p) --"ps"
2.93 + 5) \<lambda>p. length (fst p) --"ps"
2.94 + 6) size
2.95 +Result matrix:
2.96 + 1 2 3 4 5 6
2.97 +a: <= ? <= ? ? <=
2.98 +b: <= ? <= <= <= <= *)
2.99 +termination make_primes (*not finished*)
2.100 +apply (relation "measures [\<lambda>(ps, last_p, n). n - (length ps),
2.101 + \<lambda>(ps, last_p, n). n + 2 - last_p]")
2.102 +apply auto
2.103 +sorry (*by lexicographic_order unfinished subgoals*)
2.104 declare make_primes.simps [simp del] -- "next_prime_not_dvd"
2.105
2.106 +value "make_primes [2, 3] 3 3 = [2, 3]"
2.107 value "make_primes [2, 3] 3 4 = [2, 3, 5]"
2.108 value "make_primes [2, 3] 3 5 = [2, 3, 5]"
2.109 value "make_primes [2, 3] 3 6 = [2, 3, 5, 7]"
2.110 @@ -236,13 +223,32 @@
2.111 "n1 next_prime_not_dvd n2 =
2.112 (let
2.113 ps = primes_upto (n1 + 1);
2.114 - nxt = List.nth ps (List.length ps - 1) (* take_last *)
2.115 + nxt = last ps
2.116 in
2.117 if n2 mod nxt \<noteq> 0
2.118 then nxt
2.119 else nxt next_prime_not_dvd n2)"
2.120 by auto --"simp del: is_prime.simps, make_primes.simps, primes_upto.simps <-- declare"
2.121 -termination sorry (*by lexicographic_order unfinished subgoals*)
2.122 +termination (*next_prime_not_dvd ..Inner syntax error*) (*not finished*)
2.123 + apply (relation "measure (\<lambda>(n1, n2). n2 - n1)")
2.124 + apply auto
2.125 +sorry (*by lexicographic_order unfinished subgoals*)
2.126 +(*Calls:
2.127 + a) (n1, n2) ~> (xa, n2)
2.128 +Measures:
2.129 + 1) \<lambda>p. size (snd p)
2.130 + 2) \<lambda>p. size (fst p)
2.131 + 3) size
2.132 +Result matrix:
2.133 + 1 2 3
2.134 +a: <= ? <= *)
2.135 +value "1 next_prime_not_dvd 15 = 2"
2.136 +value "2 next_prime_not_dvd 15 = 7"
2.137 +value "3 next_prime_not_dvd 15 = 7"
2.138 +value "4 next_prime_not_dvd 15 = 7"
2.139 +value "5 next_prime_not_dvd 15 = 7"
2.140 +value "6 next_prime_not_dvd 15 = 7"
2.141 +value "7 next_prime_not_dvd 15 =11"
2.142
2.143 subsection {* basic notions for univariate polynomials *}
2.144
2.145 @@ -274,7 +280,7 @@
2.146 | "drop_lc0_up p =
2.147 (let l = List.length p - 1
2.148 in
2.149 - if nth p l = 0
2.150 + if p ! l = 0
2.151 then drop_lc0_up (nth_drop l p)
2.152 else p)"
2.153
2.154 @@ -287,7 +293,7 @@
2.155 (**)function deg_up :: "unipoly \<Rightarrow> nat" where
2.156 "deg_up p = ((op - 1) o length o drop_lc0_up) p"
2.157 by auto
2.158 -termination sorry
2.159 +termination sorry (* outcommented *)
2.160
2.161 (**)fun deg_up :: "unipoly \<Rightarrow> nat" where
2.162 "deg_up p = ((op - 1) o length o drop_lc0_up) p"
2.163 @@ -299,10 +305,32 @@
2.164 "deg_up p =
2.165 (let len = List.length p - 1
2.166 in
2.167 - if nth p len \<noteq> 0 then len else deg_up (nth_drop len p))"
2.168 -by auto
2.169 -termination sorry (*by lexicographic_order unfinished subgoals*)
2.170 + if p ! len \<noteq> 0 then len else deg_up (nth_drop len p))"
2.171 +by (*pat_completeness*) auto
2.172
2.173 +lemma termin_1:
2.174 + fixes p::"nat list"
2.175 + assumes "length p - Suc 0 = 0"
2.176 + shows "min (length p) (length p - Suc 0) < length p"
2.177 +proof -
2.178 + from `length p - Suc 0 = 0` have "length p = Suc 0" sorry
2.179 + from `length p = Suc 0` have "min (length p) (length p - Suc 0) = 0" by auto
2.180 + from `length p = Suc 0` `min (length p) (length p - Suc 0) = 0` show ?thesis by auto
2.181 +qed
2.182 +thm termin_1 (*length ?p - Suc 0 = 0 \<Longrightarrow> min (length ?p) (length ?p - Suc 0) < length ?p*)
2.183 +termination deg_up (*not finished*)
2.184 + apply (relation "measure (\<lambda>(p). length p)")
2.185 + apply auto
2.186 + (*apply (rule termin_1)*)
2.187 +sorry (*by lexicographic_order unfinished subgoals*)
2.188 +(*Calls:
2.189 + a) p ~> nth_drop x p
2.190 +Measures:
2.191 + 1) list_size (nat \<circ> abs)
2.192 + 2) length
2.193 +Result matrix:
2.194 + 1 2
2.195 +a: ? <= *)
2.196 value "deg_up [3, 4, 5, 6] = 3"
2.197 value "deg_up [3, 4, 5, 6, 0] = 3"
2.198 value "deg_up [1, 0, 3, 0, 0] = 2"
2.199 @@ -311,8 +339,8 @@
2.200 fun norm :: "unipoly \<Rightarrow> unipoly \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> unipoly" where
2.201 "norm p nrm m lcp i =
2.202 (if i = 0
2.203 - then [int (mod_div (nth p i) lcp m)] @ nrm
2.204 - else norm p ([int (mod_div (nth p i) lcp m)] @ nrm) m lcp (i - 1))"
2.205 + then [int (mod_div (p ! i) lcp m)] @ nrm
2.206 + else norm p ([int (mod_div (p ! i) lcp m)] @ nrm) m lcp (i - 1))"
2.207 (* normalise a unipoly such that lcoeff_up mod m = 1.
2.208 normalise :: unipoly \<Rightarrow> nat \<Rightarrow> unipoly
2.209 normalise [p_0, .., p_k] m = [q_0, .., q_k]
2.210 @@ -410,7 +438,8 @@
2.211 apply simp
2.212 done (* > 1 sec IMPROVED BY declare simp del:
2.213 centr_up_def normalise.simps mod_up_gcd.simps lcoeff_up.simps*)
2.214 -termination sorry (*by lexicographic_order LOOPS*)
2.215 +termination (*dvd_up ..Inner syntax error*) sorry (*by lexicographic_order LOOPS*) (*not finished*)
2.216 +(*cutting definition to 'fun' loops, so no Calls, Measure, Matrix ---?*)
2.217
2.218 value "[4] dvd_up [6] = False"
2.219 value "[8] dvd_up [16, 0] = True"
2.220 @@ -469,8 +498,12 @@
2.221 definition LANDAU_MIGNOTTE_bound :: "unipoly \<Rightarrow> unipoly \<Rightarrow> nat" where
2.222 "LANDAU_MIGNOTTE_bound p1 p2 =
2.223 ((power 2 (min (deg_up p1) (deg_up p2))) * (nat (gcd (lcoeff_up p1) (lcoeff_up p2))) *
2.224 - (nat (min (abs ((approx_root (sum_lmb p1 2)) div2 -(lcoeff_up p1)))
2.225 - (abs ((approx_root (sum_lmb p2 2)) div2 -(lcoeff_up p2))))))"
2.226 + (nat (min (abs ((int (approx_root (sum_lmb p1 2))) div2 -(lcoeff_up p1)))
2.227 + (abs ((int (approx_root (sum_lmb p2 2))) div2 -(lcoeff_up p2))))))"
2.228 +(* |------------| -|------------|
2.229 + |--------------------------|
2.230 + |--------------------------------|
2.231 + |-------------------------------------------------------| *)
2.232
2.233 value "LANDAU_MIGNOTTE_bound [1] [4, 5] = 1"
2.234 value "LANDAU_MIGNOTTE_bound [1, 2] [4, 5] = 2"
2.235 @@ -489,37 +522,38 @@
2.236 subsection {* modulo calculations for polynomials *}
2.237
2.238 (* pair is just local to chinese_remainder_up, is "op ~~" in library.ML *)
2.239 -fun pair :: "unipoly \<Rightarrow> unipoly \<Rightarrow> ((int * int) list)" (infix "pair" 4) where
2.240 +fun pair :: "unipoly \<Rightarrow> unipoly \<Rightarrow> ((int \<times> int) list)" (infix "pair" 4) where
2.241 "([] pair []) = []"
2.242 | "([] pair ys) = []" (*raise ListPair.UnequalLengths*)
2.243 | "(xs pair []) = []" (*raise ListPair.UnequalLengths*)
2.244 | "((x#xs) pair (y#ys)) = (x, y) # (xs pair ys)"
2.245 -fun chinese_rem :: "nat * nat \<Rightarrow> int * int \<Rightarrow> int" where
2.246 +fun chinese_rem :: "nat \<times> nat \<Rightarrow> int \<times> int \<Rightarrow> int" where
2.247 "chinese_rem (m1, m2) (p1, p2) = (int (chinese_remainder p1 m1 p2 m2))"
2.248
2.249 (* chinese_remainder_up :: int * int \<Rightarrow> unipoly * unipoly \<Rightarrow> unipoly
2.250 chinese_remainder_up (m1, m2) (p1, p2) = p
2.251 assume m1, m2 relatively prime
2.252 yields p1 = p mod m1 \<and> p2 = p mod m2 *)
2.253 -fun chinese_remainder_up :: "nat * nat \<Rightarrow> unipoly * unipoly \<Rightarrow> unipoly" where
2.254 +fun chinese_remainder_up :: "nat \<times> nat \<Rightarrow> unipoly \<times> unipoly \<Rightarrow> unipoly" where
2.255 "chinese_remainder_up (m1, m2) (p1, p2) = map (chinese_rem (m1, m2)) (p1 pair p2)"
2.256
2.257 value "chinese_remainder_up (5, 7) ([2, 2, 4, 3], [3, 2, 3, 5]) = [17, 2, 24, 33]"
2.258
2.259 -(* mod_pol is just local to mod_up *)
2.260 -function mod_pol :: "unipoly \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unipoly" where
2.261 - "mod_pol p m n = (if n < List.length p
2.262 - then mod_pol ((List.tl p) @ [(List.hd p) mod (int m)]) m (n + 1)
2.263 - else p)"
2.264 -by auto
2.265 -termination sorry (*by lexicographic_order unfinished subgoals*)
2.266 -
2.267 -(* TODO specification *)
2.268 +(* mod_up :: unipoly \<Rightarrow> int \<Rightarrow> unipoly
2.269 + mod_up [p1, p2, ..., pk] m = up
2.270 + assume m > 0
2.271 + yields up = [p1 mod m, p2 mod m, ..., pk mod m]*)
2.272 +definition mod' :: "nat \<Rightarrow> int \<Rightarrow> int" where "mod' m i = i mod (int m)"
2.273 definition mod_up :: "unipoly \<Rightarrow> nat \<Rightarrow> unipoly" (infixl "mod'_up" 70) where
2.274 - "p mod_up m = mod_pol p m 0"
2.275 + "p mod_up m = map (mod' m) p"
2.276
2.277 value "[5, 4, 7, 8, 1] mod_up 5 = [0, 4, 2, 3, 1]"
2.278 -value "[5, 4, -7, 8, -1] mod_up 5 = [0, 4, 3, 3, 4]"
2.279 +value "[5, 4,-7, 8,-1] mod_up 5 = [0, 4, 3, 3, 4]"
2.280 +
2.281 +value "curry"
2.282 +value "curry"
2.283 +value "5 mod 3::int"
2.284 +
2.285
2.286 (* euclidean algoritm in Z_p[x].
2.287 mod_up_gcd :: unipoly \<Rightarrow> unipoly \<Rightarrow> nat \<Rightarrow> unipoly
2.288 @@ -542,7 +576,26 @@
2.289 then mod_up_gcd p2 rest m
2.290 else mod_up_gcd rest p2 m)"
2.291 by auto
2.292 -termination sorry (*by lexicographic_order unfinished subgoals*)
2.293 +termination mod_up_gcd (*not finished*)
2.294 +apply (relation "measures [\<lambda>(p1, p2, m). length p1,
2.295 + \<lambda>(p1, p2, m). 00000000000000]")
2.296 +apply auto
2.297 +sorry (*by lexicographic_order unfinished subgoals*)
2.298 +(*Calls:
2.299 + a) (p1, p2, m) ~> (p2, xab, m)
2.300 + b) (p1, p2, m) ~> (xab, p2, m)
2.301 +Measures:
2.302 + 1) \<lambda>p. size (snd (snd p))
2.303 + 2) \<lambda>p. list_size (nat \<circ> abs) (fst (snd p))
2.304 + 3) \<lambda>p. length (fst (snd p))
2.305 + 4) \<lambda>p. size (snd p)
2.306 + 5) \<lambda>p. list_size (nat \<circ> abs) (fst p)
2.307 + 6) \<lambda>p. length (fst p)
2.308 + 7) size
2.309 +Result matrix:
2.310 + 1 2 3 4 5 6 7
2.311 +a: <= ? < <= ? ? <=
2.312 +b: <= <= <= <= ? ? <= *)
2.313 declare mod_up_gcd.simps [simp del] --"HENSEL_lifting_up"
2.314
2.315 value "mod_up_gcd [-18, -15, -20, 12, 20, -13, 2] [8, 28, 22, -11, -14, 1, 2] 7 = [2, 6, 0, 2, 6]"
2.316 @@ -611,7 +664,8 @@
2.317 try_new_prime_up a b d M P g p'
2.318 )"
2.319 by pat_completeness auto --"simp del: centr_up_def normalise.simps mod_up_gcd.simps"
2.320 -termination sorry (*by lexicographic_order LOOPS*)
2.321 +termination try_new_prime_up sorry (*by lexicographic_order LOOPS*) (*not finished*)
2.322 +(*cutting definition to 'fun' loops, so no Calls, Measure, Matrix ---?*)
2.323
2.324 (* HENSEL_lifting_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> unipoly
2.325 HENSEL_lifting_up p1 p2 d M p = gcd
2.326 @@ -633,7 +687,8 @@
2.327 in
2.328 if (g dvd_up a) \<and> (g dvd_up b) then g else HENSEL_lifting_up a b d M p))"
2.329 by pat_completeness auto --"simp del: centr_up_def normalise.simps mod_up_gcd.simps"
2.330 -termination sorry (*by lexicographic_order LOOPS*)
2.331 +termination HENSEL_lifting_up sorry (*by lexicographic_order LOOPS*) (*not finished*)
2.332 +(*cutting definition to 'fun' loops, so no Calls, Measure, Matrix ---?*)
2.333
2.334 (* gcd_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> unipoly
2.335 gcd_up a b = c
2.336 @@ -646,14 +701,19 @@
2.337 in
2.338 if a = b then a else
2.339 HENSEL_lifting_up a b (nat d) (2 * (nat d) * LANDAU_MIGNOTTE_bound a b) 1)"
2.340 -by pat_completeness auto --"simp del: lcoeff_up.simps +^^^?"
2.341 +by pat_completeness auto --"simp del: lcoeff_up.simps ?+ others?"
2.342 termination by lexicographic_order (*works*)
2.343
2.344 value "gcd_up [-18, -15, -20, 12, 20, -13, 2] [8, 28, 22, -11, -14, 1, 2] = [-2, -1, 1]"
2.345 -value "gcd_up [-18, -15, -20, 12, 20, -13, 2] [8, 28, 22, -11, -14, 1, 2]"
2.346 (* gcd (-1 + x^2) (x + x^2) = (1 + x) *)
2.347 value "gcd_up [-1, 0 ,1] [0, 1, 1] = [1, 1]"
2.348 -value "gcd_up [-1, 0 ,1] [0, 1, 1]"
2.349 +
2.350 +primrec nth :: "'a list => nat => 'a" (infixl "!!" 100) where
2.351 +nth_Cons: "(x # xs) !! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs !! k)"
2.352 +value "[1,2,3,4,5] ! 2"
2.353 +
2.354 +definition mult_ups2 :: "unipoly \<Rightarrow> int \<Rightarrow> unipoly" (infixl "%*" 70) where
2.355 + "p %* m = List.map (op * m) p"
2.356
2.357 (*
2.358 print_configs