src/HOL/Tools/Presburger/qelim.ML
author haftmann
Fri Feb 10 09:09:07 2006 +0100 (2006-02-10)
changeset 19008 14c1b2f5dda4
parent 15531 08c8dad8e399
child 19250 932a50e2332f
permissions -rw-r--r--
improved code generator devarification
     1 (*  Title:      HOL/Integ/qelim.ML
     2     ID:         $Id$
     3     Author:     Amine Chaieb and Tobias Nipkow, TU Muenchen
     4 
     5 File containing the implementation of the proof protocoling
     6 and proof generation for multiple quantified formulae.
     7 *)
     8 
     9 signature QELIM =
    10  sig
    11  val tproof_of_mlift_qelim: Sign.sg -> (term -> bool) ->
    12    (string list -> term -> thm) -> (term -> thm) ->
    13    (term -> thm) -> term -> thm
    14 
    15 end;
    16 
    17 structure Qelim : QELIM =
    18 struct
    19 open CooperDec;
    20 open CooperProof;
    21 
    22 val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
    23 
    24 (* List of the theorems to be used in the following*)
    25 
    26 val qe_ex_conj = thm "qe_ex_conj";
    27 val qe_ex_nconj = thm "qe_ex_nconj";
    28 val qe_ALL = thm "qe_ALL";
    29 
    30 
    31 (*============= Compact version =====*)
    32 
    33 
    34 fun decomp_qe is_at afnp nfnp qfnp sg P = 
    35    if is_at P then ([], fn [] => afnp [] P) else 
    36    case P of
    37    (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
    38    |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
    39    |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
    40    |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
    41    |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
    42    |(Const("Ex",_)$Abs(xn,xT,p)) => 
    43       let val (xn1,p1) = variant_abs(xn,xT,p) 
    44       in ([p1],
    45         fn [th1_1] => 
    46           let val th2 = [th1_1,nfnp (snd (qe_get_terms th1_1))] MRS trans
    47               val eth1 = (forall_intr (cterm_of sg (Free(xn1,xT))) th2) COMP  qe_exI
    48               val th3 = qfnp (snd(qe_get_terms eth1))
    49           in [eth1,th3] MRS trans
    50           end )
    51       end
    52 
    53    |(Const("All",_)$Abs(xn,xT,p)) => ([(HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p)], fn [th] => th RS qe_ALL)
    54    | _ => ([],fn [] => instantiate' [SOME (ctyp_of sg (type_of P))] [SOME (cterm_of sg P)] refl);
    55  
    56 
    57 fun tproof_of_mlift_qelim sg isat afnp nfnp qfnp p = 
    58    let val th1 = thm_of sg (decomp_qe isat afnp nfnp qfnp sg) p
    59        val th2 = nfnp (snd (qe_get_terms th1))
    60     in [th1,th2] MRS trans
    61     end;
    62 end;