src/HOL/Transitive_Closure.thy
changeset 22080 7bf8868ab3e4
parent 21589 1b02201d7195
child 22172 e7d6cb237b5e
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Jan 17 09:52:54 2007 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Jan 17 09:53:50 2007 +0100
     1.3 @@ -108,6 +108,12 @@
     1.4    apply (erule asm_rl exE disjE conjE cases)+
     1.5    done
     1.6  
     1.7 +lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s"
     1.8 +  apply (rule subsetI)
     1.9 +  apply (rule_tac p="x" in PairE, clarify)
    1.10 +  apply (erule rtrancl_induct, auto) 
    1.11 +  done
    1.12 +
    1.13  lemma converse_rtrancl_into_rtrancl:
    1.14    "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
    1.15    by (rule rtrancl_trans) iprover+
    1.16 @@ -263,6 +269,12 @@
    1.17  
    1.18  inductive_cases tranclE: "(a, b) : r^+"
    1.19  
    1.20 +lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
    1.21 +  apply (rule subsetI)
    1.22 +  apply (rule_tac p="x" in PairE, clarify)
    1.23 +  apply (erule trancl_induct, auto) 
    1.24 +  done
    1.25 +
    1.26  lemma trancl_unfold: "r^+ = r Un r O r^+"
    1.27    by (auto intro: trancl_into_trancl elim: tranclE)
    1.28