| author | chaieb |
| Wed, 19 May 2004 11:23:59 +0200 | |
| changeset 14758 | af3b71a46a1c |
| parent 13812 | 91713a1915ee |
| child 21669 | c68717c16013 |
| permissions | -rw-r--r-- |
| 13786 | 1 |
(* Title: HOL/UNITY/UNITY_tactics.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 2003 University of Cambridge |
|
5 |
||
6 |
Specialized UNITY tactics, and ML bindings of theorems |
|
7 |
*) |
|
8 |
||
| 13798 | 9 |
(*ListOrder*) |
10 |
val Le_def = thm "Le_def"; |
|
11 |
val Ge_def = thm "Ge_def"; |
|
12 |
val prefix_def = thm "prefix_def"; |
|
13 |
val Nil_genPrefix = thm "Nil_genPrefix"; |
|
14 |
val genPrefix_length_le = thm "genPrefix_length_le"; |
|
15 |
val cons_genPrefixE = thm "cons_genPrefixE"; |
|
16 |
val Cons_genPrefix_Cons = thm "Cons_genPrefix_Cons"; |
|
17 |
val refl_genPrefix = thm "refl_genPrefix"; |
|
18 |
val genPrefix_refl = thm "genPrefix_refl"; |
|
19 |
val genPrefix_mono = thm "genPrefix_mono"; |
|
20 |
val append_genPrefix = thm "append_genPrefix"; |
|
21 |
val genPrefix_trans_O = thm "genPrefix_trans_O"; |
|
22 |
val genPrefix_trans = thm "genPrefix_trans"; |
|
23 |
val prefix_genPrefix_trans = thm "prefix_genPrefix_trans"; |
|
24 |
val genPrefix_prefix_trans = thm "genPrefix_prefix_trans"; |
|
25 |
val trans_genPrefix = thm "trans_genPrefix"; |
|
26 |
val genPrefix_antisym = thm "genPrefix_antisym"; |
|
27 |
val antisym_genPrefix = thm "antisym_genPrefix"; |
|
28 |
val genPrefix_Nil = thm "genPrefix_Nil"; |
|
29 |
val same_genPrefix_genPrefix = thm "same_genPrefix_genPrefix"; |
|
30 |
val genPrefix_Cons = thm "genPrefix_Cons"; |
|
31 |
val genPrefix_take_append = thm "genPrefix_take_append"; |
|
32 |
val genPrefix_append_both = thm "genPrefix_append_both"; |
|
33 |
val append_cons_eq = thm "append_cons_eq"; |
|
34 |
val append_one_genPrefix = thm "append_one_genPrefix"; |
|
35 |
val genPrefix_imp_nth = thm "genPrefix_imp_nth"; |
|
36 |
val nth_imp_genPrefix = thm "nth_imp_genPrefix"; |
|
37 |
val genPrefix_iff_nth = thm "genPrefix_iff_nth"; |
|
38 |
val prefix_refl = thm "prefix_refl"; |
|
39 |
val prefix_trans = thm "prefix_trans"; |
|
40 |
val prefix_antisym = thm "prefix_antisym"; |
|
41 |
val prefix_less_le = thm "prefix_less_le"; |
|
42 |
val set_mono = thm "set_mono"; |
|
43 |
val Nil_prefix = thm "Nil_prefix"; |
|
44 |
val prefix_Nil = thm "prefix_Nil"; |
|
45 |
val Cons_prefix_Cons = thm "Cons_prefix_Cons"; |
|
46 |
val same_prefix_prefix = thm "same_prefix_prefix"; |
|
47 |
val append_prefix = thm "append_prefix"; |
|
48 |
val prefix_appendI = thm "prefix_appendI"; |
|
49 |
val prefix_Cons = thm "prefix_Cons"; |
|
50 |
val append_one_prefix = thm "append_one_prefix"; |
|
51 |
val prefix_length_le = thm "prefix_length_le"; |
|
52 |
val strict_prefix_length_less = thm "strict_prefix_length_less"; |
|
53 |
val mono_length = thm "mono_length"; |
|
54 |
val prefix_iff = thm "prefix_iff"; |
|
55 |
val prefix_snoc = thm "prefix_snoc"; |
|
56 |
val prefix_append_iff = thm "prefix_append_iff"; |
|
57 |
val common_prefix_linear = thm "common_prefix_linear"; |
|
58 |
val reflexive_Le = thm "reflexive_Le"; |
|
59 |
val antisym_Le = thm "antisym_Le"; |
|
60 |
val trans_Le = thm "trans_Le"; |
|
61 |
val pfixLe_refl = thm "pfixLe_refl"; |
|
62 |
val pfixLe_trans = thm "pfixLe_trans"; |
|
63 |
val pfixLe_antisym = thm "pfixLe_antisym"; |
|
64 |
val prefix_imp_pfixLe = thm "prefix_imp_pfixLe"; |
|
65 |
val reflexive_Ge = thm "reflexive_Ge"; |
|
66 |
val antisym_Ge = thm "antisym_Ge"; |
|
67 |
val trans_Ge = thm "trans_Ge"; |
|
68 |
val pfixGe_refl = thm "pfixGe_refl"; |
|
69 |
val pfixGe_trans = thm "pfixGe_trans"; |
|
70 |
val pfixGe_antisym = thm "pfixGe_antisym"; |
|
71 |
val prefix_imp_pfixGe = thm "prefix_imp_pfixGe"; |
|
72 |
||
73 |
||
| 13797 | 74 |
(*UNITY*) |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
75 |
val mk_total_program_def = thm "mk_total_program_def"; |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
76 |
val totalize_act_def = thm "totalize_act_def"; |
| 13797 | 77 |
val constrains_def = thm "constrains_def"; |
78 |
val stable_def = thm "stable_def"; |
|
79 |
val invariant_def = thm "invariant_def"; |
|
80 |
val increasing_def = thm "increasing_def"; |
|
81 |
val Allowed_def = thm "Allowed_def"; |
|
82 |
val Id_in_Acts = thm "Id_in_Acts"; |
|
83 |
val insert_Id_Acts = thm "insert_Id_Acts"; |
|
84 |
val Id_in_AllowedActs = thm "Id_in_AllowedActs"; |
|
85 |
val insert_Id_AllowedActs = thm "insert_Id_AllowedActs"; |
|
86 |
val Init_eq = thm "Init_eq"; |
|
87 |
val Acts_eq = thm "Acts_eq"; |
|
88 |
val AllowedActs_eq = thm "AllowedActs_eq"; |
|
89 |
val surjective_mk_program = thm "surjective_mk_program"; |
|
90 |
val program_equalityI = thm "program_equalityI"; |
|
91 |
val program_equalityE = thm "program_equalityE"; |
|
92 |
val program_equality_iff = thm "program_equality_iff"; |
|
93 |
val def_prg_Init = thm "def_prg_Init"; |
|
94 |
val def_prg_Acts = thm "def_prg_Acts"; |
|
95 |
val def_prg_AllowedActs = thm "def_prg_AllowedActs"; |
|
96 |
val def_act_simp = thm "def_act_simp"; |
|
97 |
val def_set_simp = thm "def_set_simp"; |
|
98 |
val constrainsI = thm "constrainsI"; |
|
99 |
val constrainsD = thm "constrainsD"; |
|
100 |
val constrains_empty = thm "constrains_empty"; |
|
101 |
val constrains_empty2 = thm "constrains_empty2"; |
|
102 |
val constrains_UNIV = thm "constrains_UNIV"; |
|
103 |
val constrains_UNIV2 = thm "constrains_UNIV2"; |
|
104 |
val constrains_weaken_R = thm "constrains_weaken_R"; |
|
105 |
val constrains_weaken_L = thm "constrains_weaken_L"; |
|
106 |
val constrains_weaken = thm "constrains_weaken"; |
|
107 |
val constrains_Un = thm "constrains_Un"; |
|
108 |
val constrains_UN = thm "constrains_UN"; |
|
109 |
val constrains_Un_distrib = thm "constrains_Un_distrib"; |
|
110 |
val constrains_UN_distrib = thm "constrains_UN_distrib"; |
|
111 |
val constrains_Int_distrib = thm "constrains_Int_distrib"; |
|
112 |
val constrains_INT_distrib = thm "constrains_INT_distrib"; |
|
113 |
val constrains_Int = thm "constrains_Int"; |
|
114 |
val constrains_INT = thm "constrains_INT"; |
|
115 |
val constrains_imp_subset = thm "constrains_imp_subset"; |
|
116 |
val constrains_trans = thm "constrains_trans"; |
|
117 |
val constrains_cancel = thm "constrains_cancel"; |
|
118 |
val unlessI = thm "unlessI"; |
|
119 |
val unlessD = thm "unlessD"; |
|
120 |
val stableI = thm "stableI"; |
|
121 |
val stableD = thm "stableD"; |
|
122 |
val stable_UNIV = thm "stable_UNIV"; |
|
123 |
val stable_Un = thm "stable_Un"; |
|
124 |
val stable_UN = thm "stable_UN"; |
|
125 |
val stable_Int = thm "stable_Int"; |
|
126 |
val stable_INT = thm "stable_INT"; |
|
127 |
val stable_constrains_Un = thm "stable_constrains_Un"; |
|
128 |
val stable_constrains_Int = thm "stable_constrains_Int"; |
|
129 |
val stable_constrains_stable = thm "stable_constrains_stable"; |
|
130 |
val invariantI = thm "invariantI"; |
|
131 |
val invariant_Int = thm "invariant_Int"; |
|
132 |
val increasingD = thm "increasingD"; |
|
133 |
val increasing_constant = thm "increasing_constant"; |
|
134 |
val mono_increasing_o = thm "mono_increasing_o"; |
|
135 |
val strict_increasingD = thm "strict_increasingD"; |
|
136 |
val elimination = thm "elimination"; |
|
137 |
val elimination_sing = thm "elimination_sing"; |
|
138 |
val constrains_strongest_rhs = thm "constrains_strongest_rhs"; |
|
139 |
val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest"; |
|
140 |
val Un_Diff_Diff = thm "Un_Diff_Diff"; |
|
141 |
val Int_Union_Union = thm "Int_Union_Union"; |
|
142 |
val Image_less_than = thm "Image_less_than"; |
|
143 |
val Image_inverse_less_than = thm "Image_inverse_less_than"; |
|
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
144 |
val totalize_constrains_iff = thm "totalize_constrains_iff"; |
| 13797 | 145 |
|
146 |
(*WFair*) |
|
147 |
val stable_transient_empty = thm "stable_transient_empty"; |
|
148 |
val transient_strengthen = thm "transient_strengthen"; |
|
149 |
val transientI = thm "transientI"; |
|
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
150 |
val totalize_transientI = thm "totalize_transientI"; |
| 13797 | 151 |
val transientE = thm "transientE"; |
152 |
val transient_empty = thm "transient_empty"; |
|
153 |
val ensuresI = thm "ensuresI"; |
|
154 |
val ensuresD = thm "ensuresD"; |
|
155 |
val ensures_weaken_R = thm "ensures_weaken_R"; |
|
156 |
val stable_ensures_Int = thm "stable_ensures_Int"; |
|
157 |
val stable_transient_ensures = thm "stable_transient_ensures"; |
|
158 |
val ensures_eq = thm "ensures_eq"; |
|
159 |
val leadsTo_Basis = thm "leadsTo_Basis"; |
|
160 |
val leadsTo_Trans = thm "leadsTo_Trans"; |
|
161 |
val transient_imp_leadsTo = thm "transient_imp_leadsTo"; |
|
162 |
val leadsTo_Un_duplicate = thm "leadsTo_Un_duplicate"; |
|
163 |
val leadsTo_Un_duplicate2 = thm "leadsTo_Un_duplicate2"; |
|
164 |
val leadsTo_Union = thm "leadsTo_Union"; |
|
165 |
val leadsTo_Union_Int = thm "leadsTo_Union_Int"; |
|
166 |
val leadsTo_UN = thm "leadsTo_UN"; |
|
167 |
val leadsTo_Un = thm "leadsTo_Un"; |
|
168 |
val single_leadsTo_I = thm "single_leadsTo_I"; |
|
169 |
val leadsTo_induct = thm "leadsTo_induct"; |
|
170 |
val subset_imp_ensures = thm "subset_imp_ensures"; |
|
171 |
val subset_imp_leadsTo = thm "subset_imp_leadsTo"; |
|
172 |
val leadsTo_refl = thm "leadsTo_refl"; |
|
173 |
val empty_leadsTo = thm "empty_leadsTo"; |
|
174 |
val leadsTo_UNIV = thm "leadsTo_UNIV"; |
|
175 |
val leadsTo_induct_pre = thm "leadsTo_induct_pre"; |
|
176 |
val leadsTo_weaken_R = thm "leadsTo_weaken_R"; |
|
177 |
val leadsTo_weaken_L = thm "leadsTo_weaken_L"; |
|
178 |
val leadsTo_Un_distrib = thm "leadsTo_Un_distrib"; |
|
179 |
val leadsTo_UN_distrib = thm "leadsTo_UN_distrib"; |
|
180 |
val leadsTo_Union_distrib = thm "leadsTo_Union_distrib"; |
|
181 |
val leadsTo_weaken = thm "leadsTo_weaken"; |
|
182 |
val leadsTo_Diff = thm "leadsTo_Diff"; |
|
183 |
val leadsTo_UN_UN = thm "leadsTo_UN_UN"; |
|
184 |
val leadsTo_Un_Un = thm "leadsTo_Un_Un"; |
|
185 |
val leadsTo_cancel2 = thm "leadsTo_cancel2"; |
|
186 |
val leadsTo_cancel_Diff2 = thm "leadsTo_cancel_Diff2"; |
|
187 |
val leadsTo_cancel1 = thm "leadsTo_cancel1"; |
|
188 |
val leadsTo_cancel_Diff1 = thm "leadsTo_cancel_Diff1"; |
|
189 |
val leadsTo_empty = thm "leadsTo_empty"; |
|
190 |
val psp_stable = thm "psp_stable"; |
|
191 |
val psp_stable2 = thm "psp_stable2"; |
|
192 |
val psp_ensures = thm "psp_ensures"; |
|
193 |
val psp = thm "psp"; |
|
194 |
val psp2 = thm "psp2"; |
|
195 |
val psp_unless = thm "psp_unless"; |
|
196 |
val leadsTo_wf_induct = thm "leadsTo_wf_induct"; |
|
197 |
val bounded_induct = thm "bounded_induct"; |
|
198 |
val lessThan_induct = thm "lessThan_induct"; |
|
199 |
val lessThan_bounded_induct = thm "lessThan_bounded_induct"; |
|
200 |
val greaterThan_bounded_induct = thm "greaterThan_bounded_induct"; |
|
201 |
val wlt_leadsTo = thm "wlt_leadsTo"; |
|
202 |
val leadsTo_subset = thm "leadsTo_subset"; |
|
203 |
val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt"; |
|
204 |
val wlt_increasing = thm "wlt_increasing"; |
|
205 |
val leadsTo_123 = thm "leadsTo_123"; |
|
206 |
val wlt_constrains_wlt = thm "wlt_constrains_wlt"; |
|
207 |
val completion = thm "completion"; |
|
208 |
val finite_completion = thm "finite_completion"; |
|
209 |
val stable_completion = thm "stable_completion"; |
|
210 |
val finite_stable_completion = thm "finite_stable_completion"; |
|
211 |
||
212 |
(*Constrains*) |
|
213 |
val Increasing_def = thm "Increasing_def"; |
|
214 |
val reachable_Init = thm "reachable.Init"; |
|
215 |
val reachable_Acts = thm "reachable.Acts"; |
|
216 |
val reachable_equiv_traces = thm "reachable_equiv_traces"; |
|
217 |
val Init_subset_reachable = thm "Init_subset_reachable"; |
|
218 |
val stable_reachable = thm "stable_reachable"; |
|
219 |
val invariant_reachable = thm "invariant_reachable"; |
|
220 |
val invariant_includes_reachable = thm "invariant_includes_reachable"; |
|
221 |
val constrains_reachable_Int = thm "constrains_reachable_Int"; |
|
222 |
val Constrains_eq_constrains = thm "Constrains_eq_constrains"; |
|
223 |
val constrains_imp_Constrains = thm "constrains_imp_Constrains"; |
|
224 |
val stable_imp_Stable = thm "stable_imp_Stable"; |
|
225 |
val ConstrainsI = thm "ConstrainsI"; |
|
226 |
val Constrains_empty = thm "Constrains_empty"; |
|
227 |
val Constrains_UNIV = thm "Constrains_UNIV"; |
|
228 |
val Constrains_weaken_R = thm "Constrains_weaken_R"; |
|
229 |
val Constrains_weaken_L = thm "Constrains_weaken_L"; |
|
230 |
val Constrains_weaken = thm "Constrains_weaken"; |
|
231 |
val Constrains_Un = thm "Constrains_Un"; |
|
232 |
val Constrains_UN = thm "Constrains_UN"; |
|
233 |
val Constrains_Int = thm "Constrains_Int"; |
|
234 |
val Constrains_INT = thm "Constrains_INT"; |
|
235 |
val Constrains_imp_subset = thm "Constrains_imp_subset"; |
|
236 |
val Constrains_trans = thm "Constrains_trans"; |
|
237 |
val Constrains_cancel = thm "Constrains_cancel"; |
|
238 |
val Stable_eq = thm "Stable_eq"; |
|
239 |
val Stable_eq_stable = thm "Stable_eq_stable"; |
|
240 |
val StableI = thm "StableI"; |
|
241 |
val StableD = thm "StableD"; |
|
242 |
val Stable_Un = thm "Stable_Un"; |
|
243 |
val Stable_Int = thm "Stable_Int"; |
|
244 |
val Stable_Constrains_Un = thm "Stable_Constrains_Un"; |
|
245 |
val Stable_Constrains_Int = thm "Stable_Constrains_Int"; |
|
246 |
val Stable_UN = thm "Stable_UN"; |
|
247 |
val Stable_INT = thm "Stable_INT"; |
|
248 |
val Stable_reachable = thm "Stable_reachable"; |
|
249 |
val IncreasingD = thm "IncreasingD"; |
|
250 |
val mono_Increasing_o = thm "mono_Increasing_o"; |
|
251 |
val strict_IncreasingD = thm "strict_IncreasingD"; |
|
252 |
val increasing_imp_Increasing = thm "increasing_imp_Increasing"; |
|
253 |
val Increasing_constant = thm "Increasing_constant"; |
|
254 |
val Elimination = thm "Elimination"; |
|
255 |
val Elimination_sing = thm "Elimination_sing"; |
|
256 |
val AlwaysI = thm "AlwaysI"; |
|
257 |
val AlwaysD = thm "AlwaysD"; |
|
258 |
val AlwaysE = thm "AlwaysE"; |
|
259 |
val Always_imp_Stable = thm "Always_imp_Stable"; |
|
260 |
val Always_includes_reachable = thm "Always_includes_reachable"; |
|
261 |
val invariant_imp_Always = thm "invariant_imp_Always"; |
|
262 |
val Always_reachable = thm "Always_reachable"; |
|
263 |
val Always_eq_invariant_reachable = thm "Always_eq_invariant_reachable"; |
|
264 |
val Always_eq_includes_reachable = thm "Always_eq_includes_reachable"; |
|
265 |
val Always_UNIV_eq = thm "Always_UNIV_eq"; |
|
266 |
val UNIV_AlwaysI = thm "UNIV_AlwaysI"; |
|
267 |
val Always_eq_UN_invariant = thm "Always_eq_UN_invariant"; |
|
268 |
val Always_weaken = thm "Always_weaken"; |
|
269 |
val Always_Constrains_pre = thm "Always_Constrains_pre"; |
|
270 |
val Always_Constrains_post = thm "Always_Constrains_post"; |
|
271 |
val Always_ConstrainsI = thm "Always_ConstrainsI"; |
|
272 |
val Always_ConstrainsD = thm "Always_ConstrainsD"; |
|
273 |
val Always_Constrains_weaken = thm "Always_Constrains_weaken"; |
|
274 |
val Always_Int_distrib = thm "Always_Int_distrib"; |
|
275 |
val Always_INT_distrib = thm "Always_INT_distrib"; |
|
276 |
val Always_Int_I = thm "Always_Int_I"; |
|
277 |
val Always_Compl_Un_eq = thm "Always_Compl_Un_eq"; |
|
278 |
val Always_thin = thm "Always_thin"; |
|
279 |
||
| 13796 | 280 |
(*FP*) |
281 |
val stable_FP_Orig_Int = thm "stable_FP_Orig_Int"; |
|
282 |
val FP_Orig_weakest = thm "FP_Orig_weakest"; |
|
283 |
val stable_FP_Int = thm "stable_FP_Int"; |
|
284 |
val FP_equivalence = thm "FP_equivalence"; |
|
285 |
val FP_weakest = thm "FP_weakest"; |
|
286 |
val Compl_FP = thm "Compl_FP"; |
|
287 |
val Diff_FP = thm "Diff_FP"; |
|
288 |
||
289 |
(*SubstAx*) |
|
290 |
val LeadsTo_eq_leadsTo = thm "LeadsTo_eq_leadsTo"; |
|
291 |
val Always_LeadsTo_pre = thm "Always_LeadsTo_pre"; |
|
292 |
val Always_LeadsTo_post = thm "Always_LeadsTo_post"; |
|
293 |
val Always_LeadsToI = thm "Always_LeadsToI"; |
|
294 |
val Always_LeadsToD = thm "Always_LeadsToD"; |
|
295 |
val leadsTo_imp_LeadsTo = thm "leadsTo_imp_LeadsTo"; |
|
296 |
val LeadsTo_Trans = thm "LeadsTo_Trans"; |
|
297 |
val LeadsTo_Union = thm "LeadsTo_Union"; |
|
298 |
val LeadsTo_UNIV = thm "LeadsTo_UNIV"; |
|
299 |
val LeadsTo_Un_duplicate = thm "LeadsTo_Un_duplicate"; |
|
300 |
val LeadsTo_Un_duplicate2 = thm "LeadsTo_Un_duplicate2"; |
|
301 |
val LeadsTo_UN = thm "LeadsTo_UN"; |
|
302 |
val LeadsTo_Un = thm "LeadsTo_Un"; |
|
303 |
val single_LeadsTo_I = thm "single_LeadsTo_I"; |
|
304 |
val subset_imp_LeadsTo = thm "subset_imp_LeadsTo"; |
|
305 |
val empty_LeadsTo = thm "empty_LeadsTo"; |
|
306 |
val LeadsTo_weaken_R = thm "LeadsTo_weaken_R"; |
|
307 |
val LeadsTo_weaken_L = thm "LeadsTo_weaken_L"; |
|
308 |
val LeadsTo_weaken = thm "LeadsTo_weaken"; |
|
309 |
val Always_LeadsTo_weaken = thm "Always_LeadsTo_weaken"; |
|
310 |
val LeadsTo_Un_post = thm "LeadsTo_Un_post"; |
|
311 |
val LeadsTo_Trans_Un = thm "LeadsTo_Trans_Un"; |
|
312 |
val LeadsTo_Un_distrib = thm "LeadsTo_Un_distrib"; |
|
313 |
val LeadsTo_UN_distrib = thm "LeadsTo_UN_distrib"; |
|
314 |
val LeadsTo_Union_distrib = thm "LeadsTo_Union_distrib"; |
|
315 |
val LeadsTo_Basis = thm "LeadsTo_Basis"; |
|
316 |
val EnsuresI = thm "EnsuresI"; |
|
317 |
val Always_LeadsTo_Basis = thm "Always_LeadsTo_Basis"; |
|
318 |
val LeadsTo_Diff = thm "LeadsTo_Diff"; |
|
319 |
val LeadsTo_UN_UN = thm "LeadsTo_UN_UN"; |
|
320 |
val LeadsTo_UN_UN_noindex = thm "LeadsTo_UN_UN_noindex"; |
|
321 |
val all_LeadsTo_UN_UN = thm "all_LeadsTo_UN_UN"; |
|
322 |
val LeadsTo_Un_Un = thm "LeadsTo_Un_Un"; |
|
323 |
val LeadsTo_cancel2 = thm "LeadsTo_cancel2"; |
|
324 |
val LeadsTo_cancel_Diff2 = thm "LeadsTo_cancel_Diff2"; |
|
325 |
val LeadsTo_cancel1 = thm "LeadsTo_cancel1"; |
|
326 |
val LeadsTo_cancel_Diff1 = thm "LeadsTo_cancel_Diff1"; |
|
327 |
val LeadsTo_empty = thm "LeadsTo_empty"; |
|
328 |
val PSP_Stable = thm "PSP_Stable"; |
|
329 |
val PSP_Stable2 = thm "PSP_Stable2"; |
|
330 |
val PSP = thm "PSP"; |
|
331 |
val PSP2 = thm "PSP2"; |
|
332 |
val PSP_Unless = thm "PSP_Unless"; |
|
333 |
val Stable_transient_Always_LeadsTo = thm "Stable_transient_Always_LeadsTo"; |
|
334 |
val LeadsTo_wf_induct = thm "LeadsTo_wf_induct"; |
|
335 |
val Bounded_induct = thm "Bounded_induct"; |
|
336 |
val LessThan_induct = thm "LessThan_induct"; |
|
337 |
val integ_0_le_induct = thm "integ_0_le_induct"; |
|
338 |
val LessThan_bounded_induct = thm "LessThan_bounded_induct"; |
|
339 |
val GreaterThan_bounded_induct = thm "GreaterThan_bounded_induct"; |
|
340 |
val Completion = thm "Completion"; |
|
341 |
val Finite_completion = thm "Finite_completion"; |
|
342 |
val Stable_completion = thm "Stable_completion"; |
|
343 |
val Finite_stable_completion = thm "Finite_stable_completion"; |
|
344 |
||
| 13792 | 345 |
(*Union*) |
346 |
val Init_SKIP = thm "Init_SKIP"; |
|
347 |
val Acts_SKIP = thm "Acts_SKIP"; |
|
348 |
val AllowedActs_SKIP = thm "AllowedActs_SKIP"; |
|
349 |
val reachable_SKIP = thm "reachable_SKIP"; |
|
350 |
val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff"; |
|
351 |
val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff"; |
|
352 |
val SKIP_in_stable = thm "SKIP_in_stable"; |
|
353 |
val Init_Join = thm "Init_Join"; |
|
354 |
val Acts_Join = thm "Acts_Join"; |
|
355 |
val AllowedActs_Join = thm "AllowedActs_Join"; |
|
356 |
val JN_empty = thm "JN_empty"; |
|
357 |
val JN_insert = thm "JN_insert"; |
|
358 |
val Init_JN = thm "Init_JN"; |
|
359 |
val Acts_JN = thm "Acts_JN"; |
|
360 |
val AllowedActs_JN = thm "AllowedActs_JN"; |
|
361 |
val JN_cong = thm "JN_cong"; |
|
362 |
val Join_commute = thm "Join_commute"; |
|
363 |
val Join_assoc = thm "Join_assoc"; |
|
364 |
val Join_left_commute = thm "Join_left_commute"; |
|
365 |
val Join_SKIP_left = thm "Join_SKIP_left"; |
|
366 |
val Join_SKIP_right = thm "Join_SKIP_right"; |
|
367 |
val Join_absorb = thm "Join_absorb"; |
|
368 |
val Join_left_absorb = thm "Join_left_absorb"; |
|
369 |
val Join_ac = thms "Join_ac"; |
|
370 |
val JN_absorb = thm "JN_absorb"; |
|
371 |
val JN_Un = thm "JN_Un"; |
|
372 |
val JN_constant = thm "JN_constant"; |
|
373 |
val JN_Join_distrib = thm "JN_Join_distrib"; |
|
374 |
val JN_Join_miniscope = thm "JN_Join_miniscope"; |
|
375 |
val JN_Join_diff = thm "JN_Join_diff"; |
|
376 |
val JN_constrains = thm "JN_constrains"; |
|
377 |
val Join_constrains = thm "Join_constrains"; |
|
378 |
val Join_unless = thm "Join_unless"; |
|
379 |
val Join_constrains_weaken = thm "Join_constrains_weaken"; |
|
380 |
val JN_constrains_weaken = thm "JN_constrains_weaken"; |
|
381 |
val JN_stable = thm "JN_stable"; |
|
382 |
val invariant_JN_I = thm "invariant_JN_I"; |
|
383 |
val Join_stable = thm "Join_stable"; |
|
384 |
val Join_increasing = thm "Join_increasing"; |
|
385 |
val invariant_JoinI = thm "invariant_JoinI"; |
|
386 |
val FP_JN = thm "FP_JN"; |
|
387 |
val JN_transient = thm "JN_transient"; |
|
388 |
val Join_transient = thm "Join_transient"; |
|
389 |
val Join_transient_I1 = thm "Join_transient_I1"; |
|
390 |
val Join_transient_I2 = thm "Join_transient_I2"; |
|
391 |
val JN_ensures = thm "JN_ensures"; |
|
392 |
val Join_ensures = thm "Join_ensures"; |
|
393 |
val stable_Join_constrains = thm "stable_Join_constrains"; |
|
394 |
val stable_Join_Always1 = thm "stable_Join_Always1"; |
|
395 |
val stable_Join_Always2 = thm "stable_Join_Always2"; |
|
396 |
val stable_Join_ensures1 = thm "stable_Join_ensures1"; |
|
397 |
val stable_Join_ensures2 = thm "stable_Join_ensures2"; |
|
398 |
val ok_SKIP1 = thm "ok_SKIP1"; |
|
399 |
val ok_SKIP2 = thm "ok_SKIP2"; |
|
400 |
val ok_Join_commute = thm "ok_Join_commute"; |
|
401 |
val ok_commute = thm "ok_commute"; |
|
402 |
val ok_sym = thm "ok_sym"; |
|
403 |
val ok_iff_OK = thm "ok_iff_OK"; |
|
404 |
val ok_Join_iff1 = thm "ok_Join_iff1"; |
|
405 |
val ok_Join_iff2 = thm "ok_Join_iff2"; |
|
406 |
val ok_Join_commute_I = thm "ok_Join_commute_I"; |
|
407 |
val ok_JN_iff1 = thm "ok_JN_iff1"; |
|
408 |
val ok_JN_iff2 = thm "ok_JN_iff2"; |
|
409 |
val OK_iff_ok = thm "OK_iff_ok"; |
|
410 |
val OK_imp_ok = thm "OK_imp_ok"; |
|
411 |
val Allowed_SKIP = thm "Allowed_SKIP"; |
|
412 |
val Allowed_Join = thm "Allowed_Join"; |
|
413 |
val Allowed_JN = thm "Allowed_JN"; |
|
414 |
val ok_iff_Allowed = thm "ok_iff_Allowed"; |
|
415 |
val OK_iff_Allowed = thm "OK_iff_Allowed"; |
|
416 |
val safety_prop_Acts_iff = thm "safety_prop_Acts_iff"; |
|
417 |
val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed"; |
|
418 |
val Allowed_eq = thm "Allowed_eq"; |
|
419 |
val def_prg_Allowed = thm "def_prg_Allowed"; |
|
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
420 |
val def_total_prg_Allowed = thm "def_total_prg_Allowed"; |
| 13792 | 421 |
val safety_prop_constrains = thm "safety_prop_constrains"; |
422 |
val safety_prop_stable = thm "safety_prop_stable"; |
|
423 |
val safety_prop_Int = thm "safety_prop_Int"; |
|
424 |
val safety_prop_INTER1 = thm "safety_prop_INTER1"; |
|
425 |
val safety_prop_INTER = thm "safety_prop_INTER"; |
|
426 |
val def_UNION_ok_iff = thm "def_UNION_ok_iff"; |
|
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
427 |
val totalize_JN = thm "totalize_JN"; |
| 13792 | 428 |
|
429 |
(*Comp*) |
|
430 |
val preserves_def = thm "preserves_def"; |
|
431 |
val funPair_def = thm "funPair_def"; |
|
432 |
val componentI = thm "componentI"; |
|
433 |
val component_eq_subset = thm "component_eq_subset"; |
|
434 |
val component_SKIP = thm "component_SKIP"; |
|
435 |
val component_refl = thm "component_refl"; |
|
436 |
val SKIP_minimal = thm "SKIP_minimal"; |
|
437 |
val component_Join1 = thm "component_Join1"; |
|
438 |
val component_Join2 = thm "component_Join2"; |
|
439 |
val Join_absorb1 = thm "Join_absorb1"; |
|
440 |
val Join_absorb2 = thm "Join_absorb2"; |
|
441 |
val JN_component_iff = thm "JN_component_iff"; |
|
442 |
val component_JN = thm "component_JN"; |
|
443 |
val component_trans = thm "component_trans"; |
|
444 |
val component_antisym = thm "component_antisym"; |
|
445 |
val Join_component_iff = thm "Join_component_iff"; |
|
446 |
val component_constrains = thm "component_constrains"; |
|
447 |
val program_less_le = thm "program_less_le"; |
|
448 |
val preservesI = thm "preservesI"; |
|
449 |
val preserves_imp_eq = thm "preserves_imp_eq"; |
|
450 |
val Join_preserves = thm "Join_preserves"; |
|
451 |
val JN_preserves = thm "JN_preserves"; |
|
452 |
val SKIP_preserves = thm "SKIP_preserves"; |
|
453 |
val funPair_apply = thm "funPair_apply"; |
|
454 |
val preserves_funPair = thm "preserves_funPair"; |
|
455 |
val funPair_o_distrib = thm "funPair_o_distrib"; |
|
456 |
val fst_o_funPair = thm "fst_o_funPair"; |
|
457 |
val snd_o_funPair = thm "snd_o_funPair"; |
|
458 |
val subset_preserves_o = thm "subset_preserves_o"; |
|
459 |
val preserves_subset_stable = thm "preserves_subset_stable"; |
|
460 |
val preserves_subset_increasing = thm "preserves_subset_increasing"; |
|
461 |
val preserves_id_subset_stable = thm "preserves_id_subset_stable"; |
|
462 |
val safety_prop_preserves = thm "safety_prop_preserves"; |
|
463 |
val stable_localTo_stable2 = thm "stable_localTo_stable2"; |
|
464 |
val Increasing_preserves_Stable = thm "Increasing_preserves_Stable"; |
|
465 |
val component_of_imp_component = thm "component_of_imp_component"; |
|
466 |
val component_of_refl = thm "component_of_refl"; |
|
467 |
val component_of_SKIP = thm "component_of_SKIP"; |
|
468 |
val component_of_trans = thm "component_of_trans"; |
|
469 |
val strict_component_of_eq = thm "strict_component_of_eq"; |
|
470 |
val localize_Init_eq = thm "localize_Init_eq"; |
|
471 |
val localize_Acts_eq = thm "localize_Acts_eq"; |
|
472 |
val localize_AllowedActs_eq = thm "localize_AllowedActs_eq"; |
|
473 |
||
474 |
(*Guar*) |
|
475 |
val guar_def = thm "guar_def"; |
|
476 |
val OK_insert_iff = thm "OK_insert_iff"; |
|
477 |
val ex1 = thm "ex1"; |
|
478 |
val ex2 = thm "ex2"; |
|
479 |
val ex_prop_finite = thm "ex_prop_finite"; |
|
480 |
val ex_prop_equiv = thm "ex_prop_equiv"; |
|
481 |
val uv1 = thm "uv1"; |
|
482 |
val uv2 = thm "uv2"; |
|
483 |
val uv_prop_finite = thm "uv_prop_finite"; |
|
484 |
val guaranteesI = thm "guaranteesI"; |
|
485 |
val guaranteesD = thm "guaranteesD"; |
|
486 |
val component_guaranteesD = thm "component_guaranteesD"; |
|
487 |
val guarantees_weaken = thm "guarantees_weaken"; |
|
488 |
val subset_imp_guarantees_UNIV = thm "subset_imp_guarantees_UNIV"; |
|
489 |
val subset_imp_guarantees = thm "subset_imp_guarantees"; |
|
490 |
val ex_prop_imp = thm "ex_prop_imp"; |
|
491 |
val guarantees_imp = thm "guarantees_imp"; |
|
492 |
val ex_prop_equiv2 = thm "ex_prop_equiv2"; |
|
493 |
val guarantees_UN_left = thm "guarantees_UN_left"; |
|
494 |
val guarantees_Un_left = thm "guarantees_Un_left"; |
|
495 |
val guarantees_INT_right = thm "guarantees_INT_right"; |
|
496 |
val guarantees_Int_right = thm "guarantees_Int_right"; |
|
497 |
val guarantees_Int_right_I = thm "guarantees_Int_right_I"; |
|
498 |
val guarantees_INT_right_iff = thm "guarantees_INT_right_iff"; |
|
499 |
val shunting = thm "shunting"; |
|
500 |
val contrapositive = thm "contrapositive"; |
|
501 |
val combining1 = thm "combining1"; |
|
502 |
val combining2 = thm "combining2"; |
|
503 |
val all_guarantees = thm "all_guarantees"; |
|
504 |
val ex_guarantees = thm "ex_guarantees"; |
|
505 |
val guarantees_Join_Int = thm "guarantees_Join_Int"; |
|
506 |
val guarantees_Join_Un = thm "guarantees_Join_Un"; |
|
507 |
val guarantees_JN_INT = thm "guarantees_JN_INT"; |
|
508 |
val guarantees_JN_UN = thm "guarantees_JN_UN"; |
|
509 |
val guarantees_Join_I1 = thm "guarantees_Join_I1"; |
|
510 |
val guarantees_Join_I2 = thm "guarantees_Join_I2"; |
|
511 |
val guarantees_JN_I = thm "guarantees_JN_I"; |
|
512 |
val Join_welldef_D1 = thm "Join_welldef_D1"; |
|
513 |
val Join_welldef_D2 = thm "Join_welldef_D2"; |
|
514 |
val refines_refl = thm "refines_refl"; |
|
515 |
val ex_refinement_thm = thm "ex_refinement_thm"; |
|
516 |
val uv_refinement_thm = thm "uv_refinement_thm"; |
|
517 |
val guarantees_equiv = thm "guarantees_equiv"; |
|
518 |
val wg_weakest = thm "wg_weakest"; |
|
519 |
val wg_guarantees = thm "wg_guarantees"; |
|
520 |
val wg_equiv = thm "wg_equiv"; |
|
521 |
val component_of_wg = thm "component_of_wg"; |
|
522 |
val wg_finite = thm "wg_finite"; |
|
523 |
val wg_ex_prop = thm "wg_ex_prop"; |
|
524 |
val wx_subset = thm "wx_subset"; |
|
525 |
val wx_ex_prop = thm "wx_ex_prop"; |
|
526 |
val wx_weakest = thm "wx_weakest"; |
|
527 |
val wx'_ex_prop = thm "wx'_ex_prop"; |
|
528 |
val wx_equiv = thm "wx_equiv"; |
|
529 |
val guarantees_wx_eq = thm "guarantees_wx_eq"; |
|
530 |
val stable_guarantees_Always = thm "stable_guarantees_Always"; |
|
531 |
val leadsTo_Basis = thm "leadsTo_Basis"; |
|
532 |
val constrains_guarantees_leadsTo = thm "constrains_guarantees_leadsTo"; |
|
533 |
||
| 13790 | 534 |
(*Extend*) |
535 |
val Restrict_iff = thm "Restrict_iff"; |
|
536 |
val Restrict_UNIV = thm "Restrict_UNIV"; |
|
537 |
val Restrict_empty = thm "Restrict_empty"; |
|
538 |
val Restrict_Int = thm "Restrict_Int"; |
|
539 |
val Restrict_triv = thm "Restrict_triv"; |
|
540 |
val Restrict_subset = thm "Restrict_subset"; |
|
541 |
val Restrict_eq_mono = thm "Restrict_eq_mono"; |
|
542 |
val Restrict_imageI = thm "Restrict_imageI"; |
|
543 |
val Domain_Restrict = thm "Domain_Restrict"; |
|
544 |
val Image_Restrict = thm "Image_Restrict"; |
|
545 |
val insert_Id_image_Acts = thm "insert_Id_image_Acts"; |
|
546 |
val good_mapI = thm "good_mapI"; |
|
547 |
val good_map_is_surj = thm "good_map_is_surj"; |
|
548 |
val fst_inv_equalityI = thm "fst_inv_equalityI"; |
|
549 |
val project_set_iff = thm "project_set_iff"; |
|
550 |
val extend_set_mono = thm "extend_set_mono"; |
|
551 |
val extend_set_empty = thm "extend_set_empty"; |
|
552 |
val project_set_Int_subset = thm "project_set_Int_subset"; |
|
553 |
val Init_extend = thm "Init_extend"; |
|
554 |
val Init_project = thm "Init_project"; |
|
555 |
val Acts_project = thm "Acts_project"; |
|
556 |
val project_set_UNIV = thm "project_set_UNIV"; |
|
557 |
val project_set_Union = thm "project_set_Union"; |
|
558 |
val project_act_mono = thm "project_act_mono"; |
|
559 |
val project_constrains_project_set = thm "project_constrains_project_set"; |
|
560 |
val project_stable_project_set = thm "project_stable_project_set"; |
|
561 |
||
562 |
||
563 |
(*Rename*) |
|
564 |
val good_map_bij = thm "good_map_bij"; |
|
565 |
val fst_o_inv_eq_inv = thm "fst_o_inv_eq_inv"; |
|
566 |
val mem_rename_set_iff = thm "mem_rename_set_iff"; |
|
567 |
val extend_set_eq_image = thm "extend_set_eq_image"; |
|
568 |
val Init_rename = thm "Init_rename"; |
|
569 |
val extend_set_inv = thm "extend_set_inv"; |
|
570 |
val bij_extend_act_eq_project_act = thm "bij_extend_act_eq_project_act"; |
|
571 |
val bij_extend_act = thm "bij_extend_act"; |
|
572 |
val bij_project_act = thm "bij_project_act"; |
|
573 |
val bij_inv_project_act_eq = thm "bij_inv_project_act_eq"; |
|
574 |
val Acts_project = thm "Acts_project"; |
|
575 |
val extend_inv = thm "extend_inv"; |
|
576 |
val rename_inv_rename = thm "rename_inv_rename"; |
|
577 |
val rename_rename_inv = thm "rename_rename_inv"; |
|
578 |
val rename_inv_eq = thm "rename_inv_eq"; |
|
579 |
val bij_extend = thm "bij_extend"; |
|
580 |
val bij_project = thm "bij_project"; |
|
581 |
val inv_project_eq = thm "inv_project_eq"; |
|
582 |
val Allowed_rename = thm "Allowed_rename"; |
|
583 |
val bij_rename = thm "bij_rename"; |
|
584 |
val surj_rename = thm "surj_rename"; |
|
585 |
val inj_rename_imp_inj = thm "inj_rename_imp_inj"; |
|
586 |
val surj_rename_imp_surj = thm "surj_rename_imp_surj"; |
|
587 |
val bij_rename_imp_bij = thm "bij_rename_imp_bij"; |
|
588 |
val bij_rename_iff = thm "bij_rename_iff"; |
|
589 |
val rename_SKIP = thm "rename_SKIP"; |
|
590 |
val rename_Join = thm "rename_Join"; |
|
591 |
val rename_JN = thm "rename_JN"; |
|
592 |
val rename_constrains = thm "rename_constrains"; |
|
593 |
val rename_stable = thm "rename_stable"; |
|
594 |
val rename_invariant = thm "rename_invariant"; |
|
595 |
val rename_increasing = thm "rename_increasing"; |
|
596 |
val reachable_rename_eq = thm "reachable_rename_eq"; |
|
597 |
val rename_Constrains = thm "rename_Constrains"; |
|
598 |
val rename_Stable = thm "rename_Stable"; |
|
599 |
val rename_Always = thm "rename_Always"; |
|
600 |
val rename_Increasing = thm "rename_Increasing"; |
|
601 |
val rename_transient = thm "rename_transient"; |
|
602 |
val rename_ensures = thm "rename_ensures"; |
|
603 |
val rename_leadsTo = thm "rename_leadsTo"; |
|
604 |
val rename_LeadsTo = thm "rename_LeadsTo"; |
|
605 |
val rename_rename_guarantees_eq = thm "rename_rename_guarantees_eq"; |
|
606 |
val rename_guarantees_eq_rename_inv = thm "rename_guarantees_eq_rename_inv"; |
|
607 |
val rename_preserves = thm "rename_preserves"; |
|
608 |
val ok_rename_iff = thm "ok_rename_iff"; |
|
609 |
val OK_rename_iff = thm "OK_rename_iff"; |
|
610 |
val bij_eq_rename = thm "bij_eq_rename"; |
|
611 |
val rename_image_constrains = thm "rename_image_constrains"; |
|
612 |
val rename_image_stable = thm "rename_image_stable"; |
|
613 |
val rename_image_increasing = thm "rename_image_increasing"; |
|
614 |
val rename_image_invariant = thm "rename_image_invariant"; |
|
615 |
val rename_image_Constrains = thm "rename_image_Constrains"; |
|
616 |
val rename_image_preserves = thm "rename_image_preserves"; |
|
617 |
val rename_image_Stable = thm "rename_image_Stable"; |
|
618 |
val rename_image_Increasing = thm "rename_image_Increasing"; |
|
619 |
val rename_image_Always = thm "rename_image_Always"; |
|
620 |
val rename_image_leadsTo = thm "rename_image_leadsTo"; |
|
621 |
val rename_image_LeadsTo = thm "rename_image_LeadsTo"; |
|
622 |
||
623 |
||
| 13786 | 624 |
|
625 |
(*Lift_prog*) |
|
626 |
val sub_def = thm "sub_def"; |
|
627 |
val lift_map_def = thm "lift_map_def"; |
|
628 |
val drop_map_def = thm "drop_map_def"; |
|
629 |
val insert_map_inverse = thm "insert_map_inverse"; |
|
630 |
val insert_map_delete_map_eq = thm "insert_map_delete_map_eq"; |
|
631 |
val insert_map_inject1 = thm "insert_map_inject1"; |
|
632 |
val insert_map_inject2 = thm "insert_map_inject2"; |
|
633 |
val insert_map_inject = thm "insert_map_inject"; |
|
634 |
val insert_map_inject = thm "insert_map_inject"; |
|
635 |
val lift_map_eq_iff = thm "lift_map_eq_iff"; |
|
636 |
val drop_map_lift_map_eq = thm "drop_map_lift_map_eq"; |
|
637 |
val inj_lift_map = thm "inj_lift_map"; |
|
638 |
val lift_map_drop_map_eq = thm "lift_map_drop_map_eq"; |
|
639 |
val drop_map_inject = thm "drop_map_inject"; |
|
640 |
val surj_lift_map = thm "surj_lift_map"; |
|
641 |
val bij_lift_map = thm "bij_lift_map"; |
|
642 |
val inv_lift_map_eq = thm "inv_lift_map_eq"; |
|
643 |
val inv_drop_map_eq = thm "inv_drop_map_eq"; |
|
644 |
val bij_drop_map = thm "bij_drop_map"; |
|
645 |
val sub_apply = thm "sub_apply"; |
|
646 |
val lift_set_empty = thm "lift_set_empty"; |
|
647 |
val lift_set_iff = thm "lift_set_iff"; |
|
648 |
val lift_set_iff2 = thm "lift_set_iff2"; |
|
649 |
val lift_set_mono = thm "lift_set_mono"; |
|
650 |
val lift_set_Un_distrib = thm "lift_set_Un_distrib"; |
|
651 |
val lift_set_Diff_distrib = thm "lift_set_Diff_distrib"; |
|
652 |
val bij_lift = thm "bij_lift"; |
|
653 |
val lift_SKIP = thm "lift_SKIP"; |
|
654 |
val lift_Join = thm "lift_Join"; |
|
655 |
val lift_JN = thm "lift_JN"; |
|
656 |
val lift_constrains = thm "lift_constrains"; |
|
657 |
val lift_stable = thm "lift_stable"; |
|
658 |
val lift_invariant = thm "lift_invariant"; |
|
659 |
val lift_Constrains = thm "lift_Constrains"; |
|
660 |
val lift_Stable = thm "lift_Stable"; |
|
661 |
val lift_Always = thm "lift_Always"; |
|
662 |
val lift_transient = thm "lift_transient"; |
|
663 |
val lift_ensures = thm "lift_ensures"; |
|
664 |
val lift_leadsTo = thm "lift_leadsTo"; |
|
665 |
val lift_LeadsTo = thm "lift_LeadsTo"; |
|
666 |
val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq"; |
|
667 |
val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv"; |
|
668 |
val lift_preserves_snd_I = thm "lift_preserves_snd_I"; |
|
669 |
val delete_map_eqE = thm "delete_map_eqE"; |
|
670 |
val delete_map_eqE = thm "delete_map_eqE"; |
|
671 |
val delete_map_neq_apply = thm "delete_map_neq_apply"; |
|
672 |
val vimage_o_fst_eq = thm "vimage_o_fst_eq"; |
|
673 |
val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set"; |
|
674 |
val mem_lift_act_iff = thm "mem_lift_act_iff"; |
|
675 |
val preserves_snd_lift_stable = thm "preserves_snd_lift_stable"; |
|
676 |
val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains"; |
|
677 |
val lift_map_image_Times = thm "lift_map_image_Times"; |
|
678 |
val lift_preserves_eq = thm "lift_preserves_eq"; |
|
679 |
val lift_preserves_sub = thm "lift_preserves_sub"; |
|
680 |
val o_equiv_assoc = thm "o_equiv_assoc"; |
|
681 |
val o_equiv_apply = thm "o_equiv_apply"; |
|
682 |
val fst_o_lift_map = thm "fst_o_lift_map"; |
|
683 |
val snd_o_lift_map = thm "snd_o_lift_map"; |
|
684 |
val extend_act_extend_act = thm "extend_act_extend_act"; |
|
685 |
val project_act_project_act = thm "project_act_project_act"; |
|
686 |
val project_act_extend_act = thm "project_act_extend_act"; |
|
687 |
val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst"; |
|
688 |
val UNION_OK_lift_I = thm "UNION_OK_lift_I"; |
|
689 |
val OK_lift_I = thm "OK_lift_I"; |
|
690 |
val Allowed_lift = thm "Allowed_lift"; |
|
691 |
val lift_image_preserves = thm "lift_image_preserves"; |
|
692 |
||
693 |
||
694 |
(*PPROD*) |
|
695 |
val Init_PLam = thm "Init_PLam"; |
|
696 |
val PLam_empty = thm "PLam_empty"; |
|
697 |
val PLam_SKIP = thm "PLam_SKIP"; |
|
698 |
val PLam_insert = thm "PLam_insert"; |
|
699 |
val PLam_component_iff = thm "PLam_component_iff"; |
|
700 |
val component_PLam = thm "component_PLam"; |
|
701 |
val PLam_constrains = thm "PLam_constrains"; |
|
702 |
val PLam_stable = thm "PLam_stable"; |
|
703 |
val PLam_transient = thm "PLam_transient"; |
|
704 |
val PLam_ensures = thm "PLam_ensures"; |
|
705 |
val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis"; |
|
706 |
val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant"; |
|
707 |
val PLam_preserves_fst = thm "PLam_preserves_fst"; |
|
708 |
val PLam_preserves_snd = thm "PLam_preserves_snd"; |
|
709 |
val guarantees_PLam_I = thm "guarantees_PLam_I"; |
|
710 |
val Allowed_PLam = thm "Allowed_PLam"; |
|
711 |
val PLam_preserves = thm "PLam_preserves"; |
|
712 |
||
| 13796 | 713 |
(*Follows*) |
714 |
val mono_Always_o = thm "mono_Always_o"; |
|
715 |
val mono_LeadsTo_o = thm "mono_LeadsTo_o"; |
|
716 |
val Follows_constant = thm "Follows_constant"; |
|
717 |
val mono_Follows_o = thm "mono_Follows_o"; |
|
718 |
val mono_Follows_apply = thm "mono_Follows_apply"; |
|
719 |
val Follows_trans = thm "Follows_trans"; |
|
720 |
val Follows_Increasing1 = thm "Follows_Increasing1"; |
|
721 |
val Follows_Increasing2 = thm "Follows_Increasing2"; |
|
722 |
val Follows_Bounded = thm "Follows_Bounded"; |
|
723 |
val Follows_LeadsTo = thm "Follows_LeadsTo"; |
|
724 |
val Follows_LeadsTo_pfixLe = thm "Follows_LeadsTo_pfixLe"; |
|
725 |
val Follows_LeadsTo_pfixGe = thm "Follows_LeadsTo_pfixGe"; |
|
726 |
val Always_Follows1 = thm "Always_Follows1"; |
|
727 |
val Always_Follows2 = thm "Always_Follows2"; |
|
728 |
val increasing_Un = thm "increasing_Un"; |
|
729 |
val Increasing_Un = thm "Increasing_Un"; |
|
730 |
val Always_Un = thm "Always_Un"; |
|
731 |
val Follows_Un = thm "Follows_Un"; |
|
732 |
val increasing_union = thm "increasing_union"; |
|
733 |
val Increasing_union = thm "Increasing_union"; |
|
734 |
val Always_union = thm "Always_union"; |
|
735 |
val Follows_union = thm "Follows_union"; |
|
736 |
val Follows_setsum = thm "Follows_setsum"; |
|
737 |
val Increasing_imp_Stable_pfixGe = thm "Increasing_imp_Stable_pfixGe"; |
|
738 |
val LeadsTo_le_imp_pfixGe = thm "LeadsTo_le_imp_pfixGe"; |
|
739 |
||
| 13786 | 740 |
|
| 13797 | 741 |
(*Lazy unfolding of actions or of sets*) |
742 |
fun simp_of_act def = def RS def_act_simp; |
|
743 |
||
744 |
fun simp_of_set def = def RS def_set_simp; |
|
745 |
||
746 |
||
747 |
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*) |
|
748 |
val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin |
|
749 |
||
750 |
(*Combines a list of invariance THEOREMS into one.*) |
|
751 |
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I) |
|
752 |
||
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
753 |
(*Proves "co" properties when the program is specified. Any use of invariants |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
754 |
(from weak constrains) must have been done already.*) |
| 13786 | 755 |
fun gen_constrains_tac(cs,ss) i = |
756 |
SELECT_GOAL |
|
757 |
(EVERY [REPEAT (Always_Int_tac 1), |
|
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
758 |
(*reduce the fancy safety properties to "constrains"*) |
| 13786 | 759 |
REPEAT (etac Always_ConstrainsI 1 |
760 |
ORELSE |
|
761 |
resolve_tac [StableI, stableI, |
|
762 |
constrains_imp_Constrains] 1), |
|
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
763 |
(*for safety, the totalize operator can be ignored*) |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
764 |
simp_tac (HOL_ss addsimps |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
765 |
[mk_total_program_def, totalize_constrains_iff]) 1, |
| 13786 | 766 |
rtac constrainsI 1, |
767 |
full_simp_tac ss 1, |
|
768 |
REPEAT (FIRSTGOAL (etac disjE)), |
|
769 |
ALLGOALS (clarify_tac cs), |
|
770 |
ALLGOALS (asm_lr_simp_tac ss)]) i; |
|
771 |
||
772 |
(*proves "ensures/leadsTo" properties when the program is specified*) |
|
773 |
fun gen_ensures_tac(cs,ss) sact = |
|
774 |
SELECT_GOAL |
|
775 |
(EVERY [REPEAT (Always_Int_tac 1), |
|
776 |
etac Always_LeadsTo_Basis 1 |
|
777 |
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
|
778 |
REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis, |
|
779 |
EnsuresI, ensuresI] 1), |
|
780 |
(*now there are two subgoals: co & transient*) |
|
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
781 |
simp_tac (ss addsimps [mk_total_program_def]) 2, |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
782 |
res_inst_tac [("act", sact)] totalize_transientI 2
|
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
783 |
ORELSE res_inst_tac [("act", sact)] transientI 2,
|
| 13786 | 784 |
(*simplify the command's domain*) |
785 |
simp_tac (ss addsimps [Domain_def]) 3, |
|
786 |
gen_constrains_tac (cs,ss) 1, |
|
787 |
ALLGOALS (clarify_tac cs), |
|
788 |
ALLGOALS (asm_lr_simp_tac ss)]); |
|
789 |
||
| 13797 | 790 |
fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st; |
791 |
||
| 13796 | 792 |
fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact; |
793 |
||
| 13786 | 794 |
|
795 |
(*Composition equivalences, from Lift_prog*) |
|
796 |
||
797 |
fun make_o_equivs th = |
|
798 |
[th, |
|
799 |
th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]), |
|
800 |
th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])]; |
|
801 |
||
802 |
Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair); |
|
803 |
||
804 |
Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map); |