author | haftmann |
Thu, 17 May 2007 19:49:40 +0200 | |
changeset 22997 | d4f3b015b50b |
parent 21416 | f23e4e75dfd3 |
child 23029 | 79ee75dc1e59 |
permissions | -rw-r--r-- |
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
1 |
(* Title: HOL/Import/Generate-HOL/GenHOL4Base.thy |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
2 |
ID: $Id$ |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
3 |
Author: Sebastian Skalberg (TU Muenchen) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
4 |
*) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
5 |
|
16417 | 6 |
theory GenHOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin; |
14516 | 7 |
|
8 |
import_segment "hol4"; |
|
9 |
||
10 |
setup_dump "../HOL" "HOL4Base"; |
|
11 |
||
17566 | 12 |
append_dump {*theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin*}; |
14516 | 13 |
|
14 |
import_theory bool; |
|
15 |
||
16 |
const_maps |
|
17 |
T > True |
|
18 |
F > False |
|
19 |
"!" > All |
|
20 |
"/\\" > "op &" |
|
21 |
"\\/" > "op |" |
|
22 |
"?" > Ex |
|
23 |
"?!" > Ex1 |
|
24 |
"~" > Not |
|
17188 | 25 |
COND > HOL.If |
14516 | 26 |
bool_case > Datatype.bool.bool_case |
27 |
ONE_ONE > HOL4Setup.ONE_ONE |
|
17628 | 28 |
ONTO > Fun.surj |
14516 | 29 |
TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION |
30 |
LET > HOL4Compat.LET; |
|
31 |
||
32 |
ignore_thms |
|
33 |
BOUNDED_DEF |
|
34 |
BOUNDED_THM |
|
35 |
UNBOUNDED_DEF |
|
36 |
UNBOUNDED_THM; |
|
37 |
||
38 |
end_import; |
|
39 |
||
40 |
import_theory combin; |
|
41 |
||
42 |
const_maps |
|
43 |
o > Fun.comp; |
|
44 |
||
45 |
end_import; |
|
46 |
||
47 |
import_theory sum; |
|
48 |
||
49 |
type_maps |
|
50 |
sum > "+"; |
|
51 |
||
52 |
const_maps |
|
15647 | 53 |
INL > Sum_Type.Inl |
54 |
INR > Sum_Type.Inr |
|
14516 | 55 |
ISL > HOL4Compat.ISL |
56 |
ISR > HOL4Compat.ISR |
|
57 |
OUTL > HOL4Compat.OUTL |
|
58 |
OUTR > HOL4Compat.OUTR |
|
59 |
sum_case > Datatype.sum.sum_case; |
|
60 |
||
61 |
ignore_thms |
|
62 |
sum_TY_DEF |
|
63 |
sum_ISO_DEF |
|
64 |
IS_SUM_REP |
|
65 |
INL_DEF |
|
66 |
INR_DEF |
|
67 |
sum_axiom |
|
68 |
sum_Axiom; |
|
69 |
||
70 |
end_import; |
|
71 |
||
72 |
import_theory one; |
|
73 |
||
74 |
type_maps |
|
75 |
one > Product_Type.unit; |
|
76 |
||
77 |
const_maps |
|
78 |
one > Product_Type.Unity; |
|
79 |
||
80 |
ignore_thms |
|
81 |
one_TY_DEF |
|
82 |
one_axiom |
|
83 |
one_Axiom |
|
84 |
one_DEF; |
|
85 |
||
86 |
end_import; |
|
87 |
||
88 |
import_theory option; |
|
89 |
||
90 |
type_maps |
|
91 |
option > Datatype.option; |
|
92 |
||
93 |
const_maps |
|
94 |
NONE > Datatype.option.None |
|
95 |
SOME > Datatype.option.Some |
|
96 |
option_case > Datatype.option.option_case |
|
97 |
OPTION_MAP > Datatype.option_map |
|
98 |
THE > Datatype.the |
|
99 |
IS_SOME > HOL4Compat.IS_SOME |
|
100 |
IS_NONE > HOL4Compat.IS_NONE |
|
101 |
OPTION_JOIN > HOL4Compat.OPTION_JOIN; |
|
102 |
||
103 |
ignore_thms |
|
104 |
option_axiom |
|
105 |
option_Axiom |
|
106 |
option_TY_DEF |
|
107 |
option_REP_ABS_DEF |
|
108 |
SOME_DEF |
|
109 |
NONE_DEF; |
|
110 |
||
111 |
end_import; |
|
112 |
||
113 |
import_theory marker; |
|
114 |
end_import; |
|
115 |
||
116 |
import_theory relation; |
|
117 |
||
118 |
const_renames |
|
119 |
reflexive > pred_reflexive; |
|
120 |
||
121 |
end_import; |
|
122 |
||
123 |
import_theory pair; |
|
124 |
||
125 |
type_maps |
|
126 |
prod > "*"; |
|
127 |
||
128 |
const_maps |
|
129 |
"," > Pair |
|
130 |
FST > fst |
|
131 |
SND > snd |
|
132 |
CURRY > curry |
|
133 |
UNCURRY > split |
|
134 |
"##" > prod_fun |
|
135 |
pair_case > split; |
|
136 |
||
137 |
ignore_thms |
|
138 |
prod_TY_DEF |
|
139 |
MK_PAIR_DEF |
|
140 |
IS_PAIR_DEF |
|
141 |
ABS_REP_prod |
|
142 |
COMMA_DEF; |
|
143 |
||
144 |
end_import; |
|
145 |
||
146 |
import_theory num; |
|
147 |
||
148 |
type_maps |
|
149 |
num > nat; |
|
150 |
||
151 |
const_maps |
|
152 |
SUC > Suc |
|
153 |
0 > 0 :: nat; |
|
154 |
||
155 |
ignore_thms |
|
156 |
num_TY_DEF |
|
157 |
num_ISO_DEF |
|
158 |
IS_NUM_REP |
|
159 |
ZERO_REP_DEF |
|
160 |
SUC_REP_DEF |
|
161 |
ZERO_DEF |
|
162 |
SUC_DEF; |
|
163 |
||
164 |
end_import; |
|
165 |
||
166 |
import_theory prim_rec; |
|
167 |
||
168 |
const_maps |
|
22997 | 169 |
"<" > Orderings.ord_class.less :: "[nat,nat]=>bool"; |
14516 | 170 |
|
171 |
end_import; |
|
172 |
||
173 |
import_theory arithmetic; |
|
174 |
||
175 |
const_maps |
|
176 |
ALT_ZERO > HOL4Compat.ALT_ZERO |
|
177 |
NUMERAL_BIT1 > HOL4Compat.NUMERAL_BIT1 |
|
178 |
NUMERAL_BIT2 > HOL4Compat.NUMERAL_BIT2 |
|
179 |
NUMERAL > HOL4Compat.NUMERAL |
|
180 |
num_case > Nat.nat.nat_case |
|
181 |
">" > HOL4Compat.nat_gt |
|
182 |
">=" > HOL4Compat.nat_ge |
|
183 |
FUNPOW > HOL4Compat.FUNPOW |
|
22997 | 184 |
"<=" > Orderings.ord_class.less_eq :: "[nat,nat]=>bool" |
185 |
"+" > HOL.plus_class.plus :: "[nat,nat]=>nat" |
|
186 |
"*" > HOL.times_class.times :: "[nat,nat]=>nat" |
|
187 |
"-" > HOL.minus_class.minus :: "[nat,nat]=>nat" |
|
15647 | 188 |
MIN > Orderings.min :: "[nat,nat]=>nat" |
189 |
MAX > Orderings.max :: "[nat,nat]=>nat" |
|
22997 | 190 |
DIV > Divides.div_class.div :: "[nat,nat]=>nat" |
191 |
MOD > Divides.div_class.mod :: "[nat,nat]=>nat" |
|
192 |
EXP > Nat.power_class.power :: "[nat,nat]=>nat"; |
|
14516 | 193 |
|
194 |
end_import; |
|
195 |
||
196 |
import_theory hrat; |
|
197 |
end_import; |
|
198 |
||
199 |
import_theory hreal; |
|
200 |
end_import; |
|
201 |
||
202 |
import_theory numeral; |
|
203 |
end_import; |
|
204 |
||
205 |
import_theory ind_type; |
|
206 |
end_import; |
|
207 |
||
208 |
import_theory divides; |
|
209 |
||
210 |
const_maps |
|
21416 | 211 |
divides > "Divides.dvd" :: "[nat,nat]=>bool"; |
14516 | 212 |
|
213 |
end_import; |
|
214 |
||
215 |
import_theory prime; |
|
216 |
end_import; |
|
217 |
||
218 |
import_theory list; |
|
219 |
||
220 |
type_maps |
|
221 |
list > List.list; |
|
222 |
||
223 |
const_maps |
|
224 |
CONS > List.list.Cons |
|
225 |
NIL > List.list.Nil |
|
226 |
list_case > List.list.list_case |
|
227 |
NULL > List.null |
|
228 |
HD > List.hd |
|
229 |
TL > List.tl |
|
230 |
MAP > List.map |
|
231 |
MEM > "List.op mem" |
|
232 |
FILTER > List.filter |
|
233 |
FOLDL > List.foldl |
|
234 |
EVERY > List.list_all |
|
235 |
REVERSE > List.rev |
|
236 |
LAST > List.last |
|
237 |
FRONT > List.butlast |
|
238 |
APPEND > "List.op @" |
|
239 |
FLAT > List.concat |
|
240 |
LENGTH > Nat.size |
|
241 |
REPLICATE > List.replicate |
|
242 |
list_size > HOL4Compat.list_size |
|
243 |
SUM > HOL4Compat.sum |
|
244 |
FOLDR > HOL4Compat.FOLDR |
|
245 |
EXISTS > HOL4Compat.list_exists |
|
246 |
MAP2 > HOL4Compat.map2 |
|
247 |
ZIP > HOL4Compat.ZIP |
|
248 |
UNZIP > HOL4Compat.unzip; |
|
249 |
||
250 |
ignore_thms |
|
251 |
list_TY_DEF |
|
252 |
list_repfns |
|
253 |
list0_def |
|
254 |
list1_def |
|
255 |
NIL |
|
256 |
CONS_def; |
|
257 |
||
258 |
end_import; |
|
259 |
||
260 |
import_theory pred_set; |
|
261 |
end_import; |
|
262 |
||
263 |
import_theory operator; |
|
264 |
end_import; |
|
265 |
||
266 |
import_theory rich_list; |
|
267 |
end_import; |
|
268 |
||
269 |
import_theory state_transformer; |
|
270 |
end_import; |
|
271 |
||
272 |
append_dump "end"; |
|
273 |
||
274 |
flush_dump; |
|
275 |
||
276 |
import_segment ""; |
|
277 |
||
278 |
end |