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