src/Provers/hypsubst.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 36945 9bec62c10714
child 39297 4f9e933a16e2
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
wenzelm@9532
     1
(*  Title:      Provers/hypsubst.ML
wenzelm@9532
     2
    Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
lcp@1011
     3
    Copyright   1995  University of Cambridge
lcp@1011
     4
wenzelm@15662
     5
Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "subst".
wenzelm@9628
     6
wenzelm@9628
     7
Tactic to substitute using (at least) the assumption x=t in the rest
wenzelm@9628
     8
of the subgoal, and to delete (at least) that assumption.  Original
wenzelm@9628
     9
version due to Martin Coen.
lcp@1011
    10
lcp@1011
    11
This version uses the simplifier, and requires it to be already present.
lcp@1011
    12
lcp@1011
    13
Test data:
clasohm@0
    14
wenzelm@9532
    15
Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
wenzelm@9532
    16
Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
wenzelm@9532
    17
Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
wenzelm@9532
    18
Goal "!!z. [| ?x=y; P(?x) |] ==> y = a";
lcp@1011
    19
paulson@15415
    20
Goal "!!x a. [| x = f(b); g(a) = b |] ==> P(x)";
paulson@15415
    21
paulson@15415
    22
by (bound_hyp_subst_tac 1);
lcp@1011
    23
by (hyp_subst_tac 1);
lcp@1011
    24
lcp@1011
    25
Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
wenzelm@9532
    26
Goal "P(a) --> (EX y. a=y --> P(f(a)))";
paulson@4466
    27
wenzelm@9532
    28
Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
paulson@4466
    29
\                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
wenzelm@23908
    30
by (blast_hyp_subst_tac true 1);
clasohm@0
    31
*)
clasohm@0
    32
clasohm@0
    33
signature HYPSUBST_DATA =
wenzelm@21221
    34
sig
paulson@4466
    35
  val dest_Trueprop    : term -> term
wenzelm@21221
    36
  val dest_eq          : term -> term * term
haftmann@20974
    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 *)
krauss@27572
    45
  val prop_subst       : thm               (* PROP P t ==> PROP prop (x = t ==> PROP P x) *)
wenzelm@21221
    46
end;
lcp@1011
    47
clasohm@0
    48
signature HYPSUBST =
wenzelm@21221
    49
sig
krauss@27572
    50
  val single_hyp_subst_tac   : int -> int -> tactic
krauss@27572
    51
  val single_hyp_meta_subst_tac : int -> int -> tactic
lcp@1011
    52
  val bound_hyp_subst_tac    : int -> tactic
lcp@1011
    53
  val hyp_subst_tac          : int -> tactic
wenzelm@23908
    54
  val blast_hyp_subst_tac    : bool -> int -> tactic
haftmann@20945
    55
  val stac                   : thm -> int -> tactic
wenzelm@18708
    56
  val hypsubst_setup         : theory -> theory
wenzelm@21221
    57
end;
paulson@2722
    58
wenzelm@9532
    59
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
clasohm@0
    60
struct
clasohm@0
    61
clasohm@0
    62
exception EQ_VAR;
clasohm@0
    63
wenzelm@27734
    64
val meta_subst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x \<equiv> t \<Longrightarrow> PROP P x)"
krauss@27572
    65
  by (unfold prop_def)}
krauss@27572
    66
krauss@27572
    67
(** Simple version: Just subtitute one hypothesis, specified by index k **)
krauss@27572
    68
fun gen_single_hyp_subst_tac subst_rule k = CSUBGOAL (fn (csubg, i) =>
krauss@27572
    69
 let 
krauss@27572
    70
   val pat = fold_rev (Logic.all o Free) (Logic.strip_params (term_of csubg)) (Term.dummy_pattern propT)
krauss@27572
    71
             |> cterm_of (theory_of_cterm csubg)
krauss@27572
    72
krauss@27572
    73
   val rule =
krauss@27572
    74
       Thm.lift_rule pat subst_rule (* lift just over parameters *)
krauss@27572
    75
       |> Conv.fconv_rule (MetaSimplifier.rewrite true [@{thm prop_def}])
krauss@27572
    76
 in
krauss@27572
    77
   rotate_tac k i
krauss@27572
    78
   THEN Thm.compose_no_flatten false (rule, 1) i
krauss@27572
    79
   THEN rotate_tac (~k) i
krauss@27572
    80
 end)
krauss@27572
    81
krauss@27572
    82
val single_hyp_meta_subst_tac = gen_single_hyp_subst_tac meta_subst
krauss@27572
    83
val single_hyp_subst_tac = gen_single_hyp_subst_tac Data.prop_subst
krauss@27572
    84
wenzelm@17896
    85
fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
clasohm@0
    86
wenzelm@16979
    87
(*Simplifier turns Bound variables to special Free variables:
wenzelm@16979
    88
  change it back (any Bound variable will do)*)
lcp@1011
    89
fun contract t =
berghofe@26833
    90
  (case Envir.eta_contract t of
wenzelm@20074
    91
    Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
wenzelm@16979
    92
  | t' => t');
lcp@1011
    93
wenzelm@21221
    94
val has_vars = Term.exists_subterm Term.is_Var;
wenzelm@21221
    95
val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar);
lcp@1011
    96
lcp@1011
    97
(*If novars then we forbid Vars in the equality.
wenzelm@16979
    98
  If bnd then we only look for Bound variables to eliminate.
lcp@1011
    99
  When can we safely delete the equality?
lcp@1011
   100
    Not if it equates two constants; consider 0=1.
lcp@1011
   101
    Not if it resembles x=t[x], since substitution does not eliminate x.
paulson@4299
   102
    Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
wenzelm@9532
   103
    Not if it involves a variable free in the premises,
lcp@1011
   104
        but we can't check for this -- hence bnd and bound_hyp_subst_tac
lcp@1011
   105
  Prefer to eliminate Bound variables if possible.
lcp@1011
   106
  Result:  true = use as is,  false = reorient first *)
wenzelm@21221
   107
fun inspect_pair bnd novars (t, u) =
wenzelm@21221
   108
  if novars andalso (has_tvars t orelse has_tvars u)
paulson@4179
   109
  then raise Match   (*variables in the type!*)
paulson@4179
   110
  else
lcp@1011
   111
  case (contract t, contract u) of
wenzelm@9532
   112
       (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
wenzelm@9532
   113
                       then raise Match
wenzelm@9532
   114
                       else true                (*eliminates t*)
wenzelm@9532
   115
     | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
wenzelm@9532
   116
                       then raise Match
wenzelm@9532
   117
                       else false               (*eliminates u*)
wenzelm@9532
   118
     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
wenzelm@9532
   119
                          novars andalso has_vars u
wenzelm@9532
   120
                       then raise Match
wenzelm@9532
   121
                       else true                (*eliminates t*)
wenzelm@9532
   122
     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
wenzelm@9532
   123
                          novars andalso has_vars t
wenzelm@9532
   124
                       then raise Match
wenzelm@9532
   125
                       else false               (*eliminates u*)
clasohm@0
   126
     | _ => raise Match;
clasohm@0
   127
lcp@680
   128
(*Locates a substitutable variable on the left (resp. right) of an equality
lcp@1011
   129
   assumption.  Returns the number of intervening assumptions. *)
lcp@1011
   130
fun eq_var bnd novars =
lcp@680
   131
  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
wenzelm@9532
   132
        | eq_var_aux k (Const("==>",_) $ A $ B) =
wenzelm@9532
   133
              ((k, inspect_pair bnd novars
wenzelm@9532
   134
                    (Data.dest_eq (Data.dest_Trueprop A)))
wenzelm@21227
   135
               handle TERM _ => eq_var_aux (k+1) B
wenzelm@21227
   136
                 | Match => eq_var_aux (k+1) B)
wenzelm@9532
   137
        | eq_var_aux k _ = raise EQ_VAR
lcp@680
   138
  in  eq_var_aux 0  end;
clasohm@0
   139
lcp@1011
   140
(*For the simpset.  Adds ALL suitable equalities, even if not first!
lcp@1011
   141
  No vars are allowed here, as simpsets are built from meta-assumptions*)
paulson@15415
   142
fun mk_eqs bnd th =
paulson@15415
   143
    [ if inspect_pair bnd false (Data.dest_eq
wenzelm@9532
   144
                                   (Data.dest_Trueprop (#prop (rep_thm th))))
lcp@1011
   145
      then th RS Data.eq_reflection
wenzelm@36945
   146
      else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
wenzelm@21227
   147
    handle TERM _ => [] | Match => [];
lcp@1011
   148
wenzelm@17896
   149
local
lcp@1011
   150
in
lcp@1011
   151
paulson@15415
   152
  (*Select a suitable equality assumption; substitute throughout the subgoal
paulson@15415
   153
    If bnd is true, then it replaces Bound variables only. *)
berghofe@13604
   154
  fun gen_hyp_subst_tac bnd =
wenzelm@17896
   155
    let fun tac i st = SUBGOAL (fn (Bi, _) =>
wenzelm@17896
   156
      let
wenzelm@17896
   157
        val (k, _) = eq_var bnd true Bi
wenzelm@35232
   158
        val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
wenzelm@36543
   159
          setmksimps (K (mk_eqs bnd))
berghofe@13604
   160
      in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
berghofe@13604
   161
        etac thin_rl i, rotate_tac (~k) i]
wenzelm@17896
   162
      end handle THM _ => no_tac | EQ_VAR => no_tac) i st
berghofe@13604
   163
    in REPEAT_DETERM1 o tac end;
lcp@1011
   164
lcp@1011
   165
end;
lcp@1011
   166
wenzelm@35021
   167
val ssubst = Drule.export_without_context (Data.sym RS Data.subst);
paulson@4466
   168
wenzelm@26992
   169
fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
berghofe@26833
   170
  case try (Logic.strip_assums_hyp #> hd #>
wenzelm@26992
   171
      Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
berghofe@26833
   172
    SOME (t, t') =>
berghofe@26833
   173
      let
wenzelm@26992
   174
        val Bi = Thm.term_of cBi;
berghofe@26833
   175
        val ps = Logic.strip_params Bi;
wenzelm@26992
   176
        val U = Term.fastype_of1 (rev (map snd ps), t);
berghofe@26833
   177
        val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
wenzelm@26992
   178
        val rl' = Thm.lift_rule cBi rl;
wenzelm@26992
   179
        val Var (ixn, T) = Term.head_of (Data.dest_Trueprop
wenzelm@26992
   180
          (Logic.strip_assums_concl (Thm.prop_of rl')));
berghofe@26833
   181
        val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
wenzelm@26992
   182
          (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
wenzelm@26992
   183
        val (Ts, V) = split_last (Term.binder_types T);
berghofe@26833
   184
        val u = list_abs (ps @ [("x", U)], case (if b then t else t') of
berghofe@26833
   185
            Bound j => subst_bounds (map Bound
berghofe@26833
   186
              ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
wenzelm@26992
   187
          | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
wenzelm@26992
   188
        val thy = Thm.theory_of_thm rl';
wenzelm@26992
   189
        val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
wenzelm@26992
   190
      in compose_tac (true, Drule.instantiate (instT,
berghofe@26833
   191
        map (pairself (cterm_of thy))
berghofe@26833
   192
          [(Var (ixn, Ts ---> U --> body_type T), u),
berghofe@26833
   193
           (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
berghofe@26833
   194
           (Var (fst (dest_Var (head_of v2)), Ts ---> U), list_abs (ps, t'))]) rl',
wenzelm@26992
   195
        nprems_of rl) i
berghofe@26833
   196
      end
wenzelm@26992
   197
  | NONE => no_tac);
berghofe@26833
   198
paulson@4466
   199
val imp_intr_tac = rtac Data.imp_intr;
lcp@1011
   200
berghofe@26833
   201
(* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
berghofe@26833
   202
(* premises containing meta-implications or quantifiers                *)
berghofe@26833
   203
lcp@1011
   204
(*Old version of the tactic above -- slower but the only way
lcp@1011
   205
  to handle equalities containing Vars.*)
paulson@3537
   206
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
paulson@3537
   207
      let val n = length(Logic.strip_assums_hyp Bi) - 1
wenzelm@9532
   208
          val (k,symopt) = eq_var bnd false Bi
wenzelm@9532
   209
      in
wenzelm@9532
   210
         DETERM
paulson@4466
   211
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
wenzelm@9532
   212
                   rotate_tac 1 i,
wenzelm@9532
   213
                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
berghofe@26833
   214
                   inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
wenzelm@9532
   215
                   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
clasohm@0
   216
      end
paulson@3537
   217
      handle THM _ => no_tac | EQ_VAR => no_tac);
clasohm@0
   218
clasohm@0
   219
(*Substitutes for Free or Bound variables*)
paulson@4466
   220
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
oheimb@4223
   221
        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
clasohm@0
   222
clasohm@0
   223
(*Substitutes for Bound variables only -- this is always safe*)
wenzelm@9532
   224
val bound_hyp_subst_tac =
lcp@1011
   225
    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
clasohm@0
   226
paulson@4466
   227
wenzelm@9532
   228
(** Version for Blast_tac.  Hyps that are affected by the substitution are
paulson@4466
   229
    moved to the front.  Defect: even trivial changes are noticed, such as
paulson@4466
   230
    substitutions in the arguments of a function Var. **)
paulson@4466
   231
paulson@4466
   232
(*final re-reversal of the changed assumptions*)
paulson@4466
   233
fun reverse_n_tac 0 i = all_tac
paulson@4466
   234
  | reverse_n_tac 1 i = rotate_tac ~1 i
wenzelm@9532
   235
  | reverse_n_tac n i =
paulson@4466
   236
      REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
paulson@4466
   237
      REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
paulson@4466
   238
paulson@4466
   239
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
wenzelm@9532
   240
fun all_imp_intr_tac hyps i =
paulson@4466
   241
  let fun imptac (r, [])    st = reverse_n_tac r i st
wenzelm@9532
   242
        | imptac (r, hyp::hyps) st =
wenzelm@9532
   243
           let val (hyp',_) = List.nth (prems_of st, i-1) |>
wenzelm@9532
   244
                              Logic.strip_assums_concl    |>
wenzelm@9532
   245
                              Data.dest_Trueprop          |> Data.dest_imp
wenzelm@9532
   246
               val (r',tac) = if Pattern.aeconv (hyp,hyp')
wenzelm@9532
   247
                              then (r, imp_intr_tac i THEN rotate_tac ~1 i)
wenzelm@9532
   248
                              else (*leave affected hyps at end*)
wenzelm@9532
   249
                                   (r+1, imp_intr_tac i)
wenzelm@9532
   250
           in
wenzelm@9532
   251
               case Seq.pull(tac st) of
skalberg@15531
   252
                   NONE       => Seq.single(st)
skalberg@15531
   253
                 | SOME(st',_) => imptac (r',hyps) st'
wenzelm@21221
   254
           end
paulson@4466
   255
  in  imptac (0, rev hyps)  end;
paulson@4466
   256
paulson@4466
   257
paulson@4466
   258
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
paulson@4466
   259
      let val (k,symopt) = eq_var false false Bi
wenzelm@9532
   260
          val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
paulson@4466
   261
          (*omit selected equality, returning other hyps*)
wenzelm@9532
   262
          val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
wenzelm@9532
   263
          val n = length hyps
wenzelm@9532
   264
      in
wenzelm@23908
   265
         if trace then tracing "Substituting an equality" else ();
wenzelm@9532
   266
         DETERM
paulson@4466
   267
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
wenzelm@9532
   268
                   rotate_tac 1 i,
wenzelm@9532
   269
                   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
berghofe@26833
   270
                   inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
wenzelm@9532
   271
                   all_imp_intr_tac hyps i])
paulson@4466
   272
      end
paulson@4466
   273
      handle THM _ => no_tac | EQ_VAR => no_tac);
paulson@4466
   274
wenzelm@9532
   275
wenzelm@9532
   276
(*apply an equality or definition ONCE;
wenzelm@9532
   277
  fails unless the substitution has an effect*)
wenzelm@9532
   278
fun stac th =
wenzelm@9532
   279
  let val th' = th RS Data.rev_eq_reflection handle THM _ => th
wenzelm@9532
   280
  in CHANGED_GOAL (rtac (th' RS ssubst)) end;
wenzelm@9532
   281
wenzelm@9532
   282
wenzelm@9628
   283
(* theory setup *)
wenzelm@9628
   284
wenzelm@9532
   285
val hypsubst_setup =
wenzelm@30515
   286
  Method.setup @{binding hypsubst}
wenzelm@30515
   287
    (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac))))
wenzelm@30515
   288
    "substitution using an assumption (improper)" #>
wenzelm@30515
   289
  Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
wenzelm@30515
   290
    "simple substitution";
wenzelm@9532
   291
clasohm@0
   292
end;