equal
deleted
inserted
replaced
166 |
166 |
167 apply(auto) |
167 apply(auto) |
168 done |
168 done |
169 *) |
169 *) |
170 |
170 |
|
171 |
|
172 |
|
173 |
|
174 lemma POSIX_ALT2: |
|
175 assumes "POSIX (Left v1) (ALT r1 r2)" |
|
176 shows "POSIX v1 r1" |
|
177 using assms |
|
178 unfolding POSIX_def |
|
179 apply(auto) |
|
180 apply(drule_tac x="Left v'" in spec) |
|
181 apply(simp) |
|
182 apply(drule mp) |
|
183 apply(rule Prf.intros) |
|
184 apply(auto) |
|
185 apply(erule ValOrd.cases) |
|
186 apply(simp_all) |
|
187 done |
|
188 |
|
189 lemma POSIX2_ALT: |
|
190 assumes "POSIX2 (Left v1) (ALT r1 r2)" |
|
191 shows "POSIX2 v1 r1" |
|
192 using assms |
|
193 unfolding POSIX2_def |
|
194 apply(auto) |
|
195 |
|
196 done |
|
197 |
171 lemma POSIX_ALT: |
198 lemma POSIX_ALT: |
172 assumes "POSIX (Left v1) (ALT r1 r2)" |
199 assumes "POSIX (Left v1) (ALT r1 r2)" |
173 shows "POSIX v1 r1" |
200 shows "POSIX v1 r1" |
174 using assms |
201 using assms |
175 unfolding POSIX_def |
202 unfolding POSIX_def |
288 |
315 |
289 text {* |
316 text {* |
290 The value mkeps returns is always the correct POSIX |
317 The value mkeps returns is always the correct POSIX |
291 value. |
318 value. |
292 *} |
319 *} |
|
320 |
|
321 lemma mkeps_POSIX2: |
|
322 assumes "nullable r" |
|
323 shows "POSIX2 (mkeps r) r" |
|
324 using assms |
|
325 apply(induct r) |
|
326 apply(auto)[1] |
|
327 apply(simp add: POSIX2_def) |
293 |
328 |
294 lemma mkeps_POSIX: |
329 lemma mkeps_POSIX: |
295 assumes "nullable r" |
330 assumes "nullable r" |
296 shows "POSIX (mkeps r) r" |
331 shows "POSIX (mkeps r) r" |
297 using assms |
332 using assms |