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