stripped some legacy bindings
authorhaftmann
Fri Dec 01 17:22:28 2006 +0100 (2006-12-01)
changeset 21619dea0914773f7
parent 21618 1cbb1134cb6c
child 21620 3d4bfc7f6363
stripped some legacy bindings
src/HOL/Auth/Public.thy
src/HOL/HOL.ML
src/HOL/Lattices.thy
src/HOL/Orderings.ML
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOL/Auth/Public.thy	Fri Dec 01 16:08:45 2006 +0100
     1.2 +++ b/src/HOL/Auth/Public.thy	Fri Dec 01 17:22:28 2006 +0100
     1.3 @@ -402,15 +402,14 @@
     1.4         insert_Key_singleton 
     1.5         Key_not_used insert_Key_image Un_assoc [THEN sym]
     1.6  
     1.7 -ML
     1.8 -{*
     1.9 +ML {*
    1.10  val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
    1.11  val analz_image_freshK_simps = thms "analz_image_freshK_simps";
    1.12 +val imp_disjL = thm "imp_disjL";
    1.13  
    1.14 -val analz_image_freshK_ss = 
    1.15 -     simpset() delsimps [image_insert, image_Un]
    1.16 -	       delsimps [imp_disjL]    (*reduces blow-up*)
    1.17 -	       addsimps thms "analz_image_freshK_simps"
    1.18 +val analz_image_freshK_ss = simpset() delsimps [image_insert, image_Un]
    1.19 +  delsimps [imp_disjL]    (*reduces blow-up*)
    1.20 +  addsimps thms "analz_image_freshK_simps"
    1.21  *}
    1.22  
    1.23  method_setup analz_freshK = {*
     2.1 --- a/src/HOL/HOL.ML	Fri Dec 01 16:08:45 2006 +0100
     2.2 +++ b/src/HOL/HOL.ML	Fri Dec 01 17:22:28 2006 +0100
     2.3 @@ -20,7 +20,6 @@
     2.4  
     2.5  val split_tac        = Splitter.split_tac;
     2.6  val split_inside_tac = Splitter.split_inside_tac;
     2.7 -val split_asm_tac    = Splitter.split_asm_tac;
     2.8  
     2.9  val op addsplits     = Splitter.addsplits;
    2.10  val op delsplits     = Splitter.delsplits;
    2.11 @@ -38,175 +37,100 @@
    2.12  open BasicClassical;
    2.13  open Clasimp;
    2.14  
    2.15 -val eq_reflection = thm "eq_reflection";
    2.16 -val def_imp_eq = thm "def_imp_eq";
    2.17 -val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
    2.18 -val ccontr = thm "ccontr";
    2.19 -val impI = thm "impI";
    2.20 -val impCE = thm "impCE";
    2.21 -val notI = thm "notI";
    2.22 -val notE = thm "notE";
    2.23 -val iffI = thm "iffI";
    2.24 -val iffCE = thm "iffCE";
    2.25 -val conjI = thm "conjI";
    2.26 -val conjE = thm "conjE";
    2.27 -val disjCI = thm "disjCI";
    2.28 -val disjE = thm "disjE";
    2.29 -val TrueI = thm "TrueI";
    2.30 -val FalseE = thm "FalseE";
    2.31 -val allI = thm "allI";
    2.32 +val all_conj_distrib = thm "all_conj_distrib";
    2.33 +val all_dupE = thm "all_dupE"
    2.34  val allE = thm "allE";
    2.35 -val exI = thm "exI";
    2.36 -val exE = thm "exE";
    2.37 -val ex_ex1I = thm "ex_ex1I";
    2.38 -val the_equality = thm "the_equality";
    2.39 -val mp = thm "mp";
    2.40 -val rev_mp = thm "rev_mp"
    2.41 +val allI = thm "allI";
    2.42 +val all_simps = thms "all_simps";
    2.43 +val arg_cong = thm "arg_cong";
    2.44 +val atomize_not = thm "atomize_not";
    2.45 +val box_equals = thm "box_equals"
    2.46 +val case_split = thm "case_split_thm";
    2.47 +val case_split_thm = thm "case_split_thm"
    2.48 +val cases_simp = thm "cases_simp";
    2.49 +val ccontr = thm "ccontr";
    2.50 +val choice_eq = thm "choice_eq"
    2.51  val classical = thm "classical";
    2.52 -val subst = thm "subst";
    2.53 -val refl = thm "refl";
    2.54 -val sym = thm "sym";
    2.55 -val trans = thm "trans";
    2.56 -val arg_cong = thm "arg_cong";
    2.57 -val iffD1 = thm "iffD1";
    2.58 -val iffD2 = thm "iffD2";
    2.59 -val disjE = thm "disjE";
    2.60 +val cong = thm "cong"
    2.61 +val conj_comms = thms "conj_comms";
    2.62 +val conj_cong = thm "conj_cong";
    2.63 +val conjE = thm "conjE"
    2.64  val conjE = thm "conjE";
    2.65 -val exE = thm "exE";
    2.66 -val contrapos_nn = thm "contrapos_nn";
    2.67 -val contrapos_pp = thm "contrapos_pp";
    2.68 -val notnotD = thm "notnotD";
    2.69 +val conjI = thm "conjI";
    2.70  val conjunct1 = thm "conjunct1";
    2.71  val conjunct2 = thm "conjunct2";
    2.72 -val spec = thm "spec";
    2.73 -val imp_cong = thm "imp_cong";
    2.74 -val the_sym_eq_trivial = thm "the_sym_eq_trivial";
    2.75 -val triv_forall_equality = thm "triv_forall_equality";
    2.76 -val case_split = thm "case_split_thm";
    2.77 -val ext = thm "ext"
    2.78 -val True_def = thm "True_def"
    2.79 -val All_def = thm "All_def"
    2.80 -val Ex_def = thm "Ex_def"
    2.81 -val False_def = thm "False_def"
    2.82 -val not_def = thm "not_def"
    2.83 -val and_def = thm "and_def"
    2.84 -val or_def = thm "or_def"
    2.85 -val Ex1_def = thm "Ex1_def"
    2.86 -val iff = thm "iff"
    2.87 -val True_or_False = thm "True_or_False"
    2.88 -val Let_def = thm "Let_def"
    2.89 -val if_def = thm "if_def"
    2.90 -val ssubst = thm "ssubst"
    2.91 -val box_equals = thm "box_equals"
    2.92 -val fun_cong = thm "fun_cong"
    2.93 -val cong = thm "cong"
    2.94 -val rev_iffD2 = thm "rev_iffD2"
    2.95 -val rev_iffD1 = thm "rev_iffD1"
    2.96 -val iffE = thm "iffE"
    2.97 -val eqTrueI = thm "eqTrueI"
    2.98 -val eqTrueE = thm "eqTrueE"
    2.99 -val all_dupE = thm "all_dupE"
   2.100 -val FalseE = thm "FalseE"
   2.101 -val False_neq_True = thm "False_neq_True"
   2.102 -val False_not_True = thm "False_not_True"
   2.103 -val True_not_False = thm "True_not_False"
   2.104 -val notI2 = thm "notI2"
   2.105 -val impE = thm "impE"
   2.106 -val not_sym = thm "not_sym"
   2.107 -val rev_contrapos = thm "rev_contrapos"
   2.108 -val conjE = thm "conjE"
   2.109 -val context_conjI = thm "context_conjI"
   2.110 -val disjI1 = thm "disjI1"
   2.111 -val disjI2 = thm "disjI2"
   2.112 -val rev_notE = thm "rev_notE"
   2.113 -val ex1I = thm "ex1I"
   2.114 -val ex1E = thm "ex1E"
   2.115 -val ex1_implies_ex = thm "ex1_implies_ex"
   2.116 -val the_equality = thm "the_equality"
   2.117 -val theI = thm "theI"
   2.118 -val theI' = thm "theI'"
   2.119 -val theI2 = thm "theI2"
   2.120 -val the1_equality = thm "the1_equality"
   2.121 -val excluded_middle = thm "excluded_middle"
   2.122 -val case_split_thm = thm "case_split_thm"
   2.123 -val exCI = thm "exCI"
   2.124 -val choice_eq = thm "choice_eq"
   2.125 -val eq_cong2 = thm "eq_cong2"
   2.126 -val if_cong = thm "if_cong"
   2.127 -val if_weak_cong = thm "if_weak_cong"
   2.128 -val let_weak_cong = thm "let_weak_cong"
   2.129 -val eq_cong2 = thm "eq_cong2"
   2.130 -val if_distrib = thm "if_distrib"
   2.131 -val restrict_to_left = thm "restrict_to_left"
   2.132 -val all_conj_distrib = thm "all_conj_distrib";
   2.133 -val atomize_not = thm "atomize_not";
   2.134 -val split_if = thm "split_if";
   2.135 -val split_if_asm = thm "split_if_asm";
   2.136 -val rev_conj_cong = thm "rev_conj_cong";
   2.137 -val not_all = thm "not_all";
   2.138 -val not_ex = thm "not_ex";
   2.139 -val not_iff = thm "not_iff";
   2.140 -val not_imp = thm "not_imp";
   2.141 -val not_not = thm "not_not";
   2.142 -val eta_contract_eq = thm "eta_contract_eq";
   2.143 -val eq_ac = thms "eq_ac";
   2.144 -val eq_commute = thm "eq_commute";
   2.145 -val eq_sym_conv = thm "eq_commute";
   2.146 -val neq_commute = thm "neq_commute";
   2.147 -val conj_comms = thms "conj_comms";
   2.148 -val conj_commute = thm "conj_commute";
   2.149 -val conj_cong = thm "conj_cong";
   2.150 -val conj_disj_distribL = thm "conj_disj_distribL";
   2.151 -val conj_disj_distribR = thm "conj_disj_distribR";
   2.152 -val conj_left_commute = thm "conj_left_commute";
   2.153 -val disj_comms = thms "disj_comms";
   2.154 -val disj_commute = thm "disj_commute";
   2.155 -val disj_cong = thm "disj_cong";
   2.156 -val disj_conj_distribL = thm "disj_conj_distribL";
   2.157 -val disj_conj_distribR = thm "disj_conj_distribR";
   2.158 -val disj_left_commute = thm "disj_left_commute";
   2.159 -val eq_assoc = thm "eq_assoc";
   2.160 -val eq_left_commute = thm "eq_left_commute";
   2.161 -val ex_disj_distrib = thm "ex_disj_distrib";
   2.162 -val if_P = thm "if_P";
   2.163 -val if_bool_eq_disj = thm "if_bool_eq_disj";
   2.164 -val if_def2 = thm "if_bool_eq_conj";
   2.165 -val if_not_P = thm "if_not_P";
   2.166 -val if_splits = thms "if_splits";
   2.167 -val imp_all = thm "imp_all";
   2.168 -val imp_conjL = thm "imp_conjL";
   2.169 -val imp_conjR = thm "imp_conjR";
   2.170 -val imp_disj_not1 = thm "imp_disj_not1";
   2.171 -val imp_disj_not2 = thm "imp_disj_not2";
   2.172 -val imp_ex = thm "imp_ex";
   2.173 -val meta_eq_to_obj_eq = thm "def_imp_eq";
   2.174 -val ex_simps = thms "ex_simps";
   2.175 -val all_simps = thms "all_simps";
   2.176 -val simp_thms = thms "simp_thms";
   2.177 -val Eq_FalseI = thm "Eq_FalseI";
   2.178 -val Eq_TrueI = thm "Eq_TrueI";
   2.179 -val cases_simp = thm "cases_simp";
   2.180 -val conj_assoc = thm "conj_assoc";
   2.181 +val def_imp_eq = thm "def_imp_eq";
   2.182  val de_Morgan_conj = thm "de_Morgan_conj";
   2.183  val de_Morgan_disj = thm "de_Morgan_disj";
   2.184  val disj_assoc = thm "disj_assoc";
   2.185 -val disj_not1 = thm "disj_not1";
   2.186 -val disj_not2 = thm "disj_not2";
   2.187 -val if_False = thm "if_False";
   2.188 -val if_True = thm "if_True";
   2.189 -val if_bool_eq_conj = thm "if_bool_eq_conj";
   2.190 +val disjCI = thm "disjCI";
   2.191 +val disj_comms = thms "disj_comms";
   2.192 +val disj_cong = thm "disj_cong";
   2.193 +val disjE = thm "disjE";
   2.194 +val disjI1 = thm "disjI1"
   2.195 +val disjI2 = thm "disjI2"
   2.196 +val eq_ac = thms "eq_ac";
   2.197 +val eq_cong2 = thm "eq_cong2"
   2.198 +val Eq_FalseI = thm "Eq_FalseI";
   2.199 +val eq_reflection = thm "eq_reflection";
   2.200 +val Eq_TrueI = thm "Eq_TrueI";
   2.201 +val Ex1_def = thm "Ex1_def"
   2.202 +val ex1E = thm "ex1E"
   2.203 +val ex1_implies_ex = thm "ex1_implies_ex"
   2.204 +val ex1I = thm "ex1I"
   2.205 +val excluded_middle = thm "excluded_middle"
   2.206 +val ex_disj_distrib = thm "ex_disj_distrib";
   2.207 +val exE = thm "exE";
   2.208 +val exI = thm "exI";
   2.209 +val ex_simps = thms "ex_simps";
   2.210 +val ext = thm "ext"
   2.211 +val FalseE = thm "FalseE"
   2.212 +val FalseE = thm "FalseE";
   2.213 +val fun_cong = thm "fun_cong"
   2.214  val if_cancel = thm "if_cancel";
   2.215  val if_eq_cancel = thm "if_eq_cancel";
   2.216 +val if_False = thm "if_False";
   2.217  val iff_conv_conj_imp = thm "iff_conv_conj_imp";
   2.218 +val iffD1 = thm "iffD1";
   2.219 +val iffD2 = thm "iffD2";
   2.220 +val iffI = thm "iffI";
   2.221 +val iff = thm "iff"
   2.222 +val if_splits = thms "if_splits";
   2.223 +val if_True = thm "if_True";
   2.224 +val if_weak_cong = thm "if_weak_cong"
   2.225 +val imp_all = thm "imp_all";
   2.226  val imp_cong = thm "imp_cong";
   2.227 +val imp_conjL = thm "imp_conjL";
   2.228 +val imp_conjR = thm "imp_conjR";
   2.229  val imp_conv_disj = thm "imp_conv_disj";
   2.230 -val imp_disj1 = thm "imp_disj1";
   2.231 -val imp_disj2 = thm "imp_disj2";
   2.232 -val imp_disjL = thm "imp_disjL";
   2.233 -val simp_impliesI = thm "simp_impliesI";
   2.234 -val simp_implies_cong = thm "simp_implies_cong";
   2.235 +val impE = thm "impE"
   2.236 +val impI = thm "impI";
   2.237 +val Let_def = thm "Let_def"
   2.238 +val meta_eq_to_obj_eq = thm "def_imp_eq";
   2.239 +val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
   2.240 +val mp = thm "mp";
   2.241 +val not_all = thm "not_all";
   2.242 +val notE = thm "notE";
   2.243 +val not_ex = thm "not_ex";
   2.244 +val not_iff = thm "not_iff";
   2.245 +val notI = thm "notI";
   2.246 +val not_not = thm "not_not";
   2.247 +val not_sym = thm "not_sym"
   2.248 +val refl = thm "refl";
   2.249 +val rev_mp = thm "rev_mp"
   2.250  val simp_implies_def = thm "simp_implies_def";
   2.251 +val simp_thms = thms "simp_thms";
   2.252 +val spec = thm "spec";
   2.253 +val split_if = thm "split_if";
   2.254 +val ssubst = thm "ssubst"
   2.255 +val subst = thm "subst";
   2.256 +val sym = thm "sym";
   2.257 +val the1_equality = thm "the1_equality"
   2.258 +val theI = thm "theI"
   2.259 +val theI' = thm "theI'"
   2.260 +val trans = thm "trans";
   2.261  val True_implies_equals = thm "True_implies_equals";
   2.262 +val TrueI = thm "TrueI";
   2.263  
   2.264  structure HOL =
   2.265  struct
     3.1 --- a/src/HOL/Lattices.thy	Fri Dec 01 16:08:45 2006 +0100
     3.2 +++ b/src/HOL/Lattices.thy	Fri Dec 01 17:22:28 2006 +0100
     3.3 @@ -3,7 +3,7 @@
     3.4      Author:     Tobias Nipkow
     3.5  *)
     3.6  
     3.7 -header {* Lattices via Locales *}
     3.8 +header {* Abstract lattices *}
     3.9  
    3.10  theory Lattices
    3.11  imports Orderings
    3.12 @@ -187,29 +187,4 @@
    3.13  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
    3.14                 mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
    3.15  
    3.16 -text {* ML legacy bindings *}
    3.17 -
    3.18 -ML {*
    3.19 -val Least_def = thm "Least_def";
    3.20 -val Least_equality = thm "Least_equality";
    3.21 -val min_def = thm "min_def";
    3.22 -val min_of_mono = thm "min_of_mono";
    3.23 -val max_def = thm "max_def";
    3.24 -val max_of_mono = thm "max_of_mono";
    3.25 -val min_leastL = thm "min_leastL";
    3.26 -val max_leastL = thm "max_leastL";
    3.27 -val min_leastR = thm "min_leastR";
    3.28 -val max_leastR = thm "max_leastR";
    3.29 -val le_max_iff_disj = thm "le_max_iff_disj";
    3.30 -val le_maxI1 = thm "le_maxI1";
    3.31 -val le_maxI2 = thm "le_maxI2";
    3.32 -val less_max_iff_disj = thm "less_max_iff_disj";
    3.33 -val max_less_iff_conj = thm "max_less_iff_conj";
    3.34 -val min_less_iff_conj = thm "min_less_iff_conj";
    3.35 -val min_le_iff_disj = thm "min_le_iff_disj";
    3.36 -val min_less_iff_disj = thm "min_less_iff_disj";
    3.37 -val split_min = thm "split_min";
    3.38 -val split_max = thm "split_max";
    3.39 -*}
    3.40 -
    3.41  end
     4.1 --- a/src/HOL/Orderings.ML	Fri Dec 01 16:08:45 2006 +0100
     4.2 +++ b/src/HOL/Orderings.ML	Fri Dec 01 17:22:28 2006 +0100
     4.3 @@ -1,21 +1,6 @@
     4.4  (* legacy ML bindings *)
     4.5  
     4.6 -val order_eq_refl = thm "order_eq_refl";
     4.7  val order_less_irrefl = thm "order_less_irrefl";
     4.8 -val order_le_less = thm "order_le_less";
     4.9 -val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
    4.10 -val order_less_imp_le = thm "order_less_imp_le";
    4.11 -val order_less_not_sym = thm "order_less_not_sym";
    4.12 -val order_less_asym = thm "order_less_asym";
    4.13 -val order_less_trans = thm "order_less_trans";
    4.14 -val order_le_less_trans = thm "order_le_less_trans";
    4.15 -val order_less_le_trans = thm "order_less_le_trans";
    4.16 -val order_less_imp_not_less = thm "order_less_imp_not_less";
    4.17 -val order_less_imp_triv = thm "order_less_imp_triv";
    4.18 -val order_less_imp_not_eq = thm "order_less_imp_not_eq";
    4.19 -val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
    4.20 -val linorder_less_linear = thm "linorder_less_linear";
    4.21 -val linorder_cases = thm "linorder_cases";
    4.22  val linorder_not_less = thm "linorder_not_less";
    4.23  val linorder_not_le = thm "linorder_not_le";
    4.24  val linorder_neq_iff = thm "linorder_neq_iff";
    4.25 @@ -23,8 +8,10 @@
    4.26  val order_refl = thm "order_refl";
    4.27  val order_trans = thm "order_trans";
    4.28  val order_antisym = thm "order_antisym";
    4.29 -val order_less_le = thm "order_less_le";
    4.30 -val linorder_linear = thm "linorder_linear";
    4.31  val mono_def = thm "mono_def";
    4.32  val monoI = thm "monoI";
    4.33  val monoD = thm "monoD";
    4.34 +val max_less_iff_conj = thm "max_less_iff_conj";
    4.35 +val min_less_iff_conj = thm "min_less_iff_conj";
    4.36 +val split_min = thm "split_min";
    4.37 +val split_max = thm "split_max";
     5.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Dec 01 16:08:45 2006 +0100
     5.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Dec 01 17:22:28 2006 +0100
     5.3 @@ -104,6 +104,7 @@
     5.4  text{*This ML code does the inductions directly.*}
     5.5  ML{*
     5.6  val ns_constrainsI = thm "ns_constrainsI";
     5.7 +val impCE = thm "impCE";
     5.8  
     5.9  fun ns_constrains_tac(cs,ss) i =
    5.10     SELECT_GOAL
     6.1 --- a/src/HOLCF/domain/theorems.ML	Fri Dec 01 16:08:45 2006 +0100
     6.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Dec 01 17:22:28 2006 +0100
     6.3 @@ -213,6 +213,7 @@
     6.4        val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
     6.5      in Library.foldr mk_ex (vns, conj) end;
     6.6  
     6.7 +  val conj_assoc = thm "conj_assoc";
     6.8    val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
     6.9    val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
    6.10    val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
    6.11 @@ -350,6 +351,7 @@
    6.12  end;
    6.13  
    6.14  local
    6.15 +  val rev_contrapos = thm "rev_contrapos";
    6.16    fun con_strict (con, args) = 
    6.17      let
    6.18        fun one_strict vn =
    6.19 @@ -457,6 +459,7 @@
    6.20  end;
    6.21  
    6.22  val sel_rews = sel_stricts @ sel_defins @ sel_apps;
    6.23 +val rev_contrapos = thm "rev_contrapos";
    6.24  
    6.25  val distincts_le =
    6.26    let