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