equal
deleted
inserted
replaced
154 shows "regular (Deriv_lang B A)" |
154 shows "regular (Deriv_lang B A)" |
155 proof - |
155 proof - |
156 from assms obtain r::"'a rexp" where eq: "lang r = A" by auto |
156 from assms obtain r::"'a rexp" where eq: "lang r = A" by auto |
157 have fin: "finite (pderivs_lang B r)" by (rule finite_pderivs_lang) |
157 have fin: "finite (pderivs_lang B r)" by (rule finite_pderivs_lang) |
158 |
158 |
159 have "Deriv_lang B (lang r) = (\<Union> lang ` (pderivs_lang B r))" |
159 have "Deriv_lang B (lang r) = (\<Union> (lang ` (pderivs_lang B r)))" |
160 by (simp add: Derivs_pderivs pderivs_lang_def) |
160 by (simp add: Derivs_pderivs pderivs_lang_def) |
161 also have "\<dots> = lang (\<Uplus>(pderivs_lang B r))" using fin by simp |
161 also have "\<dots> = lang (\<Uplus>(pderivs_lang B r))" using fin by simp |
162 finally have "Deriv_lang B A = lang (\<Uplus>(pderivs_lang B r))" using eq |
162 finally have "Deriv_lang B A = lang (\<Uplus>(pderivs_lang B r))" using eq |
163 by simp |
163 by simp |
164 then show "regular (Deriv_lang B A)" by auto |
164 then show "regular (Deriv_lang B A)" by auto |