src/HOL/Tools/Qelim/cooper.ML
changeset 23881 851c74f1bb69
parent 23713 db10cf19f1f8
child 24075 366d4d234814
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Jul 20 14:28:05 2007 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Jul 20 14:28:25 2007 +0200
     1.3 @@ -74,10 +74,10 @@
     1.4  | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
     1.5  | Const("Not",_) $ (Const ("op =",_)$y$_) => 
     1.6    if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
     1.7 -| Const ("Orderings.ord_class.less",_)$y$z =>
     1.8 +| Const (@{const_name HOL.less}, _) $ y$ z =>
     1.9     if term_of x aconv y then Lt (Thm.dest_arg ct) 
    1.10     else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
    1.11 -| Const ("Orderings.ord_class.less_eq",_)$y$z => 
    1.12 +| Const (@{const_name HOL.less_eq}, _) $ y $ z => 
    1.13     if term_of x aconv y then Le (Thm.dest_arg ct) 
    1.14     else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
    1.15  | Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) =>
    1.16 @@ -222,10 +222,10 @@
    1.17    end 
    1.18   | _ => addC$(mulC$one$tm)$zero;
    1.19  
    1.20 -fun lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less",T)$s$t)) = 
    1.21 -    lin vs (Const("Orderings.ord_class.less_eq",T)$t$s)
    1.22 -  | lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less_eq",T)$s$t)) = 
    1.23 -    lin vs (Const("Orderings.ord_class.less",T)$t$s)
    1.24 +fun lin (vs as x::_) (Const("Not", _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) = 
    1.25 +    lin vs (Const(@{const_name HOL.less_eq}, T) $ t $ s)
    1.26 +  | lin (vs as x::_) (Const("Not",_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) = 
    1.27 +    lin vs (Const(@{const_name HOL.less}, T) $ t $ s)
    1.28    | lin vs (Const ("Not",T)$t) = Const ("Not",T)$ (lin vs t)
    1.29    | lin (vs as x::_) (Const(@{const_name Divides.dvd},_)$d$t) = 
    1.30      HOLogic.mk_binrel @{const_name Divides.dvd} (numeral1 abs d, lint vs t)
    1.31 @@ -298,12 +298,12 @@
    1.32    fun h (acc,dacc) t = 
    1.33     case (term_of t) of
    1.34      Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
    1.35 -    if x aconv y 
    1.36 -       andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
    1.37 +    if x aconv y andalso member (op =)
    1.38 +      ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
    1.39      then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
    1.40    | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => 
    1.41 -    if x aconv y 
    1.42 -       andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
    1.43 +    if x aconv y andalso member (op =)
    1.44 +       [@{const_name HOL.less}, @{const_name HOL.less_eq}] s 
    1.45      then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
    1.46    | Const(@{const_name Divides.dvd},_)$_$(Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_) => 
    1.47      if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
    1.48 @@ -338,10 +338,12 @@
    1.49    | Const("op |",_)$_$_ => binop_conv unit_conv t
    1.50    | Const("Not",_)$_ => arg_conv unit_conv t
    1.51    | Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
    1.52 -    if x=y andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
    1.53 +    if x=y andalso member (op =)
    1.54 +      ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
    1.55      then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
    1.56    | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => 
    1.57 -    if x=y andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
    1.58 +    if x=y andalso member (op =)
    1.59 +      [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
    1.60      then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
    1.61    | Const(@{const_name Divides.dvd},_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) => 
    1.62      if x=y then 
    1.63 @@ -559,8 +561,8 @@
    1.64  fun qf_of_term ps vs t =  case t
    1.65   of Const("True",_) => T
    1.66    | Const("False",_) => F
    1.67 -  | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
    1.68 -  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
    1.69 +  | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
    1.70 +  | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
    1.71    | Const(@{const_name Divides.dvd},_)$t1$t2 => 
    1.72        (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
    1.73    | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))