using code antiquotation
authorhaftmann
Mon Feb 08 17:12:22 2010 +0100 (2010-02-08)
changeset 35045a77d200e6503
parent 35044 7c761a4bd91f
child 35046 1266f04f42ec
using code antiquotation
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 08 17:12:18 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 08 17:12:22 2010 +0100
     1.3 @@ -7,9 +7,9 @@
     1.4  theory Parametric_Ferrante_Rackoff
     1.5  imports Reflected_Multivariate_Polynomial 
     1.6    "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     1.7 +  Efficient_Nat
     1.8  begin
     1.9  
    1.10 -
    1.11  subsection {* Terms *}
    1.12  
    1.13  datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm 
    1.14 @@ -2594,13 +2594,6 @@
    1.15    by (simp add: Let_def stupid)
    1.16  
    1.17  
    1.18 -
    1.19 -(*
    1.20 -lemmas [code func] = polysub_def
    1.21 -lemmas [code func del] = Zero_nat_def
    1.22 -code_gen  "frpar" in SML to FRParTest
    1.23 -*)
    1.24 -
    1.25  section{* Second implemenation: Case splits not local *}
    1.26  
    1.27  lemma fr_eq2:  assumes lp: "islin p"
    1.28 @@ -2945,14 +2938,7 @@
    1.29  show ?thesis  unfolding frpar2_def by (auto simp add: prep)
    1.30  qed
    1.31  
    1.32 -code_module FRPar
    1.33 -  contains 
    1.34 -  frpar = "frpar"
    1.35 -  frpar2 = "frpar2"
    1.36 -  test = "%x . frpar (E(Lt (Mul 1\<^sub>p (Bound 0))))"
    1.37 -
    1.38 -ML{* 
    1.39 -
    1.40 +ML {* 
    1.41  structure ReflectedFRPar = 
    1.42  struct
    1.43  
    1.44 @@ -2983,92 +2969,93 @@
    1.45  
    1.46  fun num_of_term m t = 
    1.47   case t of
    1.48 -   Const(@{const_name Algebras.uminus},_)$t => FRPar.Neg (num_of_term m t)
    1.49 - | Const(@{const_name Algebras.plus},_)$a$b => FRPar.Add (num_of_term m a, num_of_term m b)
    1.50 - | Const(@{const_name Algebras.minus},_)$a$b => FRPar.Sub (num_of_term m a, num_of_term m b)
    1.51 - | Const(@{const_name Algebras.times},_)$a$b => FRPar.Mul (num_of_term m a, num_of_term m b)
    1.52 - | Const(@{const_name Power.power},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
    1.53 - | Const(@{const_name Algebras.divide},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.54 - | _ => (FRPar.C (HOLogic.dest_number t |> snd,1) 
    1.55 -         handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> the));
    1.56 +   Const(@{const_name Algebras.uminus},_)$t => @{code poly.Neg} (num_of_term m t)
    1.57 + | Const(@{const_name Algebras.plus},_)$a$b => @{code poly.Add} (num_of_term m a, num_of_term m b)
    1.58 + | Const(@{const_name Algebras.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
    1.59 + | Const(@{const_name Algebras.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
    1.60 + | Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
    1.61 + | Const(@{const_name Algebras.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.62 + | _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1) 
    1.63 +         handle TERM _ => @{code poly.Bound} (AList.lookup (op aconv) m t |> the));
    1.64  
    1.65  fun tm_of_term m m' t = 
    1.66   case t of
    1.67 -   Const(@{const_name Algebras.uminus},_)$t => FRPar.tm_Neg (tm_of_term m m' t)
    1.68 - | Const(@{const_name Algebras.plus},_)$a$b => FRPar.tm_Add (tm_of_term m m' a, tm_of_term m m' b)
    1.69 - | Const(@{const_name Algebras.minus},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
    1.70 - | Const(@{const_name Algebras.times},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
    1.71 - | _ => (FRPar.CP (num_of_term m' t) 
    1.72 -         handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the)
    1.73 -              | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the));
    1.74 +   Const(@{const_name Algebras.uminus},_)$t => @{code Neg} (tm_of_term m m' t)
    1.75 + | Const(@{const_name Algebras.plus},_)$a$b => @{code Add} (tm_of_term m m' a, tm_of_term m m' b)
    1.76 + | Const(@{const_name Algebras.minus},_)$a$b => @{code Sub} (tm_of_term m m' a, tm_of_term m m' b)
    1.77 + | Const(@{const_name Algebras.times},_)$a$b => @{code Mul} (num_of_term m' a, tm_of_term m m' b)
    1.78 + | _ => (@{code CP} (num_of_term m' t) 
    1.79 +         handle TERM _ => @{code Bound} (AList.lookup (op aconv) m t |> the)
    1.80 +              | Option => @{code Bound} (AList.lookup (op aconv) m t |> the));
    1.81  
    1.82  fun term_of_num T m t = 
    1.83   case t of
    1.84 -  FRPar.C (a,b) => (if b = 1 then num T a else if b=0 then (rz T) 
    1.85 +  @{code poly.C} (a,b) => (if b = 1 then num T a else if b=0 then (rz T) 
    1.86                                          else (divt T) $ num T a $ num T b)
    1.87 -| FRPar.Bound i => AList.lookup (op = : int*int -> bool) m i |> the
    1.88 -| FRPar.Add(a,b) => (plust T)$(term_of_num T m a)$(term_of_num T m b)
    1.89 -| FRPar.Mul(a,b) => (timest T)$(term_of_num T m a)$(term_of_num T m b)
    1.90 -| FRPar.Sub(a,b) => (minust T)$(term_of_num T m a)$(term_of_num T m b)
    1.91 -| FRPar.Neg a => (uminust T)$(term_of_num T m a)
    1.92 -| FRPar.Pw(a,n) => (powt T)$(term_of_num T m t)$(HOLogic.mk_number HOLogic.natT n)
    1.93 -| FRPar.CN(c,n,p) => term_of_num T m (FRPar.Add(c,FRPar.Mul(FRPar.Bound n, p)))
    1.94 +| @{code poly.Bound} i => AList.lookup (op = : int*int -> bool) m i |> the
    1.95 +| @{code poly.Add} (a,b) => (plust T)$(term_of_num T m a)$(term_of_num T m b)
    1.96 +| @{code poly.Mul} (a,b) => (timest T)$(term_of_num T m a)$(term_of_num T m b)
    1.97 +| @{code poly.Sub} (a,b) => (minust T)$(term_of_num T m a)$(term_of_num T m b)
    1.98 +| @{code poly.Neg} a => (uminust T)$(term_of_num T m a)
    1.99 +| @{code poly.Pw} (a,n) => (powt T)$(term_of_num T m t)$(HOLogic.mk_number HOLogic.natT n)
   1.100 +| @{code poly.CN} (c,n,p) => term_of_num T m (@{code poly.Add} (c, @{code poly.Mul} (@{code poly.Bound} n, p)))
   1.101  | _ => error "term_of_num: Unknown term";
   1.102  
   1.103  fun term_of_tm T m m' t = 
   1.104   case t of
   1.105 -  FRPar.CP p => term_of_num T m' p
   1.106 -| FRPar.tm_Bound i => AList.lookup (op = : int*int -> bool) m i |> the
   1.107 -| FRPar.tm_Add(a,b) => (plust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
   1.108 -| FRPar.tm_Mul(a,b) => (timest T)$(term_of_num T m' a)$(term_of_tm T m m' b)
   1.109 -| FRPar.tm_Sub(a,b) => (minust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
   1.110 -| FRPar.tm_Neg a => (uminust T)$(term_of_tm T m m' a)
   1.111 -| FRPar.CNP(n,c,p) => term_of_tm T m m' (FRPar.tm_Add(FRPar.tm_Mul(c, FRPar.tm_Bound n), p))
   1.112 +  @{code CP} p => term_of_num T m' p
   1.113 +| @{code Bound} i => AList.lookup (op = : int*int -> bool) m i |> the
   1.114 +| @{code Add} (a,b) => (plust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
   1.115 +| @{code Mul} (a,b) => (timest T)$(term_of_num T m' a)$(term_of_tm T m m' b)
   1.116 +| @{code Sub} (a,b) => (minust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
   1.117 +| @{code Neg} a => (uminust T)$(term_of_tm T m m' a)
   1.118 +| @{code CNP} (n,c,p) => term_of_tm T m m' (@{code Add}
   1.119 +     (@{code Mul} (c, @{code Bound} n), p))
   1.120  | _ => error "term_of_tm: Unknown term";
   1.121  
   1.122  fun fm_of_term m m' fm = 
   1.123   case fm of
   1.124 -    Const("True",_) => FRPar.T
   1.125 -  | Const("False",_) => FRPar.F
   1.126 -  | Const("Not",_)$p => FRPar.NOT (fm_of_term m m' p)
   1.127 -  | Const("op &",_)$p$q => FRPar.And(fm_of_term m m' p, fm_of_term m m' q)
   1.128 -  | Const("op |",_)$p$q => FRPar.Or(fm_of_term m m' p, fm_of_term m m' q)
   1.129 -  | Const("op -->",_)$p$q => FRPar.Imp(fm_of_term m m' p, fm_of_term m m' q)
   1.130 +    Const("True",_) => @{code T}
   1.131 +  | Const("False",_) => @{code F}
   1.132 +  | Const("Not",_)$p => @{code NOT} (fm_of_term m m' p)
   1.133 +  | Const("op &",_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
   1.134 +  | Const("op |",_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
   1.135 +  | Const("op -->",_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
   1.136    | Const("op =",ty)$p$q => 
   1.137 -       if domain_type ty = bT then FRPar.Iff(fm_of_term m m' p, fm_of_term m m' q)
   1.138 -       else FRPar.Eq (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
   1.139 +       if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
   1.140 +       else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
   1.141    | Const(@{const_name Algebras.less},_)$p$q => 
   1.142 -        FRPar.Lt (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
   1.143 +        @{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
   1.144    | Const(@{const_name Algebras.less_eq},_)$p$q => 
   1.145 -        FRPar.Le (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
   1.146 +        @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
   1.147    | Const("Ex",_)$Abs(xn,xT,p) => 
   1.148       let val (xn', p') =  variant_abs (xn,xT,p)
   1.149           val x = Free(xn',xT)
   1.150           fun incr i = i + 1
   1.151           val m0 = (x,0):: (map (apsnd incr) m)
   1.152 -      in FRPar.E (fm_of_term m0 m' p') end
   1.153 +      in @{code E} (fm_of_term m0 m' p') end
   1.154    | Const("All",_)$Abs(xn,xT,p) => 
   1.155       let val (xn', p') =  variant_abs (xn,xT,p)
   1.156           val x = Free(xn',xT)
   1.157           fun incr i = i + 1
   1.158           val m0 = (x,0):: (map (apsnd incr) m)
   1.159 -      in FRPar.A (fm_of_term m0 m' p') end
   1.160 +      in @{code A} (fm_of_term m0 m' p') end
   1.161    | _ => error "fm_of_term";
   1.162  
   1.163  
   1.164  fun term_of_fm T m m' t = 
   1.165    case t of
   1.166 -    FRPar.T => Const("True",bT)
   1.167 -  | FRPar.F => Const("False",bT)
   1.168 -  | FRPar.NOT p => nott $ (term_of_fm T m m' p)
   1.169 -  | FRPar.And (p,q) => conjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.170 -  | FRPar.Or (p,q) => disjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.171 -  | FRPar.Imp (p,q) => impt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.172 -  | FRPar.Iff (p,q) => ifft $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.173 -  | FRPar.Lt p => (llt T) $ (term_of_tm T m m' p) $ (rz T)
   1.174 -  | FRPar.Le p => (lle T) $ (term_of_tm T m m' p) $ (rz T)
   1.175 -  | FRPar.Eq p => (eqt T) $ (term_of_tm T m m' p) $ (rz T)
   1.176 -  | FRPar.NEq p => nott $ ((eqt T) $ (term_of_tm T m m' p) $ (rz T))
   1.177 +    @{code T} => Const("True",bT)
   1.178 +  | @{code F} => Const("False",bT)
   1.179 +  | @{code NOT} p => nott $ (term_of_fm T m m' p)
   1.180 +  | @{code And} (p,q) => conjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.181 +  | @{code Or} (p,q) => disjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.182 +  | @{code Imp} (p,q) => impt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.183 +  | @{code Iff} (p,q) => ifft $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
   1.184 +  | @{code Lt} p => (llt T) $ (term_of_tm T m m' p) $ (rz T)
   1.185 +  | @{code Le} p => (lle T) $ (term_of_tm T m m' p) $ (rz T)
   1.186 +  | @{code Eq} p => (eqt T) $ (term_of_tm T m m' p) $ (rz T)
   1.187 +  | @{code NEq} p => nott $ ((eqt T) $ (term_of_tm T m m' p) $ (rz T))
   1.188    | _ => error "term_of_fm: quantifiers!!!!???";
   1.189  
   1.190  fun frpar_oracle (T,m, m', fm) = 
   1.191 @@ -3077,7 +3064,7 @@
   1.192     val im = 0 upto (length m - 1)
   1.193     val im' = 0 upto (length m' - 1)   
   1.194   in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm T (im ~~ m) (im' ~~ m')  
   1.195 -                                                     (FRPar.frpar (fm_of_term (m ~~ im) (m' ~~ im') t))))
   1.196 +                                                     (@{code frpar} (fm_of_term (m ~~ im) (m' ~~ im') t))))
   1.197   end;
   1.198  
   1.199  fun frpar_oracle2 (T,m, m', fm) = 
   1.200 @@ -3086,7 +3073,7 @@
   1.201     val im = 0 upto (length m - 1)
   1.202     val im' = 0 upto (length m' - 1)   
   1.203   in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm T (im ~~ m) (im' ~~ m')  
   1.204 -                                                     (FRPar.frpar2 (fm_of_term (m ~~ im) (m' ~~ im') t))))
   1.205 +                                                     (@{code frpar2} (fm_of_term (m ~~ im) (m' ~~ im') t))))
   1.206   end;
   1.207  
   1.208  end;