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