equal
deleted
inserted
replaced
27 section {* Semantic Derivative of Languages *} |
27 section {* Semantic Derivative of Languages *} |
28 |
28 |
29 definition |
29 definition |
30 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
30 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
31 where |
31 where |
32 "Der c A \<equiv> {s. [c] @ s \<in> A}" |
32 "Der c A \<equiv> {s. c # s \<in> A}" |
33 |
33 |
34 lemma Der_null [simp]: |
34 lemma Der_null [simp]: |
35 shows "Der c {} = {}" |
35 shows "Der c {} = {}" |
36 unfolding Der_def |
36 unfolding Der_def |
37 by auto |
37 by auto |