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 = case t of |
|
12 Free(xn,xT) => (case AList.lookup (op =) vs t of |
|
13 NONE => error "Variable not found in the list!!" |
|
14 | SOME n => Var n) |
|
15 | Const(@{const_name HOL.zero},iT) => Cst 0 |
|
16 | Const(@{const_name HOL.one},iT) => Cst 1 |
|
17 | Bound i => Var (nat (IntInf.fromInt i)) |
|
18 | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t') |
|
19 | Const (@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) |
|
20 | Const (@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) |
|
21 | Const (@{const_name HOL.times},_)$t1$t2 => Mult (i_of_term vs t1,i_of_term vs t2) |
|
22 | Const (@{const_name Numeral.number_of},_)$t' => Cst (HOLogic.dest_numeral t') |
|
23 | _ => error "i_of_term: unknown term"; |
|
24 |
|
25 (* pseudo reification : term -> QF *) |
|
26 fun qf_of_term vs t = case t of |
|
27 Const("True",_) => T |
|
28 | Const("False",_) => F |
|
29 | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2) |
|
30 | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2) |
|
31 | Const ("Divides.dvd",_)$t1$t2 => |
|
32 Divides(i_of_term vs t1,i_of_term vs t2) |
|
33 | Const("op =",eqT)$t1$t2 => |
|
34 if (domain_type eqT = HOLogic.intT) |
|
35 then let val i1 = i_of_term vs t1 |
|
36 val i2 = i_of_term vs t2 |
|
37 in Eq (i1,i2) |
|
38 end |
|
39 else Equ(qf_of_term vs t1,qf_of_term vs t2) |
|
40 | Const("op &",_)$t1$t2 => And(qf_of_term vs t1,qf_of_term vs t2) |
|
41 | Const("op |",_)$t1$t2 => Or(qf_of_term vs t1,qf_of_term vs t2) |
|
42 | Const("op -->",_)$t1$t2 => Imp(qf_of_term vs t1,qf_of_term vs t2) |
|
43 | Const("Not",_)$t' => NOT(qf_of_term vs t') |
|
44 | Const("Ex",_)$Abs(xn,xT,p) => |
|
45 QEx(qf_of_term (map (fn(v,n) => (v,n + 1)) vs) p) |
|
46 | Const("All",_)$Abs(xn,xT,p) => |
|
47 QAll(qf_of_term (map (fn(v,n) => (v,n + 1)) vs) p) |
|
48 | _ => error "qf_of_term : unknown term!"; |
|
49 |
|
50 (* |
|
51 fun parse thy s = term_of (Thm.read_cterm thy (s, HOLogic.boolT)); |
|
52 |
|
53 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"; |
|
54 *) |
|
55 fun zip [] [] = [] |
|
56 | zip (x::xs) (y::ys) = (x,y)::(zip xs ys); |
|
57 |
|
58 |
|
59 fun start_vs t = |
|
60 let val fs = term_frees t |
|
61 in zip fs (map (nat o IntInf.fromInt) (0 upto (length fs - 1))) |
|
62 end ; |
|
63 |
|
64 (* transform intterm and QF back to terms *) |
|
65 val iT = HOLogic.intT; |
|
66 val bT = HOLogic.boolT; |
|
67 fun myassoc2 l v = |
|
68 case l of |
|
69 [] => NONE |
|
70 | (x,v')::xs => if v = v' then SOME x |
|
71 else myassoc2 xs v; |
|
72 |
|
73 fun term_of_i vs t = |
|
74 case t of |
|
75 Cst i => CooperDec.mk_number i |
|
76 | Var n => valOf (myassoc2 vs n) |
|
77 | Neg t' => Const(@{const_name HOL.uminus},iT --> iT)$(term_of_i vs t') |
|
78 | Add(t1,t2) => Const(@{const_name HOL.plus},[iT,iT] ---> iT)$ |
|
79 (term_of_i vs t1)$(term_of_i vs t2) |
|
80 | Sub(t1,t2) => Const(@{const_name HOL.minus},[iT,iT] ---> iT)$ |
|
81 (term_of_i vs t1)$(term_of_i vs t2) |
|
82 | Mult(t1,t2) => Const(@{const_name HOL.times},[iT,iT] ---> iT)$ |
|
83 (term_of_i vs t1)$(term_of_i vs t2); |
|
84 |
|
85 fun term_of_qf vs t = |
|
86 case t of |
|
87 T => HOLogic.true_const |
|
88 | F => HOLogic.false_const |
|
89 | Lt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$ |
|
90 (term_of_i vs t1)$(term_of_i vs t2) |
|
91 | Le(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$ |
|
92 (term_of_i vs t1)$(term_of_i vs t2) |
|
93 | Gt(t1,t2) => Const(@{const_name Orderings.less},[iT,iT] ---> bT)$ |
|
94 (term_of_i vs t2)$(term_of_i vs t1) |
|
95 | Ge(t1,t2) => Const(@{const_name Orderings.less_eq},[iT,iT] ---> bT)$ |
|
96 (term_of_i vs t2)$(term_of_i vs t1) |
|
97 | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$ |
|
98 (term_of_i vs t1)$(term_of_i vs t2) |
|
99 | Divides(t1,t2) => Const("Divides.dvd",[iT,iT] ---> bT)$ |
|
100 (term_of_i vs t1)$(term_of_i vs t2) |
|
101 | NOT t' => HOLogic.Not$(term_of_qf vs t') |
|
102 | And(t1,t2) => HOLogic.conj$(term_of_qf vs t1)$(term_of_qf vs t2) |
|
103 | Or(t1,t2) => HOLogic.disj$(term_of_qf vs t1)$(term_of_qf vs t2) |
|
104 | Imp(t1,t2) => HOLogic.imp$(term_of_qf vs t1)$(term_of_qf vs t2) |
|
105 | Equ(t1,t2) => (HOLogic.eq_const bT)$(term_of_qf vs t1)$ |
|
106 (term_of_qf vs t2) |
|
107 | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; |
|
108 |
|
109 (* The oracle *) |
|
110 fun presburger_oracle thy t = |
|
111 let val vs = start_vs t |
|
112 val result = lift_un (term_of_qf vs) (pa (qf_of_term vs t)) |
|
113 in |
|
114 case result of |
|
115 None => raise CooperDec.COOPER |
|
116 | Some t' => HOLogic.mk_Trueprop (HOLogic.mk_eq(t,t')) |
|
117 end ; |
|
118 |
|
119 end; |
|