src/HOL/List.ML
author nipkow
Wed May 14 10:22:09 2003 +0200 (2003-05-14)
changeset 14025 d9b155757dc8
parent 13122 c63612ffb186
child 14401 477380c74c1d
permissions -rw-r--r--
*** empty log message ***
     1 
     2 (** legacy ML bindings **)
     3 
     4 structure List =
     5 struct
     6 
     7 val thy = the_context ();
     8 
     9 structure list =
    10 struct
    11   val distinct = thms "list.distinct";
    12   val inject = thms "list.inject";
    13   val exhaust = thm "list.exhaust";
    14   val cases = thms "list.cases";
    15   val split = thm "list.split";
    16   val split_asm = thm "list.split_asm";
    17   val induct = thm "list.induct";
    18   val recs = thms "list.recs";
    19   val simps = thms "list.simps";
    20   val size = thms "list.size";
    21 end;
    22 
    23 structure lists =
    24 struct
    25   val intrs = thms "lists.intros";
    26   val elims = thms "lists.cases";
    27   val elim = thm "lists.cases";
    28   val induct = thm "lists.induct";
    29   val mk_cases = InductivePackage.the_mk_cases (the_context ()) "List.lists";
    30   val [Nil, Cons] = intrs;
    31 end;
    32 
    33 end;
    34 
    35 open List;
    36 
    37 
    38 val Cons_eq_appendI = thm "Cons_eq_appendI";
    39 val Cons_in_lex = thm "Cons_in_lex";
    40 val Nil2_notin_lex = thm "Nil2_notin_lex";
    41 val Nil_eq_concat_conv = thm "Nil_eq_concat_conv";
    42 val Nil_is_append_conv = thm "Nil_is_append_conv";
    43 val Nil_is_map_conv = thm "Nil_is_map_conv";
    44 val Nil_is_rev_conv = thm "Nil_is_rev_conv";
    45 val Nil_notin_lex = thm "Nil_notin_lex";
    46 val all_nth_imp_all_set = thm "all_nth_imp_all_set";
    47 val all_set_conv_all_nth = thm "all_set_conv_all_nth";
    48 val append1_eq_conv = thm "append1_eq_conv";
    49 val append_Cons = thm "append_Cons";
    50 val append_Nil = thm "append_Nil";
    51 val append_Nil2 = thm "append_Nil2";
    52 val append_assoc = thm "append_assoc";
    53 val append_butlast_last_id = thm "append_butlast_last_id";
    54 val append_eq_appendI = thm "append_eq_appendI";
    55 val append_eq_append_conv = thm "append_eq_append_conv";
    56 val append_eq_conv_conj = thm "append_eq_conv_conj";
    57 val append_in_lists_conv = thm "append_in_lists_conv";
    58 val append_is_Nil_conv = thm "append_is_Nil_conv";
    59 val append_same_eq = thm "append_same_eq";
    60 val append_self_conv = thm "append_self_conv";
    61 val append_self_conv2 = thm "append_self_conv2";
    62 val append_take_drop_id = thm "append_take_drop_id";
    63 val butlast_append = thm "butlast_append";
    64 val butlast_snoc = thm "butlast_snoc";
    65 val concat_append = thm "concat_append";
    66 val concat_eq_Nil_conv = thm "concat_eq_Nil_conv";
    67 val distinct_append = thm "distinct_append";
    68 val distinct_filter = thm "distinct_filter";
    69 val distinct_remdups = thm "distinct_remdups";
    70 val dropWhile_append1 = thm "dropWhile_append1";
    71 val dropWhile_append2 = thm "dropWhile_append2";
    72 val drop_0 = thm "drop_0";
    73 val drop_Cons = thm "drop_Cons";
    74 val drop_Cons' = thm "drop_Cons'";
    75 val drop_Nil = thm "drop_Nil";
    76 val drop_Suc_Cons = thm "drop_Suc_Cons";
    77 val drop_all = thm "drop_all";
    78 val drop_append = thm "drop_append";
    79 val drop_drop = thm "drop_drop";
    80 val drop_map = thm "drop_map";
    81 val elem_le_sum = thm "elem_le_sum";
    82 val eq_Nil_appendI = thm "eq_Nil_appendI";
    83 val filter_False = thm "filter_False";
    84 val filter_True = thm "filter_True";
    85 val filter_append = thm "filter_append";
    86 val filter_concat = thm "filter_concat"; 
    87 val filter_filter = thm "filter_filter";
    88 val filter_is_subset = thm "filter_is_subset";
    89 val finite_set = thm "finite_set";
    90 val foldl_Cons = thm "foldl_Cons";
    91 val foldl_Nil = thm "foldl_Nil";
    92 val foldl_append = thm "foldl_append";
    93 val hd_Cons_tl = thm "hd_Cons_tl";
    94 val hd_append = thm "hd_append";
    95 val hd_append2 = thm "hd_append2";
    96 val hd_replicate = thm "hd_replicate";
    97 val in_listsD = thm "in_listsD";
    98 val in_listsI = thm "in_listsI";
    99 val in_lists_conv_set = thm "in_lists_conv_set";
   100 val in_set_butlastD = thm "in_set_butlastD";
   101 val in_set_butlast_appendI = thm "in_set_butlast_appendI";
   102 val in_set_conv_decomp = thm "in_set_conv_decomp";
   103 val in_set_replicateD = thm "in_set_replicateD";
   104 val inj_map = thm "inj_map";
   105 val inj_mapD = thm "inj_mapD";
   106 val inj_mapI = thm "inj_mapI";
   107 val last_replicate = thm "last_replicate";
   108 val last_snoc = thm "last_snoc";
   109 val length_0_conv = thm "length_0_conv";
   110 val length_Suc_conv = thm "length_Suc_conv";
   111 val length_append = thm "length_append";
   112 val length_butlast = thm "length_butlast";
   113 val length_drop = thm "length_drop";
   114 val length_filter = thm "length_filter";
   115 val length_greater_0_conv = thm "length_greater_0_conv";
   116 val length_induct = thm "length_induct";
   117 val length_list_update = thm "length_list_update";
   118 val length_map = thm "length_map";
   119 val length_replicate = thm "length_replicate";
   120 val length_rev = thm "length_rev";
   121 val length_take = thm "length_take";
   122 val length_tl = thm "length_tl";
   123 val length_upt = thm "length_upt";
   124 val length_zip = thm "length_zip";
   125 val lex_conv = thm "lex_conv";
   126 val lex_def = thm "lex_def";
   127 val lexico_conv = thm "lexico_conv";
   128 val lexico_def = thm "lexico_def";
   129 val lexn_conv = thm "lexn_conv";
   130 val lexn_length = thm "lexn_length";
   131 val list_all2_Cons = thm "list_all2_Cons";
   132 val list_all2_Cons1 = thm "list_all2_Cons1";
   133 val list_all2_Cons2 = thm "list_all2_Cons2";
   134 val list_all2_Nil = thm "list_all2_Nil";
   135 val list_all2_Nil2 = thm "list_all2_Nil2";
   136 val list_all2_append1 = thm "list_all2_append1";
   137 val list_all2_append2 = thm "list_all2_append2";
   138 val list_all2_conv_all_nth = thm "list_all2_conv_all_nth";
   139 val list_all2_def = thm "list_all2_def";
   140 val list_all2_lengthD = thm "list_all2_lengthD";
   141 val list_all2_rev = thm "list_all2_rev";
   142 val list_all2_trans = thm "list_all2_trans";
   143 val list_all_Cons = thm "list_all_Cons";
   144 val list_all_Nil = thm "list_all_Nil";
   145 val list_all_append = thm "list_all_append";
   146 val list_all_conv = thm "list_all_conv";
   147 val list_ball_nth = thm "list_ball_nth";
   148 val list_update_overwrite = thm "list_update_overwrite";
   149 val list_update_same_conv = thm "list_update_same_conv";
   150 val listsE = thm "listsE";
   151 val lists_IntI = thm "lists_IntI";
   152 val lists_Int_eq = thm "lists_Int_eq";
   153 val lists_mono = thm "lists_mono";
   154 val map_Suc_upt = thm "map_Suc_upt";
   155 val map_append = thm "map_append";
   156 val map_compose = thm "map_compose";
   157 val map_concat = thm "map_concat";
   158 val map_cong = thm "map_cong";
   159 val map_eq_Cons_conv = thm "map_eq_Cons_conv";
   160 val map_ext = thm "map_ext";
   161 val map_ident = thm "map_ident";
   162 val map_injective = thm "map_injective";
   163 val map_is_Nil_conv = thm "map_is_Nil_conv";
   164 val map_replicate = thm "map_replicate";
   165 val neq_Nil_conv = thm "neq_Nil_conv";
   166 val not_Cons_self = thm "not_Cons_self";
   167 val not_Cons_self2 = thm "not_Cons_self2";
   168 val nth_Cons = thm "nth_Cons";
   169 val nth_Cons' = thm "nth_Cons'";
   170 val nth_Cons_0 = thm "nth_Cons_0";
   171 val nth_Cons_Suc = thm "nth_Cons_Suc";
   172 val nth_append = thm "nth_append";
   173 val nth_drop = thm "nth_drop";
   174 val nth_equalityI = thm "nth_equalityI";
   175 val nth_list_update = thm "nth_list_update";
   176 val nth_list_update_eq = thm "nth_list_update_eq";
   177 val nth_list_update_neq = thm "nth_list_update_neq";
   178 val nth_map = thm "nth_map";
   179 val nth_map_upt = thm "nth_map_upt";
   180 val nth_mem = thm "nth_mem";
   181 val nth_replicate = thm "nth_replicate";
   182 val nth_take = thm "nth_take";
   183 val nth_take_lemma = thm "nth_take_lemma";
   184 val nth_upt = thm "nth_upt";
   185 val nth_zip = thm "nth_zip";
   186 val replicate_0 = thm "replicate_0";
   187 val replicate_Suc = thm "replicate_Suc";
   188 val replicate_add = thm "replicate_add";
   189 val replicate_app_Cons_same = thm "replicate_app_Cons_same";
   190 val rev_append = thm "rev_append";
   191 val rev_concat = thm "rev_concat";
   192 val rev_drop = thm "rev_drop";
   193 val rev_exhaust = thm "rev_exhaust";
   194 val rev_induct = thm "rev_induct";
   195 val rev_is_Nil_conv = thm "rev_is_Nil_conv";
   196 val rev_is_rev_conv = thm "rev_is_rev_conv";
   197 val rev_map = thm "rev_map";
   198 val rev_replicate = thm "rev_replicate";
   199 val rev_rev_ident = thm "rev_rev_ident";
   200 val rev_take = thm "rev_take";
   201 val same_append_eq = thm "same_append_eq";
   202 val self_append_conv = thm "self_append_conv";
   203 val self_append_conv2 = thm "self_append_conv2";
   204 val set_append = thm "set_append";
   205 val set_concat = thm "set_concat";
   206 val set_conv_nth = thm "set_conv_nth";
   207 val set_empty = thm "set_empty";
   208 val set_filter = thm "set_filter";
   209 val set_map = thm "set_map";
   210 val set_mem_eq = thm "set_mem_eq";
   211 val set_remdups = thm "set_remdups";
   212 val set_replicate = thm "set_replicate";
   213 val set_replicate_conv_if = thm "set_replicate_conv_if";
   214 val set_rev = thm "set_rev";
   215 val set_subset_Cons = thm "set_subset_Cons";
   216 val set_take_whileD = thm "set_take_whileD";
   217 val set_update_subsetI = thm "set_update_subsetI";
   218 val set_update_subset_insert = thm "set_update_subset_insert";
   219 val set_upt = thm "set_upt";
   220 val set_zip = thm "set_zip";
   221 val start_le_sum = thm "start_le_sum";
   222 val sublist_Cons = thm "sublist_Cons";
   223 val sublist_append = thm "sublist_append";
   224 val sublist_def = thm "sublist_def";
   225 val sublist_empty = thm "sublist_empty";
   226 val sublist_nil = thm "sublist_nil";
   227 val sublist_shift_lemma = thm "sublist_shift_lemma";
   228 val sublist_singleton = thm "sublist_singleton";
   229 val sublist_upt_eq_take = thm "sublist_upt_eq_take";
   230 val sum_eq_0_conv = thm "sum_eq_0_conv";
   231 val takeWhile_append1 = thm "takeWhile_append1";
   232 val takeWhile_append2 = thm "takeWhile_append2";
   233 val takeWhile_dropWhile_id = thm "takeWhile_dropWhile_id";
   234 val takeWhile_tail = thm "takeWhile_tail";
   235 val take_0 = thm "take_0";
   236 val take_Cons = thm "take_Cons";
   237 val take_Cons' = thm "take_Cons'";
   238 val take_Nil = thm "take_Nil";
   239 val take_Suc_Cons = thm "take_Suc_Cons";
   240 val take_all = thm "take_all";
   241 val take_append = thm "take_append";
   242 val take_drop = thm "take_drop";
   243 val take_equalityI = thm "take_equalityI";
   244 val take_map = thm "take_map"; 
   245 val take_take = thm "take_take";
   246 val take_upt = thm "take_upt";
   247 val tl_append = thm "tl_append";
   248 val tl_append2 = thm "tl_append2";
   249 val tl_replicate = thm "tl_replicate";
   250 val update_zip = thm "update_zip";
   251 val upt_0 = thm "upt_0";
   252 val upt_Suc = thm "upt_Suc";
   253 val upt_Suc_append = thm "upt_Suc_append";
   254 val upt_add_eq_append = thm "upt_add_eq_append";
   255 val upt_conv_Cons = thm "upt_conv_Cons";
   256 val upt_conv_Nil = thm "upt_conv_Nil";
   257 val upt_rec = thm "upt_rec";
   258 val wf_lex = thm "wf_lex";
   259 val wf_lexico = thm "wf_lexico";
   260 val wf_lexn = thm "wf_lexn";
   261 val zip_Cons_Cons = thm "zip_Cons_Cons";
   262 val zip_Nil = thm "zip_Nil";
   263 val zip_append = thm "zip_append";
   264 val zip_append1 = thm "zip_append1";
   265 val zip_append2 = thm "zip_append2";
   266 val zip_replicate = thm "zip_replicate";
   267 val zip_rev = thm "zip_rev";
   268 val zip_update = thm "zip_update";