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