1(* Title: HOL/UNITY/Comp.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Author: Sidi Ehmety 4 5Composition. 6 7From Chandy and Sanders, "Reasoning About Program Composition", 8Technical Report 2000-003, University of Florida, 2000. 9*) 10 11section\<open>Composition: Basic Primitives\<close> 12 13theory Comp 14imports Union 15begin 16 17instantiation program :: (type) ord 18begin 19 20definition component_def: "F \<le> H \<longleftrightarrow> (\<exists>G. F\<squnion>G = H)" 21 22definition strict_component_def: "F < (H::'a program) \<longleftrightarrow> (F \<le> H & F \<noteq> H)" 23 24instance .. 25 26end 27 28definition component_of :: "'a program =>'a program=> bool" (infixl "component'_of" 50) 29 where "F component_of H == \<exists>G. F ok G & F\<squnion>G = H" 30 31definition strict_component_of :: "'a program\<Rightarrow>'a program=> bool" (infixl "strict'_component'_of" 50) 32 where "F strict_component_of H == F component_of H & F\<noteq>H" 33 34definition preserves :: "('a=>'b) => 'a program set" 35 where "preserves v == \<Inter>z. stable {s. v s = z}" 36 37definition localize :: "('a=>'b) => 'a program => 'a program" where 38 "localize v F == mk_program(Init F, Acts F, 39 AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G))" 40 41definition funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c" 42 where "funPair f g == %x. (f x, g x)" 43 44 45subsection\<open>The component relation\<close> 46lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F\<squnion>G)" 47apply (unfold component_def, auto) 48apply (rule_tac x = "G\<squnion>Ga" in exI) 49apply (rule_tac [2] x = "G\<squnion>F" in exI) 50apply (auto simp add: Join_ac) 51done 52 53lemma component_eq_subset: 54 "(F \<le> G) = 55 (Init G \<subseteq> Init F & Acts F \<subseteq> Acts G & AllowedActs G \<subseteq> AllowedActs F)" 56apply (unfold component_def) 57apply (force intro!: exI program_equalityI) 58done 59 60lemma component_SKIP [iff]: "SKIP \<le> F" 61apply (unfold component_def) 62apply (force intro: Join_SKIP_left) 63done 64 65lemma component_refl [iff]: "F \<le> (F :: 'a program)" 66apply (unfold component_def) 67apply (blast intro: Join_SKIP_right) 68done 69 70lemma SKIP_minimal: "F \<le> SKIP ==> F = SKIP" 71by (auto intro!: program_equalityI simp add: component_eq_subset) 72 73lemma component_Join1: "F \<le> (F\<squnion>G)" 74by (unfold component_def, blast) 75 76lemma component_Join2: "G \<le> (F\<squnion>G)" 77apply (unfold component_def) 78apply (simp add: Join_commute, blast) 79done 80 81lemma Join_absorb1: "F \<le> G ==> F\<squnion>G = G" 82by (auto simp add: component_def Join_left_absorb) 83 84lemma Join_absorb2: "G \<le> F ==> F\<squnion>G = F" 85by (auto simp add: Join_ac component_def) 86 87lemma JN_component_iff: "((JOIN I F) \<le> H) = (\<forall>i \<in> I. F i \<le> H)" 88by (simp add: component_eq_subset, blast) 89 90lemma component_JN: "i \<in> I ==> (F i) \<le> (\<Squnion>i \<in> I. (F i))" 91apply (unfold component_def) 92apply (blast intro: JN_absorb) 93done 94 95lemma component_trans: "[| F \<le> G; G \<le> H |] ==> F \<le> (H :: 'a program)" 96apply (unfold component_def) 97apply (blast intro: Join_assoc [symmetric]) 98done 99 100lemma component_antisym: "[| F \<le> G; G \<le> F |] ==> F = (G :: 'a program)" 101apply (simp (no_asm_use) add: component_eq_subset) 102apply (blast intro!: program_equalityI) 103done 104 105lemma Join_component_iff: "((F\<squnion>G) \<le> H) = (F \<le> H & G \<le> H)" 106by (simp add: component_eq_subset, blast) 107 108lemma component_constrains: "[| F \<le> G; G \<in> A co B |] ==> F \<in> A co B" 109by (auto simp add: constrains_def component_eq_subset) 110 111lemma component_stable: "[| F \<le> G; G \<in> stable A |] ==> F \<in> stable A" 112by (auto simp add: stable_def component_constrains) 113 114(*Used in Guar.thy to show that programs are partially ordered*) 115lemmas program_less_le = strict_component_def 116 117 118subsection\<open>The preserves property\<close> 119 120lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v" 121by (unfold preserves_def, blast) 122 123lemma preserves_imp_eq: 124 "[| F \<in> preserves v; act \<in> Acts F; (s,s') \<in> act |] ==> v s = v s'" 125by (unfold preserves_def stable_def constrains_def, force) 126 127lemma Join_preserves [iff]: 128 "(F\<squnion>G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)" 129by (unfold preserves_def, auto) 130 131lemma JN_preserves [iff]: 132 "(JOIN I F \<in> preserves v) = (\<forall>i \<in> I. F i \<in> preserves v)" 133by (simp add: JN_stable preserves_def, blast) 134 135lemma SKIP_preserves [iff]: "SKIP \<in> preserves v" 136by (auto simp add: preserves_def) 137 138lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)" 139by (simp add: funPair_def) 140 141lemma preserves_funPair: "preserves (funPair v w) = preserves v \<inter> preserves w" 142by (auto simp add: preserves_def stable_def constrains_def, blast) 143 144(* (F \<in> preserves (funPair v w)) = (F \<in> preserves v \<inter> preserves w) *) 145declare preserves_funPair [THEN eqset_imp_iff, iff] 146 147 148lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)" 149by (simp add: funPair_def o_def) 150 151lemma fst_o_funPair [simp]: "fst o (funPair f g) = f" 152by (simp add: funPair_def o_def) 153 154lemma snd_o_funPair [simp]: "snd o (funPair f g) = g" 155by (simp add: funPair_def o_def) 156 157lemma subset_preserves_o: "preserves v \<subseteq> preserves (w o v)" 158by (force simp add: preserves_def stable_def constrains_def) 159 160lemma preserves_subset_stable: "preserves v \<subseteq> stable {s. P (v s)}" 161apply (auto simp add: preserves_def stable_def constrains_def) 162apply (rename_tac s' s) 163apply (subgoal_tac "v s = v s'") 164apply (force+) 165done 166 167lemma preserves_subset_increasing: "preserves v \<subseteq> increasing v" 168by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def) 169 170lemma preserves_id_subset_stable: "preserves id \<subseteq> stable A" 171by (force simp add: preserves_def stable_def constrains_def) 172 173 174(** For use with def_UNION_ok_iff **) 175 176lemma safety_prop_preserves [iff]: "safety_prop (preserves v)" 177by (auto intro: safety_prop_INTER1 simp add: preserves_def) 178 179 180(** Some lemmas used only in Client.thy **) 181 182lemma stable_localTo_stable2: 183 "[| F \<in> stable {s. P (v s) (w s)}; 184 G \<in> preserves v; G \<in> preserves w |] 185 ==> F\<squnion>G \<in> stable {s. P (v s) (w s)}" 186apply simp 187apply (subgoal_tac "G \<in> preserves (funPair v w) ") 188 prefer 2 apply simp 189apply (drule_tac P1 = "case_prod Q" for Q in preserves_subset_stable [THEN subsetD], 190 auto) 191done 192 193lemma Increasing_preserves_Stable: 194 "[| F \<in> stable {s. v s \<le> w s}; G \<in> preserves v; F\<squnion>G \<in> Increasing w |] 195 ==> F\<squnion>G \<in> Stable {s. v s \<le> w s}" 196apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib) 197apply (blast intro: constrains_weaken) 198(*The G case remains*) 199apply (auto simp add: preserves_def stable_def constrains_def) 200(*We have a G-action, so delete assumptions about F-actions*) 201apply (erule_tac V = "\<forall>act \<in> Acts F. P act" for P in thin_rl) 202apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. P z act" for P in thin_rl) 203apply (subgoal_tac "v x = v xa") 204 apply auto 205apply (erule order_trans, blast) 206done 207 208(** component_of **) 209 210(* component_of is stronger than \<le> *) 211lemma component_of_imp_component: "F component_of H ==> F \<le> H" 212by (unfold component_def component_of_def, blast) 213 214 215(* component_of satisfies many of the same properties as \<le> *) 216lemma component_of_refl [simp]: "F component_of F" 217apply (unfold component_of_def) 218apply (rule_tac x = SKIP in exI, auto) 219done 220 221lemma component_of_SKIP [simp]: "SKIP component_of F" 222by (unfold component_of_def, auto) 223 224lemma component_of_trans: 225 "[| F component_of G; G component_of H |] ==> F component_of H" 226apply (unfold component_of_def) 227apply (blast intro: Join_assoc [symmetric]) 228done 229 230lemmas strict_component_of_eq = strict_component_of_def 231 232(** localize **) 233lemma localize_Init_eq [simp]: "Init (localize v F) = Init F" 234by (simp add: localize_def) 235 236lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F" 237by (simp add: localize_def) 238 239lemma localize_AllowedActs_eq [simp]: 240 "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)" 241by (unfold localize_def, auto) 242 243end 244