author | haftmann |
Mon, 20 Apr 2009 09:32:07 +0200 | |
changeset 30952 | 7ab2716dd93b |
parent 24147 | edc90be09ac1 |
child 32960 | 69916a850301 |
permissions | -rw-r--r-- |
5597 | 1 |
(* Title: HOL/UNITY/Comp.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Composition |
|
11190 | 7 |
From Chandy and Sanders, "Reasoning About Program Composition", |
8 |
Technical Report 2000-003, University of Florida, 2000. |
|
5597 | 9 |
|
13819 | 10 |
Revised by Sidi Ehmety on January 2001 |
11190 | 11 |
|
13819 | 12 |
Added: a strong form of the \<subseteq> relation (component_of) and localize |
11190 | 13 |
|
5597 | 14 |
*) |
15 |
||
13798 | 16 |
header{*Composition: Basic Primitives*} |
17 |
||
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
18 |
theory Comp |
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
19 |
imports Union |
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
20 |
begin |
5597 | 21 |
|
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
22 |
instantiation program :: (type) ord |
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
23 |
begin |
5597 | 24 |
|
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
25 |
definition |
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
26 |
component_def: "F \<le> H <-> (\<exists>G. F\<squnion>G = H)" |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
27 |
|
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
28 |
definition |
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
29 |
strict_component_def: "F < (H::'a program) <-> (F \<le> H & F \<noteq> H)" |
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
30 |
|
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
31 |
instance .. |
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
32 |
|
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
33 |
end |
11190 | 34 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7399
diff
changeset
|
35 |
constdefs |
13805 | 36 |
component_of :: "'a program =>'a program=> bool" |
11190 | 37 |
(infixl "component'_of" 50) |
13819 | 38 |
"F component_of H == \<exists>G. F ok G & F\<squnion>G = H" |
11190 | 39 |
|
13792 | 40 |
strict_component_of :: "'a program\<Rightarrow>'a program=> bool" |
11190 | 41 |
(infixl "strict'_component'_of" 50) |
13805 | 42 |
"F strict_component_of H == F component_of H & F\<noteq>H" |
13819 | 43 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7399
diff
changeset
|
44 |
preserves :: "('a=>'b) => 'a program set" |
13805 | 45 |
"preserves v == \<Inter>z. stable {s. v s = z}" |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7399
diff
changeset
|
46 |
|
11190 | 47 |
localize :: "('a=>'b) => 'a program => 'a program" |
48 |
"localize v F == mk_program(Init F, Acts F, |
|
13805 | 49 |
AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G))" |
11190 | 50 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7399
diff
changeset
|
51 |
funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c" |
11190 | 52 |
"funPair f g == %x. (f x, g x)" |
13792 | 53 |
|
54 |
||
13798 | 55 |
subsection{*The component relation*} |
13819 | 56 |
lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F\<squnion>G)" |
13792 | 57 |
apply (unfold component_def, auto) |
13819 | 58 |
apply (rule_tac x = "G\<squnion>Ga" in exI) |
59 |
apply (rule_tac [2] x = "G\<squnion>F" in exI) |
|
13792 | 60 |
apply (auto simp add: Join_ac) |
61 |
done |
|
62 |
||
13819 | 63 |
lemma component_eq_subset: |
64 |
"(F \<le> G) = |
|
13805 | 65 |
(Init G \<subseteq> Init F & Acts F \<subseteq> Acts G & AllowedActs G \<subseteq> AllowedActs F)" |
13792 | 66 |
apply (unfold component_def) |
67 |
apply (force intro!: exI program_equalityI) |
|
68 |
done |
|
69 |
||
13805 | 70 |
lemma component_SKIP [iff]: "SKIP \<le> F" |
13792 | 71 |
apply (unfold component_def) |
72 |
apply (force intro: Join_SKIP_left) |
|
73 |
done |
|
74 |
||
13805 | 75 |
lemma component_refl [iff]: "F \<le> (F :: 'a program)" |
13792 | 76 |
apply (unfold component_def) |
77 |
apply (blast intro: Join_SKIP_right) |
|
78 |
done |
|
79 |
||
13805 | 80 |
lemma SKIP_minimal: "F \<le> SKIP ==> F = SKIP" |
13792 | 81 |
by (auto intro!: program_equalityI simp add: component_eq_subset) |
82 |
||
13819 | 83 |
lemma component_Join1: "F \<le> (F\<squnion>G)" |
13792 | 84 |
by (unfold component_def, blast) |
85 |
||
13819 | 86 |
lemma component_Join2: "G \<le> (F\<squnion>G)" |
13792 | 87 |
apply (unfold component_def) |
13798 | 88 |
apply (simp add: Join_commute, blast) |
13792 | 89 |
done |
90 |
||
13819 | 91 |
lemma Join_absorb1: "F \<le> G ==> F\<squnion>G = G" |
13792 | 92 |
by (auto simp add: component_def Join_left_absorb) |
93 |
||
13819 | 94 |
lemma Join_absorb2: "G \<le> F ==> F\<squnion>G = F" |
13792 | 95 |
by (auto simp add: Join_ac component_def) |
96 |
||
13805 | 97 |
lemma JN_component_iff: "((JOIN I F) \<le> H) = (\<forall>i \<in> I. F i \<le> H)" |
13798 | 98 |
by (simp add: component_eq_subset, blast) |
13792 | 99 |
|
13805 | 100 |
lemma component_JN: "i \<in> I ==> (F i) \<le> (\<Squnion>i \<in> I. (F i))" |
13792 | 101 |
apply (unfold component_def) |
102 |
apply (blast intro: JN_absorb) |
|
103 |
done |
|
104 |
||
13805 | 105 |
lemma component_trans: "[| F \<le> G; G \<le> H |] ==> F \<le> (H :: 'a program)" |
13792 | 106 |
apply (unfold component_def) |
107 |
apply (blast intro: Join_assoc [symmetric]) |
|
108 |
done |
|
109 |
||
13805 | 110 |
lemma component_antisym: "[| F \<le> G; G \<le> F |] ==> F = (G :: 'a program)" |
13792 | 111 |
apply (simp (no_asm_use) add: component_eq_subset) |
112 |
apply (blast intro!: program_equalityI) |
|
113 |
done |
|
114 |
||
13819 | 115 |
lemma Join_component_iff: "((F\<squnion>G) \<le> H) = (F \<le> H & G \<le> H)" |
13798 | 116 |
by (simp add: component_eq_subset, blast) |
13792 | 117 |
|
13805 | 118 |
lemma component_constrains: "[| F \<le> G; G \<in> A co B |] ==> F \<in> A co B" |
13792 | 119 |
by (auto simp add: constrains_def component_eq_subset) |
120 |
||
13874 | 121 |
lemma component_stable: "[| F \<le> G; G \<in> stable A |] ==> F \<in> stable A" |
122 |
by (auto simp add: stable_def component_constrains) |
|
123 |
||
13792 | 124 |
(*Used in Guar.thy to show that programs are partially ordered*) |
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
125 |
lemmas program_less_le = strict_component_def |
13792 | 126 |
|
127 |
||
13798 | 128 |
subsection{*The preserves property*} |
13792 | 129 |
|
13805 | 130 |
lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v" |
13792 | 131 |
by (unfold preserves_def, blast) |
132 |
||
13819 | 133 |
lemma preserves_imp_eq: |
13805 | 134 |
"[| F \<in> preserves v; act \<in> Acts F; (s,s') \<in> act |] ==> v s = v s'" |
13819 | 135 |
by (unfold preserves_def stable_def constrains_def, force) |
13792 | 136 |
|
13819 | 137 |
lemma Join_preserves [iff]: |
138 |
"(F\<squnion>G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)" |
|
139 |
by (unfold preserves_def, auto) |
|
13792 | 140 |
|
141 |
lemma JN_preserves [iff]: |
|
13805 | 142 |
"(JOIN I F \<in> preserves v) = (\<forall>i \<in> I. F i \<in> preserves v)" |
13819 | 143 |
by (simp add: JN_stable preserves_def, blast) |
13792 | 144 |
|
13805 | 145 |
lemma SKIP_preserves [iff]: "SKIP \<in> preserves v" |
13792 | 146 |
by (auto simp add: preserves_def) |
147 |
||
148 |
lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)" |
|
149 |
by (simp add: funPair_def) |
|
150 |
||
13805 | 151 |
lemma preserves_funPair: "preserves (funPair v w) = preserves v \<inter> preserves w" |
13792 | 152 |
by (auto simp add: preserves_def stable_def constrains_def, blast) |
153 |
||
13805 | 154 |
(* (F \<in> preserves (funPair v w)) = (F \<in> preserves v \<inter> preserves w) *) |
13792 | 155 |
declare preserves_funPair [THEN eqset_imp_iff, iff] |
156 |
||
157 |
||
158 |
lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)" |
|
13798 | 159 |
by (simp add: funPair_def o_def) |
13792 | 160 |
|
161 |
lemma fst_o_funPair [simp]: "fst o (funPair f g) = f" |
|
13798 | 162 |
by (simp add: funPair_def o_def) |
13792 | 163 |
|
164 |
lemma snd_o_funPair [simp]: "snd o (funPair f g) = g" |
|
13798 | 165 |
by (simp add: funPair_def o_def) |
13792 | 166 |
|
13805 | 167 |
lemma subset_preserves_o: "preserves v \<subseteq> preserves (w o v)" |
13792 | 168 |
by (force simp add: preserves_def stable_def constrains_def) |
169 |
||
13805 | 170 |
lemma preserves_subset_stable: "preserves v \<subseteq> stable {s. P (v s)}" |
13792 | 171 |
apply (auto simp add: preserves_def stable_def constrains_def) |
172 |
apply (rename_tac s' s) |
|
173 |
apply (subgoal_tac "v s = v s'") |
|
174 |
apply (force+) |
|
175 |
done |
|
176 |
||
13805 | 177 |
lemma preserves_subset_increasing: "preserves v \<subseteq> increasing v" |
13792 | 178 |
by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def) |
179 |
||
13805 | 180 |
lemma preserves_id_subset_stable: "preserves id \<subseteq> stable A" |
13792 | 181 |
by (force simp add: preserves_def stable_def constrains_def) |
182 |
||
183 |
||
184 |
(** For use with def_UNION_ok_iff **) |
|
185 |
||
186 |
lemma safety_prop_preserves [iff]: "safety_prop (preserves v)" |
|
187 |
by (auto intro: safety_prop_INTER1 simp add: preserves_def) |
|
188 |
||
189 |
||
24147 | 190 |
(** Some lemmas used only in Client.thy **) |
13792 | 191 |
|
192 |
lemma stable_localTo_stable2: |
|
13819 | 193 |
"[| F \<in> stable {s. P (v s) (w s)}; |
194 |
G \<in> preserves v; G \<in> preserves w |] |
|
195 |
==> F\<squnion>G \<in> stable {s. P (v s) (w s)}" |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
196 |
apply simp |
13805 | 197 |
apply (subgoal_tac "G \<in> preserves (funPair v w) ") |
13819 | 198 |
prefer 2 apply simp |
199 |
apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], |
|
200 |
auto) |
|
13792 | 201 |
done |
202 |
||
203 |
lemma Increasing_preserves_Stable: |
|
13819 | 204 |
"[| F \<in> stable {s. v s \<le> w s}; G \<in> preserves v; F\<squnion>G \<in> Increasing w |] |
205 |
==> F\<squnion>G \<in> Stable {s. v s \<le> w s}" |
|
13792 | 206 |
apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib) |
207 |
apply (blast intro: constrains_weaken) |
|
208 |
(*The G case remains*) |
|
209 |
apply (auto simp add: preserves_def stable_def constrains_def) |
|
210 |
(*We have a G-action, so delete assumptions about F-actions*) |
|
13805 | 211 |
apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl) |
212 |
apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl) |
|
13792 | 213 |
apply (subgoal_tac "v x = v xa") |
13819 | 214 |
apply auto |
13792 | 215 |
apply (erule order_trans, blast) |
216 |
done |
|
217 |
||
218 |
(** component_of **) |
|
219 |
||
13805 | 220 |
(* component_of is stronger than \<le> *) |
221 |
lemma component_of_imp_component: "F component_of H ==> F \<le> H" |
|
13792 | 222 |
by (unfold component_def component_of_def, blast) |
223 |
||
224 |
||
13805 | 225 |
(* component_of satisfies many of the same properties as \<le> *) |
13792 | 226 |
lemma component_of_refl [simp]: "F component_of F" |
227 |
apply (unfold component_of_def) |
|
228 |
apply (rule_tac x = SKIP in exI, auto) |
|
229 |
done |
|
230 |
||
231 |
lemma component_of_SKIP [simp]: "SKIP component_of F" |
|
232 |
by (unfold component_of_def, auto) |
|
233 |
||
13819 | 234 |
lemma component_of_trans: |
13792 | 235 |
"[| F component_of G; G component_of H |] ==> F component_of H" |
236 |
apply (unfold component_of_def) |
|
237 |
apply (blast intro: Join_assoc [symmetric]) |
|
238 |
done |
|
239 |
||
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
24147
diff
changeset
|
240 |
lemmas strict_component_of_eq = strict_component_of_def |
13792 | 241 |
|
242 |
(** localize **) |
|
243 |
lemma localize_Init_eq [simp]: "Init (localize v F) = Init F" |
|
13798 | 244 |
by (simp add: localize_def) |
13792 | 245 |
|
246 |
lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F" |
|
13798 | 247 |
by (simp add: localize_def) |
13792 | 248 |
|
13819 | 249 |
lemma localize_AllowedActs_eq [simp]: |
250 |
"AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)" |
|
13798 | 251 |
by (unfold localize_def, auto) |
13792 | 252 |
|
5597 | 253 |
end |