1 Deadlock = UNITY |
1 (* Title: HOL/UNITY/Deadlock |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Deadlock examples from section 5.6 of |
|
7 Misra, "A Logic for Concurrent Programming", 1994 |
|
8 *) |
|
9 |
|
10 theory Deadlock = UNITY: |
|
11 |
|
12 (*Trivial, two-process case*) |
|
13 lemma "[| F : (A Int B) co A; F : (B Int A) co B |] ==> F : stable (A Int B)" |
|
14 by (unfold constrains_def stable_def, blast) |
|
15 |
|
16 |
|
17 (*a simplification step*) |
|
18 lemma Collect_le_Int_equals: |
|
19 "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)" |
|
20 apply (induct_tac "n") |
|
21 apply (simp_all (no_asm_simp) add: atMost_Suc) |
|
22 apply auto |
|
23 done |
|
24 |
|
25 (*Dual of the required property. Converse inclusion fails.*) |
|
26 lemma UN_Int_Compl_subset: |
|
27 "(UN i: lessThan n. A i) Int (- A n) <= |
|
28 (UN i: lessThan n. (A i) Int (- A (Suc i)))" |
|
29 apply (induct_tac "n") |
|
30 apply (simp (no_asm_simp)) |
|
31 apply (simp (no_asm) add: lessThan_Suc) |
|
32 apply blast |
|
33 done |
|
34 |
|
35 |
|
36 (*Converse inclusion fails.*) |
|
37 lemma INT_Un_Compl_subset: |
|
38 "(INT i: lessThan n. -A i Un A (Suc i)) <= |
|
39 (INT i: lessThan n. -A i) Un A n" |
|
40 apply (induct_tac "n") |
|
41 apply (simp (no_asm_simp)) |
|
42 apply (simp (no_asm_simp) add: lessThan_Suc) |
|
43 apply blast |
|
44 done |
|
45 |
|
46 |
|
47 (*Specialized rewriting*) |
|
48 lemma INT_le_equals_Int_lemma: |
|
49 "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}" |
|
50 by (blast intro: gr0I dest: INT_Un_Compl_subset [THEN subsetD]) |
|
51 |
|
52 (*Reverse direction makes it harder to invoke the ind hyp*) |
|
53 lemma INT_le_equals_Int: |
|
54 "(INT i: atMost n. A i) = |
|
55 A 0 Int (INT i: lessThan n. -A i Un A(Suc i))" |
|
56 apply (induct_tac "n", simp) |
|
57 apply (simp add: Int_ac Int_Un_distrib Int_Un_distrib2 |
|
58 INT_le_equals_Int_lemma lessThan_Suc atMost_Suc) |
|
59 done |
|
60 |
|
61 lemma INT_le_Suc_equals_Int: |
|
62 "(INT i: atMost (Suc n). A i) = |
|
63 A 0 Int (INT i: atMost n. -A i Un A(Suc i))" |
|
64 by (simp add: lessThan_Suc_atMost INT_le_equals_Int) |
|
65 |
|
66 |
|
67 (*The final deadlock example*) |
|
68 lemma |
|
69 assumes zeroprem: "F : (A 0 Int A (Suc n)) co (A 0)" |
|
70 and allprem: |
|
71 "!!i. i: atMost n ==> F : (A(Suc i) Int A i) co (-A i Un A(Suc i))" |
|
72 shows "F : stable (INT i: atMost (Suc n). A i)" |
|
73 apply (unfold stable_def) |
|
74 apply (rule constrains_Int [THEN constrains_weaken]) |
|
75 apply (rule zeroprem) |
|
76 apply (rule constrains_INT) |
|
77 apply (erule allprem) |
|
78 apply (simp add: Collect_le_Int_equals Int_assoc INT_absorb) |
|
79 apply (simp add: INT_le_Suc_equals_Int) |
|
80 done |
|
81 |
|
82 end |