equal
deleted
inserted
replaced
126 done |
126 done |
127 |
127 |
128 lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)" |
128 lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)" |
129 by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl) |
129 by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl) |
130 |
130 |
|
131 lemma trancl_power: |
|
132 "x \<in> r^+ = (\<exists>n > 0. x \<in> r^n)" |
|
133 apply (cases x) |
|
134 apply simp |
|
135 apply (rule iffI) |
|
136 apply (drule tranclD2) |
|
137 apply (clarsimp simp: rtrancl_is_UN_rel_pow) |
|
138 apply (rule_tac x="Suc x" in exI) |
|
139 apply (clarsimp simp: rel_comp_def) |
|
140 apply fastsimp |
|
141 apply clarsimp |
|
142 apply (case_tac n, simp) |
|
143 apply clarsimp |
|
144 apply (drule rel_pow_imp_rtrancl) |
|
145 apply fastsimp |
|
146 done |
131 |
147 |
132 lemma single_valued_rel_pow: |
148 lemma single_valued_rel_pow: |
133 "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)" |
149 "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)" |
134 apply (rule single_valuedI) |
150 apply (rule single_valuedI) |
135 apply (induct n) |
151 apply (induct n) |