src/HOL/Tools/Qelim/cooper.ML
changeset 24630 351a308ab58d
parent 24584 01e83ffa6c54
child 25768 1c1ca4b20ec6
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Sep 18 11:06:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Sep 18 16:08:00 2007 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4  
     1.5  open Conv;
     1.6  open Normalizer;
     1.7 -structure Integertab = TableFun(type key = Integer.int val ord = Integer.ord);
     1.8  
     1.9  exception COOPER of string * exn;
    1.10  val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
    1.11 @@ -178,10 +177,10 @@
    1.12    | linear_cmul n tm = 
    1.13      case tm of  
    1.14        Const("HOL.plus_class.plus",_)$a$b => addC$(linear_cmul n a)$(linear_cmul n b)
    1.15 -    | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (Integer.mult n) c)$x
    1.16 +    | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (fn m => n * m) c)$x
    1.17      | Const("HOL.minus_class.minus",_)$a$b => subC$(linear_cmul n a)$(linear_cmul n b)
    1.18      | (m as Const("HOL.minus_class.uminus",_))$a => m$(linear_cmul n a)
    1.19 -    | _ =>  numeral1 (Integer.mult n) tm;
    1.20 +    | _ =>  numeral1 (fn m => n * m) tm;
    1.21  fun earlier [] x y = false 
    1.22  	| earlier (h::t) x y = 
    1.23      if h aconv y then false else if h aconv x then true else earlier t x y; 
    1.24 @@ -191,7 +190,7 @@
    1.25  	 (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c1$x1)$r1,
    1.26      Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) => 
    1.27     if x1 = x2 then 
    1.28 -     let val c = numeral2 Integer.add c1 c2
    1.29 +     let val c = numeral2 (curry op +) c1 c2
    1.30  	   in if c = zero then linear_add vars r1  r2  
    1.31  	      else addC$(mulC$c$x1)$(linear_add vars  r1 r2)
    1.32       end 
    1.33 @@ -201,7 +200,7 @@
    1.34      	  addC$(mulC$c1$x1)$(linear_add vars r1 tm2)
    1.35   | (_, Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) => 
    1.36        	  addC$(mulC$c2$x2)$(linear_add vars tm1 r2) 
    1.37 - | (_,_) => numeral2 Integer.add tm1 tm2;
    1.38 + | (_,_) => numeral2 (curry op +) tm1 tm2;
    1.39   
    1.40  fun linear_neg tm = linear_cmul ~1 tm; 
    1.41  fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); 
    1.42 @@ -294,7 +293,7 @@
    1.43   let
    1.44    val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
    1.45    val x = term_of cx 
    1.46 -  val ins = insert (op = : integer*integer -> bool)
    1.47 +  val ins = insert (op = : int * int -> bool)
    1.48    fun h (acc,dacc) t = 
    1.49     case (term_of t) of
    1.50      Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
    1.51 @@ -312,7 +311,7 @@
    1.52    | Const("Not",_)$_ => h (acc,dacc) (Thm.dest_arg t)
    1.53    | _ => (acc, dacc)
    1.54    val (cs,ds) = h ([],[]) p
    1.55 -  val l = fold Integer.lcm (cs union ds) 1
    1.56 +  val l = Integer.lcms (cs union ds)
    1.57    fun cv k ct = 
    1.58      let val (tm as b$s$t) = term_of ct 
    1.59      in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
    1.60 @@ -325,10 +324,10 @@
    1.61             (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x)) 
    1.62             @{cterm "0::int"})))
    1.63     in equal_elim (Thm.symmetric th) TrueI end;
    1.64 -  val notz = let val tab = fold Integertab.update 
    1.65 -                               (ds ~~ (map (fn x => nzprop (Integer.div l x)) ds)) Integertab.empty 
    1.66 +  val notz = let val tab = fold Inttab.update 
    1.67 +                               (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty 
    1.68              in 
    1.69 -             (fn ct => (valOf (Integertab.lookup tab (ct |> term_of |> dest_numeral)) 
    1.70 +             (fn ct => (valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral)) 
    1.71                  handle Option => (writeln "noz: Theorems-Table contains no entry for"; 
    1.72                                      print_cterm ct ; raise Option)))
    1.73             end
    1.74 @@ -340,15 +339,15 @@
    1.75    | Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
    1.76      if x=y andalso member (op =)
    1.77        ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
    1.78 -    then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
    1.79 +    then cv (l div dest_numeral c) t else Thm.reflexive t
    1.80    | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => 
    1.81      if x=y andalso member (op =)
    1.82        [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
    1.83 -    then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
    1.84 +    then cv (l div dest_numeral c) t else Thm.reflexive t
    1.85    | Const(@{const_name Divides.dvd},_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) => 
    1.86      if x=y then 
    1.87        let 
    1.88 -       val k = Integer.div l (dest_numeral c)
    1.89 +       val k = l div dest_numeral c
    1.90         val kt = HOLogic.mk_number iT k
    1.91         val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] 
    1.92               ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
    1.93 @@ -384,7 +383,6 @@
    1.94  
    1.95  val D_tm = @{cpat "?D::int"};
    1.96  
    1.97 -val int_eq = (op =):integer*integer -> bool;
    1.98  fun cooperex_conv ctxt vs q = 
    1.99  let 
   1.100  
   1.101 @@ -403,11 +401,11 @@
   1.102    | Le t => (bacc, ins (plus1 t) aacc,dacc)
   1.103    | Gt t => (ins t bacc, aacc,dacc)
   1.104    | Ge t => (ins (minus1 t) bacc, aacc,dacc)
   1.105 -  | Dvd (d,s) => (bacc,aacc,insert int_eq (term_of d |> dest_numeral) dacc)
   1.106 -  | NDvd (d,s) => (bacc,aacc,insert int_eq (term_of d|> dest_numeral) dacc)
   1.107 +  | Dvd (d,s) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
   1.108 +  | NDvd (d,s) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
   1.109    | _ => (bacc, aacc, dacc)
   1.110   val (b0,a0,ds) = h p ([],[],[])
   1.111 - val d = fold Integer.lcm ds 1
   1.112 + val d = Integer.lcms ds
   1.113   val cd = Numeral.mk_cnumber @{ctyp "int"} d
   1.114   val dt = term_of cd
   1.115   fun divprop x = 
   1.116 @@ -417,9 +415,9 @@
   1.117        (Thm.capply @{cterm Trueprop} 
   1.118             (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
   1.119     in equal_elim (Thm.symmetric th) TrueI end;
   1.120 - val dvd = let val tab = fold Integertab.update
   1.121 -                               (ds ~~ (map divprop ds)) Integertab.empty in 
   1.122 -           (fn ct => (valOf (Integertab.lookup tab (term_of ct |> dest_numeral)) 
   1.123 + val dvd = let val tab = fold Inttab.update
   1.124 +                               (ds ~~ (map divprop ds)) Inttab.empty in 
   1.125 +           (fn ct => (valOf (Inttab.lookup tab (term_of ct |> dest_numeral)) 
   1.126                      handle Option => (writeln "dvd: Theorems-Table contains no entry for"; 
   1.127                                        print_cterm ct ; raise Option)))
   1.128             end
   1.129 @@ -545,7 +543,7 @@
   1.130        | SOME n => Bound n)
   1.131    | @{term "0::int"} => C 0
   1.132    | @{term "1::int"} => C 1
   1.133 -  | Term.Bound i => Bound (Integer.int i)
   1.134 +  | Term.Bound i => Bound i
   1.135    | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
   1.136    | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
   1.137    | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
   1.138 @@ -641,8 +639,7 @@
   1.139  
   1.140  fun cooper_oracle thy t = 
   1.141    let
   1.142 -    val (vs, ps) = pairself (map_index (swap o apfst Integer.int))
   1.143 -      (term_frees t, term_bools [] t);
   1.144 +    val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
   1.145    in
   1.146      equals propT $ HOLogic.mk_Trueprop t $
   1.147        HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))