added (e)res_inst_tac;
authorwenzelm
Tue Jun 10 16:43:23 2008 +0200 (2008-06-10 ago)
changeset 27120b21eec437295
parent 27119 c36c88fcdd22
child 27121 38367dbccae5
added (e)res_inst_tac;
tuned comments;
src/Pure/Isar/rule_insts.ML
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Tue Jun 10 16:43:21 2008 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Tue Jun 10 16:43:23 2008 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  sig
     1.5    val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
     1.6      thm -> int -> tactic
     1.7 +  val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
     1.8 +  val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
     1.9  end;
    1.10  
    1.11  structure RuleInsts: RULE_INSTS =
    1.12 @@ -227,7 +229,7 @@
    1.13  
    1.14  (** methods **)
    1.15  
    1.16 -(* rule_tac etc. -- refer to dynamic goal state!! *)   (* FIXME cleanup!! *)
    1.17 +(* rule_tac etc. -- refer to dynamic goal state!! *)   (* FIXME cleanup this mess!!! *)
    1.18  
    1.19  fun bires_inst_tac bires_flag ctxt insts thm =
    1.20    let
    1.21 @@ -306,6 +308,10 @@
    1.22                  | THM  (msg,_,_) => (warning msg; no_tac st);
    1.23    in tac end;
    1.24  
    1.25 +val res_inst_tac = bires_inst_tac false;
    1.26 +val eres_inst_tac = bires_inst_tac true;
    1.27 +
    1.28 +
    1.29  local
    1.30  
    1.31  fun gen_inst _ tac _ (quant, ([], thms)) =
    1.32 @@ -317,34 +323,29 @@
    1.33  
    1.34  in
    1.35  
    1.36 -val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac;
    1.37 -
    1.38 -val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac;
    1.39 +val res_inst_meth = gen_inst res_inst_tac Tactic.resolve_tac;
    1.40 +val eres_inst_meth = gen_inst eres_inst_tac Tactic.eresolve_tac;
    1.41  
    1.42  val cut_inst_meth =
    1.43    gen_inst
    1.44 -    (fn ctxt => fn insts => bires_inst_tac false ctxt insts o Tactic.make_elim_preserve)
    1.45 +    (fn ctxt => fn insts => res_inst_tac ctxt insts o Tactic.make_elim_preserve)
    1.46      Tactic.cut_rules_tac;
    1.47  
    1.48  val dres_inst_meth =
    1.49    gen_inst
    1.50 -    (fn ctxt => fn insts => bires_inst_tac true ctxt insts o Tactic.make_elim_preserve)
    1.51 +    (fn ctxt => fn insts => eres_inst_tac ctxt insts o Tactic.make_elim_preserve)
    1.52      Tactic.dresolve_tac;
    1.53  
    1.54  val forw_inst_meth =
    1.55    gen_inst
    1.56      (fn ctxt => fn insts => fn rule =>
    1.57 -       bires_inst_tac false ctxt insts (Tactic.make_elim_preserve rule) THEN'
    1.58 -       assume_tac)
    1.59 +       res_inst_tac ctxt insts (Tactic.make_elim_preserve rule) THEN' assume_tac)
    1.60      Tactic.forward_tac;
    1.61  
    1.62 -fun subgoal_tac ctxt sprop =
    1.63 -  DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl;
    1.64 -
    1.65 +fun subgoal_tac ctxt sprop = DETERM o res_inst_tac ctxt [(("psi", 0), sprop)] cut_rl;
    1.66  fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops);
    1.67  
    1.68 -fun thin_tac ctxt s =
    1.69 -  bires_inst_tac true ctxt [(("V", 0), s)] thin_rl;
    1.70 +fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] thin_rl;
    1.71  
    1.72  
    1.73  (* method syntax *)