equal
deleted
inserted
replaced
140 then show "regular (rev` A)" by blast |
140 then show "regular (rev` A)" by blast |
141 qed |
141 qed |
142 |
142 |
143 subsection {* Closure under left-quotients *} |
143 subsection {* Closure under left-quotients *} |
144 |
144 |
|
145 abbreviation |
|
146 "Ders_set A B \<equiv> \<Union>s \<in> A. Ders s B" |
|
147 |
145 lemma closure_left_quotient: |
148 lemma closure_left_quotient: |
146 assumes "regular A" |
149 assumes "regular A" |
147 shows "regular (Ders_set B A)" |
150 shows "regular (Ders_set B A)" |
148 proof - |
151 proof - |
149 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 |
150 have fin: "finite (pders_set B r)" by (rule finite_pders_set) |
153 have fin: "finite (pders_set B r)" by (rule finite_pders_set) |
151 |
154 |
152 have "Ders_set B (lang r) = (\<Union> lang ` (pders_set B r))" |
155 have "Ders_set B (lang r) = (\<Union> lang ` (pders_set B r))" |
153 by (simp add: Ders_set_pders_set) |
156 by (simp add: Ders_pders) |
154 also have "\<dots> = lang (\<Uplus>(pders_set B r))" using fin by simp |
157 also have "\<dots> = lang (\<Uplus>(pders_set B r))" using fin by simp |
155 finally have "Ders_set B A = lang (\<Uplus>(pders_set B r))" using eq |
158 finally have "Ders_set B A = lang (\<Uplus>(pders_set B r))" using eq |
156 by simp |
159 by simp |
157 then show "regular (Ders_set B A)" by auto |
160 then show "regular (Ders_set B A)" by auto |
158 qed |
161 qed |