1(* Title: HOL/UNITY/Rename.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 2000 University of Cambridge 4*) 5 6section\<open>Renaming of State Sets\<close> 7 8theory Rename imports Extend begin 9 10definition rename :: "['a => 'b, 'a program] => 'b program" where 11 "rename h == extend (%(x,u::unit). h x)" 12 13declare image_inv_f_f [simp] image_f_inv_f [simp] 14 15declare Extend.intro [simp,intro] 16 17lemma good_map_bij [simp,intro]: "bij h ==> good_map (%(x,u). h x)" 18apply (rule good_mapI) 19apply (unfold bij_def inj_on_def surj_def, auto) 20done 21 22lemma fst_o_inv_eq_inv: "bij h ==> fst (inv (%(x,u). h x) s) = inv h s" 23apply (unfold bij_def split_def, clarify) 24apply (subgoal_tac "surj (%p. h (fst p))") 25 prefer 2 apply (simp add: surj_def) 26apply (erule injD) 27apply (simp (no_asm_simp) add: surj_f_inv_f) 28apply (erule surj_f_inv_f) 29done 30 31lemma mem_rename_set_iff: "bij h ==> z \<in> h`A = (inv h z \<in> A)" 32by (force simp add: bij_is_inj bij_is_surj [THEN surj_f_inv_f]) 33 34 35lemma extend_set_eq_image [simp]: "extend_set (%(x,u). h x) A = h`A" 36by (force simp add: extend_set_def) 37 38lemma Init_rename [simp]: "Init (rename h F) = h`(Init F)" 39by (simp add: rename_def) 40 41 42subsection\<open>inverse properties\<close> 43 44lemma extend_set_inv: 45 "bij h 46 ==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)" 47apply (unfold bij_def) 48apply (rule ext) 49apply (force simp add: extend_set_def project_set_def surj_f_inv_f) 50done 51 52(** for "rename" (programs) **) 53 54lemma bij_extend_act_eq_project_act: "bij h 55 ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)" 56apply (rule ext) 57apply (force simp add: extend_act_def project_act_def bij_def surj_f_inv_f) 58done 59 60lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))" 61apply (rule bijI) 62apply (rule Extend.inj_extend_act) 63apply simp 64apply (simp add: bij_extend_act_eq_project_act) 65apply (rule surjI) 66apply (rule Extend.extend_act_inverse) 67apply (blast intro: bij_imp_bij_inv) 68done 69 70lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))" 71apply (frule bij_imp_bij_inv [THEN bij_extend_act]) 72apply (simp add: bij_extend_act_eq_project_act bij_imp_bij_inv inv_inv_eq) 73done 74 75lemma bij_inv_project_act_eq: "bij h ==> inv (project_act (%(x,u::'c). inv h x)) = 76 project_act (%(x,u::'c). h x)" 77apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric]) 78apply (rule surj_imp_inv_eq) 79apply (blast intro!: bij_extend_act bij_is_surj) 80apply (simp (no_asm_simp) add: Extend.extend_act_inverse) 81done 82 83lemma extend_inv: "bij h 84 ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV" 85apply (frule bij_imp_bij_inv) 86apply (rule ext) 87apply (rule program_equalityI) 88 apply (simp (no_asm_simp) add: extend_set_inv) 89 apply (simp add: Extend.project_act_Id Extend.Acts_extend 90 insert_Id_image_Acts bij_extend_act_eq_project_act inv_inv_eq) 91apply (simp add: Extend.AllowedActs_extend Extend.AllowedActs_project 92 bij_project_act bij_vimage_eq_inv_image bij_inv_project_act_eq) 93done 94 95lemma rename_inv_rename [simp]: "bij h ==> rename (inv h) (rename h F) = F" 96by (simp add: rename_def extend_inv Extend.extend_inverse) 97 98lemma rename_rename_inv [simp]: "bij h ==> rename h (rename (inv h) F) = F" 99apply (frule bij_imp_bij_inv) 100apply (erule inv_inv_eq [THEN subst], erule rename_inv_rename) 101done 102 103lemma rename_inv_eq: "bij h ==> rename (inv h) = inv (rename h)" 104by (rule inv_equality [symmetric], auto) 105 106(** (rename h) is bijective <=> h is bijective **) 107 108lemma bij_extend: "bij h ==> bij (extend (%(x,u::'c). h x))" 109apply (rule bijI) 110apply (blast intro: Extend.inj_extend) 111apply (rule_tac f = "extend (% (x,u) . inv h x)" in surjI) 112apply (subst (1 2) inv_inv_eq [of h, symmetric], assumption+) 113apply (simp add: bij_imp_bij_inv extend_inv [of "inv h"]) 114apply (simp add: inv_inv_eq) 115apply (rule Extend.extend_inverse) 116apply (simp add: bij_imp_bij_inv) 117done 118 119lemma bij_project: "bij h ==> bij (project (%(x,u::'c). h x) UNIV)" 120apply (subst extend_inv [symmetric]) 121apply (auto simp add: bij_imp_bij_inv bij_extend) 122done 123 124lemma inv_project_eq: 125 "bij h 126 ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)" 127apply (rule inj_imp_inv_eq) 128apply (erule bij_project [THEN bij_is_inj]) 129apply (simp (no_asm_simp) add: Extend.extend_inverse) 130done 131 132lemma Allowed_rename [simp]: 133 "bij h ==> Allowed (rename h F) = rename h ` Allowed F" 134apply (simp (no_asm_simp) add: rename_def Extend.Allowed_extend) 135apply (subst bij_vimage_eq_inv_image) 136apply (rule bij_project, blast) 137apply (simp (no_asm_simp) add: inv_project_eq) 138done 139 140lemma bij_rename: "bij h ==> bij (rename h)" 141apply (simp (no_asm_simp) add: rename_def bij_extend) 142done 143lemmas surj_rename = bij_rename [THEN bij_is_surj] 144 145lemma inj_rename_imp_inj: "inj (rename h) ==> inj h" 146apply (unfold inj_on_def, auto) 147apply (drule_tac x = "mk_program ({x}, {}, {})" in spec) 148apply (drule_tac x = "mk_program ({y}, {}, {})" in spec) 149apply (auto simp add: program_equality_iff rename_def extend_def) 150done 151 152lemma surj_rename_imp_surj: "surj (rename h) ==> surj h" 153apply (unfold surj_def, auto) 154apply (drule_tac x = "mk_program ({y}, {}, {})" in spec) 155apply (auto simp add: program_equality_iff rename_def extend_def) 156done 157 158lemma bij_rename_imp_bij: "bij (rename h) ==> bij h" 159apply (unfold bij_def) 160apply (simp (no_asm_simp) add: inj_rename_imp_inj surj_rename_imp_surj) 161done 162 163lemma bij_rename_iff [simp]: "bij (rename h) = bij h" 164by (blast intro: bij_rename bij_rename_imp_bij) 165 166 167subsection\<open>the lattice operations\<close> 168 169lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP" 170by (simp add: rename_def Extend.extend_SKIP) 171 172lemma rename_Join [simp]: 173 "bij h ==> rename h (F \<squnion> G) = rename h F \<squnion> rename h G" 174by (simp add: rename_def Extend.extend_Join) 175 176lemma rename_JN [simp]: 177 "bij h ==> rename h (JOIN I F) = (\<Squnion>i \<in> I. rename h (F i))" 178by (simp add: rename_def Extend.extend_JN) 179 180 181subsection\<open>Strong Safety: co, stable\<close> 182 183lemma rename_constrains: 184 "bij h ==> (rename h F \<in> (h`A) co (h`B)) = (F \<in> A co B)" 185apply (unfold rename_def) 186apply (subst extend_set_eq_image [symmetric])+ 187apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_constrains]) 188done 189 190lemma rename_stable: 191 "bij h ==> (rename h F \<in> stable (h`A)) = (F \<in> stable A)" 192apply (simp add: stable_def rename_constrains) 193done 194 195lemma rename_invariant: 196 "bij h ==> (rename h F \<in> invariant (h`A)) = (F \<in> invariant A)" 197apply (simp add: invariant_def rename_stable bij_is_inj [THEN inj_image_subset_iff]) 198done 199 200lemma rename_increasing: 201 "bij h ==> (rename h F \<in> increasing func) = (F \<in> increasing (func o h))" 202apply (simp add: increasing_def rename_stable [symmetric] bij_image_Collect_eq bij_is_surj [THEN surj_f_inv_f]) 203done 204 205 206subsection\<open>Weak Safety: Co, Stable\<close> 207 208lemma reachable_rename_eq: 209 "bij h ==> reachable (rename h F) = h ` (reachable F)" 210apply (simp add: rename_def Extend.reachable_extend_eq) 211done 212 213lemma rename_Constrains: 214 "bij h ==> (rename h F \<in> (h`A) Co (h`B)) = (F \<in> A Co B)" 215by (simp add: Constrains_def reachable_rename_eq rename_constrains 216 bij_is_inj image_Int [symmetric]) 217 218lemma rename_Stable: 219 "bij h ==> (rename h F \<in> Stable (h`A)) = (F \<in> Stable A)" 220by (simp add: Stable_def rename_Constrains) 221 222lemma rename_Always: "bij h ==> (rename h F \<in> Always (h`A)) = (F \<in> Always A)" 223by (simp add: Always_def rename_Stable bij_is_inj [THEN inj_image_subset_iff]) 224 225lemma rename_Increasing: 226 "bij h ==> (rename h F \<in> Increasing func) = (F \<in> Increasing (func o h))" 227by (simp add: Increasing_def rename_Stable [symmetric] bij_image_Collect_eq 228 bij_is_surj [THEN surj_f_inv_f]) 229 230 231subsection\<open>Progress: transient, ensures\<close> 232 233lemma rename_transient: 234 "bij h ==> (rename h F \<in> transient (h`A)) = (F \<in> transient A)" 235apply (unfold rename_def) 236apply (subst extend_set_eq_image [symmetric]) 237apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_transient]) 238done 239 240lemma rename_ensures: 241 "bij h ==> (rename h F \<in> (h`A) ensures (h`B)) = (F \<in> A ensures B)" 242apply (unfold rename_def) 243apply (subst extend_set_eq_image [symmetric])+ 244apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_ensures]) 245done 246 247lemma rename_leadsTo: 248 "bij h ==> (rename h F \<in> (h`A) leadsTo (h`B)) = (F \<in> A leadsTo B)" 249apply (unfold rename_def) 250apply (subst extend_set_eq_image [symmetric])+ 251apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_leadsTo]) 252done 253 254lemma rename_LeadsTo: 255 "bij h ==> (rename h F \<in> (h`A) LeadsTo (h`B)) = (F \<in> A LeadsTo B)" 256apply (unfold rename_def) 257apply (subst extend_set_eq_image [symmetric])+ 258apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_LeadsTo]) 259done 260 261lemma rename_rename_guarantees_eq: 262 "bij h ==> (rename h F \<in> (rename h ` X) guarantees 263 (rename h ` Y)) = 264 (F \<in> X guarantees Y)" 265apply (unfold rename_def) 266apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_guarantees_eq [symmetric]], assumption) 267apply (simp (no_asm_simp) add: fst_o_inv_eq_inv o_def) 268done 269 270lemma rename_guarantees_eq_rename_inv: 271 "bij h ==> (rename h F \<in> X guarantees Y) = 272 (F \<in> (rename (inv h) ` X) guarantees 273 (rename (inv h) ` Y))" 274apply (subst rename_rename_guarantees_eq [symmetric], assumption) 275apply (simp add: o_def bij_is_surj [THEN surj_f_inv_f] image_comp) 276done 277 278lemma rename_preserves: 279 "bij h ==> (rename h G \<in> preserves v) = (G \<in> preserves (v o h))" 280apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_preserves [symmetric]], assumption) 281apply (simp add: o_def fst_o_inv_eq_inv rename_def bij_is_surj [THEN surj_f_inv_f]) 282done 283 284lemma ok_rename_iff [simp]: "bij h ==> (rename h F ok rename h G) = (F ok G)" 285by (simp add: Extend.ok_extend_iff rename_def) 286 287lemma OK_rename_iff [simp]: "bij h ==> OK I (%i. rename h (F i)) = (OK I F)" 288by (simp add: Extend.OK_extend_iff rename_def) 289 290 291subsection\<open>"image" versions of the rules, for lifting "guarantees" properties\<close> 292 293(*All the proofs are similar. Better would have been to prove one 294 meta-theorem, but how can we handle the polymorphism? E.g. in 295 rename_constrains the two appearances of "co" have different types!*) 296lemmas bij_eq_rename = surj_rename [THEN surj_f_inv_f, symmetric] 297 298lemma rename_image_constrains: 299 "bij h ==> rename h ` (A co B) = (h ` A) co (h`B)" 300apply auto 301 defer 1 302 apply (rename_tac F) 303 apply (subgoal_tac "\<exists>G. F = rename h G") 304 apply (auto intro!: bij_eq_rename simp add: rename_constrains) 305done 306 307lemma rename_image_stable: "bij h ==> rename h ` stable A = stable (h ` A)" 308apply auto 309 defer 1 310 apply (rename_tac F) 311 apply (subgoal_tac "\<exists>G. F = rename h G") 312 apply (auto intro!: bij_eq_rename simp add: rename_stable) 313done 314 315lemma rename_image_increasing: 316 "bij h ==> rename h ` increasing func = increasing (func o inv h)" 317apply auto 318 defer 1 319 apply (rename_tac F) 320 apply (subgoal_tac "\<exists>G. F = rename h G") 321 apply (auto intro!: bij_eq_rename simp add: rename_increasing o_def bij_is_inj) 322done 323 324lemma rename_image_invariant: 325 "bij h ==> rename h ` invariant A = invariant (h ` A)" 326apply auto 327 defer 1 328 apply (rename_tac F) 329 apply (subgoal_tac "\<exists>G. F = rename h G") 330 apply (auto intro!: bij_eq_rename simp add: rename_invariant) 331done 332 333lemma rename_image_Constrains: 334 "bij h ==> rename h ` (A Co B) = (h ` A) Co (h`B)" 335apply auto 336 defer 1 337 apply (rename_tac F) 338 apply (subgoal_tac "\<exists>G. F = rename h G") 339 apply (auto intro!: bij_eq_rename simp add: rename_Constrains) 340done 341 342lemma rename_image_preserves: 343 "bij h ==> rename h ` preserves v = preserves (v o inv h)" 344by (simp add: o_def rename_image_stable preserves_def bij_image_INT 345 bij_image_Collect_eq) 346 347lemma rename_image_Stable: 348 "bij h ==> rename h ` Stable A = Stable (h ` A)" 349apply auto 350 defer 1 351 apply (rename_tac F) 352 apply (subgoal_tac "\<exists>G. F = rename h G") 353 apply (auto intro!: bij_eq_rename simp add: rename_Stable) 354done 355 356lemma rename_image_Increasing: 357 "bij h ==> rename h ` Increasing func = Increasing (func o inv h)" 358apply auto 359 defer 1 360 apply (rename_tac F) 361 apply (subgoal_tac "\<exists>G. F = rename h G") 362 apply (auto intro!: bij_eq_rename simp add: rename_Increasing o_def bij_is_inj) 363done 364 365lemma rename_image_Always: "bij h ==> rename h ` Always A = Always (h ` A)" 366apply auto 367 defer 1 368 apply (rename_tac F) 369 apply (subgoal_tac "\<exists>G. F = rename h G") 370 apply (auto intro!: bij_eq_rename simp add: rename_Always) 371done 372 373lemma rename_image_leadsTo: 374 "bij h ==> rename h ` (A leadsTo B) = (h ` A) leadsTo (h`B)" 375apply auto 376 defer 1 377 apply (rename_tac F) 378 apply (subgoal_tac "\<exists>G. F = rename h G") 379 apply (auto intro!: bij_eq_rename simp add: rename_leadsTo) 380done 381 382lemma rename_image_LeadsTo: 383 "bij h ==> rename h ` (A LeadsTo B) = (h ` A) LeadsTo (h`B)" 384apply auto 385 defer 1 386 apply (rename_tac F) 387 apply (subgoal_tac "\<exists>G. F = rename h G") 388 apply (auto intro!: bij_eq_rename simp add: rename_LeadsTo) 389done 390 391end 392