src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 35267 8dfd816713c6
parent 35092 cfe605c54e50
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 19 14:47:00 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 19 14:47:01 2010 +0100
     1.3 @@ -2947,10 +2947,10 @@
     1.4  fun rrelT rT = [rT,rT] ---> rT;
     1.5  fun rrT rT = [rT, rT] ---> bT;
     1.6  fun divt rT = Const(@{const_name Rings.divide},rrelT rT);
     1.7 -fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
     1.8 -fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
     1.9 -fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
    1.10 -fun uminust rT = Const(@{const_name Algebras.uminus}, rT --> rT);
    1.11 +fun timest rT = Const(@{const_name Groups.times},rrelT rT);
    1.12 +fun plust rT = Const(@{const_name Groups.plus},rrelT rT);
    1.13 +fun minust rT = Const(@{const_name Groups.minus},rrelT rT);
    1.14 +fun uminust rT = Const(@{const_name Groups.uminus}, rT --> rT);
    1.15  fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
    1.16  val brT = [bT, bT] ---> bT;
    1.17  val nott = @{term "Not"};
    1.18 @@ -2961,7 +2961,7 @@
    1.19  fun llt rT = Const(@{const_name Orderings.less},rrT rT);
    1.20  fun lle rT = Const(@{const_name Orderings.less},rrT rT);
    1.21  fun eqt rT = Const("op =",rrT rT);
    1.22 -fun rz rT = Const(@{const_name Algebras.zero},rT);
    1.23 +fun rz rT = Const(@{const_name Groups.zero},rT);
    1.24  
    1.25  fun dest_nat t = case t of
    1.26    Const ("Suc",_)$t' => 1 + dest_nat t'
    1.27 @@ -2969,10 +2969,10 @@
    1.28  
    1.29  fun num_of_term m t = 
    1.30   case t of
    1.31 -   Const(@{const_name Algebras.uminus},_)$t => @{code poly.Neg} (num_of_term m t)
    1.32 - | Const(@{const_name Algebras.plus},_)$a$b => @{code poly.Add} (num_of_term m a, num_of_term m b)
    1.33 - | Const(@{const_name Algebras.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
    1.34 - | Const(@{const_name Algebras.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
    1.35 +   Const(@{const_name Groups.uminus},_)$t => @{code poly.Neg} (num_of_term m t)
    1.36 + | Const(@{const_name Groups.plus},_)$a$b => @{code poly.Add} (num_of_term m a, num_of_term m b)
    1.37 + | Const(@{const_name Groups.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
    1.38 + | Const(@{const_name Groups.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
    1.39   | Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
    1.40   | Const(@{const_name Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.41   | _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1) 
    1.42 @@ -2980,10 +2980,10 @@
    1.43  
    1.44  fun tm_of_term m m' t = 
    1.45   case t of
    1.46 -   Const(@{const_name Algebras.uminus},_)$t => @{code Neg} (tm_of_term m m' t)
    1.47 - | Const(@{const_name Algebras.plus},_)$a$b => @{code Add} (tm_of_term m m' a, tm_of_term m m' b)
    1.48 - | Const(@{const_name Algebras.minus},_)$a$b => @{code Sub} (tm_of_term m m' a, tm_of_term m m' b)
    1.49 - | Const(@{const_name Algebras.times},_)$a$b => @{code Mul} (num_of_term m' a, tm_of_term m m' b)
    1.50 +   Const(@{const_name Groups.uminus},_)$t => @{code Neg} (tm_of_term m m' t)
    1.51 + | Const(@{const_name Groups.plus},_)$a$b => @{code Add} (tm_of_term m m' a, tm_of_term m m' b)
    1.52 + | Const(@{const_name Groups.minus},_)$a$b => @{code Sub} (tm_of_term m m' a, tm_of_term m m' b)
    1.53 + | Const(@{const_name Groups.times},_)$a$b => @{code Mul} (num_of_term m' a, tm_of_term m m' b)
    1.54   | _ => (@{code CP} (num_of_term m' t) 
    1.55           handle TERM _ => @{code Bound} (AList.lookup (op aconv) m t |> the)
    1.56                | Option => @{code Bound} (AList.lookup (op aconv) m t |> the));