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