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