equal
deleted
inserted
replaced
22 shows "A ;; {} = {}" |
22 shows "A ;; {} = {}" |
23 and "{} ;; A = {}" |
23 and "{} ;; A = {}" |
24 by (simp_all add: Sequ_def) |
24 by (simp_all add: Sequ_def) |
25 |
25 |
26 |
26 |
27 section {* Semantic Derivatives 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 |
|
34 definition |
|
35 Ders :: "string \<Rightarrow> string set \<Rightarrow> string set" |
|
36 where |
|
37 "Ders s A \<equiv> {s' | s'. s @ s' \<in> A}" |
|
38 |
33 |
39 lemma Der_null [simp]: |
34 lemma Der_null [simp]: |
40 shows "Der c {} = {}" |
35 shows "Der c {} = {}" |
41 unfolding Der_def |
36 unfolding Der_def |
42 by auto |
37 by auto |
165 shows "L (der c r) = Der c (L r)" |
160 shows "L (der c r) = Der c (L r)" |
166 apply(induct r) |
161 apply(induct r) |
167 apply(simp_all add: nullable_correctness) |
162 apply(simp_all add: nullable_correctness) |
168 done |
163 done |
169 |
164 |
170 lemma ders_correctness: |
|
171 shows "L (ders s r) = Ders s (L r)" |
|
172 apply(induct s arbitrary: r) |
|
173 apply(simp_all add: der_correctness Der_def Ders_def) |
|
174 done |
|
175 |
|
176 |
165 |
177 section {* Values *} |
166 section {* Values *} |
178 |
167 |
179 datatype val = |
168 datatype val = |
180 Void |
169 Void |