65 |
65 |
66 |
66 |
67 (*From "A Logic for Concurrent Programming", but not used in Chapter 4. |
67 (*From "A Logic for Concurrent Programming", but not used in Chapter 4. |
68 Note the use of case_tac. Reasoning about leadsTo takes practice!*) |
68 Note the use of case_tac. Reasoning about leadsTo takes practice!*) |
69 Goal "[| i<N; j<N |] ==> \ |
69 Goal "[| i<N; j<N |] ==> \ |
70 \ F : leadsTo (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)"; |
70 \ F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)"; |
71 by (case_tac "i=j" 1); |
71 by (case_tac "i=j" 1); |
72 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
72 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
73 by (rtac (TR7 RS leadsTo_weaken_R) 1); |
73 by (rtac (TR7 RS leadsTo_weaken_R) 1); |
74 by (Clarify_tac 1); |
74 by (Clarify_tac 1); |
75 by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); |
75 by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); |
76 qed "TR7_nodeOrder"; |
76 qed "TR7_nodeOrder"; |
77 |
77 |
78 |
78 |
79 (*Chapter 4 variant, the one actually used below.*) |
79 (*Chapter 4 variant, the one actually used below.*) |
80 Goal "[| i<N; j<N; i~=j |] \ |
80 Goal "[| i<N; j<N; i~=j |] \ |
81 \ ==> F : leadsTo (HasTok i) {s. (token s, i) : nodeOrder j}"; |
81 \ ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}"; |
82 by (rtac (TR7 RS leadsTo_weaken_R) 1); |
82 by (rtac (TR7 RS leadsTo_weaken_R) 1); |
83 by (Clarify_tac 1); |
83 by (Clarify_tac 1); |
84 by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); |
84 by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); |
85 qed "TR7_aux"; |
85 qed "TR7_aux"; |
86 |
86 |
89 by Auto_tac; |
89 by Auto_tac; |
90 val token_lemma = result(); |
90 val token_lemma = result(); |
91 |
91 |
92 |
92 |
93 (*Misra's TR9: the token reaches an arbitrary node*) |
93 (*Misra's TR9: the token reaches an arbitrary node*) |
94 Goal "j<N ==> F : leadsTo {s. token s < N} (HasTok j)"; |
94 Goal "j<N ==> F : {s. token s < N} leadsTo (HasTok j)"; |
95 by (rtac leadsTo_weaken_R 1); |
95 by (rtac leadsTo_weaken_R 1); |
96 by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")] |
96 by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")] |
97 (wf_nodeOrder RS bounded_induct) 1); |
97 (wf_nodeOrder RS bounded_induct) 1); |
98 by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff, |
98 by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff, |
99 HasTok_def]))); |
99 HasTok_def]))); |
103 by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def]))); |
103 by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def]))); |
104 by (ALLGOALS Blast_tac); |
104 by (ALLGOALS Blast_tac); |
105 qed "leadsTo_j"; |
105 qed "leadsTo_j"; |
106 |
106 |
107 (*Misra's TR8: a hungry process eventually eats*) |
107 (*Misra's TR8: a hungry process eventually eats*) |
108 Goal "j<N ==> F : leadsTo ({s. token s < N} Int H j) (E j)"; |
108 Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)"; |
109 by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); |
109 by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); |
110 by (rtac TR6 2); |
110 by (rtac TR6 2); |
111 by (rtac leadsTo_weaken_R 1); |
111 by (rtac leadsTo_weaken_R 1); |
112 by (rtac ([leadsTo_j, TR3] MRS psp) 1); |
112 by (rtac ([leadsTo_j, TR3] MRS psp) 1); |
113 by (ALLGOALS Blast_tac); |
113 by (ALLGOALS Blast_tac); |