src/Provers/quantifier1.ML
author wenzelm
Sun, 12 Jan 2014 14:32:22 +0100
changeset 54998 8601434fa334
parent 51717 9e7d1c139569
child 58838 59203adfc33f
permissions -rw-r--r--
tuned signature; clarified context;
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
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
    67
  val prove_one_point_all_tac: tactic
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
    68
  val prove_one_point_ex_tac: 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
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   129
        (fn {context = ctxt'', ...} => rtac 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
   130
  in singleton (Variable.export ctxt' ctxt) thm end;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   131
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   132
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   133
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   134
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   135
   Better: instantiate exI
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   136
*)
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   137
local
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   138
  val excomm = Data.ex_comm RS Data.iff_trans;
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   139
in
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   140
  val prove_one_point_ex_tac =
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   141
    qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   142
    ALLGOALS
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   143
      (EVERY' [etac Data.exE, REPEAT_DETERM o etac Data.conjE, rtac Data.exI,
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   144
        DEPTH_SOLVE_1 o ares_tac [Data.conjI]])
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   145
end;
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   146
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   147
(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   148
          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   149
*)
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   150
local
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   151
  val tac =
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   152
    SELECT_GOAL
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   153
      (EVERY1 [REPEAT o dtac Data.uncurry, REPEAT o rtac Data.impI, etac Data.mp,
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   154
        REPEAT o etac Data.conjE, REPEAT o ares_tac [Data.conjI]]);
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   155
  val allcomm = Data.all_comm RS Data.iff_trans;
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   156
in
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   157
  val prove_one_point_all_tac =
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   158
    EVERY1 [qcomm_tac allcomm Data.iff_allI, rtac Data.iff_allI, rtac Data.iffI, tac, tac];
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   159
end
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   160
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   161
fun renumber l u (Bound i) =
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   162
      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
   163
  | renumber l u (s $ t) = renumber l u s $ renumber l u t
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   164
  | 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
   165
  | renumber _ _ atom = atom;
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   166
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   167
fun quantify qC x T xs P =
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   168
  let
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   169
    fun quant [] P = P
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   170
      | quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P));
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   171
    val n = length xs;
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   172
    val Q = if n = 0 then P else renumber 0 n P;
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   173
  in quant xs (qC $ Abs (x, T, Q)) end;
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   174
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   175
fun rearrange_all ctxt ct =
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   176
  (case term_of ct of
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   177
    F as (all as Const (q, _)) $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   178
      (case extract_quant extract_imp q P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   179
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   180
      | SOME (xs, eq, Q) =>
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   181
          let val R = quantify all x T xs (Data.imp $ eq $ Q)
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   182
          in SOME (prove_conv ctxt (F, R) (K prove_one_point_all_tac)) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   183
  | _ => NONE);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   184
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   185
fun rearrange_ball tac ctxt ct =
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   186
  (case term_of ct of
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   187
    F as Ball $ A $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   188
      (case extract_imp true [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   189
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   190
      | SOME (xs, eq, Q) =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   191
          if not (null xs) then NONE
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   192
          else
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   193
            let val R = Data.imp $ eq $ Q
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   194
            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
   195
  | _ => NONE);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   196
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   197
fun rearrange_ex ctxt ct =
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   198
  (case term_of ct of
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   199
    F as (ex as Const (q, _)) $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   200
      (case extract_quant extract_conj q P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   201
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   202
      | SOME (xs, eq, Q) =>
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   203
          let val R = quantify ex x T xs (Data.conj $ eq $ Q)
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   204
          in SOME (prove_conv ctxt (F, R) (K prove_one_point_ex_tac)) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   205
  | _ => NONE);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   206
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   207
fun rearrange_bex tac ctxt ct =
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   208
  (case term_of ct of
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   209
    F as Bex $ A $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   210
      (case extract_conj true [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   211
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   212
      | SOME (xs, eq, Q) =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   213
          if not (null xs) then NONE
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   214
          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
   215
  | _ => NONE);
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   216
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 42460
diff changeset
   217
fun rearrange_Collect tac ctxt ct =
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   218
  (case term_of ct of
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   219
    F as Collect $ Abs (x, T, P) =>
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   220
      (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
   221
        NONE => NONE
42458
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   222
      | SOME (_, eq, Q) =>
5dfae6d348fd misc tuning;
wenzelm
parents: 42457
diff changeset
   223
          let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
54998
8601434fa334 tuned signature;
wenzelm
parents: 51717
diff changeset
   224
          in SOME (prove_conv ctxt (F, R) tac) end)
42459
38b9f023cc34 misc tuning and simplification;
wenzelm
parents: 42458
diff changeset
   225
  | _ => 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
   226
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   227
end;
42460
1805c67dc7aa simplified Data signature;
wenzelm
parents: 42459
diff changeset
   228