# HG changeset patch
# User wenzelm
# Date 1213478407 -7200
# Node ID b43785a81e0112d702d106865bb941f2d3cfc756
# Parent  0978b8e32fd0395d3fcfd72d2bff623f8906508e
simplified InductTacs.case_tac/induct_tac;

diff -r 0978b8e32fd0 -r b43785a81e01 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Jun 14 23:20:06 2008 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Jun 14 23:20:07 2008 +0200
@@ -247,7 +247,7 @@
        THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
 
 -- "for if"
-apply( tactic {* (case_split_tac "the_Bool v" THEN_ALL_NEW
+apply( tactic {* (InductTacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
   (asm_full_simp_tac @{simpset})) 7*})
 
 apply (tactic "forward_hyp_tac")
diff -r 0978b8e32fd0 -r b43785a81e01 src/HOL/Tools/induct_tacs.ML
--- a/src/HOL/Tools/induct_tacs.ML	Sat Jun 14 23:20:06 2008 +0200
+++ b/src/HOL/Tools/induct_tacs.ML	Sat Jun 14 23:20:07 2008 +0200
@@ -7,8 +7,10 @@
 
 signature INDUCT_TACS =
 sig
-  val case_tac: Proof.context -> string * thm option -> int -> tactic
-  val induct_tac: Proof.context -> string option list list * thm option -> int -> tactic
+  val case_tac: Proof.context -> string -> int -> tactic
+  val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
+  val induct_tac: Proof.context -> string option list list -> int -> tactic
+  val induct_rule_tac: Proof.context -> string option list list -> thm -> int -> tactic
   val setup: theory -> theory
 end
 
@@ -25,7 +27,7 @@
       error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
   in U end;
 
-fun case_tac ctxt0 (s, opt_rule) i st =
+fun gen_case_tac ctxt0 (s, opt_rule) i st =
   let
     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
     val rule =
@@ -45,6 +47,9 @@
   in RuleInsts.res_inst_tac ctxt [(xi, s)] rule i st end
   handle THM _ => Seq.empty;
 
+fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
+fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
+
 
 (* induction *)
 
@@ -59,7 +64,7 @@
 
 in
 
-fun induct_tac ctxt0 (varss, opt_rule) i st =
+fun gen_induct_tac ctxt0 (varss, opt_rule) i st =
   let
     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
     val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
@@ -100,6 +105,9 @@
 
 end;
 
+fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE);
+fun induct_rule_tac ctxt args rule = gen_induct_tac ctxt (args, SOME rule);
+
 
 (* method syntax *)
 
@@ -115,9 +123,9 @@
 
 val setup =
   Method.add_methods
-   [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) case_tac,
+   [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) gen_case_tac,
       "unstructured case analysis on types"),
-    ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rule) induct_tac,
+    ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rule) gen_induct_tac,
       "unstructured induction on types")];
 
 end;