src/HOL/Import/HOL/list.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
child 22997 d4f3b015b50b
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "EL" > "EL_def"
     7 
     8 type_maps
     9   "list" > "List.list"
    10 
    11 const_maps
    12   "list_size" > "HOL4Compat.list_size"
    13   "list_case" > "List.list.list_case"
    14   "ZIP" > "HOL4Compat.ZIP"
    15   "UNZIP" > "HOL4Compat.unzip"
    16   "TL" > "List.tl"
    17   "SUM" > "HOL4Compat.sum"
    18   "REVERSE" > "List.rev"
    19   "REPLICATE" > "List.replicate"
    20   "NULL" > "List.null"
    21   "NIL" > "List.list.Nil"
    22   "MEM" > "List.op mem"
    23   "MAP2" > "HOL4Compat.map2"
    24   "MAP" > "List.map"
    25   "LENGTH" > "Nat.size"
    26   "LAST" > "List.last"
    27   "HD" > "List.hd"
    28   "FRONT" > "List.butlast"
    29   "FOLDR" > "HOL4Compat.FOLDR"
    30   "FOLDL" > "List.foldl"
    31   "FLAT" > "List.concat"
    32   "FILTER" > "List.filter"
    33   "EXISTS" > "HOL4Compat.list_exists"
    34   "EVERY" > "List.list_all"
    35   "CONS" > "List.list.Cons"
    36   "APPEND" > "List.op @"
    37 
    38 thm_maps
    39   "list_size_def" > "HOL4Compat.list_size_def"
    40   "list_size_cong" > "HOL4Base.list.list_size_cong"
    41   "list_nchotomy" > "HOL4Compat.list_CASES"
    42   "list_induction" > "HOL4Compat.unzip.induct"
    43   "list_distinct" > "List.list.simps_1"
    44   "list_case_def" > "HOL4Compat.list_case_def"
    45   "list_case_cong" > "HOL4Compat.list_case_cong"
    46   "list_case_compute" > "HOL4Base.list.list_case_compute"
    47   "list_INDUCT" > "HOL4Compat.unzip.induct"
    48   "list_CASES" > "HOL4Compat.list_CASES"
    49   "list_Axiom_old" > "HOL4Compat.list_Axiom_old"
    50   "list_Axiom" > "HOL4Compat.list_Axiom"
    51   "list_11" > "List.list.simps_3"
    52   "ZIP_UNZIP" > "HOL4Base.list.ZIP_UNZIP"
    53   "ZIP_MAP" > "HOL4Base.list.ZIP_MAP"
    54   "ZIP" > "HOL4Compat.ZIP"
    55   "WF_LIST_PRED" > "HOL4Base.list.WF_LIST_PRED"
    56   "UNZIP_ZIP" > "HOL4Base.list.UNZIP_ZIP"
    57   "UNZIP" > "HOL4Compat.UNZIP"
    58   "TL" > "List.tl.simps_2"
    59   "SUM" > "HOL4Compat.SUM"
    60   "REVERSE_REVERSE" > "List.rev_rev_ident"
    61   "REVERSE_DEF" > "HOL4Compat.REVERSE"
    62   "REVERSE_APPEND" > "List.rev_append"
    63   "NULL_DEF" > "HOL4Compat.NULL_DEF"
    64   "NULL" > "HOL4Base.list.NULL"
    65   "NOT_NIL_CONS" > "List.list.simps_1"
    66   "NOT_EXISTS" > "HOL4Base.list.NOT_EXISTS"
    67   "NOT_EVERY" > "HOL4Base.list.NOT_EVERY"
    68   "NOT_EQ_LIST" > "HOL4Base.list.NOT_EQ_LIST"
    69   "NOT_CONS_NIL" > "List.list.simps_2"
    70   "MEM_ZIP" > "HOL4Base.list.MEM_ZIP"
    71   "MEM_MAP" > "HOL4Base.list.MEM_MAP"
    72   "MEM_EL" > "HOL4Base.list.MEM_EL"
    73   "MEM_APPEND" > "HOL4Base.list.MEM_APPEND"
    74   "MEM" > "HOL4Compat.MEM"
    75   "MAP_EQ_NIL" > "HOL4Base.list.MAP_EQ_NIL"
    76   "MAP_CONG" > "HOL4Base.list.MAP_CONG"
    77   "MAP_APPEND" > "List.map_append"
    78   "MAP2_ZIP" > "HOL4Base.list.MAP2_ZIP"
    79   "MAP2" > "HOL4Compat.MAP2"
    80   "MAP" > "HOL4Compat.MAP"
    81   "LIST_NOT_EQ" > "HOL4Base.list.LIST_NOT_EQ"
    82   "LENGTH_ZIP" > "HOL4Base.list.LENGTH_ZIP"
    83   "LENGTH_UNZIP" > "HOL4Base.list.LENGTH_UNZIP"
    84   "LENGTH_NIL" > "List.length_0_conv"
    85   "LENGTH_MAP" > "List.length_map"
    86   "LENGTH_EQ_NIL" > "HOL4Base.list.LENGTH_EQ_NIL"
    87   "LENGTH_EQ_CONS" > "HOL4Base.list.LENGTH_EQ_CONS"
    88   "LENGTH_CONS" > "HOL4Base.list.LENGTH_CONS"
    89   "LENGTH_APPEND" > "List.length_append"
    90   "LENGTH" > "HOL4Compat.LENGTH"
    91   "LAST_DEF" > "List.last.simps"
    92   "LAST_CONS" > "HOL4Base.list.LAST_CONS"
    93   "HD" > "List.hd.simps"
    94   "FRONT_DEF" > "List.butlast.simps_2"
    95   "FRONT_CONS" > "HOL4Base.list.FRONT_CONS"
    96   "FOLDR_CONG" > "HOL4Base.list.FOLDR_CONG"
    97   "FOLDR" > "HOL4Compat.FOLDR"
    98   "FOLDL_CONG" > "HOL4Base.list.FOLDL_CONG"
    99   "FOLDL" > "HOL4Compat.FOLDL"
   100   "FLAT" > "HOL4Compat.FLAT"
   101   "FILTER" > "HOL4Compat.FILTER"
   102   "EXISTS_MEM" > "HOL4Base.list.EXISTS_MEM"
   103   "EXISTS_DEF" > "HOL4Compat.list_exists_DEF"
   104   "EXISTS_CONG" > "HOL4Base.list.EXISTS_CONG"
   105   "EXISTS_APPEND" > "HOL4Base.list.EXISTS_APPEND"
   106   "EVERY_MONOTONIC" > "HOL4Base.list.EVERY_MONOTONIC"
   107   "EVERY_MEM" > "HOL4Base.list.EVERY_MEM"
   108   "EVERY_EL" > "HOL4Base.list.EVERY_EL"
   109   "EVERY_DEF" > "HOL4Compat.EVERY_DEF"
   110   "EVERY_CONJ" > "HOL4Base.list.EVERY_CONJ"
   111   "EVERY_CONG" > "HOL4Base.list.EVERY_CONG"
   112   "EVERY_APPEND" > "List.list_all_append"
   113   "EQ_LIST" > "HOL4Base.list.EQ_LIST"
   114   "EL_compute" > "HOL4Base.list.EL_compute"
   115   "EL_ZIP" > "HOL4Base.list.EL_ZIP"
   116   "EL" > "HOL4Base.list.EL"
   117   "CONS_ACYCLIC" > "HOL4Base.list.CONS_ACYCLIC"
   118   "CONS_11" > "List.list.simps_3"
   119   "CONS" > "HOL4Base.list.CONS"
   120   "APPEND_eq_NIL" > "HOL4Base.list.APPEND_eq_NIL"
   121   "APPEND_NIL" > "List.append_Nil2"
   122   "APPEND_FRONT_LAST" > "List.append_butlast_last_id"
   123   "APPEND_ASSOC" > "List.append_assoc"
   124   "APPEND_11" > "HOL4Base.list.APPEND_11"
   125   "APPEND" > "HOL4Compat.APPEND"
   126 
   127 ignore_thms
   128   "list_repfns"
   129   "list_TY_DEF"
   130   "list1_def"
   131   "list0_def"
   132   "NIL"
   133   "CONS_def"
   134 
   135 end