equal
deleted
inserted
replaced
171 lemma converse_rtranclp_into_rtranclp: "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c" |
171 lemma converse_rtranclp_into_rtranclp: "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c" |
172 by (rule rtranclp_trans) iprover+ |
172 by (rule rtranclp_trans) iprover+ |
173 |
173 |
174 lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set] |
174 lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set] |
175 |
175 |
176 text \<open>\<^medskip> More @{term "r\<^sup>*"} equations and inclusions.\<close> |
176 text \<open>\<^medskip> More \<^term>\<open>r\<^sup>*\<close> equations and inclusions.\<close> |
177 |
177 |
178 lemma rtranclp_idemp [simp]: "(r\<^sup>*\<^sup>*)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" |
178 lemma rtranclp_idemp [simp]: "(r\<^sup>*\<^sup>*)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" |
179 apply (auto intro!: order_antisym) |
179 apply (auto intro!: order_antisym) |
180 apply (erule rtranclp_induct) |
180 apply (erule rtranclp_induct) |
181 apply (rule rtranclp.rtrancl_refl) |
181 apply (rule rtranclp.rtrancl_refl) |
389 done |
389 done |
390 |
390 |
391 lemma trancl_unfold: "r\<^sup>+ = r \<union> r\<^sup>+ O r" |
391 lemma trancl_unfold: "r\<^sup>+ = r \<union> r\<^sup>+ O r" |
392 by (auto intro: trancl_into_trancl elim: tranclE) |
392 by (auto intro: trancl_into_trancl elim: tranclE) |
393 |
393 |
394 text \<open>Transitivity of @{term "r\<^sup>+"}\<close> |
394 text \<open>Transitivity of \<^term>\<open>r\<^sup>+\<close>\<close> |
395 lemma trans_trancl [simp]: "trans (r\<^sup>+)" |
395 lemma trans_trancl [simp]: "trans (r\<^sup>+)" |
396 proof (rule transI) |
396 proof (rule transI) |
397 fix x y z |
397 fix x y z |
398 assume "(x, y) \<in> r\<^sup>+" |
398 assume "(x, y) \<in> r\<^sup>+" |
399 assume "(y, z) \<in> r\<^sup>+" |
399 assume "(y, z) \<in> r\<^sup>+" |
1224 val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl}; |
1224 val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl}; |
1225 val rtrancl_trans = @{thm rtrancl_trans}; |
1225 val rtrancl_trans = @{thm rtrancl_trans}; |
1226 |
1226 |
1227 fun decomp (@{const Trueprop} $ t) = |
1227 fun decomp (@{const Trueprop} $ t) = |
1228 let |
1228 let |
1229 fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel) = |
1229 fun dec (Const (\<^const_name>\<open>Set.member\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ a $ b) $ rel) = |
1230 let |
1230 let |
1231 fun decr (Const (@{const_name rtrancl}, _ ) $ r) = (r,"r*") |
1231 fun decr (Const (\<^const_name>\<open>rtrancl\<close>, _ ) $ r) = (r,"r*") |
1232 | decr (Const (@{const_name trancl}, _ ) $ r) = (r,"r+") |
1232 | decr (Const (\<^const_name>\<open>trancl\<close>, _ ) $ r) = (r,"r+") |
1233 | decr r = (r,"r"); |
1233 | decr r = (r,"r"); |
1234 val (rel,r) = decr (Envir.beta_eta_contract rel); |
1234 val (rel,r) = decr (Envir.beta_eta_contract rel); |
1235 in SOME (a,b,rel,r) end |
1235 in SOME (a,b,rel,r) end |
1236 | dec _ = NONE |
1236 | dec _ = NONE |
1237 in dec t end |
1237 in dec t end |
1251 |
1251 |
1252 fun decomp (@{const Trueprop} $ t) = |
1252 fun decomp (@{const Trueprop} $ t) = |
1253 let |
1253 let |
1254 fun dec (rel $ a $ b) = |
1254 fun dec (rel $ a $ b) = |
1255 let |
1255 let |
1256 fun decr (Const (@{const_name rtranclp}, _ ) $ r) = (r,"r*") |
1256 fun decr (Const (\<^const_name>\<open>rtranclp\<close>, _ ) $ r) = (r,"r*") |
1257 | decr (Const (@{const_name tranclp}, _ ) $ r) = (r,"r+") |
1257 | decr (Const (\<^const_name>\<open>tranclp\<close>, _ ) $ r) = (r,"r+") |
1258 | decr r = (r,"r"); |
1258 | decr r = (r,"r"); |
1259 val (rel,r) = decr rel; |
1259 val (rel,r) = decr rel; |
1260 in SOME (a, b, rel, r) end |
1260 in SOME (a, b, rel, r) end |
1261 | dec _ = NONE |
1261 | dec _ = NONE |
1262 in dec t end |
1262 in dec t end |