src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 34974 18b41bba42b5
parent 33639 603320b93668
child 35028 108662d50512
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Jan 28 11:48:43 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Jan 28 11:48:49 2010 +0100
     1.3 @@ -2963,11 +2963,11 @@
     1.4  fun num rT x = HOLogic.mk_number rT x;
     1.5  fun rrelT rT = [rT,rT] ---> rT;
     1.6  fun rrT rT = [rT, rT] ---> bT;
     1.7 -fun divt rT = Const(@{const_name "HOL.divide"},rrelT rT);
     1.8 -fun timest rT = Const(@{const_name "HOL.times"},rrelT rT);
     1.9 -fun plust rT = Const(@{const_name "HOL.plus"},rrelT rT);
    1.10 -fun minust rT = Const(@{const_name "HOL.minus"},rrelT rT);
    1.11 -fun uminust rT = Const(@{const_name "HOL.uminus"}, rT --> rT);
    1.12 +fun divt rT = Const(@{const_name Algebras.divide},rrelT rT);
    1.13 +fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
    1.14 +fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
    1.15 +fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
    1.16 +fun uminust rT = Const(@{const_name Algebras.uminus}, rT --> rT);
    1.17  fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
    1.18  val brT = [bT, bT] ---> bT;
    1.19  val nott = @{term "Not"};
    1.20 @@ -2975,10 +2975,10 @@
    1.21  val disjt = @{term "op |"};
    1.22  val impt = @{term "op -->"};
    1.23  val ifft = @{term "op = :: bool => _"}
    1.24 -fun llt rT = Const(@{const_name "HOL.less"},rrT rT);
    1.25 -fun lle rT = Const(@{const_name "HOL.less"},rrT rT);
    1.26 +fun llt rT = Const(@{const_name Algebras.less},rrT rT);
    1.27 +fun lle rT = Const(@{const_name Algebras.less},rrT rT);
    1.28  fun eqt rT = Const("op =",rrT rT);
    1.29 -fun rz rT = Const(@{const_name "HOL.zero"},rT);
    1.30 +fun rz rT = Const(@{const_name Algebras.zero},rT);
    1.31  
    1.32  fun dest_nat t = case t of
    1.33    Const ("Suc",_)$t' => 1 + dest_nat t'
    1.34 @@ -2986,21 +2986,21 @@
    1.35  
    1.36  fun num_of_term m t = 
    1.37   case t of
    1.38 -   Const(@{const_name "uminus"},_)$t => FRPar.Neg (num_of_term m t)
    1.39 - | Const(@{const_name "HOL.plus"},_)$a$b => FRPar.Add (num_of_term m a, num_of_term m b)
    1.40 - | Const(@{const_name "HOL.minus"},_)$a$b => FRPar.Sub (num_of_term m a, num_of_term m b)
    1.41 - | Const(@{const_name "HOL.times"},_)$a$b => FRPar.Mul (num_of_term m a, num_of_term m b)
    1.42 - | Const(@{const_name "power"},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
    1.43 - | Const(@{const_name "HOL.divide"},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.44 +   Const(@{const_name Algebras.uminus},_)$t => FRPar.Neg (num_of_term m t)
    1.45 + | Const(@{const_name Algebras.plus},_)$a$b => FRPar.Add (num_of_term m a, num_of_term m b)
    1.46 + | Const(@{const_name Algebras.minus},_)$a$b => FRPar.Sub (num_of_term m a, num_of_term m b)
    1.47 + | Const(@{const_name Algebras.times},_)$a$b => FRPar.Mul (num_of_term m a, num_of_term m b)
    1.48 + | Const(@{const_name Power.power},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
    1.49 + | Const(@{const_name Algebras.divide},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.50   | _ => (FRPar.C (HOLogic.dest_number t |> snd,1) 
    1.51           handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> the));
    1.52  
    1.53  fun tm_of_term m m' t = 
    1.54   case t of
    1.55 -   Const(@{const_name "uminus"},_)$t => FRPar.tm_Neg (tm_of_term m m' t)
    1.56 - | Const(@{const_name "HOL.plus"},_)$a$b => FRPar.tm_Add (tm_of_term m m' a, tm_of_term m m' b)
    1.57 - | Const(@{const_name "HOL.minus"},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
    1.58 - | Const(@{const_name "HOL.times"},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
    1.59 +   Const(@{const_name Algebras.uminus},_)$t => FRPar.tm_Neg (tm_of_term m m' t)
    1.60 + | Const(@{const_name Algebras.plus},_)$a$b => FRPar.tm_Add (tm_of_term m m' a, tm_of_term m m' b)
    1.61 + | Const(@{const_name Algebras.minus},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
    1.62 + | Const(@{const_name Algebras.times},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
    1.63   | _ => (FRPar.CP (num_of_term m' t) 
    1.64           handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the)
    1.65                | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the));
    1.66 @@ -3040,9 +3040,9 @@
    1.67    | Const("op =",ty)$p$q => 
    1.68         if domain_type ty = bT then FRPar.Iff(fm_of_term m m' p, fm_of_term m m' q)
    1.69         else FRPar.Eq (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
    1.70 -  | Const(@{const_name "HOL.less"},_)$p$q => 
    1.71 +  | Const(@{const_name Algebras.less},_)$p$q => 
    1.72          FRPar.Lt (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
    1.73 -  | Const(@{const_name "HOL.less_eq"},_)$p$q => 
    1.74 +  | Const(@{const_name Algebras.less_eq},_)$p$q => 
    1.75          FRPar.Le (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
    1.76    | Const("Ex",_)$Abs(xn,xT,p) => 
    1.77       let val (xn', p') =  variant_abs (xn,xT,p)