760 |
760 |
761 (* Frequently needed abbreviation: distinguish between idling and non-idling |
761 (* Frequently needed abbreviation: distinguish between idling and non-idling |
762 steps of the implementation, and try to solve the idling case by simplification |
762 steps of the implementation, and try to solve the idling case by simplification |
763 *) |
763 *) |
764 ML {* |
764 ML {* |
765 fun split_idle_tac ss simps i = |
765 fun split_idle_tac ctxt simps i = |
766 TRY (rtac @{thm actionI} i) THEN |
766 let val ss = Simplifier.local_simpset_of ctxt in |
767 case_split_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN |
767 TRY (rtac @{thm actionI} i) THEN |
768 rewrite_goals_tac @{thms action_rews} THEN |
768 InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN |
769 forward_tac [temp_use @{thm Step1_4_7}] i THEN |
769 rewrite_goals_tac @{thms action_rews} THEN |
770 asm_full_simp_tac (ss addsimps simps) i |
770 forward_tac [temp_use @{thm Step1_4_7}] i THEN |
|
771 asm_full_simp_tac (ss addsimps simps) i |
|
772 end |
771 *} |
773 *} |
772 (* ---------------------------------------------------------------------- |
774 (* ---------------------------------------------------------------------- |
773 Combine steps 1.2 and 1.4 to prove that the implementation satisfies |
775 Combine steps 1.2 and 1.4 to prove that the implementation satisfies |
774 the specification's next-state relation. |
776 the specification's next-state relation. |
775 *) |
777 *) |
777 (* Steps that leave all variables unchanged are safe, so I may assume |
779 (* Steps that leave all variables unchanged are safe, so I may assume |
778 that some variable changes in the proof that a step is safe. *) |
780 that some variable changes in the proof that a step is safe. *) |
779 lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p) |
781 lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p) |
780 --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)) |
782 --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)) |
781 --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" |
783 --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" |
782 apply (tactic {* split_idle_tac @{simpset} [thm "square_def"] 1 *}) |
784 apply (tactic {* split_idle_tac @{context} [thm "square_def"] 1 *}) |
783 apply force |
785 apply force |
784 done |
786 done |
785 (* turn into (unsafe, looping!) introduction rule *) |
787 (* turn into (unsafe, looping!) introduction rule *) |
786 lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use], standard] |
788 lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use], standard] |
787 |
789 |
849 |
851 |
850 (* ------------------------------ State S1 ------------------------------ *) |
852 (* ------------------------------ State S1 ------------------------------ *) |
851 |
853 |
852 lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
854 lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
853 --> (S1 rmhist p)$ | (S2 rmhist p)$" |
855 --> (S1 rmhist p)$ | (S2 rmhist p)$" |
854 apply (tactic "split_idle_tac @{simpset} [] 1") |
856 apply (tactic "split_idle_tac @{context} [] 1") |
855 apply (auto dest!: Step1_2_1 [temp_use]) |
857 apply (auto dest!: Step1_2_1 [temp_use]) |
856 done |
858 done |
857 |
859 |
858 (* Show that the implementation can satisfy the high-level fairness requirements |
860 (* Show that the implementation can satisfy the high-level fairness requirements |
859 by entering the state S1 infinitely often. |
861 by entering the state S1 infinitely often. |
883 |
885 |
884 (* ------------------------------ State S2 ------------------------------ *) |
886 (* ------------------------------ State S2 ------------------------------ *) |
885 |
887 |
886 lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
888 lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
887 --> (S2 rmhist p)$ | (S3 rmhist p)$" |
889 --> (S2 rmhist p)$ | (S3 rmhist p)$" |
888 apply (tactic "split_idle_tac @{simpset} [] 1") |
890 apply (tactic "split_idle_tac @{context} [] 1") |
889 apply (auto dest!: Step1_2_2 [temp_use]) |
891 apply (auto dest!: Step1_2_2 [temp_use]) |
890 done |
892 done |
891 |
893 |
892 lemma S2MClkFwd_successors: "|- ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
894 lemma S2MClkFwd_successors: "|- ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
893 & <MClkFwd memCh crCh cst p>_(c p) |
895 & <MClkFwd memCh crCh cst p>_(c p) |
909 |
911 |
910 (* ------------------------------ State S3 ------------------------------ *) |
912 (* ------------------------------ State S3 ------------------------------ *) |
911 |
913 |
912 lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
914 lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
913 --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$" |
915 --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$" |
914 apply (tactic "split_idle_tac @{simpset} [] 1") |
916 apply (tactic "split_idle_tac @{context} [] 1") |
915 apply (auto dest!: Step1_2_3 [temp_use]) |
917 apply (auto dest!: Step1_2_3 [temp_use]) |
916 done |
918 done |
917 |
919 |
918 lemma S3RPC_successors: "|- ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
920 lemma S3RPC_successors: "|- ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
919 & <RPCNext crCh rmCh rst p>_(r p) |
921 & <RPCNext crCh rmCh rst p>_(r p) |
937 (* ------------- State S4 -------------------------------------------------- *) |
939 (* ------------- State S4 -------------------------------------------------- *) |
938 |
940 |
939 lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
941 lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
940 & (ALL l. $MemInv mm l) |
942 & (ALL l. $MemInv mm l) |
941 --> (S4 rmhist p)$ | (S5 rmhist p)$" |
943 --> (S4 rmhist p)$ | (S5 rmhist p)$" |
942 apply (tactic "split_idle_tac @{simpset} [] 1") |
944 apply (tactic "split_idle_tac @{context} [] 1") |
943 apply (auto dest!: Step1_2_4 [temp_use]) |
945 apply (auto dest!: Step1_2_4 [temp_use]) |
944 done |
946 done |
945 |
947 |
946 (* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *) |
948 (* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *) |
947 |
949 |
948 lemma S4a_successors: "|- $(S4 rmhist p & ires!p = #NotAResult) |
950 lemma S4a_successors: "|- $(S4 rmhist p & ires!p = #NotAResult) |
949 & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l) |
951 & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l) |
950 --> (S4 rmhist p & ires!p = #NotAResult)$ |
952 --> (S4 rmhist p & ires!p = #NotAResult)$ |
951 | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$" |
953 | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$" |
952 apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *}) |
954 apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *}) |
953 apply (auto dest!: Step1_2_4 [temp_use]) |
955 apply (auto dest!: Step1_2_4 [temp_use]) |
954 done |
956 done |
955 |
957 |
956 lemma S4aRNext_successors: "|- ($(S4 rmhist p & ires!p = #NotAResult) |
958 lemma S4aRNext_successors: "|- ($(S4 rmhist p & ires!p = #NotAResult) |
957 & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)) |
959 & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)) |
978 (* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *) |
980 (* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *) |
979 |
981 |
980 lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult) |
982 lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult) |
981 & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l) |
983 & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l) |
982 --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$" |
984 --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$" |
983 apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *}) |
985 apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *}) |
984 apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use]) |
986 apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use]) |
985 done |
987 done |
986 |
988 |
987 lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p ~= #NotAResult) |
989 lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p ~= #NotAResult) |
988 & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
990 & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
1007 |
1009 |
1008 (* ------------------------------ State S5 ------------------------------ *) |
1010 (* ------------------------------ State S5 ------------------------------ *) |
1009 |
1011 |
1010 lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
1012 lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
1011 --> (S5 rmhist p)$ | (S6 rmhist p)$" |
1013 --> (S5 rmhist p)$ | (S6 rmhist p)$" |
1012 apply (tactic "split_idle_tac @{simpset} [] 1") |
1014 apply (tactic "split_idle_tac @{context} [] 1") |
1013 apply (auto dest!: Step1_2_5 [temp_use]) |
1015 apply (auto dest!: Step1_2_5 [temp_use]) |
1014 done |
1016 done |
1015 |
1017 |
1016 lemma S5RPC_successors: "|- ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
1018 lemma S5RPC_successors: "|- ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
1017 & <RPCNext crCh rmCh rst p>_(r p) |
1019 & <RPCNext crCh rmCh rst p>_(r p) |
1033 |
1035 |
1034 (* ------------------------------ State S6 ------------------------------ *) |
1036 (* ------------------------------ State S6 ------------------------------ *) |
1035 |
1037 |
1036 lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
1038 lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) |
1037 --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$" |
1039 --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$" |
1038 apply (tactic "split_idle_tac @{simpset} [] 1") |
1040 apply (tactic "split_idle_tac @{context} [] 1") |
1039 apply (auto dest!: Step1_2_6 [temp_use]) |
1041 apply (auto dest!: Step1_2_6 [temp_use]) |
1040 done |
1042 done |
1041 |
1043 |
1042 lemma S6MClkReply_successors: |
1044 lemma S6MClkReply_successors: |
1043 "|- ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
1045 "|- ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) |
1248 & $ImpInv rmhist p |
1250 & $ImpInv rmhist p |
1249 --> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)" |
1251 --> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)" |
1250 apply clarsimp |
1252 apply clarsimp |
1251 apply (drule WriteS4 [action_use]) |
1253 apply (drule WriteS4 [action_use]) |
1252 apply assumption |
1254 apply assumption |
1253 apply (tactic "split_idle_tac @{simpset} [] 1") |
1255 apply (tactic "split_idle_tac @{context} [] 1") |
1254 apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use] |
1256 apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use] |
1255 S4RPCUnch [temp_use]) |
1257 S4RPCUnch [temp_use]) |
1256 apply (auto simp: square_def dest: S4Write [temp_use]) |
1258 apply (auto simp: square_def dest: S4Write [temp_use]) |
1257 done |
1259 done |
1258 |
1260 |