avoid polymorphic equality;
authorwenzelm
Thu Jul 05 00:06:20 2007 +0200 (2007-07-05)
changeset 2358294d0dd87cc24
parent 23581 297c6d706322
child 23583 00751df1f98c
avoid polymorphic equality;
Numeral.mk_cnumber;
src/HOL/Tools/Qelim/cooper.ML
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu Jul 05 00:06:19 2007 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Jul 05 00:06:20 2007 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4  structure Cooper: COOPER =
     1.5  struct
     1.6  open Conv;
     1.7 -open Normalizer;
     1.8  structure Integertab = TableFun(type key = Integer.int val ord = Integer.ord);
     1.9  exception COOPER of string * exn;
    1.10  val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
    1.11 @@ -321,8 +320,8 @@
    1.12      val th = 
    1.13       Simplifier.rewrite lin_ss 
    1.14        (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} 
    1.15 -           (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (mk_cnumber @{ctyp "int"} x)) 
    1.16 -           @{cterm "0::int"})))
    1.17 +         (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x)) 
    1.18 +         @{cterm "0::int"})))
    1.19     in equal_elim (Thm.symmetric th) TrueI end;
    1.20    val notz = let val tab = fold Integertab.update 
    1.21                                 (ds ~~ (map (fn x => nzprop (Integer.div l x)) ds)) Integertab.empty 
    1.22 @@ -358,7 +357,7 @@
    1.23      else Thm.reflexive t
    1.24    | _ => Thm.reflexive t
    1.25    val uth = unit_conv p
    1.26 -  val clt =  mk_cnumber @{ctyp "int"} l
    1.27 +  val clt = Numeral.mk_cnumber @{ctyp "int"} l
    1.28    val ltx = Thm.capply (Thm.capply cmulC clt) cx
    1.29    val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
    1.30    val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
    1.31 @@ -405,14 +404,14 @@
    1.32    | _ => (bacc, aacc, dacc)
    1.33   val (b0,a0,ds) = h p ([],[],[])
    1.34   val d = fold Integer.lcm ds 1
    1.35 - val cd = mk_cnumber @{ctyp "int"} d
    1.36 + val cd = Numeral.mk_cnumber @{ctyp "int"} d
    1.37   val dt = term_of cd
    1.38   fun divprop x = 
    1.39     let 
    1.40      val th = 
    1.41       Simplifier.rewrite lin_ss 
    1.42        (Thm.capply @{cterm Trueprop} 
    1.43 -           (Thm.capply (Thm.capply dvdc (mk_cnumber @{ctyp "int"} x)) cd))
    1.44 +           (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
    1.45     in equal_elim (Thm.symmetric th) TrueI end;
    1.46   val dvd = let val tab = fold Integertab.update
    1.47                                 (ds ~~ (map divprop ds)) Integertab.empty in 
    1.48 @@ -613,7 +612,7 @@
    1.49  fun myassoc2 l v =
    1.50      case l of
    1.51  	[] => NONE
    1.52 -      | (x,v')::xs => if v = v' then SOME x
    1.53 +      | (x,v': int)::xs => if v = v' then SOME x
    1.54  		      else myassoc2 xs v;
    1.55  
    1.56  fun term_of_i vs t =