132 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
132 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
133 where |
133 where |
134 "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
134 "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
135 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
135 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
136 |
136 |
137 lemma test: |
137 lemma PosOrd_def2: |
138 shows "v1 \<sqsubset>val p v2 \<longleftrightarrow> |
138 shows "v1 \<sqsubset>val p v2 \<longleftrightarrow> |
139 pflat_len v1 p > pflat_len v2 p \<and> |
139 pflat_len v1 p > pflat_len v2 p \<and> |
140 (\<forall>q \<in> Pos v1. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q) \<and> |
140 (\<forall>q \<in> Pos v1. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q) \<and> |
141 (\<forall>q \<in> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
141 (\<forall>q \<in> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
142 unfolding PosOrd_def |
142 unfolding PosOrd_def |
244 |
244 |
245 lemma PosOrd_shorterE: |
245 lemma PosOrd_shorterE: |
246 assumes "v1 :\<sqsubset>val v2" |
246 assumes "v1 :\<sqsubset>val v2" |
247 shows "length (flat v2) \<le> length (flat v1)" |
247 shows "length (flat v2) \<le> length (flat v1)" |
248 using assms unfolding PosOrd_ex_def PosOrd_def |
248 using assms unfolding PosOrd_ex_def PosOrd_def |
249 apply(auto simp add: pflat_len_def split: if_splits) |
249 apply(auto) |
250 apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le) |
250 apply(case_tac p) |
251 by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear) |
251 apply(simp add: pflat_len_simps) |
|
252 apply(drule_tac x="[]" in bspec) |
|
253 apply(simp add: Pos_empty) |
|
254 apply(simp add: pflat_len_simps) |
|
255 done |
252 |
256 |
253 lemma PosOrd_shorterI: |
257 lemma PosOrd_shorterI: |
254 assumes "length (flat v2) < length (flat v1)" |
258 assumes "length (flat v2) < length (flat v1)" |
255 shows "v1 :\<sqsubset>val v2" |
259 shows "v1 :\<sqsubset>val v2" |
256 unfolding PosOrd_ex_def PosOrd_def pflat_len_def |
260 unfolding PosOrd_ex_def PosOrd_def pflat_len_def |
269 shows "p \<in> Pos v1" |
273 shows "p \<in> Pos v1" |
270 using assms |
274 using assms |
271 unfolding pflat_len_def |
275 unfolding pflat_len_def |
272 by (auto split: if_splits) |
276 by (auto split: if_splits) |
273 |
277 |
|
278 |
274 lemma PosOrd_Left_Right: |
279 lemma PosOrd_Left_Right: |
275 assumes "flat v1 = flat v2" |
280 assumes "flat v1 = flat v2" |
276 shows "Left v1 :\<sqsubset>val Right v2" |
281 shows "Left v1 :\<sqsubset>val Right v2" |
277 unfolding PosOrd_ex_def |
282 unfolding PosOrd_ex_def |
278 apply(rule_tac x="[0]" in exI) |
283 apply(rule_tac x="[0]" in exI) |
281 |
286 |
282 lemma PosOrd_LeftE: |
287 lemma PosOrd_LeftE: |
283 assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2" |
288 assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2" |
284 shows "v1 :\<sqsubset>val v2" |
289 shows "v1 :\<sqsubset>val v2" |
285 using assms |
290 using assms |
286 unfolding PosOrd_ex_def test |
291 unfolding PosOrd_ex_def PosOrd_def2 |
287 apply(auto simp add: pflat_len_simps) |
292 apply(auto simp add: pflat_len_simps) |
288 apply(frule pflat_len_inside) |
293 apply(frule pflat_len_inside) |
289 apply(auto simp add: pflat_len_simps) |
294 apply(auto simp add: pflat_len_simps) |
290 by (metis lex_simps(3) pflat_len_simps(3)) |
295 by (metis lex_simps(3) pflat_len_simps(3)) |
291 |
296 |
292 lemma PosOrd_LeftI: |
297 lemma PosOrd_LeftI: |
293 assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2" |
298 assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2" |
294 shows "Left v1 :\<sqsubset>val Left v2" |
299 shows "Left v1 :\<sqsubset>val Left v2" |
295 using assms |
300 using assms |
296 unfolding PosOrd_ex_def test |
301 unfolding PosOrd_ex_def PosOrd_def2 |
297 apply(auto simp add: pflat_len_simps) |
302 apply(auto simp add: pflat_len_simps) |
298 by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3)) |
303 by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3)) |
299 |
304 |
300 lemma PosOrd_Left_eq: |
305 lemma PosOrd_Left_eq: |
301 assumes "flat v1 = flat v2" |
306 assumes "flat v1 = flat v2" |
306 |
311 |
307 lemma PosOrd_RightE: |
312 lemma PosOrd_RightE: |
308 assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2" |
313 assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2" |
309 shows "v1 :\<sqsubset>val v2" |
314 shows "v1 :\<sqsubset>val v2" |
310 using assms |
315 using assms |
311 unfolding PosOrd_ex_def test |
316 unfolding PosOrd_ex_def PosOrd_def2 |
312 apply(auto simp add: pflat_len_simps) |
317 apply(auto simp add: pflat_len_simps) |
313 apply(frule pflat_len_inside) |
318 apply(frule pflat_len_inside) |
314 apply(auto simp add: pflat_len_simps) |
319 apply(auto simp add: pflat_len_simps) |
315 by (metis lex_simps(3) pflat_len_simps(5)) |
320 by (metis lex_simps(3) pflat_len_simps(5)) |
316 |
321 |
317 lemma PosOrd_RightI: |
322 lemma PosOrd_RightI: |
318 assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2" |
323 assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2" |
319 shows "Right v1 :\<sqsubset>val Right v2" |
324 shows "Right v1 :\<sqsubset>val Right v2" |
320 using assms |
325 using assms |
321 unfolding PosOrd_ex_def test |
326 unfolding PosOrd_ex_def PosOrd_def2 |
322 apply(auto simp add: pflat_len_simps) |
327 apply(auto simp add: pflat_len_simps) |
323 by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5)) |
328 by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5)) |
324 |
329 |
325 |
330 |
326 lemma PosOrd_Right_eq: |
331 lemma PosOrd_Right_eq: |
329 using assms PosOrd_RightE PosOrd_RightI |
334 using assms PosOrd_RightE PosOrd_RightI |
330 by blast |
335 by blast |
331 |
336 |
332 |
337 |
333 lemma PosOrd_SeqI1: |
338 lemma PosOrd_SeqI1: |
334 assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
339 assumes "v1 :\<sqsubset>val w1" "flat (Seq v1 v2) = flat (Seq w1 w2)" |
335 shows "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" |
340 shows "Seq v1 v2 :\<sqsubset>val Seq w1 w2" |
336 using assms(1) |
341 using assms(1) |
337 apply(subst (asm) PosOrd_ex_def) |
342 apply(subst (asm) PosOrd_ex_def) |
338 apply(subst (asm) PosOrd_def) |
343 apply(subst (asm) PosOrd_def) |
339 apply(clarify) |
344 apply(clarify) |
340 apply(subst PosOrd_ex_def) |
345 apply(subst PosOrd_ex_def) |
345 apply(rule ballI) |
350 apply(rule ballI) |
346 apply(rule impI) |
351 apply(rule impI) |
347 apply(simp only: Pos.simps) |
352 apply(simp only: Pos.simps) |
348 apply(auto)[1] |
353 apply(auto)[1] |
349 apply(simp add: pflat_len_simps) |
354 apply(simp add: pflat_len_simps) |
|
355 apply(auto simp add: pflat_len_simps) |
350 using assms(2) |
356 using assms(2) |
351 apply(simp) |
357 apply(simp) |
352 apply(auto simp add: pflat_len_simps) |
358 apply(metis length_append of_nat_add) |
353 by (metis length_append of_nat_add) |
359 done |
354 |
360 |
355 lemma PosOrd_SeqI2: |
361 lemma PosOrd_SeqI2: |
356 assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'" |
362 assumes "v2 :\<sqsubset>val w2" "flat v2 = flat w2" |
357 shows "Seq v v2 :\<sqsubset>val Seq v v2'" |
363 shows "Seq v v2 :\<sqsubset>val Seq v w2" |
358 using assms(1) |
364 using assms(1) |
359 apply(subst (asm) PosOrd_ex_def) |
365 apply(subst (asm) PosOrd_ex_def) |
360 apply(subst (asm) PosOrd_def) |
366 apply(subst (asm) PosOrd_def) |
361 apply(clarify) |
367 apply(clarify) |
362 apply(subst PosOrd_ex_def) |
368 apply(subst PosOrd_ex_def) |
372 using assms(2) |
378 using assms(2) |
373 apply(simp) |
379 apply(simp) |
374 apply(auto simp add: pflat_len_simps) |
380 apply(auto simp add: pflat_len_simps) |
375 done |
381 done |
376 |
382 |
377 lemma PosOrd_SeqE: |
383 lemma PosOrd_Seq_eq: |
378 assumes "Seq v1 v2 :\<sqsubset>val Seq v1' v2'" |
384 assumes "flat v2 = flat w2" |
379 shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'" |
385 shows "(Seq v v2) :\<sqsubset>val (Seq v w2) \<longleftrightarrow> v2 :\<sqsubset>val w2" |
380 using assms |
386 using assms |
|
387 apply(auto) |
|
388 prefer 2 |
|
389 apply(simp add: PosOrd_SeqI2) |
381 apply(simp add: PosOrd_ex_def) |
390 apply(simp add: PosOrd_ex_def) |
382 apply(erule exE) |
391 apply(auto) |
383 apply(case_tac p) |
392 apply(case_tac p) |
384 apply(simp add: PosOrd_def) |
393 apply(simp add: PosOrd_def pflat_len_simps) |
385 apply(auto simp add: pflat_len_simps)[1] |
|
386 apply(rule_tac x="[]" in exI) |
|
387 apply(drule_tac x="[]" in spec) |
|
388 apply(simp add: Pos_empty pflat_len_simps) |
|
389 apply(case_tac a) |
394 apply(case_tac a) |
390 apply(rule disjI1) |
395 apply(simp add: PosOrd_def pflat_len_simps) |
391 apply(simp add: PosOrd_def) |
396 apply(clarify) |
392 apply(auto simp add: pflat_len_simps)[1] |
397 apply(case_tac nat) |
|
398 prefer 2 |
|
399 apply(simp add: PosOrd_def pflat_len_simps pflat_len_outside) |
393 apply(rule_tac x="list" in exI) |
400 apply(rule_tac x="list" in exI) |
394 apply(simp) |
401 apply(auto simp add: PosOrd_def2 pflat_len_simps) |
395 apply(rule ballI) |
402 apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2)) |
396 apply(rule impI) |
403 apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2)) |
397 apply(drule_tac x="0#q" in bspec) |
404 done |
398 apply(simp) |
405 |
399 apply(simp add: pflat_len_simps) |
406 |
400 apply(case_tac nat) |
|
401 apply(rule disjI2) |
|
402 apply(simp add: PosOrd_def) |
|
403 apply(auto simp add: pflat_len_simps) |
|
404 apply(rule_tac x="list" in exI) |
|
405 apply(simp add: Pos_empty) |
|
406 apply(rule ballI) |
|
407 apply(rule impI) |
|
408 apply(auto)[1] |
|
409 apply(drule_tac x="Suc 0#q" in bspec) |
|
410 apply(simp) |
|
411 apply(simp add: pflat_len_simps) |
|
412 apply(drule_tac x="Suc 0#q" in bspec) |
|
413 apply(simp) |
|
414 apply(simp add: pflat_len_simps) |
|
415 apply(simp add: PosOrd_def pflat_len_def) |
|
416 done |
|
417 |
407 |
418 lemma PosOrd_StarsI: |
408 lemma PosOrd_StarsI: |
419 assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)" |
409 assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)" |
420 shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)" |
410 shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)" |
421 using assms(1) |
411 using assms(1) |
497 apply(simp) |
487 apply(simp) |
498 apply(simp add: PosOrd_StarsE2) |
488 apply(simp add: PosOrd_StarsE2) |
499 done |
489 done |
500 |
490 |
501 lemma PosOrd_Stars_append_eq: |
491 lemma PosOrd_Stars_append_eq: |
502 assumes "flat (Stars vs1) = flat (Stars vs2)" |
492 assumes "flats vs1 = flats vs2" |
503 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
493 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
504 using assms |
494 using assms |
505 apply(rule_tac iffI) |
495 apply(rule_tac iffI) |
506 apply(erule PosOrd_Stars_appendE) |
496 apply(erule PosOrd_Stars_appendE) |
507 apply(rule PosOrd_Stars_appendI) |
497 apply(rule PosOrd_Stars_appendI) |
508 apply(auto) |
498 apply(auto) |
509 done |
499 done |
510 |
500 |
511 lemma PosOrd_almost_trichotomous: |
501 lemma PosOrd_almost_trichotomous: |
512 shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))" |
502 shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (length (flat v1) = length (flat v2))" |
513 apply(auto simp add: PosOrd_ex_def) |
503 apply(auto simp add: PosOrd_ex_def) |
514 apply(auto simp add: PosOrd_def) |
504 apply(auto simp add: PosOrd_def) |
515 apply(rule_tac x="[]" in exI) |
505 apply(rule_tac x="[]" in exI) |
516 apply(auto simp add: Pos_empty pflat_len_simps) |
506 apply(auto simp add: Pos_empty pflat_len_simps) |
517 apply(drule_tac x="[]" in spec) |
507 apply(drule_tac x="[]" in spec) |
518 apply(auto simp add: Pos_empty pflat_len_simps) |
508 apply(auto simp add: Pos_empty pflat_len_simps) |
519 done |
509 done |
520 |
|
521 |
|
522 lemma PosOrd_SeqE2: |
|
523 assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
|
524 shows "v1 :\<sqsubset>val v1' \<or> (intlen (flat v1) = intlen (flat v1') \<and> v2 :\<sqsubset>val v2')" |
|
525 using assms |
|
526 apply(frule_tac PosOrd_SeqE) |
|
527 apply(erule disjE) |
|
528 apply(simp) |
|
529 apply(case_tac "v1 :\<sqsubset>val v1'") |
|
530 apply(simp) |
|
531 apply(rule disjI2) |
|
532 apply(rule conjI) |
|
533 prefer 2 |
|
534 apply(simp) |
|
535 apply(auto) |
|
536 apply(auto simp add: PosOrd_ex_def) |
|
537 apply(auto simp add: PosOrd_def pflat_len_simps) |
|
538 apply(case_tac p) |
|
539 apply(auto simp add: PosOrd_def pflat_len_simps) |
|
540 apply(case_tac a) |
|
541 apply(auto simp add: PosOrd_def pflat_len_simps) |
|
542 apply (metis PosOrd_SeqI1 PosOrd_def PosOrd_ex_def PosOrd_shorterI PosOrd_assym assms less_linear) |
|
543 by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def PosOrd_assym assms of_nat_eq_iff) |
|
544 |
|
545 lemma PosOrd_SeqE4: |
|
546 assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
|
547 shows "v1 :\<sqsubset>val v1' \<or> (flat v1 = flat v1' \<and> v2 :\<sqsubset>val v2')" |
|
548 using assms |
|
549 apply(frule_tac PosOrd_SeqE) |
|
550 apply(erule disjE) |
|
551 apply(simp) |
|
552 apply(case_tac "v1 :\<sqsubset>val v1'") |
|
553 apply(simp) |
|
554 apply(rule disjI2) |
|
555 apply(rule conjI) |
|
556 prefer 2 |
|
557 apply(simp) |
|
558 apply(auto) |
|
559 apply(case_tac "length (flat v1') < length (flat v1)") |
|
560 using PosOrd_shorterI apply blast |
|
561 by (metis PosOrd_SeqI1 PosOrd_shorterI PosOrd_assym antisym_conv3 append_eq_append_conv assms(2)) |
|
562 |
510 |
563 |
511 |
564 |
512 |
565 section {* The Posix Value is smaller than any other Value *} |
513 section {* The Posix Value is smaller than any other Value *} |
566 |
514 |
669 using PosOrd_spreI as1(1) eqs by blast |
617 using PosOrd_spreI as1(1) eqs by blast |
670 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3) |
618 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3) |
671 by (auto simp add: LV_def) |
619 by (auto simp add: LV_def) |
672 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
620 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
673 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
621 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
674 thm PosOrd_SeqI1 PosOrd_SeqI2 |
622 unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_Seq_eq) |
675 unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) |
|
676 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
623 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
677 next |
624 next |
678 case (Posix_STAR1 s1 r v s2 vs v3) |
625 case (Posix_STAR1 s1 r v s2 vs v3) |
679 have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
626 have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
680 then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2)) |
627 then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2)) |
773 using Posix_LV \<open>s \<in> r \<rightarrow> vposix\<close> by blast |
720 using Posix_LV \<open>s \<in> r \<rightarrow> vposix\<close> by blast |
774 qed |
721 qed |
775 |
722 |
776 lemma Least_existence1: |
723 lemma Least_existence1: |
777 assumes "LV r s \<noteq> {}" |
724 assumes "LV r s \<noteq> {}" |
|
725 shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
|
726 using Least_existence[OF assms] assms |
|
727 using PosOrdeq_antisym by blast |
|
728 |
|
729 |
|
730 |
|
731 |
|
732 |
|
733 lemma Least_existence1_pre: |
|
734 assumes "LV r s \<noteq> {}" |
778 shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v" |
735 shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v" |
779 using Least_existence[OF assms] assms |
736 using Least_existence[OF assms] assms |
780 apply - |
737 apply - |
781 apply(erule bexE) |
738 apply(erule bexE) |
782 apply(rule_tac a="vmin" in ex1I) |
739 apply(rule_tac a="vmin" in ex1I) |