1 (* |
|
2 ID: $Id$ |
|
3 Author: Amine Chaieb and Tobias Nipkow, TU Muenchen |
|
4 |
|
5 File containing the implementation of the proof protocoling |
|
6 and proof generation for multiple quantified formulae. |
|
7 *) |
|
8 |
|
9 signature QELIM = |
|
10 sig |
|
11 val standard_qelim_conv: Proof.context -> (cterm list -> cterm -> thm) -> |
|
12 (cterm list -> Conv.conv) -> (cterm list -> cterm -> thm) -> cterm -> thm |
|
13 val gen_qelim_conv: Proof.context -> Conv.conv -> Conv.conv -> Conv.conv -> |
|
14 (cterm -> 'a -> 'a) -> 'a -> ('a -> cterm -> thm) -> |
|
15 ('a -> Conv.conv) -> ('a -> cterm -> thm) -> Conv.conv |
|
16 end; |
|
17 |
|
18 structure Qelim : QELIM = |
|
19 struct |
|
20 |
|
21 open Conv; |
|
22 |
|
23 local |
|
24 val all_not_ex = mk_meta_eq @{thm "all_not_ex"} |
|
25 in |
|
26 fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv = |
|
27 let |
|
28 val thy = ProofContext.theory_of ctxt |
|
29 fun conv env p = |
|
30 case (term_of p) of |
|
31 Const(s,T)$_$_ => if domain_type T = HOLogic.boolT |
|
32 andalso s mem ["op &","op |","op -->","op ="] |
|
33 then binop_conv (conv env) p else atcv env p |
|
34 | Const("Not",_)$_ => arg_conv (conv env) p |
|
35 | Const("Ex",_)$Abs(s,_,_) => |
|
36 let |
|
37 val (e,p0) = Thm.dest_comb p |
|
38 val (x,p') = Thm.dest_abs (SOME s) p0 |
|
39 val env' = ins x env |
|
40 val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p') |
|
41 |> Drule.arg_cong_rule e |
|
42 val th' = simpex_conv (Thm.rhs_of th) |
|
43 val (l,r) = Thm.dest_equals (cprop_of th') |
|
44 in if is_refl th' then Thm.transitive th (qcv env (Thm.rhs_of th)) |
|
45 else Thm.transitive (Thm.transitive th th') (conv env r) end |
|
46 | Const("Ex",_)$ _ => (eta_conv thy then_conv conv env) p |
|
47 | Const("All",_)$_ => |
|
48 let |
|
49 val p = Thm.dest_arg p |
|
50 val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p) |
|
51 val th = instantiate' [SOME T] [SOME p] all_not_ex |
|
52 in transitive th (conv env (Thm.rhs_of th)) |
|
53 end |
|
54 | _ => atcv env p |
|
55 in precv then_conv (conv env) then_conv postcv end |
|
56 end; |
|
57 |
|
58 fun cterm_frees ct = |
|
59 let fun h acc t = |
|
60 case (term_of t) of |
|
61 _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
|
62 | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc)) |
|
63 | Free _ => insert (op aconvc) t acc |
|
64 | _ => acc |
|
65 in h [] ct end; |
|
66 |
|
67 local |
|
68 val pcv = Simplifier.rewrite |
|
69 (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps) |
|
70 @ [@{thm "all_not_ex"}, not_all,ex_disj_distrib]) |
|
71 in |
|
72 fun standard_qelim_conv ctxt atcv ncv qcv p = |
|
73 gen_qelim_conv ctxt pcv pcv pcv cons (cterm_frees p) atcv ncv qcv p |
|
74 end; |
|
75 |
|
76 end; |
|