src/Provers/hypsubst.ML
changeset 51717 9e7d1c139569
parent 50035 4d17291eb19c
child 51798 ad3a241def73
equal deleted inserted replaced
51709:19b47bfac6ef 51717:9e7d1c139569
    46 
    46 
    47 signature HYPSUBST =
    47 signature HYPSUBST =
    48 sig
    48 sig
    49   val bound_hyp_subst_tac    : int -> tactic
    49   val bound_hyp_subst_tac    : int -> tactic
    50   val hyp_subst_tac          : int -> tactic
    50   val hyp_subst_tac          : int -> tactic
    51   val hyp_subst_tac'         : simpset -> int -> tactic
    51   val hyp_subst_tac'         : Proof.context -> int -> tactic
    52   val blast_hyp_subst_tac    : bool -> int -> tactic
    52   val blast_hyp_subst_tac    : bool -> int -> tactic
    53   val stac                   : thm -> int -> tactic
    53   val stac                   : thm -> int -> tactic
    54   val hypsubst_setup         : theory -> theory
    54   val hypsubst_setup         : theory -> theory
    55 end;
    55 end;
    56 
    56 
   125 local
   125 local
   126 in
   126 in
   127 
   127 
   128   (*Select a suitable equality assumption; substitute throughout the subgoal
   128   (*Select a suitable equality assumption; substitute throughout the subgoal
   129     If bnd is true, then it replaces Bound variables only. *)
   129     If bnd is true, then it replaces Bound variables only. *)
   130   fun gen_hyp_subst_tac opt_ss bnd =
   130   fun gen_hyp_subst_tac opt_ctxt bnd =
   131     let fun tac i st = SUBGOAL (fn (Bi, _) =>
   131     let fun tac i st = SUBGOAL (fn (Bi, _) =>
   132       let
   132       let
   133         val (k, _) = eq_var bnd true Bi
   133         val (k, _) = eq_var bnd true Bi
   134         val map_simpset = case opt_ss of
   134         val ctxt =
   135           NONE => Simplifier.global_context (Thm.theory_of_thm st)
   135           (case opt_ctxt of
   136         | SOME ss => Simplifier.inherit_context ss
   136             NONE => Proof_Context.init_global (Thm.theory_of_thm st)
   137         val hyp_subst_ss = map_simpset empty_ss |> Simplifier.set_mksimps (K (mk_eqs bnd))
   137           | SOME ctxt => ctxt)
   138       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
   138         val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
       
   139       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
   139         etac thin_rl i, rotate_tac (~k) i]
   140         etac thin_rl i, rotate_tac (~k) i]
   140       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
   141       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
   141     in REPEAT_DETERM1 o tac end;
   142     in REPEAT_DETERM1 o tac end;
   142 
   143 
   143 end;
   144 end;
   198 
   199 
   199 (*Substitutes for Free or Bound variables*)
   200 (*Substitutes for Free or Bound variables*)
   200 val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
   201 val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
   201         gen_hyp_subst_tac NONE false, vars_gen_hyp_subst_tac false];
   202         gen_hyp_subst_tac NONE false, vars_gen_hyp_subst_tac false];
   202 
   203 
   203 fun hyp_subst_tac' ss = FIRST' [ematch_tac [Data.thin_refl],
   204 fun hyp_subst_tac' ctxt = FIRST' [ematch_tac [Data.thin_refl],
   204         gen_hyp_subst_tac (SOME ss) false, vars_gen_hyp_subst_tac false];
   205         gen_hyp_subst_tac (SOME ctxt) false, vars_gen_hyp_subst_tac false];
   205 
   206 
   206 (*Substitutes for Bound variables only -- this is always safe*)
   207 (*Substitutes for Bound variables only -- this is always safe*)
   207 val bound_hyp_subst_tac =
   208 val bound_hyp_subst_tac =
   208     gen_hyp_subst_tac NONE true ORELSE' vars_gen_hyp_subst_tac true;
   209     gen_hyp_subst_tac NONE true ORELSE' vars_gen_hyp_subst_tac true;
   209 
   210