equal
deleted
inserted
replaced
80 |
80 |
81 |
81 |
82 subsection {* Reflexive-transitive closure *} |
82 subsection {* Reflexive-transitive closure *} |
83 |
83 |
84 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)" |
84 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)" |
85 by (auto simp add: expand_fun_eq) |
85 by (auto simp add: ext_iff) |
86 |
86 |
87 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*" |
87 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*" |
88 -- {* @{text rtrancl} of @{text r} contains @{text r} *} |
88 -- {* @{text rtrancl} of @{text r} contains @{text r} *} |
89 apply (simp only: split_tupled_all) |
89 apply (simp only: split_tupled_all) |
90 apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) |
90 apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) |
485 done |
485 done |
486 |
486 |
487 lemmas trancl_converseD = tranclp_converseD [to_set] |
487 lemmas trancl_converseD = tranclp_converseD [to_set] |
488 |
488 |
489 lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1" |
489 lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1" |
490 by (fastsimp simp add: expand_fun_eq |
490 by (fastsimp simp add: ext_iff |
491 intro!: tranclp_converseI dest!: tranclp_converseD) |
491 intro!: tranclp_converseI dest!: tranclp_converseD) |
492 |
492 |
493 lemmas trancl_converse = tranclp_converse [to_set] |
493 lemmas trancl_converse = tranclp_converse [to_set] |
494 |
494 |
495 lemma sym_trancl: "sym r ==> sym (r^+)" |
495 lemma sym_trancl: "sym r ==> sym (r^+)" |