src/Provers/quantifier1.ML
author wenzelm
Mon Mar 25 16:45:08 2019 +0100 (3 months ago)
changeset 69980 f2e3adfd916f
parent 60774 6c28d8ed2488
permissions -rw-r--r--
tuned signature;
     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