1.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Sun Jul 22 17:53:48 2007 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Sun Jul 22 17:53:50 2007 +0200
     1.3 @@ -1,17 +1,16 @@
     1.4  (*  Title:      HOL/Tools/Qelim/qelim.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Amine Chaieb and Tobias Nipkow, TU Muenchen
     1.7 +    Author:     Amine Chaieb, TU Muenchen
     1.8  
     1.9 -Proof protocolling and proof generation for multiple quantified formulae.
    1.10 +Generic quantifier elimination conversions for HOL formulae.
    1.11  *)
    1.12  
    1.13  signature QELIM =
    1.14  sig
    1.15 - val gen_qelim_conv: conv -> conv -> conv ->
    1.16 -   (cterm -> 'a -> 'a) -> 'a -> ('a -> cterm -> thm) ->
    1.17 -   ('a -> conv) -> ('a -> cterm -> thm) -> conv
    1.18 - val standard_qelim_conv: (cterm list -> cterm -> thm) ->
    1.19 -   (cterm list -> conv) -> (cterm list -> cterm -> thm) -> cterm -> thm
    1.20 + val gen_qelim_conv: conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a 
    1.21 +                     -> ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv
    1.22 + val standard_qelim_conv: (cterm list -> conv) -> (cterm list -> conv) 
    1.23 +                          -> (cterm list -> conv) -> conv
    1.24  end;
    1.25  
    1.26  structure Qelim: QELIM =
    1.27 @@ -19,18 +18,17 @@
    1.28  
    1.29  open Conv;
    1.30  
    1.31 -
    1.32 -(* gen_qelim_conv *)
    1.33 -
    1.34  val all_not_ex = mk_meta_eq @{thm "all_not_ex"};
    1.35  
    1.36  fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv =
    1.37   let
    1.38    fun conv env p =
    1.39     case (term_of p) of
    1.40 -    Const(s,T)$_$_ => if domain_type T = HOLogic.boolT
    1.41 -                         andalso s mem ["op &","op |","op -->","op ="]
    1.42 -                     then binop_conv (conv env) p else atcv env p
    1.43 +    Const(s,T)$_$_ => 
    1.44 +       if domain_type T = HOLogic.boolT
    1.45 +          andalso s mem ["op &","op |","op -->","op ="]
    1.46 +       then binop_conv (conv env) p 
    1.47 +       else atcv env p
    1.48    | Const("Not",_)$_ => arg_conv (conv env) p
    1.49    | Const("Ex",_)$Abs(s,_,_) =>
    1.50      let
    1.51 @@ -54,14 +52,15 @@
    1.52    | _ => atcv env p
    1.53   in precv then_conv (conv env) then_conv postcv end
    1.54  
    1.55 +(* Instantiation of some parameter for most common cases *)
    1.56  
    1.57 -(* standard_qelim_conv *)
    1.58 -
    1.59 +local
    1.60  val pcv = Simplifier.rewrite
    1.61                   (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
    1.62                       @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]);
    1.63  
    1.64 -fun standard_qelim_conv atcv ncv qcv p =
    1.65 -  gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p;
    1.66 +in fun standard_qelim_conv atcv ncv qcv p =
    1.67 +      gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p
    1.68 +end;
    1.69  
    1.70  end;