7 *) |
7 *) |
8 |
8 |
9 |
9 |
10 (*** Constrains ***) |
10 (*** Constrains ***) |
11 |
11 |
12 (*Map its type, ('a * 'a)set set, 'a set, 'a set] => bool, to just 'a*) |
12 overload_1st_set "Constrains.Constrains"; |
13 Blast.overloaded ("Constrains.Constrains", |
13 |
14 HOLogic.dest_setT o domain_type o range_type); |
14 (*F : constrains B B' |
15 |
15 ==> F : constrains (reachable F Int B) (reachable F Int B')*) |
16 (*constrains (Acts F) B B' |
|
17 ==> constrains (Acts F) (reachable F Int B) (reachable F Int B')*) |
|
18 bind_thm ("constrains_reachable_Int", |
16 bind_thm ("constrains_reachable_Int", |
19 subset_refl RS |
17 subset_refl RS |
20 rewrite_rule [stable_def] stable_reachable RS |
18 rewrite_rule [stable_def] stable_reachable RS |
21 constrains_Int); |
19 constrains_Int); |
22 |
20 |
23 Goalw [Constrains_def] "constrains (Acts F) A A' ==> Constrains F A A'"; |
21 Goalw [Constrains_def] "F : constrains A A' ==> F : Constrains A A'"; |
24 by (etac constrains_reachable_Int 1); |
22 by (blast_tac (claset() addIs [constrains_reachable_Int]) 1); |
25 qed "constrains_imp_Constrains"; |
23 qed "constrains_imp_Constrains"; |
26 |
24 |
27 Goalw [stable_def, Stable_def] "stable (Acts F) A ==> Stable F A"; |
25 Goalw [stable_def, Stable_def] "F : stable A ==> F : Stable A"; |
28 by (etac constrains_imp_Constrains 1); |
26 by (etac constrains_imp_Constrains 1); |
29 qed "stable_imp_Stable"; |
27 qed "stable_imp_Stable"; |
30 |
28 |
31 val prems = Goal |
29 val prems = Goal |
32 "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \ |
30 "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \ |
33 \ ==> Constrains F A A'"; |
31 \ ==> F : Constrains A A'"; |
34 by (rtac constrains_imp_Constrains 1); |
32 by (rtac constrains_imp_Constrains 1); |
35 by (blast_tac (claset() addIs (constrainsI::prems)) 1); |
33 by (blast_tac (claset() addIs (constrainsI::prems)) 1); |
36 qed "ConstrainsI"; |
34 qed "ConstrainsI"; |
37 |
35 |
38 Goalw [Constrains_def, constrains_def] "Constrains F {} B"; |
36 Goalw [Constrains_def, constrains_def] "F : Constrains {} B"; |
39 by (Blast_tac 1); |
37 by (Blast_tac 1); |
40 qed "Constrains_empty"; |
38 qed "Constrains_empty"; |
41 |
39 |
42 Goal "Constrains F A UNIV"; |
40 Goal "F : Constrains A UNIV"; |
43 by (blast_tac (claset() addIs [ConstrainsI]) 1); |
41 by (blast_tac (claset() addIs [ConstrainsI]) 1); |
44 qed "Constrains_UNIV"; |
42 qed "Constrains_UNIV"; |
45 AddIffs [Constrains_empty, Constrains_UNIV]; |
43 AddIffs [Constrains_empty, Constrains_UNIV]; |
46 |
44 |
47 |
45 |
48 Goalw [Constrains_def] |
46 Goalw [Constrains_def] |
49 "[| Constrains F A A'; A'<=B' |] ==> Constrains F A B'"; |
47 "[| F : Constrains A A'; A'<=B' |] ==> F : Constrains A B'"; |
50 by (blast_tac (claset() addIs [constrains_weaken_R]) 1); |
48 by (blast_tac (claset() addIs [constrains_weaken_R]) 1); |
51 qed "Constrains_weaken_R"; |
49 qed "Constrains_weaken_R"; |
52 |
50 |
53 Goalw [Constrains_def] |
51 Goalw [Constrains_def] |
54 "[| Constrains F A A'; B<=A |] ==> Constrains F B A'"; |
52 "[| F : Constrains A A'; B<=A |] ==> F : Constrains B A'"; |
55 by (blast_tac (claset() addIs [constrains_weaken_L]) 1); |
53 by (blast_tac (claset() addIs [constrains_weaken_L]) 1); |
56 qed "Constrains_weaken_L"; |
54 qed "Constrains_weaken_L"; |
57 |
55 |
58 Goalw [Constrains_def] |
56 Goalw [Constrains_def] |
59 "[| Constrains F A A'; B<=A; A'<=B' |] ==> Constrains F B B'"; |
57 "[| F : Constrains A A'; B<=A; A'<=B' |] ==> F : Constrains B B'"; |
60 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
58 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
61 qed "Constrains_weaken"; |
59 qed "Constrains_weaken"; |
62 |
60 |
63 (** Union **) |
61 (** Union **) |
64 |
62 |
65 Goalw [Constrains_def] |
63 Goalw [Constrains_def] |
66 "[| Constrains F A A'; Constrains F B B' |] \ |
64 "[| F : Constrains A A'; F : Constrains B B' |] \ |
67 \ ==> Constrains F (A Un B) (A' Un B')"; |
65 \ ==> F : Constrains (A Un B) (A' Un B')"; |
68 by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1); |
66 by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1); |
69 qed "Constrains_Un"; |
67 qed "Constrains_Un"; |
70 |
68 |
71 Goalw [Constrains_def] |
69 Goal "ALL i:I. F : Constrains (A i) (A' i) \ |
72 "ALL i:I. Constrains F (A i) (A' i) \ |
70 \ ==> F : Constrains (UN i:I. A i) (UN i:I. A' i)"; |
73 \ ==> Constrains F (UN i:I. A i) (UN i:I. A' i)"; |
71 by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); |
74 by (dtac ball_constrains_UN 1); |
72 by (dtac ball_constrains_UN 1); |
75 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
73 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
76 qed "ball_Constrains_UN"; |
74 qed "ball_Constrains_UN"; |
77 |
75 |
78 (** Intersection **) |
76 (** Intersection **) |
79 |
77 |
80 Goalw [Constrains_def] |
78 Goalw [Constrains_def] |
81 "[| Constrains F A A'; Constrains F B B' |] \ |
79 "[| F : Constrains A A'; F : Constrains B B' |] \ |
82 \ ==> Constrains F (A Int B) (A' Int B')"; |
80 \ ==> F : Constrains (A Int B) (A' Int B')"; |
83 by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1); |
81 by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1); |
84 qed "Constrains_Int"; |
82 qed "Constrains_Int"; |
85 |
83 |
86 Goalw [Constrains_def] |
84 Goal "[| ALL i:I. F : Constrains (A i) (A' i) |] \ |
87 "[| ALL i:I. Constrains F (A i) (A' i) |] \ |
85 \ ==> F : Constrains (INT i:I. A i) (INT i:I. A' i)"; |
88 \ ==> Constrains F (INT i:I. A i) (INT i:I. A' i)"; |
86 by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); |
89 by (dtac ball_constrains_INT 1); |
87 by (dtac ball_constrains_INT 1); |
90 by (dtac constrains_reachable_Int 1); |
88 by (dtac constrains_reachable_Int 1); |
91 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
89 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
92 qed "ball_Constrains_INT"; |
90 qed "ball_Constrains_INT"; |
93 |
91 |
94 Goalw [Constrains_def] |
92 Goal "F : Constrains A A' ==> reachable F Int A <= A'"; |
95 "Constrains F A A' ==> reachable F Int A <= A'"; |
93 by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); |
96 by (dtac constrains_imp_subset 1); |
94 by (dtac constrains_imp_subset 1); |
97 by (ALLGOALS |
95 by (ALLGOALS |
98 (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1]))); |
96 (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1]))); |
99 qed "Constrains_imp_subset"; |
97 qed "Constrains_imp_subset"; |
100 |
98 |
101 Goalw [Constrains_def] |
99 Goalw [Constrains_def] |
102 "[| Constrains F A B; Constrains F B C |] \ |
100 "[| F : Constrains A B; F : Constrains B C |] \ |
103 \ ==> Constrains F A C"; |
101 \ ==> F : Constrains A C"; |
104 by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1); |
102 by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1); |
105 qed "Constrains_trans"; |
103 qed "Constrains_trans"; |
106 |
104 |
107 |
105 |
108 (*** Stable ***) |
106 (*** Stable ***) |
109 |
107 |
110 Goal "Stable F A = stable (Acts F) (reachable F Int A)"; |
108 Goal "(F : Stable A) = (F : stable (reachable F Int A))"; |
111 by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1); |
109 by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1); |
112 qed "Stable_eq_stable"; |
110 qed "Stable_eq_stable"; |
113 |
111 |
114 Goalw [Stable_def] "Constrains F A A ==> Stable F A"; |
112 Goalw [Stable_def] "F : Constrains A A ==> F : Stable A"; |
115 by (assume_tac 1); |
113 by (assume_tac 1); |
116 qed "StableI"; |
114 qed "StableI"; |
117 |
115 |
118 Goalw [Stable_def] "Stable F A ==> Constrains F A A"; |
116 Goalw [Stable_def] "F : Stable A ==> F : Constrains A A"; |
119 by (assume_tac 1); |
117 by (assume_tac 1); |
120 qed "StableD"; |
118 qed "StableD"; |
121 |
119 |
122 Goalw [Stable_def] |
120 Goalw [Stable_def] |
123 "[| Stable F A; Stable F A' |] ==> Stable F (A Un A')"; |
121 "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')"; |
124 by (blast_tac (claset() addIs [Constrains_Un]) 1); |
122 by (blast_tac (claset() addIs [Constrains_Un]) 1); |
125 qed "Stable_Un"; |
123 qed "Stable_Un"; |
126 |
124 |
127 Goalw [Stable_def] |
125 Goalw [Stable_def] |
128 "[| Stable F A; Stable F A' |] ==> Stable F (A Int A')"; |
126 "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')"; |
129 by (blast_tac (claset() addIs [Constrains_Int]) 1); |
127 by (blast_tac (claset() addIs [Constrains_Int]) 1); |
130 qed "Stable_Int"; |
128 qed "Stable_Int"; |
131 |
129 |
132 Goalw [Stable_def] |
130 Goalw [Stable_def] |
133 "[| Stable F C; Constrains F A (C Un A') |] \ |
131 "[| F : Stable C; F : Constrains A (C Un A') |] \ |
134 \ ==> Constrains F (C Un A) (C Un A')"; |
132 \ ==> F : Constrains (C Un A) (C Un A')"; |
135 by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1); |
133 by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1); |
136 qed "Stable_Constrains_Un"; |
134 qed "Stable_Constrains_Un"; |
137 |
135 |
138 Goalw [Stable_def] |
136 Goalw [Stable_def] |
139 "[| Stable F C; Constrains F (C Int A) A' |] \ |
137 "[| F : Stable C; F : Constrains (C Int A) A' |] \ |
140 \ ==> Constrains F (C Int A) (C Int A')"; |
138 \ ==> F : Constrains (C Int A) (C Int A')"; |
141 by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1); |
139 by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1); |
142 qed "Stable_Constrains_Int"; |
140 qed "Stable_Constrains_Int"; |
143 |
141 |
144 Goalw [Stable_def] |
142 Goalw [Stable_def] |
145 "(ALL i:I. Stable F (A i)) ==> Stable F (INT i:I. A i)"; |
143 "(ALL i:I. F : Stable (A i)) ==> F : Stable (INT i:I. A i)"; |
146 by (etac ball_Constrains_INT 1); |
144 by (etac ball_Constrains_INT 1); |
147 qed "ball_Stable_INT"; |
145 qed "ball_Stable_INT"; |
148 |
146 |
149 Goal "Stable F (reachable F)"; |
147 Goal "F : Stable (reachable F)"; |
150 by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1); |
148 by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1); |
151 qed "Stable_reachable"; |
149 qed "Stable_reachable"; |
152 |
150 |
153 |
151 |
154 |
152 |
155 (*** The Elimination Theorem. The "free" m has become universally quantified! |
153 (*** The Elimination Theorem. The "free" m has become universally quantified! |
156 Should the premise be !!m instead of ALL m ? Would make it harder to use |
154 Should the premise be !!m instead of ALL m ? Would make it harder to use |
157 in forward proof. ***) |
155 in forward proof. ***) |
158 |
156 |
159 Goalw [Constrains_def, constrains_def] |
157 Goalw [Constrains_def, constrains_def] |
160 "[| ALL m. Constrains F {s. s x = m} (B m) |] \ |
158 "[| ALL m. F : Constrains {s. s x = m} (B m) |] \ |
161 \ ==> Constrains F {s. s x : M} (UN m:M. B m)"; |
159 \ ==> F : Constrains {s. s x : M} (UN m:M. B m)"; |
162 by (Blast_tac 1); |
160 by (Blast_tac 1); |
163 qed "Elimination"; |
161 qed "Elimination"; |
164 |
162 |
165 (*As above, but for the trivial case of a one-variable state, in which the |
163 (*As above, but for the trivial case of a one-variable state, in which the |
166 state is identified with its one variable.*) |
164 state is identified with its one variable.*) |
167 Goalw [Constrains_def, constrains_def] |
165 Goalw [Constrains_def, constrains_def] |
168 "(ALL m. Constrains F {m} (B m)) ==> Constrains F M (UN m:M. B m)"; |
166 "(ALL m. F : Constrains {m} (B m)) ==> F : Constrains M (UN m:M. B m)"; |
169 by (Blast_tac 1); |
167 by (Blast_tac 1); |
170 qed "Elimination_sing"; |
168 qed "Elimination_sing"; |
171 |
169 |
172 Goalw [Constrains_def, constrains_def] |
170 Goalw [Constrains_def, constrains_def] |
173 "[| Constrains F A (A' Un B); Constrains F B B' |] \ |
171 "[| F : Constrains A (A' Un B); F : Constrains B B' |] \ |
174 \ ==> Constrains F A (A' Un B')"; |
172 \ ==> F : Constrains A (A' Un B')"; |
175 by (Blast_tac 1); |
173 by (Blast_tac 1); |
176 qed "Constrains_cancel"; |
174 qed "Constrains_cancel"; |
177 |
175 |
178 |
176 |
179 (*** Specialized laws for handling Invariants ***) |
177 (*** Specialized laws for handling Invariants ***) |
180 |
178 |
181 (** Natural deduction rules for "Invariant F A" **) |
179 (** Natural deduction rules for "Invariant F A" **) |
182 |
180 |
183 Goal "[| Init F<=A; Stable F A |] ==> Invariant F A"; |
181 Goal "[| Init F<=A; F : Stable A |] ==> F : Invariant A"; |
184 by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1); |
182 by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1); |
185 qed "InvariantI"; |
183 qed "InvariantI"; |
186 |
184 |
187 Goal "Invariant F A ==> Init F<=A & Stable F A"; |
185 Goal "F : Invariant A ==> Init F<=A & F : Stable A"; |
188 by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1); |
186 by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1); |
189 qed "InvariantD"; |
187 qed "InvariantD"; |
190 |
188 |
191 bind_thm ("InvariantE", InvariantD RS conjE); |
189 bind_thm ("InvariantE", InvariantD RS conjE); |
192 |
190 |
193 |
191 |
194 (*The set of all reachable states is an Invariant...*) |
192 (*The set of all reachable states is an Invariant...*) |
195 Goal "Invariant F (reachable F)"; |
193 Goal "F : Invariant (reachable F)"; |
196 by (simp_tac (simpset() addsimps [Invariant_def]) 1); |
194 by (simp_tac (simpset() addsimps [Invariant_def]) 1); |
197 by (blast_tac (claset() addIs (Stable_reachable::reachable.intrs)) 1); |
195 by (blast_tac (claset() addIs (Stable_reachable::reachable.intrs)) 1); |
198 qed "Invariant_reachable"; |
196 qed "Invariant_reachable"; |
199 |
197 |
200 (*...in fact the strongest Invariant!*) |
198 (*...in fact the strongest Invariant!*) |
201 Goal "Invariant F A ==> reachable F <= A"; |
199 Goal "F : Invariant A ==> reachable F <= A"; |
202 by (full_simp_tac |
200 by (full_simp_tac |
203 (simpset() addsimps [Stable_def, Constrains_def, constrains_def, |
201 (simpset() addsimps [Stable_def, Constrains_def, constrains_def, |
204 Invariant_def]) 1); |
202 Invariant_def]) 1); |
205 by (rtac subsetI 1); |
203 by (rtac subsetI 1); |
206 by (etac reachable.induct 1); |
204 by (etac reachable.induct 1); |
207 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
205 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
208 qed "Invariant_includes_reachable"; |
206 qed "Invariant_includes_reachable"; |
209 |
207 |
210 |
208 Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def] |
211 Goal "Invariant F INV ==> reachable F Int INV = reachable F"; |
209 "F : invariant A ==> F : Invariant A"; |
|
210 by (blast_tac (claset() addIs [constrains_reachable_Int]) 1); |
|
211 qed "invariant_imp_Invariant"; |
|
212 |
|
213 Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def] |
|
214 "(F : Invariant A) = (F : invariant (reachable F Int A))"; |
|
215 by (blast_tac (claset() addIs reachable.intrs) 1); |
|
216 qed "Invariant_eq_invariant_reachable"; |
|
217 |
|
218 |
|
219 |
|
220 Goal "F : Invariant INV ==> reachable F Int INV = reachable F"; |
212 by (dtac Invariant_includes_reachable 1); |
221 by (dtac Invariant_includes_reachable 1); |
213 by (Blast_tac 1); |
222 by (Blast_tac 1); |
214 qed "reachable_Int_INV"; |
223 qed "reachable_Int_INV"; |
215 |
224 |
216 Goal "[| Invariant F INV; Constrains F (INV Int A) A' |] \ |
225 Goal "[| F : Invariant INV; F : Constrains (INV Int A) A' |] \ |
217 \ ==> Constrains F A A'"; |
226 \ ==> F : Constrains A A'"; |
218 by (asm_full_simp_tac |
227 by (asm_full_simp_tac |
219 (simpset() addsimps [Constrains_def, reachable_Int_INV, |
228 (simpset() addsimps [Constrains_def, reachable_Int_INV, |
220 Int_assoc RS sym]) 1); |
229 Int_assoc RS sym]) 1); |
221 qed "Invariant_ConstrainsI"; |
230 qed "Invariant_ConstrainsI"; |
222 |
231 |
223 (* [| Invariant F INV; Constrains F (INV Int A) A |] |
232 (* [| F : Invariant INV; F : Constrains (INV Int A) A |] |
224 ==> Stable F A *) |
233 ==> F : Stable A *) |
225 bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI); |
234 bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI); |
226 |
235 |
227 Goal "[| Invariant F INV; Constrains F A A' |] \ |
236 Goal "[| F : Invariant INV; F : Constrains A A' |] \ |
228 \ ==> Constrains F A (INV Int A')"; |
237 \ ==> F : Constrains A (INV Int A')"; |
229 by (asm_full_simp_tac |
238 by (asm_full_simp_tac |
230 (simpset() addsimps [Constrains_def, reachable_Int_INV, |
239 (simpset() addsimps [Constrains_def, reachable_Int_INV, |
231 Int_assoc RS sym]) 1); |
240 Int_assoc RS sym]) 1); |
232 qed "Invariant_ConstrainsD"; |
241 qed "Invariant_ConstrainsD"; |
233 |
242 |