tranclD2 (tranclD at the other end) + trancl_power
authorkleing
Mon Nov 05 22:48:37 2007 +0100 (2007-11-05)
changeset 2529512985023be5e
parent 25294 437d3a414bfa
child 25296 c187b7422156
tranclD2 (tranclD at the other end) + trancl_power
src/HOL/Relation_Power.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Relation_Power.thy	Mon Nov 05 22:00:21 2007 +0100
     1.2 +++ b/src/HOL/Relation_Power.thy	Mon Nov 05 22:48:37 2007 +0100
     1.3 @@ -128,6 +128,22 @@
     1.4  lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
     1.5    by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
     1.6  
     1.7 +lemma trancl_power:
     1.8 +  "x \<in> r^+ = (\<exists>n > 0. x \<in> r^n)"
     1.9 +  apply (cases x)
    1.10 +  apply simp
    1.11 +  apply (rule iffI)
    1.12 +   apply (drule tranclD2)
    1.13 +   apply (clarsimp simp: rtrancl_is_UN_rel_pow)
    1.14 +   apply (rule_tac x="Suc x" in exI)
    1.15 +   apply (clarsimp simp: rel_comp_def)
    1.16 +   apply fastsimp
    1.17 +  apply clarsimp
    1.18 +  apply (case_tac n, simp)
    1.19 +  apply clarsimp
    1.20 +  apply (drule rel_pow_imp_rtrancl)
    1.21 +  apply fastsimp
    1.22 +  done
    1.23  
    1.24  lemma single_valued_rel_pow:
    1.25      "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
     2.1 --- a/src/HOL/Transitive_Closure.thy	Mon Nov 05 22:00:21 2007 +0100
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Nov 05 22:48:37 2007 +0100
     2.3 @@ -449,6 +449,10 @@
     2.4  
     2.5  lemmas tranclD = tranclpD [to_set]
     2.6  
     2.7 +lemma tranclD2:
     2.8 +  "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R"
     2.9 +  by (blast elim: tranclE intro: trancl_into_rtrancl)
    2.10 +
    2.11  lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
    2.12    by (blast elim: tranclE dest: trancl_into_rtrancl)
    2.13