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