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