src/Provers/quantifier1.ML
 author wenzelm Sun Mar 07 12:19:47 2010 +0100 (2010-03-07) changeset 35625 9c818cab0dd0 parent 31197 c1c163ec6c44 child 35762 af3ff2ba4c54 permissions -rw-r--r--
modernized structure Object_Logic;
```     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      And similarly for the bounded quantifiers.
```
```    26
```
```    27 Gries etc call this the "1 point rules"
```
```    28
```
```    29 The above also works for !x1..xn. and ?x1..xn by moving the defined
```
```    30 qunatifier inside first, but not for nested bounded quantifiers.
```
```    31
```
```    32 For set comprehensions the basic permutations
```
```    33       ... & x = t & ...  ->  x = t & (... & ...)
```
```    34       ... & t = x & ...  ->  t = x & (... & ...)
```
```    35 are also exported.
```
```    36
```
```    37 To avoid looping, NONE is returned if the term cannot be rearranged,
```
```    38 esp if x=t/t=x sits at the front already.
```
```    39 *)
```
```    40
```
```    41 signature QUANTIFIER1_DATA =
```
```    42 sig
```
```    43   (*abstract syntax*)
```
```    44   val dest_eq: term -> (term*term*term)option
```
```    45   val dest_conj: term -> (term*term*term)option
```
```    46   val dest_imp:  term -> (term*term*term)option
```
```    47   val conj: term
```
```    48   val imp:  term
```
```    49   (*rules*)
```
```    50   val iff_reflection: thm (* P <-> Q ==> P == Q *)
```
```    51   val iffI:  thm
```
```    52   val iff_trans: thm
```
```    53   val conjI: thm
```
```    54   val conjE: thm
```
```    55   val impI:  thm
```
```    56   val mp:    thm
```
```    57   val exI:   thm
```
```    58   val exE:   thm
```
```    59   val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
```
```    60   val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
```
```    61   val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
```
```    62   val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
```
```    63   val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
```
```    64 end;
```
```    65
```
```    66 signature QUANTIFIER1 =
```
```    67 sig
```
```    68   val prove_one_point_all_tac: tactic
```
```    69   val prove_one_point_ex_tac: tactic
```
```    70   val rearrange_all: theory -> simpset -> term -> thm option
```
```    71   val rearrange_ex:  theory -> simpset -> term -> thm option
```
```    72   val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
```
```    73   val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
```
```    74   val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option
```
```    75 end;
```
```    76
```
```    77 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
```
```    78 struct
```
```    79
```
```    80 open Data;
```
```    81
```
```    82 (* FIXME: only test! *)
```
```    83 fun def xs eq =
```
```    84   (case dest_eq eq of
```
```    85      SOME(c,s,t) =>
```
```    86        let val n = length xs
```
```    87        in s = Bound n andalso not(loose_bvar1(t,n)) orelse
```
```    88           t = Bound n andalso not(loose_bvar1(s,n)) end
```
```    89    | NONE => false);
```
```    90
```
```    91 fun extract_conj fst xs t = case dest_conj t of NONE => NONE
```
```    92     | SOME(conj,P,Q) =>
```
```    93         (if def xs P then (if fst then NONE else SOME(xs,P,Q)) else
```
```    94          if def xs Q then SOME(xs,Q,P) else
```
```    95          (case extract_conj false xs P of
```
```    96             SOME(xs,eq,P') => SOME(xs,eq, conj \$ P' \$ Q)
```
```    97           | NONE => (case extract_conj false xs Q of
```
```    98                        SOME(xs,eq,Q') => SOME(xs,eq,conj \$ P \$ Q')
```
```    99                      | NONE => NONE)));
```
```   100
```
```   101 fun extract_imp fst xs t = case dest_imp t of NONE => NONE
```
```   102     | SOME(imp,P,Q) => if def xs P then (if fst then NONE else SOME(xs,P,Q))
```
```   103                        else (case extract_conj false xs P of
```
```   104                                SOME(xs,eq,P') => SOME(xs, eq, imp \$ P' \$ Q)
```
```   105                              | NONE => (case extract_imp false xs Q of
```
```   106                                           NONE => NONE
```
```   107                                         | SOME(xs,eq,Q') =>
```
```   108                                             SOME(xs,eq,imp\$P\$Q')));
```
```   109
```
```   110 fun extract_quant extract q =
```
```   111   let fun exqu xs ((qC as Const(qa,_)) \$ Abs(x,T,Q)) =
```
```   112             if qa = q then exqu ((qC,x,T)::xs) Q else NONE
```
```   113         | exqu xs P = extract (null xs) xs P
```
```   114   in exqu [] end;
```
```   115
```
```   116 fun prove_conv tac thy tu =
```
```   117   Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
```
```   118     (K (rtac iff_reflection 1 THEN tac));
```
```   119
```
```   120 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)
```
```   121
```
```   122 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
```
```   123    Better: instantiate exI
```
```   124 *)
```
```   125 local
```
```   126 val excomm = ex_comm RS iff_trans
```
```   127 in
```
```   128 val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN
```
```   129     ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
```
```   130                     DEPTH_SOLVE_1 o (ares_tac [conjI])])
```
```   131 end;
```
```   132
```
```   133 (* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
```
```   134           (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
```
```   135 *)
```
```   136 local
```
```   137 val tac = SELECT_GOAL
```
```   138           (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
```
```   139                   REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
```
```   140 val allcomm = all_comm RS iff_trans
```
```   141 in
```
```   142 val prove_one_point_all_tac =
```
```   143       EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac]
```
```   144 end
```
```   145
```
```   146 fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else
```
```   147                                    if i=u then l else i+1)
```
```   148   | renumber l u (s\$t) = renumber l u s \$ renumber l u t
```
```   149   | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t)
```
```   150   | renumber _ _ atom = atom;
```
```   151
```
```   152 fun quantify qC x T xs P =
```
```   153   let fun quant [] P = P
```
```   154         | quant ((qC,x,T)::xs) P = quant xs (qC \$ Abs(x,T,P))
```
```   155       val n = length xs
```
```   156       val Q = if n=0 then P else renumber 0 n P
```
```   157   in quant xs (qC \$ Abs(x,T,Q)) end;
```
```   158
```
```   159 fun rearrange_all thy _ (F as (all as Const(q,_)) \$ Abs(x,T, P)) =
```
```   160      (case extract_quant extract_imp q P of
```
```   161         NONE => NONE
```
```   162       | SOME(xs,eq,Q) =>
```
```   163           let val R = quantify all x T xs (imp \$ eq \$ Q)
```
```   164           in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
```
```   165   | rearrange_all _ _ _ = NONE;
```
```   166
```
```   167 fun rearrange_ball tac thy ss (F as Ball \$ A \$ Abs(x,T,P)) =
```
```   168      (case extract_imp true [] P of
```
```   169         NONE => NONE
```
```   170       | SOME(xs,eq,Q) => if not(null xs) then NONE else
```
```   171           let val R = imp \$ eq \$ Q
```
```   172           in SOME(prove_conv (tac ss) thy (F,Ball \$ A \$ Abs(x,T,R))) end)
```
```   173   | rearrange_ball _ _ _ _ = NONE;
```
```   174
```
```   175 fun rearrange_ex thy _ (F as (ex as Const(q,_)) \$ Abs(x,T,P)) =
```
```   176      (case extract_quant extract_conj q P of
```
```   177         NONE => NONE
```
```   178       | SOME(xs,eq,Q) =>
```
```   179           let val R = quantify ex x T xs (conj \$ eq \$ Q)
```
```   180           in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
```
```   181   | rearrange_ex _ _ _ = NONE;
```
```   182
```
```   183 fun rearrange_bex tac thy ss (F as Bex \$ A \$ Abs(x,T,P)) =
```
```   184      (case extract_conj true [] P of
```
```   185         NONE => NONE
```
```   186       | SOME(xs,eq,Q) => if not(null xs) then NONE else
```
```   187           SOME(prove_conv (tac ss) thy (F,Bex \$ A \$ Abs(x,T,conj\$eq\$Q))))
```
```   188   | rearrange_bex _ _ _ _ = NONE;
```
```   189
```
```   190 fun rearrange_Coll tac thy _ (F as Coll \$ Abs(x,T,P)) =
```
```   191      (case extract_conj true [] P of
```
```   192         NONE => NONE
```
```   193       | SOME(_,eq,Q) =>
```
```   194           let val R = Coll \$ Abs(x,T, conj \$ eq \$ Q)
```
```   195           in SOME(prove_conv tac thy (F,R)) end);
```
```   196
```
```   197 end;
```