src/HOL/UNITY/UNITY_tactics.ML
changeset 13797 baefae13ad37
parent 13796 19f50fa807ae
child 13798 4c1a53627500
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Thu Jan 30 10:35:56 2003 +0100
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu Jan 30 18:08:09 2003 +0100
     1.3 @@ -6,6 +6,215 @@
     1.4  Specialized UNITY tactics, and ML bindings of theorems
     1.5  *)
     1.6  
     1.7 +(*UNITY*)
     1.8 +val constrains_def = thm "constrains_def";
     1.9 +val stable_def = thm "stable_def";
    1.10 +val invariant_def = thm "invariant_def";
    1.11 +val increasing_def = thm "increasing_def";
    1.12 +val Allowed_def = thm "Allowed_def";
    1.13 +val Id_in_Acts = thm "Id_in_Acts";
    1.14 +val insert_Id_Acts = thm "insert_Id_Acts";
    1.15 +val Id_in_AllowedActs = thm "Id_in_AllowedActs";
    1.16 +val insert_Id_AllowedActs = thm "insert_Id_AllowedActs";
    1.17 +val Init_eq = thm "Init_eq";
    1.18 +val Acts_eq = thm "Acts_eq";
    1.19 +val AllowedActs_eq = thm "AllowedActs_eq";
    1.20 +val surjective_mk_program = thm "surjective_mk_program";
    1.21 +val program_equalityI = thm "program_equalityI";
    1.22 +val program_equalityE = thm "program_equalityE";
    1.23 +val program_equality_iff = thm "program_equality_iff";
    1.24 +val def_prg_Init = thm "def_prg_Init";
    1.25 +val def_prg_Acts = thm "def_prg_Acts";
    1.26 +val def_prg_AllowedActs = thm "def_prg_AllowedActs";
    1.27 +val def_prg_simps = thm "def_prg_simps";
    1.28 +val def_act_simp = thm "def_act_simp";
    1.29 +val def_set_simp = thm "def_set_simp";
    1.30 +val constrainsI = thm "constrainsI";
    1.31 +val constrainsD = thm "constrainsD";
    1.32 +val constrains_empty = thm "constrains_empty";
    1.33 +val constrains_empty2 = thm "constrains_empty2";
    1.34 +val constrains_UNIV = thm "constrains_UNIV";
    1.35 +val constrains_UNIV2 = thm "constrains_UNIV2";
    1.36 +val constrains_weaken_R = thm "constrains_weaken_R";
    1.37 +val constrains_weaken_L = thm "constrains_weaken_L";
    1.38 +val constrains_weaken = thm "constrains_weaken";
    1.39 +val constrains_Un = thm "constrains_Un";
    1.40 +val constrains_UN = thm "constrains_UN";
    1.41 +val constrains_Un_distrib = thm "constrains_Un_distrib";
    1.42 +val constrains_UN_distrib = thm "constrains_UN_distrib";
    1.43 +val constrains_Int_distrib = thm "constrains_Int_distrib";
    1.44 +val constrains_INT_distrib = thm "constrains_INT_distrib";
    1.45 +val constrains_Int = thm "constrains_Int";
    1.46 +val constrains_INT = thm "constrains_INT";
    1.47 +val constrains_imp_subset = thm "constrains_imp_subset";
    1.48 +val constrains_trans = thm "constrains_trans";
    1.49 +val constrains_cancel = thm "constrains_cancel";
    1.50 +val unlessI = thm "unlessI";
    1.51 +val unlessD = thm "unlessD";
    1.52 +val stableI = thm "stableI";
    1.53 +val stableD = thm "stableD";
    1.54 +val stable_UNIV = thm "stable_UNIV";
    1.55 +val stable_Un = thm "stable_Un";
    1.56 +val stable_UN = thm "stable_UN";
    1.57 +val stable_Int = thm "stable_Int";
    1.58 +val stable_INT = thm "stable_INT";
    1.59 +val stable_constrains_Un = thm "stable_constrains_Un";
    1.60 +val stable_constrains_Int = thm "stable_constrains_Int";
    1.61 +val stable_constrains_stable = thm "stable_constrains_stable";
    1.62 +val invariantI = thm "invariantI";
    1.63 +val invariant_Int = thm "invariant_Int";
    1.64 +val increasingD = thm "increasingD";
    1.65 +val increasing_constant = thm "increasing_constant";
    1.66 +val mono_increasing_o = thm "mono_increasing_o";
    1.67 +val strict_increasingD = thm "strict_increasingD";
    1.68 +val elimination = thm "elimination";
    1.69 +val elimination_sing = thm "elimination_sing";
    1.70 +val constrains_strongest_rhs = thm "constrains_strongest_rhs";
    1.71 +val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest";
    1.72 +val Un_Diff_Diff = thm "Un_Diff_Diff";
    1.73 +val Int_Union_Union = thm "Int_Union_Union";
    1.74 +val Image_less_than = thm "Image_less_than";
    1.75 +val Image_inverse_less_than = thm "Image_inverse_less_than";
    1.76 +
    1.77 +(*WFair*)
    1.78 +val stable_transient_empty = thm "stable_transient_empty";
    1.79 +val transient_strengthen = thm "transient_strengthen";
    1.80 +val transientI = thm "transientI";
    1.81 +val transientE = thm "transientE";
    1.82 +val transient_UNIV = thm "transient_UNIV";
    1.83 +val transient_empty = thm "transient_empty";
    1.84 +val ensuresI = thm "ensuresI";
    1.85 +val ensuresD = thm "ensuresD";
    1.86 +val ensures_weaken_R = thm "ensures_weaken_R";
    1.87 +val stable_ensures_Int = thm "stable_ensures_Int";
    1.88 +val stable_transient_ensures = thm "stable_transient_ensures";
    1.89 +val ensures_eq = thm "ensures_eq";
    1.90 +val leadsTo_Basis = thm "leadsTo_Basis";
    1.91 +val leadsTo_Trans = thm "leadsTo_Trans";
    1.92 +val transient_imp_leadsTo = thm "transient_imp_leadsTo";
    1.93 +val leadsTo_Un_duplicate = thm "leadsTo_Un_duplicate";
    1.94 +val leadsTo_Un_duplicate2 = thm "leadsTo_Un_duplicate2";
    1.95 +val leadsTo_Union = thm "leadsTo_Union";
    1.96 +val leadsTo_Union_Int = thm "leadsTo_Union_Int";
    1.97 +val leadsTo_UN = thm "leadsTo_UN";
    1.98 +val leadsTo_Un = thm "leadsTo_Un";
    1.99 +val single_leadsTo_I = thm "single_leadsTo_I";
   1.100 +val leadsTo_induct = thm "leadsTo_induct";
   1.101 +val subset_imp_ensures = thm "subset_imp_ensures";
   1.102 +val subset_imp_leadsTo = thm "subset_imp_leadsTo";
   1.103 +val leadsTo_refl = thm "leadsTo_refl";
   1.104 +val empty_leadsTo = thm "empty_leadsTo";
   1.105 +val leadsTo_UNIV = thm "leadsTo_UNIV";
   1.106 +val leadsTo_induct_pre_lemma = thm "leadsTo_induct_pre_lemma";
   1.107 +val leadsTo_induct_pre = thm "leadsTo_induct_pre";
   1.108 +val leadsTo_weaken_R = thm "leadsTo_weaken_R";
   1.109 +val leadsTo_weaken_L = thm "leadsTo_weaken_L";
   1.110 +val leadsTo_Un_distrib = thm "leadsTo_Un_distrib";
   1.111 +val leadsTo_UN_distrib = thm "leadsTo_UN_distrib";
   1.112 +val leadsTo_Union_distrib = thm "leadsTo_Union_distrib";
   1.113 +val leadsTo_weaken = thm "leadsTo_weaken";
   1.114 +val leadsTo_Diff = thm "leadsTo_Diff";
   1.115 +val leadsTo_UN_UN = thm "leadsTo_UN_UN";
   1.116 +val leadsTo_Un_Un = thm "leadsTo_Un_Un";
   1.117 +val leadsTo_cancel2 = thm "leadsTo_cancel2";
   1.118 +val leadsTo_cancel_Diff2 = thm "leadsTo_cancel_Diff2";
   1.119 +val leadsTo_cancel1 = thm "leadsTo_cancel1";
   1.120 +val leadsTo_cancel_Diff1 = thm "leadsTo_cancel_Diff1";
   1.121 +val leadsTo_empty = thm "leadsTo_empty";
   1.122 +val psp_stable = thm "psp_stable";
   1.123 +val psp_stable2 = thm "psp_stable2";
   1.124 +val psp_ensures = thm "psp_ensures";
   1.125 +val psp = thm "psp";
   1.126 +val psp2 = thm "psp2";
   1.127 +val psp_unless = thm "psp_unless";
   1.128 +val leadsTo_wf_induct_lemma = thm "leadsTo_wf_induct_lemma";
   1.129 +val leadsTo_wf_induct = thm "leadsTo_wf_induct";
   1.130 +val bounded_induct = thm "bounded_induct";
   1.131 +val lessThan_induct = thm "lessThan_induct";
   1.132 +val lessThan_bounded_induct = thm "lessThan_bounded_induct";
   1.133 +val greaterThan_bounded_induct = thm "greaterThan_bounded_induct";
   1.134 +val wlt_leadsTo = thm "wlt_leadsTo";
   1.135 +val leadsTo_subset = thm "leadsTo_subset";
   1.136 +val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt";
   1.137 +val wlt_increasing = thm "wlt_increasing";
   1.138 +val lemma1 = thm "lemma1";
   1.139 +val leadsTo_123 = thm "leadsTo_123";
   1.140 +val wlt_constrains_wlt = thm "wlt_constrains_wlt";
   1.141 +val completion_lemma = thm "completion_lemma";
   1.142 +val completion = thm "completion";
   1.143 +val finite_completion_lemma = thm "finite_completion_lemma";
   1.144 +val finite_completion = thm "finite_completion";
   1.145 +val stable_completion = thm "stable_completion";
   1.146 +val finite_stable_completion = thm "finite_stable_completion";
   1.147 +
   1.148 +(*Constrains*)
   1.149 +val Increasing_def = thm "Increasing_def";
   1.150 +val reachable_Init = thm "reachable.Init";
   1.151 +val reachable_Acts = thm "reachable.Acts";
   1.152 +val reachable_equiv_traces = thm "reachable_equiv_traces";
   1.153 +val Init_subset_reachable = thm "Init_subset_reachable";
   1.154 +val stable_reachable = thm "stable_reachable";
   1.155 +val invariant_reachable = thm "invariant_reachable";
   1.156 +val invariant_includes_reachable = thm "invariant_includes_reachable";
   1.157 +val constrains_reachable_Int = thm "constrains_reachable_Int";
   1.158 +val Constrains_eq_constrains = thm "Constrains_eq_constrains";
   1.159 +val constrains_imp_Constrains = thm "constrains_imp_Constrains";
   1.160 +val stable_imp_Stable = thm "stable_imp_Stable";
   1.161 +val ConstrainsI = thm "ConstrainsI";
   1.162 +val Constrains_empty = thm "Constrains_empty";
   1.163 +val Constrains_UNIV = thm "Constrains_UNIV";
   1.164 +val Constrains_weaken_R = thm "Constrains_weaken_R";
   1.165 +val Constrains_weaken_L = thm "Constrains_weaken_L";
   1.166 +val Constrains_weaken = thm "Constrains_weaken";
   1.167 +val Constrains_Un = thm "Constrains_Un";
   1.168 +val Constrains_UN = thm "Constrains_UN";
   1.169 +val Constrains_Int = thm "Constrains_Int";
   1.170 +val Constrains_INT = thm "Constrains_INT";
   1.171 +val Constrains_imp_subset = thm "Constrains_imp_subset";
   1.172 +val Constrains_trans = thm "Constrains_trans";
   1.173 +val Constrains_cancel = thm "Constrains_cancel";
   1.174 +val Stable_eq = thm "Stable_eq";
   1.175 +val Stable_eq_stable = thm "Stable_eq_stable";
   1.176 +val StableI = thm "StableI";
   1.177 +val StableD = thm "StableD";
   1.178 +val Stable_Un = thm "Stable_Un";
   1.179 +val Stable_Int = thm "Stable_Int";
   1.180 +val Stable_Constrains_Un = thm "Stable_Constrains_Un";
   1.181 +val Stable_Constrains_Int = thm "Stable_Constrains_Int";
   1.182 +val Stable_UN = thm "Stable_UN";
   1.183 +val Stable_INT = thm "Stable_INT";
   1.184 +val Stable_reachable = thm "Stable_reachable";
   1.185 +val IncreasingD = thm "IncreasingD";
   1.186 +val mono_Increasing_o = thm "mono_Increasing_o";
   1.187 +val strict_IncreasingD = thm "strict_IncreasingD";
   1.188 +val increasing_imp_Increasing = thm "increasing_imp_Increasing";
   1.189 +val Increasing_constant = thm "Increasing_constant";
   1.190 +val Elimination = thm "Elimination";
   1.191 +val Elimination_sing = thm "Elimination_sing";
   1.192 +val AlwaysI = thm "AlwaysI";
   1.193 +val AlwaysD = thm "AlwaysD";
   1.194 +val AlwaysE = thm "AlwaysE";
   1.195 +val Always_imp_Stable = thm "Always_imp_Stable";
   1.196 +val Always_includes_reachable = thm "Always_includes_reachable";
   1.197 +val invariant_imp_Always = thm "invariant_imp_Always";
   1.198 +val Always_reachable = thm "Always_reachable";
   1.199 +val Always_eq_invariant_reachable = thm "Always_eq_invariant_reachable";
   1.200 +val Always_eq_includes_reachable = thm "Always_eq_includes_reachable";
   1.201 +val Always_UNIV_eq = thm "Always_UNIV_eq";
   1.202 +val UNIV_AlwaysI = thm "UNIV_AlwaysI";
   1.203 +val Always_eq_UN_invariant = thm "Always_eq_UN_invariant";
   1.204 +val Always_weaken = thm "Always_weaken";
   1.205 +val Always_Constrains_pre = thm "Always_Constrains_pre";
   1.206 +val Always_Constrains_post = thm "Always_Constrains_post";
   1.207 +val Always_ConstrainsI = thm "Always_ConstrainsI";
   1.208 +val Always_ConstrainsD = thm "Always_ConstrainsD";
   1.209 +val Always_Constrains_weaken = thm "Always_Constrains_weaken";
   1.210 +val Always_Int_distrib = thm "Always_Int_distrib";
   1.211 +val Always_INT_distrib = thm "Always_INT_distrib";
   1.212 +val Always_Int_I = thm "Always_Int_I";
   1.213 +val Always_Compl_Un_eq = thm "Always_Compl_Un_eq";
   1.214 +val Always_thin = thm "Always_thin";
   1.215 +
   1.216  (*FP*)
   1.217  val stable_FP_Orig_Int = thm "stable_FP_Orig_Int";
   1.218  val FP_Orig_weakest = thm "FP_Orig_weakest";
   1.219 @@ -473,6 +682,18 @@
   1.220  val LeadsTo_le_imp_pfixGe = thm "LeadsTo_le_imp_pfixGe";
   1.221  
   1.222  
   1.223 +(*Lazy unfolding of actions or of sets*)
   1.224 +fun simp_of_act def = def RS def_act_simp;
   1.225 +
   1.226 +fun simp_of_set def = def RS def_set_simp;
   1.227 +
   1.228 +
   1.229 +(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   1.230 +val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin
   1.231 +
   1.232 +(*Combines a list of invariance THEOREMS into one.*)
   1.233 +val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I)
   1.234 +
   1.235  (*proves "co" properties when the program is specified*)
   1.236  fun gen_constrains_tac(cs,ss) i = 
   1.237     SELECT_GOAL
   1.238 @@ -504,6 +725,8 @@
   1.239  	      ALLGOALS (clarify_tac cs),
   1.240  	      ALLGOALS (asm_lr_simp_tac ss)]);
   1.241  
   1.242 +fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
   1.243 +
   1.244  fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact;
   1.245  
   1.246