src/HOL/Tools/groebner.ML
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 46497 89ccf66aa73d
child 47432 e1576d13e933
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
haftmann@37744
     1
(*  Title:      HOL/Tools/groebner.ML
wenzelm@23252
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@23252
     3
*)
wenzelm@23252
     4
wenzelm@23252
     5
signature GROEBNER =
wenzelm@23252
     6
sig
wenzelm@41453
     7
  val ring_and_ideal_conv:
chaieb@30866
     8
    {idom: thm list, ring: cterm list * thm list, field: cterm list * thm list,
chaieb@30866
     9
     vars: cterm list, semiring: cterm list * thm list, ideal : thm list} ->
wenzelm@23487
    10
    (cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
wenzelm@23487
    11
    conv ->  conv ->
wenzelm@41453
    12
     {ring_conv : conv,
haftmann@36723
    13
     simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list),
haftmann@36723
    14
     multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list,
haftmann@36723
    15
     poly_eq_ss: simpset, unwind_conv : conv}
haftmann@36723
    16
  val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
haftmann@36723
    17
  val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
haftmann@36723
    18
  val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
haftmann@36723
    19
  val algebra_method: (Proof.context -> Method.method) context_parser
wenzelm@23252
    20
end
wenzelm@23252
    21
chaieb@25251
    22
structure Groebner : GROEBNER =
wenzelm@23252
    23
struct
wenzelm@23252
    24
chaieb@25251
    25
fun is_comb ct =
chaieb@25251
    26
  (case Thm.term_of ct of
chaieb@25251
    27
    _ $ _ => true
chaieb@25251
    28
  | _ => false);
chaieb@25251
    29
chaieb@25251
    30
val concl = Thm.cprop_of #> Thm.dest_arg;
chaieb@25251
    31
chaieb@25251
    32
fun is_binop ct ct' =
chaieb@25251
    33
  (case Thm.term_of ct' of
chaieb@25251
    34
    c $ _ $ _ => term_of ct aconv c
chaieb@25251
    35
  | _ => false);
chaieb@25251
    36
chaieb@25251
    37
fun dest_binary ct ct' =
chaieb@25251
    38
  if is_binop ct ct' then Thm.dest_binop ct'
chaieb@25251
    39
  else raise CTERM ("dest_binary: bad binop", [ct, ct'])
chaieb@25251
    40
chaieb@25251
    41
fun inst_thm inst = Thm.instantiate ([], inst);
wenzelm@23557
    42
wenzelm@23252
    43
val rat_0 = Rat.zero;
wenzelm@23252
    44
val rat_1 = Rat.one;
wenzelm@23252
    45
val minus_rat = Rat.neg;
wenzelm@23252
    46
val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
wenzelm@23252
    47
fun int_of_rat a =
wenzelm@23252
    48
    case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int";
haftmann@23514
    49
val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
wenzelm@23252
    50
wenzelm@23252
    51
val (eqF_intr, eqF_elim) =
haftmann@36713
    52
  let val [th1,th2] = @{thms PFalse}
wenzelm@23252
    53
  in (fn th => th COMP th2, fn th => th COMP th1) end;
wenzelm@23252
    54
wenzelm@23252
    55
val (PFalse, PFalse') =
haftmann@36713
    56
 let val PFalse_eq = nth @{thms simp_thms} 13
wenzelm@23252
    57
 in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end;
wenzelm@23252
    58
wenzelm@23252
    59
chaieb@25251
    60
(* Type for recording history, i.e. how a polynomial was obtained. *)
wenzelm@23252
    61
wenzelm@23252
    62
datatype history =
wenzelm@24630
    63
   Start of int
wenzelm@24630
    64
 | Mmul of (Rat.rat * int list) * history
wenzelm@23252
    65
 | Add of history * history;
wenzelm@23252
    66
wenzelm@23252
    67
wenzelm@23252
    68
(* Monomial ordering. *)
wenzelm@23252
    69
wenzelm@23252
    70
fun morder_lt m1 m2=
wenzelm@23252
    71
    let fun lexorder l1 l2 =
wenzelm@23252
    72
            case (l1,l2) of
wenzelm@23252
    73
                ([],[]) => false
wenzelm@23252
    74
              | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2
wenzelm@23252
    75
              | _ => error "morder: inconsistent monomial lengths"
wenzelm@24630
    76
        val n1 = Integer.sum m1
wenzelm@24630
    77
        val n2 = Integer.sum m2 in
wenzelm@23252
    78
    n1 < n2 orelse n1 = n2 andalso lexorder m1 m2
wenzelm@23252
    79
    end;
wenzelm@23252
    80
wenzelm@23252
    81
fun morder_le m1 m2 = morder_lt m1 m2 orelse (m1 = m2);
wenzelm@23252
    82
wenzelm@23252
    83
fun morder_gt m1 m2 = morder_lt m2 m1;
wenzelm@23252
    84
wenzelm@23252
    85
(* Arithmetic on canonical polynomials. *)
wenzelm@23252
    86
wenzelm@23252
    87
fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l;
wenzelm@23252
    88
wenzelm@23252
    89
fun grob_add l1 l2 =
wenzelm@23252
    90
  case (l1,l2) of
wenzelm@23252
    91
    ([],l2) => l2
wenzelm@23252
    92
  | (l1,[]) => l1
wenzelm@23252
    93
  | ((c1,m1)::o1,(c2,m2)::o2) =>
wenzelm@23252
    94
        if m1 = m2 then
wenzelm@23252
    95
          let val c = c1+/c2 val rest = grob_add o1 o2 in
wenzelm@23252
    96
          if c =/ rat_0 then rest else (c,m1)::rest end
wenzelm@23252
    97
        else if morder_lt m2 m1 then (c1,m1)::(grob_add o1 l2)
wenzelm@23252
    98
        else (c2,m2)::(grob_add l1 o2);
wenzelm@23252
    99
wenzelm@23252
   100
fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
wenzelm@23252
   101
wenzelm@24630
   102
fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2));
wenzelm@23252
   103
wenzelm@23252
   104
fun grob_cmul cm pol = map (grob_mmul cm) pol;
wenzelm@23252
   105
wenzelm@23252
   106
fun grob_mul l1 l2 =
wenzelm@23252
   107
  case l1 of
wenzelm@23252
   108
    [] => []
wenzelm@23252
   109
  | (h1::t1) => grob_add (grob_cmul h1 l2) (grob_mul t1 l2);
wenzelm@23252
   110
wenzelm@23252
   111
fun grob_inv l =
wenzelm@23252
   112
  case l of
wenzelm@23252
   113
    [(c,vs)] => if (forall (fn x => x = 0) vs) then
wenzelm@23252
   114
                  if (c =/ rat_0) then error "grob_inv: division by zero"
wenzelm@23252
   115
                  else [(rat_1 // c,vs)]
wenzelm@23252
   116
              else error "grob_inv: non-constant divisor polynomial"
wenzelm@23252
   117
  | _ => error "grob_inv: non-constant divisor polynomial";
wenzelm@23252
   118
wenzelm@23252
   119
fun grob_div l1 l2 =
wenzelm@23252
   120
  case l2 of
wenzelm@23252
   121
    [(c,l)] => if (forall (fn x => x = 0) l) then
wenzelm@23252
   122
                 if c =/ rat_0 then error "grob_div: division by zero"
wenzelm@23252
   123
                 else grob_cmul (rat_1 // c,l) l1
wenzelm@23252
   124
             else error "grob_div: non-constant divisor polynomial"
wenzelm@23252
   125
  | _ => error "grob_div: non-constant divisor polynomial";
wenzelm@23252
   126
wenzelm@23252
   127
fun grob_pow vars l n =
wenzelm@23252
   128
  if n < 0 then error "grob_pow: negative power"
wenzelm@23252
   129
  else if n = 0 then [(rat_1,map (fn v => 0) vars)]
wenzelm@24630
   130
  else grob_mul l (grob_pow vars l (n - 1));
wenzelm@23252
   131
wenzelm@23252
   132
fun degree vn p =
wenzelm@23252
   133
 case p of
wenzelm@23252
   134
  [] => error "Zero polynomial"
wenzelm@23252
   135
| [(c,ns)] => nth ns vn
wenzelm@24630
   136
| (c,ns)::p' => Int.max (nth ns vn, degree vn p');
wenzelm@23252
   137
wenzelm@23252
   138
fun head_deg vn p = let val d = degree vn p in
wenzelm@23252
   139
 (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;
wenzelm@23252
   140
wenzelm@24630
   141
val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns);
wenzelm@23252
   142
val grob_pdiv =
wenzelm@23252
   143
 let fun pdiv_aux vn (n,a) p k s =
wenzelm@23252
   144
  if is_zerop s then (k,s) else
wenzelm@23252
   145
  let val (m,b) = head_deg vn s
wenzelm@23252
   146
  in if m < n then (k,s) else
wenzelm@24630
   147
     let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0)
wenzelm@23252
   148
                                                (snd (hd s)))]
wenzelm@23252
   149
     in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p')
wenzelm@24630
   150
        else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p'))
wenzelm@23252
   151
     end
wenzelm@23252
   152
  end
wenzelm@23252
   153
 in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s
wenzelm@23252
   154
 end;
wenzelm@23252
   155
wenzelm@23252
   156
(* Monomial division operation. *)
wenzelm@23252
   157
wenzelm@23252
   158
fun mdiv (c1,m1) (c2,m2) =
wenzelm@23252
   159
  (c1//c2,
wenzelm@24630
   160
   map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2);
wenzelm@23252
   161
wenzelm@23252
   162
(* Lowest common multiple of two monomials. *)
wenzelm@23252
   163
wenzelm@24630
   164
fun mlcm (c1,m1) (c2,m2) = (rat_1, ListPair.map Int.max (m1, m2));
wenzelm@23252
   165
wenzelm@23252
   166
(* Reduce monomial cm by polynomial pol, returning replacement for cm.  *)
wenzelm@23252
   167
wenzelm@23252
   168
fun reduce1 cm (pol,hpol) =
wenzelm@23252
   169
  case pol of
wenzelm@23252
   170
    [] => error "reduce1"
wenzelm@23252
   171
  | cm1::cms => ((let val (c,m) = mdiv cm cm1 in
wenzelm@23252
   172
                    (grob_cmul (minus_rat c,m) cms,
wenzelm@23252
   173
                     Mmul((minus_rat c,m),hpol)) end)
wenzelm@23252
   174
                handle  ERROR _ => error "reduce1");
wenzelm@23252
   175
wenzelm@23252
   176
(* Try this for all polynomials in a basis.  *)
wenzelm@23252
   177
fun tryfind f l =
wenzelm@23252
   178
    case l of
wenzelm@23252
   179
        [] => error "tryfind"
wenzelm@23252
   180
      | (h::t) => ((f h) handle ERROR _ => tryfind f t);
wenzelm@23252
   181
wenzelm@23252
   182
fun reduceb cm basis = tryfind (fn p => reduce1 cm p) basis;
wenzelm@23252
   183
wenzelm@23252
   184
(* Reduction of a polynomial (always picking largest monomial possible).     *)
wenzelm@23252
   185
wenzelm@23252
   186
fun reduce basis (pol,hist) =
wenzelm@23252
   187
  case pol of
wenzelm@23252
   188
    [] => (pol,hist)
wenzelm@23252
   189
  | cm::ptl => ((let val (q,hnew) = reduceb cm basis in
wenzelm@23252
   190
                   reduce basis (grob_add q ptl,Add(hnew,hist)) end)
wenzelm@23252
   191
               handle (ERROR _) =>
wenzelm@23252
   192
                   (let val (q,hist') = reduce basis (ptl,hist) in
wenzelm@23252
   193
                       (cm::q,hist') end));
wenzelm@23252
   194
wenzelm@23252
   195
(* Check for orthogonality w.r.t. LCM.                                       *)
wenzelm@23252
   196
wenzelm@23252
   197
fun orthogonal l p1 p2 =
wenzelm@23252
   198
  snd l = snd(grob_mmul (hd p1) (hd p2));
wenzelm@23252
   199
wenzelm@23252
   200
(* Compute S-polynomial of two polynomials.                                  *)
wenzelm@23252
   201
wenzelm@23252
   202
fun spoly cm ph1 ph2 =
wenzelm@23252
   203
  case (ph1,ph2) of
wenzelm@23252
   204
    (([],h),p) => ([],h)
wenzelm@23252
   205
  | (p,([],h)) => ([],h)
wenzelm@23252
   206
  | ((cm1::ptl1,his1),(cm2::ptl2,his2)) =>
wenzelm@23252
   207
        (grob_sub (grob_cmul (mdiv cm cm1) ptl1)
wenzelm@23252
   208
                  (grob_cmul (mdiv cm cm2) ptl2),
wenzelm@23252
   209
         Add(Mmul(mdiv cm cm1,his1),
wenzelm@23252
   210
             Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2)));
wenzelm@23252
   211
wenzelm@23252
   212
(* Make a polynomial monic.                                                  *)
wenzelm@23252
   213
wenzelm@23252
   214
fun monic (pol,hist) =
wenzelm@23579
   215
  if null pol then (pol,hist) else
wenzelm@23252
   216
  let val (c',m') = hd pol in
wenzelm@23252
   217
  (map (fn (c,m) => (c//c',m)) pol,
wenzelm@23252
   218
   Mmul((rat_1 // c',map (K 0) m'),hist)) end;
wenzelm@23252
   219
wenzelm@23252
   220
(* The most popular heuristic is to order critical pairs by LCM monomial.    *)
wenzelm@23252
   221
wenzelm@23252
   222
fun forder ((c1,m1),_) ((c2,m2),_) = morder_lt m1 m2;
wenzelm@23252
   223
wenzelm@23252
   224
fun poly_lt  p q =
wenzelm@23252
   225
  case (p,q) of
wenzelm@23252
   226
    (p,[]) => false
wenzelm@23252
   227
  | ([],q) => true
wenzelm@23252
   228
  | ((c1,m1)::o1,(c2,m2)::o2) =>
wenzelm@23252
   229
        c1 </ c2 orelse
wenzelm@23252
   230
        c1 =/ c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
wenzelm@23252
   231
wenzelm@23252
   232
fun align  ((p,hp),(q,hq)) =
wenzelm@23252
   233
  if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
wenzelm@23252
   234
wenzelm@23252
   235
fun poly_eq p1 p2 =
wenzelm@40718
   236
  eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
wenzelm@23252
   237
wenzelm@23252
   238
fun memx ((p1,h1),(p2,h2)) ppairs =
wenzelm@23252
   239
  not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
wenzelm@23252
   240
wenzelm@23252
   241
(* Buchberger's second criterion.                                            *)
wenzelm@23252
   242
wenzelm@23252
   243
fun criterion2 basis (lcm,((p1,h1),(p2,h2))) opairs =
wenzelm@23252
   244
  exists (fn g => not(poly_eq (fst g) p1) andalso not(poly_eq (fst g) p2) andalso
wenzelm@23252
   245
                   can (mdiv lcm) (hd(fst g)) andalso
wenzelm@23252
   246
                   not(memx (align (g,(p1,h1))) (map snd opairs)) andalso
wenzelm@23252
   247
                   not(memx (align (g,(p2,h2))) (map snd opairs))) basis;
wenzelm@23252
   248
wenzelm@23252
   249
(* Test for hitting constant polynomial.                                     *)
wenzelm@23252
   250
wenzelm@23252
   251
fun constant_poly p =
wenzelm@24630
   252
  length p = 1 andalso forall (fn x => x = 0) (snd(hd p));
wenzelm@23252
   253
wenzelm@23252
   254
(* Grobner basis algorithm.                                                  *)
chaieb@25251
   255
wenzelm@23252
   256
(* FIXME: try to get rid of mergesort? *)
wenzelm@23252
   257
fun merge ord l1 l2 =
wenzelm@23252
   258
 case l1 of
wenzelm@23252
   259
  [] => l2
wenzelm@23252
   260
 | h1::t1 =>
wenzelm@23252
   261
   case l2 of
wenzelm@23252
   262
    [] => l1
wenzelm@23252
   263
   | h2::t2 => if ord h1 h2 then h1::(merge ord t1 l2)
wenzelm@23252
   264
               else h2::(merge ord l1 t2);
wenzelm@23252
   265
fun mergesort ord l =
wenzelm@23252
   266
 let
wenzelm@23252
   267
 fun mergepairs l1 l2 =
wenzelm@23252
   268
  case (l1,l2) of
wenzelm@23252
   269
   ([s],[]) => s
wenzelm@23252
   270
 | (l,[]) => mergepairs [] l
wenzelm@23252
   271
 | (l,[s1]) => mergepairs (s1::l) []
wenzelm@23252
   272
 | (l,(s1::s2::ss)) => mergepairs ((merge ord s1 s2)::l) ss
wenzelm@23579
   273
 in if null l  then []  else mergepairs [] (map (fn x => [x]) l)
wenzelm@23252
   274
 end;
wenzelm@23252
   275
wenzelm@23252
   276
wenzelm@23252
   277
fun grobner_basis basis pairs =
chaieb@25251
   278
 case pairs of
chaieb@25251
   279
   [] => basis
chaieb@25251
   280
 | (l,(p1,p2))::opairs =>
chaieb@25251
   281
   let val (sph as (sp,hist)) = monic (reduce basis (spoly l p1 p2))
wenzelm@41453
   282
   in
chaieb@25251
   283
    if null sp orelse criterion2 basis (l,(p1,p2)) opairs
chaieb@25251
   284
    then grobner_basis basis opairs
chaieb@25251
   285
    else if constant_poly sp then grobner_basis (sph::basis) []
wenzelm@41453
   286
    else
wenzelm@41453
   287
     let
chaieb@25251
   288
      val rawcps = map (fn p => (mlcm (hd(fst p)) (hd sp),align(p,sph)))
chaieb@25251
   289
                              basis
chaieb@25251
   290
      val newcps = filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q)))
chaieb@25251
   291
                        rawcps
chaieb@25251
   292
     in grobner_basis (sph::basis)
chaieb@25251
   293
                 (merge forder opairs (mergesort forder newcps))
chaieb@25251
   294
     end
chaieb@25251
   295
   end;
wenzelm@23252
   296
wenzelm@23252
   297
(* Interreduce initial polynomials.                                          *)
wenzelm@23252
   298
wenzelm@23252
   299
fun grobner_interreduce rpols ipols =
wenzelm@23252
   300
  case ipols of
wenzelm@23252
   301
    [] => map monic (rev rpols)
wenzelm@23252
   302
  | p::ps => let val p' = reduce (rpols @ ps) p in
wenzelm@23579
   303
             if null (fst p') then grobner_interreduce rpols ps
wenzelm@23252
   304
             else grobner_interreduce (p'::rpols) ps end;
wenzelm@23252
   305
wenzelm@23252
   306
(* Overall function.                                                         *)
wenzelm@23252
   307
wenzelm@23252
   308
fun grobner pols =
haftmann@33063
   309
    let val npols = map_index (fn (n, p) => (p, Start n)) pols
wenzelm@23579
   310
        val phists = filter (fn (p,_) => not (null p)) npols
wenzelm@23252
   311
        val bas = grobner_interreduce [] (map monic phists)
haftmann@25538
   312
        val prs0 = map_product pair bas bas
wenzelm@23252
   313
        val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0
wenzelm@23252
   314
        val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1
wenzelm@23252
   315
        val prs3 =
wenzelm@23252
   316
            filter (fn (l,(p,q)) => not(orthogonal l (fst p) (fst q))) prs2 in
wenzelm@23252
   317
        grobner_basis bas (mergesort forder prs3) end;
wenzelm@23252
   318
wenzelm@23252
   319
(* Get proof of contradiction from Grobner basis.                            *)
chaieb@25251
   320
wenzelm@23252
   321
fun find p l =
wenzelm@23252
   322
  case l of
wenzelm@23252
   323
      [] => error "find"
wenzelm@23252
   324
    | (h::t) => if p(h) then h else find p t;
wenzelm@23252
   325
wenzelm@23252
   326
fun grobner_refute pols =
wenzelm@23252
   327
  let val gb = grobner pols in
wenzelm@23252
   328
  snd(find (fn (p,h) => length p = 1 andalso forall (fn x=> x=0) (snd(hd p))) gb)
wenzelm@23252
   329
  end;
wenzelm@23252
   330
wenzelm@23252
   331
(* Turn proof into a certificate as sum of multipliers.                      *)
wenzelm@23252
   332
(* In principle this is very inefficient: in a heavily shared proof it may   *)
wenzelm@23252
   333
(* make the same calculation many times. Could put in a cache or something.  *)
chaieb@25251
   334
wenzelm@23252
   335
fun resolve_proof vars prf =
wenzelm@23252
   336
  case prf of
wenzelm@23252
   337
    Start(~1) => []
wenzelm@23252
   338
  | Start m => [(m,[(rat_1,map (K 0) vars)])]
wenzelm@23252
   339
  | Mmul(pol,lin) =>
wenzelm@23252
   340
        let val lis = resolve_proof vars lin in
wenzelm@23252
   341
            map (fn (n,p) => (n,grob_cmul pol p)) lis end
wenzelm@23252
   342
  | Add(lin1,lin2) =>
wenzelm@23252
   343
        let val lis1 = resolve_proof vars lin1
wenzelm@23252
   344
            val lis2 = resolve_proof vars lin2
haftmann@33042
   345
            val dom = distinct (op =) (union (op =) (map fst lis1) (map fst lis2))
wenzelm@23252
   346
        in
wenzelm@23557
   347
            map (fn n => let val a = these (AList.lookup (op =) lis1 n)
wenzelm@23557
   348
                             val b = these (AList.lookup (op =) lis2 n)
wenzelm@23557
   349
                         in (n,grob_add a b) end) dom end;
wenzelm@23252
   350
wenzelm@23252
   351
(* Run the procedure and produce Weak Nullstellensatz certificate.           *)
chaieb@25251
   352
wenzelm@23252
   353
fun grobner_weak vars pols =
wenzelm@23252
   354
    let val cert = resolve_proof vars (grobner_refute pols)
wenzelm@23252
   355
        val l =
wenzelm@23252
   356
            fold_rev (fold_rev (lcm_rat o denominator_rat o fst) o snd) cert (rat_1) in
wenzelm@23252
   357
        (l,map (fn (i,p) => (i,map (fn (d,m) => (l*/d,m)) p)) cert) end;
wenzelm@23252
   358
wenzelm@23252
   359
(* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)
wenzelm@23252
   360
wenzelm@23252
   361
fun grobner_ideal vars pols pol =
wenzelm@23252
   362
  let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in
chaieb@24913
   363
  if not (null pol') then error "grobner_ideal: not in the ideal" else
wenzelm@23252
   364
  resolve_proof vars h end;
wenzelm@23252
   365
wenzelm@23252
   366
(* Produce Strong Nullstellensatz certificate for a power of pol.            *)
wenzelm@23252
   367
wenzelm@23252
   368
fun grobner_strong vars pols pol =
wenzelm@23252
   369
    let val vars' = @{cterm "True"}::vars
wenzelm@23252
   370
        val grob_z = [(rat_1,1::(map (fn x => 0) vars))]
wenzelm@23252
   371
        val grob_1 = [(rat_1,(map (fn x => 0) vars'))]
wenzelm@23252
   372
        fun augment p= map (fn (c,m) => (c,0::m)) p
wenzelm@23252
   373
        val pols' = map augment pols
wenzelm@23252
   374
        val pol' = augment pol
wenzelm@23252
   375
        val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols'
wenzelm@23252
   376
        val (l,cert) = grobner_weak vars' allpols
wenzelm@33029
   377
        val d = fold (fold (Integer.max o hd o snd) o snd) cert 0
wenzelm@23252
   378
        fun transform_monomial (c,m) =
wenzelm@23252
   379
            grob_cmul (c,tl m) (grob_pow vars pol (d - hd m))
wenzelm@23252
   380
        fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q []
wenzelm@23252
   381
        val cert' = map (fn (c,q) => (c-1,transform_polynomial q))
wenzelm@23252
   382
                        (filter (fn (k,_) => k <> 0) cert) in
wenzelm@23252
   383
        (d,l,cert') end;
wenzelm@23252
   384
wenzelm@23252
   385
wenzelm@23252
   386
(* Overall parametrized universal procedure for (semi)rings.                 *)
wenzelm@23252
   387
(* We return an ideal_conv and the actual ring prover.                       *)
chaieb@25251
   388
wenzelm@23252
   389
fun refute_disj rfn tm =
wenzelm@23252
   390
 case term_of tm of
haftmann@38795
   391
  Const(@{const_name HOL.disj},_)$l$r =>
wenzelm@41453
   392
   Drule.compose_single
wenzelm@41453
   393
    (refute_disj rfn (Thm.dest_arg tm), 2,
wenzelm@41453
   394
      Drule.compose_single (refute_disj rfn (Thm.dest_arg1 tm), 2, disjE))
wenzelm@23252
   395
  | _ => rfn tm ;
wenzelm@23252
   396
haftmann@36713
   397
val notnotD = @{thm notnotD};
wenzelm@46497
   398
fun mk_binop ct x y = Thm.apply (Thm.apply ct x) y
wenzelm@23252
   399
wenzelm@23252
   400
fun is_neg t =
wenzelm@23252
   401
    case term_of t of
haftmann@38558
   402
      (Const(@{const_name Not},_)$p) => true
wenzelm@23252
   403
    | _  => false;
wenzelm@23252
   404
fun is_eq t =
wenzelm@23252
   405
 case term_of t of
haftmann@38864
   406
 (Const(@{const_name HOL.eq},_)$_$_) => true
wenzelm@23252
   407
| _  => false;
wenzelm@23252
   408
wenzelm@23252
   409
fun end_itlist f l =
wenzelm@23252
   410
  case l of
wenzelm@23252
   411
        []     => error "end_itlist"
wenzelm@23252
   412
      | [x]    => x
wenzelm@23252
   413
      | (h::t) => f h (end_itlist f t);
wenzelm@23252
   414
wenzelm@23252
   415
val list_mk_binop = fn b => end_itlist (mk_binop b);
wenzelm@23252
   416
wenzelm@23252
   417
val list_dest_binop = fn b =>
wenzelm@23252
   418
 let fun h acc t =
chaieb@25251
   419
  ((let val (l,r) = dest_binary b t in h (h acc r) l end)
wenzelm@23252
   420
   handle CTERM _ => (t::acc)) (* Why had I handle _ => ? *)
wenzelm@23252
   421
 in h []
wenzelm@23252
   422
 end;
wenzelm@23252
   423
wenzelm@23252
   424
val strip_exists =
wenzelm@23252
   425
 let fun h (acc, t) =
wenzelm@41453
   426
      case term_of t of
wenzelm@41453
   427
       Const (@{const_name Ex}, _) $ Abs (x, T, p) =>
wenzelm@41453
   428
        h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
wenzelm@23252
   429
     | _ => (acc,t)
wenzelm@23252
   430
 in fn t => h ([],t)
wenzelm@23252
   431
 end;
wenzelm@23252
   432
wenzelm@23252
   433
fun is_forall t =
wenzelm@23252
   434
 case term_of t of
haftmann@38558
   435
  (Const(@{const_name All},_)$Abs(_,_,_)) => true
wenzelm@23252
   436
| _ => false;
wenzelm@23252
   437
wenzelm@23252
   438
val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
haftmann@36713
   439
val bool_simps = @{thms bool_simps};
haftmann@36713
   440
val nnf_simps = @{thms nnf_simps};
wenzelm@23252
   441
val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps bool_simps addsimps nnf_simps)
haftmann@36713
   442
val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms weak_dnf_simps});
wenzelm@23252
   443
val initial_conv =
wenzelm@23252
   444
    Simplifier.rewrite
wenzelm@23252
   445
     (HOL_basic_ss addsimps nnf_simps
wenzelm@35410
   446
       addsimps [not_all, not_ex]
wenzelm@35410
   447
       addsimps map (fn th => th RS sym) (@{thms ex_simps} @ @{thms all_simps}));
wenzelm@23252
   448
wenzelm@23252
   449
val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
wenzelm@23252
   450
wenzelm@23252
   451
val cTrp = @{cterm "Trueprop"};
haftmann@38795
   452
val cConj = @{cterm HOL.conj};
wenzelm@23252
   453
val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
wenzelm@46497
   454
val assume_Trueprop = Thm.apply cTrp #> Thm.assume;
wenzelm@23252
   455
val list_mk_conj = list_mk_binop cConj;
wenzelm@23252
   456
val conjs = list_dest_binop cConj;
wenzelm@46497
   457
val mk_neg = Thm.apply cNot;
wenzelm@23252
   458
wenzelm@41453
   459
fun striplist dest =
chaieb@25251
   460
 let
chaieb@25251
   461
  fun h acc x = case try dest x of
chaieb@25251
   462
    SOME (a,b) => h (h acc b) a
chaieb@25251
   463
  | NONE => x::acc
chaieb@25251
   464
 in h [] end;
wenzelm@46497
   465
fun list_mk_binop b = foldr1 (fn (s,t) => Thm.apply (Thm.apply b s) t);
chaieb@25251
   466
chaieb@25251
   467
val eq_commute = mk_meta_eq @{thm eq_commute};
chaieb@25251
   468
wenzelm@41453
   469
fun sym_conv eq =
chaieb@25251
   470
 let val (l,r) = Thm.dest_binop eq
chaieb@25251
   471
 in instantiate' [SOME (ctyp_of_term l)] [SOME l, SOME r] eq_commute
chaieb@25251
   472
 end;
chaieb@25251
   473
chaieb@25251
   474
  (* FIXME : copied from cqe.ML -- complex QE*)
chaieb@25251
   475
fun conjuncts ct =
chaieb@25251
   476
 case term_of ct of
haftmann@38795
   477
  @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
chaieb@25251
   478
| _ => [ct];
chaieb@25251
   479
chaieb@25251
   480
fun fold1 f = foldr1 (uncurry f);
chaieb@25251
   481
wenzelm@46497
   482
val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
chaieb@25251
   483
wenzelm@41453
   484
fun mk_conj_tab th =
wenzelm@41453
   485
 let fun h acc th =
chaieb@25251
   486
   case prop_of th of
wenzelm@41453
   487
   @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
chaieb@25251
   488
     h (h acc (th RS conjunct2)) (th RS conjunct1)
chaieb@25251
   489
  | @{term "Trueprop"}$p => (p,th)::acc
chaieb@25251
   490
in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
chaieb@25251
   491
haftmann@38795
   492
fun is_conj (@{term HOL.conj}$_$_) = true
chaieb@25251
   493
  | is_conj _ = false;
chaieb@25251
   494
wenzelm@41453
   495
fun prove_conj tab cjs =
wenzelm@41453
   496
 case cjs of
chaieb@25251
   497
   [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c
chaieb@25251
   498
 | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
chaieb@25251
   499
wenzelm@41453
   500
fun conj_ac_rule eq =
wenzelm@41453
   501
 let
chaieb@25251
   502
  val (l,r) = Thm.dest_equals eq
wenzelm@46497
   503
  val ctabl = mk_conj_tab (Thm.assume (Thm.apply @{cterm Trueprop} l))
wenzelm@46497
   504
  val ctabr = mk_conj_tab (Thm.assume (Thm.apply @{cterm Trueprop} r))
wenzelm@33035
   505
  fun tabl c = the (Termtab.lookup ctabl (term_of c))
wenzelm@33035
   506
  fun tabr c = the (Termtab.lookup ctabr (term_of c))
chaieb@25251
   507
  val thl  = prove_conj tabl (conjuncts r) |> implies_intr_hyps
chaieb@25251
   508
  val thr  = prove_conj tabr (conjuncts l) |> implies_intr_hyps
chaieb@25251
   509
  val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI}
wenzelm@41453
   510
 in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
chaieb@25251
   511
chaieb@25251
   512
 (* END FIXME.*)
chaieb@25251
   513
wenzelm@41453
   514
   (* Conversion for the equivalence of existential statements where
chaieb@25251
   515
      EX quantifiers are rearranged differently *)
wenzelm@41453
   516
 fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
wenzelm@46497
   517
 fun mk_ex v t = Thm.apply (ext (ctyp_of_term v)) (Thm.lambda v t)
chaieb@25251
   518
wenzelm@41453
   519
fun choose v th th' = case concl_of th of
wenzelm@41453
   520
  @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
chaieb@25251
   521
   let
chaieb@25251
   522
    val p = (funpow 2 Thm.dest_arg o cprop_of) th
chaieb@25251
   523
    val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
wenzelm@41453
   524
    val th0 = Conv.fconv_rule (Thm.beta_conversion true)
chaieb@25251
   525
        (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
wenzelm@41453
   526
    val pv = (Thm.rhs_of o Thm.beta_conversion true)
wenzelm@46497
   527
          (Thm.apply @{cterm Trueprop} (Thm.apply p v))
wenzelm@41453
   528
    val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
wenzelm@41453
   529
   in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
wenzelm@41453
   530
| _ => error ""  (* FIXME ? *)
chaieb@25251
   531
wenzelm@41453
   532
fun simple_choose v th =
wenzelm@46497
   533
   choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v)
wenzelm@41453
   534
    ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
chaieb@25251
   535
chaieb@25251
   536
wenzelm@41453
   537
 fun mkexi v th =
wenzelm@41453
   538
  let
wenzelm@46497
   539
   val p = Thm.lambda v (Thm.dest_arg (Thm.cprop_of th))
wenzelm@41453
   540
  in Thm.implies_elim
wenzelm@41453
   541
    (Conv.fconv_rule (Thm.beta_conversion true)
wenzelm@41453
   542
      (instantiate' [SOME (ctyp_of_term v)] [SOME p, SOME v] @{thm exI}))
chaieb@25251
   543
      th
chaieb@25251
   544
  end
wenzelm@41453
   545
 fun ex_eq_conv t =
wenzelm@41453
   546
  let
chaieb@25251
   547
  val (p0,q0) = Thm.dest_binop t
wenzelm@41453
   548
  val (vs',P) = strip_exists p0
wenzelm@41453
   549
  val (vs,_) = strip_exists q0
wenzelm@46497
   550
   val th = Thm.assume (Thm.apply @{cterm Trueprop} P)
wenzelm@41453
   551
   val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th))
wenzelm@41453
   552
   val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
chaieb@25251
   553
   val p = (Thm.dest_arg o Thm.dest_arg1 o cprop_of) th1
chaieb@25251
   554
   val q = (Thm.dest_arg o Thm.dest_arg o cprop_of) th1
wenzelm@41453
   555
  in Thm.implies_elim (Thm.implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2
chaieb@25251
   556
     |> mk_meta_eq
chaieb@25251
   557
  end;
chaieb@25251
   558
chaieb@25251
   559
wenzelm@41453
   560
 fun getname v = case term_of v of
chaieb@25251
   561
  Free(s,_) => s
chaieb@25251
   562
 | Var ((s,_),_) => s
chaieb@25251
   563
 | _ => "x"
wenzelm@46497
   564
 fun mk_eq s t = Thm.apply (Thm.apply @{cterm "op == :: bool => _"} s) t
wenzelm@46497
   565
 fun mkeq s t = Thm.apply @{cterm Trueprop} (Thm.apply (Thm.apply @{cterm "op = :: bool => _"} s) t)
wenzelm@41453
   566
 fun mk_exists v th = Drule.arg_cong_rule (ext (ctyp_of_term v))
chaieb@25251
   567
   (Thm.abstract_rule (getname v) v th)
wenzelm@41453
   568
 val simp_ex_conv =
chaieb@25251
   569
     Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms(39)})
chaieb@25251
   570
chaieb@25251
   571
fun frees t = Thm.add_cterm_frees t [];
chaieb@25251
   572
fun free_in v t = member op aconvc (frees t) v;
chaieb@25251
   573
chaieb@25251
   574
val vsubst = let
wenzelm@41453
   575
 fun vsubst (t,v) tm =
wenzelm@46497
   576
   (Thm.rhs_of o Thm.beta_conversion false) (Thm.apply (Thm.lambda v tm) t)
chaieb@25251
   577
in fold vsubst end;
wenzelm@23252
   578
wenzelm@23252
   579
wenzelm@23252
   580
(** main **)
wenzelm@23252
   581
wenzelm@23252
   582
fun ring_and_ideal_conv
wenzelm@41453
   583
  {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
chaieb@30866
   584
   field = (f_ops, f_rules), idom, ideal}
wenzelm@23252
   585
  dest_const mk_const ring_eq_conv ring_normalize_conv =
wenzelm@23252
   586
let
wenzelm@23252
   587
  val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
wenzelm@23252
   588
  val [ring_add_tm, ring_mul_tm, ring_pow_tm] =
wenzelm@41453
   589
    map Thm.dest_fun2 [add_pat, mul_pat, pow_pat];
wenzelm@23252
   590
wenzelm@23252
   591
  val (ring_sub_tm, ring_neg_tm) =
wenzelm@23252
   592
    (case r_ops of
wenzelm@41453
   593
     [sub_pat, neg_pat] => (Thm.dest_fun2 sub_pat, Thm.dest_fun neg_pat)
chaieb@30866
   594
    |_  => (@{cterm "True"}, @{cterm "True"}));
chaieb@30866
   595
chaieb@30866
   596
  val (field_div_tm, field_inv_tm) =
chaieb@30866
   597
    (case f_ops of
wenzelm@41453
   598
       [div_pat, inv_pat] => (Thm.dest_fun2 div_pat, Thm.dest_fun inv_pat)
chaieb@30866
   599
     | _ => (@{cterm "True"}, @{cterm "True"}));
wenzelm@23252
   600
wenzelm@23252
   601
  val [idom_thm, neq_thm] = idom;
wenzelm@41453
   602
  val [idl_sub, idl_add0] =
chaieb@25251
   603
     if length ideal = 2 then ideal else [eq_commute, eq_commute]
chaieb@30866
   604
  fun ring_dest_neg t =
wenzelm@41453
   605
    let val (l,r) = Thm.dest_comb t
wenzelm@41453
   606
    in if Term.could_unify(term_of l,term_of ring_neg_tm) then r
chaieb@30866
   607
       else raise CTERM ("ring_dest_neg", [t])
chaieb@30866
   608
    end
wenzelm@23252
   609
wenzelm@46497
   610
 val ring_mk_neg = fn tm => Thm.apply (ring_neg_tm) (tm);
chaieb@30866
   611
 fun field_dest_inv t =
wenzelm@41453
   612
    let val (l,r) = Thm.dest_comb t in
wenzelm@41453
   613
        if Term.could_unify(term_of l, term_of field_inv_tm) then r
chaieb@30866
   614
        else raise CTERM ("field_dest_inv", [t])
wenzelm@23252
   615
    end
chaieb@25251
   616
 val ring_dest_add = dest_binary ring_add_tm;
wenzelm@23252
   617
 val ring_mk_add = mk_binop ring_add_tm;
chaieb@25251
   618
 val ring_dest_sub = dest_binary ring_sub_tm;
wenzelm@23252
   619
 val ring_mk_sub = mk_binop ring_sub_tm;
chaieb@25251
   620
 val ring_dest_mul = dest_binary ring_mul_tm;
wenzelm@23252
   621
 val ring_mk_mul = mk_binop ring_mul_tm;
chaieb@30866
   622
 val field_dest_div = dest_binary field_div_tm;
chaieb@30866
   623
 val field_mk_div = mk_binop field_div_tm;
chaieb@25251
   624
 val ring_dest_pow = dest_binary ring_pow_tm;
wenzelm@23252
   625
 val ring_mk_pow = mk_binop ring_pow_tm ;
wenzelm@23252
   626
 fun grobvars tm acc =
wenzelm@23252
   627
    if can dest_const tm then acc
wenzelm@41453
   628
    else if can ring_dest_neg tm then grobvars (Thm.dest_arg tm) acc
wenzelm@41453
   629
    else if can ring_dest_pow tm then grobvars (Thm.dest_arg1 tm) acc
wenzelm@23252
   630
    else if can ring_dest_add tm orelse can ring_dest_sub tm
wenzelm@23252
   631
            orelse can ring_dest_mul tm
wenzelm@41453
   632
    then grobvars (Thm.dest_arg1 tm) (grobvars (Thm.dest_arg tm) acc)
chaieb@30866
   633
    else if can field_dest_inv tm
chaieb@30866
   634
         then
wenzelm@41453
   635
          let val gvs = grobvars (Thm.dest_arg tm) []
chaieb@30866
   636
          in if null gvs then acc else tm::acc
chaieb@30866
   637
          end
chaieb@30866
   638
    else if can field_dest_div tm then
wenzelm@41453
   639
         let val lvs = grobvars (Thm.dest_arg1 tm) acc
wenzelm@41453
   640
             val gvs = grobvars (Thm.dest_arg tm) []
chaieb@30866
   641
          in if null gvs then lvs else tm::acc
wenzelm@41453
   642
          end
wenzelm@23252
   643
    else tm::acc ;
wenzelm@23252
   644
wenzelm@23252
   645
fun grobify_term vars tm =
wenzelm@23252
   646
((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
wenzelm@23252
   647
     [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
wenzelm@23252
   648
handle  CTERM _ =>
wenzelm@23252
   649
 ((let val x = dest_const tm
wenzelm@23252
   650
 in if x =/ rat_0 then [] else [(x,map (fn v => 0) vars)]
wenzelm@23252
   651
 end)
wenzelm@23252
   652
 handle ERROR _ =>
wenzelm@23252
   653
  ((grob_neg(grobify_term vars (ring_dest_neg tm)))
wenzelm@23252
   654
  handle CTERM _ =>
wenzelm@23252
   655
   (
chaieb@30866
   656
   (grob_inv(grobify_term vars (field_dest_inv tm)))
wenzelm@41453
   657
   handle CTERM _ =>
wenzelm@23252
   658
    ((let val (l,r) = ring_dest_add tm
wenzelm@23252
   659
    in grob_add (grobify_term vars l) (grobify_term vars r)
wenzelm@23252
   660
    end)
wenzelm@23252
   661
    handle CTERM _ =>
wenzelm@23252
   662
     ((let val (l,r) = ring_dest_sub tm
wenzelm@23252
   663
     in grob_sub (grobify_term vars l) (grobify_term vars r)
wenzelm@23252
   664
     end)
wenzelm@23252
   665
     handle  CTERM _ =>
wenzelm@23252
   666
      ((let val (l,r) = ring_dest_mul tm
wenzelm@23252
   667
      in grob_mul (grobify_term vars l) (grobify_term vars r)
wenzelm@23252
   668
      end)
wenzelm@23252
   669
       handle CTERM _ =>
chaieb@30866
   670
        (  (let val (l,r) = field_dest_div tm
wenzelm@23252
   671
          in grob_div (grobify_term vars l) (grobify_term vars r)
wenzelm@23252
   672
          end)
chaieb@30866
   673
         handle CTERM _ =>
wenzelm@23252
   674
          ((let val (l,r) = ring_dest_pow tm
wenzelm@23252
   675
          in grob_pow vars (grobify_term vars l) ((term_of #> HOLogic.dest_number #> snd) r)
wenzelm@23252
   676
          end)
wenzelm@23252
   677
           handle CTERM _ => error "grobify_term: unknown or invalid term")))))))));
wenzelm@41453
   678
val eq_tm = idom_thm |> concl |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_fun2;
chaieb@25251
   679
val dest_eq = dest_binary eq_tm;
wenzelm@23252
   680
wenzelm@23252
   681
fun grobify_equation vars tm =
chaieb@25251
   682
    let val (l,r) = dest_binary eq_tm tm
wenzelm@23252
   683
    in grob_sub (grobify_term vars l) (grobify_term vars r)
wenzelm@23252
   684
    end;
wenzelm@23252
   685
wenzelm@23252
   686
fun grobify_equations tm =
wenzelm@23252
   687
 let
wenzelm@23252
   688
  val cjs = conjs tm
wenzelm@41453
   689
  val  rawvars =
wenzelm@41453
   690
    fold_rev (fn eq => fn a => grobvars (Thm.dest_arg1 eq) (grobvars (Thm.dest_arg eq) a)) cjs []
wenzelm@41453
   691
  val vars = sort (fn (x, y) => Term_Ord.term_ord (term_of x, term_of y))
wenzelm@23252
   692
                  (distinct (op aconvc) rawvars)
wenzelm@23252
   693
 in (vars,map (grobify_equation vars) cjs)
wenzelm@23252
   694
 end;
wenzelm@23252
   695
wenzelm@23252
   696
val holify_polynomial =
wenzelm@23252
   697
 let fun holify_varpow (v,n) =
haftmann@37388
   698
  if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp nat} n)  (* FIXME *)
wenzelm@23252
   699
 fun holify_monomial vars (c,m) =
wenzelm@24630
   700
  let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
wenzelm@23252
   701
   in end_itlist ring_mk_mul (mk_const c :: xps)
wenzelm@23252
   702
  end
wenzelm@23252
   703
 fun holify_polynomial vars p =
wenzelm@23579
   704
     if null p then mk_const (rat_0)
wenzelm@23252
   705
     else end_itlist ring_mk_add (map (holify_monomial vars) p)
wenzelm@23252
   706
 in holify_polynomial
wenzelm@23252
   707
 end ;
wenzelm@23252
   708
val idom_rule = simplify (HOL_basic_ss addsimps [idom_thm]);
wenzelm@23252
   709
fun prove_nz n = eqF_elim
wenzelm@23252
   710
                 (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const(rat_0))));
wenzelm@23252
   711
val neq_01 = prove_nz (rat_1);
wenzelm@23252
   712
fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
wenzelm@41453
   713
fun mk_add th1 = Thm.combination (Drule.arg_cong_rule ring_add_tm th1);
wenzelm@23252
   714
wenzelm@23252
   715
fun refute tm =
wenzelm@23557
   716
 if tm aconvc false_tm then assume_Trueprop tm else
chaieb@29800
   717
 ((let
wenzelm@23557
   718
   val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm))
wenzelm@41453
   719
   val  nths = filter (is_eq o Thm.dest_arg o concl) nths0
wenzelm@23252
   720
   val eths = filter (is_eq o concl) eths0
wenzelm@23252
   721
  in
wenzelm@23252
   722
   if null eths then
wenzelm@23252
   723
    let
wenzelm@23557
   724
      val th1 = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths
wenzelm@41453
   725
      val th2 =
wenzelm@41453
   726
        Conv.fconv_rule
wenzelm@41453
   727
          ((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
wenzelm@41453
   728
      val conc = th2 |> concl |> Thm.dest_arg
wenzelm@23252
   729
      val (l,r) = conc |> dest_eq
wenzelm@46497
   730
    in Thm.implies_intr (Thm.apply cTrp tm)
wenzelm@41453
   731
                    (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2))
wenzelm@41453
   732
                           (Thm.reflexive l |> mk_object_eq))
wenzelm@23252
   733
    end
wenzelm@23252
   734
   else
wenzelm@23252
   735
   let
wenzelm@23252
   736
    val (vars,l,cert,noteqth) =(
wenzelm@23252
   737
     if null nths then
wenzelm@23252
   738
      let val (vars,pols) = grobify_equations(list_mk_conj(map concl eths))
wenzelm@23252
   739
          val (l,cert) = grobner_weak vars pols
wenzelm@23252
   740
      in (vars,l,cert,neq_01)
wenzelm@23252
   741
      end
wenzelm@23252
   742
     else
wenzelm@23252
   743
      let
wenzelm@23557
   744
       val nth = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths
wenzelm@23252
   745
       val (vars,pol::pols) =
wenzelm@41453
   746
          grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
wenzelm@23252
   747
       val (deg,l,cert) = grobner_strong vars pols pol
wenzelm@41453
   748
       val th1 =
wenzelm@41453
   749
        Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) nth
wenzelm@24630
   750
       val th2 = funpow deg (idom_rule o HOLogic.conj_intr th1) neq_01
wenzelm@23252
   751
      in (vars,l,cert,th2)
wenzelm@23252
   752
      end)
wenzelm@23252
   753
    val cert_pos = map (fn (i,p) => (i,filter (fn (c,m) => c >/ rat_0) p)) cert
wenzelm@23252
   754
    val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
wenzelm@23252
   755
                                            (filter (fn (c,m) => c </ rat_0) p))) cert
wenzelm@23252
   756
    val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
wenzelm@23252
   757
    val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
wenzelm@23252
   758
    fun thm_fn pols =
wenzelm@41453
   759
        if null pols then Thm.reflexive(mk_const rat_0) else
wenzelm@23252
   760
        end_itlist mk_add
wenzelm@46497
   761
            (map (fn (i,p) => Drule.arg_cong_rule (Thm.apply ring_mul_tm p)
wenzelm@24630
   762
              (nth eths i |> mk_meta_eq)) pols)
wenzelm@23252
   763
    val th1 = thm_fn herts_pos
wenzelm@23252
   764
    val th2 = thm_fn herts_neg
wenzelm@41453
   765
    val th3 = HOLogic.conj_intr(mk_add (Thm.symmetric th1) th2 |> mk_object_eq) noteqth
wenzelm@41453
   766
    val th4 =
wenzelm@41453
   767
      Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
wenzelm@41453
   768
        (neq_rule l th3)
wenzelm@41453
   769
    val (l,r) = dest_eq(Thm.dest_arg(concl th4))
wenzelm@46497
   770
   in Thm.implies_intr (Thm.apply cTrp tm)
wenzelm@41453
   771
                        (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4))
wenzelm@41453
   772
                   (Thm.reflexive l |> mk_object_eq))
wenzelm@23252
   773
   end
wenzelm@41453
   774
  end) handle ERROR _ => raise CTERM ("Groebner-refute: unable to refute",[tm]))
wenzelm@23252
   775
wenzelm@23252
   776
fun ring tm =
wenzelm@23252
   777
 let
wenzelm@23252
   778
  fun mk_forall x p =
wenzelm@46497
   779
    Thm.apply
wenzelm@41453
   780
      (Drule.cterm_rule (instantiate' [SOME (ctyp_of_term x)] [])
wenzelm@46497
   781
        @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
wenzelm@41453
   782
  val avs = Thm.add_cterm_frees tm []
wenzelm@23252
   783
  val P' = fold mk_forall avs tm
wenzelm@23252
   784
  val th1 = initial_conv(mk_neg P')
wenzelm@23252
   785
  val (evs,bod) = strip_exists(concl th1) in
chaieb@25251
   786
   if is_forall bod then raise CTERM("ring: non-universal formula",[tm])
wenzelm@23252
   787
   else
wenzelm@23252
   788
   let
wenzelm@23252
   789
    val th1a = weak_dnf_conv bod
wenzelm@23252
   790
    val boda = concl th1a
wenzelm@23252
   791
    val th2a = refute_disj refute boda
wenzelm@23252
   792
    val th2b = [mk_object_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans
wenzelm@41453
   793
    val th2 = fold (fn v => fn th => (Thm.forall_intr v th) COMP allI) evs (th2b RS PFalse)
wenzelm@41453
   794
    val th3 =
wenzelm@41453
   795
      Thm.equal_elim
wenzelm@41453
   796
        (Simplifier.rewrite (HOL_basic_ss addsimps [not_ex RS sym]) (th2 |> cprop_of)) th2
wenzelm@23252
   797
    in specl avs
wenzelm@23252
   798
             ([[[mk_object_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD)
wenzelm@23252
   799
   end
wenzelm@23252
   800
 end
wenzelm@23252
   801
fun ideal tms tm ord =
wenzelm@23252
   802
 let
wenzelm@23252
   803
  val rawvars = fold_rev grobvars (tm::tms) []
wenzelm@23252
   804
  val vars = sort ord (distinct (fn (x,y) => (term_of x) aconv (term_of y)) rawvars)
wenzelm@23252
   805
  val pols = map (grobify_term vars) tms
wenzelm@23252
   806
  val pol = grobify_term vars tm
wenzelm@23252
   807
  val cert = grobner_ideal vars pols pol
haftmann@33063
   808
 in map_range (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
haftmann@33063
   809
   (length pols)
wenzelm@23252
   810
 end
chaieb@25251
   811
wenzelm@41453
   812
fun poly_eq_conv t =
chaieb@25251
   813
 let val (a,b) = Thm.dest_binop t
wenzelm@41453
   814
 in Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv ring_normalize_conv))
chaieb@25251
   815
     (instantiate' [] [SOME a, SOME b] idl_sub)
chaieb@25251
   816
 end
wenzelm@41453
   817
 val poly_eq_simproc =
wenzelm@41453
   818
  let
wenzelm@41453
   819
   fun proc phi  ss t =
chaieb@25251
   820
    let val th = poly_eq_conv t
chaieb@25251
   821
    in if Thm.is_reflexive th then NONE else SOME th
chaieb@25251
   822
    end
wenzelm@41453
   823
   in make_simproc {lhss = [Thm.lhs_of idl_sub],
chaieb@25251
   824
                name = "poly_eq_simproc", proc = proc, identifier = []}
chaieb@25251
   825
   end;
wenzelm@35410
   826
  val poly_eq_ss = HOL_basic_ss addsimps @{thms simp_thms}
chaieb@25251
   827
                        addsimprocs [poly_eq_simproc]
chaieb@25251
   828
chaieb@25251
   829
 local
chaieb@25251
   830
  fun is_defined v t =
wenzelm@41453
   831
  let
wenzelm@41453
   832
   val mons = striplist(dest_binary ring_add_tm) t
wenzelm@41453
   833
  in member (op aconvc) mons v andalso
wenzelm@41453
   834
    forall (fn m => v aconvc m
chaieb@25251
   835
          orelse not(member (op aconvc) (Thm.add_cterm_frees m []) v)) mons
chaieb@25251
   836
  end
chaieb@25251
   837
chaieb@25251
   838
  fun isolate_variable vars tm =
wenzelm@41453
   839
  let
chaieb@25251
   840
   val th = poly_eq_conv tm
chaieb@25251
   841
   val th' = (sym_conv then_conv poly_eq_conv) tm
wenzelm@41453
   842
   val (v,th1) =
chaieb@25251
   843
   case find_first(fn v=> is_defined v (Thm.dest_arg1 (Thm.rhs_of th))) vars of
chaieb@25251
   844
    SOME v => (v,th')
wenzelm@41453
   845
   | NONE => (the (find_first
chaieb@25251
   846
          (fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th)
wenzelm@41453
   847
   val th2 = Thm.transitive th1
wenzelm@41453
   848
        (instantiate' []  [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v]
chaieb@25251
   849
          idl_add0)
wenzelm@41453
   850
   in Conv.fconv_rule(funpow 2 Conv.arg_conv ring_normalize_conv) th2
chaieb@25251
   851
   end
chaieb@25251
   852
 in
chaieb@25251
   853
 fun unwind_polys_conv tm =
wenzelm@41453
   854
 let
chaieb@25251
   855
  val (vars,bod) = strip_exists tm
haftmann@38795
   856
  val cjs = striplist (dest_binary @{cterm HOL.conj}) bod
wenzelm@41453
   857
  val th1 = (the (get_first (try (isolate_variable vars)) cjs)
chaieb@25251
   858
             handle Option => raise CTERM ("unwind_polys_conv",[tm]))
chaieb@25251
   859
  val eq = Thm.lhs_of th1
haftmann@38795
   860
  val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs))
chaieb@25251
   861
  val th2 = conj_ac_rule (mk_eq bod bod')
wenzelm@41453
   862
  val th3 =
wenzelm@41453
   863
    Thm.transitive th2
wenzelm@41453
   864
      (Drule.binop_cong_rule @{cterm HOL.conj} th1
wenzelm@41453
   865
        (Thm.reflexive (Thm.dest_arg (Thm.rhs_of th2))))
chaieb@25251
   866
  val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
chaieb@25251
   867
  val vars' = (remove op aconvc v vars) @ [v]
wenzelm@41453
   868
  val th4 = Conv.fconv_rule (Conv.arg_conv simp_ex_conv) (mk_exists v th3)
chaieb@25251
   869
  val th5 = ex_eq_conv (mk_eq tm (fold mk_ex (remove op aconvc v vars) (Thm.lhs_of th4)))
wenzelm@41453
   870
 in Thm.transitive th5 (fold mk_exists (remove op aconvc v vars) th4)
chaieb@25251
   871
 end;
chaieb@25251
   872
end
chaieb@25251
   873
chaieb@25251
   874
local
chaieb@25251
   875
 fun scrub_var v m =
wenzelm@41453
   876
  let
wenzelm@41453
   877
   val ps = striplist ring_dest_mul m
chaieb@25251
   878
   val ps' = remove op aconvc v ps
chaieb@25251
   879
  in if null ps' then one_tm else fold1 ring_mk_mul ps'
chaieb@25251
   880
  end
chaieb@25251
   881
 fun find_multipliers v mons =
wenzelm@41453
   882
  let
wenzelm@41453
   883
   val mons1 = filter (fn m => free_in v m) mons
wenzelm@41453
   884
   val mons2 = map (scrub_var v) mons1
chaieb@25251
   885
   in  if null mons2 then zero_tm else fold1 ring_mk_add mons2
chaieb@25251
   886
  end
chaieb@25251
   887
chaieb@25251
   888
 fun isolate_monomials vars tm =
wenzelm@41453
   889
 let
chaieb@25251
   890
  val (cmons,vmons) =
haftmann@33049
   891
    List.partition (fn m => null (inter (op aconvc) vars (frees m)))
chaieb@25251
   892
                   (striplist ring_dest_add tm)
chaieb@25251
   893
  val cofactors = map (fn v => find_multipliers v vmons) vars
chaieb@25251
   894
  val cnc = if null cmons then zero_tm
wenzelm@46497
   895
             else Thm.apply ring_neg_tm
wenzelm@41453
   896
                    (list_mk_binop ring_add_tm cmons)
chaieb@25251
   897
  in (cofactors,cnc)
chaieb@25251
   898
  end;
chaieb@25251
   899
chaieb@25251
   900
fun isolate_variables evs ps eq =
wenzelm@41453
   901
 let
chaieb@25251
   902
  val vars = filter (fn v => free_in v eq) evs
chaieb@25251
   903
  val (qs,p) = isolate_monomials vars eq
wenzelm@41453
   904
  val rs = ideal (qs @ ps) p
wenzelm@35408
   905
              (fn (s,t) => Term_Ord.term_ord (term_of s, term_of t))
haftmann@33957
   906
 in (eq, take (length qs) rs ~~ vars)
chaieb@25251
   907
 end;
chaieb@25251
   908
 fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
chaieb@25251
   909
in
chaieb@25251
   910
 fun solve_idealism evs ps eqs =
chaieb@25251
   911
  if null evs then [] else
wenzelm@41453
   912
  let
wenzelm@33035
   913
   val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> the
chaieb@25251
   914
   val evs' = subtract op aconvc evs (map snd cfs)
chaieb@25251
   915
   val eqs' = map (subst_in_poly cfs) (remove op aconvc eq eqs)
chaieb@25251
   916
  in cfs @ solve_idealism evs' ps eqs'
chaieb@25251
   917
  end;
chaieb@25251
   918
end;
chaieb@25251
   919
chaieb@25251
   920
wenzelm@41453
   921
in {ring_conv = ring, simple_ideal = ideal, multi_ideal = solve_idealism,
chaieb@25251
   922
    poly_eq_ss = poly_eq_ss, unwind_conv = unwind_polys_conv}
wenzelm@23252
   923
end;
wenzelm@23252
   924
wenzelm@23252
   925
wenzelm@23252
   926
fun find_term bounds tm =
wenzelm@23252
   927
  (case term_of tm of
haftmann@38864
   928
    Const (@{const_name HOL.eq}, T) $ _ $ _ =>
wenzelm@23252
   929
      if domain_type T = HOLogic.boolT then find_args bounds tm
wenzelm@41453
   930
      else Thm.dest_arg tm
wenzelm@41453
   931
  | Const (@{const_name Not}, _) $ _ => find_term bounds (Thm.dest_arg tm)
wenzelm@41453
   932
  | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
wenzelm@41453
   933
  | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
haftmann@38795
   934
  | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
haftmann@38795
   935
  | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
haftmann@38786
   936
  | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
chaieb@25251
   937
  | @{term "op ==>"} $_$_ => find_args bounds tm
chaieb@25251
   938
  | Const("op ==",_)$_$_ => find_args bounds tm
wenzelm@41453
   939
  | @{term Trueprop}$_ => find_term bounds (Thm.dest_arg tm)
wenzelm@23252
   940
  | _ => raise TERM ("find_term", []))
wenzelm@23252
   941
and find_args bounds tm =
wenzelm@23252
   942
  let val (t, u) = Thm.dest_binop tm
wenzelm@23252
   943
  in (find_term bounds t handle TERM _ => find_term bounds u) end
wenzelm@23252
   944
and find_body bounds b =
wenzelm@41453
   945
  let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
wenzelm@23252
   946
  in find_term (bounds + 1) b' end;
wenzelm@23252
   947
chaieb@25251
   948
wenzelm@41453
   949
fun get_ring_ideal_convs ctxt form =
chaieb@25251
   950
 case try (find_term 0) form of
chaieb@25251
   951
  NONE => NONE
chaieb@25251
   952
| SOME tm =>
haftmann@36752
   953
  (case Semiring_Normalizer.match ctxt tm of
chaieb@25251
   954
    NONE => NONE
wenzelm@41453
   955
  | SOME (res as (theory, {is_const, dest_const,
chaieb@25251
   956
          mk_const, conv = ring_eq_conv})) =>
chaieb@25251
   957
     SOME (ring_and_ideal_conv theory
chaieb@25251
   958
          dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
haftmann@36752
   959
          (Semiring_Normalizer.semiring_normalize_wrapper ctxt res)))
chaieb@25251
   960
wenzelm@23579
   961
fun ring_solve ctxt form =
wenzelm@23252
   962
  (case try (find_term 0 (* FIXME !? *)) form of
wenzelm@41453
   963
    NONE => Thm.reflexive form
wenzelm@23252
   964
  | SOME tm =>
haftmann@36752
   965
      (case Semiring_Normalizer.match ctxt tm of
wenzelm@41453
   966
        NONE => Thm.reflexive form
wenzelm@23252
   967
      | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) =>
chaieb@25251
   968
        #ring_conv (ring_and_ideal_conv theory
chaieb@25251
   969
          dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
haftmann@36752
   970
          (Semiring_Normalizer.semiring_normalize_wrapper ctxt res)) form));
wenzelm@23252
   971
haftmann@36702
   972
fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (Simplifier.context ctxt
haftmann@36702
   973
  (HOL_basic_ss addsimps (Algebra_Simplification.get ctxt) delsimps del_thms addsimps add_thms));
haftmann@36702
   974
wenzelm@23579
   975
fun ring_tac add_ths del_ths ctxt =
wenzelm@35625
   976
  Object_Logic.full_atomize_tac
haftmann@36702
   977
  THEN' presimplify ctxt add_ths del_ths
wenzelm@23579
   978
  THEN' CSUBGOAL (fn (p, i) =>
wenzelm@35625
   979
    rtac (let val form = Object_Logic.dest_judgment p
chaieb@25251
   980
          in case get_ring_ideal_convs ctxt form of
wenzelm@41453
   981
           NONE => Thm.reflexive form
chaieb@25251
   982
          | SOME thy => #ring_conv thy form
chaieb@25251
   983
          end) i
wenzelm@23579
   984
      handle TERM _ => no_tac
wenzelm@23579
   985
        | CTERM _ => no_tac
wenzelm@23579
   986
        | THM _ => no_tac);
chaieb@23334
   987
chaieb@25251
   988
local
chaieb@25251
   989
 fun lhs t = case term_of t of
haftmann@38864
   990
  Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
chaieb@25251
   991
 | _=> raise CTERM ("ideal_tac - lhs",[t])
chaieb@25251
   992
 fun exitac NONE = no_tac
chaieb@25251
   993
   | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
wenzelm@41453
   994
in
wenzelm@41453
   995
fun ideal_tac add_ths del_ths ctxt =
haftmann@36702
   996
  presimplify ctxt add_ths del_ths
chaieb@27671
   997
 THEN'
chaieb@25251
   998
 CSUBGOAL (fn (p, i) =>
chaieb@25251
   999
  case get_ring_ideal_convs ctxt p of
chaieb@25251
  1000
   NONE => no_tac
wenzelm@41453
  1001
 | SOME thy =>
chaieb@25251
  1002
  let
chaieb@25251
  1003
   fun poly_exists_tac {asms = asms, concl = concl, prems = prems,
wenzelm@41453
  1004
            params = params, context = ctxt, schematics = scs} =
chaieb@25251
  1005
    let
chaieb@25251
  1006
     val (evs,bod) = strip_exists (Thm.dest_arg concl)
wenzelm@41453
  1007
     val ps = map_filter (try (lhs o Thm.dest_arg)) asms
wenzelm@41453
  1008
     val cfs = (map swap o #multi_ideal thy evs ps)
chaieb@25251
  1009
                   (map Thm.dest_arg1 (conjuncts bod))
chaieb@25251
  1010
     val ws = map (exitac o AList.lookup op aconvc cfs) evs
wenzelm@41453
  1011
    in EVERY (rev ws) THEN Method.insert_tac prems 1
chaieb@25251
  1012
        THEN ring_tac add_ths del_ths ctxt 1
chaieb@25251
  1013
   end
wenzelm@41453
  1014
  in
wenzelm@42793
  1015
     clarify_tac @{context} i
wenzelm@41453
  1016
     THEN Object_Logic.full_atomize_tac i
wenzelm@41453
  1017
     THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i
wenzelm@42793
  1018
     THEN clarify_tac @{context} i
chaieb@25251
  1019
     THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
chaieb@25251
  1020
     THEN SUBPROOF poly_exists_tac ctxt i
chaieb@25251
  1021
  end
chaieb@25251
  1022
 handle TERM _ => no_tac
chaieb@25251
  1023
     | CTERM _ => no_tac
wenzelm@41453
  1024
     | THM _ => no_tac);
wenzelm@23252
  1025
end;
chaieb@25251
  1026
wenzelm@41453
  1027
fun algebra_tac add_ths del_ths ctxt i =
chaieb@25251
  1028
 ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i
wenzelm@41453
  1029
haftmann@36723
  1030
local
haftmann@36723
  1031
haftmann@36723
  1032
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
haftmann@36723
  1033
val addN = "add"
haftmann@36723
  1034
val delN = "del"
haftmann@36723
  1035
val any_keyword = keyword addN || keyword delN
haftmann@36723
  1036
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
haftmann@36723
  1037
haftmann@36723
  1038
in
haftmann@36723
  1039
wenzelm@41453
  1040
val algebra_method = ((Scan.optional (keyword addN |-- thms) []) --
haftmann@36723
  1041
   (Scan.optional (keyword delN |-- thms) [])) >>
haftmann@36723
  1042
  (fn (add_ths, del_ths) => fn ctxt =>
haftmann@36723
  1043
       SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt))
chaieb@25251
  1044
chaieb@25251
  1045
end;
haftmann@36723
  1046
haftmann@36723
  1047
end;