22 |
21 |
23 (**** Component correctness proofs ****) |
22 (**** Component correctness proofs ****) |
24 |
23 |
25 (* neighbors is stable *) |
24 (* neighbors is stable *) |
26 Goal "Component i: stable {s. neighbors k s = n}"; |
25 Goal "Component i: stable {s. neighbors k s = n}"; |
|
26 by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); |
27 by (constrains_tac 1); |
27 by (constrains_tac 1); |
28 by Auto_tac; |
28 by Auto_tac; |
29 qed "Component_neighbors_stable"; |
29 qed "Component_neighbors_stable"; |
30 |
30 |
31 (* property 4 *) |
31 (* property 4 *) |
32 Goal |
32 Goal "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}"; |
33 "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}"; |
33 by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); |
34 by (constrains_tac 1); |
34 by (constrains_tac 1); |
35 qed "Component_waits_priority"; |
35 qed "Component_waits_priority"; |
36 |
36 |
37 (* property 5: charpentier and Chandy mistakenly express it as |
37 (* property 5: charpentier and Chandy mistakenly express it as |
38 'transient Highest i'. Consider the case where i has neighbors *) |
38 'transient Highest i'. Consider the case where i has neighbors *) |
39 Goal |
39 Goal |
40 "Component i: {s. neighbors i s ~= {}} Int Highest i \ |
40 "Component i: {s. neighbors i s ~= {}} Int Highest i \ |
41 \ ensures - Highest i"; |
41 \ ensures - Highest i"; |
|
42 by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); |
42 by (ensures_tac "act i" 1); |
43 by (ensures_tac "act i" 1); |
43 by (REPEAT(Fast_tac 1)); |
44 by (REPEAT(Fast_tac 1)); |
44 qed "Component_yields_priority"; |
45 qed "Component_yields_priority"; |
45 |
46 |
46 (* or better *) |
47 (* or better *) |
47 Goal "Component i: Highest i ensures Lowest i"; |
48 Goal "Component i: Highest i ensures Lowest i"; |
|
49 by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); |
48 by (ensures_tac "act i" 1); |
50 by (ensures_tac "act i" 1); |
49 by (REPEAT(Fast_tac 1)); |
51 by (REPEAT(Fast_tac 1)); |
50 qed "Component_yields_priority'"; |
52 qed "Component_yields_priority'"; |
51 |
53 |
52 (* property 6: Component doesn't introduce cycle *) |
54 (* property 6: Component doesn't introduce cycle *) |
53 Goal "Component i: Highest i co Highest i Un Lowest i"; |
55 Goal "Component i: Highest i co Highest i Un Lowest i"; |
|
56 by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); |
54 by (constrains_tac 1); |
57 by (constrains_tac 1); |
55 by (Fast_tac 1); |
58 by (Fast_tac 1); |
56 qed "Component_well_behaves"; |
59 qed "Component_well_behaves"; |
57 |
60 |
58 (* property 7: local axiom *) |
61 (* property 7: local axiom *) |
59 Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}"; |
62 Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}"; |
|
63 by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); |
60 by (constrains_tac 1); |
64 by (constrains_tac 1); |
61 qed "locality"; |
65 qed "locality"; |
62 |
66 |
63 |
67 |
64 (**** System properties ****) |
68 (**** System properties ****) |
65 (* property 8: strictly universal *) |
69 (* property 8: strictly universal *) |
66 |
70 |
67 Goalw [Safety_def] |
71 Goalw [Safety_def] "system: stable Safety"; |
68 "system: stable Safety"; |
|
69 by (rtac stable_INT 1); |
72 by (rtac stable_INT 1); |
|
73 by (asm_full_simp_tac (simpset() addsimps [system_def]) 1); |
70 by (constrains_tac 1); |
74 by (constrains_tac 1); |
71 by (Fast_tac 1); |
75 by (Fast_tac 1); |
72 qed "Safety"; |
76 qed "Safety"; |
73 |
77 |
74 (* property 13: universal *) |
78 (* property 13: universal *) |
75 Goal |
79 Goal "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}"; |
76 "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}"; |
80 by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1); |
77 by (constrains_tac 1); |
81 by (constrains_tac 1); |
78 by (Blast_tac 1); |
82 by (Blast_tac 1); |
79 qed "p13"; |
83 qed "p13"; |
80 |
84 |
81 (* property 14: the 'above set' of a Component that hasn't got |
85 (* property 14: the 'above set' of a Component that hasn't got |
82 priority doesn't increase *) |
86 priority doesn't increase *) |
83 Goal |
87 Goal |
84 "ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}"; |
88 "ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}"; |
85 by (Clarify_tac 1); |
89 by (Clarify_tac 1); |
86 by (cut_inst_tac [("i", "j")] reach_lemma 1); |
90 by (cut_inst_tac [("i", "j")] reach_lemma 1); |
|
91 by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1); |
87 by (constrains_tac 1); |
92 by (constrains_tac 1); |
88 by (auto_tac (claset(), simpset() addsimps [trancl_converse])); |
93 by (auto_tac (claset(), simpset() addsimps [trancl_converse])); |
89 qed "above_not_increase"; |
94 qed "above_not_increase"; |
90 |
95 |
91 Goal |
96 Goal |