src/Provers/quantifier1.ML
changeset 11232 558a4feebb04
parent 11221 60c6e91f6079
child 12523 0d8d5bf549b0
     1.1 --- a/src/Provers/quantifier1.ML	Thu Mar 29 12:26:37 2001 +0200
     1.2 +++ b/src/Provers/quantifier1.ML	Thu Mar 29 13:59:54 2001 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5              ? x. ... & x = t & ...
     1.6       into   ? x. x = t & ... & ...
     1.7 -     where the `? x. x = t &' in the latter formula is eliminated
     1.8 +     where the `? x. x = t &' in the latter formula must be eliminated
     1.9             by ordinary simplification. 
    1.10  
    1.11       and   ! x. (... & x = t & ...) --> P x
    1.12 @@ -15,10 +15,14 @@
    1.13       where the `!x. x=t -->' in the latter formula is eliminated
    1.14             by ordinary simplification.
    1.15  
    1.16 +     And analogously for t=x, but the eqn is not turned around!
    1.17 +
    1.18       NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
    1.19          "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
    1.20          "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
    1.21 +        As must be "? x. t=x & P(x)".
    1.22  
    1.23 +        
    1.24       And similarly for the bounded quantifiers.
    1.25  
    1.26  Gries etc call this the "1 point rules"
    1.27 @@ -29,21 +33,20 @@
    1.28    (*abstract syntax*)
    1.29    val dest_eq: term -> (term*term*term)option
    1.30    val dest_conj: term -> (term*term*term)option
    1.31 +  val dest_imp:  term -> (term*term*term)option
    1.32    val conj: term
    1.33    val imp:  term
    1.34    (*rules*)
    1.35    val iff_reflection: thm (* P <-> Q ==> P == Q *)
    1.36    val iffI:  thm
    1.37 -  val sym:   thm
    1.38    val conjI: thm
    1.39    val conjE: thm
    1.40    val impI:  thm
    1.41 -  val impE:  thm
    1.42    val mp:    thm
    1.43    val exI:   thm
    1.44    val exE:   thm
    1.45 -  val allI:  thm
    1.46 -  val allE:  thm
    1.47 +  val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
    1.48 +  val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
    1.49  end;
    1.50  
    1.51  signature QUANTIFIER1 =
    1.52 @@ -61,28 +64,31 @@
    1.53  
    1.54  open Data;
    1.55  
    1.56 +(* FIXME: only test! *)
    1.57  fun def eq = case dest_eq eq of
    1.58        Some(c,s,t) =>
    1.59 -        if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
    1.60 -        if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c$t$s)
    1.61 -        else None
    1.62 -    | None => None;
    1.63 +        s = Bound 0 andalso not(loose_bvar1(t,0)) orelse
    1.64 +        t = Bound 0 andalso not(loose_bvar1(s,0))
    1.65 +    | None => false;
    1.66  
    1.67 -fun extract conj = case dest_conj conj of
    1.68 -      Some(conj,P,Q) =>
    1.69 -        (case def P of
    1.70 -           Some eq => Some(eq,Q)
    1.71 -         | None =>
    1.72 -             (case def Q of
    1.73 -                Some eq => Some(eq,P)
    1.74 -              | None =>
    1.75 -                 (case extract P of
    1.76 -                    Some(eq,P') => Some(eq, conj $ P' $ Q)
    1.77 -                  | None =>
    1.78 -                      (case extract Q of
    1.79 -                         Some(eq,Q') => Some(eq,conj $ P $ Q')
    1.80 -                       | None => None))))
    1.81 -    | None => None;
    1.82 +fun extract_conj t = case dest_conj t of None => None
    1.83 +    | Some(conj,P,Q) =>
    1.84 +        (if def P then Some(P,Q) else
    1.85 +         if def Q then Some(Q,P) else
    1.86 +         (case extract_conj P of
    1.87 +            Some(eq,P') => Some(eq, conj $ P' $ Q)
    1.88 +          | None => (case extract_conj Q of
    1.89 +                       Some(eq,Q') => Some(eq,conj $ P $ Q')
    1.90 +                     | None => None)));
    1.91 +
    1.92 +fun extract_imp t = case dest_imp t of None => None
    1.93 +    | Some(imp,P,Q) => if def P then Some(P,Q)
    1.94 +                       else (case extract_conj P of
    1.95 +                               Some(eq,P') => Some(eq, imp $ P' $ Q)
    1.96 +                             | None => (case extract_imp Q of
    1.97 +                                          None => None
    1.98 +                                        | Some(eq,Q') => Some(eq, imp$P$Q')));
    1.99 +    
   1.100  
   1.101  fun prove_conv tac sg tu =
   1.102    let val meta_eq = cterm_of sg (Logic.mk_equals tu)
   1.103 @@ -97,44 +103,44 @@
   1.104  *)
   1.105  val prove_one_point_ex_tac = rtac iffI 1 THEN
   1.106      ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
   1.107 -                    DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);
   1.108 +                    DEPTH_SOLVE_1 o (ares_tac [conjI])]);
   1.109  
   1.110  (* Proves (! x. (... & x = t & ...) --> P x) =
   1.111            (! x. x = t --> (... & ...) --> P x)
   1.112  *)
   1.113 -val prove_one_point_all_tac = EVERY1[rtac iffI,
   1.114 -                       rtac allI, etac allE, rtac impI, rtac impI, etac mp,
   1.115 -                          REPEAT o (etac conjE),
   1.116 -                          REPEAT o (ares_tac [conjI] ORELSE' etac sym),
   1.117 -                       rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
   1.118 -                          etac impE, atac ORELSE' etac sym, etac mp,
   1.119 -                          REPEAT o (ares_tac [conjI])];
   1.120 +local
   1.121 +val tac = SELECT_GOAL
   1.122 +          (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
   1.123 +                  REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
   1.124 +in
   1.125 +val prove_one_point_all_tac = EVERY1[rtac iff_allI, rtac iffI, tac, tac]
   1.126 +end
   1.127  
   1.128 -fun rearrange_all sg _ (F as all $ Abs(x,T,(* --> *)_ $ P $ Q)) =
   1.129 -     (case extract P of
   1.130 +fun rearrange_all sg _ (F as all $ Abs(x,T, P)) =
   1.131 +     (case extract_imp P of
   1.132          None => None
   1.133 -      | Some(eq,P') =>
   1.134 -          let val R = imp $ eq $ (imp $ P' $ Q)
   1.135 +      | Some(eq,Q) =>
   1.136 +          let val R = imp $ eq $ Q
   1.137            in Some(prove_conv prove_one_point_all_tac sg (F,all$Abs(x,T,R))) end)
   1.138    | rearrange_all _ _ _ = None;
   1.139  
   1.140 -fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,(* --> *)_ $ P $ Q)) =
   1.141 -     (case extract P of
   1.142 +fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
   1.143 +     (case extract_imp P of
   1.144          None => None
   1.145 -      | Some(eq,P') =>
   1.146 -          let val R = imp $ eq $ (imp $ P' $ Q)
   1.147 +      | Some(eq,Q) =>
   1.148 +          let val R = imp $ eq $ Q
   1.149            in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
   1.150    | rearrange_ball _ _ _ _ = None;
   1.151  
   1.152  fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
   1.153 -     (case extract P of
   1.154 +     (case extract_conj P of
   1.155          None => None
   1.156        | Some(eq,Q) =>
   1.157            Some(prove_conv prove_one_point_ex_tac sg (F,ex $ Abs(x,T,conj$eq$Q))))
   1.158    | rearrange_ex _ _ _ = None;
   1.159  
   1.160  fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
   1.161 -     (case extract P of
   1.162 +     (case extract_conj P of
   1.163          None => None
   1.164        | Some(eq,Q) =>
   1.165            Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))