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