| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Wed, 07 Sep 2011 07:59:45 +0900 | |
| changeset 44763 | b50d5d694838 |
| parent 36349 | 39be26d1bc28 |
| permissions | -rw-r--r-- |
| 14516 | 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" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
30 |
"real_sub" > "Groups.minus_class.minus" :: "real => real => real" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
31 |
"real_neg" > "Groups.uminus_class.uminus" :: "real => real" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
32 |
"real_mul" > "Groups.times_class.times" :: "real => real => real" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
33 |
"real_lt" > "Orderings.ord_class.less" :: "real => real => bool" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
34 |
"real_div" > "Fields.inverse_class.divide" :: "real => real => real" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
35 |
"real_add" > "Groups.plus_class.plus" :: "real => real => real" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
36 |
"real_1" > "Groups.one_class.one" :: "real" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
37 |
"real_0" > "Groups.zero_class.zero" :: "real" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
38 |
"mk_real" > "HOL.undefined" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
39 |
"inv" > "Fields.inverse_class.inverse" :: "real => real" |
| 14516 | 40 |
"hreal_of_treal" > "HOL4Real.realax.hreal_of_treal" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
41 |
"dest_real" > "HOL.undefined" |
| 14516 | 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" > "HOL4Compat.REAL_SUP_ALLPOS" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
98 |
"REAL_MUL_SYM" > "Fields.linordered_field_class.sign_simps_21" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
99 |
"REAL_MUL_LINV" > "Fields.division_ring_class.left_inverse" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
100 |
"REAL_MUL_LID" > "Divides.arithmetic_simps_42" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
101 |
"REAL_MUL_ASSOC" > "Fields.linordered_field_class.sign_simps_22" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
102 |
"REAL_LT_TRANS" > "Orderings.order_less_trans" |
| 14516 | 103 |
"REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" |
| 15647 | 104 |
"REAL_LT_REFL" > "Orderings.order_less_irrefl" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
105 |
"REAL_LT_MUL" > "RealDef.real_mult_order" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
106 |
"REAL_LT_IADD" > "Groups.ordered_cancel_ab_semigroup_add_class.add_strict_left_mono" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
107 |
"REAL_LDISTRIB" > "Fields.linordered_field_class.sign_simps_7" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
108 |
"REAL_INV_0" > "Fields.division_ring_inverse_zero_class.inverse_zero" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
109 |
"REAL_ADD_SYM" > "Fields.linordered_field_class.sign_simps_18" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
110 |
"REAL_ADD_LINV" > "Groups.ab_group_add_class.ab_left_minus" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
111 |
"REAL_ADD_LID" > "Divides.arithmetic_simps_38" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36349
diff
changeset
|
112 |
"REAL_ADD_ASSOC" > "Fields.linordered_field_class.sign_simps_19" |
| 14516 | 113 |
"REAL_10" > "HOL4Compat.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 |