6 and proof generation for multiple quantified formulae. |
6 and proof generation for multiple quantified formulae. |
7 *) |
7 *) |
8 |
8 |
9 signature QELIM = |
9 signature QELIM = |
10 sig |
10 sig |
11 val tproof_of_mlift_qelim: theory -> (term -> bool) -> |
|
12 (string list -> term -> thm) -> (term -> thm) -> |
|
13 (term -> thm) -> term -> thm |
|
14 val standard_qelim_conv: (cterm list -> cterm -> thm) -> |
11 val standard_qelim_conv: (cterm list -> cterm -> thm) -> |
15 (cterm list -> Conv.conv) -> (cterm list -> cterm -> thm) -> cterm -> thm |
12 (cterm list -> Conv.conv) -> (cterm list -> cterm -> thm) -> cterm -> thm |
16 val gen_qelim_conv: Conv.conv -> Conv.conv -> Conv.conv -> |
13 val gen_qelim_conv: Conv.conv -> Conv.conv -> Conv.conv -> |
17 (cterm -> 'a -> 'a) -> 'a -> ('a -> cterm -> thm) -> |
14 (cterm -> 'a -> 'a) -> 'a -> ('a -> cterm -> thm) -> |
18 ('a -> Conv.conv) -> ('a -> cterm -> thm) -> Conv.conv |
15 ('a -> Conv.conv) -> ('a -> cterm -> thm) -> Conv.conv |
19 |
16 |
20 end; |
17 end; |
21 |
18 |
22 structure Qelim : QELIM = |
19 structure Qelim : QELIM = |
23 struct |
20 struct |
24 open CooperDec; |
|
25 open CooperProof; |
|
26 open Conv; |
21 open Conv; |
27 |
|
28 val cboolT = ctyp_of HOL.thy HOLogic.boolT; |
|
29 |
|
30 (* List of the theorems to be used in the following*) |
|
31 |
|
32 val qe_ex_conj = thm "qe_ex_conj"; |
|
33 val qe_ex_nconj = thm "qe_ex_nconj"; |
|
34 val qe_ALL = thm "qe_ALL"; |
|
35 |
|
36 |
|
37 (*============= Compact version =====*) |
|
38 |
|
39 |
|
40 fun decomp_qe is_at afnp nfnp qfnp sg P = |
|
41 if is_at P then ([], fn [] => afnp [] P) else |
|
42 case P of |
|
43 (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI) |
|
44 |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI) |
|
45 |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI) |
|
46 |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI) |
|
47 |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not) |
|
48 |(Const("Ex",_)$Abs(xn,xT,p)) => |
|
49 let val (xn1,p1) = Syntax.variant_abs(xn,xT,p) |
|
50 in ([p1], |
|
51 fn [th1_1] => |
|
52 let val th2 = [th1_1,nfnp (snd (qe_get_terms th1_1))] MRS trans |
|
53 val eth1 = (forall_intr (cterm_of sg (Free(xn1,xT))) th2) COMP qe_exI |
|
54 val th3 = qfnp (snd(qe_get_terms eth1)) |
|
55 in [eth1,th3] MRS trans |
|
56 end ) |
|
57 end |
|
58 |
|
59 |(Const("All",_)$Abs(xn,xT,p)) => ([(HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p)], fn [th] => th RS qe_ALL) |
|
60 | _ => ([],fn [] => instantiate' [SOME (ctyp_of sg (type_of P))] [SOME (cterm_of sg P)] refl); |
|
61 |
|
62 |
|
63 fun tproof_of_mlift_qelim sg isat afnp nfnp qfnp p = |
|
64 let val th1 = thm_of sg (decomp_qe isat afnp nfnp qfnp sg) p |
|
65 val th2 = nfnp (snd (qe_get_terms th1)) |
|
66 in [th1,th2] MRS trans |
|
67 end; |
|
68 |
22 |
69 val is_refl = op aconv o Logic.dest_equals o Thm.prop_of; |
23 val is_refl = op aconv o Logic.dest_equals o Thm.prop_of; |
70 |
24 |
71 fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv = |
25 fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv = |
72 let fun conv p = |
26 let fun conv p = |