4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 LeadsTo relation, restricted to the set of reachable states. |
6 LeadsTo relation, restricted to the set of reachable states. |
7 *) |
7 *) |
8 |
8 |
9 overload_1st_set "SubstAx.LeadsTo"; |
9 overload_1st_set "SubstAx.op LeadsTo"; |
10 |
10 |
11 |
11 |
12 (*** Specialized laws for handling invariants ***) |
12 (*** Specialized laws for handling invariants ***) |
13 |
13 |
14 (** Conjoining a safety property **) |
14 (** Conjoining a safety property **) |
15 |
15 |
16 Goal "[| reachable F <= C; F : LeadsTo (C Int A) A' |] \ |
16 Goal "[| reachable F <= C; F : (C Int A) LeadsTo A' |] \ |
17 \ ==> F : LeadsTo A A'"; |
17 \ ==> F : A LeadsTo A'"; |
18 by (asm_full_simp_tac |
18 by (asm_full_simp_tac |
19 (simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1); |
19 (simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1); |
20 qed "reachable_LeadsToI"; |
20 qed "reachable_LeadsToI"; |
21 |
21 |
22 Goal "[| reachable F <= C; F : LeadsTo A A' |] \ |
22 Goal "[| reachable F <= C; F : A LeadsTo A' |] \ |
23 \ ==> F : LeadsTo A (C Int A')"; |
23 \ ==> F : A LeadsTo (C Int A')"; |
24 by (asm_full_simp_tac |
24 by (asm_full_simp_tac |
25 (simpset() addsimps [LeadsTo_def, Int_absorb2, |
25 (simpset() addsimps [LeadsTo_def, Int_absorb2, |
26 Int_assoc RS sym]) 1); |
26 Int_assoc RS sym]) 1); |
27 qed "reachable_LeadsToD"; |
27 qed "reachable_LeadsToD"; |
28 |
28 |
29 |
29 |
30 (** Conjoining an invariant **) |
30 (** Conjoining an invariant **) |
31 |
31 |
32 (* [| Invariant F C; F : LeadsTo (C Int A) A' |] ==> F : LeadsTo A A' *) |
32 (* [| Invariant F C; F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *) |
33 bind_thm ("Invariant_LeadsToI", |
33 bind_thm ("Invariant_LeadsToI", |
34 Invariant_includes_reachable RS reachable_LeadsToI); |
34 Invariant_includes_reachable RS reachable_LeadsToI); |
35 |
35 |
36 (* [| Invariant F C; F : LeadsTo A A' |] ==> F : LeadsTo A (C Int A') *) |
36 (* [| Invariant F C; F : A LeadsTo A' |] ==> F : A LeadsTo (C Int A') *) |
37 bind_thm ("Invariant_LeadsToD", |
37 bind_thm ("Invariant_LeadsToD", |
38 Invariant_includes_reachable RS reachable_LeadsToD); |
38 Invariant_includes_reachable RS reachable_LeadsToD); |
39 |
39 |
40 |
40 |
41 |
41 |
42 |
42 |
43 (*** Introduction rules: Basis, Trans, Union ***) |
43 (*** Introduction rules: Basis, Trans, Union ***) |
44 |
44 |
45 Goal "F : leadsTo A B ==> F : LeadsTo A B"; |
45 Goal "F : A leadsTo B ==> F : A LeadsTo B"; |
46 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
46 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
47 by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1); |
47 by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1); |
48 qed "leadsTo_imp_LeadsTo"; |
48 qed "leadsTo_imp_LeadsTo"; |
49 |
49 |
50 Goal "[| F : LeadsTo A B; F : LeadsTo B C |] ==> F : LeadsTo A C"; |
50 Goal "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C"; |
51 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
51 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
52 by (blast_tac (claset() addIs [leadsTo_Trans]) 1); |
52 by (blast_tac (claset() addIs [leadsTo_Trans]) 1); |
53 qed "LeadsTo_Trans"; |
53 qed "LeadsTo_Trans"; |
54 |
54 |
55 val prems = Goalw [LeadsTo_def] |
55 val prems = Goalw [LeadsTo_def] |
56 "(!!A. A : S ==> F : LeadsTo A B) ==> F : LeadsTo (Union S) B"; |
56 "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B"; |
57 by (Simp_tac 1); |
57 by (Simp_tac 1); |
58 by (stac Int_Union 1); |
58 by (stac Int_Union 1); |
59 by (blast_tac (claset() addIs [leadsTo_UN] addDs prems) 1); |
59 by (blast_tac (claset() addIs [leadsTo_UN] addDs prems) 1); |
60 qed "LeadsTo_Union"; |
60 qed "LeadsTo_Union"; |
61 |
61 |
62 |
62 |
63 (*** Derived rules ***) |
63 (*** Derived rules ***) |
64 |
64 |
65 Goal "F : LeadsTo A UNIV"; |
65 Goal "F : A LeadsTo UNIV"; |
66 by (asm_simp_tac |
66 by (asm_simp_tac |
67 (simpset() addsimps [LeadsTo_def, Int_lower1 RS subset_imp_leadsTo]) 1); |
67 (simpset() addsimps [LeadsTo_def, Int_lower1 RS subset_imp_leadsTo]) 1); |
68 qed "LeadsTo_UNIV"; |
68 qed "LeadsTo_UNIV"; |
69 Addsimps [LeadsTo_UNIV]; |
69 Addsimps [LeadsTo_UNIV]; |
70 |
70 |
71 (*Useful with cancellation, disjunction*) |
71 (*Useful with cancellation, disjunction*) |
72 Goal "F : LeadsTo A (A' Un A') ==> F : LeadsTo A A'"; |
72 Goal "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'"; |
73 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
73 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
74 qed "LeadsTo_Un_duplicate"; |
74 qed "LeadsTo_Un_duplicate"; |
75 |
75 |
76 Goal "F : LeadsTo A (A' Un C Un C) ==> F : LeadsTo A (A' Un C)"; |
76 Goal "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)"; |
77 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
77 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
78 qed "LeadsTo_Un_duplicate2"; |
78 qed "LeadsTo_Un_duplicate2"; |
79 |
79 |
80 val prems = |
80 val prems = |
81 Goal "(!!i. i : I ==> F : LeadsTo (A i) B) ==> F : LeadsTo (UN i:I. A i) B"; |
81 Goal "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B"; |
82 by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1); |
82 by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1); |
83 by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1); |
83 by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1); |
84 qed "LeadsTo_UN"; |
84 qed "LeadsTo_UN"; |
85 |
85 |
86 (*Binary union introduction rule*) |
86 (*Binary union introduction rule*) |
87 Goal "[| F : LeadsTo A C; F : LeadsTo B C |] ==> F : LeadsTo (A Un B) C"; |
87 Goal "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C"; |
88 by (stac Un_eq_Union 1); |
88 by (stac Un_eq_Union 1); |
89 by (blast_tac (claset() addIs [LeadsTo_Union]) 1); |
89 by (blast_tac (claset() addIs [LeadsTo_Union]) 1); |
90 qed "LeadsTo_Un"; |
90 qed "LeadsTo_Un"; |
91 |
91 |
92 Goal "A <= B ==> F : LeadsTo A B"; |
92 Goal "A <= B ==> F : A LeadsTo B"; |
93 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
93 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
94 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
94 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
95 qed "subset_imp_LeadsTo"; |
95 qed "subset_imp_LeadsTo"; |
96 |
96 |
97 bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo); |
97 bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo); |
98 Addsimps [empty_LeadsTo]; |
98 Addsimps [empty_LeadsTo]; |
99 |
99 |
100 Goal "[| F : LeadsTo A A'; A' <= B' |] ==> F : LeadsTo A B'"; |
100 Goal "[| F : A LeadsTo A'; A' <= B' |] ==> F : A LeadsTo B'"; |
101 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
101 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
102 by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1); |
102 by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1); |
103 qed_spec_mp "LeadsTo_weaken_R"; |
103 qed_spec_mp "LeadsTo_weaken_R"; |
104 |
104 |
105 Goal "[| F : LeadsTo A A'; B <= A |] \ |
105 Goal "[| F : A LeadsTo A'; B <= A |] \ |
106 \ ==> F : LeadsTo B A'"; |
106 \ ==> F : B LeadsTo A'"; |
107 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
107 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
108 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1); |
108 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1); |
109 qed_spec_mp "LeadsTo_weaken_L"; |
109 qed_spec_mp "LeadsTo_weaken_L"; |
110 |
110 |
111 Goal "[| F : LeadsTo A A'; \ |
111 Goal "[| F : A LeadsTo A'; \ |
112 \ B <= A; A' <= B' |] \ |
112 \ B <= A; A' <= B' |] \ |
113 \ ==> F : LeadsTo B B'"; |
113 \ ==> F : B LeadsTo B'"; |
114 by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L, |
114 by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L, |
115 LeadsTo_Trans]) 1); |
115 LeadsTo_Trans]) 1); |
116 qed "LeadsTo_weaken"; |
116 qed "LeadsTo_weaken"; |
117 |
117 |
118 Goal "[| reachable F <= C; F : LeadsTo A A'; \ |
118 Goal "[| reachable F <= C; F : A LeadsTo A'; \ |
119 \ C Int B <= A; C Int A' <= B' |] \ |
119 \ C Int B <= A; C Int A' <= B' |] \ |
120 \ ==> F : LeadsTo B B'"; |
120 \ ==> F : B LeadsTo B'"; |
121 by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken] |
121 by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken] |
122 addIs [reachable_LeadsToD]) 1); |
122 addIs [reachable_LeadsToD]) 1); |
123 qed "reachable_LeadsTo_weaken"; |
123 qed "reachable_LeadsTo_weaken"; |
124 |
124 |
125 (** Two theorems for "proof lattices" **) |
125 (** Two theorems for "proof lattices" **) |
126 |
126 |
127 Goal "[| F : LeadsTo A B |] ==> F : LeadsTo (A Un B) B"; |
127 Goal "[| F : A LeadsTo B |] ==> F : (A Un B) LeadsTo B"; |
128 by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1); |
128 by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1); |
129 qed "LeadsTo_Un_post"; |
129 qed "LeadsTo_Un_post"; |
130 |
130 |
131 Goal "[| F : LeadsTo A B; F : LeadsTo B C |] \ |
131 Goal "[| F : A LeadsTo B; F : B LeadsTo C |] \ |
132 \ ==> F : LeadsTo (A Un B) C"; |
132 \ ==> F : (A Un B) LeadsTo C"; |
133 by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, |
133 by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, |
134 LeadsTo_weaken_L, LeadsTo_Trans]) 1); |
134 LeadsTo_weaken_L, LeadsTo_Trans]) 1); |
135 qed "LeadsTo_Trans_Un"; |
135 qed "LeadsTo_Trans_Un"; |
136 |
136 |
137 |
137 |
138 (** Distributive laws **) |
138 (** Distributive laws **) |
139 |
139 |
140 Goal "(F : LeadsTo (A Un B) C) = (F : LeadsTo A C & F : LeadsTo B C)"; |
140 Goal "(F : (A Un B) LeadsTo C) = (F : A LeadsTo C & F : B LeadsTo C)"; |
141 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1); |
141 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1); |
142 qed "LeadsTo_Un_distrib"; |
142 qed "LeadsTo_Un_distrib"; |
143 |
143 |
144 Goal "(F : LeadsTo (UN i:I. A i) B) = (ALL i : I. F : LeadsTo (A i) B)"; |
144 Goal "(F : (UN i:I. A i) LeadsTo B) = (ALL i : I. F : (A i) LeadsTo B)"; |
145 by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); |
145 by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); |
146 qed "LeadsTo_UN_distrib"; |
146 qed "LeadsTo_UN_distrib"; |
147 |
147 |
148 Goal "(F : LeadsTo (Union S) B) = (ALL A : S. F : LeadsTo A B)"; |
148 Goal "(F : (Union S) LeadsTo B) = (ALL A : S. F : A LeadsTo B)"; |
149 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); |
149 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); |
150 qed "LeadsTo_Union_distrib"; |
150 qed "LeadsTo_Union_distrib"; |
151 |
151 |
152 |
152 |
153 (** More rules using the premise "Invariant F" **) |
153 (** More rules using the premise "Invariant F" **) |
154 |
154 |
155 Goal "[| F : Constrains (A-A') (A Un A'); F : transient (A-A') |] \ |
155 Goal "[| F : (A-A') Co (A Un A'); F : transient (A-A') |] \ |
156 \ ==> F : LeadsTo A A'"; |
156 \ ==> F : A LeadsTo A'"; |
157 by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def]) 1); |
157 by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def]) 1); |
158 by (rtac (ensuresI RS leadsTo_Basis) 1); |
158 by (rtac (ensuresI RS leadsTo_Basis) 1); |
159 by (blast_tac (claset() addIs [transient_strengthen]) 2); |
159 by (blast_tac (claset() addIs [transient_strengthen]) 2); |
160 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
160 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
161 qed "LeadsTo_Basis"; |
161 qed "LeadsTo_Basis"; |
162 |
162 |
163 Goal "[| F : Invariant INV; \ |
163 Goal "[| F : Invariant INV; \ |
164 \ F : Constrains (INV Int (A-A')) (A Un A'); \ |
164 \ F : (INV Int (A-A')) Co (A Un A'); \ |
165 \ F : transient (INV Int (A-A')) |] \ |
165 \ F : transient (INV Int (A-A')) |] \ |
166 \ ==> F : LeadsTo A A'"; |
166 \ ==> F : A LeadsTo A'"; |
167 by (rtac Invariant_LeadsToI 1); |
167 by (rtac Invariant_LeadsToI 1); |
168 by (assume_tac 1); |
168 by (assume_tac 1); |
169 by (rtac LeadsTo_Basis 1); |
169 by (rtac LeadsTo_Basis 1); |
170 by (blast_tac (claset() addIs [transient_strengthen]) 2); |
170 by (blast_tac (claset() addIs [transient_strengthen]) 2); |
171 by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1); |
171 by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1); |
172 qed "Invariant_LeadsTo_Basis"; |
172 qed "Invariant_LeadsTo_Basis"; |
173 |
173 |
174 Goal "[| F : Invariant INV; \ |
174 Goal "[| F : Invariant INV; \ |
175 \ F : LeadsTo A A'; INV Int B <= A; INV Int A' <= B' |] \ |
175 \ F : A LeadsTo A'; INV Int B <= A; INV Int A' <= B' |] \ |
176 \ ==> F : LeadsTo B B'"; |
176 \ ==> F : B LeadsTo B'"; |
177 by (REPEAT (ares_tac [Invariant_includes_reachable, |
177 by (REPEAT (ares_tac [Invariant_includes_reachable, |
178 reachable_LeadsTo_weaken] 1)); |
178 reachable_LeadsTo_weaken] 1)); |
179 qed "Invariant_LeadsTo_weaken"; |
179 qed "Invariant_LeadsTo_weaken"; |
180 |
180 |
181 |
181 |
182 (*Set difference: maybe combine with leadsTo_weaken_L?? |
182 (*Set difference: maybe combine with leadsTo_weaken_L?? |
183 This is the most useful form of the "disjunction" rule*) |
183 This is the most useful form of the "disjunction" rule*) |
184 Goal "[| F : LeadsTo (A-B) C; F : LeadsTo (A Int B) C |] \ |
184 Goal "[| F : (A-B) LeadsTo C; F : (A Int B) LeadsTo C |] \ |
185 \ ==> F : LeadsTo A C"; |
185 \ ==> F : A LeadsTo C"; |
186 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1); |
186 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1); |
187 qed "LeadsTo_Diff"; |
187 qed "LeadsTo_Diff"; |
188 |
188 |
189 |
189 |
190 val prems = |
190 val prems = |
191 Goal "(!! i. i:I ==> F : LeadsTo (A i) (A' i)) \ |
191 Goal "(!! i. i:I ==> F : (A i) LeadsTo (A' i)) \ |
192 \ ==> F : LeadsTo (UN i:I. A i) (UN i:I. A' i)"; |
192 \ ==> F : (UN i:I. A i) LeadsTo (UN i:I. A' i)"; |
193 by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1); |
193 by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1); |
194 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] |
194 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] |
195 addIs prems) 1); |
195 addIs prems) 1); |
196 qed "LeadsTo_UN_UN"; |
196 qed "LeadsTo_UN_UN"; |
197 |
197 |
198 |
198 |
199 (*Version with no index set*) |
199 (*Version with no index set*) |
200 val prems = |
200 val prems = |
201 Goal "(!! i. F : LeadsTo (A i) (A' i)) \ |
201 Goal "(!! i. F : (A i) LeadsTo (A' i)) \ |
202 \ ==> F : LeadsTo (UN i. A i) (UN i. A' i)"; |
202 \ ==> F : (UN i. A i) LeadsTo (UN i. A' i)"; |
203 by (blast_tac (claset() addIs [LeadsTo_UN_UN] |
203 by (blast_tac (claset() addIs [LeadsTo_UN_UN] |
204 addIs prems) 1); |
204 addIs prems) 1); |
205 qed "LeadsTo_UN_UN_noindex"; |
205 qed "LeadsTo_UN_UN_noindex"; |
206 |
206 |
207 (*Version with no index set*) |
207 (*Version with no index set*) |
208 Goal "ALL i. F : LeadsTo (A i) (A' i) \ |
208 Goal "ALL i. F : (A i) LeadsTo (A' i) \ |
209 \ ==> F : LeadsTo (UN i. A i) (UN i. A' i)"; |
209 \ ==> F : (UN i. A i) LeadsTo (UN i. A' i)"; |
210 by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1); |
210 by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1); |
211 qed "all_LeadsTo_UN_UN"; |
211 qed "all_LeadsTo_UN_UN"; |
212 |
212 |
213 |
213 |
214 (*Binary union version*) |
214 (*Binary union version*) |
215 Goal "[| F : LeadsTo A A'; F : LeadsTo B B' |] \ |
215 Goal "[| F : A LeadsTo A'; F : B LeadsTo B' |] \ |
216 \ ==> F : LeadsTo (A Un B) (A' Un B')"; |
216 \ ==> F : (A Un B) LeadsTo (A' Un B')"; |
217 by (blast_tac (claset() addIs [LeadsTo_Un, |
217 by (blast_tac (claset() addIs [LeadsTo_Un, |
218 LeadsTo_weaken_R]) 1); |
218 LeadsTo_weaken_R]) 1); |
219 qed "LeadsTo_Un_Un"; |
219 qed "LeadsTo_Un_Un"; |
220 |
220 |
221 |
221 |
222 (** The cancellation law **) |
222 (** The cancellation law **) |
223 |
223 |
224 Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo B B' |] \ |
224 Goal "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |] \ |
225 \ ==> F : LeadsTo A (A' Un B')"; |
225 \ ==> F : A LeadsTo (A' Un B')"; |
226 by (blast_tac (claset() addIs [LeadsTo_Un_Un, |
226 by (blast_tac (claset() addIs [LeadsTo_Un_Un, |
227 subset_imp_LeadsTo, LeadsTo_Trans]) 1); |
227 subset_imp_LeadsTo, LeadsTo_Trans]) 1); |
228 qed "LeadsTo_cancel2"; |
228 qed "LeadsTo_cancel2"; |
229 |
229 |
230 Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo (B-A') B' |] \ |
230 Goal "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |] \ |
231 \ ==> F : LeadsTo A (A' Un B')"; |
231 \ ==> F : A LeadsTo (A' Un B')"; |
232 by (rtac LeadsTo_cancel2 1); |
232 by (rtac LeadsTo_cancel2 1); |
233 by (assume_tac 2); |
233 by (assume_tac 2); |
234 by (ALLGOALS Asm_simp_tac); |
234 by (ALLGOALS Asm_simp_tac); |
235 qed "LeadsTo_cancel_Diff2"; |
235 qed "LeadsTo_cancel_Diff2"; |
236 |
236 |
237 Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo B B' |] \ |
237 Goal "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] \ |
238 \ ==> F : LeadsTo A (B' Un A')"; |
238 \ ==> F : A LeadsTo (B' Un A')"; |
239 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); |
239 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); |
240 by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1); |
240 by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1); |
241 qed "LeadsTo_cancel1"; |
241 qed "LeadsTo_cancel1"; |
242 |
242 |
243 Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo (B-A') B' |] \ |
243 Goal "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |] \ |
244 \ ==> F : LeadsTo A (B' Un A')"; |
244 \ ==> F : A LeadsTo (B' Un A')"; |
245 by (rtac LeadsTo_cancel1 1); |
245 by (rtac LeadsTo_cancel1 1); |
246 by (assume_tac 2); |
246 by (assume_tac 2); |
247 by (ALLGOALS Asm_simp_tac); |
247 by (ALLGOALS Asm_simp_tac); |
248 qed "LeadsTo_cancel_Diff1"; |
248 qed "LeadsTo_cancel_Diff1"; |
249 |
249 |
250 |
250 |
251 (** The impossibility law **) |
251 (** The impossibility law **) |
252 |
252 |
253 (*The set "A" may be non-empty, but it contains no reachable states*) |
253 (*The set "A" may be non-empty, but it contains no reachable states*) |
254 Goal "F : LeadsTo A {} ==> reachable F Int A = {}"; |
254 Goal "F : A LeadsTo {} ==> reachable F Int A = {}"; |
255 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
255 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
256 by (etac leadsTo_empty 1); |
256 by (etac leadsTo_empty 1); |
257 qed "LeadsTo_empty"; |
257 qed "LeadsTo_empty"; |
258 |
258 |
259 |
259 |
260 (** PSP: Progress-Safety-Progress **) |
260 (** PSP: Progress-Safety-Progress **) |
261 |
261 |
262 (*Special case of PSP: Misra's "stable conjunction"*) |
262 (*Special case of PSP: Misra's "stable conjunction"*) |
263 Goal "[| F : LeadsTo A A'; F : Stable B |] \ |
263 Goal "[| F : A LeadsTo A'; F : Stable B |] \ |
264 \ ==> F : LeadsTo (A Int B) (A' Int B)"; |
264 \ ==> F : (A Int B) LeadsTo (A' Int B)"; |
265 by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1); |
265 by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1); |
266 by (dtac psp_stable 1); |
266 by (dtac psp_stable 1); |
267 by (assume_tac 1); |
267 by (assume_tac 1); |
268 by (asm_full_simp_tac (simpset() addsimps Int_ac) 1); |
268 by (asm_full_simp_tac (simpset() addsimps Int_ac) 1); |
269 qed "PSP_stable"; |
269 qed "PSP_stable"; |
270 |
270 |
271 Goal "[| F : LeadsTo A A'; F : Stable B |] \ |
271 Goal "[| F : A LeadsTo A'; F : Stable B |] \ |
272 \ ==> F : LeadsTo (B Int A) (B Int A')"; |
272 \ ==> F : (B Int A) LeadsTo (B Int A')"; |
273 by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1); |
273 by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1); |
274 qed "PSP_stable2"; |
274 qed "PSP_stable2"; |
275 |
275 |
276 Goalw [LeadsTo_def, Constrains_def] |
276 Goalw [LeadsTo_def, Constrains_def] |
277 "[| F : LeadsTo A A'; F : Constrains B B' |] \ |
277 "[| F : A LeadsTo A'; F : B Co B' |] \ |
278 \ ==> F : LeadsTo (A Int B) ((A' Int B) Un (B' - B))"; |
278 \ ==> F : (A Int B) LeadsTo ((A' Int B) Un (B' - B))"; |
279 by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1); |
279 by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1); |
280 qed "PSP"; |
280 qed "PSP"; |
281 |
281 |
282 Goal "[| F : LeadsTo A A'; F : Constrains B B' |] \ |
282 Goal "[| F : A LeadsTo A'; F : B Co B' |] \ |
283 \ ==> F : LeadsTo (B Int A) ((B Int A') Un (B' - B))"; |
283 \ ==> F : (B Int A) LeadsTo ((B Int A') Un (B' - B))"; |
284 by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1); |
284 by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1); |
285 qed "PSP2"; |
285 qed "PSP2"; |
286 |
286 |
287 Goalw [Unless_def] |
287 Goalw [Unless_def] |
288 "[| F : LeadsTo A A'; F : Unless B B' |] \ |
288 "[| F : A LeadsTo A'; F : B Unless B' |] \ |
289 \ ==> F : LeadsTo (A Int B) ((A' Int B) Un B')"; |
289 \ ==> F : (A Int B) LeadsTo ((A' Int B) Un B')"; |
290 by (dtac PSP 1); |
290 by (dtac PSP 1); |
291 by (assume_tac 1); |
291 by (assume_tac 1); |
292 by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, |
292 by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, |
293 subset_imp_LeadsTo]) 1); |
293 subset_imp_LeadsTo]) 1); |
294 qed "PSP_Unless"; |
294 qed "PSP_Unless"; |
295 |
295 |
296 |
296 |
297 Goal "[| F : Stable A; F : transient C; \ |
297 Goal "[| F : Stable A; F : transient C; \ |
298 \ reachable F <= (-A Un B Un C) |] ==> F : LeadsTo A B"; |
298 \ reachable F <= (-A Un B Un C) |] ==> F : A LeadsTo B"; |
299 by (etac reachable_LeadsTo_weaken 1); |
299 by (etac reachable_LeadsTo_weaken 1); |
300 by (rtac LeadsTo_Diff 1); |
300 by (rtac LeadsTo_Diff 1); |
301 by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2); |
301 by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2); |
302 by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo]))); |
302 by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo]))); |
303 qed "Stable_transient_reachable_LeadsTo"; |
303 qed "Stable_transient_reachable_LeadsTo"; |
305 |
305 |
306 (*** Induction rules ***) |
306 (*** Induction rules ***) |
307 |
307 |
308 (** Meta or object quantifier ????? **) |
308 (** Meta or object quantifier ????? **) |
309 Goal "[| wf r; \ |
309 Goal "[| wf r; \ |
310 \ ALL m. F : LeadsTo (A Int f-``{m}) \ |
310 \ ALL m. F : (A Int f-``{m}) LeadsTo \ |
311 \ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ |
311 \ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ |
312 \ ==> F : LeadsTo A B"; |
312 \ ==> F : A LeadsTo B"; |
313 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
313 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
314 by (etac leadsTo_wf_induct 1); |
314 by (etac leadsTo_wf_induct 1); |
315 by (blast_tac (claset() addIs [leadsTo_weaken]) 1); |
315 by (blast_tac (claset() addIs [leadsTo_weaken]) 1); |
316 qed "LeadsTo_wf_induct"; |
316 qed "LeadsTo_wf_induct"; |
317 |
317 |
318 |
318 |
319 Goal "[| wf r; \ |
319 Goal "[| wf r; \ |
320 \ ALL m:I. F : LeadsTo (A Int f-``{m}) \ |
320 \ ALL m:I. F : (A Int f-``{m}) LeadsTo \ |
321 \ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ |
321 \ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ |
322 \ ==> F : LeadsTo A ((A - (f-``I)) Un B)"; |
322 \ ==> F : A LeadsTo ((A - (f-``I)) Un B)"; |
323 by (etac LeadsTo_wf_induct 1); |
323 by (etac LeadsTo_wf_induct 1); |
324 by Safe_tac; |
324 by Safe_tac; |
325 by (case_tac "m:I" 1); |
325 by (case_tac "m:I" 1); |
326 by (blast_tac (claset() addIs [LeadsTo_weaken]) 1); |
326 by (blast_tac (claset() addIs [LeadsTo_weaken]) 1); |
327 by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1); |
327 by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1); |
328 qed "Bounded_induct"; |
328 qed "Bounded_induct"; |
329 |
329 |
330 |
330 |
331 Goal "[| ALL m. F : LeadsTo (A Int f-``{m}) \ |
331 Goal "[| ALL m. F : (A Int f-``{m}) LeadsTo \ |
332 \ ((A Int f-``(lessThan m)) Un B) |] \ |
332 \ ((A Int f-``(lessThan m)) Un B) |] \ |
333 \ ==> F : LeadsTo A B"; |
333 \ ==> F : A LeadsTo B"; |
334 by (rtac (wf_less_than RS LeadsTo_wf_induct) 1); |
334 by (rtac (wf_less_than RS LeadsTo_wf_induct) 1); |
335 by (Asm_simp_tac 1); |
335 by (Asm_simp_tac 1); |
336 qed "LessThan_induct"; |
336 qed "LessThan_induct"; |
337 |
337 |
338 (*Integer version. Could generalize from #0 to any lower bound*) |
338 (*Integer version. Could generalize from #0 to any lower bound*) |
339 val [reach, prem] = |
339 val [reach, prem] = |
340 Goal "[| reachable F <= {s. #0 <= f s}; \ |
340 Goal "[| reachable F <= {s. #0 <= f s}; \ |
341 \ !! z. F : LeadsTo (A Int {s. f s = z}) \ |
341 \ !! z. F : (A Int {s. f s = z}) LeadsTo \ |
342 \ ((A Int {s. f s < z}) Un B) |] \ |
342 \ ((A Int {s. f s < z}) Un B) |] \ |
343 \ ==> F : LeadsTo A B"; |
343 \ ==> F : A LeadsTo B"; |
344 by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1); |
344 by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1); |
345 by (simp_tac (simpset() addsimps [vimage_def]) 1); |
345 by (simp_tac (simpset() addsimps [vimage_def]) 1); |
346 by (rtac ([reach, prem] MRS reachable_LeadsTo_weaken) 1); |
346 by (rtac ([reach, prem] MRS reachable_LeadsTo_weaken) 1); |
347 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff])); |
347 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff])); |
348 qed "integ_0_le_induct"; |
348 qed "integ_0_le_induct"; |
349 |
349 |
350 Goal "[| ALL m:(greaterThan l). F : LeadsTo (A Int f-``{m}) \ |
350 Goal "[| ALL m:(greaterThan l). F : (A Int f-``{m}) LeadsTo \ |
351 \ ((A Int f-``(lessThan m)) Un B) |] \ |
351 \ ((A Int f-``(lessThan m)) Un B) |] \ |
352 \ ==> F : LeadsTo A ((A Int (f-``(atMost l))) Un B)"; |
352 \ ==> F : A LeadsTo ((A Int (f-``(atMost l))) Un B)"; |
353 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1); |
353 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1); |
354 by (rtac (wf_less_than RS Bounded_induct) 1); |
354 by (rtac (wf_less_than RS Bounded_induct) 1); |
355 by (Asm_simp_tac 1); |
355 by (Asm_simp_tac 1); |
356 qed "LessThan_bounded_induct"; |
356 qed "LessThan_bounded_induct"; |
357 |
357 |
358 Goal "[| ALL m:(lessThan l). F : LeadsTo (A Int f-``{m}) \ |
358 Goal "[| ALL m:(lessThan l). F : (A Int f-``{m}) LeadsTo \ |
359 \ ((A Int f-``(greaterThan m)) Un B) |] \ |
359 \ ((A Int f-``(greaterThan m)) Un B) |] \ |
360 \ ==> F : LeadsTo A ((A Int (f-``(atLeast l))) Un B)"; |
360 \ ==> F : A LeadsTo ((A Int (f-``(atLeast l))) Un B)"; |
361 by (res_inst_tac [("f","f"),("f1", "%k. l - k")] |
361 by (res_inst_tac [("f","f"),("f1", "%k. l - k")] |
362 (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1); |
362 (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1); |
363 by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1); |
363 by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1); |
364 by (Clarify_tac 1); |
364 by (Clarify_tac 1); |
365 by (case_tac "m<l" 1); |
365 by (case_tac "m<l" 1); |