1 (* Title: HOL/UNITY/Lift_prog.thy
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3 Copyright 1999 University of Cambridge
5 lift_prog, etc: replication of components and arrays of processes.
8 header{*Replication of Components*}
10 theory Lift_prog imports Rename begin
12 definition insert_map :: "[nat, 'b, nat=>'b] => (nat=>'b)" where
13 "insert_map i z f k == if k<i then f k
17 definition delete_map :: "[nat, nat=>'b] => (nat=>'b)" where
18 "delete_map i g k == if k<i then g k else g (Suc k)"
20 definition lift_map :: "[nat, 'b * ((nat=>'b) * 'c)] => (nat=>'b) * 'c" where
21 "lift_map i == %(s,(f,uu)). (insert_map i s f, uu)"
23 definition drop_map :: "[nat, (nat=>'b) * 'c] => 'b * ((nat=>'b) * 'c)" where
24 "drop_map i == %(g, uu). (g i, (delete_map i g, uu))"
26 definition lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set" where
27 "lift_set i A == lift_map i ` A"
29 definition lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program" where
30 "lift i == rename (lift_map i)"
32 (*simplifies the expression of specifications*)
33 definition sub :: "['a, 'a=>'b] => 'b" where
37 declare insert_map_def [simp] delete_map_def [simp]
39 lemma insert_map_inverse: "delete_map i (insert_map i x f) = f"
42 lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)"
44 apply (auto split add: nat_diff_split)
47 subsection{*Injectiveness proof*}
49 lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
50 by (drule_tac x = i in fun_cong, simp)
52 lemma insert_map_inject2: "(insert_map i x f) = (insert_map i y g) ==> f=g"
53 apply (drule_tac f = "delete_map i" in arg_cong)
54 apply (simp add: insert_map_inverse)
57 lemma insert_map_inject':
58 "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g"
59 by (blast dest: insert_map_inject1 insert_map_inject2)
61 lemmas insert_map_inject = insert_map_inject' [THEN conjE, elim!]
63 (*The general case: we don't assume i=i'*)
64 lemma lift_map_eq_iff [iff]:
65 "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu')))
66 = (uu = uu' & insert_map i s f = insert_map i' s' f')"
67 by (unfold lift_map_def, auto)
69 (*The !!s allows the automatic splitting of the bound variable*)
70 lemma drop_map_lift_map_eq [simp]: "!!s. drop_map i (lift_map i s) = s"
71 apply (unfold lift_map_def drop_map_def)
72 apply (force intro: insert_map_inverse)
75 lemma inj_lift_map: "inj (lift_map i)"
76 apply (unfold lift_map_def)
77 apply (rule inj_onI, auto)
80 subsection{*Surjectiveness proof*}
82 lemma lift_map_drop_map_eq [simp]: "!!s. lift_map i (drop_map i s) = s"
83 apply (unfold lift_map_def drop_map_def)
84 apply (force simp add: insert_map_delete_map_eq)
87 lemma drop_map_inject [dest!]: "(drop_map i s) = (drop_map i s') ==> s=s'"
88 by (drule_tac f = "lift_map i" in arg_cong, simp)
90 lemma surj_lift_map: "surj (lift_map i)"
92 apply (rule lift_map_drop_map_eq)
95 lemma bij_lift_map [iff]: "bij (lift_map i)"
96 by (simp add: bij_def inj_lift_map surj_lift_map)
98 lemma inv_lift_map_eq [simp]: "inv (lift_map i) = drop_map i"
99 by (rule inv_equality, auto)
101 lemma inv_drop_map_eq [simp]: "inv (drop_map i) = lift_map i"
102 by (rule inv_equality, auto)
104 lemma bij_drop_map [iff]: "bij (drop_map i)"
105 by (simp del: inv_lift_map_eq add: inv_lift_map_eq [symmetric] bij_imp_bij_inv)
107 (*sub's main property!*)
108 lemma sub_apply [simp]: "sub i f = f i"
109 by (simp add: sub_def)
111 lemma all_total_lift: "all_total F ==> all_total (lift i F)"
112 by (simp add: lift_def rename_def Extend.all_total_extend)
114 lemma insert_map_upd_same: "(insert_map i t f)(i := s) = insert_map i s f"
117 lemma insert_map_upd:
118 "(insert_map j t f)(i := s) =
119 (if i=j then insert_map i s f
120 else if i<j then insert_map j t (f(i:=s))
121 else insert_map j t (f(i - Suc 0 := s)))"
123 apply (simp split add: nat_diff_split)
124 txt{*This simplification is VERY slow*}
127 lemma insert_map_eq_diff:
128 "[| insert_map i s f = insert_map j t g; i\<noteq>j |]
129 ==> \<exists>g'. insert_map i s' f = insert_map j t g'"
130 apply (subst insert_map_upd_same [symmetric])
132 apply (simp only: insert_map_upd if_False split: split_if, blast)
135 lemma lift_map_eq_diff:
136 "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i\<noteq>j |]
137 ==> \<exists>g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
138 apply (unfold lift_map_def, auto)
139 apply (blast dest: insert_map_eq_diff)
143 subsection{*The Operator @{term lift_set}*}
145 lemma lift_set_empty [simp]: "lift_set i {} = {}"
146 by (unfold lift_set_def, auto)
148 lemma lift_set_iff: "(lift_map i x \<in> lift_set i A) = (x \<in> A)"
149 apply (unfold lift_set_def)
150 apply (rule inj_lift_map [THEN inj_image_mem_iff])
153 (*Do we really need both this one and its predecessor?*)
154 lemma lift_set_iff2 [iff]:
155 "((f,uu) \<in> lift_set i A) = ((f i, (delete_map i f, uu)) \<in> A)"
156 by (simp add: lift_set_def mem_rename_set_iff drop_map_def)
159 lemma lift_set_mono: "A \<subseteq> B ==> lift_set i A \<subseteq> lift_set i B"
160 apply (unfold lift_set_def)
161 apply (erule image_mono)
164 lemma lift_set_Un_distrib: "lift_set i (A \<union> B) = lift_set i A \<union> lift_set i B"
165 by (simp add: lift_set_def image_Un)
167 lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B"
168 apply (unfold lift_set_def)
169 apply (rule inj_lift_map [THEN image_set_diff])
173 subsection{*The Lattice Operations*}
175 lemma bij_lift [iff]: "bij (lift i)"
176 by (simp add: lift_def)
178 lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
179 by (simp add: lift_def)
181 lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
182 by (simp add: lift_def)
184 lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
185 by (simp add: lift_def)
187 subsection{*Safety: constrains, stable, invariant*}
189 lemma lift_constrains:
190 "(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)"
191 by (simp add: lift_def lift_set_def rename_constrains)
194 "(lift i F \<in> stable (lift_set i A)) = (F \<in> stable A)"
195 by (simp add: lift_def lift_set_def rename_stable)
197 lemma lift_invariant:
198 "(lift i F \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
199 by (simp add: lift_def lift_set_def rename_invariant)
201 lemma lift_Constrains:
202 "(lift i F \<in> (lift_set i A) Co (lift_set i B)) = (F \<in> A Co B)"
203 by (simp add: lift_def lift_set_def rename_Constrains)
206 "(lift i F \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
207 by (simp add: lift_def lift_set_def rename_Stable)
210 "(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)"
211 by (simp add: lift_def lift_set_def rename_Always)
213 subsection{*Progress: transient, ensures*}
215 lemma lift_transient:
216 "(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)"
217 by (simp add: lift_def lift_set_def rename_transient)
220 "(lift i F \<in> (lift_set i A) ensures (lift_set i B)) =
221 (F \<in> A ensures B)"
222 by (simp add: lift_def lift_set_def rename_ensures)
225 "(lift i F \<in> (lift_set i A) leadsTo (lift_set i B)) =
226 (F \<in> A leadsTo B)"
227 by (simp add: lift_def lift_set_def rename_leadsTo)
230 "(lift i F \<in> (lift_set i A) LeadsTo (lift_set i B)) =
231 (F \<in> A LeadsTo B)"
232 by (simp add: lift_def lift_set_def rename_LeadsTo)
237 lemma lift_lift_guarantees_eq:
238 "(lift i F \<in> (lift i ` X) guarantees (lift i ` Y)) =
239 (F \<in> X guarantees Y)"
240 apply (unfold lift_def)
241 apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric])
242 apply (simp add: o_def)
245 lemma lift_guarantees_eq_lift_inv:
246 "(lift i F \<in> X guarantees Y) =
247 (F \<in> (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
248 by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def)
251 (*To preserve snd means that the second component is there just to allow
252 guarantees properties to be stated. Converse fails, for lift i F can
253 change function components other than i*)
254 lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd"
255 apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
256 apply (simp add: lift_def rename_preserves)
257 apply (simp add: lift_map_def o_def split_def)
260 lemma delete_map_eqE':
261 "(delete_map i g) = (delete_map i g') ==> \<exists>x. g = g'(i:=x)"
262 apply (drule_tac f = "insert_map i (g i) " in arg_cong)
263 apply (simp add: insert_map_delete_map_eq)
267 lemmas delete_map_eqE = delete_map_eqE' [THEN exE, elim!]
269 lemma delete_map_neq_apply:
270 "[| delete_map j g = delete_map j g'; i\<noteq>j |] ==> g i = g' i"
273 (*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
275 lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) <*> UNIV"
278 lemma vimage_sub_eq_lift_set [simp]:
279 "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)"
282 lemma mem_lift_act_iff [iff]:
283 "((s,s') \<in> extend_act (%(x,u::unit). lift_map i x) act) =
284 ((drop_map i s, drop_map i s') \<in> act)"
285 apply (unfold extend_act_def, auto)
286 apply (rule bexI, auto)
289 lemma preserves_snd_lift_stable:
290 "[| F \<in> preserves snd; i\<noteq>j |]
291 ==> lift j F \<in> stable (lift_set i (A <*> UNIV))"
292 apply (auto simp add: lift_def lift_set_def stable_def constrains_def
293 rename_def extend_def mem_rename_set_iff)
294 apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
295 apply (drule_tac x = i in fun_cong, auto)
298 (*If i\<noteq>j then lift j F does nothing to lift_set i, and the
299 premise ensures A \<subseteq> B.*)
300 lemma constrains_imp_lift_constrains:
301 "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);
302 F j \<in> preserves snd |]
303 ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
304 apply (case_tac "i=j")
305 apply (simp add: lift_def lift_set_def rename_constrains)
306 apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
308 apply (erule constrains_imp_subset [THEN lift_set_mono])
312 lemma lift_map_image_Times:
313 "lift_map i ` (A <*> UNIV) =
314 (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
315 apply (auto intro!: bexI image_eqI simp add: lift_map_def)
316 apply (rule split_conv [symmetric])
319 lemma lift_preserves_eq:
320 "(lift i F \<in> preserves v) = (F \<in> preserves (v o lift_map i))"
321 by (simp add: lift_def rename_preserves)
323 (*A useful rewrite. If o, sub have been rewritten out already then can also
324 use it as rewrite_rule [sub_def, o_def] lift_preserves_sub*)
325 lemma lift_preserves_sub:
326 "F \<in> preserves snd
327 ==> lift i F \<in> preserves (v o sub j o fst) =
328 (if i=j then F \<in> preserves (v o fst) else True)"
329 apply (drule subset_preserves_o [THEN subsetD])
330 apply (simp add: lift_preserves_eq o_def)
331 apply (auto cong del: if_weak_cong
332 simp add: lift_map_def eq_commute split_def o_def)
336 subsection{*Lemmas to Handle Function Composition (o) More Consistently*}
338 (*Lets us prove one version of a theorem and store others*)
339 lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
340 by (simp add: fun_eq_iff o_def)
342 lemma o_equiv_apply: "f o g = h ==> \<forall>x. f(g x) = h x"
343 by (simp add: fun_eq_iff o_def)
345 lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
347 apply (auto simp add: o_def lift_map_def sub_def)
350 lemma snd_o_lift_map: "snd o lift_map i = snd o snd"
352 apply (auto simp add: o_def lift_map_def)
356 subsection{*More lemmas about extend and project*}
358 text{*They could be moved to theory Extend or Project*}
360 lemma extend_act_extend_act:
361 "extend_act h' (extend_act h act) =
362 extend_act (%(x,(y,y')). h'(h(x,y),y')) act"
363 apply (auto elim!: rev_bexI simp add: extend_act_def, blast)
366 lemma project_act_project_act:
367 "project_act h (project_act h' act) =
368 project_act (%(x,(y,y')). h'(h(x,y),y')) act"
369 by (auto elim!: rev_bexI simp add: project_act_def)
371 lemma project_act_extend_act:
372 "project_act h (extend_act h' act) =
373 {(x,x'). \<exists>s s' y y' z. (s,s') \<in> act &
374 h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}"
375 by (simp add: extend_act_def project_act_def, blast)
378 subsection{*OK and "lift"*}
380 lemma act_in_UNION_preserves_fst:
381 "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
382 apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I)
383 apply (auto simp add: preserves_def stable_def constrains_def)
386 lemma UNION_OK_lift_I:
387 "[| \<forall>i \<in> I. F i \<in> preserves snd;
388 \<forall>i \<in> I. UNION (preserves fst) Acts \<subseteq> AllowedActs (F i) |]
389 ==> OK I (%i. lift i (F i))"
390 apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
391 apply (simp add: Extend.AllowedActs_extend project_act_extend_act)
392 apply (rename_tac "act")
394 "{(x, x'). \<exists>s f u s' f' u'.
395 ((s, f, u), s', f', u') \<in> act &
396 lift_map j x = lift_map i (s, f, u) &
397 lift_map j x' = lift_map i (s', f', u') }
398 \<subseteq> { (x,x') . fst x = fst x'}")
399 apply (blast intro: act_in_UNION_preserves_fst, clarify)
400 apply (drule_tac x = j in fun_cong)+
401 apply (drule_tac x = i in bspec, assumption)
402 apply (frule preserves_imp_eq, auto)
406 "[| \<forall>i \<in> I. F i \<in> preserves snd;
407 \<forall>i \<in> I. preserves fst \<subseteq> Allowed (F i) |]
408 ==> OK I (%i. lift i (F i))"
409 by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
411 lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"
412 by (simp add: lift_def)
414 lemma lift_image_preserves:
415 "lift i ` preserves v = preserves (v o drop_map i)"
416 by (simp add: rename_image_preserves lift_def)