1(*  Title:      HOL/UNITY/Comp/Counter.thy
2    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
3    Copyright   2001  University of Cambridge
4
5From Charpentier and Chandy,
6Examples of Program Composition Illustrating the Use of Universal Properties
7   In J. Rolim (editor), Parallel and Distributed Processing,
8   Springer LNCS 1586 (1999), pages 1215-1227.
9*)
10
11section\<open>A Family of Similar Counters: Original Version\<close>
12
13theory Counter imports "../UNITY_Main" begin
14
15(* Variables are names *)
16datatype name = C | c nat
17type_synonym state = "name=>int"
18
19primrec sum  :: "[nat,state]=>int" where
20  (* sum I s = sigma_{i<I}. s (c i) *)
21  "sum 0 s = 0"
22| "sum (Suc i) s = s (c i) + sum i s"
23
24primrec sumj :: "[nat, nat, state]=>int" where
25  "sumj 0 i s = 0"
26| "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
27  
28type_synonym command = "(state*state)set"
29
30definition a :: "nat=>command" where
31 "a i = {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}"
32
33definition Component :: "nat => state program" where
34  "Component i =
35    mk_total_program({s. s C = 0 & s (c i) = 0}, {a i},
36                     \<Union>G \<in> preserves (%s. s (c i)). Acts G)"
37
38
39
40declare Component_def [THEN def_prg_Init, simp]
41declare a_def [THEN def_act_simp, simp]
42
43(* Theorems about sum and sumj *)
44lemma sum_upd_gt: "I<n ==> sum I (s(c n := x)) = sum I s"
45  by (induct I) auto
46
47
48lemma sum_upd_eq: "sum I (s(c I := x)) = sum I s"
49  by (induct I) (auto simp add: sum_upd_gt [unfolded fun_upd_def])
50
51lemma sum_upd_C: "sum I (s(C := x)) = sum I s"
52  by (induct I) auto
53
54lemma sumj_upd_ci: "sumj I i (s(c i := x)) = sumj I i s"
55  by (induct I) (auto simp add: sum_upd_eq [unfolded fun_upd_def])
56
57lemma sumj_upd_C: "sumj I i (s(C := x)) = sumj I i s"
58  by (induct I) (auto simp add: sum_upd_C [unfolded fun_upd_def])
59
60lemma sumj_sum_gt: "I<i ==> sumj I i s = sum I s"
61  by (induct I) auto
62
63lemma sumj_sum_eq: "(sumj I I s = sum I s)"
64  by (induct I) (auto simp add: sumj_sum_gt)
65
66lemma sum_sumj: "i<I ==> sum I s = s (c i) +  sumj I i s"
67  by (induct I) (auto simp add: linorder_neq_iff sumj_sum_eq)
68
69(* Correctness proofs for Components *)
70(* p2 and p3 proofs *)
71lemma p2: "Component i \<in> stable {s. s C = s (c i) + k}"
72by (simp add: Component_def, safety)
73
74lemma p3: "Component i \<in> stable {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v}"
75by (simp add: Component_def, safety)
76
77
78lemma p2_p3_lemma1: 
79"(\<forall>k. Component i \<in> stable ({s. s C = s (c i) + sumj I i k}  
80                   \<inter> {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v}))  
81   = (Component i \<in> stable {s. s C = s (c i) + sumj I i s})"
82apply (simp add: Component_def mk_total_program_def)
83apply (auto simp add: constrains_def stable_def sumj_upd_C sumj_upd_ci)
84done
85
86lemma p2_p3_lemma2: 
87"\<forall>k. Component i \<in> stable ({s. s C = s (c i) + sumj I i k} Int  
88                            {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v})"
89by (blast intro: stable_Int [OF p2 p3])
90
91lemma p2_p3: "Component i \<in> stable {s.  s C = s (c i) + sumj I i s}"
92by (auto intro!: p2_p3_lemma2 simp add: p2_p3_lemma1 [symmetric])
93
94(* Compositional Proof *)
95
96lemma sum_0': "(\<And>i. i < I ==> s (c i) = 0) ==> sum I s = 0"
97  by (induct I) auto
98
99(* I cannot be empty *)
100lemma safety:
101     "0<I ==> (\<Squnion>i \<in> {i. i<I}. Component i) \<in> invariant {s. s C = sum I s}"
102apply (simp (no_asm) add: invariant_def JN_stable sum_sumj)
103apply (force intro: p2_p3 sum_0')
104done
105
106end  
107