tuned code; toward a tightended interface with generated code
authorhaftmann
Tue May 11 18:31:36 2010 +0200 (2010-05-11)
changeset 368313037d6810fca
parent 36813 75d837441aa6
child 36832 e6078ef937df
tuned code; toward a tightended interface with generated code
src/HOL/Tools/Qelim/cooper.ML
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue May 11 08:52:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue May 11 18:31:36 2010 +0200
     1.3 @@ -77,7 +77,9 @@
     1.4  
     1.5  val iT = HOLogic.intT
     1.6  val bT = HOLogic.boolT;
     1.7 -val dest_numeral = HOLogic.dest_number #> snd;
     1.8 +val dest_number = HOLogic.dest_number #> snd;
     1.9 +val perhaps_number = try dest_number;
    1.10 +val is_number = can dest_number;
    1.11  
    1.12  val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
    1.13      map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
    1.14 @@ -171,10 +173,8 @@
    1.15  val [addC, mulC, subC] = map term_of [cadd, cmulC, cminus]
    1.16  val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];
    1.17  
    1.18 -val is_numeral = can dest_numeral;
    1.19 -
    1.20 -fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));
    1.21 -fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n));
    1.22 +fun numeral1 f n = HOLogic.mk_number iT (f (dest_number n));
    1.23 +fun numeral2 f m n = HOLogic.mk_number iT (f (dest_number m) (dest_number n));
    1.24  
    1.25  val [minus1,plus1] =
    1.26      map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
    1.27 @@ -253,16 +253,16 @@
    1.28  
    1.29  exception COOPER of string;
    1.30  
    1.31 -fun lint vars tm =  if is_numeral tm then tm  else case tm of
    1.32 +fun lint vars tm =  if is_number tm then tm  else case tm of
    1.33    Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
    1.34  | Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
    1.35  | Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
    1.36  | Const (@{const_name Groups.times}, _) $ s $ t =>
    1.37    let val s' = lint vars s
    1.38        val t' = lint vars t
    1.39 -  in if is_numeral s' then (linear_cmul (dest_numeral s') t')
    1.40 -     else if is_numeral t' then (linear_cmul (dest_numeral t') s')
    1.41 -     else raise COOPER "lint: not linear"
    1.42 +  in case perhaps_number s' of SOME n => linear_cmul n t'
    1.43 +   | NONE => (case perhaps_number t' of SOME n => linear_cmul n s'
    1.44 +   | NONE => raise COOPER "lint: not linear")
    1.45    end
    1.46   | _ => addC $ (mulC $ one $ tm) $ zero;
    1.47  
    1.48 @@ -277,14 +277,14 @@
    1.49       (case lint vs (subC$t$s) of
    1.50        (t as a$(m$c$y)$r) =>
    1.51          if x <> y then b$zero$t
    1.52 -        else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
    1.53 +        else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r
    1.54          else b$(m$c$y)$(linear_neg r)
    1.55        | t => b$zero$t)
    1.56    | lin (vs as x::_) (b$s$t) =
    1.57       (case lint vs (subC$t$s) of
    1.58        (t as a$(m$c$y)$r) =>
    1.59          if x <> y then b$zero$t
    1.60 -        else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
    1.61 +        else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r
    1.62          else b$(linear_neg r)$(m$c$y)
    1.63        | t => b$zero$t)
    1.64    | lin vs fm = fm;
    1.65 @@ -307,12 +307,12 @@
    1.66      val th = Conv.binop_conv (lint_conv ctxt vs) ct
    1.67      val (d',t') = Thm.dest_binop (Thm.rhs_of th)
    1.68      val (dt',tt') = (term_of d', term_of t')
    1.69 -  in if is_numeral dt' andalso is_numeral tt'
    1.70 +  in if is_number dt' andalso is_number tt'
    1.71       then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite presburger_ss)) th
    1.72       else
    1.73       let
    1.74        val dth =
    1.75 -      ((if dest_numeral (term_of d') < 0 then
    1.76 +      ((if dest_number (term_of d') < 0 then
    1.77            Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs)))
    1.78                             (Thm.transitive th (inst' [d',t'] dvd_uminus))
    1.79          else th) handle TERM _ => th)
    1.80 @@ -320,7 +320,7 @@
    1.81       in
    1.82        case tt' of
    1.83          Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ =>
    1.84 -        let val x = dest_numeral c
    1.85 +        let val x = dest_number c
    1.86          in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs)))
    1.87                                         (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
    1.88          else dth end
    1.89 @@ -345,13 +345,13 @@
    1.90      Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
    1.91      if x aconv y andalso member (op =)
    1.92        ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    1.93 -    then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
    1.94 +    then (ins (dest_number c) acc,dacc) else (acc,dacc)
    1.95    | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
    1.96      if x aconv y andalso member (op =)
    1.97         [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    1.98 -    then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
    1.99 +    then (ins (dest_number c) acc, dacc) else (acc,dacc)
   1.100    | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
   1.101 -    if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   1.102 +    if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
   1.103    | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   1.104    | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   1.105    | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
   1.106 @@ -374,7 +374,7 @@
   1.107      let val tab = fold Inttab.update
   1.108            (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
   1.109      in
   1.110 -      fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_numeral))
   1.111 +      fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_number))
   1.112          handle Option =>
   1.113            (writeln ("noz: Theorems-Table contains no entry for " ^
   1.114                Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
   1.115 @@ -387,15 +387,15 @@
   1.116    | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   1.117      if x=y andalso member (op =)
   1.118        ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   1.119 -    then cv (l div dest_numeral c) t else Thm.reflexive t
   1.120 +    then cv (l div dest_number c) t else Thm.reflexive t
   1.121    | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
   1.122      if x=y andalso member (op =)
   1.123        [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   1.124 -    then cv (l div dest_numeral c) t else Thm.reflexive t
   1.125 +    then cv (l div dest_number c) t else Thm.reflexive t
   1.126    | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) =>
   1.127      if x=y then
   1.128        let
   1.129 -       val k = l div dest_numeral c
   1.130 +       val k = l div dest_number c
   1.131         val kt = HOLogic.mk_number iT k
   1.132         val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
   1.133               ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
   1.134 @@ -447,8 +447,8 @@
   1.135    | Le t => (bacc, ins (plus1 t) aacc,dacc)
   1.136    | Gt t => (ins t bacc, aacc,dacc)
   1.137    | Ge t => (ins (minus1 t) bacc, aacc,dacc)
   1.138 -  | Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
   1.139 -  | NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
   1.140 +  | Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_number) dacc)
   1.141 +  | NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_number) dacc)
   1.142    | _ => (bacc, aacc, dacc)
   1.143   val (b0,a0,ds) = h p ([],[],[])
   1.144   val d = Integer.lcms ds
   1.145 @@ -462,7 +462,7 @@
   1.146     in equal_elim (Thm.symmetric th) TrueI end;
   1.147   val dvd =
   1.148     let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
   1.149 -     fn ct => the (Inttab.lookup tab (term_of ct |> dest_numeral))
   1.150 +     fn ct => the (Inttab.lookup tab (term_of ct |> dest_number))
   1.151         handle Option =>
   1.152          (writeln ("dvd: Theorems-Table contains no entry for" ^
   1.153              Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
   1.154 @@ -554,125 +554,121 @@
   1.155  fun integer_nnf_conv ctxt env =
   1.156   nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
   1.157  
   1.158 -local
   1.159 - val pcv = Simplifier.rewrite
   1.160 -     (HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4)
   1.161 -                      @ [not_all, all_not_ex, @{thm ex_disj_distrib}]))
   1.162 - val postcv = Simplifier.rewrite presburger_ss
   1.163 - fun conv ctxt p =
   1.164 -  let val _ = ()
   1.165 -  in
   1.166 -   Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
   1.167 -      (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
   1.168 -      (cooperex_conv ctxt) p
   1.169 -  end
   1.170 -  handle  CTERM s => raise COOPER "bad cterm"
   1.171 -        | THM s => raise COOPER "bad thm"
   1.172 -        | TYPE s => raise COOPER "bad type"
   1.173 -in val conv = conv
   1.174 -end;
   1.175 +val conv_ss = HOL_basic_ss addsimps
   1.176 +  (@{thms simp_thms} @ take 4 @{thms ex_simps} @ [not_all, all_not_ex, @{thm ex_disj_distrib}]);
   1.177 +
   1.178 +fun conv ctxt p =
   1.179 +  Qelim.gen_qelim_conv (Simplifier.rewrite conv_ss) (Simplifier.rewrite presburger_ss) (Simplifier.rewrite conv_ss)
   1.180 +    (cons o term_of) (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
   1.181 +    (cooperex_conv ctxt) p
   1.182 +  handle CTERM s => raise COOPER "bad cterm"
   1.183 +       | THM s => raise COOPER "bad thm"
   1.184 +       | TYPE s => raise COOPER "bad type"
   1.185  
   1.186 -fun term_bools acc t =
   1.187 +fun add_bools t =
   1.188    let
   1.189 -    val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
   1.190 -      @{term "op = :: int => _"}, @{term "op < :: int => _"},
   1.191 -      @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
   1.192 -      @{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]
   1.193 -    fun ty t = not (fastype_of t = HOLogic.boolT)
   1.194 +    val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
   1.195 +      @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
   1.196 +      @{term "Not"}, @{term "All :: (int => _) => _"},
   1.197 +      @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
   1.198 +    val is_op = member (op =) ops;
   1.199 +    val skip = not (fastype_of t = HOLogic.boolT)
   1.200    in case t of
   1.201 -      (l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b
   1.202 -              else insert (op aconv) t acc
   1.203 -    | f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a
   1.204 -              else insert (op aconv) t acc
   1.205 -    | Abs p => term_bools acc (snd (variant_abs p))
   1.206 -    | _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc
   1.207 +      (l as f $ a) $ b => if skip orelse is_op f then add_bools b o add_bools l
   1.208 +              else insert (op aconv) t
   1.209 +    | f $ a => if skip orelse is_op f then add_bools a o add_bools f
   1.210 +              else insert (op aconv) t
   1.211 +    | Abs p => add_bools (snd (variant_abs p))
   1.212 +    | _ => if skip orelse is_op t then I else insert (op aconv) t
   1.213    end;
   1.214  
   1.215 -fun i_of_term vs t = case t
   1.216 - of Free (xn, xT) => (case AList.lookup (op aconv) vs t
   1.217 -     of NONE   => raise COOPER "reification: variable not found in list"
   1.218 -      | SOME n => Cooper_Procedure.Bound n)
   1.219 -  | @{term "0::int"} => Cooper_Procedure.C 0
   1.220 -  | @{term "1::int"} => Cooper_Procedure.C 1
   1.221 -  | Term.Bound i => Cooper_Procedure.Bound i
   1.222 -  | Const(@{const_name Groups.uminus},_)$t' => Cooper_Procedure.Neg (i_of_term vs t')
   1.223 -  | Const(@{const_name Groups.plus},_)$t1$t2 => Cooper_Procedure.Add (i_of_term vs t1,i_of_term vs t2)
   1.224 -  | Const(@{const_name Groups.minus},_)$t1$t2 => Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2)
   1.225 -  | Const(@{const_name Groups.times},_)$t1$t2 =>
   1.226 -     (Cooper_Procedure.Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
   1.227 -    handle TERM _ =>
   1.228 -       (Cooper_Procedure.Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
   1.229 -        handle TERM _ => raise COOPER "reification: unsupported kind of multiplication"))
   1.230 -  | _ => (Cooper_Procedure.C (HOLogic.dest_number t |> snd)
   1.231 -           handle TERM _ => raise COOPER "reification: unknown term");
   1.232 +local structure Proc = Cooper_Procedure in
   1.233 +
   1.234 +fun i_of_term vs (Free vT) = Proc.Bound (the (AList.lookup (op =) vs vT))
   1.235 +  | i_of_term vs (Term.Bound i) = Proc.Bound i
   1.236 +  | i_of_term vs @{term "0::int"} = Proc.C 0
   1.237 +  | i_of_term vs @{term "1::int"} = Proc.C 1
   1.238 +  | i_of_term vs (t as Const (@{const_name number_of}, _) $ _) = Proc.C (dest_number t)
   1.239 +  | i_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') = Proc.Neg (i_of_term vs t')
   1.240 +  | i_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) = Proc.Add (i_of_term vs t1, i_of_term vs t2)
   1.241 +  | i_of_term vs (Const (@{const_name Groups.minus}, _) $ t1 $ t2) = Proc.Sub (i_of_term vs t1, i_of_term vs t2)
   1.242 +  | i_of_term vs (Const (@{const_name Groups.times}, _) $ t1 $ t2) = (case perhaps_number t1
   1.243 +     of SOME n => Proc.Mul (n, i_of_term vs t2)
   1.244 +      | NONE => (case perhaps_number t2
   1.245 +         of SOME n => Proc.Mul (n, i_of_term vs t1)
   1.246 +          | NONE => raise COOPER "reification: unsupported kind of multiplication"))
   1.247 +  | i_of_term _ _ = raise COOPER "reification: unknown term";
   1.248  
   1.249 -fun qf_of_term ps vs t =  case t
   1.250 - of Const("True",_) => Cooper_Procedure.T
   1.251 -  | Const("False",_) => Cooper_Procedure.F
   1.252 -  | Const(@{const_name Orderings.less},_)$t1$t2 => Cooper_Procedure.Lt (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
   1.253 -  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Cooper_Procedure.Le (Cooper_Procedure.Sub(i_of_term vs t1,i_of_term vs t2))
   1.254 -  | Const(@{const_name Rings.dvd},_)$t1$t2 =>
   1.255 -      (Cooper_Procedure.Dvd (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
   1.256 +fun qf_of_term ps vs t = case t
   1.257 + of Const (@{const_name True}, _) => Proc.T
   1.258 +  | Const (@{const_name False}, _) => Proc.F
   1.259 +  | Const (@{const_name Orderings.less}, _) $ t1 $ t2 => Proc.Lt (Proc.Sub (i_of_term vs t1, i_of_term vs t2))
   1.260 +  | Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2 => Proc.Le (Proc.Sub(i_of_term vs t1, i_of_term vs t2))
   1.261 +  | Const (@{const_name Rings.dvd}, _) $ t1 $ t2 =>
   1.262 +      (Proc.Dvd (dest_number t1, i_of_term vs t2)
   1.263          handle TERM _ => raise COOPER "reification: unsupported dvd")
   1.264 -  | @{term "op = :: int => _"}$t1$t2 => Cooper_Procedure.Eq (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
   1.265 -  | @{term "op = :: bool => _ "}$t1$t2 => Cooper_Procedure.Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
   1.266 -  | Const("op &",_)$t1$t2 => Cooper_Procedure.And(qf_of_term ps vs t1,qf_of_term ps vs t2)
   1.267 -  | Const("op |",_)$t1$t2 => Cooper_Procedure.Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
   1.268 -  | Const("op -->",_)$t1$t2 => Cooper_Procedure.Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
   1.269 -  | Const (@{const_name Not},_)$t' => Cooper_Procedure.Not(qf_of_term ps vs t')
   1.270 -  | Const("Ex",_)$Abs(xn,xT,p) =>
   1.271 +  | @{term "op = :: int => _"} $ t1 $ t2 => Proc.Eq (Proc.Sub (i_of_term vs t1, i_of_term vs t2))
   1.272 +  | @{term "op = :: bool => _ "} $ t1 $ t2 => Proc.Iff (qf_of_term ps vs t1, qf_of_term ps vs t2)
   1.273 +  | Const ("op &", _) $ t1 $t2 => Proc.And (qf_of_term ps vs t1, qf_of_term ps vs t2)
   1.274 +  | Const ("op |", _) $ t1 $ t2 => Proc.Or (qf_of_term ps vs t1, qf_of_term ps vs t2)
   1.275 +  | Const ("op -->", _) $ t1 $t2 => Proc.Imp (qf_of_term ps vs t1, qf_of_term ps vs t2)
   1.276 +  | Const (@{const_name Not}, _) $ t' => Proc.Not (qf_of_term ps vs t')
   1.277 +  | Const ("Ex", _) $ Abs (xn, xT, p) =>
   1.278       let val (xn',p') = variant_abs (xn,xT,p)
   1.279 -         val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
   1.280 -     in Cooper_Procedure.E (qf_of_term ps vs' p')
   1.281 +         val vs' = ((xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
   1.282 +     in Proc.E (qf_of_term ps vs' p')
   1.283       end
   1.284 -  | Const("All",_)$Abs(xn,xT,p) =>
   1.285 +  | Const("All", _) $ Abs (xn, xT, p) =>
   1.286       let val (xn',p') = variant_abs (xn,xT,p)
   1.287 -         val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
   1.288 -     in Cooper_Procedure.A (qf_of_term ps vs' p')
   1.289 +         val vs' = ((xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
   1.290 +     in Proc.A (qf_of_term ps vs' p')
   1.291       end
   1.292    | _ =>(case AList.lookup (op aconv) ps t of
   1.293             NONE => raise COOPER "reification: unknown term"
   1.294 -         | SOME n => Cooper_Procedure.Closed n);
   1.295 +         | SOME n => Proc.Closed n);
   1.296  
   1.297  fun term_of_i vs t = case t
   1.298 - of Cooper_Procedure.C i => HOLogic.mk_number HOLogic.intT i
   1.299 -  | Cooper_Procedure.Bound n => the (AList.lookup (op =) vs n)
   1.300 -  | Cooper_Procedure.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
   1.301 -  | Cooper_Procedure.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   1.302 -  | Cooper_Procedure.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   1.303 -  | Cooper_Procedure.Mul (i, t2) => @{term "op * :: int => _"} $
   1.304 + of Proc.C i => HOLogic.mk_number HOLogic.intT i
   1.305 +  | Proc.Bound n => Free (the (AList.lookup (op =) vs n))
   1.306 +  | Proc.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
   1.307 +  | Proc.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   1.308 +  | Proc.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   1.309 +  | Proc.Mul (i, t2) => @{term "op * :: int => _"} $
   1.310        HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
   1.311 -  | Cooper_Procedure.Cn (n, i, t') => term_of_i vs (Cooper_Procedure.Add (Cooper_Procedure.Mul (i, Cooper_Procedure.Bound n), t'));
   1.312 +  | Proc.Cn (n, i, t') => term_of_i vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
   1.313  
   1.314  fun term_of_qf ps vs t =
   1.315   case t of
   1.316 -   Cooper_Procedure.T => HOLogic.true_const
   1.317 - | Cooper_Procedure.F => HOLogic.false_const
   1.318 - | Cooper_Procedure.Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   1.319 - | Cooper_Procedure.Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
   1.320 - | Cooper_Procedure.Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   1.321 - | Cooper_Procedure.Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   1.322 - | Cooper_Procedure.Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   1.323 - | Cooper_Procedure.NEq t' => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Eq t'))
   1.324 - | Cooper_Procedure.Dvd(i,t') => @{term "op dvd :: int => _ "} $
   1.325 +   Proc.T => HOLogic.true_const
   1.326 + | Proc.F => HOLogic.false_const
   1.327 + | Proc.Lt t' => @{term "op < :: int => _ "} $ term_of_i vs t' $ @{term "0::int"}
   1.328 + | Proc.Le t' => @{term "op <= :: int => _ "} $ term_of_i vs t' $ @{term "0::int"}
   1.329 + | Proc.Gt t' => @{term "op < :: int => _ "} $ @{term "0::int"} $ term_of_i vs t'
   1.330 + | Proc.Ge t' => @{term "op <= :: int => _ "} $ @{term "0::int"} $ term_of_i vs t'
   1.331 + | Proc.Eq t' => @{term "op = :: int => _ "} $ term_of_i vs t'$ @{term "0::int"}
   1.332 + | Proc.NEq t' => term_of_qf ps vs (Proc.Not (Proc.Eq t'))
   1.333 + | Proc.Dvd (i, t') => @{term "op dvd :: int => _ "} $
   1.334      HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
   1.335 - | Cooper_Procedure.NDvd(i,t')=> term_of_qf ps vs (Cooper_Procedure.Not(Cooper_Procedure.Dvd(i,t')))
   1.336 - | Cooper_Procedure.Not t' => HOLogic.Not$(term_of_qf ps vs t')
   1.337 - | Cooper_Procedure.And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   1.338 - | Cooper_Procedure.Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   1.339 - | Cooper_Procedure.Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   1.340 - | Cooper_Procedure.Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   1.341 - | Cooper_Procedure.Closed n => the (AList.lookup (op =) ps n)
   1.342 - | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n));
   1.343 + | Proc.NDvd (i, t')=> term_of_qf ps vs (Proc.Not (Proc.Dvd (i, t')))
   1.344 + | Proc.Not t' => HOLogic.Not $ term_of_qf ps vs t'
   1.345 + | Proc.And (t1, t2) => HOLogic.conj $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   1.346 + | Proc.Or (t1, t2) => HOLogic.disj $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   1.347 + | Proc.Imp (t1, t2) => HOLogic.imp $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   1.348 + | Proc.Iff (t1, t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   1.349 + | Proc.Closed n => the (AList.lookup (op =) ps n)
   1.350 + | Proc.NClosed n => term_of_qf ps vs (Proc.Not (Proc.Closed n));
   1.351  
   1.352  fun invoke t =
   1.353    let
   1.354 -    val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
   1.355 +    val vs = map_index swap (Term.add_frees t []);
   1.356 +    val ps = map_index swap (add_bools t []);
   1.357    in
   1.358      Logic.mk_equals (HOLogic.mk_Trueprop t,
   1.359 -      HOLogic.mk_Trueprop (term_of_qf (map swap ps) (map swap vs) (Cooper_Procedure.pa (qf_of_term ps vs t))))
   1.360 +      HOLogic.mk_Trueprop (term_of_qf (map swap ps) (map swap vs) (Proc.pa (qf_of_term ps vs t))))
   1.361    end;
   1.362  
   1.363 +end;
   1.364 +
   1.365  val (_, oracle) = Context.>>> (Context.map_theory_result
   1.366    (Thm.add_oracle (Binding.name "cooper",
   1.367      (fn (ctxt, t) => Thm.cterm_of (ProofContext.theory_of ctxt) (invoke t)))));
   1.368 @@ -730,7 +726,7 @@
   1.369   | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
   1.370   | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
   1.371   | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
   1.372 - | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
   1.373 + | _ => is_number t orelse can HOLogic.dest_nat t
   1.374  
   1.375   fun ty cts t = 
   1.376   if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false