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
     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 conjI: thm
    43   val conjE: thm
    44   val impI:  thm
    45   val mp:    thm
    46   val exI:   thm
    47   val exE:   thm
    48   val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
    49   val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
    50 end;
    51 
    52 signature QUANTIFIER1 =
    53 sig
    54   val prove_one_point_all_tac: tactic
    55   val prove_one_point_ex_tac: tactic
    56   val rearrange_all: Sign.sg -> thm list -> term -> thm option
    57   val rearrange_ex:  Sign.sg -> thm list -> term -> thm option
    58   val rearrange_ball: tactic -> Sign.sg -> thm list -> term -> thm option
    59   val rearrange_bex:  tactic -> Sign.sg -> thm list -> term -> thm option
    60 end;
    61 
    62 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
    63 struct
    64 
    65 open Data;
    66 
    67 (* FIXME: only test! *)
    68 fun def eq = case dest_eq eq of
    69       Some(c,s,t) =>
    70         s = Bound 0 andalso not(loose_bvar1(t,0)) orelse
    71         t = Bound 0 andalso not(loose_bvar1(s,0))
    72     | None => false;
    73 
    74 fun extract_conj t = case dest_conj t of None => None
    75     | Some(conj,P,Q) =>
    76         (if def P then Some(P,Q) else
    77          if def Q then Some(Q,P) else
    78          (case extract_conj P of
    79             Some(eq,P') => Some(eq, conj $ P' $ Q)
    80           | None => (case extract_conj Q of
    81                        Some(eq,Q') => Some(eq,conj $ P $ Q')
    82                      | None => None)));
    83 
    84 fun extract_imp t = case dest_imp t of None => None
    85     | Some(imp,P,Q) => if def P then Some(P,Q)
    86                        else (case extract_conj P of
    87                                Some(eq,P') => Some(eq, imp $ P' $ Q)
    88                              | None => (case extract_imp Q of
    89                                           None => None
    90                                         | Some(eq,Q') => Some(eq, imp$P$Q')));
    91     
    92 
    93 fun prove_conv tac sg tu =
    94   let val meta_eq = cterm_of sg (Logic.mk_equals tu)
    95   in prove_goalw_cterm [] meta_eq (K [rtac iff_reflection 1, tac])
    96      handle ERROR =>
    97             error("The error(s) above occurred while trying to prove " ^
    98                   string_of_cterm meta_eq)
    99   end;
   100 
   101 (* Proves (? x. ... & x = t & ...) = (? x. x = t & ... & ...)
   102    Better: instantiate exI
   103 *)
   104 val prove_one_point_ex_tac = rtac iffI 1 THEN
   105     ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
   106                     DEPTH_SOLVE_1 o (ares_tac [conjI])]);
   107 
   108 (* Proves (! x. (... & x = t & ...) --> P x) =
   109           (! x. x = t --> (... & ...) --> P x)
   110 *)
   111 local
   112 val tac = SELECT_GOAL
   113           (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
   114                   REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
   115 in
   116 val prove_one_point_all_tac = EVERY1[rtac iff_allI, rtac iffI, tac, tac]
   117 end
   118 
   119 fun rearrange_all sg _ (F as all $ Abs(x,T, P)) =
   120      (case extract_imp P of
   121         None => None
   122       | Some(eq,Q) =>
   123           let val R = imp $ eq $ Q
   124           in Some(prove_conv prove_one_point_all_tac sg (F,all$Abs(x,T,R))) end)
   125   | rearrange_all _ _ _ = None;
   126 
   127 fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
   128      (case extract_imp P of
   129         None => None
   130       | Some(eq,Q) =>
   131           let val R = imp $ eq $ Q
   132           in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
   133   | rearrange_ball _ _ _ _ = None;
   134 
   135 fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
   136      (case extract_conj P of
   137         None => None
   138       | Some(eq,Q) =>
   139           Some(prove_conv prove_one_point_ex_tac sg (F,ex $ Abs(x,T,conj$eq$Q))))
   140   | rearrange_ex _ _ _ = None;
   141 
   142 fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
   143      (case extract_conj P of
   144         None => None
   145       | Some(eq,Q) =>
   146           Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
   147   | rearrange_bex _ _ _ _ = None;
   148 
   149 end;