# HG changeset patch
# User wenzelm
# Date 1213118119 -7200
# Node ID 3ede9103de8e32d8d5306d762a43a25b5b2bacf1
# Parent  0733f575b51e9c6c1ec30766fd03a6ea4cf7c73c
eliminated obsolete case_split_thm -- use case_split;
added case_split_tac (works without context);
setup for induct_tacs.ML;

diff -r 0733f575b51e -r 3ede9103de8e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jun 10 19:15:18 2008 +0200
+++ b/src/HOL/HOL.thy	Tue Jun 10 19:15:19 2008 +0200
@@ -25,6 +25,7 @@
   "~~/src/Tools/random_word.ML"
   "~~/src/Tools/atomize_elim.ML"
   "~~/src/Tools/induct.ML"
+  ("~~/src/HOL/Tools/induct_tacs.ML")
   "~~/src/Tools/code/code_name.ML"
   "~~/src/Tools/code/code_funcgr.ML"
   "~~/src/Tools/code/code_thingol.ML"
@@ -721,7 +722,7 @@
   case distinction as a natural deduction rule.
   Note that @{term "~P"} is the second case, not the first
 *}
-lemma case_split_thm:
+lemma case_split [case_names True False]:
   assumes prem1: "P ==> Q"
       and prem2: "~P ==> Q"
   shows "Q"
@@ -729,7 +730,10 @@
 apply (erule prem2)
 apply (erule prem1)
 done
-lemmas case_split = case_split_thm [case_names True False]
+
+ML {*
+  fun case_split_tac P = res_inst_tac [("P", P)] @{thm case_split}
+*}
 
 (*Classical implies (-->) elimination. *)
 lemma impCE:
@@ -1487,9 +1491,9 @@
 ML {*
 structure ProjectRule = ProjectRuleFun
 (
-  val conjunct1 = @{thm conjunct1};
-  val conjunct2 = @{thm conjunct2};
-  val mp = @{thm mp};
+  val conjunct1 = @{thm conjunct1}
+  val conjunct2 = @{thm conjunct2}
+  val mp = @{thm mp}
 )
 *}
 
@@ -1543,17 +1547,20 @@
 text {* Method setup. *}
 
 ML {*
-  structure Induct = InductFun
-  (
-    val cases_default = @{thm case_split}
-    val atomize = @{thms induct_atomize}
-    val rulify = @{thms induct_rulify}
-    val rulify_fallback = @{thms induct_rulify_fallback}
-  );
+structure Induct = InductFun
+(
+  val cases_default = @{thm case_split}
+  val atomize = @{thms induct_atomize}
+  val rulify = @{thms induct_rulify}
+  val rulify_fallback = @{thms induct_rulify_fallback}
+)
 *}
 
 setup Induct.setup
 
+use "~~/src/HOL/Tools/induct_tacs.ML"
+setup InductTacs.setup
+
 
 subsection {* Other simple lemmas and lemma duplicates *}
 
@@ -1578,7 +1585,7 @@
   apply (erule_tac x = "%z. if z = x then y else f z" in allE)
   apply (erule impE)
   apply (rule allI)
-  apply (rule_tac P = "xa = x" in case_split_thm)
+  apply (case_tac "xa = x")
   apply (drule_tac [3] x = x in fun_cong, simp_all)
   done
 
@@ -1735,7 +1742,6 @@
 val all_simps = thms "all_simps";
 val atomize_not = thm "atomize_not";
 val case_split = thm "case_split";
-val case_split_thm = thm "case_split_thm"
 val cases_simp = thm "cases_simp";
 val choice_eq = thm "choice_eq"
 val cong = thm "cong"