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