author | krauss |
Wed, 02 Feb 2011 08:47:45 +0100 | |
changeset 41686 | d8efc2490b8e |
parent 41589 | bbd861837ebc |
child 43785 | 2bd54d4b5f3d |
permissions | -rw-r--r-- |
17322 | 1 |
(* Title: HOL/Import/Generate-HOLLight/GenHOLLight.thy |
41589 | 2 |
Author: Steven Obua, TU Muenchen |
17322 | 3 |
*) |
4 |
||
5 |
theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin; |
|
6 |
||
20275 | 7 |
(*;skip_import_dir "/home/obua/tmp/cache" |
19064 | 8 |
|
20275 | 9 |
;skip_import on*) |
19064 | 10 |
|
17322 | 11 |
;import_segment "hollight"; |
12 |
||
13 |
setup_dump "../HOLLight" "HOLLight"; |
|
14 |
||
15 |
append_dump {*theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":*}; |
|
16 |
||
17 |
;import_theory hollight; |
|
18 |
||
19 |
ignore_thms |
|
20 |
TYDEF_1 |
|
21 |
DEF_one |
|
22 |
TYDEF_prod |
|
23 |
TYDEF_num |
|
24 |
IND_SUC_0_EXISTS |
|
25 |
DEF__0 |
|
26 |
DEF_SUC |
|
27 |
DEF_IND_SUC |
|
28 |
DEF_IND_0 |
|
29 |
DEF_NUM_REP |
|
19064 | 30 |
TYDEF_sum |
17322 | 31 |
DEF_INL |
19203 | 32 |
DEF_INR |
20326 | 33 |
(* TYDEF_option*); |
17322 | 34 |
|
35 |
type_maps |
|
36 |
ind > Nat.ind |
|
37 |
bool > bool |
|
38 |
fun > fun |
|
39 |
N_1 > Product_Type.unit |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset
|
40 |
prod > Product_Type.prod |
37391 | 41 |
num > Nat.nat |
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset
|
42 |
sum > Sum_Type.sum |
20326 | 43 |
(* option > Datatype.option*); |
17322 | 44 |
|
17444 | 45 |
const_renames |
46 |
"==" > "eqeq" |
|
17490 | 47 |
".." > "dotdot" |
48 |
"ALL" > ALL_list; |
|
17444 | 49 |
|
17322 | 50 |
const_maps |
51 |
T > True |
|
52 |
F > False |
|
53 |
ONE_ONE > HOL4Setup.ONE_ONE |
|
54 |
ONTO > Fun.surj |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
55 |
"=" > HOL.eq |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
37678
diff
changeset
|
56 |
"==>" > HOL.implies |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
57 |
"/\\" > HOL.conj |
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
58 |
"\\/" > HOL.disj |
17322 | 59 |
"!" > All |
60 |
"?" > Ex |
|
61 |
"?!" > Ex1 |
|
62 |
"~" > Not |
|
63 |
o > Fun.comp |
|
64 |
"@" > "Hilbert_Choice.Eps" |
|
65 |
I > Fun.id |
|
66 |
one > Product_Type.Unity |
|
67 |
LET > HOL4Compat.LET |
|
68 |
mk_pair > Product_Type.Pair_Rep |
|
69 |
"," > Pair |
|
70 |
REP_prod > Rep_Prod |
|
71 |
ABS_prod > Abs_Prod |
|
72 |
FST > fst |
|
73 |
SND > snd |
|
74 |
"_0" > 0 :: nat |
|
75 |
SUC > Suc |
|
76 |
PRE > HOLLightCompat.Pred |
|
77 |
NUMERAL > HOL4Compat.NUMERAL |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
78 |
"+" > Groups.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
79 |
"*" > Groups.times :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset
|
80 |
"-" > Groups.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
17322 | 81 |
BIT0 > HOLLightCompat.NUMERAL_BIT0 |
19064 | 82 |
BIT1 > HOL4Compat.NUMERAL_BIT1 |
83 |
INL > Sum_Type.Inl |
|
20326 | 84 |
INR > Sum_Type.Inr |
85 |
(* NONE > Datatype.None |
|
86 |
SOME > Datatype.Some; |
|
87 |
HAS_SIZE > HOLLightCompat.HAS_SIZE; *) |
|
17440
df77edc4f5d0
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17322
diff
changeset
|
88 |
|
df77edc4f5d0
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17322
diff
changeset
|
89 |
(*import_until "TYDEF_sum" |
df77edc4f5d0
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17322
diff
changeset
|
90 |
|
df77edc4f5d0
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17322
diff
changeset
|
91 |
consts |
df77edc4f5d0
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17322
diff
changeset
|
92 |
print_theorems |
df77edc4f5d0
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17322
diff
changeset
|
93 |
|
df77edc4f5d0
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17322
diff
changeset
|
94 |
import_until *) |
17322 | 95 |
|
96 |
end_import; |
|
97 |
||
98 |
append_dump "end"; |
|
99 |
||
100 |
flush_dump; |
|
101 |
||
102 |
import_segment ""; |
|
103 |
||
104 |
end |