author | wenzelm |
Sat, 10 Jun 2017 21:48:02 +0200 | |
changeset 66061 | 880db47fed30 |
parent 61075 | f6b0d827240e |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Decision_Procs/ferrante_rackoff.ML |
23466 | 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 |
||
23567 | 8 |
signature FERRANTE_RACKOFF = |
23466 | 9 |
sig |
23567 | 10 |
val dlo_conv: Proof.context -> conv |
23466 | 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 |
||
23567 | 20 |
type entry = {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list, |
23466 | 21 |
ld: thm list, qe: thm, atoms : cterm list} * |
23567 | 22 |
{isolate_conv: cterm list -> cterm -> thm, |
23466 | 23 |
whatis : cterm -> cterm -> ord, |
24 |
simpset : simpset}; |
|
25 |
||
23567 | 26 |
fun get_p1 th = |
27 |
funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) |
|
59582 | 28 |
(funpow 2 Thm.dest_arg (Thm.cprop_of th)) |> Thm.dest_arg |
23466 | 29 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
30 |
fun ferrack_conv ctxt |
23567 | 31 |
(entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, |
23466 | 32 |
ld = ld, qe = qe, atoms = atoms}, |
23567 | 33 |
{isolate_conv = icv, whatis = wi, simpset = simpset}):entry) = |
34 |
let |
|
59582 | 35 |
fun uset (vars as (x::vs)) p = case Thm.term_of p of |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
36 |
Const(@{const_name HOL.conj}, _)$ _ $ _ => |
23567 | 37 |
let |
38 |
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb |
|
23466 | 39 |
val (lS,lth) = uset vars l val (rS, rth) = uset vars r |
23567 | 40 |
in (lS@rS, Drule.binop_cong_rule b lth rth) end |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
41 |
| Const(@{const_name HOL.disj}, _)$ _ $ _ => |
23567 | 42 |
let |
43 |
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb |
|
23466 | 44 |
val (lS,lth) = uset vars l val (rS, rth) = uset vars r |
23567 | 45 |
in (lS@rS, Drule.binop_cong_rule b lth rth) end |
46 |
| _ => |
|
47 |
let |
|
48 |
val th = icv vars p |
|
23466 | 49 |
val p' = Thm.rhs_of th |
50 |
val c = wi x p' |
|
23567 | 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 |
|
23466 | 54 |
else K []) p' |
55 |
in (S,th) end |
|
56 |
||
23567 | 57 |
val ((p1_v,p2_v),(mp1_v,mp2_v)) = |
58 |
funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) |
|
59582 | 59 |
(funpow 4 Thm.dest_arg (Thm.cprop_of (hd minf))) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
56245
diff
changeset
|
60 |
|> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun) |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59970
diff
changeset
|
61 |
|> apply2 (apply2 (dest_Var o Thm.term_of)) |
23567 | 62 |
|
63 |
fun myfwd (th1, th2, th3, th4, th5) p1 p2 |
|
64 |
[(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] = |
|
23466 | 65 |
let |
66 |
val (mp1, mp2) = (get_p1 th_1, get_p1 th_1') |
|
67 |
val (pp1, pp2) = (get_p1 th_2, get_p1 th_2') |
|
23567 | 68 |
fun fw mi th th' th'' = |
69 |
let |
|
70 |
val th0 = if mi then |
|
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
40314
diff
changeset
|
71 |
Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th |
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
40314
diff
changeset
|
72 |
else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th |
36945 | 73 |
in Thm.implies_elim (Thm.implies_elim th0 th') th'' end |
23567 | 74 |
in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', |
75 |
fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') |
|
23466 | 76 |
end |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59970
diff
changeset
|
77 |
val U_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe))))) |
23567 | 78 |
fun main vs p = |
79 |
let |
|
59582 | 80 |
val ((xn,ce),(x,fm)) = (case Thm.term_of p of |
38558 | 81 |
Const(@{const_name Ex},_)$Abs(xn,xT,_) => |
23466 | 82 |
Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn |
23567 | 83 |
| _ => raise CTERM ("main QE only treats existential quantifiers!", [p])) |
59586 | 84 |
val cT = Thm.ctyp_of_cterm x |
23466 | 85 |
val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc) |
86 |
val nthx = Thm.abstract_rule xn x nth |
|
87 |
val q = Thm.rhs_of nth |
|
88 |
val qx = Thm.rhs_of nthx |
|
89 |
val enth = Drule.arg_cong_rule ce nthx |
|
60801 | 90 |
val [th0,th1] = map (Thm.instantiate' [SOME cT] []) @{thms "finite.intros"} |
23567 | 91 |
fun ins x th = |
60801 | 92 |
Thm.implies_elim (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) |
23466 | 93 |
(Thm.cprop_of th), SOME x] th1) th |
94 |
val fU = fold ins u th0 |
|
95 |
val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU) |
|
23567 | 96 |
local |
60801 | 97 |
val insI1 = Thm.instantiate' [SOME cT] [] @{thm "insertI1"} |
98 |
val insI2 = Thm.instantiate' [SOME cT] [] @{thm "insertI2"} |
|
23466 | 99 |
in |
23567 | 100 |
fun provein x S = |
59582 | 101 |
case Thm.term_of S of |
32264
0be31453f698
Set.UNIV and Set.empty are mere abbreviations for top and bot
haftmann
parents:
32149
diff
changeset
|
102 |
Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S]) |
30304
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
24584
diff
changeset
|
103 |
| Const(@{const_name insert}, _) $ y $_ => |
23466 | 104 |
let val (cy,S') = Thm.dest_binop S |
60801 | 105 |
in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1 |
106 |
else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2) |
|
23466 | 107 |
(provein x S') |
108 |
end |
|
109 |
end |
|
59582 | 110 |
val tabU = fold (fn t => fn tab => Termtab.update (Thm.term_of t, provein t cU) tab) |
23466 | 111 |
u Termtab.empty |
59582 | 112 |
val U = the o Termtab.lookup tabU o Thm.term_of |
23567 | 113 |
val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt, |
23466 | 114 |
minf_le, minf_gt, minf_ge, minf_P] = minf |
23567 | 115 |
val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt, |
23466 | 116 |
pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf |
23567 | 117 |
val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt, |
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
40314
diff
changeset
|
118 |
nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi |
23567 | 119 |
val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt, |
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
40314
diff
changeset
|
120 |
npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi |
23567 | 121 |
val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, |
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
40314
diff
changeset
|
122 |
ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld |
23567 | 123 |
|
124 |
fun decomp_mpinf fm = |
|
59582 | 125 |
case Thm.term_of fm of |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
126 |
Const(@{const_name HOL.conj},_)$_$_ => |
23567 | 127 |
let val (p,q) = Thm.dest_binop fm |
128 |
in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj) |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45654
diff
changeset
|
129 |
(Thm.lambda x p) (Thm.lambda x q)) |
23466 | 130 |
end |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
131 |
| Const(@{const_name HOL.disj},_)$_$_ => |
23567 | 132 |
let val (p,q) = Thm.dest_binop fm |
23466 | 133 |
in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj) |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45654
diff
changeset
|
134 |
(Thm.lambda x p) (Thm.lambda x q)) |
23466 | 135 |
end |
23567 | 136 |
| _ => |
23466 | 137 |
(let val c = wi x fm |
23567 | 138 |
val t = (if c=Nox then I |
139 |
else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg |
|
140 |
else if member (op =) [Gt, Ge] c then Thm.dest_arg1 |
|
141 |
else if c = NEq then (Thm.dest_arg o Thm.dest_arg) |
|
40314
b5ec88d9ac03
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38864
diff
changeset
|
142 |
else raise Fail "decomp_mpinf: Impossible case!!") fm |
23567 | 143 |
val [mi_th, pi_th, nmi_th, npi_th, ld_th] = |
60801 | 144 |
if c = Nox then map (Thm.instantiate' [] [SOME fm]) |
23466 | 145 |
[minf_P, pinf_P, nmi_P, npi_P, ld_P] |
23567 | 146 |
else |
147 |
let val [mi_th,pi_th,nmi_th,npi_th,ld_th] = |
|
60801 | 148 |
map (Thm.instantiate' [] [SOME t]) |
23466 | 149 |
(case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt] |
150 |
| Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le] |
|
151 |
| Gt => [minf_gt, pinf_gt, nmi_gt, npi_gt, ld_gt] |
|
152 |
| Ge => [minf_ge, pinf_ge, nmi_ge, npi_ge, ld_ge] |
|
153 |
| Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq] |
|
154 |
| NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq]) |
|
155 |
val tU = U t |
|
36945 | 156 |
fun Ufw th = Thm.implies_elim th tU |
23466 | 157 |
in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th] |
158 |
end |
|
159 |
in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end) |
|
160 |
val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q |
|
23567 | 161 |
val qe_th = Drule.implies_elim_list |
162 |
((fconv_rule (Thm.beta_conversion true)) |
|
60801 | 163 |
(Thm.instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th]) |
23466 | 164 |
qe)) |
23567 | 165 |
[fU, ld_th, nmi_th, npi_th, minf_th, pinf_th] |
166 |
val bex_conv = |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
167 |
Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms bex_simps(1-5)}) |
36945 | 168 |
val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th) |
23466 | 169 |
in result_th |
170 |
end |
|
171 |
||
172 |
in main |
|
173 |
end; |
|
174 |
||
23567 | 175 |
val grab_atom_bop = |
176 |
let |
|
23466 | 177 |
fun h bounds tm = |
59582 | 178 |
(case Thm.term_of tm of |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
179 |
Const (@{const_name HOL.eq}, T) $ _ $ _ => |
23567 | 180 |
if domain_type T = HOLogic.boolT then find_args bounds tm |
23466 | 181 |
else Thm.dest_fun2 tm |
38558 | 182 |
| Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm) |
183 |
| Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm) |
|
184 |
| Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm) |
|
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
185 |
| Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm |
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
186 |
| Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38558
diff
changeset
|
187 |
| Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm |
56245 | 188 |
| Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm |
189 |
| Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm |
|
190 |
| Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm) |
|
38558 | 191 |
| Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm) |
23466 | 192 |
| _ => Thm.dest_fun2 tm) |
23567 | 193 |
and find_args bounds tm = |
23466 | 194 |
(h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm) |
195 |
and find_body bounds b = |
|
196 |
let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b |
|
197 |
in h (bounds + 1) b' end; |
|
198 |
in h end; |
|
199 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
200 |
fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset = ss}) tm = |
23567 | 201 |
let |
202 |
val ss' = |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
203 |
merge_ss (simpset_of |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
204 |
(put_simpset HOL_basic_ss ctxt addsimps |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
205 |
@{thms simp_thms ex_simps all_simps not_all all_not_ex ex_disj_distrib}), ss); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
206 |
val pcv = Simplifier.rewrite (put_simpset ss' ctxt); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
207 |
val postcv = Simplifier.rewrite (put_simpset ss ctxt); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
208 |
val nnf = K (nnf_conv ctxt then_conv postcv) |
61075 | 209 |
val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_add_frees tm []) |
23466 | 210 |
(isolate_conv ctxt) nnf |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
211 |
(fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
212 |
whatis = whatis, simpset = ss}) vs |
23466 | 213 |
then_conv postcv) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
214 |
in (Simplifier.rewrite (put_simpset ss ctxt) then_conv qe_conv) tm end; |
23466 | 215 |
|
23567 | 216 |
fun dlo_instance ctxt tm = |
217 |
Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm); |
|
23486 | 218 |
|
23567 | 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); |
|
23466 | 223 |
|
23567 | 224 |
fun dlo_tac ctxt = CSUBGOAL (fn (p, i) => |
225 |
(case dlo_instance ctxt p of |
|
226 |
NONE => no_tac |
|
227 |
| SOME instance => |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
228 |
Object_Logic.full_atomize_tac ctxt i THEN |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
229 |
simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN (* FIXME already part of raw_ferrack_qe_conv? *) |
59970 | 230 |
CONVERSION (Object_Logic.judgment_conv ctxt (raw_ferrack_qe_conv ctxt instance)) i THEN |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46497
diff
changeset
|
231 |
simp_tac ctxt i)); (* FIXME really? *) |
23466 | 232 |
|
233 |
end; |