src/HOL/UNITY/UNITY_tactics.ML
changeset 24147 edc90be09ac1
parent 21669 c68717c16013
child 27208 5fe899199f85
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Fri Aug 03 16:28:25 2007 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri Aug 03 20:19:41 2007 +0200
     1.3 @@ -3,803 +3,60 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   2003  University of Cambridge
     1.6  
     1.7 -Specialized UNITY tactics, and ML bindings of theorems
     1.8 +Specialized UNITY tactics.
     1.9  *)
    1.10  
    1.11 -(*ListOrder*)
    1.12 -val Domain_def = thm "Domain_def";
    1.13 -val Le_def = thm "Le_def";
    1.14 -val Ge_def = thm "Ge_def";
    1.15 -val prefix_def = thm "prefix_def";
    1.16 -val Nil_genPrefix = thm "Nil_genPrefix";
    1.17 -val genPrefix_length_le = thm "genPrefix_length_le";
    1.18 -val cons_genPrefixE = thm "cons_genPrefixE";
    1.19 -val Cons_genPrefix_Cons = thm "Cons_genPrefix_Cons";
    1.20 -val refl_genPrefix = thm "refl_genPrefix";
    1.21 -val genPrefix_refl = thm "genPrefix_refl";
    1.22 -val genPrefix_mono = thm "genPrefix_mono";
    1.23 -val append_genPrefix = thm "append_genPrefix";
    1.24 -val genPrefix_trans_O = thm "genPrefix_trans_O";
    1.25 -val genPrefix_trans = thm "genPrefix_trans";
    1.26 -val prefix_genPrefix_trans = thm "prefix_genPrefix_trans";
    1.27 -val genPrefix_prefix_trans = thm "genPrefix_prefix_trans";
    1.28 -val trans_genPrefix = thm "trans_genPrefix";
    1.29 -val genPrefix_antisym = thm "genPrefix_antisym";
    1.30 -val antisym_genPrefix = thm "antisym_genPrefix";
    1.31 -val genPrefix_Nil = thm "genPrefix_Nil";
    1.32 -val same_genPrefix_genPrefix = thm "same_genPrefix_genPrefix";
    1.33 -val genPrefix_Cons = thm "genPrefix_Cons";
    1.34 -val genPrefix_take_append = thm "genPrefix_take_append";
    1.35 -val genPrefix_append_both = thm "genPrefix_append_both";
    1.36 -val append_cons_eq = thm "append_cons_eq";
    1.37 -val append_one_genPrefix = thm "append_one_genPrefix";
    1.38 -val genPrefix_imp_nth = thm "genPrefix_imp_nth";
    1.39 -val nth_imp_genPrefix = thm "nth_imp_genPrefix";
    1.40 -val genPrefix_iff_nth = thm "genPrefix_iff_nth";
    1.41 -val prefix_refl = thm "prefix_refl";
    1.42 -val prefix_trans = thm "prefix_trans";
    1.43 -val prefix_antisym = thm "prefix_antisym";
    1.44 -val prefix_less_le = thm "prefix_less_le";
    1.45 -val set_mono = thm "set_mono";
    1.46 -val Nil_prefix = thm "Nil_prefix";
    1.47 -val prefix_Nil = thm "prefix_Nil";
    1.48 -val Cons_prefix_Cons = thm "Cons_prefix_Cons";
    1.49 -val same_prefix_prefix = thm "same_prefix_prefix";
    1.50 -val append_prefix = thm "append_prefix";
    1.51 -val prefix_appendI = thm "prefix_appendI";
    1.52 -val prefix_Cons = thm "prefix_Cons";
    1.53 -val append_one_prefix = thm "append_one_prefix";
    1.54 -val prefix_length_le = thm "prefix_length_le";
    1.55 -val strict_prefix_length_less = thm "strict_prefix_length_less";
    1.56 -val mono_length = thm "mono_length";
    1.57 -val prefix_iff = thm "prefix_iff";
    1.58 -val prefix_snoc = thm "prefix_snoc";
    1.59 -val prefix_append_iff = thm "prefix_append_iff";
    1.60 -val common_prefix_linear = thm "common_prefix_linear";
    1.61 -val reflexive_Le = thm "reflexive_Le";
    1.62 -val antisym_Le = thm "antisym_Le";
    1.63 -val trans_Le = thm "trans_Le";
    1.64 -val pfixLe_refl = thm "pfixLe_refl";
    1.65 -val pfixLe_trans = thm "pfixLe_trans";
    1.66 -val pfixLe_antisym = thm "pfixLe_antisym";
    1.67 -val prefix_imp_pfixLe = thm "prefix_imp_pfixLe";
    1.68 -val reflexive_Ge = thm "reflexive_Ge";
    1.69 -val antisym_Ge = thm "antisym_Ge";
    1.70 -val trans_Ge = thm "trans_Ge";
    1.71 -val pfixGe_refl = thm "pfixGe_refl";
    1.72 -val pfixGe_trans = thm "pfixGe_trans";
    1.73 -val pfixGe_antisym = thm "pfixGe_antisym";
    1.74 -val prefix_imp_pfixGe = thm "prefix_imp_pfixGe";
    1.75 -
    1.76 -
    1.77 -(*UNITY*)
    1.78 -val mk_total_program_def = thm "mk_total_program_def";
    1.79 -val totalize_act_def = thm "totalize_act_def";
    1.80 -val constrains_def = thm "constrains_def";
    1.81 -val stable_def = thm "stable_def";
    1.82 -val invariant_def = thm "invariant_def";
    1.83 -val increasing_def = thm "increasing_def";
    1.84 -val Allowed_def = thm "Allowed_def";
    1.85 -val Id_in_Acts = thm "Id_in_Acts";
    1.86 -val insert_Id_Acts = thm "insert_Id_Acts";
    1.87 -val Id_in_AllowedActs = thm "Id_in_AllowedActs";
    1.88 -val insert_Id_AllowedActs = thm "insert_Id_AllowedActs";
    1.89 -val Init_eq = thm "Init_eq";
    1.90 -val Acts_eq = thm "Acts_eq";
    1.91 -val AllowedActs_eq = thm "AllowedActs_eq";
    1.92 -val surjective_mk_program = thm "surjective_mk_program";
    1.93 -val program_equalityI = thm "program_equalityI";
    1.94 -val program_equalityE = thm "program_equalityE";
    1.95 -val program_equality_iff = thm "program_equality_iff";
    1.96 -val def_prg_Init = thm "def_prg_Init";
    1.97 -val def_prg_Acts = thm "def_prg_Acts";
    1.98 -val def_prg_AllowedActs = thm "def_prg_AllowedActs";
    1.99 -val def_act_simp = thm "def_act_simp";
   1.100 -val def_set_simp = thm "def_set_simp";
   1.101 -val constrainsI = thm "constrainsI";
   1.102 -val constrainsD = thm "constrainsD";
   1.103 -val constrains_empty = thm "constrains_empty";
   1.104 -val constrains_empty2 = thm "constrains_empty2";
   1.105 -val constrains_UNIV = thm "constrains_UNIV";
   1.106 -val constrains_UNIV2 = thm "constrains_UNIV2";
   1.107 -val constrains_weaken_R = thm "constrains_weaken_R";
   1.108 -val constrains_weaken_L = thm "constrains_weaken_L";
   1.109 -val constrains_weaken = thm "constrains_weaken";
   1.110 -val constrains_Un = thm "constrains_Un";
   1.111 -val constrains_UN = thm "constrains_UN";
   1.112 -val constrains_Un_distrib = thm "constrains_Un_distrib";
   1.113 -val constrains_UN_distrib = thm "constrains_UN_distrib";
   1.114 -val constrains_Int_distrib = thm "constrains_Int_distrib";
   1.115 -val constrains_INT_distrib = thm "constrains_INT_distrib";
   1.116 -val constrains_Int = thm "constrains_Int";
   1.117 -val constrains_INT = thm "constrains_INT";
   1.118 -val constrains_imp_subset = thm "constrains_imp_subset";
   1.119 -val constrains_trans = thm "constrains_trans";
   1.120 -val constrains_cancel = thm "constrains_cancel";
   1.121 -val unlessI = thm "unlessI";
   1.122 -val unlessD = thm "unlessD";
   1.123 -val stableI = thm "stableI";
   1.124 -val stableD = thm "stableD";
   1.125 -val stable_UNIV = thm "stable_UNIV";
   1.126 -val stable_Un = thm "stable_Un";
   1.127 -val stable_UN = thm "stable_UN";
   1.128 -val stable_Int = thm "stable_Int";
   1.129 -val stable_INT = thm "stable_INT";
   1.130 -val stable_constrains_Un = thm "stable_constrains_Un";
   1.131 -val stable_constrains_Int = thm "stable_constrains_Int";
   1.132 -val stable_constrains_stable = thm "stable_constrains_stable";
   1.133 -val invariantI = thm "invariantI";
   1.134 -val invariant_Int = thm "invariant_Int";
   1.135 -val increasingD = thm "increasingD";
   1.136 -val increasing_constant = thm "increasing_constant";
   1.137 -val mono_increasing_o = thm "mono_increasing_o";
   1.138 -val strict_increasingD = thm "strict_increasingD";
   1.139 -val elimination = thm "elimination";
   1.140 -val elimination_sing = thm "elimination_sing";
   1.141 -val constrains_strongest_rhs = thm "constrains_strongest_rhs";
   1.142 -val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest";
   1.143 -val Un_Diff_Diff = thm "Un_Diff_Diff";
   1.144 -val Int_Union_Union = thm "Int_Union_Union";
   1.145 -val Image_less_than = thm "Image_less_than";
   1.146 -val Image_inverse_less_than = thm "Image_inverse_less_than";
   1.147 -val totalize_constrains_iff = thm "totalize_constrains_iff";
   1.148 -
   1.149 -(*WFair*)
   1.150 -val stable_transient_empty = thm "stable_transient_empty";
   1.151 -val transient_strengthen = thm "transient_strengthen";
   1.152 -val transientI = thm "transientI";
   1.153 -val totalize_transientI = thm "totalize_transientI";
   1.154 -val transientE = thm "transientE";
   1.155 -val transient_empty = thm "transient_empty";
   1.156 -val ensuresI = thm "ensuresI";
   1.157 -val ensuresD = thm "ensuresD";
   1.158 -val ensures_weaken_R = thm "ensures_weaken_R";
   1.159 -val stable_ensures_Int = thm "stable_ensures_Int";
   1.160 -val stable_transient_ensures = thm "stable_transient_ensures";
   1.161 -val ensures_eq = thm "ensures_eq";
   1.162 -val leadsTo_Basis = thm "leadsTo_Basis";
   1.163 -val leadsTo_Trans = thm "leadsTo_Trans";
   1.164 -val transient_imp_leadsTo = thm "transient_imp_leadsTo";
   1.165 -val leadsTo_Un_duplicate = thm "leadsTo_Un_duplicate";
   1.166 -val leadsTo_Un_duplicate2 = thm "leadsTo_Un_duplicate2";
   1.167 -val leadsTo_Union = thm "leadsTo_Union";
   1.168 -val leadsTo_Union_Int = thm "leadsTo_Union_Int";
   1.169 -val leadsTo_UN = thm "leadsTo_UN";
   1.170 -val leadsTo_Un = thm "leadsTo_Un";
   1.171 -val single_leadsTo_I = thm "single_leadsTo_I";
   1.172 -val leadsTo_induct = thm "leadsTo_induct";
   1.173 -val subset_imp_ensures = thm "subset_imp_ensures";
   1.174 -val subset_imp_leadsTo = thm "subset_imp_leadsTo";
   1.175 -val leadsTo_refl = thm "leadsTo_refl";
   1.176 -val empty_leadsTo = thm "empty_leadsTo";
   1.177 -val leadsTo_UNIV = thm "leadsTo_UNIV";
   1.178 -val leadsTo_induct_pre = thm "leadsTo_induct_pre";
   1.179 -val leadsTo_weaken_R = thm "leadsTo_weaken_R";
   1.180 -val leadsTo_weaken_L = thm "leadsTo_weaken_L";
   1.181 -val leadsTo_Un_distrib = thm "leadsTo_Un_distrib";
   1.182 -val leadsTo_UN_distrib = thm "leadsTo_UN_distrib";
   1.183 -val leadsTo_Union_distrib = thm "leadsTo_Union_distrib";
   1.184 -val leadsTo_weaken = thm "leadsTo_weaken";
   1.185 -val leadsTo_Diff = thm "leadsTo_Diff";
   1.186 -val leadsTo_UN_UN = thm "leadsTo_UN_UN";
   1.187 -val leadsTo_Un_Un = thm "leadsTo_Un_Un";
   1.188 -val leadsTo_cancel2 = thm "leadsTo_cancel2";
   1.189 -val leadsTo_cancel_Diff2 = thm "leadsTo_cancel_Diff2";
   1.190 -val leadsTo_cancel1 = thm "leadsTo_cancel1";
   1.191 -val leadsTo_cancel_Diff1 = thm "leadsTo_cancel_Diff1";
   1.192 -val leadsTo_empty = thm "leadsTo_empty";
   1.193 -val psp_stable = thm "psp_stable";
   1.194 -val psp_stable2 = thm "psp_stable2";
   1.195 -val psp_ensures = thm "psp_ensures";
   1.196 -val psp = thm "psp";
   1.197 -val psp2 = thm "psp2";
   1.198 -val psp_unless = thm "psp_unless";
   1.199 -val leadsTo_wf_induct = thm "leadsTo_wf_induct";
   1.200 -val bounded_induct = thm "bounded_induct";
   1.201 -val lessThan_induct = thm "lessThan_induct";
   1.202 -val lessThan_bounded_induct = thm "lessThan_bounded_induct";
   1.203 -val greaterThan_bounded_induct = thm "greaterThan_bounded_induct";
   1.204 -val wlt_leadsTo = thm "wlt_leadsTo";
   1.205 -val leadsTo_subset = thm "leadsTo_subset";
   1.206 -val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt";
   1.207 -val wlt_increasing = thm "wlt_increasing";
   1.208 -val leadsTo_123 = thm "leadsTo_123";
   1.209 -val wlt_constrains_wlt = thm "wlt_constrains_wlt";
   1.210 -val completion = thm "completion";
   1.211 -val finite_completion = thm "finite_completion";
   1.212 -val stable_completion = thm "stable_completion";
   1.213 -val finite_stable_completion = thm "finite_stable_completion";
   1.214 -
   1.215 -(*Constrains*)
   1.216 -val Increasing_def = thm "Increasing_def";
   1.217 -val reachable_Init = thm "reachable.Init";
   1.218 -val reachable_Acts = thm "reachable.Acts";
   1.219 -val reachable_equiv_traces = thm "reachable_equiv_traces";
   1.220 -val Init_subset_reachable = thm "Init_subset_reachable";
   1.221 -val stable_reachable = thm "stable_reachable";
   1.222 -val invariant_reachable = thm "invariant_reachable";
   1.223 -val invariant_includes_reachable = thm "invariant_includes_reachable";
   1.224 -val constrains_reachable_Int = thm "constrains_reachable_Int";
   1.225 -val Constrains_eq_constrains = thm "Constrains_eq_constrains";
   1.226 -val constrains_imp_Constrains = thm "constrains_imp_Constrains";
   1.227 -val stable_imp_Stable = thm "stable_imp_Stable";
   1.228 -val ConstrainsI = thm "ConstrainsI";
   1.229 -val Constrains_empty = thm "Constrains_empty";
   1.230 -val Constrains_UNIV = thm "Constrains_UNIV";
   1.231 -val Constrains_weaken_R = thm "Constrains_weaken_R";
   1.232 -val Constrains_weaken_L = thm "Constrains_weaken_L";
   1.233 -val Constrains_weaken = thm "Constrains_weaken";
   1.234 -val Constrains_Un = thm "Constrains_Un";
   1.235 -val Constrains_UN = thm "Constrains_UN";
   1.236 -val Constrains_Int = thm "Constrains_Int";
   1.237 -val Constrains_INT = thm "Constrains_INT";
   1.238 -val Constrains_imp_subset = thm "Constrains_imp_subset";
   1.239 -val Constrains_trans = thm "Constrains_trans";
   1.240 -val Constrains_cancel = thm "Constrains_cancel";
   1.241 -val Stable_eq = thm "Stable_eq";
   1.242 -val Stable_eq_stable = thm "Stable_eq_stable";
   1.243 -val StableI = thm "StableI";
   1.244 -val StableD = thm "StableD";
   1.245 -val Stable_Un = thm "Stable_Un";
   1.246 -val Stable_Int = thm "Stable_Int";
   1.247 -val Stable_Constrains_Un = thm "Stable_Constrains_Un";
   1.248 -val Stable_Constrains_Int = thm "Stable_Constrains_Int";
   1.249 -val Stable_UN = thm "Stable_UN";
   1.250 -val Stable_INT = thm "Stable_INT";
   1.251 -val Stable_reachable = thm "Stable_reachable";
   1.252 -val IncreasingD = thm "IncreasingD";
   1.253 -val mono_Increasing_o = thm "mono_Increasing_o";
   1.254 -val strict_IncreasingD = thm "strict_IncreasingD";
   1.255 -val increasing_imp_Increasing = thm "increasing_imp_Increasing";
   1.256 -val Increasing_constant = thm "Increasing_constant";
   1.257 -val Elimination = thm "Elimination";
   1.258 -val Elimination_sing = thm "Elimination_sing";
   1.259 -val AlwaysI = thm "AlwaysI";
   1.260 -val AlwaysD = thm "AlwaysD";
   1.261 -val AlwaysE = thm "AlwaysE";
   1.262 -val Always_imp_Stable = thm "Always_imp_Stable";
   1.263 -val Always_includes_reachable = thm "Always_includes_reachable";
   1.264 -val invariant_imp_Always = thm "invariant_imp_Always";
   1.265 -val Always_reachable = thm "Always_reachable";
   1.266 -val Always_eq_invariant_reachable = thm "Always_eq_invariant_reachable";
   1.267 -val Always_eq_includes_reachable = thm "Always_eq_includes_reachable";
   1.268 -val Always_UNIV_eq = thm "Always_UNIV_eq";
   1.269 -val UNIV_AlwaysI = thm "UNIV_AlwaysI";
   1.270 -val Always_eq_UN_invariant = thm "Always_eq_UN_invariant";
   1.271 -val Always_weaken = thm "Always_weaken";
   1.272 -val Always_Constrains_pre = thm "Always_Constrains_pre";
   1.273 -val Always_Constrains_post = thm "Always_Constrains_post";
   1.274 -val Always_ConstrainsI = thm "Always_ConstrainsI";
   1.275 -val Always_ConstrainsD = thm "Always_ConstrainsD";
   1.276 -val Always_Constrains_weaken = thm "Always_Constrains_weaken";
   1.277 -val Always_Int_distrib = thm "Always_Int_distrib";
   1.278 -val Always_INT_distrib = thm "Always_INT_distrib";
   1.279 -val Always_Int_I = thm "Always_Int_I";
   1.280 -val Always_Compl_Un_eq = thm "Always_Compl_Un_eq";
   1.281 -val Always_thin = thm "Always_thin";
   1.282 -
   1.283 -(*FP*)
   1.284 -val stable_FP_Orig_Int = thm "stable_FP_Orig_Int";
   1.285 -val FP_Orig_weakest = thm "FP_Orig_weakest";
   1.286 -val stable_FP_Int = thm "stable_FP_Int";
   1.287 -val FP_equivalence = thm "FP_equivalence";
   1.288 -val FP_weakest = thm "FP_weakest";
   1.289 -val Compl_FP = thm "Compl_FP";
   1.290 -val Diff_FP = thm "Diff_FP";
   1.291 -
   1.292 -(*SubstAx*)
   1.293 -val LeadsTo_eq_leadsTo = thm "LeadsTo_eq_leadsTo";
   1.294 -val Always_LeadsTo_pre = thm "Always_LeadsTo_pre";
   1.295 -val Always_LeadsTo_post = thm "Always_LeadsTo_post";
   1.296 -val Always_LeadsToI = thm "Always_LeadsToI";
   1.297 -val Always_LeadsToD = thm "Always_LeadsToD";
   1.298 -val leadsTo_imp_LeadsTo = thm "leadsTo_imp_LeadsTo";
   1.299 -val LeadsTo_Trans = thm "LeadsTo_Trans";
   1.300 -val LeadsTo_Union = thm "LeadsTo_Union";
   1.301 -val LeadsTo_UNIV = thm "LeadsTo_UNIV";
   1.302 -val LeadsTo_Un_duplicate = thm "LeadsTo_Un_duplicate";
   1.303 -val LeadsTo_Un_duplicate2 = thm "LeadsTo_Un_duplicate2";
   1.304 -val LeadsTo_UN = thm "LeadsTo_UN";
   1.305 -val LeadsTo_Un = thm "LeadsTo_Un";
   1.306 -val single_LeadsTo_I = thm "single_LeadsTo_I";
   1.307 -val subset_imp_LeadsTo = thm "subset_imp_LeadsTo";
   1.308 -val empty_LeadsTo = thm "empty_LeadsTo";
   1.309 -val LeadsTo_weaken_R = thm "LeadsTo_weaken_R";
   1.310 -val LeadsTo_weaken_L = thm "LeadsTo_weaken_L";
   1.311 -val LeadsTo_weaken = thm "LeadsTo_weaken";
   1.312 -val Always_LeadsTo_weaken = thm "Always_LeadsTo_weaken";
   1.313 -val LeadsTo_Un_post = thm "LeadsTo_Un_post";
   1.314 -val LeadsTo_Trans_Un = thm "LeadsTo_Trans_Un";
   1.315 -val LeadsTo_Un_distrib = thm "LeadsTo_Un_distrib";
   1.316 -val LeadsTo_UN_distrib = thm "LeadsTo_UN_distrib";
   1.317 -val LeadsTo_Union_distrib = thm "LeadsTo_Union_distrib";
   1.318 -val LeadsTo_Basis = thm "LeadsTo_Basis";
   1.319 -val EnsuresI = thm "EnsuresI";
   1.320 -val Always_LeadsTo_Basis = thm "Always_LeadsTo_Basis";
   1.321 -val LeadsTo_Diff = thm "LeadsTo_Diff";
   1.322 -val LeadsTo_UN_UN = thm "LeadsTo_UN_UN";
   1.323 -val LeadsTo_UN_UN_noindex = thm "LeadsTo_UN_UN_noindex";
   1.324 -val all_LeadsTo_UN_UN = thm "all_LeadsTo_UN_UN";
   1.325 -val LeadsTo_Un_Un = thm "LeadsTo_Un_Un";
   1.326 -val LeadsTo_cancel2 = thm "LeadsTo_cancel2";
   1.327 -val LeadsTo_cancel_Diff2 = thm "LeadsTo_cancel_Diff2";
   1.328 -val LeadsTo_cancel1 = thm "LeadsTo_cancel1";
   1.329 -val LeadsTo_cancel_Diff1 = thm "LeadsTo_cancel_Diff1";
   1.330 -val LeadsTo_empty = thm "LeadsTo_empty";
   1.331 -val PSP_Stable = thm "PSP_Stable";
   1.332 -val PSP_Stable2 = thm "PSP_Stable2";
   1.333 -val PSP = thm "PSP";
   1.334 -val PSP2 = thm "PSP2";
   1.335 -val PSP_Unless = thm "PSP_Unless";
   1.336 -val Stable_transient_Always_LeadsTo = thm "Stable_transient_Always_LeadsTo";
   1.337 -val LeadsTo_wf_induct = thm "LeadsTo_wf_induct";
   1.338 -val Bounded_induct = thm "Bounded_induct";
   1.339 -val LessThan_induct = thm "LessThan_induct";
   1.340 -val integ_0_le_induct = thm "integ_0_le_induct";
   1.341 -val LessThan_bounded_induct = thm "LessThan_bounded_induct";
   1.342 -val GreaterThan_bounded_induct = thm "GreaterThan_bounded_induct";
   1.343 -val Completion = thm "Completion";
   1.344 -val Finite_completion = thm "Finite_completion";
   1.345 -val Stable_completion = thm "Stable_completion";
   1.346 -val Finite_stable_completion = thm "Finite_stable_completion";
   1.347 -
   1.348 -(*Union*)
   1.349 -val Init_SKIP = thm "Init_SKIP";
   1.350 -val Acts_SKIP = thm "Acts_SKIP";
   1.351 -val AllowedActs_SKIP = thm "AllowedActs_SKIP";
   1.352 -val reachable_SKIP = thm "reachable_SKIP";
   1.353 -val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff";
   1.354 -val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff";
   1.355 -val SKIP_in_stable = thm "SKIP_in_stable";
   1.356 -val Init_Join = thm "Init_Join";
   1.357 -val Acts_Join = thm "Acts_Join";
   1.358 -val AllowedActs_Join = thm "AllowedActs_Join";
   1.359 -val JN_empty = thm "JN_empty";
   1.360 -val JN_insert = thm "JN_insert";
   1.361 -val Init_JN = thm "Init_JN";
   1.362 -val Acts_JN = thm "Acts_JN";
   1.363 -val AllowedActs_JN = thm "AllowedActs_JN";
   1.364 -val JN_cong = thm "JN_cong";
   1.365 -val Join_commute = thm "Join_commute";
   1.366 -val Join_assoc = thm "Join_assoc";
   1.367 -val Join_left_commute = thm "Join_left_commute";
   1.368 -val Join_SKIP_left = thm "Join_SKIP_left";
   1.369 -val Join_SKIP_right = thm "Join_SKIP_right";
   1.370 -val Join_absorb = thm "Join_absorb";
   1.371 -val Join_left_absorb = thm "Join_left_absorb";
   1.372 -val Join_ac = thms "Join_ac";
   1.373 -val JN_absorb = thm "JN_absorb";
   1.374 -val JN_Un = thm "JN_Un";
   1.375 -val JN_constant = thm "JN_constant";
   1.376 -val JN_Join_distrib = thm "JN_Join_distrib";
   1.377 -val JN_Join_miniscope = thm "JN_Join_miniscope";
   1.378 -val JN_Join_diff = thm "JN_Join_diff";
   1.379 -val JN_constrains = thm "JN_constrains";
   1.380 -val Join_constrains = thm "Join_constrains";
   1.381 -val Join_unless = thm "Join_unless";
   1.382 -val Join_constrains_weaken = thm "Join_constrains_weaken";
   1.383 -val JN_constrains_weaken = thm "JN_constrains_weaken";
   1.384 -val JN_stable = thm "JN_stable";
   1.385 -val invariant_JN_I = thm "invariant_JN_I";
   1.386 -val Join_stable = thm "Join_stable";
   1.387 -val Join_increasing = thm "Join_increasing";
   1.388 -val invariant_JoinI = thm "invariant_JoinI";
   1.389 -val FP_JN = thm "FP_JN";
   1.390 -val JN_transient = thm "JN_transient";
   1.391 -val Join_transient = thm "Join_transient";
   1.392 -val Join_transient_I1 = thm "Join_transient_I1";
   1.393 -val Join_transient_I2 = thm "Join_transient_I2";
   1.394 -val JN_ensures = thm "JN_ensures";
   1.395 -val Join_ensures = thm "Join_ensures";
   1.396 -val stable_Join_constrains = thm "stable_Join_constrains";
   1.397 -val stable_Join_Always1 = thm "stable_Join_Always1";
   1.398 -val stable_Join_Always2 = thm "stable_Join_Always2";
   1.399 -val stable_Join_ensures1 = thm "stable_Join_ensures1";
   1.400 -val stable_Join_ensures2 = thm "stable_Join_ensures2";
   1.401 -val ok_SKIP1 = thm "ok_SKIP1";
   1.402 -val ok_SKIP2 = thm "ok_SKIP2";
   1.403 -val ok_Join_commute = thm "ok_Join_commute";
   1.404 -val ok_commute = thm "ok_commute";
   1.405 -val ok_sym = thm "ok_sym";
   1.406 -val ok_iff_OK = thm "ok_iff_OK";
   1.407 -val ok_Join_iff1 = thm "ok_Join_iff1";
   1.408 -val ok_Join_iff2 = thm "ok_Join_iff2";
   1.409 -val ok_Join_commute_I = thm "ok_Join_commute_I";
   1.410 -val ok_JN_iff1 = thm "ok_JN_iff1";
   1.411 -val ok_JN_iff2 = thm "ok_JN_iff2";
   1.412 -val OK_iff_ok = thm "OK_iff_ok";
   1.413 -val OK_imp_ok = thm "OK_imp_ok";
   1.414 -val Allowed_SKIP = thm "Allowed_SKIP";
   1.415 -val Allowed_Join = thm "Allowed_Join";
   1.416 -val Allowed_JN = thm "Allowed_JN";
   1.417 -val ok_iff_Allowed = thm "ok_iff_Allowed";
   1.418 -val OK_iff_Allowed = thm "OK_iff_Allowed";
   1.419 -val safety_prop_Acts_iff = thm "safety_prop_Acts_iff";
   1.420 -val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed";
   1.421 -val Allowed_eq = thm "Allowed_eq";
   1.422 -val def_prg_Allowed = thm "def_prg_Allowed";
   1.423 -val def_total_prg_Allowed = thm "def_total_prg_Allowed";
   1.424 -val safety_prop_constrains = thm "safety_prop_constrains";
   1.425 -val safety_prop_stable = thm "safety_prop_stable";
   1.426 -val safety_prop_Int = thm "safety_prop_Int";
   1.427 -val safety_prop_INTER1 = thm "safety_prop_INTER1";
   1.428 -val safety_prop_INTER = thm "safety_prop_INTER";
   1.429 -val def_UNION_ok_iff = thm "def_UNION_ok_iff";
   1.430 -val totalize_JN = thm "totalize_JN";
   1.431 -
   1.432 -(*Comp*)
   1.433 -val preserves_def = thm "preserves_def";
   1.434 -val funPair_def = thm "funPair_def";
   1.435 -val componentI = thm "componentI";
   1.436 -val component_eq_subset = thm "component_eq_subset";
   1.437 -val component_SKIP = thm "component_SKIP";
   1.438 -val component_refl = thm "component_refl";
   1.439 -val SKIP_minimal = thm "SKIP_minimal";
   1.440 -val component_Join1 = thm "component_Join1";
   1.441 -val component_Join2 = thm "component_Join2";
   1.442 -val Join_absorb1 = thm "Join_absorb1";
   1.443 -val Join_absorb2 = thm "Join_absorb2";
   1.444 -val JN_component_iff = thm "JN_component_iff";
   1.445 -val component_JN = thm "component_JN";
   1.446 -val component_trans = thm "component_trans";
   1.447 -val component_antisym = thm "component_antisym";
   1.448 -val Join_component_iff = thm "Join_component_iff";
   1.449 -val component_constrains = thm "component_constrains";
   1.450 -val program_less_le = thm "program_less_le";
   1.451 -val preservesI = thm "preservesI";
   1.452 -val preserves_imp_eq = thm "preserves_imp_eq";
   1.453 -val Join_preserves = thm "Join_preserves";
   1.454 -val JN_preserves = thm "JN_preserves";
   1.455 -val SKIP_preserves = thm "SKIP_preserves";
   1.456 -val funPair_apply = thm "funPair_apply";
   1.457 -val preserves_funPair = thm "preserves_funPair";
   1.458 -val funPair_o_distrib = thm "funPair_o_distrib";
   1.459 -val fst_o_funPair = thm "fst_o_funPair";
   1.460 -val snd_o_funPair = thm "snd_o_funPair";
   1.461 -val subset_preserves_o = thm "subset_preserves_o";
   1.462 -val preserves_subset_stable = thm "preserves_subset_stable";
   1.463 -val preserves_subset_increasing = thm "preserves_subset_increasing";
   1.464 -val preserves_id_subset_stable = thm "preserves_id_subset_stable";
   1.465 -val safety_prop_preserves = thm "safety_prop_preserves";
   1.466 -val stable_localTo_stable2 = thm "stable_localTo_stable2";
   1.467 -val Increasing_preserves_Stable = thm "Increasing_preserves_Stable";
   1.468 -val component_of_imp_component = thm "component_of_imp_component";
   1.469 -val component_of_refl = thm "component_of_refl";
   1.470 -val component_of_SKIP = thm "component_of_SKIP";
   1.471 -val component_of_trans = thm "component_of_trans";
   1.472 -val strict_component_of_eq = thm "strict_component_of_eq";
   1.473 -val localize_Init_eq = thm "localize_Init_eq";
   1.474 -val localize_Acts_eq = thm "localize_Acts_eq";
   1.475 -val localize_AllowedActs_eq = thm "localize_AllowedActs_eq";
   1.476 -
   1.477 -(*Guar*)
   1.478 -val guar_def = thm "guar_def";
   1.479 -val OK_insert_iff = thm "OK_insert_iff";
   1.480 -val ex1 = thm "ex1";
   1.481 -val ex2 = thm "ex2";
   1.482 -val ex_prop_finite = thm "ex_prop_finite";
   1.483 -val ex_prop_equiv = thm "ex_prop_equiv";
   1.484 -val uv1 = thm "uv1";
   1.485 -val uv2 = thm "uv2";
   1.486 -val uv_prop_finite = thm "uv_prop_finite";
   1.487 -val guaranteesI = thm "guaranteesI";
   1.488 -val guaranteesD = thm "guaranteesD";
   1.489 -val component_guaranteesD = thm "component_guaranteesD";
   1.490 -val guarantees_weaken = thm "guarantees_weaken";
   1.491 -val subset_imp_guarantees_UNIV = thm "subset_imp_guarantees_UNIV";
   1.492 -val subset_imp_guarantees = thm "subset_imp_guarantees";
   1.493 -val ex_prop_imp = thm "ex_prop_imp";
   1.494 -val guarantees_imp = thm "guarantees_imp";
   1.495 -val ex_prop_equiv2 = thm "ex_prop_equiv2";
   1.496 -val guarantees_UN_left = thm "guarantees_UN_left";
   1.497 -val guarantees_Un_left = thm "guarantees_Un_left";
   1.498 -val guarantees_INT_right = thm "guarantees_INT_right";
   1.499 -val guarantees_Int_right = thm "guarantees_Int_right";
   1.500 -val guarantees_Int_right_I = thm "guarantees_Int_right_I";
   1.501 -val guarantees_INT_right_iff = thm "guarantees_INT_right_iff";
   1.502 -val shunting = thm "shunting";
   1.503 -val contrapositive = thm "contrapositive";
   1.504 -val combining1 = thm "combining1";
   1.505 -val combining2 = thm "combining2";
   1.506 -val all_guarantees = thm "all_guarantees";
   1.507 -val ex_guarantees = thm "ex_guarantees";
   1.508 -val guarantees_Join_Int = thm "guarantees_Join_Int";
   1.509 -val guarantees_Join_Un = thm "guarantees_Join_Un";
   1.510 -val guarantees_JN_INT = thm "guarantees_JN_INT";
   1.511 -val guarantees_JN_UN = thm "guarantees_JN_UN";
   1.512 -val guarantees_Join_I1 = thm "guarantees_Join_I1";
   1.513 -val guarantees_Join_I2 = thm "guarantees_Join_I2";
   1.514 -val guarantees_JN_I = thm "guarantees_JN_I";
   1.515 -val Join_welldef_D1 = thm "Join_welldef_D1";
   1.516 -val Join_welldef_D2 = thm "Join_welldef_D2";
   1.517 -val refines_refl = thm "refines_refl";
   1.518 -val ex_refinement_thm = thm "ex_refinement_thm";
   1.519 -val uv_refinement_thm = thm "uv_refinement_thm";
   1.520 -val guarantees_equiv = thm "guarantees_equiv";
   1.521 -val wg_weakest = thm "wg_weakest";
   1.522 -val wg_guarantees = thm "wg_guarantees";
   1.523 -val wg_equiv = thm "wg_equiv";
   1.524 -val component_of_wg = thm "component_of_wg";
   1.525 -val wg_finite = thm "wg_finite";
   1.526 -val wg_ex_prop = thm "wg_ex_prop";
   1.527 -val wx_subset = thm "wx_subset";
   1.528 -val wx_ex_prop = thm "wx_ex_prop";
   1.529 -val wx_weakest = thm "wx_weakest";
   1.530 -val wx'_ex_prop = thm "wx'_ex_prop";
   1.531 -val wx_equiv = thm "wx_equiv";
   1.532 -val guarantees_wx_eq = thm "guarantees_wx_eq";
   1.533 -val stable_guarantees_Always = thm "stable_guarantees_Always";
   1.534 -val leadsTo_Basis = thm "leadsTo_Basis";
   1.535 -val constrains_guarantees_leadsTo = thm "constrains_guarantees_leadsTo";
   1.536 -
   1.537 -(*Extend*)
   1.538 -val Restrict_iff = thm "Restrict_iff";
   1.539 -val Restrict_UNIV = thm "Restrict_UNIV";
   1.540 -val Restrict_empty = thm "Restrict_empty";
   1.541 -val Restrict_Int = thm "Restrict_Int";
   1.542 -val Restrict_triv = thm "Restrict_triv";
   1.543 -val Restrict_subset = thm "Restrict_subset";
   1.544 -val Restrict_eq_mono = thm "Restrict_eq_mono";
   1.545 -val Restrict_imageI = thm "Restrict_imageI";
   1.546 -val Domain_Restrict = thm "Domain_Restrict";
   1.547 -val Image_Restrict = thm "Image_Restrict";
   1.548 -val insert_Id_image_Acts = thm "insert_Id_image_Acts";
   1.549 -val good_mapI = thm "good_mapI";
   1.550 -val good_map_is_surj = thm "good_map_is_surj";
   1.551 -val fst_inv_equalityI = thm "fst_inv_equalityI";
   1.552 -val project_set_iff = thm "project_set_iff";
   1.553 -val extend_set_mono = thm "extend_set_mono";
   1.554 -val extend_set_empty = thm "extend_set_empty";
   1.555 -val project_set_Int_subset = thm "project_set_Int_subset";
   1.556 -val Init_extend = thm "Init_extend";
   1.557 -val Init_project = thm "Init_project";
   1.558 -val Acts_project = thm "Acts_project";
   1.559 -val project_set_UNIV = thm "project_set_UNIV";
   1.560 -val project_set_Union = thm "project_set_Union";
   1.561 -val project_act_mono = thm "project_act_mono";
   1.562 -val project_constrains_project_set = thm "project_constrains_project_set";
   1.563 -val project_stable_project_set = thm "project_stable_project_set";
   1.564 -
   1.565 -
   1.566 -(*Rename*)
   1.567 -val good_map_bij = thm "good_map_bij";
   1.568 -val fst_o_inv_eq_inv = thm "fst_o_inv_eq_inv";
   1.569 -val mem_rename_set_iff = thm "mem_rename_set_iff";
   1.570 -val extend_set_eq_image = thm "extend_set_eq_image";
   1.571 -val Init_rename = thm "Init_rename";
   1.572 -val extend_set_inv = thm "extend_set_inv";
   1.573 -val bij_extend_act_eq_project_act = thm "bij_extend_act_eq_project_act";
   1.574 -val bij_extend_act = thm "bij_extend_act";
   1.575 -val bij_project_act = thm "bij_project_act";
   1.576 -val bij_inv_project_act_eq = thm "bij_inv_project_act_eq";
   1.577 -val Acts_project = thm "Acts_project";
   1.578 -val extend_inv = thm "extend_inv";
   1.579 -val rename_inv_rename = thm "rename_inv_rename";
   1.580 -val rename_rename_inv = thm "rename_rename_inv";
   1.581 -val rename_inv_eq = thm "rename_inv_eq";
   1.582 -val bij_extend = thm "bij_extend";
   1.583 -val bij_project = thm "bij_project";
   1.584 -val inv_project_eq = thm "inv_project_eq";
   1.585 -val Allowed_rename = thm "Allowed_rename";
   1.586 -val bij_rename = thm "bij_rename";
   1.587 -val surj_rename = thm "surj_rename";
   1.588 -val inj_rename_imp_inj = thm "inj_rename_imp_inj";
   1.589 -val surj_rename_imp_surj = thm "surj_rename_imp_surj";
   1.590 -val bij_rename_imp_bij = thm "bij_rename_imp_bij";
   1.591 -val bij_rename_iff = thm "bij_rename_iff";
   1.592 -val rename_SKIP = thm "rename_SKIP";
   1.593 -val rename_Join = thm "rename_Join";
   1.594 -val rename_JN = thm "rename_JN";
   1.595 -val rename_constrains = thm "rename_constrains";
   1.596 -val rename_stable = thm "rename_stable";
   1.597 -val rename_invariant = thm "rename_invariant";
   1.598 -val rename_increasing = thm "rename_increasing";
   1.599 -val reachable_rename_eq = thm "reachable_rename_eq";
   1.600 -val rename_Constrains = thm "rename_Constrains";
   1.601 -val rename_Stable = thm "rename_Stable";
   1.602 -val rename_Always = thm "rename_Always";
   1.603 -val rename_Increasing = thm "rename_Increasing";
   1.604 -val rename_transient = thm "rename_transient";
   1.605 -val rename_ensures = thm "rename_ensures";
   1.606 -val rename_leadsTo = thm "rename_leadsTo";
   1.607 -val rename_LeadsTo = thm "rename_LeadsTo";
   1.608 -val rename_rename_guarantees_eq = thm "rename_rename_guarantees_eq";
   1.609 -val rename_guarantees_eq_rename_inv = thm "rename_guarantees_eq_rename_inv";
   1.610 -val rename_preserves = thm "rename_preserves";
   1.611 -val ok_rename_iff = thm "ok_rename_iff";
   1.612 -val OK_rename_iff = thm "OK_rename_iff";
   1.613 -val bij_eq_rename = thm "bij_eq_rename";
   1.614 -val rename_image_constrains = thm "rename_image_constrains";
   1.615 -val rename_image_stable = thm "rename_image_stable";
   1.616 -val rename_image_increasing = thm "rename_image_increasing";
   1.617 -val rename_image_invariant = thm "rename_image_invariant";
   1.618 -val rename_image_Constrains = thm "rename_image_Constrains";
   1.619 -val rename_image_preserves = thm "rename_image_preserves";
   1.620 -val rename_image_Stable = thm "rename_image_Stable";
   1.621 -val rename_image_Increasing = thm "rename_image_Increasing";
   1.622 -val rename_image_Always = thm "rename_image_Always";
   1.623 -val rename_image_leadsTo = thm "rename_image_leadsTo";
   1.624 -val rename_image_LeadsTo = thm "rename_image_LeadsTo";
   1.625 -
   1.626 -
   1.627 -
   1.628 -(*Lift_prog*)
   1.629 -val sub_def = thm "sub_def";
   1.630 -val lift_map_def = thm "lift_map_def";
   1.631 -val drop_map_def = thm "drop_map_def";
   1.632 -val insert_map_inverse = thm "insert_map_inverse";
   1.633 -val insert_map_delete_map_eq = thm "insert_map_delete_map_eq";
   1.634 -val insert_map_inject1 = thm "insert_map_inject1";
   1.635 -val insert_map_inject2 = thm "insert_map_inject2";
   1.636 -val insert_map_inject = thm "insert_map_inject";
   1.637 -val insert_map_inject = thm "insert_map_inject";
   1.638 -val lift_map_eq_iff = thm "lift_map_eq_iff";
   1.639 -val drop_map_lift_map_eq = thm "drop_map_lift_map_eq";
   1.640 -val inj_lift_map = thm "inj_lift_map";
   1.641 -val lift_map_drop_map_eq = thm "lift_map_drop_map_eq";
   1.642 -val drop_map_inject = thm "drop_map_inject";
   1.643 -val surj_lift_map = thm "surj_lift_map";
   1.644 -val bij_lift_map = thm "bij_lift_map";
   1.645 -val inv_lift_map_eq = thm "inv_lift_map_eq";
   1.646 -val inv_drop_map_eq = thm "inv_drop_map_eq";
   1.647 -val bij_drop_map = thm "bij_drop_map";
   1.648 -val sub_apply = thm "sub_apply";
   1.649 -val lift_set_empty = thm "lift_set_empty";
   1.650 -val lift_set_iff = thm "lift_set_iff";
   1.651 -val lift_set_iff2 = thm "lift_set_iff2";
   1.652 -val lift_set_mono = thm "lift_set_mono";
   1.653 -val lift_set_Un_distrib = thm "lift_set_Un_distrib";
   1.654 -val lift_set_Diff_distrib = thm "lift_set_Diff_distrib";
   1.655 -val bij_lift = thm "bij_lift";
   1.656 -val lift_SKIP = thm "lift_SKIP";
   1.657 -val lift_Join = thm "lift_Join";
   1.658 -val lift_JN = thm "lift_JN";
   1.659 -val lift_constrains = thm "lift_constrains";
   1.660 -val lift_stable = thm "lift_stable";
   1.661 -val lift_invariant = thm "lift_invariant";
   1.662 -val lift_Constrains = thm "lift_Constrains";
   1.663 -val lift_Stable = thm "lift_Stable";
   1.664 -val lift_Always = thm "lift_Always";
   1.665 -val lift_transient = thm "lift_transient";
   1.666 -val lift_ensures = thm "lift_ensures";
   1.667 -val lift_leadsTo = thm "lift_leadsTo";
   1.668 -val lift_LeadsTo = thm "lift_LeadsTo";
   1.669 -val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq";
   1.670 -val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv";
   1.671 -val lift_preserves_snd_I = thm "lift_preserves_snd_I";
   1.672 -val delete_map_eqE = thm "delete_map_eqE";
   1.673 -val delete_map_eqE = thm "delete_map_eqE";
   1.674 -val delete_map_neq_apply = thm "delete_map_neq_apply";
   1.675 -val vimage_o_fst_eq = thm "vimage_o_fst_eq";
   1.676 -val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set";
   1.677 -val mem_lift_act_iff = thm "mem_lift_act_iff";
   1.678 -val preserves_snd_lift_stable = thm "preserves_snd_lift_stable";
   1.679 -val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains";
   1.680 -val lift_map_image_Times = thm "lift_map_image_Times";
   1.681 -val lift_preserves_eq = thm "lift_preserves_eq";
   1.682 -val lift_preserves_sub = thm "lift_preserves_sub";
   1.683 -val o_equiv_assoc = thm "o_equiv_assoc";
   1.684 -val o_equiv_apply = thm "o_equiv_apply";
   1.685 -val fst_o_lift_map = thm "fst_o_lift_map";
   1.686 -val snd_o_lift_map = thm "snd_o_lift_map";
   1.687 -val extend_act_extend_act = thm "extend_act_extend_act";
   1.688 -val project_act_project_act = thm "project_act_project_act";
   1.689 -val project_act_extend_act = thm "project_act_extend_act";
   1.690 -val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst";
   1.691 -val UNION_OK_lift_I = thm "UNION_OK_lift_I";
   1.692 -val OK_lift_I = thm "OK_lift_I";
   1.693 -val Allowed_lift = thm "Allowed_lift";
   1.694 -val lift_image_preserves = thm "lift_image_preserves";
   1.695 -
   1.696 -
   1.697 -(*PPROD*)
   1.698 -val Init_PLam = thm "Init_PLam";
   1.699 -val PLam_empty = thm "PLam_empty";
   1.700 -val PLam_SKIP = thm "PLam_SKIP";
   1.701 -val PLam_insert = thm "PLam_insert";
   1.702 -val PLam_component_iff = thm "PLam_component_iff";
   1.703 -val component_PLam = thm "component_PLam";
   1.704 -val PLam_constrains = thm "PLam_constrains";
   1.705 -val PLam_stable = thm "PLam_stable";
   1.706 -val PLam_transient = thm "PLam_transient";
   1.707 -val PLam_ensures = thm "PLam_ensures";
   1.708 -val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis";
   1.709 -val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant";
   1.710 -val PLam_preserves_fst = thm "PLam_preserves_fst";
   1.711 -val PLam_preserves_snd = thm "PLam_preserves_snd";
   1.712 -val guarantees_PLam_I = thm "guarantees_PLam_I";
   1.713 -val Allowed_PLam = thm "Allowed_PLam";
   1.714 -val PLam_preserves = thm "PLam_preserves";
   1.715 -
   1.716 -(*Follows*)
   1.717 -val mono_Always_o = thm "mono_Always_o";
   1.718 -val mono_LeadsTo_o = thm "mono_LeadsTo_o";
   1.719 -val Follows_constant = thm "Follows_constant";
   1.720 -val mono_Follows_o = thm "mono_Follows_o";
   1.721 -val mono_Follows_apply = thm "mono_Follows_apply";
   1.722 -val Follows_trans = thm "Follows_trans";
   1.723 -val Follows_Increasing1 = thm "Follows_Increasing1";
   1.724 -val Follows_Increasing2 = thm "Follows_Increasing2";
   1.725 -val Follows_Bounded = thm "Follows_Bounded";
   1.726 -val Follows_LeadsTo = thm "Follows_LeadsTo";
   1.727 -val Follows_LeadsTo_pfixLe = thm "Follows_LeadsTo_pfixLe";
   1.728 -val Follows_LeadsTo_pfixGe = thm "Follows_LeadsTo_pfixGe";
   1.729 -val Always_Follows1 = thm "Always_Follows1";
   1.730 -val Always_Follows2 = thm "Always_Follows2";
   1.731 -val increasing_Un = thm "increasing_Un";
   1.732 -val Increasing_Un = thm "Increasing_Un";
   1.733 -val Always_Un = thm "Always_Un";
   1.734 -val Follows_Un = thm "Follows_Un";
   1.735 -val increasing_union = thm "increasing_union";
   1.736 -val Increasing_union = thm "Increasing_union";
   1.737 -val Always_union = thm "Always_union";
   1.738 -val Follows_union = thm "Follows_union";
   1.739 -val Follows_setsum = thm "Follows_setsum";
   1.740 -val Increasing_imp_Stable_pfixGe = thm "Increasing_imp_Stable_pfixGe";
   1.741 -val LeadsTo_le_imp_pfixGe = thm "LeadsTo_le_imp_pfixGe";
   1.742 -
   1.743 -
   1.744 -(*Lazy unfolding of actions or of sets*)
   1.745 -fun simp_of_act def = def RS def_act_simp;
   1.746 -
   1.747 -fun simp_of_set def = def RS def_set_simp;
   1.748 -
   1.749 -
   1.750  (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   1.751 -val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin
   1.752 +val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}
   1.753  
   1.754  (*Combines a list of invariance THEOREMS into one.*)
   1.755 -val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I)
   1.756 +val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
   1.757  
   1.758  (*Proves "co" properties when the program is specified.  Any use of invariants
   1.759    (from weak constrains) must have been done already.*)
   1.760 -fun gen_constrains_tac(cs,ss) i = 
   1.761 +fun constrains_tac(cs,ss) i =
   1.762     SELECT_GOAL
   1.763        (EVERY [REPEAT (Always_Int_tac 1),
   1.764                (*reduce the fancy safety properties to "constrains"*)
   1.765 -	      REPEAT (etac Always_ConstrainsI 1
   1.766 -		      ORELSE
   1.767 -		      resolve_tac [StableI, stableI,
   1.768 -				   constrains_imp_Constrains] 1),
   1.769 +              REPEAT (etac @{thm Always_ConstrainsI} 1
   1.770 +                      ORELSE
   1.771 +                      resolve_tac [@{thm StableI}, @{thm stableI},
   1.772 +                                   @{thm constrains_imp_Constrains}] 1),
   1.773                (*for safety, the totalize operator can be ignored*)
   1.774 -	      simp_tac (HOL_ss addsimps
   1.775 -                         [mk_total_program_def, totalize_constrains_iff]) 1,
   1.776 -	      rtac constrainsI 1,
   1.777 -	      full_simp_tac ss 1,
   1.778 -	      REPEAT (FIRSTGOAL (etac disjE)),
   1.779 -	      ALLGOALS (clarify_tac cs),
   1.780 -	      ALLGOALS (asm_lr_simp_tac ss)]) i;
   1.781 +              simp_tac (HOL_ss addsimps
   1.782 +                         [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
   1.783 +              rtac @{thm constrainsI} 1,
   1.784 +              full_simp_tac ss 1,
   1.785 +              REPEAT (FIRSTGOAL (etac disjE)),
   1.786 +              ALLGOALS (clarify_tac cs),
   1.787 +              ALLGOALS (asm_lr_simp_tac ss)]) i;
   1.788  
   1.789  (*proves "ensures/leadsTo" properties when the program is specified*)
   1.790 -fun gen_ensures_tac(cs,ss) sact = 
   1.791 +fun ensures_tac(cs,ss) sact =
   1.792      SELECT_GOAL
   1.793        (EVERY [REPEAT (Always_Int_tac 1),
   1.794 -	      etac Always_LeadsTo_Basis 1 
   1.795 -	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   1.796 -		  REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
   1.797 -				    EnsuresI, ensuresI] 1),
   1.798 -	      (*now there are two subgoals: co & transient*)
   1.799 -	      simp_tac (ss addsimps [mk_total_program_def]) 2,
   1.800 -	      res_inst_tac [("act", sact)] totalize_transientI 2 
   1.801 - 	      ORELSE res_inst_tac [("act", sact)] transientI 2,
   1.802 +              etac @{thm Always_LeadsTo_Basis} 1
   1.803 +                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   1.804 +                  REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
   1.805 +                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
   1.806 +              (*now there are two subgoals: co & transient*)
   1.807 +              simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
   1.808 +              res_inst_tac [("act", sact)] @{thm totalize_transientI} 2
   1.809 +              ORELSE res_inst_tac [("act", sact)] @{thm transientI} 2,
   1.810                   (*simplify the command's domain*)
   1.811 -	      simp_tac (ss addsimps [Domain_def]) 3,
   1.812 -	      gen_constrains_tac (cs,ss) 1,
   1.813 -	      ALLGOALS (clarify_tac cs),
   1.814 -	      ALLGOALS (asm_lr_simp_tac ss)]);
   1.815 -
   1.816 -fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
   1.817 -
   1.818 -fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact;
   1.819 +              simp_tac (ss addsimps [@{thm Domain_def}]) 3,
   1.820 +              constrains_tac (cs,ss) 1,
   1.821 +              ALLGOALS (clarify_tac cs),
   1.822 +              ALLGOALS (asm_lr_simp_tac ss)]);
   1.823  
   1.824  
   1.825  (*Composition equivalences, from Lift_prog*)
   1.826  
   1.827  fun make_o_equivs th =
   1.828      [th,
   1.829 -     th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]),
   1.830 -     th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
   1.831 +     th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
   1.832 +     th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
   1.833  
   1.834 -Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
   1.835 +Addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair});
   1.836  
   1.837 -Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);
   1.838 +Addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map});