equal
deleted
inserted
replaced
168 | Seq val val |
168 | Seq val val |
169 | Right val |
169 | Right val |
170 | Left val |
170 | Left val |
171 | Stars "val list" |
171 | Stars "val list" |
172 |
172 |
173 datatype_compat val |
|
174 |
|
175 |
173 |
176 section {* The string behind a value *} |
174 section {* The string behind a value *} |
177 |
175 |
178 fun |
176 fun |
179 flat :: "val \<Rightarrow> string" |
177 flat :: "val \<Rightarrow> string" |
213 (* "\<turnstile> vs : STAR r"*) |
211 (* "\<turnstile> vs : STAR r"*) |
214 |
212 |
215 lemma Prf_flat_L: |
213 lemma Prf_flat_L: |
216 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
214 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
217 using assms |
215 using assms |
218 apply(induct v r rule: Prf.induct) |
216 by(induct v r rule: Prf.induct) |
219 apply(auto simp add: Sequ_def) |
217 (auto simp add: Sequ_def) |
220 done |
|
221 |
218 |
222 lemma Prf_Stars: |
219 lemma Prf_Stars: |
223 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
220 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
224 shows "\<turnstile> Stars vs : STAR r" |
221 shows "\<turnstile> Stars vs : STAR r" |
225 using assms |
222 using assms |
455 have "[] \<in> STAR r \<rightarrow> v2" by fact |
452 have "[] \<in> STAR r \<rightarrow> v2" by fact |
456 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
453 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
457 qed |
454 qed |
458 |
455 |
459 |
456 |
460 (* a proof that does not need proj *) |
457 lemma Posix_injval: |
461 lemma Posix2_roy_version: |
|
462 assumes "s \<in> (der c r) \<rightarrow> v" |
458 assumes "s \<in> (der c r) \<rightarrow> v" |
463 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
459 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
464 using assms |
460 using assms |
465 proof(induct r arbitrary: s v rule: rexp.induct) |
461 proof(induct r arbitrary: s v rule: rexp.induct) |
466 case ZERO |
462 case ZERO |
634 apply(induct s arbitrary: r) |
630 apply(induct s arbitrary: r) |
635 apply(auto simp add: Posix_mkeps nullable_correctness)[1] |
631 apply(auto simp add: Posix_mkeps nullable_correctness)[1] |
636 apply(drule_tac x="der a r" in meta_spec) |
632 apply(drule_tac x="der a r" in meta_spec) |
637 apply(simp add: der_correctness Der_def) |
633 apply(simp add: der_correctness Der_def) |
638 apply(rule iffI) |
634 apply(rule iffI) |
639 apply(auto intro: Posix2_roy_version simp add: Posix1(1)) |
635 apply(auto intro: Posix_injval simp add: Posix1(1)) |
640 done |
636 done |
641 |
637 |
642 |
638 |
643 end |
639 end |