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