author paulson Fri Jan 05 10:15:48 2001 +0100 (2001-01-05) changeset 10782 ddb433987557 parent 10781 eedf2def44c1 child 10783 2781ac7a4619
new examples by Sidi Ehmety
 src/HOL/UNITY/Counter.ML file | annotate | diff | revisions src/HOL/UNITY/Counter.thy file | annotate | diff | revisions src/HOL/UNITY/Counterc.ML file | annotate | diff | revisions src/HOL/UNITY/Counterc.thy file | annotate | diff | revisions src/HOL/UNITY/Priority.ML file | annotate | diff | revisions src/HOL/UNITY/Priority.thy file | annotate | diff | revisions src/HOL/UNITY/PriorityAux.ML file | annotate | diff | revisions src/HOL/UNITY/PriorityAux.thy file | annotate | diff | revisions src/HOL/UNITY/ROOT.ML file | annotate | diff | revisions
```     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.18 +program_defs_ref := [Component_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.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.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.18 +Component_def RS def_prg_AllowedActs];
3.19 +program_defs_ref := [Component_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.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.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.18 +program_defs_ref := [Component_def, system_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.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.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.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.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.160 +by (rtac Lowest_above_subset 2);
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.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.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.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.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.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.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.234 +by (res_inst_tac [("A'", "Acyclic Int {x. above i x < m}")]
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.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.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.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";
```