(*  Title:      HOL/Tools/Qelim/qelim.ML

     Author:     Amine Chaieb, TU Muenchen

 Generic quantifier elimination conversions for HOL formulae.

 *)

 signature QELIM =

 sig

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

                      -> ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv

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

                           -> (cterm list -> conv) -> conv

 end;

 structure Qelim: QELIM =

 struct

 open Conv;

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

 fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv =

  let

   fun conv env p =

    case (term_of p) of

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

        if domain_type T = HOLogic.boolT

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

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

        then binop_conv (conv env) p 

        else atcv env p

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

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

     let

      val (e,p0) = Thm.dest_comb p

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

      val env' = ins x env

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

                    |> Drule.arg_cong_rule e

      val th' = simpex_conv (Thm.rhs_of th)

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

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

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

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

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

     let

      val p = Thm.dest_arg p

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

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

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

     end

   | _ => atcv env p

  in precv then_conv (conv env) then_conv postcv end

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

 local

 val pcv =

   Simplifier.rewrite

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

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

 in fun standard_qelim_conv atcv ncv qcv p =

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

 end;

 end;