--- a/src/HOL/IsaMakefile Wed Jul 02 16:57:57 2003 +0200
+++ b/src/HOL/IsaMakefile Thu Jul 03 10:37:25 2003 +0200
@@ -394,7 +394,7 @@
UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \
UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
UNITY/Comp/PriorityAux.ML UNITY/Comp/PriorityAux.thy \
- UNITY/Comp/Priority.ML UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
+ UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
UNITY/Comp/TimerArray.thy
@$(ISATOOL) usedir $(OUT)/HOL UNITY
--- a/src/HOL/UNITY/Comp/Priority.ML Wed Jul 02 16:57:57 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,245 +0,0 @@
-(* Title: HOL/UNITY/Priority
- ID: $Id$
- Author: Sidi O Ehmety, Cambridge University Computer Laboratory
- Copyright 2001 University of Cambridge
-
-The priority system
-
-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.
-*)
-
-Addsimps [Component_def RS def_prg_Init];
-Addsimps [highest_def, lowest_def];
-Addsimps [simp_of_act act_def];
-Addsimps (map simp_of_set [Highest_def, Lowest_def]);
-
-
-
-
-(**** Component correctness proofs ****)
-
-(* neighbors is stable *)
-Goal "Component i: stable {s. neighbors k s = n}";
-by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "Component_neighbors_stable";
-
-(* property 4 *)
-Goal "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}";
-by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
-by (constrains_tac 1);
-qed "Component_waits_priority";
-
-(* property 5: charpentier and Chandy mistakenly express it as
- 'transient Highest i'. Consider the case where i has neighbors *)
-Goal
- "Component i: {s. neighbors i s ~= {}} Int Highest i \
-\ ensures - Highest i";
-by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
-by (ensures_tac "act i" 1);
-by (REPEAT(Fast_tac 1));
-qed "Component_yields_priority";
-
-(* or better *)
-Goal "Component i: Highest i ensures Lowest i";
-by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
-by (ensures_tac "act i" 1);
-by (REPEAT(Fast_tac 1));
-qed "Component_yields_priority'";
-
-(* property 6: Component doesn't introduce cycle *)
-Goal "Component i: Highest i co Highest i Un Lowest i";
-by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
-by (constrains_tac 1);
-by (Fast_tac 1);
-qed "Component_well_behaves";
-
-(* property 7: local axiom *)
-Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}";
-by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
-by (constrains_tac 1);
-qed "locality";
-
-
-(**** System properties ****)
-(* property 8: strictly universal *)
-
-Goalw [Safety_def] "system: stable Safety";
-by (rtac stable_INT 1);
-by (asm_full_simp_tac (simpset() addsimps [system_def]) 1);
-by (constrains_tac 1);
-by (Fast_tac 1);
-qed "Safety";
-
-(* property 13: universal *)
-Goal "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
-by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1);
-by (constrains_tac 1);
-by (Blast_tac 1);
-qed "p13";
-
-(* property 14: the 'above set' of a Component that hasn't got
- priority doesn't increase *)
-Goal
-"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}";
-by (Clarify_tac 1);
-by (cut_inst_tac [("i", "j")] reach_lemma 1);
-by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1);
-by (constrains_tac 1);
-by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
-qed "above_not_increase";
-
-Goal "system: -Highest i Int {s. above i s = x} co {s. above i s <= x}";
-by (cut_inst_tac [("i", "i")] above_not_increase 1);
-by (asm_full_simp_tac
- (simpset() addsimps [trancl_converse, constrains_def]) 1);
-by (Blast_tac 1);
-qed "above_not_increase'";
-
-
-
-(* p15: universal property: all Components well behave *)
-Goal "ALL i. system: Highest i co Highest i Un Lowest i";
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "system_well_behaves";
-
-
-Goal "Acyclic = (INT i. {s. i~:above i s})";
-by (auto_tac (claset(), simpset()
- addsimps [Acyclic_def, acyclic_def, trancl_converse]));
-qed "Acyclic_eq";
-
-
-val lemma = [above_not_increase RS spec,
- system_well_behaves RS spec] MRS constrains_Un;
-Goal
-"system: stable Acyclic";
-by (auto_tac (claset() addSIs [stable_INT, stableI,
- lemma RS constrains_weaken],
- simpset() addsimps [Acyclic_eq,
- image0_r_iff_image0_trancl,trancl_converse]));
-qed "Acyclic_stable";
-
-
-Goalw [Acyclic_def, Maximal_def]
-"Acyclic <= Maximal";
-by (Clarify_tac 1);
-by (dtac above_lemma_b 1);
-by Auto_tac;
-qed "Acyclic_subset_Maximal";
-
-(* property 17: original one is an invariant *)
-Goal
-"system: stable (Acyclic Int Maximal)";
-by (simp_tac (simpset() addsimps
- [Acyclic_subset_Maximal RS Int_absorb2, Acyclic_stable]) 1);
-qed "Acyclic_Maximal_stable";
-
-
-(* propert 5: existential property *)
-
-Goal "system: Highest i leadsTo Lowest i";
-by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1);
-by (ensures_tac "act i" 1);
-by Auto_tac;
-qed "Highest_leadsTo_Lowest";
-
-(* a lowest i can never be in any abover set *)
-Goal "Lowest i <= (INT k. {s. i~:above k s})";
-by (auto_tac (claset(),
- simpset() addsimps [image0_r_iff_image0_trancl, trancl_converse]));
-qed "Lowest_above_subset";
-
-(* property 18: a simpler proof than the original, one which uses psp *)
-Goal "system: Highest i leadsTo (INT k. {s. i~:above k s})";
-by (rtac leadsTo_weaken_R 1);
-by (rtac Lowest_above_subset 2);
-by (rtac Highest_leadsTo_Lowest 1);
-qed "Highest_escapes_above";
-
-Goal
-"system: Highest j Int {s. j:above i s} leadsTo {s. j~:above i s}";
-by (blast_tac (claset() addIs
- [[Highest_escapes_above, Int_lower1, INT_lower] MRS leadsTo_weaken]) 1);
-qed "Highest_escapes_above'";
-
-(*** The main result: above set decreases ***)
-(* The original proof of the following formula was wrong *)
-val above_decreases_lemma =
-[Highest_escapes_above', above_not_increase'] MRS psp RS leadsTo_weaken;
-
-Goal "Highest i = {s. above i s ={}}";
-by (auto_tac (claset(),
- simpset() addsimps [image0_trancl_iff_image0_r]));
-qed "Highest_iff_above0";
-
-
-Goal
-"system: (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j) \
-\ leadsTo {s. above i s < x}";
-by (rtac leadsTo_UN 1);
-by (rtac single_leadsTo_I 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("x2", "above i x")] above_decreases_lemma 1);
-by (ALLGOALS(full_simp_tac (simpset() delsimps [Highest_def]
- addsimps [Highest_iff_above0])));
-by (REPEAT(Blast_tac 1));
-qed "above_decreases";
-
-(** Just a massage of conditions to have the desired form ***)
-Goalw [Maximal_def, Maximal'_def, Highest_def]
-"Maximal = Maximal'";
-by (Blast_tac 1);
-qed "Maximal_eq_Maximal'";
-
-Goal "x~={} ==> \
-\ Acyclic Int {s. above i s = x} <= \
-\ (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j)";
-by (res_inst_tac [("B", "Maximal' Int {s. above i s = x}")] subset_trans 1);
-by (simp_tac (simpset() addsimps [Maximal_eq_Maximal' RS sym]) 1);
-by (blast_tac (claset() addIs [Acyclic_subset_Maximal RS subsetD]) 1);
-by (simp_tac (simpset() delsimps [above_def] addsimps [Maximal'_def, Highest_iff_above0]) 1);
-by (Blast_tac 1);
-qed "Acyclic_subset";
-
-val above_decreases' = [above_decreases, Acyclic_subset] MRS leadsTo_weaken_L;
-val above_decreases_psp = [above_decreases', Acyclic_stable] MRS psp_stable;
-
-Goal
-"x~={}==> \
-\ system: Acyclic Int {s. above i s = x} leadsTo Acyclic Int {s. above i s < x}";
-by (etac (above_decreases_psp RS leadsTo_weaken) 1);
-by (Blast_tac 1);
-by Auto_tac;
-qed "above_decreases_psp'";
-
-
-val finite_psubset_induct = wf_finite_psubset RS leadsTo_wf_induct;
-val leadsTo_weaken_L' = rotate_prems 1 leadsTo_weaken_L;
-
-
-Goal "system: Acyclic leadsTo Highest i";
-by (res_inst_tac [("f", "%s. above i s")] finite_psubset_induct 1);
-by (asm_simp_tac (simpset() delsimps [Highest_def, thm "above_def"]
- addsimps [Highest_iff_above0,
- vimage_def, finite_psubset_def]) 1);
-by (Clarify_tac 1);
-by (case_tac "m={}" 1);
-by (rtac (Int_lower2 RS leadsTo_weaken_L') 1);
-by (force_tac (claset(), simpset() addsimps [leadsTo_refl]) 1);
-by (res_inst_tac [("A'", "Acyclic Int {x. above i x < m}")]
- leadsTo_weaken_R 1);
-by (REPEAT(blast_tac (claset() addIs [above_decreases_psp']) 1));
-qed "Progress";
-
-(* We have proved all (relevant) theorems given in the paper *)
-(* We didn't assume any thing about the relation r *)
-(* It is not necessary that r be a priority relation as assumed in the original proof *)
-(* It suffices that we start from a state which is finite and acyclic *)
--- a/src/HOL/UNITY/Comp/Priority.thy Wed Jul 02 16:57:57 2003 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy Thu Jul 03 10:37:25 2003 +0200
@@ -3,15 +3,17 @@
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
-The priority system
+
+*)
-From Charpentier and Chandy,
+header{*The priority system*}
+
+theory Priority = PriorityAux:
+
+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.
-*)
-
-Priority = PriorityAux +
+ Spriner LNCS 1586 (1999), pages 1215-1227.*}
types state = "(vertex*vertex)set"
types command = "vertex=>(state*state)set"
@@ -50,14 +52,14 @@
(* Every above set has a maximal vertex: two equivalent defs. *)
Maximal :: "state set"
- "Maximal == INT i. {s. ~highest i s-->(EX j:above i s. highest j s)}"
+ "Maximal == \<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i s. highest j s)}"
Maximal' :: "state set"
- "Maximal' == INT i. Highest i Un (UN j. {s. j:above i s} Int Highest j)"
+ "Maximal' == \<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j)"
Safety :: "state set"
- "Safety == INT i. {s. highest i s --> (ALL j:neighbors i s. ~highest j s)}"
+ "Safety == \<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)}"
(* Composition of a finite set of component;
@@ -65,4 +67,202 @@
system :: "state program"
"system == JN 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*}
+
+(* neighbors is stable *)
+lemma Component_neighbors_stable: "Component i \<in> stable {s. neighbors k s = n}"
+by (simp add: Component_def, constrains, auto)
+
+(* property 4 *)
+lemma Component_waits_priority: "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}"
+by (simp add: Component_def, constrains)
+
+(* 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 \<noteq> {}} Int Highest i
+ ensures - Highest i"
+apply (simp add: Component_def)
+apply (ensures_tac "act i", blast+)
+done
+
+(* or better *)
+lemma Component_yields_priority': "Component i \<in> Highest i ensures Lowest i"
+apply (simp add: Component_def)
+apply (ensures_tac "act i", blast+)
+done
+
+(* property 6: Component doesn't introduce cycle *)
+lemma Component_well_behaves: "Component i \<in> Highest i co Highest i Un Lowest i"
+by (simp add: Component_def, constrains, fast)
+
+(* property 7: local axiom *)
+lemma locality: "Component i \<in> stable {s. \<forall>j k. j\<noteq>i & k\<noteq>i--> ((j,k):s) = b j k}"
+by (simp add: Component_def, constrains)
+
+
+subsection{*System properties*}
+(* property 8: strictly universal *)
+
+lemma Safety: "system \<in> stable Safety"
+apply (unfold Safety_def)
+apply (rule stable_INT)
+apply (simp add: system_def, constrains, fast)
+done
+
+(* property 13: universal *)
+lemma p13: "system \<in> {s. s = q} co {s. s=q} Un {s. \<exists>i. derive i q s}"
+by (simp add: system_def Component_def mk_total_program_def totalize_JN, constrains, blast)
+
+(* property 14: the 'above set' of a Component that hasn't got
+ priority doesn't increase *)
+lemma above_not_increase:
+ "\<forall>j. system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}"
+apply clarify
+apply (cut_tac i = j in reach_lemma)
+apply (simp add: system_def Component_def mk_total_program_def totalize_JN,
+ constrains)
+apply (auto simp add: trancl_converse)
+done
+
+lemma above_not_increase':
+ "system \<in> -Highest i Int {s. above i s = x} co {s. above i s <= x}"
+apply (cut_tac i = i in above_not_increase)
+apply (simp add: trancl_converse constrains_def, blast)
+done
+
+
+
+(* p15: universal property: all Components well behave *)
+lemma system_well_behaves [rule_format]:
+ "\<forall>i. system \<in> Highest i co Highest i Un Lowest i"
+apply clarify
+apply (simp add: system_def Component_def mk_total_program_def totalize_JN,
+ constrains, auto)
+done
+
+
+lemma Acyclic_eq: "Acyclic = (\<Inter>i. {s. i\<notin>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 \<in> stable Acyclic"
+apply (simp add: stable_def Acyclic_eq)
+apply (auto intro!: constrains_INT system_co [THEN constrains_weaken]
+ simp add: image0_r_iff_image0_trancl trancl_converse)
+done
+
+
+lemma Acyclic_subset_Maximal: "Acyclic <= Maximal"
+apply (unfold Acyclic_def Maximal_def, clarify)
+apply (drule above_lemma_b, auto)
+done
+
+(* property 17: original one is an invariant *)
+lemma Acyclic_Maximal_stable: "system \<in> stable (Acyclic Int Maximal)"
+apply (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable)
+done
+
+
+(* propert 5: existential property *)
+
+lemma Highest_leadsTo_Lowest: "system \<in> Highest i leadsTo Lowest i"
+apply (simp add: system_def Component_def mk_total_program_def totalize_JN)
+apply (ensures_tac "act i", auto)
+done
+
+(* a lowest i can never be in any abover set *)
+lemma Lowest_above_subset: "Lowest i <= (\<Inter>k. {s. i\<notin>above k s})"
+by (auto simp add: image0_r_iff_image0_trancl trancl_converse)
+
+(* property 18: a simpler proof than the original, one which uses psp *)
+lemma Highest_escapes_above: "system \<in> Highest i leadsTo (\<Inter>k. {s. i\<notin>above k s})"
+apply (rule leadsTo_weaken_R)
+apply (rule_tac [2] Lowest_above_subset)
+apply (rule Highest_leadsTo_Lowest)
+done
+
+lemma Highest_escapes_above':
+ "system \<in> Highest j Int {s. j \<in> above i s} leadsTo {s. j\<notin>above i s}"
+by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower])
+
+(*** The main result: above set decreases ***)
+(* The original proof of the following formula was wrong *)
+
+lemma Highest_iff_above0: "Highest i = {s. above i s ={}}"
+by (auto simp add: image0_trancl_iff_image0_r)
+
+lemmas above_decreases_lemma =
+ psp [THEN leadsTo_weaken, OF Highest_escapes_above' above_not_increase']
+
+
+lemma above_decreases:
+ "system \<in> (\<Union>j. {s. above i s = x} Int {s. j \<in> above i s} Int Highest j)
+ leadsTo {s. above i s < x}"
+apply (rule leadsTo_UN)
+apply (rule single_leadsTo_I, clarify)
+apply (rule_tac x2 = "above i x" in above_decreases_lemma)
+apply (simp_all (no_asm_use) del: Highest_def add: Highest_iff_above0)
+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\<noteq>{} ==>
+ Acyclic Int {s. above i s = x} <=
+ (\<Union>j. {s. above i s = x} Int {s. j \<in> 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\<noteq>{}==> system \<in> 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 \<in> Acyclic leadsTo Highest i"
+apply (rule_tac f = "%s. above i s" in finite_psubset_induct)
+apply (simp del: Highest_def above_def
+ add: Highest_iff_above0 vimage_def finite_psubset_def, clarify)
+apply (case_tac "m={}")
+apply (rule Int_lower2 [THEN [2] leadsTo_weaken_L])
+apply (force simp add: leadsTo_refl)
+apply (rule_tac A' = "Acyclic Int {x. above i x < m}" in leadsTo_weaken_R)
+apply (blast intro: above_decreases_psp')+
+done
+
+
+text{*We have proved all (relevant) theorems given in the paper. We didn't
+assume any thing about the relation @{term r}. It is not necessary that
+@{term r} be a priority relation as assumed in the original proof. It
+suffices that we start from a state which is finite and acyclic.*}
+
+
end
\ No newline at end of file