src/Provers/quantifier1.ML
 changeset 4319 afb60b8bf15e child 7951 b36913c35699
equal inserted replaced
4318:9b672ea2dfe7 4319:afb60b8bf15e
`       `
`     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 val prove_ex_tac = rtac iffI 1 THEN`
`       `
`   106     ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),`
`       `
`   107                     rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)]);`
`       `
`   108 `
`       `
`   109 fun rearrange_ex sg _ (F as ex \$ Abs(x,T,P)) =`
`       `
`   110      (case extract P of`
`       `
`   111         None => None`
`       `
`   112       | Some(eq,Q) =>`
`       `
`   113           Some(prove_conv prove_ex_tac sg (F,ex \$ Abs(x,T,conj\$eq\$Q))))`
`       `
`   114   | rearrange_ex _ _ _ = None;`
`       `
`   115 `
`       `
`   116 end;`