1.1 --- a/src/Tools/isac/ProgLang/Real2002-theorems.sml Tue Aug 31 11:10:30 2010 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Real2002-theorems.sml Tue Aug 31 15:36:57 2010 +0200
1.3 @@ -443,7 +443,7 @@
1.4 "real_minus_congruent";
1.5 "real_minus";
1.6 "- Abs_REAL (realrel `` {(?x, ?y)}) = Abs_REAL (realrel `` {(?y, ?x)})"
1.7 - "real_minus_minus"; (**)"- (- (?z::real)) = ?z"
1.8 + "minus_minus"; (**)"- (- (?z::real)) = ?z"
1.9 "inj_real_minus"; "inj uminus"
1.10 "real_minus_zero"; (**)"- 0 = 0"
1.11 "real_minus_zero_iff"; (**)"(- ?x = 0) = (?x = 0)"
1.12 @@ -454,19 +454,19 @@
1.13 "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) +
1.14 Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =
1.15 Abs_REAL (realrel `` {(?x1.0 + ?x2.0, ?y1.0 + ?y2.0)})"
1.16 - "real_add_commute"; (**)"(?z::real) + (?w::real) = ?w + ?z"
1.17 - "real_add_assoc"; (**)
1.18 - "real_add_left_commute"; (**)
1.19 - "real_add_zero_left"; (**)"0 + ?z = ?z"
1.20 - "real_add_zero_right"; (**)
1.21 - "real_add_minus"; (**)"?z + - ?z = 0"
1.22 - "real_add_minus_left"; (**)
1.23 - "real_add_minus_cancel"; (**)"?z + (- ?z + ?w) = ?w"
1.24 + "add_commute"; (**)"(?z::real) + (?w::real) = ?w + ?z"
1.25 + "add_assoc"; (**)
1.26 + "add_left_commute"; (**)
1.27 + "add_0_left"; (**)"0 + ?z = ?z"
1.28 + "add_0_right"; (**)
1.29 + "right_minus"; (**)"?z + - ?z = 0"
1.30 + "right_minus_left"; (**)
1.31 + "right_minus_cancel"; (**)"?z + (- ?z + ?w) = ?w"
1.32 "real_minus_add_cancel"; (**)"- ?z + (?z + ?w) = ?w"
1.33 "real_minus_ex"; "EX y. ?x + y = 0"
1.34 "real_minus_ex1";
1.35 "real_minus_left_ex1"; "EX! y. y + ?x = 0"
1.36 - "real_add_minus_eq_minus";"?x + ?y = 0 ==> ?x = - ?y"
1.37 + "right_minus_eq_minus";"?x + ?y = 0 ==> ?x = - ?y"
1.38 "real_as_add_inverse_ex"; "EX y. ?x = - y"
1.39 "real_minus_add_distrib"; (**)"- (?x + ?y) = - ?x + - ?y"
1.40 "real_add_left_cancel"; "(?x + ?y = ?x + ?z) = (?y = ?z)"
1.41 @@ -491,23 +491,23 @@
1.42 "real_mult_assoc"; (**)
1.43 "real_mult_left_commute";
1.44 (**)"?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"
1.45 - "real_mult_1"; (**)"1 * ?z = ?z"
1.46 - "real_mult_1_right"; (**)"?z * 1 = ?z"
1.47 - "real_mult_0"; (**)
1.48 - "real_mult_0_right"; (**)"?z * 0 = 0"
1.49 + "mult_1_left"; (**)"1 * ?z = ?z"
1.50 + "mult_1_right"; (**)"?z * 1 = ?z"
1.51 + "mult_zero_left"; (**)
1.52 + "mult_zero_left_right"; (**)"?z * 0 = 0"
1.53 "real_mult_minus_eq1"; (**)"- ?x * ?y = - (?x * ?y)"
1.54 "real_mult_minus_eq2"; (**)"?x * - ?y = - (?x * ?y)"
1.55 "real_mult_minus_1"; (**)"- 1 * ?z = - ?z"
1.56 "real_mult_minus_1_right";(**)"?z * - 1 = - ?z"
1.57 "real_minus_mult_cancel"; (**)"- ?x * - ?y = ?x * ?y"
1.58 "real_minus_mult_commute";(**)"- ?x * ?y = ?x * - ?y"
1.59 - "real_add_assoc_cong";
1.60 + "add_assoc_cong";
1.61 "?z + ?v = ?z' + ?v' ==> ?z + (?v + ?w) = ?z' + (?v' + ?w)"
1.62 - "real_add_assoc_swap"; (**)"?z + (?v + ?w) = ?v + (?z + ?w)"
1.63 - "real_add_mult_distrib"; (**)"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"
1.64 - "real_add_mult_distrib2"; (**)"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"
1.65 - "real_diff_mult_distrib"; (**)"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"
1.66 - "real_diff_mult_distrib2";(**)"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"
1.67 + "add_assoc_swap"; (**)"?z + (?v + ?w) = ?v + (?z + ?w)"
1.68 + "left_distrib"; (**)"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"
1.69 + "left_distrib2"; (**)"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"
1.70 + "left_diff_distrib"; (**)"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"
1.71 + "left_diff_distrib2";(**)"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"
1.72 "real_zero_not_eq_one";
1.73 "real_zero_iff"; "0 = Abs_REAL (realrel `` {(?x, ?x)})"
1.74 "real_mult_inv_right_ex"; "?x ~= 0 ==> EX y. ?x * y = 1"
1.75 @@ -526,13 +526,13 @@
1.76 "real_inverse_1"; "inverse 1 = 1"
1.77 "real_minus_inverse"; "inverse (- ?x) = - inverse ?x"
1.78 "real_inverse_distrib"; "inverse (?x * ?y) = inverse ?x * inverse ?y"
1.79 - "real_times_divide1_eq"; (**)"?x * (?y / ?z) = ?x * ?y / ?z"
1.80 - "real_times_divide2_eq"; (**)"?y / ?z * ?x = ?y * ?x / ?z"
1.81 - "real_divide_divide1_eq"; (**)"?x / (?y / ?z) = ?x * ?z / ?y"
1.82 - "real_divide_divide2_eq"; (**)"?x / ?y / ?z = ?x / (?y * ?z)"
1.83 + "times_divide_eq_right"; (**)"?x * (?y / ?z) = ?x * ?y / ?z"
1.84 + "times_divide_eq_left"; (**)"?y / ?z * ?x = ?y * ?x / ?z"
1.85 + "divide_divide_eq_right"; (**)"?x / (?y / ?z) = ?x * ?z / ?y"
1.86 + "divide_divide_eq_left"; (**)"?x / ?y / ?z = ?x / (?y * ?z)"
1.87 "real_minus_divide_eq"; (**)"- ?x / ?y = - (?x / ?y)"
1.88 "real_divide_minus_eq"; (**)"?x / - ?y = - (?x / ?y)"
1.89 - "real_add_divide_distrib"; (**)"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
1.90 + "nadd_divide_distrib"; (**)"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
1.91 "preal_lemma_eq_rev_sum";
1.92 "[| ?x = ?y; ?x1.0 = ?y1.0 |] ==> ?x + ?y1.0 = ?x1.0 + ?y"
1.93 "preal_add_left_commute_cancel";
1.94 @@ -560,7 +560,7 @@
1.95 "real_of_preal_not_minus_gt_zero";
1.96 "real_of_preal_zero_less";
1.97 "real_of_preal_not_less_zero";
1.98 - "real_minus_minus_zero_less";
1.99 + "minus_minus_zero_less";
1.100 "real_of_preal_sum_zero_less";
1.101 "real_of_preal_minus_less_all";
1.102 "real_of_preal_not_minus_gt_all";
1.103 @@ -640,7 +640,7 @@
1.104 "real_add_left_le_mono1";
1.105 "real_add_le_mono";
1.106 "real_less_Ex";
1.107 - "real_add_minus_positive_less_self"; "0 < ?r ==> ?u + - ?r < ?u"
1.108 + "right_minus_positive_less_self"; "0 < ?r ==> ?u + - ?r < ?u"
1.109 "real_le_minus_iff"; "(- ?s <= - ?r) = (?r <= ?s)"
1.110 "real_le_square";
1.111 "real_of_posnat_one";
1.112 @@ -760,7 +760,7 @@
1.113 "[| ?i <= ?j; ?k <= ?l; 0 <= ?j; 0 <= ?k |] ==> ?i * ?k <= ?j * ?l"
1.114 RealArith0.ML:qed ------------------------------------------------------------
1.115 "real_diff_minus_eq"; (**)"?x - - ?y = ?x + ?y"
1.116 - "real_0_divide"; (**)"0 / ?x = 0"
1.117 + "divide_zero_left"; (**)"0 / ?x = 0"
1.118 "real_0_less_inverse_iff"; "(0 < inverse ?x) = (0 < ?x)"
1.119 "real_inverse_less_0_iff";
1.120 "real_0_le_inverse_iff";
1.121 @@ -803,7 +803,7 @@
1.122 "real_divide_eq_cancel1"; "(?k / ?m = ?k / ?n) = (?k = 0 | ?m = ?n)"
1.123 "real_inverse_less_iff";
1.124 "real_inverse_le_iff";
1.125 - "real_divide_1"; (**)"?x / 1 = ?x"
1.126 + "divide_1"; (**)"?x / 1 = ?x"
1.127 "real_divide_minus1"; (**)"?x / -1 = - ?x"
1.128 "real_minus1_divide"; (**)"-1 / ?x = - (1 / ?x)"
1.129 "real_lbound_gt_zero";
1.130 @@ -816,7 +816,7 @@
1.131 "real_minus_le"; "(- ?x <= ?y) = (- ?y <= ?x)"
1.132 "real_equation_minus"; (**)"(?x = - ?y) = (?y = - ?x)"
1.133 "real_minus_equation"; (**)"(- ?x = ?y) = (- ?y = ?x)"
1.134 - "real_add_minus_iff"; (**)"(?x + - ?a = 0) = (?x = ?a)"
1.135 + "right_minus_iff"; (**)"(?x + - ?a = 0) = (?x = ?a)"
1.136 "real_minus_eq_cancel"; (**)"(- ?b = - ?a) = (?b = ?a)"
1.137 "real_add_eq_0_iff"; (**)"(?x + ?y = 0) = (?y = - ?x)"
1.138 "real_add_less_0_iff"; "(?x + ?y < 0) = (?y < - ?x)"
1.139 @@ -874,7 +874,7 @@
1.140 "abs_add_less"; "[| abs ?x < ?r; abs ?y < ?s |] ==> abs (?x + ?y) < ?r + ?s"
1.141 RealAbs.ML:qed
1.142 "abs_add_minus_less";
1.143 - "real_mult_0_less"; "(0 * ?x < ?r) = (0 < ?r)"
1.144 + "mult_zero_left_less"; "(0 * ?x < ?r) = (0 < ?r)"
1.145 "real_mult_less_trans";
1.146 "real_mult_le_less_trans";
1.147 "abs_mult_less";