Theory Priority
section‹The priority system›
theory Priority imports PriorityAux begin
text‹From Charpentier and Chandy,
Examples of Program Composition Illustrating the Use of Universal Properties
In J. Rolim (editor), Parallel and Distributed Processing,
Spriner LNCS 1586 (1999), pages 1215-1227.›
type_synonym state = "(vertex*vertex)set"
type_synonym command = "vertex=>(state*state)set"
consts
init :: "(vertex*vertex)set"
text‹Following the definitions given in section 4.4›
definition highest :: "[vertex, (vertex*vertex)set]=>bool"
where "highest i r ⟷ A i r = {}"
definition lowest :: "[vertex, (vertex*vertex)set]=>bool"
where "lowest i r ⟷ R i r = {}"
definition act :: command
where "act i = {(s, s'). s'=reverse i s & highest i s}"
definition Component :: "vertex=>state program"
where "Component i = mk_total_program({init}, {act i}, UNIV)"
text‹Some Abbreviations›
definition Highest :: "vertex=>state set"
where "Highest i = {s. highest i s}"
definition Lowest :: "vertex=>state set"
where "Lowest i = {s. lowest i s}"
definition Acyclic :: "state set"
where "Acyclic = {s. acyclic s}"
definition Maximal :: "state set"
where "Maximal = (⋂i. {s. ~highest i s-->(∃j ∈ above i s. highest j s)})"
definition Maximal' :: "state set"
where "Maximal' = (⋂i. Highest i Un (⋃j. {s. j ∈ above i s} Int Highest j))"
definition Safety :: "state set"
where "Safety = (⋂i. {s. highest i s --> (∀j ∈ neighbors i s. ~highest j s)})"
definition system :: "state program"
where "system = (⨆i. Component i)"
declare highest_def [simp] lowest_def [simp]
declare Highest_def [THEN def_set_simp, simp]
and Lowest_def [THEN def_set_simp, simp]
declare Component_def [THEN def_prg_Init, simp]
declare act_def [THEN def_act_simp, simp]
subsection‹Component correctness proofs›
text‹neighbors is stable›
lemma Component_neighbors_stable: "Component i ∈ stable {s. neighbors k s = n}"
by (simp add: Component_def, safety, auto)
text‹property 4›
lemma Component_waits_priority: "Component i ∈ {s. ((i,j) ∈ s) = b} ∩ (- Highest i) co {s. ((i,j) ∈ s)=b}"
by (simp add: Component_def, safety)
text‹property 5: charpentier and Chandy mistakenly express it as
'transient Highest i'. Consider the case where i has neighbors›
lemma Component_yields_priority:
"Component i ∈ {s. neighbors i s ≠ {}} Int Highest i
ensures - Highest i"
apply (simp add: Component_def)
apply (ensures_tac "act i", blast+)
done
text‹or better›
lemma Component_yields_priority': "Component i ∈ Highest i ensures Lowest i"
apply (simp add: Component_def)
apply (ensures_tac "act i", blast+)
done
text‹property 6: Component doesn't introduce cycle›
lemma Component_well_behaves: "Component i ∈ Highest i co Highest i Un Lowest i"
by (simp add: Component_def, safety, fast)
text‹property 7: local axiom›
lemma locality: "Component i ∈ stable {s. ∀j k. j≠i & k≠i--> ((j,k) ∈ s) = b j k}"
by (simp add: Component_def, safety)
subsection‹System properties›
text‹property 8: strictly universal›
lemma Safety: "system ∈ stable Safety"
apply (unfold Safety_def)
apply (rule stable_INT)
apply (simp add: system_def, safety, fast)
done
text‹property 13: universal›
lemma p13: "system ∈ {s. s = q} co {s. s=q} Un {s. ∃i. derive i q s}"
by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, blast)
text‹property 14: the 'above set' of a Component that hasn't got
priority doesn't increase›
lemma above_not_increase:
"system ∈ -Highest i Int {s. j∉above i s} co {s. j∉above i s}"
apply (insert reach_lemma [of concl: j])
apply (simp add: system_def Component_def mk_total_program_def totalize_JN,
safety)
apply (simp add: trancl_converse, blast)
done
lemma above_not_increase':
"system ∈ -Highest i Int {s. above i s = x} co {s. above i s <= x}"
apply (insert above_not_increase [of i])
apply (simp add: trancl_converse constrains_def, blast)
done
text‹p15: universal property: all Components well behave›
lemma system_well_behaves: "system ∈ Highest i co Highest i Un Lowest i"
by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, auto)
lemma Acyclic_eq: "Acyclic = (⋂i. {s. i∉above i s})"
by (auto simp add: Acyclic_def acyclic_def trancl_converse)
lemmas system_co =
constrains_Un [OF above_not_increase [rule_format] system_well_behaves]
lemma Acyclic_stable: "system ∈ stable Acyclic"
apply (simp add: stable_def Acyclic_eq)
apply (auto intro!: constrains_INT system_co [THEN constrains_weaken]
simp add: image0_r_iff_image0_trancl trancl_converse)
done
lemma Acyclic_subset_Maximal: "Acyclic <= Maximal"
apply (unfold Acyclic_def Maximal_def, clarify)
apply (drule above_lemma_b, auto)
done
text‹property 17: original one is an invariant›
lemma Acyclic_Maximal_stable: "system ∈ stable (Acyclic Int Maximal)"
by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable)
text‹property 5: existential property›
lemma Highest_leadsTo_Lowest: "system ∈ Highest i leadsTo Lowest i"
apply (simp add: system_def Component_def mk_total_program_def totalize_JN)
apply (ensures_tac "act i", auto)
done
text‹a lowest i can never be in any abover set›
lemma Lowest_above_subset: "Lowest i <= (⋂k. {s. i∉above k s})"
by (auto simp add: image0_r_iff_image0_trancl trancl_converse)
text‹property 18: a simpler proof than the original, one which uses psp›
lemma Highest_escapes_above: "system ∈ Highest i leadsTo (⋂k. {s. i∉above k s})"
apply (rule leadsTo_weaken_R)
apply (rule_tac [2] Lowest_above_subset)
apply (rule Highest_leadsTo_Lowest)
done
lemma Highest_escapes_above':
"system ∈ Highest j Int {s. j ∈ above i s} leadsTo {s. j∉above i s}"
by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower])
subsection‹The main result: above set decreases›
text‹The original proof of the following formula was wrong›
lemma Highest_iff_above0: "Highest i = {s. above i s ={}}"
by (auto simp add: image0_trancl_iff_image0_r)
lemmas above_decreases_lemma =
psp [THEN leadsTo_weaken, OF Highest_escapes_above' above_not_increase']
lemma above_decreases:
"system ∈ (⋃j. {s. above i s = x} Int {s. j ∈ above i s} Int Highest j)
leadsTo {s. above i s < x}"
apply (rule leadsTo_UN)
apply (rule single_leadsTo_I, clarify)
apply (rule_tac x = "above i xa" in above_decreases_lemma)
apply (simp_all (no_asm_use) add: Highest_iff_above0)
apply blast+
done
lemma Maximal_eq_Maximal': "Maximal = Maximal'"
by (unfold Maximal_def Maximal'_def Highest_def, blast)
lemma Acyclic_subset:
"x≠{} ==>
Acyclic Int {s. above i s = x} <=
(⋃j. {s. above i s = x} Int {s. j ∈ above i s} Int Highest j)"
apply (rule_tac B = "Maximal' Int {s. above i s = x}" in subset_trans)
apply (simp (no_asm) add: Maximal_eq_Maximal' [symmetric])
apply (blast intro: Acyclic_subset_Maximal [THEN subsetD])
apply (simp (no_asm) del: above_def add: Maximal'_def Highest_iff_above0)
apply blast
done
lemmas above_decreases' = leadsTo_weaken_L [OF above_decreases Acyclic_subset]
lemmas above_decreases_psp = psp_stable [OF above_decreases' Acyclic_stable]
lemma above_decreases_psp':
"x≠{}==> system ∈ Acyclic Int {s. above i s = x} leadsTo
Acyclic Int {s. above i s < x}"
by (erule above_decreases_psp [THEN leadsTo_weaken], blast, auto)
lemmas finite_psubset_induct = wf_finite_psubset [THEN leadsTo_wf_induct]
lemma Progress: "system ∈ Acyclic leadsTo Highest i"
apply (rule_tac f = "%s. above i s" in finite_psubset_induct)
apply (simp del: above_def
add: Highest_iff_above0 vimage_def finite_psubset_def, clarify)
apply (case_tac "m={}")
apply (rule Int_lower2 [THEN [2] leadsTo_weaken_L])
apply (force simp add: leadsTo_refl)
apply (rule_tac A' = "Acyclic Int {x. above i x < m}" in leadsTo_weaken_R)
apply (blast intro: above_decreases_psp')+
done
text‹We have proved all (relevant) theorems given in the paper. We didn't
assume any thing about the relation \<^term>‹r›. It is not necessary that
\<^term>‹r› be a priority relation as assumed in the original proof. It
suffices that we start from a state which is finite and acyclic.›
end