author  wenzelm 
Wed, 21 Sep 2005 18:04:49 +0200  
changeset 17566  484ff733f29c 
parent 17188  a26a4fc323ed 
child 17628  f4e2587bc7a5 
permissions  rwrr 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

1 
(* Title: HOL/Import/GenerateHOL/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 

28 
ONTO > HOL4Setup.ONTO 

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 

15647  169 
"<" > "op <" :: "[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 

15647  184 
"<=" > "op <=" :: "[nat,nat]=>bool" 
185 
"+" > "op +" :: "[nat,nat]=>nat" 

186 
"*" > "op *" :: "[nat,nat]=>nat" 

187 
"" > "op " :: "[nat,nat]=>nat" 

188 
MIN > Orderings.min :: "[nat,nat]=>nat" 

189 
MAX > Orderings.max :: "[nat,nat]=>nat" 

190 
DIV > "Divides.op div" :: "[nat,nat]=>nat" 

191 
MOD > "Divides.op mod" :: "[nat,nat]=>nat" 

192 
EXP > Nat.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 

15647  211 
divides > "Divides.op 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 