1 import |
|
2 |
|
3 import_segment "hol4" |
|
4 |
|
5 def_maps |
|
6 "treal_of_hreal" > "treal_of_hreal_def" |
|
7 "treal_neg" > "treal_neg_def" |
|
8 "treal_mul" > "treal_mul_def" |
|
9 "treal_lt" > "treal_lt_def" |
|
10 "treal_inv" > "treal_inv_def" |
|
11 "treal_eq" > "treal_eq_def" |
|
12 "treal_add" > "treal_add_def" |
|
13 "treal_1" > "treal_1_def" |
|
14 "treal_0" > "treal_0_def" |
|
15 "hreal_of_treal" > "hreal_of_treal_def" |
|
16 |
|
17 type_maps |
|
18 "real" > "RealDef.real" |
|
19 |
|
20 const_maps |
|
21 "treal_of_hreal" > "HOL4Real.realax.treal_of_hreal" |
|
22 "treal_neg" > "HOL4Real.realax.treal_neg" |
|
23 "treal_mul" > "HOL4Real.realax.treal_mul" |
|
24 "treal_lt" > "HOL4Real.realax.treal_lt" |
|
25 "treal_inv" > "HOL4Real.realax.treal_inv" |
|
26 "treal_eq" > "HOL4Real.realax.treal_eq" |
|
27 "treal_add" > "HOL4Real.realax.treal_add" |
|
28 "treal_1" > "HOL4Real.realax.treal_1" |
|
29 "treal_0" > "HOL4Real.realax.treal_0" |
|
30 "real_sub" > "Groups.minus_class.minus" :: "real => real => real" |
|
31 "real_neg" > "Groups.uminus_class.uminus" :: "real => real" |
|
32 "real_mul" > "Groups.times_class.times" :: "real => real => real" |
|
33 "real_lt" > "Orderings.ord_class.less" :: "real => real => bool" |
|
34 "real_div" > "Fields.inverse_class.divide" :: "real => real => real" |
|
35 "real_add" > "Groups.plus_class.plus" :: "real => real => real" |
|
36 "real_1" > "Groups.one_class.one" :: "real" |
|
37 "real_0" > "Groups.zero_class.zero" :: "real" |
|
38 "mk_real" > "HOL.undefined" |
|
39 "inv" > "Fields.inverse_class.inverse" :: "real => real" |
|
40 "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal" |
|
41 "dest_real" > "HOL.undefined" |
|
42 |
|
43 thm_maps |
|
44 "treal_of_hreal_def" > "HOL4Real.realax.treal_of_hreal_def" |
|
45 "treal_of_hreal" > "HOL4Real.realax.treal_of_hreal" |
|
46 "treal_neg_def" > "HOL4Real.realax.treal_neg_def" |
|
47 "treal_neg" > "HOL4Real.realax.treal_neg" |
|
48 "treal_mul_def" > "HOL4Real.realax.treal_mul_def" |
|
49 "treal_mul" > "HOL4Real.realax.treal_mul" |
|
50 "treal_lt_def" > "HOL4Real.realax.treal_lt_def" |
|
51 "treal_lt" > "HOL4Real.realax.treal_lt" |
|
52 "treal_inv_def" > "HOL4Real.realax.treal_inv_def" |
|
53 "treal_inv" > "HOL4Real.realax.treal_inv" |
|
54 "treal_eq_def" > "HOL4Real.realax.treal_eq_def" |
|
55 "treal_eq" > "HOL4Real.realax.treal_eq" |
|
56 "treal_add_def" > "HOL4Real.realax.treal_add_def" |
|
57 "treal_add" > "HOL4Real.realax.treal_add" |
|
58 "treal_1_def" > "HOL4Real.realax.treal_1_def" |
|
59 "treal_1" > "HOL4Real.realax.treal_1" |
|
60 "treal_0_def" > "HOL4Real.realax.treal_0_def" |
|
61 "treal_0" > "HOL4Real.realax.treal_0" |
|
62 "hreal_of_treal_def" > "HOL4Real.realax.hreal_of_treal_def" |
|
63 "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal" |
|
64 "TREAL_NEG_WELLDEF" > "HOL4Real.realax.TREAL_NEG_WELLDEF" |
|
65 "TREAL_MUL_WELLDEFR" > "HOL4Real.realax.TREAL_MUL_WELLDEFR" |
|
66 "TREAL_MUL_WELLDEF" > "HOL4Real.realax.TREAL_MUL_WELLDEF" |
|
67 "TREAL_MUL_SYM" > "HOL4Real.realax.TREAL_MUL_SYM" |
|
68 "TREAL_MUL_LINV" > "HOL4Real.realax.TREAL_MUL_LINV" |
|
69 "TREAL_MUL_LID" > "HOL4Real.realax.TREAL_MUL_LID" |
|
70 "TREAL_MUL_ASSOC" > "HOL4Real.realax.TREAL_MUL_ASSOC" |
|
71 "TREAL_LT_WELLDEFR" > "HOL4Real.realax.TREAL_LT_WELLDEFR" |
|
72 "TREAL_LT_WELLDEFL" > "HOL4Real.realax.TREAL_LT_WELLDEFL" |
|
73 "TREAL_LT_WELLDEF" > "HOL4Real.realax.TREAL_LT_WELLDEF" |
|
74 "TREAL_LT_TRANS" > "HOL4Real.realax.TREAL_LT_TRANS" |
|
75 "TREAL_LT_TOTAL" > "HOL4Real.realax.TREAL_LT_TOTAL" |
|
76 "TREAL_LT_REFL" > "HOL4Real.realax.TREAL_LT_REFL" |
|
77 "TREAL_LT_MUL" > "HOL4Real.realax.TREAL_LT_MUL" |
|
78 "TREAL_LT_ADD" > "HOL4Real.realax.TREAL_LT_ADD" |
|
79 "TREAL_LDISTRIB" > "HOL4Real.realax.TREAL_LDISTRIB" |
|
80 "TREAL_ISO" > "HOL4Real.realax.TREAL_ISO" |
|
81 "TREAL_INV_WELLDEF" > "HOL4Real.realax.TREAL_INV_WELLDEF" |
|
82 "TREAL_INV_0" > "HOL4Real.realax.TREAL_INV_0" |
|
83 "TREAL_EQ_TRANS" > "HOL4Real.realax.TREAL_EQ_TRANS" |
|
84 "TREAL_EQ_SYM" > "HOL4Real.realax.TREAL_EQ_SYM" |
|
85 "TREAL_EQ_REFL" > "HOL4Real.realax.TREAL_EQ_REFL" |
|
86 "TREAL_EQ_EQUIV" > "HOL4Real.realax.TREAL_EQ_EQUIV" |
|
87 "TREAL_EQ_AP" > "HOL4Real.realax.TREAL_EQ_AP" |
|
88 "TREAL_BIJ_WELLDEF" > "HOL4Real.realax.TREAL_BIJ_WELLDEF" |
|
89 "TREAL_BIJ" > "HOL4Real.realax.TREAL_BIJ" |
|
90 "TREAL_ADD_WELLDEFR" > "HOL4Real.realax.TREAL_ADD_WELLDEFR" |
|
91 "TREAL_ADD_WELLDEF" > "HOL4Real.realax.TREAL_ADD_WELLDEF" |
|
92 "TREAL_ADD_SYM" > "HOL4Real.realax.TREAL_ADD_SYM" |
|
93 "TREAL_ADD_LINV" > "HOL4Real.realax.TREAL_ADD_LINV" |
|
94 "TREAL_ADD_LID" > "HOL4Real.realax.TREAL_ADD_LID" |
|
95 "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC" |
|
96 "TREAL_10" > "HOL4Real.realax.TREAL_10" |
|
97 "REAL_SUP_ALLPOS" > "Compatibility.REAL_SUP_ALLPOS" |
|
98 "REAL_MUL_SYM" > "Fields.linordered_field_class.sign_simps_21" |
|
99 "REAL_MUL_LINV" > "Fields.division_ring_class.left_inverse" |
|
100 "REAL_MUL_LID" > "Divides.arithmetic_simps_42" |
|
101 "REAL_MUL_ASSOC" > "Fields.linordered_field_class.sign_simps_22" |
|
102 "REAL_LT_TRANS" > "Orderings.order_less_trans" |
|
103 "REAL_LT_TOTAL" > "Compatibility.REAL_LT_TOTAL" |
|
104 "REAL_LT_REFL" > "Orderings.order_less_irrefl" |
|
105 "REAL_LT_MUL" > "RealDef.real_mult_order" |
|
106 "REAL_LT_IADD" > "Groups.ordered_cancel_ab_semigroup_add_class.add_strict_left_mono" |
|
107 "REAL_LDISTRIB" > "Fields.linordered_field_class.sign_simps_7" |
|
108 "REAL_INV_0" > "Fields.division_ring_inverse_zero_class.inverse_zero" |
|
109 "REAL_ADD_SYM" > "Fields.linordered_field_class.sign_simps_18" |
|
110 "REAL_ADD_LINV" > "Groups.ab_group_add_class.ab_left_minus" |
|
111 "REAL_ADD_LID" > "Divides.arithmetic_simps_38" |
|
112 "REAL_ADD_ASSOC" > "Fields.linordered_field_class.sign_simps_19" |
|
113 "REAL_10" > "Compatibility.REAL_10" |
|
114 "HREAL_RDISTRIB" > "HOL4Real.realax.HREAL_RDISTRIB" |
|
115 "HREAL_LT_REFL" > "HOL4Real.realax.HREAL_LT_REFL" |
|
116 "HREAL_LT_NE" > "HOL4Real.realax.HREAL_LT_NE" |
|
117 "HREAL_LT_LADD" > "HOL4Real.realax.HREAL_LT_LADD" |
|
118 "HREAL_LT_GT" > "HOL4Real.realax.HREAL_LT_GT" |
|
119 "HREAL_LT_ADDR" > "HOL4Real.realax.HREAL_LT_ADDR" |
|
120 "HREAL_LT_ADDL" > "HOL4Real.realax.HREAL_LT_ADDL" |
|
121 "HREAL_LT_ADD2" > "HOL4Real.realax.HREAL_LT_ADD2" |
|
122 "HREAL_EQ_LADD" > "HOL4Real.realax.HREAL_EQ_LADD" |
|
123 "HREAL_EQ_ADDR" > "HOL4Base.hreal.HREAL_NOZERO" |
|
124 "HREAL_EQ_ADDL" > "HOL4Real.realax.HREAL_EQ_ADDL" |
|
125 |
|
126 ignore_thms |
|
127 "real_tybij" |
|
128 "real_of_hreal" |
|
129 "real_neg" |
|
130 "real_mul" |
|
131 "real_lt" |
|
132 "real_inv" |
|
133 "real_add" |
|
134 "real_TY_DEF" |
|
135 "real_1" |
|
136 "real_0" |
|
137 "hreal_of_real" |
|
138 "SUP_ALLPOS_LEMMA4" |
|
139 "SUP_ALLPOS_LEMMA3" |
|
140 "SUP_ALLPOS_LEMMA2" |
|
141 "SUP_ALLPOS_LEMMA1" |
|
142 "REAL_POS" |
|
143 "REAL_ISO_EQ" |
|
144 |
|
145 end |
|