1(* Title: HOL/UNITY/Lift_prog.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1999 University of Cambridge 4 5lift_prog, etc: replication of components and arrays of processes. 6*) 7 8section\<open>Replication of Components\<close> 9 10theory Lift_prog imports Rename begin 11 12definition insert_map :: "[nat, 'b, nat=>'b] => (nat=>'b)" where 13 "insert_map i z f k == if k<i then f k 14 else if k=i then z 15 else f(k - 1)" 16 17definition delete_map :: "[nat, nat=>'b] => (nat=>'b)" where 18 "delete_map i g k == if k<i then g k else g (Suc k)" 19 20definition lift_map :: "[nat, 'b * ((nat=>'b) * 'c)] => (nat=>'b) * 'c" where 21 "lift_map i == %(s,(f,uu)). (insert_map i s f, uu)" 22 23definition drop_map :: "[nat, (nat=>'b) * 'c] => 'b * ((nat=>'b) * 'c)" where 24 "drop_map i == %(g, uu). (g i, (delete_map i g, uu))" 25 26definition lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set" where 27 "lift_set i A == lift_map i ` A" 28 29definition lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program" where 30 "lift i == rename (lift_map i)" 31 32 (*simplifies the expression of specifications*) 33definition sub :: "['a, 'a=>'b] => 'b" where 34 "sub == %i f. f i" 35 36 37declare insert_map_def [simp] delete_map_def [simp] 38 39lemma insert_map_inverse: "delete_map i (insert_map i x f) = f" 40by (rule ext, simp) 41 42lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)" 43apply (rule ext) 44apply (auto split: nat_diff_split) 45done 46 47subsection\<open>Injectiveness proof\<close> 48 49lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y" 50by (drule_tac x = i in fun_cong, simp) 51 52lemma insert_map_inject2: "(insert_map i x f) = (insert_map i y g) ==> f=g" 53apply (drule_tac f = "delete_map i" in arg_cong) 54apply (simp add: insert_map_inverse) 55done 56 57lemma insert_map_inject': 58 "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g" 59by (blast dest: insert_map_inject1 insert_map_inject2) 60 61lemmas insert_map_inject = insert_map_inject' [THEN conjE, elim!] 62 63(*The general case: we don't assume i=i'*) 64lemma lift_map_eq_iff [iff]: 65 "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu'))) 66 = (uu = uu' & insert_map i s f = insert_map i' s' f')" 67by (unfold lift_map_def, auto) 68 69(*The !!s allows the automatic splitting of the bound variable*) 70lemma drop_map_lift_map_eq [simp]: "!!s. drop_map i (lift_map i s) = s" 71apply (unfold lift_map_def drop_map_def) 72apply (force intro: insert_map_inverse) 73done 74 75lemma inj_lift_map: "inj (lift_map i)" 76apply (unfold lift_map_def) 77apply (rule inj_onI, auto) 78done 79 80subsection\<open>Surjectiveness proof\<close> 81 82lemma lift_map_drop_map_eq [simp]: "!!s. lift_map i (drop_map i s) = s" 83apply (unfold lift_map_def drop_map_def) 84apply (force simp add: insert_map_delete_map_eq) 85done 86 87lemma drop_map_inject [dest!]: "(drop_map i s) = (drop_map i s') ==> s=s'" 88by (drule_tac f = "lift_map i" in arg_cong, simp) 89 90lemma surj_lift_map: "surj (lift_map i)" 91apply (rule surjI) 92apply (rule lift_map_drop_map_eq) 93done 94 95lemma bij_lift_map [iff]: "bij (lift_map i)" 96by (simp add: bij_def inj_lift_map surj_lift_map) 97 98lemma inv_lift_map_eq [simp]: "inv (lift_map i) = drop_map i" 99by (rule inv_equality, auto) 100 101lemma inv_drop_map_eq [simp]: "inv (drop_map i) = lift_map i" 102by (rule inv_equality, auto) 103 104lemma bij_drop_map [iff]: "bij (drop_map i)" 105by (simp del: inv_lift_map_eq add: inv_lift_map_eq [symmetric] bij_imp_bij_inv) 106 107(*sub's main property!*) 108lemma sub_apply [simp]: "sub i f = f i" 109by (simp add: sub_def) 110 111lemma all_total_lift: "all_total F ==> all_total (lift i F)" 112by (simp add: lift_def rename_def Extend.all_total_extend) 113 114lemma insert_map_upd_same: "(insert_map i t f)(i := s) = insert_map i s f" 115by (rule ext, auto) 116 117lemma insert_map_upd: 118 "(insert_map j t f)(i := s) = 119 (if i=j then insert_map i s f 120 else if i<j then insert_map j t (f(i:=s)) 121 else insert_map j t (f(i - Suc 0 := s)))" 122apply (rule ext) 123apply (simp split: nat_diff_split) 124 txt\<open>This simplification is VERY slow\<close> 125done 126 127lemma insert_map_eq_diff: 128 "[| insert_map i s f = insert_map j t g; i\<noteq>j |] 129 ==> \<exists>g'. insert_map i s' f = insert_map j t g'" 130apply (subst insert_map_upd_same [symmetric]) 131apply (erule ssubst) 132apply (simp only: insert_map_upd if_False split: if_split, blast) 133done 134 135lemma lift_map_eq_diff: 136 "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i\<noteq>j |] 137 ==> \<exists>g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))" 138apply (unfold lift_map_def, auto) 139apply (blast dest: insert_map_eq_diff) 140done 141 142 143subsection\<open>The Operator \<^term>\<open>lift_set\<close>\<close> 144 145lemma lift_set_empty [simp]: "lift_set i {} = {}" 146by (unfold lift_set_def, auto) 147 148lemma lift_set_iff: "(lift_map i x \<in> lift_set i A) = (x \<in> A)" 149apply (unfold lift_set_def) 150apply (rule inj_lift_map [THEN inj_image_mem_iff]) 151done 152 153(*Do we really need both this one and its predecessor?*) 154lemma lift_set_iff2 [iff]: 155 "((f,uu) \<in> lift_set i A) = ((f i, (delete_map i f, uu)) \<in> A)" 156by (simp add: lift_set_def mem_rename_set_iff drop_map_def) 157 158 159lemma lift_set_mono: "A \<subseteq> B ==> lift_set i A \<subseteq> lift_set i B" 160apply (unfold lift_set_def) 161apply (erule image_mono) 162done 163 164lemma lift_set_Un_distrib: "lift_set i (A \<union> B) = lift_set i A \<union> lift_set i B" 165by (simp add: lift_set_def image_Un) 166 167lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B" 168apply (unfold lift_set_def) 169apply (rule inj_lift_map [THEN image_set_diff]) 170done 171 172 173subsection\<open>The Lattice Operations\<close> 174 175lemma bij_lift [iff]: "bij (lift i)" 176by (simp add: lift_def) 177 178lemma lift_SKIP [simp]: "lift i SKIP = SKIP" 179by (simp add: lift_def) 180 181lemma lift_Join [simp]: "lift i (F \<squnion> G) = lift i F \<squnion> lift i G" 182by (simp add: lift_def) 183 184lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))" 185by (simp add: lift_def) 186 187subsection\<open>Safety: constrains, stable, invariant\<close> 188 189lemma lift_constrains: 190 "(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)" 191by (simp add: lift_def lift_set_def rename_constrains) 192 193lemma lift_stable: 194 "(lift i F \<in> stable (lift_set i A)) = (F \<in> stable A)" 195by (simp add: lift_def lift_set_def rename_stable) 196 197lemma lift_invariant: 198 "(lift i F \<in> invariant (lift_set i A)) = (F \<in> invariant A)" 199by (simp add: lift_def lift_set_def rename_invariant) 200 201lemma lift_Constrains: 202 "(lift i F \<in> (lift_set i A) Co (lift_set i B)) = (F \<in> A Co B)" 203by (simp add: lift_def lift_set_def rename_Constrains) 204 205lemma lift_Stable: 206 "(lift i F \<in> Stable (lift_set i A)) = (F \<in> Stable A)" 207by (simp add: lift_def lift_set_def rename_Stable) 208 209lemma lift_Always: 210 "(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)" 211by (simp add: lift_def lift_set_def rename_Always) 212 213subsection\<open>Progress: transient, ensures\<close> 214 215lemma lift_transient: 216 "(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)" 217by (simp add: lift_def lift_set_def rename_transient) 218 219lemma lift_ensures: 220 "(lift i F \<in> (lift_set i A) ensures (lift_set i B)) = 221 (F \<in> A ensures B)" 222by (simp add: lift_def lift_set_def rename_ensures) 223 224lemma lift_leadsTo: 225 "(lift i F \<in> (lift_set i A) leadsTo (lift_set i B)) = 226 (F \<in> A leadsTo B)" 227by (simp add: lift_def lift_set_def rename_leadsTo) 228 229lemma lift_LeadsTo: 230 "(lift i F \<in> (lift_set i A) LeadsTo (lift_set i B)) = 231 (F \<in> A LeadsTo B)" 232by (simp add: lift_def lift_set_def rename_LeadsTo) 233 234 235(** guarantees **) 236 237lemma lift_lift_guarantees_eq: 238 "(lift i F \<in> (lift i ` X) guarantees (lift i ` Y)) = 239 (F \<in> X guarantees Y)" 240apply (unfold lift_def) 241apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric]) 242apply (simp add: o_def) 243done 244 245lemma lift_guarantees_eq_lift_inv: 246 "(lift i F \<in> X guarantees Y) = 247 (F \<in> (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))" 248by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def) 249 250 251(*To preserve snd means that the second component is there just to allow 252 guarantees properties to be stated. Converse fails, for lift i F can 253 change function components other than i*) 254lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd" 255apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD]) 256apply (simp add: lift_def rename_preserves) 257apply (simp add: lift_map_def o_def split_def) 258done 259 260lemma delete_map_eqE': 261 "(delete_map i g) = (delete_map i g') ==> \<exists>x. g = g'(i:=x)" 262apply (drule_tac f = "insert_map i (g i) " in arg_cong) 263apply (simp add: insert_map_delete_map_eq) 264apply (erule exI) 265done 266 267lemmas delete_map_eqE = delete_map_eqE' [THEN exE, elim!] 268 269lemma delete_map_neq_apply: 270 "[| delete_map j g = delete_map j g'; i\<noteq>j |] ==> g i = g' i" 271by force 272 273(*A set of the form (A \<times> UNIV) ignores the second (dummy) state component*) 274 275lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) \<times> UNIV" 276by auto 277 278lemma vimage_sub_eq_lift_set [simp]: 279 "(sub i -`A) \<times> UNIV = lift_set i (A \<times> UNIV)" 280by auto 281 282lemma mem_lift_act_iff [iff]: 283 "((s,s') \<in> extend_act (%(x,u::unit). lift_map i x) act) = 284 ((drop_map i s, drop_map i s') \<in> act)" 285apply (unfold extend_act_def, auto) 286apply (rule bexI, auto) 287done 288 289lemma preserves_snd_lift_stable: 290 "[| F \<in> preserves snd; i\<noteq>j |] 291 ==> lift j F \<in> stable (lift_set i (A \<times> UNIV))" 292apply (auto simp add: lift_def lift_set_def stable_def constrains_def 293 rename_def extend_def mem_rename_set_iff) 294apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def) 295apply (drule_tac x = i in fun_cong, auto) 296done 297 298(*If i\<noteq>j then lift j F does nothing to lift_set i, and the 299 premise ensures A \<subseteq> B.*) 300lemma constrains_imp_lift_constrains: 301 "[| F i \<in> (A \<times> UNIV) co (B \<times> UNIV); 302 F j \<in> preserves snd |] 303 ==> lift j (F j) \<in> (lift_set i (A \<times> UNIV)) co (lift_set i (B \<times> UNIV))" 304apply (cases "i=j") 305apply (simp add: lift_def lift_set_def rename_constrains) 306apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R], 307 assumption) 308apply (erule constrains_imp_subset [THEN lift_set_mono]) 309done 310 311(*USELESS??*) 312lemma lift_map_image_Times: 313 "lift_map i ` (A \<times> UNIV) = 314 (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) \<times> UNIV" 315apply (auto intro!: bexI image_eqI simp add: lift_map_def) 316apply (rule split_conv [symmetric]) 317done 318 319lemma lift_preserves_eq: 320 "(lift i F \<in> preserves v) = (F \<in> preserves (v o lift_map i))" 321by (simp add: lift_def rename_preserves) 322 323(*A useful rewrite. If o, sub have been rewritten out already then can also 324 use it as rewrite_rule [sub_def, o_def] lift_preserves_sub*) 325lemma lift_preserves_sub: 326 "F \<in> preserves snd 327 ==> lift i F \<in> preserves (v o sub j o fst) = 328 (if i=j then F \<in> preserves (v o fst) else True)" 329apply (drule subset_preserves_o [THEN subsetD]) 330apply (simp add: lift_preserves_eq o_def) 331apply (auto cong del: if_weak_cong 332 simp add: lift_map_def eq_commute split_def o_def) 333done 334 335 336subsection\<open>Lemmas to Handle Function Composition (o) More Consistently\<close> 337 338(*Lets us prove one version of a theorem and store others*) 339lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h" 340by (simp add: fun_eq_iff o_def) 341 342lemma o_equiv_apply: "f o g = h ==> \<forall>x. f(g x) = h x" 343by (simp add: fun_eq_iff o_def) 344 345lemma fst_o_lift_map: "sub i o fst o lift_map i = fst" 346apply (rule ext) 347apply (auto simp add: o_def lift_map_def sub_def) 348done 349 350lemma snd_o_lift_map: "snd o lift_map i = snd o snd" 351apply (rule ext) 352apply (auto simp add: o_def lift_map_def) 353done 354 355 356subsection\<open>More lemmas about extend and project\<close> 357 358text\<open>They could be moved to theory Extend or Project\<close> 359 360lemma extend_act_extend_act: 361 "extend_act h' (extend_act h act) = 362 extend_act (%(x,(y,y')). h'(h(x,y),y')) act" 363apply (auto elim!: rev_bexI simp add: extend_act_def, blast) 364done 365 366lemma project_act_project_act: 367 "project_act h (project_act h' act) = 368 project_act (%(x,(y,y')). h'(h(x,y),y')) act" 369by (auto elim!: rev_bexI simp add: project_act_def) 370 371lemma project_act_extend_act: 372 "project_act h (extend_act h' act) = 373 {(x,x'). \<exists>s s' y y' z. (s,s') \<in> act & 374 h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}" 375by (simp add: extend_act_def project_act_def, blast) 376 377 378subsection\<open>OK and "lift"\<close> 379 380lemma act_in_UNION_preserves_fst: 381 "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> \<Union>(Acts ` (preserves fst))" 382apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I) 383apply (auto simp add: preserves_def stable_def constrains_def) 384done 385 386lemma UNION_OK_lift_I: 387 "[| \<forall>i \<in> I. F i \<in> preserves snd; 388 \<forall>i \<in> I. \<Union>(Acts ` (preserves fst)) \<subseteq> AllowedActs (F i) |] 389 ==> OK I (%i. lift i (F i))" 390apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend) 391apply (simp add: Extend.AllowedActs_extend project_act_extend_act) 392apply (rename_tac "act") 393apply (subgoal_tac 394 "{(x, x'). \<exists>s f u s' f' u'. 395 ((s, f, u), s', f', u') \<in> act & 396 lift_map j x = lift_map i (s, f, u) & 397 lift_map j x' = lift_map i (s', f', u') } 398 \<subseteq> { (x,x') . fst x = fst x'}") 399apply (blast intro: act_in_UNION_preserves_fst, clarify) 400apply (drule_tac x = j in fun_cong)+ 401apply (drule_tac x = i in bspec, assumption) 402apply (frule preserves_imp_eq, auto) 403done 404 405lemma OK_lift_I: 406 "[| \<forall>i \<in> I. F i \<in> preserves snd; 407 \<forall>i \<in> I. preserves fst \<subseteq> Allowed (F i) |] 408 ==> OK I (%i. lift i (F i))" 409by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I) 410 411lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)" 412by (simp add: lift_def) 413 414lemma lift_image_preserves: 415 "lift i ` preserves v = preserves (v o drop_map i)" 416by (simp add: rename_image_preserves lift_def) 417 418end 419