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