163 definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60) |
142 definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60) |
164 where |
143 where |
165 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
144 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
166 |
145 |
167 |
146 |
|
147 lemma PosOrd_trans: |
|
148 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
|
149 shows "v1 :\<sqsubset>val v3" |
|
150 proof - |
|
151 from assms obtain p p' |
|
152 where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast |
|
153 then have pos: "p \<in> Pos v1" "p' \<in> Pos v2" unfolding PosOrd_def pflat_len_def |
|
154 by (smt not_int_zless_negative)+ |
|
155 have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p" |
|
156 by (rule lex_trichotomous) |
|
157 moreover |
|
158 { assume "p = p'" |
|
159 with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def |
|
160 by (smt Un_iff) |
|
161 then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
|
162 } |
|
163 moreover |
|
164 { assume "p \<sqsubset>lex p'" |
|
165 with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def |
|
166 by (smt Un_iff lex_trans) |
|
167 then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
|
168 } |
|
169 moreover |
|
170 { assume "p' \<sqsubset>lex p" |
|
171 with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def |
|
172 by (smt Un_iff lex_trans pflat_len_def) |
|
173 then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
|
174 } |
|
175 ultimately show "v1 :\<sqsubset>val v3" by blast |
|
176 qed |
|
177 |
|
178 lemma PosOrd_irrefl: |
|
179 assumes "v :\<sqsubset>val v" |
|
180 shows "False" |
|
181 using assms unfolding PosOrd_ex_def PosOrd_def |
|
182 by auto |
|
183 |
|
184 lemma PosOrd_assym: |
|
185 assumes "v1 :\<sqsubset>val v2" |
|
186 shows "\<not>(v2 :\<sqsubset>val v1)" |
|
187 using assms |
|
188 using PosOrd_irrefl PosOrd_trans by blast |
|
189 |
|
190 text {* |
|
191 :\<sqsubseteq>val and :\<sqsubset>val are partial orders. |
|
192 *} |
|
193 |
|
194 lemma PosOrd_ordering: |
|
195 shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
|
196 unfolding ordering_def PosOrd_ex_eq_def |
|
197 apply(auto) |
|
198 using PosOrd_irrefl apply blast |
|
199 using PosOrd_assym apply blast |
|
200 using PosOrd_trans by blast |
|
201 |
|
202 lemma PosOrd_order: |
|
203 shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
|
204 using PosOrd_ordering |
|
205 apply(simp add: class.order_def class.preorder_def class.order_axioms_def) |
|
206 unfolding ordering_def |
|
207 by blast |
|
208 |
|
209 |
|
210 lemma PosOrd_ex_eq2: |
|
211 shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)" |
|
212 using PosOrd_ordering |
|
213 unfolding ordering_def |
|
214 by auto |
|
215 |
|
216 lemma PosOrdeq_trans: |
|
217 assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3" |
|
218 shows "v1 :\<sqsubseteq>val v3" |
|
219 using assms PosOrd_ordering |
|
220 unfolding ordering_def |
|
221 by blast |
|
222 |
|
223 lemma PosOrdeq_antisym: |
|
224 assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1" |
|
225 shows "v1 = v2" |
|
226 using assms PosOrd_ordering |
|
227 unfolding ordering_def |
|
228 by blast |
|
229 |
|
230 lemma PosOrdeq_refl: |
|
231 shows "v :\<sqsubseteq>val v" |
|
232 unfolding PosOrd_ex_eq_def |
|
233 by auto |
|
234 |
|
235 |
|
236 |
|
237 |
168 lemma PosOrd_shorterE: |
238 lemma PosOrd_shorterE: |
169 assumes "v1 :\<sqsubset>val v2" |
239 assumes "v1 :\<sqsubset>val v2" |
170 shows "length (flat v2) \<le> length (flat v1)" |
240 shows "length (flat v2) \<le> length (flat v1)" |
171 using assms unfolding PosOrd_ex_def PosOrd_def |
241 using assms unfolding PosOrd_ex_def PosOrd_def |
172 apply(auto simp add: pflat_len_def intlen_int split: if_splits) |
242 apply(auto simp add: pflat_len_def split: if_splits) |
173 apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le) |
243 apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le) |
174 by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear) |
244 by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear) |
175 |
245 |
176 lemma PosOrd_shorterI: |
246 lemma PosOrd_shorterI: |
177 assumes "length (flat v2) < length (flat v1)" |
247 assumes "length (flat v2) < length (flat v1)" |
178 shows "v1 :\<sqsubset>val v2" |
248 shows "v1 :\<sqsubset>val v2" |
179 using assms |
249 unfolding PosOrd_ex_def PosOrd_def pflat_len_def |
180 unfolding PosOrd_ex_def |
250 using assms Pos_empty by force |
181 by (metis intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def) |
|
182 |
251 |
183 lemma PosOrd_spreI: |
252 lemma PosOrd_spreI: |
184 assumes "flat v' \<sqsubset>spre flat v" |
253 assumes "flat v' \<sqsubset>spre flat v" |
185 shows "v :\<sqsubset>val v'" |
254 shows "v :\<sqsubset>val v'" |
186 using assms |
255 using assms |
187 apply(rule_tac PosOrd_shorterI) |
256 apply(rule_tac PosOrd_shorterI) |
188 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all) |
257 unfolding prefix_list_def sprefix_list_def |
|
258 by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear) |
189 |
259 |
190 |
260 |
191 lemma PosOrd_Left_Right: |
261 lemma PosOrd_Left_Right: |
192 assumes "flat v1 = flat v2" |
262 assumes "flat v1 = flat v2" |
193 shows "Left v1 :\<sqsubset>val Right v2" |
263 shows "Left v1 :\<sqsubset>val Right v2" |
194 unfolding PosOrd_ex_def |
264 unfolding PosOrd_ex_def |
195 apply(rule_tac x="[0]" in exI) |
265 apply(rule_tac x="[0]" in exI) |
196 using assms |
266 using assms |
197 apply(auto simp add: PosOrd_def pflat_len_simps intlen_int) |
267 apply(auto simp add: PosOrd_def pflat_len_simps) |
198 done |
268 done |
199 |
269 |
200 lemma PosOrd_Left_eq: |
270 lemma PosOrd_Left_eq: |
201 assumes "flat v = flat v'" |
271 assumes "flat v = flat v'" |
202 shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'" |
272 shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'" |
340 apply(simp add: pflat_len_simps) |
410 apply(simp add: pflat_len_simps) |
341 apply(simp add: PosOrd_def pflat_len_def) |
411 apply(simp add: PosOrd_def pflat_len_def) |
342 done |
412 done |
343 |
413 |
344 lemma PosOrd_StarsI: |
414 lemma PosOrd_StarsI: |
345 assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
415 assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)" |
346 shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))" |
416 shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)" |
347 using assms(1) |
417 using assms(1) |
348 apply(subst (asm) PosOrd_ex_def) |
418 apply(subst (asm) PosOrd_ex_def) |
349 apply(subst (asm) PosOrd_def) |
419 apply(subst (asm) PosOrd_def) |
350 apply(clarify) |
420 apply(clarify) |
351 apply(subst PosOrd_ex_def) |
421 apply(subst PosOrd_ex_def) |
352 apply(subst PosOrd_def) |
422 apply(subst PosOrd_def) |
353 apply(rule_tac x="0#p" in exI) |
423 apply(rule_tac x="0#p" in exI) |
354 apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
424 apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
355 using assms(2) |
425 using assms(2) |
356 apply(simp add: pflat_len_simps intlen_append) |
426 apply(simp add: pflat_len_simps) |
357 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
427 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
358 done |
428 by (metis length_append of_nat_add) |
359 |
429 |
360 lemma PosOrd_StarsI2: |
430 lemma PosOrd_StarsI2: |
361 assumes "(Stars vs1) :\<sqsubset>val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" |
431 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flats vs1 = flats vs2" |
362 shows "(Stars (v#vs1)) :\<sqsubset>val (Stars (v#vs2))" |
432 shows "Stars (v#vs1) :\<sqsubset>val Stars (v#vs2)" |
363 using assms(1) |
433 using assms(1) |
364 apply(subst (asm) PosOrd_ex_def) |
434 apply(subst (asm) PosOrd_ex_def) |
365 apply(subst (asm) PosOrd_def) |
435 apply(subst (asm) PosOrd_def) |
366 apply(clarify) |
436 apply(clarify) |
367 apply(subst PosOrd_ex_def) |
437 apply(subst PosOrd_ex_def) |
368 apply(subst PosOrd_def) |
438 apply(subst PosOrd_def) |
369 apply(case_tac p) |
439 apply(case_tac p) |
370 apply(simp add: pflat_len_simps) |
440 apply(simp add: pflat_len_simps) |
371 apply(rule_tac x="[]" in exI) |
|
372 apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append) |
|
373 apply(rule_tac x="Suc a#list" in exI) |
441 apply(rule_tac x="Suc a#list" in exI) |
374 apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
442 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps assms(2)) |
375 using assms(2) |
|
376 apply(simp add: pflat_len_simps intlen_append) |
|
377 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
|
378 done |
443 done |
379 |
444 |
380 lemma PosOrd_Stars_appendI: |
445 lemma PosOrd_Stars_appendI: |
381 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
446 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
382 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
447 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
529 prefer 2 |
552 prefer 2 |
530 apply(simp) |
553 apply(simp) |
531 apply(auto) |
554 apply(auto) |
532 apply(case_tac "length (flat v1') < length (flat v1)") |
555 apply(case_tac "length (flat v1') < length (flat v1)") |
533 using PosOrd_shorterI apply blast |
556 using PosOrd_shorterI apply blast |
534 by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2)) |
557 by (metis PosOrd_SeqI1 PosOrd_shorterI PosOrd_assym antisym_conv3 append_eq_append_conv assms(2)) |
535 |
558 |
536 |
559 |
537 |
560 |
538 section {* The Posix Value is smaller than any other Value *} |
561 section {* The Posix Value is smaller than any other Value *} |
539 |
562 |
540 |
563 |
541 lemma Posix_PosOrd: |
564 lemma Posix_PosOrd: |
542 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CV r s" |
565 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> LV r s" |
543 shows "v1 :\<sqsubseteq>val v2" |
566 shows "v1 :\<sqsubseteq>val v2" |
544 using assms |
567 using assms |
545 proof (induct arbitrary: v2 rule: Posix.induct) |
568 proof (induct arbitrary: v2 rule: Posix.induct) |
546 case (Posix_ONE v) |
569 case (Posix_ONE v) |
547 have "v \<in> CV ONE []" by fact |
570 have "v \<in> LV ONE []" by fact |
548 then have "v = Void" |
571 then have "v = Void" |
549 by (simp add: CV_simps) |
572 by (simp add: LV_simps) |
550 then show "Void :\<sqsubseteq>val v" |
573 then show "Void :\<sqsubseteq>val v" |
551 by (simp add: PosOrd_ex_eq_def) |
574 by (simp add: PosOrd_ex_eq_def) |
552 next |
575 next |
553 case (Posix_CHAR c v) |
576 case (Posix_CHAR c v) |
554 have "v \<in> CV (CHAR c) [c]" by fact |
577 have "v \<in> LV (CHAR c) [c]" by fact |
555 then have "v = Char c" |
578 then have "v = Char c" |
556 by (simp add: CV_simps) |
579 by (simp add: LV_simps) |
557 then show "Char c :\<sqsubseteq>val v" |
580 then show "Char c :\<sqsubseteq>val v" |
558 by (simp add: PosOrd_ex_eq_def) |
581 by (simp add: PosOrd_ex_eq_def) |
559 next |
582 next |
560 case (Posix_ALT1 s r1 v r2 v2) |
583 case (Posix_ALT1 s r1 v r2 v2) |
561 have as1: "s \<in> r1 \<rightarrow> v" by fact |
584 have as1: "s \<in> r1 \<rightarrow> v" by fact |
562 have IH: "\<And>v2. v2 \<in> CV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
585 have IH: "\<And>v2. v2 \<in> LV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
563 have "v2 \<in> CV (ALT r1 r2) s" by fact |
586 have "v2 \<in> LV (ALT r1 r2) s" by fact |
564 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s" |
587 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s" |
565 by(auto simp add: CV_def prefix_list_def) |
588 by(auto simp add: LV_def prefix_list_def) |
566 then consider |
589 then consider |
567 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" |
590 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" |
568 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s" |
591 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s" |
569 by (auto elim: CPrf.cases) |
592 by (auto elim: Prf.cases) |
570 then show "Left v :\<sqsubseteq>val v2" |
593 then show "Left v :\<sqsubseteq>val v2" |
571 proof(cases) |
594 proof(cases) |
572 case (Left v3) |
595 case (Left v3) |
573 have "v3 \<in> CV r1 s" using Left(2,3) |
596 have "v3 \<in> LV r1 s" using Left(2,3) |
574 by (auto simp add: CV_def prefix_list_def) |
597 by (auto simp add: LV_def prefix_list_def) |
575 with IH have "v :\<sqsubseteq>val v3" by simp |
598 with IH have "v :\<sqsubseteq>val v3" by simp |
576 moreover |
599 moreover |
577 have "flat v3 = flat v" using as1 Left(3) |
600 have "flat v3 = flat v" using as1 Left(3) |
578 by (simp add: Posix1(2)) |
601 by (simp add: Posix1(2)) |
579 ultimately have "Left v :\<sqsubseteq>val Left v3" |
602 ultimately have "Left v :\<sqsubseteq>val Left v3" |
581 then show "Left v :\<sqsubseteq>val v2" unfolding Left . |
604 then show "Left v :\<sqsubseteq>val v2" unfolding Left . |
582 next |
605 next |
583 case (Right v3) |
606 case (Right v3) |
584 have "flat v3 = flat v" using as1 Right(3) |
607 have "flat v3 = flat v" using as1 Right(3) |
585 by (simp add: Posix1(2)) |
608 by (simp add: Posix1(2)) |
586 then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1 |
609 then have "Left v :\<sqsubseteq>val Right v3" |
587 by (auto simp add: PosOrd_ex_eq_def PosOrd_Left_Right) |
610 unfolding PosOrd_ex_eq_def |
|
611 by (simp add: PosOrd_Left_Right) |
588 then show "Left v :\<sqsubseteq>val v2" unfolding Right . |
612 then show "Left v :\<sqsubseteq>val v2" unfolding Right . |
589 qed |
613 qed |
590 next |
614 next |
591 case (Posix_ALT2 s r2 v r1 v2) |
615 case (Posix_ALT2 s r2 v r1 v2) |
592 have as1: "s \<in> r2 \<rightarrow> v" by fact |
616 have as1: "s \<in> r2 \<rightarrow> v" by fact |
593 have as2: "s \<notin> L r1" by fact |
617 have as2: "s \<notin> L r1" by fact |
594 have IH: "\<And>v2. v2 \<in> CV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
618 have IH: "\<And>v2. v2 \<in> LV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
595 have "v2 \<in> CV (ALT r1 r2) s" by fact |
619 have "v2 \<in> LV (ALT r1 r2) s" by fact |
596 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s" |
620 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s" |
597 by(auto simp add: CV_def prefix_list_def) |
621 by(auto simp add: LV_def prefix_list_def) |
598 then consider |
622 then consider |
599 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" |
623 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" |
600 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s" |
624 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s" |
601 by (auto elim: CPrf.cases) |
625 by (auto elim: Prf.cases) |
602 then show "Right v :\<sqsubseteq>val v2" |
626 then show "Right v :\<sqsubseteq>val v2" |
603 proof (cases) |
627 proof (cases) |
604 case (Right v3) |
628 case (Right v3) |
605 have "v3 \<in> CV r2 s" using Right(2,3) |
629 have "v3 \<in> LV r2 s" using Right(2,3) |
606 by (auto simp add: CV_def prefix_list_def) |
630 by (auto simp add: LV_def prefix_list_def) |
607 with IH have "v :\<sqsubseteq>val v3" by simp |
631 with IH have "v :\<sqsubseteq>val v3" by simp |
608 moreover |
632 moreover |
609 have "flat v3 = flat v" using as1 Right(3) |
633 have "flat v3 = flat v" using as1 Right(3) |
610 by (simp add: Posix1(2)) |
634 by (simp add: Posix1(2)) |
611 ultimately have "Right v :\<sqsubseteq>val Right v3" |
635 ultimately have "Right v :\<sqsubseteq>val Right v3" |
612 by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI) |
636 by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI) |
613 then show "Right v :\<sqsubseteq>val v2" unfolding Right . |
637 then show "Right v :\<sqsubseteq>val v2" unfolding Right . |
614 next |
638 next |
615 case (Left v3) |
639 case (Left v3) |
616 have "v3 \<in> CV r1 s" using Left(2,3) as2 |
640 have "v3 \<in> LV r1 s" using Left(2,3) as2 |
617 by (auto simp add: CV_def prefix_list_def) |
641 by (auto simp add: LV_def prefix_list_def) |
618 then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3) |
642 then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3) |
619 by (simp add: Posix1(2) CV_def) |
643 by (simp add: Posix1(2) LV_def) |
620 then have "False" using as1 as2 Left |
644 then have "False" using as1 as2 Left |
621 by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf) |
645 by (auto simp add: Posix1(2) L_flat_Prf1) |
622 then show "Right v :\<sqsubseteq>val v2" by simp |
646 then show "Right v :\<sqsubseteq>val v2" by simp |
623 qed |
647 qed |
624 next |
648 next |
625 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3) |
649 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3) |
626 have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+ |
650 have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+ |
627 then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2)) |
651 then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2)) |
628 have IH1: "\<And>v3. v3 \<in> CV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact |
652 have IH1: "\<And>v3. v3 \<in> LV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact |
629 have IH2: "\<And>v3. v3 \<in> CV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact |
653 have IH2: "\<And>v3. v3 \<in> LV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact |
630 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact |
654 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact |
631 have "v3 \<in> CV (SEQ r1 r2) (s1 @ s2)" by fact |
655 have "v3 \<in> LV (SEQ r1 r2) (s1 @ s2)" by fact |
632 then obtain v3a v3b where eqs: |
656 then obtain v3a v3b where eqs: |
633 "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2" |
657 "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2" |
634 "flat v3a @ flat v3b = s1 @ s2" |
658 "flat v3a @ flat v3b = s1 @ s2" |
635 by (force simp add: prefix_list_def CV_def elim: CPrf.cases) |
659 by (force simp add: prefix_list_def LV_def elim: Prf.cases) |
636 with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def |
660 with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def |
637 by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv) |
661 by (smt L_flat_Prf1 append_eq_append_conv2 append_self_conv) |
638 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs |
662 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs |
639 by (simp add: sprefix_list_def append_eq_conv_conj) |
663 by (simp add: sprefix_list_def append_eq_conv_conj) |
640 then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" |
664 then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" |
641 using PosOrd_spreI as1(1) eqs by blast |
665 using PosOrd_spreI as1(1) eqs by blast |
642 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CV r1 s1 \<and> v3b \<in> CV r2 s2)" using eqs(2,3) |
666 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3) |
643 by (auto simp add: CV_def) |
667 by (auto simp add: LV_def) |
644 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
668 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
645 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
669 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
646 unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) |
670 unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) |
647 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
671 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
648 next |
672 next |
649 case (Posix_STAR1 s1 r v s2 vs v3) |
673 case (Posix_STAR1 s1 r v s2 vs v3) |
650 have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
674 have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
651 then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2)) |
675 then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2)) |
652 have IH1: "\<And>v3. v3 \<in> CV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
676 have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
653 have IH2: "\<And>v3. v3 \<in> CV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
677 have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
654 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact |
678 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact |
655 have cond2: "flat v \<noteq> []" by fact |
679 have cond2: "flat v \<noteq> []" by fact |
656 have "v3 \<in> CV (STAR r) (s1 @ s2)" by fact |
680 have "v3 \<in> LV (STAR r) (s1 @ s2)" by fact |
657 then consider |
681 then consider |
658 (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" |
682 (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" |
659 "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r" |
683 "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r" |
660 "flat (Stars (v3a # vs3)) = s1 @ s2" |
684 "flat (Stars (v3a # vs3)) = s1 @ s2" |
661 | (Empty) "v3 = Stars []" |
685 | (Empty) "v3 = Stars []" |
662 unfolding CV_def |
686 unfolding LV_def |
663 apply(auto) |
687 apply(auto) |
664 apply(erule CPrf.cases) |
688 apply(erule Prf.cases) |
665 apply(simp_all) |
689 apply(simp_all) |
666 apply(auto)[1] |
690 apply(auto)[1] |
667 apply(case_tac vs) |
691 apply(case_tac vs) |
668 apply(auto) |
692 apply(auto) |
669 using CPrf.intros(6) by blast |
693 using Prf.intros(6) by blast |
670 then show "Stars (v # vs) :\<sqsubseteq>val v3" (* HERE *) |
694 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
671 proof (cases) |
695 proof (cases) |
672 case (NonEmpty v3a vs3) |
696 case (NonEmpty v3a vs3) |
673 have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . |
697 have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . |
674 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
698 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
675 unfolding prefix_list_def |
699 unfolding prefix_list_def |
676 by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7)) |
700 by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7)) |
677 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
701 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
678 by (simp add: sprefix_list_def append_eq_conv_conj) |
702 by (simp add: sprefix_list_def append_eq_conv_conj) |
679 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
703 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
680 using PosOrd_spreI as1(1) NonEmpty(4) by blast |
704 using PosOrd_spreI as1(1) NonEmpty(4) by blast |
681 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CV r s1 \<and> Stars vs3 \<in> CV (STAR r) s2)" |
705 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)" |
682 using NonEmpty(2,3) by (auto simp add: CV_def) |
706 using NonEmpty(2,3) by (auto simp add: LV_def) |
683 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
707 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
684 then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" |
708 then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" |
685 unfolding PosOrd_ex_eq_def by auto |
709 unfolding PosOrd_ex_eq_def by auto |
686 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
710 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
687 unfolding PosOrd_ex_eq_def |
711 unfolding PosOrd_ex_eq_def |
688 by (metis PosOrd_StarsI PosOrd_StarsI2 flat.simps(7) val.inject(5)) |
712 using PosOrd_StarsI PosOrd_StarsI2 by auto |
689 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
713 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
690 next |
714 next |
691 case Empty |
715 case Empty |
692 have "v3 = Stars []" by fact |
716 have "v3 = Stars []" by fact |
693 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
717 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
694 unfolding PosOrd_ex_eq_def using cond2 |
718 unfolding PosOrd_ex_eq_def using cond2 |
695 by (simp add: PosOrd_shorterI) |
719 by (simp add: PosOrd_shorterI) |
696 qed |
720 qed |
697 next |
721 next |
698 case (Posix_STAR2 r v2) |
722 case (Posix_STAR2 r v2) |
699 have "v2 \<in> CV (STAR r) []" by fact |
723 have "v2 \<in> LV (STAR r) []" by fact |
700 then have "v2 = Stars []" |
724 then have "v2 = Stars []" |
701 unfolding CV_def by (auto elim: CPrf.cases) |
725 unfolding LV_def by (auto elim: Prf.cases) |
702 then show "Stars [] :\<sqsubseteq>val v2" |
726 then show "Stars [] :\<sqsubseteq>val v2" |
703 by (simp add: PosOrd_ex_eq_def) |
727 by (simp add: PosOrd_ex_eq_def) |
704 qed |
728 qed |
705 |
729 |
706 |
730 |
707 lemma Posix_PosOrd_reverse: |
731 lemma Posix_PosOrd_reverse: |
708 assumes "s \<in> r \<rightarrow> v1" |
732 assumes "s \<in> r \<rightarrow> v1" |
709 shows "\<not>(\<exists>v2 \<in> CV r s. v2 :\<sqsubset>val v1)" |
733 shows "\<not>(\<exists>v2 \<in> LV r s. v2 :\<sqsubset>val v1)" |
710 using assms |
734 using assms |
711 by (metis Posix_PosOrd less_irrefl PosOrd_def |
735 by (metis Posix_PosOrd less_irrefl PosOrd_def |
712 PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans) |
736 PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans) |
713 |
737 |
714 |
738 |
776 |
803 |
777 |
804 |
778 |
805 |
779 section {* The Smallest Value is indeed the Posix Value *} |
806 section {* The Smallest Value is indeed the Posix Value *} |
780 |
807 |
781 text {* |
|
782 The next lemma seems to require LV instead of CV in the Star-case. |
|
783 *} |
|
784 |
|
785 lemma PosOrd_Posix: |
808 lemma PosOrd_Posix: |
786 assumes "v1 \<in> CV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1" |
809 assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1" |
787 shows "s \<in> r \<rightarrow> v1" |
810 shows "s \<in> r \<rightarrow> v1" |
788 using assms |
811 using assms |
789 proof(induct r arbitrary: s v1) |
812 proof(induct r arbitrary: s v1) |
790 case (ZERO s v1) |
813 case (ZERO s v1) |
791 have "v1 \<in> CV ZERO s" by fact |
814 have "v1 \<in> LV ZERO s" by fact |
792 then show "s \<in> ZERO \<rightarrow> v1" unfolding CV_def |
815 then show "s \<in> ZERO \<rightarrow> v1" unfolding LV_def |
793 by (auto elim: CPrf.cases) |
816 by (auto elim: Prf.cases) |
794 next |
817 next |
795 case (ONE s v1) |
818 case (ONE s v1) |
796 have "v1 \<in> CV ONE s" by fact |
819 have "v1 \<in> LV ONE s" by fact |
797 then show "s \<in> ONE \<rightarrow> v1" unfolding CV_def |
820 then show "s \<in> ONE \<rightarrow> v1" unfolding LV_def |
798 by(auto elim!: CPrf.cases intro: Posix.intros) |
821 by(auto elim!: Prf.cases intro: Posix.intros) |
799 next |
822 next |
800 case (CHAR c s v1) |
823 case (CHAR c s v1) |
801 have "v1 \<in> CV (CHAR c) s" by fact |
824 have "v1 \<in> LV (CHAR c) s" by fact |
802 then show "s \<in> CHAR c \<rightarrow> v1" unfolding CV_def |
825 then show "s \<in> CHAR c \<rightarrow> v1" unfolding LV_def |
803 by (auto elim!: CPrf.cases intro: Posix.intros) |
826 by (auto elim!: Prf.cases intro: Posix.intros) |
804 next |
827 next |
805 case (ALT r1 r2 s v1) |
828 case (ALT r1 r2 s v1) |
806 have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
829 have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
807 have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
830 have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
808 have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
831 have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
809 have as2: "v1 \<in> CV (ALT r1 r2) s" by fact |
832 have as2: "v1 \<in> LV (ALT r1 r2) s" by fact |
810 then consider |
833 then consider |
811 (Left) v1' where |
834 (Left) v1' where |
812 "v1 = Left v1'" "s = flat v1'" |
835 "v1 = Left v1'" "s = flat v1'" |
813 "v1' \<in> CV r1 s" |
836 "v1' \<in> LV r1 s" |
814 | (Right) v1' where |
837 | (Right) v1' where |
815 "v1 = Right v1'" "s = flat v1'" |
838 "v1 = Right v1'" "s = flat v1'" |
816 "v1' \<in> CV r2 s" |
839 "v1' \<in> LV r2 s" |
817 unfolding CV_def by (auto elim: CPrf.cases) |
840 unfolding LV_def by (auto elim: Prf.cases) |
818 then show "s \<in> ALT r1 r2 \<rightarrow> v1" |
841 then show "s \<in> ALT r1 r2 \<rightarrow> v1" |
819 proof (cases) |
842 proof (cases) |
820 case (Left v1') |
843 case (Left v1') |
821 have "v1' \<in> CV r1 s" using as2 |
844 have "v1' \<in> LV r1 s" using as2 |
822 unfolding CV_def Left by (auto elim: CPrf.cases) |
845 unfolding LV_def Left by (auto elim: Prf.cases) |
823 moreover |
846 moreover |
824 have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
847 have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
825 unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force |
848 unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force |
826 ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp |
849 ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp |
827 then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros) |
850 then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros) |
828 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp |
851 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp |
829 next |
852 next |
830 case (Right v1') |
853 case (Right v1') |
831 have "v1' \<in> CV r2 s" using as2 |
854 have "v1' \<in> LV r2 s" using as2 |
832 unfolding CV_def Right by (auto elim: CPrf.cases) |
855 unfolding LV_def Right by (auto elim: Prf.cases) |
833 moreover |
856 moreover |
834 have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
857 have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
835 unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force |
858 unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force |
836 ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp |
859 ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp |
837 moreover |
860 moreover |
839 then obtain v' where "v' \<in> LV r1 s" |
862 then obtain v' where "v' \<in> LV r1 s" |
840 unfolding LV_def using L_flat_Prf2 by blast |
863 unfolding LV_def using L_flat_Prf2 by blast |
841 then have "Left v' \<in> LV (ALT r1 r2) s" |
864 then have "Left v' \<in> LV (ALT r1 r2) s" |
842 unfolding LV_def by (auto intro: Prf.intros) |
865 unfolding LV_def by (auto intro: Prf.intros) |
843 with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" |
866 with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" |
844 unfolding LV_def Right by (auto) |
867 unfolding LV_def Right |
|
868 by (auto) |
845 then have False using PosOrd_Left_Right Right by blast |
869 then have False using PosOrd_Left_Right Right by blast |
846 } |
870 } |
847 then have "s \<notin> L r1" by rule |
871 then have "s \<notin> L r1" by rule |
848 ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros) |
872 ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros) |
849 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp |
873 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp |
850 qed |
874 qed |
851 next |
875 next |
852 case (SEQ r1 r2 s v1) |
876 case (SEQ r1 r2 s v1) |
853 have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
877 have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
854 have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
878 have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
855 have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
879 have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
856 have as2: "v1 \<in> CV (SEQ r1 r2) s" by fact |
880 have as2: "v1 \<in> LV (SEQ r1 r2) s" by fact |
857 then obtain |
881 then obtain |
858 v1a v1b where eqs: |
882 v1a v1b where eqs: |
859 "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b" |
883 "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b" |
860 "v1a \<in> CV r1 (flat v1a)" "v1b \<in> CV r2 (flat v1b)" |
884 "v1a \<in> LV r1 (flat v1a)" "v1b \<in> LV r2 (flat v1b)" |
861 unfolding CV_def by(auto elim: CPrf.cases) |
885 unfolding LV_def by(auto elim: Prf.cases) |
862 have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a" |
886 have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a" |
863 proof |
887 proof |
864 fix v2 |
888 fix v2 |
865 assume "v2 \<in> LV r1 (flat v1a)" |
889 assume "v2 \<in> LV r1 (flat v1a)" |
866 with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s" |
890 with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s" |
867 by (simp add: CV_def LV_def Prf.intros(1) Prf_CPrf) |
891 by (simp add: LV_def Prf.intros(1)) |
868 with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" |
892 with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" |
869 using eqs by (simp add: LV_def) |
893 using eqs by (simp add: LV_def) |
870 then show "\<not> v2 :\<sqsubset>val v1a" |
894 then show "\<not> v2 :\<sqsubset>val v1a" |
871 using PosOrd_SeqI1 by blast |
895 using PosOrd_SeqI1 by blast |
872 qed |
896 qed |
887 moreover |
911 moreover |
888 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" |
912 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" |
889 proof |
913 proof |
890 assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" |
914 assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" |
891 then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast |
915 then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast |
892 then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<turnstile> vA : r1" "flat vB = s4" "\<turnstile> vB : r2" |
916 then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<Turnstile> vA : r1" "flat vB = s4" "\<Turnstile> vB : r2" |
893 using L_flat_Prf2 by blast |
917 using L_flat_Prf2 by blast |
894 then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1 |
918 then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1 |
895 by (auto simp add: LV_def intro: Prf.intros) |
919 by (auto simp add: LV_def intro!: Prf.intros) |
896 with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto |
920 with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto |
897 then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto |
921 then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto |
898 then show "False" |
922 then show "False" |
899 using PosOrd_shorterI by blast |
923 using PosOrd_shorterI by blast |
900 qed |
924 qed |
901 ultimately |
925 ultimately |
902 show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs |
926 show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs |
903 by (rule Posix.intros) |
927 by (rule Posix.intros) |
904 next |
928 next |
905 case (STAR r s v1) |
929 case (STAR r s v1) |
906 have IH: "\<And>s v1. \<lbrakk>v1 \<in> CV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact |
930 have IH: "\<And>s v1. \<lbrakk>v1 \<in> LV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact |
907 have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact |
931 have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact |
908 have as2: "v1 \<in> CV (STAR r) s" by fact |
932 have as2: "v1 \<in> LV (STAR r) s" by fact |
909 then obtain |
933 then obtain |
910 vs where eqs: |
934 vs where eqs: |
911 "v1 = Stars vs" "s = flat (Stars vs)" |
935 "v1 = Stars vs" "s = flat (Stars vs)" |
912 "\<forall>v \<in> set vs. v \<in> CV r (flat v)" |
936 "\<forall>v \<in> set vs. v \<in> LV r (flat v)" |
913 unfolding CV_def by (auto elim: CPrf.cases) |
937 unfolding LV_def by (auto elim: Prf.cases) |
914 have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" |
938 have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" |
915 proof |
939 proof |
916 fix v |
940 fix v |
917 assume a: "v \<in> set vs" |
941 assume a: "v \<in> set vs" |
918 then obtain pre post where e: "vs = pre @ [v] @ post" |
942 then obtain pre post where e: "vs = pre @ [v] @ post" |
924 fix v2 |
948 fix v2 |
925 assume w: "v2 :\<sqsubset>val v" |
949 assume w: "v2 :\<sqsubset>val v" |
926 assume "v2 \<in> LV r (flat v)" |
950 assume "v2 \<in> LV r (flat v)" |
927 then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s" |
951 then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s" |
928 using as2 unfolding e eqs |
952 using as2 unfolding e eqs |
929 apply(auto simp add: CV_def LV_def intro!: Prf.intros)[1] |
953 apply(auto simp add: LV_def intro!: Prf.intros elim: Prf_elims dest: Prf_Stars_appendE) |
930 using CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros apply blast |
954 apply(auto dest!: Prf_Stars_appendE elim: Prf.cases) |
931 by (metis CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros(2) val.inject(5)) |
955 done |
932 then have "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)" |
956 then have "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)" |
933 using q by simp |
957 using q by simp |
934 with w show "False" |
958 with w show "False" |
935 using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq |
959 using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq |
936 PosOrd_StarsI PosOrd_Stars_appendI by auto |
960 PosOrd_StarsI PosOrd_Stars_appendI by auto |
937 qed |
961 qed |
938 with IH |
962 with IH |
939 show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs CV_def |
963 show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs LV_def |
940 by (auto elim: CPrf.cases) |
964 by (auto elim: Prf.cases) |
941 qed |
965 qed |
942 moreover |
966 moreover |
943 have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" |
967 have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" |
944 proof |
968 proof |
945 assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs" |
969 assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs" |
946 then obtain vs2 where "\<turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)" |
970 then obtain vs2 where "\<Turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)" |
947 "Stars vs2 :\<sqsubset>val Stars vs" |
971 "Stars vs2 :\<sqsubset>val Stars vs" |
948 unfolding LV_def |
972 unfolding LV_def by (force elim: Prf_elims intro: Prf.intros) |
949 apply(auto) |
|
950 apply(erule Prf.cases) |
|
951 apply(auto intro: Prf.intros) |
|
952 done |
|
953 then show "False" using as1 unfolding eqs |
973 then show "False" using as1 unfolding eqs |
954 apply - |
974 by (auto simp add: LV_def) |
955 apply(drule_tac x="Stars vs2" in bspec) |
|
956 apply(auto simp add: LV_def) |
|
957 done |
|
958 qed |
975 qed |
959 ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" |
976 ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" |
960 thm PosOrd_Posix_Stars |
977 thm PosOrd_Posix_Stars |
961 by (rule PosOrd_Posix_Stars) |
978 by (rule PosOrd_Posix_Stars) |
962 then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs . |
979 then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs . |
963 qed |
980 qed |
964 |
981 |
|
982 lemma Least_existence: |
|
983 assumes "LV r s \<noteq> {}" |
|
984 shows " \<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
|
985 proof - |
|
986 from assms |
|
987 obtain vposix where "s \<in> r \<rightarrow> vposix" |
|
988 unfolding LV_def |
|
989 using L_flat_Prf1 lexer_correct_Some by blast |
|
990 then have "\<forall>v \<in> LV r s. vposix :\<sqsubseteq>val v" |
|
991 by (simp add: Posix_PosOrd) |
|
992 then show "\<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
|
993 using Posix_LV \<open>s \<in> r \<rightarrow> vposix\<close> by blast |
|
994 qed |
|
995 |
|
996 lemma Least_existence1: |
|
997 assumes "LV r s \<noteq> {}" |
|
998 shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v" |
|
999 using Least_existence[OF assms] assms |
|
1000 apply - |
|
1001 apply(erule bexE) |
|
1002 apply(rule_tac a="vmin" in ex1I) |
|
1003 apply(auto)[1] |
|
1004 apply (metis PosOrd_Posix PosOrd_ex_eq2 PosOrd_spreI PosOrdeq_antisym Posix1(2)) |
|
1005 apply(auto)[1] |
|
1006 apply(simp add: PosOrdeq_antisym) |
|
1007 done |
|
1008 |
|
1009 lemma |
|
1010 shows "partial_order_on UNIV {(v1, v2). v1 :\<sqsubseteq>val v2}" |
|
1011 apply(simp add: partial_order_on_def) |
|
1012 apply(simp add: preorder_on_def refl_on_def) |
|
1013 apply(simp add: PosOrdeq_refl) |
|
1014 apply(auto) |
|
1015 apply(rule transI) |
|
1016 apply(auto intro: PosOrdeq_trans)[1] |
|
1017 apply(rule antisymI) |
|
1018 apply(simp add: PosOrdeq_antisym) |
|
1019 done |
|
1020 |
|
1021 lemma |
|
1022 "wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}" |
|
1023 apply(rule finite_acyclic_wf) |
|
1024 prefer 2 |
|
1025 apply(simp add: acyclic_def) |
|
1026 apply(induct_tac rule: trancl.induct) |
|
1027 apply(auto)[1] |
|
1028 oops |
|
1029 |
|
1030 |
965 unused_thms |
1031 unused_thms |
966 |
1032 |
967 end |
1033 end |