| author | haftmann |
| Wed, 22 Apr 2009 19:09:19 +0200 | |
| changeset 30959 | 458e55fd0a33 |
| parent 25930 | 83e3dd60affe |
| child 34974 | 18b41bba42b5 |
| 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" |
|
| 25762 | 30 |
"real_neg" > "HOL.uminus_class.uminus" :: "real => real" |
| 22997 | 31 |
"real_mul" > "HOL.times_class.times" :: "real => real => real" |
| 23881 | 32 |
"real_lt" > "HOL.ord_class.less" :: "real => real => bool" |
| 22997 | 33 |
"real_add" > "HOL.plus_class.plus" :: "real => real => real" |
34 |
"real_1" > "HOL.one_class.one" :: "real" |
|
35 |
"real_0" > "HOL.zero_class.zero" :: "real" |
|
36 |
"inv" > "HOL.divide_class.inverse" :: "real => real" |
|
| 14516 | 37 |
"hreal_of_treal" > "HOL4Real.realax.hreal_of_treal" |
38 |
||
39 |
thm_maps |
|
40 |
"treal_of_hreal_def" > "HOL4Real.realax.treal_of_hreal_def" |
|
41 |
"treal_of_hreal" > "HOL4Real.realax.treal_of_hreal" |
|
42 |
"treal_neg_def" > "HOL4Real.realax.treal_neg_def" |
|
43 |
"treal_neg" > "HOL4Real.realax.treal_neg" |
|
44 |
"treal_mul_def" > "HOL4Real.realax.treal_mul_def" |
|
45 |
"treal_mul" > "HOL4Real.realax.treal_mul" |
|
46 |
"treal_lt_def" > "HOL4Real.realax.treal_lt_def" |
|
47 |
"treal_lt" > "HOL4Real.realax.treal_lt" |
|
48 |
"treal_inv_def" > "HOL4Real.realax.treal_inv_def" |
|
49 |
"treal_inv" > "HOL4Real.realax.treal_inv" |
|
50 |
"treal_eq_def" > "HOL4Real.realax.treal_eq_def" |
|
51 |
"treal_eq" > "HOL4Real.realax.treal_eq" |
|
52 |
"treal_add_def" > "HOL4Real.realax.treal_add_def" |
|
53 |
"treal_add" > "HOL4Real.realax.treal_add" |
|
54 |
"treal_1_def" > "HOL4Real.realax.treal_1_def" |
|
55 |
"treal_1" > "HOL4Real.realax.treal_1" |
|
56 |
"treal_0_def" > "HOL4Real.realax.treal_0_def" |
|
57 |
"treal_0" > "HOL4Real.realax.treal_0" |
|
58 |
"hreal_of_treal_def" > "HOL4Real.realax.hreal_of_treal_def" |
|
59 |
"hreal_of_treal" > "HOL4Real.realax.hreal_of_treal" |
|
60 |
"TREAL_NEG_WELLDEF" > "HOL4Real.realax.TREAL_NEG_WELLDEF" |
|
61 |
"TREAL_MUL_WELLDEFR" > "HOL4Real.realax.TREAL_MUL_WELLDEFR" |
|
62 |
"TREAL_MUL_WELLDEF" > "HOL4Real.realax.TREAL_MUL_WELLDEF" |
|
63 |
"TREAL_MUL_SYM" > "HOL4Real.realax.TREAL_MUL_SYM" |
|
64 |
"TREAL_MUL_LINV" > "HOL4Real.realax.TREAL_MUL_LINV" |
|
65 |
"TREAL_MUL_LID" > "HOL4Real.realax.TREAL_MUL_LID" |
|
66 |
"TREAL_MUL_ASSOC" > "HOL4Real.realax.TREAL_MUL_ASSOC" |
|
67 |
"TREAL_LT_WELLDEFR" > "HOL4Real.realax.TREAL_LT_WELLDEFR" |
|
68 |
"TREAL_LT_WELLDEFL" > "HOL4Real.realax.TREAL_LT_WELLDEFL" |
|
69 |
"TREAL_LT_WELLDEF" > "HOL4Real.realax.TREAL_LT_WELLDEF" |
|
70 |
"TREAL_LT_TRANS" > "HOL4Real.realax.TREAL_LT_TRANS" |
|
71 |
"TREAL_LT_TOTAL" > "HOL4Real.realax.TREAL_LT_TOTAL" |
|
72 |
"TREAL_LT_REFL" > "HOL4Real.realax.TREAL_LT_REFL" |
|
73 |
"TREAL_LT_MUL" > "HOL4Real.realax.TREAL_LT_MUL" |
|
74 |
"TREAL_LT_ADD" > "HOL4Real.realax.TREAL_LT_ADD" |
|
75 |
"TREAL_LDISTRIB" > "HOL4Real.realax.TREAL_LDISTRIB" |
|
76 |
"TREAL_ISO" > "HOL4Real.realax.TREAL_ISO" |
|
77 |
"TREAL_INV_WELLDEF" > "HOL4Real.realax.TREAL_INV_WELLDEF" |
|
78 |
"TREAL_INV_0" > "HOL4Real.realax.TREAL_INV_0" |
|
79 |
"TREAL_EQ_TRANS" > "HOL4Real.realax.TREAL_EQ_TRANS" |
|
80 |
"TREAL_EQ_SYM" > "HOL4Real.realax.TREAL_EQ_SYM" |
|
81 |
"TREAL_EQ_REFL" > "HOL4Real.realax.TREAL_EQ_REFL" |
|
82 |
"TREAL_EQ_EQUIV" > "HOL4Real.realax.TREAL_EQ_EQUIV" |
|
83 |
"TREAL_EQ_AP" > "HOL4Real.realax.TREAL_EQ_AP" |
|
84 |
"TREAL_BIJ_WELLDEF" > "HOL4Real.realax.TREAL_BIJ_WELLDEF" |
|
85 |
"TREAL_BIJ" > "HOL4Real.realax.TREAL_BIJ" |
|
86 |
"TREAL_ADD_WELLDEFR" > "HOL4Real.realax.TREAL_ADD_WELLDEFR" |
|
87 |
"TREAL_ADD_WELLDEF" > "HOL4Real.realax.TREAL_ADD_WELLDEF" |
|
88 |
"TREAL_ADD_SYM" > "HOL4Real.realax.TREAL_ADD_SYM" |
|
89 |
"TREAL_ADD_LINV" > "HOL4Real.realax.TREAL_ADD_LINV" |
|
90 |
"TREAL_ADD_LID" > "HOL4Real.realax.TREAL_ADD_LID" |
|
91 |
"TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC" |
|
92 |
"TREAL_10" > "HOL4Real.realax.TREAL_10" |
|
93 |
"REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS" |
|
| 25930 | 94 |
"REAL_MUL_SYM" > "Int.zmult_ac_2" |
| 14516 | 95 |
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" |
| 17188 | 96 |
"REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident" |
| 14516 | 97 |
"REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC" |
98 |
"REAL_LT_TRANS" > "Set.basic_trans_rules_21" |
|
99 |
"REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" |
|
| 15647 | 100 |
"REAL_LT_REFL" > "Orderings.order_less_irrefl" |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
15647
diff
changeset
|
101 |
"REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos" |
| 14796 | 102 |
"REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono" |
| 15647 | 103 |
"REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2" |
| 17644 | 104 |
"REAL_INV_0" > "Ring_and_Field.division_by_zero_class.inverse_zero" |
| 17188 | 105 |
"REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2" |
| 14516 | 106 |
"REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" |
| 17188 | 107 |
"REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident" |
| 14516 | 108 |
"REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" |
109 |
"REAL_10" > "HOL4Compat.REAL_10" |
|
110 |
"HREAL_RDISTRIB" > "HOL4Real.realax.HREAL_RDISTRIB" |
|
111 |
"HREAL_LT_REFL" > "HOL4Real.realax.HREAL_LT_REFL" |
|
112 |
"HREAL_LT_NE" > "HOL4Real.realax.HREAL_LT_NE" |
|
113 |
"HREAL_LT_LADD" > "HOL4Real.realax.HREAL_LT_LADD" |
|
114 |
"HREAL_LT_GT" > "HOL4Real.realax.HREAL_LT_GT" |
|
115 |
"HREAL_LT_ADDR" > "HOL4Real.realax.HREAL_LT_ADDR" |
|
116 |
"HREAL_LT_ADDL" > "HOL4Real.realax.HREAL_LT_ADDL" |
|
117 |
"HREAL_LT_ADD2" > "HOL4Real.realax.HREAL_LT_ADD2" |
|
118 |
"HREAL_EQ_LADD" > "HOL4Real.realax.HREAL_EQ_LADD" |
|
119 |
"HREAL_EQ_ADDR" > "HOL4Base.hreal.HREAL_NOZERO" |
|
120 |
"HREAL_EQ_ADDL" > "HOL4Real.realax.HREAL_EQ_ADDL" |
|
121 |
||
122 |
ignore_thms |
|
123 |
"real_tybij" |
|
124 |
"real_of_hreal" |
|
125 |
"real_neg" |
|
126 |
"real_mul" |
|
127 |
"real_lt" |
|
128 |
"real_inv" |
|
129 |
"real_add" |
|
130 |
"real_TY_DEF" |
|
131 |
"real_1" |
|
132 |
"real_0" |
|
133 |
"hreal_of_real" |
|
134 |
"SUP_ALLPOS_LEMMA4" |
|
135 |
"SUP_ALLPOS_LEMMA3" |
|
136 |
"SUP_ALLPOS_LEMMA2" |
|
137 |
"SUP_ALLPOS_LEMMA1" |
|
138 |
"REAL_POS" |
|
139 |
"REAL_ISO_EQ" |
|
140 |
||
141 |
end |