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