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))))
```