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