# Theory Deadlock

Up to index of Isabelle/HOL/UNITY

theory Deadlock
imports UNITY
begin

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