author | chaieb |
Mon, 11 Jun 2007 11:06:13 +0200 | |
changeset 23317 | 90be000da2a7 |
parent 23274 | f997514ad8f4 |
child 23515 | 3e7f62e68fe4 |
permissions | -rw-r--r-- |
23274 | 1 |
(* $Id$ *) |
2 |
||
3 |
(* Reification for the autimatically generated oracle for Presburger arithmetic |
|
4 |
in HOL/ex/Reflected_Presburger.thy |
|
5 |
Author : Amine Chaieb |
|
6 |
*) |
|
7 |
||
8 |
structure Coopereif = |
|
9 |
struct |
|
10 |
||
11 |
open GeneratedCooper; |
|
12 |
||
13 |
fun i_of_term vs t = |
|
14 |
case t of |
|
15 |
Free(xn,xT) => (case AList.lookup (op aconv) vs t of |
|
16 |
NONE => error "Variable not found in the list!!" |
|
17 |
| SOME n => Bound n) |
|
18 |
| @{term "0::int"} => C 0 |
|
19 |
| @{term "1::int"} => C 1 |
|
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:
23274
diff
changeset
|
20 |
| Term.Bound i => Bound (nat i) |
23274 | 21 |
| Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t') |
22 |
| Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) |
|
23 |
| Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) |
|
24 |
| Const(@{const_name "HOL.times"},_)$t1$t2 => |
|
25 |
(Mul (HOLogic.dest_number t1 |> snd,i_of_term vs t2) |
|
26 |
handle TERM _ => |
|
27 |
(Mul (HOLogic.dest_number t2 |> snd,i_of_term vs t1) |
|
28 |
handle TERM _ => error "i_of_term: Unsupported kind of multiplication")) |
|
29 |
| _ => (C (HOLogic.dest_number t |> snd) |
|
30 |
handle TERM _ => error "i_of_term: unknown term"); |
|
31 |
||
32 |
fun qf_of_term ps vs t = |
|
33 |
case t of |
|
34 |
Const("True",_) => T |
|
35 |
| Const("False",_) => F |
|
36 |
| Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) |
|
37 |
| Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) |
|
38 |
| Const(@{const_name "Divides.dvd"},_)$t1$t2 => |
|
39 |
(Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd") |
|
40 |
| @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) |
|
41 |
| @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
42 |
| Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
43 |
| Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
44 |
| Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
45 |
| Const("Not",_)$t' => NOT(qf_of_term ps vs t') |
|
46 |
| Const("Ex",_)$Abs(xn,xT,p) => |
|
47 |
let val (xn',p') = variant_abs (xn,xT,p) |
|
48 |
val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs) |
|
49 |
in E (qf_of_term ps vs' p') |
|
50 |
end |
|
51 |
| Const("All",_)$Abs(xn,xT,p) => |
|
52 |
let val (xn',p') = variant_abs (xn,xT,p) |
|
53 |
val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs) |
|
54 |
in A (qf_of_term ps vs' p') |
|
55 |
end |
|
56 |
| _ =>(case AList.lookup (op aconv) ps t of |
|
57 |
NONE => error "qf_of_term ps : unknown term!" |
|
58 |
| SOME n => Closed n); |
|
59 |
||
60 |
local |
|
61 |
val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"}, |
|
62 |
@{term "op = :: int => _"}, @{term "op < :: int => _"}, |
|
63 |
@{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"}, |
|
64 |
@{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}] |
|
65 |
fun ty t = Bool.not (fastype_of t = HOLogic.boolT) |
|
66 |
in |
|
67 |
fun term_bools acc t = |
|
68 |
case t of |
|
69 |
(l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b |
|
70 |
else insert (op aconv) t acc |
|
71 |
| f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a |
|
72 |
else insert (op aconv) t acc |
|
73 |
| Abs p => term_bools acc (snd (variant_abs p)) |
|
74 |
| _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc |
|
75 |
end; |
|
76 |
||
77 |
||
78 |
fun start_vs t = |
|
79 |
let |
|
80 |
val fs = term_frees t |
|
81 |
val ps = term_bools [] t |
|
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:
23274
diff
changeset
|
82 |
in (fs ~~ (map nat (0 upto (length fs - 1))), |
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:
23274
diff
changeset
|
83 |
ps ~~ (map nat (0 upto (length ps - 1)))) |
23274 | 84 |
end ; |
85 |
||
86 |
val iT = HOLogic.intT; |
|
87 |
val bT = HOLogic.boolT; |
|
88 |
fun myassoc2 l v = |
|
89 |
case l of |
|
90 |
[] => NONE |
|
91 |
| (x,v')::xs => if v = v' then SOME x |
|
92 |
else myassoc2 xs v; |
|
93 |
||
94 |
fun term_of_i vs t = |
|
95 |
case t of |
|
96 |
C i => HOLogic.mk_number HOLogic.intT i |
|
97 |
| Bound n => valOf (myassoc2 vs n) |
|
98 |
| Neg t' => @{term "uminus :: int => _"}$(term_of_i vs t') |
|
99 |
| Add(t1,t2) => @{term "op +:: int => _"}$ (term_of_i vs t1)$(term_of_i vs t2) |
|
100 |
| Sub(t1,t2) => Const(@{const_name "HOL.minus"},[iT,iT] ---> iT)$ |
|
101 |
(term_of_i vs t1)$(term_of_i vs t2) |
|
102 |
| Mul(i,t2) => Const(@{const_name "HOL.times"},[iT,iT] ---> iT)$ |
|
103 |
(HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t2) |
|
104 |
| CX(i,t')=> term_of_i vs (Add(Mul (i,Bound (nat 0)),t')); |
|
105 |
||
106 |
fun term_of_qf ps vs t = |
|
107 |
case t of |
|
108 |
T => HOLogic.true_const |
|
109 |
| F => HOLogic.false_const |
|
110 |
| Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"} |
|
111 |
| Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"} |
|
112 |
| Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t' |
|
113 |
| Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t' |
|
114 |
| Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"} |
|
115 |
| NEq t' => term_of_qf ps vs (NOT(Eq t')) |
|
116 |
| Dvd(i,t') => @{term "op dvd :: int => _ "}$ |
|
117 |
(HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t') |
|
118 |
| NDvd(i,t')=> term_of_qf ps vs (NOT(Dvd(i,t'))) |
|
119 |
| NOT t' => HOLogic.Not$(term_of_qf ps vs t') |
|
120 |
| And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) |
|
121 |
| Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) |
|
122 |
| Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) |
|
123 |
| Iff(t1,t2) => (HOLogic.eq_const bT)$(term_of_qf ps vs t1)$ (term_of_qf ps vs t2) |
|
124 |
| Closed n => valOf (myassoc2 ps n) |
|
125 |
| NClosed n => term_of_qf ps vs (NOT (Closed n)) |
|
126 |
| _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; |
|
127 |
||
128 |
(* The oracle *) |
|
129 |
fun cooper_oracle thy t = |
|
130 |
let val (vs,ps) = start_vs t |
|
131 |
in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_qf ps vs (pa (qf_of_term ps vs t)))) |
|
132 |
end; |
|
133 |
||
134 |
end; |