# HG changeset patch
# User wenzelm
# Date 1204199788 -3600
# Node ID 9efd4c04eaa4664598aab9124e1bdfcbf7348015
# Parent  5cac519abe4ee424a4fe257f9398b2d83a7d64f4
rtranclE, tranclE: tuned statement, added case_names;

diff -r 5cac519abe4e -r 9efd4c04eaa4 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Feb 28 00:11:28 2008 +0100
+++ b/src/HOL/Transitive_Closure.thy	Thu Feb 28 12:56:28 2008 +0100
@@ -127,17 +127,17 @@
   shows "r^** x z" using yz xy
   by induct iprover+
 
-lemma rtranclE:
-  assumes major: "(a::'a,b) : r^*"
-    and cases: "(a = b) ==> P"
-      "!!y. [| (a,y) : r^*; (y,b) : r |] ==> P"
-  shows P
+lemma rtranclE [cases set: rtrancl]:
+  assumes major: "(a::'a, b) : r^*"
+  obtains
+    (base) "a = b"
+  | (step) y where "(a, y) : r^*" and "(y, b) : r"
   -- {* elimination of @{text rtrancl} -- by induction on a special formula *}
   apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
    apply (rule_tac [2] major [THEN rtrancl_induct])
     prefer 2 apply blast
    prefer 2 apply blast
-  apply (erule asm_rl exE disjE conjE cases)+
+  apply (erule asm_rl exE disjE conjE base step)+
   done
 
 lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s"
@@ -344,7 +344,12 @@
 
 lemmas trancl_trans_induct = tranclp_trans_induct [to_set]
 
-inductive_cases tranclE: "(a, b) : r^+"
+lemma tranclE [cases set: trancl]:
+  assumes "(a, b) : r^+"
+  obtains
+    (base) "(a, b) : r"
+  | (step) c where "(a, c) : r^+" and "(c, b) : r"
+  using assms by cases simp_all
 
 lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
   apply (rule subsetI)
@@ -575,12 +580,6 @@
 
 declare trancl_into_rtrancl [elim]
 
-declare rtranclE [cases set: rtrancl]
-declare tranclE [cases set: trancl]
-
-
-
-
 
 subsection {* Setup of transitivity reasoner *}