src/Provers/quantifier1.ML
 author nipkow Wed Oct 27 17:17:28 1999 +0200 (1999-10-27) changeset 7951 b36913c35699 parent 4319 afb60b8bf15e child 11221 60c6e91f6079 permissions -rw-r--r--
Fixed a bug in the EX simproc.
```     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 is 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      NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
```
```    19         "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
```
```    20         "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
```
```    21
```
```    22 Gries etc call this the "1 point rules"
```
```    23 *)
```
```    24
```
```    25 signature QUANTIFIER1_DATA =
```
```    26 sig
```
```    27   (*abstract syntax*)
```
```    28   val dest_eq: term -> (term*term*term)option
```
```    29   val dest_conj: term -> (term*term*term)option
```
```    30   val conj: term
```
```    31   val imp:  term
```
```    32   (*rules*)
```
```    33   val iff_reflection: thm (* P <-> Q ==> P == Q *)
```
```    34   val iffI:  thm
```
```    35   val sym:   thm
```
```    36   val conjI: thm
```
```    37   val conjE: thm
```
```    38   val impI:  thm
```
```    39   val impE:  thm
```
```    40   val mp:    thm
```
```    41   val exI:   thm
```
```    42   val exE:   thm
```
```    43   val allI:  thm
```
```    44   val allE:  thm
```
```    45 end;
```
```    46
```
```    47 signature QUANTIFIER1 =
```
```    48 sig
```
```    49   val rearrange_all: Sign.sg -> thm list -> term -> thm option
```
```    50   val rearrange_ex:  Sign.sg -> thm list -> term -> thm option
```
```    51 end;
```
```    52
```
```    53 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
```
```    54 struct
```
```    55
```
```    56 open Data;
```
```    57
```
```    58 fun def eq = case dest_eq eq of
```
```    59       Some(c,s,t) =>
```
```    60         if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
```
```    61         if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c\$t\$s)
```
```    62         else None
```
```    63     | None => None;
```
```    64
```
```    65 fun extract conj = case dest_conj conj of
```
```    66       Some(conj,P,Q) =>
```
```    67         (case def P of
```
```    68            Some eq => Some(eq,Q)
```
```    69          | None =>
```
```    70              (case def Q of
```
```    71                 Some eq => Some(eq,P)
```
```    72               | None =>
```
```    73                  (case extract P of
```
```    74                     Some(eq,P') => Some(eq, conj \$ P' \$ Q)
```
```    75                   | None =>
```
```    76                       (case extract Q of
```
```    77                          Some(eq,Q') => Some(eq,conj \$ P \$ Q')
```
```    78                        | None => None))))
```
```    79     | None => None;
```
```    80
```
```    81 fun prove_conv tac sg tu =
```
```    82   let val meta_eq = cterm_of sg (Logic.mk_equals tu)
```
```    83   in prove_goalw_cterm [] meta_eq (K [rtac iff_reflection 1, tac])
```
```    84      handle ERROR =>
```
```    85             error("The error(s) above occurred while trying to prove " ^
```
```    86                   string_of_cterm meta_eq)
```
```    87   end;
```
```    88
```
```    89 val prove_all_tac = EVERY1[rtac iffI,
```
```    90                        rtac allI, etac allE, rtac impI, rtac impI, etac mp,
```
```    91                           REPEAT o (etac conjE),
```
```    92                           REPEAT o (ares_tac [conjI] ORELSE' etac sym),
```
```    93                        rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
```
```    94                           etac impE, atac ORELSE' etac sym, etac mp,
```
```    95                           REPEAT o (ares_tac [conjI])];
```
```    96
```
```    97 fun rearrange_all sg _ (F as all \$ Abs(x,T,(* --> *)_ \$ P \$ Q)) =
```
```    98      (case extract P of
```
```    99         None => None
```
```   100       | Some(eq,P') =>
```
```   101           let val R = imp \$ eq \$ (imp \$ P' \$ Q)
```
```   102           in Some(prove_conv prove_all_tac sg (F,all\$Abs(x,T,R))) end)
```
```   103   | rearrange_all _ _ _ = None;
```
```   104
```
```   105 (* Better: instantiate exI *)
```
```   106 val prove_ex_tac = rtac iffI 1 THEN
```
```   107     ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
```
```   108                     DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);
```
```   109
```
```   110 fun rearrange_ex sg _ (F as ex \$ Abs(x,T,P)) =
```
```   111      (case extract P of
```
```   112         None => None
```
```   113       | Some(eq,Q) =>
```
```   114           Some(prove_conv prove_ex_tac sg (F,ex \$ Abs(x,T,conj\$eq\$Q))))
```
```   115   | rearrange_ex _ _ _ = None;
```
```   116
```
```   117 end;
```