equal
deleted
inserted
replaced
59 tranclp ("(_\<^sup>+\<^sup>+)" [1000] 1000) and |
59 tranclp ("(_\<^sup>+\<^sup>+)" [1000] 1000) and |
60 reflclp ("(_\<^sup>=\<^sup>=)" [1000] 1000) and |
60 reflclp ("(_\<^sup>=\<^sup>=)" [1000] 1000) and |
61 rtrancl ("(_\<^sup>*)" [1000] 999) and |
61 rtrancl ("(_\<^sup>*)" [1000] 999) and |
62 trancl ("(_\<^sup>+)" [1000] 999) and |
62 trancl ("(_\<^sup>+)" [1000] 999) and |
63 reflcl ("(_\<^sup>=)" [1000] 999) |
63 reflcl ("(_\<^sup>=)" [1000] 999) |
|
64 |
|
65 |
|
66 subsection {* Reflexive closure *} |
|
67 |
|
68 lemma reflexive_reflcl[simp]: "reflexive(r^=)" |
|
69 by(simp add:refl_def) |
|
70 |
|
71 lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r" |
|
72 by(simp add:antisym_def) |
|
73 |
|
74 lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans(r^=)" |
|
75 unfolding trans_def by blast |
64 |
76 |
65 |
77 |
66 subsection {* Reflexive-transitive closure *} |
78 subsection {* Reflexive-transitive closure *} |
67 |
79 |
68 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r Un Id)" |
80 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r Un Id)" |
544 |
556 |
545 lemma trancl_domain [simp]: "Domain (r^+) = Domain r" |
557 lemma trancl_domain [simp]: "Domain (r^+) = Domain r" |
546 by (unfold Domain_def) (blast dest: tranclD) |
558 by (unfold Domain_def) (blast dest: tranclD) |
547 |
559 |
548 lemma trancl_range [simp]: "Range (r^+) = Range r" |
560 lemma trancl_range [simp]: "Range (r^+) = Range r" |
549 by (simp add: Range_def trancl_converse [symmetric]) |
561 unfolding Range_def by(simp add: trancl_converse [symmetric]) |
550 |
562 |
551 lemma Not_Domain_rtrancl: |
563 lemma Not_Domain_rtrancl: |
552 "x ~: Domain R ==> ((x, y) : R^*) = (x = y)" |
564 "x ~: Domain R ==> ((x, y) : R^*) = (x = y)" |
553 apply auto |
565 apply auto |
554 apply (erule rev_mp) |
566 apply (erule rev_mp) |