src/HOL/UNITY/Comp/Counter.ML
 author paulson Sat Feb 08 16:05:33 2003 +0100 (2003-02-08) changeset 13812 91713a1915ee parent 13797 baefae13ad37 permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
1 (*  Title:      HOL/UNITY/Counter
2     ID:         \$Id\$
3     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
4     Copyright   2001  University of Cambridge
6 A family of similar counters, version close to the original.
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 *)
14 Addsimps [Component_def RS def_prg_Init, simp_of_act a_def];
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";
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";
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";
35 Goal "sumj I i (s(c i := x)) = sumj I i s";
36 by (induct_tac "I" 1);
37 by Auto_tac;
39     [rewrite_rule [fun_upd_def] sum_upd_eq]) 1);
40 qed "sumj_upd_ci";
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";
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";
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";
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";
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";
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";
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";
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";
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";
100 (* Compositional Proof *)
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;
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";