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