1(*  Title:      HOL/UNITY/Comp/Counterc.thy
2    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
3    Copyright   2001  University of Cambridge
4
5A family of similar counters, version with a full use of
6"compatibility ".
7
8From Charpentier and Chandy,
9Examples 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
14section\<open>A Family of Similar Counters: Version with Compatibility\<close>
15
16theory Counterc imports "../UNITY_Main" begin
17
18typedecl state
19
20consts
21  C :: "state=>int"
22  c :: "state=>nat=>int"
23
24primrec sum  :: "[nat,state]=>int" where
25  (* sum I s = sigma_{i<I}. c s i *)
26  "sum 0 s = 0"
27| "sum (Suc i) s = (c s) i + sum i s"
28
29primrec sumj :: "[nat, nat, state]=>int" where
30  "sumj 0 i s = 0"
31| "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
32  
33type_synonym command = "(state*state)set"
34
35definition a :: "nat=>command" where
36 "a i = {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
37 
38definition Component :: "nat => state program" where
39  "Component i = mk_total_program({s. C s = 0 & (c s) i = 0},
40                                  {a i},
41                                  \<Union>G \<in> preserves (%s. (c s) i). Acts G)"
42
43
44declare Component_def [THEN def_prg_Init, simp]
45declare Component_def [THEN def_prg_AllowedActs, simp]
46declare a_def [THEN def_act_simp, simp]
47
48(* Theorems about sum and sumj *)
49lemma sum_sumj_eq1: "I<i ==> sum I s = sumj I i s"
50  by (induct I) auto
51
52lemma sum_sumj_eq2: "i<I ==> sum I s  = c s i + sumj I i s"
53  by (induct I) (auto simp add: linorder_neq_iff sum_sumj_eq1)
54
55lemma sum_ext: "(\<And>i. i<I \<Longrightarrow> c s' i = c s i) ==> sum I s' = sum I s"
56  by (induct I) auto
57
58lemma sumj_ext: "(\<And>j. j<I ==> j\<noteq>i ==> c s' j =  c s j) ==> sumj I i s' = sumj I i s"
59  by (induct I) (auto intro!: sum_ext)
60
61lemma sum0: "(\<And>i. i<I ==> c s i = 0) ==> sum I s = 0"
62  by (induct I) auto
63
64
65(* Safety properties for Components *)
66
67lemma Component_ok_iff:
68     "(Component i ok G) =  
69      (G \<in> preserves (%s. c s i) & Component i \<in> Allowed G)"
70apply (auto simp add: ok_iff_Allowed Component_def [THEN def_total_prg_Allowed])
71done
72declare Component_ok_iff [iff]
73declare OK_iff_ok [iff]
74declare preserves_def [simp]
75
76
77lemma p2: "Component i \<in> stable {s. C s = (c s) i + k}"
78by (simp add: Component_def, safety)
79
80lemma p3:
81     "[| OK I Component; i\<in>I |]   
82      ==> Component i \<in> stable {s. \<forall>j\<in>I. j\<noteq>i --> c s j = c k j}"
83apply simp
84apply (unfold Component_def mk_total_program_def)
85apply (simp (no_asm_use) add: stable_def constrains_def)
86apply blast
87done
88
89
90lemma p2_p3_lemma1: 
91     "[| OK {i. i<I} Component; i<I |] ==>  
92      \<forall>k. Component i \<in> stable ({s. C s = c s i + sumj I i k} Int  
93                                {s. \<forall>j\<in>{i. i<I}. j\<noteq>i --> c s j = c k j})"
94by (blast intro: stable_Int [OF p2 p3])
95
96lemma p2_p3_lemma2:
97     "(\<forall>k. F \<in> stable ({s. C s = (c s) i + sumj I i k} Int  
98                        {s. \<forall>j\<in>{i. i<I}. j\<noteq>i --> c s j = c k j}))   
99      ==> (F \<in> stable {s. C s = c s i + sumj I i s})"
100apply (simp add: constrains_def stable_def)
101apply (force intro!: sumj_ext)
102done
103
104
105lemma p2_p3:
106     "[| OK {i. i<I} Component; i<I |]  
107      ==> Component i \<in> stable {s. C s = c s i + sumj I i s}"
108by (blast intro: p2_p3_lemma1 [THEN p2_p3_lemma2])
109
110
111(* Compositional correctness *)
112lemma safety: 
113     "[| 0<I; OK {i. i<I} Component |]   
114      ==> (\<Squnion>i\<in>{i. i<I}. (Component i)) \<in> invariant {s. C s = sum I s}"
115apply (simp (no_asm) add: invariant_def JN_stable sum_sumj_eq2)
116apply (auto intro!: sum0 p2_p3)
117done
118
119end
120