1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Sep 01 16:43:58 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Sep 02 15:11:23 2010 +0200
1.3 @@ -63,16 +63,12 @@
1.4 use_thy "Knowledge/Atools"
1.5 use_thy "Knowledge/Simplify"
1.6
1.7 -ML {*
1.8 - @{thm o_apply};
1.9 - @{thm o_apply} RS @{thm sym};
1.10 -*}
1.11 -
1.12 +use "../../../test/Tools/isac/Knowledge/poly.sml";
1.13 +use_thy "Knowledge/Poly"
1.14
1.15
1.16 text {*------------------------------------------*}
1.17 (*
1.18 -use_thy "Knowledge/Poly"
1.19 use_thy "Knowledge/Rational"
1.20 use_thy "Knowledge/PolyMinus"
1.21 use_thy "Knowledge/Equation"
2.1 --- a/src/Tools/isac/Knowledge/Delete.thy Wed Sep 01 16:43:58 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Thu Sep 02 15:11:23 2010 +0200
2.3 @@ -8,9 +8,10 @@
2.4 axioms (* theorems which are available only with long names,
2.5 which can not yet be handled in isac's scripts *)
2.6
2.7 - real_mult_left_commute "z1 * (z2 * z3) = z2 * (z1 * z3)"
2.8 + real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)"
2.9 (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*)
2.10 -
2.11 + real_mult_minus1: "-1 * z = - (z::real)"
2.12 + real_mult_2: "2 * z = z + (z::real)"
2.13
2.14 ML {*
2.15 (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var:
3.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 01 16:43:58 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Sep 02 15:11:23 2010 +0200
3.3 @@ -293,8 +293,8 @@
3.4 (*
3.5 val simplify_System =
3.6 append_rls "simplify_System" simplify_System_parenthesized
3.7 - [Thm ("sym_real_add_assoc",
3.8 - num_str (@{thm real_add_assoc} RS @{thm sym}))];
3.9 + [Thm ("sym_add_assoc",
3.10 + num_str (@{thm add_assoc} RS @{thm sym}))];
3.11 *)
3.12
3.13 val isolate_bdvs =
4.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Sep 01 16:43:58 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Sep 02 15:11:23 2010 +0200
4.3 @@ -31,108 +31,108 @@
4.4 stated as axioms, TODO: prove as theorems;
4.5 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
4.6
4.7 - realpow_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
4.8 - realpow_addI "r ^^^ (n + m) = r ^^^ n * r ^^^ m"
4.9 - realpow_addI_assoc_l "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"
4.10 - realpow_addI_assoc_r "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)"
4.11 + realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
4.12 + realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m"
4.13 + realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"
4.14 + realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)"
4.15
4.16 - realpow_oneI "r ^^^ 1 = r"
4.17 - realpow_zeroI "r ^^^ 0 = 1"
4.18 - realpow_eq_oneI "1 ^^^ n = 1"
4.19 - realpow_multI "(r * s) ^^^ n = r ^^^ n * s ^^^ n"
4.20 - realpow_multI_poly "[| r is_polyexp; s is_polyexp |] ==>
4.21 + realpow_oneI: "r ^^^ 1 = r"
4.22 + realpow_zeroI: "r ^^^ 0 = 1"
4.23 + realpow_eq_oneI: "1 ^^^ n = 1"
4.24 + realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n"
4.25 + realpow_multI_poly: "[| r is_polyexp; s is_polyexp |] ==>
4.26 (r * s) ^^^ n = r ^^^ n * s ^^^ n"
4.27 - realpow_minus_oneI "-1 ^^^ (2 * n) = 1"
4.28 + realpow_minus_oneI: "-1 ^^^ (2 * n) = 1"
4.29
4.30 - realpow_twoI "r ^^^ 2 = r * r"
4.31 - realpow_twoI_assoc_l "r * (r * s) = r ^^^ 2 * s"
4.32 - realpow_twoI_assoc_r "s * r * r = s * r ^^^ 2"
4.33 - realpow_two_atom "r is_atom ==> r * r = r ^^^ 2"
4.34 - realpow_plus_1 "r * r ^^^ n = r ^^^ (n + 1)"
4.35 - realpow_plus_1_assoc_l "r * (r ^^^ m * s) = r ^^^ (1 + m) * s"
4.36 - realpow_plus_1_assoc_l2 "r ^^^ m * (r * s) = r ^^^ (1 + m) * s"
4.37 - realpow_plus_1_assoc_r "s * r * r ^^^ m = s * r ^^^ (1 + m)"
4.38 - realpow_plus_1_atom "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)"
4.39 - realpow_def_atom "[| Not (r is_atom); 1 < n |]
4.40 + realpow_twoI: "r ^^^ 2 = r * r"
4.41 + realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s"
4.42 + realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2"
4.43 + realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2"
4.44 + realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)"
4.45 + realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s"
4.46 + realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s"
4.47 + realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)"
4.48 + realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)"
4.49 + realpow_def_atom: "[| Not (r is_atom); 1 < n |]
4.50 ==> r ^^^ n = r * r ^^^ (n + -1)"
4.51 - realpow_addI_atom "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"
4.52 + realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"
4.53
4.54
4.55 - realpow_minus_even "n is_even ==> (- r) ^^^ n = r ^^^ n"
4.56 - realpow_minus_odd "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"
4.57 + realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n"
4.58 + realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"
4.59
4.60
4.61 (* RL 020914 *)
4.62 - real_pp_binom_times "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
4.63 - real_pm_binom_times "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
4.64 - real_mp_binom_times "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
4.65 - real_mm_binom_times "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
4.66 - real_plus_binom_pow3 "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
4.67 - real_plus_binom_pow3_poly "[| a is_polyexp; b is_polyexp |] ==>
4.68 + real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
4.69 + real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
4.70 + real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
4.71 + real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
4.72 + real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
4.73 + real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==>
4.74 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
4.75 - real_minus_binom_pow3 "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
4.76 - real_minus_binom_pow3_p "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
4.77 + real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
4.78 + real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
4.79 -1*b^^^3"
4.80 -(* real_plus_binom_pow "[| n is_const; 3 < n |] ==>
4.81 +(* real_plus_binom_pow: "[| n is_const; 3 < n |] ==>
4.82 (a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
4.83 - real_plus_binom_pow4 "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
4.84 + real_plus_binom_pow4: "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
4.85 *(a + b)"
4.86 - real_plus_binom_pow4_poly "[| a is_polyexp; b is_polyexp |] ==>
4.87 + real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
4.88 (a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
4.89 *(a + b)"
4.90 - real_plus_binom_pow5 "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
4.91 + real_plus_binom_pow5: "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
4.92 *(a^^^2 + 2*a*b + b^^^2)"
4.93 - real_plus_binom_pow5_poly "[| a is_polyexp; b is_polyexp |] ==>
4.94 + real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==>
4.95 (a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2
4.96 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"
4.97 - real_diff_plus "a - b = a + -b" (*17.3.03: do_NOT_use*)
4.98 - real_diff_minus "a - b = a + -1 * b"
4.99 - real_plus_binom_times "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
4.100 - real_minus_binom_times "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
4.101 + real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*)
4.102 + real_diff_minus: "a - b = a + -1 * b"
4.103 + real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
4.104 + real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
4.105 (*WN071229 changed for Schaerding -----vvv*)
4.106 - (*real_plus_binom_pow2 "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
4.107 - real_plus_binom_pow2 "(a + b)^^^2 = (a + b) * (a + b)"
4.108 + (*real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
4.109 + real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)"
4.110 (*WN071229 changed for Schaerding -----^^^*)
4.111 - real_plus_binom_pow2_poly "[| a is_polyexp; b is_polyexp |] ==>
4.112 + real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
4.113 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
4.114 - real_minus_binom_pow2 "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
4.115 - real_minus_binom_pow2_p "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"
4.116 - real_plus_minus_binom1 "(a + b)*(a - b) = a^^^2 - b^^^2"
4.117 - real_plus_minus_binom1_p "(a + b)*(a - b) = a^^^2 + -1*b^^^2"
4.118 - real_plus_minus_binom1_p_p "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"
4.119 - real_plus_minus_binom2 "(a - b)*(a + b) = a^^^2 - b^^^2"
4.120 - real_plus_minus_binom2_p "(a - b)*(a + b) = a^^^2 + -1*b^^^2"
4.121 - real_plus_minus_binom2_p_p "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"
4.122 - real_plus_binom_times1 "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"
4.123 - real_plus_binom_times2 "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"
4.124 + real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
4.125 + real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"
4.126 + real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2"
4.127 + real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2"
4.128 + real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"
4.129 + real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2"
4.130 + real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2"
4.131 + real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"
4.132 + real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"
4.133 + real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"
4.134
4.135 - real_num_collect "[| l is_const; m is_const |] ==>
4.136 + real_num_collect: "[| l is_const; m is_const |] ==>
4.137 l * n + m * n = (l + m) * n"
4.138 (* FIXME.MG.0401: replace 'real_num_collect_assoc'
4.139 by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
4.140 - real_num_collect_assoc "[| l is_const; m is_const |] ==>
4.141 + real_num_collect_assoc: "[| l is_const; m is_const |] ==>
4.142 l * n + (m * n + k) = (l + m) * n + k"
4.143 - real_num_collect_assoc_l "[| l is_const; m is_const |] ==>
4.144 + real_num_collect_assoc_l: "[| l is_const; m is_const |] ==>
4.145 l * n + (m * n + k) = (l + m)
4.146 * n + k"
4.147 - real_num_collect_assoc_r "[| l is_const; m is_const |] ==>
4.148 + real_num_collect_assoc_r: "[| l is_const; m is_const |] ==>
4.149 (k + m * n) + l * n = k + (l + m) * n"
4.150 - real_one_collect "m is_const ==> n + m * n = (1 + m) * n"
4.151 + real_one_collect: "m is_const ==> n + m * n = (1 + m) * n"
4.152 (* FIXME.MG.0401: replace 'real_one_collect_assoc'
4.153 by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
4.154 - real_one_collect_assoc "m is_const ==> n + (m * n + k) = (1 + m)* n + k"
4.155 + real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k"
4.156
4.157 - real_one_collect_assoc_l "m is_const ==> n + (m * n + k) = (1 + m) * n + k"
4.158 - real_one_collect_assoc_r "m is_const ==> (k + n) + m * n = k + (1 + m) * n"
4.159 + real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k"
4.160 + real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n"
4.161
4.162 (* FIXME.MG.0401: replace 'real_mult_2_assoc'
4.163 by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
4.164 - real_mult_2_assoc "z1 + (z1 + k) = 2 * z1 + k"
4.165 - real_mult_2_assoc_l "z1 + (z1 + k) = 2 * z1 + k"
4.166 - real_mult_2_assoc_r "(k + z1) + z1 = k + 2 * z1"
4.167 + real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k"
4.168 + real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k"
4.169 + real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1"
4.170
4.171 - real_add_mult_distrib_poly "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w"
4.172 - real_add_mult_distrib2_poly "w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
4.173 + real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w"
4.174 + real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
4.175
4.176 text {* remark on 'polynomials'
4.177 WN020919
4.178 @@ -440,7 +440,7 @@
4.179 | size_of_term' _ = 1;
4.180
4.181 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
4.182 - (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
4.183 + (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
4.184 | term_ord' pr thy (t, u) =
4.185 (if pr then
4.186 let
4.187 @@ -468,7 +468,7 @@
4.188 end
4.189 | ord => ord)
4.190 and hd_ord (f, g) = (* ~ term.ML *)
4.191 - prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
4.192 + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
4.193 and terms_ord str pr (ts, us) =
4.194 list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
4.195 in
4.196 @@ -486,14 +486,11 @@
4.197
4.198
4.199 val expand =
4.200 - Rls{id = "expand", preconds = [],
4.201 - rew_ord = ("dummy_ord", dummy_ord),
4.202 - erls = e_rls,srls = Erls,
4.203 - calc = [],
4.204 - (*asm_thm = [],*)
4.205 + Rls{id = "expand", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
4.206 + erls = e_rls,srls = Erls, calc = [],
4.207 rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
4.208 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
4.209 - Thm ("left_distrib2",num_str @{thm left_distrib2})
4.210 + Thm ("right_distrib",num_str @{thm right_distrib})
4.211 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
4.212 ], scr = EmptyScr}:rls;
4.213
4.214 @@ -510,7 +507,7 @@
4.215 rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
4.216 (*"a - b = a + -1 * b"*)
4.217 Thm ("sym_real_mult_minus1",
4.218 - num_str (@{thm sym_real_mult_minus1} RS @{thm sym}))
4.219 + num_str (@{thm real_mult_minus1} RS @{thm sym}))
4.220 (*- ?z = "-1 * ?z"*)
4.221 ], scr = EmptyScr}:rls;
4.222 val expand_poly_ =
4.223 @@ -540,7 +537,7 @@
4.224
4.225 Thm ("left_distrib" ,num_str @{thm left_distrib}),
4.226 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
4.227 - Thm ("left_distrib2",num_str @{thm left_distrib}2),
4.228 + Thm ("right_distrib",num_str @{thm right_distrib}),
4.229 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
4.230
4.231 Thm ("realpow_multI", num_str @{thm realpow_multI}),
4.232 @@ -603,9 +600,11 @@
4.233 Thm ("real_plus_minus_binom2_p_p",num_str @{thm real_plus_minus_binom2_p_p}),
4.234 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
4.235
4.236 - Thm ("left_distrib_poly" ,num_str @{thm left_distrib_poly}),
4.237 + Thm ("real_add_mult_distrib_poly",
4.238 + num_str @{thm real_add_mult_distrib_poly}),
4.239 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
4.240 - Thm("left_distrib2_poly",num_str @{thm left_distrib2_poly}),
4.241 + Thm("real_add_mult_distrib2_poly",
4.242 + num_str @{thm real_add_mult_distrib2_poly}),
4.243 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
4.244
4.245 Thm ("realpow_multI_poly", num_str @{thm realpow_multI_poly}),
4.246 @@ -678,7 +677,7 @@
4.247 (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
4.248 Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
4.249 (*"r ^^^ 1 = r"*)
4.250 - Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI)
4.251 + Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI})
4.252 (*"1 ^^^ n = 1"*)
4.253 ], scr = EmptyScr}:rls;
4.254
4.255 @@ -712,14 +711,12 @@
4.256 val reduce_012_ =
4.257 Rls{id = "reduce_012_", preconds = [],
4.258 rew_ord = ("dummy_ord", dummy_ord),
4.259 - erls = e_rls,srls = Erls,
4.260 - calc = [],
4.261 - (*asm_thm = [],*)
4.262 + erls = e_rls,srls = Erls, calc = [],
4.263 rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
4.264 (*"1 * z = z"*)
4.265 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
4.266 (*"0 * z = 0"*)
4.267 - Thm ("mult_zero_left_right",num_str @{thm mult_zero_left}_right),
4.268 + Thm ("mult_zero_right",num_str @{thm mult_zero_right}),
4.269 (*"z * 0 = 0"*)
4.270 Thm ("add_0_left",num_str @{thm add_0_left}),
4.271 (*"0 + z = z"*)
4.272 @@ -738,8 +735,8 @@
4.273 [Thm ("sym_real_mult_assoc",
4.274 num_str (@{thm real_mult_assoc} RS @{thm sym}))
4.275 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
4.276 - (*Thm ("sym_real_add_assoc",
4.277 - num_str (@{thm real_add_assoc} RS @{thm sym}))*)
4.278 + (*Thm ("sym_add_assoc",
4.279 + num_str (@{thm add_assoc} RS @{thm sym}))*)
4.280 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
4.281 ];
4.282
4.283 @@ -783,7 +780,7 @@
4.284 (*asm_thm = [],*)
4.285 rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
4.286 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
4.287 - Thm ("left_distrib2",num_str @{thm left_distrib}2),
4.288 + Thm ("right_distrib",num_str @{thm right_distrib}),
4.289 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
4.290 (*Thm ("left_distrib1",num_str @{thm left_distrib}1),
4.291 ....... 18.3.03 undefined???*)
4.292 @@ -907,7 +904,7 @@
4.293 (*Thm ("real_mult_minus1",num_str @{thm real_mult_minus1}),14.3.03*)
4.294 (*"-1 * z = - z"*)
4.295 Thm ("minus_mult_left",
4.296 - num_str (@{thm real_mult_minus_eq1} RS @{thm sym})),
4.297 + num_str (@{thm minus_mult_left} RS @{thm sym})),
4.298 (*- (?x * ?y) = "- ?x * ?y"*)
4.299 (*Thm ("real_minus_mult_cancel",
4.300 num_str @{thm real_minus_mult_cancel}),
4.301 @@ -929,8 +926,8 @@
4.302 append_rls "discard_parentheses" e_rls
4.303 [Thm ("sym_real_mult_assoc",
4.304 num_str (@{thm real_mult_assoc} RS @{thm sym})),
4.305 - Thm ("sym_real_add_assoc",
4.306 - num_str (@{thm real_add_assoc} RS @{thm sym}))];
4.307 + Thm ("sym_add_assoc",
4.308 + num_str (@{thm add_assoc} RS @{thm sym}))];
4.309
4.310 val scr_make_polynomial =
4.311 "Script Expand_binoms t_ = " ^
4.312 @@ -987,7 +984,7 @@
4.313 }:rls); *)
4.314
4.315 val scr_expand_binoms =
4.316 -"Script Expand_binoms t_ =" ^
4.317 +"Script Expand_binoms t_t =" ^
4.318 "(Repeat " ^
4.319 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
4.320 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
4.321 @@ -1018,7 +1015,10 @@
4.322 " (Try (Repeat (Calculate plus ))) @@ " ^
4.323 " (Try (Repeat (Calculate times ))) @@ " ^
4.324 " (Try (Repeat (Calculate power_)))) " ^
4.325 -" t_)";
4.326 +" t_t)";
4.327 +
4.328 +parse thy scr_expand_binoms;
4.329 +val ---------------------------------------------- = "11111";
4.330
4.331 val expand_binoms =
4.332 Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
4.333 @@ -1027,18 +1027,23 @@
4.334 ("TIMES" , ("op *", eval_binop "#mult_")),
4.335 ("POWER", ("Atools.pow", eval_binop "#power_"))
4.336 ],
4.337 - (*asm_thm = [],*)
4.338 - rules = [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
4.339 + rules = [Thm ("real_plus_binom_pow2",
4.340 + num_str @{thm real_plus_binom_pow2}),
4.341 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
4.342 - Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
4.343 + Thm ("real_plus_binom_times",
4.344 + num_str @{thm real_plus_binom_times}),
4.345 (*"(a + b)*(a + b) = ...*)
4.346 - Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),
4.347 + Thm ("real_minus_binom_pow2",
4.348 + num_str @{thm real_minus_binom_pow2}),
4.349 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
4.350 - Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),
4.351 + Thm ("real_minus_binom_times",
4.352 + num_str @{thm real_minus_binom_times}),
4.353 (*"(a - b)*(a - b) = ...*)
4.354 - Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),
4.355 + Thm ("real_plus_minus_binom1",
4.356 + num_str @{thm real_plus_minus_binom1}),
4.357 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
4.358 - Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),
4.359 + Thm ("real_plus_minus_binom2",
4.360 + num_str @{thm real_plus_minus_binom2}),
4.361 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
4.362 (*RL 020915*)
4.363 Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
4.364 @@ -1049,57 +1054,63 @@
4.365 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
4.366 Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
4.367 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
4.368 - Thm ("realpow_multI",num_str @{thm realpow_multI}),
4.369 + Thm ("realpow_multI",num_str @{thm realpow_multI}),
4.370 (*(a*b)^^^n = a^^^n * b^^^n*)
4.371 Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
4.372 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
4.373 - Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
4.374 + Thm ("real_minus_binom_pow3",
4.375 + num_str @{thm real_minus_binom_pow3}),
4.376 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
4.377
4.378
4.379 - (* Thm ("left_distrib" ,num_str @{thm left_distrib}),
4.380 + (*Thm ("left_distrib" ,num_str @{thm left_distrib}),
4.381 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
4.382 - Thm ("left_distrib2",num_str @{thm left_distrib2}),
4.383 + Thm ("right_distrib",num_str @{thm right_distrib}),
4.384 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
4.385 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
4.386 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
4.387 Thm ("left_diff_distrib2",num_str @{thm left_diff_distrib2}),
4.388 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
4.389 - *)
4.390 -
4.391 - Thm ("mult_1_left",num_str @{thm mult_1_left}), (*"1 * z = z"*)
4.392 - Thm ("mult_zero_left",num_str @{thm mult_zero_left}), (*"0 * z = 0"*)
4.393 + *)
4.394 + Thm ("mult_1_left",num_str @{thm mult_1_left}),
4.395 + (*"1 * z = z"*)
4.396 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
4.397 + (*"0 * z = 0"*)
4.398 Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
4.399
4.400 Calc ("op +", eval_binop "#add_"),
4.401 Calc ("op *", eval_binop "#mult_"),
4.402 Calc ("Atools.pow", eval_binop "#power_"),
4.403 - (*
4.404 - Thm ("real_mult_commute",num_str @{thm real_mult_commute}), (*AC-rewriting*)
4.405 - Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}), (**)
4.406 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}), (**)
4.407 - Thm ("add_commute",num_str @{thm add_commute}), (**)
4.408 - Thm ("add_left_commute",num_str @{thm add_left_commute}), (**)
4.409 - Thm ("add_assoc",num_str @{thm add_assoc}), (**)
4.410 - *)
4.411 -
4.412 + (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
4.413 + (*AC-rewriting*)
4.414 + Thm ("real_mult_left_commute",
4.415 + num_str @{thm real_mult_left_commute}),
4.416 + Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
4.417 + Thm ("add_commute",num_str @{thm add_commute}),
4.418 + Thm ("add_left_commute",num_str @{thm add_left_commute}),
4.419 + Thm ("add_assoc",num_str @{thm add_assoc}),
4.420 + *)
4.421 Thm ("sym_realpow_twoI",
4.422 num_str (@{thm realpow_twoI} RS @{thm sym})),
4.423 (*"r1 * r1 = r1 ^^^ 2"*)
4.424 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
4.425 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
4.426 - (*Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym})),
4.427 + (*Thm ("sym_real_mult_2",
4.428 + num_str (@{thm real_mult_2} RS @{thm sym})),
4.429 (*"z1 + z1 = 2 * z1"*)*)
4.430 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
4.431 (*"z1 + (z1 + k) = 2 * z1 + k"*)
4.432
4.433 Thm ("real_num_collect",num_str @{thm real_num_collect}),
4.434 - (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
4.435 - Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
4.436 - (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
4.437 - Thm ("real_one_collect",num_str @{thm real_one_collect}),
4.438 + (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
4.439 + Thm ("real_num_collect_assoc",
4.440 + num_str @{thm real_num_collect_assoc}),
4.441 + (*"[| l is_const; m is_const |] ==>
4.442 + l * n + (m * n + k) = (l + m) * n + k"*)
4.443 + Thm ("real_one_collect",num_str @{thm real_one_collect}),
4.444 (*"m is_const ==> n + m * n = (1 + m) * n"*)
4.445 - Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
4.446 + Thm ("real_one_collect_assoc",
4.447 + num_str @{thm real_one_collect_assoc}),
4.448 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
4.449
4.450 Calc ("op +", eval_binop "#add_"),
4.451 @@ -1108,9 +1119,7 @@
4.452 ],
4.453 scr = Script ((term_of o the o (parse thy)) scr_expand_binoms)
4.454 }:rls;
4.455 -
4.456 -
4.457 -"******* Poly.ML end ******* ...RL";
4.458 +--------------------------------------------------------------------------*)
4.459
4.460
4.461 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
4.462 @@ -1347,7 +1356,6 @@
4.463 ("TIMES" ,("op *" ,eval_binop "#mult_")),
4.464 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
4.465 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
4.466 - (*asm_thm=[],*)
4.467 scr=Rfuns {init_state = init_state,
4.468 normal_form = normal_form,
4.469 locate_rule = locate_rule,
4.470 @@ -1359,7 +1367,6 @@
4.471 rew_ord = ("dummy_ord", dummy_ord),
4.472 erls = e_rls,srls = Erls,
4.473 calc = [],
4.474 - (*asm_thm = [],*)
4.475 rules = [Rls_ order_mult_
4.476 ], scr = EmptyScr}:rls;
4.477
4.478 @@ -1500,7 +1507,7 @@
4.479
4.480 Thm ("left_distrib" ,num_str @{thm left_distrib}),
4.481 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
4.482 - Thm ("left_distrib2",num_str @{thm left_distrib2}),
4.483 + Thm ("right_distrib",num_str @{thm right_distrib}),
4.484 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
4.485
4.486 Thm ("real_mult_assoc", num_str @{thm real_mult_assoc}),
5.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Sep 01 16:43:58 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Thu Sep 02 15:11:23 2010 +0200
5.3 @@ -97,7 +97,7 @@
5.4 vorzeichen_minus_weg3 "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"
5.5 vorzeichen_minus_weg4 "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"
5.6
5.7 - (*klammer_plus_plus = (real_add_assoc RS sym)*)
5.8 + (*klammer_plus_plus = (add_assoc RS sym)*)
5.9 klammer_plus_minus "a + (b - c) = (a + b) - c"
5.10 klammer_minus_plus "a - (b + c) = (a - b) - c"
5.11 klammer_minus_minus "a - (b - c) = (a - b) + c"
5.12 @@ -317,8 +317,8 @@
5.13 val klammern_aufloesen =
5.14 Rls{id = "klammern_aufloesen", preconds = [],
5.15 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
5.16 - rules = [Thm ("sym_real_add_assoc",
5.17 - num_str (@{thm real_add_assoc} RS @{thm sym})),
5.18 + rules = [Thm ("sym_add_assoc",
5.19 + num_str (@{thm add_assoc} RS @{thm sym})),
5.20 (*"a + (b + c) = (a + b) + c"*)
5.21 Thm ("klammer_plus_minus",num_str @{thm klammer_plus_minus}),
5.22 (*"a + (b - c) = (a + b) - c"*)
5.23 @@ -333,7 +333,7 @@
5.24 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
5.25 rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
5.26 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
5.27 - Thm ("left_distrib2",num_str @{thm left_distrib2}),
5.28 + Thm ("right_distrib",num_str @{thm right_distrib}),
5.29 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
5.30
5.31 Thm ("klammer_mult_minus",num_str @{thm klammer_mult_minus}),
6.1 --- a/src/Tools/isac/Knowledge/Root.thy Wed Sep 01 16:43:58 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Root.thy Thu Sep 02 15:11:23 2010 +0200
6.3 @@ -202,7 +202,7 @@
6.4
6.5 Thm ("left_distrib" ,num_str @{thm left_distrib}),
6.6 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
6.7 - Thm ("left_distrib2",num_str @{thm left_distrib2}),
6.8 + Thm ("right_distrib",num_str @{thm right_distrib}),
6.9 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
6.10 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
6.11 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
7.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Wed Sep 01 16:43:58 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Thu Sep 02 15:11:23 2010 +0200
7.3 @@ -25,7 +25,7 @@
7.4 (*.calculate numeral groundterms.*)
7.5 val calculate_RootRat =
7.6 append_rls "calculate_RootRat" calculate_Rational
7.7 - [Thm ("left_distrib2",num_str @{thm left_distrib}2),
7.8 + [Thm ("right_distrib",num_str @{thm right_distrib}),
7.9 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
7.10 Thm ("mult_1_left",num_str @{thm mult_1_left}),
7.11 (* 1 * z = z *)
8.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Sep 01 16:43:58 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Sep 02 15:11:23 2010 +0200
8.3 @@ -295,7 +295,7 @@
8.4 rew_ord = ("e_rew_ord",e_rew_ord),
8.5 erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
8.6 rules =
8.7 - [Thm ("sym_radd_assoc",num_str (@{thm radd_assoc} RS @{thm sym})),
8.8 + [Thm ("sym_add_assoc",num_str (@{thm add_assoc} RS @{thm sym})),
8.9 Thm ("sym_rmult_assoc",num_str (@{thm rmult_assoc} RS @{thm sym}))],
8.10 scr = Script ((term_of o the o (parse thy))
8.11 "empty_script")
8.12 @@ -307,7 +307,7 @@
8.13 rules =
8.14 [Thm ("radd_commute",num_str @{thm radd_commute}),
8.15 Thm ("radd_left_commute",num_str @{thm radd_left_commute}),
8.16 - Thm ("radd_assoc",num_str @{thm radd_assoc}),
8.17 + Thm ("add_assoc",num_str @{thm add_assoc}),
8.18 Thm ("rmult_commute",num_str @{thm rmult_commute}),
8.19 Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
8.20 Thm ("rmult_assoc",num_str @{thm rmult_assoc})],
8.21 @@ -339,7 +339,7 @@
8.22
8.23 " (Try (Repeat (Rewrite radd_commute False))) @@ " ^
8.24 " (Try (Repeat (Rewrite radd_left_commute False))) @@ " ^
8.25 - " (Try (Repeat (Rewrite radd_assoc False))) @@ " ^
8.26 + " (Try (Repeat (Rewrite add_assoc False))) @@ " ^
8.27 " (Try (Repeat (Rewrite rmult_commute False))) @@ " ^
8.28 " (Try (Repeat (Rewrite rmult_left_commute False))) @@ " ^
8.29 " (Try (Repeat (Rewrite rmult_assoc False))) @@ " ^
8.30 @@ -392,7 +392,7 @@
8.31
8.32 Thm ("radd_commute",num_str @{thm radd_commute}),
8.33 Thm ("radd_left_commute",num_str @{thm radd_left_commute}),
8.34 - Thm ("radd_assoc",num_str @{thm radd_assoc}),
8.35 + Thm ("add_assoc",num_str @{thm add_assoc}),
8.36 Thm ("rmult_commute",num_str @{thm rmult_commute}),
8.37 Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
8.38 Thm ("rmult_assoc",num_str @{thm rmult_assoc}),
8.39 @@ -1267,7 +1267,7 @@
8.40 (*"a - b = a + (-1) * b"*)
8.41 Thm ("left_distrib" ,num_str @{thm left_distrib}),
8.42 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
8.43 - Thm ("left_distrib2",num_str @{thm left_distrib2}),
8.44 + Thm ("right_distrib",num_str @{thm right_distrib}),
8.45 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
8.46 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
8.47 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
8.48 @@ -1366,7 +1366,6 @@
8.49 ("TIMES" , ("op *", eval_binop "#mult_")),
8.50 ("POWER", ("Atools.pow", eval_binop "#power_"))
8.51 ],
8.52 - (*asm_thm = [],*)
8.53 rules = [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
8.54 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
8.55 Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
8.56 @@ -1398,7 +1397,7 @@
8.57
8.58 (* Thm ("left_distrib" ,num_str @{thm left_distrib}}),
8.59 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
8.60 - Thm ("left_distrib2",num_str @{thm left_distrib}2}),
8.61 + Thm ("right_distrib",num_str @{thm right_distrib}),
8.62 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
8.63 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}}),
8.64 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
9.1 --- a/src/Tools/isac/ProgLang/Real2002-theorems.sml Wed Sep 01 16:43:58 2010 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,1005 +0,0 @@
9.4 -(*WN060306 from isabelle-users:
9.5 -put expressions involving plus and minus into a canonical form. Here is a possible set of
9.6 -rules:
9.7 -
9.8 - add_assoc add_commute
9.9 - diff_def minus_add_distrib
9.10 - minus_minus minus_zero
9.11 -===========================================================================*)
9.12 -
9.13 -(*
9.14 - cd ~/Isabelle2002/src/HOL/Real
9.15 - grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml
9.16 - WN 9.8.02
9.17 -
9.18 -ML> thy;
9.19 -val it =
9.20 - {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, Sum_Type,
9.21 - Relation, Record, Inductive, Transitive_Closure, Wellfounded_Recursion,
9.22 - NatDef, Nat, NatArith, Divides, Power, SetInterval, Finite_Set, Equiv,
9.23 - IntDef, Int, Datatype_Universe, Datatype, Numeral, Bin, IntArith,
9.24 - Wellfounded_Relations, Recdef, IntDiv, IntPower, NatBin, NatSimprocs,
9.25 - Relation_Power, PreList, List, Map, Hilbert_Choice, Main, Lubs, PNat, PRat,
9.26 - PReal, RealDef, RealOrd, RealInt, RealBin, RealArith0, RealArith,
9.27 - RComplete, RealAbs, RealPow, Ring_and_Field, Complex_Numbers, Real}
9.28 - : theory
9.29 -
9.30 -theories with their respective theorems found by
9.31 -grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml;
9.32 -theories listed in the the order as found in Real.thy above
9.33 -
9.34 -comments
9.35 - (**)"...theorem..." : first choice for one of the rule-sets
9.36 - "...theorem..."(*??*): to be investigated
9.37 - "...theorem... : just for documenting the contents
9.38 -*)
9.39 -
9.40 -Lubs.ML:qed -----------------------------------------------------------------
9.41 - "setleI"; "ALL y::?'a:?S::?'a set. y <= (?x::?'a) ==> ?S *<= ?x"
9.42 - "setleD"; "[| (?S::?'a set) *<= (?x::?'a); (?y::?'a) : ?S |] ==> ?y <= ?x"
9.43 - "setgeI"; "Ball (?S::?'a set) (op <= (?x::?'a)) ==> ?x <=* ?S"
9.44 - "setgeD"; "[| (?x::?'a) <=* (?S::?'a set); (?y::?'a) : ?S |] ==> ?x <= ?y"
9.45 - "leastPD1";
9.46 - "leastPD2";
9.47 - "leastPD3";
9.48 - "isLubD1";
9.49 - "isLubD1a";
9.50 - "isLub_isUb";
9.51 - "isLubD2";
9.52 - "isLubD3";
9.53 - "isLubI1";
9.54 - "isLubI2";
9.55 - "isUbD";
9.56 - "[| isUb (?R::?'a set) (?S::?'a set) (?x::?'a); (?y::?'a) : ?S |]
9.57 - ==> ?y <= ?x" "isUbD2";
9.58 - "isUbD2a";
9.59 - "isUbI";
9.60 - "isLub_le_isUb";
9.61 - "isLub_ubs";
9.62 -PNat.ML:qed ------------------------------------------------------------------
9.63 - "pnat_fun_mono"; "mono (%X::nat set. {Suc (0::nat)} Un Suc ` X)"
9.64 - "one_RepI"; "Suc (0::nat) : pnat"
9.65 - "pnat_Suc_RepI";
9.66 - "two_RepI";
9.67 - "PNat_induct";
9.68 - "[| (?i::nat) : pnat; (?P::nat => bool) (Suc (0::nat));
9.69 - !!j::nat. [| j : pnat; ?P j |] ==> ?P (Suc j) |] ==> ?P ?i"
9.70 - "pnat_induct";
9.71 - "[| (?P::pnat => bool) (1::pnat); !!n::pnat. ?P n ==> ?P (pSuc n) |]
9.72 - ==> ?P (?n::pnat)"
9.73 - "pnat_diff_induct";
9.74 - "pnatE";
9.75 - "inj_on_Abs_pnat";
9.76 - "inj_Rep_pnat";
9.77 - "zero_not_mem_pnat";
9.78 - "mem_pnat_gt_zero";
9.79 - "gt_0_mem_pnat";
9.80 - "mem_pnat_gt_0_iff";
9.81 - "Rep_pnat_gt_zero";
9.82 - "pnat_add_commute"; "(?x::pnat) + (?y::pnat) = ?y + ?x"
9.83 - "Collect_pnat_gt_0";
9.84 - "pSuc_not_one";
9.85 - "inj_pSuc";
9.86 - "pSuc_pSuc_eq";
9.87 - "n_not_pSuc_n";
9.88 - "not1_implies_pSuc";
9.89 - "pSuc_is_plus_one";
9.90 - "sum_Rep_pnat";
9.91 - "sum_Rep_pnat_sum";
9.92 - "pnat_add_assoc";
9.93 - "pnat_add_left_commute";
9.94 - "pnat_add_left_cancel";
9.95 - "pnat_add_right_cancel";
9.96 - "pnat_no_add_ident";
9.97 - "pnat_less_not_refl";
9.98 - "pnat_less_not_refl2";
9.99 - "Rep_pnat_not_less0";
9.100 - "Rep_pnat_not_less_one";
9.101 - "Rep_pnat_gt_implies_not0";
9.102 - "pnat_less_linear";
9.103 - "Rep_pnat_le_one";
9.104 - "lemma_less_ex_sum_Rep_pnat";
9.105 - "pnat_le_iff_Rep_pnat_le";
9.106 - "pnat_add_left_cancel_le";
9.107 - "pnat_add_left_cancel_less";
9.108 - "pnat_add_lessD1";
9.109 - "pnat_not_add_less1";
9.110 - "pnat_not_add_less2";
9.111 -PNat.ML:qed_spec_mp
9.112 - "pnat_add_leD1";
9.113 - "pnat_add_leD2";
9.114 -PNat.ML:qed
9.115 - "pnat_less_add_eq_less";
9.116 - "pnat_less_iff";
9.117 - "pnat_linear_Ex_eq";
9.118 - "pnat_eq_lessI";
9.119 - "Rep_pnat_mult_1";
9.120 - "Rep_pnat_mult_1_right";
9.121 - "mult_Rep_pnat";
9.122 - "mult_Rep_pnat_mult";
9.123 - "pnat_mult_commute"; "(?m::pnat) * (?n::pnat) = ?n * ?m"
9.124 - "pnat_add_mult_distrib";
9.125 - "pnat_add_mult_distrib2";
9.126 - "pnat_mult_assoc";
9.127 - "pnat_mult_left_commute";
9.128 - "pnat_mult_1";
9.129 - "pnat_mult_1_left";
9.130 - "pnat_mult_less_mono2";
9.131 - "pnat_mult_less_mono1";
9.132 - "pnat_mult_less_cancel2";
9.133 - "pnat_mult_less_cancel1";
9.134 - "pnat_mult_cancel2";
9.135 - "pnat_mult_cancel1";
9.136 - "pnat_same_multI2";
9.137 - "eq_Abs_pnat";
9.138 - "pnat_one_iff";
9.139 - "pnat_two_eq";
9.140 - "inj_pnat_of_nat";
9.141 - "nat_add_one_less";
9.142 - "nat_add_one_less1";
9.143 - "pnat_of_nat_add";
9.144 - "pnat_of_nat_less_iff";
9.145 - "pnat_of_nat_mult";
9.146 -PRat.ML:qed ------------------------------------------------------------------
9.147 - "prat_trans_lemma";
9.148 - "[| (?x1.0::pnat) * (?y2.0::pnat) = (?x2.0::pnat) * (?y1.0::pnat);
9.149 - ?x2.0 * (?y3.0::pnat) = (?x3.0::pnat) * ?y2.0 |]
9.150 - ==> ?x1.0 * ?y3.0 = ?x3.0 * ?y1.0"
9.151 - "ratrel_iff";
9.152 - "ratrelI";
9.153 - "ratrelE_lemma";
9.154 - "ratrelE";
9.155 - "ratrel_refl";
9.156 - "equiv_ratrel";
9.157 - "ratrel_in_prat";
9.158 - "inj_on_Abs_prat";
9.159 - "inj_Rep_prat";
9.160 - "inj_prat_of_pnat";
9.161 - "eq_Abs_prat";
9.162 - "qinv_congruent";
9.163 - "qinv";
9.164 - "qinv_qinv";
9.165 - "inj_qinv";
9.166 - "qinv_1";
9.167 - "prat_add_congruent2_lemma";
9.168 - "prat_add_congruent2";
9.169 - "prat_add";
9.170 - "prat_add_commute";
9.171 - "prat_add_assoc";
9.172 - "prat_add_left_commute";
9.173 - "pnat_mult_congruent2";
9.174 - "prat_mult";
9.175 - "prat_mult_commute";
9.176 - "prat_mult_assoc";
9.177 - "prat_mult_left_commute";
9.178 - "prat_mult_1";
9.179 - "prat_mult_1_right";
9.180 - "prat_of_pnat_add";
9.181 - "prat_of_pnat_mult";
9.182 - "prat_mult_qinv";
9.183 - "prat_mult_qinv_right";
9.184 - "prat_qinv_ex";
9.185 - "prat_qinv_ex1";
9.186 - "prat_qinv_left_ex1";
9.187 - "prat_mult_inv_qinv";
9.188 - "prat_as_inverse_ex";
9.189 - "qinv_mult_eq";
9.190 - "prat_add_mult_distrib";
9.191 - "prat_add_mult_distrib2";
9.192 - "prat_less_iff";
9.193 - "prat_lessI";
9.194 - "prat_lessE_lemma";
9.195 - "prat_lessE";
9.196 - "prat_less_trans";
9.197 - "prat_less_not_refl";
9.198 - "prat_less_not_sym";
9.199 - "lemma_prat_dense";
9.200 - "prat_lemma_dense";
9.201 - "prat_dense";
9.202 - "prat_add_less2_mono1";
9.203 - "prat_add_less2_mono2";
9.204 - "prat_mult_less2_mono1";
9.205 - "prat_mult_left_less2_mono1";
9.206 - "lemma_prat_add_mult_mono";
9.207 - "qless_Ex";
9.208 - "lemma_prat_less_linear";
9.209 - "prat_linear";
9.210 - "prat_linear_less2";
9.211 - "lemma1_qinv_prat_less";
9.212 - "lemma2_qinv_prat_less";
9.213 - "qinv_prat_less";
9.214 - "prat_qinv_gt_1";
9.215 - "prat_qinv_is_gt_1";
9.216 - "prat_less_1_2";
9.217 - "prat_less_qinv_2_1";
9.218 - "prat_mult_qinv_less_1";
9.219 - "prat_self_less_add_self";
9.220 - "prat_self_less_add_right";
9.221 - "prat_self_less_add_left";
9.222 - "prat_self_less_mult_right";
9.223 - "prat_leI";
9.224 - "prat_leD";
9.225 - "prat_less_le_iff";
9.226 - "not_prat_leE";
9.227 - "prat_less_imp_le";
9.228 - "prat_le_imp_less_or_eq";
9.229 - "prat_less_or_eq_imp_le";
9.230 - "prat_le_eq_less_or_eq";
9.231 - "prat_le_refl";
9.232 - "prat_le_less_trans";
9.233 - "prat_le_trans";
9.234 - "not_less_not_eq_prat_less";
9.235 - "prat_add_less_mono";
9.236 - "prat_mult_less_mono";
9.237 - "prat_mult_left_le2_mono1";
9.238 - "prat_mult_le2_mono1";
9.239 - "qinv_prat_le";
9.240 - "prat_add_left_le2_mono1";
9.241 - "prat_add_le2_mono1";
9.242 - "prat_add_le_mono";
9.243 - "prat_add_right_less_cancel";
9.244 - "prat_add_left_less_cancel";
9.245 - "Abs_prat_mult_qinv";
9.246 - "lemma_Abs_prat_le1";
9.247 - "lemma_Abs_prat_le2";
9.248 - "lemma_Abs_prat_le3";
9.249 - "pre_lemma_gleason9_34";
9.250 - "pre_lemma_gleason9_34b";
9.251 - "prat_of_pnat_less_iff";
9.252 - "lemma_prat_less_1_memEx";
9.253 - "lemma_prat_less_1_set_non_empty";
9.254 - "empty_set_psubset_lemma_prat_less_1_set";
9.255 - "lemma_prat_less_1_not_memEx";
9.256 - "lemma_prat_less_1_set_not_rat_set";
9.257 - "lemma_prat_less_1_set_psubset_rat_set";
9.258 - "preal_1";
9.259 - "{x::prat. x < prat_of_pnat (Abs_pnat (Suc (0::nat)))}
9.260 - : {A::prat set.
9.261 - {} < A &
9.262 - A < UNIV &
9.263 - (ALL y::prat:A. (ALL z::prat. z < y --> z : A) & Bex A (op < y))}"
9.264 -PReal.ML:qed -----------------------------------------------------------------
9.265 - "inj_on_Abs_preal"; "inj_on Abs_preal preal"
9.266 - "inj_Rep_preal";
9.267 - "empty_not_mem_preal";
9.268 - "one_set_mem_preal";
9.269 - "preal_psubset_empty";
9.270 - "Rep_preal_psubset_empty";
9.271 - "mem_Rep_preal_Ex";
9.272 - "prealI1";
9.273 - "[| {} < (?A::prat set); ?A < UNIV;
9.274 - ALL y::prat:?A. (ALL z::prat. z < y --> z : ?A) & Bex ?A (op < y) |]
9.275 - ==> ?A : preal"
9.276 - "prealI2";
9.277 - "prealE_lemma";
9.278 - "prealE_lemma1";
9.279 - "prealE_lemma2";
9.280 - "prealE_lemma3";
9.281 - "prealE_lemma3a";
9.282 - "prealE_lemma3b";
9.283 - "prealE_lemma4";
9.284 - "prealE_lemma4a";
9.285 - "not_mem_Rep_preal_Ex";
9.286 - "lemma_prat_less_set_mem_preal";
9.287 - "lemma_prat_set_eq";
9.288 - "inj_preal_of_prat";
9.289 - "not_in_preal_ub";
9.290 - "preal_less_not_refl";
9.291 - "preal_not_refl2";
9.292 - "preal_less_trans";
9.293 - "preal_less_not_sym";
9.294 - "preal_linear";
9.295 - "(?r1.0::preal) < (?r2.0::preal) | ?r1.0 = ?r2.0 | ?r2.0 < ?r1.0"
9.296 - "preal_linear_less2";
9.297 - "preal_add_commute"; "(?x::preal) + (?y::preal) = ?y + ?x"
9.298 - "preal_add_set_not_empty";
9.299 - "preal_not_mem_add_set_Ex";
9.300 - "preal_add_set_not_prat_set";
9.301 - "preal_add_set_lemma3";
9.302 - "preal_add_set_lemma4";
9.303 - "preal_mem_add_set";
9.304 - "preal_add_assoc";
9.305 - "preal_add_left_commute";
9.306 - "preal_mult_commute"; "(?x::preal) * (?y::preal) = ?y * ?x"
9.307 - "preal_mult_set_not_empty";
9.308 - "preal_not_mem_mult_set_Ex";
9.309 - "preal_mult_set_not_prat_set";
9.310 - "preal_mult_set_lemma3";
9.311 - "preal_mult_set_lemma4";
9.312 - "preal_mem_mult_set";
9.313 - "preal_mult_assoc";
9.314 - "preal_mult_left_commute";
9.315 - "preal_mult_1";
9.316 - "preal_mult_1_right";
9.317 - "preal_add_assoc_cong";
9.318 - "preal_add_assoc_swap";
9.319 - "mem_Rep_preal_addD";
9.320 - "mem_Rep_preal_addI";
9.321 - "mem_Rep_preal_add_iff";
9.322 - "mem_Rep_preal_multD";
9.323 - "mem_Rep_preal_multI";
9.324 - "mem_Rep_preal_mult_iff";
9.325 - "lemma_add_mult_mem_Rep_preal";
9.326 - "lemma_add_mult_mem_Rep_preal1";
9.327 - "lemma_preal_add_mult_distrib";
9.328 - "lemma_preal_add_mult_distrib2";
9.329 - "preal_add_mult_distrib2";
9.330 - "preal_add_mult_distrib";
9.331 - "qinv_not_mem_Rep_preal_Ex";
9.332 - "lemma_preal_mem_inv_set_ex";
9.333 - "preal_inv_set_not_empty";
9.334 - "qinv_mem_Rep_preal_Ex";
9.335 - "preal_not_mem_inv_set_Ex";
9.336 - "preal_inv_set_not_prat_set";
9.337 - "preal_inv_set_lemma3";
9.338 - "preal_inv_set_lemma4";
9.339 - "preal_mem_inv_set";
9.340 - "preal_mem_mult_invD";
9.341 - "lemma1_gleason9_34";
9.342 - "lemma1b_gleason9_34";
9.343 - "lemma_gleason9_34a";
9.344 - "lemma_gleason9_34";
9.345 - "lemma1_gleason9_36";
9.346 - "lemma2_gleason9_36";
9.347 - "lemma_gleason9_36";
9.348 - "lemma_gleason9_36a";
9.349 - "preal_mem_mult_invI";
9.350 - "preal_mult_inv";
9.351 - "preal_mult_inv_right";
9.352 - "eq_Abs_preal";
9.353 - "Rep_preal_self_subset";
9.354 - "Rep_preal_sum_not_subset";
9.355 - "Rep_preal_sum_not_eq";
9.356 - "preal_self_less_add_left";
9.357 - "preal_self_less_add_right";
9.358 - "preal_leD";
9.359 - "not_preal_leE";
9.360 - "preal_leI";
9.361 - "preal_less_le_iff";
9.362 - "preal_less_imp_le";
9.363 - "preal_le_imp_less_or_eq";
9.364 - "preal_less_or_eq_imp_le";
9.365 - "preal_le_refl";
9.366 - "preal_le_trans";
9.367 - "preal_le_anti_sym";
9.368 - "preal_neq_iff";
9.369 - "preal_less_le";
9.370 - "lemma_psubset_mem";
9.371 - "lemma_psubset_not_refl";
9.372 - "psubset_trans";
9.373 - "subset_psubset_trans";
9.374 - "subset_psubset_trans2";
9.375 - "psubsetD";
9.376 - "lemma_ex_mem_less_left_add1";
9.377 - "preal_less_set_not_empty";
9.378 - "lemma_ex_not_mem_less_left_add1";
9.379 - "preal_less_set_not_prat_set";
9.380 - "preal_less_set_lemma3";
9.381 - "preal_less_set_lemma4";
9.382 - "preal_mem_less_set";
9.383 - "preal_less_add_left_subsetI";
9.384 - "lemma_sum_mem_Rep_preal_ex";
9.385 - "preal_less_add_left_subsetI2";
9.386 - "preal_less_add_left";
9.387 - "preal_less_add_left_Ex";
9.388 - "preal_add_less2_mono1";
9.389 - "preal_add_less2_mono2";
9.390 - "preal_mult_less_mono1";
9.391 - "preal_mult_left_less_mono1";
9.392 - "preal_mult_left_le_mono1";
9.393 - "preal_mult_le_mono1";
9.394 - "preal_add_left_le_mono1";
9.395 - "preal_add_le_mono1";
9.396 - "preal_add_right_less_cancel";
9.397 - "preal_add_left_less_cancel";
9.398 - "preal_add_less_iff1";
9.399 - "preal_add_less_iff2";
9.400 - "preal_add_less_mono";
9.401 - "preal_mult_less_mono";
9.402 - "preal_add_right_cancel";
9.403 - "preal_add_left_cancel";
9.404 - "preal_add_left_cancel_iff";
9.405 - "preal_add_right_cancel_iff";
9.406 - "preal_sup_mem_Ex";
9.407 - "preal_sup_set_not_empty";
9.408 - "preal_sup_not_mem_Ex";
9.409 - "preal_sup_not_mem_Ex1";
9.410 - "preal_sup_set_not_prat_set";
9.411 - "preal_sup_set_not_prat_set1";
9.412 - "preal_sup_set_lemma3";
9.413 - "preal_sup_set_lemma3_1";
9.414 - "preal_sup_set_lemma4";
9.415 - "preal_sup_set_lemma4_1";
9.416 - "preal_sup";
9.417 - "preal_sup1";
9.418 - "preal_psup_leI";
9.419 - "preal_psup_leI2";
9.420 - "preal_psup_leI2b";
9.421 - "preal_psup_leI2a";
9.422 - "psup_le_ub";
9.423 - "psup_le_ub1";
9.424 - "preal_complete";
9.425 - "lemma_preal_rat_less";
9.426 - "lemma_preal_rat_less2";
9.427 - "preal_of_prat_add";
9.428 - "lemma_preal_rat_less3";
9.429 - "lemma_preal_rat_less4";
9.430 - "preal_of_prat_mult";
9.431 - "preal_of_prat_less_iff"; "(preal_of_prat ?p < preal_of_prat ?q) = (?p < ?q)"
9.432 -RealDef.ML:qed ---------------------------------------------------------------
9.433 - "preal_trans_lemma";
9.434 - "realrel_iff";
9.435 - "realrelI";
9.436 - "?x1.0 + ?y2.0 = ?x2.0 + ?y1.0 ==> ((?x1.0, ?y1.0), ?x2.0, ?y2.0) : realrel"
9.437 - "realrelE_lemma";
9.438 - "realrelE";
9.439 - "realrel_refl";
9.440 - "equiv_realrel";
9.441 - "realrel_in_real";
9.442 - "inj_on_Abs_REAL";
9.443 - "inj_Rep_REAL";
9.444 - "inj_real_of_preal";
9.445 - "eq_Abs_REAL";
9.446 - "real_minus_congruent";
9.447 - "real_minus";
9.448 - "- Abs_REAL (realrel `` {(?x, ?y)}) = Abs_REAL (realrel `` {(?y, ?x)})"
9.449 - "minus_minus"; (**)"- (- (?z::real)) = ?z"
9.450 - "inj_real_minus"; "inj uminus"
9.451 - "real_minus_zero"; (**)"- 0 = 0"
9.452 - "real_minus_zero_iff"; (**)"(- ?x = 0) = (?x = 0)"
9.453 - "real_add_congruent2";
9.454 - "congruent2 realrel
9.455 - (%p1 p2. (%(x1, y1). (%(x2, y2). realrel `` {(x1 + x2, y1 + y2)}) p2) p1)"
9.456 - "real_add";
9.457 - "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) +
9.458 - Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =
9.459 - Abs_REAL (realrel `` {(?x1.0 + ?x2.0, ?y1.0 + ?y2.0)})"
9.460 - "add_commute"; (**)"(?z::real) + (?w::real) = ?w + ?z"
9.461 - "add_assoc"; (**)
9.462 - "add_left_commute"; (**)
9.463 - "add_0_left"; (**)"0 + ?z = ?z"
9.464 - "add_0_right"; (**)
9.465 - "right_minus"; (**)"?z + - ?z = 0"
9.466 - "right_minus_left"; (**)
9.467 - "right_minus_cancel"; (**)"?z + (- ?z + ?w) = ?w"
9.468 - "real_minus_add_cancel"; (**)"- ?z + (?z + ?w) = ?w"
9.469 - "real_minus_ex"; "EX y. ?x + y = 0"
9.470 - "real_minus_ex1";
9.471 - "real_minus_left_ex1"; "EX! y. y + ?x = 0"
9.472 - "right_minus_eq_minus";"?x + ?y = 0 ==> ?x = - ?y"
9.473 - "real_as_add_inverse_ex"; "EX y. ?x = - y"
9.474 - "real_minus_add_distrib"; (**)"- (?x + ?y) = - ?x + - ?y"
9.475 - "real_add_left_cancel"; "(?x + ?y = ?x + ?z) = (?y = ?z)"
9.476 - "real_add_right_cancel"; "(?y + ?x = ?z + ?x) = (?y = ?z)"
9.477 - "real_diff_0"; (**)"0 - ?x = - ?x"
9.478 - "real_diff_0_right"; (**)"?x - 0 = ?x"
9.479 - "real_diff_self"; (**)"?x - ?x = 0"
9.480 - "real_mult_congruent2_lemma";
9.481 - "real_mult_congruent2";
9.482 - "congruent2 realrel
9.483 - (%p1 p2.
9.484 - (%(x1, y1).
9.485 - (%(x2, y2). realrel `` {(x1 * x2 + y1 * y2, x1 * y2 + x2 * y1)})
9.486 - p2) p1)"
9.487 - "real_mult";
9.488 - "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) *
9.489 - Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =
9.490 - Abs_REAL
9.491 - (realrel ``
9.492 - {(?x1.0 * ?x2.0 + ?y1.0 * ?y2.0, ?x1.0 * ?y2.0 + ?x2.0 * ?y1.0)})"
9.493 - "real_mult_commute"; (**)"?z * ?w = ?w * ?z"
9.494 - "real_mult_assoc"; (**)
9.495 - "real_mult_left_commute";
9.496 - (**)"?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"
9.497 - "mult_1_left"; (**)"1 * ?z = ?z"
9.498 - "mult_1_right"; (**)"?z * 1 = ?z"
9.499 - "mult_zero_left"; (**)
9.500 - "mult_zero_left_right"; (**)"?z * 0 = 0"
9.501 - "real_mult_minus_eq1"; (**)"- ?x * ?y = - (?x * ?y)"
9.502 - "real_mult_minus_eq2"; (**)"?x * - ?y = - (?x * ?y)"
9.503 - "real_mult_minus_1"; (**)"- 1 * ?z = - ?z"
9.504 - "real_mult_minus_1_right";(**)"?z * - 1 = - ?z"
9.505 - "real_minus_mult_cancel"; (**)"- ?x * - ?y = ?x * ?y"
9.506 - "real_minus_mult_commute";(**)"- ?x * ?y = ?x * - ?y"
9.507 - "add_assoc_cong";
9.508 - "?z + ?v = ?z' + ?v' ==> ?z + (?v + ?w) = ?z' + (?v' + ?w)"
9.509 - "add_assoc_swap"; (**)"?z + (?v + ?w) = ?v + (?z + ?w)"
9.510 - "left_distrib"; (**)"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"
9.511 - "left_distrib2"; (**)"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"
9.512 - "left_diff_distrib"; (**)"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"
9.513 - "left_diff_distrib2";(**)"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"
9.514 - "real_zero_not_eq_one";
9.515 - "real_zero_iff"; "0 = Abs_REAL (realrel `` {(?x, ?x)})"
9.516 - "real_mult_inv_right_ex"; "?x ~= 0 ==> EX y. ?x * y = 1"
9.517 - "real_mult_inv_left_ex"; "?x ~= 0 ==> inverse ?x * ?x = 1"
9.518 - "real_mult_inv_left";
9.519 - "real_mult_inv_right"; "?x ~= 0 ==> ?x * inverse ?x = 1"
9.520 - "INVERSE_ZERO"; "inverse 0 = 0"
9.521 - "DIVISION_BY_ZERO"; (*NOT for adding to default simpset*)"?a / 0 = 0"
9.522 - "real_mult_left_cancel"; (**)"?c ~= 0 ==> (?c * ?a = ?c * ?b) = (?a = ?b)"
9.523 - "real_mult_right_cancel"; (**)"?c ~= 0 ==> (?a * ?c = ?b * ?c) = (?a = ?b)"
9.524 - "real_mult_left_cancel_ccontr"; "?c * ?a ~= ?c * ?b ==> ?a ~= ?b"
9.525 - "real_mult_right_cancel_ccontr"; "?a * ?c ~= ?b * ?c ==> ?a ~= ?b"
9.526 - "real_inverse_not_zero"; "?x ~= 0 ==> inverse ?x ~= 0"
9.527 - "real_mult_not_zero"; "[| ?x ~= 0; ?y ~= 0 |] ==> ?x * ?y ~= 0"
9.528 - "real_inverse_inverse"; "inverse (inverse ?x) = ?x"
9.529 - "real_inverse_1"; "inverse 1 = 1"
9.530 - "real_minus_inverse"; "inverse (- ?x) = - inverse ?x"
9.531 - "real_inverse_distrib"; "inverse (?x * ?y) = inverse ?x * inverse ?y"
9.532 - "times_divide_eq_right"; (**)"?x * (?y / ?z) = ?x * ?y / ?z"
9.533 - "times_divide_eq_left"; (**)"?y / ?z * ?x = ?y * ?x / ?z"
9.534 - "divide_divide_eq_right"; (**)"?x / (?y / ?z) = ?x * ?z / ?y"
9.535 - "divide_divide_eq_left"; (**)"?x / ?y / ?z = ?x / (?y * ?z)"
9.536 - "real_minus_divide_eq"; (**)"- ?x / ?y = - (?x / ?y)"
9.537 - "real_divide_minus_eq"; (**)"?x / - ?y = - (?x / ?y)"
9.538 - "nadd_divide_distrib"; (**)"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
9.539 - "preal_lemma_eq_rev_sum";
9.540 - "[| ?x = ?y; ?x1.0 = ?y1.0 |] ==> ?x + ?y1.0 = ?x1.0 + ?y"
9.541 - "preal_add_left_commute_cancel";
9.542 - "?x + (?b + ?y) = ?x1.0 + (?b + ?y1.0) ==> ?x + ?y = ?x1.0 + ?y1.0"
9.543 - "preal_lemma_for_not_refl";
9.544 - "real_less_not_refl"; "~ ?R < ?R"
9.545 - "real_not_refl2";
9.546 - "preal_lemma_trans";
9.547 - "real_less_trans";
9.548 - "real_less_not_sym";
9.549 - "real_of_preal_add";
9.550 - "real_of_preal (?z1.0 + ?z2.0) = real_of_preal ?z1.0 + real_of_preal ?z2.0"
9.551 - "real_of_preal_mult";
9.552 - "real_of_preal_ExI";
9.553 - "real_of_preal_ExD";
9.554 - "real_of_preal_iff";
9.555 - "real_of_preal_trichotomy";
9.556 - "real_of_preal_trichotomyE";
9.557 - "real_of_preal_lessD";
9.558 - "real_of_preal_lessI";
9.559 - "?m1.0 < ?m2.0 ==> real_of_preal ?m1.0 < real_of_preal ?m2.0"
9.560 - "real_of_preal_less_iff1";
9.561 - "real_of_preal_minus_less_self";
9.562 - "real_of_preal_minus_less_zero";
9.563 - "real_of_preal_not_minus_gt_zero";
9.564 - "real_of_preal_zero_less";
9.565 - "real_of_preal_not_less_zero";
9.566 - "minus_minus_zero_less";
9.567 - "real_of_preal_sum_zero_less";
9.568 - "real_of_preal_minus_less_all";
9.569 - "real_of_preal_not_minus_gt_all";
9.570 - "real_of_preal_minus_less_rev1";
9.571 - "real_of_preal_minus_less_rev2";
9.572 - "real_of_preal_minus_less_rev_iff";
9.573 - "real_linear"; "?R1.0 < ?R2.0 | ?R1.0 = ?R2.0 | ?R2.0 < ?R1.0"
9.574 - "real_neq_iff";
9.575 - "real_linear_less2";
9.576 - "[| ?R1.0 < ?R2.0 ==> ?P; ?R1.0 = ?R2.0 ==> ?P; ?R2.0 < ?R1.0 ==> ?P |]
9.577 - ==> ?P"
9.578 - "real_leI";
9.579 - "real_leD"; "~ ?w < ?z ==> ?z <= ?w"
9.580 - "real_less_le_iff";
9.581 - "not_real_leE";
9.582 - "real_le_imp_less_or_eq";
9.583 - "real_less_or_eq_imp_le";
9.584 - "real_le_less";
9.585 - "real_le_refl"; "?w <= ?w"
9.586 - "real_le_linear";
9.587 - "real_le_trans"; "[| ?i <= ?j; ?j <= ?k |] ==> ?i <= ?k"
9.588 - "real_le_anti_sym"; "[| ?z <= ?w; ?w <= ?z |] ==> ?z = ?w"
9.589 - "not_less_not_eq_real_less";
9.590 - "real_less_le"; "(?w < ?z) = (?w <= ?z & ?w ~= ?z)"
9.591 - "real_minus_zero_less_iff";
9.592 - "real_minus_zero_less_iff2";
9.593 - "real_less_add_positive_left_Ex";
9.594 - "real_less_sum_gt_zero"; "?W < ?S ==> 0 < ?S + - ?W"
9.595 - "real_lemma_change_eq_subj";
9.596 - "real_sum_gt_zero_less"; "0 < ?S + - ?W ==> ?W < ?S"
9.597 - "real_less_sum_gt_0_iff"; "(0 < ?S + - ?W) = (?W < ?S)"
9.598 - "real_less_eq_diff"; "(?x < ?y) = (?x - ?y < 0)"
9.599 - "real_add_diff_eq"; (**)"?x + (?y - ?z) = ?x + ?y - ?z"
9.600 - "real_diff_add_eq"; (**)"?x - ?y + ?z = ?x + ?z - ?y"
9.601 - "real_diff_diff_eq"; (**)"?x - ?y - ?z = ?x - (?y + ?z)"
9.602 - "real_diff_diff_eq2"; (**)"?x - (?y - ?z) = ?x + ?z - ?y"
9.603 - "real_diff_less_eq"; "(?x - ?y < ?z) = (?x < ?z + ?y)"
9.604 - "real_less_diff_eq";
9.605 - "real_diff_le_eq"; "(?x - ?y <= ?z) = (?x <= ?z + ?y)"
9.606 - "real_le_diff_eq";
9.607 - "real_diff_eq_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)"
9.608 - "real_eq_diff_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)"
9.609 - "real_less_eqI";
9.610 - "real_le_eqI";
9.611 - "real_eq_eqI"; "?x - ?y = ?x' - ?y' ==> (?x = ?y) = (?x' = ?y')"
9.612 -RealOrd.ML:qed ---------------------------------------------------------------
9.613 - "real_add_cancel_21"; "(?x + (?y + ?z) = ?y + ?u) = (?x + ?z = ?u)"
9.614 - "real_add_cancel_end"; "(?x + (?y + ?z) = ?y) = (?x = - ?z)"
9.615 - "real_minus_diff_eq"; (*??*)"- (?x - ?y) = ?y - ?x"
9.616 - "real_gt_zero_preal_Ex";
9.617 - "real_gt_preal_preal_Ex";
9.618 - "real_ge_preal_preal_Ex";
9.619 - "real_less_all_preal"; "?y <= 0 ==> ALL x. ?y < real_of_preal x"
9.620 - "real_less_all_real2";
9.621 - "real_lemma_add_positive_imp_less";
9.622 - "real_ex_add_positive_left_less";"EX T. 0 < T & ?R + T = ?S ==> ?R < ?S"
9.623 - "real_less_iff_add";
9.624 - "real_of_preal_le_iff";
9.625 - "real_mult_order"; "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x * ?y"
9.626 - "neg_real_mult_order";
9.627 - "real_mult_less_0"; "[| 0 < ?x; ?y < 0 |] ==> ?x * ?y < 0"
9.628 - "real_zero_less_one"; "0 < 1"
9.629 - "real_add_right_cancel_less"; "(?v + ?z < ?w + ?z) = (?v < ?w)"
9.630 - "real_add_left_cancel_less";
9.631 - "real_add_right_cancel_le";
9.632 - "real_add_left_cancel_le";
9.633 - "real_add_less_le_mono"; "[| ?w' < ?w; ?z' <= ?z |] ==> ?w' + ?z' < ?w + ?z"
9.634 - "real_add_le_less_mono"; "[| ?w' <= ?w; ?z' < ?z |] ==> ?w' + ?z' < ?w + ?z"
9.635 - "real_add_less_mono2";
9.636 - "real_less_add_right_cancel";
9.637 - "real_less_add_left_cancel"; "?C + ?A < ?C + ?B ==> ?A < ?B"
9.638 - "real_le_add_right_cancel";
9.639 - "real_le_add_left_cancel"; "?C + ?A <= ?C + ?B ==> ?A <= ?B"
9.640 - "real_add_order"; "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x + ?y"
9.641 - "real_le_add_order";
9.642 - "real_add_less_mono";
9.643 - "real_add_left_le_mono1";
9.644 - "real_add_le_mono";
9.645 - "real_less_Ex";
9.646 - "right_minus_positive_less_self"; "0 < ?r ==> ?u + - ?r < ?u"
9.647 - "real_le_minus_iff"; "(- ?s <= - ?r) = (?r <= ?s)"
9.648 - "real_le_square";
9.649 - "real_of_posnat_one";
9.650 - "real_of_posnat_two";
9.651 - "real_of_posnat_add"; "real_of_posnat ?n1.0 + real_of_posnat ?n2.0 =
9.652 - real_of_posnat (?n1.0 + ?n2.0) + 1"
9.653 - "real_of_posnat_add_one";
9.654 - "real_of_posnat_Suc";
9.655 - "inj_real_of_posnat";
9.656 - "real_of_nat_zero";
9.657 - "real_of_nat_one"; "real (Suc 0) = 1"
9.658 - "real_of_nat_add";
9.659 - "real_of_nat_Suc";
9.660 - "real_of_nat_less_iff";
9.661 - "real_of_nat_le_iff";
9.662 - "inj_real_of_nat";
9.663 - "real_of_nat_ge_zero";
9.664 - "real_of_nat_mult";
9.665 - "real_of_nat_inject";
9.666 -RealOrd.ML:qed_spec_mp
9.667 - "real_of_nat_diff";
9.668 -RealOrd.ML:qed
9.669 - "real_of_nat_zero_iff";
9.670 - "real_of_nat_neg_int";
9.671 - "real_inverse_gt_0";
9.672 - "real_inverse_less_0";
9.673 - "real_mult_less_mono1";
9.674 - "real_mult_less_mono2";
9.675 - "real_mult_less_cancel1";
9.676 - "(?k * ?m < ?k * ?n) = (0 < ?k & ?m < ?n | ?k < 0 & ?n < ?m)"
9.677 - "real_mult_less_cancel2";
9.678 - "real_mult_less_iff1";
9.679 - "real_mult_less_iff2";
9.680 - "real_mult_le_cancel_iff1";
9.681 - "real_mult_le_cancel_iff2";
9.682 - "real_mult_le_less_mono1";
9.683 - "real_mult_less_mono";
9.684 - "real_mult_less_mono'";
9.685 - "real_gt_zero"; "1 <= ?x ==> 0 < ?x"
9.686 - "real_mult_self_le"; "[| 1 < ?r; 1 <= ?x |] ==> ?x <= ?r * ?x"
9.687 - "real_mult_self_le2";
9.688 - "real_inverse_less_swap";
9.689 - "real_mult_is_0";
9.690 - "real_inverse_add";
9.691 - "real_minus_zero_le_iff";
9.692 - "real_minus_zero_le_iff2";
9.693 - "real_sum_squares_cancel"; "?x * ?x + ?y * ?y = 0 ==> ?x = 0"
9.694 - "real_sum_squares_cancel2"; "?x * ?x + ?y * ?y = 0 ==> ?y = 0"
9.695 - "real_0_less_mult_iff";
9.696 - "real_0_le_mult_iff";
9.697 - "real_mult_less_0_iff"; "(?x * ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)"
9.698 - "real_mult_le_0_iff";
9.699 -RealInt.ML:qed ---------------------------------------------------------------
9.700 - "real_of_int_congruent";
9.701 - "real_of_int"; "real (Abs_Integ (intrel `` {(?i, ?j)})) =
9.702 - Abs_REAL
9.703 - (realrel ``
9.704 - {(preal_of_prat (prat_of_pnat (pnat_of_nat ?i)),
9.705 - preal_of_prat (prat_of_pnat (pnat_of_nat ?j)))})"
9.706 - "inj_real_of_int";
9.707 - "real_of_int_zero";
9.708 - "real_of_one";
9.709 - "real_of_int_add"; "real ?x + real ?y = real (?x + ?y)"
9.710 - "real_of_int_minus";
9.711 - "real_of_int_diff";
9.712 - "real_of_int_mult"; "real ?x * real ?y = real (?x * ?y)"
9.713 - "real_of_int_Suc";
9.714 - "real_of_int_real_of_nat";
9.715 - "real_of_nat_real_of_int";
9.716 - "real_of_int_zero_cancel";
9.717 - "real_of_int_less_cancel";
9.718 - "real_of_int_inject";
9.719 - "real_of_int_less_mono";
9.720 - "real_of_int_less_iff";
9.721 - "real_of_int_le_iff";
9.722 -RealBin.ML:qed ---------------------------------------------------------------
9.723 - "real_number_of"; "real (number_of ?w) = number_of ?w"
9.724 - "real_numeral_0_eq_0";
9.725 - "real_numeral_1_eq_1";
9.726 - "add_real_number_of";
9.727 - "minus_real_number_of";
9.728 - "diff_real_number_of";
9.729 - "mult_real_number_of";
9.730 - "real_mult_2"; (**)"2 * ?z = ?z + ?z"
9.731 - "real_mult_2_right"; (**)"?z * 2 = ?z + ?z"
9.732 - "eq_real_number_of";
9.733 - "less_real_number_of";
9.734 - "le_real_number_of_eq_not_less";
9.735 - "real_minus_1_eq_m1"; "- 1 = -1"(*uminus.. = "-.."*)
9.736 - "real_mult_minus1"; (**)"-1 * ?z = - ?z"
9.737 - "real_mult_minus1_right"; (**)"?z * -1 = - ?z"
9.738 - "zero_less_real_of_nat_iff";"(0 < real ?n) = (0 < ?n)"
9.739 - "zero_le_real_of_nat_iff";
9.740 - "real_add_number_of_left";
9.741 - "real_mult_number_of_left";
9.742 - "number_of ?v * (number_of ?w * ?z) = number_of (bin_mult ?v ?w) * ?z"
9.743 - "real_add_number_of_diff1";
9.744 - "real_add_number_of_diff2";"number_of ?v + (?c - number_of ?w) =
9.745 - number_of (bin_add ?v (bin_minus ?w)) + ?c"
9.746 - "real_of_nat_number_of";
9.747 - "real (number_of ?v) = (if neg (number_of ?v) then 0 else number_of ?v)"
9.748 - "real_less_iff_diff_less_0"; "(?x < ?y) = (?x - ?y < 0)"
9.749 - "real_eq_iff_diff_eq_0";
9.750 - "real_le_iff_diff_le_0";
9.751 - "left_real_add_mult_distrib";
9.752 - (**)"?i * ?u + (?j * ?u + ?k) = (?i + ?j) * ?u + ?k"
9.753 - "real_eq_add_iff1";
9.754 - "(?i * ?u + ?m = ?j * ?u + ?n) = ((?i - ?j) * ?u + ?m = ?n)"
9.755 - "real_eq_add_iff2";
9.756 - "real_less_add_iff1";
9.757 - "real_less_add_iff2";
9.758 - "real_le_add_iff1";
9.759 - "real_le_add_iff2";
9.760 - "real_mult_le_mono1";
9.761 - "real_mult_le_mono2";
9.762 - "real_mult_le_mono";
9.763 - "[| ?i <= ?j; ?k <= ?l; 0 <= ?j; 0 <= ?k |] ==> ?i * ?k <= ?j * ?l"
9.764 -RealArith0.ML:qed ------------------------------------------------------------
9.765 - "real_diff_minus_eq"; (**)"?x - - ?y = ?x + ?y"
9.766 - "divide_zero_left"; (**)"0 / ?x = 0"
9.767 - "real_0_less_inverse_iff"; "(0 < inverse ?x) = (0 < ?x)"
9.768 - "real_inverse_less_0_iff";
9.769 - "real_0_le_inverse_iff";
9.770 - "real_inverse_le_0_iff";
9.771 - "REAL_DIVIDE_ZERO"; "?x / 0 = 0"(*!!!*)
9.772 - "real_inverse_eq_divide";
9.773 - "real_0_less_divide_iff";"(0 < ?x / ?y) = (0 < ?x & 0 < ?y | ?x < 0 & ?y < 0)"
9.774 - "real_divide_less_0_iff";"(?x / ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)"
9.775 - "real_0_le_divide_iff";
9.776 - "real_divide_le_0_iff";
9.777 - "(?x / ?y <= 0) = ((?x <= 0 | ?y <= 0) & (0 <= ?x | 0 <= ?y))"
9.778 - "real_inverse_zero_iff";
9.779 - "real_divide_eq_0_iff"; "(?x / ?y = 0) = (?x = 0 | ?y = 0)"(*!!!*)
9.780 - "real_divide_self_eq"; "?h ~= 0 ==> ?h / ?h = 1"(**)
9.781 - "real_minus_less_minus"; "(- ?y < - ?x) = (?x < ?y)"
9.782 - "real_mult_less_mono1_neg"; "[| ?i < ?j; ?k < 0 |] ==> ?j * ?k < ?i * ?k"
9.783 - "real_mult_less_mono2_neg";
9.784 - "real_mult_le_mono1_neg";
9.785 - "real_mult_le_mono2_neg";
9.786 - "real_mult_less_cancel2";
9.787 - "real_mult_le_cancel2";
9.788 - "real_mult_less_cancel1";
9.789 - "real_mult_le_cancel1";
9.790 - "real_mult_eq_cancel1"; "(?k * ?m = ?k * ?n) = (?k = 0 | ?m = ?n)"
9.791 - "real_mult_eq_cancel2"; "(?m * ?k = ?n * ?k) = (?k = 0 | ?m = ?n)"
9.792 - "real_mult_div_cancel1"; (**)"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"
9.793 - "real_mult_div_cancel_disj";
9.794 - "?k * ?m / (?k * ?n) = (if ?k = 0 then 0 else ?m / ?n)"
9.795 - "pos_real_le_divide_eq";
9.796 - "neg_real_le_divide_eq";
9.797 - "pos_real_divide_le_eq";
9.798 - "neg_real_divide_le_eq";
9.799 - "pos_real_less_divide_eq";
9.800 - "neg_real_less_divide_eq";
9.801 - "pos_real_divide_less_eq";
9.802 - "neg_real_divide_less_eq";
9.803 - "real_eq_divide_eq"; (**)"?z ~= 0 ==> (?x = ?y / ?z) = (?x * ?z = ?y)"
9.804 - "real_divide_eq_eq"; (**)"?z ~= 0 ==> (?y / ?z = ?x) = (?y = ?x * ?z)"
9.805 - "real_divide_eq_cancel2"; "(?m / ?k = ?n / ?k) = (?k = 0 | ?m = ?n)"
9.806 - "real_divide_eq_cancel1"; "(?k / ?m = ?k / ?n) = (?k = 0 | ?m = ?n)"
9.807 - "real_inverse_less_iff";
9.808 - "real_inverse_le_iff";
9.809 - "divide_1"; (**)"?x / 1 = ?x"
9.810 - "real_divide_minus1"; (**)"?x / -1 = - ?x"
9.811 - "real_minus1_divide"; (**)"-1 / ?x = - (1 / ?x)"
9.812 - "real_lbound_gt_zero";
9.813 - "[| 0 < ?d1.0; 0 < ?d2.0 |] ==> EX e. 0 < e & e < ?d1.0 & e < ?d2.0"
9.814 - "real_inverse_eq_iff"; "(inverse ?x = inverse ?y) = (?x = ?y)"
9.815 - "real_divide_eq_iff"; "(?z / ?x = ?z / ?y) = (?z = 0 | ?x = ?y)"
9.816 - "real_less_minus"; "(?x < - ?y) = (?y < - ?x)"
9.817 - "real_minus_less"; "(- ?x < ?y) = (- ?y < ?x)"
9.818 - "real_le_minus";
9.819 - "real_minus_le"; "(- ?x <= ?y) = (- ?y <= ?x)"
9.820 - "real_equation_minus"; (**)"(?x = - ?y) = (?y = - ?x)"
9.821 - "real_minus_equation"; (**)"(- ?x = ?y) = (- ?y = ?x)"
9.822 - "right_minus_iff"; (**)"(?x + - ?a = 0) = (?x = ?a)"
9.823 - "real_minus_eq_cancel"; (**)"(- ?b = - ?a) = (?b = ?a)"
9.824 - "real_add_eq_0_iff"; (**)"(?x + ?y = 0) = (?y = - ?x)"
9.825 - "real_add_less_0_iff"; "(?x + ?y < 0) = (?y < - ?x)"
9.826 - "real_0_less_add_iff";
9.827 - "real_add_le_0_iff";
9.828 - "real_0_le_add_iff";
9.829 - "real_0_less_diff_iff"; "(0 < ?x - ?y) = (?y < ?x)"
9.830 - "real_0_le_diff_iff";
9.831 - "real_minus_diff_eq"; (**)"- (?x - ?y) = ?y - ?x"
9.832 - "real_less_half_sum"; "?x < ?y ==> ?x < (?x + ?y) / 2"
9.833 - "real_gt_half_sum";
9.834 - "real_dense"; "?x < ?y ==> EX r. ?x < r & r < ?y"
9.835 -RealArith ///!!!///-----------------------------------------------------------
9.836 -RComplete.ML:qed -------------------------------------------------------------
9.837 - "real_sum_of_halves"; (**)"?x / 2 + ?x / 2 = ?x"
9.838 - "real_sup_lemma1";
9.839 - "real_sup_lemma2";
9.840 - "posreal_complete";
9.841 - "real_isLub_unique";
9.842 - "real_order_restrict";
9.843 - "posreals_complete";
9.844 - "real_sup_lemma3";
9.845 - "lemma_le_swap2";
9.846 - "lemma_real_complete2b";
9.847 - "reals_complete";
9.848 - "real_of_nat_Suc_gt_zero";
9.849 - "reals_Archimedean"; "0 < ?x ==> EX n. inverse (real (Suc n)) < ?x"
9.850 - "reals_Archimedean2";
9.851 -RealAbs.ML:qed
9.852 - "abs_nat_number_of";
9.853 - "abs (number_of ?v) =
9.854 - (if neg (number_of ?v) then number_of (bin_minus ?v) else number_of ?v)"
9.855 - "abs_split";
9.856 - "abs_iff";
9.857 - "abs_zero"; "abs 0 = 0"
9.858 - "abs_one";
9.859 - "abs_eqI1";
9.860 - "abs_eqI2";
9.861 - "abs_minus_eqI2";
9.862 - "abs_minus_eqI1";
9.863 - "abs_ge_zero"; "0 <= abs ?x"
9.864 - "abs_idempotent"; "abs (abs ?x) = abs ?x"
9.865 - "abs_zero_iff"; "(abs ?x = 0) = (?x = 0)"
9.866 - "abs_ge_self"; "?x <= abs ?x"
9.867 - "abs_ge_minus_self";
9.868 - "abs_mult"; "abs (?x * ?y) = abs ?x * abs ?y"
9.869 - "abs_inverse"; "abs (inverse ?x) = inverse (abs ?x)"
9.870 - "abs_mult_inverse";
9.871 - "abs_triangle_ineq"; "abs (?x + ?y) <= abs ?x + abs ?y"
9.872 - "abs_triangle_ineq_four";
9.873 - "abs_minus_cancel";
9.874 - "abs_minus_add_cancel";
9.875 - "abs_triangle_minus_ineq";
9.876 -RealAbs.ML:qed_spec_mp
9.877 - "abs_add_less"; "[| abs ?x < ?r; abs ?y < ?s |] ==> abs (?x + ?y) < ?r + ?s"
9.878 -RealAbs.ML:qed
9.879 - "abs_add_minus_less";
9.880 - "mult_zero_left_less"; "(0 * ?x < ?r) = (0 < ?r)"
9.881 - "real_mult_less_trans";
9.882 - "real_mult_le_less_trans";
9.883 - "abs_mult_less";
9.884 - "abs_mult_less2";
9.885 - "abs_less_gt_zero";
9.886 - "abs_minus_one"; "abs -1 = 1"
9.887 - "abs_disj"; "abs ?x = ?x | abs ?x = - ?x"
9.888 - "abs_interval_iff";
9.889 - "abs_le_interval_iff";
9.890 - "abs_add_pos_gt_zero";
9.891 - "abs_add_one_gt_zero";
9.892 - "abs_not_less_zero";
9.893 - "abs_circle"; "abs ?h < abs ?y - abs ?x ==> abs (?x + ?h) < abs ?y"
9.894 - "abs_le_zero_iff";
9.895 - "real_0_less_abs_iff";
9.896 - "abs_real_of_nat_cancel";
9.897 - "abs_add_one_not_less_self";
9.898 - "abs_triangle_ineq_three"; "abs (?w + ?x + ?y) <= abs ?w + abs ?x + abs ?y"
9.899 - "abs_diff_less_imp_gt_zero";
9.900 - "abs_diff_less_imp_gt_zero2";
9.901 - "abs_diff_less_imp_gt_zero3";
9.902 - "abs_diff_less_imp_gt_zero4";
9.903 - "abs_triangle_ineq_minus_cancel";
9.904 - "abs_sum_triangle_ineq";
9.905 - "abs (?x + ?y + (- ?l + - ?m)) <= abs (?x + - ?l) + abs (?y + - ?m)"
9.906 -RealPow.ML:qed
9.907 - "realpow_zero"; "0 ^ Suc ?n = 0"
9.908 -RealPow.ML:qed_spec_mp
9.909 - "realpow_not_zero"; "?r ~= 0 ==> ?r ^ ?n ~= 0"
9.910 - "realpow_zero_zero"; "?r ^ ?n = 0 ==> ?r = 0"
9.911 - "realpow_inverse"; "inverse (?r ^ ?n) = inverse ?r ^ ?n"
9.912 - "realpow_abs"; "abs (?r ^ ?n) = abs ?r ^ ?n"
9.913 - "realpow_add"; (**)"?r ^ (?n + ?m) = ?r ^ ?n * ?r ^ ?m"
9.914 - "realpow_one"; (**)"?r ^ 1 = ?r"
9.915 - "realpow_two"; (**)"?r ^ Suc (Suc 0) = ?r * ?r"
9.916 -RealPow.ML:qed_spec_mp
9.917 - "realpow_gt_zero"; "0 < ?r ==> 0 < ?r ^ ?n"
9.918 - "realpow_ge_zero"; "0 <= ?r ==> 0 <= ?r ^ ?n"
9.919 - "realpow_le"; "0 <= ?x & ?x <= ?y ==> ?x ^ ?n <= ?y ^ ?n"
9.920 - "realpow_less";
9.921 -RealPow.ML:qed
9.922 - "realpow_eq_one"; (**)"1 ^ ?n = 1"
9.923 - "abs_realpow_minus_one"; "abs (-1 ^ ?n) = 1"
9.924 - "realpow_mult"; (**)"(?r * ?s) ^ ?n = ?r ^ ?n * ?s ^ ?n"
9.925 - "realpow_two_le"; "0 <= ?r ^ Suc (Suc 0)"
9.926 - "abs_realpow_two";
9.927 - "realpow_two_abs"; "abs ?x ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)"
9.928 - "realpow_two_gt_one";
9.929 -RealPow.ML:qed_spec_mp
9.930 - "realpow_ge_one"; "1 < ?r ==> 1 <= ?r ^ ?n"
9.931 -RealPow.ML:qed
9.932 - "realpow_ge_one2";
9.933 - "two_realpow_ge_one";
9.934 - "two_realpow_gt";
9.935 - "realpow_minus_one"; (**)"-1 ^ (2 * ?n) = 1"
9.936 - "realpow_minus_one_odd"; "-1 ^ Suc (2 * ?n) = - 1"
9.937 - "realpow_minus_one_even";
9.938 -RealPow.ML:qed_spec_mp
9.939 - "realpow_Suc_less";
9.940 - "realpow_Suc_le"; "0 <= ?r & ?r < 1 ==> ?r ^ Suc ?n <= ?r ^ ?n"
9.941 -RealPow.ML:qed
9.942 - "realpow_zero_le"; "0 <= 0 ^ ?n"
9.943 -RealPow.ML:qed_spec_mp
9.944 - "realpow_Suc_le2";
9.945 -RealPow.ML:qed
9.946 - "realpow_Suc_le3";
9.947 -RealPow.ML:qed_spec_mp
9.948 - "realpow_less_le"; "0 <= ?r & ?r < 1 & ?n < ?N ==> ?r ^ ?N <= ?r ^ ?n"
9.949 -RealPow.ML:qed
9.950 - "realpow_le_le"; "[| 0 <= ?r; ?r < 1; ?n <= ?N |] ==> ?r ^ ?N <= ?r ^ ?n"
9.951 - "realpow_Suc_le_self";
9.952 - "realpow_Suc_less_one";
9.953 -RealPow.ML:qed_spec_mp
9.954 - "realpow_le_Suc";
9.955 - "realpow_less_Suc";
9.956 - "realpow_le_Suc2";
9.957 - "realpow_gt_ge";
9.958 - "realpow_gt_ge2";
9.959 -RealPow.ML:qed
9.960 - "realpow_ge_ge"; "[| 1 < ?r; ?n <= ?N |] ==> ?r ^ ?n <= ?r ^ ?N"
9.961 - "realpow_ge_ge2";
9.962 -RealPow.ML:qed_spec_mp
9.963 - "realpow_Suc_ge_self";
9.964 - "realpow_Suc_ge_self2";
9.965 -RealPow.ML:qed
9.966 - "realpow_ge_self";
9.967 - "realpow_ge_self2";
9.968 -RealPow.ML:qed_spec_mp
9.969 - "realpow_minus_mult"; "0 < ?n ==> ?x ^ (?n - 1) * ?x = ?x ^ ?n"
9.970 - "realpow_two_mult_inverse";
9.971 - "?r ~= 0 ==> ?r * inverse ?r ^ Suc (Suc 0) = inverse ?r"
9.972 - "realpow_two_minus"; "(- ?x) ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)"
9.973 - "realpow_two_diff";
9.974 - "realpow_two_disj";
9.975 - "realpow_diff";
9.976 - "[| ?x ~= 0; ?m <= ?n |] ==> ?x ^ (?n - ?m) = ?x ^ ?n * inverse (?x ^ ?m)"
9.977 - "realpow_real_of_nat";
9.978 - "realpow_real_of_nat_two_pos"; "0 < real (Suc (Suc 0) ^ ?n)"
9.979 -RealPow.ML:qed_spec_mp
9.980 - "realpow_increasing";
9.981 - "realpow_Suc_cancel_eq";
9.982 - "[| 0 <= ?x; 0 <= ?y; ?x ^ Suc ?n = ?y ^ Suc ?n |] ==> ?x = ?y"
9.983 -RealPow.ML:qed
9.984 - "realpow_eq_0_iff"; "(?x ^ ?n = 0) = (?x = 0 & 0 < ?n)"
9.985 - "zero_less_realpow_abs_iff";
9.986 - "zero_le_realpow_abs";
9.987 - "real_of_int_power"; "real ?x ^ ?n = real (?x ^ ?n)"
9.988 - "power_real_number_of"; "number_of ?v ^ ?n = real (number_of ?v ^ ?n)"
9.989 -Ring_and_Field ---///!!!///---------------------------------------------------
9.990 -Complex_Numbers --///!!!///---------------------------------------------------
9.991 -Real -------------///!!!///---------------------------------------------------
9.992 -real_arith0.ML:qed "";
9.993 -real_arith0.ML:qed "";
9.994 -real_arith0.ML:qed "";
9.995 -real_arith0.ML:qed "";
9.996 -real_arith0.ML:qed "";
9.997 -real_arith0.ML:qed "";
9.998 -real_arith0.ML:qed "";
9.999 -real_arith0.ML:qed "";
9.1000 -real_arith0.ML:qed "";
9.1001 -
9.1002 -
9.1003 -
9.1004 -
9.1005 -
9.1006 -
9.1007 -
9.1008 -
10.1 --- a/test/Tools/isac/Knowledge/poly.sml Wed Sep 01 16:43:58 2010 +0200
10.2 +++ b/test/Tools/isac/Knowledge/poly.sml Thu Sep 02 15:11:23 2010 +0200
10.3 @@ -13,6 +13,7 @@
10.4 "-----------------------------------------------------------------";
10.5 "table of contents -----------------------------------------------";
10.6 "-----------------------------------------------------------------";
10.7 +"-------- build Script Expand_binoms -----------------------------";
10.8 "-------- investigate new uniary minus ---------------------------";
10.9 "-------- Bsple aus Schalk I -------------------------------------";
10.10 "-------- Script 'simplification for_polynomials' ----------------";
10.11 @@ -25,6 +26,50 @@
10.12 "-----------------------------------------------------------------";
10.13
10.14
10.15 +"-------- build Script Expand_binoms -----------------------------";
10.16 +"-------- build Script Expand_binoms -----------------------------";
10.17 +"-------- build Script Expand_binoms -----------------------------";
10.18 +val scr_expand_binoms =
10.19 +"Script Expand_binoms t_t =" ^
10.20 +"(Repeat " ^
10.21 +"((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
10.22 +" (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
10.23 +" (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
10.24 +" (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
10.25 +" (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
10.26 +" (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
10.27 +
10.28 +" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
10.29 +" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
10.30 +" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
10.31 +
10.32 +" (Try (Repeat (Calculate plus ))) @@ " ^
10.33 +" (Try (Repeat (Calculate times ))) @@ " ^
10.34 +" (Try (Repeat (Calculate power_))) @@ " ^
10.35 +
10.36 +" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
10.37 +" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
10.38 +" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
10.39 +" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
10.40 +
10.41 +" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
10.42 +" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
10.43 +
10.44 +" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
10.45 +" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
10.46 +
10.47 +" (Try (Repeat (Calculate plus ))) @@ " ^
10.48 +" (Try (Repeat (Calculate times ))) @@ " ^
10.49 +" (Try (Repeat (Calculate power_)))) " ^
10.50 +" t_t)";
10.51 +val scr_expand_binoms =
10.52 +"Script Expand_binoms t_t = t_t";
10.53 +
10.54 +val ---------------------------------------------- = "11111";
10.55 +parse thy scr_expand_binoms;
10.56 +val ---------------------------------------------- = "22222";
10.57 +(*----------------------------------------------
10.58 +
10.59 "-------- investigate new uniary minus ---------------------------";
10.60 "-------- investigate new uniary minus ---------------------------";
10.61 "-------- investigate new uniary minus ---------------------------";
10.62 @@ -420,4 +465,4 @@
10.63 val t2 = str2term "3 * a + (2 * b + 3 * b)";
10.64
10.65
10.66 -
10.67 +----------------------------------------------*)