23466
|
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;
|