--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Counter.ML Fri Jan 05 10:15:48 2001 +0100
@@ -0,0 +1,142 @@
+(* Title: HOL/UNITY/Counter
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+A family of similar counters, version close to the original.
+
+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];
+program_defs_ref := [Component_def];
+Addsimps (map simp_of_act [a_def]);
+
+(* Theorems about sum and sumj *)
+Goal "ALL n. I<n --> sum I (s(c n := x)) = sum I s";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed_spec_mp "sum_upd_gt";
+
+
+Goal "sum I (s(c I := x)) = sum I s";
+by (induct_tac "I" 1);
+by Auto_tac;
+by (simp_tac (simpset()
+ addsimps [rewrite_rule [fun_upd_def] sum_upd_gt]) 1);
+qed "sum_upd_eq";
+
+Goal "sum I (s(C := x)) = sum I s";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed "sum_upd_C";
+
+Goal "sumj I i (s(c i := x)) = sumj I i s";
+by (induct_tac "I" 1);
+by Auto_tac;
+by (simp_tac (simpset() addsimps
+ [rewrite_rule [fun_upd_def] sum_upd_eq]) 1);
+qed "sumj_upd_ci";
+
+Goal "sumj I i (s(C := x)) = sumj I i s";
+by (induct_tac "I" 1);
+by Auto_tac;
+by (simp_tac (simpset()
+ addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1);
+qed "sumj_upd_C";
+
+Goal "ALL i. I<i--> (sumj I i s = sum I s)";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed_spec_mp "sumj_sum_gt";
+
+Goal "(sumj I I s = sum I s)";
+by (induct_tac "I" 1);
+by Auto_tac;
+by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1);
+qed "sumj_sum_eq";
+
+Goal "ALL i. i<I-->(sum I s = s (c i) + sumj I i s)";
+by (induct_tac "I" 1);
+by Auto_tac;
+by (etac nat_neqE 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [sumj_sum_eq])));
+qed_spec_mp "sum_sumj";
+
+(* Correctness proofs for Components *)
+(* p2 and p3 proofs *)
+Goal "Component i : stable {s. s C = s (c i) + k}";
+by (constrains_tac 1);
+qed "p2";
+
+Goal
+"Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}";
+by (constrains_tac 1);
+qed "p3";
+
+
+Goal
+"(ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} \
+\ Int {s. ALL v. v~=c i & v~=C --> s v = k v})) \
+\ = (Component i: stable {s. s C = s (c i) + sumj I i s})";
+by (auto_tac (claset(), simpset()
+ addsimps [constrains_def, stable_def,Component_def,
+ sumj_upd_C, sumj_upd_ci]));
+qed "p2_p3_lemma1";
+
+Goal
+"ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} Int \
+\ {s. ALL v. v~=c i & v~=C --> s v = k v})";
+by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
+qed "p2_p3_lemma2";
+
+
+Goal
+"Component i: stable {s. s C = s (c i) + sumj I i s}";
+by (auto_tac (claset() addSIs [p2_p3_lemma2],
+ simpset() addsimps [p2_p3_lemma1 RS sym]));
+qed "p2_p3";
+
+(* Compositional Proof *)
+
+Goal "(ALL i. i < I --> s (c i) = #0) --> sum I s = #0";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed "sum_0'";
+val sum0_lemma = (sum_0' RS mp) RS sym;
+
+(* I could'nt be empty *)
+Goalw [invariant_def]
+"!!I. 0<I ==> (JN i:{i. i<I}. Component i):invariant {s. s C = sum I s}";
+by (simp_tac (simpset() addsimps [JN_stable,Init_JN,sum_sumj]) 1);
+by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1);
+qed "safety";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Counter.thy Fri Jan 05 10:15:48 2001 +0100
@@ -0,0 +1,41 @@
+(* Title: HOL/UNITY/Counter
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+A family of similar counters, version close to the original.
+
+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.
+*)
+
+Counter = Comp +
+(* Variables are names *)
+datatype name = C | c nat
+types state = name=>int
+
+consts
+ sum :: "[nat,state]=>int"
+ sumj :: "[nat, nat, state]=>int"
+
+primrec (* sum I s = sigma_{i<I}. s (c i) *)
+ "sum 0 s = #0"
+ "sum (Suc i) s = s (c i) + sum i s"
+
+primrec
+ "sumj 0 i s = #0"
+ "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
+
+types command = "(state*state)set"
+
+constdefs
+ a :: "nat=>command"
+ "a i == {(s, s'). s'=s(c i:= s (c i) + #1, C:= s C + #1)}"
+
+ Component :: "nat => state program"
+ "Component i ==
+ mk_program({s. s C = #0 & s (c i) = #0}, {a i},
+ UN G: preserves (%s. s (c i)). Acts G)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Counterc.ML Fri Jan 05 10:15:48 2001 +0100
@@ -0,0 +1,130 @@
+(* Title: HOL/UNITY/Counterc
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+A family of similar counters, version with a full use of "compatibility "
+
+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,
+Component_def RS def_prg_AllowedActs];
+program_defs_ref := [Component_def];
+Addsimps (map simp_of_act [a_def]);
+
+(* Theorems about sum and sumj *)
+Goal "ALL i. I<i--> (sum I s = sumj I i s)";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed_spec_mp "sum_sumj_eq1";
+
+Goal "i<I --> sum I s = c s i + sumj I i s";
+by (induct_tac "I" 1);
+by (auto_tac (claset() addSEs [nat_neqE],
+ simpset() addsimps [sum_sumj_eq1]));
+qed_spec_mp "sum_sumj_eq2";
+
+Goal
+"(ALL i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)";
+by (induct_tac "I" 1 THEN Auto_tac);
+qed_spec_mp "sum_ext";
+
+Goal
+"(ALL j. j<I & j~=i --> c s' j = c s j) --> (sumj I i s' = sumj I i s)";
+by (induct_tac "I" 1);
+by Safe_tac;
+by (auto_tac (claset() addSIs [sum_ext], simpset()));
+qed_spec_mp "sumj_ext";
+
+
+Goal "(ALL i. i<I --> c s i = #0) --> sum I s = #0";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed "sum0";
+
+
+(* Safety properties for Components *)
+
+Goal "(Component i ok G) = \
+\ (G: preserves (%s. c s i) & Component i:Allowed G)";
+by (auto_tac (claset(),
+ simpset() addsimps [ok_iff_Allowed, Component_def RS def_prg_Allowed]));
+qed "Component_ok_iff";
+AddIffs [Component_ok_iff];
+AddIffs [OK_iff_ok];
+Addsimps [preserves_def];
+
+
+Goal "Component i: stable {s. C s = (c s) i + k}";
+by (constrains_tac 1);
+qed "p2";
+
+Goal
+"[| OK I Component; i:I |] ==> \
+\ Component i: stable {s. ALL j:I. j~=i --> c s j = c k j}";
+by (full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 1);
+by (Blast_tac 1);
+qed "p3";
+
+
+Goal
+"[| OK {i. i<I} Component; i<I |] ==> \
+\ ALL k. Component i: stable ({s. C s = c s i + sumj I i k} Int \
+\ {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})";
+by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
+qed "p2_p3_lemma1";
+
+
+Goal
+"(ALL k. F:stable ({s. C s = (c s) i + sumj I i k} Int \
+\ {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})) ==> \
+\ (F:stable {s. C s = c s i + sumj I i s})";
+by (full_simp_tac (simpset() addsimps [constrains_def, stable_def]) 1);
+by (force_tac (claset() addSIs [sumj_ext], simpset()) 1);
+qed "p2_p3_lemma2";
+
+
+Goal
+"[| OK {i. i<I} Component; i<I |] ==> \
+\ Component i: stable {s. C s = c s i + sumj I i s}";
+by (blast_tac (claset() addIs [p2_p3_lemma1 RS p2_p3_lemma2]) 1);
+qed "p2_p3";
+
+
+(* Compositional correctness *)
+Goalw [invariant_def]
+ "[| 0<I; OK {i. i<I} Component |] ==> \
+\ (JN i:{i. i<I}. (Component i)) : invariant {s. C s = sum I s}";
+by (simp_tac (simpset() addsimps [JN_stable, sum_sumj_eq2]) 1);
+by (auto_tac (claset() addSIs [sum0 RS mp, p2_p3],
+ simpset()));
+qed "safety";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Counterc.thy Fri Jan 05 10:15:48 2001 +0100
@@ -0,0 +1,43 @@
+(* Title: HOL/UNITY/Counterc
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+A family of similar counters, version with a full use of "compatibility "
+
+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.
+*)
+
+Counterc = Comp +
+types state
+arities state :: term
+
+consts
+ C :: "state=>int"
+ c :: "state=>nat=>int"
+
+consts
+ sum :: "[nat,state]=>int"
+ sumj :: "[nat, nat, state]=>int"
+
+primrec (* sum I s = sigma_{i<I}. c s i *)
+ "sum 0 s = #0"
+ "sum (Suc i) s = (c s) i + sum i s"
+
+primrec
+ "sumj 0 i s = #0"
+ "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
+
+types command = "(state*state)set"
+
+constdefs
+ a :: "nat=>command"
+ "a i == {(s, s'). (c s') i = (c s) i + #1 & (C s') = (C s) + #1}"
+
+ Component :: "nat => state program"
+ "Component i == mk_program({s. C s = #0 & (c s) i = #0}, {a i},
+ UN G: preserves (%s. (c s) i). Acts G)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Priority.ML Fri Jan 05 10:15:48 2001 +0100
@@ -0,0 +1,239 @@
+(* 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];
+program_defs_ref := [Component_def, system_def];
+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 (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 (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 (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 (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 (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 (constrains_tac 1);
+qed "locality";
+
+
+(**** System properties ****)
+(* property 8: strictly universal *)
+
+Goalw [Safety_def]
+ "system: stable Safety";
+by (rtac stable_INT 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 (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 (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 (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 (ensures_tac "act i" 1);
+by (auto_tac (claset(), simpset() addsimps [Component_def]));
+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, 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 *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Priority.thy Fri Jan 05 10:15:48 2001 +0100
@@ -0,0 +1,68 @@
+(* 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.
+*)
+
+Priority = PriorityAux + Comp + SubstAx +
+
+types state = "(vertex*vertex)set"
+types command = "vertex=>(state*state)set"
+
+consts
+ (* the initial state *)
+ init :: "(vertex*vertex)set"
+
+constdefs
+ (* from the definitions given in section 4.4 *)
+ (* i has highest priority in r *)
+ highest :: "[vertex, (vertex*vertex)set]=>bool"
+ "highest i r == A i r = {}"
+
+ (* i has lowest priority in r *)
+ lowest :: "[vertex, (vertex*vertex)set]=>bool"
+ "lowest i r == R i r = {}"
+
+ act :: command
+ "act i == {(s, s'). s'=reverse i s & highest i s}"
+
+ (* All components start with the same initial state *)
+ Component :: "vertex=>state program"
+ "Component i == mk_program({init}, {act i}, UNIV)"
+
+ (* Abbreviations *)
+ Highest :: "vertex=>state set"
+ "Highest i == {s. highest i s}"
+
+ Lowest :: "vertex=>state set"
+ "Lowest i == {s. lowest i s}"
+
+ Acyclic :: "state set"
+ "Acyclic == {s. acyclic s}"
+
+ (* 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' :: "state set"
+ "Maximal' == INT i. Highest i Un (UN j. {s. j:above i s} Int Highest j)"
+
+
+ Safety :: "state set"
+ "Safety == INT i. {s. highest i s --> (ALL j:neighbors i s. ~highest j s)}"
+
+
+ (* Composition of a finite set of component;
+ the vertex 'UNIV' is finite by assumption *)
+
+ system :: "state program"
+ "system == JN i. Component i"
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/PriorityAux.ML Fri Jan 05 10:15:48 2001 +0100
@@ -0,0 +1,116 @@
+(* Title: HOL/UNITY/PriorityAux
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Auxiliary definitions needed in Priority.thy
+*)
+
+Addsimps [derive_def, derive1_def, symcl_def, A_def, R_def,
+ above_def, reach_def, reverse_def, neighbors_def];
+
+(*All vertex sets are finite \\<dots>*)
+AddIffs [[subset_UNIV, finite_vertex_univ] MRS finite_subset];
+
+(* and relatons over vertex are finite too *)
+AddIffs [[subset_UNIV, [finite_vertex_univ, finite_vertex_univ]
+ MRS finite_Prod_UNIV] MRS finite_subset];
+
+
+(* The equalities (above i r = {}) = (A i r = {})
+ and (reach i r = {}) = (R i r) rely on the following theorem *)
+
+Goal "((r^+)^^{i} = {}) = (r^^{i} = {})";
+by Auto_tac;
+by (etac trancl_induct 1);
+by Auto_tac;
+qed "image0_trancl_iff_image0_r";
+
+(* Another form usefull in some situation *)
+Goal "(r^^{i}={}) = (ALL x. ((i,x):r^+) = False)";
+by Auto_tac;
+by (dtac (image0_trancl_iff_image0_r RS ssubst) 1);
+by Auto_tac;
+qed "image0_r_iff_image0_trancl";
+
+
+(* In finite universe acyclic coincides with wf *)
+Goal
+"!!r::(vertex*vertex)set. acyclic r = wf r";
+by (auto_tac (claset(), simpset() addsimps [wf_iff_acyclic_if_finite]));
+qed "acyclic_eq_wf";
+
+(* derive and derive1 are equivalent *)
+Goal "derive i r q = derive1 i r q";
+by Auto_tac;
+qed "derive_derive1_eq";
+
+(* Lemma 1 *)
+Goalw [reach_def]
+"[| x:reach i q; derive1 k r q |] ==> x~=k --> x:reach i r";
+by (etac ImageE 1);
+by (etac trancl_induct 1);
+by (case_tac "i=k" 1);
+by (auto_tac (claset() addIs [r_into_trancl], simpset()));
+by (dres_inst_tac [("x", "y")] spec 1);
+by (rotate_tac ~1 1);
+by (dres_inst_tac [("x", "z")] spec 1);
+by (auto_tac (claset() addDs [r_into_trancl] addIs [trancl_trans], simpset()));
+qed "lemma1_a";
+
+Goal "ALL k r q. derive k r q -->(reach i q <= (reach i r Un {k}))";
+by (REPEAT(rtac allI 1));
+by (rtac impI 1);
+by (rtac subsetI 1 THEN dtac lemma1_a 1);
+by (auto_tac (claset(), simpset() addsimps [derive_derive1_eq]
+ delsimps [reach_def, derive_def, derive1_def]));
+qed "reach_lemma";
+
+(* An other possible formulation of the above theorem based on
+ the equivalence x:reach y r = y:above x r *)
+Goal
+"(ALL i. reach i q <= (reach i r Un {k})) =\
+\ (ALL x. x~=k --> (ALL i. i~:above x r --> i~:above x q))";
+by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
+qed "reach_above_lemma";
+
+(* Lemma 2 *)
+Goal
+"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)^^{z}={})";
+by Auto_tac;
+by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1);
+by Auto_tac;
+qed "maximal_converse_image0";
+
+Goal
+ "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})";
+by (full_simp_tac (simpset()
+ addsimps [acyclic_eq_wf, wf_eq_minimal]) 1);
+by (dres_inst_tac [("x", "((r^-1)^+)^^{i}")] spec 1);
+by Auto_tac;
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (simpset()
+ addsimps [maximal_converse_image0, trancl_converse]) 1);
+qed "above_lemma_a";
+
+
+Goal
+ "acyclic r ==> above i r~={}-->(EX j:above i r. above j r = {})";
+by (dtac above_lemma_a 1);
+by (auto_tac (claset(), simpset()
+ addsimps [image0_trancl_iff_image0_r]));
+qed "above_lemma_b";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/PriorityAux.thy Fri Jan 05 10:15:48 2001 +0100
@@ -0,0 +1,53 @@
+(* Title: HOL/UNITY/PriorityAux
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Auxiliary definitions needed in Priority.thy
+*)
+
+PriorityAux = Main +
+
+types vertex
+arities vertex::term
+
+constdefs
+ (* symmetric closure: removes the orientation of a relation *)
+ symcl :: "(vertex*vertex)set=>(vertex*vertex)set"
+ "symcl r == r Un (r^-1)"
+
+ (* Neighbors of a vertex i *)
+ neighbors :: "[vertex, (vertex*vertex)set]=>vertex set"
+ "neighbors i r == ((r Un r^-1)^^{i}) - {i}"
+
+ R :: "[vertex, (vertex*vertex)set]=>vertex set"
+ "R i r == r^^{i}"
+
+ A :: "[vertex, (vertex*vertex)set]=>vertex set"
+ "A i r == (r^-1)^^{i}"
+
+ (* reachable and above vertices: the original notation was R* and A* *)
+ reach :: "[vertex, (vertex*vertex)set]=> vertex set"
+ "reach i r == (r^+)^^{i}"
+
+ above :: "[vertex, (vertex*vertex)set]=> vertex set"
+ "above i r == ((r^-1)^+)^^{i}"
+
+ reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set"
+ "reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1"
+
+ (* The original definition *)
+ derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
+ "derive1 i r q == symcl r = symcl q &
+ (ALL k k'. k~=i & k'~=i -->((k,k'):r) = ((k,k'):q)) &
+ A i r = {} & R i q = {}"
+
+ (* Our alternative definition *)
+ derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
+ "derive i r q == A i r = {} & (q = reverse i r)"
+
+rules
+ (* we assume that the universe of vertices is finite *)
+ finite_vertex_univ "finite (UNIV :: vertex set)"
+
+end
--- a/src/HOL/UNITY/ROOT.ML Thu Jan 04 19:41:13 2001 +0100
+++ b/src/HOL/UNITY/ROOT.ML Fri Jan 05 10:15:48 2001 +0100
@@ -21,6 +21,11 @@
time_use_thy "Comp";
time_use_thy "Reachability";
+(*Universal properties examples*)
+time_use_thy "Counter";
+time_use_thy "Counterc";
+time_use_thy "Priority";
+
(*Allocator example*)
time_use_thy "PPROD";
time_use_thy "TimerArray";