1(* Title: HOL/UNITY/Comp/Priority.thy 2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory 3 Copyright 2001 University of Cambridge 4*) 5 6section\<open>The priority system\<close> 7 8theory Priority imports PriorityAux begin 9 10text\<open>From Charpentier and Chandy, 11Examples of Program Composition Illustrating the Use of Universal Properties 12 In J. Rolim (editor), Parallel and Distributed Processing, 13 Spriner LNCS 1586 (1999), pages 1215-1227.\<close> 14 15type_synonym state = "(vertex*vertex)set" 16type_synonym command = "vertex=>(state*state)set" 17 18consts 19 init :: "(vertex*vertex)set" 20 \<comment> \<open>the initial state\<close> 21 22text\<open>Following the definitions given in section 4.4\<close> 23 24definition highest :: "[vertex, (vertex*vertex)set]=>bool" 25 where "highest i r \<longleftrightarrow> A i r = {}" 26 \<comment> \<open>i has highest priority in r\<close> 27 28definition lowest :: "[vertex, (vertex*vertex)set]=>bool" 29 where "lowest i r \<longleftrightarrow> R i r = {}" 30 \<comment> \<open>i has lowest priority in r\<close> 31 32definition act :: command 33 where "act i = {(s, s'). s'=reverse i s & highest i s}" 34 35definition Component :: "vertex=>state program" 36 where "Component i = mk_total_program({init}, {act i}, UNIV)" 37 \<comment> \<open>All components start with the same initial state\<close> 38 39 40text\<open>Some Abbreviations\<close> 41definition Highest :: "vertex=>state set" 42 where "Highest i = {s. highest i s}" 43 44definition Lowest :: "vertex=>state set" 45 where "Lowest i = {s. lowest i s}" 46 47definition Acyclic :: "state set" 48 where "Acyclic = {s. acyclic s}" 49 50 51definition Maximal :: "state set" 52 \<comment> \<open>Every ``above'' set has a maximal vertex\<close> 53 where "Maximal = (\<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i s. highest j s)})" 54 55definition Maximal' :: "state set" 56 \<comment> \<open>Maximal vertex: equivalent definition\<close> 57 where "Maximal' = (\<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j))" 58 59 60definition Safety :: "state set" 61 where "Safety = (\<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)})" 62 63 64 (* Composition of a finite set of component; 65 the vertex 'UNIV' is finite by assumption *) 66 67definition system :: "state program" 68 where "system = (\<Squnion>i. Component i)" 69 70 71declare highest_def [simp] lowest_def [simp] 72declare Highest_def [THEN def_set_simp, simp] 73 and Lowest_def [THEN def_set_simp, simp] 74 75declare Component_def [THEN def_prg_Init, simp] 76declare act_def [THEN def_act_simp, simp] 77 78 79 80subsection\<open>Component correctness proofs\<close> 81 82text\<open>neighbors is stable\<close> 83lemma Component_neighbors_stable: "Component i \<in> stable {s. neighbors k s = n}" 84by (simp add: Component_def, safety, auto) 85 86text\<open>property 4\<close> 87lemma Component_waits_priority: "Component i \<in> {s. ((i,j) \<in> s) = b} \<inter> (- Highest i) co {s. ((i,j) \<in> s)=b}" 88by (simp add: Component_def, safety) 89 90text\<open>property 5: charpentier and Chandy mistakenly express it as 91 'transient Highest i'. Consider the case where i has neighbors\<close> 92lemma Component_yields_priority: 93 "Component i \<in> {s. neighbors i s \<noteq> {}} Int Highest i 94 ensures - Highest i" 95apply (simp add: Component_def) 96apply (ensures_tac "act i", blast+) 97done 98 99text\<open>or better\<close> 100lemma Component_yields_priority': "Component i \<in> Highest i ensures Lowest i" 101apply (simp add: Component_def) 102apply (ensures_tac "act i", blast+) 103done 104 105text\<open>property 6: Component doesn't introduce cycle\<close> 106lemma Component_well_behaves: "Component i \<in> Highest i co Highest i Un Lowest i" 107by (simp add: Component_def, safety, fast) 108 109text\<open>property 7: local axiom\<close> 110lemma locality: "Component i \<in> stable {s. \<forall>j k. j\<noteq>i & k\<noteq>i--> ((j,k) \<in> s) = b j k}" 111by (simp add: Component_def, safety) 112 113 114subsection\<open>System properties\<close> 115text\<open>property 8: strictly universal\<close> 116 117lemma Safety: "system \<in> stable Safety" 118apply (unfold Safety_def) 119apply (rule stable_INT) 120apply (simp add: system_def, safety, fast) 121done 122 123text\<open>property 13: universal\<close> 124lemma p13: "system \<in> {s. s = q} co {s. s=q} Un {s. \<exists>i. derive i q s}" 125by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, blast) 126 127text\<open>property 14: the 'above set' of a Component that hasn't got 128 priority doesn't increase\<close> 129lemma above_not_increase: 130 "system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}" 131apply (insert reach_lemma [of concl: j]) 132apply (simp add: system_def Component_def mk_total_program_def totalize_JN, 133 safety) 134apply (simp add: trancl_converse, blast) 135done 136 137lemma above_not_increase': 138 "system \<in> -Highest i Int {s. above i s = x} co {s. above i s <= x}" 139apply (insert above_not_increase [of i]) 140apply (simp add: trancl_converse constrains_def, blast) 141done 142 143 144 145text\<open>p15: universal property: all Components well behave\<close> 146lemma system_well_behaves: "system \<in> Highest i co Highest i Un Lowest i" 147 by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, auto) 148 149 150lemma Acyclic_eq: "Acyclic = (\<Inter>i. {s. i\<notin>above i s})" 151 by (auto simp add: Acyclic_def acyclic_def trancl_converse) 152 153 154lemmas system_co = 155 constrains_Un [OF above_not_increase [rule_format] system_well_behaves] 156 157lemma Acyclic_stable: "system \<in> stable Acyclic" 158apply (simp add: stable_def Acyclic_eq) 159apply (auto intro!: constrains_INT system_co [THEN constrains_weaken] 160 simp add: image0_r_iff_image0_trancl trancl_converse) 161done 162 163 164lemma Acyclic_subset_Maximal: "Acyclic <= Maximal" 165apply (unfold Acyclic_def Maximal_def, clarify) 166apply (drule above_lemma_b, auto) 167done 168 169text\<open>property 17: original one is an invariant\<close> 170lemma Acyclic_Maximal_stable: "system \<in> stable (Acyclic Int Maximal)" 171by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable) 172 173 174text\<open>property 5: existential property\<close> 175 176lemma Highest_leadsTo_Lowest: "system \<in> Highest i leadsTo Lowest i" 177apply (simp add: system_def Component_def mk_total_program_def totalize_JN) 178apply (ensures_tac "act i", auto) 179done 180 181text\<open>a lowest i can never be in any abover set\<close> 182lemma Lowest_above_subset: "Lowest i <= (\<Inter>k. {s. i\<notin>above k s})" 183by (auto simp add: image0_r_iff_image0_trancl trancl_converse) 184 185text\<open>property 18: a simpler proof than the original, one which uses psp\<close> 186lemma Highest_escapes_above: "system \<in> Highest i leadsTo (\<Inter>k. {s. i\<notin>above k s})" 187apply (rule leadsTo_weaken_R) 188apply (rule_tac [2] Lowest_above_subset) 189apply (rule Highest_leadsTo_Lowest) 190done 191 192lemma Highest_escapes_above': 193 "system \<in> Highest j Int {s. j \<in> above i s} leadsTo {s. j\<notin>above i s}" 194by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower]) 195 196subsection\<open>The main result: above set decreases\<close> 197 198text\<open>The original proof of the following formula was wrong\<close> 199 200lemma Highest_iff_above0: "Highest i = {s. above i s ={}}" 201by (auto simp add: image0_trancl_iff_image0_r) 202 203lemmas above_decreases_lemma = 204 psp [THEN leadsTo_weaken, OF Highest_escapes_above' above_not_increase'] 205 206 207lemma above_decreases: 208 "system \<in> (\<Union>j. {s. above i s = x} Int {s. j \<in> above i s} Int Highest j) 209 leadsTo {s. above i s < x}" 210apply (rule leadsTo_UN) 211apply (rule single_leadsTo_I, clarify) 212apply (rule_tac x = "above i xa" in above_decreases_lemma) 213apply (simp_all (no_asm_use) add: Highest_iff_above0) 214apply blast+ 215done 216 217(** Just a massage of conditions to have the desired form ***) 218lemma Maximal_eq_Maximal': "Maximal = Maximal'" 219by (unfold Maximal_def Maximal'_def Highest_def, blast) 220 221lemma Acyclic_subset: 222 "x\<noteq>{} ==> 223 Acyclic Int {s. above i s = x} <= 224 (\<Union>j. {s. above i s = x} Int {s. j \<in> above i s} Int Highest j)" 225apply (rule_tac B = "Maximal' Int {s. above i s = x}" in subset_trans) 226apply (simp (no_asm) add: Maximal_eq_Maximal' [symmetric]) 227apply (blast intro: Acyclic_subset_Maximal [THEN subsetD]) 228apply (simp (no_asm) del: above_def add: Maximal'_def Highest_iff_above0) 229apply blast 230done 231 232lemmas above_decreases' = leadsTo_weaken_L [OF above_decreases Acyclic_subset] 233lemmas above_decreases_psp = psp_stable [OF above_decreases' Acyclic_stable] 234 235lemma above_decreases_psp': 236"x\<noteq>{}==> system \<in> Acyclic Int {s. above i s = x} leadsTo 237 Acyclic Int {s. above i s < x}" 238by (erule above_decreases_psp [THEN leadsTo_weaken], blast, auto) 239 240 241lemmas finite_psubset_induct = wf_finite_psubset [THEN leadsTo_wf_induct] 242 243 244lemma Progress: "system \<in> Acyclic leadsTo Highest i" 245apply (rule_tac f = "%s. above i s" in finite_psubset_induct) 246apply (simp del: above_def 247 add: Highest_iff_above0 vimage_def finite_psubset_def, clarify) 248apply (case_tac "m={}") 249apply (rule Int_lower2 [THEN [2] leadsTo_weaken_L]) 250apply (force simp add: leadsTo_refl) 251apply (rule_tac A' = "Acyclic Int {x. above i x < m}" in leadsTo_weaken_R) 252apply (blast intro: above_decreases_psp')+ 253done 254 255 256text\<open>We have proved all (relevant) theorems given in the paper. We didn't 257assume any thing about the relation \<^term>\<open>r\<close>. It is not necessary that 258\<^term>\<open>r\<close> be a priority relation as assumed in the original proof. It 259suffices that we start from a state which is finite and acyclic.\<close> 260 261 262end 263