equal
deleted
inserted
replaced
85 lemma EF_lemma: |
85 lemma EF_lemma: |
86 "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"; |
86 "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"; |
87 apply(rule equalityI); |
87 apply(rule equalityI); |
88 apply(rule subsetI); |
88 apply(rule subsetI); |
89 apply(simp); |
89 apply(simp); |
90 apply(erule lfp_induct); |
90 apply(erule lfp_induct_set); |
91 apply(rule mono_ef); |
91 apply(rule mono_ef); |
92 apply(simp); |
92 apply(simp); |
93 apply(blast intro: rtrancl_trans); |
93 apply(blast intro: rtrancl_trans); |
94 apply(rule subsetI); |
94 apply(rule subsetI); |
95 apply(simp, clarify); |
95 apply(simp, clarify); |