equal
deleted
inserted
replaced
772 lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n" |
772 lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n" |
773 by(induct n) auto |
773 by(induct n) auto |
774 |
774 |
775 lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R" |
775 lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R" |
776 by (induct n) (simp, simp add: O_assoc [symmetric]) |
776 by (induct n) (simp, simp add: O_assoc [symmetric]) |
|
777 |
|
778 lemma rel_pow_empty: |
|
779 "0 < n ==> ({} :: 'a * 'a => bool) ^^ n = {}" |
|
780 by (cases n) auto |
777 |
781 |
778 lemma rtrancl_imp_UN_rel_pow: |
782 lemma rtrancl_imp_UN_rel_pow: |
779 assumes "p \<in> R^*" |
783 assumes "p \<in> R^*" |
780 shows "p \<in> (\<Union>n. R ^^ n)" |
784 shows "p \<in> (\<Union>n. R ^^ n)" |
781 proof (cases p) |
785 proof (cases p) |