|
14516
|
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"
|
|
22997
|
25 |
"LENGTH" > "Nat.size_class.size"
|
|
14516
|
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"
|
|
23029
|
36 |
"APPEND" > "List.append"
|
|
14516
|
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
|