src/Provers/hypsubst.ML
changeset 58826 2ed2eaabe3df
parent 57509 cca0db87b653
child 58838 59203adfc33f
equal deleted inserted replaced
58825:2065f49da190 58826:2ed2eaabe3df
    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_thin         : 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
       
    56 end;
    55 end;
    57 
    56 
    58 functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
    57 functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
    59 struct
    58 struct
    60 
    59 
   118               ((k, check_free (B :: hs) (inspect_pair bnd novars
   117               ((k, check_free (B :: hs) (inspect_pair bnd novars
   119                     (Data.dest_eq (Data.dest_Trueprop A))))
   118                     (Data.dest_eq (Data.dest_Trueprop A))))
   120                handle TERM _ => eq_var_aux (k+1) B (A :: hs)
   119                handle TERM _ => eq_var_aux (k+1) B (A :: hs)
   121                  | Match => eq_var_aux (k+1) B (A :: hs))
   120                  | Match => eq_var_aux (k+1) B (A :: hs))
   122       | eq_var_aux k _ _ = raise EQ_VAR
   121       | eq_var_aux k _ _ = raise EQ_VAR
   123   
   122 
   124   in  eq_var_aux 0 t [] end;
   123   in  eq_var_aux 0 t [] end;
   125 
   124 
   126 val thin_free_eq_tac = SUBGOAL (fn (t, i) => let
   125 val thin_free_eq_tac = SUBGOAL (fn (t, i) => let
   127      val (k, _) = eq_var false false false t
   126      val (k, _) = eq_var false false false t
   128      val ok = (eq_var false false true t |> fst) > k
   127      val ok = (eq_var false false true t |> fst) > k
   226 fun hyp_subst_tac_thin thin ctxt =
   225 fun hyp_subst_tac_thin thin ctxt =
   227   REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
   226   REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
   228     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
   227     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
   229     if thin then thin_free_eq_tac else K no_tac];
   228     if thin then thin_free_eq_tac else K no_tac];
   230 
   229 
   231 val (hyp_subst_thin, hyp_subst_thin_setup) = Attrib.config_bool
   230 val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);
   232     @{binding hypsubst_thin} (K false);
   231 
   233 
   232 fun hyp_subst_tac ctxt =
   234 fun hyp_subst_tac ctxt = hyp_subst_tac_thin
   233   hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt;
   235     (Config.get ctxt hyp_subst_thin) ctxt
       
   236 
   234 
   237 (*Substitutes for Bound variables only -- this is always safe*)
   235 (*Substitutes for Bound variables only -- this is always safe*)
   238 fun bound_hyp_subst_tac ctxt =
   236 fun bound_hyp_subst_tac ctxt =
   239   REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
   237   REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
   240     ORELSE' vars_gen_hyp_subst_tac true);
   238     ORELSE' vars_gen_hyp_subst_tac true);
   294 fun stac th =
   292 fun stac th =
   295   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   293   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   296   in CHANGED_GOAL (rtac (th' RS ssubst)) end;
   294   in CHANGED_GOAL (rtac (th' RS ssubst)) end;
   297 
   295 
   298 
   296 
   299 (* theory setup *)
   297 (* method setup *)
   300 
   298 
   301 val hypsubst_setup =
   299 val _ =
   302   Method.setup @{binding hypsubst}
   300   Theory.setup
   303     (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
   301    (Method.setup @{binding hypsubst}
   304     "substitution using an assumption (improper)" #>
   302       (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
   305   Method.setup @{binding hypsubst_thin}
   303       "substitution using an assumption (improper)" #>
   306     (Scan.succeed (fn ctxt => SIMPLE_METHOD'
   304     Method.setup @{binding hypsubst_thin}
   307         (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
   305       (Scan.succeed (fn ctxt => SIMPLE_METHOD'
   308     "substitution using an assumption, eliminating assumptions" #>
   306           (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
   309   hyp_subst_thin_setup #>
   307       "substitution using an assumption, eliminating assumptions" #>
   310   Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
   308     Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
   311     "simple substitution";
   309       "simple substitution");
   312 
   310 
   313 end;
   311 end;