src/HOL/UNITY/Comp/Priority.ML
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13796 19f50fa807ae
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
paulson@11194
     1
(*  Title:      HOL/UNITY/Priority
paulson@11194
     2
    ID:         $Id$
paulson@11194
     3
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
paulson@11194
     4
    Copyright   2001  University of Cambridge
paulson@11194
     5
paulson@11194
     6
The priority system
paulson@11194
     7
paulson@11194
     8
From Charpentier and Chandy,
paulson@11194
     9
Examples of Program Composition Illustrating the Use of Universal Properties
paulson@11194
    10
   In J. Rolim (editor), Parallel and Distributed Processing,
paulson@11194
    11
   Spriner LNCS 1586 (1999), pages 1215-1227.
paulson@11194
    12
*)
paulson@11194
    13
paulson@11194
    14
Addsimps [Component_def RS def_prg_Init];
paulson@11194
    15
Addsimps [highest_def, lowest_def];
paulson@11194
    16
Addsimps [simp_of_act  act_def];
paulson@11194
    17
Addsimps (map simp_of_set [Highest_def, Lowest_def]);
paulson@11194
    18
paulson@11194
    19
paulson@11194
    20
paulson@11194
    21
paulson@11194
    22
(**** Component correctness proofs  ****)
paulson@11194
    23
paulson@11194
    24
(* neighbors is stable  *)
paulson@11194
    25
Goal "Component i: stable {s. neighbors k s = n}";
paulson@13796
    26
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
paulson@11194
    27
by (constrains_tac 1);
paulson@11194
    28
by Auto_tac;
paulson@11194
    29
qed "Component_neighbors_stable";
paulson@11194
    30
paulson@11194
    31
(* property 4 *)
paulson@13796
    32
Goal "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}";
paulson@13796
    33
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
paulson@11194
    34
by (constrains_tac 1);
paulson@11194
    35
qed "Component_waits_priority";  
paulson@11194
    36
paulson@11194
    37
(* property 5: charpentier and Chandy mistakenly express it as
paulson@11194
    38
 'transient Highest i'. Consider the case where i has neighbors *)
paulson@11194
    39
Goal
paulson@11194
    40
 "Component i: {s. neighbors i s ~= {}} Int Highest i \
paulson@11194
    41
\              ensures - Highest i";
paulson@13796
    42
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
paulson@11194
    43
by (ensures_tac "act i" 1);
paulson@11194
    44
by (REPEAT(Fast_tac 1));
paulson@11194
    45
qed "Component_yields_priority"; 
paulson@11194
    46
paulson@11194
    47
(* or better *)
paulson@11194
    48
Goal "Component i: Highest i ensures Lowest i";
paulson@13796
    49
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
paulson@11194
    50
by (ensures_tac "act i" 1);
paulson@11194
    51
by (REPEAT(Fast_tac 1));
paulson@11194
    52
qed "Component_yields_priority'";
paulson@11194
    53
paulson@11194
    54
(* property 6: Component doesn't introduce cycle *)
paulson@11194
    55
Goal "Component i: Highest i co Highest i Un Lowest i";
paulson@13796
    56
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
paulson@11194
    57
by (constrains_tac 1);
paulson@11194
    58
by (Fast_tac 1);
paulson@11194
    59
qed "Component_well_behaves"; 
paulson@11194
    60
paulson@11194
    61
(* property 7: local axiom *)
paulson@11194
    62
Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}";
paulson@13796
    63
by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
paulson@11194
    64
by (constrains_tac 1);
paulson@11194
    65
qed "locality";  
paulson@11194
    66
paulson@11194
    67
paulson@11194
    68
(**** System  properties  ****)
paulson@11194
    69
(* property 8: strictly universal *)
paulson@11194
    70
paulson@13796
    71
Goalw [Safety_def] "system: stable Safety";
paulson@11194
    72
by (rtac stable_INT 1);
paulson@13796
    73
by (asm_full_simp_tac (simpset() addsimps [system_def]) 1); 
paulson@11194
    74
by (constrains_tac 1);
paulson@11194
    75
by (Fast_tac 1);
paulson@11194
    76
qed "Safety"; 
paulson@11194
    77
paulson@11194
    78
(* property 13: universal *)
paulson@13796
    79
Goal "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
paulson@13812
    80
by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
paulson@11194
    81
by (constrains_tac 1);
paulson@11194
    82
by (Blast_tac 1);
paulson@11194
    83
qed "p13";
paulson@11194
    84
paulson@11194
    85
(* property 14: the 'above set' of a Component that hasn't got 
paulson@11194
    86
      priority doesn't increase *)
paulson@11194
    87
Goal
paulson@11194
    88
"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}";
paulson@11194
    89
by (Clarify_tac 1);
paulson@11194
    90
by (cut_inst_tac [("i", "j")] reach_lemma 1);
paulson@13812
    91
by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
paulson@11194
    92
by (constrains_tac 1);
paulson@11194
    93
by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
paulson@11194
    94
qed "above_not_increase";  
paulson@11194
    95
paulson@13812
    96
Goal "system: -Highest i Int {s. above i s = x} co {s. above i s <= x}";
paulson@11194
    97
by (cut_inst_tac [("i", "i")] above_not_increase 1);
paulson@13812
    98
by (asm_full_simp_tac
paulson@13812
    99
    (simpset() addsimps [trancl_converse, constrains_def]) 1); 
paulson@11194
   100
by (Blast_tac 1);
paulson@11194
   101
qed "above_not_increase'";  
paulson@11194
   102
paulson@11194
   103
paulson@11194
   104
paulson@11194
   105
(* p15: universal property: all Components well behave  *)
paulson@11194
   106
Goal "ALL i. system: Highest i co Highest i Un Lowest i";
paulson@11194
   107
by (Clarify_tac 1);
paulson@13812
   108
by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
paulson@11194
   109
by (constrains_tac 1);
paulson@11194
   110
by Auto_tac;
paulson@11194
   111
qed "system_well_behaves";  
paulson@11194
   112
paulson@11194
   113
paulson@11194
   114
Goal "Acyclic = (INT i. {s. i~:above i s})";
paulson@11194
   115
by (auto_tac (claset(), simpset() 
paulson@11194
   116
   addsimps [Acyclic_def, acyclic_def, trancl_converse]));
paulson@11194
   117
qed "Acyclic_eq";
paulson@11194
   118
paulson@11194
   119
paulson@11194
   120
val lemma = [above_not_increase RS spec, 
paulson@11194
   121
           system_well_behaves RS spec] MRS constrains_Un;
paulson@11194
   122
Goal 
paulson@11194
   123
"system: stable Acyclic";
paulson@11194
   124
by (auto_tac (claset() addSIs [stable_INT, stableI, 
paulson@11194
   125
                               lemma RS constrains_weaken],
paulson@11194
   126
              simpset() addsimps [Acyclic_eq, 
paulson@11194
   127
                    image0_r_iff_image0_trancl,trancl_converse]));
paulson@11194
   128
qed "Acyclic_stable";
paulson@11194
   129
paulson@11194
   130
paulson@11194
   131
Goalw [Acyclic_def, Maximal_def]
paulson@11194
   132
"Acyclic <= Maximal";
paulson@11194
   133
by (Clarify_tac 1);
paulson@11194
   134
by (dtac above_lemma_b 1);
paulson@11194
   135
by Auto_tac;
paulson@11194
   136
qed "Acyclic_subset_Maximal";
paulson@11194
   137
paulson@11194
   138
(* property 17: original one is an invariant *)
paulson@11194
   139
Goal 
paulson@11194
   140
"system: stable (Acyclic Int Maximal)";
paulson@11194
   141
by (simp_tac (simpset() addsimps 
paulson@11194
   142
     [Acyclic_subset_Maximal RS Int_absorb2, Acyclic_stable]) 1);
paulson@11194
   143
qed "Acyclic_Maximal_stable";  
paulson@11194
   144
paulson@11194
   145
paulson@11194
   146
(* propert 5: existential property *)
paulson@11194
   147
paulson@11194
   148
Goal "system: Highest i leadsTo Lowest i";
paulson@13812
   149
by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
paulson@11194
   150
by (ensures_tac "act i" 1);
paulson@13812
   151
by Auto_tac;
paulson@11194
   152
qed "Highest_leadsTo_Lowest";
paulson@11194
   153
paulson@11194
   154
(* a lowest i can never be in any abover set *) 
paulson@11194
   155
Goal "Lowest i <= (INT k. {s. i~:above k s})";
paulson@11194
   156
by (auto_tac (claset(), 
paulson@11194
   157
          simpset() addsimps [image0_r_iff_image0_trancl, trancl_converse]));
paulson@11194
   158
qed  "Lowest_above_subset";
paulson@11194
   159
paulson@11194
   160
(* property 18: a simpler proof than the original, one which uses psp *)
paulson@11194
   161
Goal "system: Highest i leadsTo (INT k. {s. i~:above k s})";
paulson@11194
   162
by (rtac leadsTo_weaken_R 1);
paulson@11194
   163
by (rtac Lowest_above_subset 2);
paulson@11194
   164
by (rtac Highest_leadsTo_Lowest 1);
paulson@11194
   165
qed "Highest_escapes_above";
paulson@11194
   166
paulson@11194
   167
Goal 
paulson@11194
   168
"system: Highest j Int {s. j:above i s} leadsTo {s. j~:above i s}";
paulson@11194
   169
by (blast_tac (claset() addIs 
paulson@11194
   170
   [[Highest_escapes_above, Int_lower1, INT_lower] MRS leadsTo_weaken]) 1);
paulson@11194
   171
qed "Highest_escapes_above'"; 
paulson@11194
   172
paulson@11194
   173
(*** The main result: above set decreases ***)
paulson@11194
   174
(* The original proof of the following formula was wrong *)
paulson@11194
   175
val above_decreases_lemma = 
paulson@11194
   176
[Highest_escapes_above', above_not_increase'] MRS psp RS leadsTo_weaken;
paulson@11194
   177
paulson@11194
   178
Goal "Highest i = {s. above i s ={}}";
paulson@11194
   179
by (auto_tac (claset(), 
paulson@11194
   180
        simpset() addsimps [image0_trancl_iff_image0_r]));
paulson@11194
   181
qed "Highest_iff_above0";
paulson@11194
   182
paulson@11194
   183
paulson@11194
   184
Goal 
paulson@11194
   185
"system: (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j) \
paulson@11194
   186
\          leadsTo {s. above i s < x}";
paulson@11194
   187
by (rtac leadsTo_UN 1);
paulson@11194
   188
by (rtac single_leadsTo_I 1);
paulson@11194
   189
by (Clarify_tac 1);
paulson@11194
   190
by (res_inst_tac [("x2", "above i x")] above_decreases_lemma 1);
paulson@11194
   191
by (ALLGOALS(full_simp_tac (simpset() delsimps [Highest_def]
paulson@11194
   192
                  addsimps [Highest_iff_above0])));
paulson@11194
   193
by (REPEAT(Blast_tac 1));
paulson@11194
   194
qed "above_decreases";  
paulson@11194
   195
paulson@11194
   196
(** Just a massage of conditions to have the desired form ***)
paulson@11194
   197
Goalw [Maximal_def, Maximal'_def, Highest_def]
paulson@11194
   198
"Maximal = Maximal'";
paulson@11194
   199
by (Blast_tac 1);
paulson@11194
   200
qed "Maximal_eq_Maximal'";
paulson@11194
   201
paulson@11194
   202
Goal "x~={} ==> \
paulson@11194
   203
\   Acyclic Int {s. above i s = x} <= \
paulson@11194
   204
\   (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j)";
paulson@11194
   205
by (res_inst_tac [("B", "Maximal' Int {s. above i s = x}")] subset_trans 1);
paulson@11194
   206
by (simp_tac (simpset() addsimps [Maximal_eq_Maximal' RS sym]) 1);
paulson@11194
   207
by (blast_tac (claset() addIs [Acyclic_subset_Maximal RS subsetD]) 1);
paulson@11194
   208
by (simp_tac (simpset() delsimps [above_def] addsimps [Maximal'_def, Highest_iff_above0]) 1);
paulson@11194
   209
by (Blast_tac 1);
paulson@11194
   210
qed "Acyclic_subset";
paulson@11194
   211
paulson@11194
   212
val above_decreases' = [above_decreases, Acyclic_subset] MRS leadsTo_weaken_L;
paulson@11194
   213
val above_decreases_psp = [above_decreases', Acyclic_stable] MRS psp_stable;
paulson@11194
   214
paulson@11194
   215
Goal 
paulson@11194
   216
"x~={}==> \
paulson@11194
   217
\ system: Acyclic Int {s. above i s = x} leadsTo Acyclic Int {s. above i s < x}";
paulson@11194
   218
by (etac (above_decreases_psp RS leadsTo_weaken) 1);
paulson@11194
   219
by (Blast_tac 1);
paulson@11194
   220
by Auto_tac;
paulson@11194
   221
qed "above_decreases_psp'";
paulson@11194
   222
paulson@11194
   223
paulson@11194
   224
val finite_psubset_induct = wf_finite_psubset RS leadsTo_wf_induct;
paulson@11194
   225
val leadsTo_weaken_L' = rotate_prems 1 leadsTo_weaken_L;
paulson@11194
   226
paulson@11194
   227
paulson@11194
   228
Goal "system: Acyclic leadsTo Highest i";
paulson@11194
   229
by (res_inst_tac [("f", "%s. above i s")] finite_psubset_induct 1);
wenzelm@11701
   230
by (asm_simp_tac (simpset() delsimps [Highest_def, thm "above_def"]
paulson@11194
   231
                            addsimps [Highest_iff_above0,
paulson@11194
   232
                                      vimage_def, finite_psubset_def]) 1); 
paulson@11194
   233
by (Clarify_tac 1);
paulson@11194
   234
by (case_tac "m={}" 1);
paulson@11194
   235
by (rtac (Int_lower2 RS leadsTo_weaken_L') 1);
paulson@11194
   236
by (force_tac (claset(), simpset() addsimps [leadsTo_refl]) 1);
paulson@11194
   237
by (res_inst_tac [("A'", "Acyclic Int {x. above i x < m}")] 
paulson@11194
   238
    leadsTo_weaken_R 1);
paulson@11194
   239
by (REPEAT(blast_tac (claset() addIs [above_decreases_psp']) 1));
paulson@11194
   240
qed "Progress";
paulson@11194
   241
paulson@11194
   242
(* We have proved all (relevant) theorems given in the paper *)
paulson@11194
   243
(* We didn't assume any thing about the relation r *)
paulson@11194
   244
(* It is not necessary that r be a priority relation as assumed in the original proof *)
paulson@11194
   245
(* It suffices that we start from a state which is finite and acyclic *)