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