1 |
1 |
2 |
2 |
3 (*** Deadlock examples from section 5.6 ***) |
3 (*** Deadlock examples from section 5.6 ***) |
4 |
4 |
5 (*Trivial, two-process case*) |
5 (*Trivial, two-process case*) |
6 goalw thy [constrains_def, stable_def] |
6 Goalw [constrains_def, stable_def] |
7 "!!Acts. [| constrains Acts (A Int B) A; constrains Acts (B Int A) B |] \ |
7 "!!Acts. [| constrains Acts (A Int B) A; constrains Acts (B Int A) B |] \ |
8 \ ==> stable Acts (A Int B)"; |
8 \ ==> stable Acts (A Int B)"; |
9 by (Blast_tac 1); |
9 by (Blast_tac 1); |
10 result(); |
10 result(); |
11 |
11 |
12 |
12 |
13 goal thy "{i. i < Suc n} = insert n {i. i < n}"; |
13 Goal "{i. i < Suc n} = insert n {i. i < n}"; |
14 by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1); |
14 by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1); |
15 qed "Collect_less_Suc_insert"; |
15 qed "Collect_less_Suc_insert"; |
16 |
16 |
17 |
17 |
18 goal thy "{i. i <= Suc n} = insert (Suc n) {i. i <= n}"; |
18 Goal "{i. i <= Suc n} = insert (Suc n) {i. i <= n}"; |
19 by (blast_tac (claset() addSEs [le_SucE] addIs [le_SucI]) 1); |
19 by (blast_tac (claset() addSEs [le_SucE] addIs [le_SucI]) 1); |
20 qed "Collect_le_Suc_insert"; |
20 qed "Collect_le_Suc_insert"; |
21 |
21 |
22 |
22 |
23 (*a simplification step*) |
23 (*a simplification step*) |
24 goal thy "(INT i:{i. i <= n}. A(Suc i) Int A i) = \ |
24 Goal "(INT i:{i. i <= n}. A(Suc i) Int A i) = \ |
25 \ (INT i:{i. i <= Suc n}. A i)"; |
25 \ (INT i:{i. i <= Suc n}. A i)"; |
26 by (induct_tac "n" 1); |
26 by (induct_tac "n" 1); |
27 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Collect_le_Suc_insert]))); |
27 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Collect_le_Suc_insert]))); |
28 by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1); |
28 by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1); |
29 qed "Collect_le_Int_equals"; |
29 qed "Collect_le_Int_equals"; |
30 |
30 |
31 |
31 |
32 (*Dual of the required property. Converse inclusion fails.*) |
32 (*Dual of the required property. Converse inclusion fails.*) |
33 goal thy "(UN i:{i. i < n}. A i) Int Compl (A n) <= \ |
33 Goal "(UN i:{i. i < n}. A i) Int Compl (A n) <= \ |
34 \ (UN i:{i. i < n}. (A i) Int Compl (A(Suc i)))"; |
34 \ (UN i:{i. i < n}. (A i) Int Compl (A(Suc i)))"; |
35 by (induct_tac "n" 1); |
35 by (induct_tac "n" 1); |
36 by (Asm_simp_tac 1); |
36 by (Asm_simp_tac 1); |
37 by (simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1); |
37 by (simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1); |
38 by (Blast_tac 1); |
38 by (Blast_tac 1); |
39 qed "UN_Int_Compl_subset"; |
39 qed "UN_Int_Compl_subset"; |
40 |
40 |
41 |
41 |
42 (*Converse inclusion fails.*) |
42 (*Converse inclusion fails.*) |
43 goal thy "(INT i:{i. i < n}. Compl(A i) Un A (Suc i)) <= \ |
43 Goal "(INT i:{i. i < n}. Compl(A i) Un A (Suc i)) <= \ |
44 \ (INT i:{i. i < n}. Compl(A i)) Un A n"; |
44 \ (INT i:{i. i < n}. Compl(A i)) Un A n"; |
45 by (induct_tac "n" 1); |
45 by (induct_tac "n" 1); |
46 by (Asm_simp_tac 1); |
46 by (Asm_simp_tac 1); |
47 by (asm_simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1); |
47 by (asm_simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1); |
48 by (Blast_tac 1); |
48 by (Blast_tac 1); |
49 qed "INT_Un_Compl_subset"; |
49 qed "INT_Un_Compl_subset"; |
50 |
50 |
51 |
51 |
52 (*Specialized rewriting*) |
52 (*Specialized rewriting*) |
53 goal thy "A 0 Int (Compl (A n) Int \ |
53 Goal "A 0 Int (Compl (A n) Int \ |
54 \ (INT i:{i. i < n}. Compl(A i) Un A (Suc i))) = {}"; |
54 \ (INT i:{i. i < n}. Compl(A i) Un A (Suc i))) = {}"; |
55 by (blast_tac (claset() addIs [gr0I] |
55 by (blast_tac (claset() addIs [gr0I] |
56 addDs [impOfSubs INT_Un_Compl_subset]) 1); |
56 addDs [impOfSubs INT_Un_Compl_subset]) 1); |
57 val lemma = result(); |
57 val lemma = result(); |
58 |
58 |
59 (*Reverse direction makes it harder to invoke the ind hyp*) |
59 (*Reverse direction makes it harder to invoke the ind hyp*) |
60 goal thy "(INT i:{i. i <= n}. A i) = \ |
60 Goal "(INT i:{i. i <= n}. A i) = \ |
61 \ A 0 Int (INT i:{i. i < n}. Compl(A i) Un A(Suc i))"; |
61 \ A 0 Int (INT i:{i. i < n}. Compl(A i) Un A(Suc i))"; |
62 by (induct_tac "n" 1); |
62 by (induct_tac "n" 1); |
63 by (Asm_simp_tac 1); |
63 by (Asm_simp_tac 1); |
64 by (asm_simp_tac |
64 by (asm_simp_tac |
65 (simpset() addsimps (Int_ac @ |
65 (simpset() addsimps (Int_ac @ |
66 [Int_Un_distrib, Int_Un_distrib2, lemma, |
66 [Int_Un_distrib, Int_Un_distrib2, lemma, |
67 Collect_less_Suc_insert, Collect_le_Suc_insert])) 1); |
67 Collect_less_Suc_insert, Collect_le_Suc_insert])) 1); |
68 qed "INT_le_equals_Int"; |
68 qed "INT_le_equals_Int"; |
69 |
69 |
70 goal thy "(INT i:{i. i <= Suc n}. A i) = \ |
70 Goal "(INT i:{i. i <= Suc n}. A i) = \ |
71 \ A 0 Int (INT i:{i. i <= n}. Compl(A i) Un A(Suc i))"; |
71 \ A 0 Int (INT i:{i. i <= n}. Compl(A i) Un A(Suc i))"; |
72 by (simp_tac (simpset() addsimps [le_eq_less_Suc RS sym, |
72 by (simp_tac (simpset() addsimps [le_eq_less_Suc RS sym, |
73 INT_le_equals_Int]) 1); |
73 INT_le_equals_Int]) 1); |
74 qed "INT_le_Suc_equals_Int"; |
74 qed "INT_le_Suc_equals_Int"; |
75 |
75 |