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