equal
deleted
inserted
replaced
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_lang B r)" by (rule finite_pders_lang) |
153 have fin: "finite (pders_lang B r)" by (rule finite_pders_lang) |
154 |
154 |
155 have "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang 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 pders_lang_def) |
157 also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp |
157 also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp |
158 finally have "Ders_lang B A = lang (\<Uplus>(pders_lang 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_lang B A)" by auto |
160 then show "regular (Ders_lang B A)" by auto |
161 qed |
161 qed |