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

23904

9 
val gen_qelim_conv: conv > conv > conv > (cterm > 'a > 'a) > 'a


10 
> ('a > conv) > ('a > conv) > ('a > conv) > conv


11 
val standard_qelim_conv: (cterm list > conv) > (cterm list > conv)


12 
> (cterm list > conv) > conv

23466

13 
end;


14 

23489

15 
structure Qelim: QELIM =

23466

16 
struct


17 


18 
open Conv;


19 

23489

20 
val all_not_ex = mk_meta_eq @{thm "all_not_ex"};


21 

23524

22 
fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv =

23489

23 
let

23466

24 
fun conv env p =

23489

25 
case (term_of p) of

23904

26 
Const(s,T)$_$_ =>


27 
if domain_type T = HOLogic.boolT

30657

28 
andalso member (op =) [@{const_name "op &"}, @{const_name "op "},


29 
@{const_name "op >"}, @{const_name "op ="}] s

23904

30 
then binop_conv (conv env) p


31 
else atcv env p

32603

32 
 Const(@{const_name Not},_)$_ => arg_conv (conv env) p


33 
 Const(@{const_name Ex},_)$Abs(s,_,_) =>

23489

34 
let

23466

35 
val (e,p0) = Thm.dest_comb p


36 
val (x,p') = Thm.dest_abs (SOME s) p0


37 
val env' = ins x env


38 
val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')


39 
> Drule.arg_cong_rule e


40 
val th' = simpex_conv (Thm.rhs_of th)


41 
val (l,r) = Thm.dest_equals (cprop_of th')

23593

42 
in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))

23466

43 
else Thm.transitive (Thm.transitive th th') (conv env r) end

32603

44 
 Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p


45 
 Const(@{const_name All},_)$_ =>

23489

46 
let

23466

47 
val p = Thm.dest_arg p


48 
val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)

23489

49 
val th = instantiate' [SOME T] [SOME p] all_not_ex

36945

50 
in Thm.transitive th (conv env (Thm.rhs_of th))

23466

51 
end


52 
 _ => atcv env p


53 
in precv then_conv (conv env) then_conv postcv end

23489

54 

23904

55 
(* Instantiation of some parameter for most common cases *)

23489

56 

23904

57 
local

35410

58 
val pcv =


59 
Simplifier.rewrite


60 
(HOL_basic_ss addsimps (@{thms simp_thms} @ @{thms ex_simps} @ @{thms all_simps} @


61 
[@{thm all_not_ex}, not_all, @{thm ex_disj_distrib}]));

23466

62 

23904

63 
in fun standard_qelim_conv atcv ncv qcv p =


64 
gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p


65 
end;

23466

66 


67 
end;
