1(* Title: HOL/UNITY/PPROD.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5Abstraction over replicated components (PLam) 6General products of programs (Pi operation) 7 8Some dead wood here! 9*) 10 11theory PPROD imports Lift_prog begin 12 13definition PLam :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program] 14 => ((nat=>'b) * 'c) program" where 15 "PLam I F == \<Squnion>i \<in> I. lift i (F i)" 16 17syntax 18 "_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set" ("(3plam _:_./ _)" 10) 19translations 20 "plam x : A. B" == "CONST PLam A (%x. B)" 21 22 23(*** Basic properties ***) 24 25lemma Init_PLam [simp]: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))" 26by (simp add: PLam_def lift_def lift_set_def) 27 28lemma PLam_empty [simp]: "PLam {} F = SKIP" 29by (simp add: PLam_def) 30 31lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP" 32by (simp add: PLam_def JN_constant) 33 34lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) \<squnion> (PLam I F)" 35by (unfold PLam_def, auto) 36 37lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)" 38by (simp add: PLam_def JN_component_iff) 39 40lemma component_PLam: "i \<in> I ==> lift i (F i) \<le> (PLam I F)" 41apply (unfold PLam_def) 42(*blast_tac doesn't use HO unification*) 43apply (fast intro: component_JN) 44done 45 46 47(** Safety & Progress: but are they used anywhere? **) 48 49lemma PLam_constrains: 50 "[| i \<in> I; \<forall>j. F j \<in> preserves snd |] 51 ==> (PLam I F \<in> (lift_set i (A \<times> UNIV)) co 52 (lift_set i (B \<times> UNIV))) = 53 (F i \<in> (A \<times> UNIV) co (B \<times> UNIV))" 54apply (simp add: PLam_def JN_constrains) 55apply (subst insert_Diff [symmetric], assumption) 56apply (simp add: lift_constrains) 57apply (blast intro: constrains_imp_lift_constrains) 58done 59 60lemma PLam_stable: 61 "[| i \<in> I; \<forall>j. F j \<in> preserves snd |] 62 ==> (PLam I F \<in> stable (lift_set i (A \<times> UNIV))) = 63 (F i \<in> stable (A \<times> UNIV))" 64by (simp add: stable_def PLam_constrains) 65 66lemma PLam_transient: 67 "i \<in> I ==> 68 PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)" 69by (simp add: JN_transient PLam_def) 70 71text\<open>This holds because the \<^term>\<open>F j\<close> cannot change \<^term>\<open>lift_set i\<close>\<close> 72lemma PLam_ensures: 73 "[| i \<in> I; F i \<in> (A \<times> UNIV) ensures (B \<times> UNIV); 74 \<forall>j. F j \<in> preserves snd |] 75 ==> PLam I F \<in> lift_set i (A \<times> UNIV) ensures lift_set i (B \<times> UNIV)" 76apply (simp add: ensures_def PLam_constrains PLam_transient 77 lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] 78 Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric]) 79apply (rule rev_bexI, assumption) 80apply (simp add: lift_transient) 81done 82 83lemma PLam_leadsTo_Basis: 84 "[| i \<in> I; 85 F i \<in> ((A \<times> UNIV) - (B \<times> UNIV)) co 86 ((A \<times> UNIV) \<union> (B \<times> UNIV)); 87 F i \<in> transient ((A \<times> UNIV) - (B \<times> UNIV)); 88 \<forall>j. F j \<in> preserves snd |] 89 ==> PLam I F \<in> lift_set i (A \<times> UNIV) leadsTo lift_set i (B \<times> UNIV)" 90by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI) 91 92 93 94(** invariant **) 95 96lemma invariant_imp_PLam_invariant: 97 "[| F i \<in> invariant (A \<times> UNIV); i \<in> I; 98 \<forall>j. F j \<in> preserves snd |] 99 ==> PLam I F \<in> invariant (lift_set i (A \<times> UNIV))" 100by (auto simp add: PLam_stable invariant_def) 101 102 103lemma PLam_preserves_fst [simp]: 104 "\<forall>j. F j \<in> preserves snd 105 ==> (PLam I F \<in> preserves (v o sub j o fst)) = 106 (if j \<in> I then F j \<in> preserves (v o fst) else True)" 107by (simp add: PLam_def lift_preserves_sub) 108 109lemma PLam_preserves_snd [simp,intro]: 110 "\<forall>j. F j \<in> preserves snd ==> PLam I F \<in> preserves snd" 111by (simp add: PLam_def lift_preserves_snd_I) 112 113 114 115(*** guarantees properties ***) 116 117text\<open>This rule looks unsatisfactory because it refers to \<^term>\<open>lift\<close>. 118 One must use 119 \<open>lift_guarantees_eq_lift_inv\<close> to rewrite the first subgoal and 120 something like \<open>lift_preserves_sub\<close> to rewrite the third. However 121 there's no obvious alternative for the third premise.\<close> 122lemma guarantees_PLam_I: 123 "[| lift i (F i) \<in> X guarantees Y; i \<in> I; 124 OK I (\<lambda>i. lift i (F i)) |] 125 ==> (PLam I F) \<in> X guarantees Y" 126apply (unfold PLam_def) 127apply (simp add: guarantees_JN_I) 128done 129 130lemma Allowed_PLam [simp]: 131 "Allowed (PLam I F) = (\<Inter>i \<in> I. lift i ` Allowed(F i))" 132by (simp add: PLam_def) 133 134 135lemma PLam_preserves [simp]: 136 "(PLam I F) \<in> preserves v = (\<forall>i \<in> I. F i \<in> preserves (v o lift_map i))" 137by (simp add: PLam_def lift_def rename_preserves) 138 139 140(**UNUSED 141 (*The f0 premise ensures that the product is well-defined.*) 142 lemma PLam_invariant_imp_invariant: 143 "[| PLam I F \<in> invariant (lift_set i A); i \<in> I; 144 f0: Init (PLam I F) |] ==> F i \<in> invariant A" 145 apply (auto simp add: invariant_def) 146 apply (drule_tac c = "f0 (i:=x) " in subsetD) 147 apply auto 148 done 149 150 lemma PLam_invariant: 151 "[| i \<in> I; f0: Init (PLam I F) |] 152 ==> (PLam I F \<in> invariant (lift_set i A)) = (F i \<in> invariant A)" 153 apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant) 154 done 155 156 (*The f0 premise isn't needed if F is a constant program because then 157 we get an initial state by replicating that of F*) 158 lemma reachable_PLam: 159 "i \<in> I 160 ==> ((plam x \<in> I. F) \<in> invariant (lift_set i A)) = (F \<in> invariant A)" 161 apply (auto simp add: invariant_def) 162 done 163**) 164 165 166(**UNUSED 167 (** Reachability **) 168 169 Goal "[| f \<in> reachable (PLam I F); i \<in> I |] ==> f i \<in> reachable (F i)" 170 apply (erule reachable.induct) 171 apply (auto intro: reachable.intrs) 172 done 173 174 (*Result to justify a re-organization of this file*) 175 lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))" 176 by auto 177 178 lemma reachable_PLam_subset1: 179 "reachable (PLam I F) \<subseteq> (\<Inter>i \<in> I. lift_set i (reachable (F i)))" 180 apply (force dest!: reachable_PLam) 181 done 182 183 (*simplify using reachable_lift??*) 184 lemma reachable_lift_Join_PLam [rule_format]: 185 "[| i \<notin> I; A \<in> reachable (F i) |] 186 ==> \<forall>f. f \<in> reachable (PLam I F) 187 --> f(i:=A) \<in> reachable (lift i (F i) \<squnion> PLam I F)" 188 apply (erule reachable.induct) 189 apply (ALLGOALS Clarify_tac) 190 apply (erule reachable.induct) 191 (*Init, Init case*) 192 apply (force intro: reachable.intrs) 193 (*Init of F, action of PLam F case*) 194 apply (rule_tac act = act in reachable.Acts) 195 apply force 196 apply assumption 197 apply (force intro: ext) 198 (*induction over the 2nd "reachable" assumption*) 199 apply (erule_tac xa = f in reachable.induct) 200 (*Init of PLam F, action of F case*) 201 apply (rule_tac act = "lift_act i act" in reachable.Acts) 202 apply force 203 apply (force intro: reachable.Init) 204 apply (force intro: ext simp add: lift_act_def) 205 (*last case: an action of PLam I F*) 206 apply (rule_tac act = acta in reachable.Acts) 207 apply force 208 apply assumption 209 apply (force intro: ext) 210 done 211 212 213 (*The index set must be finite: otherwise infinitely many copies of F can 214 perform actions, and PLam can never catch up in finite time.*) 215 lemma reachable_PLam_subset2: 216 "finite I 217 ==> (\<Inter>i \<in> I. lift_set i (reachable (F i))) \<subseteq> reachable (PLam I F)" 218 apply (erule finite_induct) 219 apply (simp (no_asm)) 220 apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert) 221 done 222 223 lemma reachable_PLam_eq: 224 "finite I ==> 225 reachable (PLam I F) = (\<Inter>i \<in> I. lift_set i (reachable (F i)))" 226 apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2])) 227 done 228 229 230 (** Co **) 231 232 lemma Constrains_imp_PLam_Constrains: 233 "[| F i \<in> A Co B; i \<in> I; finite I |] 234 ==> PLam I F \<in> (lift_set i A) Co (lift_set i B)" 235 apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq) 236 apply (auto simp add: constrains_def PLam_def) 237 apply (REPEAT (blast intro: reachable.intrs)) 238 done 239 240 241 242 lemma PLam_Constrains: 243 "[| i \<in> I; finite I; f0: Init (PLam I F) |] 244 ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) = 245 (F i \<in> A Co B)" 246 apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains) 247 done 248 249 lemma PLam_Stable: 250 "[| i \<in> I; finite I; f0: Init (PLam I F) |] 251 ==> (PLam I F \<in> Stable (lift_set i A)) = (F i \<in> Stable A)" 252 apply (simp del: Init_PLam add: Stable_def PLam_Constrains) 253 done 254 255 256 (** const_PLam (no dependence on i) doesn't require the f0 premise **) 257 258 lemma const_PLam_Constrains: 259 "[| i \<in> I; finite I |] 260 ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) = 261 (F \<in> A Co B)" 262 apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains) 263 done 264 265 lemma const_PLam_Stable: 266 "[| i \<in> I; finite I |] 267 ==> ((plam x \<in> I. F) \<in> Stable (lift_set i A)) = (F \<in> Stable A)" 268 apply (simp add: Stable_def const_PLam_Constrains) 269 done 270 271 lemma const_PLam_Increasing: 272 "[| i \<in> I; finite I |] 273 ==> ((plam x \<in> I. F) \<in> Increasing (f o sub i)) = (F \<in> Increasing f)" 274 apply (unfold Increasing_def) 275 apply (subgoal_tac "\<forall>z. {s. z \<subseteq> (f o sub i) s} = lift_set i {s. z \<subseteq> f s}") 276 apply (asm_simp_tac (simpset () add: lift_set_sub) 2) 277 apply (simp add: finite_lessThan const_PLam_Stable) 278 done 279**) 280 281 282end 283