src/HOL/Tools/Qelim/qelim.ML
author haftmann
Sat Aug 28 16:14:32 2010 +0200 (2010-08-28)
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 41453 c03593812297
permissions -rw-r--r--
formerly unnamed infix equality now named HOL.eq
     1 (*  Title:      HOL/Tools/Qelim/qelim.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3 
     4 Generic quantifier elimination conversions for HOL formulae.
     5 *)
     6 
     7 signature QELIM =
     8 sig
     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
    13 end;
    14 
    15 structure Qelim: QELIM =
    16 struct
    17 
    18 open Conv;
    19 
    20 val all_not_ex = mk_meta_eq @{thm "all_not_ex"};
    21 
    22 fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv =
    23  let
    24   fun conv env p =
    25    case (term_of p) of
    26     Const(s,T)$_$_ => 
    27        if domain_type T = HOLogic.boolT
    28           andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
    29             @{const_name HOL.implies}, @{const_name HOL.eq}] s
    30        then binop_conv (conv env) p 
    31        else atcv env p
    32   | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
    33   | Const(@{const_name Ex},_)$Abs(s,_,_) =>
    34     let
    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')
    42     in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
    43        else Thm.transitive (Thm.transitive th th') (conv env r) end
    44   | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
    45   | Const(@{const_name All},_)$_ =>
    46     let
    47      val p = Thm.dest_arg p
    48      val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
    49      val th = instantiate' [SOME T] [SOME p] all_not_ex
    50     in Thm.transitive th (conv env (Thm.rhs_of th))
    51     end
    52   | _ => atcv env p
    53  in precv then_conv (conv env) then_conv postcv end
    54 
    55 (* Instantiation of some parameter for most common cases *)
    56 
    57 local
    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}]));
    62 
    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;
    66 
    67 end;