src/HOL/UNITY/Comp/Counter.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 58310 91ea607a34d8 child 58889 5b7a9633cfa8 permissions -rw-r--r--
specialized specification: avoid trivial instances
1 (*  Title:      HOL/UNITY/Comp/Counter.thy
2     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
3     Copyright   2001  University of Cambridge
5 From Charpentier and Chandy,
6 Examples 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 *)
11 header{*A Family of Similar Counters: Original Version*}
13 theory Counter imports "../UNITY_Main" begin
15 (* Variables are names *)
16 datatype name = C | c nat
17 type_synonym state = "name=>int"
19 primrec 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"
24 primrec 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)"
28 type_synonym command = "(state*state)set"
30 definition a :: "nat=>command" where
31  "a i = {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}"
33 definition 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)"
40 declare Component_def [THEN def_prg_Init, simp]
41 declare a_def [THEN def_act_simp, simp]
43 (* Theorems about sum and sumj *)
44 lemma sum_upd_gt: "I<n ==> sum I (s(c n := x)) = sum I s"
45   by (induct I) auto
48 lemma 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])
51 lemma sum_upd_C: "sum I (s(C := x)) = sum I s"
52   by (induct I) auto
54 lemma 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])
57 lemma 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])
60 lemma sumj_sum_gt: "I<i ==> sumj I i s = sum I s"
61   by (induct I) auto
63 lemma sumj_sum_eq: "(sumj I I s = sum I s)"
64   by (induct I) (auto simp add: sumj_sum_gt)
66 lemma 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)
69 (* Correctness proofs for Components *)
70 (* p2 and p3 proofs *)
71 lemma p2: "Component i \<in> stable {s. s C = s (c i) + k}"
72 by (simp add: Component_def, safety)
74 lemma p3: "Component i \<in> stable {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v}"
75 by (simp add: Component_def, safety)
78 lemma 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})"
82 apply (simp add: Component_def mk_total_program_def)
83 apply (auto simp add: constrains_def stable_def sumj_upd_C sumj_upd_ci)
84 done
86 lemma 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})"
89 by (blast intro: stable_Int [OF p2 p3])
91 lemma p2_p3: "Component i \<in> stable {s.  s C = s (c i) + sumj I i s}"
92 by (auto intro!: p2_p3_lemma2 simp add: p2_p3_lemma1 [symmetric])
94 (* Compositional Proof *)
96 lemma sum_0': "(\<And>i. i < I ==> s (c i) = 0) ==> sum I s = 0"
97   by (induct I) auto
99 (* I cannot be empty *)
100 lemma safety:
101      "0<I ==> (\<Squnion>i \<in> {i. i<I}. Component i) \<in> invariant {s. s C = sum I s}"
102 apply (simp (no_asm) add: invariant_def JN_stable sum_sumj)
103 apply (force intro: p2_p3 sum_0')
104 done
106 end