# HG changeset patch # User paulson # Date 960372858 -7200 # Node ID ca761fe227d8572d3edd04e04668d063e570a649 # Parent 4d4521cbbcca2ef61cdd92071f51c5bfee364636 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. diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/HahnBanach/Aux.thy --- 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 diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/Hyperreal/HyperDef.ML --- 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"; diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/PNat.ML --- 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"; diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/PRat.ML --- 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])); diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/PReal.ML --- 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])); diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/RComplete.ML --- 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); diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/ROOT.ML --- 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"; diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/RealAbs.ML --- 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); diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/RealBin.ML --- 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]; + diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/RealDef.ML --- 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 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)))" diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/RealInt.ML --- 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"; diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/RealOrd.ML --- 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 x*z 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 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 x 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 x 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 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 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 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 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 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 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 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 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])); diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/RealOrd.thy --- 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 diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/RealPow.ML --- 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";