(* Title: HOL/UNITY/Deadlock ID: $Id: Deadlock.thy,v 1.4 2005/06/17 14:13:10 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Deadlock examples from section 5.6 of Misra, "A Logic for Concurrent Programming", 1994 *) theory Deadlock imports UNITY begin (*Trivial, two-process case*) lemma "[| F ∈ (A ∩ B) co A; F ∈ (B ∩ A) co B |] ==> F ∈ stable (A ∩ B)" by (unfold constrains_def stable_def, blast) (*a simplification step*) lemma Collect_le_Int_equals: "(\<Inter>i ∈ atMost n. A(Suc i) ∩ A i) = (\<Inter>i ∈ atMost (Suc n). A i)" apply (induct_tac "n") apply (auto simp add: atMost_Suc) done (*Dual of the required property. Converse inclusion fails.*) lemma UN_Int_Compl_subset: "(\<Union>i ∈ lessThan n. A i) ∩ (- A n) ⊆ (\<Union>i ∈ lessThan n. (A i) ∩ (- A (Suc i)))" apply (induct_tac "n", simp) apply (simp add: lessThan_Suc, blast) done (*Converse inclusion fails.*) lemma INT_Un_Compl_subset: "(\<Inter>i ∈ lessThan n. -A i ∪ A (Suc i)) ⊆ (\<Inter>i ∈ lessThan n. -A i) ∪ A n" apply (induct_tac "n", simp) apply (simp add: lessThan_Suc, blast) done (*Specialized rewriting*) lemma INT_le_equals_Int_lemma: "A 0 ∩ (-(A n) ∩ (\<Inter>i ∈ lessThan n. -A i ∪ A (Suc i))) = {}" by (blast intro: gr0I dest: INT_Un_Compl_subset [THEN subsetD]) (*Reverse direction makes it harder to invoke the ind hyp*) lemma INT_le_equals_Int: "(\<Inter>i ∈ atMost n. A i) = A 0 ∩ (\<Inter>i ∈ lessThan n. -A i ∪ A(Suc i))" apply (induct_tac "n", simp) apply (simp add: Int_ac Int_Un_distrib Int_Un_distrib2 INT_le_equals_Int_lemma lessThan_Suc atMost_Suc) done lemma INT_le_Suc_equals_Int: "(\<Inter>i ∈ atMost (Suc n). A i) = A 0 ∩ (\<Inter>i ∈ atMost n. -A i ∪ A(Suc i))" by (simp add: lessThan_Suc_atMost INT_le_equals_Int) (*The final deadlock example*) lemma assumes zeroprem: "F ∈ (A 0 ∩ A (Suc n)) co (A 0)" and allprem: "!!i. i ∈ atMost n ==> F ∈ (A(Suc i) ∩ A i) co (-A i ∪ A(Suc i))" shows "F ∈ stable (\<Inter>i ∈ atMost (Suc n). A i)" apply (unfold stable_def) apply (rule constrains_Int [THEN constrains_weaken]) apply (rule zeroprem) apply (rule constrains_INT) apply (erule allprem) apply (simp add: Collect_le_Int_equals Int_assoc INT_absorb) apply (simp add: INT_le_Suc_equals_Int) done end
lemma
[| F ∈ A ∩ B co A; F ∈ B ∩ A co B |] ==> F ∈ stable (A ∩ B)
lemma Collect_le_Int_equals:
(INT i<=n. A (Suc i) ∩ A i) = (INT i<=Suc n. A i)
lemma UN_Int_Compl_subset:
(UN i<n. A i) ∩ - A n ⊆ (UN i<n. A i ∩ - A (Suc i))
lemma INT_Un_Compl_subset:
(INT i<n. - A i ∪ A (Suc i)) ⊆ (INT i<n. - A i) ∪ A n
lemma INT_le_equals_Int_lemma:
A 0 ∩ (- A n ∩ (INT i<n. - A i ∪ A (Suc i))) = {}
lemma INT_le_equals_Int:
(INT i<=n. A i) = A 0 ∩ (INT i<n. - A i ∪ A (Suc i))
lemma INT_le_Suc_equals_Int:
(INT i<=Suc n. A i) = A 0 ∩ (INT i<=n. - A i ∪ A (Suc i))
lemma
[| F ∈ A 0 ∩ A (Suc n) co A 0; !!i. i ∈ {..n} ==> F ∈ A (Suc i) ∩ A i co - A i ∪ A (Suc i) |] ==> F ∈ stable (INT i<=Suc n. A i)