1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/ProgLang/Real2002-theorems.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,1005 @@
1.4 +(*WN060306 from isabelle-users:
1.5 +put expressions involving plus and minus into a canonical form. Here is a possible set of
1.6 +rules:
1.7 +
1.8 + add_assoc add_commute
1.9 + diff_def minus_add_distrib
1.10 + minus_minus minus_zero
1.11 +===========================================================================*)
1.12 +
1.13 +(*
1.14 + cd ~/Isabelle2002/src/HOL/Real
1.15 + grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml
1.16 + WN 9.8.02
1.17 +
1.18 +ML> thy;
1.19 +val it =
1.20 + {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, Sum_Type,
1.21 + Relation, Record, Inductive, Transitive_Closure, Wellfounded_Recursion,
1.22 + NatDef, Nat, NatArith, Divides, Power, SetInterval, Finite_Set, Equiv,
1.23 + IntDef, Int, Datatype_Universe, Datatype, Numeral, Bin, IntArith,
1.24 + Wellfounded_Relations, Recdef, IntDiv, IntPower, NatBin, NatSimprocs,
1.25 + Relation_Power, PreList, List, Map, Hilbert_Choice, Main, Lubs, PNat, PRat,
1.26 + PReal, RealDef, RealOrd, RealInt, RealBin, RealArith0, RealArith,
1.27 + RComplete, RealAbs, RealPow, Ring_and_Field, Complex_Numbers, Real}
1.28 + : theory
1.29 +
1.30 +theories with their respective theorems found by
1.31 +grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml;
1.32 +theories listed in the the order as found in Real.thy above
1.33 +
1.34 +comments
1.35 + (**)"...theorem..." : first choice for one of the rule-sets
1.36 + "...theorem..."(*??*): to be investigated
1.37 + "...theorem... : just for documenting the contents
1.38 +*)
1.39 +
1.40 +Lubs.ML:qed -----------------------------------------------------------------
1.41 + "setleI"; "ALL y::?'a:?S::?'a set. y <= (?x::?'a) ==> ?S *<= ?x"
1.42 + "setleD"; "[| (?S::?'a set) *<= (?x::?'a); (?y::?'a) : ?S |] ==> ?y <= ?x"
1.43 + "setgeI"; "Ball (?S::?'a set) (op <= (?x::?'a)) ==> ?x <=* ?S"
1.44 + "setgeD"; "[| (?x::?'a) <=* (?S::?'a set); (?y::?'a) : ?S |] ==> ?x <= ?y"
1.45 + "leastPD1";
1.46 + "leastPD2";
1.47 + "leastPD3";
1.48 + "isLubD1";
1.49 + "isLubD1a";
1.50 + "isLub_isUb";
1.51 + "isLubD2";
1.52 + "isLubD3";
1.53 + "isLubI1";
1.54 + "isLubI2";
1.55 + "isUbD";
1.56 + "[| isUb (?R::?'a set) (?S::?'a set) (?x::?'a); (?y::?'a) : ?S |]
1.57 + ==> ?y <= ?x" "isUbD2";
1.58 + "isUbD2a";
1.59 + "isUbI";
1.60 + "isLub_le_isUb";
1.61 + "isLub_ubs";
1.62 +PNat.ML:qed ------------------------------------------------------------------
1.63 + "pnat_fun_mono"; "mono (%X::nat set. {Suc (0::nat)} Un Suc ` X)"
1.64 + "one_RepI"; "Suc (0::nat) : pnat"
1.65 + "pnat_Suc_RepI";
1.66 + "two_RepI";
1.67 + "PNat_induct";
1.68 + "[| (?i::nat) : pnat; (?P::nat => bool) (Suc (0::nat));
1.69 + !!j::nat. [| j : pnat; ?P j |] ==> ?P (Suc j) |] ==> ?P ?i"
1.70 + "pnat_induct";
1.71 + "[| (?P::pnat => bool) (1::pnat); !!n::pnat. ?P n ==> ?P (pSuc n) |]
1.72 + ==> ?P (?n::pnat)"
1.73 + "pnat_diff_induct";
1.74 + "pnatE";
1.75 + "inj_on_Abs_pnat";
1.76 + "inj_Rep_pnat";
1.77 + "zero_not_mem_pnat";
1.78 + "mem_pnat_gt_zero";
1.79 + "gt_0_mem_pnat";
1.80 + "mem_pnat_gt_0_iff";
1.81 + "Rep_pnat_gt_zero";
1.82 + "pnat_add_commute"; "(?x::pnat) + (?y::pnat) = ?y + ?x"
1.83 + "Collect_pnat_gt_0";
1.84 + "pSuc_not_one";
1.85 + "inj_pSuc";
1.86 + "pSuc_pSuc_eq";
1.87 + "n_not_pSuc_n";
1.88 + "not1_implies_pSuc";
1.89 + "pSuc_is_plus_one";
1.90 + "sum_Rep_pnat";
1.91 + "sum_Rep_pnat_sum";
1.92 + "pnat_add_assoc";
1.93 + "pnat_add_left_commute";
1.94 + "pnat_add_left_cancel";
1.95 + "pnat_add_right_cancel";
1.96 + "pnat_no_add_ident";
1.97 + "pnat_less_not_refl";
1.98 + "pnat_less_not_refl2";
1.99 + "Rep_pnat_not_less0";
1.100 + "Rep_pnat_not_less_one";
1.101 + "Rep_pnat_gt_implies_not0";
1.102 + "pnat_less_linear";
1.103 + "Rep_pnat_le_one";
1.104 + "lemma_less_ex_sum_Rep_pnat";
1.105 + "pnat_le_iff_Rep_pnat_le";
1.106 + "pnat_add_left_cancel_le";
1.107 + "pnat_add_left_cancel_less";
1.108 + "pnat_add_lessD1";
1.109 + "pnat_not_add_less1";
1.110 + "pnat_not_add_less2";
1.111 +PNat.ML:qed_spec_mp
1.112 + "pnat_add_leD1";
1.113 + "pnat_add_leD2";
1.114 +PNat.ML:qed
1.115 + "pnat_less_add_eq_less";
1.116 + "pnat_less_iff";
1.117 + "pnat_linear_Ex_eq";
1.118 + "pnat_eq_lessI";
1.119 + "Rep_pnat_mult_1";
1.120 + "Rep_pnat_mult_1_right";
1.121 + "mult_Rep_pnat";
1.122 + "mult_Rep_pnat_mult";
1.123 + "pnat_mult_commute"; "(?m::pnat) * (?n::pnat) = ?n * ?m"
1.124 + "pnat_add_mult_distrib";
1.125 + "pnat_add_mult_distrib2";
1.126 + "pnat_mult_assoc";
1.127 + "pnat_mult_left_commute";
1.128 + "pnat_mult_1";
1.129 + "pnat_mult_1_left";
1.130 + "pnat_mult_less_mono2";
1.131 + "pnat_mult_less_mono1";
1.132 + "pnat_mult_less_cancel2";
1.133 + "pnat_mult_less_cancel1";
1.134 + "pnat_mult_cancel2";
1.135 + "pnat_mult_cancel1";
1.136 + "pnat_same_multI2";
1.137 + "eq_Abs_pnat";
1.138 + "pnat_one_iff";
1.139 + "pnat_two_eq";
1.140 + "inj_pnat_of_nat";
1.141 + "nat_add_one_less";
1.142 + "nat_add_one_less1";
1.143 + "pnat_of_nat_add";
1.144 + "pnat_of_nat_less_iff";
1.145 + "pnat_of_nat_mult";
1.146 +PRat.ML:qed ------------------------------------------------------------------
1.147 + "prat_trans_lemma";
1.148 + "[| (?x1.0::pnat) * (?y2.0::pnat) = (?x2.0::pnat) * (?y1.0::pnat);
1.149 + ?x2.0 * (?y3.0::pnat) = (?x3.0::pnat) * ?y2.0 |]
1.150 + ==> ?x1.0 * ?y3.0 = ?x3.0 * ?y1.0"
1.151 + "ratrel_iff";
1.152 + "ratrelI";
1.153 + "ratrelE_lemma";
1.154 + "ratrelE";
1.155 + "ratrel_refl";
1.156 + "equiv_ratrel";
1.157 + "ratrel_in_prat";
1.158 + "inj_on_Abs_prat";
1.159 + "inj_Rep_prat";
1.160 + "inj_prat_of_pnat";
1.161 + "eq_Abs_prat";
1.162 + "qinv_congruent";
1.163 + "qinv";
1.164 + "qinv_qinv";
1.165 + "inj_qinv";
1.166 + "qinv_1";
1.167 + "prat_add_congruent2_lemma";
1.168 + "prat_add_congruent2";
1.169 + "prat_add";
1.170 + "prat_add_commute";
1.171 + "prat_add_assoc";
1.172 + "prat_add_left_commute";
1.173 + "pnat_mult_congruent2";
1.174 + "prat_mult";
1.175 + "prat_mult_commute";
1.176 + "prat_mult_assoc";
1.177 + "prat_mult_left_commute";
1.178 + "prat_mult_1";
1.179 + "prat_mult_1_right";
1.180 + "prat_of_pnat_add";
1.181 + "prat_of_pnat_mult";
1.182 + "prat_mult_qinv";
1.183 + "prat_mult_qinv_right";
1.184 + "prat_qinv_ex";
1.185 + "prat_qinv_ex1";
1.186 + "prat_qinv_left_ex1";
1.187 + "prat_mult_inv_qinv";
1.188 + "prat_as_inverse_ex";
1.189 + "qinv_mult_eq";
1.190 + "prat_add_mult_distrib";
1.191 + "prat_add_mult_distrib2";
1.192 + "prat_less_iff";
1.193 + "prat_lessI";
1.194 + "prat_lessE_lemma";
1.195 + "prat_lessE";
1.196 + "prat_less_trans";
1.197 + "prat_less_not_refl";
1.198 + "prat_less_not_sym";
1.199 + "lemma_prat_dense";
1.200 + "prat_lemma_dense";
1.201 + "prat_dense";
1.202 + "prat_add_less2_mono1";
1.203 + "prat_add_less2_mono2";
1.204 + "prat_mult_less2_mono1";
1.205 + "prat_mult_left_less2_mono1";
1.206 + "lemma_prat_add_mult_mono";
1.207 + "qless_Ex";
1.208 + "lemma_prat_less_linear";
1.209 + "prat_linear";
1.210 + "prat_linear_less2";
1.211 + "lemma1_qinv_prat_less";
1.212 + "lemma2_qinv_prat_less";
1.213 + "qinv_prat_less";
1.214 + "prat_qinv_gt_1";
1.215 + "prat_qinv_is_gt_1";
1.216 + "prat_less_1_2";
1.217 + "prat_less_qinv_2_1";
1.218 + "prat_mult_qinv_less_1";
1.219 + "prat_self_less_add_self";
1.220 + "prat_self_less_add_right";
1.221 + "prat_self_less_add_left";
1.222 + "prat_self_less_mult_right";
1.223 + "prat_leI";
1.224 + "prat_leD";
1.225 + "prat_less_le_iff";
1.226 + "not_prat_leE";
1.227 + "prat_less_imp_le";
1.228 + "prat_le_imp_less_or_eq";
1.229 + "prat_less_or_eq_imp_le";
1.230 + "prat_le_eq_less_or_eq";
1.231 + "prat_le_refl";
1.232 + "prat_le_less_trans";
1.233 + "prat_le_trans";
1.234 + "not_less_not_eq_prat_less";
1.235 + "prat_add_less_mono";
1.236 + "prat_mult_less_mono";
1.237 + "prat_mult_left_le2_mono1";
1.238 + "prat_mult_le2_mono1";
1.239 + "qinv_prat_le";
1.240 + "prat_add_left_le2_mono1";
1.241 + "prat_add_le2_mono1";
1.242 + "prat_add_le_mono";
1.243 + "prat_add_right_less_cancel";
1.244 + "prat_add_left_less_cancel";
1.245 + "Abs_prat_mult_qinv";
1.246 + "lemma_Abs_prat_le1";
1.247 + "lemma_Abs_prat_le2";
1.248 + "lemma_Abs_prat_le3";
1.249 + "pre_lemma_gleason9_34";
1.250 + "pre_lemma_gleason9_34b";
1.251 + "prat_of_pnat_less_iff";
1.252 + "lemma_prat_less_1_memEx";
1.253 + "lemma_prat_less_1_set_non_empty";
1.254 + "empty_set_psubset_lemma_prat_less_1_set";
1.255 + "lemma_prat_less_1_not_memEx";
1.256 + "lemma_prat_less_1_set_not_rat_set";
1.257 + "lemma_prat_less_1_set_psubset_rat_set";
1.258 + "preal_1";
1.259 + "{x::prat. x < prat_of_pnat (Abs_pnat (Suc (0::nat)))}
1.260 + : {A::prat set.
1.261 + {} < A &
1.262 + A < UNIV &
1.263 + (ALL y::prat:A. (ALL z::prat. z < y --> z : A) & Bex A (op < y))}"
1.264 +PReal.ML:qed -----------------------------------------------------------------
1.265 + "inj_on_Abs_preal"; "inj_on Abs_preal preal"
1.266 + "inj_Rep_preal";
1.267 + "empty_not_mem_preal";
1.268 + "one_set_mem_preal";
1.269 + "preal_psubset_empty";
1.270 + "Rep_preal_psubset_empty";
1.271 + "mem_Rep_preal_Ex";
1.272 + "prealI1";
1.273 + "[| {} < (?A::prat set); ?A < UNIV;
1.274 + ALL y::prat:?A. (ALL z::prat. z < y --> z : ?A) & Bex ?A (op < y) |]
1.275 + ==> ?A : preal"
1.276 + "prealI2";
1.277 + "prealE_lemma";
1.278 + "prealE_lemma1";
1.279 + "prealE_lemma2";
1.280 + "prealE_lemma3";
1.281 + "prealE_lemma3a";
1.282 + "prealE_lemma3b";
1.283 + "prealE_lemma4";
1.284 + "prealE_lemma4a";
1.285 + "not_mem_Rep_preal_Ex";
1.286 + "lemma_prat_less_set_mem_preal";
1.287 + "lemma_prat_set_eq";
1.288 + "inj_preal_of_prat";
1.289 + "not_in_preal_ub";
1.290 + "preal_less_not_refl";
1.291 + "preal_not_refl2";
1.292 + "preal_less_trans";
1.293 + "preal_less_not_sym";
1.294 + "preal_linear";
1.295 + "(?r1.0::preal) < (?r2.0::preal) | ?r1.0 = ?r2.0 | ?r2.0 < ?r1.0"
1.296 + "preal_linear_less2";
1.297 + "preal_add_commute"; "(?x::preal) + (?y::preal) = ?y + ?x"
1.298 + "preal_add_set_not_empty";
1.299 + "preal_not_mem_add_set_Ex";
1.300 + "preal_add_set_not_prat_set";
1.301 + "preal_add_set_lemma3";
1.302 + "preal_add_set_lemma4";
1.303 + "preal_mem_add_set";
1.304 + "preal_add_assoc";
1.305 + "preal_add_left_commute";
1.306 + "preal_mult_commute"; "(?x::preal) * (?y::preal) = ?y * ?x"
1.307 + "preal_mult_set_not_empty";
1.308 + "preal_not_mem_mult_set_Ex";
1.309 + "preal_mult_set_not_prat_set";
1.310 + "preal_mult_set_lemma3";
1.311 + "preal_mult_set_lemma4";
1.312 + "preal_mem_mult_set";
1.313 + "preal_mult_assoc";
1.314 + "preal_mult_left_commute";
1.315 + "preal_mult_1";
1.316 + "preal_mult_1_right";
1.317 + "preal_add_assoc_cong";
1.318 + "preal_add_assoc_swap";
1.319 + "mem_Rep_preal_addD";
1.320 + "mem_Rep_preal_addI";
1.321 + "mem_Rep_preal_add_iff";
1.322 + "mem_Rep_preal_multD";
1.323 + "mem_Rep_preal_multI";
1.324 + "mem_Rep_preal_mult_iff";
1.325 + "lemma_add_mult_mem_Rep_preal";
1.326 + "lemma_add_mult_mem_Rep_preal1";
1.327 + "lemma_preal_add_mult_distrib";
1.328 + "lemma_preal_add_mult_distrib2";
1.329 + "preal_add_mult_distrib2";
1.330 + "preal_add_mult_distrib";
1.331 + "qinv_not_mem_Rep_preal_Ex";
1.332 + "lemma_preal_mem_inv_set_ex";
1.333 + "preal_inv_set_not_empty";
1.334 + "qinv_mem_Rep_preal_Ex";
1.335 + "preal_not_mem_inv_set_Ex";
1.336 + "preal_inv_set_not_prat_set";
1.337 + "preal_inv_set_lemma3";
1.338 + "preal_inv_set_lemma4";
1.339 + "preal_mem_inv_set";
1.340 + "preal_mem_mult_invD";
1.341 + "lemma1_gleason9_34";
1.342 + "lemma1b_gleason9_34";
1.343 + "lemma_gleason9_34a";
1.344 + "lemma_gleason9_34";
1.345 + "lemma1_gleason9_36";
1.346 + "lemma2_gleason9_36";
1.347 + "lemma_gleason9_36";
1.348 + "lemma_gleason9_36a";
1.349 + "preal_mem_mult_invI";
1.350 + "preal_mult_inv";
1.351 + "preal_mult_inv_right";
1.352 + "eq_Abs_preal";
1.353 + "Rep_preal_self_subset";
1.354 + "Rep_preal_sum_not_subset";
1.355 + "Rep_preal_sum_not_eq";
1.356 + "preal_self_less_add_left";
1.357 + "preal_self_less_add_right";
1.358 + "preal_leD";
1.359 + "not_preal_leE";
1.360 + "preal_leI";
1.361 + "preal_less_le_iff";
1.362 + "preal_less_imp_le";
1.363 + "preal_le_imp_less_or_eq";
1.364 + "preal_less_or_eq_imp_le";
1.365 + "preal_le_refl";
1.366 + "preal_le_trans";
1.367 + "preal_le_anti_sym";
1.368 + "preal_neq_iff";
1.369 + "preal_less_le";
1.370 + "lemma_psubset_mem";
1.371 + "lemma_psubset_not_refl";
1.372 + "psubset_trans";
1.373 + "subset_psubset_trans";
1.374 + "subset_psubset_trans2";
1.375 + "psubsetD";
1.376 + "lemma_ex_mem_less_left_add1";
1.377 + "preal_less_set_not_empty";
1.378 + "lemma_ex_not_mem_less_left_add1";
1.379 + "preal_less_set_not_prat_set";
1.380 + "preal_less_set_lemma3";
1.381 + "preal_less_set_lemma4";
1.382 + "preal_mem_less_set";
1.383 + "preal_less_add_left_subsetI";
1.384 + "lemma_sum_mem_Rep_preal_ex";
1.385 + "preal_less_add_left_subsetI2";
1.386 + "preal_less_add_left";
1.387 + "preal_less_add_left_Ex";
1.388 + "preal_add_less2_mono1";
1.389 + "preal_add_less2_mono2";
1.390 + "preal_mult_less_mono1";
1.391 + "preal_mult_left_less_mono1";
1.392 + "preal_mult_left_le_mono1";
1.393 + "preal_mult_le_mono1";
1.394 + "preal_add_left_le_mono1";
1.395 + "preal_add_le_mono1";
1.396 + "preal_add_right_less_cancel";
1.397 + "preal_add_left_less_cancel";
1.398 + "preal_add_less_iff1";
1.399 + "preal_add_less_iff2";
1.400 + "preal_add_less_mono";
1.401 + "preal_mult_less_mono";
1.402 + "preal_add_right_cancel";
1.403 + "preal_add_left_cancel";
1.404 + "preal_add_left_cancel_iff";
1.405 + "preal_add_right_cancel_iff";
1.406 + "preal_sup_mem_Ex";
1.407 + "preal_sup_set_not_empty";
1.408 + "preal_sup_not_mem_Ex";
1.409 + "preal_sup_not_mem_Ex1";
1.410 + "preal_sup_set_not_prat_set";
1.411 + "preal_sup_set_not_prat_set1";
1.412 + "preal_sup_set_lemma3";
1.413 + "preal_sup_set_lemma3_1";
1.414 + "preal_sup_set_lemma4";
1.415 + "preal_sup_set_lemma4_1";
1.416 + "preal_sup";
1.417 + "preal_sup1";
1.418 + "preal_psup_leI";
1.419 + "preal_psup_leI2";
1.420 + "preal_psup_leI2b";
1.421 + "preal_psup_leI2a";
1.422 + "psup_le_ub";
1.423 + "psup_le_ub1";
1.424 + "preal_complete";
1.425 + "lemma_preal_rat_less";
1.426 + "lemma_preal_rat_less2";
1.427 + "preal_of_prat_add";
1.428 + "lemma_preal_rat_less3";
1.429 + "lemma_preal_rat_less4";
1.430 + "preal_of_prat_mult";
1.431 + "preal_of_prat_less_iff"; "(preal_of_prat ?p < preal_of_prat ?q) = (?p < ?q)"
1.432 +RealDef.ML:qed ---------------------------------------------------------------
1.433 + "preal_trans_lemma";
1.434 + "realrel_iff";
1.435 + "realrelI";
1.436 + "?x1.0 + ?y2.0 = ?x2.0 + ?y1.0 ==> ((?x1.0, ?y1.0), ?x2.0, ?y2.0) : realrel"
1.437 + "realrelE_lemma";
1.438 + "realrelE";
1.439 + "realrel_refl";
1.440 + "equiv_realrel";
1.441 + "realrel_in_real";
1.442 + "inj_on_Abs_REAL";
1.443 + "inj_Rep_REAL";
1.444 + "inj_real_of_preal";
1.445 + "eq_Abs_REAL";
1.446 + "real_minus_congruent";
1.447 + "real_minus";
1.448 + "- Abs_REAL (realrel `` {(?x, ?y)}) = Abs_REAL (realrel `` {(?y, ?x)})"
1.449 + "real_minus_minus"; (**)"- (- (?z::real)) = ?z"
1.450 + "inj_real_minus"; "inj uminus"
1.451 + "real_minus_zero"; (**)"- 0 = 0"
1.452 + "real_minus_zero_iff"; (**)"(- ?x = 0) = (?x = 0)"
1.453 + "real_add_congruent2";
1.454 + "congruent2 realrel
1.455 + (%p1 p2. (%(x1, y1). (%(x2, y2). realrel `` {(x1 + x2, y1 + y2)}) p2) p1)"
1.456 + "real_add";
1.457 + "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) +
1.458 + Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =
1.459 + Abs_REAL (realrel `` {(?x1.0 + ?x2.0, ?y1.0 + ?y2.0)})"
1.460 + "real_add_commute"; (**)"(?z::real) + (?w::real) = ?w + ?z"
1.461 + "real_add_assoc"; (**)
1.462 + "real_add_left_commute"; (**)
1.463 + "real_add_zero_left"; (**)"0 + ?z = ?z"
1.464 + "real_add_zero_right"; (**)
1.465 + "real_add_minus"; (**)"?z + - ?z = 0"
1.466 + "real_add_minus_left"; (**)
1.467 + "real_add_minus_cancel"; (**)"?z + (- ?z + ?w) = ?w"
1.468 + "real_minus_add_cancel"; (**)"- ?z + (?z + ?w) = ?w"
1.469 + "real_minus_ex"; "EX y. ?x + y = 0"
1.470 + "real_minus_ex1";
1.471 + "real_minus_left_ex1"; "EX! y. y + ?x = 0"
1.472 + "real_add_minus_eq_minus";"?x + ?y = 0 ==> ?x = - ?y"
1.473 + "real_as_add_inverse_ex"; "EX y. ?x = - y"
1.474 + "real_minus_add_distrib"; (**)"- (?x + ?y) = - ?x + - ?y"
1.475 + "real_add_left_cancel"; "(?x + ?y = ?x + ?z) = (?y = ?z)"
1.476 + "real_add_right_cancel"; "(?y + ?x = ?z + ?x) = (?y = ?z)"
1.477 + "real_diff_0"; (**)"0 - ?x = - ?x"
1.478 + "real_diff_0_right"; (**)"?x - 0 = ?x"
1.479 + "real_diff_self"; (**)"?x - ?x = 0"
1.480 + "real_mult_congruent2_lemma";
1.481 + "real_mult_congruent2";
1.482 + "congruent2 realrel
1.483 + (%p1 p2.
1.484 + (%(x1, y1).
1.485 + (%(x2, y2). realrel `` {(x1 * x2 + y1 * y2, x1 * y2 + x2 * y1)})
1.486 + p2) p1)"
1.487 + "real_mult";
1.488 + "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) *
1.489 + Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =
1.490 + Abs_REAL
1.491 + (realrel ``
1.492 + {(?x1.0 * ?x2.0 + ?y1.0 * ?y2.0, ?x1.0 * ?y2.0 + ?x2.0 * ?y1.0)})"
1.493 + "real_mult_commute"; (**)"?z * ?w = ?w * ?z"
1.494 + "real_mult_assoc"; (**)
1.495 + "real_mult_left_commute";
1.496 + (**)"?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"
1.497 + "real_mult_1"; (**)"1 * ?z = ?z"
1.498 + "real_mult_1_right"; (**)"?z * 1 = ?z"
1.499 + "real_mult_0"; (**)
1.500 + "real_mult_0_right"; (**)"?z * 0 = 0"
1.501 + "real_mult_minus_eq1"; (**)"- ?x * ?y = - (?x * ?y)"
1.502 + "real_mult_minus_eq2"; (**)"?x * - ?y = - (?x * ?y)"
1.503 + "real_mult_minus_1"; (**)"- 1 * ?z = - ?z"
1.504 + "real_mult_minus_1_right";(**)"?z * - 1 = - ?z"
1.505 + "real_minus_mult_cancel"; (**)"- ?x * - ?y = ?x * ?y"
1.506 + "real_minus_mult_commute";(**)"- ?x * ?y = ?x * - ?y"
1.507 + "real_add_assoc_cong";
1.508 + "?z + ?v = ?z' + ?v' ==> ?z + (?v + ?w) = ?z' + (?v' + ?w)"
1.509 + "real_add_assoc_swap"; (**)"?z + (?v + ?w) = ?v + (?z + ?w)"
1.510 + "real_add_mult_distrib"; (**)"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"
1.511 + "real_add_mult_distrib2"; (**)"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"
1.512 + "real_diff_mult_distrib"; (**)"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"
1.513 + "real_diff_mult_distrib2";(**)"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"
1.514 + "real_zero_not_eq_one";
1.515 + "real_zero_iff"; "0 = Abs_REAL (realrel `` {(?x, ?x)})"
1.516 + "real_mult_inv_right_ex"; "?x ~= 0 ==> EX y. ?x * y = 1"
1.517 + "real_mult_inv_left_ex"; "?x ~= 0 ==> inverse ?x * ?x = 1"
1.518 + "real_mult_inv_left";
1.519 + "real_mult_inv_right"; "?x ~= 0 ==> ?x * inverse ?x = 1"
1.520 + "INVERSE_ZERO"; "inverse 0 = 0"
1.521 + "DIVISION_BY_ZERO"; (*NOT for adding to default simpset*)"?a / 0 = 0"
1.522 + "real_mult_left_cancel"; (**)"?c ~= 0 ==> (?c * ?a = ?c * ?b) = (?a = ?b)"
1.523 + "real_mult_right_cancel"; (**)"?c ~= 0 ==> (?a * ?c = ?b * ?c) = (?a = ?b)"
1.524 + "real_mult_left_cancel_ccontr"; "?c * ?a ~= ?c * ?b ==> ?a ~= ?b"
1.525 + "real_mult_right_cancel_ccontr"; "?a * ?c ~= ?b * ?c ==> ?a ~= ?b"
1.526 + "real_inverse_not_zero"; "?x ~= 0 ==> inverse ?x ~= 0"
1.527 + "real_mult_not_zero"; "[| ?x ~= 0; ?y ~= 0 |] ==> ?x * ?y ~= 0"
1.528 + "real_inverse_inverse"; "inverse (inverse ?x) = ?x"
1.529 + "real_inverse_1"; "inverse 1 = 1"
1.530 + "real_minus_inverse"; "inverse (- ?x) = - inverse ?x"
1.531 + "real_inverse_distrib"; "inverse (?x * ?y) = inverse ?x * inverse ?y"
1.532 + "real_times_divide1_eq"; (**)"?x * (?y / ?z) = ?x * ?y / ?z"
1.533 + "real_times_divide2_eq"; (**)"?y / ?z * ?x = ?y * ?x / ?z"
1.534 + "real_divide_divide1_eq"; (**)"?x / (?y / ?z) = ?x * ?z / ?y"
1.535 + "real_divide_divide2_eq"; (**)"?x / ?y / ?z = ?x / (?y * ?z)"
1.536 + "real_minus_divide_eq"; (**)"- ?x / ?y = - (?x / ?y)"
1.537 + "real_divide_minus_eq"; (**)"?x / - ?y = - (?x / ?y)"
1.538 + "real_add_divide_distrib"; (**)"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
1.539 + "preal_lemma_eq_rev_sum";
1.540 + "[| ?x = ?y; ?x1.0 = ?y1.0 |] ==> ?x + ?y1.0 = ?x1.0 + ?y"
1.541 + "preal_add_left_commute_cancel";
1.542 + "?x + (?b + ?y) = ?x1.0 + (?b + ?y1.0) ==> ?x + ?y = ?x1.0 + ?y1.0"
1.543 + "preal_lemma_for_not_refl";
1.544 + "real_less_not_refl"; "~ ?R < ?R"
1.545 + "real_not_refl2";
1.546 + "preal_lemma_trans";
1.547 + "real_less_trans";
1.548 + "real_less_not_sym";
1.549 + "real_of_preal_add";
1.550 + "real_of_preal (?z1.0 + ?z2.0) = real_of_preal ?z1.0 + real_of_preal ?z2.0"
1.551 + "real_of_preal_mult";
1.552 + "real_of_preal_ExI";
1.553 + "real_of_preal_ExD";
1.554 + "real_of_preal_iff";
1.555 + "real_of_preal_trichotomy";
1.556 + "real_of_preal_trichotomyE";
1.557 + "real_of_preal_lessD";
1.558 + "real_of_preal_lessI";
1.559 + "?m1.0 < ?m2.0 ==> real_of_preal ?m1.0 < real_of_preal ?m2.0"
1.560 + "real_of_preal_less_iff1";
1.561 + "real_of_preal_minus_less_self";
1.562 + "real_of_preal_minus_less_zero";
1.563 + "real_of_preal_not_minus_gt_zero";
1.564 + "real_of_preal_zero_less";
1.565 + "real_of_preal_not_less_zero";
1.566 + "real_minus_minus_zero_less";
1.567 + "real_of_preal_sum_zero_less";
1.568 + "real_of_preal_minus_less_all";
1.569 + "real_of_preal_not_minus_gt_all";
1.570 + "real_of_preal_minus_less_rev1";
1.571 + "real_of_preal_minus_less_rev2";
1.572 + "real_of_preal_minus_less_rev_iff";
1.573 + "real_linear"; "?R1.0 < ?R2.0 | ?R1.0 = ?R2.0 | ?R2.0 < ?R1.0"
1.574 + "real_neq_iff";
1.575 + "real_linear_less2";
1.576 + "[| ?R1.0 < ?R2.0 ==> ?P; ?R1.0 = ?R2.0 ==> ?P; ?R2.0 < ?R1.0 ==> ?P |]
1.577 + ==> ?P"
1.578 + "real_leI";
1.579 + "real_leD"; "~ ?w < ?z ==> ?z <= ?w"
1.580 + "real_less_le_iff";
1.581 + "not_real_leE";
1.582 + "real_le_imp_less_or_eq";
1.583 + "real_less_or_eq_imp_le";
1.584 + "real_le_less";
1.585 + "real_le_refl"; "?w <= ?w"
1.586 + "real_le_linear";
1.587 + "real_le_trans"; "[| ?i <= ?j; ?j <= ?k |] ==> ?i <= ?k"
1.588 + "real_le_anti_sym"; "[| ?z <= ?w; ?w <= ?z |] ==> ?z = ?w"
1.589 + "not_less_not_eq_real_less";
1.590 + "real_less_le"; "(?w < ?z) = (?w <= ?z & ?w ~= ?z)"
1.591 + "real_minus_zero_less_iff";
1.592 + "real_minus_zero_less_iff2";
1.593 + "real_less_add_positive_left_Ex";
1.594 + "real_less_sum_gt_zero"; "?W < ?S ==> 0 < ?S + - ?W"
1.595 + "real_lemma_change_eq_subj";
1.596 + "real_sum_gt_zero_less"; "0 < ?S + - ?W ==> ?W < ?S"
1.597 + "real_less_sum_gt_0_iff"; "(0 < ?S + - ?W) = (?W < ?S)"
1.598 + "real_less_eq_diff"; "(?x < ?y) = (?x - ?y < 0)"
1.599 + "real_add_diff_eq"; (**)"?x + (?y - ?z) = ?x + ?y - ?z"
1.600 + "real_diff_add_eq"; (**)"?x - ?y + ?z = ?x + ?z - ?y"
1.601 + "real_diff_diff_eq"; (**)"?x - ?y - ?z = ?x - (?y + ?z)"
1.602 + "real_diff_diff_eq2"; (**)"?x - (?y - ?z) = ?x + ?z - ?y"
1.603 + "real_diff_less_eq"; "(?x - ?y < ?z) = (?x < ?z + ?y)"
1.604 + "real_less_diff_eq";
1.605 + "real_diff_le_eq"; "(?x - ?y <= ?z) = (?x <= ?z + ?y)"
1.606 + "real_le_diff_eq";
1.607 + "real_diff_eq_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)"
1.608 + "real_eq_diff_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)"
1.609 + "real_less_eqI";
1.610 + "real_le_eqI";
1.611 + "real_eq_eqI"; "?x - ?y = ?x' - ?y' ==> (?x = ?y) = (?x' = ?y')"
1.612 +RealOrd.ML:qed ---------------------------------------------------------------
1.613 + "real_add_cancel_21"; "(?x + (?y + ?z) = ?y + ?u) = (?x + ?z = ?u)"
1.614 + "real_add_cancel_end"; "(?x + (?y + ?z) = ?y) = (?x = - ?z)"
1.615 + "real_minus_diff_eq"; (*??*)"- (?x - ?y) = ?y - ?x"
1.616 + "real_gt_zero_preal_Ex";
1.617 + "real_gt_preal_preal_Ex";
1.618 + "real_ge_preal_preal_Ex";
1.619 + "real_less_all_preal"; "?y <= 0 ==> ALL x. ?y < real_of_preal x"
1.620 + "real_less_all_real2";
1.621 + "real_lemma_add_positive_imp_less";
1.622 + "real_ex_add_positive_left_less";"EX T. 0 < T & ?R + T = ?S ==> ?R < ?S"
1.623 + "real_less_iff_add";
1.624 + "real_of_preal_le_iff";
1.625 + "real_mult_order"; "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x * ?y"
1.626 + "neg_real_mult_order";
1.627 + "real_mult_less_0"; "[| 0 < ?x; ?y < 0 |] ==> ?x * ?y < 0"
1.628 + "real_zero_less_one"; "0 < 1"
1.629 + "real_add_right_cancel_less"; "(?v + ?z < ?w + ?z) = (?v < ?w)"
1.630 + "real_add_left_cancel_less";
1.631 + "real_add_right_cancel_le";
1.632 + "real_add_left_cancel_le";
1.633 + "real_add_less_le_mono"; "[| ?w' < ?w; ?z' <= ?z |] ==> ?w' + ?z' < ?w + ?z"
1.634 + "real_add_le_less_mono"; "[| ?w' <= ?w; ?z' < ?z |] ==> ?w' + ?z' < ?w + ?z"
1.635 + "real_add_less_mono2";
1.636 + "real_less_add_right_cancel";
1.637 + "real_less_add_left_cancel"; "?C + ?A < ?C + ?B ==> ?A < ?B"
1.638 + "real_le_add_right_cancel";
1.639 + "real_le_add_left_cancel"; "?C + ?A <= ?C + ?B ==> ?A <= ?B"
1.640 + "real_add_order"; "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x + ?y"
1.641 + "real_le_add_order";
1.642 + "real_add_less_mono";
1.643 + "real_add_left_le_mono1";
1.644 + "real_add_le_mono";
1.645 + "real_less_Ex";
1.646 + "real_add_minus_positive_less_self"; "0 < ?r ==> ?u + - ?r < ?u"
1.647 + "real_le_minus_iff"; "(- ?s <= - ?r) = (?r <= ?s)"
1.648 + "real_le_square";
1.649 + "real_of_posnat_one";
1.650 + "real_of_posnat_two";
1.651 + "real_of_posnat_add"; "real_of_posnat ?n1.0 + real_of_posnat ?n2.0 =
1.652 + real_of_posnat (?n1.0 + ?n2.0) + 1"
1.653 + "real_of_posnat_add_one";
1.654 + "real_of_posnat_Suc";
1.655 + "inj_real_of_posnat";
1.656 + "real_of_nat_zero";
1.657 + "real_of_nat_one"; "real (Suc 0) = 1"
1.658 + "real_of_nat_add";
1.659 + "real_of_nat_Suc";
1.660 + "real_of_nat_less_iff";
1.661 + "real_of_nat_le_iff";
1.662 + "inj_real_of_nat";
1.663 + "real_of_nat_ge_zero";
1.664 + "real_of_nat_mult";
1.665 + "real_of_nat_inject";
1.666 +RealOrd.ML:qed_spec_mp
1.667 + "real_of_nat_diff";
1.668 +RealOrd.ML:qed
1.669 + "real_of_nat_zero_iff";
1.670 + "real_of_nat_neg_int";
1.671 + "real_inverse_gt_0";
1.672 + "real_inverse_less_0";
1.673 + "real_mult_less_mono1";
1.674 + "real_mult_less_mono2";
1.675 + "real_mult_less_cancel1";
1.676 + "(?k * ?m < ?k * ?n) = (0 < ?k & ?m < ?n | ?k < 0 & ?n < ?m)"
1.677 + "real_mult_less_cancel2";
1.678 + "real_mult_less_iff1";
1.679 + "real_mult_less_iff2";
1.680 + "real_mult_le_cancel_iff1";
1.681 + "real_mult_le_cancel_iff2";
1.682 + "real_mult_le_less_mono1";
1.683 + "real_mult_less_mono";
1.684 + "real_mult_less_mono'";
1.685 + "real_gt_zero"; "1 <= ?x ==> 0 < ?x"
1.686 + "real_mult_self_le"; "[| 1 < ?r; 1 <= ?x |] ==> ?x <= ?r * ?x"
1.687 + "real_mult_self_le2";
1.688 + "real_inverse_less_swap";
1.689 + "real_mult_is_0";
1.690 + "real_inverse_add";
1.691 + "real_minus_zero_le_iff";
1.692 + "real_minus_zero_le_iff2";
1.693 + "real_sum_squares_cancel"; "?x * ?x + ?y * ?y = 0 ==> ?x = 0"
1.694 + "real_sum_squares_cancel2"; "?x * ?x + ?y * ?y = 0 ==> ?y = 0"
1.695 + "real_0_less_mult_iff";
1.696 + "real_0_le_mult_iff";
1.697 + "real_mult_less_0_iff"; "(?x * ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)"
1.698 + "real_mult_le_0_iff";
1.699 +RealInt.ML:qed ---------------------------------------------------------------
1.700 + "real_of_int_congruent";
1.701 + "real_of_int"; "real (Abs_Integ (intrel `` {(?i, ?j)})) =
1.702 + Abs_REAL
1.703 + (realrel ``
1.704 + {(preal_of_prat (prat_of_pnat (pnat_of_nat ?i)),
1.705 + preal_of_prat (prat_of_pnat (pnat_of_nat ?j)))})"
1.706 + "inj_real_of_int";
1.707 + "real_of_int_zero";
1.708 + "real_of_one";
1.709 + "real_of_int_add"; "real ?x + real ?y = real (?x + ?y)"
1.710 + "real_of_int_minus";
1.711 + "real_of_int_diff";
1.712 + "real_of_int_mult"; "real ?x * real ?y = real (?x * ?y)"
1.713 + "real_of_int_Suc";
1.714 + "real_of_int_real_of_nat";
1.715 + "real_of_nat_real_of_int";
1.716 + "real_of_int_zero_cancel";
1.717 + "real_of_int_less_cancel";
1.718 + "real_of_int_inject";
1.719 + "real_of_int_less_mono";
1.720 + "real_of_int_less_iff";
1.721 + "real_of_int_le_iff";
1.722 +RealBin.ML:qed ---------------------------------------------------------------
1.723 + "real_number_of"; "real (number_of ?w) = number_of ?w"
1.724 + "real_numeral_0_eq_0";
1.725 + "real_numeral_1_eq_1";
1.726 + "add_real_number_of";
1.727 + "minus_real_number_of";
1.728 + "diff_real_number_of";
1.729 + "mult_real_number_of";
1.730 + "real_mult_2"; (**)"2 * ?z = ?z + ?z"
1.731 + "real_mult_2_right"; (**)"?z * 2 = ?z + ?z"
1.732 + "eq_real_number_of";
1.733 + "less_real_number_of";
1.734 + "le_real_number_of_eq_not_less";
1.735 + "real_minus_1_eq_m1"; "- 1 = -1"(*uminus.. = "-.."*)
1.736 + "real_mult_minus1"; (**)"-1 * ?z = - ?z"
1.737 + "real_mult_minus1_right"; (**)"?z * -1 = - ?z"
1.738 + "zero_less_real_of_nat_iff";"(0 < real ?n) = (0 < ?n)"
1.739 + "zero_le_real_of_nat_iff";
1.740 + "real_add_number_of_left";
1.741 + "real_mult_number_of_left";
1.742 + "number_of ?v * (number_of ?w * ?z) = number_of (bin_mult ?v ?w) * ?z"
1.743 + "real_add_number_of_diff1";
1.744 + "real_add_number_of_diff2";"number_of ?v + (?c - number_of ?w) =
1.745 + number_of (bin_add ?v (bin_minus ?w)) + ?c"
1.746 + "real_of_nat_number_of";
1.747 + "real (number_of ?v) = (if neg (number_of ?v) then 0 else number_of ?v)"
1.748 + "real_less_iff_diff_less_0"; "(?x < ?y) = (?x - ?y < 0)"
1.749 + "real_eq_iff_diff_eq_0";
1.750 + "real_le_iff_diff_le_0";
1.751 + "left_real_add_mult_distrib";
1.752 + (**)"?i * ?u + (?j * ?u + ?k) = (?i + ?j) * ?u + ?k"
1.753 + "real_eq_add_iff1";
1.754 + "(?i * ?u + ?m = ?j * ?u + ?n) = ((?i - ?j) * ?u + ?m = ?n)"
1.755 + "real_eq_add_iff2";
1.756 + "real_less_add_iff1";
1.757 + "real_less_add_iff2";
1.758 + "real_le_add_iff1";
1.759 + "real_le_add_iff2";
1.760 + "real_mult_le_mono1";
1.761 + "real_mult_le_mono2";
1.762 + "real_mult_le_mono";
1.763 + "[| ?i <= ?j; ?k <= ?l; 0 <= ?j; 0 <= ?k |] ==> ?i * ?k <= ?j * ?l"
1.764 +RealArith0.ML:qed ------------------------------------------------------------
1.765 + "real_diff_minus_eq"; (**)"?x - - ?y = ?x + ?y"
1.766 + "real_0_divide"; (**)"0 / ?x = 0"
1.767 + "real_0_less_inverse_iff"; "(0 < inverse ?x) = (0 < ?x)"
1.768 + "real_inverse_less_0_iff";
1.769 + "real_0_le_inverse_iff";
1.770 + "real_inverse_le_0_iff";
1.771 + "REAL_DIVIDE_ZERO"; "?x / 0 = 0"(*!!!*)
1.772 + "real_inverse_eq_divide";
1.773 + "real_0_less_divide_iff";"(0 < ?x / ?y) = (0 < ?x & 0 < ?y | ?x < 0 & ?y < 0)"
1.774 + "real_divide_less_0_iff";"(?x / ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)"
1.775 + "real_0_le_divide_iff";
1.776 + "real_divide_le_0_iff";
1.777 + "(?x / ?y <= 0) = ((?x <= 0 | ?y <= 0) & (0 <= ?x | 0 <= ?y))"
1.778 + "real_inverse_zero_iff";
1.779 + "real_divide_eq_0_iff"; "(?x / ?y = 0) = (?x = 0 | ?y = 0)"(*!!!*)
1.780 + "real_divide_self_eq"; "?h ~= 0 ==> ?h / ?h = 1"(**)
1.781 + "real_minus_less_minus"; "(- ?y < - ?x) = (?x < ?y)"
1.782 + "real_mult_less_mono1_neg"; "[| ?i < ?j; ?k < 0 |] ==> ?j * ?k < ?i * ?k"
1.783 + "real_mult_less_mono2_neg";
1.784 + "real_mult_le_mono1_neg";
1.785 + "real_mult_le_mono2_neg";
1.786 + "real_mult_less_cancel2";
1.787 + "real_mult_le_cancel2";
1.788 + "real_mult_less_cancel1";
1.789 + "real_mult_le_cancel1";
1.790 + "real_mult_eq_cancel1"; "(?k * ?m = ?k * ?n) = (?k = 0 | ?m = ?n)"
1.791 + "real_mult_eq_cancel2"; "(?m * ?k = ?n * ?k) = (?k = 0 | ?m = ?n)"
1.792 + "real_mult_div_cancel1"; (**)"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"
1.793 + "real_mult_div_cancel_disj";
1.794 + "?k * ?m / (?k * ?n) = (if ?k = 0 then 0 else ?m / ?n)"
1.795 + "pos_real_le_divide_eq";
1.796 + "neg_real_le_divide_eq";
1.797 + "pos_real_divide_le_eq";
1.798 + "neg_real_divide_le_eq";
1.799 + "pos_real_less_divide_eq";
1.800 + "neg_real_less_divide_eq";
1.801 + "pos_real_divide_less_eq";
1.802 + "neg_real_divide_less_eq";
1.803 + "real_eq_divide_eq"; (**)"?z ~= 0 ==> (?x = ?y / ?z) = (?x * ?z = ?y)"
1.804 + "real_divide_eq_eq"; (**)"?z ~= 0 ==> (?y / ?z = ?x) = (?y = ?x * ?z)"
1.805 + "real_divide_eq_cancel2"; "(?m / ?k = ?n / ?k) = (?k = 0 | ?m = ?n)"
1.806 + "real_divide_eq_cancel1"; "(?k / ?m = ?k / ?n) = (?k = 0 | ?m = ?n)"
1.807 + "real_inverse_less_iff";
1.808 + "real_inverse_le_iff";
1.809 + "real_divide_1"; (**)"?x / 1 = ?x"
1.810 + "real_divide_minus1"; (**)"?x / -1 = - ?x"
1.811 + "real_minus1_divide"; (**)"-1 / ?x = - (1 / ?x)"
1.812 + "real_lbound_gt_zero";
1.813 + "[| 0 < ?d1.0; 0 < ?d2.0 |] ==> EX e. 0 < e & e < ?d1.0 & e < ?d2.0"
1.814 + "real_inverse_eq_iff"; "(inverse ?x = inverse ?y) = (?x = ?y)"
1.815 + "real_divide_eq_iff"; "(?z / ?x = ?z / ?y) = (?z = 0 | ?x = ?y)"
1.816 + "real_less_minus"; "(?x < - ?y) = (?y < - ?x)"
1.817 + "real_minus_less"; "(- ?x < ?y) = (- ?y < ?x)"
1.818 + "real_le_minus";
1.819 + "real_minus_le"; "(- ?x <= ?y) = (- ?y <= ?x)"
1.820 + "real_equation_minus"; (**)"(?x = - ?y) = (?y = - ?x)"
1.821 + "real_minus_equation"; (**)"(- ?x = ?y) = (- ?y = ?x)"
1.822 + "real_add_minus_iff"; (**)"(?x + - ?a = 0) = (?x = ?a)"
1.823 + "real_minus_eq_cancel"; (**)"(- ?b = - ?a) = (?b = ?a)"
1.824 + "real_add_eq_0_iff"; (**)"(?x + ?y = 0) = (?y = - ?x)"
1.825 + "real_add_less_0_iff"; "(?x + ?y < 0) = (?y < - ?x)"
1.826 + "real_0_less_add_iff";
1.827 + "real_add_le_0_iff";
1.828 + "real_0_le_add_iff";
1.829 + "real_0_less_diff_iff"; "(0 < ?x - ?y) = (?y < ?x)"
1.830 + "real_0_le_diff_iff";
1.831 + "real_minus_diff_eq"; (**)"- (?x - ?y) = ?y - ?x"
1.832 + "real_less_half_sum"; "?x < ?y ==> ?x < (?x + ?y) / 2"
1.833 + "real_gt_half_sum";
1.834 + "real_dense"; "?x < ?y ==> EX r. ?x < r & r < ?y"
1.835 +RealArith ///!!!///-----------------------------------------------------------
1.836 +RComplete.ML:qed -------------------------------------------------------------
1.837 + "real_sum_of_halves"; (**)"?x / 2 + ?x / 2 = ?x"
1.838 + "real_sup_lemma1";
1.839 + "real_sup_lemma2";
1.840 + "posreal_complete";
1.841 + "real_isLub_unique";
1.842 + "real_order_restrict";
1.843 + "posreals_complete";
1.844 + "real_sup_lemma3";
1.845 + "lemma_le_swap2";
1.846 + "lemma_real_complete2b";
1.847 + "reals_complete";
1.848 + "real_of_nat_Suc_gt_zero";
1.849 + "reals_Archimedean"; "0 < ?x ==> EX n. inverse (real (Suc n)) < ?x"
1.850 + "reals_Archimedean2";
1.851 +RealAbs.ML:qed
1.852 + "abs_nat_number_of";
1.853 + "abs (number_of ?v) =
1.854 + (if neg (number_of ?v) then number_of (bin_minus ?v) else number_of ?v)"
1.855 + "abs_split";
1.856 + "abs_iff";
1.857 + "abs_zero"; "abs 0 = 0"
1.858 + "abs_one";
1.859 + "abs_eqI1";
1.860 + "abs_eqI2";
1.861 + "abs_minus_eqI2";
1.862 + "abs_minus_eqI1";
1.863 + "abs_ge_zero"; "0 <= abs ?x"
1.864 + "abs_idempotent"; "abs (abs ?x) = abs ?x"
1.865 + "abs_zero_iff"; "(abs ?x = 0) = (?x = 0)"
1.866 + "abs_ge_self"; "?x <= abs ?x"
1.867 + "abs_ge_minus_self";
1.868 + "abs_mult"; "abs (?x * ?y) = abs ?x * abs ?y"
1.869 + "abs_inverse"; "abs (inverse ?x) = inverse (abs ?x)"
1.870 + "abs_mult_inverse";
1.871 + "abs_triangle_ineq"; "abs (?x + ?y) <= abs ?x + abs ?y"
1.872 + "abs_triangle_ineq_four";
1.873 + "abs_minus_cancel";
1.874 + "abs_minus_add_cancel";
1.875 + "abs_triangle_minus_ineq";
1.876 +RealAbs.ML:qed_spec_mp
1.877 + "abs_add_less"; "[| abs ?x < ?r; abs ?y < ?s |] ==> abs (?x + ?y) < ?r + ?s"
1.878 +RealAbs.ML:qed
1.879 + "abs_add_minus_less";
1.880 + "real_mult_0_less"; "(0 * ?x < ?r) = (0 < ?r)"
1.881 + "real_mult_less_trans";
1.882 + "real_mult_le_less_trans";
1.883 + "abs_mult_less";
1.884 + "abs_mult_less2";
1.885 + "abs_less_gt_zero";
1.886 + "abs_minus_one"; "abs -1 = 1"
1.887 + "abs_disj"; "abs ?x = ?x | abs ?x = - ?x"
1.888 + "abs_interval_iff";
1.889 + "abs_le_interval_iff";
1.890 + "abs_add_pos_gt_zero";
1.891 + "abs_add_one_gt_zero";
1.892 + "abs_not_less_zero";
1.893 + "abs_circle"; "abs ?h < abs ?y - abs ?x ==> abs (?x + ?h) < abs ?y"
1.894 + "abs_le_zero_iff";
1.895 + "real_0_less_abs_iff";
1.896 + "abs_real_of_nat_cancel";
1.897 + "abs_add_one_not_less_self";
1.898 + "abs_triangle_ineq_three"; "abs (?w + ?x + ?y) <= abs ?w + abs ?x + abs ?y"
1.899 + "abs_diff_less_imp_gt_zero";
1.900 + "abs_diff_less_imp_gt_zero2";
1.901 + "abs_diff_less_imp_gt_zero3";
1.902 + "abs_diff_less_imp_gt_zero4";
1.903 + "abs_triangle_ineq_minus_cancel";
1.904 + "abs_sum_triangle_ineq";
1.905 + "abs (?x + ?y + (- ?l + - ?m)) <= abs (?x + - ?l) + abs (?y + - ?m)"
1.906 +RealPow.ML:qed
1.907 + "realpow_zero"; "0 ^ Suc ?n = 0"
1.908 +RealPow.ML:qed_spec_mp
1.909 + "realpow_not_zero"; "?r ~= 0 ==> ?r ^ ?n ~= 0"
1.910 + "realpow_zero_zero"; "?r ^ ?n = 0 ==> ?r = 0"
1.911 + "realpow_inverse"; "inverse (?r ^ ?n) = inverse ?r ^ ?n"
1.912 + "realpow_abs"; "abs (?r ^ ?n) = abs ?r ^ ?n"
1.913 + "realpow_add"; (**)"?r ^ (?n + ?m) = ?r ^ ?n * ?r ^ ?m"
1.914 + "realpow_one"; (**)"?r ^ 1 = ?r"
1.915 + "realpow_two"; (**)"?r ^ Suc (Suc 0) = ?r * ?r"
1.916 +RealPow.ML:qed_spec_mp
1.917 + "realpow_gt_zero"; "0 < ?r ==> 0 < ?r ^ ?n"
1.918 + "realpow_ge_zero"; "0 <= ?r ==> 0 <= ?r ^ ?n"
1.919 + "realpow_le"; "0 <= ?x & ?x <= ?y ==> ?x ^ ?n <= ?y ^ ?n"
1.920 + "realpow_less";
1.921 +RealPow.ML:qed
1.922 + "realpow_eq_one"; (**)"1 ^ ?n = 1"
1.923 + "abs_realpow_minus_one"; "abs (-1 ^ ?n) = 1"
1.924 + "realpow_mult"; (**)"(?r * ?s) ^ ?n = ?r ^ ?n * ?s ^ ?n"
1.925 + "realpow_two_le"; "0 <= ?r ^ Suc (Suc 0)"
1.926 + "abs_realpow_two";
1.927 + "realpow_two_abs"; "abs ?x ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)"
1.928 + "realpow_two_gt_one";
1.929 +RealPow.ML:qed_spec_mp
1.930 + "realpow_ge_one"; "1 < ?r ==> 1 <= ?r ^ ?n"
1.931 +RealPow.ML:qed
1.932 + "realpow_ge_one2";
1.933 + "two_realpow_ge_one";
1.934 + "two_realpow_gt";
1.935 + "realpow_minus_one"; (**)"-1 ^ (2 * ?n) = 1"
1.936 + "realpow_minus_one_odd"; "-1 ^ Suc (2 * ?n) = - 1"
1.937 + "realpow_minus_one_even";
1.938 +RealPow.ML:qed_spec_mp
1.939 + "realpow_Suc_less";
1.940 + "realpow_Suc_le"; "0 <= ?r & ?r < 1 ==> ?r ^ Suc ?n <= ?r ^ ?n"
1.941 +RealPow.ML:qed
1.942 + "realpow_zero_le"; "0 <= 0 ^ ?n"
1.943 +RealPow.ML:qed_spec_mp
1.944 + "realpow_Suc_le2";
1.945 +RealPow.ML:qed
1.946 + "realpow_Suc_le3";
1.947 +RealPow.ML:qed_spec_mp
1.948 + "realpow_less_le"; "0 <= ?r & ?r < 1 & ?n < ?N ==> ?r ^ ?N <= ?r ^ ?n"
1.949 +RealPow.ML:qed
1.950 + "realpow_le_le"; "[| 0 <= ?r; ?r < 1; ?n <= ?N |] ==> ?r ^ ?N <= ?r ^ ?n"
1.951 + "realpow_Suc_le_self";
1.952 + "realpow_Suc_less_one";
1.953 +RealPow.ML:qed_spec_mp
1.954 + "realpow_le_Suc";
1.955 + "realpow_less_Suc";
1.956 + "realpow_le_Suc2";
1.957 + "realpow_gt_ge";
1.958 + "realpow_gt_ge2";
1.959 +RealPow.ML:qed
1.960 + "realpow_ge_ge"; "[| 1 < ?r; ?n <= ?N |] ==> ?r ^ ?n <= ?r ^ ?N"
1.961 + "realpow_ge_ge2";
1.962 +RealPow.ML:qed_spec_mp
1.963 + "realpow_Suc_ge_self";
1.964 + "realpow_Suc_ge_self2";
1.965 +RealPow.ML:qed
1.966 + "realpow_ge_self";
1.967 + "realpow_ge_self2";
1.968 +RealPow.ML:qed_spec_mp
1.969 + "realpow_minus_mult"; "0 < ?n ==> ?x ^ (?n - 1) * ?x = ?x ^ ?n"
1.970 + "realpow_two_mult_inverse";
1.971 + "?r ~= 0 ==> ?r * inverse ?r ^ Suc (Suc 0) = inverse ?r"
1.972 + "realpow_two_minus"; "(- ?x) ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)"
1.973 + "realpow_two_diff";
1.974 + "realpow_two_disj";
1.975 + "realpow_diff";
1.976 + "[| ?x ~= 0; ?m <= ?n |] ==> ?x ^ (?n - ?m) = ?x ^ ?n * inverse (?x ^ ?m)"
1.977 + "realpow_real_of_nat";
1.978 + "realpow_real_of_nat_two_pos"; "0 < real (Suc (Suc 0) ^ ?n)"
1.979 +RealPow.ML:qed_spec_mp
1.980 + "realpow_increasing";
1.981 + "realpow_Suc_cancel_eq";
1.982 + "[| 0 <= ?x; 0 <= ?y; ?x ^ Suc ?n = ?y ^ Suc ?n |] ==> ?x = ?y"
1.983 +RealPow.ML:qed
1.984 + "realpow_eq_0_iff"; "(?x ^ ?n = 0) = (?x = 0 & 0 < ?n)"
1.985 + "zero_less_realpow_abs_iff";
1.986 + "zero_le_realpow_abs";
1.987 + "real_of_int_power"; "real ?x ^ ?n = real (?x ^ ?n)"
1.988 + "power_real_number_of"; "number_of ?v ^ ?n = real (number_of ?v ^ ?n)"
1.989 +Ring_and_Field ---///!!!///---------------------------------------------------
1.990 +Complex_Numbers --///!!!///---------------------------------------------------
1.991 +Real -------------///!!!///---------------------------------------------------
1.992 +real_arith0.ML:qed "";
1.993 +real_arith0.ML:qed "";
1.994 +real_arith0.ML:qed "";
1.995 +real_arith0.ML:qed "";
1.996 +real_arith0.ML:qed "";
1.997 +real_arith0.ML:qed "";
1.998 +real_arith0.ML:qed "";
1.999 +real_arith0.ML:qed "";
1.1000 +real_arith0.ML:qed "";
1.1001 +
1.1002 +
1.1003 +
1.1004 +
1.1005 +
1.1006 +
1.1007 +
1.1008 +