8 From Misra, "A Logic for Concurrent Programming", 1994 |
8 From Misra, "A Logic for Concurrent Programming", 1994 |
9 *) |
9 *) |
10 |
10 |
11 open SubstAx; |
11 open SubstAx; |
12 |
12 |
13 (*constrains Acts B B' ==> constrains Acts (reachable Init Acts Int B) |
13 (*constrains Acts B B' ==> constrains Acts (reachable(Init,Acts) Int B) |
14 (reachable Init Acts Int B') *) |
14 (reachable(Init,Acts) Int B') *) |
15 bind_thm ("constrains_reachable", |
15 bind_thm ("constrains_reachable", |
16 rewrite_rule [stable_def] stable_reachable RS constrains_Int); |
16 rewrite_rule [stable_def] stable_reachable RS constrains_Int); |
17 |
17 |
18 |
18 |
19 (*** Introduction rules: Basis, Trans, Union ***) |
19 (*** Introduction rules: Basis, Trans, Union ***) |
20 |
20 |
21 Goalw [LeadsTo_def] |
21 Goal "leadsTo Acts A B ==> LeadsTo(Init,Acts) A B"; |
22 "!!Acts. leadsTo Acts A B ==> LeadsTo Init Acts A B"; |
22 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
23 by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1); |
23 by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1); |
24 qed "leadsTo_imp_LeadsTo"; |
24 qed "leadsTo_imp_LeadsTo"; |
25 |
25 |
26 Goalw [LeadsTo_def] |
26 Goal "[| constrains Acts (reachable(Init,Acts) Int (A - A')) \ |
27 "!!Acts. [| constrains Acts (reachable Init Acts Int (A - A')) \ |
|
28 \ (A Un A'); \ |
27 \ (A Un A'); \ |
29 \ transient Acts (reachable Init Acts Int (A-A')) |] \ |
28 \ transient Acts (reachable(Init,Acts) Int (A-A')) |] \ |
30 \ ==> LeadsTo Init Acts A A'"; |
29 \ ==> LeadsTo(Init,Acts) A A'"; |
|
30 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
31 by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1); |
31 by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1); |
32 by (assume_tac 2); |
32 by (assume_tac 2); |
33 by (asm_simp_tac |
33 by (asm_simp_tac |
34 (simpset() addsimps [Int_Un_distrib RS sym, Diff_Int_distrib RS sym, |
34 (simpset() addsimps [Int_Un_distrib RS sym, Diff_Int_distrib RS sym, |
35 stable_constrains_Int]) 1); |
35 stable_constrains_Int]) 1); |
36 qed "LeadsTo_Basis"; |
36 qed "LeadsTo_Basis"; |
37 |
37 |
38 Goalw [LeadsTo_def] |
38 Goal "[| LeadsTo(Init,Acts) A B; LeadsTo(Init,Acts) B C |] \ |
39 "!!Acts. [| LeadsTo Init Acts A B; LeadsTo Init Acts B C |] \ |
39 \ ==> LeadsTo(Init,Acts) A C"; |
40 \ ==> LeadsTo Init Acts A C"; |
40 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
41 by (blast_tac (claset() addIs [leadsTo_Trans]) 1); |
41 by (blast_tac (claset() addIs [leadsTo_Trans]) 1); |
42 qed "LeadsTo_Trans"; |
42 qed "LeadsTo_Trans"; |
43 |
43 |
44 val prems = goalw thy [LeadsTo_def] |
44 val [prem] = goalw thy [LeadsTo_def] |
45 "(!!A. A : S ==> LeadsTo Init Acts A B) ==> LeadsTo Init Acts (Union S) B"; |
45 "(!!A. A : S ==> LeadsTo(Init,Acts) A B) ==> LeadsTo(Init,Acts) (Union S) B"; |
|
46 by (Simp_tac 1); |
46 by (stac Int_Union 1); |
47 by (stac Int_Union 1); |
47 by (blast_tac (claset() addIs (leadsTo_UN::prems)) 1); |
48 by (blast_tac (claset() addIs [leadsTo_UN, |
|
49 simplify (simpset()) prem]) 1); |
48 qed "LeadsTo_Union"; |
50 qed "LeadsTo_Union"; |
49 |
51 |
50 |
52 |
51 (*** Derived rules ***) |
53 (*** Derived rules ***) |
52 |
54 |
53 Goal "!!Acts. id: Acts ==> LeadsTo Init Acts A UNIV"; |
55 Goal "id: Acts ==> LeadsTo(Init,Acts) A UNIV"; |
54 by (asm_simp_tac (simpset() addsimps [LeadsTo_def, |
56 by (asm_simp_tac (simpset() addsimps [LeadsTo_def, |
55 Int_lower1 RS subset_imp_leadsTo]) 1); |
57 Int_lower1 RS subset_imp_leadsTo]) 1); |
56 qed "LeadsTo_UNIV"; |
58 qed "LeadsTo_UNIV"; |
57 Addsimps [LeadsTo_UNIV]; |
59 Addsimps [LeadsTo_UNIV]; |
58 |
60 |
59 (*Useful with cancellation, disjunction*) |
61 (*Useful with cancellation, disjunction*) |
60 Goal "!!Acts. LeadsTo Init Acts A (A' Un A') ==> LeadsTo Init Acts A A'"; |
62 Goal "LeadsTo(Init,Acts) A (A' Un A') ==> LeadsTo(Init,Acts) A A'"; |
61 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
63 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
62 qed "LeadsTo_Un_duplicate"; |
64 qed "LeadsTo_Un_duplicate"; |
63 |
65 |
64 Goal "!!Acts. LeadsTo Init Acts A (A' Un C Un C) ==> LeadsTo Init Acts A (A' Un C)"; |
66 Goal "LeadsTo(Init,Acts) A (A' Un C Un C) ==> LeadsTo(Init,Acts) A (A' Un C)"; |
65 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
67 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
66 qed "LeadsTo_Un_duplicate2"; |
68 qed "LeadsTo_Un_duplicate2"; |
67 |
69 |
68 val prems = goal thy |
70 val prems = goal thy |
69 "(!!i. i : I ==> LeadsTo Init Acts (A i) B) \ |
71 "(!!i. i : I ==> LeadsTo(Init,Acts) (A i) B) \ |
70 \ ==> LeadsTo Init Acts (UN i:I. A i) B"; |
72 \ ==> LeadsTo(Init,Acts) (UN i:I. A i) B"; |
71 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); |
73 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); |
72 by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1); |
74 by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1); |
73 qed "LeadsTo_UN"; |
75 qed "LeadsTo_UN"; |
74 |
76 |
75 (*Binary union introduction rule*) |
77 (*Binary union introduction rule*) |
76 Goal |
78 Goal |
77 "!!C. [| LeadsTo Init Acts A C; LeadsTo Init Acts B C |] ==> LeadsTo Init Acts (A Un B) C"; |
79 "[| LeadsTo(Init,Acts) A C; LeadsTo(Init,Acts) B C |] ==> LeadsTo(Init,Acts) (A Un B) C"; |
78 by (stac Un_eq_Union 1); |
80 by (stac Un_eq_Union 1); |
79 by (blast_tac (claset() addIs [LeadsTo_Union]) 1); |
81 by (blast_tac (claset() addIs [LeadsTo_Union]) 1); |
80 qed "LeadsTo_Un"; |
82 qed "LeadsTo_Un"; |
81 |
83 |
82 |
84 |
83 Goalw [LeadsTo_def] |
85 Goal "[| reachable(Init,Acts) Int A <= B; id: Acts |] \ |
84 "!!A B. [| reachable Init Acts Int A <= B; id: Acts |] \ |
86 \ ==> LeadsTo(Init,Acts) A B"; |
85 \ ==> LeadsTo Init Acts A B"; |
87 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
86 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
88 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
87 qed "Int_subset_imp_LeadsTo"; |
89 qed "Int_subset_imp_LeadsTo"; |
88 |
90 |
89 Goalw [LeadsTo_def] |
91 Goal "[| A <= B; id: Acts |] ==> LeadsTo(Init,Acts) A B"; |
90 "!!A B. [| A <= B; id: Acts |] \ |
92 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
91 \ ==> LeadsTo Init Acts A B"; |
|
92 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
93 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
93 qed "subset_imp_LeadsTo"; |
94 qed "subset_imp_LeadsTo"; |
94 |
95 |
95 bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo); |
96 bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo); |
96 Addsimps [empty_LeadsTo]; |
97 Addsimps [empty_LeadsTo]; |
97 |
98 |
98 Goal |
99 Goal "[| reachable(Init,Acts) Int A = {}; id: Acts |] \ |
99 "!!A B. [| reachable Init Acts Int A = {}; id: Acts |] \ |
100 \ ==> LeadsTo(Init,Acts) A B"; |
100 \ ==> LeadsTo Init Acts A B"; |
|
101 by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1); |
101 by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1); |
102 qed "Int_empty_LeadsTo"; |
102 qed "Int_empty_LeadsTo"; |
103 |
103 |
104 |
104 |
105 Goalw [LeadsTo_def] |
105 Goal "[| LeadsTo(Init,Acts) A A'; \ |
106 "!!Acts. [| LeadsTo Init Acts A A'; \ |
106 \ reachable(Init,Acts) Int A' <= B' |] \ |
107 \ reachable Init Acts Int A' <= B' |] \ |
107 \ ==> LeadsTo(Init,Acts) A B'"; |
108 \ ==> LeadsTo Init Acts A B'"; |
108 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
109 by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1); |
109 by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1); |
110 qed_spec_mp "LeadsTo_weaken_R"; |
110 qed_spec_mp "LeadsTo_weaken_R"; |
111 |
111 |
112 |
112 |
113 Goalw [LeadsTo_def] |
113 Goal "[| LeadsTo(Init,Acts) A A'; \ |
114 "!!Acts. [| LeadsTo Init Acts A A'; \ |
114 \ reachable(Init,Acts) Int B <= A; id: Acts |] \ |
115 \ reachable Init Acts Int B <= A; id: Acts |] \ |
115 \ ==> LeadsTo(Init,Acts) B A'"; |
116 \ ==> LeadsTo Init Acts B A'"; |
116 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
117 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1); |
117 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1); |
118 qed_spec_mp "LeadsTo_weaken_L"; |
118 qed_spec_mp "LeadsTo_weaken_L"; |
119 |
119 |
120 |
120 |
121 (*Distributes over binary unions*) |
121 (*Distributes over binary unions*) |
122 Goal |
122 Goal |
123 "!!C. id: Acts ==> \ |
123 "id: Acts ==> \ |
124 \ LeadsTo Init Acts (A Un B) C = \ |
124 \ LeadsTo(Init,Acts) (A Un B) C = \ |
125 \ (LeadsTo Init Acts A C & LeadsTo Init Acts B C)"; |
125 \ (LeadsTo(Init,Acts) A C & LeadsTo(Init,Acts) B C)"; |
126 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1); |
126 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1); |
127 qed "LeadsTo_Un_distrib"; |
127 qed "LeadsTo_Un_distrib"; |
128 |
128 |
129 Goal |
129 Goal |
130 "!!C. id: Acts ==> \ |
130 "id: Acts ==> \ |
131 \ LeadsTo Init Acts (UN i:I. A i) B = \ |
131 \ LeadsTo(Init,Acts) (UN i:I. A i) B = \ |
132 \ (ALL i : I. LeadsTo Init Acts (A i) B)"; |
132 \ (ALL i : I. LeadsTo(Init,Acts) (A i) B)"; |
133 by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); |
133 by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); |
134 qed "LeadsTo_UN_distrib"; |
134 qed "LeadsTo_UN_distrib"; |
135 |
135 |
136 Goal |
136 Goal |
137 "!!C. id: Acts ==> \ |
137 "id: Acts ==> \ |
138 \ LeadsTo Init Acts (Union S) B = \ |
138 \ LeadsTo(Init,Acts) (Union S) B = \ |
139 \ (ALL A : S. LeadsTo Init Acts A B)"; |
139 \ (ALL A : S. LeadsTo(Init,Acts) A B)"; |
140 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); |
140 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); |
141 qed "LeadsTo_Union_distrib"; |
141 qed "LeadsTo_Union_distrib"; |
142 |
142 |
143 |
143 |
144 Goal |
144 Goal |
145 "!!Acts. [| LeadsTo Init Acts A A'; id: Acts; \ |
145 "[| LeadsTo(Init,Acts) A A'; id: Acts; \ |
146 \ reachable Init Acts Int B <= A; \ |
146 \ reachable(Init,Acts) Int B <= A; \ |
147 \ reachable Init Acts Int A' <= B' |] \ |
147 \ reachable(Init,Acts) Int A' <= B' |] \ |
148 \ ==> LeadsTo Init Acts B B'"; |
148 \ ==> LeadsTo(Init,Acts) B B'"; |
149 (*PROOF FAILED: why?*) |
149 (*PROOF FAILED: why?*) |
150 by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R, |
150 by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R, |
151 LeadsTo_weaken_L]) 1); |
151 LeadsTo_weaken_L]) 1); |
152 qed "LeadsTo_weaken"; |
152 qed "LeadsTo_weaken"; |
153 |
153 |
154 |
154 |
155 (*Set difference: maybe combine with leadsTo_weaken_L??*) |
155 (*Set difference: maybe combine with leadsTo_weaken_L??*) |
156 Goal |
156 Goal |
157 "!!C. [| LeadsTo Init Acts (A-B) C; LeadsTo Init Acts B C; id: Acts |] \ |
157 "[| LeadsTo(Init,Acts) (A-B) C; LeadsTo(Init,Acts) B C; id: Acts |] \ |
158 \ ==> LeadsTo Init Acts A C"; |
158 \ ==> LeadsTo(Init,Acts) A C"; |
159 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1); |
159 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1); |
160 qed "LeadsTo_Diff"; |
160 qed "LeadsTo_Diff"; |
161 |
161 |
162 |
162 |
163 (** Meta or object quantifier ??????????????????? |
163 (** Meta or object quantifier ??????????????????? |
164 see ball_constrains_UN in UNITY.ML***) |
164 see ball_constrains_UN in UNITY.ML***) |
165 |
165 |
166 val prems = goal thy |
166 val prems = goal thy |
167 "(!! i. i:I ==> LeadsTo Init Acts (A i) (A' i)) \ |
167 "(!! i. i:I ==> LeadsTo(Init,Acts) (A i) (A' i)) \ |
168 \ ==> LeadsTo Init Acts (UN i:I. A i) (UN i:I. A' i)"; |
168 \ ==> LeadsTo(Init,Acts) (UN i:I. A i) (UN i:I. A' i)"; |
169 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); |
169 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1); |
170 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] |
170 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] |
171 addIs prems) 1); |
171 addIs prems) 1); |
172 qed "LeadsTo_UN_UN"; |
172 qed "LeadsTo_UN_UN"; |
173 |
173 |
174 |
174 |
175 (*Version with no index set*) |
175 (*Version with no index set*) |
176 val prems = goal thy |
176 val prems = goal thy |
177 "(!! i. LeadsTo Init Acts (A i) (A' i)) \ |
177 "(!! i. LeadsTo(Init,Acts) (A i) (A' i)) \ |
178 \ ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)"; |
178 \ ==> LeadsTo(Init,Acts) (UN i. A i) (UN i. A' i)"; |
179 by (blast_tac (claset() addIs [LeadsTo_UN_UN] |
179 by (blast_tac (claset() addIs [LeadsTo_UN_UN] |
180 addIs prems) 1); |
180 addIs prems) 1); |
181 qed "LeadsTo_UN_UN_noindex"; |
181 qed "LeadsTo_UN_UN_noindex"; |
182 |
182 |
183 (*Version with no index set*) |
183 (*Version with no index set*) |
184 Goal |
184 Goal |
185 "!!Acts. ALL i. LeadsTo Init Acts (A i) (A' i) \ |
185 "ALL i. LeadsTo(Init,Acts) (A i) (A' i) \ |
186 \ ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)"; |
186 \ ==> LeadsTo(Init,Acts) (UN i. A i) (UN i. A' i)"; |
187 by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1); |
187 by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1); |
188 qed "all_LeadsTo_UN_UN"; |
188 qed "all_LeadsTo_UN_UN"; |
189 |
189 |
190 |
190 |
191 (*Binary union version*) |
191 (*Binary union version*) |
192 Goal "!!Acts. [| LeadsTo Init Acts A A'; LeadsTo Init Acts B B' |] \ |
192 Goal "[| LeadsTo(Init,Acts) A A'; LeadsTo(Init,Acts) B B' |] \ |
193 \ ==> LeadsTo Init Acts (A Un B) (A' Un B')"; |
193 \ ==> LeadsTo(Init,Acts) (A Un B) (A' Un B')"; |
194 by (blast_tac (claset() addIs [LeadsTo_Un, |
194 by (blast_tac (claset() addIs [LeadsTo_Un, |
195 LeadsTo_weaken_R]) 1); |
195 LeadsTo_weaken_R]) 1); |
196 qed "LeadsTo_Un_Un"; |
196 qed "LeadsTo_Un_Un"; |
197 |
197 |
198 |
198 |
199 (** The cancellation law **) |
199 (** The cancellation law **) |
200 |
200 |
201 Goal |
201 Goal |
202 "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts B B'; \ |
202 "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) B B'; \ |
203 \ id: Acts |] \ |
203 \ id: Acts |] \ |
204 \ ==> LeadsTo Init Acts A (A' Un B')"; |
204 \ ==> LeadsTo(Init,Acts) A (A' Un B')"; |
205 by (blast_tac (claset() addIs [LeadsTo_Un_Un, |
205 by (blast_tac (claset() addIs [LeadsTo_Un_Un, |
206 subset_imp_LeadsTo, LeadsTo_Trans]) 1); |
206 subset_imp_LeadsTo, LeadsTo_Trans]) 1); |
207 qed "LeadsTo_cancel2"; |
207 qed "LeadsTo_cancel2"; |
208 |
208 |
209 Goal |
209 Goal |
210 "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts (B-A') B'; id: Acts |] \ |
210 "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \ |
211 \ ==> LeadsTo Init Acts A (A' Un B')"; |
211 \ ==> LeadsTo(Init,Acts) A (A' Un B')"; |
212 by (rtac LeadsTo_cancel2 1); |
212 by (rtac LeadsTo_cancel2 1); |
213 by (assume_tac 2); |
213 by (assume_tac 2); |
214 by (ALLGOALS Asm_simp_tac); |
214 by (ALLGOALS Asm_simp_tac); |
215 qed "LeadsTo_cancel_Diff2"; |
215 qed "LeadsTo_cancel_Diff2"; |
216 |
216 |
217 Goal |
217 Goal |
218 "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts B B'; id: Acts |] \ |
218 "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) B B'; id: Acts |] \ |
219 \ ==> LeadsTo Init Acts A (B' Un A')"; |
219 \ ==> LeadsTo(Init,Acts) A (B' Un A')"; |
220 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); |
220 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); |
221 by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1); |
221 by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1); |
222 qed "LeadsTo_cancel1"; |
222 qed "LeadsTo_cancel1"; |
223 |
223 |
224 Goal |
224 Goal |
225 "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts (B-A') B'; id: Acts |] \ |
225 "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \ |
226 \ ==> LeadsTo Init Acts A (B' Un A')"; |
226 \ ==> LeadsTo(Init,Acts) A (B' Un A')"; |
227 by (rtac LeadsTo_cancel1 1); |
227 by (rtac LeadsTo_cancel1 1); |
228 by (assume_tac 2); |
228 by (assume_tac 2); |
229 by (ALLGOALS Asm_simp_tac); |
229 by (ALLGOALS Asm_simp_tac); |
230 qed "LeadsTo_cancel_Diff1"; |
230 qed "LeadsTo_cancel_Diff1"; |
231 |
231 |
232 |
232 |
233 |
233 |
234 (** The impossibility law **) |
234 (** The impossibility law **) |
235 |
235 |
236 Goalw [LeadsTo_def] |
236 Goal "LeadsTo(Init,Acts) A {} ==> reachable(Init,Acts) Int A = {}"; |
237 "!!Acts. LeadsTo Init Acts A {} ==> reachable Init Acts Int A = {}"; |
237 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
238 by (Full_simp_tac 1); |
|
239 by (etac leadsTo_empty 1); |
238 by (etac leadsTo_empty 1); |
240 qed "LeadsTo_empty"; |
239 qed "LeadsTo_empty"; |
241 |
240 |
242 |
241 |
243 (** PSP: Progress-Safety-Progress **) |
242 (** PSP: Progress-Safety-Progress **) |
244 |
243 |
245 (*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *) |
244 (*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *) |
246 Goalw [LeadsTo_def] |
245 Goal "[| LeadsTo(Init,Acts) A A'; stable Acts B |] \ |
247 "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \ |
246 \ ==> LeadsTo(Init,Acts) (A Int B) (A' Int B)"; |
248 \ ==> LeadsTo Init Acts (A Int B) (A' Int B)"; |
247 by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_assoc RS sym, |
249 by (asm_simp_tac (simpset() addsimps [Int_assoc RS sym, PSP_stable]) 1); |
248 PSP_stable]) 1); |
250 qed "R_PSP_stable"; |
249 qed "R_PSP_stable"; |
251 |
250 |
252 Goal |
251 Goal "[| LeadsTo(Init,Acts) A A'; stable Acts B |] \ |
253 "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \ |
252 \ ==> LeadsTo(Init,Acts) (B Int A) (B Int A')"; |
254 \ ==> LeadsTo Init Acts (B Int A) (B Int A')"; |
|
255 by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1); |
253 by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1); |
256 qed "R_PSP_stable2"; |
254 qed "R_PSP_stable2"; |
257 |
255 |
258 |
256 |
259 Goalw [LeadsTo_def] |
257 Goal "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \ |
260 "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \ |
258 \ ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B) Un (B' - B))"; |
261 \ ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un (B' - B))"; |
259 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); |
262 by (dtac PSP 1); |
260 by (dtac PSP 1); |
263 by (etac constrains_reachable 1); |
261 by (etac constrains_reachable 1); |
264 by (etac leadsTo_weaken 2); |
262 by (etac leadsTo_weaken 2); |
265 by (ALLGOALS Blast_tac); |
263 by (ALLGOALS Blast_tac); |
266 qed "R_PSP"; |
264 qed "R_PSP"; |
267 |
265 |
268 Goal |
266 Goal |
269 "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \ |
267 "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \ |
270 \ ==> LeadsTo Init Acts (B Int A) ((B Int A') Un (B' - B))"; |
268 \ ==> LeadsTo(Init,Acts) (B Int A) ((B Int A') Un (B' - B))"; |
271 by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1); |
269 by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1); |
272 qed "R_PSP2"; |
270 qed "R_PSP2"; |
273 |
271 |
274 Goalw [unless_def] |
272 Goalw [unless_def] |
275 "!!Acts. [| LeadsTo Init Acts A A'; unless Acts B B'; id: Acts |] \ |
273 "[| LeadsTo(Init,Acts) A A'; unless Acts B B'; id: Acts |] \ |
276 \ ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un B')"; |
274 \ ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B) Un B')"; |
277 by (dtac R_PSP 1); |
275 by (dtac R_PSP 1); |
278 by (assume_tac 1); |
276 by (assume_tac 1); |
279 by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2); |
277 by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2); |
280 by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2); |
278 by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2); |
281 by (etac LeadsTo_Diff 2); |
279 by (etac LeadsTo_Diff 2); |