diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Scripts/Real2002-theorems.sml --- a/src/Tools/isac/Scripts/Real2002-theorems.sml Wed Aug 25 15:15:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1005 +0,0 @@ -(*WN060306 from isabelle-users: -put expressions involving plus and minus into a canonical form. Here is a possible set of -rules: - - add_assoc add_commute - diff_def minus_add_distrib - minus_minus minus_zero -===========================================================================*) - -(* - cd ~/Isabelle2002/src/HOL/Real - grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml - WN 9.8.02 - -ML> thy; -val it = - {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp, Sum_Type, - Relation, Record, Inductive, Transitive_Closure, Wellfounded_Recursion, - NatDef, Nat, NatArith, Divides, Power, SetInterval, Finite_Set, Equiv, - IntDef, Int, Datatype_Universe, Datatype, Numeral, Bin, IntArith, - Wellfounded_Relations, Recdef, IntDiv, IntPower, NatBin, NatSimprocs, - Relation_Power, PreList, List, Map, Hilbert_Choice, Main, Lubs, PNat, PRat, - PReal, RealDef, RealOrd, RealInt, RealBin, RealArith0, RealArith, - RComplete, RealAbs, RealPow, Ring_and_Field, Complex_Numbers, Real} - : theory - -theories with their respective theorems found by -grep qed *.ML > ~/develop/isac/Isa02/Real2002-theorems.sml; -theories listed in the the order as found in Real.thy above - -comments - (**)"...theorem..." : first choice for one of the rule-sets - "...theorem..."(*??*): to be investigated - "...theorem... : just for documenting the contents -*) - -Lubs.ML:qed ----------------------------------------------------------------- - "setleI"; "ALL y::?'a:?S::?'a set. y <= (?x::?'a) ==> ?S *<= ?x" - "setleD"; "[| (?S::?'a set) *<= (?x::?'a); (?y::?'a) : ?S |] ==> ?y <= ?x" - "setgeI"; "Ball (?S::?'a set) (op <= (?x::?'a)) ==> ?x <=* ?S" - "setgeD"; "[| (?x::?'a) <=* (?S::?'a set); (?y::?'a) : ?S |] ==> ?x <= ?y" - "leastPD1"; - "leastPD2"; - "leastPD3"; - "isLubD1"; - "isLubD1a"; - "isLub_isUb"; - "isLubD2"; - "isLubD3"; - "isLubI1"; - "isLubI2"; - "isUbD"; - "[| isUb (?R::?'a set) (?S::?'a set) (?x::?'a); (?y::?'a) : ?S |] - ==> ?y <= ?x" "isUbD2"; - "isUbD2a"; - "isUbI"; - "isLub_le_isUb"; - "isLub_ubs"; -PNat.ML:qed ------------------------------------------------------------------ - "pnat_fun_mono"; "mono (%X::nat set. {Suc (0::nat)} Un Suc ` X)" - "one_RepI"; "Suc (0::nat) : pnat" - "pnat_Suc_RepI"; - "two_RepI"; - "PNat_induct"; - "[| (?i::nat) : pnat; (?P::nat => bool) (Suc (0::nat)); - !!j::nat. [| j : pnat; ?P j |] ==> ?P (Suc j) |] ==> ?P ?i" - "pnat_induct"; - "[| (?P::pnat => bool) (1::pnat); !!n::pnat. ?P n ==> ?P (pSuc n) |] - ==> ?P (?n::pnat)" - "pnat_diff_induct"; - "pnatE"; - "inj_on_Abs_pnat"; - "inj_Rep_pnat"; - "zero_not_mem_pnat"; - "mem_pnat_gt_zero"; - "gt_0_mem_pnat"; - "mem_pnat_gt_0_iff"; - "Rep_pnat_gt_zero"; - "pnat_add_commute"; "(?x::pnat) + (?y::pnat) = ?y + ?x" - "Collect_pnat_gt_0"; - "pSuc_not_one"; - "inj_pSuc"; - "pSuc_pSuc_eq"; - "n_not_pSuc_n"; - "not1_implies_pSuc"; - "pSuc_is_plus_one"; - "sum_Rep_pnat"; - "sum_Rep_pnat_sum"; - "pnat_add_assoc"; - "pnat_add_left_commute"; - "pnat_add_left_cancel"; - "pnat_add_right_cancel"; - "pnat_no_add_ident"; - "pnat_less_not_refl"; - "pnat_less_not_refl2"; - "Rep_pnat_not_less0"; - "Rep_pnat_not_less_one"; - "Rep_pnat_gt_implies_not0"; - "pnat_less_linear"; - "Rep_pnat_le_one"; - "lemma_less_ex_sum_Rep_pnat"; - "pnat_le_iff_Rep_pnat_le"; - "pnat_add_left_cancel_le"; - "pnat_add_left_cancel_less"; - "pnat_add_lessD1"; - "pnat_not_add_less1"; - "pnat_not_add_less2"; -PNat.ML:qed_spec_mp - "pnat_add_leD1"; - "pnat_add_leD2"; -PNat.ML:qed - "pnat_less_add_eq_less"; - "pnat_less_iff"; - "pnat_linear_Ex_eq"; - "pnat_eq_lessI"; - "Rep_pnat_mult_1"; - "Rep_pnat_mult_1_right"; - "mult_Rep_pnat"; - "mult_Rep_pnat_mult"; - "pnat_mult_commute"; "(?m::pnat) * (?n::pnat) = ?n * ?m" - "pnat_add_mult_distrib"; - "pnat_add_mult_distrib2"; - "pnat_mult_assoc"; - "pnat_mult_left_commute"; - "pnat_mult_1"; - "pnat_mult_1_left"; - "pnat_mult_less_mono2"; - "pnat_mult_less_mono1"; - "pnat_mult_less_cancel2"; - "pnat_mult_less_cancel1"; - "pnat_mult_cancel2"; - "pnat_mult_cancel1"; - "pnat_same_multI2"; - "eq_Abs_pnat"; - "pnat_one_iff"; - "pnat_two_eq"; - "inj_pnat_of_nat"; - "nat_add_one_less"; - "nat_add_one_less1"; - "pnat_of_nat_add"; - "pnat_of_nat_less_iff"; - "pnat_of_nat_mult"; -PRat.ML:qed ------------------------------------------------------------------ - "prat_trans_lemma"; - "[| (?x1.0::pnat) * (?y2.0::pnat) = (?x2.0::pnat) * (?y1.0::pnat); - ?x2.0 * (?y3.0::pnat) = (?x3.0::pnat) * ?y2.0 |] - ==> ?x1.0 * ?y3.0 = ?x3.0 * ?y1.0" - "ratrel_iff"; - "ratrelI"; - "ratrelE_lemma"; - "ratrelE"; - "ratrel_refl"; - "equiv_ratrel"; - "ratrel_in_prat"; - "inj_on_Abs_prat"; - "inj_Rep_prat"; - "inj_prat_of_pnat"; - "eq_Abs_prat"; - "qinv_congruent"; - "qinv"; - "qinv_qinv"; - "inj_qinv"; - "qinv_1"; - "prat_add_congruent2_lemma"; - "prat_add_congruent2"; - "prat_add"; - "prat_add_commute"; - "prat_add_assoc"; - "prat_add_left_commute"; - "pnat_mult_congruent2"; - "prat_mult"; - "prat_mult_commute"; - "prat_mult_assoc"; - "prat_mult_left_commute"; - "prat_mult_1"; - "prat_mult_1_right"; - "prat_of_pnat_add"; - "prat_of_pnat_mult"; - "prat_mult_qinv"; - "prat_mult_qinv_right"; - "prat_qinv_ex"; - "prat_qinv_ex1"; - "prat_qinv_left_ex1"; - "prat_mult_inv_qinv"; - "prat_as_inverse_ex"; - "qinv_mult_eq"; - "prat_add_mult_distrib"; - "prat_add_mult_distrib2"; - "prat_less_iff"; - "prat_lessI"; - "prat_lessE_lemma"; - "prat_lessE"; - "prat_less_trans"; - "prat_less_not_refl"; - "prat_less_not_sym"; - "lemma_prat_dense"; - "prat_lemma_dense"; - "prat_dense"; - "prat_add_less2_mono1"; - "prat_add_less2_mono2"; - "prat_mult_less2_mono1"; - "prat_mult_left_less2_mono1"; - "lemma_prat_add_mult_mono"; - "qless_Ex"; - "lemma_prat_less_linear"; - "prat_linear"; - "prat_linear_less2"; - "lemma1_qinv_prat_less"; - "lemma2_qinv_prat_less"; - "qinv_prat_less"; - "prat_qinv_gt_1"; - "prat_qinv_is_gt_1"; - "prat_less_1_2"; - "prat_less_qinv_2_1"; - "prat_mult_qinv_less_1"; - "prat_self_less_add_self"; - "prat_self_less_add_right"; - "prat_self_less_add_left"; - "prat_self_less_mult_right"; - "prat_leI"; - "prat_leD"; - "prat_less_le_iff"; - "not_prat_leE"; - "prat_less_imp_le"; - "prat_le_imp_less_or_eq"; - "prat_less_or_eq_imp_le"; - "prat_le_eq_less_or_eq"; - "prat_le_refl"; - "prat_le_less_trans"; - "prat_le_trans"; - "not_less_not_eq_prat_less"; - "prat_add_less_mono"; - "prat_mult_less_mono"; - "prat_mult_left_le2_mono1"; - "prat_mult_le2_mono1"; - "qinv_prat_le"; - "prat_add_left_le2_mono1"; - "prat_add_le2_mono1"; - "prat_add_le_mono"; - "prat_add_right_less_cancel"; - "prat_add_left_less_cancel"; - "Abs_prat_mult_qinv"; - "lemma_Abs_prat_le1"; - "lemma_Abs_prat_le2"; - "lemma_Abs_prat_le3"; - "pre_lemma_gleason9_34"; - "pre_lemma_gleason9_34b"; - "prat_of_pnat_less_iff"; - "lemma_prat_less_1_memEx"; - "lemma_prat_less_1_set_non_empty"; - "empty_set_psubset_lemma_prat_less_1_set"; - "lemma_prat_less_1_not_memEx"; - "lemma_prat_less_1_set_not_rat_set"; - "lemma_prat_less_1_set_psubset_rat_set"; - "preal_1"; - "{x::prat. x < prat_of_pnat (Abs_pnat (Suc (0::nat)))} - : {A::prat set. - {} < A & - A < UNIV & - (ALL y::prat:A. (ALL z::prat. z < y --> z : A) & Bex A (op < y))}" -PReal.ML:qed ----------------------------------------------------------------- - "inj_on_Abs_preal"; "inj_on Abs_preal preal" - "inj_Rep_preal"; - "empty_not_mem_preal"; - "one_set_mem_preal"; - "preal_psubset_empty"; - "Rep_preal_psubset_empty"; - "mem_Rep_preal_Ex"; - "prealI1"; - "[| {} < (?A::prat set); ?A < UNIV; - ALL y::prat:?A. (ALL z::prat. z < y --> z : ?A) & Bex ?A (op < y) |] - ==> ?A : preal" - "prealI2"; - "prealE_lemma"; - "prealE_lemma1"; - "prealE_lemma2"; - "prealE_lemma3"; - "prealE_lemma3a"; - "prealE_lemma3b"; - "prealE_lemma4"; - "prealE_lemma4a"; - "not_mem_Rep_preal_Ex"; - "lemma_prat_less_set_mem_preal"; - "lemma_prat_set_eq"; - "inj_preal_of_prat"; - "not_in_preal_ub"; - "preal_less_not_refl"; - "preal_not_refl2"; - "preal_less_trans"; - "preal_less_not_sym"; - "preal_linear"; - "(?r1.0::preal) < (?r2.0::preal) | ?r1.0 = ?r2.0 | ?r2.0 < ?r1.0" - "preal_linear_less2"; - "preal_add_commute"; "(?x::preal) + (?y::preal) = ?y + ?x" - "preal_add_set_not_empty"; - "preal_not_mem_add_set_Ex"; - "preal_add_set_not_prat_set"; - "preal_add_set_lemma3"; - "preal_add_set_lemma4"; - "preal_mem_add_set"; - "preal_add_assoc"; - "preal_add_left_commute"; - "preal_mult_commute"; "(?x::preal) * (?y::preal) = ?y * ?x" - "preal_mult_set_not_empty"; - "preal_not_mem_mult_set_Ex"; - "preal_mult_set_not_prat_set"; - "preal_mult_set_lemma3"; - "preal_mult_set_lemma4"; - "preal_mem_mult_set"; - "preal_mult_assoc"; - "preal_mult_left_commute"; - "preal_mult_1"; - "preal_mult_1_right"; - "preal_add_assoc_cong"; - "preal_add_assoc_swap"; - "mem_Rep_preal_addD"; - "mem_Rep_preal_addI"; - "mem_Rep_preal_add_iff"; - "mem_Rep_preal_multD"; - "mem_Rep_preal_multI"; - "mem_Rep_preal_mult_iff"; - "lemma_add_mult_mem_Rep_preal"; - "lemma_add_mult_mem_Rep_preal1"; - "lemma_preal_add_mult_distrib"; - "lemma_preal_add_mult_distrib2"; - "preal_add_mult_distrib2"; - "preal_add_mult_distrib"; - "qinv_not_mem_Rep_preal_Ex"; - "lemma_preal_mem_inv_set_ex"; - "preal_inv_set_not_empty"; - "qinv_mem_Rep_preal_Ex"; - "preal_not_mem_inv_set_Ex"; - "preal_inv_set_not_prat_set"; - "preal_inv_set_lemma3"; - "preal_inv_set_lemma4"; - "preal_mem_inv_set"; - "preal_mem_mult_invD"; - "lemma1_gleason9_34"; - "lemma1b_gleason9_34"; - "lemma_gleason9_34a"; - "lemma_gleason9_34"; - "lemma1_gleason9_36"; - "lemma2_gleason9_36"; - "lemma_gleason9_36"; - "lemma_gleason9_36a"; - "preal_mem_mult_invI"; - "preal_mult_inv"; - "preal_mult_inv_right"; - "eq_Abs_preal"; - "Rep_preal_self_subset"; - "Rep_preal_sum_not_subset"; - "Rep_preal_sum_not_eq"; - "preal_self_less_add_left"; - "preal_self_less_add_right"; - "preal_leD"; - "not_preal_leE"; - "preal_leI"; - "preal_less_le_iff"; - "preal_less_imp_le"; - "preal_le_imp_less_or_eq"; - "preal_less_or_eq_imp_le"; - "preal_le_refl"; - "preal_le_trans"; - "preal_le_anti_sym"; - "preal_neq_iff"; - "preal_less_le"; - "lemma_psubset_mem"; - "lemma_psubset_not_refl"; - "psubset_trans"; - "subset_psubset_trans"; - "subset_psubset_trans2"; - "psubsetD"; - "lemma_ex_mem_less_left_add1"; - "preal_less_set_not_empty"; - "lemma_ex_not_mem_less_left_add1"; - "preal_less_set_not_prat_set"; - "preal_less_set_lemma3"; - "preal_less_set_lemma4"; - "preal_mem_less_set"; - "preal_less_add_left_subsetI"; - "lemma_sum_mem_Rep_preal_ex"; - "preal_less_add_left_subsetI2"; - "preal_less_add_left"; - "preal_less_add_left_Ex"; - "preal_add_less2_mono1"; - "preal_add_less2_mono2"; - "preal_mult_less_mono1"; - "preal_mult_left_less_mono1"; - "preal_mult_left_le_mono1"; - "preal_mult_le_mono1"; - "preal_add_left_le_mono1"; - "preal_add_le_mono1"; - "preal_add_right_less_cancel"; - "preal_add_left_less_cancel"; - "preal_add_less_iff1"; - "preal_add_less_iff2"; - "preal_add_less_mono"; - "preal_mult_less_mono"; - "preal_add_right_cancel"; - "preal_add_left_cancel"; - "preal_add_left_cancel_iff"; - "preal_add_right_cancel_iff"; - "preal_sup_mem_Ex"; - "preal_sup_set_not_empty"; - "preal_sup_not_mem_Ex"; - "preal_sup_not_mem_Ex1"; - "preal_sup_set_not_prat_set"; - "preal_sup_set_not_prat_set1"; - "preal_sup_set_lemma3"; - "preal_sup_set_lemma3_1"; - "preal_sup_set_lemma4"; - "preal_sup_set_lemma4_1"; - "preal_sup"; - "preal_sup1"; - "preal_psup_leI"; - "preal_psup_leI2"; - "preal_psup_leI2b"; - "preal_psup_leI2a"; - "psup_le_ub"; - "psup_le_ub1"; - "preal_complete"; - "lemma_preal_rat_less"; - "lemma_preal_rat_less2"; - "preal_of_prat_add"; - "lemma_preal_rat_less3"; - "lemma_preal_rat_less4"; - "preal_of_prat_mult"; - "preal_of_prat_less_iff"; "(preal_of_prat ?p < preal_of_prat ?q) = (?p < ?q)" -RealDef.ML:qed --------------------------------------------------------------- - "preal_trans_lemma"; - "realrel_iff"; - "realrelI"; - "?x1.0 + ?y2.0 = ?x2.0 + ?y1.0 ==> ((?x1.0, ?y1.0), ?x2.0, ?y2.0) : realrel" - "realrelE_lemma"; - "realrelE"; - "realrel_refl"; - "equiv_realrel"; - "realrel_in_real"; - "inj_on_Abs_REAL"; - "inj_Rep_REAL"; - "inj_real_of_preal"; - "eq_Abs_REAL"; - "real_minus_congruent"; - "real_minus"; - "- Abs_REAL (realrel `` {(?x, ?y)}) = Abs_REAL (realrel `` {(?y, ?x)})" - "real_minus_minus"; (**)"- (- (?z::real)) = ?z" - "inj_real_minus"; "inj uminus" - "real_minus_zero"; (**)"- 0 = 0" - "real_minus_zero_iff"; (**)"(- ?x = 0) = (?x = 0)" - "real_add_congruent2"; - "congruent2 realrel - (%p1 p2. (%(x1, y1). (%(x2, y2). realrel `` {(x1 + x2, y1 + y2)}) p2) p1)" - "real_add"; - "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) + - Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) = - Abs_REAL (realrel `` {(?x1.0 + ?x2.0, ?y1.0 + ?y2.0)})" - "real_add_commute"; (**)"(?z::real) + (?w::real) = ?w + ?z" - "real_add_assoc"; (**) - "real_add_left_commute"; (**) - "real_add_zero_left"; (**)"0 + ?z = ?z" - "real_add_zero_right"; (**) - "real_add_minus"; (**)"?z + - ?z = 0" - "real_add_minus_left"; (**) - "real_add_minus_cancel"; (**)"?z + (- ?z + ?w) = ?w" - "real_minus_add_cancel"; (**)"- ?z + (?z + ?w) = ?w" - "real_minus_ex"; "EX y. ?x + y = 0" - "real_minus_ex1"; - "real_minus_left_ex1"; "EX! y. y + ?x = 0" - "real_add_minus_eq_minus";"?x + ?y = 0 ==> ?x = - ?y" - "real_as_add_inverse_ex"; "EX y. ?x = - y" - "real_minus_add_distrib"; (**)"- (?x + ?y) = - ?x + - ?y" - "real_add_left_cancel"; "(?x + ?y = ?x + ?z) = (?y = ?z)" - "real_add_right_cancel"; "(?y + ?x = ?z + ?x) = (?y = ?z)" - "real_diff_0"; (**)"0 - ?x = - ?x" - "real_diff_0_right"; (**)"?x - 0 = ?x" - "real_diff_self"; (**)"?x - ?x = 0" - "real_mult_congruent2_lemma"; - "real_mult_congruent2"; - "congruent2 realrel - (%p1 p2. - (%(x1, y1). - (%(x2, y2). realrel `` {(x1 * x2 + y1 * y2, x1 * y2 + x2 * y1)}) - p2) p1)" - "real_mult"; - "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) * - Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) = - Abs_REAL - (realrel `` - {(?x1.0 * ?x2.0 + ?y1.0 * ?y2.0, ?x1.0 * ?y2.0 + ?x2.0 * ?y1.0)})" - "real_mult_commute"; (**)"?z * ?w = ?w * ?z" - "real_mult_assoc"; (**) - "real_mult_left_commute"; - (**)"?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)" - "real_mult_1"; (**)"1 * ?z = ?z" - "real_mult_1_right"; (**)"?z * 1 = ?z" - "real_mult_0"; (**) - "real_mult_0_right"; (**)"?z * 0 = 0" - "real_mult_minus_eq1"; (**)"- ?x * ?y = - (?x * ?y)" - "real_mult_minus_eq2"; (**)"?x * - ?y = - (?x * ?y)" - "real_mult_minus_1"; (**)"- 1 * ?z = - ?z" - "real_mult_minus_1_right";(**)"?z * - 1 = - ?z" - "real_minus_mult_cancel"; (**)"- ?x * - ?y = ?x * ?y" - "real_minus_mult_commute";(**)"- ?x * ?y = ?x * - ?y" - "real_add_assoc_cong"; - "?z + ?v = ?z' + ?v' ==> ?z + (?v + ?w) = ?z' + (?v' + ?w)" - "real_add_assoc_swap"; (**)"?z + (?v + ?w) = ?v + (?z + ?w)" - "real_add_mult_distrib"; (**)"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w" - "real_add_mult_distrib2"; (**)"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0" - "real_diff_mult_distrib"; (**)"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w" - "real_diff_mult_distrib2";(**)"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0" - "real_zero_not_eq_one"; - "real_zero_iff"; "0 = Abs_REAL (realrel `` {(?x, ?x)})" - "real_mult_inv_right_ex"; "?x ~= 0 ==> EX y. ?x * y = 1" - "real_mult_inv_left_ex"; "?x ~= 0 ==> inverse ?x * ?x = 1" - "real_mult_inv_left"; - "real_mult_inv_right"; "?x ~= 0 ==> ?x * inverse ?x = 1" - "INVERSE_ZERO"; "inverse 0 = 0" - "DIVISION_BY_ZERO"; (*NOT for adding to default simpset*)"?a / 0 = 0" - "real_mult_left_cancel"; (**)"?c ~= 0 ==> (?c * ?a = ?c * ?b) = (?a = ?b)" - "real_mult_right_cancel"; (**)"?c ~= 0 ==> (?a * ?c = ?b * ?c) = (?a = ?b)" - "real_mult_left_cancel_ccontr"; "?c * ?a ~= ?c * ?b ==> ?a ~= ?b" - "real_mult_right_cancel_ccontr"; "?a * ?c ~= ?b * ?c ==> ?a ~= ?b" - "real_inverse_not_zero"; "?x ~= 0 ==> inverse ?x ~= 0" - "real_mult_not_zero"; "[| ?x ~= 0; ?y ~= 0 |] ==> ?x * ?y ~= 0" - "real_inverse_inverse"; "inverse (inverse ?x) = ?x" - "real_inverse_1"; "inverse 1 = 1" - "real_minus_inverse"; "inverse (- ?x) = - inverse ?x" - "real_inverse_distrib"; "inverse (?x * ?y) = inverse ?x * inverse ?y" - "real_times_divide1_eq"; (**)"?x * (?y / ?z) = ?x * ?y / ?z" - "real_times_divide2_eq"; (**)"?y / ?z * ?x = ?y * ?x / ?z" - "real_divide_divide1_eq"; (**)"?x / (?y / ?z) = ?x * ?z / ?y" - "real_divide_divide2_eq"; (**)"?x / ?y / ?z = ?x / (?y * ?z)" - "real_minus_divide_eq"; (**)"- ?x / ?y = - (?x / ?y)" - "real_divide_minus_eq"; (**)"?x / - ?y = - (?x / ?y)" - "real_add_divide_distrib"; (**)"(?x + ?y) / ?z = ?x / ?z + ?y / ?z" - "preal_lemma_eq_rev_sum"; - "[| ?x = ?y; ?x1.0 = ?y1.0 |] ==> ?x + ?y1.0 = ?x1.0 + ?y" - "preal_add_left_commute_cancel"; - "?x + (?b + ?y) = ?x1.0 + (?b + ?y1.0) ==> ?x + ?y = ?x1.0 + ?y1.0" - "preal_lemma_for_not_refl"; - "real_less_not_refl"; "~ ?R < ?R" - "real_not_refl2"; - "preal_lemma_trans"; - "real_less_trans"; - "real_less_not_sym"; - "real_of_preal_add"; - "real_of_preal (?z1.0 + ?z2.0) = real_of_preal ?z1.0 + real_of_preal ?z2.0" - "real_of_preal_mult"; - "real_of_preal_ExI"; - "real_of_preal_ExD"; - "real_of_preal_iff"; - "real_of_preal_trichotomy"; - "real_of_preal_trichotomyE"; - "real_of_preal_lessD"; - "real_of_preal_lessI"; - "?m1.0 < ?m2.0 ==> real_of_preal ?m1.0 < real_of_preal ?m2.0" - "real_of_preal_less_iff1"; - "real_of_preal_minus_less_self"; - "real_of_preal_minus_less_zero"; - "real_of_preal_not_minus_gt_zero"; - "real_of_preal_zero_less"; - "real_of_preal_not_less_zero"; - "real_minus_minus_zero_less"; - "real_of_preal_sum_zero_less"; - "real_of_preal_minus_less_all"; - "real_of_preal_not_minus_gt_all"; - "real_of_preal_minus_less_rev1"; - "real_of_preal_minus_less_rev2"; - "real_of_preal_minus_less_rev_iff"; - "real_linear"; "?R1.0 < ?R2.0 | ?R1.0 = ?R2.0 | ?R2.0 < ?R1.0" - "real_neq_iff"; - "real_linear_less2"; - "[| ?R1.0 < ?R2.0 ==> ?P; ?R1.0 = ?R2.0 ==> ?P; ?R2.0 < ?R1.0 ==> ?P |] - ==> ?P" - "real_leI"; - "real_leD"; "~ ?w < ?z ==> ?z <= ?w" - "real_less_le_iff"; - "not_real_leE"; - "real_le_imp_less_or_eq"; - "real_less_or_eq_imp_le"; - "real_le_less"; - "real_le_refl"; "?w <= ?w" - "real_le_linear"; - "real_le_trans"; "[| ?i <= ?j; ?j <= ?k |] ==> ?i <= ?k" - "real_le_anti_sym"; "[| ?z <= ?w; ?w <= ?z |] ==> ?z = ?w" - "not_less_not_eq_real_less"; - "real_less_le"; "(?w < ?z) = (?w <= ?z & ?w ~= ?z)" - "real_minus_zero_less_iff"; - "real_minus_zero_less_iff2"; - "real_less_add_positive_left_Ex"; - "real_less_sum_gt_zero"; "?W < ?S ==> 0 < ?S + - ?W" - "real_lemma_change_eq_subj"; - "real_sum_gt_zero_less"; "0 < ?S + - ?W ==> ?W < ?S" - "real_less_sum_gt_0_iff"; "(0 < ?S + - ?W) = (?W < ?S)" - "real_less_eq_diff"; "(?x < ?y) = (?x - ?y < 0)" - "real_add_diff_eq"; (**)"?x + (?y - ?z) = ?x + ?y - ?z" - "real_diff_add_eq"; (**)"?x - ?y + ?z = ?x + ?z - ?y" - "real_diff_diff_eq"; (**)"?x - ?y - ?z = ?x - (?y + ?z)" - "real_diff_diff_eq2"; (**)"?x - (?y - ?z) = ?x + ?z - ?y" - "real_diff_less_eq"; "(?x - ?y < ?z) = (?x < ?z + ?y)" - "real_less_diff_eq"; - "real_diff_le_eq"; "(?x - ?y <= ?z) = (?x <= ?z + ?y)" - "real_le_diff_eq"; - "real_diff_eq_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)" - "real_eq_diff_eq"; (**)"(?x - ?y = ?z) = (?x = ?z + ?y)" - "real_less_eqI"; - "real_le_eqI"; - "real_eq_eqI"; "?x - ?y = ?x' - ?y' ==> (?x = ?y) = (?x' = ?y')" -RealOrd.ML:qed --------------------------------------------------------------- - "real_add_cancel_21"; "(?x + (?y + ?z) = ?y + ?u) = (?x + ?z = ?u)" - "real_add_cancel_end"; "(?x + (?y + ?z) = ?y) = (?x = - ?z)" - "real_minus_diff_eq"; (*??*)"- (?x - ?y) = ?y - ?x" - "real_gt_zero_preal_Ex"; - "real_gt_preal_preal_Ex"; - "real_ge_preal_preal_Ex"; - "real_less_all_preal"; "?y <= 0 ==> ALL x. ?y < real_of_preal x" - "real_less_all_real2"; - "real_lemma_add_positive_imp_less"; - "real_ex_add_positive_left_less";"EX T. 0 < T & ?R + T = ?S ==> ?R < ?S" - "real_less_iff_add"; - "real_of_preal_le_iff"; - "real_mult_order"; "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x * ?y" - "neg_real_mult_order"; - "real_mult_less_0"; "[| 0 < ?x; ?y < 0 |] ==> ?x * ?y < 0" - "real_zero_less_one"; "0 < 1" - "real_add_right_cancel_less"; "(?v + ?z < ?w + ?z) = (?v < ?w)" - "real_add_left_cancel_less"; - "real_add_right_cancel_le"; - "real_add_left_cancel_le"; - "real_add_less_le_mono"; "[| ?w' < ?w; ?z' <= ?z |] ==> ?w' + ?z' < ?w + ?z" - "real_add_le_less_mono"; "[| ?w' <= ?w; ?z' < ?z |] ==> ?w' + ?z' < ?w + ?z" - "real_add_less_mono2"; - "real_less_add_right_cancel"; - "real_less_add_left_cancel"; "?C + ?A < ?C + ?B ==> ?A < ?B" - "real_le_add_right_cancel"; - "real_le_add_left_cancel"; "?C + ?A <= ?C + ?B ==> ?A <= ?B" - "real_add_order"; "[| 0 < ?x; 0 < ?y |] ==> 0 < ?x + ?y" - "real_le_add_order"; - "real_add_less_mono"; - "real_add_left_le_mono1"; - "real_add_le_mono"; - "real_less_Ex"; - "real_add_minus_positive_less_self"; "0 < ?r ==> ?u + - ?r < ?u" - "real_le_minus_iff"; "(- ?s <= - ?r) = (?r <= ?s)" - "real_le_square"; - "real_of_posnat_one"; - "real_of_posnat_two"; - "real_of_posnat_add"; "real_of_posnat ?n1.0 + real_of_posnat ?n2.0 = - real_of_posnat (?n1.0 + ?n2.0) + 1" - "real_of_posnat_add_one"; - "real_of_posnat_Suc"; - "inj_real_of_posnat"; - "real_of_nat_zero"; - "real_of_nat_one"; "real (Suc 0) = 1" - "real_of_nat_add"; - "real_of_nat_Suc"; - "real_of_nat_less_iff"; - "real_of_nat_le_iff"; - "inj_real_of_nat"; - "real_of_nat_ge_zero"; - "real_of_nat_mult"; - "real_of_nat_inject"; -RealOrd.ML:qed_spec_mp - "real_of_nat_diff"; -RealOrd.ML:qed - "real_of_nat_zero_iff"; - "real_of_nat_neg_int"; - "real_inverse_gt_0"; - "real_inverse_less_0"; - "real_mult_less_mono1"; - "real_mult_less_mono2"; - "real_mult_less_cancel1"; - "(?k * ?m < ?k * ?n) = (0 < ?k & ?m < ?n | ?k < 0 & ?n < ?m)" - "real_mult_less_cancel2"; - "real_mult_less_iff1"; - "real_mult_less_iff2"; - "real_mult_le_cancel_iff1"; - "real_mult_le_cancel_iff2"; - "real_mult_le_less_mono1"; - "real_mult_less_mono"; - "real_mult_less_mono'"; - "real_gt_zero"; "1 <= ?x ==> 0 < ?x" - "real_mult_self_le"; "[| 1 < ?r; 1 <= ?x |] ==> ?x <= ?r * ?x" - "real_mult_self_le2"; - "real_inverse_less_swap"; - "real_mult_is_0"; - "real_inverse_add"; - "real_minus_zero_le_iff"; - "real_minus_zero_le_iff2"; - "real_sum_squares_cancel"; "?x * ?x + ?y * ?y = 0 ==> ?x = 0" - "real_sum_squares_cancel2"; "?x * ?x + ?y * ?y = 0 ==> ?y = 0" - "real_0_less_mult_iff"; - "real_0_le_mult_iff"; - "real_mult_less_0_iff"; "(?x * ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)" - "real_mult_le_0_iff"; -RealInt.ML:qed --------------------------------------------------------------- - "real_of_int_congruent"; - "real_of_int"; "real (Abs_Integ (intrel `` {(?i, ?j)})) = - Abs_REAL - (realrel `` - {(preal_of_prat (prat_of_pnat (pnat_of_nat ?i)), - preal_of_prat (prat_of_pnat (pnat_of_nat ?j)))})" - "inj_real_of_int"; - "real_of_int_zero"; - "real_of_one"; - "real_of_int_add"; "real ?x + real ?y = real (?x + ?y)" - "real_of_int_minus"; - "real_of_int_diff"; - "real_of_int_mult"; "real ?x * real ?y = real (?x * ?y)" - "real_of_int_Suc"; - "real_of_int_real_of_nat"; - "real_of_nat_real_of_int"; - "real_of_int_zero_cancel"; - "real_of_int_less_cancel"; - "real_of_int_inject"; - "real_of_int_less_mono"; - "real_of_int_less_iff"; - "real_of_int_le_iff"; -RealBin.ML:qed --------------------------------------------------------------- - "real_number_of"; "real (number_of ?w) = number_of ?w" - "real_numeral_0_eq_0"; - "real_numeral_1_eq_1"; - "add_real_number_of"; - "minus_real_number_of"; - "diff_real_number_of"; - "mult_real_number_of"; - "real_mult_2"; (**)"2 * ?z = ?z + ?z" - "real_mult_2_right"; (**)"?z * 2 = ?z + ?z" - "eq_real_number_of"; - "less_real_number_of"; - "le_real_number_of_eq_not_less"; - "real_minus_1_eq_m1"; "- 1 = -1"(*uminus.. = "-.."*) - "real_mult_minus1"; (**)"-1 * ?z = - ?z" - "real_mult_minus1_right"; (**)"?z * -1 = - ?z" - "zero_less_real_of_nat_iff";"(0 < real ?n) = (0 < ?n)" - "zero_le_real_of_nat_iff"; - "real_add_number_of_left"; - "real_mult_number_of_left"; - "number_of ?v * (number_of ?w * ?z) = number_of (bin_mult ?v ?w) * ?z" - "real_add_number_of_diff1"; - "real_add_number_of_diff2";"number_of ?v + (?c - number_of ?w) = - number_of (bin_add ?v (bin_minus ?w)) + ?c" - "real_of_nat_number_of"; - "real (number_of ?v) = (if neg (number_of ?v) then 0 else number_of ?v)" - "real_less_iff_diff_less_0"; "(?x < ?y) = (?x - ?y < 0)" - "real_eq_iff_diff_eq_0"; - "real_le_iff_diff_le_0"; - "left_real_add_mult_distrib"; - (**)"?i * ?u + (?j * ?u + ?k) = (?i + ?j) * ?u + ?k" - "real_eq_add_iff1"; - "(?i * ?u + ?m = ?j * ?u + ?n) = ((?i - ?j) * ?u + ?m = ?n)" - "real_eq_add_iff2"; - "real_less_add_iff1"; - "real_less_add_iff2"; - "real_le_add_iff1"; - "real_le_add_iff2"; - "real_mult_le_mono1"; - "real_mult_le_mono2"; - "real_mult_le_mono"; - "[| ?i <= ?j; ?k <= ?l; 0 <= ?j; 0 <= ?k |] ==> ?i * ?k <= ?j * ?l" -RealArith0.ML:qed ------------------------------------------------------------ - "real_diff_minus_eq"; (**)"?x - - ?y = ?x + ?y" - "real_0_divide"; (**)"0 / ?x = 0" - "real_0_less_inverse_iff"; "(0 < inverse ?x) = (0 < ?x)" - "real_inverse_less_0_iff"; - "real_0_le_inverse_iff"; - "real_inverse_le_0_iff"; - "REAL_DIVIDE_ZERO"; "?x / 0 = 0"(*!!!*) - "real_inverse_eq_divide"; - "real_0_less_divide_iff";"(0 < ?x / ?y) = (0 < ?x & 0 < ?y | ?x < 0 & ?y < 0)" - "real_divide_less_0_iff";"(?x / ?y < 0) = (0 < ?x & ?y < 0 | ?x < 0 & 0 < ?y)" - "real_0_le_divide_iff"; - "real_divide_le_0_iff"; - "(?x / ?y <= 0) = ((?x <= 0 | ?y <= 0) & (0 <= ?x | 0 <= ?y))" - "real_inverse_zero_iff"; - "real_divide_eq_0_iff"; "(?x / ?y = 0) = (?x = 0 | ?y = 0)"(*!!!*) - "real_divide_self_eq"; "?h ~= 0 ==> ?h / ?h = 1"(**) - "real_minus_less_minus"; "(- ?y < - ?x) = (?x < ?y)" - "real_mult_less_mono1_neg"; "[| ?i < ?j; ?k < 0 |] ==> ?j * ?k < ?i * ?k" - "real_mult_less_mono2_neg"; - "real_mult_le_mono1_neg"; - "real_mult_le_mono2_neg"; - "real_mult_less_cancel2"; - "real_mult_le_cancel2"; - "real_mult_less_cancel1"; - "real_mult_le_cancel1"; - "real_mult_eq_cancel1"; "(?k * ?m = ?k * ?n) = (?k = 0 | ?m = ?n)" - "real_mult_eq_cancel2"; "(?m * ?k = ?n * ?k) = (?k = 0 | ?m = ?n)" - "real_mult_div_cancel1"; (**)"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n" - "real_mult_div_cancel_disj"; - "?k * ?m / (?k * ?n) = (if ?k = 0 then 0 else ?m / ?n)" - "pos_real_le_divide_eq"; - "neg_real_le_divide_eq"; - "pos_real_divide_le_eq"; - "neg_real_divide_le_eq"; - "pos_real_less_divide_eq"; - "neg_real_less_divide_eq"; - "pos_real_divide_less_eq"; - "neg_real_divide_less_eq"; - "real_eq_divide_eq"; (**)"?z ~= 0 ==> (?x = ?y / ?z) = (?x * ?z = ?y)" - "real_divide_eq_eq"; (**)"?z ~= 0 ==> (?y / ?z = ?x) = (?y = ?x * ?z)" - "real_divide_eq_cancel2"; "(?m / ?k = ?n / ?k) = (?k = 0 | ?m = ?n)" - "real_divide_eq_cancel1"; "(?k / ?m = ?k / ?n) = (?k = 0 | ?m = ?n)" - "real_inverse_less_iff"; - "real_inverse_le_iff"; - "real_divide_1"; (**)"?x / 1 = ?x" - "real_divide_minus1"; (**)"?x / -1 = - ?x" - "real_minus1_divide"; (**)"-1 / ?x = - (1 / ?x)" - "real_lbound_gt_zero"; - "[| 0 < ?d1.0; 0 < ?d2.0 |] ==> EX e. 0 < e & e < ?d1.0 & e < ?d2.0" - "real_inverse_eq_iff"; "(inverse ?x = inverse ?y) = (?x = ?y)" - "real_divide_eq_iff"; "(?z / ?x = ?z / ?y) = (?z = 0 | ?x = ?y)" - "real_less_minus"; "(?x < - ?y) = (?y < - ?x)" - "real_minus_less"; "(- ?x < ?y) = (- ?y < ?x)" - "real_le_minus"; - "real_minus_le"; "(- ?x <= ?y) = (- ?y <= ?x)" - "real_equation_minus"; (**)"(?x = - ?y) = (?y = - ?x)" - "real_minus_equation"; (**)"(- ?x = ?y) = (- ?y = ?x)" - "real_add_minus_iff"; (**)"(?x + - ?a = 0) = (?x = ?a)" - "real_minus_eq_cancel"; (**)"(- ?b = - ?a) = (?b = ?a)" - "real_add_eq_0_iff"; (**)"(?x + ?y = 0) = (?y = - ?x)" - "real_add_less_0_iff"; "(?x + ?y < 0) = (?y < - ?x)" - "real_0_less_add_iff"; - "real_add_le_0_iff"; - "real_0_le_add_iff"; - "real_0_less_diff_iff"; "(0 < ?x - ?y) = (?y < ?x)" - "real_0_le_diff_iff"; - "real_minus_diff_eq"; (**)"- (?x - ?y) = ?y - ?x" - "real_less_half_sum"; "?x < ?y ==> ?x < (?x + ?y) / 2" - "real_gt_half_sum"; - "real_dense"; "?x < ?y ==> EX r. ?x < r & r < ?y" -RealArith ///!!!///----------------------------------------------------------- -RComplete.ML:qed ------------------------------------------------------------- - "real_sum_of_halves"; (**)"?x / 2 + ?x / 2 = ?x" - "real_sup_lemma1"; - "real_sup_lemma2"; - "posreal_complete"; - "real_isLub_unique"; - "real_order_restrict"; - "posreals_complete"; - "real_sup_lemma3"; - "lemma_le_swap2"; - "lemma_real_complete2b"; - "reals_complete"; - "real_of_nat_Suc_gt_zero"; - "reals_Archimedean"; "0 < ?x ==> EX n. inverse (real (Suc n)) < ?x" - "reals_Archimedean2"; -RealAbs.ML:qed - "abs_nat_number_of"; - "abs (number_of ?v) = - (if neg (number_of ?v) then number_of (bin_minus ?v) else number_of ?v)" - "abs_split"; - "abs_iff"; - "abs_zero"; "abs 0 = 0" - "abs_one"; - "abs_eqI1"; - "abs_eqI2"; - "abs_minus_eqI2"; - "abs_minus_eqI1"; - "abs_ge_zero"; "0 <= abs ?x" - "abs_idempotent"; "abs (abs ?x) = abs ?x" - "abs_zero_iff"; "(abs ?x = 0) = (?x = 0)" - "abs_ge_self"; "?x <= abs ?x" - "abs_ge_minus_self"; - "abs_mult"; "abs (?x * ?y) = abs ?x * abs ?y" - "abs_inverse"; "abs (inverse ?x) = inverse (abs ?x)" - "abs_mult_inverse"; - "abs_triangle_ineq"; "abs (?x + ?y) <= abs ?x + abs ?y" - "abs_triangle_ineq_four"; - "abs_minus_cancel"; - "abs_minus_add_cancel"; - "abs_triangle_minus_ineq"; -RealAbs.ML:qed_spec_mp - "abs_add_less"; "[| abs ?x < ?r; abs ?y < ?s |] ==> abs (?x + ?y) < ?r + ?s" -RealAbs.ML:qed - "abs_add_minus_less"; - "real_mult_0_less"; "(0 * ?x < ?r) = (0 < ?r)" - "real_mult_less_trans"; - "real_mult_le_less_trans"; - "abs_mult_less"; - "abs_mult_less2"; - "abs_less_gt_zero"; - "abs_minus_one"; "abs -1 = 1" - "abs_disj"; "abs ?x = ?x | abs ?x = - ?x" - "abs_interval_iff"; - "abs_le_interval_iff"; - "abs_add_pos_gt_zero"; - "abs_add_one_gt_zero"; - "abs_not_less_zero"; - "abs_circle"; "abs ?h < abs ?y - abs ?x ==> abs (?x + ?h) < abs ?y" - "abs_le_zero_iff"; - "real_0_less_abs_iff"; - "abs_real_of_nat_cancel"; - "abs_add_one_not_less_self"; - "abs_triangle_ineq_three"; "abs (?w + ?x + ?y) <= abs ?w + abs ?x + abs ?y" - "abs_diff_less_imp_gt_zero"; - "abs_diff_less_imp_gt_zero2"; - "abs_diff_less_imp_gt_zero3"; - "abs_diff_less_imp_gt_zero4"; - "abs_triangle_ineq_minus_cancel"; - "abs_sum_triangle_ineq"; - "abs (?x + ?y + (- ?l + - ?m)) <= abs (?x + - ?l) + abs (?y + - ?m)" -RealPow.ML:qed - "realpow_zero"; "0 ^ Suc ?n = 0" -RealPow.ML:qed_spec_mp - "realpow_not_zero"; "?r ~= 0 ==> ?r ^ ?n ~= 0" - "realpow_zero_zero"; "?r ^ ?n = 0 ==> ?r = 0" - "realpow_inverse"; "inverse (?r ^ ?n) = inverse ?r ^ ?n" - "realpow_abs"; "abs (?r ^ ?n) = abs ?r ^ ?n" - "realpow_add"; (**)"?r ^ (?n + ?m) = ?r ^ ?n * ?r ^ ?m" - "realpow_one"; (**)"?r ^ 1 = ?r" - "realpow_two"; (**)"?r ^ Suc (Suc 0) = ?r * ?r" -RealPow.ML:qed_spec_mp - "realpow_gt_zero"; "0 < ?r ==> 0 < ?r ^ ?n" - "realpow_ge_zero"; "0 <= ?r ==> 0 <= ?r ^ ?n" - "realpow_le"; "0 <= ?x & ?x <= ?y ==> ?x ^ ?n <= ?y ^ ?n" - "realpow_less"; -RealPow.ML:qed - "realpow_eq_one"; (**)"1 ^ ?n = 1" - "abs_realpow_minus_one"; "abs (-1 ^ ?n) = 1" - "realpow_mult"; (**)"(?r * ?s) ^ ?n = ?r ^ ?n * ?s ^ ?n" - "realpow_two_le"; "0 <= ?r ^ Suc (Suc 0)" - "abs_realpow_two"; - "realpow_two_abs"; "abs ?x ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)" - "realpow_two_gt_one"; -RealPow.ML:qed_spec_mp - "realpow_ge_one"; "1 < ?r ==> 1 <= ?r ^ ?n" -RealPow.ML:qed - "realpow_ge_one2"; - "two_realpow_ge_one"; - "two_realpow_gt"; - "realpow_minus_one"; (**)"-1 ^ (2 * ?n) = 1" - "realpow_minus_one_odd"; "-1 ^ Suc (2 * ?n) = - 1" - "realpow_minus_one_even"; -RealPow.ML:qed_spec_mp - "realpow_Suc_less"; - "realpow_Suc_le"; "0 <= ?r & ?r < 1 ==> ?r ^ Suc ?n <= ?r ^ ?n" -RealPow.ML:qed - "realpow_zero_le"; "0 <= 0 ^ ?n" -RealPow.ML:qed_spec_mp - "realpow_Suc_le2"; -RealPow.ML:qed - "realpow_Suc_le3"; -RealPow.ML:qed_spec_mp - "realpow_less_le"; "0 <= ?r & ?r < 1 & ?n < ?N ==> ?r ^ ?N <= ?r ^ ?n" -RealPow.ML:qed - "realpow_le_le"; "[| 0 <= ?r; ?r < 1; ?n <= ?N |] ==> ?r ^ ?N <= ?r ^ ?n" - "realpow_Suc_le_self"; - "realpow_Suc_less_one"; -RealPow.ML:qed_spec_mp - "realpow_le_Suc"; - "realpow_less_Suc"; - "realpow_le_Suc2"; - "realpow_gt_ge"; - "realpow_gt_ge2"; -RealPow.ML:qed - "realpow_ge_ge"; "[| 1 < ?r; ?n <= ?N |] ==> ?r ^ ?n <= ?r ^ ?N" - "realpow_ge_ge2"; -RealPow.ML:qed_spec_mp - "realpow_Suc_ge_self"; - "realpow_Suc_ge_self2"; -RealPow.ML:qed - "realpow_ge_self"; - "realpow_ge_self2"; -RealPow.ML:qed_spec_mp - "realpow_minus_mult"; "0 < ?n ==> ?x ^ (?n - 1) * ?x = ?x ^ ?n" - "realpow_two_mult_inverse"; - "?r ~= 0 ==> ?r * inverse ?r ^ Suc (Suc 0) = inverse ?r" - "realpow_two_minus"; "(- ?x) ^ Suc (Suc 0) = ?x ^ Suc (Suc 0)" - "realpow_two_diff"; - "realpow_two_disj"; - "realpow_diff"; - "[| ?x ~= 0; ?m <= ?n |] ==> ?x ^ (?n - ?m) = ?x ^ ?n * inverse (?x ^ ?m)" - "realpow_real_of_nat"; - "realpow_real_of_nat_two_pos"; "0 < real (Suc (Suc 0) ^ ?n)" -RealPow.ML:qed_spec_mp - "realpow_increasing"; - "realpow_Suc_cancel_eq"; - "[| 0 <= ?x; 0 <= ?y; ?x ^ Suc ?n = ?y ^ Suc ?n |] ==> ?x = ?y" -RealPow.ML:qed - "realpow_eq_0_iff"; "(?x ^ ?n = 0) = (?x = 0 & 0 < ?n)" - "zero_less_realpow_abs_iff"; - "zero_le_realpow_abs"; - "real_of_int_power"; "real ?x ^ ?n = real (?x ^ ?n)" - "power_real_number_of"; "number_of ?v ^ ?n = real (number_of ?v ^ ?n)" -Ring_and_Field ---///!!!///--------------------------------------------------- -Complex_Numbers --///!!!///--------------------------------------------------- -Real -------------///!!!///--------------------------------------------------- -real_arith0.ML:qed ""; -real_arith0.ML:qed ""; -real_arith0.ML:qed ""; -real_arith0.ML:qed ""; -real_arith0.ML:qed ""; -real_arith0.ML:qed ""; -real_arith0.ML:qed ""; -real_arith0.ML:qed ""; -real_arith0.ML:qed ""; - - - - - - - -