Conversion of UNITY/Comp/Priority.thy to a linear Isar script
authorpaulson
Thu Jul 03 10:37:25 2003 +0200 (2003-07-03)
changeset 14087cb07c3948668
parent 14086 a9be38579840
child 14088 61bd46feb919
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
src/HOL/IsaMakefile
src/HOL/UNITY/Comp/Priority.ML
src/HOL/UNITY/Comp/Priority.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Jul 02 16:57:57 2003 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jul 03 10:37:25 2003 +0200
     1.3 @@ -394,7 +394,7 @@
     1.4    UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \
     1.5    UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
     1.6    UNITY/Comp/PriorityAux.ML UNITY/Comp/PriorityAux.thy \
     1.7 -  UNITY/Comp/Priority.ML UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
     1.8 +  UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
     1.9    UNITY/Comp/TimerArray.thy
    1.10  	@$(ISATOOL) usedir $(OUT)/HOL UNITY
    1.11  
     2.1 --- a/src/HOL/UNITY/Comp/Priority.ML	Wed Jul 02 16:57:57 2003 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,245 +0,0 @@
     2.4 -(*  Title:      HOL/UNITY/Priority
     2.5 -    ID:         $Id$
     2.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     2.7 -    Copyright   2001  University of Cambridge
     2.8 -
     2.9 -The priority system
    2.10 -
    2.11 -From Charpentier and Chandy,
    2.12 -Examples of Program Composition Illustrating the Use of Universal Properties
    2.13 -   In J. Rolim (editor), Parallel and Distributed Processing,
    2.14 -   Spriner LNCS 1586 (1999), pages 1215-1227.
    2.15 -*)
    2.16 -
    2.17 -Addsimps [Component_def RS def_prg_Init];
    2.18 -Addsimps [highest_def, lowest_def];
    2.19 -Addsimps [simp_of_act  act_def];
    2.20 -Addsimps (map simp_of_set [Highest_def, Lowest_def]);
    2.21 -
    2.22 -
    2.23 -
    2.24 -
    2.25 -(**** Component correctness proofs  ****)
    2.26 -
    2.27 -(* neighbors is stable  *)
    2.28 -Goal "Component i: stable {s. neighbors k s = n}";
    2.29 -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
    2.30 -by (constrains_tac 1);
    2.31 -by Auto_tac;
    2.32 -qed "Component_neighbors_stable";
    2.33 -
    2.34 -(* property 4 *)
    2.35 -Goal "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}";
    2.36 -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
    2.37 -by (constrains_tac 1);
    2.38 -qed "Component_waits_priority";  
    2.39 -
    2.40 -(* property 5: charpentier and Chandy mistakenly express it as
    2.41 - 'transient Highest i'. Consider the case where i has neighbors *)
    2.42 -Goal
    2.43 - "Component i: {s. neighbors i s ~= {}} Int Highest i \
    2.44 -\              ensures - Highest i";
    2.45 -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
    2.46 -by (ensures_tac "act i" 1);
    2.47 -by (REPEAT(Fast_tac 1));
    2.48 -qed "Component_yields_priority"; 
    2.49 -
    2.50 -(* or better *)
    2.51 -Goal "Component i: Highest i ensures Lowest i";
    2.52 -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
    2.53 -by (ensures_tac "act i" 1);
    2.54 -by (REPEAT(Fast_tac 1));
    2.55 -qed "Component_yields_priority'";
    2.56 -
    2.57 -(* property 6: Component doesn't introduce cycle *)
    2.58 -Goal "Component i: Highest i co Highest i Un Lowest i";
    2.59 -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
    2.60 -by (constrains_tac 1);
    2.61 -by (Fast_tac 1);
    2.62 -qed "Component_well_behaves"; 
    2.63 -
    2.64 -(* property 7: local axiom *)
    2.65 -Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}";
    2.66 -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); 
    2.67 -by (constrains_tac 1);
    2.68 -qed "locality";  
    2.69 -
    2.70 -
    2.71 -(**** System  properties  ****)
    2.72 -(* property 8: strictly universal *)
    2.73 -
    2.74 -Goalw [Safety_def] "system: stable Safety";
    2.75 -by (rtac stable_INT 1);
    2.76 -by (asm_full_simp_tac (simpset() addsimps [system_def]) 1); 
    2.77 -by (constrains_tac 1);
    2.78 -by (Fast_tac 1);
    2.79 -qed "Safety"; 
    2.80 -
    2.81 -(* property 13: universal *)
    2.82 -Goal "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
    2.83 -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
    2.84 -by (constrains_tac 1);
    2.85 -by (Blast_tac 1);
    2.86 -qed "p13";
    2.87 -
    2.88 -(* property 14: the 'above set' of a Component that hasn't got 
    2.89 -      priority doesn't increase *)
    2.90 -Goal
    2.91 -"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}";
    2.92 -by (Clarify_tac 1);
    2.93 -by (cut_inst_tac [("i", "j")] reach_lemma 1);
    2.94 -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
    2.95 -by (constrains_tac 1);
    2.96 -by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
    2.97 -qed "above_not_increase";  
    2.98 -
    2.99 -Goal "system: -Highest i Int {s. above i s = x} co {s. above i s <= x}";
   2.100 -by (cut_inst_tac [("i", "i")] above_not_increase 1);
   2.101 -by (asm_full_simp_tac
   2.102 -    (simpset() addsimps [trancl_converse, constrains_def]) 1); 
   2.103 -by (Blast_tac 1);
   2.104 -qed "above_not_increase'";  
   2.105 -
   2.106 -
   2.107 -
   2.108 -(* p15: universal property: all Components well behave  *)
   2.109 -Goal "ALL i. system: Highest i co Highest i Un Lowest i";
   2.110 -by (Clarify_tac 1);
   2.111 -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
   2.112 -by (constrains_tac 1);
   2.113 -by Auto_tac;
   2.114 -qed "system_well_behaves";  
   2.115 -
   2.116 -
   2.117 -Goal "Acyclic = (INT i. {s. i~:above i s})";
   2.118 -by (auto_tac (claset(), simpset() 
   2.119 -   addsimps [Acyclic_def, acyclic_def, trancl_converse]));
   2.120 -qed "Acyclic_eq";
   2.121 -
   2.122 -
   2.123 -val lemma = [above_not_increase RS spec, 
   2.124 -           system_well_behaves RS spec] MRS constrains_Un;
   2.125 -Goal 
   2.126 -"system: stable Acyclic";
   2.127 -by (auto_tac (claset() addSIs [stable_INT, stableI, 
   2.128 -                               lemma RS constrains_weaken],
   2.129 -              simpset() addsimps [Acyclic_eq, 
   2.130 -                    image0_r_iff_image0_trancl,trancl_converse]));
   2.131 -qed "Acyclic_stable";
   2.132 -
   2.133 -
   2.134 -Goalw [Acyclic_def, Maximal_def]
   2.135 -"Acyclic <= Maximal";
   2.136 -by (Clarify_tac 1);
   2.137 -by (dtac above_lemma_b 1);
   2.138 -by Auto_tac;
   2.139 -qed "Acyclic_subset_Maximal";
   2.140 -
   2.141 -(* property 17: original one is an invariant *)
   2.142 -Goal 
   2.143 -"system: stable (Acyclic Int Maximal)";
   2.144 -by (simp_tac (simpset() addsimps 
   2.145 -     [Acyclic_subset_Maximal RS Int_absorb2, Acyclic_stable]) 1);
   2.146 -qed "Acyclic_Maximal_stable";  
   2.147 -
   2.148 -
   2.149 -(* propert 5: existential property *)
   2.150 -
   2.151 -Goal "system: Highest i leadsTo Lowest i";
   2.152 -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); 
   2.153 -by (ensures_tac "act i" 1);
   2.154 -by Auto_tac;
   2.155 -qed "Highest_leadsTo_Lowest";
   2.156 -
   2.157 -(* a lowest i can never be in any abover set *) 
   2.158 -Goal "Lowest i <= (INT k. {s. i~:above k s})";
   2.159 -by (auto_tac (claset(), 
   2.160 -          simpset() addsimps [image0_r_iff_image0_trancl, trancl_converse]));
   2.161 -qed  "Lowest_above_subset";
   2.162 -
   2.163 -(* property 18: a simpler proof than the original, one which uses psp *)
   2.164 -Goal "system: Highest i leadsTo (INT k. {s. i~:above k s})";
   2.165 -by (rtac leadsTo_weaken_R 1);
   2.166 -by (rtac Lowest_above_subset 2);
   2.167 -by (rtac Highest_leadsTo_Lowest 1);
   2.168 -qed "Highest_escapes_above";
   2.169 -
   2.170 -Goal 
   2.171 -"system: Highest j Int {s. j:above i s} leadsTo {s. j~:above i s}";
   2.172 -by (blast_tac (claset() addIs 
   2.173 -   [[Highest_escapes_above, Int_lower1, INT_lower] MRS leadsTo_weaken]) 1);
   2.174 -qed "Highest_escapes_above'"; 
   2.175 -
   2.176 -(*** The main result: above set decreases ***)
   2.177 -(* The original proof of the following formula was wrong *)
   2.178 -val above_decreases_lemma = 
   2.179 -[Highest_escapes_above', above_not_increase'] MRS psp RS leadsTo_weaken;
   2.180 -
   2.181 -Goal "Highest i = {s. above i s ={}}";
   2.182 -by (auto_tac (claset(), 
   2.183 -        simpset() addsimps [image0_trancl_iff_image0_r]));
   2.184 -qed "Highest_iff_above0";
   2.185 -
   2.186 -
   2.187 -Goal 
   2.188 -"system: (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j) \
   2.189 -\          leadsTo {s. above i s < x}";
   2.190 -by (rtac leadsTo_UN 1);
   2.191 -by (rtac single_leadsTo_I 1);
   2.192 -by (Clarify_tac 1);
   2.193 -by (res_inst_tac [("x2", "above i x")] above_decreases_lemma 1);
   2.194 -by (ALLGOALS(full_simp_tac (simpset() delsimps [Highest_def]
   2.195 -                  addsimps [Highest_iff_above0])));
   2.196 -by (REPEAT(Blast_tac 1));
   2.197 -qed "above_decreases";  
   2.198 -
   2.199 -(** Just a massage of conditions to have the desired form ***)
   2.200 -Goalw [Maximal_def, Maximal'_def, Highest_def]
   2.201 -"Maximal = Maximal'";
   2.202 -by (Blast_tac 1);
   2.203 -qed "Maximal_eq_Maximal'";
   2.204 -
   2.205 -Goal "x~={} ==> \
   2.206 -\   Acyclic Int {s. above i s = x} <= \
   2.207 -\   (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j)";
   2.208 -by (res_inst_tac [("B", "Maximal' Int {s. above i s = x}")] subset_trans 1);
   2.209 -by (simp_tac (simpset() addsimps [Maximal_eq_Maximal' RS sym]) 1);
   2.210 -by (blast_tac (claset() addIs [Acyclic_subset_Maximal RS subsetD]) 1);
   2.211 -by (simp_tac (simpset() delsimps [above_def] addsimps [Maximal'_def, Highest_iff_above0]) 1);
   2.212 -by (Blast_tac 1);
   2.213 -qed "Acyclic_subset";
   2.214 -
   2.215 -val above_decreases' = [above_decreases, Acyclic_subset] MRS leadsTo_weaken_L;
   2.216 -val above_decreases_psp = [above_decreases', Acyclic_stable] MRS psp_stable;
   2.217 -
   2.218 -Goal 
   2.219 -"x~={}==> \
   2.220 -\ system: Acyclic Int {s. above i s = x} leadsTo Acyclic Int {s. above i s < x}";
   2.221 -by (etac (above_decreases_psp RS leadsTo_weaken) 1);
   2.222 -by (Blast_tac 1);
   2.223 -by Auto_tac;
   2.224 -qed "above_decreases_psp'";
   2.225 -
   2.226 -
   2.227 -val finite_psubset_induct = wf_finite_psubset RS leadsTo_wf_induct;
   2.228 -val leadsTo_weaken_L' = rotate_prems 1 leadsTo_weaken_L;
   2.229 -
   2.230 -
   2.231 -Goal "system: Acyclic leadsTo Highest i";
   2.232 -by (res_inst_tac [("f", "%s. above i s")] finite_psubset_induct 1);
   2.233 -by (asm_simp_tac (simpset() delsimps [Highest_def, thm "above_def"]
   2.234 -                            addsimps [Highest_iff_above0,
   2.235 -                                      vimage_def, finite_psubset_def]) 1); 
   2.236 -by (Clarify_tac 1);
   2.237 -by (case_tac "m={}" 1);
   2.238 -by (rtac (Int_lower2 RS leadsTo_weaken_L') 1);
   2.239 -by (force_tac (claset(), simpset() addsimps [leadsTo_refl]) 1);
   2.240 -by (res_inst_tac [("A'", "Acyclic Int {x. above i x < m}")] 
   2.241 -    leadsTo_weaken_R 1);
   2.242 -by (REPEAT(blast_tac (claset() addIs [above_decreases_psp']) 1));
   2.243 -qed "Progress";
   2.244 -
   2.245 -(* We have proved all (relevant) theorems given in the paper *)
   2.246 -(* We didn't assume any thing about the relation r *)
   2.247 -(* It is not necessary that r be a priority relation as assumed in the original proof *)
   2.248 -(* It suffices that we start from a state which is finite and acyclic *)
     3.1 --- a/src/HOL/UNITY/Comp/Priority.thy	Wed Jul 02 16:57:57 2003 +0200
     3.2 +++ b/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 03 10:37:25 2003 +0200
     3.3 @@ -3,15 +3,17 @@
     3.4      Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     3.5      Copyright   2001  University of Cambridge
     3.6  
     3.7 -The priority system
     3.8 +
     3.9 +*)
    3.10  
    3.11 -From Charpentier and Chandy,
    3.12 +header{*The priority system*}
    3.13 +
    3.14 +theory Priority = PriorityAux:
    3.15 +
    3.16 +text{*From Charpentier and Chandy,
    3.17  Examples of Program Composition Illustrating the Use of Universal Properties
    3.18     In J. Rolim (editor), Parallel and Distributed Processing,
    3.19 -   Spriner LNCS 1586 (1999), pages 1215-1227.
    3.20 -*)
    3.21 -
    3.22 -Priority = PriorityAux +
    3.23 +   Spriner LNCS 1586 (1999), pages 1215-1227.*}
    3.24  
    3.25  types state = "(vertex*vertex)set"
    3.26  types command = "vertex=>(state*state)set"
    3.27 @@ -50,14 +52,14 @@
    3.28    (* Every above set has a maximal vertex: two equivalent defs. *)
    3.29  
    3.30    Maximal :: "state set"
    3.31 -  "Maximal == INT i. {s. ~highest i s-->(EX j:above i  s. highest j s)}"
    3.32 +  "Maximal == \<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i  s. highest j s)}"
    3.33  
    3.34    Maximal' :: "state set"
    3.35 -  "Maximal' == INT i. Highest i Un (UN j. {s. j:above i s} Int Highest j)"
    3.36 +  "Maximal' == \<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j)"
    3.37  
    3.38    
    3.39    Safety :: "state set"
    3.40 -  "Safety == INT i. {s. highest i s --> (ALL j:neighbors i s. ~highest j s)}"
    3.41 +  "Safety == \<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)}"
    3.42  
    3.43  
    3.44    (* Composition of a finite set of component;
    3.45 @@ -65,4 +67,202 @@
    3.46    
    3.47    system :: "state program"
    3.48    "system == JN i. Component i"
    3.49 +
    3.50 +
    3.51 +declare highest_def [simp] lowest_def [simp]
    3.52 +declare Highest_def [THEN def_set_simp, simp] 
    3.53 +    and Lowest_def  [THEN def_set_simp, simp]
    3.54 +
    3.55 +declare Component_def [THEN def_prg_Init, simp]
    3.56 +declare act_def [THEN def_act_simp, simp]
    3.57 +
    3.58 +
    3.59 +
    3.60 +subsection{*Component correctness proofs*}
    3.61 +
    3.62 +(* neighbors is stable  *)
    3.63 +lemma Component_neighbors_stable: "Component i \<in> stable {s. neighbors k s = n}"
    3.64 +by (simp add: Component_def, constrains, auto)
    3.65 +
    3.66 +(* property 4 *)
    3.67 +lemma Component_waits_priority: "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}"
    3.68 +by (simp add: Component_def, constrains)
    3.69 +
    3.70 +(* property 5: charpentier and Chandy mistakenly express it as
    3.71 + 'transient Highest i'. Consider the case where i has neighbors *)
    3.72 +lemma Component_yields_priority: 
    3.73 + "Component i: {s. neighbors i s \<noteq> {}} Int Highest i  
    3.74 +               ensures - Highest i"
    3.75 +apply (simp add: Component_def)
    3.76 +apply (ensures_tac "act i", blast+) 
    3.77 +done
    3.78 +
    3.79 +(* or better *)
    3.80 +lemma Component_yields_priority': "Component i \<in> Highest i ensures Lowest i"
    3.81 +apply (simp add: Component_def)
    3.82 +apply (ensures_tac "act i", blast+) 
    3.83 +done
    3.84 +
    3.85 +(* property 6: Component doesn't introduce cycle *)
    3.86 +lemma Component_well_behaves: "Component i \<in> Highest i co Highest i Un Lowest i"
    3.87 +by (simp add: Component_def, constrains, fast)
    3.88 +
    3.89 +(* property 7: local axiom *)
    3.90 +lemma locality: "Component i \<in> stable {s. \<forall>j k. j\<noteq>i & k\<noteq>i--> ((j,k):s) = b j k}"
    3.91 +by (simp add: Component_def, constrains)
    3.92 +
    3.93 +
    3.94 +subsection{*System  properties*}
    3.95 +(* property 8: strictly universal *)
    3.96 +
    3.97 +lemma Safety: "system \<in> stable Safety"
    3.98 +apply (unfold Safety_def)
    3.99 +apply (rule stable_INT)
   3.100 +apply (simp add: system_def, constrains, fast)
   3.101 +done
   3.102 +
   3.103 +(* property 13: universal *)
   3.104 +lemma p13: "system \<in> {s. s = q} co {s. s=q} Un {s. \<exists>i. derive i q s}"
   3.105 +by (simp add: system_def Component_def mk_total_program_def totalize_JN, constrains, blast)
   3.106 +
   3.107 +(* property 14: the 'above set' of a Component that hasn't got 
   3.108 +      priority doesn't increase *)
   3.109 +lemma above_not_increase: 
   3.110 +     "\<forall>j. system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}"
   3.111 +apply clarify
   3.112 +apply (cut_tac i = j in reach_lemma)
   3.113 +apply (simp add: system_def Component_def mk_total_program_def totalize_JN, 
   3.114 +       constrains)
   3.115 +apply (auto simp add: trancl_converse)
   3.116 +done
   3.117 +
   3.118 +lemma above_not_increase':
   3.119 +     "system \<in> -Highest i Int {s. above i s = x} co {s. above i s <= x}"
   3.120 +apply (cut_tac i = i in above_not_increase)
   3.121 +apply (simp add: trancl_converse constrains_def, blast)
   3.122 +done
   3.123 +
   3.124 +
   3.125 +
   3.126 +(* p15: universal property: all Components well behave  *)
   3.127 +lemma system_well_behaves [rule_format]:
   3.128 +     "\<forall>i. system \<in> Highest i co Highest i Un Lowest i"
   3.129 +apply clarify
   3.130 +apply (simp add: system_def Component_def mk_total_program_def totalize_JN, 
   3.131 +       constrains, auto)
   3.132 +done
   3.133 +
   3.134 +
   3.135 +lemma Acyclic_eq: "Acyclic = (\<Inter>i. {s. i\<notin>above i s})"
   3.136 +by (auto simp add: Acyclic_def acyclic_def trancl_converse)
   3.137 +
   3.138 +
   3.139 +lemmas system_co =
   3.140 +      constrains_Un [OF above_not_increase [rule_format] system_well_behaves] 
   3.141 +
   3.142 +lemma Acyclic_stable: "system \<in> stable Acyclic"
   3.143 +apply (simp add: stable_def Acyclic_eq) 
   3.144 +apply (auto intro!: constrains_INT system_co [THEN constrains_weaken] 
   3.145 +            simp add: image0_r_iff_image0_trancl trancl_converse)
   3.146 +done
   3.147 +
   3.148 +
   3.149 +lemma Acyclic_subset_Maximal: "Acyclic <= Maximal"
   3.150 +apply (unfold Acyclic_def Maximal_def, clarify)
   3.151 +apply (drule above_lemma_b, auto)
   3.152 +done
   3.153 +
   3.154 +(* property 17: original one is an invariant *)
   3.155 +lemma Acyclic_Maximal_stable: "system \<in> stable (Acyclic Int Maximal)"
   3.156 +apply (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable)
   3.157 +done
   3.158 +
   3.159 +
   3.160 +(* propert 5: existential property *)
   3.161 +
   3.162 +lemma Highest_leadsTo_Lowest: "system \<in> Highest i leadsTo Lowest i"
   3.163 +apply (simp add: system_def Component_def mk_total_program_def totalize_JN)
   3.164 +apply (ensures_tac "act i", auto)
   3.165 +done
   3.166 +
   3.167 +(* a lowest i can never be in any abover set *) 
   3.168 +lemma Lowest_above_subset: "Lowest i <= (\<Inter>k. {s. i\<notin>above k s})"
   3.169 +by (auto simp add: image0_r_iff_image0_trancl trancl_converse)
   3.170 +
   3.171 +(* property 18: a simpler proof than the original, one which uses psp *)
   3.172 +lemma Highest_escapes_above: "system \<in> Highest i leadsTo (\<Inter>k. {s. i\<notin>above k s})"
   3.173 +apply (rule leadsTo_weaken_R)
   3.174 +apply (rule_tac [2] Lowest_above_subset)
   3.175 +apply (rule Highest_leadsTo_Lowest)
   3.176 +done
   3.177 +
   3.178 +lemma Highest_escapes_above':
   3.179 +     "system \<in> Highest j Int {s. j \<in> above i s} leadsTo {s. j\<notin>above i s}"
   3.180 +by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower])
   3.181 +
   3.182 +(*** The main result: above set decreases ***)
   3.183 +(* The original proof of the following formula was wrong *)
   3.184 +
   3.185 +lemma Highest_iff_above0: "Highest i = {s. above i s ={}}"
   3.186 +by (auto simp add: image0_trancl_iff_image0_r)
   3.187 +
   3.188 +lemmas above_decreases_lemma = 
   3.189 +     psp [THEN leadsTo_weaken, OF Highest_escapes_above' above_not_increase'] 
   3.190 +
   3.191 +
   3.192 +lemma above_decreases: 
   3.193 +     "system \<in> (\<Union>j. {s. above i s = x} Int {s. j \<in> above i s} Int Highest j)  
   3.194 +               leadsTo {s. above i s < x}"
   3.195 +apply (rule leadsTo_UN)
   3.196 +apply (rule single_leadsTo_I, clarify)
   3.197 +apply (rule_tac x2 = "above i x" in above_decreases_lemma)
   3.198 +apply (simp_all (no_asm_use) del: Highest_def add: Highest_iff_above0)
   3.199 +apply blast+
   3.200 +done
   3.201 +
   3.202 +(** Just a massage of conditions to have the desired form ***)
   3.203 +lemma Maximal_eq_Maximal': "Maximal = Maximal'"
   3.204 +by (unfold Maximal_def Maximal'_def Highest_def, blast)
   3.205 +
   3.206 +lemma Acyclic_subset:
   3.207 +   "x\<noteq>{} ==>  
   3.208 +    Acyclic Int {s. above i s = x} <=  
   3.209 +    (\<Union>j. {s. above i s = x} Int {s. j \<in> above i s} Int Highest j)"
   3.210 +apply (rule_tac B = "Maximal' Int {s. above i s = x}" in subset_trans)
   3.211 +apply (simp (no_asm) add: Maximal_eq_Maximal' [symmetric])
   3.212 +apply (blast intro: Acyclic_subset_Maximal [THEN subsetD])
   3.213 +apply (simp (no_asm) del: above_def add: Maximal'_def Highest_iff_above0)
   3.214 +apply blast
   3.215 +done
   3.216 +
   3.217 +lemmas above_decreases' = leadsTo_weaken_L [OF above_decreases Acyclic_subset]
   3.218 +lemmas above_decreases_psp = psp_stable [OF above_decreases' Acyclic_stable]
   3.219 +
   3.220 +lemma above_decreases_psp': 
   3.221 +"x\<noteq>{}==> system \<in> Acyclic Int {s. above i s = x} leadsTo 
   3.222 +                   Acyclic Int {s. above i s < x}"
   3.223 +by (erule above_decreases_psp [THEN leadsTo_weaken], blast, auto)
   3.224 +
   3.225 +
   3.226 +lemmas finite_psubset_induct = wf_finite_psubset [THEN leadsTo_wf_induct]
   3.227 +
   3.228 +
   3.229 +lemma Progress: "system \<in> Acyclic leadsTo Highest i"
   3.230 +apply (rule_tac f = "%s. above i s" in finite_psubset_induct)
   3.231 +apply (simp del: Highest_def above_def
   3.232 +            add: Highest_iff_above0 vimage_def finite_psubset_def, clarify)
   3.233 +apply (case_tac "m={}")
   3.234 +apply (rule Int_lower2 [THEN [2] leadsTo_weaken_L])
   3.235 +apply (force simp add: leadsTo_refl)
   3.236 +apply (rule_tac A' = "Acyclic Int {x. above i x < m}" in leadsTo_weaken_R)
   3.237 +apply (blast intro: above_decreases_psp')+
   3.238 +done
   3.239 +
   3.240 +
   3.241 +text{*We have proved all (relevant) theorems given in the paper.  We didn't
   3.242 +assume any thing about the relation @{term r}.  It is not necessary that
   3.243 +@{term r} be a priority relation as assumed in the original proof.  It
   3.244 +suffices that we start from a state which is finite and acyclic.*}
   3.245 +
   3.246 +
   3.247  end
   3.248 \ No newline at end of file