src/HOL/Relation_Power.thy
changeset 25295 12985023be5e
parent 24996 ebd5f4cc7118
child 25861 494d9301cc75
     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)"