author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 16417 9bc16273c2d4 child 26824 32e612e77edb permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     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 imports UNITY begin
```
```    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
```