src/Provers/quantifier1.ML
changeset 4319 afb60b8bf15e
child 7951 b36913c35699
equal deleted inserted replaced
4318:9b672ea2dfe7 4319:afb60b8bf15e
       
     1 (*  Title:      Provers/quantifier1
       
     2     ID:         $Id$
       
     3     Author:     Tobias Nipkow
       
     4     Copyright   1997  TU Munich
       
     5 
       
     6 Simplification procedures for turning
       
     7 
       
     8             ? x. ... & x = t & ...
       
     9      into   ? x. x = t & ... & ...
       
    10      where the `? x. x = t &' in the latter formula is eliminated
       
    11            by ordinary simplification. 
       
    12 
       
    13      and   ! x. (... & x = t & ...) --> P x
       
    14      into  ! x. x = t --> (... & ...) --> P x
       
    15      where the `!x. x=t -->' in the latter formula is eliminated
       
    16            by ordinary simplification.
       
    17 
       
    18      NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
       
    19         "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
       
    20         "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
       
    21 
       
    22 Gries etc call this the "1 point rules"
       
    23 *)
       
    24 
       
    25 signature QUANTIFIER1_DATA =
       
    26 sig
       
    27   (*abstract syntax*)
       
    28   val dest_eq: term -> (term*term*term)option
       
    29   val dest_conj: term -> (term*term*term)option
       
    30   val conj: term
       
    31   val imp:  term
       
    32   (*rules*)
       
    33   val iff_reflection: thm (* P <-> Q ==> P == Q *)
       
    34   val iffI:  thm
       
    35   val sym:   thm
       
    36   val conjI: thm
       
    37   val conjE: thm
       
    38   val impI:  thm
       
    39   val impE:  thm
       
    40   val mp:    thm
       
    41   val exI:   thm
       
    42   val exE:   thm
       
    43   val allI:  thm
       
    44   val allE:  thm
       
    45 end;
       
    46 
       
    47 signature QUANTIFIER1 =
       
    48 sig
       
    49   val rearrange_all: Sign.sg -> thm list -> term -> thm option
       
    50   val rearrange_ex:  Sign.sg -> thm list -> term -> thm option
       
    51 end;
       
    52 
       
    53 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
       
    54 struct
       
    55 
       
    56 open Data;
       
    57 
       
    58 fun def eq = case dest_eq eq of
       
    59       Some(c,s,t) =>
       
    60         if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
       
    61         if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c$t$s)
       
    62         else None
       
    63     | None => None;
       
    64 
       
    65 fun extract conj = case dest_conj conj of
       
    66       Some(conj,P,Q) =>
       
    67         (case def P of
       
    68            Some eq => Some(eq,Q)
       
    69          | None =>
       
    70              (case def Q of
       
    71                 Some eq => Some(eq,P)
       
    72               | None =>
       
    73                  (case extract P of
       
    74                     Some(eq,P') => Some(eq, conj $ P' $ Q)
       
    75                   | None =>
       
    76                       (case extract Q of
       
    77                          Some(eq,Q') => Some(eq,conj $ P $ Q')
       
    78                        | None => None))))
       
    79     | None => None;
       
    80 
       
    81 fun prove_conv tac sg tu =
       
    82   let val meta_eq = cterm_of sg (Logic.mk_equals tu)
       
    83   in prove_goalw_cterm [] meta_eq (K [rtac iff_reflection 1, tac])
       
    84      handle ERROR =>
       
    85             error("The error(s) above occurred while trying to prove " ^
       
    86                   string_of_cterm meta_eq)
       
    87   end;
       
    88 
       
    89 val prove_all_tac = EVERY1[rtac iffI,
       
    90                        rtac allI, etac allE, rtac impI, rtac impI, etac mp,
       
    91                           REPEAT o (etac conjE),
       
    92                           REPEAT o (ares_tac [conjI] ORELSE' etac sym),
       
    93                        rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
       
    94                           etac impE, atac ORELSE' etac sym, etac mp,
       
    95                           REPEAT o (ares_tac [conjI])];
       
    96 
       
    97 fun rearrange_all sg _ (F as all $ Abs(x,T,(* --> *)_ $ P $ Q)) =
       
    98      (case extract P of
       
    99         None => None
       
   100       | Some(eq,P') =>
       
   101           let val R = imp $ eq $ (imp $ P' $ Q)
       
   102           in Some(prove_conv prove_all_tac sg (F,all$Abs(x,T,R))) end)
       
   103   | rearrange_all _ _ _ = None;
       
   104 
       
   105 val prove_ex_tac = rtac iffI 1 THEN
       
   106     ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
       
   107                     rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)]);
       
   108 
       
   109 fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
       
   110      (case extract P of
       
   111         None => None
       
   112       | Some(eq,Q) =>
       
   113           Some(prove_conv prove_ex_tac sg (F,ex $ Abs(x,T,conj$eq$Q))))
       
   114   | rearrange_ex _ _ _ = None;
       
   115 
       
   116 end;