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