equal
deleted
inserted
replaced
1 theory RegLangs |
1 theory RegLangs |
2 imports Main "~~/src/HOL/Library/Sublist" |
2 imports Main "HOL-Library.Sublist" |
3 begin |
3 begin |
4 |
4 |
5 section \<open>Sequential Composition of Languages\<close> |
5 section \<open>Sequential Composition of Languages\<close> |
6 |
6 |
7 definition |
7 definition |
194 |
194 |
195 lemma ders_snoc: |
195 lemma ders_snoc: |
196 shows "ders (s @ [c]) r = der c (ders s r)" |
196 shows "ders (s @ [c]) r = der c (ders s r)" |
197 by (simp add: ders_append) |
197 by (simp add: ders_append) |
198 |
198 |
|
199 |
|
200 (* |
|
201 datatype ctxt = |
|
202 SeqC rexp bool |
|
203 | AltCL rexp |
|
204 | AltCR rexp |
|
205 | StarC rexp |
|
206 |
|
207 function |
|
208 down :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list" |
|
209 and up :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list" |
|
210 where |
|
211 "down c (SEQ r1 r2) ctxts = |
|
212 (if (nullable r1) then down c r1 (SeqC r2 True # ctxts) |
|
213 else down c r1 (SeqC r2 False # ctxts))" |
|
214 | "down c (CH d) ctxts = |
|
215 (if c = d then up c ONE ctxts else up c ZERO ctxts)" |
|
216 | "down c ONE ctxts = up c ZERO ctxts" |
|
217 | "down c ZERO ctxts = up c ZERO ctxts" |
|
218 | "down c (ALT r1 r2) ctxts = down c r1 (AltCR r2 # ctxts)" |
|
219 | "down c (STAR r1) ctxts = down c r1 (StarC r1 # ctxts)" |
|
220 | "up c r [] = (r, [])" |
|
221 | "up c r (SeqC r2 False # ctxts) = up c (SEQ r r2) ctxts" |
|
222 | "up c r (SeqC r2 True # ctxts) = down c r2 (AltCL (SEQ r r2) # ctxts)" |
|
223 | "up c r (AltCL r1 # ctxts) = up c (ALT r1 r) ctxts" |
|
224 | "up c r (AltCR r2 # ctxts) = down c r2 (AltCL r # ctxts)" |
|
225 | "up c r (StarC r1 # ctxts) = up c (SEQ r (STAR r1)) ctxts" |
|
226 apply(pat_completeness) |
|
227 apply(auto) |
|
228 done |
|
229 |
|
230 termination |
|
231 sorry |
|
232 |
|
233 *) |
|
234 |
|
235 |
199 end |
236 end |