imports UNITY
```(*  Title:      HOL/UNITY/Simple/Deadlock.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Deadlock examples from section 5.6 of
Misra, "A Logic for Concurrent Programming", 1994
*)

(*Trivial, two-process case*)
lemma "[| F ∈ (A ∩ B) co A;  F ∈ (B ∩ A) co B |] ==> F ∈ stable (A ∩ B)"
unfolding constrains_def stable_def by blast

(*a simplification step*)
lemma Collect_le_Int_equals:
"(⋂i ∈ atMost n. A(Suc i) ∩ A i) = (⋂i ∈ atMost (Suc n). A i)"
by (induct n) (auto simp add: atMost_Suc)

(*Dual of the required property.  Converse inclusion fails.*)
lemma UN_Int_Compl_subset:
"(⋃i ∈ lessThan n. A i) ∩ (- A n) ⊆
(⋃i ∈ lessThan n. (A i) ∩ (- A (Suc i)))"
by (induct n) (auto simp: lessThan_Suc)

(*Converse inclusion fails.*)
lemma INT_Un_Compl_subset:
"(⋂i ∈ lessThan n. -A i ∪ A (Suc i))  ⊆
(⋂i ∈ lessThan n. -A i) ∪ A n"
by (induct n) (auto simp: lessThan_Suc)

(*Specialized rewriting*)
lemma INT_le_equals_Int_lemma:
"A 0 ∩ (-(A n) ∩ (⋂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:
"(⋂i ∈ atMost n. A i) =
A 0 ∩ (⋂i ∈ lessThan n. -A i ∪ A(Suc i))"
by (induct n)
INT_le_equals_Int_lemma lessThan_Suc atMost_Suc)

lemma INT_le_Suc_equals_Int:
"(⋂i ∈ atMost (Suc n). A i) =
A 0 ∩ (⋂i ∈ atMost n. -A i ∪ A(Suc i))"

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 (⋂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)