1 (* Title: HOL/UNITY/Counter |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 A family of similar counters, version close to the original. |
|
7 |
|
8 From Charpentier and Chandy, |
|
9 Examples of Program Composition Illustrating the Use of Universal Properties |
|
10 In J. Rolim (editor), Parallel and Distributed Processing, |
|
11 Spriner LNCS 1586 (1999), pages 1215-1227. |
|
12 *) |
|
13 |
|
14 Addsimps [Component_def RS def_prg_Init, simp_of_act a_def]; |
|
15 |
|
16 (* Theorems about sum and sumj *) |
|
17 Goal "\\<forall>n. I<n --> sum I (s(c n := x)) = sum I s"; |
|
18 by (induct_tac "I" 1); |
|
19 by Auto_tac; |
|
20 qed_spec_mp "sum_upd_gt"; |
|
21 |
|
22 |
|
23 Goal "sum I (s(c I := x)) = sum I s"; |
|
24 by (induct_tac "I" 1); |
|
25 by Auto_tac; |
|
26 by (simp_tac (simpset() |
|
27 addsimps [rewrite_rule [fun_upd_def] sum_upd_gt]) 1); |
|
28 qed "sum_upd_eq"; |
|
29 |
|
30 Goal "sum I (s(C := x)) = sum I s"; |
|
31 by (induct_tac "I" 1); |
|
32 by Auto_tac; |
|
33 qed "sum_upd_C"; |
|
34 |
|
35 Goal "sumj I i (s(c i := x)) = sumj I i s"; |
|
36 by (induct_tac "I" 1); |
|
37 by Auto_tac; |
|
38 by (simp_tac (simpset() addsimps |
|
39 [rewrite_rule [fun_upd_def] sum_upd_eq]) 1); |
|
40 qed "sumj_upd_ci"; |
|
41 |
|
42 Goal "sumj I i (s(C := x)) = sumj I i s"; |
|
43 by (induct_tac "I" 1); |
|
44 by Auto_tac; |
|
45 by (simp_tac (simpset() |
|
46 addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1); |
|
47 qed "sumj_upd_C"; |
|
48 |
|
49 Goal "\\<forall>i. I<i--> (sumj I i s = sum I s)"; |
|
50 by (induct_tac "I" 1); |
|
51 by Auto_tac; |
|
52 qed_spec_mp "sumj_sum_gt"; |
|
53 |
|
54 Goal "(sumj I I s = sum I s)"; |
|
55 by (induct_tac "I" 1); |
|
56 by Auto_tac; |
|
57 by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1); |
|
58 qed "sumj_sum_eq"; |
|
59 |
|
60 Goal "\\<forall>i. i<I-->(sum I s = s (c i) + sumj I i s)"; |
|
61 by (induct_tac "I" 1); |
|
62 by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq])); |
|
63 qed_spec_mp "sum_sumj"; |
|
64 |
|
65 (* Correctness proofs for Components *) |
|
66 (* p2 and p3 proofs *) |
|
67 Goal "Component i \\<in> stable {s. s C = s (c i) + k}"; |
|
68 by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); |
|
69 by (constrains_tac 1); |
|
70 qed "p2"; |
|
71 |
|
72 Goal "Component i \\<in> stable {s. \\<forall>v. v~=c i & v~=C --> s v = k v}"; |
|
73 by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); |
|
74 by (constrains_tac 1); |
|
75 qed "p3"; |
|
76 |
|
77 |
|
78 Goal |
|
79 "(\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} \ |
|
80 \ \\<inter> {s. \\<forall>v. v~=c i & v~=C --> s v = k v})) \ |
|
81 \ = (Component i \\<in> stable {s. s C = s (c i) + sumj I i s})"; |
|
82 by (asm_full_simp_tac (simpset() addsimps [Component_def, mk_total_program_def]) 1); |
|
83 by (auto_tac (claset(), simpset() |
|
84 addsimps [constrains_def, stable_def, sumj_upd_C, sumj_upd_ci])); |
|
85 qed "p2_p3_lemma1"; |
|
86 |
|
87 Goal |
|
88 "\\<forall>k. Component i \\<in> stable ({s. s C = s (c i) + sumj I i k} Int \ |
|
89 \ {s. \\<forall>v. v~=c i & v~=C --> s v = k v})"; |
|
90 by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1); |
|
91 qed "p2_p3_lemma2"; |
|
92 |
|
93 |
|
94 Goal |
|
95 "Component i \\<in> stable {s. s C = s (c i) + sumj I i s}"; |
|
96 by (auto_tac (claset() addSIs [p2_p3_lemma2], |
|
97 simpset() addsimps [p2_p3_lemma1 RS sym])); |
|
98 qed "p2_p3"; |
|
99 |
|
100 (* Compositional Proof *) |
|
101 |
|
102 Goal "(\\<forall>i. i < I --> s (c i) = 0) --> sum I s = 0"; |
|
103 by (induct_tac "I" 1); |
|
104 by Auto_tac; |
|
105 qed "sum_0'"; |
|
106 val sum0_lemma = (sum_0' RS mp) RS sym; |
|
107 |
|
108 (* I could'nt be empty *) |
|
109 Goalw [invariant_def] |
|
110 "!!I. 0<I ==> (\\<Squnion>i \\<in> {i. i<I}. Component i) \\<in> invariant {s. s C = sum I s}"; |
|
111 by (simp_tac (simpset() addsimps [JN_stable, sum_sumj]) 1); |
|
112 by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1); |
|
113 qed "safety"; |
|