--- a/src/HOL/Import/HOL/real.imp Wed Sep 07 00:08:09 2011 +0200
+++ b/src/HOL/Import/HOL/real.imp Wed Sep 07 07:59:45 2011 +0900
@@ -10,14 +10,14 @@
const_maps
"sup" > "HOL4Real.real.sup"
"sum" > "HOL4Real.real.sum"
- "real_sub" > "Groups.minus" :: "real => real => real"
+ "real_sub" > "Groups.minus_class.minus" :: "real => real => real"
"real_of_num" > "RealDef.real" :: "nat => real"
- "real_lte" > "Orderings.less_eq" :: "real => real => bool"
+ "real_lte" > "Orderings.ord_class.less_eq" :: "real => real => bool"
"real_gt" > "HOL4Compat.real_gt"
"real_ge" > "HOL4Compat.real_ge"
"pow" > "Power.power_class.power" :: "real => nat => real"
- "abs" > "Groups.abs" :: "real => real"
- "/" > "Ring.divide" :: "real => real => real"
+ "abs" > "Groups.abs_class.abs" :: "real => real"
+ "/" > "Fields.inverse_class.divide" :: "real => real => real"
thm_maps
"sup_def" > "HOL4Real.real.sup_def"
@@ -25,13 +25,13 @@
"sumc" > "HOL4Real.real.sumc"
"sum_def" > "HOL4Real.real.sum_def"
"sum" > "HOL4Real.real.sum"
- "real_sub" > "Groups.diff_minus"
+ "real_sub" > "Fields.linordered_field_class.sign_simps_16"
"real_of_num" > "HOL4Compat.real_of_num"
"real_lte" > "HOL4Compat.real_lte"
- "real_lt" > "Orderings.linorder_not_le"
- "real_gt" > "HOL4Compat.real_gt"
+ "real_lt" > "Orderings.linorder_class.not_le"
+ "real_gt" > "HOL4Compat.GREATER_DEF"
"real_ge" > "HOL4Compat.real_ge"
- "real_div" > "Ring.divide_inverse"
+ "real_div" > "Fields.division_ring_class.divide_inverse"
"pow" > "HOL4Compat.pow"
"abs" > "HOL4Compat.abs"
"SUP_LEMMA3" > "HOL4Real.real.SUP_LEMMA3"
@@ -70,40 +70,40 @@
"REAL_SUP_EXISTS" > "HOL4Real.real.REAL_SUP_EXISTS"
"REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
"REAL_SUP" > "HOL4Real.real.REAL_SUP"
- "REAL_SUMSQ" > "HOL4Real.real.REAL_SUMSQ"
+ "REAL_SUMSQ" > "Nat_Numeral.linordered_ring_strict_class.sum_squares_eq_zero_iff"
"REAL_SUB_TRIANGLE" > "HOL4Real.real.REAL_SUB_TRIANGLE"
"REAL_SUB_SUB2" > "HOL4Real.real.REAL_SUB_SUB2"
"REAL_SUB_SUB" > "HOL4Real.real.REAL_SUB_SUB"
- "REAL_SUB_RZERO" > "Groups.diff_0_right"
- "REAL_SUB_RNEG" > "Groups.diff_minus_eq_add"
- "REAL_SUB_REFL" > "Groups.diff_self"
- "REAL_SUB_RDISTRIB" > "Rings.ring_eq_simps_3"
+ "REAL_SUB_RZERO" > "Groups.group_add_class.diff_0_right"
+ "REAL_SUB_RNEG" > "Groups.group_add_class.diff_minus_eq_add"
+ "REAL_SUB_REFL" > "Groups.group_add_class.diff_self"
+ "REAL_SUB_RDISTRIB" > "Fields.linordered_field_class.sign_simps_5"
"REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2"
- "REAL_SUB_LZERO" > "Groups.diff_0"
+ "REAL_SUB_LZERO" > "Groups.group_add_class.diff_0"
"REAL_SUB_LT" > "HOL4Real.real.REAL_SUB_LT"
"REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG"
"REAL_SUB_LE" > "HOL4Real.real.REAL_SUB_LE"
- "REAL_SUB_LDISTRIB" > "Rings.ring_eq_simps_4"
+ "REAL_SUB_LDISTRIB" > "Fields.linordered_field_class.sign_simps_6"
"REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2"
"REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2"
- "REAL_SUB_ADD" > "Groups.diff_add_cancel"
- "REAL_SUB_ABS" > "Groups.abs_triangle_ineq2"
- "REAL_SUB_0" > "Groups.diff_eq_0_iff_eq"
- "REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff"
- "REAL_RINV_UNIQ" > "Rings.inverse_unique"
- "REAL_RDISTRIB" > "Rings.ring_eq_simps_1"
- "REAL_POW_POW" > "Power.power_mult"
+ "REAL_SUB_ADD" > "Groups.group_add_class.diff_add_cancel"
+ "REAL_SUB_ABS" > "Groups.ordered_ab_group_add_abs_class.abs_triangle_ineq2"
+ "REAL_SUB_0" > "Groups.ab_group_add_class.diff_eq_0_iff_eq"
+ "REAL_RNEG_UNIQ" > "Groups.group_add_class.add_eq_0_iff"
+ "REAL_RINV_UNIQ" > "Fields.division_ring_class.inverse_unique"
+ "REAL_RDISTRIB" > "Fields.linordered_field_class.sign_simps_8"
+ "REAL_POW_POW" > "Power.monoid_mult_class.power_mult"
"REAL_POW_MONO_LT" > "HOL4Real.real.REAL_POW_MONO_LT"
"REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2"
- "REAL_POW_LT" > "Power.zero_less_power"
+ "REAL_POW_LT" > "Power.linordered_semidom_class.zero_less_power"
"REAL_POW_INV" > "Power.power_inverse"
"REAL_POW_DIV" > "Power.power_divide"
- "REAL_POW_ADD" > "Power.power_add"
- "REAL_POW2_ABS" > "Nat_Numeral.power2_abs"
+ "REAL_POW_ADD" > "Power.monoid_mult_class.power_add"
+ "REAL_POW2_ABS" > "Nat_Numeral.linordered_idom_class.power2_abs"
"REAL_POS_NZ" > "HOL4Real.real.REAL_POS_NZ"
"REAL_POS" > "RealDef.real_of_nat_ge_zero"
"REAL_POASQ" > "HOL4Real.real.REAL_POASQ"
- "REAL_OVER1" > "Rings.divide_1"
+ "REAL_OVER1" > "Fields.division_ring_class.divide_1"
"REAL_OF_NUM_SUC" > "RealDef.real_of_nat_Suc"
"REAL_OF_NUM_POW" > "RealDef.power_real_of_nat"
"REAL_OF_NUM_MUL" > "RealDef.real_of_nat_mult"
@@ -112,239 +112,239 @@
"REAL_OF_NUM_ADD" > "RealDef.real_of_nat_add"
"REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT"
"REAL_NOT_LT" > "HOL4Compat.real_lte"
- "REAL_NOT_LE" > "Orderings.linorder_not_le"
- "REAL_NEG_SUB" > "Groups.minus_diff_eq"
- "REAL_NEG_RMUL" > "Rings.mult_minus_right"
- "REAL_NEG_NEG" > "Groups.minus_minus"
- "REAL_NEG_MUL2" > "Rings.minus_mult_minus"
- "REAL_NEG_MINUS1" > "HOL4Real.real.REAL_NEG_MINUS1"
- "REAL_NEG_LT0" > "Groups.neg_less_0_iff_less"
- "REAL_NEG_LMUL" > "Rings.mult_minus_left"
- "REAL_NEG_LE0" > "Groups.neg_le_0_iff_le"
- "REAL_NEG_INV" > "Rings.nonzero_inverse_minus_eq"
- "REAL_NEG_GT0" > "Groups.neg_0_less_iff_less"
- "REAL_NEG_GE0" > "Groups.neg_0_le_iff_le"
- "REAL_NEG_EQ0" > "Groups.neg_equal_0_iff_equal"
+ "REAL_NOT_LE" > "Orderings.linorder_class.not_le"
+ "REAL_NEG_SUB" > "Groups.ab_group_add_class.minus_diff_eq"
+ "REAL_NEG_RMUL" > "Int.int_arith_rules_14"
+ "REAL_NEG_NEG" > "Groups.group_add_class.minus_minus"
+ "REAL_NEG_MUL2" > "Rings.ring_class.minus_mult_minus"
+ "REAL_NEG_MINUS1" > "Semiring_Normalization.comm_ring_1_class.normalizing_ring_rules_1"
+ "REAL_NEG_LT0" > "Groups.ordered_ab_group_add_class.neg_less_0_iff_less"
+ "REAL_NEG_LMUL" > "Int.int_arith_rules_13"
+ "REAL_NEG_LE0" > "Groups.ordered_ab_group_add_class.neg_le_0_iff_le"
+ "REAL_NEG_INV" > "Fields.division_ring_class.nonzero_inverse_minus_eq"
+ "REAL_NEG_GT0" > "Groups.ordered_ab_group_add_class.neg_0_less_iff_less"
+ "REAL_NEG_GE0" > "Groups.ordered_ab_group_add_class.neg_0_le_iff_le"
+ "REAL_NEG_EQ0" > "Groups.group_add_class.neg_equal_0_iff_equal"
"REAL_NEG_EQ" > "HOL4Real.real.REAL_NEG_EQ"
- "REAL_NEG_ADD" > "Groups.minus_add_distrib"
- "REAL_NEG_0" > "Groups.minus_zero"
- "REAL_NEGNEG" > "Groups.minus_minus"
- "REAL_MUL_SYM" > "Int.zmult_ac_2"
- "REAL_MUL_RZERO" > "Rings.mult_zero_right"
- "REAL_MUL_RNEG" > "Rings.mult_minus_right"
- "REAL_MUL_RINV" > "Rings.right_inverse"
- "REAL_MUL_RID" > "Finite_Set.AC_mult.f_e.ident"
- "REAL_MUL_LZERO" > "Rings.mult_zero_left"
- "REAL_MUL_LNEG" > "Rings.mult_minus_left"
- "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
- "REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
- "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
+ "REAL_NEG_ADD" > "Groups.ab_group_add_class.minus_add_distrib"
+ "REAL_NEG_0" > "Groups.group_add_class.minus_zero"
+ "REAL_NEGNEG" > "Groups.group_add_class.minus_minus"
+ "REAL_MUL_SYM" > "Fields.linordered_field_class.sign_simps_21"
+ "REAL_MUL_RZERO" > "Divides.arithmetic_simps_41"
+ "REAL_MUL_RNEG" > "Int.int_arith_rules_14"
+ "REAL_MUL_RINV" > "Fields.division_ring_class.right_inverse"
+ "REAL_MUL_RID" > "Divides.arithmetic_simps_43"
+ "REAL_MUL_LZERO" > "Divides.arithmetic_simps_40"
+ "REAL_MUL_LNEG" > "Int.int_arith_rules_13"
+ "REAL_MUL_LINV" > "Fields.division_ring_class.left_inverse"
+ "REAL_MUL_LID" > "Divides.arithmetic_simps_42"
+ "REAL_MUL_ASSOC" > "Fields.linordered_field_class.sign_simps_22"
"REAL_MUL" > "RealDef.real_of_nat_mult"
"REAL_MIDDLE2" > "HOL4Real.real.REAL_MIDDLE2"
"REAL_MIDDLE1" > "HOL4Real.real.REAL_MIDDLE1"
- "REAL_MEAN" > "Rings.dense"
- "REAL_LT_TRANS" > "Set.basic_trans_rules_21"
+ "REAL_MEAN" > "Orderings.dense_linorder_class.dense"
+ "REAL_LT_TRANS" > "Orderings.order_less_trans"
"REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
- "REAL_LT_SUB_RADD" > "Groups.compare_rls_6"
- "REAL_LT_SUB_LADD" > "Groups.compare_rls_7"
- "REAL_LT_RMUL_IMP" > "Rings.mult_strict_right_mono"
+ "REAL_LT_SUB_RADD" > "Fields.linordered_field_class.sign_simps_4"
+ "REAL_LT_SUB_LADD" > "Fields.linordered_field_class.sign_simps_3"
+ "REAL_LT_RMUL_IMP" > "Rings.linordered_semiring_strict_class.mult_strict_right_mono"
"REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0"
"REAL_LT_RMUL" > "RealDef.real_mult_less_iff1"
"REAL_LT_REFL" > "Orderings.order_less_irrefl"
- "REAL_LT_RDIV_EQ" > "Rings.pos_less_divide_eq"
+ "REAL_LT_RDIV_EQ" > "Fields.linordered_field_class.pos_less_divide_eq"
"REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0"
"REAL_LT_RDIV" > "HOL4Real.real.REAL_LT_RDIV"
- "REAL_LT_RADD" > "Groups.add_less_cancel_right"
+ "REAL_LT_RADD" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_right"
"REAL_LT_NZ" > "HOL4Real.real.REAL_LT_NZ"
"REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL"
- "REAL_LT_NEG" > "Groups.neg_less_iff_less"
+ "REAL_LT_NEG" > "Groups.ordered_ab_group_add_class.neg_less_iff_less"
"REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE"
- "REAL_LT_MUL2" > "Rings.mult_strict_mono'"
- "REAL_LT_MUL" > "Rings.mult_pos_pos"
- "REAL_LT_LMUL_IMP" > "Rings.linordered_comm_semiring_strict_class.mult_strict_mono"
+ "REAL_LT_MUL2" > "Rings.linordered_semiring_strict_class.mult_strict_mono'"
+ "REAL_LT_MUL" > "RealDef.real_mult_order"
+ "REAL_LT_LMUL_IMP" > "RealDef.real_mult_less_mono2"
"REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0"
- "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL"
- "REAL_LT_LE" > "Orderings.order_class.order_less_le"
- "REAL_LT_LDIV_EQ" > "Rings.pos_divide_less_eq"
- "REAL_LT_LADD" > "Groups.add_less_cancel_left"
- "REAL_LT_INV_EQ" > "Rings.inverse_positive_iff_positive"
- "REAL_LT_INV" > "Rings.less_imp_inverse_less"
- "REAL_LT_IMP_NE" > "Orderings.less_imp_neq"
+ "REAL_LT_LMUL" > "Rings.linordered_ring_strict_class.mult_less_cancel_left_pos"
+ "REAL_LT_LE" > "Orderings.order_class.less_le"
+ "REAL_LT_LDIV_EQ" > "Fields.linordered_field_class.pos_divide_less_eq"
+ "REAL_LT_LADD" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_left"
+ "REAL_LT_INV_EQ" > "Fields.linordered_field_inverse_zero_class.inverse_positive_iff_positive"
+ "REAL_LT_INV" > "Fields.linordered_field_class.less_imp_inverse_less"
+ "REAL_LT_IMP_NE" > "Orderings.order_class.less_imp_neq"
"REAL_LT_IMP_LE" > "Orderings.order_less_imp_le"
- "REAL_LT_IADD" > "Groups.add_strict_left_mono"
+ "REAL_LT_IADD" > "Groups.ordered_cancel_ab_semigroup_add_class.add_strict_left_mono"
"REAL_LT_HALF2" > "HOL4Real.real.REAL_LT_HALF2"
- "REAL_LT_HALF1" > "NatSimprocs.half_gt_zero_iff"
+ "REAL_LT_HALF1" > "Int.half_gt_zero_iff"
"REAL_LT_GT" > "Orderings.order_less_not_sym"
"REAL_LT_FRACTION_0" > "HOL4Real.real.REAL_LT_FRACTION_0"
"REAL_LT_FRACTION" > "HOL4Real.real.REAL_LT_FRACTION"
- "REAL_LT_DIV" > "Rings.divide_pos_pos"
+ "REAL_LT_DIV" > "Fields.linordered_field_class.divide_pos_pos"
"REAL_LT_ANTISYM" > "HOL4Real.real.REAL_LT_ANTISYM"
- "REAL_LT_ADD_SUB" > "Groups.compare_rls_7"
+ "REAL_LT_ADD_SUB" > "Fields.linordered_field_class.sign_simps_3"
"REAL_LT_ADDR" > "HOL4Real.real.REAL_LT_ADDR"
"REAL_LT_ADDNEG2" > "HOL4Real.real.REAL_LT_ADDNEG2"
"REAL_LT_ADDNEG" > "HOL4Real.real.REAL_LT_ADDNEG"
"REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL"
- "REAL_LT_ADD2" > "Groups.add_strict_mono"
+ "REAL_LT_ADD2" > "Groups.add_mono_thms_linordered_field_5"
"REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1"
- "REAL_LT_ADD" > "Groups.add_pos_pos"
+ "REAL_LT_ADD" > "Groups.ordered_comm_monoid_add_class.add_pos_pos"
"REAL_LT_1" > "HOL4Real.real.REAL_LT_1"
- "REAL_LT_01" > "Rings.zero_less_one"
- "REAL_LTE_TRANS" > "Set.basic_trans_rules_24"
+ "REAL_LT_01" > "Rings.linordered_semidom_class.zero_less_one"
+ "REAL_LTE_TRANS" > "Orderings.order_less_le_trans"
"REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL"
"REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM"
- "REAL_LTE_ADD2" > "Groups.add_less_le_mono"
- "REAL_LTE_ADD" > "Groups.add_pos_nonneg"
+ "REAL_LTE_ADD2" > "Groups.add_mono_thms_linordered_field_3"
+ "REAL_LTE_ADD" > "Groups.ordered_comm_monoid_add_class.add_pos_nonneg"
"REAL_LT1_POW2" > "HOL4Real.real.REAL_LT1_POW2"
"REAL_LT" > "RealDef.real_of_nat_less_iff"
- "REAL_LNEG_UNIQ" > "HOL4Real.real.REAL_LNEG_UNIQ"
+ "REAL_LNEG_UNIQ" > "Groups.group_add_class.eq_neg_iff_add_eq_0"
"REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ"
- "REAL_LE_TRANS" > "Set.basic_trans_rules_25"
- "REAL_LE_TOTAL" > "Orderings.linorder_class.linorder_linear"
- "REAL_LE_SUB_RADD" > "Groups.compare_rls_8"
- "REAL_LE_SUB_LADD" > "Groups.compare_rls_9"
- "REAL_LE_SQUARE" > "Rings.zero_le_square"
- "REAL_LE_RNEG" > "Groups.le_eq_neg"
- "REAL_LE_RMUL_IMP" > "Rings.mult_right_mono"
+ "REAL_LE_TRANS" > "Orderings.order_trans_rules_23"
+ "REAL_LE_TOTAL" > "Orderings.linorder_class.linear"
+ "REAL_LE_SUB_RADD" > "Fields.linordered_field_class.sign_simps_2"
+ "REAL_LE_SUB_LADD" > "Fields.linordered_field_class.sign_simps_1"
+ "REAL_LE_SQUARE" > "Rings.linordered_ring_class.zero_le_square"
+ "REAL_LE_RNEG" > "HOL4Real.real.REAL_LE_RNEG"
+ "REAL_LE_RMUL_IMP" > "Rings.ordered_semiring_class.mult_right_mono"
"REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1"
- "REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl"
- "REAL_LE_RDIV_EQ" > "Rings.pos_le_divide_eq"
- "REAL_LE_RDIV" > "Rings.mult_imp_le_div_pos"
- "REAL_LE_RADD" > "Groups.add_le_cancel_right"
- "REAL_LE_POW2" > "Nat_Numeral.zero_compare_simps_12"
+ "REAL_LE_REFL" > "Orderings.preorder_class.order_refl"
+ "REAL_LE_RDIV_EQ" > "Fields.linordered_field_class.pos_le_divide_eq"
+ "REAL_LE_RDIV" > "Fields.linordered_field_class.mult_imp_le_div_pos"
+ "REAL_LE_RADD" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_right"
+ "REAL_LE_POW2" > "Nat_Numeral.linordered_idom_class.zero_le_power2"
"REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL"
- "REAL_LE_NEGR" > "Groups.le_minus_self_iff"
- "REAL_LE_NEGL" > "Groups.minus_le_self_iff"
- "REAL_LE_NEG2" > "Groups.neg_le_iff_le"
- "REAL_LE_NEG" > "Groups.neg_le_iff_le"
- "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2"
- "REAL_LE_MUL" > "Rings.mult_nonneg_nonneg"
- "REAL_LE_LT" > "Orderings.order_le_less"
+ "REAL_LE_NEGR" > "Groups.linordered_ab_group_add_class.le_minus_self_iff"
+ "REAL_LE_NEGL" > "Groups.linordered_ab_group_add_class.minus_le_self_iff"
+ "REAL_LE_NEG2" > "Groups.ordered_ab_group_add_class.neg_le_iff_le"
+ "REAL_LE_NEG" > "Groups.ordered_ab_group_add_class.neg_le_iff_le"
+ "REAL_LE_MUL2" > "Rings.ordered_semiring_class.mult_mono'"
+ "REAL_LE_MUL" > "Rings.mult_sign_intros_1"
+ "REAL_LE_LT" > "Orderings.order_class.le_less"
"REAL_LE_LNEG" > "RealDef.real_0_le_add_iff"
- "REAL_LE_LMUL_IMP" > "Rings.mult_mono"
+ "REAL_LE_LMUL_IMP" > "Rings.ordered_comm_semiring_class.comm_mult_left_mono"
"REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2"
- "REAL_LE_LDIV_EQ" > "Rings.pos_divide_le_eq"
- "REAL_LE_LDIV" > "Rings.mult_imp_div_pos_le"
- "REAL_LE_LADD_IMP" > "Groups.add_left_mono"
- "REAL_LE_LADD" > "Groups.add_le_cancel_left"
- "REAL_LE_INV_EQ" > "Rings.inverse_nonnegative_iff_nonnegative"
+ "REAL_LE_LDIV_EQ" > "Fields.linordered_field_class.pos_divide_le_eq"
+ "REAL_LE_LDIV" > "Fields.linordered_field_class.mult_imp_div_pos_le"
+ "REAL_LE_LADD_IMP" > "Groups.ordered_ab_semigroup_add_class.add_left_mono"
+ "REAL_LE_LADD" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left"
+ "REAL_LE_INV_EQ" > "Fields.linordered_field_inverse_zero_class.inverse_nonnegative_iff_nonnegative"
"REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV"
- "REAL_LE_DOUBLE" > "Groups.zero_le_double_add_iff_zero_le_single_add"
+ "REAL_LE_DOUBLE" > "Groups.linordered_ab_group_add_class.zero_le_double_add_iff_zero_le_single_add"
"REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV"
- "REAL_LE_ANTISYM" > "Orderings.order_eq_iff"
+ "REAL_LE_ANTISYM" > "Orderings.order_class.eq_iff"
"REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR"
"REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL"
- "REAL_LE_ADD2" > "Groups.add_mono"
- "REAL_LE_ADD" > "Groups.add_nonneg_nonneg"
- "REAL_LE_01" > "Rings.zero_le_one"
- "REAL_LET_TRANS" > "Set.basic_trans_rules_23"
- "REAL_LET_TOTAL" > "Orderings.linorder_le_less_linear"
+ "REAL_LE_ADD2" > "Groups.add_mono_thms_linordered_semiring_1"
+ "REAL_LE_ADD" > "Groups.ordered_comm_monoid_add_class.add_nonneg_nonneg"
+ "REAL_LE_01" > "Rings.linordered_semidom_class.zero_le_one"
+ "REAL_LET_TRANS" > "Orderings.order_le_less_trans"
+ "REAL_LET_TOTAL" > "Orderings.linorder_class.le_less_linear"
"REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM"
- "REAL_LET_ADD2" > "Groups.add_le_less_mono"
- "REAL_LET_ADD" > "Groups.add_nonneg_pos"
+ "REAL_LET_ADD2" > "Groups.add_mono_thms_linordered_field_4"
+ "REAL_LET_ADD" > "Groups.ordered_comm_monoid_add_class.add_nonneg_pos"
"REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2"
"REAL_LE" > "RealDef.real_of_nat_le_iff"
- "REAL_LDISTRIB" > "Rings.ring_eq_simps_2"
- "REAL_INV_POS" > "Rings.positive_imp_inverse_positive"
- "REAL_INV_NZ" > "Rings.nonzero_imp_inverse_nonzero"
+ "REAL_LDISTRIB" > "Fields.linordered_field_class.sign_simps_7"
+ "REAL_INV_POS" > "Fields.linordered_field_class.positive_imp_inverse_positive"
+ "REAL_INV_NZ" > "Fields.division_ring_class.nonzero_imp_inverse_nonzero"
"REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
- "REAL_INV_LT1" > "Fields.one_less_inverse"
- "REAL_INV_INV" > "Rings.inverse_inverse_eq"
- "REAL_INV_EQ_0" > "Rings.inverse_nonzero_iff_nonzero"
- "REAL_INV_1OVER" > "Rings.inverse_eq_divide"
- "REAL_INV_0" > "Rings.division_ring_inverse_zero_class.inverse_zero"
- "REAL_INVINV" > "Rings.nonzero_inverse_inverse_eq"
- "REAL_INV1" > "Rings.inverse_1"
+ "REAL_INV_LT1" > "Fields.linordered_field_class.one_less_inverse"
+ "REAL_INV_INV" > "Fields.division_ring_inverse_zero_class.inverse_inverse_eq"
+ "REAL_INV_EQ_0" > "Fields.division_ring_inverse_zero_class.inverse_nonzero_iff_nonzero"
+ "REAL_INV_1OVER" > "Fields.division_ring_class.inverse_eq_divide"
+ "REAL_INV_0" > "Fields.division_ring_inverse_zero_class.inverse_zero"
+ "REAL_INVINV" > "Fields.division_ring_class.nonzero_inverse_inverse_eq"
+ "REAL_INV1" > "Fields.division_ring_class.inverse_1"
"REAL_INJ" > "RealDef.real_of_nat_inject"
"REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves"
"REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ"
- "REAL_EQ_SUB_RADD" > "Rings.ring_eq_simps_15"
- "REAL_EQ_SUB_LADD" > "Rings.ring_eq_simps_16"
- "REAL_EQ_RMUL_IMP" > "Rings.field_mult_cancel_right_lemma"
- "REAL_EQ_RMUL" > "Rings.field_mult_cancel_right"
+ "REAL_EQ_SUB_RADD" > "Fields.linordered_field_class.sign_simps_12"
+ "REAL_EQ_SUB_LADD" > "Fields.linordered_field_class.sign_simps_11"
+ "REAL_EQ_RMUL_IMP" > "HOL4Real.real.REAL_EQ_RMUL_IMP"
+ "REAL_EQ_RMUL" > "Rings.mult_compare_simps_13"
"REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ"
- "REAL_EQ_RADD" > "Groups.add_right_cancel"
- "REAL_EQ_NEG" > "Groups.neg_equal_iff_equal"
- "REAL_EQ_MUL_LCANCEL" > "Rings.field_mult_cancel_left"
+ "REAL_EQ_RADD" > "Groups.cancel_semigroup_add_class.add_right_cancel"
+ "REAL_EQ_NEG" > "Groups.group_add_class.neg_equal_iff_equal"
+ "REAL_EQ_MUL_LCANCEL" > "Rings.mult_compare_simps_14"
"REAL_EQ_LMUL_IMP" > "HOL4Real.real.REAL_EQ_LMUL_IMP"
"REAL_EQ_LMUL2" > "RealDef.real_mult_left_cancel"
- "REAL_EQ_LMUL" > "Rings.field_mult_cancel_left"
+ "REAL_EQ_LMUL" > "Rings.mult_compare_simps_14"
"REAL_EQ_LDIV_EQ" > "HOL4Real.real.REAL_EQ_LDIV_EQ"
- "REAL_EQ_LADD" > "Groups.add_left_cancel"
+ "REAL_EQ_LADD" > "Groups.cancel_semigroup_add_class.add_left_cancel"
"REAL_EQ_IMP_LE" > "Orderings.order_eq_refl"
- "REAL_ENTIRE" > "Rings.field_mult_eq_0_iff"
+ "REAL_ENTIRE" > "Rings.ring_no_zero_divisors_class.mult_eq_0_iff"
"REAL_DOWN2" > "RealDef.real_lbound_gt_zero"
"REAL_DOWN" > "HOL4Real.real.REAL_DOWN"
"REAL_DOUBLE" > "Int.mult_2"
"REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL"
- "REAL_DIV_REFL" > "Rings.divide_self"
+ "REAL_DIV_REFL" > "Fields.division_ring_class.divide_self"
"REAL_DIV_MUL2" > "HOL4Real.real.REAL_DIV_MUL2"
- "REAL_DIV_LZERO" > "Rings.divide_zero_left"
+ "REAL_DIV_LZERO" > "Fields.division_ring_class.divide_zero_left"
"REAL_DIV_LMUL" > "HOL4Real.real.REAL_DIV_LMUL"
- "REAL_DIFFSQ" > "HOL4Real.real.REAL_DIFFSQ"
- "REAL_ARCH_LEAST" > "HOL4Real.real.REAL_ARCH_LEAST"
+ "REAL_DIFFSQ" > "Rings.comm_ring_class.square_diff_square_factored"
+ "REAL_ARCH_LEAST" > "Transcendental.reals_Archimedean4"
"REAL_ARCH" > "RComplete.reals_Archimedean3"
- "REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
+ "REAL_ADD_SYM" > "Fields.linordered_field_class.sign_simps_18"
"REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2"
"REAL_ADD_SUB" > "HOL4Real.real.REAL_ADD_SUB"
- "REAL_ADD_RINV" > "Groups.right_minus"
+ "REAL_ADD_RINV" > "Groups.group_add_class.right_minus"
"REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ"
- "REAL_ADD_RID" > "Finite_Set.AC_add.f_e.ident"
- "REAL_ADD_RDISTRIB" > "Rings.ring_eq_simps_1"
- "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
+ "REAL_ADD_RID" > "Divides.arithmetic_simps_39"
+ "REAL_ADD_RDISTRIB" > "Fields.linordered_field_class.sign_simps_8"
+ "REAL_ADD_LINV" > "Groups.ab_group_add_class.ab_left_minus"
"REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ"
- "REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident"
- "REAL_ADD_LDISTRIB" > "Rings.ring_eq_simps_2"
- "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
- "REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2"
+ "REAL_ADD_LID" > "Divides.arithmetic_simps_38"
+ "REAL_ADD_LDISTRIB" > "Fields.linordered_field_class.sign_simps_7"
+ "REAL_ADD_ASSOC" > "Fields.linordered_field_class.sign_simps_19"
+ "REAL_ADD2_SUB2" > "RealDef.add_diff_add"
"REAL_ADD" > "RealDef.real_of_nat_add"
- "REAL_ABS_TRIANGLE" > "Groups.abs_triangle_ineq"
- "REAL_ABS_POS" > "Groups.abs_ge_zero"
- "REAL_ABS_MUL" > "Rings.abs_mult"
- "REAL_ABS_0" > "Int.bin_arith_simps_28"
+ "REAL_ABS_TRIANGLE" > "Groups.ordered_ab_group_add_abs_class.abs_triangle_ineq"
+ "REAL_ABS_POS" > "Groups.ordered_ab_group_add_abs_class.abs_ge_zero"
+ "REAL_ABS_MUL" > "Rings.linordered_idom_class.abs_mult"
+ "REAL_ABS_0" > "Divides.arithmetic_simps_27"
"REAL_10" > "HOL4Compat.REAL_10"
"REAL_1" > "HOL4Real.real.REAL_1"
"REAL_0" > "HOL4Real.real.REAL_0"
"REAL" > "RealDef.real_of_nat_Suc"
"POW_ZERO_EQ" > "HOL4Real.real.POW_ZERO_EQ"
- "POW_ZERO" > "RealPow.realpow_zero_zero"
+ "POW_ZERO" > "HOL4Real.real.POW_ZERO"
"POW_POS_LT" > "HOL4Real.real.POW_POS_LT"
- "POW_POS" > "Power.zero_le_power"
+ "POW_POS" > "Power.linordered_semidom_class.zero_le_power"
"POW_PLUS1" > "HOL4Real.real.POW_PLUS1"
- "POW_ONE" > "Power.power_one"
- "POW_NZ" > "Power.field_power_not_zero"
- "POW_MUL" > "Power.power_mult_distrib"
- "POW_MINUS1" > "Nat_Numeral.power_minus1_even"
+ "POW_ONE" > "Power.monoid_mult_class.power_one"
+ "POW_NZ" > "Power.ring_1_no_zero_divisors_class.field_power_not_zero"
+ "POW_MUL" > "Power.comm_monoid_mult_class.power_mult_distrib"
+ "POW_MINUS1" > "Nat_Numeral.ring_1_class.power_minus1_even"
"POW_M1" > "HOL4Real.real.POW_M1"
"POW_LT" > "HOL4Real.real.POW_LT"
- "POW_LE" > "Power.power_mono"
- "POW_INV" > "Power.nonzero_power_inverse"
- "POW_EQ" > "Power.power_inject_base"
- "POW_ADD" > "Power.power_add"
- "POW_ABS" > "Power.power_abs"
- "POW_2_LT" > "RealPow.two_realpow_gt"
- "POW_2_LE1" > "RealPow.two_realpow_ge_one"
- "POW_2" > "Nat_Numeral.power2_eq_square"
- "POW_1" > "Power.power_one_right"
+ "POW_LE" > "Power.linordered_semidom_class.power_mono"
+ "POW_INV" > "Power.division_ring_class.nonzero_power_inverse"
+ "POW_EQ" > "Power.linordered_semidom_class.power_inject_base"
+ "POW_ADD" > "Power.monoid_mult_class.power_add"
+ "POW_ABS" > "Power.linordered_idom_class.power_abs"
+ "POW_2_LT" > "RealDef.two_realpow_gt"
+ "POW_2_LE1" > "RealDef.two_realpow_ge_one"
+ "POW_2" > "Nat_Numeral.monoid_mult_class.power2_eq_square"
+ "POW_1" > "Power.monoid_mult_class.power_one_right"
"POW_0" > "Power.power_0_Suc"
- "ABS_ZERO" > "Groups.abs_eq_0"
- "ABS_TRIANGLE" > "Groups.abs_triangle_ineq"
+ "ABS_ZERO" > "Groups.ordered_ab_group_add_abs_class.abs_eq_0"
+ "ABS_TRIANGLE" > "Groups.ordered_ab_group_add_abs_class.abs_triangle_ineq"
"ABS_SUM" > "HOL4Real.real.ABS_SUM"
- "ABS_SUB_ABS" > "Groups.abs_triangle_ineq3"
- "ABS_SUB" > "Groups.abs_minus_commute"
+ "ABS_SUB_ABS" > "Groups.ordered_ab_group_add_abs_class.abs_triangle_ineq3"
+ "ABS_SUB" > "Groups.ordered_ab_group_add_abs_class.abs_minus_commute"
"ABS_STILLNZ" > "HOL4Real.real.ABS_STILLNZ"
"ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2"
"ABS_SIGN" > "HOL4Real.real.ABS_SIGN"
"ABS_REFL" > "HOL4Real.real.ABS_REFL"
- "ABS_POW2" > "Nat_Numeral.abs_power2"
- "ABS_POS" > "Groups.abs_ge_zero"
- "ABS_NZ" > "Groups.zero_less_abs_iff"
- "ABS_NEG" > "Groups.abs_minus_cancel"
+ "ABS_POW2" > "Nat_Numeral.linordered_idom_class.abs_power2"
+ "ABS_POS" > "Groups.ordered_ab_group_add_abs_class.abs_ge_zero"
+ "ABS_NZ" > "Groups.ordered_ab_group_add_abs_class.zero_less_abs_iff"
+ "ABS_NEG" > "Groups.ordered_ab_group_add_abs_class.abs_minus_cancel"
"ABS_N" > "RealDef.abs_real_of_nat_cancel"
- "ABS_MUL" > "Rings.abs_mult"
+ "ABS_MUL" > "Rings.linordered_idom_class.abs_mult"
"ABS_LT_MUL2" > "HOL4Real.real.ABS_LT_MUL2"
- "ABS_LE" > "Groups.abs_ge_self"
- "ABS_INV" > "Rings.nonzero_abs_inverse"
- "ABS_DIV" > "Rings.nonzero_abs_divide"
+ "ABS_LE" > "Groups.ordered_ab_group_add_abs_class.abs_ge_self"
+ "ABS_INV" > "Fields.linordered_field_class.nonzero_abs_inverse"
+ "ABS_DIV" > "Fields.linordered_field_class.nonzero_abs_divide"
"ABS_CIRCLE" > "HOL4Real.real.ABS_CIRCLE"
"ABS_CASES" > "HOL4Real.real.ABS_CASES"
"ABS_BOUNDS" > "RealDef.abs_le_interval_iff"
@@ -352,8 +352,8 @@
"ABS_BETWEEN2" > "HOL4Real.real.ABS_BETWEEN2"
"ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1"
"ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN"
- "ABS_ABS" > "Groups.abs_idempotent"
- "ABS_1" > "Int.bin_arith_simps_29"
- "ABS_0" > "Int.bin_arith_simps_28"
+ "ABS_ABS" > "Groups.ordered_ab_group_add_abs_class.abs_idempotent"
+ "ABS_1" > "Divides.arithmetic_simps_28"
+ "ABS_0" > "Divides.arithmetic_simps_27"
end