rtranclE, tranclE: tuned statement, added case_names;
authorwenzelm
Thu Feb 28 12:56:28 2008 +0100 (2008-02-28)
changeset 261749efd4c04eaa4
parent 26173 5cac519abe4e
child 26175 11e338832c31
rtranclE, tranclE: tuned statement, added case_names;
src/HOL/Transitive_Closure.thy
     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