--- 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
--- 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";
--- 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
--- 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";
--- 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 <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","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 <r2; 0r < y|] \
-\ ==> 0r < r2 * y";
+Goal "[| 0r < r1; r1 <r2; 0r < y|] ==> 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 <r2; 0r <= x; x < y|] \
-\ ==> r1 * x < r2 * y";
+Goal "[| 0r < r1; r1 <r2; 0r <= x; x < y|] ==> 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 <r2; 0r <= x; x < y|] \
-\ ==> r1 * x < r2 * y";
+Goal "[| 0r <= r1; r1 <r2; 0r <= x; x < y|] ==> 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()));
--- /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*)
+
--- /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
--- 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));
--- /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];
--- /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
--- 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";