# HG changeset patch
# User paulson
# Date 978686148 -3600
# Node ID ddb433987557243b3a86d0fceff128007545435f
# Parent  eedf2def44c1935b11ee9e7863c695d8706b77d3
new examples by Sidi Ehmety

diff -r eedf2def44c1 -r ddb433987557 src/HOL/UNITY/Counter.ML
--- /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";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 
+
+
+
+
diff -r eedf2def44c1 -r ddb433987557 src/HOL/UNITY/Counter.thy
--- /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  
diff -r eedf2def44c1 -r ddb433987557 src/HOL/UNITY/Counterc.ML
--- /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";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 
+
+
+
+
diff -r eedf2def44c1 -r ddb433987557 src/HOL/UNITY/Counterc.thy
--- /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  
diff -r eedf2def44c1 -r ddb433987557 src/HOL/UNITY/Priority.ML
--- /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 *)
diff -r eedf2def44c1 -r ddb433987557 src/HOL/UNITY/Priority.thy
--- /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
diff -r eedf2def44c1 -r ddb433987557 src/HOL/UNITY/PriorityAux.ML
--- /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";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff -r eedf2def44c1 -r ddb433987557 src/HOL/UNITY/PriorityAux.thy
--- /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
diff -r eedf2def44c1 -r ddb433987557 src/HOL/UNITY/ROOT.ML
--- 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";