|
17322
|
1 |
(* Title: HOL/Import/Generate-HOLLight/GenHOLLight.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Steven Obua (TU Muenchen)
|
|
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
|
|
|
7 |
|
|
|
8 |
ML {* reset ProofKernel.debug; *}
|
|
|
9 |
ML {* reset Shuffler.debug; *}
|
|
|
10 |
ML {* set show_types; set show_sorts; *}
|
|
|
11 |
|
|
|
12 |
;import_segment "hollight";
|
|
|
13 |
|
|
|
14 |
setup_dump "../HOLLight" "HOLLight";
|
|
|
15 |
|
|
|
16 |
append_dump {*theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":*};
|
|
|
17 |
|
|
|
18 |
;import_theory hollight;
|
|
|
19 |
|
|
|
20 |
ignore_thms
|
|
|
21 |
TYDEF_1
|
|
|
22 |
DEF_one
|
|
|
23 |
TYDEF_prod
|
|
|
24 |
TYDEF_num
|
|
|
25 |
IND_SUC_0_EXISTS
|
|
|
26 |
DEF__0
|
|
|
27 |
DEF_SUC
|
|
|
28 |
DEF_IND_SUC
|
|
|
29 |
DEF_IND_0
|
|
|
30 |
DEF_NUM_REP
|
|
|
31 |
TYDEF_sum
|
|
|
32 |
DEF_INL
|
|
|
33 |
DEF_INR;
|
|
|
34 |
|
|
|
35 |
type_maps
|
|
|
36 |
ind > Nat.ind
|
|
|
37 |
bool > bool
|
|
|
38 |
fun > fun
|
|
|
39 |
N_1 > Product_Type.unit
|
|
|
40 |
prod > "*"
|
|
|
41 |
num > nat
|
|
|
42 |
sum > "+";
|
|
|
43 |
|
|
|
44 |
const_maps
|
|
|
45 |
T > True
|
|
|
46 |
F > False
|
|
|
47 |
ONE_ONE > HOL4Setup.ONE_ONE
|
|
|
48 |
ONTO > Fun.surj
|
|
|
49 |
"=" > "op ="
|
|
|
50 |
"==>" > "op -->"
|
|
|
51 |
"/\\" > "op &"
|
|
|
52 |
"\\/" > "op |"
|
|
|
53 |
"!" > All
|
|
|
54 |
"?" > Ex
|
|
|
55 |
"?!" > Ex1
|
|
|
56 |
"~" > Not
|
|
|
57 |
o > Fun.comp
|
|
|
58 |
"@" > "Hilbert_Choice.Eps"
|
|
|
59 |
I > Fun.id
|
|
|
60 |
one > Product_Type.Unity
|
|
|
61 |
LET > HOL4Compat.LET
|
|
|
62 |
mk_pair > Product_Type.Pair_Rep
|
|
|
63 |
"," > Pair
|
|
|
64 |
REP_prod > Rep_Prod
|
|
|
65 |
ABS_prod > Abs_Prod
|
|
|
66 |
FST > fst
|
|
|
67 |
SND > snd
|
|
|
68 |
"_0" > 0 :: nat
|
|
|
69 |
SUC > Suc
|
|
|
70 |
PRE > HOLLightCompat.Pred
|
|
|
71 |
NUMERAL > HOL4Compat.NUMERAL
|
|
|
72 |
"+" > "op +" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
|
|
|
73 |
"*" > "op *" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
|
|
|
74 |
"-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
|
|
|
75 |
BIT0 > HOLLightCompat.NUMERAL_BIT0
|
|
|
76 |
BIT1 > HOL4Compat.NUMERAL_BIT1
|
|
|
77 |
INL > Sum_Type.Inl
|
|
|
78 |
INR > Sum_Type.Inr;
|
|
|
79 |
|
|
|
80 |
end_import;
|
|
|
81 |
|
|
|
82 |
append_dump "end";
|
|
|
83 |
|
|
|
84 |
flush_dump;
|
|
|
85 |
|
|
|
86 |
import_segment "";
|
|
|
87 |
|
|
|
88 |
end
|