|
14516
|
1 |
theory GenHOL4Real = GenHOL4Base:
|
|
|
2 |
|
|
|
3 |
import_segment "hol4";
|
|
|
4 |
|
|
|
5 |
setup_dump "../HOL" "HOL4Real";
|
|
|
6 |
|
|
|
7 |
append_dump "theory HOL4Real = HOL4Base:";
|
|
|
8 |
|
|
|
9 |
import_theory realax;
|
|
|
10 |
|
|
|
11 |
type_maps
|
|
|
12 |
real > RealDef.real;
|
|
|
13 |
|
|
|
14 |
const_maps
|
|
|
15 |
real_0 > 0 :: real
|
|
|
16 |
real_1 > 1 :: real
|
|
|
17 |
real_neg > uminus :: "real \<Rightarrow> real"
|
|
|
18 |
inv > HOL.inverse :: "real \<Rightarrow> real"
|
|
|
19 |
real_add > "op +" :: "[real,real] \<Rightarrow> real"
|
|
|
20 |
real_mul > "op *" :: "[real,real] \<Rightarrow> real"
|
|
|
21 |
real_lt > "op <" :: "[real,real] \<Rightarrow> bool";
|
|
|
22 |
|
|
|
23 |
ignore_thms
|
|
|
24 |
real_TY_DEF
|
|
|
25 |
real_tybij
|
|
|
26 |
real_0
|
|
|
27 |
real_1
|
|
|
28 |
real_neg
|
|
|
29 |
real_inv
|
|
|
30 |
real_add
|
|
|
31 |
real_mul
|
|
|
32 |
real_lt
|
|
|
33 |
real_of_hreal
|
|
|
34 |
hreal_of_real
|
|
|
35 |
REAL_ISO_EQ
|
|
|
36 |
REAL_POS
|
|
|
37 |
SUP_ALLPOS_LEMMA1
|
|
|
38 |
SUP_ALLPOS_LEMMA2
|
|
|
39 |
SUP_ALLPOS_LEMMA3
|
|
|
40 |
SUP_ALLPOS_LEMMA4;
|
|
|
41 |
|
|
|
42 |
end_import;
|
|
|
43 |
|
|
|
44 |
import_theory real;
|
|
|
45 |
|
|
|
46 |
const_maps
|
|
|
47 |
real_gt > HOL4Compat.real_gt
|
|
|
48 |
real_ge > HOL4Compat.real_ge
|
|
|
49 |
real_lte > "op <=" :: "[real,real] \<Rightarrow> bool"
|
|
|
50 |
real_sub > "op -" :: "[real,real] \<Rightarrow> real"
|
|
|
51 |
"/" > HOL.divide :: "[real,real] \<Rightarrow> real"
|
|
|
52 |
pow > Nat.power :: "[real,nat] \<Rightarrow> real"
|
|
|
53 |
abs > HOL.abs :: "real \<Rightarrow> real"
|
|
|
54 |
real_of_num > RealDef.real :: "nat \<Rightarrow> real";
|
|
|
55 |
|
|
|
56 |
end_import;
|
|
|
57 |
|
|
|
58 |
import_theory topology;
|
|
|
59 |
end_import;
|
|
|
60 |
|
|
|
61 |
import_theory nets;
|
|
|
62 |
end_import;
|
|
|
63 |
|
|
|
64 |
import_theory seq;
|
|
|
65 |
end_import;
|
|
|
66 |
|
|
|
67 |
import_theory lim;
|
|
|
68 |
end_import;
|
|
|
69 |
|
|
|
70 |
import_theory powser;
|
|
|
71 |
end_import;
|
|
|
72 |
|
|
|
73 |
import_theory transc;
|
|
|
74 |
end_import;
|
|
|
75 |
|
|
|
76 |
import_theory poly;
|
|
|
77 |
end_import;
|
|
|
78 |
|
|
|
79 |
append_dump "end";
|
|
|
80 |
|
|
|
81 |
flush_dump;
|
|
|
82 |
|
|
|
83 |
import_segment "";
|
|
|
84 |
|
|
|
85 |
end
|