src/HOL/Complex/ex/mireif.ML
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 23881 851c74f1bb69
child 25919 8b1c0d434824
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
     1 (*  Title:      HOL/Complex/ex/mireif.ML
     2     ID:         $Id$
     3     Author:     Amine Chaieb, TU Muenchen
     4 
     5 Oracle for Mixed Real-Integer auantifier elimination
     6 based on the verified code in HOL/Complex/ex/MIR.thy.
     7 *)
     8 
     9 structure ReflectedMir =
    10 struct
    11 
    12 open Mir;
    13 
    14 exception MIR;
    15 
    16 fun num_of_term vs t = 
    17     case t of
    18         Free(xn,xT) => (case AList.lookup (op =) vs t of 
    19                            NONE   => error "Variable not found in the list!"
    20                          | SOME n => Bound n)
    21       | Const("RealDef.real",_)$ @{term "0::int"} => C 0
    22       | Const("RealDef.real",_)$ @{term "1::int"} => C 1
    23       | @{term "0::real"} => C 0
    24       | @{term "1::real"} => C 1
    25       | Term.Bound i => Bound (nat i)
    26       | Const(@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
    27       | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
    28       | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
    29       | Const (@{const_name "HOL.times"},_)$t1$t2 => 
    30         (case (num_of_term vs t1) of C i => 
    31                                      Mul (i,num_of_term vs t2)
    32                                    | _ => error "num_of_term: unsupported Multiplication")
    33       | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.floor"},_)$ t') => Floor (num_of_term vs t')
    34       | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.ceiling"},_)$ t') => Neg(Floor (Neg (num_of_term vs t')))
    35       | Const("RealDef.real",_) $ Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
    36       | Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
    37       | _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t));
    38         
    39 
    40 (* pseudo reification : term -> fm *)
    41 fun fm_of_term vs t = 
    42     case t of 
    43         Const("True",_) => T
    44       | Const("False",_) => F
    45       | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
    46       | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
    47       | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 => 
    48         Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
    49       | Const("op =",eqT)$t1$t2 => 
    50         if (domain_type eqT = @{typ real})
    51         then Eq (Sub (num_of_term vs t1, num_of_term vs t2)) 
    52         else Iff (fm_of_term vs t1, fm_of_term vs t2)
    53       | Const("op &",_)$t1$t2 => And (fm_of_term vs t1, fm_of_term vs t2)
    54       | Const("op |",_)$t1$t2 => Or (fm_of_term vs t1, fm_of_term vs t2)
    55       | Const("op -->",_)$t1$t2 => Imp (fm_of_term vs t1, fm_of_term vs t2)
    56       | Const("Not",_)$t' => Not (fm_of_term vs t')
    57       | Const("Ex",_)$Abs(xn,xT,p) => 
    58         E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
    59       | Const("All",_)$Abs(xn,xT,p) => 
    60         A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p)
    61       | _ => error ("fm_of_term : unknown term!" ^ Display.raw_string_of_term t);
    62 
    63 fun start_vs t =
    64     let val fs = term_frees t
    65     in fs ~~ map nat (0 upto  (length fs - 1))
    66     end ;
    67 
    68 (* transform num and fm back to terms *)
    69 
    70 fun myassoc2 l v =
    71     case l of
    72         [] => NONE
    73       | (x,v')::xs => if v = v' then SOME x
    74                       else myassoc2 xs v;
    75 
    76 val realC = @{term "real :: int => _"};
    77 val rzero = @{term "0::real"};
    78 
    79 fun term_of_num vs t =
    80     case t of 
    81         C i => realC $ (HOLogic.mk_number HOLogic.intT i)
    82       | Bound n => valOf (myassoc2 vs n)
    83       | Neg (Floor (Neg t')) => realC $ (@{term "ceiling"} $ term_of_num vs t')
    84       | Neg t' => @{term "uminus:: real => _"} $ term_of_num vs t'
    85       | Add(t1,t2) => @{term "op +:: real => _"} $ term_of_num vs t1 $ term_of_num vs t2
    86       | Sub(t1,t2) => @{term "op -:: real => _"} $ term_of_num vs t1 $ term_of_num vs t2
    87       | Mul(i,t2) => @{term "op -:: real => _"} $ term_of_num vs (C i) $ term_of_num vs t2
    88       | Floor t => realC $ (@{term "floor"} $ term_of_num vs t)
    89       | Cn(n,i,t) => term_of_num vs (Add(Mul(i,Bound n),t))
    90       | Cf(c,t,s) => term_of_num vs (Add(Mul(c,Floor t),s));
    91 
    92 fun term_of_fm vs t = 
    93     case t of 
    94         T => HOLogic.true_const 
    95       | F => HOLogic.false_const
    96       | Lt t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero
    97       | Le t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero
    98       | Gt t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t
    99       | Ge t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t
   100       | Eq t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero
   101       | NEq t => term_of_fm vs (Not (Eq t))
   102       | NDvd (i,t) => term_of_fm vs (Not (Dvd (i,t)))
   103       | Dvd (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t
   104       | Not t' => HOLogic.Not$(term_of_fm vs t')
   105       | And(t1,t2) => HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
   106       | Or(t1,t2) => HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
   107       | Imp(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
   108       | Iff(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2)
   109       | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
   110 
   111 (* The oracle *)
   112 
   113 fun mircfr_oracle thy t = 
   114     let 
   115         val vs = start_vs t
   116     in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm vs (mircfrqe (fm_of_term vs t))))
   117     end;
   118 
   119 fun mirlfr_oracle thy t = 
   120     let 
   121         val vs = start_vs t
   122     in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm vs (mirlfrqe (fm_of_term vs t))))
   123     end;
   124 
   125 end;