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