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