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
wenzelm@23489
     1
(*  Title:      HOL/Tools/Qelim/qelim.ML
chaieb@23904
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@23466
     3
chaieb@23904
     4
Generic quantifier elimination conversions for HOL formulae.
wenzelm@23466
     5
*)
wenzelm@23466
     6
wenzelm@23466
     7
signature QELIM =
wenzelm@23466
     8
sig
chaieb@23904
     9
 val gen_qelim_conv: conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a 
chaieb@23904
    10
                     -> ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv
chaieb@23904
    11
 val standard_qelim_conv: (cterm list -> conv) -> (cterm list -> conv) 
chaieb@23904
    12
                          -> (cterm list -> conv) -> conv
wenzelm@23466
    13
end;
wenzelm@23466
    14
wenzelm@23489
    15
structure Qelim: QELIM =
wenzelm@23466
    16
struct
wenzelm@23466
    17
wenzelm@23466
    18
open Conv;
wenzelm@23466
    19
wenzelm@23489
    20
val all_not_ex = mk_meta_eq @{thm "all_not_ex"};
wenzelm@23489
    21
chaieb@23524
    22
fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv =
wenzelm@23489
    23
 let
wenzelm@23466
    24
  fun conv env p =
wenzelm@23489
    25
   case (term_of p) of
chaieb@23904
    26
    Const(s,T)$_$_ => 
chaieb@23904
    27
       if domain_type T = HOLogic.boolT
haftmann@38795
    28
          andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
haftmann@38864
    29
            @{const_name HOL.implies}, @{const_name HOL.eq}] s
chaieb@23904
    30
       then binop_conv (conv env) p 
chaieb@23904
    31
       else atcv env p
haftmann@32603
    32
  | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
haftmann@32603
    33
  | Const(@{const_name Ex},_)$Abs(s,_,_) =>
wenzelm@23489
    34
    let
wenzelm@23466
    35
     val (e,p0) = Thm.dest_comb p
wenzelm@23466
    36
     val (x,p') = Thm.dest_abs (SOME s) p0
wenzelm@23466
    37
     val env' = ins x env
wenzelm@23466
    38
     val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
wenzelm@23466
    39
                   |> Drule.arg_cong_rule e
wenzelm@23466
    40
     val th' = simpex_conv (Thm.rhs_of th)
wenzelm@23466
    41
     val (l,r) = Thm.dest_equals (cprop_of th')
wenzelm@23593
    42
    in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
wenzelm@23466
    43
       else Thm.transitive (Thm.transitive th th') (conv env r) end
haftmann@32603
    44
  | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
haftmann@32603
    45
  | Const(@{const_name All},_)$_ =>
wenzelm@23489
    46
    let
wenzelm@23466
    47
     val p = Thm.dest_arg p
wenzelm@23466
    48
     val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
wenzelm@23489
    49
     val th = instantiate' [SOME T] [SOME p] all_not_ex
wenzelm@36945
    50
    in Thm.transitive th (conv env (Thm.rhs_of th))
wenzelm@23466
    51
    end
wenzelm@23466
    52
  | _ => atcv env p
wenzelm@23466
    53
 in precv then_conv (conv env) then_conv postcv end
wenzelm@23489
    54
chaieb@23904
    55
(* Instantiation of some parameter for most common cases *)
wenzelm@23489
    56
chaieb@23904
    57
local
wenzelm@35410
    58
val pcv =
wenzelm@35410
    59
  Simplifier.rewrite
wenzelm@35410
    60
    (HOL_basic_ss addsimps (@{thms simp_thms} @ @{thms ex_simps} @ @{thms all_simps} @
wenzelm@35410
    61
        [@{thm all_not_ex}, not_all, @{thm ex_disj_distrib}]));
wenzelm@23466
    62
chaieb@23904
    63
in fun standard_qelim_conv atcv ncv qcv p =
chaieb@23904
    64
      gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p
chaieb@23904
    65
end;
wenzelm@23466
    66
wenzelm@23466
    67
end;