1 (* Title: HOL/Tools/Qelim/ferrante_rackoff.ML |
|
2 Author: Amine Chaieb, TU Muenchen |
|
3 |
|
4 Ferrante and Rackoff's algorithm for quantifier elimination in dense |
|
5 linear orders. Proof-synthesis and tactic. |
|
6 *) |
|
7 |
|
8 signature FERRANTE_RACKOFF = |
|
9 sig |
|
10 val dlo_conv: Proof.context -> conv |
|
11 val dlo_tac: Proof.context -> int -> tactic |
|
12 end; |
|
13 |
|
14 structure FerranteRackoff: FERRANTE_RACKOFF = |
|
15 struct |
|
16 |
|
17 open Ferrante_Rackoff_Data; |
|
18 open Conv; |
|
19 |
|
20 type entry = {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list, |
|
21 ld: thm list, qe: thm, atoms : cterm list} * |
|
22 {isolate_conv: cterm list -> cterm -> thm, |
|
23 whatis : cterm -> cterm -> ord, |
|
24 simpset : simpset}; |
|
25 |
|
26 fun get_p1 th = |
|
27 funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) |
|
28 (funpow 2 Thm.dest_arg (cprop_of th)) |> Thm.dest_arg |
|
29 |
|
30 fun ferrack_conv |
|
31 (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, |
|
32 ld = ld, qe = qe, atoms = atoms}, |
|
33 {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) = |
|
34 let |
|
35 fun uset (vars as (x::vs)) p = case term_of p of |
|
36 Const("op &", _)$ _ $ _ => |
|
37 let |
|
38 val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb |
|
39 val (lS,lth) = uset vars l val (rS, rth) = uset vars r |
|
40 in (lS@rS, Drule.binop_cong_rule b lth rth) end |
|
41 | Const("op |", _)$ _ $ _ => |
|
42 let |
|
43 val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb |
|
44 val (lS,lth) = uset vars l val (rS, rth) = uset vars r |
|
45 in (lS@rS, Drule.binop_cong_rule b lth rth) end |
|
46 | _ => |
|
47 let |
|
48 val th = icv vars p |
|
49 val p' = Thm.rhs_of th |
|
50 val c = wi x p' |
|
51 val S = (if member (op =) [Lt, Le, Eq] c then single o Thm.dest_arg |
|
52 else if member (op =) [Gt, Ge] c then single o Thm.dest_arg1 |
|
53 else if c = NEq then single o Thm.dest_arg o Thm.dest_arg |
|
54 else K []) p' |
|
55 in (S,th) end |
|
56 |
|
57 val ((p1_v,p2_v),(mp1_v,mp2_v)) = |
|
58 funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) |
|
59 (funpow 4 Thm.dest_arg (cprop_of (hd minf))) |
|
60 |> Thm.dest_binop |> pairself Thm.dest_binop |> apfst (pairself Thm.dest_fun) |
|
61 |
|
62 fun myfwd (th1, th2, th3, th4, th5) p1 p2 |
|
63 [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] = |
|
64 let |
|
65 val (mp1, mp2) = (get_p1 th_1, get_p1 th_1') |
|
66 val (pp1, pp2) = (get_p1 th_2, get_p1 th_2') |
|
67 fun fw mi th th' th'' = |
|
68 let |
|
69 val th0 = if mi then |
|
70 instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th |
|
71 else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th |
|
72 in Thm.implies_elim (Thm.implies_elim th0 th') th'' end |
|
73 in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', |
|
74 fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') |
|
75 end |
|
76 val U_v = (Thm.dest_arg o Thm.dest_arg o Thm.dest_arg1) (cprop_of qe) |
|
77 fun main vs p = |
|
78 let |
|
79 val ((xn,ce),(x,fm)) = (case term_of p of |
|
80 Const("Ex",_)$Abs(xn,xT,_) => |
|
81 Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn |
|
82 | _ => raise CTERM ("main QE only treats existential quantifiers!", [p])) |
|
83 val cT = ctyp_of_term x |
|
84 val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc) |
|
85 val nthx = Thm.abstract_rule xn x nth |
|
86 val q = Thm.rhs_of nth |
|
87 val qx = Thm.rhs_of nthx |
|
88 val enth = Drule.arg_cong_rule ce nthx |
|
89 val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"} |
|
90 fun ins x th = |
|
91 Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) |
|
92 (Thm.cprop_of th), SOME x] th1) th |
|
93 val fU = fold ins u th0 |
|
94 val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU) |
|
95 local |
|
96 val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"} |
|
97 val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"} |
|
98 in |
|
99 fun provein x S = |
|
100 case term_of S of |
|
101 Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S]) |
|
102 | Const(@{const_name insert}, _) $ y $_ => |
|
103 let val (cy,S') = Thm.dest_binop S |
|
104 in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1 |
|
105 else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) |
|
106 (provein x S') |
|
107 end |
|
108 end |
|
109 val tabU = fold (fn t => fn tab => Termtab.update (term_of t, provein t cU) tab) |
|
110 u Termtab.empty |
|
111 val U = the o Termtab.lookup tabU o term_of |
|
112 val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt, |
|
113 minf_le, minf_gt, minf_ge, minf_P] = minf |
|
114 val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt, |
|
115 pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf |
|
116 val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt, |
|
117 nmi_le, nmi_gt, nmi_ge, nmi_P] = map (instantiate ([],[(U_v,cU)])) nmi |
|
118 val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt, |
|
119 npi_le, npi_gt, npi_ge, npi_P] = map (instantiate ([],[(U_v,cU)])) npi |
|
120 val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, |
|
121 ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld |
|
122 |
|
123 fun decomp_mpinf fm = |
|
124 case term_of fm of |
|
125 Const("op &",_)$_$_ => |
|
126 let val (p,q) = Thm.dest_binop fm |
|
127 in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj) |
|
128 (Thm.cabs x p) (Thm.cabs x q)) |
|
129 end |
|
130 | Const("op |",_)$_$_ => |
|
131 let val (p,q) = Thm.dest_binop fm |
|
132 in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj) |
|
133 (Thm.cabs x p) (Thm.cabs x q)) |
|
134 end |
|
135 | _ => |
|
136 (let val c = wi x fm |
|
137 val t = (if c=Nox then I |
|
138 else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg |
|
139 else if member (op =) [Gt, Ge] c then Thm.dest_arg1 |
|
140 else if c = NEq then (Thm.dest_arg o Thm.dest_arg) |
|
141 else sys_error "decomp_mpinf: Impossible case!!") fm |
|
142 val [mi_th, pi_th, nmi_th, npi_th, ld_th] = |
|
143 if c = Nox then map (instantiate' [] [SOME fm]) |
|
144 [minf_P, pinf_P, nmi_P, npi_P, ld_P] |
|
145 else |
|
146 let val [mi_th,pi_th,nmi_th,npi_th,ld_th] = |
|
147 map (instantiate' [] [SOME t]) |
|
148 (case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt] |
|
149 | Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le] |
|
150 | Gt => [minf_gt, pinf_gt, nmi_gt, npi_gt, ld_gt] |
|
151 | Ge => [minf_ge, pinf_ge, nmi_ge, npi_ge, ld_ge] |
|
152 | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq] |
|
153 | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq]) |
|
154 val tU = U t |
|
155 fun Ufw th = Thm.implies_elim th tU |
|
156 in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th] |
|
157 end |
|
158 in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end) |
|
159 val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q |
|
160 val qe_th = Drule.implies_elim_list |
|
161 ((fconv_rule (Thm.beta_conversion true)) |
|
162 (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th]) |
|
163 qe)) |
|
164 [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th] |
|
165 val bex_conv = |
|
166 Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)})) |
|
167 val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th) |
|
168 in result_th |
|
169 end |
|
170 |
|
171 in main |
|
172 end; |
|
173 |
|
174 val grab_atom_bop = |
|
175 let |
|
176 fun h bounds tm = |
|
177 (case term_of tm of |
|
178 Const ("op =", T) $ _ $ _ => |
|
179 if domain_type T = HOLogic.boolT then find_args bounds tm |
|
180 else Thm.dest_fun2 tm |
|
181 | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm) |
|
182 | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm) |
|
183 | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm) |
|
184 | Const ("op &", _) $ _ $ _ => find_args bounds tm |
|
185 | Const ("op |", _) $ _ $ _ => find_args bounds tm |
|
186 | Const ("op -->", _) $ _ $ _ => find_args bounds tm |
|
187 | Const ("==>", _) $ _ $ _ => find_args bounds tm |
|
188 | Const ("==", _) $ _ $ _ => find_args bounds tm |
|
189 | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm) |
|
190 | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm) |
|
191 | _ => Thm.dest_fun2 tm) |
|
192 and find_args bounds tm = |
|
193 (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm) |
|
194 and find_body bounds b = |
|
195 let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b |
|
196 in h (bounds + 1) b' end; |
|
197 in h end; |
|
198 |
|
199 fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset}) tm = |
|
200 let |
|
201 val ss = simpset |
|
202 val ss' = |
|
203 merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps) |
|
204 @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss) |
|
205 |> Simplifier.inherit_context ss |
|
206 val pcv = Simplifier.rewrite ss' |
|
207 val postcv = Simplifier.rewrite ss |
|
208 val nnf = K (nnf_conv then_conv postcv) |
|
209 val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm []) |
|
210 (isolate_conv ctxt) nnf |
|
211 (fn vs => ferrack_conv (thy,{isolate_conv = isolate_conv ctxt, |
|
212 whatis = whatis, simpset = simpset}) vs |
|
213 then_conv postcv) |
|
214 in (Simplifier.rewrite ss then_conv qe_conv) tm end; |
|
215 |
|
216 fun dlo_instance ctxt tm = |
|
217 Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm); |
|
218 |
|
219 fun dlo_conv ctxt tm = |
|
220 (case dlo_instance ctxt tm of |
|
221 NONE => raise CTERM ("ferrackqe_conv: no corresponding instance in context!", [tm]) |
|
222 | SOME instance => raw_ferrack_qe_conv ctxt instance tm); |
|
223 |
|
224 fun dlo_tac ctxt = CSUBGOAL (fn (p, i) => |
|
225 (case dlo_instance ctxt p of |
|
226 NONE => no_tac |
|
227 | SOME instance => |
|
228 Object_Logic.full_atomize_tac i THEN |
|
229 simp_tac (#simpset (snd instance)) i THEN (* FIXME already part of raw_ferrack_qe_conv? *) |
|
230 CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN |
|
231 simp_tac (simpset_of ctxt) i)); (* FIXME really? *) |
|
232 |
|
233 end; |
|