1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Apr 05 21:02:31 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Apr 05 21:05:20 2000 +0200
     1.3 @@ -169,46 +169,65 @@
     1.4  
     1.5  (* generic induction tactic for datatypes *)
     1.6  
     1.7 -fun induct_tac s i state =
     1.8 +fun gen_induct_tac (vars, opt_rule) i state =
     1.9    let
    1.10 -    val vars = Syntax.read_idents s;
    1.11      val (_, _, Bi, _) = dest_state (state, i);
    1.12      val {sign, ...} = rep_thm state;
    1.13 -    val tn = find_tname (hd vars) Bi;
    1.14 -    val {induction, ...} = datatype_info_sg_err sign tn;
    1.15 +    val (rule, rule_name) =
    1.16 +      (case opt_rule of
    1.17 +        Some r => (r, "Induction rule")
    1.18 +      | None =>
    1.19 +          let val tn = find_tname (hd vars) Bi
    1.20 +          in (#induction (datatype_info_sg_err sign tn), "Induction rule for type " ^ tn) end);
    1.21      val ind_vnames = map (fn (_ $ Var (ixn, _)) =>
    1.22        implode (tl (explode (Syntax.string_of_vname ixn))))
    1.23 -        (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induction)));
    1.24 +        (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of rule)));
    1.25      val insts = (ind_vnames ~~ vars) handle LIST _ =>
    1.26 -      error ("Induction rule for type " ^ tn ^ " has different number of variables")
    1.27 -  in
    1.28 -    occs_in_prems (res_inst_tac insts induction) vars i state
    1.29 -  end;
    1.30 +      error (rule_name ^ " has different number of variables");
    1.31 +  in occs_in_prems (Tactic.res_inst_tac insts rule) vars i state end;
    1.32 +
    1.33 +fun induct_tac s = gen_induct_tac (Syntax.read_idents s, None);
    1.34  
    1.35  
    1.36  (* generic case tactic for datatypes *)
    1.37  
    1.38 -fun case_tac aterm i state =
    1.39 -  let val name = infer_tname state i aterm in
    1.40 -    if name = HOLogic.boolN then res_inst_tac [("P", aterm)] case_split_thm i state
    1.41 -    else
    1.42 -      let
    1.43 -        val {exhaustion, ...} = datatype_info_sg_err (Thm.sign_of_thm state) name;
    1.44 -        val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
    1.45 -          (hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))));
    1.46 -        val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
    1.47 -      in res_inst_tac [(exh_vname, aterm)] exhaustion i state end
    1.48 -  end;
    1.49 +fun case_inst_tac t rule i state =
    1.50 +  let
    1.51 +    val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
    1.52 +      (hd (Logic.strip_assums_hyp (hd (Thm.prems_of rule))));
    1.53 +    val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)));
    1.54 +  in Tactic.res_inst_tac [(exh_vname, t)] rule i state end;
    1.55 +
    1.56 +fun gen_case_tac (t, Some rule) i state = case_inst_tac t rule i state
    1.57 +  | gen_case_tac (t, None) i state =
    1.58 +      let val tn = infer_tname state i t in
    1.59 +        if tn = HOLogic.boolN then Tactic.res_inst_tac [("P", t)] case_split_thm i state
    1.60 +        else case_inst_tac t (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn)) i state
    1.61 +      end;
    1.62 +
    1.63 +fun case_tac t = gen_case_tac (t, None);
    1.64 +
    1.65  
    1.66  
    1.67  (** Isar tactic emulations **)
    1.68  
    1.69 -fun tactic_syntax tac = #2 oo Method.syntax (Args.goal_spec HEADGOAL -- Scan.lift Args.name >>
    1.70 -  (fn (quant, s) => Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac s))));
    1.71 +local
    1.72 +
    1.73 +val rule_spec = Scan.option (Scan.lift (Args.$$$ "rule" -- Args.$$$ ":") |-- Attrib.local_thm);
    1.74 +
    1.75 +fun tactic_syntax args tac =
    1.76 +  #2 oo Method.syntax (Args.goal_spec HEADGOAL -- (Scan.lift args -- rule_spec) >>
    1.77 +    (fn (quant, x) => Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac x))));
    1.78 +
    1.79 +in
    1.80  
    1.81  val tactic_emulations =
    1.82 - [("induct_tac", tactic_syntax induct_tac, "induct_tac emulation (dynamic instantiation!)"),
    1.83 -  ("case_tac", tactic_syntax case_tac, "case_tac emulation (dynamic instantiation!)")];
    1.84 + [("induct_tac", tactic_syntax (Scan.repeat1 Args.name) gen_induct_tac,
    1.85 +    "induct_tac emulation (dynamic instantiation!)"),
    1.86 +  ("case_tac", tactic_syntax Args.name gen_case_tac,
    1.87 +    "case_tac emulation (dynamic instantiation!)")];
    1.88 +
    1.89 +end;
    1.90  
    1.91  
    1.92  
    1.93 @@ -253,7 +272,8 @@
    1.94        | proj i n thm =
    1.95            (if i + 1 < n then (fn th => th RS conjunct1) else I)
    1.96              (Library.funpow i (fn th => th RS conjunct2) thm)
    1.97 -          |> Drule.standard;
    1.98 +          |> Drule.standard
    1.99 +          |> RuleCases.name (RuleCases.get thm);
   1.100  
   1.101      fun add (ths, (name, {index, descr, induction, exhaustion, ...}: datatype_info)) =
   1.102        (("", proj index (length descr) induction), [InductMethod.induct_type_global name]) ::