# HG changeset patch
# User paulson
# Date 1061294060 -7200
# Node ID 76a6ba67bd15680f5aca48071fa65a94e068b421
# Parent  12f6f18e7afc96a096914f980c3b262b1d7c9fbe
new case_tac

diff -r 12f6f18e7afc -r 76a6ba67bd15 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Tue Aug 19 13:53:58 2003 +0200
+++ b/src/ZF/Cardinal.thy	Tue Aug 19 13:54:20 2003 +0200
@@ -267,8 +267,7 @@
 done
 
 lemma Ord_Least [intro,simp,TC]: "Ord(LEAST x. P(x))"
-apply (rule_tac P = "EX i. Ord(i) & P(i)" in case_split_thm)  
-    (*case_tac method not available yet; needs "inductive"*)
+apply (case_tac "\<exists>i. Ord(i) & P(i)")  
 apply safe
 apply (rule Least_le [THEN ltE])
 prefer 3 apply assumption+
@@ -380,7 +379,7 @@
 
 lemma Card_cardinal: "Card(|A|)"
 apply (unfold cardinal_def)
-apply (rule_tac P =  "EX i. Ord (i) & i \<approx> A" in case_split_thm)
+apply (case_tac "EX i. Ord (i) & i \<approx> A")
  txt{*degenerate case*}
  prefer 2 apply (erule Least_0 [THEN ssubst], rule Card_0)
 txt{*real case: A is isomorphic to some ordinal*}
@@ -790,7 +789,7 @@
 
 lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
 apply (unfold Finite_def)
-apply (rule_tac P =  "y:x" in case_split_thm)
+apply (case_tac "y:x")
 apply (simp add: cons_absorb)
 apply (erule bexE)
 apply (rule bexI)
@@ -974,7 +973,7 @@
 apply (blast intro: wf_onI)
 apply (rule wf_onI)
 apply (simp add: wf_on_def wf_def)
-apply (rule_tac P =  "x:Z" in case_split_thm)
+apply (case_tac "x:Z")
  txt{*x:Z case*}
  apply (drule_tac x = x in bspec, assumption)
  apply (blast elim: mem_irrefl mem_asym)
diff -r 12f6f18e7afc -r 76a6ba67bd15 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Tue Aug 19 13:53:58 2003 +0200
+++ b/src/ZF/Epsilon.thy	Tue Aug 19 13:54:20 2003 +0200
@@ -118,7 +118,7 @@
 apply (simp add: Transset_def) 
 apply (rule_tac a=x in eps_induct, clarify) 
 apply (drule bspec, assumption) 
-apply (rule_tac P = "x=0" in case_split_thm, auto)
+apply (case_tac "x=0", auto)
 done
 
 lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A";
diff -r 12f6f18e7afc -r 76a6ba67bd15 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Tue Aug 19 13:53:58 2003 +0200
+++ b/src/ZF/Nat.thy	Tue Aug 19 13:54:20 2003 +0200
@@ -217,11 +217,9 @@
 by (simp add: quasinat_def nat_case_def) 
 
 lemma nat_cases_disj: "k=0 | (\<exists>y. k = succ(y)) | ~ quasinat(k)"
-txt{*The @{text case_tac} method is not yet available.*}
-apply (rule_tac P = "k=0" in case_split_thm, simp) 
-apply (rule_tac P = "\<exists>m. k = succ(m)" in case_split_thm, simp) 
-apply simp 
-apply (simp add: quasinat_def) 
+apply (case_tac "k=0", simp) 
+apply (case_tac "\<exists>m. k = succ(m)") 
+apply (simp_all add: quasinat_def) 
 done
 
 lemma nat_cases:
diff -r 12f6f18e7afc -r 76a6ba67bd15 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Tue Aug 19 13:53:58 2003 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Tue Aug 19 13:54:20 2003 +0200
@@ -83,6 +83,8 @@
 
 
 (*Given a variable, find the inductive set associated it in the assumptions*)
+exception Find_tname of string
+
 fun find_tname var Bi =
   let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
              (v, #1 (dest_Const (head_of A)))
@@ -90,7 +92,7 @@
       val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
           (#2 (strip_context Bi))
   in case assoc (pairs, var) of
-       None => error ("Cannot determine datatype of " ^ quote var)
+       None => raise Find_tname ("Cannot determine datatype of " ^ quote var)
      | Some t => t
   end;
 
@@ -118,13 +120,16 @@
         String.substring (ind_vname, 1, size ind_vname-1)
   in
     eres_inst_tac [(vname',var)] rule i state
-  end;
+  end
+  handle Find_tname msg =>
+            if exh then (*try boolean case analysis instead*)
+		case_tac var i state
+            else error msg;
 
 val exhaust_tac = exhaust_induct_tac true;
 val induct_tac = exhaust_induct_tac false;
 
 
-
 (**** declare non-datatype as datatype ****)
 
 fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
@@ -201,8 +206,8 @@
   Method.add_methods
     [("induct_tac", Method.goal_args Args.name induct_tac,
       "induct_tac emulation (dynamic instantiation!)"),
-     ("case_tac", Method.goal_args Args.name case_tac,
-      "case_tac emulation (dynamic instantiation!)")]];
+     ("case_tac", Method.goal_args Args.name exhaust_tac,
+      "datatype case_tac emulation (dynamic instantiation!)")]];
 
 
 (* outer syntax *)
diff -r 12f6f18e7afc -r 76a6ba67bd15 src/ZF/func.thy
--- a/src/ZF/func.thy	Tue Aug 19 13:53:58 2003 +0200
+++ b/src/ZF/func.thy	Tue Aug 19 13:54:20 2003 +0200
@@ -462,7 +462,7 @@
 
 lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)"
 apply (simp add: update_def)
-apply (rule_tac P="z \<in> domain(f)" in case_split_thm)   
+apply (case_tac "z \<in> domain(f)")   
 apply (simp_all add: apply_0)
 done
 
diff -r 12f6f18e7afc -r 76a6ba67bd15 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Tue Aug 19 13:53:58 2003 +0200
+++ b/src/ZF/upair.thy	Tue Aug 19 13:54:20 2003 +0200
@@ -223,8 +223,7 @@
 
 lemma split_if [split]:
      "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
-(*no case_tac yet!*)
-by (rule_tac P=Q in case_split_thm, simp_all)
+by (case_tac Q, simp_all)
 
 (** Rewrite rules for boolean case-splitting: faster than 
 	addsplits[split_if]