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