equal
deleted
inserted
replaced
127 lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*" |
127 lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*" |
128 by (drule rtrancl_mono, simp) |
128 by (drule rtrancl_mono, simp) |
129 |
129 |
130 lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*" |
130 lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*" |
131 apply (drule rtrancl_mono) |
131 apply (drule rtrancl_mono) |
132 apply (drule rtrancl_mono, simp, blast) |
132 apply (drule rtrancl_mono, simp) |
133 done |
133 done |
134 |
134 |
135 lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*" |
135 lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*" |
136 by (blast intro!: rtrancl_subset intro: r_into_rtrancl rtrancl_mono [THEN subsetD]) |
136 by (blast intro!: rtrancl_subset intro: r_into_rtrancl rtrancl_mono [THEN subsetD]) |
137 |
137 |