1.1 --- a/src/Tools/isac/Scripts/Real2002-theorems.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,1005 +0,0 @@
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 -