author | haftmann |
Thu, 28 Jun 2007 19:09:38 +0200 | |
changeset 23515 | 3e7f62e68fe4 |
parent 23317 | 90be000da2a7 |
child 23808 | 4e4b92e76219 |
permissions | -rw-r--r-- |
23515 | 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. |
|
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
6 |
*) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
7 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
8 |
structure ReflectedFerrack = |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
9 |
struct |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
10 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
11 |
open Ferrack; |
23515 | 12 |
open ReflectedFerrack |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
13 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
14 |
exception LINR; |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
15 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
16 |
(* pseudo reification : term -> intterm *) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
17 |
val iT = HOLogic.intT; |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
18 |
val rT = Type ("RealDef.real",[]); |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
19 |
val bT = HOLogic.boolT; |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
20 |
val realC = Const("RealDef.real",iT --> rT); |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
21 |
val rzero = Const("0",rT); |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
22 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
23 |
fun num_of_term vs t = |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
24 |
case t of |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
25 |
Free(xn,xT) => (case AList.lookup (op =) vs t of |
23515 | 26 |
NONE => error "Variable not found in the list!" |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
27 |
| SOME n => Bound n) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
28 |
| Const("RealDef.real",_)$ @{term "0::int"} => C 0 |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
29 |
| Const("RealDef.real",_)$ @{term "1::int"} => C 1 |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
30 |
| @{term "0::real"} => C 0 |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
31 |
| @{term "0::real"} => C 1 |
23515 | 32 |
| Term.Bound i => Bound (Integer.nat i) |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
33 |
| Const(@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t') |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
34 |
| Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
35 |
| Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
36 |
| Const (@{const_name "HOL.times"},_)$t1$t2 => |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
37 |
(case (num_of_term vs t1) of C i => |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
38 |
Mul (i,num_of_term vs t2) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
39 |
| _ => error "num_of_term: unsupported Multiplication") |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
40 |
| Const("RealDef.real",_) $ Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t') |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
41 |
| Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t') |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
42 |
| _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t)); |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
43 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
44 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
45 |
(* pseudo reification : term -> fm *) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
46 |
fun fm_of_term vs t = |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
47 |
case t of |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
48 |
Const("True",_) => T |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
49 |
| Const("False",_) => F |
23515 | 50 |
| Const(@{const_name "Orderings.less"},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2)) |
51 |
| Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2)) |
|
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
52 |
| Const("op =",eqT)$t1$t2 => |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
53 |
if (domain_type eqT = rT) |
23515 | 54 |
then Eqa (Sub (num_of_term vs t1,num_of_term vs t2)) |
55 |
else Iffa(fm_of_term vs t1,fm_of_term vs t2) |
|
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
56 |
| Const("op &",_)$t1$t2 => And(fm_of_term vs t1,fm_of_term vs t2) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
57 |
| Const("op |",_)$t1$t2 => Or(fm_of_term vs t1,fm_of_term vs t2) |
23515 | 58 |
| Const("op -->",_)$t1$t2 => Impa(fm_of_term vs t1,fm_of_term vs t2) |
59 |
| Const("Not",_)$t' => Nota(fm_of_term vs t') |
|
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
60 |
| Const("Ex",_)$Term.Abs(xn,xT,p) => |
23317
90be000da2a7
Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed
chaieb
parents:
23264
diff
changeset
|
61 |
E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p) |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
62 |
| Const("All",_)$Term.Abs(xn,xT,p) => |
23317
90be000da2a7
Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed
chaieb
parents:
23264
diff
changeset
|
63 |
A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p) |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
64 |
| _ => error ("fm_of_term : unknown term!" ^ (Display.raw_string_of_term t)); |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
65 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
66 |
fun zip [] [] = [] |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
67 |
| zip (x::xs) (y::ys) = (x,y)::(zip xs ys); |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
68 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
69 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
70 |
fun start_vs t = |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
71 |
let val fs = term_frees t |
23515 | 72 |
in zip fs (map Integer.nat (0 upto (length fs - 1))) |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
73 |
end ; |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
74 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
75 |
(* transform num and fm back to terms *) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
76 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
77 |
fun myassoc2 l v = |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
78 |
case l of |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
79 |
[] => NONE |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
80 |
| (x,v')::xs => if v = v' then SOME x |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
81 |
else myassoc2 xs v; |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
82 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
83 |
fun term_of_num vs t = |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
84 |
case t of |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
85 |
C i => realC $ (HOLogic.mk_number HOLogic.intT i) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
86 |
| Bound n => valOf (myassoc2 vs n) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
87 |
| Neg t' => Const(@{const_name "HOL.uminus"},rT --> rT)$(term_of_num vs t') |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
88 |
| Add(t1,t2) => Const(@{const_name "HOL.plus"},[rT,rT] ---> rT)$ |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
89 |
(term_of_num vs t1)$(term_of_num vs t2) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
90 |
| Sub(t1,t2) => Const(@{const_name "HOL.minus"},[rT,rT] ---> rT)$ |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
91 |
(term_of_num vs t1)$(term_of_num vs t2) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
92 |
| Mul(i,t2) => Const(@{const_name "HOL.times"},[rT,rT] ---> rT)$ |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
93 |
(term_of_num vs (C i))$(term_of_num vs t2) |
23515 | 94 |
| Cn(n,i,t) => term_of_num vs (Add (Mul(i,Bound n),t)); |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
95 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
96 |
fun term_of_fm vs t = |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
97 |
case t of |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
98 |
T => HOLogic.true_const |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
99 |
| F => HOLogic.false_const |
23515 | 100 |
| Lta t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$ |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
101 |
(term_of_num vs t)$ rzero |
23515 | 102 |
| Lea t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$ |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
103 |
(term_of_num vs t)$ rzero |
23515 | 104 |
| Gta t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$ |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
105 |
rzero $(term_of_num vs t) |
23515 | 106 |
| Gea t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$ |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
107 |
rzero $(term_of_num vs t) |
23515 | 108 |
| Eqa t => Const("op =",[rT,rT] ---> bT)$ |
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
109 |
(term_of_num vs t)$ rzero |
23515 | 110 |
| NEq t => term_of_fm vs (Nota (Eqa t)) |
111 |
| Nota t' => HOLogic.Not$(term_of_fm vs t') |
|
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
112 |
| And(t1,t2) => HOLogic.conj$(term_of_fm vs t1)$(term_of_fm vs t2) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
113 |
| Or(t1,t2) => HOLogic.disj$(term_of_fm vs t1)$(term_of_fm vs t2) |
23515 | 114 |
| Impa(t1,t2) => HOLogic.imp$(term_of_fm vs t1)$(term_of_fm vs t2) |
115 |
| Iffa(t1,t2) => (HOLogic.eq_const bT)$(term_of_fm vs t1)$ |
|
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
116 |
(term_of_fm vs t2) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
117 |
| _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
118 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
119 |
(* The oracle *) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
120 |
|
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
121 |
fun linrqe_oracle thy t = |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
122 |
let |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
123 |
val vs = start_vs t |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
124 |
in HOLogic.mk_Trueprop (HOLogic.mk_eq(t, term_of_fm vs (linrqe (fm_of_term vs t)))) |
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
125 |
end; |
23515 | 126 |
|
23264
324622260d29
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
chaieb
parents:
diff
changeset
|
127 |
end; |