1(*  Title:      HOL/UNITY/PPROD.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4
5Abstraction over replicated components (PLam)
6General products of programs (Pi operation)
7
8Some dead wood here!
9*)
10
11theory PPROD imports Lift_prog begin
12
13definition PLam :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
14            => ((nat=>'b) * 'c) program" where
15    "PLam I F == \<Squnion>i \<in> I. lift i (F i)"
16
17syntax
18  "_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"  ("(3plam _:_./ _)" 10)
19translations
20  "plam x : A. B" == "CONST PLam A (%x. B)"
21
22
23(*** Basic properties ***)
24
25lemma Init_PLam [simp]: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))"
26by (simp add: PLam_def lift_def lift_set_def)
27
28lemma PLam_empty [simp]: "PLam {} F = SKIP"
29by (simp add: PLam_def)
30
31lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
32by (simp add: PLam_def JN_constant)
33
34lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) \<squnion> (PLam I F)"
35by (unfold PLam_def, auto)
36
37lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
38by (simp add: PLam_def JN_component_iff)
39
40lemma component_PLam: "i \<in> I ==> lift i (F i) \<le> (PLam I F)"
41apply (unfold PLam_def)
42(*blast_tac doesn't use HO unification*)
43apply (fast intro: component_JN)
44done
45
46
47(** Safety & Progress: but are they used anywhere? **)
48
49lemma PLam_constrains:
50     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
51      ==> (PLam I F \<in> (lift_set i (A \<times> UNIV)) co
52                      (lift_set i (B \<times> UNIV)))  =
53          (F i \<in> (A \<times> UNIV) co (B \<times> UNIV))"
54apply (simp add: PLam_def JN_constrains)
55apply (subst insert_Diff [symmetric], assumption)
56apply (simp add: lift_constrains)
57apply (blast intro: constrains_imp_lift_constrains)
58done
59
60lemma PLam_stable:
61     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]
62      ==> (PLam I F \<in> stable (lift_set i (A \<times> UNIV))) =
63          (F i \<in> stable (A \<times> UNIV))"
64by (simp add: stable_def PLam_constrains)
65
66lemma PLam_transient:
67     "i \<in> I ==>
68    PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
69by (simp add: JN_transient PLam_def)
70
71text\<open>This holds because the @{term "F j"} cannot change @{term "lift_set i"}\<close>
72lemma PLam_ensures:
73     "[| i \<in> I;  F i \<in> (A \<times> UNIV) ensures (B \<times> UNIV);
74         \<forall>j. F j \<in> preserves snd |]
75      ==> PLam I F \<in> lift_set i (A \<times> UNIV) ensures lift_set i (B \<times> UNIV)"
76apply (simp add: ensures_def PLam_constrains PLam_transient
77              lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric]
78              Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
79apply (rule rev_bexI, assumption)
80apply (simp add: lift_transient)
81done
82
83lemma PLam_leadsTo_Basis:
84     "[| i \<in> I;
85         F i \<in> ((A \<times> UNIV) - (B \<times> UNIV)) co
86               ((A \<times> UNIV) \<union> (B \<times> UNIV));
87         F i \<in> transient ((A \<times> UNIV) - (B \<times> UNIV));
88         \<forall>j. F j \<in> preserves snd |]
89      ==> PLam I F \<in> lift_set i (A \<times> UNIV) leadsTo lift_set i (B \<times> UNIV)"
90by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
91
92
93
94(** invariant **)
95
96lemma invariant_imp_PLam_invariant:
97     "[| F i \<in> invariant (A \<times> UNIV);  i \<in> I;
98         \<forall>j. F j \<in> preserves snd |]
99      ==> PLam I F \<in> invariant (lift_set i (A \<times> UNIV))"
100by (auto simp add: PLam_stable invariant_def)
101
102
103lemma PLam_preserves_fst [simp]:
104     "\<forall>j. F j \<in> preserves snd
105      ==> (PLam I F \<in> preserves (v o sub j o fst)) =
106          (if j \<in> I then F j \<in> preserves (v o fst) else True)"
107by (simp add: PLam_def lift_preserves_sub)
108
109lemma PLam_preserves_snd [simp,intro]:
110     "\<forall>j. F j \<in> preserves snd ==> PLam I F \<in> preserves snd"
111by (simp add: PLam_def lift_preserves_snd_I)
112
113
114
115(*** guarantees properties ***)
116
117text\<open>This rule looks unsatisfactory because it refers to @{term lift}. 
118  One must use
119  \<open>lift_guarantees_eq_lift_inv\<close> to rewrite the first subgoal and
120  something like \<open>lift_preserves_sub\<close> to rewrite the third.  However
121  there's no obvious alternative for the third premise.\<close>
122lemma guarantees_PLam_I:
123    "[| lift i (F i) \<in> X guarantees Y;  i \<in> I;
124        OK I (\<lambda>i. lift i (F i)) |]
125     ==> (PLam I F) \<in> X guarantees Y"
126apply (unfold PLam_def)
127apply (simp add: guarantees_JN_I)
128done
129
130lemma Allowed_PLam [simp]:
131     "Allowed (PLam I F) = (\<Inter>i \<in> I. lift i ` Allowed(F i))"
132by (simp add: PLam_def)
133
134
135lemma PLam_preserves [simp]:
136     "(PLam I F) \<in> preserves v = (\<forall>i \<in> I. F i \<in> preserves (v o lift_map i))"
137by (simp add: PLam_def lift_def rename_preserves)
138
139
140(**UNUSED
141    (*The f0 premise ensures that the product is well-defined.*)
142    lemma PLam_invariant_imp_invariant:
143     "[| PLam I F \<in> invariant (lift_set i A);  i \<in> I;
144             f0: Init (PLam I F) |] ==> F i \<in> invariant A"
145    apply (auto simp add: invariant_def)
146    apply (drule_tac c = "f0 (i:=x) " in subsetD)
147    apply auto
148    done
149
150    lemma PLam_invariant:
151     "[| i \<in> I;  f0: Init (PLam I F) |]
152          ==> (PLam I F \<in> invariant (lift_set i A)) = (F i \<in> invariant A)"
153    apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
154    done
155
156    (*The f0 premise isn't needed if F is a constant program because then
157      we get an initial state by replicating that of F*)
158    lemma reachable_PLam:
159     "i \<in> I
160          ==> ((plam x \<in> I. F) \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
161    apply (auto simp add: invariant_def)
162    done
163**)
164
165
166(**UNUSED
167    (** Reachability **)
168
169    Goal "[| f \<in> reachable (PLam I F);  i \<in> I |] ==> f i \<in> reachable (F i)"
170    apply (erule reachable.induct)
171    apply (auto intro: reachable.intrs)
172    done
173
174    (*Result to justify a re-organization of this file*)
175    lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))"
176    by auto
177
178    lemma reachable_PLam_subset1:
179     "reachable (PLam I F) \<subseteq> (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
180    apply (force dest!: reachable_PLam)
181    done
182
183    (*simplify using reachable_lift??*)
184    lemma reachable_lift_Join_PLam [rule_format]:
185      "[| i \<notin> I;  A \<in> reachable (F i) |]
186       ==> \<forall>f. f \<in> reachable (PLam I F)
187                  --> f(i:=A) \<in> reachable (lift i (F i) \<squnion> PLam I F)"
188    apply (erule reachable.induct)
189    apply (ALLGOALS Clarify_tac)
190    apply (erule reachable.induct)
191    (*Init, Init case*)
192    apply (force intro: reachable.intrs)
193    (*Init of F, action of PLam F case*)
194    apply (rule_tac act = act in reachable.Acts)
195    apply force
196    apply assumption
197    apply (force intro: ext)
198    (*induction over the 2nd "reachable" assumption*)
199    apply (erule_tac xa = f in reachable.induct)
200    (*Init of PLam F, action of F case*)
201    apply (rule_tac act = "lift_act i act" in reachable.Acts)
202    apply force
203    apply (force intro: reachable.Init)
204    apply (force intro: ext simp add: lift_act_def)
205    (*last case: an action of PLam I F*)
206    apply (rule_tac act = acta in reachable.Acts)
207    apply force
208    apply assumption
209    apply (force intro: ext)
210    done
211
212
213    (*The index set must be finite: otherwise infinitely many copies of F can
214      perform actions, and PLam can never catch up in finite time.*)
215    lemma reachable_PLam_subset2:
216     "finite I
217          ==> (\<Inter>i \<in> I. lift_set i (reachable (F i))) \<subseteq> reachable (PLam I F)"
218    apply (erule finite_induct)
219    apply (simp (no_asm))
220    apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
221    done
222
223    lemma reachable_PLam_eq:
224     "finite I ==>
225          reachable (PLam I F) = (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
226    apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
227    done
228
229
230    (** Co **)
231
232    lemma Constrains_imp_PLam_Constrains:
233     "[| F i \<in> A Co B;  i \<in> I;  finite I |]
234          ==> PLam I F \<in> (lift_set i A) Co (lift_set i B)"
235    apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
236    apply (auto simp add: constrains_def PLam_def)
237    apply (REPEAT (blast intro: reachable.intrs))
238    done
239
240
241
242    lemma PLam_Constrains:
243     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]
244          ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =
245              (F i \<in> A Co B)"
246    apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
247    done
248
249    lemma PLam_Stable:
250     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]
251          ==> (PLam I F \<in> Stable (lift_set i A)) = (F i \<in> Stable A)"
252    apply (simp del: Init_PLam add: Stable_def PLam_Constrains)
253    done
254
255
256    (** const_PLam (no dependence on i) doesn't require the f0 premise **)
257
258    lemma const_PLam_Constrains:
259     "[| i \<in> I;  finite I |]
260          ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =
261              (F \<in> A Co B)"
262    apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
263    done
264
265    lemma const_PLam_Stable:
266     "[| i \<in> I;  finite I |]
267          ==> ((plam x \<in> I. F) \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
268    apply (simp add: Stable_def const_PLam_Constrains)
269    done
270
271    lemma const_PLam_Increasing:
272         "[| i \<in> I;  finite I |]
273          ==> ((plam x \<in> I. F) \<in> Increasing (f o sub i)) = (F \<in> Increasing f)"
274    apply (unfold Increasing_def)
275    apply (subgoal_tac "\<forall>z. {s. z \<subseteq> (f o sub i) s} = lift_set i {s. z \<subseteq> f s}")
276    apply (asm_simp_tac (simpset () add: lift_set_sub) 2)
277    apply (simp add: finite_lessThan const_PLam_Stable)
278    done
279**)
280
281
282end
283