1 (* Title: HOL/UNITY/UNITY_tactics.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 2003 University of Cambridge
6 Specialized UNITY tactics, and ML bindings of theorems
10 val Restrict_iff = thm "Restrict_iff";
11 val Restrict_UNIV = thm "Restrict_UNIV";
12 val Restrict_empty = thm "Restrict_empty";
13 val Restrict_Int = thm "Restrict_Int";
14 val Restrict_triv = thm "Restrict_triv";
15 val Restrict_subset = thm "Restrict_subset";
16 val Restrict_eq_mono = thm "Restrict_eq_mono";
17 val Restrict_imageI = thm "Restrict_imageI";
18 val Domain_Restrict = thm "Domain_Restrict";
19 val Image_Restrict = thm "Image_Restrict";
20 val insert_Id_image_Acts = thm "insert_Id_image_Acts";
21 val good_mapI = thm "good_mapI";
22 val good_map_is_surj = thm "good_map_is_surj";
23 val fst_inv_equalityI = thm "fst_inv_equalityI";
24 val project_set_iff = thm "project_set_iff";
25 val extend_set_mono = thm "extend_set_mono";
26 val extend_set_empty = thm "extend_set_empty";
27 val project_set_Int_subset = thm "project_set_Int_subset";
28 val Init_extend = thm "Init_extend";
29 val Init_project = thm "Init_project";
30 val Acts_project = thm "Acts_project";
31 val project_set_UNIV = thm "project_set_UNIV";
32 val project_set_Union = thm "project_set_Union";
33 val project_act_mono = thm "project_act_mono";
34 val project_constrains_project_set = thm "project_constrains_project_set";
35 val project_stable_project_set = thm "project_stable_project_set";
39 val good_map_bij = thm "good_map_bij";
40 val fst_o_inv_eq_inv = thm "fst_o_inv_eq_inv";
41 val mem_rename_set_iff = thm "mem_rename_set_iff";
42 val extend_set_eq_image = thm "extend_set_eq_image";
43 val Init_rename = thm "Init_rename";
44 val extend_set_inv = thm "extend_set_inv";
45 val bij_extend_act_eq_project_act = thm "bij_extend_act_eq_project_act";
46 val bij_extend_act = thm "bij_extend_act";
47 val bij_project_act = thm "bij_project_act";
48 val bij_inv_project_act_eq = thm "bij_inv_project_act_eq";
49 val Acts_project = thm "Acts_project";
50 val extend_inv = thm "extend_inv";
51 val rename_inv_rename = thm "rename_inv_rename";
52 val rename_rename_inv = thm "rename_rename_inv";
53 val rename_inv_eq = thm "rename_inv_eq";
54 val bij_extend = thm "bij_extend";
55 val bij_project = thm "bij_project";
56 val inv_project_eq = thm "inv_project_eq";
57 val Allowed_rename = thm "Allowed_rename";
58 val bij_rename = thm "bij_rename";
59 val surj_rename = thm "surj_rename";
60 val inj_rename_imp_inj = thm "inj_rename_imp_inj";
61 val surj_rename_imp_surj = thm "surj_rename_imp_surj";
62 val bij_rename_imp_bij = thm "bij_rename_imp_bij";
63 val bij_rename_iff = thm "bij_rename_iff";
64 val rename_SKIP = thm "rename_SKIP";
65 val rename_Join = thm "rename_Join";
66 val rename_JN = thm "rename_JN";
67 val rename_constrains = thm "rename_constrains";
68 val rename_stable = thm "rename_stable";
69 val rename_invariant = thm "rename_invariant";
70 val rename_increasing = thm "rename_increasing";
71 val reachable_rename_eq = thm "reachable_rename_eq";
72 val rename_Constrains = thm "rename_Constrains";
73 val rename_Stable = thm "rename_Stable";
74 val rename_Always = thm "rename_Always";
75 val rename_Increasing = thm "rename_Increasing";
76 val rename_transient = thm "rename_transient";
77 val rename_ensures = thm "rename_ensures";
78 val rename_leadsTo = thm "rename_leadsTo";
79 val rename_LeadsTo = thm "rename_LeadsTo";
80 val rename_rename_guarantees_eq = thm "rename_rename_guarantees_eq";
81 val rename_guarantees_eq_rename_inv = thm "rename_guarantees_eq_rename_inv";
82 val rename_preserves = thm "rename_preserves";
83 val ok_rename_iff = thm "ok_rename_iff";
84 val OK_rename_iff = thm "OK_rename_iff";
85 val bij_eq_rename = thm "bij_eq_rename";
86 val rename_image_constrains = thm "rename_image_constrains";
87 val rename_image_stable = thm "rename_image_stable";
88 val rename_image_increasing = thm "rename_image_increasing";
89 val rename_image_invariant = thm "rename_image_invariant";
90 val rename_image_Constrains = thm "rename_image_Constrains";
91 val rename_image_preserves = thm "rename_image_preserves";
92 val rename_image_Stable = thm "rename_image_Stable";
93 val rename_image_Increasing = thm "rename_image_Increasing";
94 val rename_image_Always = thm "rename_image_Always";
95 val rename_image_leadsTo = thm "rename_image_leadsTo";
96 val rename_image_LeadsTo = thm "rename_image_LeadsTo";
101 val sub_def = thm "sub_def";
102 val lift_map_def = thm "lift_map_def";
103 val drop_map_def = thm "drop_map_def";
104 val insert_map_inverse = thm "insert_map_inverse";
105 val insert_map_delete_map_eq = thm "insert_map_delete_map_eq";
106 val insert_map_inject1 = thm "insert_map_inject1";
107 val insert_map_inject2 = thm "insert_map_inject2";
108 val insert_map_inject = thm "insert_map_inject";
109 val insert_map_inject = thm "insert_map_inject";
110 val lift_map_eq_iff = thm "lift_map_eq_iff";
111 val drop_map_lift_map_eq = thm "drop_map_lift_map_eq";
112 val inj_lift_map = thm "inj_lift_map";
113 val lift_map_drop_map_eq = thm "lift_map_drop_map_eq";
114 val drop_map_inject = thm "drop_map_inject";
115 val surj_lift_map = thm "surj_lift_map";
116 val bij_lift_map = thm "bij_lift_map";
117 val inv_lift_map_eq = thm "inv_lift_map_eq";
118 val inv_drop_map_eq = thm "inv_drop_map_eq";
119 val bij_drop_map = thm "bij_drop_map";
120 val sub_apply = thm "sub_apply";
121 val lift_set_empty = thm "lift_set_empty";
122 val lift_set_iff = thm "lift_set_iff";
123 val lift_set_iff2 = thm "lift_set_iff2";
124 val lift_set_mono = thm "lift_set_mono";
125 val lift_set_Un_distrib = thm "lift_set_Un_distrib";
126 val lift_set_Diff_distrib = thm "lift_set_Diff_distrib";
127 val bij_lift = thm "bij_lift";
128 val lift_SKIP = thm "lift_SKIP";
129 val lift_Join = thm "lift_Join";
130 val lift_JN = thm "lift_JN";
131 val lift_constrains = thm "lift_constrains";
132 val lift_stable = thm "lift_stable";
133 val lift_invariant = thm "lift_invariant";
134 val lift_Constrains = thm "lift_Constrains";
135 val lift_Stable = thm "lift_Stable";
136 val lift_Always = thm "lift_Always";
137 val lift_transient = thm "lift_transient";
138 val lift_ensures = thm "lift_ensures";
139 val lift_leadsTo = thm "lift_leadsTo";
140 val lift_LeadsTo = thm "lift_LeadsTo";
141 val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq";
142 val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv";
143 val lift_preserves_snd_I = thm "lift_preserves_snd_I";
144 val delete_map_eqE = thm "delete_map_eqE";
145 val delete_map_eqE = thm "delete_map_eqE";
146 val delete_map_neq_apply = thm "delete_map_neq_apply";
147 val vimage_o_fst_eq = thm "vimage_o_fst_eq";
148 val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set";
149 val mem_lift_act_iff = thm "mem_lift_act_iff";
150 val preserves_snd_lift_stable = thm "preserves_snd_lift_stable";
151 val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains";
152 val insert_map_upd_same = thm "insert_map_upd_same";
153 val insert_map_upd = thm "insert_map_upd";
154 val insert_map_eq_diff = thm "insert_map_eq_diff";
155 val lift_map_eq_diff = thm "lift_map_eq_diff";
156 val lift_transient_eq_disj = thm "lift_transient_eq_disj";
157 val lift_map_image_Times = thm "lift_map_image_Times";
158 val lift_preserves_eq = thm "lift_preserves_eq";
159 val lift_preserves_sub = thm "lift_preserves_sub";
160 val o_equiv_assoc = thm "o_equiv_assoc";
161 val o_equiv_apply = thm "o_equiv_apply";
162 val fst_o_lift_map = thm "fst_o_lift_map";
163 val snd_o_lift_map = thm "snd_o_lift_map";
164 val extend_act_extend_act = thm "extend_act_extend_act";
165 val project_act_project_act = thm "project_act_project_act";
166 val project_act_extend_act = thm "project_act_extend_act";
167 val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst";
168 val UNION_OK_lift_I = thm "UNION_OK_lift_I";
169 val OK_lift_I = thm "OK_lift_I";
170 val Allowed_lift = thm "Allowed_lift";
171 val lift_image_preserves = thm "lift_image_preserves";
175 val Init_PLam = thm "Init_PLam";
176 val PLam_empty = thm "PLam_empty";
177 val PLam_SKIP = thm "PLam_SKIP";
178 val PLam_insert = thm "PLam_insert";
179 val PLam_component_iff = thm "PLam_component_iff";
180 val component_PLam = thm "component_PLam";
181 val PLam_constrains = thm "PLam_constrains";
182 val PLam_stable = thm "PLam_stable";
183 val PLam_transient = thm "PLam_transient";
184 val PLam_ensures = thm "PLam_ensures";
185 val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis";
186 val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant";
187 val PLam_preserves_fst = thm "PLam_preserves_fst";
188 val PLam_preserves_snd = thm "PLam_preserves_snd";
189 val guarantees_PLam_I = thm "guarantees_PLam_I";
190 val Allowed_PLam = thm "Allowed_PLam";
191 val PLam_preserves = thm "PLam_preserves";
194 (*proves "co" properties when the program is specified*)
195 fun gen_constrains_tac(cs,ss) i =
197 (EVERY [REPEAT (Always_Int_tac 1),
198 REPEAT (etac Always_ConstrainsI 1
200 resolve_tac [StableI, stableI,
201 constrains_imp_Constrains] 1),
204 REPEAT (FIRSTGOAL (etac disjE)),
205 ALLGOALS (clarify_tac cs),
206 ALLGOALS (asm_lr_simp_tac ss)]) i;
208 (*proves "ensures/leadsTo" properties when the program is specified*)
209 fun gen_ensures_tac(cs,ss) sact =
211 (EVERY [REPEAT (Always_Int_tac 1),
212 etac Always_LeadsTo_Basis 1
213 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
214 REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
215 EnsuresI, ensuresI] 1),
216 (*now there are two subgoals: co & transient*)
218 res_inst_tac [("act", sact)] transientI 2,
219 (*simplify the command's domain*)
220 simp_tac (ss addsimps [Domain_def]) 3,
221 gen_constrains_tac (cs,ss) 1,
222 ALLGOALS (clarify_tac cs),
223 ALLGOALS (asm_lr_simp_tac ss)]);
226 (*Composition equivalences, from Lift_prog*)
228 fun make_o_equivs th =
230 th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]),
231 th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
233 Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
235 Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);