author  avigad 
Tue, 12 Jul 2005 17:56:03 +0200  
changeset 16775  c1b87ef4a1c3 
parent 15647  b1f486a9c56b 
child 17188  a26a4fc323ed 
permissions  rwrr 
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" 

13 
"real_sub" > "op " :: "real => real => real" 

14 
"real_of_num" > "RealDef.real" :: "nat => real" 

15 
"real_lte" > "op <=" :: "real => real => bool" 

16 
"real_gt" > "HOL4Compat.real_gt" 

17 
"real_ge" > "HOL4Compat.real_ge" 

18 
"pow" > "Nat.power" :: "real => nat => real" 

19 
"abs" > "HOL.abs" :: "real => real" 

20 
"/" > "HOL.divide" :: "real => real => real" 

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" 

34 
"real_div" > "Ring_and_Field.field.divide_inverse" 

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" 

14516  90 
"REAL_SUB_ABS" > "HOL4Real.real.REAL_SUB_ABS" 
14796  91 
"REAL_SUB_0" > "OrderedGroup.eq_iff_diff_eq_0" 
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" 
96 
"REAL_POW_MONO_LT" > "Power.power_strict_increasing" 

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" 

102 
"REAL_POW2_ABS" > "NatBin.power2_abs" 

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" 
14516  117 
"REAL_NEG_RMUL" > "Ring_and_Field.minus_mult_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" 
14516  122 
"REAL_NEG_LMUL" > "Ring_and_Field.minus_mult_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" 

15647  132 
"REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_6" 
14516  133 
"REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right" 
134 
"REAL_MUL_RNEG" > "Ring_and_Field.minus_mult_right" 

135 
"REAL_MUL_RINV" > "Ring_and_Field.right_inverse" 

14796  136 
"REAL_MUL_RID" > "OrderedGroup.monoid_mult.mult_1_right" 
14516  137 
"REAL_MUL_LZERO" > "Ring_and_Field.mult_zero_left" 
138 
"REAL_MUL_LNEG" > "Ring_and_Field.minus_mult_left" 

139 
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" 

14796  140 
"REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1" 
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" 

150 
"REAL_LT_RMUL_IMP" > "Ring_and_Field.ordered_semiring_strict.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" 
14796  164 
"REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict.mult_strict_mono" 
14516  165 
"REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0" 
166 
"REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL" 

15647  167 
"REAL_LT_LE" > "Orderings.order.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" 

180 
"REAL_LT_DIV" > "HOL4Real.real.REAL_LT_DIV" 

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" 
189 
"REAL_LT_ADD" > "RealDef.real_add_order" 

190 
"REAL_LT_1" > "HOL4Real.real.REAL_LT_1" 

14796  191 
"REAL_LT_01" > "Ring_and_Field.ordered_semidom.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" 
14516  196 
"REAL_LTE_ADD" > "HOL4Real.real.REAL_LTE_ADD" 
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" 

15647  202 
"REAL_LE_TOTAL" > "Orderings.linorder.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" 
207 
"REAL_LE_RMUL_IMP" > "Ring_and_Field.pordered_semiring.mult_right_mono" 

14516  208 
"REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1" 
15647  209 
"REAL_LE_REFL" > "Orderings.order.order_refl" 
14516  210 
"REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq" 
211 
"REAL_LE_RDIV" > "HOL4Real.real.REAL_LE_RDIV" 

14796  212 
"REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right" 
15647  213 
"REAL_LE_POW2" > "NatBin.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" 
14796  223 
"REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.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" 

226 
"REAL_LE_LDIV" > "HOL4Real.real.REAL_LE_LDIV" 

14796  227 
"REAL_LE_LADD_IMP" > "OrderedGroup.pordered_ab_semigroup_add.add_left_mono" 
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" 
14516  237 
"REAL_LE_ADD" > "RealDef.real_le_add_order" 
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" 
14516  243 
"REAL_LET_ADD" > "HOL4Real.real.REAL_LET_ADD" 
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" 

254 
"REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero" 

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" 

277 
"REAL_DOUBLE" > "IntArith.mult_2" 

278 
"REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL" 

279 
"REAL_DIV_REFL" > "Ring_and_Field.divide_self" 

280 
"REAL_DIV_MUL2" > "Ring_and_Field.nonzero_mult_divide_cancel_left" 

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" 

14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

286 
"REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9" 
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" 
14796  291 
"REAL_ADD_RID" > "OrderedGroup.add_0_right" 
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" 

14796  295 
"REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0" 
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" 
14796  303 
"REAL_ABS_0" > "OrderedGroup.abs_zero" 
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" 

316 
"POW_MINUS1" > "NatBin.power_minus1_even" 

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" 

326 
"POW_2" > "NatBin.power2_eq_square" 

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" 
332 
"ABS_SUB_ABS" > "HOL4Real.real.ABS_SUB_ABS" 

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" 

338 
"ABS_POW2" > "NatBin.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" 
14516  356 
"ABS_1" > "Ring_and_Field.abs_one" 
14796  357 
"ABS_0" > "OrderedGroup.abs_zero" 
14516  358 

359 
end 