src/HOL/UNITY/Lift_prog.thy
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 13836 6d0392fc6dc5
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
     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 = Rename:
    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 
   118 subsection{*The Operator @{term lift_set}*}
   119 
   120 lemma lift_set_empty [simp]: "lift_set i {} = {}"
   121 by (unfold lift_set_def, auto)
   122 
   123 lemma lift_set_iff: "(lift_map i x \<in> lift_set i A) = (x \<in> A)"
   124 apply (unfold lift_set_def)
   125 apply (rule inj_lift_map [THEN inj_image_mem_iff])
   126 done
   127 
   128 (*Do we really need both this one and its predecessor?*)
   129 lemma lift_set_iff2 [iff]:
   130      "((f,uu) \<in> lift_set i A) = ((f i, (delete_map i f, uu)) \<in> A)"
   131 by (simp add: lift_set_def mem_rename_set_iff drop_map_def)
   132 
   133 
   134 lemma lift_set_mono: "A \<subseteq> B ==> lift_set i A \<subseteq> lift_set i B"
   135 apply (unfold lift_set_def)
   136 apply (erule image_mono)
   137 done
   138 
   139 lemma lift_set_Un_distrib: "lift_set i (A \<union> B) = lift_set i A \<union> lift_set i B"
   140 by (simp add: lift_set_def image_Un)
   141 
   142 lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B"
   143 apply (unfold lift_set_def)
   144 apply (rule inj_lift_map [THEN image_set_diff])
   145 done
   146 
   147 
   148 subsection{*The Lattice Operations*}
   149 
   150 lemma bij_lift [iff]: "bij (lift i)"
   151 by (simp add: lift_def)
   152 
   153 lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
   154 by (simp add: lift_def)
   155 
   156 lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
   157 by (simp add: lift_def)
   158 
   159 lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
   160 by (simp add: lift_def)
   161 
   162 subsection{*Safety: constrains, stable, invariant*}
   163 
   164 lemma lift_constrains: 
   165      "(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)"
   166 by (simp add: lift_def lift_set_def rename_constrains)
   167 
   168 lemma lift_stable: 
   169      "(lift i F \<in> stable (lift_set i A)) = (F \<in> stable A)"
   170 by (simp add: lift_def lift_set_def rename_stable)
   171 
   172 lemma lift_invariant: 
   173      "(lift i F \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
   174 by (simp add: lift_def lift_set_def rename_invariant)
   175 
   176 lemma lift_Constrains: 
   177      "(lift i F \<in> (lift_set i A) Co (lift_set i B)) = (F \<in> A Co B)"
   178 by (simp add: lift_def lift_set_def rename_Constrains)
   179 
   180 lemma lift_Stable: 
   181      "(lift i F \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
   182 by (simp add: lift_def lift_set_def rename_Stable)
   183 
   184 lemma lift_Always: 
   185      "(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)"
   186 by (simp add: lift_def lift_set_def rename_Always)
   187 
   188 subsection{*Progress: transient, ensures*}
   189 
   190 lemma lift_transient: 
   191      "(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)"
   192 by (simp add: lift_def lift_set_def rename_transient)
   193 
   194 lemma lift_ensures: 
   195      "(lift i F \<in> (lift_set i A) ensures (lift_set i B)) =  
   196       (F \<in> A ensures B)"
   197 by (simp add: lift_def lift_set_def rename_ensures)
   198 
   199 lemma lift_leadsTo: 
   200      "(lift i F \<in> (lift_set i A) leadsTo (lift_set i B)) =  
   201       (F \<in> A leadsTo B)"
   202 by (simp add: lift_def lift_set_def rename_leadsTo)
   203 
   204 lemma lift_LeadsTo: 
   205      "(lift i F \<in> (lift_set i A) LeadsTo (lift_set i B)) =   
   206       (F \<in> A LeadsTo B)"
   207 by (simp add: lift_def lift_set_def rename_LeadsTo)
   208 
   209 
   210 (** guarantees **)
   211 
   212 lemma lift_lift_guarantees_eq: 
   213      "(lift i F \<in> (lift i ` X) guarantees (lift i ` Y)) =  
   214       (F \<in> X guarantees Y)"
   215 apply (unfold lift_def)
   216 apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric])
   217 apply (simp add: o_def)
   218 done
   219 
   220 lemma lift_guarantees_eq_lift_inv:
   221      "(lift i F \<in> X guarantees Y) =  
   222       (F \<in> (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
   223 by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def)
   224 
   225 
   226 (*To preserve snd means that the second component is there just to allow
   227   guarantees properties to be stated.  Converse fails, for lift i F can 
   228   change function components other than i*)
   229 lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd"
   230 apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
   231 apply (simp add: lift_def rename_preserves)
   232 apply (simp add: lift_map_def o_def split_def)
   233 done
   234 
   235 lemma delete_map_eqE':
   236      "(delete_map i g) = (delete_map i g') ==> \<exists>x. g = g'(i:=x)"
   237 apply (drule_tac f = "insert_map i (g i) " in arg_cong)
   238 apply (simp add: insert_map_delete_map_eq)
   239 apply (erule exI)
   240 done
   241 
   242 lemmas delete_map_eqE = delete_map_eqE' [THEN exE, elim!]
   243 
   244 lemma delete_map_neq_apply:
   245      "[| delete_map j g = delete_map j g';  i\<noteq>j |] ==> g i = g' i"
   246 by force
   247 
   248 (*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
   249 
   250 lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) <*> UNIV"
   251 by auto
   252 
   253 lemma vimage_sub_eq_lift_set [simp]:
   254      "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)"
   255 by auto
   256 
   257 lemma mem_lift_act_iff [iff]: 
   258      "((s,s') \<in> extend_act (%(x,u::unit). lift_map i x) act) =  
   259       ((drop_map i s, drop_map i s') \<in> act)"
   260 apply (unfold extend_act_def, auto)
   261 apply (rule bexI, auto)
   262 done
   263 
   264 lemma preserves_snd_lift_stable:
   265      "[| F \<in> preserves snd;  i\<noteq>j |]  
   266       ==> lift j F \<in> stable (lift_set i (A <*> UNIV))"
   267 apply (auto simp add: lift_def lift_set_def stable_def constrains_def 
   268                       rename_def extend_def mem_rename_set_iff)
   269 apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
   270 apply (drule_tac x = i in fun_cong, auto)
   271 done
   272 
   273 (*If i\<noteq>j then lift j F  does nothing to lift_set i, and the 
   274   premise ensures A \<subseteq> B.*)
   275 lemma constrains_imp_lift_constrains:
   276     "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);   
   277         F j \<in> preserves snd |]   
   278      ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
   279 apply (case_tac "i=j")
   280 apply (simp add: lift_def lift_set_def rename_constrains)
   281 apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
   282        assumption)
   283 apply (erule constrains_imp_subset [THEN lift_set_mono])
   284 done
   285 
   286 (*USELESS??*)
   287 lemma lift_map_image_Times:
   288      "lift_map i ` (A <*> UNIV) =  
   289       (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
   290 apply (auto intro!: bexI image_eqI simp add: lift_map_def)
   291 apply (rule split_conv [symmetric])
   292 done
   293 
   294 lemma lift_preserves_eq:
   295      "(lift i F \<in> preserves v) = (F \<in> preserves (v o lift_map i))"
   296 by (simp add: lift_def rename_preserves)
   297 
   298 (*A useful rewrite.  If o, sub have been rewritten out already then can also
   299   use it as   rewrite_rule [sub_def, o_def] lift_preserves_sub*)
   300 lemma lift_preserves_sub:
   301      "F \<in> preserves snd  
   302       ==> lift i F \<in> preserves (v o sub j o fst) =  
   303           (if i=j then F \<in> preserves (v o fst) else True)"
   304 apply (drule subset_preserves_o [THEN subsetD])
   305 apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
   306 apply (auto cong del: if_weak_cong 
   307             simp add: lift_map_def eq_commute split_def o_def)
   308 done
   309 
   310 
   311 subsection{*Lemmas to Handle Function Composition (o) More Consistently*}
   312 
   313 (*Lets us prove one version of a theorem and store others*)
   314 lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
   315 by (simp add: expand_fun_eq o_def)
   316 
   317 lemma o_equiv_apply: "f o g = h ==> \<forall>x. f(g x) = h x"
   318 by (simp add: expand_fun_eq o_def)
   319 
   320 lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
   321 apply (rule ext)
   322 apply (auto simp add: o_def lift_map_def sub_def)
   323 done
   324 
   325 lemma snd_o_lift_map: "snd o lift_map i = snd o snd"
   326 apply (rule ext)
   327 apply (auto simp add: o_def lift_map_def)
   328 done
   329 
   330 
   331 subsection{*More lemmas about extend and project*}
   332 
   333 text{*They could be moved to theory Extend or Project*}
   334 
   335 lemma extend_act_extend_act:
   336      "extend_act h' (extend_act h act) =  
   337       extend_act (%(x,(y,y')). h'(h(x,y),y')) act"
   338 apply (auto elim!: rev_bexI simp add: extend_act_def, blast) 
   339 done
   340 
   341 lemma project_act_project_act:
   342      "project_act h (project_act h' act) =  
   343       project_act (%(x,(y,y')). h'(h(x,y),y')) act"
   344 by (auto elim!: rev_bexI simp add: project_act_def)
   345 
   346 lemma project_act_extend_act:
   347      "project_act h (extend_act h' act) =  
   348         {(x,x'). \<exists>s s' y y' z. (s,s') \<in> act &  
   349                  h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}"
   350 by (simp add: extend_act_def project_act_def, blast)
   351 
   352 
   353 subsection{*OK and "lift"*}
   354 
   355 lemma act_in_UNION_preserves_fst:
   356      "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
   357 apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I)
   358 apply (auto simp add: preserves_def stable_def constrains_def)
   359 done
   360 
   361 lemma UNION_OK_lift_I:
   362      "[| \<forall>i \<in> I. F i \<in> preserves snd;   
   363          \<forall>i \<in> I. UNION (preserves fst) Acts \<subseteq> AllowedActs (F i) |]  
   364       ==> OK I (%i. lift i (F i))"
   365 apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
   366 apply (simp add: Extend.AllowedActs_extend project_act_extend_act)
   367 apply (rename_tac "act")
   368 apply (subgoal_tac
   369        "{(x, x'). \<exists>s f u s' f' u'. 
   370                     ((s, f, u), s', f', u') \<in> act & 
   371                     lift_map j x = lift_map i (s, f, u) & 
   372                     lift_map j x' = lift_map i (s', f', u') } 
   373                 \<subseteq> { (x,x') . fst x = fst x'}")
   374 apply (blast intro: act_in_UNION_preserves_fst, clarify)
   375 apply (drule_tac x = j in fun_cong)+
   376 apply (drule_tac x = i in bspec, assumption)
   377 apply (frule preserves_imp_eq, auto)
   378 done
   379 
   380 lemma OK_lift_I:
   381      "[| \<forall>i \<in> I. F i \<in> preserves snd;   
   382          \<forall>i \<in> I. preserves fst \<subseteq> Allowed (F i) |]  
   383       ==> OK I (%i. lift i (F i))"
   384 by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
   385 
   386 lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"
   387 by (simp add: lift_def Allowed_rename)
   388 
   389 lemma lift_image_preserves:
   390      "lift i ` preserves v = preserves (v o drop_map i)"
   391 by (simp add: rename_image_preserves lift_def inv_lift_map_eq)
   392 
   393 end