src/Provers/quantifier1.ML
author wenzelm
Fri, 22 Apr 2011 14:38:49 +0200
changeset 42457 de868abd131e
parent 42456 13b4b6ba3593
child 42458 5dfae6d348fd
permissions -rw-r--r--
do not open ML structures;
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
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    10
           by ordinary simplification. 
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)".
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
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*)
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    43
  val dest_eq: term -> (term*term*term)option
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    44
  val dest_conj: term -> (term*term*term)option
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    45
  val dest_imp:  term -> (term*term*term)option
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    46
  val conj: term
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    47
  val imp:  term
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 *)
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
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
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    54
  val impI:  thm
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    55
  val mp:    thm
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    56
  val exI:   thm
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
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
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
    69
  val rearrange_all: simpset -> term -> thm option
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
    70
  val rearrange_ex: simpset -> term -> thm option
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
    71
  val rearrange_ball: tactic -> simpset -> term -> thm option
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
    72
  val rearrange_bex: tactic -> simpset -> term -> thm option
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
    73
  val rearrange_Collect: tactic -> simpset -> term -> thm option
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    74
end;
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    75
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    76
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
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
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
    82
     SOME(c,s,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
    83
       let val n = length xs
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
    84
       in s = Bound n andalso not(loose_bvar1(t,n)) orelse
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
    85
          t = Bound n andalso not(loose_bvar1(s,n)) end
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
    86
   | NONE => false);
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    87
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
    88
fun extract_conj fst xs t = case Data.dest_conj t of NONE => NONE
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    89
    | SOME(conj,P,Q) =>
31197
c1c163ec6c44 fine-tuned elimination of comprehensions involving x=t.
nipkow
parents: 31166
diff changeset
    90
        (if def xs P then (if fst then NONE else SOME(xs,P,Q)) else
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    91
         if def xs Q then SOME(xs,Q,P) else
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
    92
         (case extract_conj false xs P of
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
    93
            SOME(xs,eq,P') => SOME(xs,eq, Data.conj $ P' $ Q)
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
    94
          | NONE => (case extract_conj false xs Q of
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
    95
                       SOME(xs,eq,Q') => SOME(xs,eq,Data.conj $ P $ Q')
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    96
                     | NONE => NONE)));
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    97
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
    98
fun extract_imp fst xs t = case Data.dest_imp t of NONE => NONE
31197
c1c163ec6c44 fine-tuned elimination of comprehensions involving x=t.
nipkow
parents: 31166
diff changeset
    99
    | SOME(imp,P,Q) => if def xs P then (if fst then NONE else SOME(xs,P,Q))
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
   100
                       else (case extract_conj false xs P of
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   101
                               SOME(xs,eq,P') => SOME(xs, eq, Data.imp $ P' $ Q)
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
   102
                             | NONE => (case extract_imp false xs Q of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   103
                                          NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   104
                                        | SOME(xs,eq,Q') =>
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   105
                                            SOME(xs,eq,Data.imp$P$Q')));
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   106
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   107
fun extract_quant extract q =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   108
  let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   109
            if qa = q then exqu ((qC,x,T)::xs) Q else 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
   110
        | exqu xs P = extract (null xs) xs P
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
   111
  in exqu [] end;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   112
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   113
fun prove_conv tac ss tu =
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   114
  let
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   115
    val ctxt = Simplifier.the_context ss;
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   116
    val (goal, ctxt') =
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   117
      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
   118
    val thm =
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   119
      Goal.prove ctxt' [] [] goal (K (rtac Data.iff_reflection 1 THEN tac));
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   120
  in singleton (Variable.export ctxt' ctxt) thm end;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   121
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   122
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   123
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   124
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   125
   Better: instantiate exI
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   126
*)
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   127
local
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   128
val excomm = Data.ex_comm RS Data.iff_trans
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   129
in
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   130
val prove_one_point_ex_tac = qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   131
    ALLGOALS(EVERY'[etac Data.exE, REPEAT_DETERM o (etac Data.conjE), rtac Data.exI,
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   132
                    DEPTH_SOLVE_1 o (ares_tac [Data.conjI])])
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   133
end;
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   134
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   135
(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   136
          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   137
*)
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   138
local
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   139
val tac = SELECT_GOAL
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   140
          (EVERY1[REPEAT o (dtac Data.uncurry), REPEAT o (rtac Data.impI), etac Data.mp,
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   141
                  REPEAT o (etac Data.conjE), REPEAT o (ares_tac [Data.conjI])])
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   142
val allcomm = Data.all_comm RS Data.iff_trans
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   143
in
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   144
val prove_one_point_all_tac =
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   145
      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
   146
end
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   147
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   148
fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   149
                                   if i=u then l else i+1)
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   150
  | renumber l u (s$t) = renumber l u s $ renumber l u t
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   151
  | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t)
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   152
  | renumber _ _ atom = atom;
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
fun quantify qC x T xs P =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   155
  let fun quant [] P = P
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   156
        | quant ((qC,x,T)::xs) P = quant xs (qC $ Abs(x,T,P))
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   157
      val n = length xs
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   158
      val Q = if n=0 then P else renumber 0 n P
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   159
  in quant xs (qC $ Abs(x,T,Q)) end;
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   160
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   161
fun rearrange_all ss (F as (all as Const(q,_)) $ Abs(x,T, 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
   162
     (case extract_quant extract_imp q P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   163
        NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   164
      | SOME(xs,eq,Q) =>
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   165
          let val R = quantify all x T xs (Data.imp $ eq $ Q)
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   166
          in SOME (prove_conv prove_one_point_all_tac ss (F,R)) end)
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   167
  | rearrange_all _ _ = NONE;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   168
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   169
fun rearrange_ball tac ss (F as Ball $ A $ Abs(x,T,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
   170
     (case extract_imp true [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   171
        NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   172
      | SOME(xs,eq,Q) => if not(null xs) then NONE else
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   173
          let val R = Data.imp $ eq $ Q
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   174
          in SOME (prove_conv tac ss (F,Ball $ A $ Abs(x,T,R))) end)
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   175
  | rearrange_ball _ _ _ = NONE;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   176
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   177
fun rearrange_ex ss (F as (ex as Const(q,_)) $ Abs(x,T,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
   178
     (case extract_quant extract_conj q P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   179
        NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   180
      | SOME(xs,eq,Q) =>
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   181
          let val R = quantify ex x T xs (Data.conj $ eq $ Q)
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   182
          in SOME(prove_conv prove_one_point_ex_tac ss (F,R)) end)
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   183
  | rearrange_ex _ _ = NONE;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   184
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   185
fun rearrange_bex tac ss (F as Bex $ A $ Abs(x,T,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
   186
     (case extract_conj true [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   187
        NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   188
      | SOME(xs,eq,Q) => if not(null xs) then NONE else
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   189
          SOME(prove_conv tac ss (F,Bex $ A $ Abs(x,T,Data.conj$eq$Q))))
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   190
  | rearrange_bex _ _ _ = NONE;
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   191
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   192
fun rearrange_Collect tac ss (F as Coll $ Abs(x,T,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
   193
     (case extract_conj true [] P of
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
   194
        NONE => NONE
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
   195
      | SOME(_,eq,Q) =>
42457
de868abd131e do not open ML structures;
wenzelm
parents: 42456
diff changeset
   196
          let val R = Coll $ Abs(x,T, Data.conj $ eq $ Q)
42456
13b4b6ba3593 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents: 42361
diff changeset
   197
          in SOME(prove_conv tac ss (F,R)) end);
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
   198
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   199
end;