First round of changes, towards installation of simprocs
* replacing 0r by (0::real0
* better rewriting, especially pulling out signs in (-x)*y = - (x*y), etc.
--- a/src/HOL/Real/HahnBanach/Aux.thy Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Wed Jun 07 12:14:18 2000 +0200
@@ -109,13 +109,13 @@
thus ?thesis by (simp only: real_mult_commute)
qed
-lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x"
-proof -
- assume "#0 < x"
- hence "0r < x" by simp
- hence "0r < rinv x" by (rule real_rinv_gt_zero)
- thus ?thesis by simp
-qed
+lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x";
+proof -;
+ assume "#0 < x";
+ have "0 < x"; by simp;
+ hence "0 < rinv x"; by (rule real_rinv_gt_zero);
+ thus ?thesis; by simp;
+qed;
lemma real_mult_inv_right1: "x ~= #0 ==> x*rinv(x) = #1"
by simp
@@ -127,7 +127,7 @@
"[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"
proof -
assume "#0 <= x" "#0 <= y"
- have "[|0r <= x; 0r <= y|] ==> 0r <= x * y"
+ have "[|0 <= x; 0 <= y|] ==> 0 <= x * y"
by (rule real_le_mult_order)
thus ?thesis by (simp!)
qed
@@ -139,7 +139,7 @@
also have "a * ... = a * - x + a * - y"
by (simp only: real_add_mult_distrib2)
also have "... = - a * x - a * y"
- by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1)
+ by simp;
finally show ?thesis .
qed
@@ -149,7 +149,7 @@
also have "a * ... = a * x + a * - y"
by (simp only: real_add_mult_distrib2)
also have "... = a * x - a * y"
- by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1)
+ by simp;
finally show ?thesis .
qed
--- a/src/HOL/Real/Hyperreal/HyperDef.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Wed Jun 07 12:14:18 2000 +0200
@@ -587,29 +587,29 @@
Goal "-(x * y) = -x * (y::hypreal)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
- hypreal_mult,real_minus_mult_eq1]
- @ real_mult_ac @ real_add_ac));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_minus, hypreal_mult]
+ @ real_mult_ac @ real_add_ac));
qed "hypreal_minus_mult_eq1";
Goal "-(x * y) = (x::hypreal) * -y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
- hypreal_mult,real_minus_mult_eq2]
- @ real_mult_ac @ real_add_ac));
+ hypreal_mult]
+ @ real_mult_ac @ real_add_ac));
qed "hypreal_minus_mult_eq2";
Goal "-x*-y = x*(y::hypreal)";
by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
- hypreal_minus_mult_eq1 RS sym]) 1);
+ hypreal_minus_mult_eq1 RS sym]) 1);
qed "hypreal_minus_mult_cancel";
Addsimps [hypreal_minus_mult_cancel];
Goal "-x*y = (x::hypreal)*-y";
by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
- hypreal_minus_mult_eq1 RS sym]) 1);
+ hypreal_minus_mult_eq1 RS sym]) 1);
qed "hypreal_minus_mult_commute";
--- a/src/HOL/Real/PNat.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/PNat.ML Wed Jun 07 12:14:18 2000 +0200
@@ -289,7 +289,7 @@
qed "Rep_pnat_le_one";
Goalw [pnat_less_def]
- "!! (z1::nat). z1 < z2 ==> ? z3. z1 + Rep_pnat z3 = z2";
+ "!! (z1::nat). z1 < z2 ==> EX z3. z1 + Rep_pnat z3 = z2";
by (dtac less_imp_add_positive 1);
by (force_tac (claset() addSIs [Abs_pnat_inverse],
simpset() addsimps [Collect_pnat_gt_0]) 1);
@@ -473,7 +473,7 @@
(* ordering on positive naturals in terms of existence of sum *)
(* could provide alternative definition -- Gleason *)
Goalw [pnat_less_def,pnat_add_def]
- "(z1::pnat) < z2 = (? z3. z1 + z3 = z2)";
+ "(z1::pnat) < z2 = (EX z3. z1 + z3 = z2)";
by (rtac iffI 1);
by (res_inst_tac [("t","z2")] (Rep_pnat_inverse RS subst) 1);
by (dtac lemma_less_ex_sum_Rep_pnat 1);
@@ -484,8 +484,8 @@
Rep_pnat_gt_zero] delsimps [add_0_right]));
qed "pnat_less_iff";
-Goal "(? (x::pnat). z1 + x = z2) | z1 = z2 \
-\ |(? x. z2 + x = z1)";
+Goal "(EX (x::pnat). z1 + x = z2) | z1 = z2 \
+\ |(EX x. z2 + x = z1)";
by (cut_facts_tac [pnat_less_linear] 1);
by (asm_full_simp_tac (simpset() addsimps [pnat_less_iff]) 1);
qed "pnat_linear_Ex_eq";
--- a/src/HOL/Real/PRat.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/PRat.ML Wed Jun 07 12:14:18 2000 +0200
@@ -270,11 +270,11 @@
by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1);
qed "prat_mult_qinv_right";
-Goal "? y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
+Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1);
qed "prat_qinv_ex";
-Goal "?! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
+Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset()));
by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1);
@@ -282,7 +282,7 @@
prat_mult_1,prat_mult_1_right]) 1);
qed "prat_qinv_ex1";
-Goal "?! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1)";
+Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1)";
by (auto_tac (claset() addIs [prat_mult_qinv],simpset()));
by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1);
@@ -296,7 +296,7 @@
by (Blast_tac 1);
qed "prat_mult_inv_qinv";
-Goal "? y. x = qinv y";
+Goal "EX y. x = qinv y";
by (cut_inst_tac [("x","x")] prat_qinv_ex 1);
by (etac exE 1 THEN dtac prat_mult_inv_qinv 1);
by (Fast_tac 1);
@@ -386,7 +386,7 @@
bind_thm ("prat_less_asym", prat_less_not_sym RS swap);
(* half of positive fraction exists- Gleason p. 120- Proposition 9-2.6(i)*)
-Goal "!(q::prat). ? x. x + x = q";
+Goal "!(q::prat). EX x. x + x = q";
by (rtac allI 1);
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
by (res_inst_tac [("x","Abs_prat (ratrel ^^ {(x, y+y)})")] exI 1);
@@ -396,7 +396,7 @@
pnat_add_mult_distrib2]));
qed "lemma_prat_dense";
-Goal "? (x::prat). x + x = q";
+Goal "EX (x::prat). x + x = q";
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
by (res_inst_tac [("x","Abs_prat (ratrel ^^ {(x, y+y)})")] exI 1);
by (auto_tac (claset(),simpset() addsimps
@@ -407,7 +407,7 @@
(* there exists a number between any two positive fractions *)
(* Gleason p. 120- Proposition 9-2.6(iv) *)
Goalw [prat_less_def]
- "!! (q1::prat). q1 < q2 ==> ? x. q1 < x & x < q2";
+ "!! (q1::prat). q1 < q2 ==> EX x. q1 < x & x < q2";
by (auto_tac (claset() addIs [lemma_prat_dense],simpset()));
by (res_inst_tac [("x","T")] (lemma_prat_dense RS allE) 1);
by (etac exE 1);
@@ -442,7 +442,7 @@
qed "prat_mult_left_less2_mono1";
(* there is no smallest positive fraction *)
-Goalw [prat_less_def] "? (x::prat). x < y";
+Goalw [prat_less_def] "EX (x::prat). x < y";
by (cut_facts_tac [lemma_prat_dense] 1);
by (Fast_tac 1);
qed "qless_Ex";
@@ -765,7 +765,7 @@
(*** of preal type as defined using Dedekind Sections in PReal ***)
(*** Show that exists positive real `one' ***)
-Goal "? q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
+Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1);
qed "lemma_prat_less_1_memEx";
@@ -781,7 +781,7 @@
qed "empty_set_psubset_lemma_prat_less_1_set";
(*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***)
-Goal "? q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
+Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] exI 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "lemma_prat_less_1_not_memEx";
@@ -803,7 +803,7 @@
Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
\ A < UNIV & \
\ (!y: A. ((!z. z < y --> z: A) & \
-\ (? u: A. y < u)))}";
+\ (EX u: A. y < u)))}";
by (auto_tac (claset() addDs [prat_less_trans],
simpset() addsimps [empty_set_psubset_lemma_prat_less_1_set,
lemma_prat_less_1_set_psubset_rat_set]));
--- a/src/HOL/Real/PReal.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/PReal.ML Wed Jun 07 12:14:18 2000 +0200
@@ -44,7 +44,7 @@
by (rtac (Rep_preal RS preal_psubset_empty) 1);
qed "Rep_preal_psubset_empty";
-Goal "? x. x: Rep_preal X";
+Goal "EX x. x: Rep_preal X";
by (cut_inst_tac [("x","X")] Rep_preal_psubset_empty 1);
by (auto_tac (claset() addIs [(equals0I RS sym)],
simpset() addsimps [psubset_def]));
@@ -52,22 +52,22 @@
Goalw [preal_def]
"[| {} < A; A < UNIV; \
-\ (!y: A. ((!z. z < y --> z: A) & \
-\ (? u: A. y < u))) |] ==> A : preal";
+\ (ALL y: A. ((ALL z. z < y --> z: A) & \
+\ (EX u: A. y < u))) |] ==> A : preal";
by (Fast_tac 1);
qed "prealI1";
Goalw [preal_def]
"[| {} < A; A < UNIV; \
-\ !y: A. (!z. z < y --> z: A); \
-\ !y: A. (? u: A. y < u) |] ==> A : preal";
+\ ALL y: A. (ALL z. z < y --> z: A); \
+\ ALL y: A. (EX u: A. y < u) |] ==> A : preal";
by (Best_tac 1);
qed "prealI2";
Goalw [preal_def]
"A : preal ==> {} < A & A < UNIV & \
-\ (!y: A. ((!z. z < y --> z: A) & \
-\ (? u: A. y < u)))";
+\ (ALL y: A. ((ALL z. z < y --> z: A) & \
+\ (EX u: A. y < u)))";
by (Fast_tac 1);
qed "prealE_lemma";
@@ -85,11 +85,11 @@
by (Fast_tac 1);
qed "prealE_lemma2";
-Goalw [preal_def] "A : preal ==> !y: A. (!z. z < y --> z: A)";
+Goalw [preal_def] "A : preal ==> ALL y: A. (ALL z. z < y --> z: A)";
by (Fast_tac 1);
qed "prealE_lemma3";
-Goal "[| A : preal; y: A |] ==> (!z. z < y --> z: A)";
+Goal "[| A : preal; y: A |] ==> (ALL z. z < y --> z: A)";
by (fast_tac (claset() addSDs [prealE_lemma3]) 1);
qed "prealE_lemma3a";
@@ -97,15 +97,15 @@
by (fast_tac (claset() addSDs [prealE_lemma3a]) 1);
qed "prealE_lemma3b";
-Goalw [preal_def] "A : preal ==> !y: A. (? u: A. y < u)";
+Goalw [preal_def] "A : preal ==> ALL y: A. (EX u: A. y < u)";
by (Fast_tac 1);
qed "prealE_lemma4";
-Goal "[| A : preal; y: A |] ==> ? u: A. y < u";
+Goal "[| A : preal; y: A |] ==> EX u: A. y < u";
by (fast_tac (claset() addSDs [prealE_lemma4]) 1);
qed "prealE_lemma4a";
-Goal "? x. x~: Rep_preal X";
+Goal "EX x. x~: Rep_preal X";
by (cut_inst_tac [("x","X")] Rep_preal 1);
by (dtac prealE_lemma2 1);
by (rtac ccontr 1);
@@ -148,7 +148,7 @@
(* A positive fraction not in a positive real is an upper bound *)
(* Gleason p. 122 - Remark (1) *)
-Goal "x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
+Goal "x ~: Rep_preal(R) ==> ALL y: Rep_preal(R). y < x";
by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset()));
qed "not_in_preal_ub";
@@ -207,13 +207,13 @@
(** lemmas for proving positive reals addition set in preal **)
(** Part 1 of Dedekind sections def **)
-Goal "{} < {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y}";
+Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
qed "preal_add_set_not_empty";
(** Part 2 of Dedekind sections def **)
-Goal "? q. q ~: {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y}";
+Goal "EX q. q ~: {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
by (REPEAT(etac exE 1));
@@ -224,7 +224,7 @@
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "preal_not_mem_add_set_Ex";
-Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y} < UNIV";
+Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y} < UNIV";
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_add_set_Ex 1);
by (etac exE 1);
@@ -233,8 +233,8 @@
qed "preal_add_set_not_prat_set";
(** Part 3 of Dedekind sections def **)
-Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
-\ !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x + y}";
+Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. \
+\ ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x + y}";
by Auto_tac;
by (ftac prat_mult_qinv_less_1 1);
by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1)")]
@@ -250,14 +250,14 @@
RS sym,prat_add_assoc RS sym,prat_mult_assoc]));
qed "preal_add_set_lemma3";
-Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
-\ ? u: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. y < u";
+Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. \
+\ EX u: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. y < u";
by Auto_tac;
by (dtac (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset() addIs [prat_add_less2_mono1],simpset()));
qed "preal_add_set_lemma4";
-Goal "{w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y} : preal";
+Goal "{w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y} : preal";
by (rtac prealI2 1);
by (rtac preal_add_set_not_empty 1);
by (rtac preal_add_set_not_prat_set 1);
@@ -297,13 +297,13 @@
(** lemmas for proving positive reals multiplication set in preal **)
(** Part 1 of Dedekind sections def **)
-Goal "{} < {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y}";
+Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
qed "preal_mult_set_not_empty";
(** Part 2 of Dedekind sections def **)
-Goal "? q. q ~: {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y}";
+Goal "EX q. q ~: {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
by (REPEAT(etac exE 1));
@@ -314,7 +314,7 @@
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "preal_not_mem_mult_set_Ex";
-Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y} < UNIV";
+Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y} < UNIV";
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_mult_set_Ex 1);
by (etac exE 1);
@@ -323,8 +323,8 @@
qed "preal_mult_set_not_prat_set";
(** Part 3 of Dedekind sections def **)
-Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. \
-\ !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x * y}";
+Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. \
+\ ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x * y}";
by Auto_tac;
by (forw_inst_tac [("x","qinv(ya)"),("q1.0","z")]
prat_mult_left_less2_mono1 1);
@@ -335,14 +335,14 @@
by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
qed "preal_mult_set_lemma3";
-Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. \
-\ ? u: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. y < u";
+Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. \
+\ EX u: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. y < u";
by Auto_tac;
by (dtac (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset() addIs [prat_mult_less2_mono1],simpset()));
qed "preal_mult_set_lemma4";
-Goal "{w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y} : preal";
+Goal "{w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y} : preal";
by (rtac prealI2 1);
by (rtac preal_mult_set_not_empty 1);
by (rtac preal_mult_set_not_prat_set 1);
@@ -410,39 +410,39 @@
(** lemmas **)
Goalw [preal_add_def]
"z: Rep_preal(R+S) ==> \
-\ ? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y";
+\ EX x: Rep_preal(R). EX y: Rep_preal(S). z = x + y";
by (dtac (preal_mem_add_set RS Abs_preal_inverse RS subst) 1);
by (Fast_tac 1);
qed "mem_Rep_preal_addD";
Goalw [preal_add_def]
- "? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y \
+ "EX x: Rep_preal(R). EX y: Rep_preal(S). z = x + y \
\ ==> z: Rep_preal(R+S)";
by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
by (Fast_tac 1);
qed "mem_Rep_preal_addI";
-Goal " z: Rep_preal(R+S) = (? x: Rep_preal(R). \
-\ ? y: Rep_preal(S). z = x + y)";
+Goal " z: Rep_preal(R+S) = (EX x: Rep_preal(R). \
+\ EX y: Rep_preal(S). z = x + y)";
by (fast_tac (claset() addSIs [mem_Rep_preal_addD,mem_Rep_preal_addI]) 1);
qed "mem_Rep_preal_add_iff";
Goalw [preal_mult_def]
"z: Rep_preal(R*S) ==> \
-\ ? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y";
+\ EX x: Rep_preal(R). EX y: Rep_preal(S). z = x * y";
by (dtac (preal_mem_mult_set RS Abs_preal_inverse RS subst) 1);
by (Fast_tac 1);
qed "mem_Rep_preal_multD";
Goalw [preal_mult_def]
- "? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y \
+ "EX x: Rep_preal(R). EX y: Rep_preal(S). z = x * y \
\ ==> z: Rep_preal(R*S)";
by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
by (Fast_tac 1);
qed "mem_Rep_preal_multI";
-Goal " z: Rep_preal(R*S) = (? x: Rep_preal(R). \
-\ ? y: Rep_preal(S). z = x * y)";
+Goal " z: Rep_preal(R*S) = (EX x: Rep_preal(R). \
+\ EX y: Rep_preal(S). z = x * y)";
by (fast_tac (claset() addSIs [mem_Rep_preal_multD,mem_Rep_preal_multI]) 1);
qed "mem_Rep_preal_mult_iff";
@@ -507,13 +507,13 @@
(*** Prove existence of inverse ***)
(*** Inverse is a positive real ***)
-Goal "? y. qinv(y) ~: Rep_preal X";
+Goal "EX y. qinv(y) ~: Rep_preal X";
by (cut_inst_tac [("X","X")] not_mem_Rep_preal_Ex 1);
by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
by Auto_tac;
qed "qinv_not_mem_Rep_preal_Ex";
-Goal "? q. q: {x. ? y. x < y & qinv y ~: Rep_preal A}";
+Goal "EX q. q: {x. EX y. x < y & qinv y ~: Rep_preal A}";
by (cut_inst_tac [("X","A")] qinv_not_mem_Rep_preal_Ex 1);
by Auto_tac;
by (cut_inst_tac [("y","y")] qless_Ex 1);
@@ -521,19 +521,19 @@
qed "lemma_preal_mem_inv_set_ex";
(** Part 1 of Dedekind sections def **)
-Goal "{} < {x. ? y. x < y & qinv y ~: Rep_preal A}";
+Goal "{} < {x. EX y. x < y & qinv y ~: Rep_preal A}";
by (cut_facts_tac [lemma_preal_mem_inv_set_ex] 1);
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
qed "preal_inv_set_not_empty";
(** Part 2 of Dedekind sections def **)
-Goal "? y. qinv(y) : Rep_preal X";
+Goal "EX y. qinv(y) : Rep_preal X";
by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
by Auto_tac;
qed "qinv_mem_Rep_preal_Ex";
-Goal "? x. x ~: {x. ? y. x < y & qinv y ~: Rep_preal A}";
+Goal "EX x. x ~: {x. EX y. x < y & qinv y ~: Rep_preal A}";
by (rtac ccontr 1);
by (cut_inst_tac [("X","A")] qinv_mem_Rep_preal_Ex 1);
by Auto_tac;
@@ -544,7 +544,7 @@
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "preal_not_mem_inv_set_Ex";
-Goal "{x. ? y. x < y & qinv y ~: Rep_preal A} < UNIV";
+Goal "{x. EX y. x < y & qinv y ~: Rep_preal A} < UNIV";
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (cut_inst_tac [("A","A")] preal_not_mem_inv_set_Ex 1);
by (etac exE 1);
@@ -553,19 +553,19 @@
qed "preal_inv_set_not_prat_set";
(** Part 3 of Dedekind sections def **)
-Goal "! y: {x. ? y. x < y & qinv y ~: Rep_preal A}. \
- \ !z. z < y --> z : {x. ? y. x < y & qinv y ~: Rep_preal A}";
+Goal "ALL y: {x. EX y. x < y & qinv y ~: Rep_preal A}. \
+ \ ALL z. z < y --> z : {x. EX y. x < y & qinv y ~: Rep_preal A}";
by Auto_tac;
by (res_inst_tac [("x","ya")] exI 1);
by (auto_tac (claset() addIs [prat_less_trans],simpset()));
qed "preal_inv_set_lemma3";
-Goal "! y: {x. ? y. x < y & qinv y ~: Rep_preal A}. \
-\ Bex {x. ? y. x < y & qinv y ~: Rep_preal A} (op < y)";
+Goal "ALL y: {x. EX y. x < y & qinv y ~: Rep_preal A}. \
+\ Bex {x. EX y. x < y & qinv y ~: Rep_preal A} (op < y)";
by (blast_tac (claset() addDs [prat_dense]) 1);
qed "preal_inv_set_lemma4";
-Goal "{x. ? y. x < y & qinv(y) ~: Rep_preal(A)} : preal";
+Goal "{x. EX y. x < y & qinv(y) ~: Rep_preal(A)} : preal";
by (rtac prealI2 1);
by (rtac preal_inv_set_not_empty 1);
by (rtac preal_inv_set_not_prat_set 1);
@@ -585,8 +585,8 @@
qed "preal_mem_mult_invD";
(*** Gleason's Lemma 9-3.4 p 122 ***)
-Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
-\ ? xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
+Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
+\ EX xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
by (cut_facts_tac [mem_Rep_preal_Ex] 1);
by (res_inst_tac [("n","p")] pnat_induct 1);
by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
@@ -603,7 +603,7 @@
simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
qed "lemma1b_gleason9_34";
-Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
+Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
by (cut_inst_tac [("X","A")] not_mem_Rep_preal_Ex 1);
by (etac exE 1);
by (dtac not_in_preal_ub 1);
@@ -618,7 +618,7 @@
simpset() addsimps [prat_of_pnat_def]));
qed "lemma_gleason9_34a";
-Goal "? r: Rep_preal(R). r + x ~: Rep_preal(R)";
+Goal "EX r: Rep_preal(R). r + x ~: Rep_preal(R)";
by (rtac ccontr 1);
by (blast_tac (claset() addIs [lemma_gleason9_34a]) 1);
qed "lemma_gleason9_34";
@@ -639,7 +639,7 @@
(******)
(*** FIXME: long! ***)
-Goal "prat_of_pnat 1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
+Goal "prat_of_pnat 1p < x ==> EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
by (Fast_tac 1);
@@ -663,7 +663,7 @@
qed "lemma_gleason9_36";
Goal "prat_of_pnat (Abs_pnat 1) < x ==> \
-\ ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
+\ EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
by (rtac lemma_gleason9_36 1);
by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
qed "lemma_gleason9_36a";
@@ -813,7 +813,7 @@
(**** Define the D required and show that it is a positive real ****)
(* useful lemmas - proved elsewhere? *)
-Goalw [psubset_def] "A < B ==> ? x. x ~: A & x : B";
+Goalw [psubset_def] "A < B ==> EX x. x ~: A & x : B";
by (etac conjE 1);
by (etac swap 1);
by (etac equalityI 1);
@@ -843,7 +843,7 @@
(** Part 1 of Dedekind sections def **)
Goalw [preal_less_def]
"A < B ==> \
-\ ? q. q : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
+\ EX q. q : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by (EVERY1[dtac lemma_psubset_mem, etac exE, etac conjE]);
by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
@@ -851,13 +851,13 @@
Goal
"A < B ==> \
-\ {} < {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
+\ {} < {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by (dtac lemma_ex_mem_less_left_add1 1);
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
qed "preal_less_set_not_empty";
(** Part 2 of Dedekind sections def **)
-Goal "? q. q ~: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
+Goal "EX q. q ~: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by (cut_inst_tac [("X","B")] not_mem_Rep_preal_Ex 1);
by (etac exE 1);
by (res_inst_tac [("x","x")] exI 1);
@@ -866,7 +866,7 @@
by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset()));
qed "lemma_ex_not_mem_less_left_add1";
-Goal "{d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
+Goal "{d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (cut_inst_tac [("A","A"),("B","B")] lemma_ex_not_mem_less_left_add1 1);
by (etac exE 1);
@@ -875,16 +875,16 @@
qed "preal_less_set_not_prat_set";
(** Part 3 of Dedekind sections def **)
-Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
- \ !z. z < y --> z : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
+Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
+ \ ALL z. z < y --> z : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by Auto_tac;
by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
by (dtac (Rep_preal RS prealE_lemma3b) 1);
by Auto_tac;
qed "preal_less_set_lemma3";
-Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
-\ Bex {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
+Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
+\ Bex {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
by Auto_tac;
by (dtac (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_def,prat_add_assoc]));
@@ -892,7 +892,7 @@
Goal
"!! (A::preal). A < B ==> \
-\ {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}: preal";
+\ {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}: preal";
by (rtac prealI2 1);
by (rtac preal_less_set_not_empty 1);
by (rtac preal_less_set_not_prat_set 2);
@@ -904,7 +904,7 @@
(** proving that A + D <= B **)
Goalw [preal_le_def]
"!! (A::preal). A < B ==> \
-\ A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) <= B";
+\ A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) <= B";
by (rtac subsetI 1);
by (dtac mem_Rep_preal_addD 1);
by (auto_tac (claset(),simpset() addsimps [
@@ -918,14 +918,14 @@
(** proving that B <= A + D --- trickier **)
(** lemma **)
-Goal "x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
+Goal "x : Rep_preal(B) ==> EX e. x + e : Rep_preal(B)";
by (dtac (Rep_preal RS prealE_lemma4a) 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
qed "lemma_sum_mem_Rep_preal_ex";
Goalw [preal_le_def]
"!! (A::preal). A < B ==> \
-\ B <= A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)})";
+\ B <= A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)})";
by (rtac subsetI 1);
by (res_inst_tac [("Q","x: Rep_preal(A)")] (excluded_middle RS disjE) 1);
by (rtac mem_Rep_preal_addI 1);
@@ -945,12 +945,12 @@
(*** required proof ***)
Goal "!! (A::preal). A < B ==> \
-\ A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) = B";
+\ A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) = B";
by (blast_tac (claset() addIs [preal_le_anti_sym,
preal_less_add_left_subsetI,preal_less_add_left_subsetI2]) 1);
qed "preal_less_add_left";
-Goal "!! (A::preal). A < B ==> ? D. A + D = B";
+Goal "!! (A::preal). A < B ==> EX D. A + D = B";
by (fast_tac (claset() addDs [preal_less_add_left]) 1);
qed "preal_less_add_left_Ex";
@@ -1070,23 +1070,23 @@
(*** Completeness of preal ***)
(*** prove that supremum is a cut ***)
-Goal "? (X::preal). X: P ==> \
-\ ? q. q: {w. ? X. X : P & w : Rep_preal X}";
+Goal "EX (X::preal). X: P ==> \
+\ EX q. q: {w. EX X. X : P & w : Rep_preal X}";
by Safe_tac;
by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
by Auto_tac;
qed "preal_sup_mem_Ex";
(** Part 1 of Dedekind def **)
-Goal "? (X::preal). X: P ==> \
-\ {} < {w. ? X : P. w : Rep_preal X}";
+Goal "EX (X::preal). X: P ==> \
+\ {} < {w. EX X : P. w : Rep_preal X}";
by (dtac preal_sup_mem_Ex 1);
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
qed "preal_sup_set_not_empty";
(** Part 2 of Dedekind sections def **)
-Goalw [preal_less_def] "? Y. (! X: P. X < Y) \
-\ ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}"; (**)
+Goalw [preal_less_def] "EX Y. (ALL X: P. X < Y) \
+\ ==> EX q. q ~: {w. EX X. X: P & w: Rep_preal(X)}"; (**)
by (auto_tac (claset(),simpset() addsimps [psubset_def]));
by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
by (etac exE 1);
@@ -1094,8 +1094,8 @@
by (auto_tac (claset() addSDs [bspec],simpset()));
qed "preal_sup_not_mem_Ex";
-Goalw [preal_le_def] "? Y. (! X: P. X <= Y) \
-\ ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}";
+Goalw [preal_le_def] "EX Y. (ALL X: P. X <= Y) \
+\ ==> EX q. q ~: {w. EX X. X: P & w: Rep_preal(X)}";
by (Step_tac 1);
by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
by (etac exE 1);
@@ -1103,16 +1103,16 @@
by (auto_tac (claset() addSDs [bspec],simpset()));
qed "preal_sup_not_mem_Ex1";
-Goal "? Y. (! X: P. X < Y) \
-\ ==> {w. ? X: P. w: Rep_preal(X)} < UNIV"; (**)
+Goal "EX Y. (ALL X: P. X < Y) \
+\ ==> {w. EX X: P. w: Rep_preal(X)} < UNIV"; (**)
by (dtac preal_sup_not_mem_Ex 1);
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (eres_inst_tac [("c","q")] equalityCE 1);
by Auto_tac;
qed "preal_sup_set_not_prat_set";
-Goal "? Y. (! X: P. X <= Y) \
-\ ==> {w. ? X: P. w: Rep_preal(X)} < UNIV";
+Goal "EX Y. (ALL X: P. X <= Y) \
+\ ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";
by (dtac preal_sup_not_mem_Ex1 1);
by (auto_tac (claset() addSIs [psubsetI],simpset()));
by (eres_inst_tac [("c","q")] equalityCE 1);
@@ -1120,32 +1120,32 @@
qed "preal_sup_set_not_prat_set1";
(** Part 3 of Dedekind sections def **)
-Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
-\ ==> ! y: {w. ? X: P. w: Rep_preal X}. \
-\ !z. z < y --> z: {w. ? X: P. w: Rep_preal X}"; (**)
+Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \
+\ ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
+\ ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}"; (**)
by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
qed "preal_sup_set_lemma3";
-Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
-\ ==> ! y: {w. ? X: P. w: Rep_preal X}. \
-\ !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";
+Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
+\ ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
+\ ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";
by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
qed "preal_sup_set_lemma3_1";
-Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
-\ ==> !y: {w. ? X: P. w: Rep_preal X}. \
-\ Bex {w. ? X: P. w: Rep_preal X} (op < y)"; (**)
+Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \
+\ ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
+\ Bex {w. EX X: P. w: Rep_preal X} (op < y)"; (**)
by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
qed "preal_sup_set_lemma4";
-Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
-\ ==> !y: {w. ? X: P. w: Rep_preal X}. \
-\ Bex {w. ? X: P. w: Rep_preal X} (op < y)";
+Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
+\ ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
+\ Bex {w. EX X: P. w: Rep_preal X} (op < y)";
by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
qed "preal_sup_set_lemma4_1";
-Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
-\ ==> {w. ? X: P. w: Rep_preal(X)}: preal"; (**)
+Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \
+\ ==> {w. EX X: P. w: Rep_preal(X)}: preal"; (**)
by (rtac prealI2 1);
by (rtac preal_sup_set_not_empty 1);
by (rtac preal_sup_set_not_prat_set 2);
@@ -1154,8 +1154,8 @@
by Auto_tac;
qed "preal_sup";
-Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
-\ ==> {w. ? X: P. w: Rep_preal(X)}: preal";
+Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
+\ ==> {w. EX X: P. w: Rep_preal(X)}: preal";
by (rtac prealI2 1);
by (rtac preal_sup_set_not_empty 1);
by (rtac preal_sup_set_not_prat_set1 2);
@@ -1164,27 +1164,27 @@
by Auto_tac;
qed "preal_sup1";
-Goalw [psup_def] "? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P"; (**)
+Goalw [psup_def] "EX Y. (ALL X:P. X < Y) ==> ALL x: P. x <= psup P"; (**)
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (rtac (preal_sup RS Abs_preal_inverse RS ssubst) 1);
by Auto_tac;
qed "preal_psup_leI";
-Goalw [psup_def] "? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
+Goalw [psup_def] "EX Y. (ALL X:P. X <= Y) ==> ALL x: P. x <= psup P";
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (rtac (preal_sup1 RS Abs_preal_inverse RS ssubst) 1);
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
qed "preal_psup_leI2";
-Goal "[| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P"; (**)
+Goal "[| EX Y. (ALL X:P. X < Y); x : P |] ==> x <= psup P"; (**)
by (blast_tac (claset() addSDs [preal_psup_leI]) 1);
qed "preal_psup_leI2b";
-Goal "[| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
+Goal "[| EX Y. (ALL X:P. X <= Y); x : P |] ==> x <= psup P";
by (blast_tac (claset() addSDs [preal_psup_leI2]) 1);
qed "preal_psup_leI2a";
-Goalw [psup_def] "[| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y"; (**)
+Goalw [psup_def] "[| EX X. X : P; ALL X:P. X < Y |] ==> psup P <= Y"; (**)
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (dtac (([exI,exI] MRS preal_sup) RS Abs_preal_inverse RS subst) 1);
by (rotate_tac 1 2);
@@ -1192,7 +1192,7 @@
by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def]));
qed "psup_le_ub";
-Goalw [psup_def] "[| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
+Goalw [psup_def] "[| EX X. X : P; ALL X:P. X <= Y |] ==> psup P <= Y";
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
by (dtac (([exI,exI] MRS preal_sup1) RS Abs_preal_inverse RS subst) 1);
by (rotate_tac 1 2);
@@ -1202,8 +1202,8 @@
qed "psup_le_ub1";
(** supremum property **)
-Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
-\ ==> (!Y. (? X: P. Y < X) = (Y < psup P))";
+Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \
+\ ==> (ALL Y. (EX X: P. Y < X) = (Y < psup P))";
by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
by (Fast_tac 1);
by (auto_tac (claset() addSIs [psubsetI],simpset() addsimps [psup_def,preal_less_def]));
--- a/src/HOL/Real/RComplete.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RComplete.ML Wed Jun 07 12:14:18 2000 +0200
@@ -14,16 +14,16 @@
previously in Real.ML.
---------------------------------------------------------*)
(*a few lemmas*)
-Goal "! x:P. #0 < x ==> \
-\ ((? x:P. y < x) = (? X. real_of_preal X : P & \
+Goal "ALL x:P. #0 < x ==> \
+\ ((EX x:P. y < x) = (EX X. real_of_preal X : P & \
\ y < real_of_preal X))";
by (blast_tac (claset() addSDs [bspec,rename_numerals thy
real_gt_zero_preal_Ex RS iffD1]) 1);
qed "real_sup_lemma1";
-Goal "[| ! x:P. #0 < x; ? x. x: P; ? y. !x: P. x < y |] \
-\ ==> (? X. X: {w. real_of_preal w : P}) & \
-\ (? Y. !X: {w. real_of_preal w : P}. X < Y)";
+Goal "[| ALL x:P. #0 < x; EX x. x: P; EX y. ALL x: P. x < y |] \
+\ ==> (EX X. X: {w. real_of_preal w : P}) & \
+\ (EX Y. ALL X: {w. real_of_preal w : P}. X < Y)";
by (rtac conjI 1);
by (blast_tac (claset() addDs [bspec, rename_numerals thy
real_gt_zero_preal_Ex RS iffD1]) 1);
@@ -49,8 +49,8 @@
only have one case split
**)
-Goal "[| ! x:P. (#0::real) < x; ? x. x: P; ? y. !x: P. x < y |] \
-\ ==> (? S. !y. (? x: P. y < x) = (y < S))";
+Goal "[| ALL x:P. (#0::real) < x; EX x. x: P; EX y. ALL x: P. x < y |] \
+\ ==> (EX S. ALL y. (EX x: P. y < x) = (y < S))";
by (res_inst_tac
[("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1);
by Auto_tac;
@@ -128,7 +128,7 @@
(*-------------------------------
Lemmas
-------------------------------*)
-Goal "! y : {z. ? x: P. z = x + (-xa) + #1} Int {x. #0 < x}. #0 < y";
+Goal "ALL y : {z. EX x: P. z = x + (-xa) + #1} Int {x. #0 < x}. #0 < y";
by Auto_tac;
qed "real_sup_lemma3";
@@ -158,9 +158,9 @@
Goal "[| EX X. X: S; EX Y. isUb (UNIV::real set) S Y |] \
\ ==> EX t. isLub (UNIV :: real set) S t";
by (Step_tac 1);
-by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + #1} \
+by (subgoal_tac "EX u. u: {z. EX x: S. z = x + (-X) + #1} \
\ Int {x. #0 < x}" 1);
-by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + #1} \
+by (subgoal_tac "isUb (UNIV::real set) ({z. EX x: S. z = x + (-X) + #1} \
\ Int {x. #0 < x}) (Y + (-X) + #1)" 1);
by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1);
by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac,
@@ -168,7 +168,7 @@
by (res_inst_tac [("x","t + X + (-#1)")] exI 1);
by (rtac isLubI2 1);
by (rtac setgeI 2 THEN Step_tac 2);
-by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + #1} \
+by (subgoal_tac "isUb (UNIV:: real set) ({z. EX x: S. z = x + (-X) + #1} \
\ Int {x. #0 < x}) (y + (-X) + #1)" 2);
by (dres_inst_tac [("y","(y + (- X) + #1)")] isLub_le_isUb 2
THEN assume_tac 2);
--- a/src/HOL/Real/ROOT.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/ROOT.ML Wed Jun 07 12:14:18 2000 +0200
@@ -8,7 +8,5 @@
Linear real arithmetic is installed in RealBin.ML.
*)
-time_use_thy "RealDef";
-use "simproc.ML";
time_use_thy "Real";
time_use_thy "Hyperreal/HyperDef";
--- a/src/HOL/Real/RealAbs.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealAbs.ML Wed Jun 07 12:14:18 2000 +0200
@@ -86,26 +86,15 @@
by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
qed "abs_ge_minus_self";
-(* case splits nightmare *)
Goalw [abs_real_def] "abs (x * y) = abs x * abs (y::real)";
-by (auto_tac (claset(),
- simpset() addsimps [real_minus_mult_eq1, real_minus_mult_commute,
- real_minus_mult_eq2]));
-by (blast_tac (claset() addDs [full_rename_numerals thy real_le_mult_order]) 1);
-by (auto_tac (claset() addSDs [not_real_leE], simpset()));
-by (EVERY1[dtac (full_rename_numerals thy real_mult_le_zero),
- assume_tac, dtac real_le_anti_sym]);
-by (EVERY[dtac (full_rename_numerals thy real_mult_le_zero) 3,
- assume_tac 3, dtac real_le_anti_sym 3]);
-by (dtac (full_rename_numerals thy real_mult_less_zero1) 5 THEN assume_tac 5);
-by (auto_tac (claset() addDs [real_less_asym,sym],
- simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac));
+by (auto_tac (claset() addSDs [order_antisym],
+ simpset() addsimps [real_0_le_times_iff]));
qed "abs_mult";
Goalw [abs_real_def] "x~= (#0::real) ==> abs(rinv(x)) = rinv(abs(x))";
-by (auto_tac (claset(), simpset() addsimps [real_le_less] @
- (map (full_rename_numerals thy) [real_minus_rinv,
- real_rinv_gt_zero])));
+by (auto_tac (claset(),
+ simpset() addsimps [real_le_less] @
+ (map (full_rename_numerals thy) [real_minus_rinv, real_rinv_gt_zero])));
by (etac (full_rename_numerals thy (real_rinv_less_zero
RSN (2,real_less_asym))) 1);
by (arith_tac 1);
--- a/src/HOL/Real/RealBin.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealBin.ML Wed Jun 07 12:14:18 2000 +0200
@@ -13,7 +13,7 @@
qed "real_number_of";
Addsimps [real_number_of];
-Goalw [real_number_of_def] "0r = #0";
+Goalw [real_number_of_def] "(0::real) = #0";
by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1);
qed "zero_eq_numeral_0";
@@ -109,14 +109,14 @@
Addsimps [le_real_number_of_eq_not_less];
-(*** New versions of existing theorems involving 0r, 1r ***)
+(*** New versions of existing theorems involving 0, 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*)
+(*Maps 0 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];
@@ -124,7 +124,7 @@
fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th);
-(*Now insert some identities previously stated for 0r and 1r*)
+(*Now insert some identities previously stated for 0 and 1r*)
(** RealDef & Real **)
@@ -136,6 +136,17 @@
real_mult_minus_1_right, real_mult_minus_1, real_rinv_1,
real_minus_zero_less_iff]);
+AddIffs (map (rename_numerals thy) [real_mult_is_0, real_0_is_mult]);
+
+bind_thm ("real_0_less_times_iff",
+ rename_numerals thy real_zero_less_times_iff);
+bind_thm ("real_0_le_times_iff",
+ rename_numerals thy real_zero_le_times_iff);
+bind_thm ("real_times_less_0_iff",
+ rename_numerals thy real_times_less_zero_iff);
+bind_thm ("real_times_le_0_iff",
+ rename_numerals thy real_times_le_zero_iff);
+
(*Perhaps add some theorems that aren't in the default simpset, as
done in Integ/NatBin.ML*)
@@ -201,3 +212,27 @@
asm_full_simplify real_numeral_ss (change_theory thy th);
+(** Simplification of arithmetic when nested to the right **)
+
+Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::real)";
+by Auto_tac;
+qed "real_add_number_of_left";
+
+Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::real)";
+by (simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
+qed "real_mult_number_of_left";
+
+Goalw [real_diff_def]
+ "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::real)";
+by (rtac real_add_number_of_left 1);
+qed "real_add_number_of_diff1";
+
+Goal "number_of v + (c - number_of w) = \
+\ number_of (bin_add v (bin_minus w)) + (c::real)";
+by (stac (diff_real_number_of RS sym) 1);
+by Auto_tac;
+qed "real_add_number_of_diff2";
+
+Addsimps [real_add_number_of_left, real_mult_number_of_left,
+ real_add_number_of_diff1, real_add_number_of_diff2];
+
--- a/src/HOL/Real/RealDef.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealDef.ML Wed Jun 07 12:14:18 2000 +0200
@@ -135,13 +135,13 @@
by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1);
qed "inj_real_minus";
-Goalw [real_zero_def] "-0r = 0r";
+Goalw [real_zero_def] "-0 = (0::real)";
by (simp_tac (simpset() addsimps [real_minus]) 1);
qed "real_minus_zero";
Addsimps [real_minus_zero];
-Goal "(-x = 0r) = (x = 0r)";
+Goal "(-x = 0) = (x = (0::real))";
by (res_inst_tac [("z","x")] eq_Abs_real 1);
by (auto_tac (claset(),
simpset() addsimps [real_zero_def, real_minus] @ preal_add_ac));
@@ -149,10 +149,6 @@
Addsimps [real_minus_zero_iff];
-Goal "(-x ~= 0r) = (x ~= 0r)";
-by Auto_tac;
-qed "real_minus_not_zero_iff";
-
(*** Congruence property for addition ***)
Goalw [congruent2_def]
"congruent2 realrel (%p1 p2. \
@@ -196,25 +192,25 @@
(* real addition is an AC operator *)
bind_thms ("real_add_ac", [real_add_assoc,real_add_commute,real_add_left_commute]);
-Goalw [real_of_preal_def,real_zero_def] "0r + z = z";
+Goalw [real_of_preal_def,real_zero_def] "(0::real) + z = z";
by (res_inst_tac [("z","z")] eq_Abs_real 1);
by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1);
qed "real_add_zero_left";
Addsimps [real_add_zero_left];
-Goal "z + 0r = z";
+Goal "z + (0::real) = z";
by (simp_tac (simpset() addsimps [real_add_commute]) 1);
qed "real_add_zero_right";
Addsimps [real_add_zero_right];
-Goalw [real_zero_def] "z + (-z) = 0r";
+Goalw [real_zero_def] "z + (-z) = (0::real)";
by (res_inst_tac [("z","z")] eq_Abs_real 1);
by (asm_full_simp_tac (simpset() addsimps [real_minus,
real_add, preal_add_commute]) 1);
qed "real_add_minus";
Addsimps [real_add_minus];
-Goal "(-z) + z = 0r";
+Goal "(-z) + z = (0::real)";
by (simp_tac (simpset() addsimps [real_add_commute]) 1);
qed "real_add_minus_left";
Addsimps [real_add_minus_left];
@@ -230,31 +226,31 @@
Addsimps [real_add_minus_cancel, real_minus_add_cancel];
-Goal "? y. (x::real) + y = 0r";
+Goal "EX y. (x::real) + y = 0";
by (blast_tac (claset() addIs [real_add_minus]) 1);
qed "real_minus_ex";
-Goal "?! y. (x::real) + y = 0r";
+Goal "EX! y. (x::real) + y = 0";
by (auto_tac (claset() addIs [real_add_minus],simpset()));
by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
qed "real_minus_ex1";
-Goal "?! y. y + (x::real) = 0r";
+Goal "EX! y. y + (x::real) = 0";
by (auto_tac (claset() addIs [real_add_minus_left],simpset()));
by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
qed "real_minus_left_ex1";
-Goal "x + y = 0r ==> x = -y";
+Goal "x + y = (0::real) ==> x = -y";
by (cut_inst_tac [("z","y")] real_add_minus_left 1);
by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1);
by (Blast_tac 1);
qed "real_add_minus_eq_minus";
-Goal "? (y::real). x = -y";
+Goal "EX (y::real). x = -y";
by (cut_inst_tac [("x","x")] real_minus_ex 1);
by (etac exE 1 THEN dtac real_add_minus_eq_minus 1);
by (Fast_tac 1);
@@ -278,29 +274,29 @@
by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
qed "real_add_right_cancel";
-Goal "((x::real) = y) = (0r = x + (- y))";
+Goal "((x::real) = y) = (0 = x + (- y))";
by (Step_tac 1);
by (res_inst_tac [("x1","-y")]
(real_add_right_cancel RS iffD1) 2);
by Auto_tac;
qed "real_eq_minus_iff";
-Goal "((x::real) = y) = (x + (- y) = 0r)";
+Goal "((x::real) = y) = (x + (- y) = 0)";
by (Step_tac 1);
by (res_inst_tac [("x1","-y")]
(real_add_right_cancel RS iffD1) 2);
by Auto_tac;
qed "real_eq_minus_iff2";
-Goal "0r - x = -x";
+Goal "(0::real) - x = -x";
by (simp_tac (simpset() addsimps [real_diff_def]) 1);
qed "real_diff_0";
-Goal "x - 0r = x";
+Goal "x - (0::real) = x";
by (simp_tac (simpset() addsimps [real_diff_def]) 1);
qed "real_diff_0_right";
-Goal "x - x = 0r";
+Goal "x - x = (0::real)";
by (simp_tac (simpset() addsimps [real_diff_def]) 1);
qed "real_diff_self";
@@ -355,13 +351,15 @@
preal_add_ac @ preal_mult_ac) 1);
qed "real_mult_assoc";
-qed_goal "real_mult_left_commute" thy
- "(z1::real) * (z2 * z3) = z2 * (z1 * z3)"
- (fn _ => [rtac (real_mult_commute RS trans) 1, rtac (real_mult_assoc RS trans) 1,
- rtac (real_mult_commute RS arg_cong) 1]);
+Goal "(z1::real) * (z2 * z3) = z2 * (z1 * z3)";
+by (rtac (real_mult_commute RS trans) 1);
+by (rtac (real_mult_assoc RS trans) 1);
+by (rtac (real_mult_commute RS arg_cong) 1);
+qed "real_mult_left_commute";
(* real multiplication is an AC operator *)
-bind_thms ("real_mult_ac", [real_mult_assoc, real_mult_commute, real_mult_left_commute]);
+bind_thms ("real_mult_ac",
+ [real_mult_assoc, real_mult_commute, real_mult_left_commute]);
Goalw [real_one_def,pnat_one_def] "1r * z = z";
by (res_inst_tac [("z","z")] eq_Abs_real 1);
@@ -379,14 +377,14 @@
Addsimps [real_mult_1_right];
-Goalw [real_zero_def,pnat_one_def] "0r * z = 0r";
+Goalw [real_zero_def,pnat_one_def] "0 * z = (0::real)";
by (res_inst_tac [("z","z")] eq_Abs_real 1);
by (asm_full_simp_tac (simpset() addsimps [real_mult,
preal_add_mult_distrib2,preal_mult_1_right]
@ preal_mult_ac @ preal_add_ac) 1);
qed "real_mult_0";
-Goal "z * 0r = 0r";
+Goal "z * 0 = (0::real)";
by (simp_tac (simpset() addsimps [real_mult_commute, real_mult_0]) 1);
qed "real_mult_0_right";
@@ -401,19 +399,16 @@
qed "real_minus_mult_eq1";
Goal "-(x * y) = x * (- y :: real)";
-by (res_inst_tac [("z","x")] eq_Abs_real 1);
-by (res_inst_tac [("z","y")] eq_Abs_real 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_minus,real_mult]
- @ preal_mult_ac @ preal_add_ac));
+by (simp_tac (simpset() addsimps [inst "z" "x" real_mult_commute,
+ real_minus_mult_eq1]) 1);
qed "real_minus_mult_eq2";
+Addsimps [real_minus_mult_eq1 RS sym, real_minus_mult_eq2 RS sym];
+
Goal "(- 1r) * z = -z";
-by (simp_tac (simpset() addsimps [real_minus_mult_eq1 RS sym]) 1);
+by (Simp_tac 1);
qed "real_mult_minus_1";
-Addsimps [real_mult_minus_1];
-
Goal "z * (- 1r) = -z";
by (stac real_mult_commute 1);
by (Simp_tac 1);
@@ -455,15 +450,15 @@
preal_add_ac @ preal_mult_ac) 1);
qed "real_add_mult_distrib";
-val real_mult_commute'= read_instantiate [("z","w")] real_mult_commute;
+val real_mult_commute'= inst "z" "w" real_mult_commute;
Goal "(w::real) * (z1 + z2) = (w * z1) + (w * z2)";
-by (simp_tac (simpset() addsimps [real_mult_commute',real_add_mult_distrib]) 1);
+by (simp_tac (simpset() addsimps [real_mult_commute',
+ real_add_mult_distrib]) 1);
qed "real_add_mult_distrib2";
Goalw [real_diff_def] "((z1::real) - z2) * w = (z1 * w) - (z2 * w)";
-by (simp_tac (simpset() addsimps [real_add_mult_distrib,
- real_minus_mult_eq1]) 1);
+by (simp_tac (simpset() addsimps [real_add_mult_distrib]) 1);
qed "real_diff_mult_distrib";
Goal "(w::real) * (z1 - z2) = (w * z1) - (w * z2)";
@@ -472,19 +467,19 @@
qed "real_diff_mult_distrib2";
(*** one and zero are distinct ***)
-Goalw [real_zero_def,real_one_def] "0r ~= 1r";
+Goalw [real_zero_def,real_one_def] "0 ~= 1r";
by (auto_tac (claset(),
simpset() addsimps [preal_self_less_add_left RS preal_not_refl2]));
qed "real_zero_not_eq_one";
(*** existence of inverse ***)
-(** lemma -- alternative definition for 0r **)
-Goalw [real_zero_def] "0r = Abs_real (realrel ^^ {(x, x)})";
+(** lemma -- alternative definition of 0 **)
+Goalw [real_zero_def] "0 = Abs_real (realrel ^^ {(x, x)})";
by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
qed "real_zero_iff";
Goalw [real_zero_def,real_one_def]
- "!!(x::real). x ~= 0r ==> ? y. x*y = 1r";
+ "!!(x::real). x ~= 0 ==> EX y. x*y = 1r";
by (res_inst_tac [("z","x")] eq_Abs_real 1);
by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
@@ -502,30 +497,30 @@
@ preal_add_ac @ preal_mult_ac));
qed "real_mult_inv_right_ex";
-Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r";
+Goal "!!(x::real). x ~= 0 ==> EX y. y*x = 1r";
by (asm_simp_tac (simpset() addsimps [real_mult_commute,
real_mult_inv_right_ex]) 1);
qed "real_mult_inv_left_ex";
-Goalw [rinv_def] "x ~= 0r ==> rinv(x)*x = 1r";
+Goalw [rinv_def] "x ~= 0 ==> rinv(x)*x = 1r";
by (ftac real_mult_inv_left_ex 1);
by (Step_tac 1);
by (rtac selectI2 1);
by Auto_tac;
qed "real_mult_inv_left";
-Goal "x ~= 0r ==> x*rinv(x) = 1r";
+Goal "x ~= 0 ==> x*rinv(x) = 1r";
by (auto_tac (claset() addIs [real_mult_commute RS subst],
simpset() addsimps [real_mult_inv_left]));
qed "real_mult_inv_right";
-Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
+Goal "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)";
by Auto_tac;
by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1);
qed "real_mult_left_cancel";
-Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
+Goal "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)";
by (Step_tac 1);
by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
by (asm_full_simp_tac
@@ -540,7 +535,7 @@
by Auto_tac;
qed "real_mult_right_cancel_ccontr";
-Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
+Goalw [rinv_def] "x ~= 0 ==> rinv(x) ~= 0";
by (ftac real_mult_inv_left_ex 1);
by (etac exE 1);
by (rtac selectI2 1);
@@ -551,7 +546,7 @@
Addsimps [real_mult_inv_left,real_mult_inv_right];
-Goal "[| x ~= 0r; y ~= 0r |] ==> x * y ~= 0r";
+Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)";
by (Step_tac 1);
by (dres_inst_tac [("f","%z. rinv x*z")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
@@ -559,7 +554,7 @@
bind_thm ("real_mult_not_zeroE",real_mult_not_zero RS notE);
-Goal "x ~= 0r ==> rinv(rinv x) = x";
+Goal "x ~= 0 ==> rinv(rinv x) = x";
by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1);
by (etac rinv_not_zero 1);
by (auto_tac (claset() addDs [rinv_not_zero],simpset()));
@@ -567,21 +562,19 @@
Goalw [rinv_def] "rinv(1r) = 1r";
by (cut_facts_tac [real_zero_not_eq_one RS
- not_sym RS real_mult_inv_left_ex] 1);
-by (etac exE 1);
-by (rtac selectI2 1);
+ not_sym RS real_mult_inv_left_ex] 1);
by (auto_tac (claset(),
- simpset() addsimps
- [real_zero_not_eq_one RS not_sym]));
+ simpset() addsimps [real_zero_not_eq_one RS not_sym]));
qed "real_rinv_1";
Addsimps [real_rinv_1];
-Goal "x ~= 0r ==> rinv(-x) = -rinv(x)";
+Goal "x ~= 0 ==> rinv(-x) = -rinv(x)";
by (res_inst_tac [("c1","-x")] (real_mult_right_cancel RS iffD1) 1);
+by (stac real_mult_inv_left 2);
by Auto_tac;
qed "real_minus_rinv";
-Goal "[| x ~= 0r; y ~= 0r |] ==> rinv(x*y) = rinv(x)*rinv(y)";
+Goal "[| x ~= 0; y ~= 0 |] ==> rinv(x*y) = rinv(x)*rinv(y)";
by (forw_inst_tac [("y","y")] real_mult_not_zero 1 THEN assume_tac 1);
by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
@@ -682,13 +675,13 @@
Goalw [real_of_preal_def]
"!!(x::preal). y < x ==> \
-\ ? m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m";
+\ EX m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m";
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
simpset() addsimps preal_add_ac));
qed "real_of_preal_ExI";
Goalw [real_of_preal_def]
- "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = \
+ "!!(x::preal). EX m. Abs_real (realrel ^^ {(x,y)}) = \
\ real_of_preal m ==> y < x";
by (auto_tac (claset(),
simpset() addsimps
@@ -697,13 +690,13 @@
[preal_add_assoc RS sym,preal_self_less_add_left]) 1);
qed "real_of_preal_ExD";
-Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m) = (y < x)";
+Goal "(EX m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m) = (y < x)";
by (blast_tac (claset() addSIs [real_of_preal_ExI,real_of_preal_ExD]) 1);
qed "real_of_preal_iff";
(*** Gleason prop 9-4.4 p 127 ***)
Goalw [real_of_preal_def,real_zero_def]
- "? m. (x::real) = real_of_preal m | x = 0r | x = -(real_of_preal m)";
+ "EX m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)";
by (res_inst_tac [("z","x")] eq_Abs_real 1);
by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac));
by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1);
@@ -713,7 +706,7 @@
qed "real_of_preal_trichotomy";
Goal "!!P. [| !!m. x = real_of_preal m ==> P; \
-\ x = 0r ==> P; \
+\ x = 0 ==> P; \
\ !!m. x = -(real_of_preal m) ==> P |] ==> P";
by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
by Auto_tac;
@@ -756,7 +749,7 @@
preal_add_assoc RS sym]) 1);
qed "real_of_preal_minus_less_self";
-Goalw [real_zero_def] "- real_of_preal m < 0r";
+Goalw [real_zero_def] "- real_of_preal m < 0";
by (auto_tac (claset(),
simpset() addsimps [real_of_preal_def,
real_less_def,real_minus]));
@@ -767,13 +760,13 @@
[preal_self_less_add_right] @ preal_add_ac) 1);
qed "real_of_preal_minus_less_zero";
-Goal "~ 0r < - real_of_preal m";
+Goal "~ 0 < - real_of_preal m";
by (cut_facts_tac [real_of_preal_minus_less_zero] 1);
by (fast_tac (claset() addDs [real_less_trans]
addEs [real_less_irrefl]) 1);
qed "real_of_preal_not_minus_gt_zero";
-Goalw [real_zero_def] "0r < real_of_preal m";
+Goalw [real_zero_def] "0 < real_of_preal m";
by (auto_tac (claset(),simpset() addsimps
[real_of_preal_def,real_less_def,real_minus]));
by (REPEAT(rtac exI 1));
@@ -783,20 +776,20 @@
[preal_self_less_add_right] @ preal_add_ac) 1);
qed "real_of_preal_zero_less";
-Goal "~ real_of_preal m < 0r";
+Goal "~ real_of_preal m < 0";
by (cut_facts_tac [real_of_preal_zero_less] 1);
by (blast_tac (claset() addDs [real_less_trans]
addEs [real_less_irrefl]) 1);
qed "real_of_preal_not_less_zero";
-Goal "0r < - (- real_of_preal m)";
+Goal "0 < - (- real_of_preal m)";
by (simp_tac (simpset() addsimps
[real_of_preal_zero_less]) 1);
qed "real_minus_minus_zero_less";
(* another lemma *)
Goalw [real_zero_def]
- "0r < real_of_preal m + real_of_preal m1";
+ "0 < real_of_preal m + real_of_preal m1";
by (auto_tac (claset(),
simpset() addsimps [real_of_preal_def,
real_less_def,real_add]));
@@ -962,7 +955,7 @@
by (blast_tac (claset() addSEs [real_less_asym]) 1);
qed "real_less_le";
-Goal "(0r < -R) = (R < 0r)";
+Goal "(0 < -R) = (R < (0::real))";
by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
by (auto_tac (claset(),
simpset() addsimps [real_of_preal_not_minus_gt_zero,
@@ -972,7 +965,7 @@
Addsimps [real_minus_zero_less_iff];
-Goal "(-R < 0r) = (0r < R)";
+Goal "(-R < 0) = ((0::real) < R)";
by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
by (auto_tac (claset(),
simpset() addsimps [real_of_preal_not_minus_gt_zero,
@@ -981,7 +974,7 @@
qed "real_minus_zero_less_iff2";
(*Alternative definition for real_less*)
-Goal "R < S ==> ? T. 0r < T & R + T = S";
+Goal "R < S ==> EX T::real. 0 < T & R + T = S";
by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
by (ALLGOALS(res_inst_tac [("x","S")] real_of_preal_trichotomyE));
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
@@ -999,7 +992,7 @@
qed "real_less_add_positive_left_Ex";
(** change naff name(s)! **)
-Goal "(W < S) ==> (0r < S + (-W))";
+Goal "(W < S) ==> (0 < S + (-W::real))";
by (dtac real_less_add_positive_left_Ex 1);
by (auto_tac (claset(),
simpset() addsimps [real_add_minus,
@@ -1011,7 +1004,7 @@
qed "real_lemma_change_eq_subj";
(* FIXME: long! *)
-Goal "(0r < S + (-W)) ==> (W < S)";
+Goal "(0 < S + (-W::real)) ==> (W < S)";
by (rtac ccontr 1);
by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
by (auto_tac (claset(),
@@ -1026,13 +1019,13 @@
by (auto_tac (claset() addEs [real_less_asym], simpset()));
qed "real_sum_gt_zero_less";
-Goal "(0r < S + (-W)) = (W < S)";
+Goal "(0 < S + (-W::real)) = (W < S)";
by (blast_tac (claset() addIs [real_less_sum_gt_zero,
real_sum_gt_zero_less]) 1);
qed "real_less_sum_gt_0_iff";
-Goalw [real_diff_def] "(x<y) = (x-y < 0r)";
+Goalw [real_diff_def] "(x<y) = (x-y < (0::real))";
by (stac (real_minus_zero_less_iff RS sym) 1);
by (simp_tac (simpset() addsimps [real_add_commute,
real_less_sum_gt_0_iff]) 1);
--- a/src/HOL/Real/RealDef.thy Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealDef.thy Wed Jun 07 12:14:18 2000 +0200
@@ -15,17 +15,16 @@
instance
- real :: {ord, plus, times, minus}
+ real :: {ord, zero, plus, times, minus}
consts
- "0r" :: real ("0r")
"1r" :: real ("1r")
defs
real_zero_def
- "0r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
+ "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
preal_of_prat(prat_of_pnat 1p))})"
real_one_def
"1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) +
@@ -44,7 +43,7 @@
preal_of_prat(prat_of_pnat 1p))})"
rinv :: real => real
- "rinv(R) == (@S. R ~= 0r & S*R = 1r)"
+ "rinv(R) == (@S. R ~= 0 & S*R = 1r)"
real_of_posnat :: nat => real
"real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
--- a/src/HOL/Real/RealInt.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealInt.ML Wed Jun 07 12:14:18 2000 +0200
@@ -37,7 +37,7 @@
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";
+Goalw [int_def,real_zero_def] "real_of_int (int 0) = 0";
by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1);
qed "real_of_int_zero";
@@ -97,13 +97,13 @@
qed "real_of_nat_real_of_int";
(* put with other properties of real_of_nat? *)
-Goal "neg z ==> real_of_nat (nat z) = 0r";
+Goal "neg z ==> real_of_nat (nat z) = 0";
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)";
+Goal "(real_of_int x = 0) = (x = int 0)";
by (auto_tac (claset() addIs [inj_real_of_int RS injD],
HOL_ss addsimps [real_of_int_zero]));
qed "real_of_int_zero_cancel";
--- a/src/HOL/Real/RealOrd.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealOrd.ML Wed Jun 07 12:14:18 2000 +0200
@@ -5,30 +5,89 @@
Description: Type "real" is a linear order
*)
-Goal "(0r < x) = (? y. x = real_of_preal y)";
+(**** The simproc abel_cancel ****)
+
+(*** Two lemmas needed for the simprocs ***)
+
+(*Deletion of other terms in the formula, seeking the -x at the front of z*)
+Goal "((x::real) + (y + z) = y + u) = ((x + z) = u)";
+by (stac real_add_left_commute 1);
+by (rtac real_add_left_cancel 1);
+qed "real_add_cancel_21";
+
+(*A further rule to deal with the case that
+ everything gets cancelled on the right.*)
+Goal "((x::real) + (y + z) = y) = (x = -z)";
+by (stac real_add_left_commute 1);
+by (res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1
+ THEN stac real_add_left_cancel 1);
+by (simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1);
+qed "real_add_cancel_end";
+
+
+structure Real_Cancel_Data =
+struct
+ val ss = HOL_ss
+ val eq_reflection = eq_reflection
+
+ val thy = RealDef.thy
+ val T = HOLogic.realT
+ val zero = Const ("0", T)
+ val restrict_to_left = restrict_to_left
+ val add_cancel_21 = real_add_cancel_21
+ val add_cancel_end = real_add_cancel_end
+ val add_left_cancel = real_add_left_cancel
+ val add_assoc = real_add_assoc
+ val add_commute = real_add_commute
+ val add_left_commute = real_add_left_commute
+ val add_0 = real_add_zero_left
+ val add_0_right = real_add_zero_right
+
+ val eq_diff_eq = real_eq_diff_eq
+ val eqI_rules = [real_less_eqI, real_eq_eqI, real_le_eqI]
+ fun dest_eqI th =
+ #1 (HOLogic.dest_bin "op =" HOLogic.boolT
+ (HOLogic.dest_Trueprop (concl_of th)))
+
+ val diff_def = real_diff_def
+ val minus_add_distrib = real_minus_add_distrib
+ val minus_minus = real_minus_minus
+ val minus_0 = real_minus_zero
+ val add_inverses = [real_add_minus, real_add_minus_left];
+ val cancel_simps = [real_add_minus_cancel, real_minus_add_cancel]
+end;
+
+structure Real_Cancel = Abel_Cancel (Real_Cancel_Data);
+
+Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
+
+
+(**** Theorems about the ordering ****)
+
+Goal "(0 < x) = (EX y. x = real_of_preal y)";
by (auto_tac (claset(), simpset() addsimps [real_of_preal_zero_less]));
by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
by (blast_tac (claset() addSEs [real_less_irrefl,
real_of_preal_not_minus_gt_zero RS notE]) 1);
qed "real_gt_zero_preal_Ex";
-Goal "real_of_preal z < x ==> ? y. x = real_of_preal y";
+Goal "real_of_preal z < x ==> EX y. x = real_of_preal y";
by (blast_tac (claset() addSDs [real_of_preal_zero_less RS real_less_trans]
addIs [real_gt_zero_preal_Ex RS iffD1]) 1);
qed "real_gt_preal_preal_Ex";
-Goal "real_of_preal z <= x ==> ? y. x = real_of_preal y";
+Goal "real_of_preal z <= x ==> EX y. x = real_of_preal y";
by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
real_gt_preal_preal_Ex]) 1);
qed "real_ge_preal_preal_Ex";
-Goal "y <= 0r ==> !x. y < real_of_preal x";
+Goal "y <= 0 ==> ALL x. y < real_of_preal x";
by (auto_tac (claset() addEs [real_le_imp_less_or_eq RS disjE]
addIs [real_of_preal_zero_less RSN(2,real_less_trans)],
simpset() addsimps [real_of_preal_zero_less]));
qed "real_less_all_preal";
-Goal "~ 0r < y ==> !x. y < real_of_preal x";
+Goal "~ 0 < y ==> ALL x. y < real_of_preal x";
by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1);
qed "real_less_all_real2";
@@ -38,22 +97,22 @@
by (simp_tac (simpset() addsimps [real_add_commute]) 1);
qed "real_less_swap_iff";
-Goal "[| R + L = S; 0r < L |] ==> R < S";
+Goal "[| R + L = S; (0::real) < L |] ==> R < S";
by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
by (auto_tac (claset(), simpset() addsimps real_add_ac));
qed "real_lemma_add_positive_imp_less";
-Goal "? T. 0r < T & R + T = S ==> R < S";
+Goal "EX T::real. 0 < T & R + T = S ==> R < S";
by (blast_tac (claset() addIs [real_lemma_add_positive_imp_less]) 1);
qed "real_ex_add_positive_left_less";
(*Alternative definition for real_less. NOT for rewriting*)
-Goal "(R < S) = (? T. 0r < T & R + T = S)";
+Goal "(R < S) = (EX T::real. 0 < T & R + T = S)";
by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex,
real_ex_add_positive_left_less]) 1);
qed "real_less_iff_add";
-Goal "(0r < x) = (-x < x)";
+Goal "((0::real) < x) = (-x < x)";
by Safe_tac;
by (rtac ccontr 2 THEN forward_tac
[real_leI RS real_le_imp_less_or_eq] 2);
@@ -65,17 +124,17 @@
[real_gt_zero_preal_Ex,real_of_preal_minus_less_self]));
qed "real_gt_zero_iff";
-Goal "(x < 0r) = (x < -x)";
+Goal "(x < (0::real)) = (x < -x)";
by (rtac (real_minus_zero_less_iff RS subst) 1);
by (stac real_gt_zero_iff 1);
by (Full_simp_tac 1);
qed "real_lt_zero_iff";
-Goalw [real_le_def] "(0r <= x) = (-x <= x)";
+Goalw [real_le_def] "((0::real) <= x) = (-x <= x)";
by (auto_tac (claset(), simpset() addsimps [real_lt_zero_iff RS sym]));
qed "real_ge_zero_iff";
-Goalw [real_le_def] "(x <= 0r) = (x <= -x)";
+Goalw [real_le_def] "(x <= (0::real)) = (x <= -x)";
by (auto_tac (claset(), simpset() addsimps [real_gt_zero_iff RS sym]));
qed "real_le_zero_iff";
@@ -86,31 +145,31 @@
by (etac preal_less_irrefl 1);
qed "real_of_preal_le_iff";
-Goal "[| 0r < x; 0r < y |] ==> 0r < x * y";
+Goal "[| 0 < x; 0 < y |] ==> (0::real) < x * y";
by (auto_tac (claset(), simpset() addsimps [real_gt_zero_preal_Ex]));
by (res_inst_tac [("x","y*ya")] exI 1);
by (full_simp_tac (simpset() addsimps [real_of_preal_mult]) 1);
qed "real_mult_order";
-Goal "[| x < 0r; y < 0r |] ==> 0r < x * y";
+Goal "[| x < 0; y < 0 |] ==> (0::real) < x * y";
by (REPEAT(dtac (real_minus_zero_less_iff RS iffD2) 1));
by (dtac real_mult_order 1 THEN assume_tac 1);
by (Asm_full_simp_tac 1);
qed "real_mult_less_zero1";
-Goal "[| 0r <= x; 0r <= y |] ==> 0r <= x * y";
+Goal "[| 0 <= x; 0 <= y |] ==> (0::real) <= x * y";
by (REPEAT(dtac real_le_imp_less_or_eq 1));
by (auto_tac (claset() addIs [real_mult_order, real_less_imp_le],
simpset()));
qed "real_le_mult_order";
-Goal "[| 0r < x; 0r <= y |] ==> 0r <= x * y";
+Goal "[| 0 < x; 0 <= y |] ==> (0::real) <= x * y";
by (dtac real_le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [real_mult_order,
real_less_imp_le],simpset()));
qed "real_less_le_mult_order";
-Goal "[| x <= 0r; y <= 0r |] ==> 0r <= x * y";
+Goal "[| x <= 0; y <= 0 |] ==> (0::real) <= x * y";
by (rtac real_less_or_eq_imp_le 1);
by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
by Auto_tac;
@@ -118,7 +177,7 @@
by (auto_tac (claset() addDs [real_mult_less_zero1],simpset()));
qed "real_mult_le_zero1";
-Goal "[| 0r <= x; y < 0r |] ==> x * y <= 0r";
+Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::real)";
by (rtac real_less_or_eq_imp_le 1);
by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
by Auto_tac;
@@ -128,14 +187,14 @@
addIs [real_minus_mult_eq2 RS ssubst]) 1);
qed "real_mult_le_zero";
-Goal "[| 0r < x; y < 0r |] ==> x*y < 0r";
+Goal "[| 0 < x; y < 0 |] ==> x*y < (0::real)";
by (dtac (real_minus_zero_less_iff RS iffD2) 1);
by (dtac real_mult_order 1 THEN assume_tac 1);
by (rtac (real_minus_zero_less_iff RS iffD1) 1);
-by (asm_full_simp_tac (simpset() addsimps [real_minus_mult_eq2]) 1);
+by (Asm_full_simp_tac 1);
qed "real_mult_less_zero";
-Goalw [real_one_def] "0r < 1r";
+Goalw [real_one_def] "0 < 1r";
by (auto_tac (claset() addIs [real_gt_zero_preal_Ex RS iffD2],
simpset() addsimps [real_of_preal_def]));
qed "real_zero_less_one";
@@ -198,13 +257,13 @@
by (Full_simp_tac 1);
qed "real_le_add_left_cancel";
-Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
+Goal "[| 0 < x; 0 < y |] ==> (0::real) < x + y";
by (etac real_less_trans 1);
by (dtac real_add_less_mono2 1);
by (Full_simp_tac 1);
qed "real_add_order";
-Goal "[| 0r <= x; 0r <= y |] ==> 0r <= x + y";
+Goal "[| 0 <= x; 0 <= y |] ==> (0::real) <= x + y";
by (REPEAT(dtac real_le_imp_less_or_eq 1));
by (auto_tac (claset() addIs [real_add_order, real_less_imp_le],
simpset()));
@@ -233,7 +292,7 @@
simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one]));
qed "real_less_Ex";
-Goal "0r < r ==> u + (-r) < u";
+Goal "(0::real) < r ==> u + (-r) < u";
by (res_inst_tac [("C","r")] real_less_add_right_cancel 1);
by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
qed "real_add_minus_positive_less_self";
@@ -249,13 +308,13 @@
qed "real_le_minus_iff";
Addsimps [real_le_minus_iff RS sym];
-Goal "0r <= 1r";
+Goal "0 <= 1r";
by (rtac (real_zero_less_one RS real_less_imp_le) 1);
qed "real_zero_le_one";
Addsimps [real_zero_le_one];
-Goal "0r <= x*x";
-by (res_inst_tac [("R2.0","0r"),("R1.0","x")] real_linear_less2 1);
+Goal "(0::real) <= x*x";
+by (res_inst_tac [("R2.0","0"),("R1.0","x")] real_linear_less2 1);
by (auto_tac (claset() addIs [real_mult_order,
real_mult_less_zero1,real_less_imp_le],
simpset()));
@@ -305,12 +364,12 @@
by (etac (inj_pnat_of_nat RS injD) 1);
qed "inj_real_of_posnat";
-Goalw [real_of_posnat_def] "0r < real_of_posnat n";
+Goalw [real_of_posnat_def] "0 < real_of_posnat n";
by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
by (Blast_tac 1);
qed "real_of_posnat_less_zero";
-Goal "real_of_posnat n ~= 0r";
+Goal "real_of_posnat n ~= 0";
by (rtac (real_of_posnat_less_zero RS real_not_refl2 RS not_sym) 1);
qed "real_of_posnat_not_eq_zero";
Addsimps[real_of_posnat_not_eq_zero];
@@ -324,7 +383,7 @@
qed "real_of_posnat_less_one";
Addsimps [real_of_posnat_less_one];
-Goal "rinv(real_of_posnat n) ~= 0r";
+Goal "rinv(real_of_posnat n) ~= 0";
by (rtac ((real_of_posnat_less_zero RS
real_not_refl2 RS not_sym) RS rinv_not_zero) 1);
qed "real_of_posnat_rinv_not_zero";
@@ -340,7 +399,7 @@
real_not_refl2 RS not_sym)]) 1);
qed "real_of_posnat_rinv_inj";
-Goal "0r < x ==> 0r < rinv x";
+Goal "0 < x ==> 0 < rinv x";
by (EVERY1[rtac ccontr, dtac real_leI]);
by (forward_tac [real_minus_zero_less_iff2 RS iffD2] 1);
by (forward_tac [real_not_refl2 RS not_sym] 1);
@@ -351,7 +410,7 @@
simpset() addsimps [real_minus_mult_eq1 RS sym]));
qed "real_rinv_gt_zero";
-Goal "x < 0r ==> rinv x < 0r";
+Goal "x < 0 ==> rinv x < 0";
by (ftac real_not_refl2 1);
by (dtac (real_minus_zero_less_iff RS iffD2) 1);
by (rtac (real_minus_zero_less_iff RS iffD1) 1);
@@ -359,14 +418,13 @@
by (auto_tac (claset() addIs [real_rinv_gt_zero], simpset()));
qed "real_rinv_less_zero";
-Goal "0r < rinv(real_of_posnat n)";
+Goal "0 < rinv(real_of_posnat n)";
by (rtac (real_of_posnat_less_zero RS real_rinv_gt_zero) 1);
qed "real_of_posnat_rinv_gt_zero";
Addsimps [real_of_posnat_rinv_gt_zero];
Goal "x+x = x*(1r+1r)";
-by (simp_tac (simpset() addsimps
- [real_add_mult_distrib2]) 1);
+by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
qed "real_add_self";
Goal "x < x + 1r";
@@ -379,12 +437,12 @@
by (rtac real_self_less_add_one 1);
qed "real_one_less_two";
-Goal "0r < 1r + 1r";
+Goal "0 < 1r + 1r";
by (rtac ([real_zero_less_one,
real_one_less_two] MRS real_less_trans) 1);
qed "real_zero_less_two";
-Goal "1r + 1r ~= 0r";
+Goal "1r + 1r ~= 0";
by (rtac (real_zero_less_two RS real_not_refl2 RS not_sym) 1);
qed "real_two_not_zero";
@@ -395,7 +453,7 @@
by (full_simp_tac (simpset() addsimps [real_mult_assoc]) 1);
qed "real_sum_of_halves";
-Goal "[| 0r<z; x<y |] ==> x*z<y*z";
+Goal "[| (0::real) < z; x < y |] ==> x*z < y*z";
by (rotate_tac 1 1);
by (dtac real_less_sum_gt_zero 1);
by (rtac real_sum_gt_zero_less 1);
@@ -404,11 +462,11 @@
real_minus_mult_eq2 RS sym, real_mult_commute ]) 1);
qed "real_mult_less_mono1";
-Goal "[| 0r<z; x<y |] ==> z*x<z*y";
+Goal "[| (0::real) < z; x < y |] ==> z*x < z*y";
by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_less_mono1]) 1);
qed "real_mult_less_mono2";
-Goal "[| 0r<z; x*z<y*z |] ==> x<y";
+Goal "[| (0::real) < z; x*z < y*z |] ==> x < y";
by (forw_inst_tac [("x","x*z")] (real_rinv_gt_zero
RS real_mult_less_mono1) 1);
by (auto_tac (claset(),
@@ -416,17 +474,17 @@
[real_mult_assoc,real_not_refl2 RS not_sym]));
qed "real_mult_less_cancel1";
-Goal "[| 0r<z; z*x<z*y |] ==> x<y";
+Goal "[| (0::real) < z; z*x < z*y |] ==> x < y";
by (etac real_mult_less_cancel1 1);
by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1);
qed "real_mult_less_cancel2";
-Goal "0r < z ==> (x*z < y*z) = (x < y)";
+Goal "(0::real) < z ==> (x*z < y*z) = (x < y)";
by (blast_tac (claset() addIs [real_mult_less_mono1,
real_mult_less_cancel1]) 1);
qed "real_mult_less_iff1";
-Goal "0r < z ==> (z*x < z*y) = (x < y)";
+Goal "(0::real) < z ==> (z*x < z*y) = (x < y)";
by (blast_tac (claset() addIs [real_mult_less_mono2,
real_mult_less_cancel2]) 1);
qed "real_mult_less_iff2";
@@ -434,60 +492,60 @@
Addsimps [real_mult_less_iff1,real_mult_less_iff2];
(* 05/00 *)
-Goalw [real_le_def] "[| 0r<z; x*z<=y*z |] ==> x<=y";
+Goalw [real_le_def] "[| (0::real) < z; x*z<=y*z |] ==> x<=y";
by (Auto_tac);
qed "real_mult_le_cancel1";
-Goalw [real_le_def] "!!(x::real). [| 0r<z; z*x<=z*y |] ==> x<=y";
+Goalw [real_le_def] "[| (0::real) < z; z*x<=z*y |] ==> x<=y";
by (Auto_tac);
qed "real_mult_le_cancel2";
-Goalw [real_le_def] "0r < z ==> (x*z <= y*z) = (x <= y)";
+Goalw [real_le_def] "(0::real) < z ==> (x*z <= y*z) = (x <= y)";
by (Auto_tac);
qed "real_mult_le_cancel_iff1";
-Goalw [real_le_def] "0r < z ==> (z*x <= z*y) = (x <= y)";
+Goalw [real_le_def] "(0::real) < z ==> (z*x <= z*y) = (x <= y)";
by (Auto_tac);
qed "real_mult_le_cancel_iff2";
Addsimps [real_mult_le_cancel_iff1,real_mult_le_cancel_iff2];
-Goal "[| 0r<=z; x<y |] ==> x*z<=y*z";
+Goal "[| (0::real) <= z; x < y |] ==> x*z <= y*z";
by (EVERY1 [rtac real_less_or_eq_imp_le, dtac real_le_imp_less_or_eq]);
by (auto_tac (claset() addIs [real_mult_less_mono1],simpset()));
qed "real_mult_le_less_mono1";
-Goal "[| 0r<=z; x<y |] ==> z*x<=z*y";
+Goal "[| (0::real) <= z; x < y |] ==> z*x <= z*y";
by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_le_less_mono1]) 1);
qed "real_mult_le_less_mono2";
-Goal "[| 0r<=z; x<=y |] ==> z*x<=z*y";
+Goal "[| (0::real) <= z; x <= y |] ==> z*x <= z*y";
by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1);
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 "[| (0::real) < r1; r1 < r2; 0 < 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 [("R1.0","0")] real_less_trans 2);
by (dres_inst_tac [("x","r1")] real_mult_less_mono1 3);
by Auto_tac;
by (blast_tac (claset() addIs [real_less_trans]) 1);
qed "real_mult_less_mono";
-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);
+Goal "[| (0::real) < r1; r1 < r2; 0 < y|] ==> 0 < r2 * y";
+by (rtac real_mult_order 1);
+by (assume_tac 2);
+by (blast_tac (claset() addIs [real_less_trans]) 1);
qed "real_mult_order_trans";
-Goal "[| 0r < r1; r1 <r2; 0r <= x; x < y|] ==> r1 * x < r2 * y";
+Goal "[| (0::real) < r1; r1 < r2; 0 <= 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 "[| (0::real) <= r1; r1 < r2; 0 <= 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],
@@ -497,7 +555,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 "[| (0::real) < r1; r1 <= r2; 0 <= 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,
@@ -505,7 +563,7 @@
simpset()));
qed "real_mult_le_mono";
-Goal "[| 0r < r1; r1 < r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y";
+Goal "[| (0::real) < r1; r1 < r2; 0 <= 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,
@@ -513,20 +571,20 @@
simpset()));
qed "real_mult_le_mono2";
-Goal "[| 0r <= r1; r1 < r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y";
+Goal "[| (0::real) <= r1; r1 < r2; 0 <= 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 "[| (0::real) <= r1; r1 <= r2; 0 <= 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()));
qed "real_mult_le_mono4";
-Goal "1r <= x ==> 0r < x";
+Goal "1r <= x ==> 0 < x";
by (rtac ccontr 1 THEN dtac real_leI 1);
by (dtac real_le_trans 1 THEN assume_tac 1);
by (auto_tac (claset() addDs [real_zero_less_one RSN (2,real_le_less_trans)],
@@ -562,8 +620,7 @@
qed "real_gt_half_sum";
Goal "x < y ==> EX r::real. x < r & r < y";
-by (blast_tac (claset() addSIs [real_less_half_sum,
- real_gt_half_sum]) 1);
+by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1);
qed "real_dense";
Goal "(EX n. rinv(real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)";
@@ -603,7 +660,7 @@
Addsimps [real_of_posnat_less_iff];
-Goal "0r < u ==> (u < rinv (real_of_posnat n)) = (real_of_posnat n < rinv(u))";
+Goal "0 < u ==> (u < rinv (real_of_posnat n)) = (real_of_posnat n < rinv(u))";
by (Step_tac 1);
by (res_inst_tac [("n2","n")] (real_of_posnat_less_zero RS
real_rinv_gt_zero RS real_mult_less_cancel1) 1);
@@ -620,13 +677,13 @@
real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
qed "real_of_posnat_less_rinv_iff";
-Goal "0r < u ==> (u = rinv(real_of_posnat n)) = (real_of_posnat n = rinv u)";
+Goal "0 < u ==> (u = rinv(real_of_posnat n)) = (real_of_posnat n = rinv u)";
by (auto_tac (claset(),
simpset() addsimps [real_rinv_rinv,
real_of_posnat_less_zero,real_not_refl2 RS not_sym]));
qed "real_of_posnat_rinv_eq_iff";
-Goal "[| 0r < r; r < x |] ==> rinv x < rinv r";
+Goal "[| 0 < r; r < x |] ==> rinv x < rinv r";
by (ftac real_less_trans 1 THEN assume_tac 1);
by (ftac real_rinv_gt_zero 1);
by (forw_inst_tac [("x","x")] real_rinv_gt_zero 1);
@@ -641,7 +698,7 @@
not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1);
qed "real_rinv_less_swap";
-Goal "[| 0r < r; 0r < x|] ==> (r < x) = (rinv x < rinv r)";
+Goal "[| 0 < r; 0 < x|] ==> (r < x) = (rinv x < rinv r)";
by (auto_tac (claset() addIs [real_rinv_less_swap],simpset()));
by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1);
by (etac (real_not_refl2 RS not_sym) 1);
@@ -676,7 +733,7 @@
qed "real_add_minus_rinv_real_of_posnat_le";
Addsimps [real_add_minus_rinv_real_of_posnat_le];
-Goal "0r < r ==> r*(1r + (-rinv(real_of_posnat n))) < r";
+Goal "0 < r ==> r*(1r + (-rinv(real_of_posnat n))) < r";
by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
by (auto_tac (claset() addIs [real_mult_order],
@@ -685,44 +742,43 @@
real_minus_zero_less_iff2]));
qed "real_mult_less_self";
-Goal "0r <= 1r + (-rinv(real_of_posnat n))";
+Goal "0 <= 1r + (-rinv(real_of_posnat n))";
by (res_inst_tac [("C","rinv(real_of_posnat n)")] real_le_add_right_cancel 1);
by (simp_tac (simpset() addsimps [real_add_assoc,
real_of_posnat_rinv_le_iff]) 1);
qed "real_add_one_minus_rinv_ge_zero";
-Goal "0r < r ==> 0r <= r*(1r + (-rinv(real_of_posnat n)))";
+Goal "0 < r ==> 0 <= r*(1r + (-rinv(real_of_posnat n)))";
by (dtac (real_add_one_minus_rinv_ge_zero RS real_mult_le_less_mono1) 1);
by Auto_tac;
qed "real_mult_add_one_minus_ge_zero";
-Goal "x*y = 0r ==> x = 0r | y = 0r";
-by (auto_tac (claset() addIs [ccontr] addDs [real_mult_not_zero],
- simpset()));
-qed "real_mult_zero_disj";
-
-Goal "x + x*y = x*(1r + y)";
-by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
-qed "real_add_mult_distrib_one";
+Goal "(x*y = 0) = (x = 0 | y = (0::real))";
+by Auto_tac;
+by (blast_tac (claset() addIs [ccontr] addDs [real_mult_not_zero]) 1);
+qed "real_mult_is_0";
-Goal "[| x ~= 1r; y * x = y |] ==> y = 0r";
-by (dtac (sym RS (real_eq_minus_iff RS iffD1)) 1);
-by (dtac sym 1);
-by (asm_full_simp_tac (simpset() addsimps [real_minus_mult_eq2,
- real_add_mult_distrib_one]) 1);
-by (dtac real_mult_zero_disj 1);
+Goal "(0 = x*y) = (0 = x | (0::real) = y)";
+by (stac eq_commute 1 THEN stac real_mult_is_0 1);
+by Auto_tac;
+qed "real_0_is_mult";
+AddIffs [real_mult_is_0, real_0_is_mult];
+
+Goal "[| x ~= 1r; y * x = y |] ==> y = 0";
+by (subgoal_tac "y*(1r + -x) = 0" 1);
+by (stac real_add_mult_distrib2 2);
by (auto_tac (claset(),
simpset() addsimps [real_eq_minus_iff2 RS sym]));
qed "real_mult_eq_self_zero";
Addsimps [real_mult_eq_self_zero];
-Goal "[| x ~= 1r; y = y * x |] ==> y = 0r";
+Goal "[| x ~= 1r; y = y * x |] ==> y = 0";
by (dtac sym 1);
by (Asm_full_simp_tac 1);
qed "real_mult_eq_self_zero2";
Addsimps [real_mult_eq_self_zero2];
-Goal "[| 0r <= x*y; 0r < x |] ==> 0r <= y";
+Goal "[| 0 <= x*y; 0 < x |] ==> (0::real) <= y";
by (ftac real_rinv_gt_zero 1);
by (dres_inst_tac [("x","rinv x")] real_less_le_mult_order 1);
by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2);
@@ -730,7 +786,7 @@
simpset() addsimps [real_mult_assoc RS sym]));
qed "real_mult_ge_zero_cancel";
-Goal "[|x ~= 0r; y ~= 0r |] ==> rinv(x) + rinv(y) = (x + y)*rinv(x*y)";
+Goal "[|x ~= 0; y ~= 0 |] ==> rinv(x) + rinv(y) = (x + y)*rinv(x*y)";
by (asm_full_simp_tac (simpset() addsimps
[real_rinv_distrib,real_add_mult_distrib,
real_mult_assoc RS sym]) 1);
@@ -740,37 +796,74 @@
qed "real_rinv_add";
(* 05/00 *)
-Goal "(0r <= -R) = (R <= 0r)";
+Goal "(0 <= -R) = (R <= (0::real))";
by (auto_tac (claset() addDs [sym],
simpset() addsimps [real_le_less]));
qed "real_minus_zero_le_iff";
-Goal "(-R <= 0r) = (0r <= R)";
+Goal "(-R <= 0) = ((0::real) <= R)";
by (auto_tac (claset(),simpset() addsimps
[real_minus_zero_less_iff2,real_le_less]));
qed "real_minus_zero_le_iff2";
-Goal "-(x*x) <= 0r";
+Goal "-(x*x) <= (0::real)";
by (simp_tac (simpset() addsimps [real_minus_zero_le_iff2]) 1);
qed "real_minus_squre_le_zero";
Addsimps [real_minus_squre_le_zero];
-Goal "x * x + y * y = 0r ==> x = 0r";
+Goal "x * x + y * y = 0 ==> x = (0::real)";
by (dtac real_add_minus_eq_minus 1);
by (cut_inst_tac [("x","x")] real_le_square 1);
by (Auto_tac THEN dtac real_le_anti_sym 1);
-by (auto_tac (claset() addDs [real_mult_zero_disj],simpset()));
+by Auto_tac;
qed "real_sum_squares_cancel";
-Goal "x * x + y * y = 0r ==> y = 0r";
+Goal "x * x + y * y = 0 ==> y = (0::real)";
by (res_inst_tac [("y","x")] real_sum_squares_cancel 1);
by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
qed "real_sum_squares_cancel2";
(*----------------------------------------------------------------------------
+ Some convenient biconditionals for products of signs (lcp)
+ ----------------------------------------------------------------------------*)
+
+Goal "((0::real) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, real_less_le_iff,
+ real_mult_order, real_mult_less_zero1]));
+by (ALLGOALS (rtac ccontr));
+by (auto_tac (claset(), simpset() addsimps [order_le_less, real_less_le_iff]));
+by (ALLGOALS (etac rev_mp));
+by (ALLGOALS (dtac real_mult_less_zero THEN' assume_tac));
+by (auto_tac (claset() addDs [order_less_not_sym],
+ simpset() addsimps [real_mult_commute]));
+qed "real_zero_less_times_iff";
+
+Goal "((0::real) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, real_less_le_iff,
+ real_zero_less_times_iff]));
+qed "real_zero_le_times_iff";
+
+Goal "(x*y < (0::real)) = (0 < x & y < 0 | x < 0 & 0 < y)";
+by (auto_tac (claset(),
+ simpset() addsimps [real_zero_le_times_iff,
+ linorder_not_le RS sym]));
+by (auto_tac (claset() addDs [order_less_not_sym],
+ simpset() addsimps [linorder_not_le]));
+qed "real_times_less_zero_iff";
+
+Goal "(x*y <= (0::real)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)";
+by (auto_tac (claset() addDs [order_less_not_sym],
+ simpset() addsimps [real_zero_less_times_iff,
+ linorder_not_less RS sym]));
+qed "real_times_le_zero_iff";
+
+
+(*----------------------------------------------------------------------------
Another embedding of the naturals in the reals (see real_of_posnat)
----------------------------------------------------------------------------*)
-Goalw [real_of_nat_def] "real_of_nat 0 = 0r";
+Goalw [real_of_nat_def] "real_of_nat 0 = 0";
by (full_simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
qed "real_of_nat_zero";
@@ -801,7 +894,7 @@
simpset() addsimps [real_of_nat_def,real_add_right_cancel]));
qed "inj_real_of_nat";
-Goalw [real_of_nat_def] "0r <= real_of_nat n";
+Goalw [real_of_nat_def] "0 <= real_of_nat n";
by (res_inst_tac [("C","1r")] real_le_add_right_cancel 1);
by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
qed "real_of_nat_ge_zero";
@@ -844,7 +937,7 @@
by (etac real_of_nat_minus 1);
qed "real_of_nat_diff2";
-Goal "(real_of_nat n ~= 0r) = (n ~= 0)";
+Goal "(real_of_nat n ~= 0) = (n ~= 0)";
by (auto_tac (claset() addIs [inj_real_of_nat RS injD],
simpset() addsimps [real_of_nat_zero RS sym]
delsimps [neq0_conv]));
--- a/src/HOL/Real/RealOrd.thy Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealOrd.thy Wed Jun 07 12:14:18 2000 +0200
@@ -2,7 +2,8 @@
ID: $Id$
Author: Jacques D. Fleuriot and Lawrence C. Paulson
Copyright: 1998 University of Cambridge
- Description: Type "real" is a linear order
+ Description: Type "real" is a linear order and also
+ satisfies plus_ac0: + is an AC-operator with zero
*)
RealOrd = RealDef +
@@ -10,4 +11,6 @@
instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
instance real :: linorder (real_le_linear)
+instance real :: plus_ac0 (real_add_commute,real_add_assoc,real_add_zero_left)
+
end
--- a/src/HOL/Real/RealPow.ML Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealPow.ML Wed Jun 07 12:14:18 2000 +0200
@@ -12,13 +12,12 @@
Goal "r ~= (#0::real) --> r ^ n ~= #0";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [real_mult_not_zeroE],
- simpset() addsimps [real_zero_not_eq_one RS not_sym]));
+by Auto_tac;
qed_spec_mp "realpow_not_zero";
Goal "r ^ n = (#0::real) ==> r = #0";
by (rtac ccontr 1);
-by (auto_tac (claset() addDs [realpow_not_zero],simpset()));
+by (auto_tac (claset() addDs [realpow_not_zero], simpset()));
qed "realpow_zero_zero";
Goal "r ~= #0 --> rinv(r ^ n) = (rinv r) ^ n";
@@ -383,65 +382,57 @@
goalw RealPow.thy [real_diff_def]
"((x::real) ^ 2 = y ^ 2) = (x = y | x = -y)";
by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
-by (dtac (rename_numerals thy ((real_eq_minus_iff RS iffD1)
- RS sym)) 1);
-by (auto_tac (claset() addSDs [full_rename_numerals thy
- real_mult_zero_disj] addDs [full_rename_numerals thy
- real_add_minus_eq_minus], simpset() addsimps
- [realpow_two_add_minus] delsimps [realpow_Suc]));
+by (dtac (rename_numerals thy (real_eq_minus_iff RS iffD1 RS sym)) 1);
+by (auto_tac (claset() addDs [full_rename_numerals thy real_add_minus_eq_minus],
+ simpset() addsimps [realpow_two_add_minus] delsimps [realpow_Suc]));
qed "realpow_two_disj";
(* used in Transc *)
-Goal "!!x. [|x ~= #0; m <= n |] ==> \
-\ x ^ (n - m) = x ^ n * rinv(x ^ m)";
-by (auto_tac (claset(),simpset() addsimps [le_eq_less_or_eq,
- less_iff_Suc_add,realpow_add,
- realpow_not_zero] @ real_mult_ac));
+Goal "[|x ~= #0; m <= n |] ==> x ^ (n - m) = x ^ n * rinv(x ^ m)";
+by (auto_tac (claset(),
+ simpset() addsimps [le_eq_less_or_eq,
+ less_iff_Suc_add,realpow_add,
+ realpow_not_zero] @ real_mult_ac));
qed "realpow_diff";
Goal "real_of_nat (m) ^ n = real_of_nat (m ^ n)";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [real_of_nat_one,
- real_of_nat_mult]));
+by (auto_tac (claset(),
+ simpset() addsimps [real_of_nat_one, real_of_nat_mult]));
qed "realpow_real_of_nat";
Goal "#0 < real_of_nat (2 ^ n)";
by (induct_tac "n" 1);
by (auto_tac (claset() addSIs [full_rename_numerals thy real_mult_order],
- simpset() addsimps [real_of_nat_mult RS sym,real_of_nat_one]));
+ simpset() addsimps [real_of_nat_mult RS sym,real_of_nat_one]));
by (simp_tac (simpset() addsimps [rename_numerals thy
- (real_of_nat_zero RS sym)]) 1);
+ (real_of_nat_zero RS sym)]) 1);
qed "realpow_real_of_nat_two_pos";
Addsimps [realpow_real_of_nat_two_pos];
-(* FIXME: annoyingly long proof! *)
+
+
+
+(*** REALORD.ML, AFTER real_rinv_less_iff ***)
+Goal "[| 0 < r; 0 < x|] ==> (rinv x <= rinv r) = (r <= x)";
+by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
+ real_rinv_less_iff]) 1);
+qed "real_rinv_le_iff";
+
Goal "(#0::real) <= x & #0 <= y & x ^ Suc n <= y ^ Suc n --> x <= y";
by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
by (dtac not_real_leE 1);
-by (auto_tac (claset() addDs [real_less_asym],
- simpset() addsimps [real_le_less]));
-by (forw_inst_tac [("r","y")]
- (full_rename_numerals thy real_rinv_less_swap) 1);
-by (rtac real_linear_less2 2);
-by (rtac real_linear_less2 5);
-by (dtac (full_rename_numerals thy
- ((real_not_refl2 RS not_sym) RS real_mult_not_zero)) 9);
-by (Auto_tac);
-by (forw_inst_tac [("t","#0")] (real_not_refl2 RS not_sym) 1);
-by (forward_tac [full_rename_numerals thy real_rinv_gt_zero] 1);
-by (forw_inst_tac [("t","#0")] (real_not_refl2 RS not_sym) 3);
-by (dtac (full_rename_numerals thy real_rinv_gt_zero) 3);
-by (dtac (full_rename_numerals thy real_mult_less_zero) 3);
-by (forw_inst_tac [("x","(y * y ^ n)"),("r1.0","y")]
- (full_rename_numerals thy real_mult_less_mono) 2);
-by (dres_inst_tac [("x","x * (x * x ^ n)"),("r1.0","rinv x")]
- (full_rename_numerals thy real_mult_less_mono) 1);
-by (Auto_tac);
-by (auto_tac (claset() addIs (map (full_rename_numerals thy )
- [real_mult_order,realpow_gt_zero]),
- simpset() addsimps [real_mult_assoc
- RS sym,real_not_refl2 RS not_sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [inst "x" "#0" order_le_less,
+ real_times_le_0_iff]));
+by (subgoal_tac "rinv x * (x * (x * x ^ n)) <= rinv y * (y * (y * y ^ n))" 1);
+by (rtac real_mult_le_mono 2);
+by (asm_full_simp_tac (simpset() addsimps [realpow_ge_zero, real_0_le_times_iff]) 4);
+by (asm_full_simp_tac (simpset() addsimps [real_rinv_le_iff]) 3);
+by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
+by (rtac real_rinv_gt_zero 1);
+by Auto_tac;
qed_spec_mp "realpow_increasing";
Goal "(#0::real) <= x & #0 <= y & x ^ Suc n = y ^ Suc n --> x = y";