equal
deleted
inserted
replaced
141 qed |
141 qed |
142 |
142 |
143 subsection {* Closure under left-quotients *} |
143 subsection {* Closure under left-quotients *} |
144 |
144 |
145 abbreviation |
145 abbreviation |
146 "Ders_set A B \<equiv> \<Union>s \<in> A. Ders s B" |
146 "Ders_lang A B \<equiv> \<Union>s \<in> A. Ders s B" |
147 |
147 |
148 lemma closure_left_quotient: |
148 lemma closure_left_quotient: |
149 assumes "regular A" |
149 assumes "regular A" |
150 shows "regular (Ders_set B A)" |
150 shows "regular (Ders_lang B A)" |
151 proof - |
151 proof - |
152 from assms obtain r::"'a rexp" where eq: "lang r = A" by auto |
152 from assms obtain r::"'a rexp" where eq: "lang r = A" by auto |
153 have fin: "finite (pders_set B r)" by (rule finite_pders_set) |
153 have fin: "finite (pders_lang B r)" by (rule finite_pders_lang) |
154 |
154 |
155 have "Ders_set B (lang r) = (\<Union> lang ` (pders_set B r))" |
155 have "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))" |
156 by (simp add: Ders_pders) |
156 by (simp add: Ders_pders) |
157 also have "\<dots> = lang (\<Uplus>(pders_set B r))" using fin by simp |
157 also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp |
158 finally have "Ders_set B A = lang (\<Uplus>(pders_set B r))" using eq |
158 finally have "Ders_lang B A = lang (\<Uplus>(pders_lang B r))" using eq |
159 by simp |
159 by simp |
160 then show "regular (Ders_set B A)" by auto |
160 then show "regular (Ders_lang B A)" by auto |
161 qed |
161 qed |
162 |
162 |
163 |
163 |
164 end |
164 end |