src/Provers/quantifier1.ML
author wenzelm
Thu Aug 08 23:46:09 2002 +0200 (2002-08-08)
changeset 13480 bb72bd43c6c3
parent 12523 0d8d5bf549b0
child 15027 d23887300b96
permissions -rw-r--r--
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
     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         
    26      And similarly for the bounded quantifiers.
    27 
    28 Gries etc call this the "1 point rules"
    29 *)
    30 
    31 signature QUANTIFIER1_DATA =
    32 sig
    33   (*abstract syntax*)
    34   val dest_eq: term -> (term*term*term)option
    35   val dest_conj: term -> (term*term*term)option
    36   val dest_imp:  term -> (term*term*term)option
    37   val conj: term
    38   val imp:  term
    39   (*rules*)
    40   val iff_reflection: thm (* P <-> Q ==> P == Q *)
    41   val iffI:  thm
    42   val iff_trans: thm
    43   val conjI: thm
    44   val conjE: thm
    45   val impI:  thm
    46   val mp:    thm
    47   val exI:   thm
    48   val exE:   thm
    49   val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
    50   val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
    51   val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
    52   val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
    53   val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
    54 end;
    55 
    56 signature QUANTIFIER1 =
    57 sig
    58   val prove_one_point_all_tac: tactic
    59   val prove_one_point_ex_tac: tactic
    60   val rearrange_all: Sign.sg -> thm list -> term -> thm option
    61   val rearrange_ex:  Sign.sg -> thm list -> term -> thm option
    62   val rearrange_ball: tactic -> Sign.sg -> thm list -> term -> thm option
    63   val rearrange_bex:  tactic -> Sign.sg -> thm list -> term -> thm option
    64 end;
    65 
    66 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
    67 struct
    68 
    69 open Data;
    70 
    71 (* FIXME: only test! *)
    72 fun def xs eq =
    73   let val n = length xs
    74   in case dest_eq eq of
    75       Some(c,s,t) =>
    76         s = Bound n andalso not(loose_bvar1(t,n)) orelse
    77         t = Bound n andalso not(loose_bvar1(s,n))
    78     | None => false
    79   end;
    80 
    81 fun extract_conj xs t = case dest_conj t of None => None
    82     | Some(conj,P,Q) =>
    83         (if def xs P then Some(xs,P,Q) else
    84          if def xs Q then Some(xs,Q,P) else
    85          (case extract_conj xs P of
    86             Some(xs,eq,P') => Some(xs,eq, conj $ P' $ Q)
    87           | None => (case extract_conj xs Q of
    88                        Some(xs,eq,Q') => Some(xs,eq,conj $ P $ Q')
    89                      | None => None)));
    90 
    91 fun extract_imp xs t = case dest_imp t of None => None
    92     | Some(imp,P,Q) => if def xs P then Some(xs,P,Q)
    93                        else (case extract_conj xs P of
    94                                Some(xs,eq,P') => Some(xs, eq, imp $ P' $ Q)
    95                              | None => (case extract_imp xs Q of
    96                                           None => None
    97                                         | Some(xs,eq,Q') =>
    98                                             Some(xs,eq,imp$P$Q')));
    99 
   100 fun extract_quant extract q =
   101   let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) =
   102             if qa = q then exqu ((qC,x,T)::xs) Q else None
   103         | exqu xs P = extract xs P
   104   in exqu end;
   105 
   106 fun prove_conv tac sg tu =
   107   Tactic.prove sg [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
   108 
   109 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
   110 
   111 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
   112    Better: instantiate exI
   113 *)
   114 local
   115 val excomm = ex_comm RS iff_trans
   116 in
   117 val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN
   118     ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
   119                     DEPTH_SOLVE_1 o (ares_tac [conjI])])
   120 end;
   121 
   122 (* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
   123           (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
   124 *)
   125 local
   126 val tac = SELECT_GOAL
   127           (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
   128                   REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
   129 val allcomm = all_comm RS iff_trans
   130 in
   131 val prove_one_point_all_tac =
   132       EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac]
   133 end
   134 
   135 fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else
   136                                    if i=u then l else i+1)
   137   | renumber l u (s$t) = renumber l u s $ renumber l u t
   138   | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t)
   139   | renumber _ _ atom = atom;
   140 
   141 fun quantify qC x T xs P =
   142   let fun quant [] P = P
   143         | quant ((qC,x,T)::xs) P = quant xs (qC $ Abs(x,T,P))
   144       val n = length xs
   145       val Q = if n=0 then P else renumber 0 n P
   146   in quant xs (qC $ Abs(x,T,Q)) end;
   147 
   148 fun rearrange_all sg _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
   149      (case extract_quant extract_imp q [] P of
   150         None => None
   151       | Some(xs,eq,Q) =>
   152           let val R = quantify all x T xs (imp $ eq $ Q)
   153           in Some(prove_conv prove_one_point_all_tac sg (F,R)) end)
   154   | rearrange_all _ _ _ = None;
   155 
   156 fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
   157      (case extract_imp [] P of
   158         None => None
   159       | Some(xs,eq,Q) => if not(null xs) then None else
   160           let val R = imp $ eq $ Q
   161           in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
   162   | rearrange_ball _ _ _ _ = None;
   163 
   164 fun rearrange_ex sg _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
   165      (case extract_quant extract_conj q [] P of
   166         None => None
   167       | Some(xs,eq,Q) =>
   168           let val R = quantify ex x T xs (conj $ eq $ Q)
   169           in Some(prove_conv prove_one_point_ex_tac sg (F,R)) end)
   170   | rearrange_ex _ _ _ = None;
   171 
   172 fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
   173      (case extract_conj [] P of
   174         None => None
   175       | Some(xs,eq,Q) => if not(null xs) then None else
   176           Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
   177   | rearrange_bex _ _ _ _ = None;
   178 
   179 end;