src/Provers/quantifier1.ML
author wenzelm
Sun, 11 Jan 2009 21:49:59 +0100
changeset 29450 ac7f67be7f1f
parent 20049 f48c4a3a34bc
child 31166 a90fe83f58ea
permissions -rw-r--r--
tuned categories;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     1
(*  Title:      Provers/quantifier1
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     4
    Copyright   1997  TU Munich
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     5
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     6
Simplification procedures for turning
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     7
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     8
            ? x. ... & x = t & ...
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
     9
     into   ? x. x = t & ... & ...
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    10
     where the `? x. x = t &' in the latter formula must be eliminated
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    11
           by ordinary simplification. 
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    12
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    13
     and   ! x. (... & x = t & ...) --> P x
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    14
     into  ! x. x = t --> (... & ...) --> P x
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    15
     where the `!x. x=t -->' in the latter formula is eliminated
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    16
           by ordinary simplification.
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    17
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    18
     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
    19
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    20
     NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    21
        "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    22
        "!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
    23
        As must be "? x. t=x & P(x)".
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    24
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    25
        
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
    26
     And similarly for the bounded quantifiers.
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
    27
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    28
Gries etc call this the "1 point rules"
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    29
*)
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    30
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    31
signature QUANTIFIER1_DATA =
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    32
sig
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    33
  (*abstract syntax*)
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    34
  val dest_eq: term -> (term*term*term)option
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    35
  val dest_conj: term -> (term*term*term)option
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    36
  val dest_imp:  term -> (term*term*term)option
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    37
  val conj: term
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    38
  val imp:  term
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    39
  (*rules*)
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    40
  val iff_reflection: thm (* P <-> Q ==> P == Q *)
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    41
  val iffI:  thm
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    42
  val iff_trans: thm
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    43
  val conjI: thm
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    44
  val conjE: thm
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    45
  val impI:  thm
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    46
  val mp:    thm
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    47
  val exI:   thm
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    48
  val exE:   thm
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    49
  val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    50
  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
    51
  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
    52
  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
    53
  val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    54
end;
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    55
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    56
signature QUANTIFIER1 =
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    57
sig
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
    58
  val prove_one_point_all_tac: tactic
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
    59
  val prove_one_point_ex_tac: tactic
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    60
  val rearrange_all: theory -> simpset -> term -> thm option
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    61
  val rearrange_ex:  theory -> simpset -> term -> thm option
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    62
  val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
    63
  val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
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
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    67
struct
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    68
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    69
open Data;
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    70
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    71
(* FIXME: only test! *)
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    72
fun def xs eq =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    73
  let val n = length xs
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    74
  in case dest_eq eq of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    75
      SOME(c,s,t) =>
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    76
        s = Bound n andalso not(loose_bvar1(t,n)) orelse
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    77
        t = Bound n andalso not(loose_bvar1(s,n))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    78
    | NONE => false
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    79
  end;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
    80
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    81
fun extract_conj xs t = case dest_conj t of NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    82
    | SOME(conj,P,Q) =>
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    83
        (if def xs P then SOME(xs,P,Q) else
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    84
         if def xs Q then SOME(xs,Q,P) else
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    85
         (case extract_conj xs P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    86
            SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    87
          | NONE => (case extract_conj xs Q of
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    88
                       SOME(xs,eq,Q') => SOME(xs,eq,conj $ P $ Q')
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    89
                     | NONE => NONE)));
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
    90
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    91
fun extract_imp xs t = case dest_imp t of NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    92
    | SOME(imp,P,Q) => if def xs P then SOME(xs,P,Q)
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    93
                       else (case extract_conj xs P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    94
                               SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    95
                             | NONE => (case extract_imp xs Q of
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    96
                                          NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    97
                                        | SOME(xs,eq,Q') =>
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    98
                                            SOME(xs,eq,imp$P$Q')));
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
    99
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   100
fun extract_quant extract q =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   101
  let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   102
            if qa = q then exqu ((qC,x,T)::xs) Q else NONE
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   103
        | exqu xs P = extract xs P
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   104
  in exqu end;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   105
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
   106
fun prove_conv tac thy tu =
20049
f48c4a3a34bc Goal.prove: context;
wenzelm
parents: 17956
diff changeset
   107
  Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
f48c4a3a34bc Goal.prove: context;
wenzelm
parents: 17956
diff changeset
   108
    (K (rtac iff_reflection 1 THEN tac));
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   109
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   110
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
   111
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   112
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   113
   Better: instantiate exI
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   114
*)
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   115
local
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   116
val excomm = ex_comm RS iff_trans
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   117
in
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   118
val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   119
    ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   120
                    DEPTH_SOLVE_1 o (ares_tac [conjI])])
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   121
end;
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   122
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   123
(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   124
          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   125
*)
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   126
local
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   127
val tac = SELECT_GOAL
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   128
          (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   129
                  REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   130
val allcomm = all_comm RS iff_trans
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   131
in
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   132
val prove_one_point_all_tac =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   133
      EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac]
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   134
end
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   135
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   136
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
   137
                                   if i=u then l else i+1)
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   138
  | 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
   139
  | 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
   140
  | renumber _ _ atom = atom;
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   141
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   142
fun quantify qC x T xs P =
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   143
  let fun quant [] P = P
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   144
        | 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
   145
      val n = length xs
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   146
      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
   147
  in quant xs (qC $ Abs(x,T,Q)) end;
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   148
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
   149
fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   150
     (case extract_quant extract_imp q [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   151
        NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   152
      | SOME(xs,eq,Q) =>
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   153
          let val R = quantify all x T xs (imp $ eq $ Q)
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
   154
          in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   155
  | rearrange_all _ _ _ = NONE;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   156
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
   157
fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) =
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   158
     (case extract_imp [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   159
        NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   160
      | SOME(xs,eq,Q) => if not(null xs) then NONE else
11232
558a4feebb04 generalization of 1 point rules for ALL
nipkow
parents: 11221
diff changeset
   161
          let val R = imp $ eq $ Q
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
   162
          in SOME(prove_conv (tac ss) thy (F,Ball $ A $ Abs(x,T,R))) end)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   163
  | rearrange_ball _ _ _ _ = NONE;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   164
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
   165
fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   166
     (case extract_quant extract_conj q [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   167
        NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   168
      | SOME(xs,eq,Q) =>
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   169
          let val R = quantify ex x T xs (conj $ eq $ Q)
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
   170
          in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   171
  | rearrange_ex _ _ _ = NONE;
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   172
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
   173
fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) =
12523
0d8d5bf549b0 now permutations of quantifiers are allowed as well.
nipkow
parents: 11232
diff changeset
   174
     (case extract_conj [] P of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   175
        NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   176
      | SOME(xs,eq,Q) => if not(null xs) then NONE else
17002
fb9261990ffe simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15531
diff changeset
   177
          SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
   178
  | rearrange_bex _ _ _ _ = NONE;
11221
60c6e91f6079 added simproc for bounded quantifiers
nipkow
parents: 7951
diff changeset
   179
4319
afb60b8bf15e Quantifier elimination procs.
nipkow
parents:
diff changeset
   180
end;