|
1 (* $Id$ *) |
|
2 (* The oracle for Presburger arithmetic based on the verified Code *) |
|
3 (* in HOL/ex/Reflected_Presburger.thy *) |
|
4 |
|
5 structure ReflectedCooper = |
|
6 struct |
|
7 |
|
8 open Generated; |
|
9 (* pseudo reification : term -> intterm *) |
|
10 |
|
11 fun i_of_term vs t = |
|
12 case t of |
|
13 Free(xn,xT) => (case assoc(vs,t) of |
|
14 NONE => error "Variable not found in the list!!" |
|
15 | SOME n => Var n) |
|
16 | Const("0",iT) => Cst 0 |
|
17 | Const("1",iT) => Cst 1 |
|
18 | Bound i => Var (nat i) |
|
19 | Const("uminus",_)$t' => Neg (i_of_term vs t') |
|
20 | Const ("op +",_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) |
|
21 | Const ("op -",_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) |
|
22 | Const ("op *",_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2) |
|
23 | Const ("Numeral.number_of",_)$t' => Cst (HOLogic.dest_binum t') |
|
24 | _ => error "i_of_term: unknown term"; |
|
25 |
|
26 |
|
27 (* pseudo reification : term -> QF *) |
|
28 fun qf_of_term vs t = |
|
29 case t of |
|
30 Const("True",_) => T |
|
31 | Const("False",_) => F |
|
32 | Const("op <",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2) |
|
33 | Const("op <=",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2) |
|
34 | Const ("Divides.op dvd",_)$t1$t2 => |
|
35 Divides(i_of_term vs t1,i_of_term vs t2) |
|
36 | Const("op =",eqT)$t1$t2 => |
|
37 if (domain_type eqT = HOLogic.intT) |
|
38 then let val i1 = i_of_term vs t1 |
|
39 val i2 = i_of_term vs t2 |
|
40 in Eq (i1,i2) |
|
41 end |
|
42 else Equ(qf_of_term vs t1,qf_of_term vs t2) |
|
43 | Const("op &",_)$t1$t2 => And(qf_of_term vs t1,qf_of_term vs t2) |
|
44 | Const("op |",_)$t1$t2 => Or(qf_of_term vs t1,qf_of_term vs t2) |
|
45 | Const("op -->",_)$t1$t2 => Imp(qf_of_term vs t1,qf_of_term vs t2) |
|
46 | Const("Not",_)$t' => NOT(qf_of_term vs t') |
|
47 | Const("Ex",_)$Abs(xn,xT,p) => |
|
48 QEx(qf_of_term (map (fn(v,n) => (v,n + 1)) vs) p) |
|
49 | Const("All",_)$Abs(xn,xT,p) => |
|
50 QAll(qf_of_term (map (fn(v,n) => (v,n + 1)) vs) p) |
|
51 | _ => error "qf_of_term : unknown term!"; |
|
52 |
|
53 (* |
|
54 fun parse s = term_of (read_cterm (sign_of Main.thy) (s,HOLogic.boolT)); |
|
55 |
|
56 val t = parse "ALL (i::int) (j::int). i < 8* j --> (i - 1 = j + 3 + 2*j) & (j <= -i + k ) | 4 = i | 5 dvd i"; |
|
57 *) |
|
58 fun zip [] [] = [] |
|
59 | zip (x::xs) (y::ys) = (x,y)::(zip xs ys); |
|
60 |
|
61 |
|
62 fun start_vs t = |
|
63 let val fs = term_frees t |
|
64 in zip fs (map nat (0 upto (length fs - 1))) |
|
65 end ; |
|
66 |
|
67 (* transform intterm and QF back to terms *) |
|
68 val iT = HOLogic.intT; |
|
69 val bT = HOLogic.boolT; |
|
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 fun term_of_i vs t = |
|
77 case t of |
|
78 Cst i => CooperDec.mk_numeral i |
|
79 | Var n => valOf (myassoc2 vs n) |
|
80 | Neg t' => Const("uminus",iT --> iT)$(term_of_i vs t') |
|
81 | Add(t1,t2) => Const("op +",[iT,iT] ---> iT)$ |
|
82 (term_of_i vs t1)$(term_of_i vs t2) |
|
83 | Sub(t1,t2) => Const("op -",[iT,iT] ---> iT)$ |
|
84 (term_of_i vs t1)$(term_of_i vs t2) |
|
85 | Mult(t1,t2) => Const("op *",[iT,iT] ---> iT)$ |
|
86 (term_of_i vs t1)$(term_of_i vs t2); |
|
87 |
|
88 fun term_of_qf vs t = |
|
89 case t of |
|
90 T => HOLogic.true_const |
|
91 | F => HOLogic.false_const |
|
92 | Lt(t1,t2) => Const("op <",[iT,iT] ---> bT)$ |
|
93 (term_of_i vs t1)$(term_of_i vs t2) |
|
94 | Le(t1,t2) => Const("op <=",[iT,iT] ---> bT)$ |
|
95 (term_of_i vs t1)$(term_of_i vs t2) |
|
96 | Gt(t1,t2) => Const("op <",[iT,iT] ---> bT)$ |
|
97 (term_of_i vs t2)$(term_of_i vs t1) |
|
98 | Ge(t1,t2) => Const("op <=",[iT,iT] ---> bT)$ |
|
99 (term_of_i vs t2)$(term_of_i vs t1) |
|
100 | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$ |
|
101 (term_of_i vs t1)$(term_of_i vs t2) |
|
102 | Divides(t1,t2) => Const("Divides.op dvd",[iT,iT] ---> bT)$ |
|
103 (term_of_i vs t1)$(term_of_i vs t2) |
|
104 | NOT t' => HOLogic.Not$(term_of_qf vs t') |
|
105 | And(t1,t2) => HOLogic.conj$(term_of_qf vs t1)$(term_of_qf vs t2) |
|
106 | Or(t1,t2) => HOLogic.disj$(term_of_qf vs t1)$(term_of_qf vs t2) |
|
107 | Imp(t1,t2) => HOLogic.imp$(term_of_qf vs t1)$(term_of_qf vs t2) |
|
108 | Equ(t1,t2) => (HOLogic.eq_const bT)$(term_of_qf vs t1)$ |
|
109 (term_of_qf vs t2) |
|
110 | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; |
|
111 |
|
112 (* The oracle *) |
|
113 exception COOPER; |
|
114 |
|
115 fun presburger_oracle thy t = |
|
116 let val vs = start_vs t |
|
117 val result = lift_un (term_of_qf vs) (pa (qf_of_term vs t)) |
|
118 in |
|
119 case result of |
|
120 None => raise COOPER |
|
121 | Some t' => HOLogic.mk_Trueprop (HOLogic.mk_eq(t,t')) |
|
122 end ; |
|
123 |
|
124 end; |