src/HOL/Tools/Qelim/cooper.ML
author haftmann
Mon May 10 13:58:18 2010 +0200 (2010-05-10)
changeset 36798 3981db162131
parent 36797 cb074cec7a30
child 36799 628fe06cbeff
permissions -rw-r--r--
less complex organization of cooper source code
     1 (*  Title:      HOL/Tools/Qelim/cooper.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     4 
     5 signature COOPER_DATA =
     6 sig
     7   type entry
     8   val get: Proof.context -> entry
     9   val del: term list -> attribute
    10   val add: term list -> attribute 
    11   val setup: theory -> theory
    12 end;
    13 
    14 signature COOPER =
    15 sig
    16   val cooper_conv: Proof.context -> conv
    17   exception COOPER of string * exn
    18 end;
    19 
    20 signature COOPER_REIFY =
    21 sig
    22   val cooper_oracle: cterm -> cterm
    23 end;
    24 
    25 structure CooperData : COOPER_DATA =
    26 struct
    27 
    28 type entry = simpset * (term list);
    29 
    30 val allowed_consts = 
    31   [@{term "op + :: int => _"}, @{term "op + :: nat => _"},
    32    @{term "op - :: int => _"}, @{term "op - :: nat => _"},
    33    @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    34    @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    35    @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
    36    @{term "Int.Bit0"}, @{term "Int.Bit1"},
    37    @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
    38    @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
    39    @{term "op < :: int => _"}, @{term "op < :: nat => _"},
    40    @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
    41    @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"},
    42    @{term "abs :: int => _"},
    43    @{term "max :: int => _"}, @{term "max :: nat => _"},
    44    @{term "min :: int => _"}, @{term "min :: nat => _"},
    45    @{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*)
    46    @{term "Not"}, @{term "Suc"},
    47    @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
    48    @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
    49    @{term "nat"}, @{term "int"},
    50    @{term "Int.Bit0"}, @{term "Int.Bit1"},
    51    @{term "Int.Pls"}, @{term "Int.Min"},
    52    @{term "Int.number_of :: int => int"}, @{term "Int.number_of :: int => nat"},
    53    @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
    54    @{term "True"}, @{term "False"}];
    55 
    56 structure Data = Generic_Data
    57 (
    58   type T = simpset * term list;
    59   val empty = (HOL_ss, allowed_consts);
    60   val extend  = I;
    61   fun merge ((ss1, ts1), (ss2, ts2)) =
    62     (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
    63 );
    64 
    65 val get = Data.get o Context.Proof;
    66 
    67 fun add ts = Thm.declaration_attribute (fn th => fn context => 
    68   context |> Data.map (fn (ss,ts') => 
    69      (ss addsimps [th], merge (op aconv) (ts',ts) ))) 
    70 
    71 fun del ts = Thm.declaration_attribute (fn th => fn context => 
    72   context |> Data.map (fn (ss,ts') => 
    73      (ss delsimps [th], subtract (op aconv) ts' ts ))) 
    74 
    75 
    76 (* theory setup *)
    77 
    78 local
    79 
    80 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    81 
    82 val constsN = "consts";
    83 val any_keyword = keyword constsN
    84 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    85 val terms = thms >> map (term_of o Drule.dest_term);
    86 
    87 fun optional scan = Scan.optional scan [];
    88 
    89 in
    90 
    91 val setup =
    92   Attrib.setup @{binding presburger}
    93     ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
    94       optional (keyword constsN |-- terms) >> add) "Cooper data";
    95 
    96 end;
    97 
    98 end;
    99 
   100 structure Cooper: COOPER =
   101 struct
   102 
   103 exception COOPER of string * exn;
   104 fun simp_thms_conv ctxt =
   105   Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
   106 val FWD = Drule.implies_elim_list;
   107 
   108 val true_tm = @{cterm "True"};
   109 val false_tm = @{cterm "False"};
   110 val zdvd1_eq = @{thm "zdvd1_eq"};
   111 val presburger_ss = @{simpset} addsimps [zdvd1_eq];
   112 val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac});
   113 
   114 val iT = HOLogic.intT
   115 val bT = HOLogic.boolT;
   116 val dest_numeral = HOLogic.dest_number #> snd;
   117 
   118 val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
   119     map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
   120 
   121 val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
   122     map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
   123 
   124 val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =
   125     map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
   126 
   127 val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
   128 
   129 val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
   130 
   131 val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
   132       asetgt, asetge, asetdvd, asetndvd,asetP],
   133      [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle,
   134       bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]]  = [@{thms "aset"}, @{thms "bset"}];
   135 
   136 val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}];
   137 
   138 val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
   139 
   140 val [zdvd_mono,simp_from_to,all_not_ex] =
   141      [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
   142 
   143 val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"};
   144 
   145 val eval_ss = presburger_ss addsimps [simp_from_to] delsimps [insert_iff,bex_triv];
   146 val eval_conv = Simplifier.rewrite eval_ss;
   147 
   148 (* recognising cterm without moving to terms *)
   149 
   150 datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm
   151             | Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm
   152             | Dvd of cterm*cterm | NDvd of cterm*cterm | Nox
   153 
   154 fun whatis x ct =
   155 ( case (term_of ct) of
   156   Const("op &",_)$_$_ => And (Thm.dest_binop ct)
   157 | Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)
   158 | Const ("op =",_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
   159 | Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
   160   if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
   161 | Const (@{const_name Orderings.less}, _) $ y$ z =>
   162    if term_of x aconv y then Lt (Thm.dest_arg ct)
   163    else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
   164 | Const (@{const_name Orderings.less_eq}, _) $ y $ z =>
   165    if term_of x aconv y then Le (Thm.dest_arg ct)
   166    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
   167 | Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_) =>
   168    if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
   169 | Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_)) =>
   170    if term_of x aconv y then
   171    NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
   172 | _ => Nox)
   173   handle CTERM _ => Nox;
   174 
   175 fun get_pmi_term t =
   176   let val (x,eq) =
   177      (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
   178         (Thm.dest_arg t)
   179 in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end;
   180 
   181 val get_pmi = get_pmi_term o cprop_of;
   182 
   183 val p_v' = @{cpat "?P' :: int => bool"};
   184 val q_v' = @{cpat "?Q' :: int => bool"};
   185 val p_v = @{cpat "?P:: int => bool"};
   186 val q_v = @{cpat "?Q:: int => bool"};
   187 
   188 fun myfwd (th1, th2, th3) p q
   189       [(th_1,th_2,th_3), (th_1',th_2',th_3')] =
   190   let
   191    val (mp', mq') = (get_pmi th_1, get_pmi th_1')
   192    val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
   193                    [th_1, th_1']
   194    val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
   195    val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
   196   in (mi_th, set_th, infD_th)
   197   end;
   198 
   199 val inst' = fn cts => instantiate' [] (map SOME cts);
   200 val infDTrue = instantiate' [] [SOME true_tm] infDP;
   201 val infDFalse = instantiate' [] [SOME false_tm] infDP;
   202 
   203 val cadd =  @{cterm "op + :: int => _"}
   204 val cmulC =  @{cterm "op * :: int => _"}
   205 val cminus =  @{cterm "op - :: int => _"}
   206 val cone =  @{cterm "1 :: int"}
   207 val [addC, mulC, subC] = map term_of [cadd, cmulC, cminus]
   208 val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];
   209 
   210 val is_numeral = can dest_numeral;
   211 
   212 fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));
   213 fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n));
   214 
   215 val [minus1,plus1] =
   216     map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
   217 
   218 fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
   219                            asetgt, asetge,asetdvd,asetndvd,asetP,
   220                            infDdvd, infDndvd, asetconj,
   221                            asetdisj, infDconj, infDdisj] cp =
   222  case (whatis x cp) of
   223   And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
   224 | Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
   225 | Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse))
   226 | NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue))
   227 | Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse))
   228 | Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse))
   229 | Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue))
   230 | Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue))
   231 | Dvd (d,s) =>
   232    ([],let val dd = dvd d
   233        in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end)
   234 | NDvd(d,s) => ([],let val dd = dvd d
   235         in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
   236 | _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP));
   237 
   238 fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt,
   239                            bsetge,bsetdvd,bsetndvd,bsetP,
   240                            infDdvd, infDndvd, bsetconj,
   241                            bsetdisj, infDconj, infDdisj] cp =
   242  case (whatis x cp) of
   243   And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
   244 | Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
   245 | Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse))
   246 | NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue))
   247 | Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue))
   248 | Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue))
   249 | Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse))
   250 | Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse))
   251 | Dvd (d,s) => ([],let val dd = dvd d
   252         in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end)
   253 | NDvd (d,s) => ([],let val dd = dvd d
   254         in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
   255 | _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP))
   256 
   257     (* Canonical linear form for terms, formulae etc.. *)
   258 fun provelin ctxt t = Goal.prove ctxt [] [] t
   259   (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
   260 fun linear_cmul 0 tm = zero
   261   | linear_cmul n tm = case tm of
   262       Const (@{const_name Groups.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
   263     | Const (@{const_name Groups.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
   264     | Const (@{const_name Groups.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
   265     | (m as Const (@{const_name Groups.uminus}, _)) $ a => m $ linear_cmul n a
   266     | _ => numeral1 (fn m => n * m) tm;
   267 fun earlier [] x y = false
   268   | earlier (h::t) x y =
   269     if h aconv y then false else if h aconv x then true else earlier t x y;
   270 
   271 fun linear_add vars tm1 tm2 = case (tm1, tm2) of
   272     (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1,
   273     Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
   274    if x1 = x2 then
   275      let val c = numeral2 Integer.add c1 c2
   276       in if c = zero then linear_add vars r1 r2
   277          else addC$(mulC$c$x1)$(linear_add vars r1 r2)
   278      end
   279      else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
   280    else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
   281  | (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) =>
   282       addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
   283  | (_, Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
   284       addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
   285  | (_, _) => numeral2 Integer.add tm1 tm2;
   286 
   287 fun linear_neg tm = linear_cmul ~1 tm;
   288 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
   289 
   290 
   291 fun lint vars tm =  if is_numeral tm then tm  else case tm of
   292   Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
   293 | Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
   294 | Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
   295 | Const (@{const_name Groups.times}, _) $ s $ t =>
   296   let val s' = lint vars s
   297       val t' = lint vars t
   298   in if is_numeral s' then (linear_cmul (dest_numeral s') t')
   299      else if is_numeral t' then (linear_cmul (dest_numeral t') s')
   300      else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm]))
   301   end
   302  | _ => addC $ (mulC $ one $ tm) $ zero;
   303 
   304 fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Orderings.less}, T) $ s $ t)) =
   305     lin vs (Const (@{const_name Orderings.less_eq}, T) $ t $ s)
   306   | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Orderings.less_eq}, T) $ s $ t)) =
   307     lin vs (Const (@{const_name Orderings.less}, T) $ t $ s)
   308   | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   309   | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
   310     HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
   311   | lin (vs as x::_) ((b as Const("op =",_))$s$t) =
   312      (case lint vs (subC$t$s) of
   313       (t as a$(m$c$y)$r) =>
   314         if x <> y then b$zero$t
   315         else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
   316         else b$(m$c$y)$(linear_neg r)
   317       | t => b$zero$t)
   318   | lin (vs as x::_) (b$s$t) =
   319      (case lint vs (subC$t$s) of
   320       (t as a$(m$c$y)$r) =>
   321         if x <> y then b$zero$t
   322         else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
   323         else b$(linear_neg r)$(m$c$y)
   324       | t => b$zero$t)
   325   | lin vs fm = fm;
   326 
   327 fun lint_conv ctxt vs ct =
   328 let val t = term_of ct
   329 in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop))
   330              RS eq_reflection
   331 end;
   332 
   333 fun is_intrel_type T = T = @{typ "int => int => bool"};
   334 
   335 fun is_intrel (b$_$_) = is_intrel_type (fastype_of b)
   336   | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b)
   337   | is_intrel _ = false;
   338 
   339 fun linearize_conv ctxt vs ct = case term_of ct of
   340   Const(@{const_name Rings.dvd},_)$d$t =>
   341   let
   342     val th = Conv.binop_conv (lint_conv ctxt vs) ct
   343     val (d',t') = Thm.dest_binop (Thm.rhs_of th)
   344     val (dt',tt') = (term_of d', term_of t')
   345   in if is_numeral dt' andalso is_numeral tt'
   346      then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite presburger_ss)) th
   347      else
   348      let
   349       val dth =
   350       ((if dest_numeral (term_of d') < 0 then
   351           Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs)))
   352                            (Thm.transitive th (inst' [d',t'] dvd_uminus))
   353         else th) handle TERM _ => th)
   354       val d'' = Thm.rhs_of dth |> Thm.dest_arg1
   355      in
   356       case tt' of
   357         Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ =>
   358         let val x = dest_numeral c
   359         in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs)))
   360                                        (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
   361         else dth end
   362       | _ => dth
   363      end
   364   end
   365 | Const (@{const_name Not},_)$(Const(@{const_name Rings.dvd},_)$_$_) => Conv.arg_conv (linearize_conv ctxt vs) ct
   366 | t => if is_intrel t
   367       then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
   368        RS eq_reflection
   369       else reflexive ct;
   370 
   371 val dvdc = @{cterm "op dvd :: int => _"};
   372 
   373 fun unify ctxt q =
   374  let
   375   val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
   376   val x = term_of cx
   377   val ins = insert (op = : int * int -> bool)
   378   fun h (acc,dacc) t =
   379    case (term_of t) of
   380     Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   381     if x aconv y andalso member (op =)
   382       ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   383     then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
   384   | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
   385     if x aconv y andalso member (op =)
   386        [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   387     then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
   388   | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
   389     if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   390   | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   391   | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   392   | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
   393   | _ => (acc, dacc)
   394   val (cs,ds) = h ([],[]) p
   395   val l = Integer.lcms (union (op =) cs ds)
   396   fun cv k ct =
   397     let val (tm as b$s$t) = term_of ct
   398     in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
   399          |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end
   400   fun nzprop x =
   401    let
   402     val th =
   403      Simplifier.rewrite lin_ss
   404       (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
   405            (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
   406            @{cterm "0::int"})))
   407    in equal_elim (Thm.symmetric th) TrueI end;
   408   val notz =
   409     let val tab = fold Inttab.update
   410           (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
   411     in
   412       fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_numeral))
   413         handle Option =>
   414           (writeln ("noz: Theorems-Table contains no entry for " ^
   415               Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
   416     end
   417   fun unit_conv t =
   418    case (term_of t) of
   419    Const("op &",_)$_$_ => Conv.binop_conv unit_conv t
   420   | Const("op |",_)$_$_ => Conv.binop_conv unit_conv t
   421   | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
   422   | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   423     if x=y andalso member (op =)
   424       ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   425     then cv (l div dest_numeral c) t else Thm.reflexive t
   426   | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
   427     if x=y andalso member (op =)
   428       [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   429     then cv (l div dest_numeral c) t else Thm.reflexive t
   430   | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) =>
   431     if x=y then
   432       let
   433        val k = l div dest_numeral c
   434        val kt = HOLogic.mk_number iT k
   435        val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
   436              ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
   437        val (d',t') = (mulC$kt$d, mulC$kt$r)
   438        val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop))
   439                    RS eq_reflection
   440        val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop))
   441                  RS eq_reflection
   442       in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end
   443     else Thm.reflexive t
   444   | _ => Thm.reflexive t
   445   val uth = unit_conv p
   446   val clt =  Numeral.mk_cnumber @{ctyp "int"} l
   447   val ltx = Thm.capply (Thm.capply cmulC clt) cx
   448   val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
   449   val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
   450   val thf = transitive th
   451       (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
   452   val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
   453                   ||> beta_conversion true |>> Thm.symmetric
   454  in transitive (transitive lth thf) rth end;
   455 
   456 
   457 val emptyIS = @{cterm "{}::int set"};
   458 val insert_tm = @{cterm "insert :: int => _"};
   459 fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
   460 val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;
   461 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
   462                                       |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
   463                       [asetP,bsetP];
   464 
   465 val D_tm = @{cpat "?D::int"};
   466 
   467 fun cooperex_conv ctxt vs q =
   468 let
   469 
   470  val uth = unify ctxt q
   471  val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth))
   472  val ins = insert (op aconvc)
   473  fun h t (bacc,aacc,dacc) =
   474   case (whatis x t) of
   475     And (p,q) => h q (h p (bacc,aacc,dacc))
   476   | Or (p,q) => h q  (h p (bacc,aacc,dacc))
   477   | Eq t => (ins (minus1 t) bacc,
   478              ins (plus1 t) aacc,dacc)
   479   | NEq t => (ins t bacc,
   480               ins t aacc, dacc)
   481   | Lt t => (bacc, ins t aacc, dacc)
   482   | Le t => (bacc, ins (plus1 t) aacc,dacc)
   483   | Gt t => (ins t bacc, aacc,dacc)
   484   | Ge t => (ins (minus1 t) bacc, aacc,dacc)
   485   | Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
   486   | NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
   487   | _ => (bacc, aacc, dacc)
   488  val (b0,a0,ds) = h p ([],[],[])
   489  val d = Integer.lcms ds
   490  val cd = Numeral.mk_cnumber @{ctyp "int"} d
   491  fun divprop x =
   492    let
   493     val th =
   494      Simplifier.rewrite lin_ss
   495       (Thm.capply @{cterm Trueprop}
   496            (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
   497    in equal_elim (Thm.symmetric th) TrueI end;
   498  val dvd =
   499    let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
   500      fn ct => the (Inttab.lookup tab (term_of ct |> dest_numeral))
   501        handle Option =>
   502         (writeln ("dvd: Theorems-Table contains no entry for" ^
   503             Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
   504    end
   505  val dp =
   506    let val th = Simplifier.rewrite lin_ss
   507       (Thm.capply @{cterm Trueprop}
   508            (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
   509    in equal_elim (Thm.symmetric th) TrueI end;
   510     (* A and B set *)
   511    local
   512      val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
   513      val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
   514    in
   515     fun provein x S =
   516      case term_of S of
   517         Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
   518       | Const(@{const_name insert}, _) $ y $ _ =>
   519          let val (cy,S') = Thm.dest_binop S
   520          in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
   521          else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   522                            (provein x S')
   523          end
   524    end
   525 
   526  val al = map (lint vs o term_of) a0
   527  val bl = map (lint vs o term_of) b0
   528  val (sl,s0,f,abths,cpth) =
   529    if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
   530    then
   531     (bl,b0,decomp_minf,
   532      fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
   533                      [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
   534                    (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
   535                         [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
   536                          bsetdisj,infDconj, infDdisj]),
   537                        cpmi)
   538      else (al,a0,decomp_pinf,fn A =>
   539           (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
   540                    [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
   541                    (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
   542                    [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
   543                          asetdisj,infDconj, infDdisj]),cppi)
   544  val cpth =
   545   let
   546    val sths = map (fn (tl,t0) =>
   547                       if tl = term_of t0
   548                       then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
   549                       else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0)
   550                                  |> HOLogic.mk_Trueprop))
   551                    (sl ~~ s0)
   552    val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths)
   553    val S = mkISet csl
   554    val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab)
   555                     csl Termtab.empty
   556    val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
   557    val inS =
   558      let
   559       val tab = fold Termtab.update
   560         (map (fn eq =>
   561                 let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
   562                     val th = if term_of s = term_of t
   563                              then the (Termtab.lookup inStab (term_of s))
   564                              else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
   565                                 [eq, the (Termtab.lookup inStab (term_of s))]
   566                  in (term_of t, th) end)
   567                   sths) Termtab.empty
   568         in
   569           fn ct => the (Termtab.lookup tab (term_of ct))
   570             handle Option =>
   571               (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct));
   572                 raise Option)
   573         end
   574        val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p
   575    in [dp, inf, nb, pd] MRS cpth
   576    end
   577  val cpth' = Thm.transitive uth (cpth RS eq_reflection)
   578 in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv) (Thm.rhs_of cpth'))
   579 end;
   580 
   581 fun literals_conv bops uops env cv =
   582  let fun h t =
   583   case (term_of t) of
   584    b$_$_ => if member (op aconv) bops b then Conv.binop_conv h t else cv env t
   585  | u$_ => if member (op aconv) uops u then Conv.arg_conv h t else cv env t
   586  | _ => cv env t
   587  in h end;
   588 
   589 fun integer_nnf_conv ctxt env =
   590  nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
   591 
   592 local
   593  val pcv = Simplifier.rewrite
   594      (HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4)
   595                       @ [not_all, all_not_ex, @{thm ex_disj_distrib}]))
   596  val postcv = Simplifier.rewrite presburger_ss
   597  fun conv ctxt p =
   598   let val _ = ()
   599   in
   600    Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
   601       (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
   602       (cooperex_conv ctxt) p
   603   end
   604   handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)
   605         | THM s => raise COOPER ("Cooper Failed", THM s)
   606         | TYPE s => raise COOPER ("Cooper Failed", TYPE s)
   607 in val cooper_conv = conv
   608 end;
   609 end;
   610 
   611 structure Coopereif : COOPER_REIFY =
   612 struct
   613 
   614 fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);
   615 fun i_of_term vs t = case t
   616  of Free (xn, xT) => (case AList.lookup (op aconv) vs t
   617      of NONE   => cooper "Variable not found in the list!"
   618       | SOME n => Cooper_Procedure.Bound n)
   619   | @{term "0::int"} => Cooper_Procedure.C 0
   620   | @{term "1::int"} => Cooper_Procedure.C 1
   621   | Term.Bound i => Cooper_Procedure.Bound i
   622   | Const(@{const_name Groups.uminus},_)$t' => Cooper_Procedure.Neg (i_of_term vs t')
   623   | Const(@{const_name Groups.plus},_)$t1$t2 => Cooper_Procedure.Add (i_of_term vs t1,i_of_term vs t2)
   624   | Const(@{const_name Groups.minus},_)$t1$t2 => Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2)
   625   | Const(@{const_name Groups.times},_)$t1$t2 =>
   626      (Cooper_Procedure.Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
   627     handle TERM _ =>
   628        (Cooper_Procedure.Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
   629         handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
   630   | _ => (Cooper_Procedure.C (HOLogic.dest_number t |> snd)
   631            handle TERM _ => cooper "Reification: unknown term");
   632 
   633 fun qf_of_term ps vs t =  case t
   634  of Const("True",_) => Cooper_Procedure.T
   635   | Const("False",_) => Cooper_Procedure.F
   636   | Const(@{const_name Orderings.less},_)$t1$t2 => Cooper_Procedure.Lt (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
   637   | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Cooper_Procedure.Le (Cooper_Procedure.Sub(i_of_term vs t1,i_of_term vs t2))
   638   | Const(@{const_name Rings.dvd},_)$t1$t2 =>
   639       (Cooper_Procedure.Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
   640   | @{term "op = :: int => _"}$t1$t2 => Cooper_Procedure.Eq (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
   641   | @{term "op = :: bool => _ "}$t1$t2 => Cooper_Procedure.Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
   642   | Const("op &",_)$t1$t2 => Cooper_Procedure.And(qf_of_term ps vs t1,qf_of_term ps vs t2)
   643   | Const("op |",_)$t1$t2 => Cooper_Procedure.Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
   644   | Const("op -->",_)$t1$t2 => Cooper_Procedure.Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
   645   | Const (@{const_name Not},_)$t' => Cooper_Procedure.Not(qf_of_term ps vs t')
   646   | Const("Ex",_)$Abs(xn,xT,p) =>
   647      let val (xn',p') = variant_abs (xn,xT,p)
   648          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
   649      in Cooper_Procedure.E (qf_of_term ps vs' p')
   650      end
   651   | Const("All",_)$Abs(xn,xT,p) =>
   652      let val (xn',p') = variant_abs (xn,xT,p)
   653          val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
   654      in Cooper_Procedure.A (qf_of_term ps vs' p')
   655      end
   656   | _ =>(case AList.lookup (op aconv) ps t of
   657            NONE => cooper "Reification: unknown term!"
   658          | SOME n => Cooper_Procedure.Closed n);
   659 
   660 local
   661  val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
   662              @{term "op = :: int => _"}, @{term "op < :: int => _"},
   663              @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
   664              @{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]
   665 fun ty t = Bool.not (fastype_of t = HOLogic.boolT)
   666 in
   667 fun term_bools acc t =
   668 case t of
   669     (l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b
   670             else insert (op aconv) t acc
   671   | f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a
   672             else insert (op aconv) t acc
   673   | Abs p => term_bools acc (snd (variant_abs p))
   674   | _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc
   675 end;
   676 
   677 fun myassoc2 l v =
   678     case l of
   679   [] => NONE
   680       | (x,v')::xs => if v = v' then SOME x
   681           else myassoc2 xs v;
   682 
   683 fun term_of_i vs t = case t
   684  of Cooper_Procedure.C i => HOLogic.mk_number HOLogic.intT i
   685   | Cooper_Procedure.Bound n => the (myassoc2 vs n)
   686   | Cooper_Procedure.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
   687   | Cooper_Procedure.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   688   | Cooper_Procedure.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   689   | Cooper_Procedure.Mul (i, t2) => @{term "op * :: int => _"} $
   690       HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
   691   | Cooper_Procedure.Cn (n, i, t') => term_of_i vs (Cooper_Procedure.Add (Cooper_Procedure.Mul (i, Cooper_Procedure.Bound n), t'));
   692 
   693 fun term_of_qf ps vs t =
   694  case t of
   695    Cooper_Procedure.T => HOLogic.true_const
   696  | Cooper_Procedure.F => HOLogic.false_const
   697  | Cooper_Procedure.Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   698  | Cooper_Procedure.Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
   699  | Cooper_Procedure.Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   700  | Cooper_Procedure.Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   701  | Cooper_Procedure.Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   702  | Cooper_Procedure.NEq t' => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Eq t'))
   703  | Cooper_Procedure.Dvd(i,t') => @{term "op dvd :: int => _ "} $
   704     HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
   705  | Cooper_Procedure.NDvd(i,t')=> term_of_qf ps vs (Cooper_Procedure.Not(Cooper_Procedure.Dvd(i,t')))
   706  | Cooper_Procedure.Not t' => HOLogic.Not$(term_of_qf ps vs t')
   707  | Cooper_Procedure.And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   708  | Cooper_Procedure.Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   709  | Cooper_Procedure.Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   710  | Cooper_Procedure.Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   711  | Cooper_Procedure.Closed n => the (myassoc2 ps n)
   712  | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n))
   713  | _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!";
   714 
   715 fun cooper_oracle ct =
   716   let
   717     val thy = Thm.theory_of_cterm ct;
   718     val t = Thm.term_of ct;
   719     val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
   720   in
   721     Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
   722       HOLogic.mk_Trueprop (term_of_qf ps vs (Cooper_Procedure.pa (qf_of_term ps vs t)))))
   723   end;
   724 
   725 end;