(* Title: HOL/UNITY/Comp/Counterc.thy Author: Sidi O Ehmety, Cambridge University Computer Laboratory Copyright 2001 University of Cambridge
A family of similar counters, version with a full use of "compatibility ".
From Charpentier and Chandy, Examples of Program Composition Illustrating the Use of Universal Properties In J. Rolim (editor), Parallel and Distributed Processing, Spriner LNCS 1586 (1999), pages 1215-1227.
*)
section\<open>A Family of Similar Counters: Version with Compatibility\<close>
theory Counterc imports"../UNITY_Main"begin
typedecl state
consts
C :: "state=>int"
c :: "state=>nat=>int"
primrec sum :: "[nat,state]=>int"where (* sum I s = sigma_{i<I}. c s i *) "sum 0 s = 0"
| "sum (Suc i) s = (c s) i + sum i s"
primrec sumj :: "[nat, nat, state]=>int"where "sumj 0 i s = 0"
| "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
type_synonym command = "(state*state)set"
definition a :: "nat=>command"where "a i = {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
definition Component :: "nat => state program"where "Component i = mk_total_program({s. C s = 0 & (c s) i = 0},
{a i}, \<Union>G \<in> preserves (%s. (c s) i). Acts G)"
(* Theorems about sum and sumj *) lemma sum_sumj_eq1: "I sum I s = sumj I i s" by (induct I) auto
lemma sum_sumj_eq2: "i sum I s = c s i + sumj I i s" by (induct I) (auto simp add: linorder_neq_iff sum_sumj_eq1)
lemma sum_ext: "(\i. i c s' i = c s i) ==> sum I s' = sum I s" by (induct I) auto
lemma sumj_ext: "(\j. j j\i ==> c s' j = c s j) ==> sumj I i s' = sumj I i s" by (induct I) (auto intro!: sum_ext)
lemma sum0: "(\i. i c s i = 0) ==> sum I s = 0" by (induct I) auto
(* Safety properties for Components *)
lemma Component_ok_iff: "(Component i ok G) =
(G \<in> preserves (%s. c s i) & Component i \<in> Allowed G)" apply (auto simp add: ok_iff_Allowed Component_def [THEN def_total_prg_Allowed]) done declare Component_ok_iff [iff] declare OK_iff_ok [iff] declare preserves_def [simp]
lemma p2: "Component i \ stable {s. C s = (c s) i + k}" by (simp add: Component_def, safety)
lemma p3: "[| OK I Component; i\I |]
==> Component i \<in> stable {s. \<forall>j\<in>I. j\<noteq>i --> c s j = c k j}" apply simp apply (unfold Component_def mk_total_program_def) apply (simp (no_asm_use) add: stable_def constrains_def) apply blast done
lemma p2_p3_lemma1: "[| OK {i. i \<forall>k. Component i \<in> stable ({s. C s = c s i + sumj I i k} Int
{s. \<forall>j\<in>{i. i<I}. j\<noteq>i --> c s j = c k j})" by (blast intro: stable_Int [OF p2 p3])
lemma p2_p3_lemma2: "(\k. F \ stable ({s. C s = (c s) i + sumj I i k} Int
{s. \<forall>j\<in>{i. i<I}. j\<noteq>i --> c s j = c k j}))
==> (F \<in> stable {s. C s = c s i + sumj I i s})" apply (simp add: constrains_def stable_def) apply (force intro!: sumj_ext) done
lemma p2_p3: "[| OK {i. i
==> Component i \<in> stable {s. C s = c s i + sumj I i s}" by (blast intro: p2_p3_lemma1 [THEN p2_p3_lemma2])
(* Compositional correctness *) lemma safety: "[| 0
==> (\<Squnion>i\<in>{i. i<I}. (Component i)) \<in> invariant {s. C s = sum I s}" apply (simp (no_asm) add: invariant_def JN_stable sum_sumj_eq2) apply (auto intro!: sum0 p2_p3) done
end
[ zur Elbe Produktseite wechseln0.11Quellennavigators
Analyse erneut starten
]
