327 apply clarify |
327 apply clarify |
328 apply(case_tac i,simp,simp) |
328 apply(case_tac i,simp,simp) |
329 apply(rule_tac x=0 in exI,simp) |
329 apply(rule_tac x=0 in exI,simp) |
330 done |
330 done |
331 |
331 |
332 lemma Basic_sound: |
332 lemma Basic_sound: |
333 " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar; |
333 " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar; |
334 stable pre rely; stable post rely\<rbrakk> |
334 stable pre rely; stable post rely\<rbrakk> |
335 \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]" |
335 \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]" |
336 apply(unfold com_validity_def) |
336 apply(unfold com_validity_def) |
337 apply clarify |
337 apply clarify |
367 apply clarify |
367 apply clarify |
368 apply simp |
368 apply simp |
369 apply(drule_tac s="Some (Basic f)" in sym,simp) |
369 apply(drule_tac s="Some (Basic f)" in sym,simp) |
370 apply(case_tac "x!Suc j",simp) |
370 apply(case_tac "x!Suc j",simp) |
371 apply(rule ctran.elims,simp) |
371 apply(rule ctran.elims,simp) |
372 apply(simp_all) |
372 apply(simp_all) |
373 apply(drule_tac c=sa in subsetD,simp) |
373 apply(drule_tac c=sa in subsetD,simp) |
374 apply clarify |
374 apply clarify |
375 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all) |
375 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all) |
376 apply(case_tac x,simp+) |
376 apply(case_tac x,simp+) |
377 apply(erule_tac x=i in allE) |
377 apply(erule_tac x=i in allE) |
378 apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all) |
378 apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all) |
|
379 apply arith+ |
379 apply(case_tac x) |
380 apply(case_tac x) |
380 apply(simp add:last_length)+ |
381 apply(simp add:last_length)+ |
381 done |
382 done |
382 |
383 |
383 subsubsection{* Soundness of the Await rule *} |
384 subsubsection{* Soundness of the Await rule *} |
384 |
385 |
385 lemma unique_ctran_Await [rule_format]: |
386 lemma unique_ctran_Await [rule_format]: |
494 apply clarify |
495 apply clarify |
495 apply simp |
496 apply simp |
496 apply(drule_tac s="Some (Await b P)" in sym,simp) |
497 apply(drule_tac s="Some (Await b P)" in sym,simp) |
497 apply(case_tac "x!Suc j",simp) |
498 apply(case_tac "x!Suc j",simp) |
498 apply(rule ctran.elims,simp) |
499 apply(rule ctran.elims,simp) |
499 apply(simp_all) |
500 apply(simp_all) |
500 apply(drule Star_imp_cptn) |
501 apply(drule Star_imp_cptn) |
501 apply clarify |
502 apply clarify |
502 apply(erule_tac x=sa in allE) |
503 apply(erule_tac x=sa in allE) |
503 apply clarify |
504 apply clarify |
504 apply(erule_tac x=sa in allE) |
505 apply(erule_tac x=sa in allE) |
508 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp) |
509 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp) |
509 apply(erule etran.elims,simp) |
510 apply(erule etran.elims,simp) |
510 apply simp |
511 apply simp |
511 apply clarify |
512 apply clarify |
512 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all) |
513 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all) |
513 apply(case_tac x,simp+) |
514 apply(case_tac x,simp+) |
514 apply(erule_tac x=i in allE) |
515 apply(erule_tac x=i in allE) |
515 apply(erule_tac i=j in unique_ctran_Await,force,simp_all) |
516 apply(erule_tac i=j in unique_ctran_Await,force,simp_all) |
|
517 apply arith+ |
516 apply(case_tac x) |
518 apply(case_tac x) |
517 apply(simp add:last_length)+ |
519 apply(simp add:last_length)+ |
518 done |
520 done |
519 |
521 |
520 subsubsection{* Soundness of the Conditional rule *} |
522 subsubsection{* Soundness of the Conditional rule *} |
521 |
|
522 ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *) |
|
523 |
523 |
524 lemma Cond_sound: |
524 lemma Cond_sound: |
525 "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post]; |
525 "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post]; |
526 \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk> |
526 \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk> |
527 \<Longrightarrow> \<Turnstile> (Cond b P1 P2) sat [pre, rely, guar, post]" |
527 \<Longrightarrow> \<Turnstile> (Cond b P1 P2) sat [pre, rely, guar, post]" |
535 apply(frule_tac j="0" and k="length x - 1" and p=pre in stability,simp+) |
535 apply(frule_tac j="0" and k="length x - 1" and p=pre in stability,simp+) |
536 apply(case_tac x,simp+) |
536 apply(case_tac x,simp+) |
537 apply(simp add:assum_def) |
537 apply(simp add:assum_def) |
538 apply(simp add:assum_def) |
538 apply(simp add:assum_def) |
539 apply(erule_tac m="length x" in etran_or_ctran,simp+) |
539 apply(erule_tac m="length x" in etran_or_ctran,simp+) |
540 apply(case_tac x,simp+) |
|
541 apply(case_tac x, (simp add:last_length)+) |
540 apply(case_tac x, (simp add:last_length)+) |
542 apply(erule exE) |
541 apply(erule exE) |
543 apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence) |
542 apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence) |
544 apply clarify |
543 apply clarify |
545 apply (simp add:assum_def) |
544 apply (simp add:assum_def) |
547 apply(erule_tac m="Suc m" in etran_or_ctran,simp+) |
546 apply(erule_tac m="Suc m" in etran_or_ctran,simp+) |
548 apply(erule ctran.elims,simp_all) |
547 apply(erule ctran.elims,simp_all) |
549 apply(erule_tac x="sa" in allE) |
548 apply(erule_tac x="sa" in allE) |
550 apply(drule_tac c="drop (Suc m) x" in subsetD) |
549 apply(drule_tac c="drop (Suc m) x" in subsetD) |
551 apply simp |
550 apply simp |
552 apply(rule conjI) |
|
553 apply force |
|
554 apply clarify |
551 apply clarify |
555 apply(subgoal_tac "(Suc m) + i \<le> length x") |
|
556 apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x") |
|
557 apply(rotate_tac -2) |
|
558 apply simp |
|
559 apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE) |
|
560 apply(subgoal_tac "Suc (Suc (m + i)) < length x",simp) |
|
561 apply arith |
|
562 apply arith |
|
563 apply arith |
|
564 apply simp |
552 apply simp |
565 apply clarify |
553 apply clarify |
566 apply(case_tac "i\<le>m") |
554 apply(case_tac "i\<le>m") |
567 apply(drule le_imp_less_or_eq) |
555 apply(drule le_imp_less_or_eq) |
568 apply(erule disjE) |
556 apply(erule disjE) |
569 apply(erule_tac x=i in allE, erule impE, assumption) |
557 apply(erule_tac x=i in allE, erule impE, assumption) |
570 apply simp+ |
558 apply simp+ |
571 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE) |
559 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE) |
572 apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x") |
560 apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x") |
573 apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x") |
561 apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x") |
574 apply(rotate_tac -2) |
562 apply(rotate_tac -2) |
575 apply simp |
|
576 apply(erule mp) |
|
577 apply arith |
|
578 apply arith |
|
579 apply arith |
|
580 apply(case_tac "length (drop (Suc m) x)",simp) |
|
581 apply(erule_tac x="sa" in allE) |
|
582 back |
|
583 apply(drule_tac c="drop (Suc m) x" in subsetD,simp) |
|
584 apply(rule conjI) |
|
585 apply force |
|
586 apply clarify |
|
587 apply(subgoal_tac "(Suc m) + i \<le> length x") |
|
588 apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x") |
|
589 apply(rotate_tac -2) |
|
590 apply simp |
|
591 apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE) |
|
592 apply(subgoal_tac "Suc (Suc (m + i)) < length x") |
|
593 apply simp |
|
594 apply arith |
|
595 apply arith |
|
596 apply arith |
|
597 apply simp |
|
598 apply clarify |
|
599 apply(case_tac "i\<le>m") |
|
600 apply(drule le_imp_less_or_eq) |
|
601 apply(erule disjE) |
|
602 apply(erule_tac x=i in allE, erule impE, assumption) |
|
603 apply simp |
|
604 apply simp |
563 apply simp |
605 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE) |
|
606 apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x") |
|
607 apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x") |
|
608 apply(rotate_tac -2) |
|
609 apply simp |
|
610 apply(erule mp) |
|
611 apply arith |
|
612 apply arith |
564 apply arith |
613 apply arith |
565 apply arith |
614 done |
566 apply(case_tac "length (drop (Suc m) x)",simp) |
615 |
567 apply(erule_tac x="sa" in allE) |
616 ML {* fast_arith_split_limit := 9; *} (* FIXME *) |
568 back |
|
569 apply(drule_tac c="drop (Suc m) x" in subsetD,simp) |
|
570 apply clarify |
|
571 apply simp |
|
572 apply clarify |
|
573 apply(case_tac "i\<le>m") |
|
574 apply(drule le_imp_less_or_eq) |
|
575 apply(erule disjE) |
|
576 apply(erule_tac x=i in allE, erule impE, assumption) |
|
577 apply simp |
|
578 apply simp |
|
579 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE) |
|
580 apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x") |
|
581 apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x") |
|
582 apply(rotate_tac -2) |
|
583 apply simp |
|
584 apply arith |
|
585 apply arith |
|
586 done |
617 |
587 |
618 subsubsection{* Soundness of the Sequential rule *} |
588 subsubsection{* Soundness of the Sequential rule *} |
619 |
589 |
620 inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t" |
590 inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t" |
621 |
591 |
654 apply(simp only :nth_append length_map last_length nth_map) |
624 apply(simp only :nth_append length_map last_length nth_map) |
655 apply(case_tac "last((Some P, sa) # xs)") |
625 apply(case_tac "last((Some P, sa) # xs)") |
656 apply(simp add:lift_def) |
626 apply(simp add:lift_def) |
657 apply simp |
627 apply simp |
658 done |
628 done |
659 |
|
660 declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del] |
629 declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del] |
661 |
630 |
662 lemma Seq_sound2 [rule_format]: |
631 lemma Seq_sound2 [rule_format]: |
663 "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x |
632 "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x |
664 \<longrightarrow> fst(x!i)=Some Q \<longrightarrow> |
633 \<longrightarrow> fst(x!i)=Some Q \<longrightarrow> |
734 apply(erule ssubst) |
702 apply(erule ssubst) |
735 apply (simp add:lift_def) |
703 apply (simp add:lift_def) |
736 apply(case_tac "(x # xs) ! length xs",simp) |
704 apply(case_tac "(x # xs) ! length xs",simp) |
737 apply simp |
705 apply simp |
738 done |
706 done |
739 |
|
740 ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *) |
|
741 |
707 |
742 lemma Seq_sound: |
708 lemma Seq_sound: |
743 "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk> |
709 "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk> |
744 \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]" |
710 \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]" |
745 apply(unfold com_validity_def) |
711 apply(unfold com_validity_def) |
874 apply(rule conjI,clarify) |
838 apply(rule conjI,clarify) |
875 apply(case_tac ys,simp+) |
839 apply(case_tac ys,simp+) |
876 apply clarify |
840 apply clarify |
877 apply(case_tac ys,simp+) |
841 apply(case_tac ys,simp+) |
878 done |
842 done |
879 |
|
880 ML {* fast_arith_split_limit := 9; *} (* FIXME *) |
|
881 |
843 |
882 subsubsection{* Soundness of the While rule *} |
844 subsubsection{* Soundness of the While rule *} |
883 |
845 |
884 lemma last_append[rule_format]: |
846 lemma last_append[rule_format]: |
885 "\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))" |
847 "\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))" |
921 apply(erule mp) |
883 apply(erule mp) |
922 apply(case_tac "last xs") |
884 apply(case_tac "last xs") |
923 apply(simp add:lift_def) |
885 apply(simp add:lift_def) |
924 apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps) |
886 apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps) |
925 done |
887 done |
926 |
|
927 ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *) |
|
928 |
888 |
929 lemma While_sound_aux [rule_format]: |
889 lemma While_sound_aux [rule_format]: |
930 "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar; |
890 "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar; |
931 stable pre rely; stable post rely; x \<in> cptn_mod \<rbrakk> |
891 stable pre rely; stable post rely; x \<in> cptn_mod \<rbrakk> |
932 \<Longrightarrow> \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)" |
892 \<Longrightarrow> \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)" |
1090 apply (simp del:map.simps last.simps) |
1050 apply (simp del:map.simps last.simps) |
1091 apply simp |
1051 apply simp |
1092 apply simp |
1052 apply simp |
1093 done |
1053 done |
1094 |
1054 |
1095 ML {* fast_arith_split_limit := 9; *} (* FIXME *) |
|
1096 |
|
1097 lemma While_sound: |
1055 lemma While_sound: |
1098 "\<lbrakk>stable pre rely; pre \<inter> - b \<subseteq> post; stable post rely; |
1056 "\<lbrakk>stable pre rely; pre \<inter> - b \<subseteq> post; stable post rely; |
1099 \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk> |
1057 \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk> |
1100 \<Longrightarrow> \<Turnstile> While b P sat [pre, rely, guar, post]" |
1058 \<Longrightarrow> \<Turnstile> While b P sat [pre, rely, guar, post]" |
1101 apply(unfold com_validity_def) |
1059 apply(unfold com_validity_def) |