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