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