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