# HG changeset patch # User kleing # Date 1194299317 -3600 # Node ID 12985023be5e43f742d5c8af4308736b30b92e53 # Parent 437d3a414bfa5f7c7803cea2d69871d6db99173d tranclD2 (tranclD at the other end) + trancl_power diff -r 437d3a414bfa -r 12985023be5e src/HOL/Relation_Power.thy --- a/src/HOL/Relation_Power.thy Mon Nov 05 22:00:21 2007 +0100 +++ b/src/HOL/Relation_Power.thy Mon Nov 05 22:48:37 2007 +0100 @@ -128,6 +128,22 @@ lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)" by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl) +lemma trancl_power: + "x \ r^+ = (\n > 0. x \ r^n)" + apply (cases x) + apply simp + apply (rule iffI) + apply (drule tranclD2) + apply (clarsimp simp: rtrancl_is_UN_rel_pow) + apply (rule_tac x="Suc x" in exI) + apply (clarsimp simp: rel_comp_def) + apply fastsimp + apply clarsimp + apply (case_tac n, simp) + apply clarsimp + apply (drule rel_pow_imp_rtrancl) + apply fastsimp + done lemma single_valued_rel_pow: "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)" diff -r 437d3a414bfa -r 12985023be5e src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Mon Nov 05 22:00:21 2007 +0100 +++ b/src/HOL/Transitive_Closure.thy Mon Nov 05 22:48:37 2007 +0100 @@ -449,6 +449,10 @@ lemmas tranclD = tranclpD [to_set] +lemma tranclD2: + "(x, y) \ R\<^sup>+ \ \z. (x, z) \ R\<^sup>* \ (z, y) \ R" + by (blast elim: tranclE intro: trancl_into_rtrancl) + lemma irrefl_tranclI: "r^-1 \ r^* = {} ==> (x, x) \ r^+" by (blast elim: tranclE dest: trancl_into_rtrancl)