src/HOL/List.ML
changeset 21669 c68717c16013
parent 21668 2d811ae6752a
child 21670 704510b508ef
     1.1 --- a/src/HOL/List.ML	Tue Dec 05 22:14:53 2006 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,231 +0,0 @@
     1.4 -
     1.5 -(** legacy ML bindings **)
     1.6 -
     1.7 -val Cons_eq_appendI = thm "Cons_eq_appendI";
     1.8 -val Cons_in_lex = thm "Cons_in_lex";
     1.9 -val Nil2_notin_lex = thm "Nil2_notin_lex";
    1.10 -val Nil_eq_concat_conv = thm "Nil_eq_concat_conv";
    1.11 -val Nil_is_append_conv = thm "Nil_is_append_conv";
    1.12 -val Nil_is_map_conv = thm "Nil_is_map_conv";
    1.13 -val Nil_is_rev_conv = thm "Nil_is_rev_conv";
    1.14 -val Nil_notin_lex = thm "Nil_notin_lex";
    1.15 -val all_nth_imp_all_set = thm "all_nth_imp_all_set";
    1.16 -val all_set_conv_all_nth = thm "all_set_conv_all_nth";
    1.17 -val append1_eq_conv = thm "append1_eq_conv";
    1.18 -val append_Cons = thm "append_Cons";
    1.19 -val append_Nil = thm "append_Nil";
    1.20 -val append_Nil2 = thm "append_Nil2";
    1.21 -val append_assoc = thm "append_assoc";
    1.22 -val append_butlast_last_id = thm "append_butlast_last_id";
    1.23 -val append_eq_appendI = thm "append_eq_appendI";
    1.24 -val append_eq_append_conv = thm "append_eq_append_conv";
    1.25 -val append_eq_conv_conj = thm "append_eq_conv_conj";
    1.26 -val append_in_lists_conv = thm "append_in_lists_conv";
    1.27 -val append_is_Nil_conv = thm "append_is_Nil_conv";
    1.28 -val append_same_eq = thm "append_same_eq";
    1.29 -val append_self_conv = thm "append_self_conv";
    1.30 -val append_self_conv2 = thm "append_self_conv2";
    1.31 -val append_take_drop_id = thm "append_take_drop_id";
    1.32 -val butlast_append = thm "butlast_append";
    1.33 -val butlast_snoc = thm "butlast_snoc";
    1.34 -val concat_append = thm "concat_append";
    1.35 -val concat_eq_Nil_conv = thm "concat_eq_Nil_conv";
    1.36 -val distinct_append = thm "distinct_append";
    1.37 -val distinct_filter = thm "distinct_filter";
    1.38 -val distinct_remdups = thm "distinct_remdups";
    1.39 -val dropWhile_append1 = thm "dropWhile_append1";
    1.40 -val dropWhile_append2 = thm "dropWhile_append2";
    1.41 -val drop_0 = thm "drop_0";
    1.42 -val drop_Cons = thm "drop_Cons";
    1.43 -val drop_Cons' = thm "drop_Cons'";
    1.44 -val drop_Nil = thm "drop_Nil";
    1.45 -val drop_Suc_Cons = thm "drop_Suc_Cons";
    1.46 -val drop_all = thm "drop_all";
    1.47 -val drop_append = thm "drop_append";
    1.48 -val drop_drop = thm "drop_drop";
    1.49 -val drop_map = thm "drop_map";
    1.50 -val elem_le_sum = thm "elem_le_sum";
    1.51 -val eq_Nil_appendI = thm "eq_Nil_appendI";
    1.52 -val filter_False = thm "filter_False";
    1.53 -val filter_True = thm "filter_True";
    1.54 -val filter_append = thm "filter_append";
    1.55 -val filter_concat = thm "filter_concat"; 
    1.56 -val filter_filter = thm "filter_filter";
    1.57 -val filter_is_subset = thm "filter_is_subset";
    1.58 -val finite_set = thm "finite_set";
    1.59 -val foldl_Cons = thm "foldl_Cons";
    1.60 -val foldl_Nil = thm "foldl_Nil";
    1.61 -val foldl_append = thm "foldl_append";
    1.62 -val hd_Cons_tl = thm "hd_Cons_tl";
    1.63 -val hd_append = thm "hd_append";
    1.64 -val hd_append2 = thm "hd_append2";
    1.65 -val hd_replicate = thm "hd_replicate";
    1.66 -val in_listsD = thm "in_listsD";
    1.67 -val in_listsI = thm "in_listsI";
    1.68 -val in_lists_conv_set = thm "in_lists_conv_set";
    1.69 -val in_set_butlastD = thm "in_set_butlastD";
    1.70 -val in_set_butlast_appendI = thm "in_set_butlast_appendI";
    1.71 -val in_set_conv_decomp = thm "in_set_conv_decomp";
    1.72 -val in_set_replicateD = thm "in_set_replicateD";
    1.73 -val inj_map = thm "inj_map";
    1.74 -val inj_mapD = thm "inj_mapD";
    1.75 -val inj_mapI = thm "inj_mapI";
    1.76 -val last_replicate = thm "last_replicate";
    1.77 -val last_snoc = thm "last_snoc";
    1.78 -val length_0_conv = thm "length_0_conv";
    1.79 -val length_Suc_conv = thm "length_Suc_conv";
    1.80 -val length_append = thm "length_append";
    1.81 -val length_butlast = thm "length_butlast";
    1.82 -val length_drop = thm "length_drop";
    1.83 -val length_filter_le = thm "length_filter_le";
    1.84 -val length_greater_0_conv = thm "length_greater_0_conv";
    1.85 -val length_induct = thm "length_induct";
    1.86 -val length_list_update = thm "length_list_update";
    1.87 -val length_map = thm "length_map";
    1.88 -val length_replicate = thm "length_replicate";
    1.89 -val length_rev = thm "length_rev";
    1.90 -val length_take = thm "length_take";
    1.91 -val length_tl = thm "length_tl";
    1.92 -val length_upt = thm "length_upt";
    1.93 -val length_zip = thm "length_zip";
    1.94 -val lex_conv = thm "lex_conv";
    1.95 -val lex_def = thm "lex_def";
    1.96 -val lenlex_conv = thm "lenlex_conv";
    1.97 -val lenlex_def = thm "lenlex_def";
    1.98 -val lexn_conv = thm "lexn_conv";
    1.99 -val lexn_length = thm "lexn_length";
   1.100 -val list_all2_Cons = thm "list_all2_Cons";
   1.101 -val list_all2_Cons1 = thm "list_all2_Cons1";
   1.102 -val list_all2_Cons2 = thm "list_all2_Cons2";
   1.103 -val list_all2_Nil = thm "list_all2_Nil";
   1.104 -val list_all2_Nil2 = thm "list_all2_Nil2";
   1.105 -val list_all2_append1 = thm "list_all2_append1";
   1.106 -val list_all2_append2 = thm "list_all2_append2";
   1.107 -val list_all2_conv_all_nth = thm "list_all2_conv_all_nth";
   1.108 -val list_all2_def = thm "list_all2_def";
   1.109 -val list_all2_lengthD = thm "list_all2_lengthD";
   1.110 -val list_all2_rev = thm "list_all2_rev";
   1.111 -val list_all2_trans = thm "list_all2_trans";
   1.112 -val list_all_append = thm "list_all_append";
   1.113 -val list_all_iff = thm "list_all_iff";
   1.114 -val list_ball_nth = thm "list_ball_nth";
   1.115 -val list_update_overwrite = thm "list_update_overwrite";
   1.116 -val list_update_same_conv = thm "list_update_same_conv";
   1.117 -val listsE = thm "listsE";
   1.118 -val lists_IntI = thm "lists_IntI";
   1.119 -val lists_Int_eq = thm "lists_Int_eq";
   1.120 -val lists_mono = thm "lists_mono";
   1.121 -val map_Suc_upt = thm "map_Suc_upt";
   1.122 -val map_append = thm "map_append";
   1.123 -val map_compose = thm "map_compose";
   1.124 -val map_concat = thm "map_concat";
   1.125 -val map_cong = thm "map_cong";
   1.126 -val map_eq_Cons_conv = thm "map_eq_Cons_conv";
   1.127 -val map_ext = thm "map_ext";
   1.128 -val map_ident = thm "map_ident";
   1.129 -val map_injective = thm "map_injective";
   1.130 -val map_is_Nil_conv = thm "map_is_Nil_conv";
   1.131 -val map_replicate = thm "map_replicate";
   1.132 -val neq_Nil_conv = thm "neq_Nil_conv";
   1.133 -val not_Cons_self = thm "not_Cons_self";
   1.134 -val not_Cons_self2 = thm "not_Cons_self2";
   1.135 -val nth_Cons = thm "nth_Cons";
   1.136 -val nth_Cons' = thm "nth_Cons'";
   1.137 -val nth_Cons_0 = thm "nth_Cons_0";
   1.138 -val nth_Cons_Suc = thm "nth_Cons_Suc";
   1.139 -val nth_append = thm "nth_append";
   1.140 -val nth_drop = thm "nth_drop";
   1.141 -val nth_equalityI = thm "nth_equalityI";
   1.142 -val nth_list_update = thm "nth_list_update";
   1.143 -val nth_list_update_eq = thm "nth_list_update_eq";
   1.144 -val nth_list_update_neq = thm "nth_list_update_neq";
   1.145 -val nth_map_upt = thm "nth_map_upt";
   1.146 -val nth_mem = thm "nth_mem";
   1.147 -val nth_replicate = thm "nth_replicate";
   1.148 -val nth_take = thm "nth_take";
   1.149 -val nth_take_lemma = thm "nth_take_lemma";
   1.150 -val nth_upt = thm "nth_upt";
   1.151 -val nth_zip = thm "nth_zip";
   1.152 -val replicate_0 = thm "replicate_0";
   1.153 -val replicate_Suc = thm "replicate_Suc";
   1.154 -val replicate_add = thm "replicate_add";
   1.155 -val replicate_app_Cons_same = thm "replicate_app_Cons_same";
   1.156 -val rev_append = thm "rev_append";
   1.157 -val rev_concat = thm "rev_concat";
   1.158 -val rev_drop = thm "rev_drop";
   1.159 -val rev_exhaust = thm "rev_exhaust";
   1.160 -val rev_induct = thm "rev_induct";
   1.161 -val rev_is_Nil_conv = thm "rev_is_Nil_conv";
   1.162 -val rev_is_rev_conv = thm "rev_is_rev_conv";
   1.163 -val rev_map = thm "rev_map";
   1.164 -val rev_replicate = thm "rev_replicate";
   1.165 -val rev_rev_ident = thm "rev_rev_ident";
   1.166 -val rev_take = thm "rev_take";
   1.167 -val same_append_eq = thm "same_append_eq";
   1.168 -val self_append_conv = thm "self_append_conv";
   1.169 -val self_append_conv2 = thm "self_append_conv2";
   1.170 -val set_append = thm "set_append";
   1.171 -val set_concat = thm "set_concat";
   1.172 -val set_conv_nth = thm "set_conv_nth";
   1.173 -val set_empty = thm "set_empty";
   1.174 -val set_filter = thm "set_filter";
   1.175 -val set_map = thm "set_map";
   1.176 -val mem_ii = thm "mem_iff";
   1.177 -val set_remdups = thm "set_remdups";
   1.178 -val set_replicate = thm "set_replicate";
   1.179 -val set_replicate_conv_if = thm "set_replicate_conv_if";
   1.180 -val set_rev = thm "set_rev";
   1.181 -val set_subset_Cons = thm "set_subset_Cons";
   1.182 -val set_take_whileD = thm "set_take_whileD";
   1.183 -val set_update_subsetI = thm "set_update_subsetI";
   1.184 -val set_update_subset_insert = thm "set_update_subset_insert";
   1.185 -val set_upt = thm "set_upt";
   1.186 -val set_zip = thm "set_zip";
   1.187 -val start_le_sum = thm "start_le_sum";
   1.188 -val sublist_Cons = thm "sublist_Cons";
   1.189 -val sublist_append = thm "sublist_append";
   1.190 -val sublist_def = thm "sublist_def";
   1.191 -val sublist_empty = thm "sublist_empty";
   1.192 -val sublist_nil = thm "sublist_nil";
   1.193 -val sublist_shift_lemma = thm "sublist_shift_lemma";
   1.194 -val sublist_singleton = thm "sublist_singleton";
   1.195 -val sublist_upt_eq_take = thm "sublist_upt_eq_take";
   1.196 -val sum_eq_0_conv = thm "sum_eq_0_conv";
   1.197 -val takeWhile_append1 = thm "takeWhile_append1";
   1.198 -val takeWhile_append2 = thm "takeWhile_append2";
   1.199 -val takeWhile_dropWhile_id = thm "takeWhile_dropWhile_id";
   1.200 -val takeWhile_tail = thm "takeWhile_tail";
   1.201 -val take_0 = thm "take_0";
   1.202 -val take_Cons = thm "take_Cons";
   1.203 -val take_Cons' = thm "take_Cons'";
   1.204 -val take_Nil = thm "take_Nil";
   1.205 -val take_Suc_Cons = thm "take_Suc_Cons";
   1.206 -val take_all = thm "take_all";
   1.207 -val take_append = thm "take_append";
   1.208 -val take_drop = thm "take_drop";
   1.209 -val take_equalityI = thm "take_equalityI";
   1.210 -val take_map = thm "take_map"; 
   1.211 -val take_take = thm "take_take";
   1.212 -val take_upt = thm "take_upt";
   1.213 -val tl_append = thm "tl_append";
   1.214 -val tl_append2 = thm "tl_append2";
   1.215 -val tl_replicate = thm "tl_replicate";
   1.216 -val update_zip = thm "update_zip";
   1.217 -val upt_0 = thm "upt_0";
   1.218 -val upt_Suc = thm "upt_Suc";
   1.219 -val upt_Suc_append = thm "upt_Suc_append";
   1.220 -val upt_add_eq_append = thm "upt_add_eq_append";
   1.221 -val upt_conv_Cons = thm "upt_conv_Cons";
   1.222 -val upt_conv_Nil = thm "upt_conv_Nil";
   1.223 -val upt_rec = thm "upt_rec";
   1.224 -val wf_lex = thm "wf_lex";
   1.225 -val wf_lenlex = thm "wf_lenlex";
   1.226 -val wf_lexn = thm "wf_lexn";
   1.227 -val zip_Cons_Cons = thm "zip_Cons_Cons";
   1.228 -val zip_Nil = thm "zip_Nil";
   1.229 -val zip_append = thm "zip_append";
   1.230 -val zip_append1 = thm "zip_append1";
   1.231 -val zip_append2 = thm "zip_append2";
   1.232 -val zip_replicate = thm "zip_replicate";
   1.233 -val zip_rev = thm "zip_rev";
   1.234 -val zip_update = thm "zip_update";