src/HOL/List.ML
author haftmann
Tue, 08 Aug 2006 08:19:44 +0200
changeset 20355 50aaae6ae4db
parent 18362 e8b7e0a22727
permissions -rw-r--r--
cleanup code generation for Numerals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
13114
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
     2
(** legacy ML bindings **)
3860
a29ab43f7174 More lemmas, esp. ~Bex and ~Ball conversions.
nipkow
parents: 3842
diff changeset
     3
13114
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
     4
val Cons_eq_appendI = thm "Cons_eq_appendI";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
     5
val Cons_in_lex = thm "Cons_in_lex";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
     6
val Nil2_notin_lex = thm "Nil2_notin_lex";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
     7
val Nil_eq_concat_conv = thm "Nil_eq_concat_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
     8
val Nil_is_append_conv = thm "Nil_is_append_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
     9
val Nil_is_map_conv = thm "Nil_is_map_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    10
val Nil_is_rev_conv = thm "Nil_is_rev_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    11
val Nil_notin_lex = thm "Nil_notin_lex";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    12
val all_nth_imp_all_set = thm "all_nth_imp_all_set";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    13
val all_set_conv_all_nth = thm "all_set_conv_all_nth";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    14
val append1_eq_conv = thm "append1_eq_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    15
val append_Cons = thm "append_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    16
val append_Nil = thm "append_Nil";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    17
val append_Nil2 = thm "append_Nil2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    18
val append_assoc = thm "append_assoc";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    19
val append_butlast_last_id = thm "append_butlast_last_id";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    20
val append_eq_appendI = thm "append_eq_appendI";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    21
val append_eq_append_conv = thm "append_eq_append_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    22
val append_eq_conv_conj = thm "append_eq_conv_conj";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    23
val append_in_lists_conv = thm "append_in_lists_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    24
val append_is_Nil_conv = thm "append_is_Nil_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    25
val append_same_eq = thm "append_same_eq";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    26
val append_self_conv = thm "append_self_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    27
val append_self_conv2 = thm "append_self_conv2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    28
val append_take_drop_id = thm "append_take_drop_id";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    29
val butlast_append = thm "butlast_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    30
val butlast_snoc = thm "butlast_snoc";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    31
val concat_append = thm "concat_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    32
val concat_eq_Nil_conv = thm "concat_eq_Nil_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    33
val distinct_append = thm "distinct_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    34
val distinct_filter = thm "distinct_filter";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    35
val distinct_remdups = thm "distinct_remdups";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    36
val dropWhile_append1 = thm "dropWhile_append1";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    37
val dropWhile_append2 = thm "dropWhile_append2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    38
val drop_0 = thm "drop_0";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    39
val drop_Cons = thm "drop_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    40
val drop_Cons' = thm "drop_Cons'";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    41
val drop_Nil = thm "drop_Nil";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    42
val drop_Suc_Cons = thm "drop_Suc_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    43
val drop_all = thm "drop_all";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    44
val drop_append = thm "drop_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    45
val drop_drop = thm "drop_drop";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    46
val drop_map = thm "drop_map";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    47
val elem_le_sum = thm "elem_le_sum";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    48
val eq_Nil_appendI = thm "eq_Nil_appendI";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    49
val filter_False = thm "filter_False";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    50
val filter_True = thm "filter_True";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    51
val filter_append = thm "filter_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    52
val filter_concat = thm "filter_concat"; 
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    53
val filter_filter = thm "filter_filter";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    54
val filter_is_subset = thm "filter_is_subset";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    55
val finite_set = thm "finite_set";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    56
val foldl_Cons = thm "foldl_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    57
val foldl_Nil = thm "foldl_Nil";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    58
val foldl_append = thm "foldl_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    59
val hd_Cons_tl = thm "hd_Cons_tl";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    60
val hd_append = thm "hd_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    61
val hd_append2 = thm "hd_append2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    62
val hd_replicate = thm "hd_replicate";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    63
val in_listsD = thm "in_listsD";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    64
val in_listsI = thm "in_listsI";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    65
val in_lists_conv_set = thm "in_lists_conv_set";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    66
val in_set_butlastD = thm "in_set_butlastD";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    67
val in_set_butlast_appendI = thm "in_set_butlast_appendI";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    68
val in_set_conv_decomp = thm "in_set_conv_decomp";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    69
val in_set_replicateD = thm "in_set_replicateD";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    70
val inj_map = thm "inj_map";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    71
val inj_mapD = thm "inj_mapD";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    72
val inj_mapI = thm "inj_mapI";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    73
val last_replicate = thm "last_replicate";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    74
val last_snoc = thm "last_snoc";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    75
val length_0_conv = thm "length_0_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    76
val length_Suc_conv = thm "length_Suc_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    77
val length_append = thm "length_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    78
val length_butlast = thm "length_butlast";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    79
val length_drop = thm "length_drop";
15246
0984a2c2868b added and renamed
nipkow
parents: 14401
diff changeset
    80
val length_filter_le = thm "length_filter_le";
13114
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    81
val length_greater_0_conv = thm "length_greater_0_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    82
val length_induct = thm "length_induct";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    83
val length_list_update = thm "length_list_update";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    84
val length_map = thm "length_map";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    85
val length_replicate = thm "length_replicate";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    86
val length_rev = thm "length_rev";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    87
val length_take = thm "length_take";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    88
val length_tl = thm "length_tl";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    89
val length_upt = thm "length_upt";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    90
val length_zip = thm "length_zip";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    91
val lex_conv = thm "lex_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    92
val lex_def = thm "lex_def";
15693
3a67e61c6e96 tuned Map, renamed lex stuff in List.
nipkow
parents: 15246
diff changeset
    93
val lenlex_conv = thm "lenlex_conv";
3a67e61c6e96 tuned Map, renamed lex stuff in List.
nipkow
parents: 15246
diff changeset
    94
val lenlex_def = thm "lenlex_def";
13114
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    95
val lexn_conv = thm "lexn_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    96
val lexn_length = thm "lexn_length";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    97
val list_all2_Cons = thm "list_all2_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    98
val list_all2_Cons1 = thm "list_all2_Cons1";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
    99
val list_all2_Cons2 = thm "list_all2_Cons2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   100
val list_all2_Nil = thm "list_all2_Nil";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   101
val list_all2_Nil2 = thm "list_all2_Nil2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   102
val list_all2_append1 = thm "list_all2_append1";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   103
val list_all2_append2 = thm "list_all2_append2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   104
val list_all2_conv_all_nth = thm "list_all2_conv_all_nth";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   105
val list_all2_def = thm "list_all2_def";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   106
val list_all2_lengthD = thm "list_all2_lengthD";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   107
val list_all2_rev = thm "list_all2_rev";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   108
val list_all2_trans = thm "list_all2_trans";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   109
val list_all_append = thm "list_all_append";
17086
0eb0c9259dd7 added quite a few functions for code generation
nipkow
parents: 15693
diff changeset
   110
val list_all_iff = thm "list_all_iff";
13114
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   111
val list_ball_nth = thm "list_ball_nth";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   112
val list_update_overwrite = thm "list_update_overwrite";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   113
val list_update_same_conv = thm "list_update_same_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   114
val listsE = thm "listsE";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   115
val lists_IntI = thm "lists_IntI";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   116
val lists_Int_eq = thm "lists_Int_eq";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   117
val lists_mono = thm "lists_mono";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   118
val map_Suc_upt = thm "map_Suc_upt";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   119
val map_append = thm "map_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   120
val map_compose = thm "map_compose";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   121
val map_concat = thm "map_concat";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   122
val map_cong = thm "map_cong";
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13122
diff changeset
   123
val map_eq_Cons_conv = thm "map_eq_Cons_conv";
13114
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   124
val map_ext = thm "map_ext";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   125
val map_ident = thm "map_ident";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   126
val map_injective = thm "map_injective";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   127
val map_is_Nil_conv = thm "map_is_Nil_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   128
val map_replicate = thm "map_replicate";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   129
val neq_Nil_conv = thm "neq_Nil_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   130
val not_Cons_self = thm "not_Cons_self";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   131
val not_Cons_self2 = thm "not_Cons_self2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   132
val nth_Cons = thm "nth_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   133
val nth_Cons' = thm "nth_Cons'";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   134
val nth_Cons_0 = thm "nth_Cons_0";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   135
val nth_Cons_Suc = thm "nth_Cons_Suc";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   136
val nth_append = thm "nth_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   137
val nth_drop = thm "nth_drop";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   138
val nth_equalityI = thm "nth_equalityI";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   139
val nth_list_update = thm "nth_list_update";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   140
val nth_list_update_eq = thm "nth_list_update_eq";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   141
val nth_list_update_neq = thm "nth_list_update_neq";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   142
val nth_map_upt = thm "nth_map_upt";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   143
val nth_mem = thm "nth_mem";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   144
val nth_replicate = thm "nth_replicate";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   145
val nth_take = thm "nth_take";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   146
val nth_take_lemma = thm "nth_take_lemma";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   147
val nth_upt = thm "nth_upt";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   148
val nth_zip = thm "nth_zip";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   149
val replicate_0 = thm "replicate_0";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   150
val replicate_Suc = thm "replicate_Suc";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   151
val replicate_add = thm "replicate_add";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   152
val replicate_app_Cons_same = thm "replicate_app_Cons_same";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   153
val rev_append = thm "rev_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   154
val rev_concat = thm "rev_concat";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   155
val rev_drop = thm "rev_drop";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   156
val rev_exhaust = thm "rev_exhaust";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   157
val rev_induct = thm "rev_induct";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   158
val rev_is_Nil_conv = thm "rev_is_Nil_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   159
val rev_is_rev_conv = thm "rev_is_rev_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   160
val rev_map = thm "rev_map";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   161
val rev_replicate = thm "rev_replicate";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   162
val rev_rev_ident = thm "rev_rev_ident";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   163
val rev_take = thm "rev_take";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   164
val same_append_eq = thm "same_append_eq";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   165
val self_append_conv = thm "self_append_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   166
val self_append_conv2 = thm "self_append_conv2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   167
val set_append = thm "set_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   168
val set_concat = thm "set_concat";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   169
val set_conv_nth = thm "set_conv_nth";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   170
val set_empty = thm "set_empty";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   171
val set_filter = thm "set_filter";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   172
val set_map = thm "set_map";
17086
0eb0c9259dd7 added quite a few functions for code generation
nipkow
parents: 15693
diff changeset
   173
val mem_ii = thm "mem_iff";
13114
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   174
val set_remdups = thm "set_remdups";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   175
val set_replicate = thm "set_replicate";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   176
val set_replicate_conv_if = thm "set_replicate_conv_if";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   177
val set_rev = thm "set_rev";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   178
val set_subset_Cons = thm "set_subset_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   179
val set_take_whileD = thm "set_take_whileD";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   180
val set_update_subsetI = thm "set_update_subsetI";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   181
val set_update_subset_insert = thm "set_update_subset_insert";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   182
val set_upt = thm "set_upt";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   183
val set_zip = thm "set_zip";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   184
val start_le_sum = thm "start_le_sum";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   185
val sublist_Cons = thm "sublist_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   186
val sublist_append = thm "sublist_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   187
val sublist_def = thm "sublist_def";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   188
val sublist_empty = thm "sublist_empty";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   189
val sublist_nil = thm "sublist_nil";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   190
val sublist_shift_lemma = thm "sublist_shift_lemma";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   191
val sublist_singleton = thm "sublist_singleton";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   192
val sublist_upt_eq_take = thm "sublist_upt_eq_take";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   193
val sum_eq_0_conv = thm "sum_eq_0_conv";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   194
val takeWhile_append1 = thm "takeWhile_append1";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   195
val takeWhile_append2 = thm "takeWhile_append2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   196
val takeWhile_dropWhile_id = thm "takeWhile_dropWhile_id";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   197
val takeWhile_tail = thm "takeWhile_tail";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   198
val take_0 = thm "take_0";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   199
val take_Cons = thm "take_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   200
val take_Cons' = thm "take_Cons'";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   201
val take_Nil = thm "take_Nil";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   202
val take_Suc_Cons = thm "take_Suc_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   203
val take_all = thm "take_all";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   204
val take_append = thm "take_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   205
val take_drop = thm "take_drop";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   206
val take_equalityI = thm "take_equalityI";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   207
val take_map = thm "take_map"; 
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   208
val take_take = thm "take_take";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   209
val take_upt = thm "take_upt";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   210
val tl_append = thm "tl_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   211
val tl_append2 = thm "tl_append2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   212
val tl_replicate = thm "tl_replicate";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   213
val update_zip = thm "update_zip";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   214
val upt_0 = thm "upt_0";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   215
val upt_Suc = thm "upt_Suc";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   216
val upt_Suc_append = thm "upt_Suc_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   217
val upt_add_eq_append = thm "upt_add_eq_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   218
val upt_conv_Cons = thm "upt_conv_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   219
val upt_conv_Nil = thm "upt_conv_Nil";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   220
val upt_rec = thm "upt_rec";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   221
val wf_lex = thm "wf_lex";
15693
3a67e61c6e96 tuned Map, renamed lex stuff in List.
nipkow
parents: 15246
diff changeset
   222
val wf_lenlex = thm "wf_lenlex";
13114
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   223
val wf_lexn = thm "wf_lexn";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   224
val zip_Cons_Cons = thm "zip_Cons_Cons";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   225
val zip_Nil = thm "zip_Nil";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   226
val zip_append = thm "zip_append";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   227
val zip_append1 = thm "zip_append1";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   228
val zip_append2 = thm "zip_append2";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   229
val zip_replicate = thm "zip_replicate";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   230
val zip_rev = thm "zip_rev";
f2b00262bdfc converted;
wenzelm
parents: 13096
diff changeset
   231
val zip_update = thm "zip_update";