author | paulson |
Wed, 10 Jul 2002 16:54:07 +0200 | |
changeset 13339 | 0f89104dd377 |
parent 12484 | 7ad150f5fc10 |
child 14046 | 6616e6c53d48 |
permissions | -rw-r--r-- |
11479 | 1 |
(* Title: ZF/UNITY/Comp.ML |
2 |
ID: $Id$ |
|
3 |
Author: Sidi O Ehmety, Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
Composition |
|
6 |
From Chandy and Sanders, "Reasoning About Program Composition" |
|
7 |
||
8 |
Revised by Sidi Ehmety on January 2001 |
|
9 |
||
10 |
*) |
|
11 |
||
12 |
(*** component and strict_component relations ***) |
|
13 |
||
14 |
Goalw [component_def] |
|
15 |
"H component F | H component G ==> H component (F Join G)"; |
|
16 |
by Auto_tac; |
|
17 |
by (res_inst_tac [("x", "Ga Join G")] exI 1); |
|
18 |
by (res_inst_tac [("x", "G Join F")] exI 2); |
|
19 |
by (auto_tac (claset(), simpset() addsimps Join_ac)); |
|
20 |
qed "componentI"; |
|
21 |
||
22 |
Goalw [component_def] |
|
23 |
"G:program ==> (F component G) <-> \ |
|
24 |
\ (Init(G) <= Init(F) & Acts(F) <= Acts(G) & AllowedActs(G) <= AllowedActs(F))"; |
|
25 |
by Auto_tac; |
|
26 |
by (rtac exI 1); |
|
27 |
by (rtac program_equalityI 1); |
|
28 |
by Auto_tac; |
|
29 |
qed "component_eq_subset"; |
|
30 |
||
31 |
Goalw [component_def] |
|
32 |
"F:program ==> SKIP component F"; |
|
33 |
by (res_inst_tac [("x", "F")] exI 1); |
|
34 |
by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1); |
|
35 |
qed "component_SKIP"; |
|
36 |
||
37 |
Goalw [component_def] |
|
38 |
"F:program ==> F component F"; |
|
39 |
by (res_inst_tac [("x", "F")] exI 1); |
|
40 |
by (force_tac (claset() addIs [Join_SKIP_right], simpset()) 1); |
|
41 |
qed "component_refl"; |
|
42 |
||
43 |
Addsimps [component_SKIP, component_refl]; |
|
44 |
||
45 |
Goal "F component SKIP ==> programify(F) = SKIP"; |
|
46 |
by (rtac program_equalityI 1); |
|
47 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_eq_subset]))); |
|
48 |
by (Blast_tac 1); |
|
49 |
qed "SKIP_minimal"; |
|
50 |
||
51 |
Goalw [component_def] "F component (F Join G)"; |
|
52 |
by (Blast_tac 1); |
|
53 |
qed "component_Join1"; |
|
54 |
||
55 |
Goalw [component_def] "G component (F Join G)"; |
|
56 |
by (simp_tac (simpset() addsimps [Join_commute]) 1); |
|
57 |
by (Blast_tac 1); |
|
58 |
qed "component_Join2"; |
|
59 |
||
60 |
Goal "F component G ==> F Join G = G"; |
|
61 |
by (auto_tac (claset(), simpset() |
|
62 |
addsimps [component_def, Join_left_absorb])); |
|
63 |
qed "Join_absorb1"; |
|
64 |
||
65 |
Goal "G component F ==> F Join G = F"; |
|
66 |
by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def])); |
|
67 |
qed "Join_absorb2"; |
|
68 |
||
12220 | 69 |
Goal "H:program==>(JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)"; |
11479 | 70 |
by (case_tac "I=0" 1); |
71 |
by (Force_tac 1); |
|
72 |
by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
73 |
by Auto_tac; |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12484
diff
changeset
|
74 |
by (Blast_tac 1); |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12484
diff
changeset
|
75 |
by (rename_tac "y" 1); |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12484
diff
changeset
|
76 |
by (dres_inst_tac [("c", "y"), ("A", "AllowedActs(H)")] subsetD 1); |
11479 | 77 |
by (REPEAT(blast_tac (claset() addSEs [not_emptyE]) 1)); |
78 |
qed "JN_component_iff"; |
|
79 |
||
12195 | 80 |
Goalw [component_def] "i:I ==> F(i) component (JN i:I. (F(i)))"; |
11479 | 81 |
by (blast_tac (claset() addIs [JN_absorb]) 1); |
82 |
qed "component_JN"; |
|
83 |
||
84 |
Goalw [component_def] "[| F component G; G component H |] ==> F component H"; |
|
85 |
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); |
|
86 |
qed "component_trans"; |
|
87 |
||
12195 | 88 |
Goal "[| F:program; G:program |] ==>(F component G & G component F) --> F = G"; |
11479 | 89 |
by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
90 |
by (Clarify_tac 1); |
|
91 |
by (rtac program_equalityI 1); |
|
92 |
by Auto_tac; |
|
93 |
qed "component_antisym"; |
|
94 |
||
95 |
Goal "H:program ==> ((F Join G) component H) <-> (F component H & G component H)"; |
|
96 |
by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
97 |
by (Blast_tac 1); |
|
98 |
qed "Join_component_iff"; |
|
99 |
||
100 |
Goal "[| F component G; G:A co B; F:program |] ==> F : A co B"; |
|
12484 | 101 |
by (ftac constrainsD2 1); |
11479 | 102 |
by (rotate_tac ~1 1); |
103 |
by (auto_tac (claset(), |
|
104 |
simpset() addsimps [constrains_def, component_eq_subset])); |
|
105 |
qed "component_constrains"; |
|
106 |
||
12195 | 107 |
(* Used in Guar.thy to show that programs are partially ordered*) |
11479 | 108 |
(* bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);*) |
109 |
||
110 |
(*** preserves ***) |
|
111 |
||
12195 | 112 |
val prems = Goalw [preserves_def] |
11479 | 113 |
"ALL z. F:stable({s:state. f(s) = z}) ==> F:preserves(f)"; |
114 |
by Auto_tac; |
|
115 |
by (blast_tac (claset() addDs [stableD2]) 1); |
|
12195 | 116 |
qed "preserves_aux"; |
117 |
bind_thm("preservesI", allI RS preserves_aux); |
|
11479 | 118 |
|
119 |
Goalw [preserves_def, stable_def, constrains_def] |
|
120 |
"[| F:preserves(f); act : Acts(F); <s,t> : act |] ==> f(s) = f(t)"; |
|
121 |
by (subgoal_tac "s:state & t:state" 1); |
|
12195 | 122 |
by (blast_tac (claset() addSDs [Acts_type RS subsetD]) 2); |
11479 | 123 |
by Auto_tac; |
124 |
by (dres_inst_tac [("x", "f(s)")] spec 1); |
|
125 |
by (dres_inst_tac [("x", "act")] bspec 1); |
|
126 |
by Auto_tac; |
|
127 |
qed "preserves_imp_eq"; |
|
128 |
||
129 |
Goalw [preserves_def] |
|
130 |
"(F Join G : preserves(v)) <-> \ |
|
131 |
\ (programify(F) : preserves(v) & programify(G) : preserves(v))"; |
|
132 |
by (auto_tac (claset(), simpset() addsimps [INT_iff])); |
|
133 |
qed "Join_preserves"; |
|
134 |
||
135 |
Goal "(JOIN(I,F): preserves(v)) <-> (ALL i:I. programify(F(i)):preserves(v))"; |
|
12195 | 136 |
by (auto_tac (claset(), simpset() addsimps [JN_stable, preserves_def, INT_iff])); |
11479 | 137 |
qed "JN_preserves"; |
138 |
||
139 |
Goal "SKIP : preserves(v)"; |
|
12195 | 140 |
by (auto_tac (claset(), simpset() addsimps [preserves_def, INT_iff])); |
11479 | 141 |
qed "SKIP_preserves"; |
142 |
||
143 |
AddIffs [Join_preserves, JN_preserves, SKIP_preserves]; |
|
144 |
||
12195 | 145 |
(** Added by Sidi **) |
11479 | 146 |
(** component_of **) |
147 |
||
148 |
(* component_of is stronger than component *) |
|
149 |
Goalw [component_def, component_of_def] |
|
150 |
"F component_of H ==> F component H"; |
|
151 |
by (Blast_tac 1); |
|
152 |
qed "component_of_imp_component"; |
|
153 |
||
12195 | 154 |
(* component_of satisfies many of component's properties *) |
11479 | 155 |
Goalw [component_of_def] |
156 |
"F:program ==> F component_of F"; |
|
157 |
by (res_inst_tac [("x", "SKIP")] exI 1); |
|
158 |
by Auto_tac; |
|
159 |
qed "component_of_refl"; |
|
160 |
||
161 |
Goalw [component_of_def] |
|
162 |
"F:program ==>SKIP component_of F"; |
|
163 |
by Auto_tac; |
|
164 |
by (res_inst_tac [("x", "F")] exI 1); |
|
165 |
by Auto_tac; |
|
166 |
qed "component_of_SKIP"; |
|
167 |
Addsimps [component_of_refl, component_of_SKIP]; |
|
168 |
||
169 |
Goalw [component_of_def] |
|
170 |
"[| F component_of G; G component_of H |] ==> F component_of H"; |
|
171 |
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); |
|
172 |
qed "component_of_trans"; |
|
173 |
||
174 |
(** localize **) |
|
175 |
Goalw [localize_def] |
|
176 |
"Init(localize(v,F)) = Init(F)"; |
|
177 |
by (Simp_tac 1); |
|
178 |
qed "localize_Init_eq"; |
|
179 |
||
180 |
Goalw [localize_def] |
|
181 |
"Acts(localize(v,F)) = Acts(F)"; |
|
182 |
by (Simp_tac 1); |
|
183 |
qed "localize_Acts_eq"; |
|
184 |
||
185 |
Goalw [localize_def] |
|
12195 | 186 |
"AllowedActs(localize(v,F)) = AllowedActs(F) Int (UN G:preserves(v). Acts(G))"; |
187 |
by (rtac equalityI 1); |
|
188 |
by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); |
|
11479 | 189 |
qed "localize_AllowedActs_eq"; |
190 |
||
12195 | 191 |
AddIffs [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq]; |
192 |