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