src/Provers/quantifier1.ML
author nipkow
Mon Dec 17 14:21:59 2001 +0100 (2001-12-17)
changeset 12523 0d8d5bf549b0
parent 11232 558a4feebb04
child 13480 bb72bd43c6c3
permissions -rw-r--r--
now permutations of quantifiers are allowed as well.
nipkow@4319
     1
(*  Title:      Provers/quantifier1
nipkow@4319
     2
    ID:         $Id$
nipkow@4319
     3
    Author:     Tobias Nipkow
nipkow@4319
     4
    Copyright   1997  TU Munich
nipkow@4319
     5
nipkow@4319
     6
Simplification procedures for turning
nipkow@4319
     7
nipkow@4319
     8
            ? x. ... & x = t & ...
nipkow@4319
     9
     into   ? x. x = t & ... & ...
nipkow@11232
    10
     where the `? x. x = t &' in the latter formula must be eliminated
nipkow@4319
    11
           by ordinary simplification. 
nipkow@4319
    12
nipkow@4319
    13
     and   ! x. (... & x = t & ...) --> P x
nipkow@4319
    14
     into  ! x. x = t --> (... & ...) --> P x
nipkow@4319
    15
     where the `!x. x=t -->' in the latter formula is eliminated
nipkow@4319
    16
           by ordinary simplification.
nipkow@4319
    17
nipkow@11232
    18
     And analogously for t=x, but the eqn is not turned around!
nipkow@11232
    19
nipkow@4319
    20
     NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
nipkow@4319
    21
        "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
nipkow@4319
    22
        "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
nipkow@11232
    23
        As must be "? x. t=x & P(x)".
nipkow@4319
    24
nipkow@11232
    25
        
nipkow@11221
    26
     And similarly for the bounded quantifiers.
nipkow@11221
    27
nipkow@4319
    28
Gries etc call this the "1 point rules"
nipkow@4319
    29
*)
nipkow@4319
    30
nipkow@4319
    31
signature QUANTIFIER1_DATA =
nipkow@4319
    32
sig
nipkow@4319
    33
  (*abstract syntax*)
nipkow@4319
    34
  val dest_eq: term -> (term*term*term)option
nipkow@4319
    35
  val dest_conj: term -> (term*term*term)option
nipkow@11232
    36
  val dest_imp:  term -> (term*term*term)option
nipkow@4319
    37
  val conj: term
nipkow@4319
    38
  val imp:  term
nipkow@4319
    39
  (*rules*)
nipkow@4319
    40
  val iff_reflection: thm (* P <-> Q ==> P == Q *)
nipkow@4319
    41
  val iffI:  thm
nipkow@12523
    42
  val iff_trans: thm
nipkow@4319
    43
  val conjI: thm
nipkow@4319
    44
  val conjE: thm
nipkow@4319
    45
  val impI:  thm
nipkow@4319
    46
  val mp:    thm
nipkow@4319
    47
  val exI:   thm
nipkow@4319
    48
  val exE:   thm
nipkow@11232
    49
  val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
nipkow@11232
    50
  val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
nipkow@12523
    51
  val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
nipkow@12523
    52
  val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
nipkow@12523
    53
  val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
nipkow@4319
    54
end;
nipkow@4319
    55
nipkow@4319
    56
signature QUANTIFIER1 =
nipkow@4319
    57
sig
nipkow@11221
    58
  val prove_one_point_all_tac: tactic
nipkow@11221
    59
  val prove_one_point_ex_tac: tactic
nipkow@4319
    60
  val rearrange_all: Sign.sg -> thm list -> term -> thm option
nipkow@4319
    61
  val rearrange_ex:  Sign.sg -> thm list -> term -> thm option
nipkow@11221
    62
  val rearrange_ball: tactic -> Sign.sg -> thm list -> term -> thm option
nipkow@11221
    63
  val rearrange_bex:  tactic -> Sign.sg -> thm list -> term -> thm option
nipkow@4319
    64
end;
nipkow@4319
    65
nipkow@4319
    66
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
nipkow@4319
    67
struct
nipkow@4319
    68
nipkow@4319
    69
open Data;
nipkow@4319
    70
nipkow@11232
    71
(* FIXME: only test! *)
nipkow@12523
    72
fun def xs eq =
nipkow@12523
    73
  let val n = length xs
nipkow@12523
    74
  in case dest_eq eq of
nipkow@4319
    75
      Some(c,s,t) =>
nipkow@12523
    76
        s = Bound n andalso not(loose_bvar1(t,n)) orelse
nipkow@12523
    77
        t = Bound n andalso not(loose_bvar1(s,n))
nipkow@12523
    78
    | None => false
nipkow@12523
    79
  end;
nipkow@4319
    80
nipkow@12523
    81
fun extract_conj xs t = case dest_conj t of None => None
nipkow@11232
    82
    | Some(conj,P,Q) =>
nipkow@12523
    83
        (if def xs P then Some(xs,P,Q) else
nipkow@12523
    84
         if def xs Q then Some(xs,Q,P) else
nipkow@12523
    85
         (case extract_conj xs P of
nipkow@12523
    86
            Some(xs,eq,P') => Some(xs,eq, conj $ P' $ Q)
nipkow@12523
    87
          | None => (case extract_conj xs Q of
nipkow@12523
    88
                       Some(xs,eq,Q') => Some(xs,eq,conj $ P $ Q')
nipkow@11232
    89
                     | None => None)));
nipkow@11232
    90
nipkow@12523
    91
fun extract_imp xs t = case dest_imp t of None => None
nipkow@12523
    92
    | Some(imp,P,Q) => if def xs P then Some(xs,P,Q)
nipkow@12523
    93
                       else (case extract_conj xs P of
nipkow@12523
    94
                               Some(xs,eq,P') => Some(xs, eq, imp $ P' $ Q)
nipkow@12523
    95
                             | None => (case extract_imp xs Q of
nipkow@11232
    96
                                          None => None
nipkow@12523
    97
                                        | Some(xs,eq,Q') =>
nipkow@12523
    98
                                            Some(xs,eq,imp$P$Q')));
nipkow@12523
    99
nipkow@12523
   100
fun extract_quant extract q =
nipkow@12523
   101
  let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) =
nipkow@12523
   102
            if qa = q then exqu ((qC,x,T)::xs) Q else None
nipkow@12523
   103
        | exqu xs P = extract xs P
nipkow@12523
   104
  in exqu end;
nipkow@4319
   105
nipkow@4319
   106
fun prove_conv tac sg tu =
nipkow@4319
   107
  let val meta_eq = cterm_of sg (Logic.mk_equals tu)
nipkow@4319
   108
  in prove_goalw_cterm [] meta_eq (K [rtac iff_reflection 1, tac])
nipkow@4319
   109
     handle ERROR =>
nipkow@4319
   110
            error("The error(s) above occurred while trying to prove " ^
nipkow@4319
   111
                  string_of_cterm meta_eq)
nipkow@4319
   112
  end;
nipkow@4319
   113
nipkow@12523
   114
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
nipkow@12523
   115
nipkow@12523
   116
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
nipkow@11221
   117
   Better: instantiate exI
nipkow@11221
   118
*)
nipkow@12523
   119
local
nipkow@12523
   120
val excomm = ex_comm RS iff_trans
nipkow@12523
   121
in
nipkow@12523
   122
val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN
nipkow@11221
   123
    ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
nipkow@12523
   124
                    DEPTH_SOLVE_1 o (ares_tac [conjI])])
nipkow@12523
   125
end;
nipkow@11221
   126
nipkow@12523
   127
(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
nipkow@12523
   128
          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
nipkow@11221
   129
*)
nipkow@11232
   130
local
nipkow@11232
   131
val tac = SELECT_GOAL
nipkow@11232
   132
          (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
nipkow@11232
   133
                  REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
nipkow@12523
   134
val allcomm = all_comm RS iff_trans
nipkow@11232
   135
in
nipkow@12523
   136
val prove_one_point_all_tac =
nipkow@12523
   137
      EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac]
nipkow@11232
   138
end
nipkow@4319
   139
nipkow@12523
   140
fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else
nipkow@12523
   141
                                   if i=u then l else i+1)
nipkow@12523
   142
  | renumber l u (s$t) = renumber l u s $ renumber l u t
nipkow@12523
   143
  | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t)
nipkow@12523
   144
  | renumber _ _ atom = atom;
nipkow@12523
   145
nipkow@12523
   146
fun quantify qC x T xs P =
nipkow@12523
   147
  let fun quant [] P = P
nipkow@12523
   148
        | quant ((qC,x,T)::xs) P = quant xs (qC $ Abs(x,T,P))
nipkow@12523
   149
      val n = length xs
nipkow@12523
   150
      val Q = if n=0 then P else renumber 0 n P
nipkow@12523
   151
  in quant xs (qC $ Abs(x,T,Q)) end;
nipkow@12523
   152
nipkow@12523
   153
fun rearrange_all sg _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
nipkow@12523
   154
     (case extract_quant extract_imp q [] P of
nipkow@4319
   155
        None => None
nipkow@12523
   156
      | Some(xs,eq,Q) =>
nipkow@12523
   157
          let val R = quantify all x T xs (imp $ eq $ Q)
nipkow@12523
   158
          in Some(prove_conv prove_one_point_all_tac sg (F,R)) end)
nipkow@4319
   159
  | rearrange_all _ _ _ = None;
nipkow@4319
   160
nipkow@11232
   161
fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
nipkow@12523
   162
     (case extract_imp [] P of
nipkow@11221
   163
        None => None
nipkow@12523
   164
      | Some(xs,eq,Q) => if not(null xs) then None else
nipkow@11232
   165
          let val R = imp $ eq $ Q
nipkow@11221
   166
          in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
nipkow@11221
   167
  | rearrange_ball _ _ _ _ = None;
nipkow@4319
   168
nipkow@12523
   169
fun rearrange_ex sg _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
nipkow@12523
   170
     (case extract_quant extract_conj q [] P of
nipkow@4319
   171
        None => None
nipkow@12523
   172
      | Some(xs,eq,Q) =>
nipkow@12523
   173
          let val R = quantify ex x T xs (conj $ eq $ Q)
nipkow@12523
   174
          in Some(prove_conv prove_one_point_ex_tac sg (F,R)) end)
nipkow@4319
   175
  | rearrange_ex _ _ _ = None;
nipkow@4319
   176
nipkow@11221
   177
fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
nipkow@12523
   178
     (case extract_conj [] P of
nipkow@11221
   179
        None => None
nipkow@12523
   180
      | Some(xs,eq,Q) => if not(null xs) then None else
nipkow@11221
   181
          Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
nipkow@11221
   182
  | rearrange_bex _ _ _ _ = None;
nipkow@11221
   183
nipkow@4319
   184
end;