src/HOL/Import/HOL/real.imp
changeset 17188 a26a4fc323ed
parent 16775 c1b87ef4a1c3
child 17644 bd59bfd4bf37
--- a/src/HOL/Import/HOL/real.imp	Mon Aug 29 16:25:24 2005 +0200
+++ b/src/HOL/Import/HOL/real.imp	Mon Aug 29 16:51:39 2005 +0200
@@ -87,13 +87,13 @@
   "REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2"
   "REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2"
   "REAL_SUB_ADD" > "OrderedGroup.diff_add_cancel"
-  "REAL_SUB_ABS" > "HOL4Real.real.REAL_SUB_ABS"
-  "REAL_SUB_0" > "OrderedGroup.eq_iff_diff_eq_0"
+  "REAL_SUB_ABS" > "OrderedGroup.abs_triangle_ineq2"
+  "REAL_SUB_0" > "OrderedGroup.diff_eq_0_iff_eq"
   "REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff"
   "REAL_RINV_UNIQ" > "Ring_and_Field.inverse_unique"
   "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_1"
   "REAL_POW_POW" > "Power.power_mult"
-  "REAL_POW_MONO_LT" > "Power.power_strict_increasing"
+  "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_INV" > "Power.power_inverse"
@@ -114,12 +114,12 @@
   "REAL_NOT_LT" > "HOL4Compat.real_lte"
   "REAL_NOT_LE" > "Orderings.linorder_not_le"
   "REAL_NEG_SUB" > "OrderedGroup.minus_diff_eq"
-  "REAL_NEG_RMUL" > "Ring_and_Field.minus_mult_right"
+  "REAL_NEG_RMUL" > "Ring_and_Field.mult_minus_right"
   "REAL_NEG_NEG" > "OrderedGroup.minus_minus"
   "REAL_NEG_MUL2" > "Ring_and_Field.minus_mult_minus"
   "REAL_NEG_MINUS1" > "HOL4Real.real.REAL_NEG_MINUS1"
   "REAL_NEG_LT0" > "OrderedGroup.neg_less_0_iff_less"
-  "REAL_NEG_LMUL" > "Ring_and_Field.minus_mult_left"
+  "REAL_NEG_LMUL" > "Ring_and_Field.mult_minus_left"
   "REAL_NEG_LE0" > "OrderedGroup.neg_le_0_iff_le"
   "REAL_NEG_INV" > "Ring_and_Field.nonzero_inverse_minus_eq"
   "REAL_NEG_GT0" > "OrderedGroup.neg_0_less_iff_less"
@@ -129,15 +129,15 @@
   "REAL_NEG_ADD" > "OrderedGroup.minus_add_distrib"
   "REAL_NEG_0" > "OrderedGroup.minus_zero"
   "REAL_NEGNEG" > "OrderedGroup.minus_minus"
-  "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_6"
+  "REAL_MUL_SYM" > "IntDef.zmult_ac_2"
   "REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right"
-  "REAL_MUL_RNEG" > "Ring_and_Field.minus_mult_right"
+  "REAL_MUL_RNEG" > "Ring_and_Field.mult_minus_right"
   "REAL_MUL_RINV" > "Ring_and_Field.right_inverse"
-  "REAL_MUL_RID" > "OrderedGroup.monoid_mult.mult_1_right"
+  "REAL_MUL_RID" > "Finite_Set.AC_mult.f_e.ident"
   "REAL_MUL_LZERO" > "Ring_and_Field.mult_zero_left"
-  "REAL_MUL_LNEG" > "Ring_and_Field.minus_mult_left"
+  "REAL_MUL_LNEG" > "Ring_and_Field.mult_minus_left"
   "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
-  "REAL_MUL_LID" > "OrderedGroup.comm_monoid_mult.mult_1"
+  "REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
   "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
   "REAL_MUL" > "RealDef.real_of_nat_mult"
   "REAL_MIDDLE2" > "HOL4Real.real.REAL_MIDDLE2"
@@ -177,7 +177,7 @@
   "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" > "HOL4Real.real.REAL_LT_DIV"
+  "REAL_LT_DIV" > "Ring_and_Field.divide_pos_pos"
   "REAL_LT_ANTISYM" > "HOL4Real.real.REAL_LT_ANTISYM"
   "REAL_LT_ADD_SUB" > "OrderedGroup.compare_rls_7"
   "REAL_LT_ADDR" > "HOL4Real.real.REAL_LT_ADDR"
@@ -186,14 +186,14 @@
   "REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL"
   "REAL_LT_ADD2" > "OrderedGroup.add_strict_mono"
   "REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1"
-  "REAL_LT_ADD" > "RealDef.real_add_order"
+  "REAL_LT_ADD" > "OrderedGroup.add_pos_pos"
   "REAL_LT_1" > "HOL4Real.real.REAL_LT_1"
   "REAL_LT_01" > "Ring_and_Field.ordered_semidom.zero_less_one"
   "REAL_LTE_TRANS" > "Set.basic_trans_rules_24"
   "REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL"
   "REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM"
   "REAL_LTE_ADD2" > "OrderedGroup.add_less_le_mono"
-  "REAL_LTE_ADD" > "HOL4Real.real.REAL_LTE_ADD"
+  "REAL_LTE_ADD" > "OrderedGroup.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"
@@ -206,9 +206,9 @@
   "REAL_LE_RNEG" > "OrderedGroup.le_eq_neg"
   "REAL_LE_RMUL_IMP" > "Ring_and_Field.pordered_semiring.mult_right_mono"
   "REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1"
-  "REAL_LE_REFL" > "Orderings.order.order_refl"
+  "REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl"
   "REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq"
-  "REAL_LE_RDIV" > "HOL4Real.real.REAL_LE_RDIV"
+  "REAL_LE_RDIV" > "Ring_and_Field.mult_imp_le_div_pos"
   "REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right"
   "REAL_LE_POW2" > "NatBin.zero_compare_simps_12"
   "REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL"
@@ -223,7 +223,7 @@
   "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.mult_mono"
   "REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2"
   "REAL_LE_LDIV_EQ" > "Ring_and_Field.pos_divide_le_eq"
-  "REAL_LE_LDIV" > "HOL4Real.real.REAL_LE_LDIV"
+  "REAL_LE_LDIV" > "Ring_and_Field.mult_imp_div_pos_le"
   "REAL_LE_LADD_IMP" > "OrderedGroup.pordered_ab_semigroup_add.add_left_mono"
   "REAL_LE_LADD" > "OrderedGroup.add_le_cancel_left"
   "REAL_LE_INV_EQ" > "Ring_and_Field.inverse_nonnegative_iff_nonnegative"
@@ -234,13 +234,13 @@
   "REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR"
   "REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL"
   "REAL_LE_ADD2" > "OrderedGroup.add_mono"
-  "REAL_LE_ADD" > "RealDef.real_le_add_order"
+  "REAL_LE_ADD" > "OrderedGroup.add_nonneg_nonneg"
   "REAL_LE_01" > "Ring_and_Field.zero_le_one"
   "REAL_LET_TRANS" > "Set.basic_trans_rules_23"
   "REAL_LET_TOTAL" > "Orderings.linorder_le_less_linear"
   "REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM"
   "REAL_LET_ADD2" > "OrderedGroup.add_le_less_mono"
-  "REAL_LET_ADD" > "HOL4Real.real.REAL_LET_ADD"
+  "REAL_LET_ADD" > "OrderedGroup.add_nonneg_pos"
   "REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2"
   "REAL_LE" > "RealDef.real_of_nat_le_iff"
   "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2"
@@ -277,22 +277,22 @@
   "REAL_DOUBLE" > "IntArith.mult_2"
   "REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL"
   "REAL_DIV_REFL" > "Ring_and_Field.divide_self"
-  "REAL_DIV_MUL2" > "Ring_and_Field.nonzero_mult_divide_cancel_left"
+  "REAL_DIV_MUL2" > "HOL4Real.real.REAL_DIV_MUL2"
   "REAL_DIV_LZERO" > "Ring_and_Field.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_ARCH" > "RComplete.reals_Archimedean3"
-  "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
+  "REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
   "REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2"
   "REAL_ADD_SUB" > "HOL4Real.real.REAL_ADD_SUB"
   "REAL_ADD_RINV" > "OrderedGroup.right_minus"
   "REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ"
-  "REAL_ADD_RID" > "OrderedGroup.add_0_right"
+  "REAL_ADD_RID" > "Finite_Set.AC_add.f_e.ident"
   "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_1"
   "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
   "REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ"
-  "REAL_ADD_LID" > "OrderedGroup.comm_monoid_add.add_0"
+  "REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident"
   "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2"
   "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
   "REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2"
@@ -300,7 +300,7 @@
   "REAL_ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq"
   "REAL_ABS_POS" > "OrderedGroup.abs_ge_zero"
   "REAL_ABS_MUL" > "Ring_and_Field.abs_mult"
-  "REAL_ABS_0" > "OrderedGroup.abs_zero"
+  "REAL_ABS_0" > "Numeral.bin_arith_simps_28"
   "REAL_10" > "HOL4Compat.REAL_10"
   "REAL_1" > "HOL4Real.real.REAL_1"
   "REAL_0" > "HOL4Real.real.REAL_0"
@@ -329,7 +329,7 @@
   "ABS_ZERO" > "OrderedGroup.abs_eq_0"
   "ABS_TRIANGLE" > "OrderedGroup.abs_triangle_ineq"
   "ABS_SUM" > "HOL4Real.real.ABS_SUM"
-  "ABS_SUB_ABS" > "HOL4Real.real.ABS_SUB_ABS"
+  "ABS_SUB_ABS" > "OrderedGroup.abs_triangle_ineq3"
   "ABS_SUB" > "OrderedGroup.abs_minus_commute"
   "ABS_STILLNZ" > "HOL4Real.real.ABS_STILLNZ"
   "ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2"
@@ -353,7 +353,7 @@
   "ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1"
   "ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN"
   "ABS_ABS" > "OrderedGroup.abs_idempotent"
-  "ABS_1" > "Ring_and_Field.abs_one"
-  "ABS_0" > "OrderedGroup.abs_zero"
+  "ABS_1" > "Numeral.bin_arith_simps_29"
+  "ABS_0" > "Numeral.bin_arith_simps_28"
 
 end