author | wenzelm |
Tue, 28 Jul 2015 19:49:54 +0200 | |
changeset 60818 | 5e11a6e2b044 |
parent 60801 | 7664e0916eec |
child 61075 | f6b0d827240e |
permissions | -rw-r--r-- |
23489 | 1 |
(* Title: HOL/Tools/Qelim/qelim.ML |
23904 | 2 |
Author: Amine Chaieb, TU Muenchen |
23466 | 3 |
|
23904 | 4 |
Generic quantifier elimination conversions for HOL formulae. |
23466 | 5 |
*) |
6 |
||
7 |
signature QELIM = |
|
8 |
sig |
|
41453 | 9 |
val gen_qelim_conv: conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a -> |
10 |
('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
11 |
val standard_qelim_conv: Proof.context -> |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
12 |
(cterm list -> conv) -> (cterm list -> conv) -> |
41453 | 13 |
(cterm list -> conv) -> conv |
23466 | 14 |
end; |
15 |
||
23489 | 16 |
structure Qelim: QELIM = |
23466 | 17 |
struct |
18 |
||
23489 | 19 |
val all_not_ex = mk_meta_eq @{thm "all_not_ex"}; |
20 |
||
23524 | 21 |
fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv = |
23489 | 22 |
let |
23466 | 23 |
fun conv env p = |
59582 | 24 |
case Thm.term_of p of |
41453 | 25 |
Const(s,T)$_$_ => |
23904 | 26 |
if domain_type T = HOLogic.boolT |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
27 |
andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj}, |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
28 |
@{const_name HOL.implies}, @{const_name HOL.eq}] s |
41453 | 29 |
then Conv.binop_conv (conv env) p |
23904 | 30 |
else atcv env p |
41453 | 31 |
| Const(@{const_name Not},_)$_ => Conv.arg_conv (conv env) p |
32603 | 32 |
| Const(@{const_name Ex},_)$Abs(s,_,_) => |
23489 | 33 |
let |
23466 | 34 |
val (e,p0) = Thm.dest_comb p |
35 |
val (x,p') = Thm.dest_abs (SOME s) p0 |
|
36 |
val env' = ins x env |
|
37 |
val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p') |
|
38 |
|> Drule.arg_cong_rule e |
|
39 |
val th' = simpex_conv (Thm.rhs_of th) |
|
59582 | 40 |
val (_, r) = Thm.dest_equals (Thm.cprop_of th') |
23593 | 41 |
in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th)) |
23466 | 42 |
else Thm.transitive (Thm.transitive th th') (conv env r) end |
32603 | 43 |
| Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p |
44 |
| Const(@{const_name All},_)$_ => |
|
23489 | 45 |
let |
23466 | 46 |
val p = Thm.dest_arg p |
47 |
val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p) |
|
60801 | 48 |
val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex |
36945 | 49 |
in Thm.transitive th (conv env (Thm.rhs_of th)) |
23466 | 50 |
end |
51 |
| _ => atcv env p |
|
52 |
in precv then_conv (conv env) then_conv postcv end |
|
23489 | 53 |
|
23904 | 54 |
(* Instantiation of some parameter for most common cases *) |
23489 | 55 |
|
23904 | 56 |
local |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
57 |
|
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
58 |
val ss = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
59 |
simpset_of |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
60 |
(put_simpset HOL_basic_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
61 |
addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib}); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
62 |
fun pcv ctxt = Simplifier.rewrite (put_simpset ss ctxt) |
23466 | 63 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
64 |
in |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
65 |
|
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
66 |
fun standard_qelim_conv ctxt atcv ncv qcv p = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
67 |
let val pcv = pcv ctxt |
60818 | 68 |
in gen_qelim_conv pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45654
diff
changeset
|
69 |
|
23904 | 70 |
end; |
23466 | 71 |
|
72 |
end; |