src/Provers/hypsubst.ML
author nipkow
Fri May 17 11:25:07 2002 +0200 (2002-05-17 ago)
changeset 13157 4a4599f78f18
parent 12377 c1e3e7d3f469
child 13604 57bfacbbaeda
permissions -rw-r--r--
allowed more general split rules to cope with div/mod 2
wenzelm@9532
     1
(*  Title:      Provers/hypsubst.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@9532
     3
    Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
lcp@1011
     4
    Copyright   1995  University of Cambridge
lcp@1011
     5
wenzelm@9628
     6
Basic equational reasoning: (hyp_)subst method and symmetric attribute.
wenzelm@9628
     7
wenzelm@9628
     8
Tactic to substitute using (at least) the assumption x=t in the rest
wenzelm@9628
     9
of the subgoal, and to delete (at least) that assumption.  Original
wenzelm@9628
    10
version due to Martin Coen.
lcp@1011
    11
lcp@1011
    12
This version uses the simplifier, and requires it to be already present.
lcp@1011
    13
lcp@1011
    14
Test data:
clasohm@0
    15
wenzelm@9532
    16
Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
wenzelm@9532
    17
Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
wenzelm@9532
    18
Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
wenzelm@9532
    19
Goal "!!z. [| ?x=y; P(?x) |] ==> y = a";
lcp@1011
    20
lcp@1011
    21
by (hyp_subst_tac 1);
lcp@1011
    22
by (bound_hyp_subst_tac 1);
lcp@1011
    23
lcp@1011
    24
Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
wenzelm@9532
    25
Goal "P(a) --> (EX y. a=y --> P(f(a)))";
paulson@4466
    26
wenzelm@9532
    27
Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
paulson@4466
    28
\                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
paulson@4466
    29
by (blast_hyp_subst_tac (ref true) 1);
clasohm@0
    30
*)
clasohm@0
    31
clasohm@0
    32
signature HYPSUBST_DATA =
clasohm@0
    33
  sig
lcp@1011
    34
  structure Simplifier : SIMPLIFIER
paulson@4466
    35
  val dest_Trueprop    : term -> term
wenzelm@9532
    36
  val dest_eq          : term -> term*term*typ
wenzelm@9532
    37
  val dest_imp         : term -> term*term
wenzelm@9532
    38
  val eq_reflection    : thm               (* a=b ==> a==b *)
wenzelm@9532
    39
  val rev_eq_reflection: thm               (* a==b ==> a=b *)
wenzelm@9532
    40
  val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
wenzelm@9532
    41
  val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
wenzelm@9532
    42
  val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
wenzelm@9532
    43
  val sym              : thm               (* a=b ==> b=a *)
oheimb@4223
    44
  val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
paulson@4466
    45
  end;
clasohm@0
    46
lcp@1011
    47
clasohm@0
    48
signature HYPSUBST =
clasohm@0
    49
  sig
lcp@1011
    50
  val bound_hyp_subst_tac    : int -> tactic
lcp@1011
    51
  val hyp_subst_tac          : int -> tactic
paulson@4466
    52
  val blast_hyp_subst_tac    : bool ref -> int -> tactic
clasohm@0
    53
    (*exported purely for debugging purposes*)
lcp@1011
    54
  val gen_hyp_subst_tac      : bool -> int -> tactic
lcp@1011
    55
  val vars_gen_hyp_subst_tac : bool -> int -> tactic
lcp@1011
    56
  val eq_var                 : bool -> bool -> term -> int * bool
paulson@4179
    57
  val inspect_pair           : bool -> bool -> term * term * typ -> bool
lcp@1011
    58
  val mk_eqs                 : thm -> thm list
lcp@1011
    59
  val thin_leading_eqs_tac   : bool -> int -> int -> tactic
wenzelm@9532
    60
  val stac		     : thm -> int -> tactic
wenzelm@9532
    61
  val hypsubst_setup         : (theory -> theory) list
clasohm@0
    62
  end;
clasohm@0
    63
paulson@2722
    64
paulson@2722
    65
wenzelm@9532
    66
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
clasohm@0
    67
struct
clasohm@0
    68
clasohm@0
    69
exception EQ_VAR;
clasohm@0
    70
paulson@2174
    71
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
clasohm@0
    72
lcp@1011
    73
local val odot = ord"."
lcp@1011
    74
in
wenzelm@9532
    75
(*Simplifier turns Bound variables to dotted Free variables:
lcp@1011
    76
  change it back (any Bound variable will do)
lcp@1011
    77
*)
lcp@1011
    78
fun contract t =
paulson@2722
    79
    case Pattern.eta_contract_atom t of
wenzelm@9532
    80
        Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
lcp@1011
    81
      | t'        => t'
lcp@1011
    82
end;
lcp@1011
    83
lcp@1011
    84
fun has_vars t = maxidx_of_term t <> ~1;
lcp@1011
    85
lcp@1011
    86
(*If novars then we forbid Vars in the equality.
wenzelm@9532
    87
  If bnd then we only look for Bound (or dotted Free) variables to eliminate.
lcp@1011
    88
  When can we safely delete the equality?
lcp@1011
    89
    Not if it equates two constants; consider 0=1.
lcp@1011
    90
    Not if it resembles x=t[x], since substitution does not eliminate x.
paulson@4299
    91
    Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
wenzelm@9532
    92
    Not if it involves a variable free in the premises,
lcp@1011
    93
        but we can't check for this -- hence bnd and bound_hyp_subst_tac
lcp@1011
    94
  Prefer to eliminate Bound variables if possible.
lcp@1011
    95
  Result:  true = use as is,  false = reorient first *)
paulson@4179
    96
fun inspect_pair bnd novars (t,u,T) =
wenzelm@9532
    97
  if novars andalso maxidx_of_typ T <> ~1
paulson@4179
    98
  then raise Match   (*variables in the type!*)
paulson@4179
    99
  else
lcp@1011
   100
  case (contract t, contract u) of
wenzelm@9532
   101
       (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
wenzelm@9532
   102
                       then raise Match
wenzelm@9532
   103
                       else true                (*eliminates t*)
wenzelm@9532
   104
     | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
wenzelm@9532
   105
                       then raise Match
wenzelm@9532
   106
                       else false               (*eliminates u*)
wenzelm@9532
   107
     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
wenzelm@9532
   108
                          novars andalso has_vars u
wenzelm@9532
   109
                       then raise Match
wenzelm@9532
   110
                       else true                (*eliminates t*)
wenzelm@9532
   111
     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
wenzelm@9532
   112
                          novars andalso has_vars t
wenzelm@9532
   113
                       then raise Match
wenzelm@9532
   114
                       else false               (*eliminates u*)
clasohm@0
   115
     | _ => raise Match;
clasohm@0
   116
lcp@680
   117
(*Locates a substitutable variable on the left (resp. right) of an equality
lcp@1011
   118
   assumption.  Returns the number of intervening assumptions. *)
lcp@1011
   119
fun eq_var bnd novars =
lcp@680
   120
  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
wenzelm@9532
   121
        | eq_var_aux k (Const("==>",_) $ A $ B) =
wenzelm@9532
   122
              ((k, inspect_pair bnd novars
wenzelm@9532
   123
                    (Data.dest_eq (Data.dest_Trueprop A)))
wenzelm@9532
   124
                      (*Exception comes from inspect_pair or dest_eq*)
wenzelm@9532
   125
               handle _ => eq_var_aux (k+1) B)
wenzelm@9532
   126
        | eq_var_aux k _ = raise EQ_VAR
lcp@680
   127
  in  eq_var_aux 0  end;
clasohm@0
   128
lcp@1011
   129
(*We do not try to delete ALL equality assumptions at once.  But
lcp@1011
   130
  it is easy to handle several consecutive equality assumptions in a row.
lcp@1011
   131
  Note that we have to inspect the proof state after doing the rewriting,
lcp@1011
   132
  since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
lcp@1011
   133
  must NOT be deleted.  Tactic must rotate or delete m assumptions.
lcp@1011
   134
*)
paulson@3537
   135
fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
lcp@1011
   136
    let fun count []      = 0
wenzelm@9532
   137
          | count (A::Bs) = ((inspect_pair bnd true
wenzelm@9532
   138
                              (Data.dest_eq (Data.dest_Trueprop A));
wenzelm@9532
   139
                              1 + count Bs)
paulson@4466
   140
                             handle _ => 0)
paulson@2143
   141
        val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
paulson@2722
   142
    in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
lcp@1011
   143
    end);
lcp@1011
   144
lcp@1011
   145
(*For the simpset.  Adds ALL suitable equalities, even if not first!
lcp@1011
   146
  No vars are allowed here, as simpsets are built from meta-assumptions*)
wenzelm@9532
   147
fun mk_eqs th =
wenzelm@9532
   148
    [ if inspect_pair false false (Data.dest_eq
wenzelm@9532
   149
                                   (Data.dest_Trueprop (#prop (rep_thm th))))
lcp@1011
   150
      then th RS Data.eq_reflection
wenzelm@9532
   151
      else symmetric(th RS Data.eq_reflection) (*reorient*) ]
paulson@4466
   152
    handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)
lcp@1011
   153
wenzelm@9532
   154
local open Simplifier
lcp@1011
   155
in
lcp@1011
   156
lcp@1011
   157
  val hyp_subst_ss = empty_ss setmksimps mk_eqs
lcp@1011
   158
lcp@1011
   159
  (*Select a suitable equality assumption and substitute throughout the subgoal
lcp@1011
   160
    Replaces only Bound variables if bnd is true*)
paulson@3537
   161
  fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
wenzelm@9532
   162
        let val n = length(Logic.strip_assums_hyp Bi) - 1
wenzelm@9532
   163
            val (k,_) = eq_var bnd true Bi
wenzelm@9532
   164
        in
wenzelm@9532
   165
           DETERM (EVERY [rotate_tac k i,
wenzelm@9532
   166
                          asm_full_simp_tac hyp_subst_ss i,
wenzelm@9532
   167
                          etac thin_rl i,
wenzelm@9532
   168
                          thin_leading_eqs_tac bnd (n-k) i])
wenzelm@9532
   169
        end
wenzelm@9532
   170
        handle THM _ => no_tac | EQ_VAR => no_tac);
lcp@1011
   171
lcp@1011
   172
end;
lcp@1011
   173
paulson@4466
   174
val ssubst = standard (Data.sym RS Data.subst);
paulson@4466
   175
paulson@4466
   176
val imp_intr_tac = rtac Data.imp_intr;
lcp@1011
   177
lcp@1011
   178
(*Old version of the tactic above -- slower but the only way
lcp@1011
   179
  to handle equalities containing Vars.*)
paulson@3537
   180
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
paulson@3537
   181
      let val n = length(Logic.strip_assums_hyp Bi) - 1
wenzelm@9532
   182
          val (k,symopt) = eq_var bnd false Bi
wenzelm@9532
   183
      in
wenzelm@9532
   184
         DETERM
paulson@4466
   185
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
wenzelm@9532
   186
                   rotate_tac 1 i,
wenzelm@9532
   187
                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
wenzelm@9532
   188
                   etac (if symopt then ssubst else Data.subst) i,
wenzelm@9532
   189
                   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
clasohm@0
   190
      end
paulson@3537
   191
      handle THM _ => no_tac | EQ_VAR => no_tac);
clasohm@0
   192
clasohm@0
   193
(*Substitutes for Free or Bound variables*)
paulson@4466
   194
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
oheimb@4223
   195
        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
clasohm@0
   196
clasohm@0
   197
(*Substitutes for Bound variables only -- this is always safe*)
wenzelm@9532
   198
val bound_hyp_subst_tac =
lcp@1011
   199
    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
clasohm@0
   200
paulson@4466
   201
wenzelm@9532
   202
(** Version for Blast_tac.  Hyps that are affected by the substitution are
paulson@4466
   203
    moved to the front.  Defect: even trivial changes are noticed, such as
paulson@4466
   204
    substitutions in the arguments of a function Var. **)
paulson@4466
   205
paulson@4466
   206
(*final re-reversal of the changed assumptions*)
paulson@4466
   207
fun reverse_n_tac 0 i = all_tac
paulson@4466
   208
  | reverse_n_tac 1 i = rotate_tac ~1 i
wenzelm@9532
   209
  | reverse_n_tac n i =
paulson@4466
   210
      REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
paulson@4466
   211
      REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
paulson@4466
   212
paulson@4466
   213
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
wenzelm@9532
   214
fun all_imp_intr_tac hyps i =
paulson@4466
   215
  let fun imptac (r, [])    st = reverse_n_tac r i st
wenzelm@9532
   216
        | imptac (r, hyp::hyps) st =
wenzelm@9532
   217
           let val (hyp',_) = List.nth (prems_of st, i-1) |>
wenzelm@9532
   218
                              Logic.strip_assums_concl    |>
wenzelm@9532
   219
                              Data.dest_Trueprop          |> Data.dest_imp
wenzelm@9532
   220
               val (r',tac) = if Pattern.aeconv (hyp,hyp')
wenzelm@9532
   221
                              then (r, imp_intr_tac i THEN rotate_tac ~1 i)
wenzelm@9532
   222
                              else (*leave affected hyps at end*)
wenzelm@9532
   223
                                   (r+1, imp_intr_tac i)
wenzelm@9532
   224
           in
wenzelm@9532
   225
               case Seq.pull(tac st) of
wenzelm@9532
   226
                   None       => Seq.single(st)
wenzelm@9532
   227
                 | Some(st',_) => imptac (r',hyps) st'
wenzelm@9532
   228
           end handle _ => error "?? in blast_hyp_subst_tac"
paulson@4466
   229
  in  imptac (0, rev hyps)  end;
paulson@4466
   230
paulson@4466
   231
paulson@4466
   232
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
paulson@4466
   233
      let val (k,symopt) = eq_var false false Bi
wenzelm@9532
   234
          val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
paulson@4466
   235
          (*omit selected equality, returning other hyps*)
wenzelm@9532
   236
          val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
wenzelm@9532
   237
          val n = length hyps
wenzelm@9532
   238
      in
wenzelm@12262
   239
         if !trace then tracing "Substituting an equality" else ();
wenzelm@9532
   240
         DETERM
paulson@4466
   241
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
wenzelm@9532
   242
                   rotate_tac 1 i,
wenzelm@9532
   243
                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
wenzelm@9532
   244
                   etac (if symopt then ssubst else Data.subst) i,
wenzelm@9532
   245
                   all_imp_intr_tac hyps i])
paulson@4466
   246
      end
paulson@4466
   247
      handle THM _ => no_tac | EQ_VAR => no_tac);
paulson@4466
   248
wenzelm@9532
   249
wenzelm@9532
   250
(*apply an equality or definition ONCE;
wenzelm@9532
   251
  fails unless the substitution has an effect*)
wenzelm@9532
   252
fun stac th =
wenzelm@9532
   253
  let val th' = th RS Data.rev_eq_reflection handle THM _ => th
wenzelm@9532
   254
  in CHANGED_GOAL (rtac (th' RS ssubst)) end;
wenzelm@9532
   255
wenzelm@9532
   256
wenzelm@9628
   257
(* proof methods *)
wenzelm@9532
   258
wenzelm@9705
   259
val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac);
wenzelm@10821
   260
val hyp_subst_meth =
wenzelm@10821
   261
  Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
wenzelm@9532
   262
wenzelm@9628
   263
wenzelm@9628
   264
(* theory setup *)
wenzelm@9628
   265
wenzelm@9532
   266
val hypsubst_setup =
wenzelm@9532
   267
 [Method.add_methods
wenzelm@9628
   268
  [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
wenzelm@12377
   269
   ("subst", subst_meth, "substitution")]];
wenzelm@9532
   270
clasohm@0
   271
end;