src/HOL/Transitive_Closure.thy
 changeset 26174 9efd4c04eaa4 parent 25425 9191942c4ead child 26179 bc5d582d6cfe
```     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Feb 28 00:11:28 2008 +0100
1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Feb 28 12:56:28 2008 +0100
1.3 @@ -127,17 +127,17 @@
1.4    shows "r^** x z" using yz xy
1.5    by induct iprover+
1.6
1.7 -lemma rtranclE:
1.8 -  assumes major: "(a::'a,b) : r^*"
1.9 -    and cases: "(a = b) ==> P"
1.10 -      "!!y. [| (a,y) : r^*; (y,b) : r |] ==> P"
1.11 -  shows P
1.12 +lemma rtranclE [cases set: rtrancl]:
1.13 +  assumes major: "(a::'a, b) : r^*"
1.14 +  obtains
1.15 +    (base) "a = b"
1.16 +  | (step) y where "(a, y) : r^*" and "(y, b) : r"
1.17    -- {* elimination of @{text rtrancl} -- by induction on a special formula *}
1.18    apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
1.19     apply (rule_tac [2] major [THEN rtrancl_induct])
1.20      prefer 2 apply blast
1.21     prefer 2 apply blast
1.22 -  apply (erule asm_rl exE disjE conjE cases)+
1.23 +  apply (erule asm_rl exE disjE conjE base step)+
1.24    done
1.25
1.26  lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s"
1.27 @@ -344,7 +344,12 @@
1.28
1.29  lemmas trancl_trans_induct = tranclp_trans_induct [to_set]
1.30
1.31 -inductive_cases tranclE: "(a, b) : r^+"
1.32 +lemma tranclE [cases set: trancl]:
1.33 +  assumes "(a, b) : r^+"
1.34 +  obtains
1.35 +    (base) "(a, b) : r"
1.36 +  | (step) c where "(a, c) : r^+" and "(c, b) : r"
1.37 +  using assms by cases simp_all
1.38
1.39  lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
1.40    apply (rule subsetI)
1.41 @@ -575,12 +580,6 @@
1.42
1.43  declare trancl_into_rtrancl [elim]
1.44
1.45 -declare rtranclE [cases set: rtrancl]
1.46 -declare tranclE [cases set: trancl]
1.47 -
1.48 -
1.49 -
1.50 -
1.51
1.52  subsection {* Setup of transitivity reasoner *}
1.53
```