setup [trans] rules for calculational Isar reasoning
authorkleing
Sun Dec 09 14:34:18 2001 +0100 (2001-12-09)
changeset 12428f3033eed309a
parent 12427 37cfec8dfe8e
child 12429 15c13bdc94c8
setup [trans] rules for calculational Isar reasoning
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Transitive_Closure.thy	Sat Dec 08 17:34:46 2001 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Sun Dec 09 14:34:18 2001 +0100
     1.3 @@ -95,6 +95,36 @@
     1.4   apply (auto)
     1.5   by (erule rev_mp, erule rtrancl_induct, auto)
     1.6  
     1.7 +(* more about converse rtrancl and trancl, should be merged with main body *)
     1.8 +
     1.9 +lemma converse_rtrancl_into_rtrancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R^* \<Longrightarrow> (a,c) \<in> R^*"
    1.10 +  by (erule rtrancl_induct) (fast intro: rtrancl_into_rtrancl)+
    1.11 +
    1.12 +lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+"
    1.13 +  by (fast intro: trancl_trans)
    1.14 +
    1.15 +lemma trancl_into_trancl [rule_format]:
    1.16 +  "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r \<longrightarrow> (a,c) \<in> r\<^sup>+"
    1.17 +  apply (erule trancl_induct)   
    1.18 +   apply (fast intro: r_r_into_trancl)
    1.19 +  apply (fast intro: r_r_into_trancl trancl_trans)
    1.20 +  done
    1.21 +
    1.22 +lemma trancl_rtrancl_trancl:
    1.23 +  "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r\<^sup>* \<Longrightarrow> (a,c) \<in> r\<^sup>+"
    1.24 +  apply (drule tranclD)
    1.25 +  apply (erule exE, erule conjE)
    1.26 +  apply (drule rtrancl_trans, assumption)
    1.27 +  apply (drule rtrancl_into_trancl2, assumption)
    1.28 +  apply assumption
    1.29 +  done
    1.30 +
    1.31 +lemmas [trans] = r_r_into_trancl trancl_trans rtrancl_trans 
    1.32 +                 trancl_into_trancl trancl_into_trancl2
    1.33 +                 rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
    1.34 +                 rtrancl_trancl_trancl trancl_rtrancl_trancl
    1.35 +
    1.36 +declare trancl_into_rtrancl [elim]
    1.37  
    1.38  declare rtrancl_induct [induct set: rtrancl]
    1.39  declare rtranclE [cases set: rtrancl]