src/Provers/hypsubst.ML
author wenzelm
Thu Oct 30 16:55:29 2014 +0100 (2014-10-30)
changeset 58838 59203adfc33f
parent 58826 2ed2eaabe3df
child 58950 d07464875dd4
permissions -rw-r--r--
eliminated aliases;
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
rafal@48107
     5
Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst".
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 *)
wenzelm@21221
    45
end;
lcp@1011
    46
clasohm@0
    47
signature HYPSUBST =
wenzelm@21221
    48
sig
wenzelm@51798
    49
  val bound_hyp_subst_tac    : Proof.context -> int -> tactic
thomas@57492
    50
  val hyp_subst_tac_thin     : bool -> Proof.context -> int -> tactic
wenzelm@57509
    51
  val hyp_subst_thin         : bool Config.T
wenzelm@51798
    52
  val hyp_subst_tac          : Proof.context -> int -> tactic
wenzelm@23908
    53
  val blast_hyp_subst_tac    : bool -> int -> tactic
haftmann@20945
    54
  val stac                   : thm -> int -> tactic
wenzelm@21221
    55
end;
paulson@2722
    56
wenzelm@42799
    57
functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
clasohm@0
    58
struct
clasohm@0
    59
clasohm@0
    60
exception EQ_VAR;
clasohm@0
    61
wenzelm@16979
    62
(*Simplifier turns Bound variables to special Free variables:
wenzelm@16979
    63
  change it back (any Bound variable will do)*)
lcp@1011
    64
fun contract t =
berghofe@26833
    65
  (case Envir.eta_contract t of
wenzelm@20074
    66
    Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
wenzelm@16979
    67
  | t' => t');
lcp@1011
    68
wenzelm@21221
    69
val has_vars = Term.exists_subterm Term.is_Var;
wenzelm@21221
    70
val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar);
lcp@1011
    71
lcp@1011
    72
(*If novars then we forbid Vars in the equality.
wenzelm@16979
    73
  If bnd then we only look for Bound variables to eliminate.
lcp@1011
    74
  When can we safely delete the equality?
lcp@1011
    75
    Not if it equates two constants; consider 0=1.
lcp@1011
    76
    Not if it resembles x=t[x], since substitution does not eliminate x.
paulson@4299
    77
    Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
wenzelm@9532
    78
    Not if it involves a variable free in the premises,
lcp@1011
    79
        but we can't check for this -- hence bnd and bound_hyp_subst_tac
lcp@1011
    80
  Prefer to eliminate Bound variables if possible.
thomas@57492
    81
  Result:  true = use as is,  false = reorient first
thomas@57492
    82
    also returns var to substitute, relevant if it is Free *)
wenzelm@21221
    83
fun inspect_pair bnd novars (t, u) =
wenzelm@21221
    84
  if novars andalso (has_tvars t orelse has_tvars u)
paulson@4179
    85
  then raise Match   (*variables in the type!*)
paulson@4179
    86
  else
wenzelm@42082
    87
    (case (contract t, contract u) of
wenzelm@42082
    88
      (Bound i, _) =>
wenzelm@42082
    89
        if loose_bvar1 (u, i) orelse novars andalso has_vars u
wenzelm@42082
    90
        then raise Match
thomas@57492
    91
        else (true, Bound i)                (*eliminates t*)
wenzelm@42082
    92
    | (_, Bound i) =>
wenzelm@42082
    93
        if loose_bvar1 (t, i) orelse novars andalso has_vars t
wenzelm@42082
    94
        then raise Match
thomas@57492
    95
        else (false, Bound i)               (*eliminates u*)
wenzelm@42082
    96
    | (t' as Free _, _) =>
wenzelm@42082
    97
        if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u
wenzelm@42082
    98
        then raise Match
thomas@57492
    99
        else (true, t')                (*eliminates t*)
wenzelm@42082
   100
    | (_, u' as Free _) =>
wenzelm@42082
   101
        if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t
wenzelm@42082
   102
        then raise Match
thomas@57492
   103
        else (false, u')               (*eliminates u*)
wenzelm@42082
   104
    | _ => raise Match);
clasohm@0
   105
lcp@680
   106
(*Locates a substitutable variable on the left (resp. right) of an equality
lcp@1011
   107
   assumption.  Returns the number of intervening assumptions. *)
thomas@57492
   108
fun eq_var bnd novars check_frees t =
thomas@57492
   109
  let
thomas@57492
   110
    fun check_free ts (orient, Free f)
thomas@57492
   111
      = if not check_frees orelse not orient
thomas@57492
   112
            orelse exists (curry Logic.occs (Free f)) ts
thomas@57492
   113
        then (orient, true) else raise Match
thomas@57492
   114
      | check_free ts (orient, _) = (orient, false)
thomas@57492
   115
    fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) hs = eq_var_aux k t hs
thomas@57492
   116
      | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) hs =
thomas@57492
   117
              ((k, check_free (B :: hs) (inspect_pair bnd novars
thomas@57492
   118
                    (Data.dest_eq (Data.dest_Trueprop A))))
thomas@57492
   119
               handle TERM _ => eq_var_aux (k+1) B (A :: hs)
thomas@57492
   120
                 | Match => eq_var_aux (k+1) B (A :: hs))
thomas@57492
   121
      | eq_var_aux k _ _ = raise EQ_VAR
wenzelm@58826
   122
thomas@57492
   123
  in  eq_var_aux 0 t [] end;
thomas@57492
   124
thomas@57492
   125
val thin_free_eq_tac = SUBGOAL (fn (t, i) => let
thomas@57492
   126
     val (k, _) = eq_var false false false t
thomas@57492
   127
     val ok = (eq_var false false true t |> fst) > k
thomas@57492
   128
        handle EQ_VAR => true
wenzelm@58838
   129
   in if ok then EVERY [rotate_tac k i, eresolve_tac [thin_rl] i, rotate_tac (~k) i]
thomas@57492
   130
    else no_tac
thomas@57492
   131
   end handle EQ_VAR => no_tac)
clasohm@0
   132
lcp@1011
   133
(*For the simpset.  Adds ALL suitable equalities, even if not first!
lcp@1011
   134
  No vars are allowed here, as simpsets are built from meta-assumptions*)
paulson@15415
   135
fun mk_eqs bnd th =
thomas@57492
   136
    [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) |> fst
lcp@1011
   137
      then th RS Data.eq_reflection
wenzelm@36945
   138
      else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
wenzelm@21227
   139
    handle TERM _ => [] | Match => [];
lcp@1011
   140
thomas@57492
   141
fun bool2s true = "true" | bool2s false = "false"
thomas@57492
   142
wenzelm@17896
   143
local
lcp@1011
   144
in
lcp@1011
   145
paulson@15415
   146
  (*Select a suitable equality assumption; substitute throughout the subgoal
paulson@15415
   147
    If bnd is true, then it replaces Bound variables only. *)
wenzelm@51798
   148
  fun gen_hyp_subst_tac ctxt bnd =
thomas@57492
   149
    SUBGOAL (fn (Bi, i) =>
wenzelm@17896
   150
      let
thomas@57492
   151
        val (k, (orient, is_free)) = eq_var bnd true true Bi
wenzelm@51717
   152
        val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
wenzelm@51717
   153
      in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
wenzelm@58838
   154
        if not is_free then eresolve_tac [thin_rl] i
wenzelm@58838
   155
          else if orient then eresolve_tac [Data.rev_mp] i
wenzelm@58838
   156
          else eresolve_tac [Data.sym RS Data.rev_mp] i,
thomas@57492
   157
        rotate_tac (~k) i,
wenzelm@58838
   158
        if is_free then resolve_tac [Data.imp_intr] i else all_tac]
thomas@57492
   159
      end handle THM _ => no_tac | EQ_VAR => no_tac)
lcp@1011
   160
lcp@1011
   161
end;
lcp@1011
   162
wenzelm@45659
   163
val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst);
paulson@4466
   164
wenzelm@26992
   165
fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
berghofe@26833
   166
  case try (Logic.strip_assums_hyp #> hd #>
wenzelm@26992
   167
      Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
berghofe@26833
   168
    SOME (t, t') =>
berghofe@26833
   169
      let
wenzelm@26992
   170
        val Bi = Thm.term_of cBi;
berghofe@26833
   171
        val ps = Logic.strip_params Bi;
wenzelm@26992
   172
        val U = Term.fastype_of1 (rev (map snd ps), t);
berghofe@26833
   173
        val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
wenzelm@26992
   174
        val rl' = Thm.lift_rule cBi rl;
wenzelm@26992
   175
        val Var (ixn, T) = Term.head_of (Data.dest_Trueprop
wenzelm@26992
   176
          (Logic.strip_assums_concl (Thm.prop_of rl')));
berghofe@26833
   177
        val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
wenzelm@26992
   178
          (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
wenzelm@26992
   179
        val (Ts, V) = split_last (Term.binder_types T);
wenzelm@46219
   180
        val u =
wenzelm@46219
   181
          fold_rev Term.abs (ps @ [("x", U)])
wenzelm@46219
   182
            (case (if b then t else t') of
wenzelm@46219
   183
              Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
wenzelm@46219
   184
            | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
wenzelm@26992
   185
        val thy = Thm.theory_of_thm rl';
wenzelm@26992
   186
        val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
wenzelm@46219
   187
      in
wenzelm@46219
   188
        compose_tac (true, Drule.instantiate_normalize (instT,
wenzelm@46219
   189
          map (pairself (cterm_of thy))
wenzelm@46219
   190
            [(Var (ixn, Ts ---> U --> body_type T), u),
wenzelm@46219
   191
             (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
wenzelm@46219
   192
             (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
wenzelm@46219
   193
          nprems_of rl) i
berghofe@26833
   194
      end
wenzelm@26992
   195
  | NONE => no_tac);
berghofe@26833
   196
wenzelm@58838
   197
val imp_intr_tac = resolve_tac [Data.imp_intr];
lcp@1011
   198
thomas@57492
   199
fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
thomas@57492
   200
val dup_subst = rev_dup_elim ssubst
thomas@57492
   201
berghofe@26833
   202
(* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
berghofe@26833
   203
(* premises containing meta-implications or quantifiers                *)
berghofe@26833
   204
lcp@1011
   205
(*Old version of the tactic above -- slower but the only way
lcp@1011
   206
  to handle equalities containing Vars.*)
paulson@3537
   207
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
paulson@3537
   208
      let val n = length(Logic.strip_assums_hyp Bi) - 1
thomas@57492
   209
          val (k, (orient, is_free)) = eq_var bnd false true Bi
thomas@57492
   210
          val rl = if is_free then dup_subst else ssubst
thomas@57492
   211
          val rl = if orient then rl else Data.sym RS rl
wenzelm@9532
   212
      in
wenzelm@9532
   213
         DETERM
wenzelm@58838
   214
           (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
wenzelm@9532
   215
                   rotate_tac 1 i,
wenzelm@58838
   216
                   REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
thomas@57492
   217
                   inst_subst_tac orient rl i,
wenzelm@9532
   218
                   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
clasohm@0
   219
      end
paulson@3537
   220
      handle THM _ => no_tac | EQ_VAR => no_tac);
clasohm@0
   221
thomas@57492
   222
(*Substitutes for Free or Bound variables,
thomas@57492
   223
  discarding equalities on Bound variables
thomas@57492
   224
  and on Free variables if thin=true*)
thomas@57492
   225
fun hyp_subst_tac_thin thin ctxt =
thomas@57492
   226
  REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
thomas@57492
   227
    gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
thomas@57492
   228
    if thin then thin_free_eq_tac else K no_tac];
thomas@57492
   229
wenzelm@58826
   230
val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);
thomas@57492
   231
wenzelm@58826
   232
fun hyp_subst_tac ctxt =
wenzelm@58826
   233
  hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt;
clasohm@0
   234
clasohm@0
   235
(*Substitutes for Bound variables only -- this is always safe*)
wenzelm@51798
   236
fun bound_hyp_subst_tac ctxt =
thomas@57492
   237
  REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
thomas@57492
   238
    ORELSE' vars_gen_hyp_subst_tac true);
paulson@4466
   239
wenzelm@9532
   240
(** Version for Blast_tac.  Hyps that are affected by the substitution are
paulson@4466
   241
    moved to the front.  Defect: even trivial changes are noticed, such as
paulson@4466
   242
    substitutions in the arguments of a function Var. **)
paulson@4466
   243
paulson@4466
   244
(*final re-reversal of the changed assumptions*)
paulson@4466
   245
fun reverse_n_tac 0 i = all_tac
paulson@4466
   246
  | reverse_n_tac 1 i = rotate_tac ~1 i
wenzelm@9532
   247
  | reverse_n_tac n i =
wenzelm@58838
   248
      REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac [Data.rev_mp] i) THEN
paulson@4466
   249
      REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
paulson@4466
   250
paulson@4466
   251
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
wenzelm@9532
   252
fun all_imp_intr_tac hyps i =
wenzelm@42364
   253
  let
wenzelm@42364
   254
    fun imptac (r, []) st = reverse_n_tac r i st
wenzelm@42364
   255
      | imptac (r, hyp::hyps) st =
wenzelm@42364
   256
          let
wenzelm@42364
   257
            val (hyp', _) =
wenzelm@42366
   258
              term_of (Thm.cprem_of st i)
wenzelm@42364
   259
              |> Logic.strip_assums_concl
wenzelm@42364
   260
              |> Data.dest_Trueprop |> Data.dest_imp;
wenzelm@42364
   261
            val (r', tac) =
wenzelm@52131
   262
              if Envir.aeconv (hyp, hyp')
wenzelm@42364
   263
              then (r, imp_intr_tac i THEN rotate_tac ~1 i)
wenzelm@42364
   264
              else (*leave affected hyps at end*) (r + 1, imp_intr_tac i);
wenzelm@42364
   265
          in
wenzelm@42364
   266
            (case Seq.pull (tac st) of
wenzelm@42364
   267
              NONE => Seq.single st
wenzelm@42364
   268
            | SOME (st', _) => imptac (r', hyps) st')
wenzelm@42364
   269
          end
wenzelm@42364
   270
  in imptac (0, rev hyps) end;
paulson@4466
   271
paulson@4466
   272
paulson@4466
   273
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
thomas@57492
   274
      let val (k, (symopt, _)) = eq_var false false false Bi
wenzelm@9532
   275
          val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
paulson@4466
   276
          (*omit selected equality, returning other hyps*)
wenzelm@9532
   277
          val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
wenzelm@9532
   278
          val n = length hyps
wenzelm@9532
   279
      in
wenzelm@23908
   280
         if trace then tracing "Substituting an equality" else ();
wenzelm@9532
   281
         DETERM
wenzelm@58838
   282
           (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
wenzelm@9532
   283
                   rotate_tac 1 i,
wenzelm@58838
   284
                   REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
berghofe@26833
   285
                   inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
wenzelm@9532
   286
                   all_imp_intr_tac hyps i])
paulson@4466
   287
      end
paulson@4466
   288
      handle THM _ => no_tac | EQ_VAR => no_tac);
paulson@4466
   289
wenzelm@9532
   290
(*apply an equality or definition ONCE;
wenzelm@9532
   291
  fails unless the substitution has an effect*)
wenzelm@9532
   292
fun stac th =
wenzelm@9532
   293
  let val th' = th RS Data.rev_eq_reflection handle THM _ => th
wenzelm@58838
   294
  in CHANGED_GOAL (resolve_tac [th' RS ssubst]) end;
wenzelm@9532
   295
wenzelm@9532
   296
wenzelm@58826
   297
(* method setup *)
wenzelm@9628
   298
wenzelm@58826
   299
val _ =
wenzelm@58826
   300
  Theory.setup
wenzelm@58826
   301
   (Method.setup @{binding hypsubst}
wenzelm@58826
   302
      (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
wenzelm@58826
   303
      "substitution using an assumption (improper)" #>
wenzelm@58826
   304
    Method.setup @{binding hypsubst_thin}
wenzelm@58826
   305
      (Scan.succeed (fn ctxt => SIMPLE_METHOD'
wenzelm@58826
   306
          (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
wenzelm@58826
   307
      "substitution using an assumption, eliminating assumptions" #>
wenzelm@58826
   308
    Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
wenzelm@58826
   309
      "simple substitution");
wenzelm@9532
   310
clasohm@0
   311
end;