src/Pure/Isar/rule_insts.ML
changeset 30515 bca05b17b618
parent 30510 4120fc59dd85
child 30528 7173bf123335
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Fri Mar 13 23:32:40 2009 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Fri Mar 13 23:50:05 2009 +0100
     1.3 @@ -386,61 +386,48 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun gen_inst _ tac _ (quant, ([], thms)) =
     1.8 -      METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
     1.9 -  | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
    1.10 -      METHOD (fn facts =>
    1.11 -        quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm))
    1.12 -  | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
    1.13 +fun inst_meth inst_tac tac =
    1.14 +  Args.goal_spec --
    1.15 +  Scan.optional (Scan.lift
    1.16 +    (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
    1.17 +  Attrib.thms >>
    1.18 +  (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
    1.19 +    if null insts then quant (Method.insert_tac facts THEN' tac thms)
    1.20 +    else
    1.21 +      (case thms of
    1.22 +        [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
    1.23 +      | _ => error "Cannot have instantiations with multiple rules")));
    1.24  
    1.25  in
    1.26  
    1.27 -val res_inst_meth = gen_inst res_inst_tac Tactic.resolve_tac;
    1.28 -val eres_inst_meth = gen_inst eres_inst_tac Tactic.eresolve_tac;
    1.29 -val cut_inst_meth = gen_inst cut_inst_tac Tactic.cut_rules_tac;
    1.30 -val dres_inst_meth = gen_inst dres_inst_tac Tactic.dresolve_tac;
    1.31 -val forw_inst_meth = gen_inst forw_inst_tac Tactic.forward_tac;
    1.32 +val res_inst_meth = inst_meth res_inst_tac Tactic.resolve_tac;
    1.33 +val eres_inst_meth = inst_meth eres_inst_tac Tactic.eresolve_tac;
    1.34 +val cut_inst_meth = inst_meth cut_inst_tac Tactic.cut_rules_tac;
    1.35 +val dres_inst_meth = inst_meth dres_inst_tac Tactic.dresolve_tac;
    1.36 +val forw_inst_meth = inst_meth forw_inst_tac Tactic.forward_tac;
    1.37  
    1.38  end;
    1.39  
    1.40  
    1.41 -(* method syntax *)
    1.42 -
    1.43 -val insts =
    1.44 -  Scan.optional (Scan.lift
    1.45 -    (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
    1.46 -    -- Attrib.thms;
    1.47 -
    1.48 -fun inst_args f src ctxt =
    1.49 -  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
    1.50 -
    1.51 -val insts_var =
    1.52 -  Scan.optional (Scan.lift
    1.53 -    (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
    1.54 -    -- Attrib.thms;
    1.55 -
    1.56 -fun inst_args_var f src ctxt =
    1.57 -  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
    1.58 -
    1.59 -
    1.60  (* setup *)
    1.61  
    1.62  val _ = Context.>> (Context.map_theory
    1.63 -  (Method.add_methods
    1.64 -   [("rule_tac", inst_args_var res_inst_meth,
    1.65 -      "apply rule (dynamic instantiation)"),
    1.66 -    ("erule_tac", inst_args_var eres_inst_meth,
    1.67 -      "apply rule in elimination manner (dynamic instantiation)"),
    1.68 -    ("drule_tac", inst_args_var dres_inst_meth,
    1.69 -      "apply rule in destruct manner (dynamic instantiation)"),
    1.70 -    ("frule_tac", inst_args_var forw_inst_meth,
    1.71 -      "apply rule in forward manner (dynamic instantiation)"),
    1.72 -    ("cut_tac", inst_args_var cut_inst_meth,
    1.73 -      "cut rule (dynamic instantiation)"),
    1.74 -    ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name_source) subgoals_tac,
    1.75 -      "insert subgoal (dynamic instantiation)"),
    1.76 -    ("thin_tac", Method.goal_args_ctxt Args.name_source thin_tac,
    1.77 -      "remove premise (dynamic instantiation)")]));
    1.78 + (Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #>
    1.79 +  Method.setup (Binding.name "erule_tac") eres_inst_meth
    1.80 +    "apply rule in elimination manner (dynamic instantiation)" #>
    1.81 +  Method.setup (Binding.name "drule_tac") dres_inst_meth
    1.82 +    "apply rule in destruct manner (dynamic instantiation)" #>
    1.83 +  Method.setup (Binding.name "frule_tac") forw_inst_meth
    1.84 +    "apply rule in forward manner (dynamic instantiation)" #>
    1.85 +  Method.setup (Binding.name "cut_tac") cut_inst_meth "cut rule (dynamic instantiation)" #>
    1.86 +  Method.setup (Binding.name "subgoal_tac")
    1.87 +    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
    1.88 +      (fn (quant, props) => fn ctxt => SIMPLE_METHOD'' quant (subgoals_tac ctxt props)))
    1.89 +    "insert subgoal (dynamic instantiation)" #>
    1.90 +  Method.setup (Binding.name "thin_tac")
    1.91 +    (Args.goal_spec -- Scan.lift Args.name_source >>
    1.92 +      (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
    1.93 +      "remove premise (dynamic instantiation)"));
    1.94  
    1.95  end;
    1.96