src/Provers/quantifier1.ML
 author haftmann Mon Feb 06 20:56:34 2017 +0100 (2017-02-06) changeset 64990 c6a7de505796 parent 60774 6c28d8ed2488 permissions -rw-r--r--
more explicit errors in pathological cases
```     1 (*  Title:      Provers/quantifier1.ML
```
```     2     Author:     Tobias Nipkow
```
```     3     Copyright   1997  TU Munich
```
```     4
```
```     5 Simplification procedures for turning
```
```     6
```
```     7             ? x. ... & x = t & ...
```
```     8      into   ? x. x = t & ... & ...
```
```     9      where the `? x. x = t &' in the latter formula must be eliminated
```
```    10            by ordinary simplification.
```
```    11
```
```    12      and   ! x. (... & x = t & ...) --> P x
```
```    13      into  ! x. x = t --> (... & ...) --> P x
```
```    14      where the `!x. x=t -->' in the latter formula is eliminated
```
```    15            by ordinary simplification.
```
```    16
```
```    17      And analogously for t=x, but the eqn is not turned around!
```
```    18
```
```    19      NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
```
```    20         "!x. x=t --> P(x)" is covered by the congruence rule for -->;
```
```    21         "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
```
```    22         As must be "? x. t=x & P(x)".
```
```    23
```
```    24      And similarly for the bounded quantifiers.
```
```    25
```
```    26 Gries etc call this the "1 point rules"
```
```    27
```
```    28 The above also works for !x1..xn. and ?x1..xn by moving the defined
```
```    29 quantifier inside first, but not for nested bounded quantifiers.
```
```    30
```
```    31 For set comprehensions the basic permutations
```
```    32       ... & x = t & ...  ->  x = t & (... & ...)
```
```    33       ... & t = x & ...  ->  t = x & (... & ...)
```
```    34 are also exported.
```
```    35
```
```    36 To avoid looping, NONE is returned if the term cannot be rearranged,
```
```    37 esp if x=t/t=x sits at the front already.
```
```    38 *)
```
```    39
```
```    40 signature QUANTIFIER1_DATA =
```
```    41 sig
```
```    42   (*abstract syntax*)
```
```    43   val dest_eq: term -> (term * term) option
```
```    44   val dest_conj: term -> (term * term) option
```
```    45   val dest_imp: term -> (term * term) option
```
```    46   val conj: term
```
```    47   val imp: term
```
```    48   (*rules*)
```
```    49   val iff_reflection: thm (* P <-> Q ==> P == Q *)
```
```    50   val iffI: thm
```
```    51   val iff_trans: thm
```
```    52   val conjI: thm
```
```    53   val conjE: thm
```
```    54   val impI: thm
```
```    55   val mp: thm
```
```    56   val exI: thm
```
```    57   val exE: thm
```
```    58   val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
```
```    59   val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
```
```    60   val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
```
```    61   val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
```
```    62   val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
```
```    63 end;
```
```    64
```
```    65 signature QUANTIFIER1 =
```
```    66 sig
```
```    67   val prove_one_point_all_tac: Proof.context -> tactic
```
```    68   val prove_one_point_ex_tac: Proof.context -> tactic
```
```    69   val rearrange_all: Proof.context -> cterm -> thm option
```
```    70   val rearrange_ex: Proof.context -> cterm -> thm option
```
```    71   val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
```
```    72   val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
```
```    73   val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
```
```    74 end;
```
```    75
```
```    76 functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
```
```    77 struct
```
```    78
```
```    79 (* FIXME: only test! *)
```
```    80 fun def xs eq =
```
```    81   (case Data.dest_eq eq of
```
```    82     SOME (s, t) =>
```
```    83       let val n = length xs in
```
```    84         s = Bound n andalso not (loose_bvar1 (t, n)) orelse
```
```    85         t = Bound n andalso not (loose_bvar1 (s, n))
```
```    86       end
```
```    87   | NONE => false);
```
```    88
```
```    89 fun extract_conj fst xs t =
```
```    90   (case Data.dest_conj t of
```
```    91     NONE => NONE
```
```    92   | SOME (P, Q) =>
```
```    93       if def xs P then (if fst then NONE else SOME (xs, P, Q))
```
```    94       else if def xs Q then SOME (xs, Q, P)
```
```    95       else
```
```    96         (case extract_conj false xs P of
```
```    97           SOME (xs, eq, P') => SOME (xs, eq, Data.conj \$ P' \$ Q)
```
```    98         | NONE =>
```
```    99             (case extract_conj false xs Q of
```
```   100               SOME (xs, eq, Q') => SOME (xs, eq, Data.conj \$ P \$ Q')
```
```   101             | NONE => NONE)));
```
```   102
```
```   103 fun extract_imp fst xs t =
```
```   104   (case Data.dest_imp t of
```
```   105     NONE => NONE
```
```   106   | SOME (P, Q) =>
```
```   107       if def xs P then (if fst then NONE else SOME (xs, P, Q))
```
```   108       else
```
```   109         (case extract_conj false xs P of
```
```   110           SOME (xs, eq, P') => SOME (xs, eq, Data.imp \$ P' \$ Q)
```
```   111         | NONE =>
```
```   112             (case extract_imp false xs Q of
```
```   113               NONE => NONE
```
```   114             | SOME (xs, eq, Q') => SOME (xs, eq, Data.imp \$ P \$ Q'))));
```
```   115
```
```   116 fun extract_quant extract q =
```
```   117   let
```
```   118     fun exqu xs ((qC as Const (qa, _)) \$ Abs (x, T, Q)) =
```
```   119           if qa = q then exqu ((qC, x, T) :: xs) Q else NONE
```
```   120       | exqu xs P = extract (null xs) xs P
```
```   121   in exqu [] end;
```
```   122
```
```   123 fun prove_conv ctxt tu tac =
```
```   124   let
```
```   125     val (goal, ctxt') =
```
```   126       yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
```
```   127     val thm =
```
```   128       Goal.prove ctxt' [] [] goal
```
```   129         (fn {context = ctxt'', ...} =>
```
```   130           resolve_tac ctxt'' [Data.iff_reflection] 1 THEN tac ctxt'');
```
```   131   in singleton (Variable.export ctxt' ctxt) thm end;
```
```   132
```
```   133 fun qcomm_tac ctxt qcomm qI i =
```
```   134   REPEAT_DETERM (resolve_tac ctxt [qcomm] i THEN resolve_tac ctxt [qI] i);
```
```   135
```
```   136 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
```
```   137    Better: instantiate exI
```
```   138 *)
```
```   139 local
```
```   140   val excomm = Data.ex_comm RS Data.iff_trans;
```
```   141 in
```
```   142   fun prove_one_point_ex_tac ctxt =
```
```   143     qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN
```
```   144     ALLGOALS
```
```   145       (EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE],
```
```   146         resolve_tac ctxt [Data.exI],
```
```   147         DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]])
```
```   148 end;
```
```   149
```
```   150 (* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
```
```   151           (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
```
```   152 *)
```
```   153 local
```
```   154   fun tac ctxt =
```
```   155     SELECT_GOAL
```
```   156       (EVERY1 [REPEAT o dresolve_tac ctxt [Data.uncurry],
```
```   157         REPEAT o resolve_tac ctxt [Data.impI],
```
```   158         eresolve_tac ctxt [Data.mp],
```
```   159         REPEAT o eresolve_tac ctxt [Data.conjE],
```
```   160         REPEAT o ares_tac ctxt [Data.conjI]]);
```
```   161   val allcomm = Data.all_comm RS Data.iff_trans;
```
```   162 in
```
```   163   fun prove_one_point_all_tac ctxt =
```
```   164     EVERY1 [qcomm_tac ctxt allcomm Data.iff_allI,
```
```   165       resolve_tac ctxt [Data.iff_allI],
```
```   166       resolve_tac ctxt [Data.iffI], tac ctxt, tac ctxt];
```
```   167 end
```
```   168
```
```   169 fun renumber l u (Bound i) =
```
```   170       Bound (if i < l orelse i > u then i else if i = u then l else i + 1)
```
```   171   | renumber l u (s \$ t) = renumber l u s \$ renumber l u t
```
```   172   | renumber l u (Abs (x, T, t)) = Abs (x, T, renumber (l + 1) (u + 1) t)
```
```   173   | renumber _ _ atom = atom;
```
```   174
```
```   175 fun quantify qC x T xs P =
```
```   176   let
```
```   177     fun quant [] P = P
```
```   178       | quant ((qC, x, T) :: xs) P = quant xs (qC \$ Abs (x, T, P));
```
```   179     val n = length xs;
```
```   180     val Q = if n = 0 then P else renumber 0 n P;
```
```   181   in quant xs (qC \$ Abs (x, T, Q)) end;
```
```   182
```
```   183 fun rearrange_all ctxt ct =
```
```   184   (case Thm.term_of ct of
```
```   185     F as (all as Const (q, _)) \$ Abs (x, T, P) =>
```
```   186       (case extract_quant extract_imp q P of
```
```   187         NONE => NONE
```
```   188       | SOME (xs, eq, Q) =>
```
```   189           let val R = quantify all x T xs (Data.imp \$ eq \$ Q)
```
```   190           in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end)
```
```   191   | _ => NONE);
```
```   192
```
```   193 fun rearrange_ball tac ctxt ct =
```
```   194   (case Thm.term_of ct of
```
```   195     F as Ball \$ A \$ Abs (x, T, P) =>
```
```   196       (case extract_imp true [] P of
```
```   197         NONE => NONE
```
```   198       | SOME (xs, eq, Q) =>
```
```   199           if not (null xs) then NONE
```
```   200           else
```
```   201             let val R = Data.imp \$ eq \$ Q
```
```   202             in SOME (prove_conv ctxt (F, Ball \$ A \$ Abs (x, T, R)) tac) end)
```
```   203   | _ => NONE);
```
```   204
```
```   205 fun rearrange_ex ctxt ct =
```
```   206   (case Thm.term_of ct of
```
```   207     F as (ex as Const (q, _)) \$ Abs (x, T, P) =>
```
```   208       (case extract_quant extract_conj q P of
```
```   209         NONE => NONE
```
```   210       | SOME (xs, eq, Q) =>
```
```   211           let val R = quantify ex x T xs (Data.conj \$ eq \$ Q)
```
```   212           in SOME (prove_conv ctxt (F, R) prove_one_point_ex_tac) end)
```
```   213   | _ => NONE);
```
```   214
```
```   215 fun rearrange_bex tac ctxt ct =
```
```   216   (case Thm.term_of ct of
```
```   217     F as Bex \$ A \$ Abs (x, T, P) =>
```
```   218       (case extract_conj true [] P of
```
```   219         NONE => NONE
```
```   220       | SOME (xs, eq, Q) =>
```
```   221           if not (null xs) then NONE
```
```   222           else SOME (prove_conv ctxt (F, Bex \$ A \$ Abs (x, T, Data.conj \$ eq \$ Q)) tac))
```
```   223   | _ => NONE);
```
```   224
```
```   225 fun rearrange_Collect tac ctxt ct =
```
```   226   (case Thm.term_of ct of
```
```   227     F as Collect \$ Abs (x, T, P) =>
```
```   228       (case extract_conj true [] P of
```
```   229         NONE => NONE
```
```   230       | SOME (_, eq, Q) =>
```
```   231           let val R = Collect \$ Abs (x, T, Data.conj \$ eq \$ Q)
```
```   232           in SOME (prove_conv ctxt (F, R) tac) end)
```
```   233   | _ => NONE);
```
```   234
```
```   235 end;
```
```   236
```