| author | haftmann |
| Thu, 18 Nov 2010 17:01:16 +0100 | |
| changeset 40855 | 30d512bf47a7 |
| parent 39028 | 848be46708dc |
| child 41837 | bbd861837ebc |
| permissions | -rw-r--r-- |
1 (* Title: HOL/Import/Generate-HOL/GenHOL4Base.thy
2 ID: $Id$
3 Author: Sebastian Skalberg (TU Muenchen)
4 *)
6 theory GenHOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin;
8 import_segment "hol4";
10 setup_dump "../HOL" "HOL4Base";
12 append_dump {*theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin*};
14 import_theory bool;
16 const_maps
17 T > True
18 F > False
19 "!" > All
20 "/\\" > HOL.conj
21 "\\/" > HOL.disj
22 "?" > Ex
23 "?!" > Ex1
24 "~" > Not
25 COND > HOL.If
26 bool_case > Datatype.bool.bool_case
27 ONE_ONE > HOL4Setup.ONE_ONE
28 ONTO > Fun.surj
29 TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
30 LET > HOL4Compat.LET;
32 ignore_thms
33 BOUNDED_DEF
34 BOUNDED_THM
35 UNBOUNDED_DEF
36 UNBOUNDED_THM;
38 end_import;
40 import_theory combin;
42 const_maps
43 o > Fun.comp;
45 end_import;
47 import_theory sum;
49 type_maps
50 sum > "+";
52 const_maps
53 INL > Sum_Type.Inl
54 INR > Sum_Type.Inr
55 ISL > HOL4Compat.ISL
56 ISR > HOL4Compat.ISR
57 OUTL > HOL4Compat.OUTL
58 OUTR > HOL4Compat.OUTR
59 sum_case > Datatype.sum.sum_case;
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;
70 end_import;
72 import_theory one;
74 type_maps
75 one > Product_Type.unit;
77 const_maps
78 one > Product_Type.Unity;
80 ignore_thms
81 one_TY_DEF
82 one_axiom
83 one_Axiom
84 one_DEF;
86 end_import;
88 import_theory option;
90 type_maps
91 option > Option.option;
93 const_maps
94 NONE > Option.option.None
95 SOME > Option.option.Some
96 option_case > Option.option.option_case
97 OPTION_MAP > Option.map
98 THE > Option.the
99 IS_SOME > HOL4Compat.IS_SOME
100 IS_NONE > HOL4Compat.IS_NONE
101 OPTION_JOIN > HOL4Compat.OPTION_JOIN;
103 ignore_thms
104 option_axiom
105 option_Axiom
106 option_TY_DEF
107 option_REP_ABS_DEF
108 SOME_DEF
109 NONE_DEF;
111 end_import;
113 import_theory marker;
114 end_import;
116 import_theory relation;
118 const_renames
119 reflexive > pred_reflexive;
121 end_import;
123 import_theory pair;
125 type_maps
126 prod > Product_Type.prod;
128 const_maps
129 "," > Pair
130 FST > fst
131 SND > snd
132 CURRY > curry
133 UNCURRY > split
134 "##" > map_pair
135 pair_case > split;
137 ignore_thms
138 prod_TY_DEF
139 MK_PAIR_DEF
140 IS_PAIR_DEF
141 ABS_REP_prod
142 COMMA_DEF;
144 end_import;
146 import_theory num;
148 type_maps
149 num > nat;
151 const_maps
152 SUC > Suc
153 0 > 0 :: nat;
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;
164 end_import;
166 import_theory prim_rec;
168 const_maps
169 "<" > Orderings.less :: "[nat,nat]=>bool";
171 end_import;
173 import_theory arithmetic;
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
184 "<=" > Orderings.less_eq :: "[nat,nat]=>bool"
185 "+" > Groups.plus :: "[nat,nat]=>nat"
186 "*" > Groups.times :: "[nat,nat]=>nat"
187 "-" > Groups.minus :: "[nat,nat]=>nat"
188 MIN > Orderings.min :: "[nat,nat]=>nat"
189 MAX > Orderings.max :: "[nat,nat]=>nat"
190 DIV > Divides.div :: "[nat,nat]=>nat"
191 MOD > Divides.mod :: "[nat,nat]=>nat"
192 EXP > Power.power :: "[nat,nat]=>nat";
194 end_import;
196 import_theory hrat;
197 end_import;
199 import_theory hreal;
200 end_import;
202 import_theory numeral;
203 end_import;
205 import_theory ind_type;
206 end_import;
208 import_theory divides;
210 const_maps
211 divides > Divides.times_class.dvd :: "[nat,nat]=>bool";
213 end_import;
215 import_theory prime;
216 end_import;
218 import_theory list;
220 type_maps
221 list > List.list;
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.append
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;
250 ignore_thms
251 list_TY_DEF
252 list_repfns
253 list0_def
254 list1_def
255 NIL
256 CONS_def;
258 end_import;
260 import_theory pred_set;
261 end_import;
263 import_theory operator;
264 end_import;
266 import_theory rich_list;
267 end_import;
269 import_theory state_transformer;
270 end_import;
272 append_dump "end";
274 flush_dump;
276 import_segment "";
278 end