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