src/HOL/Tools/Qelim/cooper.ML
changeset 35267 8dfd816713c6
parent 35092 cfe605c54e50
child 35410 1ea89d2a1bd4
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Feb 19 14:47:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Feb 19 14:47:01 2010 +0100
     1.3 @@ -79,9 +79,9 @@
     1.4  | Const (@{const_name Orderings.less_eq}, _) $ y $ z =>
     1.5     if term_of x aconv y then Le (Thm.dest_arg ct)
     1.6     else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
     1.7 -| Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
     1.8 +| Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_) =>
     1.9     if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
    1.10 -| Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_)) =>
    1.11 +| Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_)) =>
    1.12     if term_of x aconv y then
    1.13     NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
    1.14  | _ => Nox)
    1.15 @@ -175,18 +175,18 @@
    1.16    (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
    1.17  fun linear_cmul 0 tm = zero
    1.18    | linear_cmul n tm = case tm of
    1.19 -      Const (@{const_name Algebras.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
    1.20 -    | Const (@{const_name Algebras.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
    1.21 -    | Const (@{const_name Algebras.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
    1.22 -    | (m as Const (@{const_name Algebras.uminus}, _)) $ a => m $ linear_cmul n a
    1.23 +      Const (@{const_name Groups.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
    1.24 +    | Const (@{const_name Groups.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
    1.25 +    | Const (@{const_name Groups.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
    1.26 +    | (m as Const (@{const_name Groups.uminus}, _)) $ a => m $ linear_cmul n a
    1.27      | _ => numeral1 (fn m => n * m) tm;
    1.28  fun earlier [] x y = false
    1.29    | earlier (h::t) x y =
    1.30      if h aconv y then false else if h aconv x then true else earlier t x y;
    1.31  
    1.32  fun linear_add vars tm1 tm2 = case (tm1, tm2) of
    1.33 -    (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1,
    1.34 -    Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
    1.35 +    (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1,
    1.36 +    Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
    1.37     if x1 = x2 then
    1.38       let val c = numeral2 Integer.add c1 c2
    1.39        in if c = zero then linear_add vars r1 r2
    1.40 @@ -194,9 +194,9 @@
    1.41       end
    1.42       else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
    1.43     else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
    1.44 - | (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1, _) =>
    1.45 + | (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) =>
    1.46        addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
    1.47 - | (_, Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
    1.48 + | (_, Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
    1.49        addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
    1.50   | (_, _) => numeral2 Integer.add tm1 tm2;
    1.51  
    1.52 @@ -205,10 +205,10 @@
    1.53  
    1.54  
    1.55  fun lint vars tm =  if is_numeral tm then tm  else case tm of
    1.56 -  Const (@{const_name Algebras.uminus}, _) $ t => linear_neg (lint vars t)
    1.57 -| Const (@{const_name Algebras.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
    1.58 -| Const (@{const_name Algebras.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
    1.59 -| Const (@{const_name Algebras.times}, _) $ s $ t =>
    1.60 +  Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
    1.61 +| Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
    1.62 +| Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
    1.63 +| Const (@{const_name Groups.times}, _) $ s $ t =>
    1.64    let val s' = lint vars s
    1.65        val t' = lint vars t
    1.66    in if is_numeral s' then (linear_cmul (dest_numeral s') t')
    1.67 @@ -270,7 +270,7 @@
    1.68        val d'' = Thm.rhs_of dth |> Thm.dest_arg1
    1.69       in
    1.70        case tt' of
    1.71 -        Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$_)$_ =>
    1.72 +        Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ =>
    1.73          let val x = dest_numeral c
    1.74          in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
    1.75                                         (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
    1.76 @@ -293,15 +293,15 @@
    1.77    val ins = insert (op = : int * int -> bool)
    1.78    fun h (acc,dacc) t =
    1.79     case (term_of t) of
    1.80 -    Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
    1.81 +    Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
    1.82      if x aconv y andalso member (op =)
    1.83        ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    1.84      then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
    1.85 -  | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
    1.86 +  | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
    1.87      if x aconv y andalso member (op =)
    1.88         [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    1.89      then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
    1.90 -  | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
    1.91 +  | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
    1.92      if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
    1.93    | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
    1.94    | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
    1.95 @@ -335,15 +335,15 @@
    1.96     Const("op &",_)$_$_ => binop_conv unit_conv t
    1.97    | Const("op |",_)$_$_ => binop_conv unit_conv t
    1.98    | Const (@{const_name Not},_)$_ => arg_conv unit_conv t
    1.99 -  | Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
   1.100 +  | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   1.101      if x=y andalso member (op =)
   1.102        ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   1.103      then cv (l div dest_numeral c) t else Thm.reflexive t
   1.104 -  | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
   1.105 +  | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
   1.106      if x=y andalso member (op =)
   1.107        [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   1.108      then cv (l div dest_numeral c) t else Thm.reflexive t
   1.109 -  | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
   1.110 +  | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) =>
   1.111      if x=y then
   1.112        let
   1.113         val k = l div dest_numeral c
   1.114 @@ -546,10 +546,10 @@
   1.115    | @{term "0::int"} => C 0
   1.116    | @{term "1::int"} => C 1
   1.117    | Term.Bound i => Bound i
   1.118 -  | Const(@{const_name Algebras.uminus},_)$t' => Neg (i_of_term vs t')
   1.119 -  | Const(@{const_name Algebras.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
   1.120 -  | Const(@{const_name Algebras.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
   1.121 -  | Const(@{const_name Algebras.times},_)$t1$t2 =>
   1.122 +  | Const(@{const_name Groups.uminus},_)$t' => Neg (i_of_term vs t')
   1.123 +  | Const(@{const_name Groups.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
   1.124 +  | Const(@{const_name Groups.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
   1.125 +  | Const(@{const_name Groups.times},_)$t1$t2 =>
   1.126       (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
   1.127      handle TERM _ =>
   1.128         (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)