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