new examples by Sidi Ehmety
authorpaulson
Fri Jan 05 10:15:48 2001 +0100 (2001-01-05)
changeset 10782ddb433987557
parent 10781 eedf2def44c1
child 10783 2781ac7a4619
new examples by Sidi Ehmety
src/HOL/UNITY/Counter.ML
src/HOL/UNITY/Counter.thy
src/HOL/UNITY/Counterc.ML
src/HOL/UNITY/Counterc.thy
src/HOL/UNITY/Priority.ML
src/HOL/UNITY/Priority.thy
src/HOL/UNITY/PriorityAux.ML
src/HOL/UNITY/PriorityAux.thy
src/HOL/UNITY/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Counter.ML	Fri Jan 05 10:15:48 2001 +0100
     1.3 @@ -0,0 +1,142 @@
     1.4 +(*  Title:      HOL/UNITY/Counter
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     1.7 +    Copyright   2001  University of Cambridge
     1.8 +
     1.9 +A family of similar counters, version close to the original. 
    1.10 +
    1.11 +From Charpentier and Chandy,
    1.12 +Examples of Program Composition Illustrating the Use of Universal Properties
    1.13 +   In J. Rolim (editor), Parallel and Distributed Processing,
    1.14 +   Spriner LNCS 1586 (1999), pages 1215-1227.
    1.15 +*)
    1.16 +
    1.17 +Addsimps [Component_def RS def_prg_Init];
    1.18 +program_defs_ref := [Component_def];
    1.19 +Addsimps (map simp_of_act  [a_def]);
    1.20 +
    1.21 +(* Theorems about sum and sumj *)
    1.22 +Goal "ALL n. I<n --> sum I (s(c n := x)) = sum I s";
    1.23 +by (induct_tac "I" 1);
    1.24 +by Auto_tac;
    1.25 +qed_spec_mp "sum_upd_gt";
    1.26 +
    1.27 +
    1.28 +Goal "sum I (s(c I := x)) = sum I s";
    1.29 +by (induct_tac "I" 1);
    1.30 +by Auto_tac;
    1.31 +by (simp_tac (simpset() 
    1.32 +    addsimps [rewrite_rule [fun_upd_def] sum_upd_gt]) 1);
    1.33 +qed "sum_upd_eq";
    1.34 +
    1.35 +Goal "sum I (s(C := x)) = sum I s";
    1.36 +by (induct_tac "I" 1);
    1.37 +by Auto_tac;
    1.38 +qed "sum_upd_C";
    1.39 +
    1.40 +Goal "sumj I i (s(c i := x)) = sumj I i s";
    1.41 +by (induct_tac "I" 1);
    1.42 +by Auto_tac;
    1.43 +by (simp_tac (simpset() addsimps 
    1.44 +    [rewrite_rule [fun_upd_def] sum_upd_eq]) 1);
    1.45 +qed "sumj_upd_ci";
    1.46 +
    1.47 +Goal "sumj I i (s(C := x)) = sumj I i s";
    1.48 +by (induct_tac "I" 1);
    1.49 +by Auto_tac;
    1.50 +by (simp_tac (simpset() 
    1.51 +    addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1);
    1.52 +qed "sumj_upd_C";
    1.53 +
    1.54 +Goal "ALL i. I<i--> (sumj I i s = sum I s)";
    1.55 +by (induct_tac "I" 1);
    1.56 +by Auto_tac;
    1.57 +qed_spec_mp  "sumj_sum_gt";
    1.58 +
    1.59 +Goal "(sumj I I s = sum I s)";
    1.60 +by (induct_tac "I" 1);
    1.61 +by Auto_tac;
    1.62 +by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1);
    1.63 +qed "sumj_sum_eq";
    1.64 +
    1.65 +Goal "ALL i. i<I-->(sum I s = s (c i) +  sumj I i s)";
    1.66 +by (induct_tac "I" 1);
    1.67 +by Auto_tac;
    1.68 +by (etac nat_neqE 1);
    1.69 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [sumj_sum_eq])));
    1.70 +qed_spec_mp "sum_sumj";
    1.71 +
    1.72 +(* Correctness proofs for Components *)
    1.73 +(* p2 and p3 proofs *)
    1.74 +Goal "Component i : stable {s. s C = s (c i) + k}";
    1.75 +by (constrains_tac 1);
    1.76 +qed "p2";
    1.77 +
    1.78 +Goal 
    1.79 +"Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}";
    1.80 +by (constrains_tac 1);
    1.81 +qed "p3";
    1.82 +
    1.83 +
    1.84 +Goal 
    1.85 +"(ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} \
    1.86 +\                  Int {s. ALL v. v~=c i & v~=C --> s v = k v})) \
    1.87 +\  = (Component i: stable {s. s C = s (c i) + sumj I i s})";
    1.88 +by (auto_tac (claset(), simpset() 
    1.89 +     addsimps [constrains_def, stable_def,Component_def,
    1.90 +               sumj_upd_C, sumj_upd_ci]));
    1.91 +qed "p2_p3_lemma1";
    1.92 +
    1.93 +Goal 
    1.94 +"ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} Int \
    1.95 +\                             {s. ALL v. v~=c i & v~=C --> s v = k v})";
    1.96 +by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
    1.97 +qed "p2_p3_lemma2";
    1.98 +
    1.99 +
   1.100 +Goal 
   1.101 +"Component i: stable {s.  s C = s (c i) + sumj I i s}";
   1.102 +by (auto_tac (claset() addSIs [p2_p3_lemma2],
   1.103 +              simpset() addsimps [p2_p3_lemma1 RS sym]));
   1.104 +qed "p2_p3";
   1.105 +
   1.106 +(* Compositional Proof *)
   1.107 +
   1.108 +Goal "(ALL i. i < I --> s (c i) = #0) --> sum I s = #0";
   1.109 +by (induct_tac "I" 1);
   1.110 +by Auto_tac;
   1.111 +qed "sum_0'";
   1.112 +val sum0_lemma =  (sum_0' RS mp) RS sym;
   1.113 +
   1.114 +(* I could'nt be empty *)
   1.115 +Goalw [invariant_def] 
   1.116 +"!!I. 0<I ==> (JN i:{i. i<I}. Component i):invariant {s. s C = sum I s}";
   1.117 +by (simp_tac (simpset() addsimps [JN_stable,Init_JN,sum_sumj]) 1);
   1.118 +by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1);
   1.119 +qed "safety";
   1.120 +
   1.121 +
   1.122 +
   1.123 +
   1.124 +
   1.125 +
   1.126 +
   1.127 +
   1.128 +
   1.129 +
   1.130 +
   1.131 +
   1.132 +
   1.133 +
   1.134 +
   1.135 +
   1.136 +
   1.137 +
   1.138 +
   1.139 +
   1.140 +
   1.141 + 
   1.142 +
   1.143 +
   1.144 +
   1.145 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/UNITY/Counter.thy	Fri Jan 05 10:15:48 2001 +0100
     2.3 @@ -0,0 +1,41 @@
     2.4 +(*  Title:      HOL/UNITY/Counter
     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 +A family of similar counters, version close to the original. 
    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 +Counter =  Comp +
    2.18 +(* Variables are names *)
    2.19 +datatype name = C | c nat
    2.20 +types state = name=>int
    2.21 +
    2.22 +consts  
    2.23 +  sum  :: "[nat,state]=>int"
    2.24 +  sumj :: "[nat, nat, state]=>int"
    2.25 +
    2.26 +primrec (* sum I s = sigma_{i<I}. s (c i) *)
    2.27 +  "sum 0 s = #0"
    2.28 +  "sum (Suc i) s = s (c i) + sum i s"
    2.29 +
    2.30 +primrec
    2.31 +  "sumj 0 i s = #0"
    2.32 +  "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
    2.33 +  
    2.34 +types command = "(state*state)set"
    2.35 +
    2.36 +constdefs
    2.37 +  a :: "nat=>command"
    2.38 + "a i == {(s, s'). s'=s(c i:= s (c i) + #1, C:= s C + #1)}"
    2.39 +
    2.40 +  Component :: "nat => state program"
    2.41 +  "Component i ==
    2.42 +    mk_program({s. s C = #0 & s (c i) = #0}, {a i},
    2.43 +	       UN G: preserves (%s. s (c i)). Acts G)"
    2.44 +end  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/UNITY/Counterc.ML	Fri Jan 05 10:15:48 2001 +0100
     3.3 @@ -0,0 +1,130 @@
     3.4 +(*  Title:      HOL/UNITY/Counterc
     3.5 +    ID:         $Id$
     3.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     3.7 +    Copyright   2001  University of Cambridge
     3.8 +
     3.9 +A family of similar counters, version with a full use of "compatibility "
    3.10 +
    3.11 +From Charpentier and Chandy,
    3.12 +Examples of Program Composition Illustrating the Use of Universal Properties
    3.13 +   In J. Rolim (editor), Parallel and Distributed Processing,
    3.14 +   Spriner LNCS 1586 (1999), pages 1215-1227.
    3.15 +*)
    3.16 +
    3.17 +Addsimps [Component_def RS def_prg_Init, 
    3.18 +Component_def RS def_prg_AllowedActs];
    3.19 +program_defs_ref := [Component_def];
    3.20 +Addsimps (map simp_of_act  [a_def]);
    3.21 +
    3.22 +(* Theorems about sum and sumj *)
    3.23 +Goal "ALL i. I<i--> (sum I s = sumj I i s)";
    3.24 +by (induct_tac "I" 1);
    3.25 +by Auto_tac;
    3.26 +qed_spec_mp  "sum_sumj_eq1";
    3.27 +
    3.28 +Goal "i<I --> sum I s  = c s i + sumj I i s";
    3.29 +by (induct_tac "I" 1);
    3.30 +by (auto_tac (claset() addSEs [nat_neqE],
    3.31 +              simpset() addsimps [sum_sumj_eq1]));
    3.32 +qed_spec_mp "sum_sumj_eq2";
    3.33 +
    3.34 +Goal 
    3.35 +"(ALL i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)";
    3.36 +by (induct_tac "I" 1 THEN Auto_tac);
    3.37 +qed_spec_mp "sum_ext";
    3.38 +
    3.39 +Goal 
    3.40 +"(ALL j. j<I & j~=i --> c s' j =  c s j) --> (sumj I i s' = sumj I i s)";
    3.41 +by (induct_tac "I" 1);
    3.42 +by Safe_tac;
    3.43 +by (auto_tac (claset() addSIs [sum_ext], simpset()));
    3.44 +qed_spec_mp "sumj_ext";
    3.45 +
    3.46 +
    3.47 +Goal "(ALL i. i<I --> c s i = #0) -->  sum I s = #0";
    3.48 +by (induct_tac "I" 1);
    3.49 +by Auto_tac;
    3.50 +qed "sum0";
    3.51 +
    3.52 +
    3.53 +(* Safety properties for Components *)
    3.54 +
    3.55 +Goal "(Component i ok G) = \
    3.56 +\     (G: preserves (%s. c s i) & Component i:Allowed G)";
    3.57 +by (auto_tac (claset(), 
    3.58 +  simpset() addsimps [ok_iff_Allowed, Component_def RS def_prg_Allowed]));  
    3.59 +qed "Component_ok_iff";
    3.60 +AddIffs [Component_ok_iff];
    3.61 +AddIffs [OK_iff_ok];
    3.62 +Addsimps [preserves_def];
    3.63 +
    3.64 +
    3.65 +Goal "Component i: stable {s. C s = (c s) i + k}";
    3.66 +by (constrains_tac 1);
    3.67 +qed "p2";
    3.68 +
    3.69 +Goal 
    3.70 +"[| OK I Component; i:I |] ==> \
    3.71 +\ Component i: stable {s. ALL j:I. j~=i --> c s j = c k j}";
    3.72 +by (full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 1);
    3.73 +by (Blast_tac 1);
    3.74 +qed "p3";
    3.75 +
    3.76 +
    3.77 +Goal 
    3.78 +"[| OK {i. i<I} Component; i<I |] ==> \
    3.79 +\ ALL k. Component i: stable ({s. C s = c s i + sumj I i k} Int \
    3.80 +\                             {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})";
    3.81 +by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
    3.82 +qed "p2_p3_lemma1";
    3.83 +
    3.84 +
    3.85 +Goal 
    3.86 +"(ALL k. F:stable ({s. C s = (c s) i + sumj I i k} Int \
    3.87 +\                 {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})) ==> \
    3.88 +\ (F:stable {s. C s = c s i + sumj I i s})";
    3.89 +by (full_simp_tac (simpset() addsimps [constrains_def, stable_def]) 1);
    3.90 +by (force_tac (claset() addSIs [sumj_ext], simpset()) 1);
    3.91 +qed "p2_p3_lemma2";
    3.92 +
    3.93 +
    3.94 +Goal 
    3.95 +"[| OK {i. i<I} Component; i<I |] ==> \
    3.96 +\ Component i: stable {s. C s = c s i + sumj I i s}";
    3.97 +by (blast_tac (claset() addIs [p2_p3_lemma1 RS p2_p3_lemma2]) 1);
    3.98 +qed "p2_p3";
    3.99 +
   3.100 +
   3.101 +(* Compositional correctness *)
   3.102 +Goalw [invariant_def]
   3.103 + "[| 0<I; OK {i. i<I} Component |] ==> \
   3.104 +\     (JN i:{i. i<I}. (Component i)) : invariant {s. C s = sum I s}";
   3.105 +by (simp_tac (simpset() addsimps [JN_stable, sum_sumj_eq2]) 1);
   3.106 +by (auto_tac (claset() addSIs [sum0 RS mp, p2_p3], 
   3.107 +              simpset()));
   3.108 +qed "safety";
   3.109 +
   3.110 +
   3.111 +
   3.112 +
   3.113 +
   3.114 +
   3.115 +
   3.116 +
   3.117 +
   3.118 +
   3.119 +
   3.120 +
   3.121 +
   3.122 +
   3.123 +
   3.124 +
   3.125 +
   3.126 +
   3.127 +
   3.128 +
   3.129 + 
   3.130 +
   3.131 +
   3.132 +
   3.133 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/UNITY/Counterc.thy	Fri Jan 05 10:15:48 2001 +0100
     4.3 @@ -0,0 +1,43 @@
     4.4 +(*  Title:      HOL/UNITY/Counterc
     4.5 +    ID:         $Id$
     4.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     4.7 +    Copyright   2001  University of Cambridge
     4.8 +
     4.9 +A family of similar counters, version with a full use of "compatibility "
    4.10 +
    4.11 +From Charpentier and Chandy,
    4.12 +Examples of Program Composition Illustrating the Use of Universal Properties
    4.13 +   In J. Rolim (editor), Parallel and Distributed Processing,
    4.14 +   Spriner LNCS 1586 (1999), pages 1215-1227.
    4.15 +*)
    4.16 +
    4.17 +Counterc =  Comp +
    4.18 +types state
    4.19 +arities state :: term
    4.20 +
    4.21 +consts
    4.22 +  C :: "state=>int"
    4.23 +  c :: "state=>nat=>int"
    4.24 +
    4.25 +consts  
    4.26 +  sum  :: "[nat,state]=>int"
    4.27 +  sumj :: "[nat, nat, state]=>int"
    4.28 +
    4.29 +primrec (* sum I s = sigma_{i<I}. c s i *)
    4.30 +  "sum 0 s = #0"
    4.31 +  "sum (Suc i) s = (c s) i + sum i s"
    4.32 +
    4.33 +primrec
    4.34 +  "sumj 0 i s = #0"
    4.35 +  "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
    4.36 +  
    4.37 +types command = "(state*state)set"
    4.38 +
    4.39 +constdefs
    4.40 +  a :: "nat=>command"
    4.41 + "a i == {(s, s'). (c s') i = (c s) i + #1 & (C s') = (C s) + #1}"
    4.42 + 
    4.43 +  Component :: "nat => state program"
    4.44 +  "Component i == mk_program({s. C s = #0 & (c s) i = #0}, {a i},
    4.45 +	       UN G: preserves (%s. (c s) i). Acts G)"
    4.46 +end  
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/UNITY/Priority.ML	Fri Jan 05 10:15:48 2001 +0100
     5.3 @@ -0,0 +1,239 @@
     5.4 +(*  Title:      HOL/UNITY/Priority
     5.5 +    ID:         $Id$
     5.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     5.7 +    Copyright   2001  University of Cambridge
     5.8 +
     5.9 +The priority system
    5.10 +
    5.11 +From Charpentier and Chandy,
    5.12 +Examples of Program Composition Illustrating the Use of Universal Properties
    5.13 +   In J. Rolim (editor), Parallel and Distributed Processing,
    5.14 +   Spriner LNCS 1586 (1999), pages 1215-1227.
    5.15 +*)
    5.16 +
    5.17 +Addsimps [Component_def RS def_prg_Init];
    5.18 +program_defs_ref := [Component_def, system_def];
    5.19 +Addsimps [highest_def, lowest_def];
    5.20 +Addsimps [simp_of_act  act_def];
    5.21 +Addsimps (map simp_of_set [Highest_def, Lowest_def]);
    5.22 +
    5.23 +
    5.24 +
    5.25 +
    5.26 +(**** Component correctness proofs  ****)
    5.27 +
    5.28 +(* neighbors is stable  *)
    5.29 +Goal "Component i: stable {s. neighbors k s = n}";
    5.30 +by (constrains_tac 1);
    5.31 +by Auto_tac;
    5.32 +qed "Component_neighbors_stable";
    5.33 +
    5.34 +(* property 4 *)
    5.35 +Goal 
    5.36 +"Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}";
    5.37 +by (constrains_tac 1);
    5.38 +qed "Component_waits_priority";  
    5.39 +
    5.40 +(* property 5: charpentier and Chandy mistakenly express it as
    5.41 + 'transient Highest i'. Consider the case where i has neighbors *)
    5.42 +Goal
    5.43 + "Component i: {s. neighbors i s ~= {}} Int Highest i \
    5.44 +\              ensures - Highest i";
    5.45 +by (ensures_tac "act i" 1);
    5.46 +by (REPEAT(Fast_tac 1));
    5.47 +qed "Component_yields_priority"; 
    5.48 +
    5.49 +(* or better *)
    5.50 +Goal "Component i: Highest i ensures Lowest i";
    5.51 +by (ensures_tac "act i" 1);
    5.52 +by (REPEAT(Fast_tac 1));
    5.53 +qed "Component_yields_priority'";
    5.54 +
    5.55 +(* property 6: Component doesn't introduce cycle *)
    5.56 +Goal "Component i: Highest i co Highest i Un Lowest i";
    5.57 +by (constrains_tac 1);
    5.58 +by (Fast_tac 1);
    5.59 +qed "Component_well_behaves"; 
    5.60 +
    5.61 +(* property 7: local axiom *)
    5.62 +Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}";
    5.63 +by (constrains_tac 1);
    5.64 +qed "locality";  
    5.65 +
    5.66 +
    5.67 +(**** System  properties  ****)
    5.68 +(* property 8: strictly universal *)
    5.69 +
    5.70 +Goalw [Safety_def] 
    5.71 +    "system: stable Safety";
    5.72 +by (rtac stable_INT 1);
    5.73 +by (constrains_tac 1);
    5.74 +by (Fast_tac 1);
    5.75 +qed "Safety"; 
    5.76 +
    5.77 +(* property 13: universal *)
    5.78 +Goal
    5.79 +"system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
    5.80 +by (constrains_tac 1);
    5.81 +by (Blast_tac 1);
    5.82 +qed "p13";
    5.83 +
    5.84 +(* property 14: the 'above set' of a Component that hasn't got 
    5.85 +      priority doesn't increase *)
    5.86 +Goal
    5.87 +"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}";
    5.88 +by (Clarify_tac 1);
    5.89 +by (cut_inst_tac [("i", "j")] reach_lemma 1);
    5.90 +by (constrains_tac 1);
    5.91 +by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
    5.92 +qed "above_not_increase";  
    5.93 +
    5.94 +Goal 
    5.95 +"system: -Highest i Int {s. above i s = x} co {s. above i s <= x}";
    5.96 +by (cut_inst_tac [("i", "i")] above_not_increase 1);
    5.97 +by (asm_full_simp_tac (simpset() addsimps 
    5.98 +                 [trancl_converse, constrains_def]) 1); 
    5.99 +by (Blast_tac 1);
   5.100 +qed "above_not_increase'";  
   5.101 +
   5.102 +
   5.103 +
   5.104 +(* p15: universal property: all Components well behave  *)
   5.105 +Goal "ALL i. system: Highest i co Highest i Un Lowest i";
   5.106 +by (Clarify_tac 1);
   5.107 +by (constrains_tac 1);
   5.108 +by Auto_tac;
   5.109 +qed "system_well_behaves";  
   5.110 +
   5.111 +
   5.112 +Goal "Acyclic = (INT i. {s. i~:above i s})";
   5.113 +by (auto_tac (claset(), simpset() 
   5.114 +   addsimps [Acyclic_def, acyclic_def, trancl_converse]));
   5.115 +qed "Acyclic_eq";
   5.116 +
   5.117 +
   5.118 +val lemma = [above_not_increase RS spec, 
   5.119 +           system_well_behaves RS spec] MRS constrains_Un;
   5.120 +Goal 
   5.121 +"system: stable Acyclic";
   5.122 +by (auto_tac (claset() addSIs [stable_INT, stableI, 
   5.123 +                               lemma RS constrains_weaken],
   5.124 +              simpset() addsimps [Acyclic_eq, 
   5.125 +                    image0_r_iff_image0_trancl,trancl_converse]));
   5.126 +qed "Acyclic_stable";
   5.127 +
   5.128 +
   5.129 +Goalw [Acyclic_def, Maximal_def]
   5.130 +"Acyclic <= Maximal";
   5.131 +by (Clarify_tac 1);
   5.132 +by (dtac above_lemma_b 1);
   5.133 +by Auto_tac;
   5.134 +qed "Acyclic_subset_Maximal";
   5.135 +
   5.136 +(* property 17: original one is an invariant *)
   5.137 +Goal 
   5.138 +"system: stable (Acyclic Int Maximal)";
   5.139 +by (simp_tac (simpset() addsimps 
   5.140 +     [Acyclic_subset_Maximal RS Int_absorb2, Acyclic_stable]) 1);
   5.141 +qed "Acyclic_Maximal_stable";  
   5.142 +
   5.143 +
   5.144 +(* propert 5: existential property *)
   5.145 +
   5.146 +Goal "system: Highest i leadsTo Lowest i";
   5.147 +by (ensures_tac "act i" 1);
   5.148 +by (auto_tac (claset(), simpset() addsimps [Component_def]));
   5.149 +qed "Highest_leadsTo_Lowest";
   5.150 +
   5.151 +(* a lowest i can never be in any abover set *) 
   5.152 +Goal "Lowest i <= (INT k. {s. i~:above k s})";
   5.153 +by (auto_tac (claset(), 
   5.154 +          simpset() addsimps [image0_r_iff_image0_trancl, trancl_converse]));
   5.155 +qed  "Lowest_above_subset";
   5.156 +
   5.157 +(* property 18: a simpler proof than the original, one which uses psp *)
   5.158 +Goal "system: Highest i leadsTo (INT k. {s. i~:above k s})";
   5.159 +by (rtac leadsTo_weaken_R 1);
   5.160 +by (rtac Lowest_above_subset 2);
   5.161 +by (rtac Highest_leadsTo_Lowest 1);
   5.162 +qed "Highest_escapes_above";
   5.163 +
   5.164 +Goal 
   5.165 +"system: Highest j Int {s. j:above i s} leadsTo {s. j~:above i s}";
   5.166 +by (blast_tac (claset() addIs 
   5.167 +   [[Highest_escapes_above, Int_lower1, INT_lower] MRS leadsTo_weaken]) 1);
   5.168 +qed "Highest_escapes_above'"; 
   5.169 +
   5.170 +(*** The main result: above set decreases ***)
   5.171 +(* The original proof of the following formula was wrong *)
   5.172 +val above_decreases_lemma = 
   5.173 +[Highest_escapes_above', above_not_increase'] MRS psp RS leadsTo_weaken;
   5.174 +
   5.175 +Goal "Highest i = {s. above i s ={}}";
   5.176 +by (auto_tac (claset(), 
   5.177 +        simpset() addsimps [image0_trancl_iff_image0_r]));
   5.178 +qed "Highest_iff_above0";
   5.179 +
   5.180 +
   5.181 +Goal 
   5.182 +"system: (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j) \
   5.183 +\          leadsTo {s. above i s < x}";
   5.184 +by (rtac leadsTo_UN 1);
   5.185 +by (rtac single_leadsTo_I 1);
   5.186 +by (Clarify_tac 1);
   5.187 +by (res_inst_tac [("x2", "above i x")] above_decreases_lemma 1);
   5.188 +by (ALLGOALS(full_simp_tac (simpset() delsimps [Highest_def]
   5.189 +                  addsimps [Highest_iff_above0])));
   5.190 +by (REPEAT(Blast_tac 1));
   5.191 +qed "above_decreases";  
   5.192 +
   5.193 +(** Just a massage of conditions to have the desired form ***)
   5.194 +Goalw [Maximal_def, Maximal'_def, Highest_def]
   5.195 +"Maximal = Maximal'";
   5.196 +by (Blast_tac 1);
   5.197 +qed "Maximal_eq_Maximal'";
   5.198 +
   5.199 +Goal "x~={} ==> \
   5.200 +\   Acyclic Int {s. above i s = x} <= \
   5.201 +\   (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j)";
   5.202 +by (res_inst_tac [("B", "Maximal' Int {s. above i s = x}")] subset_trans 1);
   5.203 +by (simp_tac (simpset() addsimps [Maximal_eq_Maximal' RS sym]) 1);
   5.204 +by (blast_tac (claset() addIs [Acyclic_subset_Maximal RS subsetD]) 1);
   5.205 +by (simp_tac (simpset() delsimps [above_def] addsimps [Maximal'_def, Highest_iff_above0]) 1);
   5.206 +by (Blast_tac 1);
   5.207 +qed "Acyclic_subset";
   5.208 +
   5.209 +val above_decreases' = [above_decreases, Acyclic_subset] MRS leadsTo_weaken_L;
   5.210 +val above_decreases_psp = [above_decreases', Acyclic_stable] MRS psp_stable;
   5.211 +
   5.212 +Goal 
   5.213 +"x~={}==> \
   5.214 +\ system: Acyclic Int {s. above i s = x} leadsTo Acyclic Int {s. above i s < x}";
   5.215 +by (etac (above_decreases_psp RS leadsTo_weaken) 1);
   5.216 +by (Blast_tac 1);
   5.217 +by Auto_tac;
   5.218 +qed "above_decreases_psp'";
   5.219 +
   5.220 +
   5.221 +val finite_psubset_induct = wf_finite_psubset RS leadsTo_wf_induct;
   5.222 +val leadsTo_weaken_L' = rotate_prems 1 leadsTo_weaken_L;
   5.223 +
   5.224 +
   5.225 +Goal "system: Acyclic leadsTo Highest i";
   5.226 +by (res_inst_tac [("f", "%s. above i s")] finite_psubset_induct 1);
   5.227 +by (asm_simp_tac (simpset() delsimps [Highest_def, above_def] 
   5.228 +                            addsimps [Highest_iff_above0,
   5.229 +                                      vimage_def, finite_psubset_def]) 1); 
   5.230 +by (Clarify_tac 1);
   5.231 +by (case_tac "m={}" 1);
   5.232 +by (rtac (Int_lower2 RS leadsTo_weaken_L') 1);
   5.233 +by (force_tac (claset(), simpset() addsimps [leadsTo_refl]) 1);
   5.234 +by (res_inst_tac [("A'", "Acyclic Int {x. above i x < m}")] 
   5.235 +    leadsTo_weaken_R 1);
   5.236 +by (REPEAT(blast_tac (claset() addIs [above_decreases_psp']) 1));
   5.237 +qed "Progress";
   5.238 +
   5.239 +(* We have proved all (relevant) theorems given in the paper *)
   5.240 +(* We didn't assume any thing about the relation r *)
   5.241 +(* It is not necessary that r be a priority relation as assumed in the original proof *)
   5.242 +(* It suffices that we start from a state which is finite and acyclic *)
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/UNITY/Priority.thy	Fri Jan 05 10:15:48 2001 +0100
     6.3 @@ -0,0 +1,68 @@
     6.4 +(*  Title:      HOL/UNITY/Priority
     6.5 +    ID:         $Id$
     6.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     6.7 +    Copyright   2001  University of Cambridge
     6.8 +
     6.9 +The priority system
    6.10 +
    6.11 +From Charpentier and Chandy,
    6.12 +Examples of Program Composition Illustrating the Use of Universal Properties
    6.13 +   In J. Rolim (editor), Parallel and Distributed Processing,
    6.14 +   Spriner LNCS 1586 (1999), pages 1215-1227.
    6.15 +*)
    6.16 +
    6.17 +Priority = PriorityAux + Comp + SubstAx +
    6.18 +
    6.19 +types state = "(vertex*vertex)set"
    6.20 +types command = "vertex=>(state*state)set"
    6.21 +  
    6.22 +consts
    6.23 +  (* the initial state *)
    6.24 +  init :: "(vertex*vertex)set"  
    6.25 +
    6.26 +constdefs
    6.27 +  (* from the definitions given in section 4.4 *)
    6.28 +  (* i has highest priority in r *)
    6.29 +  highest :: "[vertex, (vertex*vertex)set]=>bool"
    6.30 +  "highest i r == A i r = {}"
    6.31 +  
    6.32 +  (* i has lowest priority in r *)
    6.33 +  lowest :: "[vertex, (vertex*vertex)set]=>bool"
    6.34 +  "lowest i r == R i r = {}"
    6.35 +
    6.36 +  act :: command
    6.37 +  "act i == {(s, s'). s'=reverse i s & highest i s}"
    6.38 +
    6.39 +  (* All components start with the same initial state *)
    6.40 +  Component :: "vertex=>state program"
    6.41 +  "Component i == mk_program({init}, {act i}, UNIV)"
    6.42 +
    6.43 +  (* Abbreviations *)
    6.44 +  Highest :: "vertex=>state set"
    6.45 +  "Highest i == {s. highest i s}"
    6.46 +
    6.47 +  Lowest :: "vertex=>state set"
    6.48 +  "Lowest i == {s. lowest i s}"
    6.49 +
    6.50 +  Acyclic :: "state set"
    6.51 +  "Acyclic == {s. acyclic s}"
    6.52 +
    6.53 +  (* Every above set has a maximal vertex: two equivalent defs. *)
    6.54 +
    6.55 +  Maximal :: "state set"
    6.56 +  "Maximal == INT i. {s. ~highest i s-->(EX j:above i  s. highest j s)}"
    6.57 +
    6.58 +  Maximal' :: "state set"
    6.59 +  "Maximal' == INT i. Highest i Un (UN j. {s. j:above i s} Int Highest j)"
    6.60 +
    6.61 +  
    6.62 +  Safety :: "state set"
    6.63 +  "Safety == INT i. {s. highest i s --> (ALL j:neighbors i s. ~highest j s)}"
    6.64 +
    6.65 +
    6.66 +  (* Composition of a finite set of component;
    6.67 +     the vertex 'UNIV' is finite by assumption *)
    6.68 +  
    6.69 +  system :: "state program"
    6.70 +  "system == JN i. Component i"
    6.71 +end
    6.72 \ No newline at end of file
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/UNITY/PriorityAux.ML	Fri Jan 05 10:15:48 2001 +0100
     7.3 @@ -0,0 +1,116 @@
     7.4 +(*  Title:      HOL/UNITY/PriorityAux
     7.5 +    ID:         $Id$
     7.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     7.7 +    Copyright   2001  University of Cambridge
     7.8 +
     7.9 +Auxiliary definitions needed in Priority.thy
    7.10 +*)
    7.11 +
    7.12 +Addsimps [derive_def, derive1_def, symcl_def, A_def, R_def,  
    7.13 +          above_def, reach_def, reverse_def, neighbors_def];
    7.14 +
    7.15 +(*All vertex sets are finite \\<dots>*)
    7.16 +AddIffs [[subset_UNIV, finite_vertex_univ] MRS finite_subset];
    7.17 +
    7.18 +(* and relatons over vertex are finite too *)
    7.19 +AddIffs [[subset_UNIV, [finite_vertex_univ, finite_vertex_univ] 
    7.20 +           MRS finite_Prod_UNIV] MRS finite_subset];
    7.21 +
    7.22 +
    7.23 +(* The equalities (above i r = {}) = (A i r = {}) 
    7.24 +   and (reach i r = {}) = (R i r) rely on the following theorem  *)
    7.25 +
    7.26 +Goal "((r^+)^^{i} = {}) = (r^^{i} = {})";
    7.27 +by Auto_tac;
    7.28 +by (etac trancl_induct 1);
    7.29 +by Auto_tac;
    7.30 +qed "image0_trancl_iff_image0_r";
    7.31 +
    7.32 +(* Another form usefull in some situation *)
    7.33 +Goal "(r^^{i}={}) = (ALL x. ((i,x):r^+) = False)";
    7.34 +by Auto_tac;
    7.35 +by (dtac (image0_trancl_iff_image0_r RS ssubst) 1);
    7.36 +by Auto_tac;
    7.37 +qed "image0_r_iff_image0_trancl";
    7.38 +
    7.39 +
    7.40 +(* In finite universe acyclic coincides with wf *)
    7.41 +Goal 
    7.42 +"!!r::(vertex*vertex)set. acyclic r = wf r";
    7.43 +by (auto_tac (claset(), simpset() addsimps [wf_iff_acyclic_if_finite]));
    7.44 +qed "acyclic_eq_wf";
    7.45 +
    7.46 +(* derive and derive1 are equivalent *)
    7.47 +Goal "derive i r q = derive1 i r q";
    7.48 +by Auto_tac;
    7.49 +qed "derive_derive1_eq";
    7.50 +
    7.51 +(* Lemma 1 *)
    7.52 +Goalw [reach_def]
    7.53 +"[| x:reach i q; derive1 k r q |] ==> x~=k --> x:reach i r";
    7.54 +by (etac ImageE 1);
    7.55 +by (etac trancl_induct 1);
    7.56 +by (case_tac "i=k" 1);
    7.57 +by (auto_tac (claset() addIs [r_into_trancl], simpset()));
    7.58 +by (dres_inst_tac [("x", "y")] spec 1);
    7.59 +by (rotate_tac ~1 1);
    7.60 +by (dres_inst_tac [("x", "z")] spec 1);
    7.61 +by (auto_tac (claset() addDs [r_into_trancl] addIs [trancl_trans], simpset()));
    7.62 +qed "lemma1_a";
    7.63 +
    7.64 +Goal "ALL k r q. derive k r q -->(reach i q <= (reach i r Un {k}))";
    7.65 +by (REPEAT(rtac allI 1));
    7.66 +by (rtac impI 1);
    7.67 +by (rtac subsetI 1 THEN dtac lemma1_a 1);
    7.68 +by (auto_tac (claset(), simpset() addsimps [derive_derive1_eq]
    7.69 +                    delsimps [reach_def, derive_def, derive1_def]));
    7.70 +qed "reach_lemma";
    7.71 +
    7.72 +(* An other possible formulation of the above theorem based on
    7.73 +   the equivalence x:reach y r = y:above x r                  *)
    7.74 +Goal 
    7.75 +"(ALL i. reach i q <= (reach i r Un {k})) =\
    7.76 +\ (ALL x. x~=k --> (ALL i. i~:above x r --> i~:above x q))";
    7.77 +by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
    7.78 +qed "reach_above_lemma";
    7.79 +
    7.80 +(* Lemma 2 *)
    7.81 +Goal 
    7.82 +"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)^^{z}={})";
    7.83 +by Auto_tac;
    7.84 +by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1);
    7.85 +by Auto_tac;
    7.86 +qed "maximal_converse_image0";
    7.87 +
    7.88 +Goal
    7.89 + "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})";
    7.90 +by (full_simp_tac (simpset() 
    7.91 +            addsimps [acyclic_eq_wf, wf_eq_minimal]) 1);
    7.92 +by (dres_inst_tac [("x", "((r^-1)^+)^^{i}")] spec 1);
    7.93 +by Auto_tac;
    7.94 +by (rotate_tac ~1 1);
    7.95 +by (asm_full_simp_tac (simpset() 
    7.96 +        addsimps [maximal_converse_image0, trancl_converse]) 1);
    7.97 +qed "above_lemma_a";
    7.98 +
    7.99 +
   7.100 +Goal
   7.101 + "acyclic r ==> above i r~={}-->(EX j:above i r. above j r = {})";
   7.102 +by (dtac above_lemma_a 1);
   7.103 +by (auto_tac (claset(), simpset() 
   7.104 +        addsimps [image0_trancl_iff_image0_r]));
   7.105 +qed "above_lemma_b";
   7.106 +
   7.107 +
   7.108 +
   7.109 +
   7.110 +
   7.111 +
   7.112 +
   7.113 +
   7.114 +
   7.115 +
   7.116 +
   7.117 +
   7.118 +
   7.119 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/UNITY/PriorityAux.thy	Fri Jan 05 10:15:48 2001 +0100
     8.3 @@ -0,0 +1,53 @@
     8.4 +(*  Title:      HOL/UNITY/PriorityAux
     8.5 +    ID:         $Id$
     8.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     8.7 +    Copyright   2001  University of Cambridge
     8.8 +
     8.9 +Auxiliary definitions needed in Priority.thy
    8.10 +*)
    8.11 +
    8.12 +PriorityAux  =  Main +
    8.13 +
    8.14 +types vertex
    8.15 +arities vertex::term
    8.16 +  
    8.17 +constdefs
    8.18 +  (* symmetric closure: removes the orientation of a relation *)
    8.19 +  symcl :: "(vertex*vertex)set=>(vertex*vertex)set"
    8.20 +  "symcl r == r Un (r^-1)"
    8.21 +
    8.22 +  (* Neighbors of a vertex i *)
    8.23 +  neighbors :: "[vertex, (vertex*vertex)set]=>vertex set"
    8.24 + "neighbors i r == ((r Un r^-1)^^{i}) - {i}"
    8.25 +
    8.26 +  R :: "[vertex, (vertex*vertex)set]=>vertex set"
    8.27 +  "R i r == r^^{i}"
    8.28 +
    8.29 +  A :: "[vertex, (vertex*vertex)set]=>vertex set"
    8.30 +  "A i r == (r^-1)^^{i}"
    8.31 +
    8.32 +  (* reachable and above vertices: the original notation was R* and A* *)  
    8.33 +  reach :: "[vertex, (vertex*vertex)set]=> vertex set"
    8.34 +  "reach i r == (r^+)^^{i}"
    8.35 +
    8.36 +  above :: "[vertex, (vertex*vertex)set]=> vertex set"
    8.37 +  "above i r == ((r^-1)^+)^^{i}"  
    8.38 +
    8.39 +  reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set"
    8.40 +  "reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1"
    8.41 +
    8.42 +  (* The original definition *)
    8.43 +  derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
    8.44 +  "derive1 i r q == symcl r = symcl q &
    8.45 +                    (ALL k k'. k~=i & k'~=i -->((k,k'):r) = ((k,k'):q)) &
    8.46 +                    A i r = {} & R i q = {}"
    8.47 +
    8.48 +  (* Our alternative definition *)
    8.49 +  derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
    8.50 +  "derive i r q == A i r = {} & (q = reverse i r)"
    8.51 +
    8.52 +rules
    8.53 +  (* we assume that the universe of vertices is finite  *)
    8.54 +  finite_vertex_univ "finite (UNIV :: vertex set)"
    8.55 +
    8.56 +end
     9.1 --- a/src/HOL/UNITY/ROOT.ML	Thu Jan 04 19:41:13 2001 +0100
     9.2 +++ b/src/HOL/UNITY/ROOT.ML	Fri Jan 05 10:15:48 2001 +0100
     9.3 @@ -21,6 +21,11 @@
     9.4  time_use_thy "Comp";
     9.5  time_use_thy "Reachability";
     9.6  
     9.7 +(*Universal properties examples*)
     9.8 +time_use_thy "Counter";
     9.9 +time_use_thy "Counterc";
    9.10 +time_use_thy "Priority";
    9.11 +
    9.12  (*Allocator example*)
    9.13  time_use_thy "PPROD";
    9.14  time_use_thy "TimerArray";