src/HOL/Transitive_Closure.thy
changeset 47433 07f4bf913230
parent 47202 69cee87927f0
child 47492 2631a12fb2d1
     1.1 --- a/src/HOL/Transitive_Closure.thy	Tue Apr 03 08:55:06 2012 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Apr 03 17:26:30 2012 +0900
     1.3 @@ -726,7 +726,7 @@
     1.4  lemma relpowp_relpow_eq [pred_set_conv]:
     1.5    fixes R :: "'a rel"
     1.6    shows "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"
     1.7 -  by (induct n) (simp_all add: rel_compp_rel_comp_eq)
     1.8 +  by (induct n) (simp_all add: relcompp_relcomp_eq)
     1.9  
    1.10  text {* for code generation *}
    1.11  
    1.12 @@ -849,7 +849,7 @@
    1.13     apply (drule tranclD2)
    1.14     apply (clarsimp simp: rtrancl_is_UN_relpow)
    1.15     apply (rule_tac x="Suc n" in exI)
    1.16 -   apply (clarsimp simp: rel_comp_unfold)
    1.17 +   apply (clarsimp simp: relcomp_unfold)
    1.18     apply fastforce
    1.19    apply clarsimp
    1.20    apply (case_tac n, simp)
    1.21 @@ -870,7 +870,7 @@
    1.22  next
    1.23    case (Suc n)
    1.24    show ?case
    1.25 -  proof (simp add: rel_comp_unfold Suc)
    1.26 +  proof (simp add: relcomp_unfold Suc)
    1.27      show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R)
    1.28       = (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))"
    1.29      (is "?l = ?r")
    1.30 @@ -979,7 +979,7 @@
    1.31  apply(auto dest: relpow_finite_bounded1)
    1.32  done
    1.33  
    1.34 -lemma finite_rel_comp[simp,intro]:
    1.35 +lemma finite_relcomp[simp,intro]:
    1.36  assumes "finite R" and "finite S"
    1.37  shows "finite(R O S)"
    1.38  proof-