1.1 --- a/src/HOL/HOL.thy Tue Jun 10 19:15:18 2008 +0200
1.2 +++ b/src/HOL/HOL.thy Tue Jun 10 19:15:19 2008 +0200
1.3 @@ -25,6 +25,7 @@
1.4 "~~/src/Tools/random_word.ML"
1.5 "~~/src/Tools/atomize_elim.ML"
1.6 "~~/src/Tools/induct.ML"
1.7 + ("~~/src/HOL/Tools/induct_tacs.ML")
1.8 "~~/src/Tools/code/code_name.ML"
1.9 "~~/src/Tools/code/code_funcgr.ML"
1.10 "~~/src/Tools/code/code_thingol.ML"
1.11 @@ -721,7 +722,7 @@
1.12 case distinction as a natural deduction rule.
1.13 Note that @{term "~P"} is the second case, not the first
1.14 *}
1.15 -lemma case_split_thm:
1.16 +lemma case_split [case_names True False]:
1.17 assumes prem1: "P ==> Q"
1.18 and prem2: "~P ==> Q"
1.19 shows "Q"
1.20 @@ -729,7 +730,10 @@
1.21 apply (erule prem2)
1.22 apply (erule prem1)
1.23 done
1.24 -lemmas case_split = case_split_thm [case_names True False]
1.25 +
1.26 +ML {*
1.27 + fun case_split_tac P = res_inst_tac [("P", P)] @{thm case_split}
1.28 +*}
1.29
1.30 (*Classical implies (-->) elimination. *)
1.31 lemma impCE:
1.32 @@ -1487,9 +1491,9 @@
1.33 ML {*
1.34 structure ProjectRule = ProjectRuleFun
1.35 (
1.36 - val conjunct1 = @{thm conjunct1};
1.37 - val conjunct2 = @{thm conjunct2};
1.38 - val mp = @{thm mp};
1.39 + val conjunct1 = @{thm conjunct1}
1.40 + val conjunct2 = @{thm conjunct2}
1.41 + val mp = @{thm mp}
1.42 )
1.43 *}
1.44
1.45 @@ -1543,17 +1547,20 @@
1.46 text {* Method setup. *}
1.47
1.48 ML {*
1.49 - structure Induct = InductFun
1.50 - (
1.51 - val cases_default = @{thm case_split}
1.52 - val atomize = @{thms induct_atomize}
1.53 - val rulify = @{thms induct_rulify}
1.54 - val rulify_fallback = @{thms induct_rulify_fallback}
1.55 - );
1.56 +structure Induct = InductFun
1.57 +(
1.58 + val cases_default = @{thm case_split}
1.59 + val atomize = @{thms induct_atomize}
1.60 + val rulify = @{thms induct_rulify}
1.61 + val rulify_fallback = @{thms induct_rulify_fallback}
1.62 +)
1.63 *}
1.64
1.65 setup Induct.setup
1.66
1.67 +use "~~/src/HOL/Tools/induct_tacs.ML"
1.68 +setup InductTacs.setup
1.69 +
1.70
1.71 subsection {* Other simple lemmas and lemma duplicates *}
1.72
1.73 @@ -1578,7 +1585,7 @@
1.74 apply (erule_tac x = "%z. if z = x then y else f z" in allE)
1.75 apply (erule impE)
1.76 apply (rule allI)
1.77 - apply (rule_tac P = "xa = x" in case_split_thm)
1.78 + apply (case_tac "xa = x")
1.79 apply (drule_tac [3] x = x in fun_cong, simp_all)
1.80 done
1.81
1.82 @@ -1735,7 +1742,6 @@
1.83 val all_simps = thms "all_simps";
1.84 val atomize_not = thm "atomize_not";
1.85 val case_split = thm "case_split";
1.86 -val case_split_thm = thm "case_split_thm"
1.87 val cases_simp = thm "cases_simp";
1.88 val choice_eq = thm "choice_eq"
1.89 val cong = thm "cong"