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