# HG changeset patch # User paulson # Date 935080601 -7200 # Node ID dff3470c5c62669b1c688796f12fc46ad0baae91 # Parent 8aa66ddc0bea0f110e8771abba1b30e0c80d46a9 real literals using binary arithmetic diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/Hyperreal/HyperDef.thy --- a/src/HOL/Real/Hyperreal/HyperDef.thy Thu Aug 19 17:06:05 1999 +0200 +++ b/src/HOL/Real/Hyperreal/HyperDef.thy Thu Aug 19 18:36:41 1999 +0200 @@ -5,7 +5,7 @@ Description : Construction of hyperreals using ultrafilters *) -HyperDef = Filter + Real + +HyperDef = Filter + RealBin + consts diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/PNat.ML --- a/src/HOL/Real/PNat.ML Thu Aug 19 17:06:05 1999 +0200 +++ b/src/HOL/Real/PNat.ML Thu Aug 19 18:36:41 1999 +0200 @@ -708,3 +708,9 @@ qed "pnat_of_nat_less_iff"; Addsimps [pnat_of_nat_less_iff RS sym]; +goalw PNat.thy [pnat_mult_def,pnat_of_nat_def] + "pnat_of_nat n1 * pnat_of_nat n2 = \ +\ pnat_of_nat (n1 * n2 + n1 + n2)"; +by (auto_tac (claset(),simpset() addsimps [mult_Rep_pnat_mult, + pnat_add_def,Abs_pnat_inverse,gt_0_mem_pnat])); +qed "pnat_of_nat_mult"; diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/RComplete.thy --- a/src/HOL/Real/RComplete.thy Thu Aug 19 17:06:05 1999 +0200 +++ b/src/HOL/Real/RComplete.thy Thu Aug 19 18:36:41 1999 +0200 @@ -6,5 +6,5 @@ reals and reals *) -RComplete = Lubs + Real +RComplete = Lubs + RealBin diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/ROOT.ML --- a/src/HOL/Real/ROOT.ML Thu Aug 19 17:06:05 1999 +0200 +++ b/src/HOL/Real/ROOT.ML Thu Aug 19 18:36:41 1999 +0200 @@ -11,7 +11,6 @@ set proof_timing; time_use_thy "RealDef"; use "simproc.ML"; -time_use_thy "RealAbs"; time_use_thy "RComplete"; time_use_thy "Hyperreal/Filter"; time_use_thy "Hyperreal/HyperDef"; diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/Real.ML --- a/src/HOL/Real/Real.ML Thu Aug 19 17:06:05 1999 +0200 +++ b/src/HOL/Real/Real.ML Thu Aug 19 18:36:41 1999 +0200 @@ -280,7 +280,7 @@ qed "real_of_posnat_two"; Goalw [real_of_posnat_def] - "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r"; + "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r"; by (full_simp_tac (simpset() addsimps [real_of_posnat_one RS sym, real_of_posnat_def,real_of_preal_add RS sym,preal_of_prat_add RS sym, prat_of_pnat_add RS sym,pnat_of_nat_add]) 1); @@ -292,13 +292,9 @@ by (full_simp_tac (simpset() addsimps [real_of_posnat_two,real_add_assoc]) 1); qed "real_of_posnat_add_one"; -Goal "Suc n = n + 1"; -by Auto_tac; -qed "lemmaS"; - Goal "real_of_posnat (Suc n) = real_of_posnat n + 1r"; -by (stac lemmaS 1); -by (rtac real_of_posnat_add_one 1); +by (stac (real_of_posnat_add_one RS sym) 1); +by (Simp_tac 1); qed "real_of_posnat_Suc"; Goal "inj(real_of_posnat)"; @@ -369,7 +365,7 @@ qed "real_of_posnat_rinv_gt_zero"; Addsimps [real_of_posnat_rinv_gt_zero]; -Goal "x+x=x*(1r+1r)"; +Goal "x+x = x*(1r+1r)"; by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1); qed "real_add_self"; @@ -452,8 +448,7 @@ by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset())); qed "real_mult_le_le_mono1"; -Goal "[| 0r < r1; r1 r1 * x < r2 * y"; +Goal "[| 0r < r1; r1 r1 * x < r2 * y"; by (dres_inst_tac [("x","x")] real_mult_less_mono2 1); by (dres_inst_tac [("R1.0","0r")] real_less_trans 2); by (dres_inst_tac [("x","r1")] real_mult_less_mono1 3); @@ -461,22 +456,19 @@ by (blast_tac (claset() addIs [real_less_trans]) 1); qed "real_mult_less_mono"; -Goal "[| 0r < r1; r1 0r < r2 * y"; +Goal "[| 0r < r1; r1 0r < r2 * y"; by (dres_inst_tac [("R1.0","0r")] real_less_trans 1); by (assume_tac 1); by (blast_tac (claset() addIs [real_mult_order]) 1); qed "real_mult_order_trans"; -Goal "[| 0r < r1; r1 r1 * x < r2 * y"; +Goal "[| 0r < r1; r1 r1 * x < r2 * y"; by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] addIs [real_mult_less_mono,real_mult_order_trans], simpset())); qed "real_mult_less_mono3"; -Goal "[| 0r <= r1; r1 r1 * x < r2 * y"; +Goal "[| 0r <= r1; r1 r1 * x < r2 * y"; by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] addIs [real_mult_less_mono,real_mult_order_trans, real_mult_order], @@ -486,8 +478,7 @@ by (blast_tac (claset() addIs [real_mult_order]) 1); qed "real_mult_less_mono4"; -Goal "[| 0r < r1; r1 <= r2; 0r <= x; x <= y |] \ -\ ==> r1 * x <= r2 * y"; +Goal "[| 0r < r1; r1 <= r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y"; by (rtac real_less_or_eq_imp_le 1); by (REPEAT(dtac real_le_imp_less_or_eq 1)); by (auto_tac (claset() addIs [real_mult_less_mono, @@ -495,8 +486,7 @@ simpset())); qed "real_mult_le_mono"; -Goal "[| 0r < r1; r1 < r2; 0r <= x; x <= y |] \ -\ ==> r1 * x <= r2 * y"; +Goal "[| 0r < r1; r1 < r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y"; by (rtac real_less_or_eq_imp_le 1); by (REPEAT(dtac real_le_imp_less_or_eq 1)); by (auto_tac (claset() addIs [real_mult_less_mono, real_mult_order_trans, @@ -504,16 +494,14 @@ simpset())); qed "real_mult_le_mono2"; -Goal "[| 0r <= r1; r1 < r2; 0r <= x; x <= y |] \ -\ ==> r1 * x <= r2 * y"; +Goal "[| 0r <= r1; r1 < r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y"; by (dtac real_le_imp_less_or_eq 1); by (auto_tac (claset() addIs [real_mult_le_mono2],simpset())); by (dtac real_le_trans 1 THEN assume_tac 1); by (auto_tac (claset() addIs [real_less_le_mult_order], simpset())); qed "real_mult_le_mono3"; -Goal "[| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] \ -\ ==> r1 * x <= r2 * y"; +Goal "[| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y"; by (dres_inst_tac [("x","r1")] real_le_imp_less_or_eq 1); by (auto_tac (claset() addIs [real_mult_le_mono3, real_mult_le_le_mono1], simpset())); diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/RealBin.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/RealBin.ML Thu Aug 19 18:36:41 1999 +0200 @@ -0,0 +1,153 @@ +(* Title: HOL/RealBin.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1999 University of Cambridge + +Binary arithmetic for the reals (integer literals only) +*) + +(** real_of_int (coercion from int to real) **) + +Goal "real_of_int (number_of w) = number_of w"; +by (simp_tac (simpset() addsimps [real_number_of_def]) 1); +qed "real_number_of"; +Addsimps [real_number_of]; + +Goalw [real_number_of_def] "0r = #0"; +by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1); +qed "zero_eq_numeral_0"; + +Goalw [real_number_of_def] "1r = #1"; +by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1); +qed "one_eq_numeral_1"; + +(** Addition **) + +Goal "(number_of v :: real) + number_of v' = number_of (bin_add v v')"; +by (simp_tac + (simpset_of Int.thy addsimps [real_number_of_def, + real_of_int_add, number_of_add]) 1); +qed "add_real_number_of"; + +Addsimps [add_real_number_of]; + + +(** Subtraction **) + +Goalw [real_number_of_def] "- (number_of w :: real) = number_of (bin_minus w)"; +by (simp_tac + (simpset_of Int.thy addsimps [number_of_minus, real_of_int_minus]) 1); +qed "minus_real_number_of"; + +Goalw [real_number_of_def] + "(number_of v :: real) - number_of w = number_of (bin_add v (bin_minus w))"; +by (simp_tac + (simpset_of Int.thy addsimps [diff_number_of_eq, real_of_int_diff]) 1); +qed "diff_real_number_of"; + +Addsimps [minus_real_number_of, diff_real_number_of]; + + +(** Multiplication **) + +Goal "(number_of v :: real) * number_of v' = number_of (bin_mult v v')"; +by (simp_tac + (simpset_of Int.thy addsimps [real_number_of_def, + real_of_int_mult, number_of_mult]) 1); +qed "mult_real_number_of"; + +Addsimps [mult_real_number_of]; + + +(*** Comparisons ***) + +(** Equals (=) **) + +Goal "((number_of v :: real) = number_of v') = \ +\ iszero (number_of (bin_add v (bin_minus v')))"; +by (simp_tac + (simpset_of Int.thy addsimps [real_number_of_def, + real_of_int_eq_iff, eq_number_of_eq]) 1); +qed "eq_real_number_of"; + +Addsimps [eq_real_number_of]; + +(** Less-than (<) **) + +(*"neg" is used in rewrite rules for binary comparisons*) +Goal "((number_of v :: real) < number_of v') = \ +\ neg (number_of (bin_add v (bin_minus v')))"; +by (simp_tac + (simpset_of Int.thy addsimps [real_number_of_def, real_of_int_less_iff, + less_number_of_eq_neg]) 1); +qed "less_real_number_of"; + +Addsimps [less_real_number_of]; + + +(** Less-than-or-equals (<=) **) + +Goal "(number_of x <= (number_of y::real)) = \ +\ (~ number_of y < (number_of x::real))"; +by (rtac (linorder_not_less RS sym) 1); +qed "le_real_number_of_eq_not_less"; + +Addsimps [le_real_number_of_eq_not_less]; + + +(** rabs (absolute value) **) + +Goalw [rabs_def] + "rabs (number_of v :: real) = \ +\ (if neg (number_of v) then number_of (bin_minus v) \ +\ else number_of v)"; +by (simp_tac + (simpset_of Int.thy addsimps + bin_arith_simps@ + [minus_real_number_of, zero_eq_numeral_0, le_real_number_of_eq_not_less, + less_real_number_of, real_of_int_le_iff]) 1); +qed "rabs_nat_number_of"; + +Addsimps [rabs_nat_number_of]; + + +(*** New versions of existing theorems involving 0r, 1r ***) + +Goal "- #1 = (#-1::real)"; +by (Simp_tac 1); +qed "minus_numeral_one"; + + +(*Maps 0r to #0 and 1r to #1 and -1r to #-1*) +val real_numeral_ss = + HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, + minus_numeral_one]; + +fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th); + + +fun inst x t = read_instantiate_sg (sign_of RealBin.thy) [(x,t)]; + + +(*Now insert some identities previously stated for 0r and 1r*) + +(** RealDef & Real **) + +Addsimps (map (rename_numerals thy) + [real_minus_zero, real_minus_zero_iff, + real_add_zero_left, real_add_zero_right, + real_diff_0, real_diff_0_right, + real_mult_0_right, real_mult_0, real_mult_1_right, real_mult_1, + real_mult_minus_1_right, real_mult_minus_1, real_rinv_1, + real_minus_zero_less_iff]); + +(** RealPow **) + +Addsimps (map (rename_numerals thy) + [realpow_zero, realpow_two_le, realpow_zero_le, + realpow_eq_one, rabs_minus_realpow_one, rabs_realpow_minus_one, + realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]); + +(*Perhaps add some theorems that aren't in the default simpset, as + done in Integ/NatBin.ML*) + diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/RealBin.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/RealBin.thy Thu Aug 19 18:36:41 1999 +0200 @@ -0,0 +1,21 @@ +(* Title: HOL/RealBin.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1999 University of Cambridge + +Binary arithmetic for the reals + +This case is reduced to that for the integers +*) + +RealBin = RealInt + Bin + RealPow + + +instance + real :: number + +defs + real_number_of_def + "number_of v == real_of_int (number_of v)" + (*::bin=>real ::bin=>int*) + +end diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/RealDef.ML --- a/src/HOL/Real/RealDef.ML Thu Aug 19 17:06:05 1999 +0200 +++ b/src/HOL/Real/RealDef.ML Thu Aug 19 18:36:41 1999 +0200 @@ -748,8 +748,8 @@ Goalw [real_zero_def] "- real_of_preal m < 0r"; by (auto_tac (claset(), - simpset() addsimps [real_of_preal_def, - real_less_def,real_minus])); + simpset() addsimps [real_of_preal_def, + real_less_def,real_minus])); by (REPEAT(rtac exI 1)); by (EVERY[rtac conjI 1, rtac conjI 2]); by (REPEAT(Blast_tac 2)); @@ -776,7 +776,7 @@ Goal "~ real_of_preal m < 0r"; by (cut_facts_tac [real_of_preal_zero_less] 1); by (blast_tac (claset() addDs [real_less_trans] - addEs [real_less_irrefl]) 1); + addEs [real_less_irrefl]) 1); qed "real_of_preal_not_less_zero"; Goal "0r < - (- real_of_preal m)"; @@ -789,7 +789,7 @@ "0r < real_of_preal m + real_of_preal m1"; by (auto_tac (claset(), simpset() addsimps [real_of_preal_def, - real_less_def,real_add])); + real_less_def,real_add])); by (REPEAT(rtac exI 1)); by (EVERY[rtac conjI 1, rtac conjI 2]); by (REPEAT(Blast_tac 2)); diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/RealInt.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/RealInt.ML Thu Aug 19 18:36:41 1999 +0200 @@ -0,0 +1,145 @@ +(* Title: RealInt.ML + ID: $Id$ + Author: Jacques D. Fleuriot + Copyright: 1999 University of Edinburgh + Description: Embedding the integers in the reals +*) + + +Goalw [congruent_def] + "congruent intrel (%p. split (%i j. realrel ^^ \ +\ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \ +\ preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)"; +by (auto_tac (claset(),simpset() addsimps [pnat_of_nat_add, + prat_of_pnat_add RS sym,preal_of_prat_add RS sym])); +qed "real_of_int_congruent"; + +val real_of_int_ize = RSLIST [equiv_intrel, real_of_int_congruent]; + +Goalw [real_of_int_def] + "real_of_int (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)))})"; +by (res_inst_tac [("f","Abs_real")] arg_cong 1); +by (simp_tac (simpset() addsimps + [realrel_in_real RS Abs_real_inverse, + real_of_int_ize UN_equiv_class]) 1); +qed "real_of_int"; + +Goal "inj(real_of_int)"; +by (rtac injI 1); +by (res_inst_tac [("z","x")] eq_Abs_Integ 1); +by (res_inst_tac [("z","y")] eq_Abs_Integ 1); +by (auto_tac (claset() addSDs [inj_preal_of_prat RS injD, + inj_prat_of_pnat RS injD,inj_pnat_of_nat RS injD], + simpset() addsimps [real_of_int,preal_of_prat_add RS sym, + prat_of_pnat_add RS sym,pnat_of_nat_add])); +qed "inj_real_of_int"; + +Goalw [int_def,real_zero_def] "real_of_int (int 0) = 0r"; +by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1); +qed "real_of_int_zero"; + +Goalw [int_def,real_one_def] "real_of_int (int 1) = 1r"; +by (auto_tac (claset(), + simpset() addsimps [real_of_int, + preal_of_prat_add RS sym,pnat_two_eq, + prat_of_pnat_add RS sym,pnat_one_iff RS sym])); +qed "real_of_int_one"; + +Goal "real_of_int x + real_of_int y = real_of_int (x + y)"; +by (res_inst_tac [("z","x")] eq_Abs_Integ 1); +by (res_inst_tac [("z","y")] eq_Abs_Integ 1); +by (auto_tac (claset(),simpset() addsimps [real_of_int, + preal_of_prat_add RS sym,prat_of_pnat_add RS sym, + zadd,real_add,pnat_of_nat_add] @ pnat_add_ac)); +qed "real_of_int_add"; + +Goal "-real_of_int x = real_of_int (-x)"; +by (res_inst_tac [("z","x")] eq_Abs_Integ 1); +by (auto_tac (claset(),simpset() addsimps [real_of_int, + real_minus,zminus])); +qed "real_of_int_minus"; + +Goalw [zdiff_def,real_diff_def] + "real_of_int x - real_of_int y = real_of_int (x - y)"; +by (simp_tac (simpset() addsimps [real_of_int_add, + real_of_int_minus]) 1); +qed "real_of_int_diff"; + +Goal "real_of_int x * real_of_int y = real_of_int (x * y)"; +by (res_inst_tac [("z","x")] eq_Abs_Integ 1); +by (res_inst_tac [("z","y")] eq_Abs_Integ 1); +by (auto_tac (claset(),simpset() addsimps [real_of_int, + real_mult,zmult,preal_of_prat_mult RS sym,pnat_of_nat_mult, + prat_of_pnat_mult RS sym,preal_of_prat_add RS sym, + prat_of_pnat_add RS sym,pnat_of_nat_add] @ mult_ac @add_ac + @ pnat_add_ac)); +qed "real_of_int_mult"; + +Goal "real_of_int (int (Suc n)) = real_of_int (int n) + 1r"; +by (simp_tac (simpset() addsimps [real_of_int_one RS sym, + real_of_int_add,zadd_int]) 1); +qed "real_of_int_Suc"; + +(* relating two of the embeddings *) +Goal "real_of_int (int n) = real_of_nat n"; +by (induct_tac "n" 1); +by (auto_tac (claset(),simpset() addsimps [real_of_int_zero, + real_of_nat_zero,real_of_int_Suc,real_of_nat_Suc])); +qed "real_of_int_real_of_nat"; + +Goal "~neg z ==> real_of_nat (nat z) = real_of_int z"; +by (asm_simp_tac (simpset() addsimps [not_neg_nat, + real_of_int_real_of_nat RS sym]) 1); +qed "real_of_nat_real_of_int"; + +(* put with other properties of real_of_nat? *) +Goal "neg z ==> real_of_nat (nat z) = 0r"; +by (asm_simp_tac (simpset() addsimps [neg_nat, + real_of_nat_zero]) 1); +qed "real_of_nat_neg_int"; +Addsimps [real_of_nat_neg_int]; + +Goal "(real_of_int x = 0r) = (x = int 0)"; +by (auto_tac (claset() addIs [inj_real_of_int RS injD], + simpset() addsimps [real_of_int_zero])); +qed "real_of_int_zero_cancel"; +Addsimps [real_of_int_zero_cancel]; + +Goal "real_of_int x < real_of_int y ==> x < y"; +by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1); +by (auto_tac (claset(), + simpset() addsimps [zle_iff_zadd, real_of_int_add RS sym, + real_of_int_real_of_nat, + real_of_nat_zero RS sym])); +qed "real_of_int_less_cancel"; + +Goal "x < y ==> (real_of_int x < real_of_int y)"; +by (auto_tac (claset(), + simpset() addsimps [zless_iff_Suc_zadd, real_of_int_add RS sym, + real_of_int_real_of_nat, + real_of_nat_Suc])); +by (simp_tac (simpset() addsimps [real_of_nat_one RS + sym,real_of_nat_zero RS sym,real_of_nat_add]) 1); +qed "real_of_int_less_mono"; + +Goal "(real_of_int x < real_of_int y) = (x < y)"; +by (auto_tac (claset() addIs [real_of_int_less_cancel, + real_of_int_less_mono], + simpset())); +qed "real_of_int_less_iff"; +Addsimps [real_of_int_less_iff]; + +Goal "(real_of_int x <= real_of_int y) = (x <= y)"; +by (auto_tac (claset(), + simpset() addsimps [real_le_def, zle_def])); +qed "real_of_int_le_iff"; +Addsimps [real_of_int_le_iff]; + +Goal "(real_of_int x = real_of_int y) = (x = y)"; +by (auto_tac (claset() addSIs [order_antisym], + simpset() addsimps [real_of_int_le_iff RS iffD1])); +qed "real_of_int_eq_iff"; +Addsimps [real_of_int_eq_iff]; diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/RealInt.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/RealInt.thy Thu Aug 19 18:36:41 1999 +0200 @@ -0,0 +1,17 @@ +(* Title: RealInt.thy + ID: $Id$ + Author: Jacques D. Fleuriot + Copyright: 1999 University of Edinburgh + Description: Embedding the integers in the reals +*) + +RealInt = Real + Int + + +constdefs + real_of_int :: int => real + "real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ^^ + {(preal_of_prat(prat_of_pnat(pnat_of_nat i)), + preal_of_prat(prat_of_pnat(pnat_of_nat j)))})" + + +end diff -r 8aa66ddc0bea -r dff3470c5c62 src/HOL/Real/RealPow.ML --- a/src/HOL/Real/RealPow.ML Thu Aug 19 17:06:05 1999 +0200 +++ b/src/HOL/Real/RealPow.ML Thu Aug 19 18:36:41 1999 +0200 @@ -17,7 +17,7 @@ simpset() addsimps [real_zero_not_eq_one RS not_sym])); qed_spec_mp "realpow_not_zero"; -Goal "!!r. r ^ n = 0r ==> r = 0r"; +Goal "r ^ n = 0r ==> r = 0r"; by (blast_tac (claset() addIs [ccontr] addDs [realpow_not_zero]) 1); qed "realpow_zero_zero"; @@ -128,7 +128,7 @@ qed "realpow_two_rabs"; Addsimps [realpow_two_rabs]; -Goal "!!r. 1r < r ==> 1r < r ^ 2"; +Goal "1r < r ==> 1r < r ^ 2"; by (auto_tac (claset(),simpset() addsimps [realpow_two])); by (cut_facts_tac [real_zero_less_one] 1); by (forw_inst_tac [("R1.0","0r")] real_less_trans 1); @@ -137,7 +137,7 @@ by (auto_tac (claset() addIs [real_less_trans],simpset())); qed "realpow_two_gt_one"; -Goal "!!r. 1r <= r ==> 1r <= r ^ 2"; +Goal "1r <= r ==> 1r <= r ^ 2"; by (etac (real_le_imp_less_or_eq RS disjE) 1); by (etac (realpow_two_gt_one RS real_less_imp_le) 1); by (asm_simp_tac (simpset()) 1); @@ -154,7 +154,7 @@ simpset() addsimps [real_zero_less_one])); qed_spec_mp "realpow_ge_one"; -Goal "!!r. 1r < r ==> 1r < r ^ (Suc n)"; +Goal "1r < r ==> 1r < r ^ (Suc n)"; by (forw_inst_tac [("n","n")] realpow_ge_one 1); by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1); by (dtac sym 2); @@ -164,13 +164,13 @@ simpset())); qed "realpow_Suc_gt_one"; -Goal "!!r. 1r <= r ==> 1r <= r ^ n"; +Goal "1r <= r ==> 1r <= r ^ n"; by (dtac real_le_imp_less_or_eq 1); by (auto_tac (claset() addDs [realpow_ge_one], simpset())); qed "realpow_ge_one2"; -Goal "!!r. 0r < r ==> 0r < r ^ Suc n"; +Goal "0r < r ==> 0r < r ^ Suc n"; by (forw_inst_tac [("n","n")] realpow_ge_zero 1); by (forw_inst_tac [("n1","n")] ((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1); @@ -178,7 +178,7 @@ addIs [real_mult_order],simpset())); qed "realpow_Suc_gt_zero"; -Goal "!!r. 0r <= r ==> 0r <= r ^ Suc n"; +Goal "0r <= r ==> 0r <= r ^ Suc n"; by (etac (real_le_imp_less_or_eq RS disjE) 1); by (etac (realpow_ge_zero) 1); by (asm_simp_tac (simpset()) 1); @@ -194,12 +194,11 @@ Goal "real_of_nat n < (1r + 1r) ^ n"; by (induct_tac "n" 1); -by (rtac (lemmaS RS ssubst) 2); -by (rtac (real_of_nat_add RS subst) 2); -by (auto_tac (claset(),simpset() addsimps [real_of_nat_zero, - real_zero_less_one,real_add_mult_distrib,real_of_nat_one])); -by (blast_tac (claset() addSIs [real_add_less_le_mono, - two_realpow_ge_one]) 1); +by (auto_tac (claset(), + simpset() addsimps [real_of_nat_Suc, real_of_nat_zero, + real_zero_less_one,real_add_mult_distrib, + real_of_nat_one])); +by (blast_tac (claset() addSIs [real_add_less_le_mono, two_realpow_ge_one]) 1); qed "two_realpow_gt"; Addsimps [two_realpow_gt,two_realpow_ge_one]; @@ -249,7 +248,7 @@ realpow_Suc_less]) 1); qed_spec_mp "realpow_Suc_le2"; -Goal "!!r. [| 0r <= r; r < 1r |] ==> r ^ Suc n <= r ^ n"; +Goal "[| 0r <= r; r < 1r |] ==> r ^ Suc n <= r ^ n"; by (etac (real_le_imp_less_or_eq RS disjE) 1); by (rtac realpow_Suc_le2 1); by (Auto_tac); @@ -266,20 +265,19 @@ [less_Suc_eq])); qed_spec_mp "realpow_less_le"; -Goal "!!r. [| 0r <= r; r < 1r; n <= N |] \ -\ ==> r ^ N <= r ^ n"; +Goal "[| 0r <= r; r < 1r; n <= N |] ==> r ^ N <= r ^ n"; by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); by (auto_tac (claset() addIs [realpow_less_le], simpset())); qed "realpow_le_le"; -Goal "!!r. [| 0r < r; r < 1r |] ==> r ^ Suc n <= r"; +Goal "[| 0r < r; r < 1r |] ==> r ^ Suc n <= r"; by (dres_inst_tac [("n","1"),("N","Suc n")] (real_less_imp_le RS realpow_le_le) 1); by (Auto_tac); qed "realpow_Suc_le_self"; -Goal "!!r. [| 0r < r; r < 1r |] ==> r ^ Suc n < 1r"; +Goal "[| 0r < r; r < 1r |] ==> r ^ Suc n < 1r"; by (blast_tac (claset() addIs [realpow_Suc_le_self, real_le_less_trans]) 1); qed "realpow_Suc_less_one"; @@ -327,35 +325,35 @@ simpset() addsimps [less_Suc_eq])); qed_spec_mp "realpow_gt_ge2"; -Goal "!!r. [| 1r < r; n <= N |] ==> r ^ n <= r ^ N"; +Goal "[| 1r < r; n <= N |] ==> r ^ n <= r ^ N"; by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); by (auto_tac (claset() addIs [realpow_gt_ge],simpset())); qed "realpow_ge_ge"; -Goal "!!r. [| 1r <= r; n <= N |] ==> r ^ n <= r ^ N"; +Goal "[| 1r <= r; n <= N |] ==> r ^ n <= r ^ N"; by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); by (auto_tac (claset() addIs [realpow_gt_ge2],simpset())); qed "realpow_ge_ge2"; -Goal "!!r. 1r < r ==> r <= r ^ Suc n"; +Goal "1r < r ==> r <= r ^ Suc n"; by (dres_inst_tac [("n","1"),("N","Suc n")] realpow_ge_ge 1); by (Auto_tac); qed_spec_mp "realpow_Suc_ge_self"; -Goal "!!r. 1r <= r ==> r <= r ^ Suc n"; +Goal "1r <= r ==> r <= r ^ Suc n"; by (dres_inst_tac [("n","1"),("N","Suc n")] realpow_ge_ge2 1); by (Auto_tac); qed_spec_mp "realpow_Suc_ge_self2"; -Goal "!!r. [| 1r < r; 0 < n |] ==> r <= r ^ n"; +Goal "[| 1r < r; 0 < n |] ==> r <= r ^ n"; by (dtac (less_not_refl2 RS not0_implies_Suc) 1); by (auto_tac (claset() addSIs [realpow_Suc_ge_self],simpset())); qed "realpow_ge_self"; -Goal "!!r. [| 1r <= r; 0 < n |] ==> r <= r ^ n"; +Goal "[| 1r <= r; 0 < n |] ==> r <= r ^ n"; by (dtac (less_not_refl2 RS not0_implies_Suc) 1); by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset())); qed "realpow_ge_self2"; @@ -367,7 +365,7 @@ qed_spec_mp "realpow_minus_mult"; Addsimps [realpow_minus_mult]; -Goal "!!r. r ~= 0r ==> r * rinv(r) ^ 2 = rinv r"; +Goal "r ~= 0r ==> r * rinv(r) ^ 2 = rinv r"; by (asm_simp_tac (simpset() addsimps [realpow_two, real_mult_assoc RS sym]) 1); qed "realpow_two_mult_rinv";