1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly.thy Tue Mar 05 20:51:15 2013 +0100
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly.thy Wed Mar 06 09:43:41 2013 +0100
1.3 @@ -183,23 +183,23 @@
1.4 subsection {* auxiliary functions for univariate polynomials *}
1.5 ML {*
1.6 (* leading coefficient *)
1.7 - fun lcoeff (uvp: unipoly) =
1.8 - if nth uvp (List.length uvp - 1) <> 0
1.9 - then nth uvp (List.length uvp - 1)
1.10 - else lcoeff (nth_drop (length uvp - 1) uvp);
1.11 + fun lcoeff (p: unipoly) =
1.12 + if nth p (List.length p - 1) <> 0
1.13 + then nth p (List.length p - 1)
1.14 + else lcoeff (nth_drop (length p - 1) p : unipoly);
1.15
1.16 (* degree *)
1.17 - fun deg (uvp: unipoly) =
1.18 - if nth uvp (length uvp - 1) <> 0
1.19 - then length uvp - 1
1.20 - else deg (nth_drop (length uvp - 1) uvp);
1.21 + fun deg (p: unipoly) =
1.22 + if nth p (length p - 1) <> 0
1.23 + then length p - 1
1.24 + else deg (nth_drop (length p - 1) p : unipoly);
1.25
1.26 (* drop leading coefficients equal 0 *)
1.27 fun drop_lc0 [] = []
1.28 - | drop_lc0 (uvp: unipoly) =
1.29 - if nth uvp (length uvp - 1) = 0
1.30 - then drop_lc0 (nth_drop (length uvp - 1) uvp)
1.31 - else uvp;
1.32 + | drop_lc0 (p: unipoly) =
1.33 + if nth p (length p - 1) = 0
1.34 + then drop_lc0 (nth_drop (length p - 1) p : unipoly)
1.35 + else p;
1.36
1.37 (* normalise a unipoly such that lcoeff mod m = 1.
1.38 normalise :: unipoly \<Rightarrow> nat \<Rightarrow> unipoly
1.39 @@ -220,37 +220,34 @@
1.40
1.41 (* scalar multiplication *)
1.42 infix %*
1.43 - fun (p: unipoly) %* n = map (Integer.mult n) p: unipoly
1.44 + fun (p: unipoly) %* n = map (Integer.mult n) p : unipoly
1.45
1.46 (* scalar divison *)
1.47 infix %/
1.48 fun (p: unipoly) %/ n =
1.49 let fun swapf f a b = f b a (* swaps the arguments of a function *)
1.50 - in map (swapf (curry op div2) n) p: unipoly end;
1.51 + in map (swapf (curry op div2) n) p : unipoly end;
1.52
1.53 (* minus of polys *)
1.54 infix %-%
1.55 - fun (p1: unipoly) %-% (p2: unipoly) = map2 (curry op -) p1
1.56 - (p2 @ replicate(List.length p1 - List.length p2) 0)
1.57 + fun (p1: unipoly) %-% (p2: unipoly) =
1.58 + map2 (curry op -) p1 (p2 @ replicate (List.length p1 - List.length p2) 0) : unipoly
1.59
1.60 (* dvd for univariate polynomials *)
1.61 infix %|%
1.62 - fun [] %|% [] = false
1.63 - | [] %|% _ = false
1.64 - | _ %|% [] = false
1.65 - | [d: int] %|% [i: int] =
1.66 - if abs d <= abs i andalso i mod d = 0 then true else false
1.67 - | (d: unipoly) %|% (p: unipoly) =
1.68 + fun [d] %|% [p] =
1.69 + if abs d <= abs p andalso p mod d = 0 then true else false
1.70 + | (ds: unipoly) %|% (ps: unipoly) =
1.71 let
1.72 - val d = drop_lc0 d;
1.73 - val p = drop_lc0 p;
1.74 - val d000 = (replicate (List.length p - List.length d) 0) @ d ;
1.75 - val quot = lcoeff p div2 lcoeff d000;
1.76 - val rest = drop_lc0 (p %-% (d000 %* quot));
1.77 + val ds = drop_lc0 ds;
1.78 + val ps = drop_lc0 ps;
1.79 + val d000 = (replicate (List.length ps - List.length ds) 0) @ ds ;
1.80 + val quot = (lcoeff ps) div2 (lcoeff d000);
1.81 + val rest = drop_lc0 (ps %-% (d000 %* quot));
1.82 in
1.83 if rest = [] then true else
1.84 - if quot <> 0 andalso List.length d <= List.length rest
1.85 - then d %|% rest
1.86 + if quot <> 0 andalso List.length ds <= List.length rest
1.87 + then ds %|% rest
1.88 else false
1.89 end
1.90
1.91 @@ -264,7 +261,7 @@
1.92 val mi = m div2 2;
1.93 val mid = if m mod mi = 0 then mi else mi + 1;
1.94 fun centr m mid p_i = if mid < p_i then p_i - m else p_i;
1.95 - in map (centr m mid) p end;
1.96 + in map (centr m mid) p : unipoly end;
1.97
1.98 (*** landau mignotte bound (Winkler p91)
1.99 every coefficient of the gcd of a and b in Z[x] is bounded in absolute value by
2.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Tue Mar 05 20:51:15 2013 +0100
2.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Wed Mar 06 09:43:41 2013 +0100
2.3 @@ -11,6 +11,7 @@
2.4 the style of GCD_Poly.thy has been adapted to the function package.
2.5 *}
2.6
2.7 +(* WN130304 see Algebra/poly/LongDiv.thy: lcoeff_def*)
2.8 (*---------------------------------------------------------------------------------------------
2.9 declare [[simp_trace_depth_limit = 99]]
2.10 declare [[simp_trace = true]]
2.11 @@ -300,6 +301,8 @@
2.12 value "[8, -7, 0, 1] minus_up [-2, 2, 3, 0] = [10, -9, -3, 1]"
2.13 value "[8, 7, 6, 5, 4] minus_up [2, 2, 3, 1, 1] = [6, 5, 3, 4, 3]"
2.14
2.15 +ML {*1-1-1-1-1-1-1-1-1-1-1-1-1-1-1-1-1*}
2.16 +
2.17 (* dvd for univariate polynomials *)
2.18 (*---------------------------------------------------------------------------------------------
2.19 declare [[simp_trace_depth_limit = 99]]
2.20 @@ -582,9 +585,8 @@
2.21 (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))
2.22 in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) *)
2.23 -------------------------------------------------------------------------------------------
2.24 - 2nd trial --> 3 unsolvable subgoals
2.25 + 2nd trial --> 3 unsolvable subgoals on compatiblity of patterns
2.26 -------------------------------------------------------------------------------------------
2.27 ----------------------------------------------------------------------------------------------*)
2.28 function dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where
2.29 "[] dvd_up p = False"
2.30 | "d dvd_up [] = False"
2.31 @@ -616,20 +618,108 @@
2.32 (*goal (3 subgoals): ### the 1st subgoals disappears, the others are the same
2.33 1. \<And>p d pa. ([], p) = (d, pa) \<Longrightarrow>
2.34 False = (let d = drop_lc0 d; p = drop_lc0 pa; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))
2.35 - in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)
2.36 + in if rest = [] then True else if quot \<noteq> 0 \<and> replicate length d \<le> length rest then dvd_up_sumC (d, rest) else False)
2.37 2. \<And>d da p. (d, []) = (da, p) \<Longrightarrow>
2.38 False = (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))
2.39 in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)
2.40 3. \<And>d i da p. ([d], [i]) = (da, p) \<Longrightarrow>
2.41 (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) =
2.42 (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))
2.43 - in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) *)
2.44 + in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)
2.45 +---------------------------------------------------------------------------------------------
2.46 +but completing the sequence of equations doesn't help,
2.47 +because the most difficult subgoal (3. above, 4. above above) remains the same.
2.48 +---------------------------------------------------------------------------------------------
2.49 +*)
2.50 +------------------------------GCD_Poly ML-->Isabelle:-------------------------------------------*)
2.51 +function dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where
2.52 + "[d] dvd_up [p] =
2.53 + (if (\<bar>d\<bar> \<le> \<bar>p\<bar>) & (p mod d = 0) then True else False)"
2.54 +| "ds dvd_up ps =
2.55 + (let
2.56 + ds = drop_lc0 ds; ps = drop_lc0 ps;
2.57 + d000 = (List.replicate (List.length ps - List.length ds) 0) @ ds;
2.58 + quot = (lcoeff ps) div2 (lcoeff d000);
2.59 + rest = drop_lc0 (ps minus_up (d000 mult_ups quot))
2.60 + in
2.61 + if rest = [] then True else
2.62 + if quot \<noteq> 0 & List.length ds \<le> List.length rest then ds dvd_up rest else False)"
2.63 +(*using [[show_types = true]]*)
2.64 +apply pat_completeness
2.65 +apply simp
2.66 +defer
2.67 +apply simp
2.68 +(*---------------------------------------------------------------------------------------------
2.69 + 1. \<And>(d\<Colon>int) (p\<Colon>int) (ds\<Colon>int list) ps\<Colon>int list.
2.70 + ([d], [p]) = (ds, ps) \<Longrightarrow>
2.71 + (if \<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int) then True else False) =
2.72 + (let ds\<Colon>int list = drop_lc0 ds; ps\<Colon>int list = drop_lc0 ps;
2.73 + d000\<Colon>int list = replicate (length ps - length ds) (0\<Colon>int) @ ds;
2.74 + quot\<Colon>int = (lcoeff ps) div2 (lcoeff d000);
2.75 + rest\<Colon>int list = drop_lc0 (ps minus_up (d000 mult_ups quot))
2.76 + in if rest = [] then True
2.77 + else if quot \<noteq> (0\<Colon>int) \<and> length ds \<le> length rest then dvd_up_sumC (ds, rest) else False)
2.78 +---------------------------------------------------------------------------------------------*)
2.79 +(*apply simp*)
2.80 +(*apply (subst Product_Type.Pair_eq) ???*)
2.81 +sorry
2.82
2.83 +find_theorems "_ \<and> _ = _ \<and> _"
2.84
2.85 +lemma d000: "ds = [d] \<and> ps = [p] \<longrightarrow> replicate (length ps - length ds) (0\<Colon>int) @ ds = [d]"
2.86 +by simp
2.87 +thm d000
2.88
2.89 +lemma quot: "([d] mult_ups ((lcoeff [p]) div2 (lcoeff [d]))) = [p]"
2.90 +(*by simp ..loops GOON*)
2.91 sorry
2.92 +
2.93 +lemma lem\<^isub>_1: "\<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int) \<and> d \<noteq> 0 \<and> p \<noteq> 0 \<longrightarrow>
2.94 + drop_lc0 ([p] minus_up (d000 mult_ups quot)) = []"
2.95 +sorry
2.96 +
2.97 +
2.98 +lemma pat_compatibility [case_names equ\<^isub>1_true equ\<^isub>1_false]:
2.99 + fixes d p :: int and ds ps :: "unipoly"
2.100 + assumes args_equal: "([d], [p]) = (ds, ps)" and not_zero: "d \<noteq> 0 \<and> p \<noteq> 0"
2.101 + assumes equ\<^isub>1_true: " \<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int)"
2.102 + assumes equ\<^isub>1_false: "\<not> (\<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int))"
2.103 + shows "(if \<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int) then True else False) \<equiv>
2.104 + (let ds = drop_lc0 ds; ps = drop_lc0 ps;
2.105 + d000 = replicate (length ps - length ds) (0\<Colon>int) @ ds;
2.106 + quot = lcoeff ps div2 lcoeff d000;
2.107 + rest = drop_lc0 (ps minus_up (d000 div_ups quot))
2.108 + in if rest = [] then True else
2.109 + if quot \<noteq> (0\<Colon>int) \<and> length ds \<le> length rest then dvd_up_sumC (ds, rest) else False)"
2.110 + (is "?equ\<^isub>1 \<equiv> ?equ\<^isub>2")
2.111 +proof -
2.112 + have args_equal': "[d] = ds \<and> [p] = ps" using args_equal by auto (*(rule Pair_eq) ?!?*)
2.113 + assume equ\<^isub>2: "?equ\<^isub>2"
2.114 + have equ\<^isub>2':
2.115 + "let d000 = replicate (length [p] - length [d]) (0\<Colon>int) @ [d];
2.116 + quot = lcoeff [p] div2 lcoeff d000;
2.117 + rest = drop_lc0 ([p] minus_up (d000 div_ups quot))
2.118 + in if rest = [] then True else
2.119 + if quot \<noteq> (0\<Colon>int) \<and> length [d] \<le> length rest then dvd_up_sumC ([d], rest) else False"
2.120 + using args_equal' equ\<^isub>2 (*by auto*)
2.121 + proof -
2.122 + from not_zero have 1: "[d] = drop_lc0 [d]" by auto
2.123 + from not_zero have 2: "[p] = drop_lc0 [p]" by auto
2.124 +(*
2.125 + from equ\<^isub>1_true have ?equ\<^isub>1 by auto
2.126 + from args_equal' equ\<^isub>1_false have "~ ?equ\<^isub>2"
2.127 + proof -
2.128 +*)
2.129 +oops
2.130 +
2.131 ML {*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*}
2.132
2.133 +value "replicate 5 (0::int)"
2.134 +value "-7 div2 (0::int)"
2.135 +value "[0, 0, 0] div_ups (0::int)"
2.136 +value "[1, -2, 3] minus_up [0, 0, 0]"
2.137 +
2.138 +value "xxx"
2.139 (*---------------------------------------------------------------------------------------------
2.140 (*
2.141 value "[2, 3] dvd_up [8, 22, 15] = True"
3.1 --- a/test/Tools/isac/Test_Some2.thy Tue Mar 05 20:51:15 2013 +0100
3.2 +++ b/test/Tools/isac/Test_Some2.thy Wed Mar 06 09:43:41 2013 +0100
3.3 @@ -7,20 +7,6 @@
3.4 use"~~/test/Tools/isac/Knowledge/gcd_poly.sml"
3.5
3.6 ML {*
3.7 -gcd_poly
3.8 -[(~3,[2,0]),(1,[5,0]),(3,[0,1]),(~6,[1,1]),(~1,[3,1]),(2,[4,1]),(1,[3,2]),(~1,[1,3]),(2,[2,3])]
3.9 -[(2,[2,0]),(~2,[0,1]),(4,[1,1]),(~1,[3,1]),(1,[1,2]),(~1,[2,2]),(~1,[0,3]),(2,[1,3])]
3.10 -*}
3.11 -ML {*
3.12 -*}
3.13 -ML {**}
3.14 -ML {*
3.15 -*}
3.16 -ML {*
3.17 -*}
3.18 -ML {*
3.19 -*}
3.20 -ML {*
3.21 *}
3.22 ML {*
3.23 *}