src/Provers/quantifier1.ML
author wenzelm
Sun, 13 Dec 2020 23:11:41 +0100
changeset 72907 3883f536d84d
parent 71916 435cdc772110
permissions -rw-r--r--
unused (see 29566b6810f7);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35762
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 31197
diff changeset
     1
(*  Title:      Provers/quantifier1.ML
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     2
    Author:     Tobias Nipkow
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     3
    Copyright   1997  TU Munich
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     4
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     5
Simplification procedures for turning
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     6
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     7
            ? x. ... & x = t & ...
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     8
     into   ? x. x = t & ... & ...
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
     9
     where the `? x. x = t &' in the latter formula must be eliminated
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    10
           by ordinary simplification.
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    11
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    12
     and   ! x. (... & x = t & ...) --> P x
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    13
     into  ! x. x = t --> (... & ...) --> P x
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    14
     where the `!x. x=t -->' in the latter formula is eliminated
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    15
           by ordinary simplification.
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    16
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    17
     And analogously for t=x, but the eqn is not turned around!
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    18
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    19
     NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
38456
6769ccd90ad6 typos in comment
blanchet
parents: 36610
diff changeset
    20
        "!x. x=t --> P(x)" is covered by the congruence rule for -->;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    21
        "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    22
        As must be "? x. t=x & P(x)".
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    23
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
    24
     And similarly for the bounded quantifiers.
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
    25
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    26
Gries etc call this the "1 point rules"
31166
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
    27
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
    28
The above also works for !x1..xn. and ?x1..xn by moving the defined
38456
6769ccd90ad6 typos in comment
blanchet
parents: 36610
diff changeset
    29
quantifier inside first, but not for nested bounded quantifiers.
31166
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
    30
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
    31
For set comprehensions the basic permutations
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
    32
      ... & x = t & ...  ->  x = t & (... & ...)
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
    33
      ... & t = x & ...  ->  t = x & (... & ...)
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
    34
are also exported.
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
    35
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
    36
To avoid looping, NONE is returned if the term cannot be rearranged,
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
    37
esp if x=t/t=x sits at the front already.
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    38
*)
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    39
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    40
signature QUANTIFIER1_DATA =
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    41
sig
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    42
  (*abstract syntax*)
42460
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
    43
  val dest_eq: term -> (term * term) option
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
    44
  val dest_conj: term -> (term * term) option
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
    45
  val dest_imp: term -> (term * term) option
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    46
  val conj: term
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    47
  val imp: term
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    48
  (*rules*)
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    49
  val iff_reflection: thm (* P <-> Q ==> P == Q *)
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    50
  val iffI: thm
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    51
  val iff_trans: thm
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    52
  val conjI: thm
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    53
  val conjE: thm
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    54
  val impI: thm
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    55
  val mp: thm
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    56
  val exI: thm
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    57
  val exE: thm
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    58
  val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    59
  val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    60
  val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    61
  val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    62
  val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
71916
435cdc772110 specific atomization inert to later rule set modifications
haftmann
parents: 71915
diff changeset
    63
  val atomize: Proof.context -> conv
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    64
end;
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    65
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    66
signature QUANTIFIER1 =
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    67
sig
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
    68
  val rearrange_all: Proof.context -> cterm -> thm option
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
    69
  val rearrange_All: Proof.context -> cterm -> thm option
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
    70
  val rearrange_Ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
    71
  val rearrange_Ex: Proof.context -> cterm -> thm option
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
    72
  val rearrange_Bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
    73
  val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    74
end;
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    75
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    76
functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    77
struct
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    78
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    79
(* FIXME: only test! *)
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    80
fun def xs eq =
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
    81
  (case Data.dest_eq eq of
42460
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
    82
    SOME (s, t) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    83
      let val n = length xs in
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    84
        s = Bound n andalso not (loose_bvar1 (t, n)) orelse
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    85
        t = Bound n andalso not (loose_bvar1 (s, n))
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    86
      end
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    87
  | NONE => false);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    88
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    89
fun extract_conj fst xs t =
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    90
  (case Data.dest_conj t of
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    91
    NONE => NONE
42460
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
    92
  | SOME (P, Q) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    93
      if def xs P then (if fst then NONE else SOME (xs, P, Q))
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    94
      else if def xs Q then SOME (xs, Q, P)
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    95
      else
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    96
        (case extract_conj false xs P of
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    97
          SOME (xs, eq, P') => SOME (xs, eq, Data.conj $ P' $ Q)
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    98
        | NONE =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
    99
            (case extract_conj false xs Q of
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   100
              SOME (xs, eq, Q') => SOME (xs, eq, Data.conj $ P $ Q')
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   101
            | NONE => NONE)));
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   102
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   103
fun extract_imp fst xs t =
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   104
  (case Data.dest_imp t of
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   105
    NONE => NONE
42460
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
   106
  | SOME (P, Q) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   107
      if def xs P then (if fst then NONE else SOME (xs, P, Q))
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   108
      else
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   109
        (case extract_conj false xs P of
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   110
          SOME (xs, eq, P') => SOME (xs, eq, Data.imp $ P' $ Q)
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   111
        | NONE =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   112
            (case extract_imp false xs Q of
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   113
              NONE => NONE
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   114
            | SOME (xs, eq, Q') => SOME (xs, eq, Data.imp $ P $ Q'))));
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   115
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   116
fun extract_conj_from_judgment ctxt fst xs t =
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   117
  if Object_Logic.is_judgment ctxt t
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   118
  then
71773
7c2f4dd48fb6 more robust judgment handling
haftmann
parents: 71512
diff changeset
   119
    let
7c2f4dd48fb6 more robust judgment handling
haftmann
parents: 71512
diff changeset
   120
      val judg $ t' = t
7c2f4dd48fb6 more robust judgment handling
haftmann
parents: 71512
diff changeset
   121
    in
7c2f4dd48fb6 more robust judgment handling
haftmann
parents: 71512
diff changeset
   122
      case extract_conj fst xs t' of
7c2f4dd48fb6 more robust judgment handling
haftmann
parents: 71512
diff changeset
   123
          NONE => NONE
7c2f4dd48fb6 more robust judgment handling
haftmann
parents: 71512
diff changeset
   124
        | SOME (xs, eq, P) => SOME (xs, judg $ eq, judg $ P)
7c2f4dd48fb6 more robust judgment handling
haftmann
parents: 71512
diff changeset
   125
    end
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   126
  else NONE;
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   127
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   128
fun extract_implies ctxt fst xs t =
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   129
  (case try Logic.dest_implies t of
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   130
    NONE => NONE
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   131
  | SOME (P, Q) =>
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   132
      if def xs P then (if fst then NONE else SOME (xs, P, Q))
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   133
      else
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   134
        (case extract_conj_from_judgment ctxt false xs P of
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   135
          SOME (xs, eq, P') => SOME (xs, eq, Logic.implies $ P' $ Q)
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   136
        | NONE =>
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   137
            (case extract_implies ctxt false xs Q of
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   138
              NONE => NONE
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   139
            | SOME (xs, eq, Q') => (SOME (xs, eq, Logic.implies $ P $ Q')))));
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   140
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   141
fun extract_quant ctxt extract q =
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   142
  let
42460
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
   143
    fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) =
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   144
          if qa = q then exqu ((qC, x, T) :: xs) Q else NONE
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   145
      | exqu xs P = extract ctxt (null xs) xs P
31166
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
   146
  in exqu [] end;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   147
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   148
fun iff_reflection_tac ctxt =
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   149
  resolve_tac ctxt [Data.iff_reflection] 1;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   150
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   151
fun qcomm_tac ctxt qcomm qI i =
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   152
  REPEAT_DETERM (resolve_tac ctxt [qcomm] i THEN resolve_tac ctxt [qI] i);
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   153
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   154
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   155
   Better: instantiate exI
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   156
*)
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   157
local
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   158
  val excomm = Data.ex_comm RS Data.iff_trans;
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   159
in
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   160
  fun prove_one_point_Ex_tac ctxt =
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   161
    qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   162
    ALLGOALS
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   163
      (EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE],
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   164
        resolve_tac ctxt [Data.exI],
60774
6c28d8ed2488 proper context;
wenzelm
parents: 59582
diff changeset
   165
        DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]])
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   166
end;
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   167
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   168
(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   169
          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   170
*)
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   171
local
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   172
  fun tac ctxt =
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   173
    SELECT_GOAL
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   174
      (EVERY1 [REPEAT o dresolve_tac ctxt [Data.uncurry],
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   175
        REPEAT o resolve_tac ctxt [Data.impI],
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   176
        eresolve_tac ctxt [Data.mp],
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   177
        REPEAT o eresolve_tac ctxt [Data.conjE],
60774
6c28d8ed2488 proper context;
wenzelm
parents: 59582
diff changeset
   178
        REPEAT o ares_tac ctxt [Data.conjI]]);
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   179
  val all_comm = Data.all_comm RS Data.iff_trans;
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   180
  val All_comm = @{thm swap_params [THEN transitive]};
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   181
in
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   182
  fun prove_one_point_All_tac ctxt =
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   183
    EVERY1 [qcomm_tac ctxt all_comm Data.iff_allI,
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   184
      resolve_tac ctxt [Data.iff_allI],
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   185
      resolve_tac ctxt [Data.iffI],
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   186
      tac ctxt,
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   187
      tac ctxt];
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   188
  fun prove_one_point_all_tac ctxt =
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   189
    EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI},
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   190
      resolve_tac ctxt [@{thm equal_allI}],
71916
435cdc772110 specific atomization inert to later rule set modifications
haftmann
parents: 71915
diff changeset
   191
      CONVERSION (Data.atomize ctxt),
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   192
      resolve_tac ctxt [@{thm equal_intr_rule}],
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   193
      tac ctxt,
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   194
      tac ctxt];
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   195
end
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   196
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   197
fun prove_conv ctxt tu tac =
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   198
  let
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   199
    val (goal, ctxt') =
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   200
      yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   201
    val thm =
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   202
      Goal.prove ctxt' [] [] goal
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   203
        (fn {context = ctxt'', ...} => tac ctxt'');
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   204
  in singleton (Variable.export ctxt' ctxt) thm end;
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   205
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   206
fun renumber l u (Bound i) =
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   207
      Bound (if i < l orelse i > u then i else if i = u then l else i + 1)
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   208
  | renumber l u (s $ t) = renumber l u s $ renumber l u t
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   209
  | renumber l u (Abs (x, T, t)) = Abs (x, T, renumber (l + 1) (u + 1) t)
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   210
  | renumber _ _ atom = atom;
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   211
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   212
fun quantify qC x T xs P =
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   213
  let
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   214
    fun quant [] P = P
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   215
      | quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P));
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   216
    val n = length xs;
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   217
    val Q = if n = 0 then P else renumber 0 n P;
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   218
  in quant xs (qC $ Abs (x, T, Q)) end;
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   219
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   220
fun rearrange_all ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   221
  (case Thm.term_of ct of
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   222
    F as (all as Const (q, _)) $ Abs (x, T, P) =>
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   223
      (case extract_quant ctxt extract_implies q P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   224
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   225
      | SOME (xs, eq, Q) =>
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   226
          let val R = quantify all x T xs (Logic.implies $ eq $ Q)
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   227
            in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end)
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   228
  | _ => NONE);
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   229
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   230
fun rearrange_All ctxt ct =
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   231
  (case Thm.term_of ct of
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   232
    F as (all as Const (q, _)) $ Abs (x, T, P) =>
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   233
      (case extract_quant ctxt (K extract_imp) q P of
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   234
        NONE => NONE
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   235
      | SOME (xs, eq, Q) =>
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   236
          let val R = quantify all x T xs (Data.imp $ eq $ Q)
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   237
          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_All_tac)) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   238
  | _ => NONE);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   239
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   240
fun rearrange_Ball tac ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   241
  (case Thm.term_of ct of
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   242
    F as Ball $ A $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   243
      (case extract_imp true [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   244
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   245
      | SOME (xs, eq, Q) =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   246
          if not (null xs) then NONE
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   247
          else
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   248
            let val R = Data.imp $ eq $ Q
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   249
            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R))
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   250
              (iff_reflection_tac THEN' tac THEN' prove_one_point_All_tac)) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   251
  | _ => NONE);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   252
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   253
fun rearrange_Ex ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   254
  (case Thm.term_of ct of
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   255
    F as (ex as Const (q, _)) $ Abs (x, T, P) =>
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   256
      (case extract_quant ctxt (K extract_conj) q P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   257
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   258
      | SOME (xs, eq, Q) =>
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   259
          let val R = quantify ex x T xs (Data.conj $ eq $ Q)
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   260
          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_Ex_tac)) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   261
  | _ => NONE);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   262
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   263
fun rearrange_Bex tac ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   264
  (case Thm.term_of ct of
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   265
    F as Bex $ A $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   266
      (case extract_conj true [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   267
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   268
      | SOME (xs, eq, Q) =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   269
          if not (null xs) then NONE
71886
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   270
          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))
4f4695757980 better closeup and more consistent terminology
haftmann
parents: 71773
diff changeset
   271
            (iff_reflection_tac THEN' tac THEN' prove_one_point_Ex_tac)))
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   272
  | _ => NONE);
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   273
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   274
fun rearrange_Collect tac ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   275
  (case Thm.term_of ct of
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   276
    F as Collect $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   277
      (case extract_conj true [] P of
31166
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
   278
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   279
      | SOME (_, eq, Q) =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   280
          let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
71512
fe93a863d946 infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents: 60774
diff changeset
   281
          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' tac)) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   282
  | _ => NONE);
31166
a90fe83f58ea "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents: 20049
diff changeset
   283
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   284
end;
42460
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
   285