delete Groebner_Basis directory -- only one file left
authorhaftmann
Fri May 07 16:12:25 2010 +0200 (2010-05-07)
changeset 36752cf558aeb35b0
parent 36751 7f1da69cacb3
child 36753 5cf4e9128f22
delete Groebner_Basis directory -- only one file left
src/HOL/Groebner_Basis.thy
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/groebner.ML
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri May 07 15:05:52 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri May 07 16:12:25 2010 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  theory Groebner_Basis
     1.5  imports Semiring_Normalization
     1.6  uses
     1.7 -  ("Tools/Groebner_Basis/groebner.ML")
     1.8 +  ("Tools/groebner.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Groebner Bases *}
    1.12 @@ -40,7 +40,7 @@
    1.13  
    1.14  setup Algebra_Simplification.setup
    1.15  
    1.16 -use "Tools/Groebner_Basis/groebner.ML"
    1.17 +use "Tools/groebner.ML"
    1.18  
    1.19  method_setup algebra = Groebner.algebra_method
    1.20    "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
     2.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Fri May 07 15:05:52 2010 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,1045 +0,0 @@
     2.4 -(*  Title:      HOL/Tools/Groebner_Basis/groebner.ML
     2.5 -    Author:     Amine Chaieb, TU Muenchen
     2.6 -*)
     2.7 -
     2.8 -signature GROEBNER =
     2.9 -sig
    2.10 -  val ring_and_ideal_conv :
    2.11 -    {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list,
    2.12 -     vars: cterm list, semiring: cterm list * thm list, ideal : thm list} ->
    2.13 -    (cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
    2.14 -    conv ->  conv ->
    2.15 -     {ring_conv : conv, 
    2.16 -     simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list),
    2.17 -     multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list,
    2.18 -     poly_eq_ss: simpset, unwind_conv : conv}
    2.19 -  val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
    2.20 -  val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
    2.21 -  val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
    2.22 -  val algebra_method: (Proof.context -> Method.method) context_parser
    2.23 -end
    2.24 -
    2.25 -structure Groebner : GROEBNER =
    2.26 -struct
    2.27 -
    2.28 -open Conv Drule Thm;
    2.29 -
    2.30 -fun is_comb ct =
    2.31 -  (case Thm.term_of ct of
    2.32 -    _ $ _ => true
    2.33 -  | _ => false);
    2.34 -
    2.35 -val concl = Thm.cprop_of #> Thm.dest_arg;
    2.36 -
    2.37 -fun is_binop ct ct' =
    2.38 -  (case Thm.term_of ct' of
    2.39 -    c $ _ $ _ => term_of ct aconv c
    2.40 -  | _ => false);
    2.41 -
    2.42 -fun dest_binary ct ct' =
    2.43 -  if is_binop ct ct' then Thm.dest_binop ct'
    2.44 -  else raise CTERM ("dest_binary: bad binop", [ct, ct'])
    2.45 -
    2.46 -fun inst_thm inst = Thm.instantiate ([], inst);
    2.47 -
    2.48 -val rat_0 = Rat.zero;
    2.49 -val rat_1 = Rat.one;
    2.50 -val minus_rat = Rat.neg;
    2.51 -val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
    2.52 -fun int_of_rat a =
    2.53 -    case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int";
    2.54 -val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
    2.55 -
    2.56 -val (eqF_intr, eqF_elim) =
    2.57 -  let val [th1,th2] = @{thms PFalse}
    2.58 -  in (fn th => th COMP th2, fn th => th COMP th1) end;
    2.59 -
    2.60 -val (PFalse, PFalse') =
    2.61 - let val PFalse_eq = nth @{thms simp_thms} 13
    2.62 - in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end;
    2.63 -
    2.64 -
    2.65 -(* Type for recording history, i.e. how a polynomial was obtained. *)
    2.66 -
    2.67 -datatype history =
    2.68 -   Start of int
    2.69 - | Mmul of (Rat.rat * int list) * history
    2.70 - | Add of history * history;
    2.71 -
    2.72 -
    2.73 -(* Monomial ordering. *)
    2.74 -
    2.75 -fun morder_lt m1 m2=
    2.76 -    let fun lexorder l1 l2 =
    2.77 -            case (l1,l2) of
    2.78 -                ([],[]) => false
    2.79 -              | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2
    2.80 -              | _ => error "morder: inconsistent monomial lengths"
    2.81 -        val n1 = Integer.sum m1
    2.82 -        val n2 = Integer.sum m2 in
    2.83 -    n1 < n2 orelse n1 = n2 andalso lexorder m1 m2
    2.84 -    end;
    2.85 -
    2.86 -fun morder_le m1 m2 = morder_lt m1 m2 orelse (m1 = m2);
    2.87 -
    2.88 -fun morder_gt m1 m2 = morder_lt m2 m1;
    2.89 -
    2.90 -(* Arithmetic on canonical polynomials. *)
    2.91 -
    2.92 -fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l;
    2.93 -
    2.94 -fun grob_add l1 l2 =
    2.95 -  case (l1,l2) of
    2.96 -    ([],l2) => l2
    2.97 -  | (l1,[]) => l1
    2.98 -  | ((c1,m1)::o1,(c2,m2)::o2) =>
    2.99 -        if m1 = m2 then
   2.100 -          let val c = c1+/c2 val rest = grob_add o1 o2 in
   2.101 -          if c =/ rat_0 then rest else (c,m1)::rest end
   2.102 -        else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
   2.103 -        else (c2,m2)::(grob_add l1 o2);
   2.104 -
   2.105 -fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
   2.106 -
   2.107 -fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2));
   2.108 -
   2.109 -fun grob_cmul cm pol = map (grob_mmul cm) pol;
   2.110 -
   2.111 -fun grob_mul l1 l2 =
   2.112 -  case l1 of
   2.113 -    [] => []
   2.114 -  | (h1::t1) => grob_add (grob_cmul h1 l2) (grob_mul t1 l2);
   2.115 -
   2.116 -fun grob_inv l =
   2.117 -  case l of
   2.118 -    [(c,vs)] => if (forall (fn x => x = 0) vs) then
   2.119 -                  if (c =/ rat_0) then error "grob_inv: division by zero"
   2.120 -                  else [(rat_1 // c,vs)]
   2.121 -              else error "grob_inv: non-constant divisor polynomial"
   2.122 -  | _ => error "grob_inv: non-constant divisor polynomial";
   2.123 -
   2.124 -fun grob_div l1 l2 =
   2.125 -  case l2 of
   2.126 -    [(c,l)] => if (forall (fn x => x = 0) l) then
   2.127 -                 if c =/ rat_0 then error "grob_div: division by zero"
   2.128 -                 else grob_cmul (rat_1 // c,l) l1
   2.129 -             else error "grob_div: non-constant divisor polynomial"
   2.130 -  | _ => error "grob_div: non-constant divisor polynomial";
   2.131 -
   2.132 -fun grob_pow vars l n =
   2.133 -  if n < 0 then error "grob_pow: negative power"
   2.134 -  else if n = 0 then [(rat_1,map (fn v => 0) vars)]
   2.135 -  else grob_mul l (grob_pow vars l (n - 1));
   2.136 -
   2.137 -fun degree vn p =
   2.138 - case p of
   2.139 -  [] => error "Zero polynomial"
   2.140 -| [(c,ns)] => nth ns vn
   2.141 -| (c,ns)::p' => Int.max (nth ns vn, degree vn p');
   2.142 -
   2.143 -fun head_deg vn p = let val d = degree vn p in
   2.144 - (d,fold (fn (c,r) => fn q => grob_add q [(c, map_index (fn (i,n) => if i = vn then 0 else n) r)]) (filter (fn (c,ns) => c <>/ rat_0 andalso nth ns vn = d) p) []) end;
   2.145 -
   2.146 -val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns);
   2.147 -val grob_pdiv =
   2.148 - let fun pdiv_aux vn (n,a) p k s =
   2.149 -  if is_zerop s then (k,s) else
   2.150 -  let val (m,b) = head_deg vn s
   2.151 -  in if m < n then (k,s) else
   2.152 -     let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0)
   2.153 -                                                (snd (hd s)))]
   2.154 -     in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p')
   2.155 -        else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p'))
   2.156 -     end
   2.157 -  end
   2.158 - in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s
   2.159 - end;
   2.160 -
   2.161 -(* Monomial division operation. *)
   2.162 -
   2.163 -fun mdiv (c1,m1) (c2,m2) =
   2.164 -  (c1//c2,
   2.165 -   map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2);
   2.166 -
   2.167 -(* Lowest common multiple of two monomials. *)
   2.168 -
   2.169 -fun mlcm (c1,m1) (c2,m2) = (rat_1, ListPair.map Int.max (m1, m2));
   2.170 -
   2.171 -(* Reduce monomial cm by polynomial pol, returning replacement for cm.  *)
   2.172 -
   2.173 -fun reduce1 cm (pol,hpol) =
   2.174 -  case pol of
   2.175 -    [] => error "reduce1"
   2.176 -  | cm1::cms => ((let val (c,m) = mdiv cm cm1 in
   2.177 -                    (grob_cmul (minus_rat c,m) cms,
   2.178 -                     Mmul((minus_rat c,m),hpol)) end)
   2.179 -                handle  ERROR _ => error "reduce1");
   2.180 -
   2.181 -(* Try this for all polynomials in a basis.  *)
   2.182 -fun tryfind f l =
   2.183 -    case l of
   2.184 -        [] => error "tryfind"
   2.185 -      | (h::t) => ((f h) handle ERROR _ => tryfind f t);
   2.186 -
   2.187 -fun reduceb cm basis = tryfind (fn p => reduce1 cm p) basis;
   2.188 -
   2.189 -(* Reduction of a polynomial (always picking largest monomial possible).     *)
   2.190 -
   2.191 -fun reduce basis (pol,hist) =
   2.192 -  case pol of
   2.193 -    [] => (pol,hist)
   2.194 -  | cm::ptl => ((let val (q,hnew) = reduceb cm basis in
   2.195 -                   reduce basis (grob_add q ptl,Add(hnew,hist)) end)
   2.196 -               handle (ERROR _) =>
   2.197 -                   (let val (q,hist') = reduce basis (ptl,hist) in
   2.198 -                       (cm::q,hist') end));
   2.199 -
   2.200 -(* Check for orthogonality w.r.t. LCM.                                       *)
   2.201 -
   2.202 -fun orthogonal l p1 p2 =
   2.203 -  snd l = snd(grob_mmul (hd p1) (hd p2));
   2.204 -
   2.205 -(* Compute S-polynomial of two polynomials.                                  *)
   2.206 -
   2.207 -fun spoly cm ph1 ph2 =
   2.208 -  case (ph1,ph2) of
   2.209 -    (([],h),p) => ([],h)
   2.210 -  | (p,([],h)) => ([],h)
   2.211 -  | ((cm1::ptl1,his1),(cm2::ptl2,his2)) =>
   2.212 -        (grob_sub (grob_cmul (mdiv cm cm1) ptl1)
   2.213 -                  (grob_cmul (mdiv cm cm2) ptl2),
   2.214 -         Add(Mmul(mdiv cm cm1,his1),
   2.215 -             Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2)));
   2.216 -
   2.217 -(* Make a polynomial monic.                                                  *)
   2.218 -
   2.219 -fun monic (pol,hist) =
   2.220 -  if null pol then (pol,hist) else
   2.221 -  let val (c',m') = hd pol in
   2.222 -  (map (fn (c,m) => (c//c',m)) pol,
   2.223 -   Mmul((rat_1 // c',map (K 0) m'),hist)) end;
   2.224 -
   2.225 -(* The most popular heuristic is to order critical pairs by LCM monomial.    *)
   2.226 -
   2.227 -fun forder ((c1,m1),_) ((c2,m2),_) = morder_lt m1 m2;
   2.228 -
   2.229 -fun poly_lt  p q =
   2.230 -  case (p,q) of
   2.231 -    (p,[]) => false
   2.232 -  | ([],q) => true
   2.233 -  | ((c1,m1)::o1,(c2,m2)::o2) =>
   2.234 -        c1 </ c2 orelse
   2.235 -        c1 =/ c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
   2.236 -
   2.237 -fun align  ((p,hp),(q,hq)) =
   2.238 -  if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
   2.239 -fun forall2 p l1 l2 =
   2.240 -  case (l1,l2) of
   2.241 -    ([],[]) => true
   2.242 -  | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
   2.243 -  | _ => false;
   2.244 -
   2.245 -fun poly_eq p1 p2 =
   2.246 -  forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2;
   2.247 -
   2.248 -fun memx ((p1,h1),(p2,h2)) ppairs =
   2.249 -  not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
   2.250 -
   2.251 -(* Buchberger's second criterion.                                            *)
   2.252 -
   2.253 -fun criterion2 basis (lcm,((p1,h1),(p2,h2))) opairs =
   2.254 -  exists (fn g => not(poly_eq (fst g) p1) andalso not(poly_eq (fst g) p2) andalso
   2.255 -                   can (mdiv lcm) (hd(fst g)) andalso
   2.256 -                   not(memx (align (g,(p1,h1))) (map snd opairs)) andalso
   2.257 -                   not(memx (align (g,(p2,h2))) (map snd opairs))) basis;
   2.258 -
   2.259 -(* Test for hitting constant polynomial.                                     *)
   2.260 -
   2.261 -fun constant_poly p =
   2.262 -  length p = 1 andalso forall (fn x => x = 0) (snd(hd p));
   2.263 -
   2.264 -(* Grobner basis algorithm.                                                  *)
   2.265 -
   2.266 -(* FIXME: try to get rid of mergesort? *)
   2.267 -fun merge ord l1 l2 =
   2.268 - case l1 of
   2.269 -  [] => l2
   2.270 - | h1::t1 =>
   2.271 -   case l2 of
   2.272 -    [] => l1
   2.273 -   | h2::t2 => if ord h1 h2 then h1::(merge ord t1 l2)
   2.274 -               else h2::(merge ord l1 t2);
   2.275 -fun mergesort ord l =
   2.276 - let
   2.277 - fun mergepairs l1 l2 =
   2.278 -  case (l1,l2) of
   2.279 -   ([s],[]) => s
   2.280 - | (l,[]) => mergepairs [] l
   2.281 - | (l,[s1]) => mergepairs (s1::l) []
   2.282 - | (l,(s1::s2::ss)) => mergepairs ((merge ord s1 s2)::l) ss
   2.283 - in if null l  then []  else mergepairs [] (map (fn x => [x]) l)
   2.284 - end;
   2.285 -
   2.286 -
   2.287 -fun grobner_basis basis pairs =
   2.288 - case pairs of
   2.289 -   [] => basis
   2.290 - | (l,(p1,p2))::opairs =>
   2.291 -   let val (sph as (sp,hist)) = monic (reduce basis (spoly l p1 p2))
   2.292 -   in 
   2.293 -    if null sp orelse criterion2 basis (l,(p1,p2)) opairs
   2.294 -    then grobner_basis basis opairs
   2.295 -    else if constant_poly sp then grobner_basis (sph::basis) []
   2.296 -    else 
   2.297 -     let 
   2.298 -      val rawcps = map (fn p => (mlcm (hd(fst p)) (hd sp),align(p,sph)))
   2.299 -                              basis
   2.300 -      val newcps = filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q)))
   2.301 -                        rawcps
   2.302 -     in grobner_basis (sph::basis)
   2.303 -                 (merge forder opairs (mergesort forder newcps))
   2.304 -     end
   2.305 -   end;
   2.306 -
   2.307 -(* Interreduce initial polynomials.                                          *)
   2.308 -
   2.309 -fun grobner_interreduce rpols ipols =
   2.310 -  case ipols of
   2.311 -    [] => map monic (rev rpols)
   2.312 -  | p::ps => let val p' = reduce (rpols @ ps) p in
   2.313 -             if null (fst p') then grobner_interreduce rpols ps
   2.314 -             else grobner_interreduce (p'::rpols) ps end;
   2.315 -
   2.316 -(* Overall function.                                                         *)
   2.317 -
   2.318 -fun grobner pols =
   2.319 -    let val npols = map_index (fn (n, p) => (p, Start n)) pols
   2.320 -        val phists = filter (fn (p,_) => not (null p)) npols
   2.321 -        val bas = grobner_interreduce [] (map monic phists)
   2.322 -        val prs0 = map_product pair bas bas
   2.323 -        val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0
   2.324 -        val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1
   2.325 -        val prs3 =
   2.326 -            filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) prs2 in
   2.327 -        grobner_basis bas (mergesort forder prs3) end;
   2.328 -
   2.329 -(* Get proof of contradiction from Grobner basis.                            *)
   2.330 -
   2.331 -fun find p l =
   2.332 -  case l of
   2.333 -      [] => error "find"
   2.334 -    | (h::t) => if p(h) then h else find p t;
   2.335 -
   2.336 -fun grobner_refute pols =
   2.337 -  let val gb = grobner pols in
   2.338 -  snd(find (fn (p,h) => length p = 1 andalso forall (fn x=> x=0) (snd(hd p))) gb)
   2.339 -  end;
   2.340 -
   2.341 -(* Turn proof into a certificate as sum of multipliers.                      *)
   2.342 -(* In principle this is very inefficient: in a heavily shared proof it may   *)
   2.343 -(* make the same calculation many times. Could put in a cache or something.  *)
   2.344 -
   2.345 -fun resolve_proof vars prf =
   2.346 -  case prf of
   2.347 -    Start(~1) => []
   2.348 -  | Start m => [(m,[(rat_1,map (K 0) vars)])]
   2.349 -  | Mmul(pol,lin) =>
   2.350 -        let val lis = resolve_proof vars lin in
   2.351 -            map (fn (n,p) => (n,grob_cmul pol p)) lis end
   2.352 -  | Add(lin1,lin2) =>
   2.353 -        let val lis1 = resolve_proof vars lin1
   2.354 -            val lis2 = resolve_proof vars lin2
   2.355 -            val dom = distinct (op =) (union (op =) (map fst lis1) (map fst lis2))
   2.356 -        in
   2.357 -            map (fn n => let val a = these (AList.lookup (op =) lis1 n)
   2.358 -                             val b = these (AList.lookup (op =) lis2 n)
   2.359 -                         in (n,grob_add a b) end) dom end;
   2.360 -
   2.361 -(* Run the procedure and produce Weak Nullstellensatz certificate.           *)
   2.362 -
   2.363 -fun grobner_weak vars pols =
   2.364 -    let val cert = resolve_proof vars (grobner_refute pols)
   2.365 -        val l =
   2.366 -            fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
   2.367 -        (l,map (fn (i,p) => (i,map (fn (d,m) => (l*/d,m)) p)) cert) end;
   2.368 -
   2.369 -(* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)
   2.370 -
   2.371 -fun grobner_ideal vars pols pol =
   2.372 -  let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in
   2.373 -  if not (null pol') then error "grobner_ideal: not in the ideal" else
   2.374 -  resolve_proof vars h end;
   2.375 -
   2.376 -(* Produce Strong Nullstellensatz certificate for a power of pol.            *)
   2.377 -
   2.378 -fun grobner_strong vars pols pol =
   2.379 -    let val vars' = @{cterm "True"}::vars
   2.380 -        val grob_z = [(rat_1,1::(map (fn x => 0) vars))]
   2.381 -        val grob_1 = [(rat_1,(map (fn x => 0) vars'))]
   2.382 -        fun augment p= map (fn (c,m) => (c,0::m)) p
   2.383 -        val pols' = map augment pols
   2.384 -        val pol' = augment pol
   2.385 -        val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols'
   2.386 -        val (l,cert) = grobner_weak vars' allpols
   2.387 -        val d = fold (fold (Integer.max o hd o snd) o snd) cert 0
   2.388 -        fun transform_monomial (c,m) =
   2.389 -            grob_cmul (c,tl m) (grob_pow vars pol (d - hd m))
   2.390 -        fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q []
   2.391 -        val cert' = map (fn (c,q) => (c-1,transform_polynomial q))
   2.392 -                        (filter (fn (k,_) => k <> 0) cert) in
   2.393 -        (d,l,cert') end;
   2.394 -
   2.395 -
   2.396 -(* Overall parametrized universal procedure for (semi)rings.                 *)
   2.397 -(* We return an ideal_conv and the actual ring prover.                       *)
   2.398 -
   2.399 -fun refute_disj rfn tm =
   2.400 - case term_of tm of
   2.401 -  Const("op |",_)$l$r =>
   2.402 -   compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
   2.403 -  | _ => rfn tm ;
   2.404 -
   2.405 -val notnotD = @{thm notnotD};
   2.406 -fun mk_binop ct x y = capply (capply ct x) y
   2.407 -
   2.408 -val mk_comb = capply;
   2.409 -fun is_neg t =
   2.410 -    case term_of t of
   2.411 -      (Const("Not",_)$p) => true
   2.412 -    | _  => false;
   2.413 -fun is_eq t =
   2.414 - case term_of t of
   2.415 - (Const("op =",_)$_$_) => true
   2.416 -| _  => false;
   2.417 -
   2.418 -fun end_itlist f l =
   2.419 -  case l of
   2.420 -        []     => error "end_itlist"
   2.421 -      | [x]    => x
   2.422 -      | (h::t) => f h (end_itlist f t);
   2.423 -
   2.424 -val list_mk_binop = fn b => end_itlist (mk_binop b);
   2.425 -
   2.426 -val list_dest_binop = fn b =>
   2.427 - let fun h acc t =
   2.428 -  ((let val (l,r) = dest_binary b t in h (h acc r) l end)
   2.429 -   handle CTERM _ => (t::acc)) (* Why had I handle _ => ? *)
   2.430 - in h []
   2.431 - end;
   2.432 -
   2.433 -val strip_exists =
   2.434 - let fun h (acc, t) =
   2.435 -      case (term_of t) of
   2.436 -       Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
   2.437 -     | _ => (acc,t)
   2.438 - in fn t => h ([],t)
   2.439 - end;
   2.440 -
   2.441 -fun is_forall t =
   2.442 - case term_of t of
   2.443 -  (Const("All",_)$Abs(_,_,_)) => true
   2.444 -| _ => false;
   2.445 -
   2.446 -val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
   2.447 -val bool_simps = @{thms bool_simps};
   2.448 -val nnf_simps = @{thms nnf_simps};
   2.449 -val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps bool_simps addsimps nnf_simps)
   2.450 -val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms weak_dnf_simps});
   2.451 -val initial_conv =
   2.452 -    Simplifier.rewrite
   2.453 -     (HOL_basic_ss addsimps nnf_simps
   2.454 -       addsimps [not_all, not_ex]
   2.455 -       addsimps map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps}));
   2.456 -
   2.457 -val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   2.458 -
   2.459 -val cTrp = @{cterm "Trueprop"};
   2.460 -val cConj = @{cterm "op &"};
   2.461 -val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
   2.462 -val assume_Trueprop = mk_comb cTrp #> assume;
   2.463 -val list_mk_conj = list_mk_binop cConj;
   2.464 -val conjs = list_dest_binop cConj;
   2.465 -val mk_neg = mk_comb cNot;
   2.466 -
   2.467 -fun striplist dest = 
   2.468 - let
   2.469 -  fun h acc x = case try dest x of
   2.470 -    SOME (a,b) => h (h acc b) a
   2.471 -  | NONE => x::acc
   2.472 - in h [] end;
   2.473 -fun list_mk_binop b = foldr1 (fn (s,t) => Thm.capply (Thm.capply b s) t);
   2.474 -
   2.475 -val eq_commute = mk_meta_eq @{thm eq_commute};
   2.476 -
   2.477 -fun sym_conv eq = 
   2.478 - let val (l,r) = Thm.dest_binop eq
   2.479 - in instantiate' [SOME (ctyp_of_term l)] [SOME l, SOME r] eq_commute
   2.480 - end;
   2.481 -
   2.482 -  (* FIXME : copied from cqe.ML -- complex QE*)
   2.483 -fun conjuncts ct =
   2.484 - case term_of ct of
   2.485 -  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
   2.486 -| _ => [ct];
   2.487 -
   2.488 -fun fold1 f = foldr1 (uncurry f);
   2.489 -
   2.490 -val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
   2.491 -
   2.492 -fun mk_conj_tab th = 
   2.493 - let fun h acc th = 
   2.494 -   case prop_of th of
   2.495 -   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
   2.496 -     h (h acc (th RS conjunct2)) (th RS conjunct1)
   2.497 -  | @{term "Trueprop"}$p => (p,th)::acc
   2.498 -in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
   2.499 -
   2.500 -fun is_conj (@{term "op &"}$_$_) = true
   2.501 -  | is_conj _ = false;
   2.502 -
   2.503 -fun prove_conj tab cjs = 
   2.504 - case cjs of 
   2.505 -   [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c
   2.506 - | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
   2.507 -
   2.508 -fun conj_ac_rule eq = 
   2.509 - let 
   2.510 -  val (l,r) = Thm.dest_equals eq
   2.511 -  val ctabl = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} l))
   2.512 -  val ctabr = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} r))
   2.513 -  fun tabl c = the (Termtab.lookup ctabl (term_of c))
   2.514 -  fun tabr c = the (Termtab.lookup ctabr (term_of c))
   2.515 -  val thl  = prove_conj tabl (conjuncts r) |> implies_intr_hyps
   2.516 -  val thr  = prove_conj tabr (conjuncts l) |> implies_intr_hyps
   2.517 -  val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI}
   2.518 - in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end;
   2.519 -
   2.520 - (* END FIXME.*)
   2.521 -
   2.522 -   (* Conversion for the equivalence of existential statements where 
   2.523 -      EX quantifiers are rearranged differently *)
   2.524 - fun ext T = cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   2.525 - fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
   2.526 -
   2.527 -fun choose v th th' = case concl_of th of 
   2.528 -  @{term Trueprop} $ (Const("Ex",_)$_) => 
   2.529 -   let
   2.530 -    val p = (funpow 2 Thm.dest_arg o cprop_of) th
   2.531 -    val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   2.532 -    val th0 = fconv_rule (Thm.beta_conversion true)
   2.533 -        (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
   2.534 -    val pv = (Thm.rhs_of o Thm.beta_conversion true) 
   2.535 -          (Thm.capply @{cterm Trueprop} (Thm.capply p v))
   2.536 -    val th1 = forall_intr v (implies_intr pv th')
   2.537 -   in implies_elim (implies_elim th0 th) th1  end
   2.538 -| _ => error ""
   2.539 -
   2.540 -fun simple_choose v th = 
   2.541 -   choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
   2.542 -
   2.543 -
   2.544 - fun mkexi v th = 
   2.545 -  let 
   2.546 -   val p = Thm.cabs v (Thm.dest_arg (Thm.cprop_of th))
   2.547 -  in implies_elim 
   2.548 -    (fconv_rule (Thm.beta_conversion true) (instantiate' [SOME (ctyp_of_term v)] [SOME p, SOME v] @{thm exI}))
   2.549 -      th
   2.550 -  end
   2.551 - fun ex_eq_conv t = 
   2.552 -  let 
   2.553 -  val (p0,q0) = Thm.dest_binop t
   2.554 -  val (vs',P) = strip_exists p0 
   2.555 -  val (vs,_) = strip_exists q0 
   2.556 -   val th = assume (Thm.capply @{cterm Trueprop} P)
   2.557 -   val th1 =  implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th))
   2.558 -   val th2 =  implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
   2.559 -   val p = (Thm.dest_arg o Thm.dest_arg1 o cprop_of) th1
   2.560 -   val q = (Thm.dest_arg o Thm.dest_arg o cprop_of) th1
   2.561 -  in implies_elim (implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2
   2.562 -     |> mk_meta_eq
   2.563 -  end;
   2.564 -
   2.565 -
   2.566 - fun getname v = case term_of v of 
   2.567 -  Free(s,_) => s
   2.568 - | Var ((s,_),_) => s
   2.569 - | _ => "x"
   2.570 - fun mk_eq s t = Thm.capply (Thm.capply @{cterm "op == :: bool => _"} s) t
   2.571 - fun mkeq s t = Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply @{cterm "op = :: bool => _"} s) t)
   2.572 - fun mk_exists v th = arg_cong_rule (ext (ctyp_of_term v))
   2.573 -   (Thm.abstract_rule (getname v) v th)
   2.574 - val simp_ex_conv = 
   2.575 -     Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms(39)})
   2.576 -
   2.577 -fun frees t = Thm.add_cterm_frees t [];
   2.578 -fun free_in v t = member op aconvc (frees t) v;
   2.579 -
   2.580 -val vsubst = let
   2.581 - fun vsubst (t,v) tm =  
   2.582 -   (Thm.rhs_of o Thm.beta_conversion false) (Thm.capply (Thm.cabs v tm) t)
   2.583 -in fold vsubst end;
   2.584 -
   2.585 -
   2.586 -(** main **)
   2.587 -
   2.588 -fun ring_and_ideal_conv
   2.589 -  {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
   2.590 -   field = (f_ops, f_rules), idom, ideal}
   2.591 -  dest_const mk_const ring_eq_conv ring_normalize_conv =
   2.592 -let
   2.593 -  val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
   2.594 -  val [ring_add_tm, ring_mul_tm, ring_pow_tm] =
   2.595 -    map dest_fun2 [add_pat, mul_pat, pow_pat];
   2.596 -
   2.597 -  val (ring_sub_tm, ring_neg_tm) =
   2.598 -    (case r_ops of
   2.599 -     [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat)
   2.600 -    |_  => (@{cterm "True"}, @{cterm "True"}));
   2.601 -
   2.602 -  val (field_div_tm, field_inv_tm) =
   2.603 -    (case f_ops of
   2.604 -       [div_pat, inv_pat] => (dest_fun2 div_pat, dest_fun inv_pat)
   2.605 -     | _ => (@{cterm "True"}, @{cterm "True"}));
   2.606 -
   2.607 -  val [idom_thm, neq_thm] = idom;
   2.608 -  val [idl_sub, idl_add0] = 
   2.609 -     if length ideal = 2 then ideal else [eq_commute, eq_commute]
   2.610 -  fun ring_dest_neg t =
   2.611 -    let val (l,r) = dest_comb t 
   2.612 -    in if Term.could_unify(term_of l,term_of ring_neg_tm) then r 
   2.613 -       else raise CTERM ("ring_dest_neg", [t])
   2.614 -    end
   2.615 -
   2.616 - val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
   2.617 - fun field_dest_inv t =
   2.618 -    let val (l,r) = dest_comb t in
   2.619 -        if Term.could_unify(term_of l, term_of field_inv_tm) then r 
   2.620 -        else raise CTERM ("field_dest_inv", [t])
   2.621 -    end
   2.622 - val ring_dest_add = dest_binary ring_add_tm;
   2.623 - val ring_mk_add = mk_binop ring_add_tm;
   2.624 - val ring_dest_sub = dest_binary ring_sub_tm;
   2.625 - val ring_mk_sub = mk_binop ring_sub_tm;
   2.626 - val ring_dest_mul = dest_binary ring_mul_tm;
   2.627 - val ring_mk_mul = mk_binop ring_mul_tm;
   2.628 - val field_dest_div = dest_binary field_div_tm;
   2.629 - val field_mk_div = mk_binop field_div_tm;
   2.630 - val ring_dest_pow = dest_binary ring_pow_tm;
   2.631 - val ring_mk_pow = mk_binop ring_pow_tm ;
   2.632 - fun grobvars tm acc =
   2.633 -    if can dest_const tm then acc
   2.634 -    else if can ring_dest_neg tm then grobvars (dest_arg tm) acc
   2.635 -    else if can ring_dest_pow tm then grobvars (dest_arg1 tm) acc
   2.636 -    else if can ring_dest_add tm orelse can ring_dest_sub tm
   2.637 -            orelse can ring_dest_mul tm
   2.638 -    then grobvars (dest_arg1 tm) (grobvars (dest_arg tm) acc)
   2.639 -    else if can field_dest_inv tm
   2.640 -         then
   2.641 -          let val gvs = grobvars (dest_arg tm) [] 
   2.642 -          in if null gvs then acc else tm::acc
   2.643 -          end
   2.644 -    else if can field_dest_div tm then
   2.645 -         let val lvs = grobvars (dest_arg1 tm) acc
   2.646 -             val gvs = grobvars (dest_arg tm) []
   2.647 -          in if null gvs then lvs else tm::acc
   2.648 -          end 
   2.649 -    else tm::acc ;
   2.650 -
   2.651 -fun grobify_term vars tm =
   2.652 -((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
   2.653 -     [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
   2.654 -handle  CTERM _ =>
   2.655 - ((let val x = dest_const tm
   2.656 - in if x =/ rat_0 then [] else [(x,map (fn v => 0) vars)]
   2.657 - end)
   2.658 - handle ERROR _ =>
   2.659 -  ((grob_neg(grobify_term vars (ring_dest_neg tm)))
   2.660 -  handle CTERM _ =>
   2.661 -   (
   2.662 -   (grob_inv(grobify_term vars (field_dest_inv tm)))
   2.663 -   handle CTERM _ => 
   2.664 -    ((let val (l,r) = ring_dest_add tm
   2.665 -    in grob_add (grobify_term vars l) (grobify_term vars r)
   2.666 -    end)
   2.667 -    handle CTERM _ =>
   2.668 -     ((let val (l,r) = ring_dest_sub tm
   2.669 -     in grob_sub (grobify_term vars l) (grobify_term vars r)
   2.670 -     end)
   2.671 -     handle  CTERM _ =>
   2.672 -      ((let val (l,r) = ring_dest_mul tm
   2.673 -      in grob_mul (grobify_term vars l) (grobify_term vars r)
   2.674 -      end)
   2.675 -       handle CTERM _ =>
   2.676 -        (  (let val (l,r) = field_dest_div tm
   2.677 -          in grob_div (grobify_term vars l) (grobify_term vars r)
   2.678 -          end)
   2.679 -         handle CTERM _ =>
   2.680 -          ((let val (l,r) = ring_dest_pow tm
   2.681 -          in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r)
   2.682 -          end)
   2.683 -           handle CTERM _ => error "grobify_term: unknown or invalid term")))))))));
   2.684 -val eq_tm = idom_thm |> concl |> dest_arg |> dest_arg |> dest_fun2;
   2.685 -val dest_eq = dest_binary eq_tm;
   2.686 -
   2.687 -fun grobify_equation vars tm =
   2.688 -    let val (l,r) = dest_binary eq_tm tm
   2.689 -    in grob_sub (grobify_term vars l) (grobify_term vars r)
   2.690 -    end;
   2.691 -
   2.692 -fun grobify_equations tm =
   2.693 - let
   2.694 -  val cjs = conjs tm
   2.695 -  val  rawvars = fold_rev (fn eq => fn a =>
   2.696 -                                       grobvars (dest_arg1 eq) (grobvars (dest_arg eq) a)) cjs []
   2.697 -  val vars = sort (fn (x, y) => Term_Ord.term_ord(term_of x,term_of y))
   2.698 -                  (distinct (op aconvc) rawvars)
   2.699 - in (vars,map (grobify_equation vars) cjs)
   2.700 - end;
   2.701 -
   2.702 -val holify_polynomial =
   2.703 - let fun holify_varpow (v,n) =
   2.704 -  if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n)  (* FIXME *)
   2.705 - fun holify_monomial vars (c,m) =
   2.706 -  let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
   2.707 -   in end_itlist ring_mk_mul (mk_const c :: xps)
   2.708 -  end
   2.709 - fun holify_polynomial vars p =
   2.710 -     if null p then mk_const (rat_0)
   2.711 -     else end_itlist ring_mk_add (map (holify_monomial vars) p)
   2.712 - in holify_polynomial
   2.713 - end ;
   2.714 -val idom_rule = simplify (HOL_basic_ss addsimps [idom_thm]);
   2.715 -fun prove_nz n = eqF_elim
   2.716 -                 (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0))));
   2.717 -val neq_01 = prove_nz (rat_1);
   2.718 -fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
   2.719 -fun mk_add th1 = combination(arg_cong_rule ring_add_tm th1);
   2.720 -
   2.721 -fun refute tm =
   2.722 - if tm aconvc false_tm then assume_Trueprop tm else
   2.723 - ((let
   2.724 -   val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm))
   2.725 -   val  nths = filter (is_eq o dest_arg o concl) nths0
   2.726 -   val eths = filter (is_eq o concl) eths0
   2.727 -  in
   2.728 -   if null eths then
   2.729 -    let
   2.730 -      val th1 = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths
   2.731 -      val th2 = Conv.fconv_rule
   2.732 -                ((arg_conv #> arg_conv)
   2.733 -                     (binop_conv ring_normalize_conv)) th1
   2.734 -      val conc = th2 |> concl |> dest_arg
   2.735 -      val (l,r) = conc |> dest_eq
   2.736 -    in implies_intr (mk_comb cTrp tm)
   2.737 -                    (equal_elim (arg_cong_rule cTrp (eqF_intr th2))
   2.738 -                           (reflexive l |> mk_object_eq))
   2.739 -    end
   2.740 -   else
   2.741 -   let
   2.742 -    val (vars,l,cert,noteqth) =(
   2.743 -     if null nths then
   2.744 -      let val (vars,pols) = grobify_equations(list_mk_conj(map concl eths))
   2.745 -          val (l,cert) = grobner_weak vars pols
   2.746 -      in (vars,l,cert,neq_01)
   2.747 -      end
   2.748 -     else
   2.749 -      let
   2.750 -       val nth = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths
   2.751 -       val (vars,pol::pols) =
   2.752 -          grobify_equations(list_mk_conj(dest_arg(concl nth)::map concl eths))
   2.753 -       val (deg,l,cert) = grobner_strong vars pols pol
   2.754 -       val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth
   2.755 -       val th2 = funpow deg (idom_rule o HOLogic.conj_intr th1) neq_01
   2.756 -      in (vars,l,cert,th2)
   2.757 -      end)
   2.758 -    val cert_pos = map (fn (i,p) => (i,filter (fn (c,m) => c >/ rat_0) p)) cert
   2.759 -    val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
   2.760 -                                            (filter (fn (c,m) => c </ rat_0) p))) cert
   2.761 -    val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
   2.762 -    val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
   2.763 -    fun thm_fn pols =
   2.764 -        if null pols then reflexive(mk_const rat_0) else
   2.765 -        end_itlist mk_add
   2.766 -            (map (fn (i,p) => arg_cong_rule (mk_comb ring_mul_tm p)
   2.767 -              (nth eths i |> mk_meta_eq)) pols)
   2.768 -    val th1 = thm_fn herts_pos
   2.769 -    val th2 = thm_fn herts_neg
   2.770 -    val th3 = HOLogic.conj_intr(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth
   2.771 -    val th4 = Conv.fconv_rule ((arg_conv o arg_conv o binop_conv) ring_normalize_conv)
   2.772 -                               (neq_rule l th3)
   2.773 -    val (l,r) = dest_eq(dest_arg(concl th4))
   2.774 -   in implies_intr (mk_comb cTrp tm)
   2.775 -                        (equal_elim (arg_cong_rule cTrp (eqF_intr th4))
   2.776 -                   (reflexive l |> mk_object_eq))
   2.777 -   end
   2.778 -  end) handle ERROR _ => raise CTERM ("Gorbner-refute: unable to refute",[tm]))
   2.779 -
   2.780 -fun ring tm =
   2.781 - let
   2.782 -  fun mk_forall x p =
   2.783 -      mk_comb (cterm_rule (instantiate' [SOME (ctyp_of_term x)] []) @{cpat "All:: (?'a => bool) => _"}) (cabs x p)
   2.784 -  val avs = add_cterm_frees tm []
   2.785 -  val P' = fold mk_forall avs tm
   2.786 -  val th1 = initial_conv(mk_neg P')
   2.787 -  val (evs,bod) = strip_exists(concl th1) in
   2.788 -   if is_forall bod then raise CTERM("ring: non-universal formula",[tm])
   2.789 -   else
   2.790 -   let
   2.791 -    val th1a = weak_dnf_conv bod
   2.792 -    val boda = concl th1a
   2.793 -    val th2a = refute_disj refute boda
   2.794 -    val th2b = [mk_object_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans
   2.795 -    val th2 = fold (fn v => fn th => (forall_intr v th) COMP allI) evs (th2b RS PFalse)
   2.796 -    val th3 = equal_elim
   2.797 -                (Simplifier.rewrite (HOL_basic_ss addsimps [not_ex RS sym])
   2.798 -                          (th2 |> cprop_of)) th2
   2.799 -    in specl avs
   2.800 -             ([[[mk_object_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD)
   2.801 -   end
   2.802 - end
   2.803 -fun ideal tms tm ord =
   2.804 - let
   2.805 -  val rawvars = fold_rev grobvars (tm::tms) []
   2.806 -  val vars = sort ord (distinct (fn (x,y) => (term_of x) aconv (term_of y)) rawvars)
   2.807 -  val pols = map (grobify_term vars) tms
   2.808 -  val pol = grobify_term vars tm
   2.809 -  val cert = grobner_ideal vars pols pol
   2.810 - in map_range (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
   2.811 -   (length pols)
   2.812 - end
   2.813 -
   2.814 -fun poly_eq_conv t = 
   2.815 - let val (a,b) = Thm.dest_binop t
   2.816 - in fconv_rule (arg_conv (arg1_conv ring_normalize_conv)) 
   2.817 -     (instantiate' [] [SOME a, SOME b] idl_sub)
   2.818 - end
   2.819 - val poly_eq_simproc = 
   2.820 -  let 
   2.821 -   fun proc phi  ss t = 
   2.822 -    let val th = poly_eq_conv t
   2.823 -    in if Thm.is_reflexive th then NONE else SOME th
   2.824 -    end
   2.825 -   in make_simproc {lhss = [Thm.lhs_of idl_sub], 
   2.826 -                name = "poly_eq_simproc", proc = proc, identifier = []}
   2.827 -   end;
   2.828 -  val poly_eq_ss = HOL_basic_ss addsimps @{thms simp_thms}
   2.829 -                        addsimprocs [poly_eq_simproc]
   2.830 -
   2.831 - local
   2.832 -  fun is_defined v t =
   2.833 -  let 
   2.834 -   val mons = striplist(dest_binary ring_add_tm) t 
   2.835 -  in member (op aconvc) mons v andalso 
   2.836 -    forall (fn m => v aconvc m 
   2.837 -          orelse not(member (op aconvc) (Thm.add_cterm_frees m []) v)) mons
   2.838 -  end
   2.839 -
   2.840 -  fun isolate_variable vars tm =
   2.841 -  let 
   2.842 -   val th = poly_eq_conv tm
   2.843 -   val th' = (sym_conv then_conv poly_eq_conv) tm
   2.844 -   val (v,th1) = 
   2.845 -   case find_first(fn v=> is_defined v (Thm.dest_arg1 (Thm.rhs_of th))) vars of
   2.846 -    SOME v => (v,th')
   2.847 -   | NONE => (the (find_first 
   2.848 -          (fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th)
   2.849 -   val th2 = transitive th1 
   2.850 -        (instantiate' []  [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v] 
   2.851 -          idl_add0)
   2.852 -   in fconv_rule(funpow 2 arg_conv ring_normalize_conv) th2
   2.853 -   end
   2.854 - in
   2.855 - fun unwind_polys_conv tm =
   2.856 - let 
   2.857 -  val (vars,bod) = strip_exists tm
   2.858 -  val cjs = striplist (dest_binary @{cterm "op &"}) bod
   2.859 -  val th1 = (the (get_first (try (isolate_variable vars)) cjs) 
   2.860 -             handle Option => raise CTERM ("unwind_polys_conv",[tm]))
   2.861 -  val eq = Thm.lhs_of th1
   2.862 -  val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs))
   2.863 -  val th2 = conj_ac_rule (mk_eq bod bod')
   2.864 -  val th3 = transitive th2 
   2.865 -         (Drule.binop_cong_rule @{cterm "op &"} th1 
   2.866 -                (reflexive (Thm.dest_arg (Thm.rhs_of th2))))
   2.867 -  val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
   2.868 -  val vars' = (remove op aconvc v vars) @ [v]
   2.869 -  val th4 = fconv_rule (arg_conv simp_ex_conv) (mk_exists v th3)
   2.870 -  val th5 = ex_eq_conv (mk_eq tm (fold mk_ex (remove op aconvc v vars) (Thm.lhs_of th4)))
   2.871 - in transitive th5 (fold mk_exists (remove op aconvc v vars) th4)
   2.872 - end;
   2.873 -end
   2.874 -
   2.875 -local
   2.876 - fun scrub_var v m =
   2.877 -  let 
   2.878 -   val ps = striplist ring_dest_mul m 
   2.879 -   val ps' = remove op aconvc v ps
   2.880 -  in if null ps' then one_tm else fold1 ring_mk_mul ps'
   2.881 -  end
   2.882 - fun find_multipliers v mons =
   2.883 -  let 
   2.884 -   val mons1 = filter (fn m => free_in v m) mons 
   2.885 -   val mons2 = map (scrub_var v) mons1 
   2.886 -   in  if null mons2 then zero_tm else fold1 ring_mk_add mons2
   2.887 -  end
   2.888 -
   2.889 - fun isolate_monomials vars tm =
   2.890 - let 
   2.891 -  val (cmons,vmons) =
   2.892 -    List.partition (fn m => null (inter (op aconvc) vars (frees m)))
   2.893 -                   (striplist ring_dest_add tm)
   2.894 -  val cofactors = map (fn v => find_multipliers v vmons) vars
   2.895 -  val cnc = if null cmons then zero_tm
   2.896 -             else Thm.capply ring_neg_tm
   2.897 -                    (list_mk_binop ring_add_tm cmons) 
   2.898 -  in (cofactors,cnc)
   2.899 -  end;
   2.900 -
   2.901 -fun isolate_variables evs ps eq =
   2.902 - let 
   2.903 -  val vars = filter (fn v => free_in v eq) evs
   2.904 -  val (qs,p) = isolate_monomials vars eq
   2.905 -  val rs = ideal (qs @ ps) p 
   2.906 -              (fn (s,t) => Term_Ord.term_ord (term_of s, term_of t))
   2.907 - in (eq, take (length qs) rs ~~ vars)
   2.908 - end;
   2.909 - fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
   2.910 -in
   2.911 - fun solve_idealism evs ps eqs =
   2.912 -  if null evs then [] else
   2.913 -  let 
   2.914 -   val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> the
   2.915 -   val evs' = subtract op aconvc evs (map snd cfs)
   2.916 -   val eqs' = map (subst_in_poly cfs) (remove op aconvc eq eqs)
   2.917 -  in cfs @ solve_idealism evs' ps eqs'
   2.918 -  end;
   2.919 -end;
   2.920 -
   2.921 -
   2.922 -in {ring_conv = ring, simple_ideal = ideal, multi_ideal = solve_idealism, 
   2.923 -    poly_eq_ss = poly_eq_ss, unwind_conv = unwind_polys_conv}
   2.924 -end;
   2.925 -
   2.926 -
   2.927 -fun find_term bounds tm =
   2.928 -  (case term_of tm of
   2.929 -    Const ("op =", T) $ _ $ _ =>
   2.930 -      if domain_type T = HOLogic.boolT then find_args bounds tm
   2.931 -      else dest_arg tm
   2.932 -  | Const ("Not", _) $ _ => find_term bounds (dest_arg tm)
   2.933 -  | Const ("All", _) $ _ => find_body bounds (dest_arg tm)
   2.934 -  | Const ("Ex", _) $ _ => find_body bounds (dest_arg tm)
   2.935 -  | Const ("op &", _) $ _ $ _ => find_args bounds tm
   2.936 -  | Const ("op |", _) $ _ $ _ => find_args bounds tm
   2.937 -  | Const ("op -->", _) $ _ $ _ => find_args bounds tm
   2.938 -  | @{term "op ==>"} $_$_ => find_args bounds tm
   2.939 -  | Const("op ==",_)$_$_ => find_args bounds tm
   2.940 -  | @{term Trueprop}$_ => find_term bounds (dest_arg tm)
   2.941 -  | _ => raise TERM ("find_term", []))
   2.942 -and find_args bounds tm =
   2.943 -  let val (t, u) = Thm.dest_binop tm
   2.944 -  in (find_term bounds t handle TERM _ => find_term bounds u) end
   2.945 -and find_body bounds b =
   2.946 -  let val (_, b') = dest_abs (SOME (Name.bound bounds)) b
   2.947 -  in find_term (bounds + 1) b' end;
   2.948 -
   2.949 -
   2.950 -fun get_ring_ideal_convs ctxt form = 
   2.951 - case try (find_term 0) form of
   2.952 -  NONE => NONE
   2.953 -| SOME tm =>
   2.954 -  (case Normalizer.match ctxt tm of
   2.955 -    NONE => NONE
   2.956 -  | SOME (res as (theory, {is_const, dest_const, 
   2.957 -          mk_const, conv = ring_eq_conv})) =>
   2.958 -     SOME (ring_and_ideal_conv theory
   2.959 -          dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
   2.960 -          (Normalizer.semiring_normalize_wrapper ctxt res)))
   2.961 -
   2.962 -fun ring_solve ctxt form =
   2.963 -  (case try (find_term 0 (* FIXME !? *)) form of
   2.964 -    NONE => reflexive form
   2.965 -  | SOME tm =>
   2.966 -      (case Normalizer.match ctxt tm of
   2.967 -        NONE => reflexive form
   2.968 -      | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) =>
   2.969 -        #ring_conv (ring_and_ideal_conv theory
   2.970 -          dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
   2.971 -          (Normalizer.semiring_normalize_wrapper ctxt res)) form));
   2.972 -
   2.973 -fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (Simplifier.context ctxt
   2.974 -  (HOL_basic_ss addsimps (Algebra_Simplification.get ctxt) delsimps del_thms addsimps add_thms));
   2.975 -
   2.976 -fun ring_tac add_ths del_ths ctxt =
   2.977 -  Object_Logic.full_atomize_tac
   2.978 -  THEN' presimplify ctxt add_ths del_ths
   2.979 -  THEN' CSUBGOAL (fn (p, i) =>
   2.980 -    rtac (let val form = Object_Logic.dest_judgment p
   2.981 -          in case get_ring_ideal_convs ctxt form of
   2.982 -           NONE => reflexive form
   2.983 -          | SOME thy => #ring_conv thy form
   2.984 -          end) i
   2.985 -      handle TERM _ => no_tac
   2.986 -        | CTERM _ => no_tac
   2.987 -        | THM _ => no_tac);
   2.988 -
   2.989 -local
   2.990 - fun lhs t = case term_of t of
   2.991 -  Const("op =",_)$_$_ => Thm.dest_arg1 t
   2.992 - | _=> raise CTERM ("ideal_tac - lhs",[t])
   2.993 - fun exitac NONE = no_tac
   2.994 -   | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
   2.995 -in 
   2.996 -fun ideal_tac add_ths del_ths ctxt = 
   2.997 -  presimplify ctxt add_ths del_ths
   2.998 - THEN'
   2.999 - CSUBGOAL (fn (p, i) =>
  2.1000 -  case get_ring_ideal_convs ctxt p of
  2.1001 -   NONE => no_tac
  2.1002 - | SOME thy => 
  2.1003 -  let
  2.1004 -   fun poly_exists_tac {asms = asms, concl = concl, prems = prems,
  2.1005 -            params = params, context = ctxt, schematics = scs} = 
  2.1006 -    let
  2.1007 -     val (evs,bod) = strip_exists (Thm.dest_arg concl)
  2.1008 -     val ps = map_filter (try (lhs o Thm.dest_arg)) asms 
  2.1009 -     val cfs = (map swap o #multi_ideal thy evs ps) 
  2.1010 -                   (map Thm.dest_arg1 (conjuncts bod))
  2.1011 -     val ws = map (exitac o AList.lookup op aconvc cfs) evs
  2.1012 -    in EVERY (rev ws) THEN Method.insert_tac prems 1 
  2.1013 -        THEN ring_tac add_ths del_ths ctxt 1
  2.1014 -   end
  2.1015 -  in  
  2.1016 -     clarify_tac @{claset} i 
  2.1017 -     THEN Object_Logic.full_atomize_tac i 
  2.1018 -     THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i 
  2.1019 -     THEN clarify_tac @{claset} i 
  2.1020 -     THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
  2.1021 -     THEN SUBPROOF poly_exists_tac ctxt i
  2.1022 -  end
  2.1023 - handle TERM _ => no_tac
  2.1024 -     | CTERM _ => no_tac
  2.1025 -     | THM _ => no_tac); 
  2.1026 -end;
  2.1027 -
  2.1028 -fun algebra_tac add_ths del_ths ctxt i = 
  2.1029 - ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i
  2.1030 - 
  2.1031 -local
  2.1032 -
  2.1033 -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
  2.1034 -val addN = "add"
  2.1035 -val delN = "del"
  2.1036 -val any_keyword = keyword addN || keyword delN
  2.1037 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
  2.1038 -
  2.1039 -in
  2.1040 -
  2.1041 -val algebra_method = ((Scan.optional (keyword addN |-- thms) []) -- 
  2.1042 -   (Scan.optional (keyword delN |-- thms) [])) >>
  2.1043 -  (fn (add_ths, del_ths) => fn ctxt =>
  2.1044 -       SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt))
  2.1045 -
  2.1046 -end;
  2.1047 -
  2.1048 -end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/groebner.ML	Fri May 07 16:12:25 2010 +0200
     3.3 @@ -0,0 +1,1045 @@
     3.4 +(*  Title:      HOL/Tools/Groebner_Basis/groebner.ML
     3.5 +    Author:     Amine Chaieb, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +signature GROEBNER =
     3.9 +sig
    3.10 +  val ring_and_ideal_conv :
    3.11 +    {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list,
    3.12 +     vars: cterm list, semiring: cterm list * thm list, ideal : thm list} ->
    3.13 +    (cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
    3.14 +    conv ->  conv ->
    3.15 +     {ring_conv : conv, 
    3.16 +     simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list),
    3.17 +     multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list,
    3.18 +     poly_eq_ss: simpset, unwind_conv : conv}
    3.19 +  val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
    3.20 +  val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
    3.21 +  val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
    3.22 +  val algebra_method: (Proof.context -> Method.method) context_parser
    3.23 +end
    3.24 +
    3.25 +structure Groebner : GROEBNER =
    3.26 +struct
    3.27 +
    3.28 +open Conv Drule Thm;
    3.29 +
    3.30 +fun is_comb ct =
    3.31 +  (case Thm.term_of ct of
    3.32 +    _ $ _ => true
    3.33 +  | _ => false);
    3.34 +
    3.35 +val concl = Thm.cprop_of #> Thm.dest_arg;
    3.36 +
    3.37 +fun is_binop ct ct' =
    3.38 +  (case Thm.term_of ct' of
    3.39 +    c $ _ $ _ => term_of ct aconv c
    3.40 +  | _ => false);
    3.41 +
    3.42 +fun dest_binary ct ct' =
    3.43 +  if is_binop ct ct' then Thm.dest_binop ct'
    3.44 +  else raise CTERM ("dest_binary: bad binop", [ct, ct'])
    3.45 +
    3.46 +fun inst_thm inst = Thm.instantiate ([], inst);
    3.47 +
    3.48 +val rat_0 = Rat.zero;
    3.49 +val rat_1 = Rat.one;
    3.50 +val minus_rat = Rat.neg;
    3.51 +val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
    3.52 +fun int_of_rat a =
    3.53 +    case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int";
    3.54 +val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
    3.55 +
    3.56 +val (eqF_intr, eqF_elim) =
    3.57 +  let val [th1,th2] = @{thms PFalse}
    3.58 +  in (fn th => th COMP th2, fn th => th COMP th1) end;
    3.59 +
    3.60 +val (PFalse, PFalse') =
    3.61 + let val PFalse_eq = nth @{thms simp_thms} 13
    3.62 + in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end;
    3.63 +
    3.64 +
    3.65 +(* Type for recording history, i.e. how a polynomial was obtained. *)
    3.66 +
    3.67 +datatype history =
    3.68 +   Start of int
    3.69 + | Mmul of (Rat.rat * int list) * history
    3.70 + | Add of history * history;
    3.71 +
    3.72 +
    3.73 +(* Monomial ordering. *)
    3.74 +
    3.75 +fun morder_lt m1 m2=
    3.76 +    let fun lexorder l1 l2 =
    3.77 +            case (l1,l2) of
    3.78 +                ([],[]) => false
    3.79 +              | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2
    3.80 +              | _ => error "morder: inconsistent monomial lengths"
    3.81 +        val n1 = Integer.sum m1
    3.82 +        val n2 = Integer.sum m2 in
    3.83 +    n1 < n2 orelse n1 = n2 andalso lexorder m1 m2
    3.84 +    end;
    3.85 +
    3.86 +fun morder_le m1 m2 = morder_lt m1 m2 orelse (m1 = m2);
    3.87 +
    3.88 +fun morder_gt m1 m2 = morder_lt m2 m1;
    3.89 +
    3.90 +(* Arithmetic on canonical polynomials. *)
    3.91 +
    3.92 +fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l;
    3.93 +
    3.94 +fun grob_add l1 l2 =
    3.95 +  case (l1,l2) of
    3.96 +    ([],l2) => l2
    3.97 +  | (l1,[]) => l1
    3.98 +  | ((c1,m1)::o1,(c2,m2)::o2) =>
    3.99 +        if m1 = m2 then
   3.100 +          let val c = c1+/c2 val rest = grob_add o1 o2 in
   3.101 +          if c =/ rat_0 then rest else (c,m1)::rest end
   3.102 +        else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
   3.103 +        else (c2,m2)::(grob_add l1 o2);
   3.104 +
   3.105 +fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
   3.106 +
   3.107 +fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2));
   3.108 +
   3.109 +fun grob_cmul cm pol = map (grob_mmul cm) pol;
   3.110 +
   3.111 +fun grob_mul l1 l2 =
   3.112 +  case l1 of
   3.113 +    [] => []
   3.114 +  | (h1::t1) => grob_add (grob_cmul h1 l2) (grob_mul t1 l2);
   3.115 +
   3.116 +fun grob_inv l =
   3.117 +  case l of
   3.118 +    [(c,vs)] => if (forall (fn x => x = 0) vs) then
   3.119 +                  if (c =/ rat_0) then error "grob_inv: division by zero"
   3.120 +                  else [(rat_1 // c,vs)]
   3.121 +              else error "grob_inv: non-constant divisor polynomial"
   3.122 +  | _ => error "grob_inv: non-constant divisor polynomial";
   3.123 +
   3.124 +fun grob_div l1 l2 =
   3.125 +  case l2 of
   3.126 +    [(c,l)] => if (forall (fn x => x = 0) l) then
   3.127 +                 if c =/ rat_0 then error "grob_div: division by zero"
   3.128 +                 else grob_cmul (rat_1 // c,l) l1
   3.129 +             else error "grob_div: non-constant divisor polynomial"
   3.130 +  | _ => error "grob_div: non-constant divisor polynomial";
   3.131 +
   3.132 +fun grob_pow vars l n =
   3.133 +  if n < 0 then error "grob_pow: negative power"
   3.134 +  else if n = 0 then [(rat_1,map (fn v => 0) vars)]
   3.135 +  else grob_mul l (grob_pow vars l (n - 1));
   3.136 +
   3.137 +fun degree vn p =
   3.138 + case p of
   3.139 +  [] => error "Zero polynomial"
   3.140 +| [(c,ns)] => nth ns vn
   3.141 +| (c,ns)::p' => Int.max (nth ns vn, degree vn p');
   3.142 +
   3.143 +fun head_deg vn p = let val d = degree vn p in
   3.144 + (d,fold (fn (c,r) => fn q => grob_add q [(c, map_index (fn (i,n) => if i = vn then 0 else n) r)]) (filter (fn (c,ns) => c <>/ rat_0 andalso nth ns vn = d) p) []) end;
   3.145 +
   3.146 +val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns);
   3.147 +val grob_pdiv =
   3.148 + let fun pdiv_aux vn (n,a) p k s =
   3.149 +  if is_zerop s then (k,s) else
   3.150 +  let val (m,b) = head_deg vn s
   3.151 +  in if m < n then (k,s) else
   3.152 +     let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0)
   3.153 +                                                (snd (hd s)))]
   3.154 +     in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p')
   3.155 +        else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p'))
   3.156 +     end
   3.157 +  end
   3.158 + in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s
   3.159 + end;
   3.160 +
   3.161 +(* Monomial division operation. *)
   3.162 +
   3.163 +fun mdiv (c1,m1) (c2,m2) =
   3.164 +  (c1//c2,
   3.165 +   map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2);
   3.166 +
   3.167 +(* Lowest common multiple of two monomials. *)
   3.168 +
   3.169 +fun mlcm (c1,m1) (c2,m2) = (rat_1, ListPair.map Int.max (m1, m2));
   3.170 +
   3.171 +(* Reduce monomial cm by polynomial pol, returning replacement for cm.  *)
   3.172 +
   3.173 +fun reduce1 cm (pol,hpol) =
   3.174 +  case pol of
   3.175 +    [] => error "reduce1"
   3.176 +  | cm1::cms => ((let val (c,m) = mdiv cm cm1 in
   3.177 +                    (grob_cmul (minus_rat c,m) cms,
   3.178 +                     Mmul((minus_rat c,m),hpol)) end)
   3.179 +                handle  ERROR _ => error "reduce1");
   3.180 +
   3.181 +(* Try this for all polynomials in a basis.  *)
   3.182 +fun tryfind f l =
   3.183 +    case l of
   3.184 +        [] => error "tryfind"
   3.185 +      | (h::t) => ((f h) handle ERROR _ => tryfind f t);
   3.186 +
   3.187 +fun reduceb cm basis = tryfind (fn p => reduce1 cm p) basis;
   3.188 +
   3.189 +(* Reduction of a polynomial (always picking largest monomial possible).     *)
   3.190 +
   3.191 +fun reduce basis (pol,hist) =
   3.192 +  case pol of
   3.193 +    [] => (pol,hist)
   3.194 +  | cm::ptl => ((let val (q,hnew) = reduceb cm basis in
   3.195 +                   reduce basis (grob_add q ptl,Add(hnew,hist)) end)
   3.196 +               handle (ERROR _) =>
   3.197 +                   (let val (q,hist') = reduce basis (ptl,hist) in
   3.198 +                       (cm::q,hist') end));
   3.199 +
   3.200 +(* Check for orthogonality w.r.t. LCM.                                       *)
   3.201 +
   3.202 +fun orthogonal l p1 p2 =
   3.203 +  snd l = snd(grob_mmul (hd p1) (hd p2));
   3.204 +
   3.205 +(* Compute S-polynomial of two polynomials.                                  *)
   3.206 +
   3.207 +fun spoly cm ph1 ph2 =
   3.208 +  case (ph1,ph2) of
   3.209 +    (([],h),p) => ([],h)
   3.210 +  | (p,([],h)) => ([],h)
   3.211 +  | ((cm1::ptl1,his1),(cm2::ptl2,his2)) =>
   3.212 +        (grob_sub (grob_cmul (mdiv cm cm1) ptl1)
   3.213 +                  (grob_cmul (mdiv cm cm2) ptl2),
   3.214 +         Add(Mmul(mdiv cm cm1,his1),
   3.215 +             Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2)));
   3.216 +
   3.217 +(* Make a polynomial monic.                                                  *)
   3.218 +
   3.219 +fun monic (pol,hist) =
   3.220 +  if null pol then (pol,hist) else
   3.221 +  let val (c',m') = hd pol in
   3.222 +  (map (fn (c,m) => (c//c',m)) pol,
   3.223 +   Mmul((rat_1 // c',map (K 0) m'),hist)) end;
   3.224 +
   3.225 +(* The most popular heuristic is to order critical pairs by LCM monomial.    *)
   3.226 +
   3.227 +fun forder ((c1,m1),_) ((c2,m2),_) = morder_lt m1 m2;
   3.228 +
   3.229 +fun poly_lt  p q =
   3.230 +  case (p,q) of
   3.231 +    (p,[]) => false
   3.232 +  | ([],q) => true
   3.233 +  | ((c1,m1)::o1,(c2,m2)::o2) =>
   3.234 +        c1 </ c2 orelse
   3.235 +        c1 =/ c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
   3.236 +
   3.237 +fun align  ((p,hp),(q,hq)) =
   3.238 +  if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
   3.239 +fun forall2 p l1 l2 =
   3.240 +  case (l1,l2) of
   3.241 +    ([],[]) => true
   3.242 +  | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
   3.243 +  | _ => false;
   3.244 +
   3.245 +fun poly_eq p1 p2 =
   3.246 +  forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2;
   3.247 +
   3.248 +fun memx ((p1,h1),(p2,h2)) ppairs =
   3.249 +  not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
   3.250 +
   3.251 +(* Buchberger's second criterion.                                            *)
   3.252 +
   3.253 +fun criterion2 basis (lcm,((p1,h1),(p2,h2))) opairs =
   3.254 +  exists (fn g => not(poly_eq (fst g) p1) andalso not(poly_eq (fst g) p2) andalso
   3.255 +                   can (mdiv lcm) (hd(fst g)) andalso
   3.256 +                   not(memx (align (g,(p1,h1))) (map snd opairs)) andalso
   3.257 +                   not(memx (align (g,(p2,h2))) (map snd opairs))) basis;
   3.258 +
   3.259 +(* Test for hitting constant polynomial.                                     *)
   3.260 +
   3.261 +fun constant_poly p =
   3.262 +  length p = 1 andalso forall (fn x => x = 0) (snd(hd p));
   3.263 +
   3.264 +(* Grobner basis algorithm.                                                  *)
   3.265 +
   3.266 +(* FIXME: try to get rid of mergesort? *)
   3.267 +fun merge ord l1 l2 =
   3.268 + case l1 of
   3.269 +  [] => l2
   3.270 + | h1::t1 =>
   3.271 +   case l2 of
   3.272 +    [] => l1
   3.273 +   | h2::t2 => if ord h1 h2 then h1::(merge ord t1 l2)
   3.274 +               else h2::(merge ord l1 t2);
   3.275 +fun mergesort ord l =
   3.276 + let
   3.277 + fun mergepairs l1 l2 =
   3.278 +  case (l1,l2) of
   3.279 +   ([s],[]) => s
   3.280 + | (l,[]) => mergepairs [] l
   3.281 + | (l,[s1]) => mergepairs (s1::l) []
   3.282 + | (l,(s1::s2::ss)) => mergepairs ((merge ord s1 s2)::l) ss
   3.283 + in if null l  then []  else mergepairs [] (map (fn x => [x]) l)
   3.284 + end;
   3.285 +
   3.286 +
   3.287 +fun grobner_basis basis pairs =
   3.288 + case pairs of
   3.289 +   [] => basis
   3.290 + | (l,(p1,p2))::opairs =>
   3.291 +   let val (sph as (sp,hist)) = monic (reduce basis (spoly l p1 p2))
   3.292 +   in 
   3.293 +    if null sp orelse criterion2 basis (l,(p1,p2)) opairs
   3.294 +    then grobner_basis basis opairs
   3.295 +    else if constant_poly sp then grobner_basis (sph::basis) []
   3.296 +    else 
   3.297 +     let 
   3.298 +      val rawcps = map (fn p => (mlcm (hd(fst p)) (hd sp),align(p,sph)))
   3.299 +                              basis
   3.300 +      val newcps = filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q)))
   3.301 +                        rawcps
   3.302 +     in grobner_basis (sph::basis)
   3.303 +                 (merge forder opairs (mergesort forder newcps))
   3.304 +     end
   3.305 +   end;
   3.306 +
   3.307 +(* Interreduce initial polynomials.                                          *)
   3.308 +
   3.309 +fun grobner_interreduce rpols ipols =
   3.310 +  case ipols of
   3.311 +    [] => map monic (rev rpols)
   3.312 +  | p::ps => let val p' = reduce (rpols @ ps) p in
   3.313 +             if null (fst p') then grobner_interreduce rpols ps
   3.314 +             else grobner_interreduce (p'::rpols) ps end;
   3.315 +
   3.316 +(* Overall function.                                                         *)
   3.317 +
   3.318 +fun grobner pols =
   3.319 +    let val npols = map_index (fn (n, p) => (p, Start n)) pols
   3.320 +        val phists = filter (fn (p,_) => not (null p)) npols
   3.321 +        val bas = grobner_interreduce [] (map monic phists)
   3.322 +        val prs0 = map_product pair bas bas
   3.323 +        val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0
   3.324 +        val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1
   3.325 +        val prs3 =
   3.326 +            filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) prs2 in
   3.327 +        grobner_basis bas (mergesort forder prs3) end;
   3.328 +
   3.329 +(* Get proof of contradiction from Grobner basis.                            *)
   3.330 +
   3.331 +fun find p l =
   3.332 +  case l of
   3.333 +      [] => error "find"
   3.334 +    | (h::t) => if p(h) then h else find p t;
   3.335 +
   3.336 +fun grobner_refute pols =
   3.337 +  let val gb = grobner pols in
   3.338 +  snd(find (fn (p,h) => length p = 1 andalso forall (fn x=> x=0) (snd(hd p))) gb)
   3.339 +  end;
   3.340 +
   3.341 +(* Turn proof into a certificate as sum of multipliers.                      *)
   3.342 +(* In principle this is very inefficient: in a heavily shared proof it may   *)
   3.343 +(* make the same calculation many times. Could put in a cache or something.  *)
   3.344 +
   3.345 +fun resolve_proof vars prf =
   3.346 +  case prf of
   3.347 +    Start(~1) => []
   3.348 +  | Start m => [(m,[(rat_1,map (K 0) vars)])]
   3.349 +  | Mmul(pol,lin) =>
   3.350 +        let val lis = resolve_proof vars lin in
   3.351 +            map (fn (n,p) => (n,grob_cmul pol p)) lis end
   3.352 +  | Add(lin1,lin2) =>
   3.353 +        let val lis1 = resolve_proof vars lin1
   3.354 +            val lis2 = resolve_proof vars lin2
   3.355 +            val dom = distinct (op =) (union (op =) (map fst lis1) (map fst lis2))
   3.356 +        in
   3.357 +            map (fn n => let val a = these (AList.lookup (op =) lis1 n)
   3.358 +                             val b = these (AList.lookup (op =) lis2 n)
   3.359 +                         in (n,grob_add a b) end) dom end;
   3.360 +
   3.361 +(* Run the procedure and produce Weak Nullstellensatz certificate.           *)
   3.362 +
   3.363 +fun grobner_weak vars pols =
   3.364 +    let val cert = resolve_proof vars (grobner_refute pols)
   3.365 +        val l =
   3.366 +            fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
   3.367 +        (l,map (fn (i,p) => (i,map (fn (d,m) => (l*/d,m)) p)) cert) end;
   3.368 +
   3.369 +(* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)
   3.370 +
   3.371 +fun grobner_ideal vars pols pol =
   3.372 +  let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in
   3.373 +  if not (null pol') then error "grobner_ideal: not in the ideal" else
   3.374 +  resolve_proof vars h end;
   3.375 +
   3.376 +(* Produce Strong Nullstellensatz certificate for a power of pol.            *)
   3.377 +
   3.378 +fun grobner_strong vars pols pol =
   3.379 +    let val vars' = @{cterm "True"}::vars
   3.380 +        val grob_z = [(rat_1,1::(map (fn x => 0) vars))]
   3.381 +        val grob_1 = [(rat_1,(map (fn x => 0) vars'))]
   3.382 +        fun augment p= map (fn (c,m) => (c,0::m)) p
   3.383 +        val pols' = map augment pols
   3.384 +        val pol' = augment pol
   3.385 +        val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols'
   3.386 +        val (l,cert) = grobner_weak vars' allpols
   3.387 +        val d = fold (fold (Integer.max o hd o snd) o snd) cert 0
   3.388 +        fun transform_monomial (c,m) =
   3.389 +            grob_cmul (c,tl m) (grob_pow vars pol (d - hd m))
   3.390 +        fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q []
   3.391 +        val cert' = map (fn (c,q) => (c-1,transform_polynomial q))
   3.392 +                        (filter (fn (k,_) => k <> 0) cert) in
   3.393 +        (d,l,cert') end;
   3.394 +
   3.395 +
   3.396 +(* Overall parametrized universal procedure for (semi)rings.                 *)
   3.397 +(* We return an ideal_conv and the actual ring prover.                       *)
   3.398 +
   3.399 +fun refute_disj rfn tm =
   3.400 + case term_of tm of
   3.401 +  Const("op |",_)$l$r =>
   3.402 +   compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
   3.403 +  | _ => rfn tm ;
   3.404 +
   3.405 +val notnotD = @{thm notnotD};
   3.406 +fun mk_binop ct x y = capply (capply ct x) y
   3.407 +
   3.408 +val mk_comb = capply;
   3.409 +fun is_neg t =
   3.410 +    case term_of t of
   3.411 +      (Const("Not",_)$p) => true
   3.412 +    | _  => false;
   3.413 +fun is_eq t =
   3.414 + case term_of t of
   3.415 + (Const("op =",_)$_$_) => true
   3.416 +| _  => false;
   3.417 +
   3.418 +fun end_itlist f l =
   3.419 +  case l of
   3.420 +        []     => error "end_itlist"
   3.421 +      | [x]    => x
   3.422 +      | (h::t) => f h (end_itlist f t);
   3.423 +
   3.424 +val list_mk_binop = fn b => end_itlist (mk_binop b);
   3.425 +
   3.426 +val list_dest_binop = fn b =>
   3.427 + let fun h acc t =
   3.428 +  ((let val (l,r) = dest_binary b t in h (h acc r) l end)
   3.429 +   handle CTERM _ => (t::acc)) (* Why had I handle _ => ? *)
   3.430 + in h []
   3.431 + end;
   3.432 +
   3.433 +val strip_exists =
   3.434 + let fun h (acc, t) =
   3.435 +      case (term_of t) of
   3.436 +       Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
   3.437 +     | _ => (acc,t)
   3.438 + in fn t => h ([],t)
   3.439 + end;
   3.440 +
   3.441 +fun is_forall t =
   3.442 + case term_of t of
   3.443 +  (Const("All",_)$Abs(_,_,_)) => true
   3.444 +| _ => false;
   3.445 +
   3.446 +val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
   3.447 +val bool_simps = @{thms bool_simps};
   3.448 +val nnf_simps = @{thms nnf_simps};
   3.449 +val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps bool_simps addsimps nnf_simps)
   3.450 +val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms weak_dnf_simps});
   3.451 +val initial_conv =
   3.452 +    Simplifier.rewrite
   3.453 +     (HOL_basic_ss addsimps nnf_simps
   3.454 +       addsimps [not_all, not_ex]
   3.455 +       addsimps map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps}));
   3.456 +
   3.457 +val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   3.458 +
   3.459 +val cTrp = @{cterm "Trueprop"};
   3.460 +val cConj = @{cterm "op &"};
   3.461 +val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
   3.462 +val assume_Trueprop = mk_comb cTrp #> assume;
   3.463 +val list_mk_conj = list_mk_binop cConj;
   3.464 +val conjs = list_dest_binop cConj;
   3.465 +val mk_neg = mk_comb cNot;
   3.466 +
   3.467 +fun striplist dest = 
   3.468 + let
   3.469 +  fun h acc x = case try dest x of
   3.470 +    SOME (a,b) => h (h acc b) a
   3.471 +  | NONE => x::acc
   3.472 + in h [] end;
   3.473 +fun list_mk_binop b = foldr1 (fn (s,t) => Thm.capply (Thm.capply b s) t);
   3.474 +
   3.475 +val eq_commute = mk_meta_eq @{thm eq_commute};
   3.476 +
   3.477 +fun sym_conv eq = 
   3.478 + let val (l,r) = Thm.dest_binop eq
   3.479 + in instantiate' [SOME (ctyp_of_term l)] [SOME l, SOME r] eq_commute
   3.480 + end;
   3.481 +
   3.482 +  (* FIXME : copied from cqe.ML -- complex QE*)
   3.483 +fun conjuncts ct =
   3.484 + case term_of ct of
   3.485 +  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
   3.486 +| _ => [ct];
   3.487 +
   3.488 +fun fold1 f = foldr1 (uncurry f);
   3.489 +
   3.490 +val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
   3.491 +
   3.492 +fun mk_conj_tab th = 
   3.493 + let fun h acc th = 
   3.494 +   case prop_of th of
   3.495 +   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
   3.496 +     h (h acc (th RS conjunct2)) (th RS conjunct1)
   3.497 +  | @{term "Trueprop"}$p => (p,th)::acc
   3.498 +in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
   3.499 +
   3.500 +fun is_conj (@{term "op &"}$_$_) = true
   3.501 +  | is_conj _ = false;
   3.502 +
   3.503 +fun prove_conj tab cjs = 
   3.504 + case cjs of 
   3.505 +   [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c
   3.506 + | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
   3.507 +
   3.508 +fun conj_ac_rule eq = 
   3.509 + let 
   3.510 +  val (l,r) = Thm.dest_equals eq
   3.511 +  val ctabl = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} l))
   3.512 +  val ctabr = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} r))
   3.513 +  fun tabl c = the (Termtab.lookup ctabl (term_of c))
   3.514 +  fun tabr c = the (Termtab.lookup ctabr (term_of c))
   3.515 +  val thl  = prove_conj tabl (conjuncts r) |> implies_intr_hyps
   3.516 +  val thr  = prove_conj tabr (conjuncts l) |> implies_intr_hyps
   3.517 +  val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI}
   3.518 + in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end;
   3.519 +
   3.520 + (* END FIXME.*)
   3.521 +
   3.522 +   (* Conversion for the equivalence of existential statements where 
   3.523 +      EX quantifiers are rearranged differently *)
   3.524 + fun ext T = cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   3.525 + fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
   3.526 +
   3.527 +fun choose v th th' = case concl_of th of 
   3.528 +  @{term Trueprop} $ (Const("Ex",_)$_) => 
   3.529 +   let
   3.530 +    val p = (funpow 2 Thm.dest_arg o cprop_of) th
   3.531 +    val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   3.532 +    val th0 = fconv_rule (Thm.beta_conversion true)
   3.533 +        (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
   3.534 +    val pv = (Thm.rhs_of o Thm.beta_conversion true) 
   3.535 +          (Thm.capply @{cterm Trueprop} (Thm.capply p v))
   3.536 +    val th1 = forall_intr v (implies_intr pv th')
   3.537 +   in implies_elim (implies_elim th0 th) th1  end
   3.538 +| _ => error ""
   3.539 +
   3.540 +fun simple_choose v th = 
   3.541 +   choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
   3.542 +
   3.543 +
   3.544 + fun mkexi v th = 
   3.545 +  let 
   3.546 +   val p = Thm.cabs v (Thm.dest_arg (Thm.cprop_of th))
   3.547 +  in implies_elim 
   3.548 +    (fconv_rule (Thm.beta_conversion true) (instantiate' [SOME (ctyp_of_term v)] [SOME p, SOME v] @{thm exI}))
   3.549 +      th
   3.550 +  end
   3.551 + fun ex_eq_conv t = 
   3.552 +  let 
   3.553 +  val (p0,q0) = Thm.dest_binop t
   3.554 +  val (vs',P) = strip_exists p0 
   3.555 +  val (vs,_) = strip_exists q0 
   3.556 +   val th = assume (Thm.capply @{cterm Trueprop} P)
   3.557 +   val th1 =  implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th))
   3.558 +   val th2 =  implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
   3.559 +   val p = (Thm.dest_arg o Thm.dest_arg1 o cprop_of) th1
   3.560 +   val q = (Thm.dest_arg o Thm.dest_arg o cprop_of) th1
   3.561 +  in implies_elim (implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2
   3.562 +     |> mk_meta_eq
   3.563 +  end;
   3.564 +
   3.565 +
   3.566 + fun getname v = case term_of v of 
   3.567 +  Free(s,_) => s
   3.568 + | Var ((s,_),_) => s
   3.569 + | _ => "x"
   3.570 + fun mk_eq s t = Thm.capply (Thm.capply @{cterm "op == :: bool => _"} s) t
   3.571 + fun mkeq s t = Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply @{cterm "op = :: bool => _"} s) t)
   3.572 + fun mk_exists v th = arg_cong_rule (ext (ctyp_of_term v))
   3.573 +   (Thm.abstract_rule (getname v) v th)
   3.574 + val simp_ex_conv = 
   3.575 +     Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms(39)})
   3.576 +
   3.577 +fun frees t = Thm.add_cterm_frees t [];
   3.578 +fun free_in v t = member op aconvc (frees t) v;
   3.579 +
   3.580 +val vsubst = let
   3.581 + fun vsubst (t,v) tm =  
   3.582 +   (Thm.rhs_of o Thm.beta_conversion false) (Thm.capply (Thm.cabs v tm) t)
   3.583 +in fold vsubst end;
   3.584 +
   3.585 +
   3.586 +(** main **)
   3.587 +
   3.588 +fun ring_and_ideal_conv
   3.589 +  {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
   3.590 +   field = (f_ops, f_rules), idom, ideal}
   3.591 +  dest_const mk_const ring_eq_conv ring_normalize_conv =
   3.592 +let
   3.593 +  val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
   3.594 +  val [ring_add_tm, ring_mul_tm, ring_pow_tm] =
   3.595 +    map dest_fun2 [add_pat, mul_pat, pow_pat];
   3.596 +
   3.597 +  val (ring_sub_tm, ring_neg_tm) =
   3.598 +    (case r_ops of
   3.599 +     [sub_pat, neg_pat] => (dest_fun2 sub_pat, dest_fun neg_pat)
   3.600 +    |_  => (@{cterm "True"}, @{cterm "True"}));
   3.601 +
   3.602 +  val (field_div_tm, field_inv_tm) =
   3.603 +    (case f_ops of
   3.604 +       [div_pat, inv_pat] => (dest_fun2 div_pat, dest_fun inv_pat)
   3.605 +     | _ => (@{cterm "True"}, @{cterm "True"}));
   3.606 +
   3.607 +  val [idom_thm, neq_thm] = idom;
   3.608 +  val [idl_sub, idl_add0] = 
   3.609 +     if length ideal = 2 then ideal else [eq_commute, eq_commute]
   3.610 +  fun ring_dest_neg t =
   3.611 +    let val (l,r) = dest_comb t 
   3.612 +    in if Term.could_unify(term_of l,term_of ring_neg_tm) then r 
   3.613 +       else raise CTERM ("ring_dest_neg", [t])
   3.614 +    end
   3.615 +
   3.616 + val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
   3.617 + fun field_dest_inv t =
   3.618 +    let val (l,r) = dest_comb t in
   3.619 +        if Term.could_unify(term_of l, term_of field_inv_tm) then r 
   3.620 +        else raise CTERM ("field_dest_inv", [t])
   3.621 +    end
   3.622 + val ring_dest_add = dest_binary ring_add_tm;
   3.623 + val ring_mk_add = mk_binop ring_add_tm;
   3.624 + val ring_dest_sub = dest_binary ring_sub_tm;
   3.625 + val ring_mk_sub = mk_binop ring_sub_tm;
   3.626 + val ring_dest_mul = dest_binary ring_mul_tm;
   3.627 + val ring_mk_mul = mk_binop ring_mul_tm;
   3.628 + val field_dest_div = dest_binary field_div_tm;
   3.629 + val field_mk_div = mk_binop field_div_tm;
   3.630 + val ring_dest_pow = dest_binary ring_pow_tm;
   3.631 + val ring_mk_pow = mk_binop ring_pow_tm ;
   3.632 + fun grobvars tm acc =
   3.633 +    if can dest_const tm then acc
   3.634 +    else if can ring_dest_neg tm then grobvars (dest_arg tm) acc
   3.635 +    else if can ring_dest_pow tm then grobvars (dest_arg1 tm) acc
   3.636 +    else if can ring_dest_add tm orelse can ring_dest_sub tm
   3.637 +            orelse can ring_dest_mul tm
   3.638 +    then grobvars (dest_arg1 tm) (grobvars (dest_arg tm) acc)
   3.639 +    else if can field_dest_inv tm
   3.640 +         then
   3.641 +          let val gvs = grobvars (dest_arg tm) [] 
   3.642 +          in if null gvs then acc else tm::acc
   3.643 +          end
   3.644 +    else if can field_dest_div tm then
   3.645 +         let val lvs = grobvars (dest_arg1 tm) acc
   3.646 +             val gvs = grobvars (dest_arg tm) []
   3.647 +          in if null gvs then lvs else tm::acc
   3.648 +          end 
   3.649 +    else tm::acc ;
   3.650 +
   3.651 +fun grobify_term vars tm =
   3.652 +((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
   3.653 +     [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
   3.654 +handle  CTERM _ =>
   3.655 + ((let val x = dest_const tm
   3.656 + in if x =/ rat_0 then [] else [(x,map (fn v => 0) vars)]
   3.657 + end)
   3.658 + handle ERROR _ =>
   3.659 +  ((grob_neg(grobify_term vars (ring_dest_neg tm)))
   3.660 +  handle CTERM _ =>
   3.661 +   (
   3.662 +   (grob_inv(grobify_term vars (field_dest_inv tm)))
   3.663 +   handle CTERM _ => 
   3.664 +    ((let val (l,r) = ring_dest_add tm
   3.665 +    in grob_add (grobify_term vars l) (grobify_term vars r)
   3.666 +    end)
   3.667 +    handle CTERM _ =>
   3.668 +     ((let val (l,r) = ring_dest_sub tm
   3.669 +     in grob_sub (grobify_term vars l) (grobify_term vars r)
   3.670 +     end)
   3.671 +     handle  CTERM _ =>
   3.672 +      ((let val (l,r) = ring_dest_mul tm
   3.673 +      in grob_mul (grobify_term vars l) (grobify_term vars r)
   3.674 +      end)
   3.675 +       handle CTERM _ =>
   3.676 +        (  (let val (l,r) = field_dest_div tm
   3.677 +          in grob_div (grobify_term vars l) (grobify_term vars r)
   3.678 +          end)
   3.679 +         handle CTERM _ =>
   3.680 +          ((let val (l,r) = ring_dest_pow tm
   3.681 +          in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r)
   3.682 +          end)
   3.683 +           handle CTERM _ => error "grobify_term: unknown or invalid term")))))))));
   3.684 +val eq_tm = idom_thm |> concl |> dest_arg |> dest_arg |> dest_fun2;
   3.685 +val dest_eq = dest_binary eq_tm;
   3.686 +
   3.687 +fun grobify_equation vars tm =
   3.688 +    let val (l,r) = dest_binary eq_tm tm
   3.689 +    in grob_sub (grobify_term vars l) (grobify_term vars r)
   3.690 +    end;
   3.691 +
   3.692 +fun grobify_equations tm =
   3.693 + let
   3.694 +  val cjs = conjs tm
   3.695 +  val  rawvars = fold_rev (fn eq => fn a =>
   3.696 +                                       grobvars (dest_arg1 eq) (grobvars (dest_arg eq) a)) cjs []
   3.697 +  val vars = sort (fn (x, y) => Term_Ord.term_ord(term_of x,term_of y))
   3.698 +                  (distinct (op aconvc) rawvars)
   3.699 + in (vars,map (grobify_equation vars) cjs)
   3.700 + end;
   3.701 +
   3.702 +val holify_polynomial =
   3.703 + let fun holify_varpow (v,n) =
   3.704 +  if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n)  (* FIXME *)
   3.705 + fun holify_monomial vars (c,m) =
   3.706 +  let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
   3.707 +   in end_itlist ring_mk_mul (mk_const c :: xps)
   3.708 +  end
   3.709 + fun holify_polynomial vars p =
   3.710 +     if null p then mk_const (rat_0)
   3.711 +     else end_itlist ring_mk_add (map (holify_monomial vars) p)
   3.712 + in holify_polynomial
   3.713 + end ;
   3.714 +val idom_rule = simplify (HOL_basic_ss addsimps [idom_thm]);
   3.715 +fun prove_nz n = eqF_elim
   3.716 +                 (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0))));
   3.717 +val neq_01 = prove_nz (rat_1);
   3.718 +fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
   3.719 +fun mk_add th1 = combination(arg_cong_rule ring_add_tm th1);
   3.720 +
   3.721 +fun refute tm =
   3.722 + if tm aconvc false_tm then assume_Trueprop tm else
   3.723 + ((let
   3.724 +   val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm))
   3.725 +   val  nths = filter (is_eq o dest_arg o concl) nths0
   3.726 +   val eths = filter (is_eq o concl) eths0
   3.727 +  in
   3.728 +   if null eths then
   3.729 +    let
   3.730 +      val th1 = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths
   3.731 +      val th2 = Conv.fconv_rule
   3.732 +                ((arg_conv #> arg_conv)
   3.733 +                     (binop_conv ring_normalize_conv)) th1
   3.734 +      val conc = th2 |> concl |> dest_arg
   3.735 +      val (l,r) = conc |> dest_eq
   3.736 +    in implies_intr (mk_comb cTrp tm)
   3.737 +                    (equal_elim (arg_cong_rule cTrp (eqF_intr th2))
   3.738 +                           (reflexive l |> mk_object_eq))
   3.739 +    end
   3.740 +   else
   3.741 +   let
   3.742 +    val (vars,l,cert,noteqth) =(
   3.743 +     if null nths then
   3.744 +      let val (vars,pols) = grobify_equations(list_mk_conj(map concl eths))
   3.745 +          val (l,cert) = grobner_weak vars pols
   3.746 +      in (vars,l,cert,neq_01)
   3.747 +      end
   3.748 +     else
   3.749 +      let
   3.750 +       val nth = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths
   3.751 +       val (vars,pol::pols) =
   3.752 +          grobify_equations(list_mk_conj(dest_arg(concl nth)::map concl eths))
   3.753 +       val (deg,l,cert) = grobner_strong vars pols pol
   3.754 +       val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth
   3.755 +       val th2 = funpow deg (idom_rule o HOLogic.conj_intr th1) neq_01
   3.756 +      in (vars,l,cert,th2)
   3.757 +      end)
   3.758 +    val cert_pos = map (fn (i,p) => (i,filter (fn (c,m) => c >/ rat_0) p)) cert
   3.759 +    val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
   3.760 +                                            (filter (fn (c,m) => c </ rat_0) p))) cert
   3.761 +    val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
   3.762 +    val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
   3.763 +    fun thm_fn pols =
   3.764 +        if null pols then reflexive(mk_const rat_0) else
   3.765 +        end_itlist mk_add
   3.766 +            (map (fn (i,p) => arg_cong_rule (mk_comb ring_mul_tm p)
   3.767 +              (nth eths i |> mk_meta_eq)) pols)
   3.768 +    val th1 = thm_fn herts_pos
   3.769 +    val th2 = thm_fn herts_neg
   3.770 +    val th3 = HOLogic.conj_intr(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth
   3.771 +    val th4 = Conv.fconv_rule ((arg_conv o arg_conv o binop_conv) ring_normalize_conv)
   3.772 +                               (neq_rule l th3)
   3.773 +    val (l,r) = dest_eq(dest_arg(concl th4))
   3.774 +   in implies_intr (mk_comb cTrp tm)
   3.775 +                        (equal_elim (arg_cong_rule cTrp (eqF_intr th4))
   3.776 +                   (reflexive l |> mk_object_eq))
   3.777 +   end
   3.778 +  end) handle ERROR _ => raise CTERM ("Gorbner-refute: unable to refute",[tm]))
   3.779 +
   3.780 +fun ring tm =
   3.781 + let
   3.782 +  fun mk_forall x p =
   3.783 +      mk_comb (cterm_rule (instantiate' [SOME (ctyp_of_term x)] []) @{cpat "All:: (?'a => bool) => _"}) (cabs x p)
   3.784 +  val avs = add_cterm_frees tm []
   3.785 +  val P' = fold mk_forall avs tm
   3.786 +  val th1 = initial_conv(mk_neg P')
   3.787 +  val (evs,bod) = strip_exists(concl th1) in
   3.788 +   if is_forall bod then raise CTERM("ring: non-universal formula",[tm])
   3.789 +   else
   3.790 +   let
   3.791 +    val th1a = weak_dnf_conv bod
   3.792 +    val boda = concl th1a
   3.793 +    val th2a = refute_disj refute boda
   3.794 +    val th2b = [mk_object_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans
   3.795 +    val th2 = fold (fn v => fn th => (forall_intr v th) COMP allI) evs (th2b RS PFalse)
   3.796 +    val th3 = equal_elim
   3.797 +                (Simplifier.rewrite (HOL_basic_ss addsimps [not_ex RS sym])
   3.798 +                          (th2 |> cprop_of)) th2
   3.799 +    in specl avs
   3.800 +             ([[[mk_object_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD)
   3.801 +   end
   3.802 + end
   3.803 +fun ideal tms tm ord =
   3.804 + let
   3.805 +  val rawvars = fold_rev grobvars (tm::tms) []
   3.806 +  val vars = sort ord (distinct (fn (x,y) => (term_of x) aconv (term_of y)) rawvars)
   3.807 +  val pols = map (grobify_term vars) tms
   3.808 +  val pol = grobify_term vars tm
   3.809 +  val cert = grobner_ideal vars pols pol
   3.810 + in map_range (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
   3.811 +   (length pols)
   3.812 + end
   3.813 +
   3.814 +fun poly_eq_conv t = 
   3.815 + let val (a,b) = Thm.dest_binop t
   3.816 + in fconv_rule (arg_conv (arg1_conv ring_normalize_conv)) 
   3.817 +     (instantiate' [] [SOME a, SOME b] idl_sub)
   3.818 + end
   3.819 + val poly_eq_simproc = 
   3.820 +  let 
   3.821 +   fun proc phi  ss t = 
   3.822 +    let val th = poly_eq_conv t
   3.823 +    in if Thm.is_reflexive th then NONE else SOME th
   3.824 +    end
   3.825 +   in make_simproc {lhss = [Thm.lhs_of idl_sub], 
   3.826 +                name = "poly_eq_simproc", proc = proc, identifier = []}
   3.827 +   end;
   3.828 +  val poly_eq_ss = HOL_basic_ss addsimps @{thms simp_thms}
   3.829 +                        addsimprocs [poly_eq_simproc]
   3.830 +
   3.831 + local
   3.832 +  fun is_defined v t =
   3.833 +  let 
   3.834 +   val mons = striplist(dest_binary ring_add_tm) t 
   3.835 +  in member (op aconvc) mons v andalso 
   3.836 +    forall (fn m => v aconvc m 
   3.837 +          orelse not(member (op aconvc) (Thm.add_cterm_frees m []) v)) mons
   3.838 +  end
   3.839 +
   3.840 +  fun isolate_variable vars tm =
   3.841 +  let 
   3.842 +   val th = poly_eq_conv tm
   3.843 +   val th' = (sym_conv then_conv poly_eq_conv) tm
   3.844 +   val (v,th1) = 
   3.845 +   case find_first(fn v=> is_defined v (Thm.dest_arg1 (Thm.rhs_of th))) vars of
   3.846 +    SOME v => (v,th')
   3.847 +   | NONE => (the (find_first 
   3.848 +          (fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th)
   3.849 +   val th2 = transitive th1 
   3.850 +        (instantiate' []  [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v] 
   3.851 +          idl_add0)
   3.852 +   in fconv_rule(funpow 2 arg_conv ring_normalize_conv) th2
   3.853 +   end
   3.854 + in
   3.855 + fun unwind_polys_conv tm =
   3.856 + let 
   3.857 +  val (vars,bod) = strip_exists tm
   3.858 +  val cjs = striplist (dest_binary @{cterm "op &"}) bod
   3.859 +  val th1 = (the (get_first (try (isolate_variable vars)) cjs) 
   3.860 +             handle Option => raise CTERM ("unwind_polys_conv",[tm]))
   3.861 +  val eq = Thm.lhs_of th1
   3.862 +  val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs))
   3.863 +  val th2 = conj_ac_rule (mk_eq bod bod')
   3.864 +  val th3 = transitive th2 
   3.865 +         (Drule.binop_cong_rule @{cterm "op &"} th1 
   3.866 +                (reflexive (Thm.dest_arg (Thm.rhs_of th2))))
   3.867 +  val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
   3.868 +  val vars' = (remove op aconvc v vars) @ [v]
   3.869 +  val th4 = fconv_rule (arg_conv simp_ex_conv) (mk_exists v th3)
   3.870 +  val th5 = ex_eq_conv (mk_eq tm (fold mk_ex (remove op aconvc v vars) (Thm.lhs_of th4)))
   3.871 + in transitive th5 (fold mk_exists (remove op aconvc v vars) th4)
   3.872 + end;
   3.873 +end
   3.874 +
   3.875 +local
   3.876 + fun scrub_var v m =
   3.877 +  let 
   3.878 +   val ps = striplist ring_dest_mul m 
   3.879 +   val ps' = remove op aconvc v ps
   3.880 +  in if null ps' then one_tm else fold1 ring_mk_mul ps'
   3.881 +  end
   3.882 + fun find_multipliers v mons =
   3.883 +  let 
   3.884 +   val mons1 = filter (fn m => free_in v m) mons 
   3.885 +   val mons2 = map (scrub_var v) mons1 
   3.886 +   in  if null mons2 then zero_tm else fold1 ring_mk_add mons2
   3.887 +  end
   3.888 +
   3.889 + fun isolate_monomials vars tm =
   3.890 + let 
   3.891 +  val (cmons,vmons) =
   3.892 +    List.partition (fn m => null (inter (op aconvc) vars (frees m)))
   3.893 +                   (striplist ring_dest_add tm)
   3.894 +  val cofactors = map (fn v => find_multipliers v vmons) vars
   3.895 +  val cnc = if null cmons then zero_tm
   3.896 +             else Thm.capply ring_neg_tm
   3.897 +                    (list_mk_binop ring_add_tm cmons) 
   3.898 +  in (cofactors,cnc)
   3.899 +  end;
   3.900 +
   3.901 +fun isolate_variables evs ps eq =
   3.902 + let 
   3.903 +  val vars = filter (fn v => free_in v eq) evs
   3.904 +  val (qs,p) = isolate_monomials vars eq
   3.905 +  val rs = ideal (qs @ ps) p 
   3.906 +              (fn (s,t) => Term_Ord.term_ord (term_of s, term_of t))
   3.907 + in (eq, take (length qs) rs ~~ vars)
   3.908 + end;
   3.909 + fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
   3.910 +in
   3.911 + fun solve_idealism evs ps eqs =
   3.912 +  if null evs then [] else
   3.913 +  let 
   3.914 +   val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> the
   3.915 +   val evs' = subtract op aconvc evs (map snd cfs)
   3.916 +   val eqs' = map (subst_in_poly cfs) (remove op aconvc eq eqs)
   3.917 +  in cfs @ solve_idealism evs' ps eqs'
   3.918 +  end;
   3.919 +end;
   3.920 +
   3.921 +
   3.922 +in {ring_conv = ring, simple_ideal = ideal, multi_ideal = solve_idealism, 
   3.923 +    poly_eq_ss = poly_eq_ss, unwind_conv = unwind_polys_conv}
   3.924 +end;
   3.925 +
   3.926 +
   3.927 +fun find_term bounds tm =
   3.928 +  (case term_of tm of
   3.929 +    Const ("op =", T) $ _ $ _ =>
   3.930 +      if domain_type T = HOLogic.boolT then find_args bounds tm
   3.931 +      else dest_arg tm
   3.932 +  | Const ("Not", _) $ _ => find_term bounds (dest_arg tm)
   3.933 +  | Const ("All", _) $ _ => find_body bounds (dest_arg tm)
   3.934 +  | Const ("Ex", _) $ _ => find_body bounds (dest_arg tm)
   3.935 +  | Const ("op &", _) $ _ $ _ => find_args bounds tm
   3.936 +  | Const ("op |", _) $ _ $ _ => find_args bounds tm
   3.937 +  | Const ("op -->", _) $ _ $ _ => find_args bounds tm
   3.938 +  | @{term "op ==>"} $_$_ => find_args bounds tm
   3.939 +  | Const("op ==",_)$_$_ => find_args bounds tm
   3.940 +  | @{term Trueprop}$_ => find_term bounds (dest_arg tm)
   3.941 +  | _ => raise TERM ("find_term", []))
   3.942 +and find_args bounds tm =
   3.943 +  let val (t, u) = Thm.dest_binop tm
   3.944 +  in (find_term bounds t handle TERM _ => find_term bounds u) end
   3.945 +and find_body bounds b =
   3.946 +  let val (_, b') = dest_abs (SOME (Name.bound bounds)) b
   3.947 +  in find_term (bounds + 1) b' end;
   3.948 +
   3.949 +
   3.950 +fun get_ring_ideal_convs ctxt form = 
   3.951 + case try (find_term 0) form of
   3.952 +  NONE => NONE
   3.953 +| SOME tm =>
   3.954 +  (case Semiring_Normalizer.match ctxt tm of
   3.955 +    NONE => NONE
   3.956 +  | SOME (res as (theory, {is_const, dest_const, 
   3.957 +          mk_const, conv = ring_eq_conv})) =>
   3.958 +     SOME (ring_and_ideal_conv theory
   3.959 +          dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
   3.960 +          (Semiring_Normalizer.semiring_normalize_wrapper ctxt res)))
   3.961 +
   3.962 +fun ring_solve ctxt form =
   3.963 +  (case try (find_term 0 (* FIXME !? *)) form of
   3.964 +    NONE => reflexive form
   3.965 +  | SOME tm =>
   3.966 +      (case Semiring_Normalizer.match ctxt tm of
   3.967 +        NONE => reflexive form
   3.968 +      | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) =>
   3.969 +        #ring_conv (ring_and_ideal_conv theory
   3.970 +          dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
   3.971 +          (Semiring_Normalizer.semiring_normalize_wrapper ctxt res)) form));
   3.972 +
   3.973 +fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (Simplifier.context ctxt
   3.974 +  (HOL_basic_ss addsimps (Algebra_Simplification.get ctxt) delsimps del_thms addsimps add_thms));
   3.975 +
   3.976 +fun ring_tac add_ths del_ths ctxt =
   3.977 +  Object_Logic.full_atomize_tac
   3.978 +  THEN' presimplify ctxt add_ths del_ths
   3.979 +  THEN' CSUBGOAL (fn (p, i) =>
   3.980 +    rtac (let val form = Object_Logic.dest_judgment p
   3.981 +          in case get_ring_ideal_convs ctxt form of
   3.982 +           NONE => reflexive form
   3.983 +          | SOME thy => #ring_conv thy form
   3.984 +          end) i
   3.985 +      handle TERM _ => no_tac
   3.986 +        | CTERM _ => no_tac
   3.987 +        | THM _ => no_tac);
   3.988 +
   3.989 +local
   3.990 + fun lhs t = case term_of t of
   3.991 +  Const("op =",_)$_$_ => Thm.dest_arg1 t
   3.992 + | _=> raise CTERM ("ideal_tac - lhs",[t])
   3.993 + fun exitac NONE = no_tac
   3.994 +   | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
   3.995 +in 
   3.996 +fun ideal_tac add_ths del_ths ctxt = 
   3.997 +  presimplify ctxt add_ths del_ths
   3.998 + THEN'
   3.999 + CSUBGOAL (fn (p, i) =>
  3.1000 +  case get_ring_ideal_convs ctxt p of
  3.1001 +   NONE => no_tac
  3.1002 + | SOME thy => 
  3.1003 +  let
  3.1004 +   fun poly_exists_tac {asms = asms, concl = concl, prems = prems,
  3.1005 +            params = params, context = ctxt, schematics = scs} = 
  3.1006 +    let
  3.1007 +     val (evs,bod) = strip_exists (Thm.dest_arg concl)
  3.1008 +     val ps = map_filter (try (lhs o Thm.dest_arg)) asms 
  3.1009 +     val cfs = (map swap o #multi_ideal thy evs ps) 
  3.1010 +                   (map Thm.dest_arg1 (conjuncts bod))
  3.1011 +     val ws = map (exitac o AList.lookup op aconvc cfs) evs
  3.1012 +    in EVERY (rev ws) THEN Method.insert_tac prems 1 
  3.1013 +        THEN ring_tac add_ths del_ths ctxt 1
  3.1014 +   end
  3.1015 +  in  
  3.1016 +     clarify_tac @{claset} i 
  3.1017 +     THEN Object_Logic.full_atomize_tac i 
  3.1018 +     THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i 
  3.1019 +     THEN clarify_tac @{claset} i 
  3.1020 +     THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
  3.1021 +     THEN SUBPROOF poly_exists_tac ctxt i
  3.1022 +  end
  3.1023 + handle TERM _ => no_tac
  3.1024 +     | CTERM _ => no_tac
  3.1025 +     | THM _ => no_tac); 
  3.1026 +end;
  3.1027 +
  3.1028 +fun algebra_tac add_ths del_ths ctxt i = 
  3.1029 + ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i
  3.1030 + 
  3.1031 +local
  3.1032 +
  3.1033 +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
  3.1034 +val addN = "add"
  3.1035 +val delN = "del"
  3.1036 +val any_keyword = keyword addN || keyword delN
  3.1037 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
  3.1038 +
  3.1039 +in
  3.1040 +
  3.1041 +val algebra_method = ((Scan.optional (keyword addN |-- thms) []) -- 
  3.1042 +   (Scan.optional (keyword delN |-- thms) [])) >>
  3.1043 +  (fn (add_ths, del_ths) => fn ctxt =>
  3.1044 +       SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt))
  3.1045 +
  3.1046 +end;
  3.1047 +
  3.1048 +end;