src/Provers/quantifier1.ML
author wenzelm
Fri, 23 Nov 2018 16:43:11 +0100
changeset 69334 6b49700da068
parent 60774 6c28d8ed2488
child 71512 fe93a863d946
permissions -rw-r--r--
clarified font_domain: strict excludes e.g. space character;
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) *)
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    63
end;
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    64
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    65
signature QUANTIFIER1 =
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    66
sig
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
    67
  val prove_one_point_all_tac: Proof.context -> tactic
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
    68
  val prove_one_point_ex_tac: Proof.context -> tactic
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
    69
  val rearrange_all: Proof.context -> cterm -> thm option
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
    70
  val rearrange_ex: Proof.context -> cterm -> thm option
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
    71
  val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
    72
  val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
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
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   116
fun extract_quant extract q =
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   117
  let
42460
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
   118
    fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) =
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   119
          if qa = q then exqu ((qC, x, T) :: xs) Q else NONE
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   120
      | exqu xs P = extract (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
   121
  in exqu [] end;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   122
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   123
fun prove_conv ctxt tu tac =
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   124
  let
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   125
    val (goal, ctxt') =
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   126
      yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   127
    val thm =
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   128
      Goal.prove ctxt' [] [] goal
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   129
        (fn {context = ctxt'', ...} =>
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   130
          resolve_tac ctxt'' [Data.iff_reflection] 1 THEN tac ctxt'');
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   131
  in singleton (Variable.export ctxt' ctxt) thm end;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   132
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   133
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
   134
  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
   135
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   136
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   137
   Better: instantiate exI
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   138
*)
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   139
local
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   140
  val excomm = Data.ex_comm RS Data.iff_trans;
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   141
in
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   142
  fun prove_one_point_ex_tac ctxt =
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   143
    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
   144
    ALLGOALS
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   145
      (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
   146
        resolve_tac ctxt [Data.exI],
60774
6c28d8ed2488 proper context;
wenzelm
parents: 59582
diff changeset
   147
        DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]])
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   148
end;
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   149
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   150
(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   151
          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   152
*)
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   153
local
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   154
  fun tac ctxt =
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   155
    SELECT_GOAL
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   156
      (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
   157
        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
   158
        eresolve_tac ctxt [Data.mp],
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   159
        REPEAT o eresolve_tac ctxt [Data.conjE],
60774
6c28d8ed2488 proper context;
wenzelm
parents: 59582
diff changeset
   160
        REPEAT o ares_tac ctxt [Data.conjI]]);
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   161
  val allcomm = Data.all_comm RS Data.iff_trans;
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   162
in
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   163
  fun prove_one_point_all_tac ctxt =
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   164
    EVERY1 [qcomm_tac ctxt allcomm Data.iff_allI,
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   165
      resolve_tac ctxt [Data.iff_allI],
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   166
      resolve_tac ctxt [Data.iffI], tac ctxt, tac ctxt];
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   167
end
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   168
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   169
fun renumber l u (Bound i) =
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   170
      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
   171
  | renumber l u (s $ t) = renumber l u s $ renumber l u t
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   172
  | 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
   173
  | renumber _ _ atom = atom;
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   174
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   175
fun quantify qC x T xs P =
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   176
  let
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   177
    fun quant [] P = P
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   178
      | quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P));
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   179
    val n = length xs;
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   180
    val Q = if n = 0 then P else renumber 0 n P;
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   181
  in quant xs (qC $ Abs (x, T, Q)) end;
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   182
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   183
fun rearrange_all ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   184
  (case Thm.term_of ct of
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   185
    F as (all as Const (q, _)) $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   186
      (case extract_quant extract_imp q P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   187
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   188
      | SOME (xs, eq, Q) =>
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   189
          let val R = quantify all x T xs (Data.imp $ eq $ Q)
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   190
          in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   191
  | _ => NONE);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   192
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   193
fun rearrange_ball tac ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   194
  (case Thm.term_of ct of
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   195
    F as Ball $ A $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   196
      (case extract_imp true [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   197
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   198
      | SOME (xs, eq, Q) =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   199
          if not (null xs) then NONE
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   200
          else
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   201
            let val R = Data.imp $ eq $ Q
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   202
            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   203
  | _ => NONE);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   204
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   205
fun rearrange_ex ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   206
  (case Thm.term_of ct of
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   207
    F as (ex as Const (q, _)) $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   208
      (case extract_quant extract_conj q P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   209
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   210
      | SOME (xs, eq, Q) =>
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   211
          let val R = quantify ex x T xs (Data.conj $ eq $ Q)
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58838
diff changeset
   212
          in SOME (prove_conv ctxt (F, R) prove_one_point_ex_tac) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   213
  | _ => NONE);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   214
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   215
fun rearrange_bex tac ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   216
  (case Thm.term_of ct of
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   217
    F as Bex $ A $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   218
      (case extract_conj true [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   219
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   220
      | SOME (xs, eq, Q) =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   221
          if not (null xs) then NONE
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   222
          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac))
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   223
  | _ => NONE);
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   224
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   225
fun rearrange_Collect tac ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   226
  (case Thm.term_of ct of
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   227
    F as Collect $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   228
      (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
   229
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   230
      | SOME (_, eq, Q) =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   231
          let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   232
          in SOME (prove_conv ctxt (F, R) tac) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   233
  | _ => 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
   234
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   235
end;
42460
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
   236