27 qed "transient_strengthen"; |
27 qed "transient_strengthen"; |
28 |
28 |
29 Goalw [transient_def] |
29 Goalw [transient_def] |
30 "[| act: Acts F; A <= Domain act; act^^A <= -A |] ==> F : transient A"; |
30 "[| act: Acts F; A <= Domain act; act^^A <= -A |] ==> F : transient A"; |
31 by (Blast_tac 1); |
31 by (Blast_tac 1); |
32 qed "transient_mem"; |
32 qed "transientI"; |
|
33 |
|
34 val major::prems = |
|
35 Goalw [transient_def] |
|
36 "[| F : transient A; \ |
|
37 \ !!act. [| act: Acts F; A <= Domain act; act^^A <= -A |] ==> P |] \ |
|
38 \ ==> P"; |
|
39 by (rtac (major RS CollectD RS bexE) 1); |
|
40 by (blast_tac (claset() addIs prems) 1); |
|
41 qed "transientE"; |
33 |
42 |
34 Goalw [transient_def] "transient UNIV = {}"; |
43 Goalw [transient_def] "transient UNIV = {}"; |
35 by Auto_tac; |
44 by Auto_tac; |
36 qed "transient_UNIV"; |
45 qed "transient_UNIV"; |
37 |
46 |
51 Goalw [ensures_def] |
60 Goalw [ensures_def] |
52 "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"; |
61 "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"; |
53 by (Blast_tac 1); |
62 by (Blast_tac 1); |
54 qed "ensuresD"; |
63 qed "ensuresD"; |
55 |
64 |
56 (*The L-version (precondition strengthening) doesn't hold for ENSURES*) |
|
57 Goalw [ensures_def] |
65 Goalw [ensures_def] |
58 "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'"; |
66 "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'"; |
59 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); |
67 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); |
60 qed "ensures_weaken_R"; |
68 qed "ensures_weaken_R"; |
61 |
69 |
62 Goalw [ensures_def, constrains_def, transient_def] |
70 (*The L-version (precondition strengthening) fails, but we have this*) |
63 "F : A ensures UNIV"; |
|
64 by Auto_tac; |
|
65 qed "ensures_UNIV"; |
|
66 |
|
67 Goalw [ensures_def] |
71 Goalw [ensures_def] |
68 "[| F : stable C; \ |
72 "[| F : stable C; F : A ensures B |] \ |
69 \ F : (C Int (A - A')) co (A Un A'); \ |
73 \ ==> F : (C Int A) ensures (C Int B)"; |
70 \ F : transient (C Int (A-A')) |] \ |
74 by (auto_tac (claset(), |
71 \ ==> F : (C Int A) ensures (C Int A')"; |
75 simpset() addsimps [ensures_def, |
72 by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym, |
76 Int_Un_distrib RS sym, |
73 Diff_Int_distrib RS sym, |
77 Diff_Int_distrib RS sym])); |
74 stable_constrains_Int]) 1); |
78 by (blast_tac (claset() addIs [transient_strengthen]) 2); |
|
79 by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1); |
75 qed "stable_ensures_Int"; |
80 qed "stable_ensures_Int"; |
76 |
81 |
|
82 (*NEVER USED*) |
77 Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B"; |
83 Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B"; |
78 by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); |
84 by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); |
79 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); |
85 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); |
80 qed "stable_transient_ensures"; |
86 qed "stable_transient_ensures"; |
81 |
87 |
93 |
99 |
94 Goal "F : transient A ==> F : A leadsTo (-A)"; |
100 Goal "F : transient A ==> F : A leadsTo (-A)"; |
95 by (asm_simp_tac |
101 by (asm_simp_tac |
96 (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1); |
102 (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1); |
97 qed "transient_imp_leadsTo"; |
103 qed "transient_imp_leadsTo"; |
98 |
|
99 Goal "F : A leadsTo UNIV"; |
|
100 by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1); |
|
101 qed "leadsTo_UNIV"; |
|
102 Addsimps [leadsTo_UNIV]; |
|
103 |
104 |
104 (*Useful with cancellation, disjunction*) |
105 (*Useful with cancellation, disjunction*) |
105 Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"; |
106 Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"; |
106 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
107 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
107 qed "leadsTo_Un_duplicate"; |
108 qed "leadsTo_Un_duplicate"; |
162 bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); |
163 bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); |
163 |
164 |
164 bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo); |
165 bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo); |
165 Addsimps [empty_leadsTo]; |
166 Addsimps [empty_leadsTo]; |
166 |
167 |
|
168 bind_thm ("leadsTo_UNIV", subset_UNIV RS subset_imp_leadsTo); |
|
169 Addsimps [leadsTo_UNIV]; |
|
170 |
167 |
171 |
168 Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"; |
172 Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"; |
169 by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1); |
173 by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1); |
170 qed "leadsTo_weaken_R"; |
174 qed "leadsTo_weaken_R"; |
171 |
175 |
207 \ ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"; |
211 \ ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"; |
208 by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1); |
212 by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1); |
209 by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] |
213 by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] |
210 addIs prems) 1); |
214 addIs prems) 1); |
211 qed "leadsTo_UN_UN"; |
215 qed "leadsTo_UN_UN"; |
212 |
|
213 |
|
214 (*Version with no index set*) |
|
215 val prems = goal thy |
|
216 "(!! i. F : (A i) leadsTo (A' i)) \ |
|
217 \ ==> F : (UN i. A i) leadsTo (UN i. A' i)"; |
|
218 by (blast_tac (claset() addIs [leadsTo_UN_UN] |
|
219 addIs prems) 1); |
|
220 qed "leadsTo_UN_UN_noindex"; |
|
221 |
|
222 (*Version with no index set*) |
|
223 Goal "ALL i. F : (A i) leadsTo (A' i) \ |
|
224 \ ==> F : (UN i. A i) leadsTo (UN i. A' i)"; |
|
225 by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1); |
|
226 qed "all_leadsTo_UN_UN"; |
|
227 |
|
228 |
216 |
229 (*Binary union version*) |
217 (*Binary union version*) |
230 Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \ |
218 Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \ |
231 \ ==> F : (A Un B) leadsTo (A' Un B')"; |
219 \ ==> F : (A Un B) leadsTo (A' Un B')"; |
232 by (blast_tac (claset() addIs [leadsTo_Un, |
220 by (blast_tac (claset() addIs [leadsTo_Un, |