src/Pure/Isar/rule_insts.ML
changeset 30545 8209a7196389
parent 30528 7173bf123335
child 30551 24e156db414c
equal deleted inserted replaced
30544:0ed8fe16331a 30545:8209a7196389
    14   val forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    14   val forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    15   val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    15   val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    16   val thin_tac: Proof.context -> string -> int -> tactic
    16   val thin_tac: Proof.context -> string -> int -> tactic
    17   val subgoal_tac: Proof.context -> string -> int -> tactic
    17   val subgoal_tac: Proof.context -> string -> int -> tactic
    18   val subgoals_tac: Proof.context -> string list -> int -> tactic
    18   val subgoals_tac: Proof.context -> string list -> int -> tactic
       
    19   val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
       
    20     (thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
    19 end;
    21 end;
    20 
    22 
    21 signature RULE_INSTS =
    23 signature RULE_INSTS =
    22 sig
    24 sig
    23   include BASIC_RULE_INSTS
    25   include BASIC_RULE_INSTS
   381 
   383 
   382 (** methods **)
   384 (** methods **)
   383 
   385 
   384 (* rule_tac etc. -- refer to dynamic goal state! *)
   386 (* rule_tac etc. -- refer to dynamic goal state! *)
   385 
   387 
   386 local
   388 fun method inst_tac tac =
   387 
       
   388 fun inst_meth inst_tac tac =
       
   389   Args.goal_spec --
   389   Args.goal_spec --
   390   Scan.optional (Scan.lift
   390   Scan.optional (Scan.lift
   391     (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
   391     (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
   392   Attrib.thms >>
   392   Attrib.thms >>
   393   (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
   393   (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
   395     else
   395     else
   396       (case thms of
   396       (case thms of
   397         [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
   397         [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
   398       | _ => error "Cannot have instantiations with multiple rules")));
   398       | _ => error "Cannot have instantiations with multiple rules")));
   399 
   399 
   400 in
   400 val res_inst_meth = method res_inst_tac Tactic.resolve_tac;
   401 
   401 val eres_inst_meth = method eres_inst_tac Tactic.eresolve_tac;
   402 val res_inst_meth = inst_meth res_inst_tac Tactic.resolve_tac;
   402 val cut_inst_meth = method cut_inst_tac Tactic.cut_rules_tac;
   403 val eres_inst_meth = inst_meth eres_inst_tac Tactic.eresolve_tac;
   403 val dres_inst_meth = method dres_inst_tac Tactic.dresolve_tac;
   404 val cut_inst_meth = inst_meth cut_inst_tac Tactic.cut_rules_tac;
   404 val forw_inst_meth = method forw_inst_tac Tactic.forward_tac;
   405 val dres_inst_meth = inst_meth dres_inst_tac Tactic.dresolve_tac;
       
   406 val forw_inst_meth = inst_meth forw_inst_tac Tactic.forward_tac;
       
   407 
       
   408 end;
       
   409 
   405 
   410 
   406 
   411 (* setup *)
   407 (* setup *)
   412 
   408 
   413 val _ = Context.>> (Context.map_theory
   409 val _ = Context.>> (Context.map_theory