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