src/Provers/quantifier1.ML
author wenzelm
Sat Mar 13 16:44:12 2010 +0100 (2010-03-13)
changeset 35762 af3ff2ba4c54
parent 31197 c1c163ec6c44
child 36610 bafd82950e24
permissions -rw-r--r--
removed old CVS Ids;
tuned headers;
wenzelm@35762
     1
(*  Title:      Provers/quantifier1.ML
nipkow@4319
     2
    Author:     Tobias Nipkow
nipkow@4319
     3
    Copyright   1997  TU Munich
nipkow@4319
     4
nipkow@4319
     5
Simplification procedures for turning
nipkow@4319
     6
nipkow@4319
     7
            ? x. ... & x = t & ...
nipkow@4319
     8
     into   ? x. x = t & ... & ...
nipkow@11232
     9
     where the `? x. x = t &' in the latter formula must be eliminated
nipkow@4319
    10
           by ordinary simplification. 
nipkow@4319
    11
nipkow@4319
    12
     and   ! x. (... & x = t & ...) --> P x
nipkow@4319
    13
     into  ! x. x = t --> (... & ...) --> P x
nipkow@4319
    14
     where the `!x. x=t -->' in the latter formula is eliminated
nipkow@4319
    15
           by ordinary simplification.
nipkow@4319
    16
nipkow@11232
    17
     And analogously for t=x, but the eqn is not turned around!
nipkow@11232
    18
nipkow@4319
    19
     NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
nipkow@4319
    20
        "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
nipkow@4319
    21
        "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
nipkow@11232
    22
        As must be "? x. t=x & P(x)".
nipkow@11232
    23
        
nipkow@11221
    24
     And similarly for the bounded quantifiers.
nipkow@11221
    25
nipkow@4319
    26
Gries etc call this the "1 point rules"
nipkow@31166
    27
nipkow@31166
    28
The above also works for !x1..xn. and ?x1..xn by moving the defined
nipkow@31166
    29
qunatifier inside first, but not for nested bounded quantifiers.
nipkow@31166
    30
nipkow@31166
    31
For set comprehensions the basic permutations
nipkow@31166
    32
      ... & x = t & ...  ->  x = t & (... & ...)
nipkow@31166
    33
      ... & t = x & ...  ->  t = x & (... & ...)
nipkow@31166
    34
are also exported.
nipkow@31166
    35
nipkow@31166
    36
To avoid looping, NONE is returned if the term cannot be rearranged,
nipkow@31166
    37
esp if x=t/t=x sits at the front already.
nipkow@4319
    38
*)
nipkow@4319
    39
nipkow@4319
    40
signature QUANTIFIER1_DATA =
nipkow@4319
    41
sig
nipkow@4319
    42
  (*abstract syntax*)
nipkow@4319
    43
  val dest_eq: term -> (term*term*term)option
nipkow@4319
    44
  val dest_conj: term -> (term*term*term)option
nipkow@11232
    45
  val dest_imp:  term -> (term*term*term)option
nipkow@4319
    46
  val conj: term
nipkow@4319
    47
  val imp:  term
nipkow@4319
    48
  (*rules*)
nipkow@4319
    49
  val iff_reflection: thm (* P <-> Q ==> P == Q *)
nipkow@4319
    50
  val iffI:  thm
nipkow@12523
    51
  val iff_trans: thm
nipkow@4319
    52
  val conjI: thm
nipkow@4319
    53
  val conjE: thm
nipkow@4319
    54
  val impI:  thm
nipkow@4319
    55
  val mp:    thm
nipkow@4319
    56
  val exI:   thm
nipkow@4319
    57
  val exE:   thm
nipkow@11232
    58
  val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
nipkow@11232
    59
  val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
nipkow@12523
    60
  val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
nipkow@12523
    61
  val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
nipkow@12523
    62
  val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
nipkow@4319
    63
end;
nipkow@4319
    64
nipkow@4319
    65
signature QUANTIFIER1 =
nipkow@4319
    66
sig
nipkow@11221
    67
  val prove_one_point_all_tac: tactic
nipkow@11221
    68
  val prove_one_point_ex_tac: tactic
wenzelm@17002
    69
  val rearrange_all: theory -> simpset -> term -> thm option
wenzelm@17002
    70
  val rearrange_ex:  theory -> simpset -> term -> thm option
wenzelm@17002
    71
  val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
wenzelm@17002
    72
  val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
nipkow@31166
    73
  val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option
nipkow@4319
    74
end;
nipkow@4319
    75
nipkow@4319
    76
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
nipkow@4319
    77
struct
nipkow@4319
    78
nipkow@4319
    79
open Data;
nipkow@4319
    80
nipkow@11232
    81
(* FIXME: only test! *)
nipkow@12523
    82
fun def xs eq =
nipkow@31166
    83
  (case dest_eq eq of
nipkow@31166
    84
     SOME(c,s,t) =>
nipkow@31166
    85
       let val n = length xs
nipkow@31166
    86
       in s = Bound n andalso not(loose_bvar1(t,n)) orelse
nipkow@31166
    87
          t = Bound n andalso not(loose_bvar1(s,n)) end
nipkow@31166
    88
   | NONE => false);
nipkow@4319
    89
nipkow@31166
    90
fun extract_conj fst xs t = case dest_conj t of NONE => NONE
skalberg@15531
    91
    | SOME(conj,P,Q) =>
nipkow@31197
    92
        (if def xs P then (if fst then NONE else SOME(xs,P,Q)) else
skalberg@15531
    93
         if def xs Q then SOME(xs,Q,P) else
nipkow@31166
    94
         (case extract_conj false xs P of
skalberg@15531
    95
            SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q)
nipkow@31166
    96
          | NONE => (case extract_conj false xs Q of
skalberg@15531
    97
                       SOME(xs,eq,Q') => SOME(xs,eq,conj $ P $ Q')
skalberg@15531
    98
                     | NONE => NONE)));
nipkow@11232
    99
nipkow@31166
   100
fun extract_imp fst xs t = case dest_imp t of NONE => NONE
nipkow@31197
   101
    | SOME(imp,P,Q) => if def xs P then (if fst then NONE else SOME(xs,P,Q))
nipkow@31166
   102
                       else (case extract_conj false xs P of
skalberg@15531
   103
                               SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q)
nipkow@31166
   104
                             | NONE => (case extract_imp false xs Q of
skalberg@15531
   105
                                          NONE => NONE
skalberg@15531
   106
                                        | SOME(xs,eq,Q') =>
skalberg@15531
   107
                                            SOME(xs,eq,imp$P$Q')));
nipkow@12523
   108
nipkow@12523
   109
fun extract_quant extract q =
nipkow@12523
   110
  let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) =
skalberg@15531
   111
            if qa = q then exqu ((qC,x,T)::xs) Q else NONE
nipkow@31166
   112
        | exqu xs P = extract (null xs) xs P
nipkow@31166
   113
  in exqu [] end;
nipkow@4319
   114
wenzelm@17002
   115
fun prove_conv tac thy tu =
wenzelm@20049
   116
  Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
wenzelm@20049
   117
    (K (rtac iff_reflection 1 THEN tac));
nipkow@4319
   118
nipkow@12523
   119
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
nipkow@12523
   120
nipkow@12523
   121
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
nipkow@11221
   122
   Better: instantiate exI
nipkow@11221
   123
*)
nipkow@12523
   124
local
nipkow@12523
   125
val excomm = ex_comm RS iff_trans
nipkow@12523
   126
in
nipkow@12523
   127
val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN
nipkow@11221
   128
    ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
nipkow@12523
   129
                    DEPTH_SOLVE_1 o (ares_tac [conjI])])
nipkow@12523
   130
end;
nipkow@11221
   131
nipkow@12523
   132
(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
nipkow@12523
   133
          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
nipkow@11221
   134
*)
nipkow@11232
   135
local
nipkow@11232
   136
val tac = SELECT_GOAL
nipkow@11232
   137
          (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
nipkow@11232
   138
                  REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
nipkow@12523
   139
val allcomm = all_comm RS iff_trans
nipkow@11232
   140
in
nipkow@12523
   141
val prove_one_point_all_tac =
nipkow@12523
   142
      EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac]
nipkow@11232
   143
end
nipkow@4319
   144
nipkow@12523
   145
fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else
nipkow@12523
   146
                                   if i=u then l else i+1)
nipkow@12523
   147
  | renumber l u (s$t) = renumber l u s $ renumber l u t
nipkow@12523
   148
  | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t)
nipkow@12523
   149
  | renumber _ _ atom = atom;
nipkow@12523
   150
nipkow@12523
   151
fun quantify qC x T xs P =
nipkow@12523
   152
  let fun quant [] P = P
nipkow@12523
   153
        | quant ((qC,x,T)::xs) P = quant xs (qC $ Abs(x,T,P))
nipkow@12523
   154
      val n = length xs
nipkow@12523
   155
      val Q = if n=0 then P else renumber 0 n P
nipkow@12523
   156
  in quant xs (qC $ Abs(x,T,Q)) end;
nipkow@12523
   157
wenzelm@17002
   158
fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
nipkow@31166
   159
     (case extract_quant extract_imp q P of
skalberg@15531
   160
        NONE => NONE
skalberg@15531
   161
      | SOME(xs,eq,Q) =>
nipkow@12523
   162
          let val R = quantify all x T xs (imp $ eq $ Q)
wenzelm@17002
   163
          in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
skalberg@15531
   164
  | rearrange_all _ _ _ = NONE;
nipkow@4319
   165
wenzelm@17002
   166
fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) =
nipkow@31166
   167
     (case extract_imp true [] P of
skalberg@15531
   168
        NONE => NONE
skalberg@15531
   169
      | SOME(xs,eq,Q) => if not(null xs) then NONE else
nipkow@11232
   170
          let val R = imp $ eq $ Q
wenzelm@17002
   171
          in SOME(prove_conv (tac ss) thy (F,Ball $ A $ Abs(x,T,R))) end)
skalberg@15531
   172
  | rearrange_ball _ _ _ _ = NONE;
nipkow@4319
   173
wenzelm@17002
   174
fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
nipkow@31166
   175
     (case extract_quant extract_conj q P of
skalberg@15531
   176
        NONE => NONE
skalberg@15531
   177
      | SOME(xs,eq,Q) =>
nipkow@12523
   178
          let val R = quantify ex x T xs (conj $ eq $ Q)
wenzelm@17002
   179
          in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
skalberg@15531
   180
  | rearrange_ex _ _ _ = NONE;
nipkow@4319
   181
wenzelm@17002
   182
fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) =
nipkow@31166
   183
     (case extract_conj true [] P of
skalberg@15531
   184
        NONE => NONE
skalberg@15531
   185
      | SOME(xs,eq,Q) => if not(null xs) then NONE else
wenzelm@17002
   186
          SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
skalberg@15531
   187
  | rearrange_bex _ _ _ _ = NONE;
nipkow@11221
   188
nipkow@31166
   189
fun rearrange_Coll tac thy _ (F as Coll $ Abs(x,T,P)) =
nipkow@31166
   190
     (case extract_conj true [] P of
nipkow@31166
   191
        NONE => NONE
nipkow@31166
   192
      | SOME(_,eq,Q) =>
nipkow@31166
   193
          let val R = Coll $ Abs(x,T, conj $ eq $ Q)
nipkow@31166
   194
          in SOME(prove_conv tac thy (F,R)) end);
nipkow@31166
   195
nipkow@4319
   196
end;