34 "_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>=)" [1000] 999) |
34 "_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>=)" [1000] 999) |
35 |
35 |
36 use "Transitive_Closure_lemmas.ML" |
36 use "Transitive_Closure_lemmas.ML" |
37 |
37 |
38 |
38 |
39 lemma reflcl_trancl [simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*" |
39 lemma reflcl_trancl [simp]: "(r^+)^= = r^*" |
40 apply safe |
40 apply safe |
41 apply (erule trancl_into_rtrancl) |
41 apply (erule trancl_into_rtrancl) |
42 apply (blast elim: rtranclE dest: rtrancl_into_trancl1) |
42 apply (blast elim: rtranclE dest: rtrancl_into_trancl1) |
43 done |
43 done |
44 |
44 |
45 lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*" |
45 lemma trancl_reflcl [simp]: "(r^=)^+ = r^*" |
46 apply safe |
46 apply safe |
47 apply (drule trancl_into_rtrancl) |
47 apply (drule trancl_into_rtrancl) |
48 apply simp |
48 apply simp |
49 apply (erule rtranclE) |
49 apply (erule rtranclE) |
50 apply safe |
50 apply safe |
53 apply (rule rtrancl_into_trancl1) |
53 apply (rule rtrancl_into_trancl1) |
54 apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD]) |
54 apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD]) |
55 apply fast |
55 apply fast |
56 done |
56 done |
57 |
57 |
58 lemma trancl_empty [simp]: "{}\<^sup>+ = {}" |
58 lemma trancl_empty [simp]: "{}^+ = {}" |
59 by (auto elim: trancl_induct) |
59 by (auto elim: trancl_induct) |
60 |
60 |
61 lemma rtrancl_empty [simp]: "{}\<^sup>* = Id" |
61 lemma rtrancl_empty [simp]: "{}^* = Id" |
62 by (rule subst [OF reflcl_trancl]) simp |
62 by (rule subst [OF reflcl_trancl]) simp |
63 |
63 |
64 lemma rtranclD: "(a, b) \<in> R\<^sup>* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R\<^sup>+" |
64 lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+" |
65 by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl) |
65 by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl) |
66 |
66 |
67 |
67 |
68 (* should be merged with the main body of lemmas: *) |
68 (* should be merged with the main body of lemmas: *) |
69 |
69 |
70 lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV" |
70 lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV" |
71 by blast |
71 by blast |
72 |
72 |
73 lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV" |
73 lemma Range_rtrancl [simp]: "Range (R^*) = UNIV" |
74 by blast |
74 by blast |
75 |
75 |
76 lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R Un S)\<^sup>*" |
76 lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*" |
77 by (rule rtrancl_Un_rtrancl [THEN subst]) fast |
77 by (rule rtrancl_Un_rtrancl [THEN subst]) fast |
78 |
78 |
79 lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* ==> x \<in> (R \<union> S)\<^sup>*" |
79 lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*" |
80 by (blast intro: subsetD [OF rtrancl_Un_subset]) |
80 by (blast intro: subsetD [OF rtrancl_Un_subset]) |
81 |
81 |
82 lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r" |
82 lemma trancl_domain [simp]: "Domain (r^+) = Domain r" |
83 by (unfold Domain_def) (blast dest: tranclD) |
83 by (unfold Domain_def) (blast dest: tranclD) |
84 |
84 |
85 lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r" |
85 lemma trancl_range [simp]: "Range (r^+) = Range r" |
86 by (simp add: Range_def trancl_converse [symmetric]) |
86 by (simp add: Range_def trancl_converse [symmetric]) |
87 |
87 |
88 end |
88 end |