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