| author | haftmann |
| Fri, 05 Feb 2010 14:33:50 +0100 | |
| changeset 35028 | 108662d50512 |
| parent 34974 | 18b41bba42b5 |
| child 35050 | 9f841f20dca6 |
| permissions | -rw-r--r-- |
| 14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
def_maps |
|
6 |
"sup" > "sup_def" |
|
7 |
"sumc" > "sumc_def" |
|
8 |
"sum" > "sum_def" |
|
9 |
||
10 |
const_maps |
|
11 |
"sup" > "HOL4Real.real.sup" |
|
12 |
"sum" > "HOL4Real.real.sum" |
|
|
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
30925
diff
changeset
|
13 |
"real_sub" > "Algebras.minus" :: "real => real => real" |
| 14516 | 14 |
"real_of_num" > "RealDef.real" :: "nat => real" |
|
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
30925
diff
changeset
|
15 |
"real_lte" > "Algebras.less_eq" :: "real => real => bool" |
| 14516 | 16 |
"real_gt" > "HOL4Compat.real_gt" |
17 |
"real_ge" > "HOL4Compat.real_ge" |
|
| 24996 | 18 |
"pow" > "Power.power_class.power" :: "real => nat => real" |
|
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
30925
diff
changeset
|
19 |
"abs" > "Algebras.abs" :: "real => real" |
|
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
30925
diff
changeset
|
20 |
"/" > "Algebras.divide" :: "real => real => real" |
| 14516 | 21 |
|
22 |
thm_maps |
|
23 |
"sup_def" > "HOL4Real.real.sup_def" |
|
24 |
"sup" > "HOL4Real.real.sup" |
|
25 |
"sumc" > "HOL4Real.real.sumc" |
|
26 |
"sum_def" > "HOL4Real.real.sum_def" |
|
27 |
"sum" > "HOL4Real.real.sum" |
|
| 14847 | 28 |
"real_sub" > "OrderedGroup.diff_def" |
| 14516 | 29 |
"real_of_num" > "HOL4Compat.real_of_num" |
30 |
"real_lte" > "HOL4Compat.real_lte" |
|
| 15647 | 31 |
"real_lt" > "Orderings.linorder_not_le" |
| 14516 | 32 |
"real_gt" > "HOL4Compat.real_gt" |
33 |
"real_ge" > "HOL4Compat.real_ge" |
|
| 17644 | 34 |
"real_div" > "Ring_and_Field.field_class.divide_inverse" |
| 14516 | 35 |
"pow" > "HOL4Compat.pow" |
36 |
"abs" > "HOL4Compat.abs" |
|
37 |
"SUP_LEMMA3" > "HOL4Real.real.SUP_LEMMA3" |
|
38 |
"SUP_LEMMA2" > "HOL4Real.real.SUP_LEMMA2" |
|
39 |
"SUP_LEMMA1" > "HOL4Real.real.SUP_LEMMA1" |
|
40 |
"SUM_ZERO" > "HOL4Real.real.SUM_ZERO" |
|
41 |
"SUM_TWO" > "HOL4Real.real.SUM_TWO" |
|
42 |
"SUM_SUBST" > "HOL4Real.real.SUM_SUBST" |
|
43 |
"SUM_SUB" > "HOL4Real.real.SUM_SUB" |
|
44 |
"SUM_REINDEX" > "HOL4Real.real.SUM_REINDEX" |
|
45 |
"SUM_POS_GEN" > "HOL4Real.real.SUM_POS_GEN" |
|
46 |
"SUM_POS" > "HOL4Real.real.SUM_POS" |
|
47 |
"SUM_PERMUTE_0" > "HOL4Real.real.SUM_PERMUTE_0" |
|
48 |
"SUM_OFFSET" > "HOL4Real.real.SUM_OFFSET" |
|
49 |
"SUM_NSUB" > "HOL4Real.real.SUM_NSUB" |
|
50 |
"SUM_NEG" > "HOL4Real.real.SUM_NEG" |
|
51 |
"SUM_LE" > "HOL4Real.real.SUM_LE" |
|
52 |
"SUM_GROUP" > "HOL4Real.real.SUM_GROUP" |
|
53 |
"SUM_EQ" > "HOL4Real.real.SUM_EQ" |
|
54 |
"SUM_DIFF" > "HOL4Real.real.SUM_DIFF" |
|
55 |
"SUM_DEF" > "HOL4Real.real.SUM_DEF" |
|
56 |
"SUM_CMUL" > "HOL4Real.real.SUM_CMUL" |
|
57 |
"SUM_CANCEL" > "HOL4Real.real.SUM_CANCEL" |
|
58 |
"SUM_BOUND" > "HOL4Real.real.SUM_BOUND" |
|
59 |
"SUM_ADD" > "HOL4Real.real.SUM_ADD" |
|
60 |
"SUM_ABS_LE" > "HOL4Real.real.SUM_ABS_LE" |
|
61 |
"SUM_ABS" > "HOL4Real.real.SUM_ABS" |
|
62 |
"SUM_2" > "HOL4Real.real.SUM_2" |
|
63 |
"SUM_1" > "HOL4Real.real.SUM_1" |
|
64 |
"SUM_0" > "HOL4Real.real.SUM_0" |
|
65 |
"SETOK_LE_LT" > "HOL4Real.real.SETOK_LE_LT" |
|
66 |
"REAL_SUP_UBOUND_LE" > "HOL4Real.real.REAL_SUP_UBOUND_LE" |
|
67 |
"REAL_SUP_UBOUND" > "HOL4Real.real.REAL_SUP_UBOUND" |
|
68 |
"REAL_SUP_SOMEPOS" > "HOL4Real.real.REAL_SUP_SOMEPOS" |
|
69 |
"REAL_SUP_LE" > "HOL4Real.real.REAL_SUP_LE" |
|
70 |
"REAL_SUP_EXISTS" > "HOL4Real.real.REAL_SUP_EXISTS" |
|
71 |
"REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS" |
|
72 |
"REAL_SUP" > "HOL4Real.real.REAL_SUP" |
|
73 |
"REAL_SUMSQ" > "HOL4Real.real.REAL_SUMSQ" |
|
74 |
"REAL_SUB_TRIANGLE" > "HOL4Real.real.REAL_SUB_TRIANGLE" |
|
75 |
"REAL_SUB_SUB2" > "HOL4Real.real.REAL_SUB_SUB2" |
|
76 |
"REAL_SUB_SUB" > "HOL4Real.real.REAL_SUB_SUB" |
|
| 14796 | 77 |
"REAL_SUB_RZERO" > "OrderedGroup.diff_0_right" |
78 |
"REAL_SUB_RNEG" > "OrderedGroup.diff_minus_eq_add" |
|
79 |
"REAL_SUB_REFL" > "OrderedGroup.diff_self" |
|
| 15647 | 80 |
"REAL_SUB_RDISTRIB" > "Ring_and_Field.ring_eq_simps_3" |
| 14516 | 81 |
"REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2" |
| 14796 | 82 |
"REAL_SUB_LZERO" > "OrderedGroup.diff_0" |
| 15647 | 83 |
"REAL_SUB_LT" > "HOL4Real.real.REAL_SUB_LT" |
| 14516 | 84 |
"REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG" |
| 15647 | 85 |
"REAL_SUB_LE" > "HOL4Real.real.REAL_SUB_LE" |
86 |
"REAL_SUB_LDISTRIB" > "Ring_and_Field.ring_eq_simps_4" |
|
| 14516 | 87 |
"REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2" |
| 14796 | 88 |
"REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2" |
89 |
"REAL_SUB_ADD" > "OrderedGroup.diff_add_cancel" |
|
| 17188 | 90 |
"REAL_SUB_ABS" > "OrderedGroup.abs_triangle_ineq2" |
91 |
"REAL_SUB_0" > "OrderedGroup.diff_eq_0_iff_eq" |
|
| 14516 | 92 |
"REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff" |
| 15647 | 93 |
"REAL_RINV_UNIQ" > "Ring_and_Field.inverse_unique" |
94 |
"REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_1" |
|
| 14516 | 95 |
"REAL_POW_POW" > "Power.power_mult" |
| 17188 | 96 |
"REAL_POW_MONO_LT" > "HOL4Real.real.REAL_POW_MONO_LT" |
| 14516 | 97 |
"REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2" |
98 |
"REAL_POW_LT" > "Power.zero_less_power" |
|
99 |
"REAL_POW_INV" > "Power.power_inverse" |
|
100 |
"REAL_POW_DIV" > "Power.power_divide" |
|
101 |
"REAL_POW_ADD" > "Power.power_add" |
|
| 30925 | 102 |
"REAL_POW2_ABS" > "Nat_Numeral.power2_abs" |
| 14516 | 103 |
"REAL_POS_NZ" > "HOL4Real.real.REAL_POS_NZ" |
104 |
"REAL_POS" > "RealDef.real_of_nat_ge_zero" |
|
105 |
"REAL_POASQ" > "HOL4Real.real.REAL_POASQ" |
|
106 |
"REAL_OVER1" > "Ring_and_Field.divide_1" |
|
107 |
"REAL_OF_NUM_SUC" > "RealDef.real_of_nat_Suc" |
|
108 |
"REAL_OF_NUM_POW" > "RealPow.realpow_real_of_nat" |
|
109 |
"REAL_OF_NUM_MUL" > "RealDef.real_of_nat_mult" |
|
110 |
"REAL_OF_NUM_LE" > "RealDef.real_of_nat_le_iff" |
|
111 |
"REAL_OF_NUM_EQ" > "RealDef.real_of_nat_inject" |
|
112 |
"REAL_OF_NUM_ADD" > "RealDef.real_of_nat_add" |
|
113 |
"REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT" |
|
114 |
"REAL_NOT_LT" > "HOL4Compat.real_lte" |
|
| 15647 | 115 |
"REAL_NOT_LE" > "Orderings.linorder_not_le" |
| 14796 | 116 |
"REAL_NEG_SUB" > "OrderedGroup.minus_diff_eq" |
| 17188 | 117 |
"REAL_NEG_RMUL" > "Ring_and_Field.mult_minus_right" |
| 14796 | 118 |
"REAL_NEG_NEG" > "OrderedGroup.minus_minus" |
| 14516 | 119 |
"REAL_NEG_MUL2" > "Ring_and_Field.minus_mult_minus" |
120 |
"REAL_NEG_MINUS1" > "HOL4Real.real.REAL_NEG_MINUS1" |
|
| 14796 | 121 |
"REAL_NEG_LT0" > "OrderedGroup.neg_less_0_iff_less" |
| 17188 | 122 |
"REAL_NEG_LMUL" > "Ring_and_Field.mult_minus_left" |
| 14796 | 123 |
"REAL_NEG_LE0" > "OrderedGroup.neg_le_0_iff_le" |
| 14516 | 124 |
"REAL_NEG_INV" > "Ring_and_Field.nonzero_inverse_minus_eq" |
| 14796 | 125 |
"REAL_NEG_GT0" > "OrderedGroup.neg_0_less_iff_less" |
126 |
"REAL_NEG_GE0" > "OrderedGroup.neg_0_le_iff_le" |
|
127 |
"REAL_NEG_EQ0" > "OrderedGroup.neg_equal_0_iff_equal" |
|
| 14516 | 128 |
"REAL_NEG_EQ" > "HOL4Real.real.REAL_NEG_EQ" |
| 14796 | 129 |
"REAL_NEG_ADD" > "OrderedGroup.minus_add_distrib" |
130 |
"REAL_NEG_0" > "OrderedGroup.minus_zero" |
|
131 |
"REAL_NEGNEG" > "OrderedGroup.minus_minus" |
|
| 25930 | 132 |
"REAL_MUL_SYM" > "Int.zmult_ac_2" |
| 14516 | 133 |
"REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right" |
| 17188 | 134 |
"REAL_MUL_RNEG" > "Ring_and_Field.mult_minus_right" |
| 14516 | 135 |
"REAL_MUL_RINV" > "Ring_and_Field.right_inverse" |
| 17188 | 136 |
"REAL_MUL_RID" > "Finite_Set.AC_mult.f_e.ident" |
| 14516 | 137 |
"REAL_MUL_LZERO" > "Ring_and_Field.mult_zero_left" |
| 17188 | 138 |
"REAL_MUL_LNEG" > "Ring_and_Field.mult_minus_left" |
| 14516 | 139 |
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" |
| 17188 | 140 |
"REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident" |
| 14516 | 141 |
"REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC" |
142 |
"REAL_MUL" > "RealDef.real_of_nat_mult" |
|
143 |
"REAL_MIDDLE2" > "HOL4Real.real.REAL_MIDDLE2" |
|
144 |
"REAL_MIDDLE1" > "HOL4Real.real.REAL_MIDDLE1" |
|
145 |
"REAL_MEAN" > "Ring_and_Field.dense" |
|
146 |
"REAL_LT_TRANS" > "Set.basic_trans_rules_21" |
|
147 |
"REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" |
|
| 14796 | 148 |
"REAL_LT_SUB_RADD" > "OrderedGroup.compare_rls_6" |
149 |
"REAL_LT_SUB_LADD" > "OrderedGroup.compare_rls_7" |
|
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
150 |
"REAL_LT_RMUL_IMP" > "Ring_and_Field.mult_strict_right_mono" |
| 14516 | 151 |
"REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0" |
152 |
"REAL_LT_RMUL" > "RealDef.real_mult_less_iff1" |
|
| 15647 | 153 |
"REAL_LT_REFL" > "Orderings.order_less_irrefl" |
| 14516 | 154 |
"REAL_LT_RDIV_EQ" > "Ring_and_Field.pos_less_divide_eq" |
155 |
"REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0" |
|
156 |
"REAL_LT_RDIV" > "HOL4Real.real.REAL_LT_RDIV" |
|
| 14796 | 157 |
"REAL_LT_RADD" > "OrderedGroup.add_less_cancel_right" |
| 14516 | 158 |
"REAL_LT_NZ" > "HOL4Real.real.REAL_LT_NZ" |
159 |
"REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL" |
|
| 14796 | 160 |
"REAL_LT_NEG" > "OrderedGroup.neg_less_iff_less" |
| 14516 | 161 |
"REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE" |
162 |
"REAL_LT_MUL2" > "Ring_and_Field.mult_strict_mono'" |
|
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
15647
diff
changeset
|
163 |
"REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos" |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
164 |
"REAL_LT_LMUL_IMP" > "Ring_and_Field.linordered_comm_semiring_strict_class.mult_strict_mono" |
| 14516 | 165 |
"REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0" |
166 |
"REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL" |
|
| 17644 | 167 |
"REAL_LT_LE" > "Orderings.order_class.order_less_le" |
| 14516 | 168 |
"REAL_LT_LDIV_EQ" > "Ring_and_Field.pos_divide_less_eq" |
| 14796 | 169 |
"REAL_LT_LADD" > "OrderedGroup.add_less_cancel_left" |
| 14516 | 170 |
"REAL_LT_INV_EQ" > "Ring_and_Field.inverse_positive_iff_positive" |
171 |
"REAL_LT_INV" > "Ring_and_Field.less_imp_inverse_less" |
|
| 15647 | 172 |
"REAL_LT_IMP_NE" > "Orderings.less_imp_neq" |
173 |
"REAL_LT_IMP_LE" > "Orderings.order_less_imp_le" |
|
| 14796 | 174 |
"REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono" |
| 14516 | 175 |
"REAL_LT_HALF2" > "HOL4Real.real.REAL_LT_HALF2" |
176 |
"REAL_LT_HALF1" > "NatSimprocs.half_gt_zero_iff" |
|
| 15647 | 177 |
"REAL_LT_GT" > "Orderings.order_less_not_sym" |
| 14516 | 178 |
"REAL_LT_FRACTION_0" > "HOL4Real.real.REAL_LT_FRACTION_0" |
179 |
"REAL_LT_FRACTION" > "HOL4Real.real.REAL_LT_FRACTION" |
|
| 17188 | 180 |
"REAL_LT_DIV" > "Ring_and_Field.divide_pos_pos" |
| 14516 | 181 |
"REAL_LT_ANTISYM" > "HOL4Real.real.REAL_LT_ANTISYM" |
| 14796 | 182 |
"REAL_LT_ADD_SUB" > "OrderedGroup.compare_rls_7" |
| 14516 | 183 |
"REAL_LT_ADDR" > "HOL4Real.real.REAL_LT_ADDR" |
184 |
"REAL_LT_ADDNEG2" > "HOL4Real.real.REAL_LT_ADDNEG2" |
|
185 |
"REAL_LT_ADDNEG" > "HOL4Real.real.REAL_LT_ADDNEG" |
|
186 |
"REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL" |
|
| 14796 | 187 |
"REAL_LT_ADD2" > "OrderedGroup.add_strict_mono" |
| 14516 | 188 |
"REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1" |
| 17188 | 189 |
"REAL_LT_ADD" > "OrderedGroup.add_pos_pos" |
| 14516 | 190 |
"REAL_LT_1" > "HOL4Real.real.REAL_LT_1" |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
191 |
"REAL_LT_01" > "Ring_and_Field.zero_less_one" |
| 14516 | 192 |
"REAL_LTE_TRANS" > "Set.basic_trans_rules_24" |
193 |
"REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL" |
|
194 |
"REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM" |
|
| 14796 | 195 |
"REAL_LTE_ADD2" > "OrderedGroup.add_less_le_mono" |
| 17188 | 196 |
"REAL_LTE_ADD" > "OrderedGroup.add_pos_nonneg" |
| 14516 | 197 |
"REAL_LT1_POW2" > "HOL4Real.real.REAL_LT1_POW2" |
198 |
"REAL_LT" > "RealDef.real_of_nat_less_iff" |
|
199 |
"REAL_LNEG_UNIQ" > "HOL4Real.real.REAL_LNEG_UNIQ" |
|
200 |
"REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ" |
|
201 |
"REAL_LE_TRANS" > "Set.basic_trans_rules_25" |
|
| 17644 | 202 |
"REAL_LE_TOTAL" > "Orderings.linorder_class.linorder_linear" |
| 14796 | 203 |
"REAL_LE_SUB_RADD" > "OrderedGroup.compare_rls_8" |
204 |
"REAL_LE_SUB_LADD" > "OrderedGroup.compare_rls_9" |
|
| 14516 | 205 |
"REAL_LE_SQUARE" > "Ring_and_Field.zero_le_square" |
| 14796 | 206 |
"REAL_LE_RNEG" > "OrderedGroup.le_eq_neg" |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
207 |
"REAL_LE_RMUL_IMP" > "Ring_and_Field.mult_right_mono" |
| 14516 | 208 |
"REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1" |
| 17188 | 209 |
"REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl" |
| 14516 | 210 |
"REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq" |
| 17188 | 211 |
"REAL_LE_RDIV" > "Ring_and_Field.mult_imp_le_div_pos" |
| 14796 | 212 |
"REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right" |
| 30925 | 213 |
"REAL_LE_POW2" > "Nat_Numeral.zero_compare_simps_12" |
| 14516 | 214 |
"REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL" |
| 14796 | 215 |
"REAL_LE_NEGR" > "OrderedGroup.le_minus_self_iff" |
216 |
"REAL_LE_NEGL" > "OrderedGroup.minus_le_self_iff" |
|
217 |
"REAL_LE_NEG2" > "OrderedGroup.neg_le_iff_le" |
|
218 |
"REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le" |
|
| 14516 | 219 |
"REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2" |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
15647
diff
changeset
|
220 |
"REAL_LE_MUL" > "Ring_and_Field.mult_nonneg_nonneg" |
| 15647 | 221 |
"REAL_LE_LT" > "Orderings.order_le_less" |
| 14516 | 222 |
"REAL_LE_LNEG" > "RealDef.real_0_le_add_iff" |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
223 |
"REAL_LE_LMUL_IMP" > "Ring_and_Field.mult_mono" |
| 14516 | 224 |
"REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2" |
225 |
"REAL_LE_LDIV_EQ" > "Ring_and_Field.pos_divide_le_eq" |
|
| 17188 | 226 |
"REAL_LE_LDIV" > "Ring_and_Field.mult_imp_div_pos_le" |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
227 |
"REAL_LE_LADD_IMP" > "OrderedGroup.add_left_mono" |
| 14796 | 228 |
"REAL_LE_LADD" > "OrderedGroup.add_le_cancel_left" |
| 14516 | 229 |
"REAL_LE_INV_EQ" > "Ring_and_Field.inverse_nonnegative_iff_nonnegative" |
230 |
"REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV" |
|
| 14796 | 231 |
"REAL_LE_DOUBLE" > "OrderedGroup.zero_le_double_add_iff_zero_le_single_add" |
| 14516 | 232 |
"REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV" |
| 15647 | 233 |
"REAL_LE_ANTISYM" > "Orderings.order_eq_iff" |
| 14516 | 234 |
"REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR" |
235 |
"REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL" |
|
| 14796 | 236 |
"REAL_LE_ADD2" > "OrderedGroup.add_mono" |
| 17188 | 237 |
"REAL_LE_ADD" > "OrderedGroup.add_nonneg_nonneg" |
| 14516 | 238 |
"REAL_LE_01" > "Ring_and_Field.zero_le_one" |
239 |
"REAL_LET_TRANS" > "Set.basic_trans_rules_23" |
|
| 15647 | 240 |
"REAL_LET_TOTAL" > "Orderings.linorder_le_less_linear" |
| 14516 | 241 |
"REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM" |
| 14796 | 242 |
"REAL_LET_ADD2" > "OrderedGroup.add_le_less_mono" |
| 17188 | 243 |
"REAL_LET_ADD" > "OrderedGroup.add_nonneg_pos" |
| 14516 | 244 |
"REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2" |
245 |
"REAL_LE" > "RealDef.real_of_nat_le_iff" |
|
| 15647 | 246 |
"REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2" |
| 14516 | 247 |
"REAL_INV_POS" > "Ring_and_Field.positive_imp_inverse_positive" |
248 |
"REAL_INV_NZ" > "Ring_and_Field.nonzero_imp_inverse_nonzero" |
|
249 |
"REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL" |
|
250 |
"REAL_INV_LT1" > "RealDef.real_inverse_gt_one" |
|
251 |
"REAL_INV_INV" > "Ring_and_Field.inverse_inverse_eq" |
|
252 |
"REAL_INV_EQ_0" > "Ring_and_Field.inverse_nonzero_iff_nonzero" |
|
253 |
"REAL_INV_1OVER" > "Ring_and_Field.inverse_eq_divide" |
|
| 17644 | 254 |
"REAL_INV_0" > "Ring_and_Field.division_by_zero_class.inverse_zero" |
| 14516 | 255 |
"REAL_INVINV" > "Ring_and_Field.nonzero_inverse_inverse_eq" |
256 |
"REAL_INV1" > "Ring_and_Field.inverse_1" |
|
257 |
"REAL_INJ" > "RealDef.real_of_nat_inject" |
|
258 |
"REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves" |
|
259 |
"REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ" |
|
|
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
260 |
"REAL_EQ_SUB_RADD" > "Ring_and_Field.ring_eq_simps_15" |
|
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
261 |
"REAL_EQ_SUB_LADD" > "Ring_and_Field.ring_eq_simps_16" |
| 14516 | 262 |
"REAL_EQ_RMUL_IMP" > "Ring_and_Field.field_mult_cancel_right_lemma" |
263 |
"REAL_EQ_RMUL" > "Ring_and_Field.field_mult_cancel_right" |
|
264 |
"REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ" |
|
| 14796 | 265 |
"REAL_EQ_RADD" > "OrderedGroup.add_right_cancel" |
266 |
"REAL_EQ_NEG" > "OrderedGroup.neg_equal_iff_equal" |
|
| 14516 | 267 |
"REAL_EQ_MUL_LCANCEL" > "Ring_and_Field.field_mult_cancel_left" |
268 |
"REAL_EQ_LMUL_IMP" > "HOL4Real.real.REAL_EQ_LMUL_IMP" |
|
269 |
"REAL_EQ_LMUL2" > "RealDef.real_mult_left_cancel" |
|
270 |
"REAL_EQ_LMUL" > "Ring_and_Field.field_mult_cancel_left" |
|
271 |
"REAL_EQ_LDIV_EQ" > "HOL4Real.real.REAL_EQ_LDIV_EQ" |
|
| 14796 | 272 |
"REAL_EQ_LADD" > "OrderedGroup.add_left_cancel" |
| 15647 | 273 |
"REAL_EQ_IMP_LE" > "Orderings.order_eq_refl" |
| 14516 | 274 |
"REAL_ENTIRE" > "Ring_and_Field.field_mult_eq_0_iff" |
275 |
"REAL_DOWN2" > "RealDef.real_lbound_gt_zero" |
|
276 |
"REAL_DOWN" > "HOL4Real.real.REAL_DOWN" |
|
| 25930 | 277 |
"REAL_DOUBLE" > "Int.mult_2" |
| 14516 | 278 |
"REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL" |
279 |
"REAL_DIV_REFL" > "Ring_and_Field.divide_self" |
|
| 17188 | 280 |
"REAL_DIV_MUL2" > "HOL4Real.real.REAL_DIV_MUL2" |
| 14516 | 281 |
"REAL_DIV_LZERO" > "Ring_and_Field.divide_zero_left" |
282 |
"REAL_DIV_LMUL" > "HOL4Real.real.REAL_DIV_LMUL" |
|
283 |
"REAL_DIFFSQ" > "HOL4Real.real.REAL_DIFFSQ" |
|
284 |
"REAL_ARCH_LEAST" > "HOL4Real.real.REAL_ARCH_LEAST" |
|
285 |
"REAL_ARCH" > "RComplete.reals_Archimedean3" |
|
| 17188 | 286 |
"REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2" |
| 14516 | 287 |
"REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2" |
| 14796 | 288 |
"REAL_ADD_SUB" > "HOL4Real.real.REAL_ADD_SUB" |
289 |
"REAL_ADD_RINV" > "OrderedGroup.right_minus" |
|
| 14516 | 290 |
"REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ" |
| 17188 | 291 |
"REAL_ADD_RID" > "Finite_Set.AC_add.f_e.ident" |
| 15647 | 292 |
"REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_1" |
| 14516 | 293 |
"REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" |
294 |
"REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ" |
|
| 17188 | 295 |
"REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident" |
| 15647 | 296 |
"REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2" |
| 14516 | 297 |
"REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC" |
298 |
"REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2" |
|
299 |
"REAL_ADD" > "RealDef.real_of_nat_add" |
|
| 14796 | 300 |
"REAL_ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq" |
301 |
"REAL_ABS_POS" > "OrderedGroup.abs_ge_zero" |
|
| 14516 | 302 |
"REAL_ABS_MUL" > "Ring_and_Field.abs_mult" |
| 25930 | 303 |
"REAL_ABS_0" > "Int.bin_arith_simps_28" |
| 14516 | 304 |
"REAL_10" > "HOL4Compat.REAL_10" |
305 |
"REAL_1" > "HOL4Real.real.REAL_1" |
|
306 |
"REAL_0" > "HOL4Real.real.REAL_0" |
|
307 |
"REAL" > "RealDef.real_of_nat_Suc" |
|
308 |
"POW_ZERO_EQ" > "HOL4Real.real.POW_ZERO_EQ" |
|
309 |
"POW_ZERO" > "RealPow.realpow_zero_zero" |
|
310 |
"POW_POS_LT" > "HOL4Real.real.POW_POS_LT" |
|
311 |
"POW_POS" > "Power.zero_le_power" |
|
312 |
"POW_PLUS1" > "HOL4Real.real.POW_PLUS1" |
|
313 |
"POW_ONE" > "Power.power_one" |
|
314 |
"POW_NZ" > "Power.field_power_not_zero" |
|
315 |
"POW_MUL" > "Power.power_mult_distrib" |
|
| 30925 | 316 |
"POW_MINUS1" > "Nat_Numeral.power_minus1_even" |
| 14516 | 317 |
"POW_M1" > "HOL4Real.real.POW_M1" |
318 |
"POW_LT" > "HOL4Real.real.POW_LT" |
|
319 |
"POW_LE" > "Power.power_mono" |
|
320 |
"POW_INV" > "Power.nonzero_power_inverse" |
|
321 |
"POW_EQ" > "Power.power_inject_base" |
|
322 |
"POW_ADD" > "Power.power_add" |
|
323 |
"POW_ABS" > "Power.power_abs" |
|
324 |
"POW_2_LT" > "RealPow.two_realpow_gt" |
|
325 |
"POW_2_LE1" > "RealPow.two_realpow_ge_one" |
|
| 30925 | 326 |
"POW_2" > "Nat_Numeral.power2_eq_square" |
| 14516 | 327 |
"POW_1" > "Power.power_one_right" |
328 |
"POW_0" > "Power.power_0_Suc" |
|
| 14796 | 329 |
"ABS_ZERO" > "OrderedGroup.abs_eq_0" |
330 |
"ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq" |
|
| 14516 | 331 |
"ABS_SUM" > "HOL4Real.real.ABS_SUM" |
| 17188 | 332 |
"ABS_SUB_ABS" > "OrderedGroup.abs_triangle_ineq3" |
| 15647 | 333 |
"ABS_SUB" > "OrderedGroup.abs_minus_commute" |
| 14516 | 334 |
"ABS_STILLNZ" > "HOL4Real.real.ABS_STILLNZ" |
335 |
"ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2" |
|
336 |
"ABS_SIGN" > "HOL4Real.real.ABS_SIGN" |
|
337 |
"ABS_REFL" > "HOL4Real.real.ABS_REFL" |
|
| 30925 | 338 |
"ABS_POW2" > "Nat_Numeral.abs_power2" |
| 14796 | 339 |
"ABS_POS" > "OrderedGroup.abs_ge_zero" |
340 |
"ABS_NZ" > "OrderedGroup.zero_less_abs_iff" |
|
341 |
"ABS_NEG" > "OrderedGroup.abs_minus_cancel" |
|
| 14516 | 342 |
"ABS_N" > "RealDef.abs_real_of_nat_cancel" |
343 |
"ABS_MUL" > "Ring_and_Field.abs_mult" |
|
344 |
"ABS_LT_MUL2" > "HOL4Real.real.ABS_LT_MUL2" |
|
| 14796 | 345 |
"ABS_LE" > "OrderedGroup.abs_ge_self" |
| 14516 | 346 |
"ABS_INV" > "Ring_and_Field.nonzero_abs_inverse" |
347 |
"ABS_DIV" > "Ring_and_Field.nonzero_abs_divide" |
|
348 |
"ABS_CIRCLE" > "HOL4Real.real.ABS_CIRCLE" |
|
349 |
"ABS_CASES" > "HOL4Real.real.ABS_CASES" |
|
350 |
"ABS_BOUNDS" > "RealDef.abs_le_interval_iff" |
|
351 |
"ABS_BOUND" > "HOL4Real.real.ABS_BOUND" |
|
352 |
"ABS_BETWEEN2" > "HOL4Real.real.ABS_BETWEEN2" |
|
353 |
"ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1" |
|
354 |
"ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN" |
|
| 14796 | 355 |
"ABS_ABS" > "OrderedGroup.abs_idempotent" |
| 25930 | 356 |
"ABS_1" > "Int.bin_arith_simps_29" |
357 |
"ABS_0" > "Int.bin_arith_simps_28" |
|
| 14516 | 358 |
|
359 |
end |