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