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