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 "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t') |
|
36 | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t') |
|
37 | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global Pure.thy 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 "Int.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!" ^ Syntax.string_of_term_global Pure.thy 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; |
|