src/HOL/Tools/Qelim/cooper.ML
author haftmann
Mon May 10 15:33:32 2010 +0200 (2010-05-10)
changeset 36807 abcfc8372694
parent 36806 fc27b0465a4c
child 36831 3037d6810fca
permissions -rw-r--r--
tuned; dropped strange myassoc2
     1 (*  Title:      HOL/Tools/Qelim/cooper.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3 
     4 Presburger arithmetic by Cooper's algorithm.
     5 *)
     6 
     7 signature COOPER =
     8 sig
     9   type entry
    10   val get: Proof.context -> entry
    11   val del: term list -> attribute
    12   val add: term list -> attribute 
    13   val conv: Proof.context -> conv
    14   val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
    15   val method: (Proof.context -> Method.method) context_parser
    16   val setup: theory -> theory
    17 end;
    18 
    19 structure Cooper: COOPER =
    20 struct
    21 
    22 type entry = simpset * term list;
    23 
    24 val allowed_consts = 
    25   [@{term "op + :: int => _"}, @{term "op + :: nat => _"},
    26    @{term "op - :: int => _"}, @{term "op - :: nat => _"},
    27    @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    28    @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    29    @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
    30    @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
    31    @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
    32    @{term "op < :: int => _"}, @{term "op < :: nat => _"},
    33    @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
    34    @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"},
    35    @{term "abs :: int => _"},
    36    @{term "max :: int => _"}, @{term "max :: nat => _"},
    37    @{term "min :: int => _"}, @{term "min :: nat => _"},
    38    @{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*)
    39    @{term "Not"}, @{term "Suc"},
    40    @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
    41    @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
    42    @{term "nat"}, @{term "int"},
    43    @{term "Int.Bit0"}, @{term "Int.Bit1"},
    44    @{term "Int.Pls"}, @{term "Int.Min"},
    45    @{term "Int.number_of :: int => int"}, @{term "Int.number_of :: int => nat"},
    46    @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
    47    @{term "True"}, @{term "False"}];
    48 
    49 structure Data = Generic_Data
    50 (
    51   type T = simpset * term list;
    52   val empty = (HOL_ss, allowed_consts);
    53   val extend  = I;
    54   fun merge ((ss1, ts1), (ss2, ts2)) =
    55     (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
    56 );
    57 
    58 val get = Data.get o Context.Proof;
    59 
    60 fun add ts = Thm.declaration_attribute (fn th => fn context => 
    61   context |> Data.map (fn (ss,ts') => 
    62      (ss addsimps [th], merge (op aconv) (ts',ts) ))) 
    63 
    64 fun del ts = Thm.declaration_attribute (fn th => fn context => 
    65   context |> Data.map (fn (ss,ts') => 
    66      (ss delsimps [th], subtract (op aconv) ts' ts ))) 
    67 
    68 fun simp_thms_conv ctxt =
    69   Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
    70 val FWD = Drule.implies_elim_list;
    71 
    72 val true_tm = @{cterm "True"};
    73 val false_tm = @{cterm "False"};
    74 val zdvd1_eq = @{thm "zdvd1_eq"};
    75 val presburger_ss = @{simpset} addsimps [zdvd1_eq];
    76 val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac});
    77 
    78 val iT = HOLogic.intT
    79 val bT = HOLogic.boolT;
    80 val dest_numeral = HOLogic.dest_number #> snd;
    81 
    82 val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
    83     map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
    84 
    85 val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
    86     map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
    87 
    88 val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =
    89     map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
    90 
    91 val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
    92 
    93 val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
    94 
    95 val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
    96       asetgt, asetge, asetdvd, asetndvd,asetP],
    97      [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle,
    98       bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]]  = [@{thms "aset"}, @{thms "bset"}];
    99 
   100 val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}];
   101 
   102 val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
   103 
   104 val [zdvd_mono,simp_from_to,all_not_ex] =
   105      [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
   106 
   107 val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"};
   108 
   109 val eval_ss = presburger_ss addsimps [simp_from_to] delsimps [insert_iff,bex_triv];
   110 val eval_conv = Simplifier.rewrite eval_ss;
   111 
   112 (* recognising cterm without moving to terms *)
   113 
   114 datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm
   115             | Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm
   116             | Dvd of cterm*cterm | NDvd of cterm*cterm | Nox
   117 
   118 fun whatis x ct =
   119 ( case (term_of ct) of
   120   Const("op &",_)$_$_ => And (Thm.dest_binop ct)
   121 | Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)
   122 | Const ("op =",_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
   123 | Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
   124   if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
   125 | Const (@{const_name Orderings.less}, _) $ y$ z =>
   126    if term_of x aconv y then Lt (Thm.dest_arg ct)
   127    else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
   128 | Const (@{const_name Orderings.less_eq}, _) $ y $ z =>
   129    if term_of x aconv y then Le (Thm.dest_arg ct)
   130    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
   131 | Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_) =>
   132    if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
   133 | Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_)) =>
   134    if term_of x aconv y then
   135    NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
   136 | _ => Nox)
   137   handle CTERM _ => Nox;
   138 
   139 fun get_pmi_term t =
   140   let val (x,eq) =
   141      (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
   142         (Thm.dest_arg t)
   143 in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end;
   144 
   145 val get_pmi = get_pmi_term o cprop_of;
   146 
   147 val p_v' = @{cpat "?P' :: int => bool"};
   148 val q_v' = @{cpat "?Q' :: int => bool"};
   149 val p_v = @{cpat "?P:: int => bool"};
   150 val q_v = @{cpat "?Q:: int => bool"};
   151 
   152 fun myfwd (th1, th2, th3) p q
   153       [(th_1,th_2,th_3), (th_1',th_2',th_3')] =
   154   let
   155    val (mp', mq') = (get_pmi th_1, get_pmi th_1')
   156    val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
   157                    [th_1, th_1']
   158    val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
   159    val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
   160   in (mi_th, set_th, infD_th)
   161   end;
   162 
   163 val inst' = fn cts => instantiate' [] (map SOME cts);
   164 val infDTrue = instantiate' [] [SOME true_tm] infDP;
   165 val infDFalse = instantiate' [] [SOME false_tm] infDP;
   166 
   167 val cadd =  @{cterm "op + :: int => _"}
   168 val cmulC =  @{cterm "op * :: int => _"}
   169 val cminus =  @{cterm "op - :: int => _"}
   170 val cone =  @{cterm "1 :: int"}
   171 val [addC, mulC, subC] = map term_of [cadd, cmulC, cminus]
   172 val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];
   173 
   174 val is_numeral = can dest_numeral;
   175 
   176 fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));
   177 fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n));
   178 
   179 val [minus1,plus1] =
   180     map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
   181 
   182 fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
   183                            asetgt, asetge,asetdvd,asetndvd,asetP,
   184                            infDdvd, infDndvd, asetconj,
   185                            asetdisj, infDconj, infDdisj] cp =
   186  case (whatis x cp) of
   187   And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
   188 | Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
   189 | Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse))
   190 | NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue))
   191 | Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse))
   192 | Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse))
   193 | Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue))
   194 | Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue))
   195 | Dvd (d,s) =>
   196    ([],let val dd = dvd d
   197        in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end)
   198 | NDvd(d,s) => ([],let val dd = dvd d
   199         in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
   200 | _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP));
   201 
   202 fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt,
   203                            bsetge,bsetdvd,bsetndvd,bsetP,
   204                            infDdvd, infDndvd, bsetconj,
   205                            bsetdisj, infDconj, infDdisj] cp =
   206  case (whatis x cp) of
   207   And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
   208 | Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
   209 | Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse))
   210 | NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue))
   211 | Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue))
   212 | Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue))
   213 | Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse))
   214 | Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse))
   215 | Dvd (d,s) => ([],let val dd = dvd d
   216         in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end)
   217 | NDvd (d,s) => ([],let val dd = dvd d
   218         in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
   219 | _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP))
   220 
   221     (* Canonical linear form for terms, formulae etc.. *)
   222 fun provelin ctxt t = Goal.prove ctxt [] [] t
   223   (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
   224 fun linear_cmul 0 tm = zero
   225   | linear_cmul n tm = case tm of
   226       Const (@{const_name Groups.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
   227     | Const (@{const_name Groups.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
   228     | Const (@{const_name Groups.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
   229     | (m as Const (@{const_name Groups.uminus}, _)) $ a => m $ linear_cmul n a
   230     | _ => numeral1 (fn m => n * m) tm;
   231 fun earlier [] x y = false
   232   | earlier (h::t) x y =
   233     if h aconv y then false else if h aconv x then true else earlier t x y;
   234 
   235 fun linear_add vars tm1 tm2 = case (tm1, tm2) of
   236     (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1,
   237     Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
   238    if x1 = x2 then
   239      let val c = numeral2 Integer.add c1 c2
   240       in if c = zero then linear_add vars r1 r2
   241          else addC$(mulC$c$x1)$(linear_add vars r1 r2)
   242      end
   243      else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
   244    else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
   245  | (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) =>
   246       addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
   247  | (_, Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
   248       addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
   249  | (_, _) => numeral2 Integer.add tm1 tm2;
   250 
   251 fun linear_neg tm = linear_cmul ~1 tm;
   252 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
   253 
   254 exception COOPER of string;
   255 
   256 fun lint vars tm =  if is_numeral tm then tm  else case tm of
   257   Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
   258 | Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
   259 | Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
   260 | Const (@{const_name Groups.times}, _) $ s $ t =>
   261   let val s' = lint vars s
   262       val t' = lint vars t
   263   in if is_numeral s' then (linear_cmul (dest_numeral s') t')
   264      else if is_numeral t' then (linear_cmul (dest_numeral t') s')
   265      else raise COOPER "lint: not linear"
   266   end
   267  | _ => addC $ (mulC $ one $ tm) $ zero;
   268 
   269 fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Orderings.less}, T) $ s $ t)) =
   270     lin vs (Const (@{const_name Orderings.less_eq}, T) $ t $ s)
   271   | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Orderings.less_eq}, T) $ s $ t)) =
   272     lin vs (Const (@{const_name Orderings.less}, T) $ t $ s)
   273   | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   274   | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
   275     HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
   276   | lin (vs as x::_) ((b as Const("op =",_))$s$t) =
   277      (case lint vs (subC$t$s) of
   278       (t as a$(m$c$y)$r) =>
   279         if x <> y then b$zero$t
   280         else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
   281         else b$(m$c$y)$(linear_neg r)
   282       | t => b$zero$t)
   283   | lin (vs as x::_) (b$s$t) =
   284      (case lint vs (subC$t$s) of
   285       (t as a$(m$c$y)$r) =>
   286         if x <> y then b$zero$t
   287         else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
   288         else b$(linear_neg r)$(m$c$y)
   289       | t => b$zero$t)
   290   | lin vs fm = fm;
   291 
   292 fun lint_conv ctxt vs ct =
   293 let val t = term_of ct
   294 in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop))
   295              RS eq_reflection
   296 end;
   297 
   298 fun is_intrel_type T = T = @{typ "int => int => bool"};
   299 
   300 fun is_intrel (b$_$_) = is_intrel_type (fastype_of b)
   301   | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b)
   302   | is_intrel _ = false;
   303 
   304 fun linearize_conv ctxt vs ct = case term_of ct of
   305   Const(@{const_name Rings.dvd},_)$d$t =>
   306   let
   307     val th = Conv.binop_conv (lint_conv ctxt vs) ct
   308     val (d',t') = Thm.dest_binop (Thm.rhs_of th)
   309     val (dt',tt') = (term_of d', term_of t')
   310   in if is_numeral dt' andalso is_numeral tt'
   311      then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite presburger_ss)) th
   312      else
   313      let
   314       val dth =
   315       ((if dest_numeral (term_of d') < 0 then
   316           Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs)))
   317                            (Thm.transitive th (inst' [d',t'] dvd_uminus))
   318         else th) handle TERM _ => th)
   319       val d'' = Thm.rhs_of dth |> Thm.dest_arg1
   320      in
   321       case tt' of
   322         Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ =>
   323         let val x = dest_numeral c
   324         in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs)))
   325                                        (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
   326         else dth end
   327       | _ => dth
   328      end
   329   end
   330 | Const (@{const_name Not},_)$(Const(@{const_name Rings.dvd},_)$_$_) => Conv.arg_conv (linearize_conv ctxt vs) ct
   331 | t => if is_intrel t
   332       then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
   333        RS eq_reflection
   334       else reflexive ct;
   335 
   336 val dvdc = @{cterm "op dvd :: int => _"};
   337 
   338 fun unify ctxt q =
   339  let
   340   val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
   341   val x = term_of cx
   342   val ins = insert (op = : int * int -> bool)
   343   fun h (acc,dacc) t =
   344    case (term_of t) of
   345     Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   346     if x aconv y andalso member (op =)
   347       ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   348     then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
   349   | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
   350     if x aconv y andalso member (op =)
   351        [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   352     then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
   353   | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
   354     if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   355   | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   356   | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   357   | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
   358   | _ => (acc, dacc)
   359   val (cs,ds) = h ([],[]) p
   360   val l = Integer.lcms (union (op =) cs ds)
   361   fun cv k ct =
   362     let val (tm as b$s$t) = term_of ct
   363     in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
   364          |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end
   365   fun nzprop x =
   366    let
   367     val th =
   368      Simplifier.rewrite lin_ss
   369       (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
   370            (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
   371            @{cterm "0::int"})))
   372    in equal_elim (Thm.symmetric th) TrueI end;
   373   val notz =
   374     let val tab = fold Inttab.update
   375           (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
   376     in
   377       fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_numeral))
   378         handle Option =>
   379           (writeln ("noz: Theorems-Table contains no entry for " ^
   380               Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
   381     end
   382   fun unit_conv t =
   383    case (term_of t) of
   384    Const("op &",_)$_$_ => Conv.binop_conv unit_conv t
   385   | Const("op |",_)$_$_ => Conv.binop_conv unit_conv t
   386   | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
   387   | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   388     if x=y andalso member (op =)
   389       ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   390     then cv (l div dest_numeral c) t else Thm.reflexive t
   391   | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
   392     if x=y andalso member (op =)
   393       [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   394     then cv (l div dest_numeral c) t else Thm.reflexive t
   395   | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) =>
   396     if x=y then
   397       let
   398        val k = l div dest_numeral c
   399        val kt = HOLogic.mk_number iT k
   400        val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
   401              ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
   402        val (d',t') = (mulC$kt$d, mulC$kt$r)
   403        val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop))
   404                    RS eq_reflection
   405        val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop))
   406                  RS eq_reflection
   407       in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end
   408     else Thm.reflexive t
   409   | _ => Thm.reflexive t
   410   val uth = unit_conv p
   411   val clt =  Numeral.mk_cnumber @{ctyp "int"} l
   412   val ltx = Thm.capply (Thm.capply cmulC clt) cx
   413   val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
   414   val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
   415   val thf = transitive th
   416       (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
   417   val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
   418                   ||> beta_conversion true |>> Thm.symmetric
   419  in transitive (transitive lth thf) rth end;
   420 
   421 
   422 val emptyIS = @{cterm "{}::int set"};
   423 val insert_tm = @{cterm "insert :: int => _"};
   424 fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
   425 val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;
   426 val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
   427                                       |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
   428                       [asetP,bsetP];
   429 
   430 val D_tm = @{cpat "?D::int"};
   431 
   432 fun cooperex_conv ctxt vs q =
   433 let
   434 
   435  val uth = unify ctxt q
   436  val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth))
   437  val ins = insert (op aconvc)
   438  fun h t (bacc,aacc,dacc) =
   439   case (whatis x t) of
   440     And (p,q) => h q (h p (bacc,aacc,dacc))
   441   | Or (p,q) => h q  (h p (bacc,aacc,dacc))
   442   | Eq t => (ins (minus1 t) bacc,
   443              ins (plus1 t) aacc,dacc)
   444   | NEq t => (ins t bacc,
   445               ins t aacc, dacc)
   446   | Lt t => (bacc, ins t aacc, dacc)
   447   | Le t => (bacc, ins (plus1 t) aacc,dacc)
   448   | Gt t => (ins t bacc, aacc,dacc)
   449   | Ge t => (ins (minus1 t) bacc, aacc,dacc)
   450   | Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
   451   | NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
   452   | _ => (bacc, aacc, dacc)
   453  val (b0,a0,ds) = h p ([],[],[])
   454  val d = Integer.lcms ds
   455  val cd = Numeral.mk_cnumber @{ctyp "int"} d
   456  fun divprop x =
   457    let
   458     val th =
   459      Simplifier.rewrite lin_ss
   460       (Thm.capply @{cterm Trueprop}
   461            (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
   462    in equal_elim (Thm.symmetric th) TrueI end;
   463  val dvd =
   464    let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
   465      fn ct => the (Inttab.lookup tab (term_of ct |> dest_numeral))
   466        handle Option =>
   467         (writeln ("dvd: Theorems-Table contains no entry for" ^
   468             Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
   469    end
   470  val dp =
   471    let val th = Simplifier.rewrite lin_ss
   472       (Thm.capply @{cterm Trueprop}
   473            (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
   474    in equal_elim (Thm.symmetric th) TrueI end;
   475     (* A and B set *)
   476    local
   477      val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
   478      val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
   479    in
   480     fun provein x S =
   481      case term_of S of
   482         Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
   483       | Const(@{const_name insert}, _) $ y $ _ =>
   484          let val (cy,S') = Thm.dest_binop S
   485          in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
   486          else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   487                            (provein x S')
   488          end
   489    end
   490 
   491  val al = map (lint vs o term_of) a0
   492  val bl = map (lint vs o term_of) b0
   493  val (sl,s0,f,abths,cpth) =
   494    if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
   495    then
   496     (bl,b0,decomp_minf,
   497      fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
   498                      [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
   499                    (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
   500                         [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
   501                          bsetdisj,infDconj, infDdisj]),
   502                        cpmi)
   503      else (al,a0,decomp_pinf,fn A =>
   504           (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
   505                    [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
   506                    (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
   507                    [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
   508                          asetdisj,infDconj, infDdisj]),cppi)
   509  val cpth =
   510   let
   511    val sths = map (fn (tl,t0) =>
   512                       if tl = term_of t0
   513                       then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
   514                       else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0)
   515                                  |> HOLogic.mk_Trueprop))
   516                    (sl ~~ s0)
   517    val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths)
   518    val S = mkISet csl
   519    val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab)
   520                     csl Termtab.empty
   521    val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
   522    val inS =
   523      let
   524       val tab = fold Termtab.update
   525         (map (fn eq =>
   526                 let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
   527                     val th = if term_of s = term_of t
   528                              then the (Termtab.lookup inStab (term_of s))
   529                              else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
   530                                 [eq, the (Termtab.lookup inStab (term_of s))]
   531                  in (term_of t, th) end)
   532                   sths) Termtab.empty
   533         in
   534           fn ct => the (Termtab.lookup tab (term_of ct))
   535             handle Option =>
   536               (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct));
   537                 raise Option)
   538         end
   539        val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p
   540    in [dp, inf, nb, pd] MRS cpth
   541    end
   542  val cpth' = Thm.transitive uth (cpth RS eq_reflection)
   543 in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv) (Thm.rhs_of cpth'))
   544 end;
   545 
   546 fun literals_conv bops uops env cv =
   547  let fun h t =
   548   case (term_of t) of
   549    b$_$_ => if member (op aconv) bops b then Conv.binop_conv h t else cv env t
   550  | u$_ => if member (op aconv) uops u then Conv.arg_conv h t else cv env t
   551  | _ => cv env t
   552  in h end;
   553 
   554 fun integer_nnf_conv ctxt env =
   555  nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
   556 
   557 local
   558  val pcv = Simplifier.rewrite
   559      (HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4)
   560                       @ [not_all, all_not_ex, @{thm ex_disj_distrib}]))
   561  val postcv = Simplifier.rewrite presburger_ss
   562  fun conv ctxt p =
   563   let val _ = ()
   564   in
   565    Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
   566       (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
   567       (cooperex_conv ctxt) p
   568   end
   569   handle  CTERM s => raise COOPER "bad cterm"
   570         | THM s => raise COOPER "bad thm"
   571         | TYPE s => raise COOPER "bad type"
   572 in val conv = conv
   573 end;
   574 
   575 fun term_bools acc t =
   576   let
   577     val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
   578       @{term "op = :: int => _"}, @{term "op < :: int => _"},
   579       @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
   580       @{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]
   581     fun ty t = not (fastype_of t = HOLogic.boolT)
   582   in case t of
   583       (l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b
   584               else insert (op aconv) t acc
   585     | f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a
   586               else insert (op aconv) t acc
   587     | Abs p => term_bools acc (snd (variant_abs p))
   588     | _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc
   589   end;
   590 
   591 fun i_of_term vs t = case t
   592  of Free (xn, xT) => (case AList.lookup (op aconv) vs t
   593      of NONE   => raise COOPER "reification: variable not found in list"
   594       | SOME n => Cooper_Procedure.Bound n)
   595   | @{term "0::int"} => Cooper_Procedure.C 0
   596   | @{term "1::int"} => Cooper_Procedure.C 1
   597   | Term.Bound i => Cooper_Procedure.Bound i
   598   | Const(@{const_name Groups.uminus},_)$t' => Cooper_Procedure.Neg (i_of_term vs t')
   599   | Const(@{const_name Groups.plus},_)$t1$t2 => Cooper_Procedure.Add (i_of_term vs t1,i_of_term vs t2)
   600   | Const(@{const_name Groups.minus},_)$t1$t2 => Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2)
   601   | Const(@{const_name Groups.times},_)$t1$t2 =>
   602      (Cooper_Procedure.Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
   603     handle TERM _ =>
   604        (Cooper_Procedure.Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
   605         handle TERM _ => raise COOPER "reification: unsupported kind of multiplication"))
   606   | _ => (Cooper_Procedure.C (HOLogic.dest_number t |> snd)
   607            handle TERM _ => raise COOPER "reification: unknown term");
   608 
   609 fun qf_of_term ps vs t =  case t
   610  of Const("True",_) => Cooper_Procedure.T
   611   | Const("False",_) => Cooper_Procedure.F
   612   | Const(@{const_name Orderings.less},_)$t1$t2 => Cooper_Procedure.Lt (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
   613   | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Cooper_Procedure.Le (Cooper_Procedure.Sub(i_of_term vs t1,i_of_term vs t2))
   614   | Const(@{const_name Rings.dvd},_)$t1$t2 =>
   615       (Cooper_Procedure.Dvd (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
   616         handle TERM _ => raise COOPER "reification: unsupported dvd")
   617   | @{term "op = :: int => _"}$t1$t2 => Cooper_Procedure.Eq (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
   618   | @{term "op = :: bool => _ "}$t1$t2 => Cooper_Procedure.Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
   619   | Const("op &",_)$t1$t2 => Cooper_Procedure.And(qf_of_term ps vs t1,qf_of_term ps vs t2)
   620   | Const("op |",_)$t1$t2 => Cooper_Procedure.Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
   621   | Const("op -->",_)$t1$t2 => Cooper_Procedure.Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
   622   | Const (@{const_name Not},_)$t' => Cooper_Procedure.Not(qf_of_term ps vs t')
   623   | Const("Ex",_)$Abs(xn,xT,p) =>
   624      let val (xn',p') = variant_abs (xn,xT,p)
   625          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
   626      in Cooper_Procedure.E (qf_of_term ps vs' p')
   627      end
   628   | Const("All",_)$Abs(xn,xT,p) =>
   629      let val (xn',p') = variant_abs (xn,xT,p)
   630          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
   631      in Cooper_Procedure.A (qf_of_term ps vs' p')
   632      end
   633   | _ =>(case AList.lookup (op aconv) ps t of
   634            NONE => raise COOPER "reification: unknown term"
   635          | SOME n => Cooper_Procedure.Closed n);
   636 
   637 fun term_of_i vs t = case t
   638  of Cooper_Procedure.C i => HOLogic.mk_number HOLogic.intT i
   639   | Cooper_Procedure.Bound n => the (AList.lookup (op =) vs n)
   640   | Cooper_Procedure.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
   641   | Cooper_Procedure.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   642   | Cooper_Procedure.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   643   | Cooper_Procedure.Mul (i, t2) => @{term "op * :: int => _"} $
   644       HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
   645   | Cooper_Procedure.Cn (n, i, t') => term_of_i vs (Cooper_Procedure.Add (Cooper_Procedure.Mul (i, Cooper_Procedure.Bound n), t'));
   646 
   647 fun term_of_qf ps vs t =
   648  case t of
   649    Cooper_Procedure.T => HOLogic.true_const
   650  | Cooper_Procedure.F => HOLogic.false_const
   651  | Cooper_Procedure.Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   652  | Cooper_Procedure.Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
   653  | Cooper_Procedure.Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   654  | Cooper_Procedure.Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   655  | Cooper_Procedure.Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   656  | Cooper_Procedure.NEq t' => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Eq t'))
   657  | Cooper_Procedure.Dvd(i,t') => @{term "op dvd :: int => _ "} $
   658     HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
   659  | Cooper_Procedure.NDvd(i,t')=> term_of_qf ps vs (Cooper_Procedure.Not(Cooper_Procedure.Dvd(i,t')))
   660  | Cooper_Procedure.Not t' => HOLogic.Not$(term_of_qf ps vs t')
   661  | Cooper_Procedure.And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   662  | Cooper_Procedure.Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   663  | Cooper_Procedure.Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   664  | Cooper_Procedure.Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   665  | Cooper_Procedure.Closed n => the (AList.lookup (op =) ps n)
   666  | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n));
   667 
   668 fun invoke t =
   669   let
   670     val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
   671   in
   672     Logic.mk_equals (HOLogic.mk_Trueprop t,
   673       HOLogic.mk_Trueprop (term_of_qf (map swap ps) (map swap vs) (Cooper_Procedure.pa (qf_of_term ps vs t))))
   674   end;
   675 
   676 val (_, oracle) = Context.>>> (Context.map_theory_result
   677   (Thm.add_oracle (Binding.name "cooper",
   678     (fn (ctxt, t) => Thm.cterm_of (ProofContext.theory_of ctxt) (invoke t)))));
   679 
   680 val comp_ss = HOL_ss addsimps @{thms semiring_norm};
   681 
   682 fun strip_objimp ct =
   683   (case Thm.term_of ct of
   684     Const ("op -->", _) $ _ $ _ =>
   685       let val (A, B) = Thm.dest_binop ct
   686       in A :: strip_objimp B end
   687   | _ => [ct]);
   688 
   689 fun strip_objall ct = 
   690  case term_of ct of 
   691   Const ("All", _) $ Abs (xn,xT,p) => 
   692    let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
   693    in apfst (cons (a,v)) (strip_objall t')
   694    end
   695 | _ => ([],ct);
   696 
   697 local
   698   val all_maxscope_ss = 
   699      HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
   700 in
   701 fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
   702   CSUBGOAL (fn (p', i) =>
   703     let
   704      val (qvs, p) = strip_objall (Thm.dest_arg p')
   705      val (ps, c) = split_last (strip_objimp p)
   706      val qs = filter P ps
   707      val q = if P c then c else @{cterm "False"}
   708      val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
   709          (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
   710      val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
   711      val ntac = (case qs of [] => q aconvc @{cterm "False"}
   712                          | _ => false)
   713     in 
   714     if ntac then no_tac
   715       else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
   716     end)
   717 end;
   718 
   719 local
   720  fun isnum t = case t of 
   721    Const(@{const_name Groups.zero},_) => true
   722  | Const(@{const_name Groups.one},_) => true
   723  | @{term "Suc"}$s => isnum s
   724  | @{term "nat"}$s => isnum s
   725  | @{term "int"}$s => isnum s
   726  | Const(@{const_name Groups.uminus},_)$s => isnum s
   727  | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r
   728  | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r
   729  | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
   730  | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
   731  | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
   732  | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
   733  | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
   734 
   735  fun ty cts t = 
   736  if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false 
   737     else case term_of t of 
   738       c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c
   739                then not (isnum l orelse isnum r)
   740                else not (member (op aconv) cts c)
   741     | c$_ => not (member (op aconv) cts c)
   742     | c => not (member (op aconv) cts c)
   743 
   744  val term_constants =
   745   let fun h acc t = case t of
   746     Const _ => insert (op aconv) t acc
   747   | a$b => h (h acc a) b
   748   | Abs (_,_,t) => h acc t
   749   | _ => acc
   750  in h [] end;
   751 in 
   752 fun is_relevant ctxt ct = 
   753  subset (op aconv) (term_constants (term_of ct) , snd (get ctxt))
   754  andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
   755  andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
   756 
   757 fun int_nat_terms ctxt ct =
   758  let 
   759   val cts = snd (get ctxt)
   760   fun h acc t = if ty cts t then insert (op aconvc) t acc else
   761    case (term_of t) of
   762     _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
   763   | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
   764   | _ => acc
   765  in h [] ct end
   766 end;
   767 
   768 fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
   769  let 
   770    fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
   771    fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
   772    val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
   773    val p' = fold_rev gen ts p
   774  in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
   775 
   776 local
   777 val ss1 = comp_ss
   778   addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
   779       @ map (fn r => r RS sym) 
   780         [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
   781          @{thm "zmult_int"}]
   782     addsplits [@{thm "zdiff_int_split"}]
   783 
   784 val ss2 = HOL_basic_ss
   785   addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
   786             @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
   787             @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
   788   addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
   789 val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
   790   @ map (symmetric o mk_meta_eq) 
   791     [@{thm "dvd_eq_mod_eq_0"},
   792      @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
   793      @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
   794   @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
   795      @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
   796      @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
   797      @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
   798      @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
   799   @ @{thms add_ac}
   800  addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
   801  val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
   802      [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
   803       @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
   804 in
   805 fun nat_to_int_tac ctxt = 
   806   simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
   807   simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
   808   simp_tac (Simplifier.context ctxt comp_ss);
   809 
   810 fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
   811 fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
   812 end;
   813 
   814 fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
   815    let
   816     val cpth = 
   817        if !quick_and_dirty 
   818        then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
   819        else Conv.arg_conv (conv ctxt) p
   820     val p' = Thm.rhs_of cpth
   821     val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
   822    in rtac th i end
   823    handle COOPER _ => no_tac);
   824 
   825 fun finish_tac q = SUBGOAL (fn (_, i) =>
   826   (if q then I else TRY) (rtac TrueI i));
   827 
   828 fun tac elim add_ths del_ths ctxt =
   829 let val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths
   830     val aprems = Arith_Data.get_arith_facts ctxt
   831 in
   832   Method.insert_tac aprems
   833   THEN_ALL_NEW Object_Logic.full_atomize_tac
   834   THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   835   THEN_ALL_NEW simp_tac ss
   836   THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
   837   THEN_ALL_NEW Object_Logic.full_atomize_tac
   838   THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
   839   THEN_ALL_NEW Object_Logic.full_atomize_tac
   840   THEN_ALL_NEW div_mod_tac ctxt
   841   THEN_ALL_NEW splits_tac ctxt
   842   THEN_ALL_NEW simp_tac ss
   843   THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   844   THEN_ALL_NEW nat_to_int_tac ctxt
   845   THEN_ALL_NEW (core_tac ctxt)
   846   THEN_ALL_NEW finish_tac elim
   847 end;
   848 
   849 val method =
   850   let
   851     fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   852     fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
   853     val addN = "add"
   854     val delN = "del"
   855     val elimN = "elim"
   856     val any_keyword = keyword addN || keyword delN || simple_keyword elimN
   857     val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   858   in
   859     Scan.optional (simple_keyword elimN >> K false) true --
   860     Scan.optional (keyword addN |-- thms) [] --
   861     Scan.optional (keyword delN |-- thms) [] >>
   862     (fn ((elim, add_ths), del_ths) => fn ctxt =>
   863       SIMPLE_METHOD' (tac elim add_ths del_ths ctxt))
   864   end;
   865 
   866 
   867 (* theory setup *)
   868 
   869 local
   870 
   871 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
   872 
   873 val constsN = "consts";
   874 val any_keyword = keyword constsN
   875 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   876 val terms = thms >> map (term_of o Drule.dest_term);
   877 
   878 fun optional scan = Scan.optional scan [];
   879 
   880 in
   881 
   882 val setup =
   883   Attrib.setup @{binding presburger}
   884     ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
   885       optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
   886   #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] []));
   887 
   888 end;
   889 
   890 end;