equal
deleted
inserted
replaced
214 where "Derivs xs A = { ys. xs @ ys \<in> A }" |
214 where "Derivs xs A = { ys. xs @ ys \<in> A }" |
215 |
215 |
216 abbreviation |
216 abbreviation |
217 Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang" |
217 Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang" |
218 where |
218 where |
219 "Derivss s As \<equiv> \<Union> (Derivs s) ` As" |
219 "Derivss s As \<equiv> \<Union> (Derivs s ` As)" |
220 |
220 |
221 |
221 |
222 lemma Deriv_empty[simp]: "Deriv a {} = {}" |
222 lemma Deriv_empty[simp]: "Deriv a {} = {}" |
223 and Deriv_epsilon[simp]: "Deriv a {[]} = {}" |
223 and Deriv_epsilon[simp]: "Deriv a {[]} = {}" |
224 and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})" |
224 and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})" |