src/HOL/UNITY/UNITY_tactics.ML
changeset 13792 d1811693899c
parent 13790 8d7e9fce8c50
child 13796 19f50fa807ae
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Wed Jan 29 16:29:38 2003 +0100
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Wed Jan 29 16:34:51 2003 +0100
     1.3 @@ -6,6 +6,193 @@
     1.4  Specialized UNITY tactics, and ML bindings of theorems
     1.5  *)
     1.6  
     1.7 +(*Union*)
     1.8 +val Init_SKIP = thm "Init_SKIP";
     1.9 +val Acts_SKIP = thm "Acts_SKIP";
    1.10 +val AllowedActs_SKIP = thm "AllowedActs_SKIP";
    1.11 +val reachable_SKIP = thm "reachable_SKIP";
    1.12 +val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff";
    1.13 +val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff";
    1.14 +val SKIP_in_stable = thm "SKIP_in_stable";
    1.15 +val Init_Join = thm "Init_Join";
    1.16 +val Acts_Join = thm "Acts_Join";
    1.17 +val AllowedActs_Join = thm "AllowedActs_Join";
    1.18 +val JN_empty = thm "JN_empty";
    1.19 +val JN_insert = thm "JN_insert";
    1.20 +val Init_JN = thm "Init_JN";
    1.21 +val Acts_JN = thm "Acts_JN";
    1.22 +val AllowedActs_JN = thm "AllowedActs_JN";
    1.23 +val JN_cong = thm "JN_cong";
    1.24 +val Join_commute = thm "Join_commute";
    1.25 +val Join_assoc = thm "Join_assoc";
    1.26 +val Join_left_commute = thm "Join_left_commute";
    1.27 +val Join_SKIP_left = thm "Join_SKIP_left";
    1.28 +val Join_SKIP_right = thm "Join_SKIP_right";
    1.29 +val Join_absorb = thm "Join_absorb";
    1.30 +val Join_left_absorb = thm "Join_left_absorb";
    1.31 +val Join_ac = thms "Join_ac";
    1.32 +val JN_absorb = thm "JN_absorb";
    1.33 +val JN_Un = thm "JN_Un";
    1.34 +val JN_constant = thm "JN_constant";
    1.35 +val JN_Join_distrib = thm "JN_Join_distrib";
    1.36 +val JN_Join_miniscope = thm "JN_Join_miniscope";
    1.37 +val JN_Join_diff = thm "JN_Join_diff";
    1.38 +val JN_constrains = thm "JN_constrains";
    1.39 +val Join_constrains = thm "Join_constrains";
    1.40 +val Join_unless = thm "Join_unless";
    1.41 +val Join_constrains_weaken = thm "Join_constrains_weaken";
    1.42 +val JN_constrains_weaken = thm "JN_constrains_weaken";
    1.43 +val JN_stable = thm "JN_stable";
    1.44 +val invariant_JN_I = thm "invariant_JN_I";
    1.45 +val Join_stable = thm "Join_stable";
    1.46 +val Join_increasing = thm "Join_increasing";
    1.47 +val invariant_JoinI = thm "invariant_JoinI";
    1.48 +val FP_JN = thm "FP_JN";
    1.49 +val JN_transient = thm "JN_transient";
    1.50 +val Join_transient = thm "Join_transient";
    1.51 +val Join_transient_I1 = thm "Join_transient_I1";
    1.52 +val Join_transient_I2 = thm "Join_transient_I2";
    1.53 +val JN_ensures = thm "JN_ensures";
    1.54 +val Join_ensures = thm "Join_ensures";
    1.55 +val stable_Join_constrains = thm "stable_Join_constrains";
    1.56 +val stable_Join_Always1 = thm "stable_Join_Always1";
    1.57 +val stable_Join_Always2 = thm "stable_Join_Always2";
    1.58 +val stable_Join_ensures1 = thm "stable_Join_ensures1";
    1.59 +val stable_Join_ensures2 = thm "stable_Join_ensures2";
    1.60 +val ok_SKIP1 = thm "ok_SKIP1";
    1.61 +val ok_SKIP2 = thm "ok_SKIP2";
    1.62 +val ok_Join_commute = thm "ok_Join_commute";
    1.63 +val ok_commute = thm "ok_commute";
    1.64 +val ok_sym = thm "ok_sym";
    1.65 +val ok_iff_OK = thm "ok_iff_OK";
    1.66 +val ok_Join_iff1 = thm "ok_Join_iff1";
    1.67 +val ok_Join_iff2 = thm "ok_Join_iff2";
    1.68 +val ok_Join_commute_I = thm "ok_Join_commute_I";
    1.69 +val ok_JN_iff1 = thm "ok_JN_iff1";
    1.70 +val ok_JN_iff2 = thm "ok_JN_iff2";
    1.71 +val OK_iff_ok = thm "OK_iff_ok";
    1.72 +val OK_imp_ok = thm "OK_imp_ok";
    1.73 +val Allowed_SKIP = thm "Allowed_SKIP";
    1.74 +val Allowed_Join = thm "Allowed_Join";
    1.75 +val Allowed_JN = thm "Allowed_JN";
    1.76 +val ok_iff_Allowed = thm "ok_iff_Allowed";
    1.77 +val OK_iff_Allowed = thm "OK_iff_Allowed";
    1.78 +val safety_prop_Acts_iff = thm "safety_prop_Acts_iff";
    1.79 +val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed";
    1.80 +val Allowed_eq = thm "Allowed_eq";
    1.81 +val def_prg_Allowed = thm "def_prg_Allowed";
    1.82 +val safety_prop_constrains = thm "safety_prop_constrains";
    1.83 +val safety_prop_stable = thm "safety_prop_stable";
    1.84 +val safety_prop_Int = thm "safety_prop_Int";
    1.85 +val safety_prop_INTER1 = thm "safety_prop_INTER1";
    1.86 +val safety_prop_INTER = thm "safety_prop_INTER";
    1.87 +val def_UNION_ok_iff = thm "def_UNION_ok_iff";
    1.88 +
    1.89 +(*Comp*)
    1.90 +val preserves_def = thm "preserves_def";
    1.91 +val funPair_def = thm "funPair_def";
    1.92 +val componentI = thm "componentI";
    1.93 +val component_eq_subset = thm "component_eq_subset";
    1.94 +val component_SKIP = thm "component_SKIP";
    1.95 +val component_refl = thm "component_refl";
    1.96 +val SKIP_minimal = thm "SKIP_minimal";
    1.97 +val component_Join1 = thm "component_Join1";
    1.98 +val component_Join2 = thm "component_Join2";
    1.99 +val Join_absorb1 = thm "Join_absorb1";
   1.100 +val Join_absorb2 = thm "Join_absorb2";
   1.101 +val JN_component_iff = thm "JN_component_iff";
   1.102 +val component_JN = thm "component_JN";
   1.103 +val component_trans = thm "component_trans";
   1.104 +val component_antisym = thm "component_antisym";
   1.105 +val Join_component_iff = thm "Join_component_iff";
   1.106 +val component_constrains = thm "component_constrains";
   1.107 +val program_less_le = thm "program_less_le";
   1.108 +val preservesI = thm "preservesI";
   1.109 +val preserves_imp_eq = thm "preserves_imp_eq";
   1.110 +val Join_preserves = thm "Join_preserves";
   1.111 +val JN_preserves = thm "JN_preserves";
   1.112 +val SKIP_preserves = thm "SKIP_preserves";
   1.113 +val funPair_apply = thm "funPair_apply";
   1.114 +val preserves_funPair = thm "preserves_funPair";
   1.115 +val funPair_o_distrib = thm "funPair_o_distrib";
   1.116 +val fst_o_funPair = thm "fst_o_funPair";
   1.117 +val snd_o_funPair = thm "snd_o_funPair";
   1.118 +val subset_preserves_o = thm "subset_preserves_o";
   1.119 +val preserves_subset_stable = thm "preserves_subset_stable";
   1.120 +val preserves_subset_increasing = thm "preserves_subset_increasing";
   1.121 +val preserves_id_subset_stable = thm "preserves_id_subset_stable";
   1.122 +val safety_prop_preserves = thm "safety_prop_preserves";
   1.123 +val stable_localTo_stable2 = thm "stable_localTo_stable2";
   1.124 +val Increasing_preserves_Stable = thm "Increasing_preserves_Stable";
   1.125 +val component_of_imp_component = thm "component_of_imp_component";
   1.126 +val component_of_refl = thm "component_of_refl";
   1.127 +val component_of_SKIP = thm "component_of_SKIP";
   1.128 +val component_of_trans = thm "component_of_trans";
   1.129 +val strict_component_of_eq = thm "strict_component_of_eq";
   1.130 +val localize_Init_eq = thm "localize_Init_eq";
   1.131 +val localize_Acts_eq = thm "localize_Acts_eq";
   1.132 +val localize_AllowedActs_eq = thm "localize_AllowedActs_eq";
   1.133 +
   1.134 +(*Guar*)
   1.135 +val guar_def = thm "guar_def";
   1.136 +val OK_insert_iff = thm "OK_insert_iff";
   1.137 +val ex1 = thm "ex1";
   1.138 +val ex2 = thm "ex2";
   1.139 +val ex_prop_finite = thm "ex_prop_finite";
   1.140 +val ex_prop_equiv = thm "ex_prop_equiv";
   1.141 +val uv1 = thm "uv1";
   1.142 +val uv2 = thm "uv2";
   1.143 +val uv_prop_finite = thm "uv_prop_finite";
   1.144 +val guaranteesI = thm "guaranteesI";
   1.145 +val guaranteesD = thm "guaranteesD";
   1.146 +val component_guaranteesD = thm "component_guaranteesD";
   1.147 +val guarantees_weaken = thm "guarantees_weaken";
   1.148 +val subset_imp_guarantees_UNIV = thm "subset_imp_guarantees_UNIV";
   1.149 +val subset_imp_guarantees = thm "subset_imp_guarantees";
   1.150 +val ex_prop_imp = thm "ex_prop_imp";
   1.151 +val guarantees_imp = thm "guarantees_imp";
   1.152 +val ex_prop_equiv2 = thm "ex_prop_equiv2";
   1.153 +val guarantees_UN_left = thm "guarantees_UN_left";
   1.154 +val guarantees_Un_left = thm "guarantees_Un_left";
   1.155 +val guarantees_INT_right = thm "guarantees_INT_right";
   1.156 +val guarantees_Int_right = thm "guarantees_Int_right";
   1.157 +val guarantees_Int_right_I = thm "guarantees_Int_right_I";
   1.158 +val guarantees_INT_right_iff = thm "guarantees_INT_right_iff";
   1.159 +val shunting = thm "shunting";
   1.160 +val contrapositive = thm "contrapositive";
   1.161 +val combining1 = thm "combining1";
   1.162 +val combining2 = thm "combining2";
   1.163 +val all_guarantees = thm "all_guarantees";
   1.164 +val ex_guarantees = thm "ex_guarantees";
   1.165 +val guarantees_Join_Int = thm "guarantees_Join_Int";
   1.166 +val guarantees_Join_Un = thm "guarantees_Join_Un";
   1.167 +val guarantees_JN_INT = thm "guarantees_JN_INT";
   1.168 +val guarantees_JN_UN = thm "guarantees_JN_UN";
   1.169 +val guarantees_Join_I1 = thm "guarantees_Join_I1";
   1.170 +val guarantees_Join_I2 = thm "guarantees_Join_I2";
   1.171 +val guarantees_JN_I = thm "guarantees_JN_I";
   1.172 +val Join_welldef_D1 = thm "Join_welldef_D1";
   1.173 +val Join_welldef_D2 = thm "Join_welldef_D2";
   1.174 +val refines_refl = thm "refines_refl";
   1.175 +val ex_refinement_thm = thm "ex_refinement_thm";
   1.176 +val uv_refinement_thm = thm "uv_refinement_thm";
   1.177 +val guarantees_equiv = thm "guarantees_equiv";
   1.178 +val wg_weakest = thm "wg_weakest";
   1.179 +val wg_guarantees = thm "wg_guarantees";
   1.180 +val wg_equiv = thm "wg_equiv";
   1.181 +val component_of_wg = thm "component_of_wg";
   1.182 +val wg_finite = thm "wg_finite";
   1.183 +val wg_ex_prop = thm "wg_ex_prop";
   1.184 +val wx_subset = thm "wx_subset";
   1.185 +val wx_ex_prop = thm "wx_ex_prop";
   1.186 +val wx_weakest = thm "wx_weakest";
   1.187 +val wx'_ex_prop = thm "wx'_ex_prop";
   1.188 +val wx_equiv = thm "wx_equiv";
   1.189 +val guarantees_wx_eq = thm "guarantees_wx_eq";
   1.190 +val stable_guarantees_Always = thm "stable_guarantees_Always";
   1.191 +val leadsTo_Basis = thm "leadsTo_Basis";
   1.192 +val constrains_guarantees_leadsTo = thm "constrains_guarantees_leadsTo";
   1.193 +
   1.194  (*Extend*)
   1.195  val Restrict_iff = thm "Restrict_iff";
   1.196  val Restrict_UNIV = thm "Restrict_UNIV";