--- a/src/HOL/UNITY/UNITY_tactics.ML Wed Jan 29 16:29:38 2003 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Wed Jan 29 16:34:51 2003 +0100
@@ -6,6 +6,193 @@
Specialized UNITY tactics, and ML bindings of theorems
*)
+(*Union*)
+val Init_SKIP = thm "Init_SKIP";
+val Acts_SKIP = thm "Acts_SKIP";
+val AllowedActs_SKIP = thm "AllowedActs_SKIP";
+val reachable_SKIP = thm "reachable_SKIP";
+val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff";
+val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff";
+val SKIP_in_stable = thm "SKIP_in_stable";
+val Init_Join = thm "Init_Join";
+val Acts_Join = thm "Acts_Join";
+val AllowedActs_Join = thm "AllowedActs_Join";
+val JN_empty = thm "JN_empty";
+val JN_insert = thm "JN_insert";
+val Init_JN = thm "Init_JN";
+val Acts_JN = thm "Acts_JN";
+val AllowedActs_JN = thm "AllowedActs_JN";
+val JN_cong = thm "JN_cong";
+val Join_commute = thm "Join_commute";
+val Join_assoc = thm "Join_assoc";
+val Join_left_commute = thm "Join_left_commute";
+val Join_SKIP_left = thm "Join_SKIP_left";
+val Join_SKIP_right = thm "Join_SKIP_right";
+val Join_absorb = thm "Join_absorb";
+val Join_left_absorb = thm "Join_left_absorb";
+val Join_ac = thms "Join_ac";
+val JN_absorb = thm "JN_absorb";
+val JN_Un = thm "JN_Un";
+val JN_constant = thm "JN_constant";
+val JN_Join_distrib = thm "JN_Join_distrib";
+val JN_Join_miniscope = thm "JN_Join_miniscope";
+val JN_Join_diff = thm "JN_Join_diff";
+val JN_constrains = thm "JN_constrains";
+val Join_constrains = thm "Join_constrains";
+val Join_unless = thm "Join_unless";
+val Join_constrains_weaken = thm "Join_constrains_weaken";
+val JN_constrains_weaken = thm "JN_constrains_weaken";
+val JN_stable = thm "JN_stable";
+val invariant_JN_I = thm "invariant_JN_I";
+val Join_stable = thm "Join_stable";
+val Join_increasing = thm "Join_increasing";
+val invariant_JoinI = thm "invariant_JoinI";
+val FP_JN = thm "FP_JN";
+val JN_transient = thm "JN_transient";
+val Join_transient = thm "Join_transient";
+val Join_transient_I1 = thm "Join_transient_I1";
+val Join_transient_I2 = thm "Join_transient_I2";
+val JN_ensures = thm "JN_ensures";
+val Join_ensures = thm "Join_ensures";
+val stable_Join_constrains = thm "stable_Join_constrains";
+val stable_Join_Always1 = thm "stable_Join_Always1";
+val stable_Join_Always2 = thm "stable_Join_Always2";
+val stable_Join_ensures1 = thm "stable_Join_ensures1";
+val stable_Join_ensures2 = thm "stable_Join_ensures2";
+val ok_SKIP1 = thm "ok_SKIP1";
+val ok_SKIP2 = thm "ok_SKIP2";
+val ok_Join_commute = thm "ok_Join_commute";
+val ok_commute = thm "ok_commute";
+val ok_sym = thm "ok_sym";
+val ok_iff_OK = thm "ok_iff_OK";
+val ok_Join_iff1 = thm "ok_Join_iff1";
+val ok_Join_iff2 = thm "ok_Join_iff2";
+val ok_Join_commute_I = thm "ok_Join_commute_I";
+val ok_JN_iff1 = thm "ok_JN_iff1";
+val ok_JN_iff2 = thm "ok_JN_iff2";
+val OK_iff_ok = thm "OK_iff_ok";
+val OK_imp_ok = thm "OK_imp_ok";
+val Allowed_SKIP = thm "Allowed_SKIP";
+val Allowed_Join = thm "Allowed_Join";
+val Allowed_JN = thm "Allowed_JN";
+val ok_iff_Allowed = thm "ok_iff_Allowed";
+val OK_iff_Allowed = thm "OK_iff_Allowed";
+val safety_prop_Acts_iff = thm "safety_prop_Acts_iff";
+val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed";
+val Allowed_eq = thm "Allowed_eq";
+val def_prg_Allowed = thm "def_prg_Allowed";
+val safety_prop_constrains = thm "safety_prop_constrains";
+val safety_prop_stable = thm "safety_prop_stable";
+val safety_prop_Int = thm "safety_prop_Int";
+val safety_prop_INTER1 = thm "safety_prop_INTER1";
+val safety_prop_INTER = thm "safety_prop_INTER";
+val def_UNION_ok_iff = thm "def_UNION_ok_iff";
+
+(*Comp*)
+val preserves_def = thm "preserves_def";
+val funPair_def = thm "funPair_def";
+val componentI = thm "componentI";
+val component_eq_subset = thm "component_eq_subset";
+val component_SKIP = thm "component_SKIP";
+val component_refl = thm "component_refl";
+val SKIP_minimal = thm "SKIP_minimal";
+val component_Join1 = thm "component_Join1";
+val component_Join2 = thm "component_Join2";
+val Join_absorb1 = thm "Join_absorb1";
+val Join_absorb2 = thm "Join_absorb2";
+val JN_component_iff = thm "JN_component_iff";
+val component_JN = thm "component_JN";
+val component_trans = thm "component_trans";
+val component_antisym = thm "component_antisym";
+val Join_component_iff = thm "Join_component_iff";
+val component_constrains = thm "component_constrains";
+val program_less_le = thm "program_less_le";
+val preservesI = thm "preservesI";
+val preserves_imp_eq = thm "preserves_imp_eq";
+val Join_preserves = thm "Join_preserves";
+val JN_preserves = thm "JN_preserves";
+val SKIP_preserves = thm "SKIP_preserves";
+val funPair_apply = thm "funPair_apply";
+val preserves_funPair = thm "preserves_funPair";
+val funPair_o_distrib = thm "funPair_o_distrib";
+val fst_o_funPair = thm "fst_o_funPair";
+val snd_o_funPair = thm "snd_o_funPair";
+val subset_preserves_o = thm "subset_preserves_o";
+val preserves_subset_stable = thm "preserves_subset_stable";
+val preserves_subset_increasing = thm "preserves_subset_increasing";
+val preserves_id_subset_stable = thm "preserves_id_subset_stable";
+val safety_prop_preserves = thm "safety_prop_preserves";
+val stable_localTo_stable2 = thm "stable_localTo_stable2";
+val Increasing_preserves_Stable = thm "Increasing_preserves_Stable";
+val component_of_imp_component = thm "component_of_imp_component";
+val component_of_refl = thm "component_of_refl";
+val component_of_SKIP = thm "component_of_SKIP";
+val component_of_trans = thm "component_of_trans";
+val strict_component_of_eq = thm "strict_component_of_eq";
+val localize_Init_eq = thm "localize_Init_eq";
+val localize_Acts_eq = thm "localize_Acts_eq";
+val localize_AllowedActs_eq = thm "localize_AllowedActs_eq";
+
+(*Guar*)
+val guar_def = thm "guar_def";
+val OK_insert_iff = thm "OK_insert_iff";
+val ex1 = thm "ex1";
+val ex2 = thm "ex2";
+val ex_prop_finite = thm "ex_prop_finite";
+val ex_prop_equiv = thm "ex_prop_equiv";
+val uv1 = thm "uv1";
+val uv2 = thm "uv2";
+val uv_prop_finite = thm "uv_prop_finite";
+val guaranteesI = thm "guaranteesI";
+val guaranteesD = thm "guaranteesD";
+val component_guaranteesD = thm "component_guaranteesD";
+val guarantees_weaken = thm "guarantees_weaken";
+val subset_imp_guarantees_UNIV = thm "subset_imp_guarantees_UNIV";
+val subset_imp_guarantees = thm "subset_imp_guarantees";
+val ex_prop_imp = thm "ex_prop_imp";
+val guarantees_imp = thm "guarantees_imp";
+val ex_prop_equiv2 = thm "ex_prop_equiv2";
+val guarantees_UN_left = thm "guarantees_UN_left";
+val guarantees_Un_left = thm "guarantees_Un_left";
+val guarantees_INT_right = thm "guarantees_INT_right";
+val guarantees_Int_right = thm "guarantees_Int_right";
+val guarantees_Int_right_I = thm "guarantees_Int_right_I";
+val guarantees_INT_right_iff = thm "guarantees_INT_right_iff";
+val shunting = thm "shunting";
+val contrapositive = thm "contrapositive";
+val combining1 = thm "combining1";
+val combining2 = thm "combining2";
+val all_guarantees = thm "all_guarantees";
+val ex_guarantees = thm "ex_guarantees";
+val guarantees_Join_Int = thm "guarantees_Join_Int";
+val guarantees_Join_Un = thm "guarantees_Join_Un";
+val guarantees_JN_INT = thm "guarantees_JN_INT";
+val guarantees_JN_UN = thm "guarantees_JN_UN";
+val guarantees_Join_I1 = thm "guarantees_Join_I1";
+val guarantees_Join_I2 = thm "guarantees_Join_I2";
+val guarantees_JN_I = thm "guarantees_JN_I";
+val Join_welldef_D1 = thm "Join_welldef_D1";
+val Join_welldef_D2 = thm "Join_welldef_D2";
+val refines_refl = thm "refines_refl";
+val ex_refinement_thm = thm "ex_refinement_thm";
+val uv_refinement_thm = thm "uv_refinement_thm";
+val guarantees_equiv = thm "guarantees_equiv";
+val wg_weakest = thm "wg_weakest";
+val wg_guarantees = thm "wg_guarantees";
+val wg_equiv = thm "wg_equiv";
+val component_of_wg = thm "component_of_wg";
+val wg_finite = thm "wg_finite";
+val wg_ex_prop = thm "wg_ex_prop";
+val wx_subset = thm "wx_subset";
+val wx_ex_prop = thm "wx_ex_prop";
+val wx_weakest = thm "wx_weakest";
+val wx'_ex_prop = thm "wx'_ex_prop";
+val wx_equiv = thm "wx_equiv";
+val guarantees_wx_eq = thm "guarantees_wx_eq";
+val stable_guarantees_Always = thm "stable_guarantees_Always";
+val leadsTo_Basis = thm "leadsTo_Basis";
+val constrains_guarantees_leadsTo = thm "constrains_guarantees_leadsTo";
+
(*Extend*)
val Restrict_iff = thm "Restrict_iff";
val Restrict_UNIV = thm "Restrict_UNIV";