src/HOL/UNITY/Simple/Token.thy
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13806 fd40c9d9076b
child 15618 05bad476e0f0
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
     1 (*  Title:      HOL/UNITY/Token
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 The Token Ring.
     7 
     8 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
     9 *)
    10 
    11 
    12 theory Token = WFair:
    13 
    14 (*process states*)
    15 datatype pstate = Hungry | Eating | Thinking
    16 
    17 record state =
    18   token :: "nat"
    19   proc  :: "nat => pstate"
    20 
    21 
    22 constdefs
    23   HasTok :: "nat => state set"
    24     "HasTok i == {s. token s = i}"
    25 
    26   H :: "nat => state set"
    27     "H i == {s. proc s i = Hungry}"
    28 
    29   E :: "nat => state set"
    30     "E i == {s. proc s i = Eating}"
    31 
    32   T :: "nat => state set"
    33     "T i == {s. proc s i = Thinking}"
    34 
    35 
    36 locale Token =
    37   fixes N and F and nodeOrder and "next"   
    38   defines nodeOrder_def:
    39        "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    40 	 	       (lessThan N <*> lessThan N)"
    41       and next_def:
    42        "next i == (Suc i) mod N"
    43   assumes N_positive [iff]: "0<N"
    44       and TR2:  "F \<in> (T i) co (T i \<union> H i)"
    45       and TR3:  "F \<in> (H i) co (H i \<union> E i)"
    46       and TR4:  "F \<in> (H i - HasTok i) co (H i)"
    47       and TR5:  "F \<in> (HasTok i) co (HasTok i \<union> -(E i))"
    48       and TR6:  "F \<in> (H i \<inter> HasTok i) leadsTo (E i)"
    49       and TR7:  "F \<in> (HasTok i) leadsTo (HasTok (next i))"
    50 
    51 
    52 lemma HasToK_partition: "[| s \<in> HasTok i; s \<in> HasTok j |] ==> i=j"
    53 by (unfold HasTok_def, auto)
    54 
    55 lemma not_E_eq: "(s \<notin> E i) = (s \<in> H i | s \<in> T i)"
    56 apply (simp add: H_def E_def T_def)
    57 apply (case_tac "proc s i", auto)
    58 done
    59 
    60 lemma (in Token) token_stable: "F \<in> stable (-(E i) \<union> (HasTok i))"
    61 apply (unfold stable_def)
    62 apply (rule constrains_weaken)
    63 apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
    64 apply (auto simp add: not_E_eq)
    65 apply (simp_all add: H_def E_def T_def)
    66 done
    67 
    68 
    69 (*** Progress under weak fairness ***)
    70 
    71 lemma (in Token) wf_nodeOrder: "wf(nodeOrder j)"
    72 apply (unfold nodeOrder_def)
    73 apply (rule wf_less_than [THEN wf_inv_image, THEN wf_subset], blast)
    74 done
    75 
    76 lemma (in Token) nodeOrder_eq: 
    77      "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
    78 apply (unfold nodeOrder_def next_def inv_image_def)
    79 apply (auto simp add: mod_Suc mod_geq)
    80 apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
    81 done
    82 
    83 (*From "A Logic for Concurrent Programming", but not used in Chapter 4.
    84   Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
    85 lemma (in Token) TR7_nodeOrder:
    86      "[| i<N; j<N |] ==>    
    87       F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
    88 apply (case_tac "i=j")
    89 apply (blast intro: subset_imp_leadsTo)
    90 apply (rule TR7 [THEN leadsTo_weaken_R])
    91 apply (auto simp add: HasTok_def nodeOrder_eq)
    92 done
    93 
    94 
    95 (*Chapter 4 variant, the one actually used below.*)
    96 lemma (in Token) TR7_aux: "[| i<N; j<N; i\<noteq>j |]     
    97       ==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
    98 apply (rule TR7 [THEN leadsTo_weaken_R])
    99 apply (auto simp add: HasTok_def nodeOrder_eq)
   100 done
   101 
   102 lemma (in Token) token_lemma:
   103      "({s. token s < N} \<inter> token -` {m}) = (if m<N then token -` {m} else {})"
   104 by auto
   105 
   106 
   107 (*Misra's TR9: the token reaches an arbitrary node*)
   108 lemma  (in Token) leadsTo_j: "j<N ==> F \<in> {s. token s < N} leadsTo (HasTok j)"
   109 apply (rule leadsTo_weaken_R)
   110 apply (rule_tac I = "-{j}" and f = token and B = "{}" 
   111        in wf_nodeOrder [THEN bounded_induct])
   112 apply (simp_all (no_asm_simp) add: token_lemma vimage_Diff HasTok_def)
   113  prefer 2 apply blast
   114 apply clarify
   115 apply (rule TR7_aux [THEN leadsTo_weaken])
   116 apply (auto simp add: HasTok_def nodeOrder_def)
   117 done
   118 
   119 (*Misra's TR8: a hungry process eventually eats*)
   120 lemma (in Token) token_progress:
   121      "j<N ==> F \<in> ({s. token s < N} \<inter> H j) leadsTo (E j)"
   122 apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
   123 apply (rule_tac [2] TR6)
   124 apply (rule psp [OF leadsTo_j TR3, THEN leadsTo_weaken], blast+)
   125 done
   126 
   127 
   128 end