1(* Title: ZF/UNITY/Comp.thy 2 Author: Sidi O Ehmety, Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5From Chandy and Sanders, "Reasoning About Program Composition", 6Technical Report 2000-003, University of Florida, 2000. 7 8Revised by Sidi Ehmety on January 2001 9 10Added: a strong form of the order relation over component and localize 11 12Theory ported from HOL. 13 14*) 15 16section\<open>Composition\<close> 17 18theory Comp imports Union Increasing begin 19 20definition 21 component :: "[i,i]=>o" (infixl "component" 65) where 22 "F component H == (\<exists>G. F \<squnion> G = H)" 23 24definition 25 strict_component :: "[i,i]=>o" (infixl "strict'_component" 65) where 26 "F strict_component H == F component H & F\<noteq>H" 27 28definition 29 (* A stronger form of the component relation *) 30 component_of :: "[i,i]=>o" (infixl "component'_of" 65) where 31 "F component_of H == (\<exists>G. F ok G & F \<squnion> G = H)" 32 33definition 34 strict_component_of :: "[i,i]=>o" (infixl "strict'_component'_of" 65) where 35 "F strict_component_of H == F component_of H & F\<noteq>H" 36 37definition 38 (* Preserves a state function f, in particular a variable *) 39 preserves :: "(i=>i)=>i" where 40 "preserves(f) == {F:program. \<forall>z. F: stable({s:state. f(s) = z})}" 41 42definition 43 fun_pair :: "[i=>i, i =>i] =>(i=>i)" where 44 "fun_pair(f, g) == %x. <f(x), g(x)>" 45 46definition 47 localize :: "[i=>i, i] => i" where 48 "localize(f,F) == mk_program(Init(F), Acts(F), 49 AllowedActs(F) \<inter> (\<Union>G\<in>preserves(f). Acts(G)))" 50 51 52(*** component and strict_component relations ***) 53 54lemma componentI: 55 "H component F | H component G ==> H component (F \<squnion> G)" 56apply (unfold component_def, auto) 57apply (rule_tac x = "Ga \<squnion> G" in exI) 58apply (rule_tac [2] x = "G \<squnion> F" in exI) 59apply (auto simp add: Join_ac) 60done 61 62lemma component_eq_subset: 63 "G \<in> program ==> (F component G) \<longleftrightarrow> 64 (Init(G) \<subseteq> Init(F) & Acts(F) \<subseteq> Acts(G) & AllowedActs(G) \<subseteq> AllowedActs(F))" 65apply (unfold component_def, auto) 66apply (rule exI) 67apply (rule program_equalityI, auto) 68done 69 70lemma component_SKIP [simp]: "F \<in> program ==> SKIP component F" 71apply (unfold component_def) 72apply (rule_tac x = F in exI) 73apply (force intro: Join_SKIP_left) 74done 75 76lemma component_refl [simp]: "F \<in> program ==> F component F" 77apply (unfold component_def) 78apply (rule_tac x = F in exI) 79apply (force intro: Join_SKIP_right) 80done 81 82lemma SKIP_minimal: "F component SKIP ==> programify(F) = SKIP" 83apply (rule program_equalityI) 84apply (simp_all add: component_eq_subset, blast) 85done 86 87lemma component_Join1: "F component (F \<squnion> G)" 88by (unfold component_def, blast) 89 90lemma component_Join2: "G component (F \<squnion> G)" 91apply (unfold component_def) 92apply (simp (no_asm) add: Join_commute) 93apply blast 94done 95 96lemma Join_absorb1: "F component G ==> F \<squnion> G = G" 97by (auto simp add: component_def Join_left_absorb) 98 99lemma Join_absorb2: "G component F ==> F \<squnion> G = F" 100by (auto simp add: Join_ac component_def) 101 102lemma JOIN_component_iff: 103 "H \<in> program==>(JOIN(I,F) component H) \<longleftrightarrow> (\<forall>i \<in> I. F(i) component H)" 104apply (case_tac "I=0", force) 105apply (simp (no_asm_simp) add: component_eq_subset) 106apply auto 107apply blast 108apply (rename_tac "y") 109apply (drule_tac c = y and A = "AllowedActs (H)" in subsetD) 110apply (blast elim!: not_emptyE)+ 111done 112 113lemma component_JOIN: "i \<in> I ==> F(i) component (\<Squnion>i \<in> I. (F(i)))" 114apply (unfold component_def) 115apply (blast intro: JOIN_absorb) 116done 117 118lemma component_trans: "[| F component G; G component H |] ==> F component H" 119apply (unfold component_def) 120apply (blast intro: Join_assoc [symmetric]) 121done 122 123lemma component_antisym: 124 "[| F \<in> program; G \<in> program |] ==>(F component G & G component F) \<longrightarrow> F = G" 125apply (simp (no_asm_simp) add: component_eq_subset) 126apply clarify 127apply (rule program_equalityI, auto) 128done 129 130lemma Join_component_iff: 131 "H \<in> program ==> 132 ((F \<squnion> G) component H) \<longleftrightarrow> (F component H & G component H)" 133apply (simp (no_asm_simp) add: component_eq_subset) 134apply blast 135done 136 137lemma component_constrains: 138 "[| F component G; G \<in> A co B; F \<in> program |] ==> F \<in> A co B" 139apply (frule constrainsD2) 140apply (auto simp add: constrains_def component_eq_subset) 141done 142 143 144(*** preserves ***) 145 146lemma preserves_is_safety_prop [simp]: "safety_prop(preserves(f))" 147apply (unfold preserves_def safety_prop_def) 148apply (auto dest: ActsD simp add: stable_def constrains_def) 149apply (drule_tac c = act in subsetD, auto) 150done 151 152lemma preservesI [rule_format]: 153 "\<forall>z. F \<in> stable({s \<in> state. f(s) = z}) ==> F \<in> preserves(f)" 154apply (auto simp add: preserves_def) 155apply (blast dest: stableD2) 156done 157 158lemma preserves_imp_eq: 159 "[| F \<in> preserves(f); act \<in> Acts(F); <s,t> \<in> act |] ==> f(s) = f(t)" 160apply (unfold preserves_def stable_def constrains_def) 161apply (subgoal_tac "s \<in> state & t \<in> state") 162 prefer 2 apply (blast dest!: Acts_type [THEN subsetD], force) 163done 164 165lemma Join_preserves [iff]: 166"(F \<squnion> G \<in> preserves(v)) \<longleftrightarrow> 167 (programify(F) \<in> preserves(v) & programify(G) \<in> preserves(v))" 168by (auto simp add: preserves_def INT_iff) 169 170lemma JOIN_preserves [iff]: 171 "(JOIN(I,F): preserves(v)) \<longleftrightarrow> (\<forall>i \<in> I. programify(F(i)):preserves(v))" 172by (auto simp add: JOIN_stable preserves_def INT_iff) 173 174lemma SKIP_preserves [iff]: "SKIP \<in> preserves(v)" 175by (auto simp add: preserves_def INT_iff) 176 177lemma fun_pair_apply [simp]: "fun_pair(f,g,x) = <f(x), g(x)>" 178apply (unfold fun_pair_def) 179apply (simp (no_asm)) 180done 181 182lemma preserves_fun_pair: 183 "preserves(fun_pair(v,w)) = preserves(v) \<inter> preserves(w)" 184apply (rule equalityI) 185apply (auto simp add: preserves_def stable_def constrains_def, blast+) 186done 187 188lemma preserves_fun_pair_iff [iff]: 189 "F \<in> preserves(fun_pair(v, w)) \<longleftrightarrow> F \<in> preserves(v) \<inter> preserves(w)" 190by (simp add: preserves_fun_pair) 191 192lemma fun_pair_comp_distrib: 193 "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)" 194by (simp add: fun_pair_def metacomp_def) 195 196lemma comp_apply [simp]: "(f comp g)(x) = f(g(x))" 197by (simp add: metacomp_def) 198 199lemma preserves_type: "preserves(v)<=program" 200by (unfold preserves_def, auto) 201 202lemma preserves_into_program [TC]: "F \<in> preserves(f) ==> F \<in> program" 203by (blast intro: preserves_type [THEN subsetD]) 204 205lemma subset_preserves_comp: "preserves(f) \<subseteq> preserves(g comp f)" 206apply (auto simp add: preserves_def stable_def constrains_def) 207apply (drule_tac x = "f (xb)" in spec) 208apply (drule_tac x = act in bspec, auto) 209done 210 211lemma imp_preserves_comp: "F \<in> preserves(f) ==> F \<in> preserves(g comp f)" 212by (blast intro: subset_preserves_comp [THEN subsetD]) 213 214lemma preserves_subset_stable: "preserves(f) \<subseteq> stable({s \<in> state. P(f(s))})" 215apply (auto simp add: preserves_def stable_def constrains_def) 216apply (rename_tac s' s) 217apply (subgoal_tac "f (s) = f (s') ") 218apply (force+) 219done 220 221lemma preserves_imp_stable: 222 "F \<in> preserves(f) ==> F \<in> stable({s \<in> state. P(f(s))})" 223by (blast intro: preserves_subset_stable [THEN subsetD]) 224 225lemma preserves_imp_increasing: 226 "[| F \<in> preserves(f); \<forall>x \<in> state. f(x):A |] ==> F \<in> Increasing.increasing(A, r, f)" 227apply (unfold Increasing.increasing_def) 228apply (auto intro: preserves_into_program) 229apply (rule_tac P = "%x. <k, x>:r" in preserves_imp_stable, auto) 230done 231 232lemma preserves_id_subset_stable: 233 "st_set(A) ==> preserves(%x. x) \<subseteq> stable(A)" 234apply (unfold preserves_def stable_def constrains_def, auto) 235apply (drule_tac x = xb in spec) 236apply (drule_tac x = act in bspec) 237apply (auto dest: ActsD) 238done 239 240lemma preserves_id_imp_stable: 241 "[| F \<in> preserves(%x. x); st_set(A) |] ==> F \<in> stable(A)" 242by (blast intro: preserves_id_subset_stable [THEN subsetD]) 243 244(** Added by Sidi **) 245(** component_of **) 246 247(* component_of is stronger than component *) 248lemma component_of_imp_component: 249"F component_of H ==> F component H" 250apply (unfold component_def component_of_def, blast) 251done 252 253(* component_of satisfies many of component's properties *) 254lemma component_of_refl [simp]: "F \<in> program ==> F component_of F" 255apply (unfold component_of_def) 256apply (rule_tac x = SKIP in exI, auto) 257done 258 259lemma component_of_SKIP [simp]: "F \<in> program ==>SKIP component_of F" 260apply (unfold component_of_def, auto) 261apply (rule_tac x = F in exI, auto) 262done 263 264lemma component_of_trans: 265 "[| F component_of G; G component_of H |] ==> F component_of H" 266apply (unfold component_of_def) 267apply (blast intro: Join_assoc [symmetric]) 268done 269 270(** localize **) 271lemma localize_Init_eq [simp]: "Init(localize(v,F)) = Init(F)" 272by (unfold localize_def, simp) 273 274lemma localize_Acts_eq [simp]: "Acts(localize(v,F)) = Acts(F)" 275by (unfold localize_def, simp) 276 277lemma localize_AllowedActs_eq [simp]: 278 "AllowedActs(localize(v,F)) = AllowedActs(F) \<inter> (\<Union>G \<in> preserves(v). Acts(G))" 279apply (unfold localize_def) 280apply (rule equalityI) 281apply (auto dest: Acts_type [THEN subsetD]) 282done 283 284 285(** Theorems used in ClientImpl **) 286 287lemma stable_localTo_stable2: 288 "[| F \<in> stable({s \<in> state. P(f(s), g(s))}); G \<in> preserves(f); G \<in> preserves(g) |] 289 ==> F \<squnion> G \<in> stable({s \<in> state. P(f(s), g(s))})" 290apply (auto dest: ActsD preserves_into_program simp add: stable_def constrains_def) 291apply (case_tac "act \<in> Acts (F) ") 292apply auto 293apply (drule preserves_imp_eq) 294apply (drule_tac [3] preserves_imp_eq, auto) 295done 296 297lemma Increasing_preserves_Stable: 298 "[| F \<in> stable({s \<in> state. <f(s), g(s)>:r}); G \<in> preserves(f); 299 F \<squnion> G \<in> Increasing(A, r, g); 300 \<forall>x \<in> state. f(x):A & g(x):A |] 301 ==> F \<squnion> G \<in> Stable({s \<in> state. <f(s), g(s)>:r})" 302apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib) 303apply (simp_all add: constrains_type [THEN subsetD] preserves_type [THEN subsetD]) 304apply (blast intro: constrains_weaken) 305(*The G case remains*) 306apply (auto dest: ActsD simp add: preserves_def stable_def constrains_def ball_conj_distrib all_conj_distrib) 307(*We have a G-action, so delete assumptions about F-actions*) 308apply (erule_tac V = "\<forall>act \<in> Acts (F). P (act)" for P in thin_rl) 309apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . P (k,act)" for P in thin_rl) 310apply (subgoal_tac "f (x) = f (xa) ") 311apply (auto dest!: bspec) 312done 313 314 315(** Lemma used in AllocImpl **) 316 317lemma Constrains_UN_left: 318 "[| \<forall>x \<in> I. F \<in> A(x) Co B; F \<in> program |] ==> F:(\<Union>x \<in> I. A(x)) Co B" 319by (unfold Constrains_def constrains_def, auto) 320 321 322lemma stable_Join_Stable: 323 "[| F \<in> stable({s \<in> state. P(f(s), g(s))}); 324 \<forall>k \<in> A. F \<squnion> G \<in> Stable({s \<in> state. P(k, g(s))}); 325 G \<in> preserves(f); \<forall>s \<in> state. f(s):A|] 326 ==> F \<squnion> G \<in> Stable({s \<in> state. P(f(s), g(s))})" 327apply (unfold stable_def Stable_def preserves_def) 328apply (rule_tac A = "(\<Union>k \<in> A. {s \<in> state. f(s)=k} \<inter> {s \<in> state. P (f (s), g (s))})" in Constrains_weaken_L) 329prefer 2 apply blast 330apply (rule Constrains_UN_left, auto) 331apply (rule_tac A = "{s \<in> state. f(s)=k} \<inter> {s \<in> state. P (f (s), g (s))} \<inter> {s \<in> state. P (k, g (s))}" and A' = "({s \<in> state. f(s)=k} \<union> {s \<in> state. P (f (s), g (s))}) \<inter> {s \<in> state. P (k, g (s))}" in Constrains_weaken) 332 prefer 2 apply blast 333 prefer 2 apply blast 334apply (rule Constrains_Int) 335apply (rule constrains_imp_Constrains) 336apply (auto simp add: constrains_type [THEN subsetD]) 337apply (blast intro: constrains_weaken) 338apply (drule_tac x = k in spec) 339apply (blast intro: constrains_weaken) 340done 341 342end 343