# Theory Priority

theory Priority
imports PriorityAux
```(*  Title:      HOL/UNITY/Comp/Priority.thy
Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
*)

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"
― ‹the initial state›

text‹Following the definitions given in section 4.4›

definition highest :: "[vertex, (vertex*vertex)set]=>bool"
where "highest i r ⟷ A i r = {}"
― ‹i has highest priority in r›

definition lowest :: "[vertex, (vertex*vertex)set]=>bool"
where "lowest i r ⟷ R i r = {}"
― ‹i has lowest priority in 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"
― ‹Every ``above'' set has a maximal vertex›
where "Maximal = (⋂i. {s. ~highest i s-->(∃j ∈ above i  s. highest j s)})"

definition Maximal' :: "state set"
― ‹Maximal vertex: equivalent definition›
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)})"

(* Composition of a finite set of component;
the vertex 'UNIV' is finite by assumption *)

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}"

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 (ensures_tac "act i", blast+)
done

text‹or better›
lemma Component_yields_priority': "Component i ∈ Highest i ensures Lowest i"
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}"

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)
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 (auto intro!: constrains_INT system_co [THEN constrains_weaken]
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›

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_tac [2] Lowest_above_subset)
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 ={}}"

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_tac x = "above i xa" in above_decreases_lemma)
apply blast+
done

(** Just a massage of conditions to have the desired form ***)
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
apply (case_tac "m={}")
apply (rule Int_lower2 [THEN [2] leadsTo_weaken_L])