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