src/Provers/hypsubst.ML
changeset 57509 cca0db87b653
parent 57492 74bf65a1910a
child 58826 2ed2eaabe3df
equal deleted inserted replaced
57508:19240ff4b02d 57509:cca0db87b653
    46 
    46 
    47 signature HYPSUBST =
    47 signature HYPSUBST =
    48 sig
    48 sig
    49   val bound_hyp_subst_tac    : Proof.context -> int -> tactic
    49   val bound_hyp_subst_tac    : Proof.context -> int -> tactic
    50   val hyp_subst_tac_thin     : bool -> Proof.context -> int -> tactic
    50   val hyp_subst_tac_thin     : bool -> Proof.context -> int -> tactic
    51   val hyp_subst_thins        : bool Config.T
    51   val hyp_subst_thin         : bool Config.T
    52   val hyp_subst_tac          : Proof.context -> int -> tactic
    52   val hyp_subst_tac          : Proof.context -> int -> tactic
    53   val blast_hyp_subst_tac    : bool -> int -> tactic
    53   val blast_hyp_subst_tac    : bool -> int -> tactic
    54   val stac                   : thm -> int -> tactic
    54   val stac                   : thm -> int -> tactic
    55   val hypsubst_setup         : theory -> theory
    55   val hypsubst_setup         : theory -> theory
    56 end;
    56 end;
   226 fun hyp_subst_tac_thin thin ctxt =
   226 fun hyp_subst_tac_thin thin ctxt =
   227   REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
   227   REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
   228     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
   228     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
   229     if thin then thin_free_eq_tac else K no_tac];
   229     if thin then thin_free_eq_tac else K no_tac];
   230 
   230 
   231 val (hyp_subst_thins, hyp_subst_thins_setup) = Attrib.config_bool
   231 val (hyp_subst_thin, hyp_subst_thin_setup) = Attrib.config_bool
   232     @{binding hypsubst_thin} (K false);
   232     @{binding hypsubst_thin} (K false);
   233 
   233 
   234 fun hyp_subst_tac ctxt = hyp_subst_tac_thin
   234 fun hyp_subst_tac ctxt = hyp_subst_tac_thin
   235     (Config.get ctxt hyp_subst_thins) ctxt
   235     (Config.get ctxt hyp_subst_thin) ctxt
   236 
   236 
   237 (*Substitutes for Bound variables only -- this is always safe*)
   237 (*Substitutes for Bound variables only -- this is always safe*)
   238 fun bound_hyp_subst_tac ctxt =
   238 fun bound_hyp_subst_tac ctxt =
   239   REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
   239   REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
   240     ORELSE' vars_gen_hyp_subst_tac true);
   240     ORELSE' vars_gen_hyp_subst_tac true);
   304     "substitution using an assumption (improper)" #>
   304     "substitution using an assumption (improper)" #>
   305   Method.setup @{binding hypsubst_thin}
   305   Method.setup @{binding hypsubst_thin}
   306     (Scan.succeed (fn ctxt => SIMPLE_METHOD'
   306     (Scan.succeed (fn ctxt => SIMPLE_METHOD'
   307         (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
   307         (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
   308     "substitution using an assumption, eliminating assumptions" #>
   308     "substitution using an assumption, eliminating assumptions" #>
   309   hyp_subst_thins_setup #>
   309   hyp_subst_thin_setup #>
   310   Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
   310   Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
   311     "simple substitution";
   311     "simple substitution";
   312 
   312 
   313 end;
   313 end;