# HG changeset patch # User paulson # Date 1072990027 -3600 # Node ID 9c0b5e081037edd90a8117dcc6a7cf0223c00cd5 # Parent 6137d24eef7911d2e951da6956e4728cf8ec9b76 conversion of Real/PReal to Isar script; type "complex" is now in class "field" diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Complex/CLim.ML --- a/src/HOL/Complex/CLim.ML Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Complex/CLim.ML Thu Jan 01 21:47:07 2004 +0100 @@ -5,9 +5,9 @@ differentiation for complex functions *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Limit of complex to complex function *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) Goalw [NSCLIM_def,NSCRLIM_def] "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)"; @@ -106,9 +106,9 @@ by (blast_tac (claset() addIs [CLIM_NSCLIM,NSCLIM_CLIM]) 1); qed "CLIM_NSCLIM_iff"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Limit of complex to real function *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) Goalw [CRLIM_def,NSCRLIM_def,capprox_def] "f -- x --CR> L ==> f -- x --NSCR> L"; @@ -409,9 +409,9 @@ qed "CLIM_CRLIM_Re_Im_iff"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Continuity *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) Goalw [isNSContc_def] "[| isNSContc f a; y @c= hcomplex_of_complex a |] \ @@ -552,9 +552,9 @@ Addsimps [isNSContc_const]; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* functions from complex to reals *) -(* -----------------------------------------------------------------------------------*) +(* ----------------------------------------------------------------------*) Goalw [isNSContCR_def] "[| isNSContCR f a; y @c= hcomplex_of_complex a |] \ @@ -619,9 +619,9 @@ by (etac CLIM_CRLIM_Im 1); qed "isContc_isContCR_Im"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Derivatives *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) Goalw [cderiv_def] "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"; @@ -661,9 +661,9 @@ qed "NSCDeriv_unique"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Differentiability *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) Goalw [cdifferentiable_def] "f cdifferentiable x ==> EX D. CDERIV f x :> D"; @@ -686,9 +686,9 @@ qed "NSCdifferentiableI"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Alternative definition for differentiability *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) Goalw [CLIM_def] "((%h. (f(a + h) - f(a))/h) -- 0 --C> D) = \ @@ -710,9 +710,9 @@ qed "CDERIV_iff2"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Equivalence of NS and standard defs of differentiation *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (*** first equivalence ***) Goalw [nscderiv_def,NSCLIM_def] @@ -767,10 +767,10 @@ isNSContc_isContc_iff RS sym,NSCDERIV_isNSContc]) 1); qed "CDERIV_isContc"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Differentiation rules for combinations of functions follow from clear, *) (* straightforard, algebraic manipulations *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* use simple constant nslimit theorem *) Goal "(NSCDERIV (%x. k) x :> 0)"; @@ -791,7 +791,7 @@ simpset() addsimps [hcomplex_add_divide_distrib,hcomplex_diff_def])); by (dres_inst_tac [("b","hcomplex_of_complex Da"), ("d","hcomplex_of_complex Db")] capprox_add 1); -by (auto_tac (claset(), simpset() addsimps hcomplex_add_ac)); +by (auto_tac (claset(), simpset() addsimps add_ac)); qed "NSCDERIV_add"; Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \ @@ -803,7 +803,7 @@ (*** lemmas for multiplication ***) Goal "((a::hcomplex)*b) - (c*d) = (b*(a - c)) + (c*(b - d))"; -by (simp_tac (simpset() addsimps [hcomplex_diff_mult_distrib2]) 1); +by (simp_tac (simpset() addsimps [right_diff_distrib]) 1); val lemma_nscderiv1 = result(); Goal "[| (x + y) / z = hcomplex_of_complex D + yb; z ~= 0; \ @@ -833,7 +833,7 @@ by (dres_inst_tac [("D","Db")] lemma_nscderiv2 1); by (dtac (capprox_minus_iff RS iffD2 RS (bex_CInfinitesimal_iff2 RS iffD2)) 4); by (auto_tac (claset() addSIs [capprox_add_mono1], - simpset() addsimps [hcomplex_add_mult_distrib, hcomplex_add_mult_distrib2, + simpset() addsimps [hcomplex_add_mult_distrib, right_distrib, hcomplex_mult_commute, hcomplex_add_assoc])); by (res_inst_tac [("w1","hcomplex_of_complex Db * hcomplex_of_complex (f x)")] (hcomplex_add_commute RS subst) 1); @@ -855,7 +855,10 @@ (simpset() addsimps [complex_times_divide1_eq RS sym, NSCDERIV_NSCLIM_iff, complex_minus_mult_eq2, complex_add_mult_distrib2 RS sym, complex_diff_def] - delsimps [complex_times_divide1_eq, complex_minus_mult_eq2 RS sym]) 1); + delsimps [complex_times_divide1_eq, complex_minus_mult_eq2 RS sym] + delsimps [times_divide_eq_right, minus_mult_right RS sym] + +) 1); by (etac (NSCLIM_const RS NSCLIM_mult) 1); qed "NSCDERIV_cmult"; @@ -868,7 +871,10 @@ by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,complex_diff_def]) 1); by (res_inst_tac [("t","f x")] (complex_minus_minus RS subst) 1); by (asm_simp_tac (simpset() addsimps [complex_minus_add_distrib RS sym] - delsimps [complex_minus_add_distrib, complex_minus_minus]) 1); + delsimps [complex_minus_add_distrib, complex_minus_minus] + delsimps [minus_add_distrib, minus_minus] + +) 1); by (etac NSCLIM_minus 1); qed "NSCDERIV_minus"; @@ -995,9 +1001,9 @@ by (auto_tac (claset() addDs [CDERIV_chain], simpset() addsimps [o_def])); qed "CDERIV_chain2"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Differentiation of natural number powers *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) Goal "NSCDERIV (%x. x) x :> 1"; by (auto_tac (claset(), @@ -1029,7 +1035,8 @@ by (dtac (CDERIV_Id RS CDERIV_mult) 2); by (auto_tac (claset(), simpset() addsimps [complex_of_real_add RS sym, - complex_add_mult_distrib,real_of_nat_Suc] delsimps [complex_of_real_add])); + complex_add_mult_distrib,real_of_nat_Suc] + delsimps [complex_of_real_add])); by (case_tac "n" 1); by (auto_tac (claset(), simpset() addsimps [complex_mult_assoc, complex_add_commute])); @@ -1062,24 +1069,19 @@ by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute,numeral_2_eq_2]) 2); by (auto_tac (claset(), simpset() addsimps [starfunC_inverse_inverse,hcomplex_diff_def] - delsimps [minus_mult_right RS sym, minus_mult_left RS sym, - hcomplex_minus_mult_eq1 RS sym, - hcomplex_minus_mult_eq2 RS sym])); + delsimps [minus_mult_left RS sym, minus_mult_right RS sym])); by (asm_simp_tac (simpset() addsimps [inverse_add, - inverse_mult_distrib RS sym, hcomplex_minus_inverse RS sym] - @ hcomplex_add_ac @ hcomplex_mult_ac + inverse_mult_distrib RS sym, inverse_minus_eq RS sym] + @ add_ac @ mult_ac delsimps [inverse_minus_eq, - inverse_mult_distrib, minus_mult_right RS sym, minus_mult_left RS sym, - hcomplex_minus_mult_eq1 RS sym, - hcomplex_minus_mult_eq2 RS sym] ) 1); -by (asm_simp_tac (HOL_ss addsimps [hcomplex_mult_assoc RS sym, - hcomplex_add_mult_distrib2]) 1); + inverse_mult_distrib, minus_mult_right RS sym, minus_mult_left RS sym] ) 1); +by (asm_simp_tac (HOL_ss addsimps [mult_assoc RS sym, right_distrib]) 1); by (res_inst_tac [("y"," inverse(- hcomplex_of_complex x * hcomplex_of_complex x)")] capprox_trans 1); by (rtac inverse_add_CInfinitesimal_capprox2 1); by (auto_tac (claset() addSDs [hcomplex_of_complex_CFinite_diff_CInfinitesimal] addIs [CFinite_mult], - simpset() addsimps [hcomplex_minus_inverse RS sym])); + simpset() addsimps [inverse_minus_eq RS sym])); by (rtac CInfinitesimal_CFinite_mult2 1); by Auto_tac; qed "NSCDERIV_inverse"; @@ -1090,16 +1092,16 @@ qed "CDERIV_inverse"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Derivative of inverse *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) Goal "[| CDERIV f x :> d; f(x) ~= 0 |] \ \ ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"; by (rtac (complex_mult_commute RS subst) 1); by (asm_simp_tac (simpset() addsimps [complex_minus_mult_eq1, - complexpow_inverse] delsimps [complexpow_Suc, - complex_minus_mult_eq1 RS sym]) 1); + complexpow_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym, +complex_minus_mult_eq1 RS sym]) 1); by (fold_goals_tac [o_def]); by (blast_tac (claset() addSIs [CDERIV_chain,CDERIV_inverse]) 1); qed "CDERIV_inverse_fun"; @@ -1110,9 +1112,9 @@ CDERIV_inverse_fun] delsimps [complexpow_Suc]) 1); qed "NSCDERIV_inverse_fun"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Derivative of quotient *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) Goal "x ~= (0::complex) \\ (x * inverse(x) ^ 2) = inverse x"; @@ -1129,8 +1131,7 @@ by (asm_full_simp_tac (simpset() addsimps [complex_divide_def, complex_add_mult_distrib2, complexpow_inverse,complex_minus_mult_eq1] @ complex_mult_ac - delsimps [complexpow_Suc, complex_minus_mult_eq1 RS sym, - complex_minus_mult_eq2 RS sym]) 1); + delsimps [complexpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1); qed "CDERIV_quotient"; Goal "[| NSCDERIV f x :> d; NSCDERIV g x :> e; g(x) ~= 0 |] \ @@ -1140,9 +1141,9 @@ qed "NSCDERIV_quotient"; -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) (* Caratheodory formulation of derivative at a point: standard proof *) -(*------------------------------------------------------------------------------------*) +(*-----------------------------------------------------------------------*) Goalw [CLIM_def] diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Complex/Complex.thy --- a/src/HOL/Complex/Complex.thy Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Complex/Complex.thy Thu Jan 01 21:47:07 2004 +0100 @@ -483,28 +483,6 @@ apply (auto simp add: complex_mult complex_minus real_diff_def) done -declare complex_minus_mult_eq1 [symmetric, simp] complex_minus_mult_eq2 [symmetric, simp] - -lemma complex_mult_minus_one: "-(1::complex) * z = -z" -apply (simp (no_asm)) -done -declare complex_mult_minus_one [simp] - -lemma complex_mult_minus_one_right: "z * -(1::complex) = -z" -apply (subst complex_mult_commute) -apply (simp (no_asm)) -done -declare complex_mult_minus_one_right [simp] - -lemma complex_minus_mult_cancel: "-x * -y = x * (y::complex)" -apply (simp (no_asm)) -done -declare complex_minus_mult_cancel [simp] - -lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)" -apply (simp (no_asm)) -done - lemma complex_add_mult_distrib: "((z1::complex) + z2) * w = (z1 * w) + (z2 * w)" apply (rule_tac z = z1 in eq_Abs_complex) apply (rule_tac z = z2 in eq_Abs_complex) @@ -541,6 +519,13 @@ apply (simp (no_asm) add: complex_divide_def COMPLEX_INVERSE_ZERO) done +instance complex :: division_by_zero +proof + fix x :: complex + show "inverse 0 = (0::complex)" by (rule COMPLEX_INVERSE_ZERO) + show "x/0 = 0" by (rule COMPLEX_DIVISION_BY_ZERO) +qed + lemma complex_mult_inv_left: "z ~= (0::complex) ==> inverse(z) * z = 1" apply (rule_tac z = z in eq_Abs_complex) apply (auto simp add: complex_mult complex_inverse complex_one_def @@ -554,6 +539,61 @@ by (auto intro: complex_mult_commute [THEN subst]) declare complex_mult_inv_right [simp] + +subsection {* The field of complex numbers *} + +instance complex :: field +proof + fix z u v w :: complex + show "(u + v) + w = u + (v + w)" + by (rule complex_add_assoc) + show "z + w = w + z" + by (rule complex_add_commute) + show "0 + z = z" + by (rule complex_add_zero_left) + show "-z + z = 0" + by (rule complex_add_minus_left_zero) + show "z - w = z + -w" + by (simp add: complex_diff_def) + show "(u * v) * w = u * (v * w)" + by (rule complex_mult_assoc) + show "z * w = w * z" + by (rule complex_mult_commute) + show "1 * z = z" + by (rule complex_mult_one_left) + show "0 \ (1::complex)" --{*for some reason it has to be early*} + by (rule complex_zero_not_eq_one) + show "(u + v) * w = u * w + v * w" + by (rule complex_add_mult_distrib) + assume neq: "w \ 0" + thus "z / w = z * inverse w" + by (simp add: complex_divide_def) + show "inverse w * w = 1" + by (simp add: neq complex_mult_inv_left) +qed + + +lemma complex_mult_minus_one: "-(1::complex) * z = -z" +apply (simp (no_asm)) +done +declare complex_mult_minus_one [simp] + +lemma complex_mult_minus_one_right: "z * -(1::complex) = -z" +apply (subst complex_mult_commute) +apply (simp (no_asm)) +done +declare complex_mult_minus_one_right [simp] + +lemma complex_minus_mult_cancel: "-x * -y = x * (y::complex)" +apply (simp (no_asm)) +done +declare complex_minus_mult_cancel [simp] + +lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)" +apply (simp (no_asm)) +done + + lemma complex_mult_left_cancel: "(c::complex) ~= 0 ==> (c*a=c*b) = (a=b)" apply auto apply (drule_tac f = "%x. x*inverse c" in arg_cong) @@ -603,11 +643,7 @@ done lemma complex_inverse_distrib: "inverse(x*y) = inverse x * inverse (y::complex)" -apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO) -apply (case_tac "y = 0", simp add: COMPLEX_INVERSE_ZERO) -apply (rule_tac c1 = "x*y" in complex_mult_left_cancel [THEN iffD1]) -apply (auto simp add: complex_mult_not_zero complex_mult_ac) -apply (auto simp add: complex_mult_not_zero complex_mult_assoc [symmetric]) +apply (rule inverse_mult_distrib) done diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Complex/ComplexArith0.ML --- a/src/HOL/Complex/ComplexArith0.ML Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Complex/ComplexArith0.ML Thu Jan 01 21:47:07 2004 +0100 @@ -24,8 +24,6 @@ Goal "(inverse(x::complex) = 0) = (x = 0)"; by (auto_tac (claset(), simpset() addsimps [COMPLEX_INVERSE_ZERO])); -by (rtac ccontr 1); -by (blast_tac (claset() addDs [complex_inverse_not_zero]) 1); qed "complex_inverse_zero_iff"; Addsimps [complex_inverse_zero_iff]; @@ -287,7 +285,6 @@ Goal "(-b = -a) = (b = (a::complex))"; by Auto_tac; -by (etac ( inj_complex_minus RS injD) 1); qed "complex_minus_eq_cancel"; Addsimps [complex_minus_eq_cancel]; diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Complex/NSCA.ML --- a/src/HOL/Complex/NSCA.ML Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Complex/NSCA.ML Thu Jan 01 21:47:07 2004 +0100 @@ -420,9 +420,9 @@ val prem1::prem2::rest = goalw thy [capprox_def,hcomplex_diff_def] "[| a @c= b; c @c= d |] ==> a+c @c= b+d"; -by (rtac (hcomplex_minus_add_distrib RS ssubst) 1); +by (rtac (minus_add_distrib RS ssubst) 1); by (rtac (hcomplex_add_assoc RS ssubst) 1); -by (res_inst_tac [("y1","c")] (hcomplex_add_left_commute RS subst) 1); +by (res_inst_tac [("b1","c")] (add_left_commute RS subst) 1); by (rtac (hcomplex_add_assoc RS subst) 1); by (rtac ([prem1,prem2] MRS CInfinitesimal_add) 1); qed "capprox_add"; @@ -449,7 +449,7 @@ Goalw [capprox_def,hcomplex_diff_def] "[| a @c= b; c: CFinite|] ==> a*c @c= b*c"; by (asm_full_simp_tac (HOL_ss addsimps [CInfinitesimal_CFinite_mult, - hcomplex_minus_mult_eq1,hcomplex_add_mult_distrib RS sym]) 1); + minus_mult_left,hcomplex_add_mult_distrib RS sym]) 1); qed "capprox_mult1"; Goal "[|a @c= b; c: CFinite|] ==> c*a @c= c*b"; @@ -525,8 +525,8 @@ Goal "d + b @c= d + c ==> b @c= c"; by (dtac (capprox_minus_iff RS iffD1) 1); by (asm_full_simp_tac (simpset() addsimps - [hcomplex_minus_add_distrib,capprox_minus_iff RS sym] - @ hcomplex_add_ac) 1); + [minus_add_distrib,capprox_minus_iff RS sym] + @ add_ac) 1); qed "capprox_add_left_cancel"; Goal "b + d @c= c + d ==> b @c= c"; @@ -538,7 +538,7 @@ Goal "b @c= c ==> d + b @c= d + c"; by (rtac (capprox_minus_iff RS iffD2) 1); by (asm_full_simp_tac (simpset() addsimps - [capprox_minus_iff RS sym] @ hcomplex_add_ac) 1); + [capprox_minus_iff RS sym] @ add_ac) 1); qed "capprox_add_mono1"; Goal "b @c= c ==> b + a @c= c + a"; @@ -1223,7 +1223,7 @@ by (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))" 1); by (dtac sym 2 THEN dtac sym 2); by (Asm_full_simp_tac 2); -by (asm_simp_tac (simpset() addsimps hcomplex_add_ac) 1); +by (asm_simp_tac (simpset() addsimps add_ac) 1); by (REPEAT(dtac stc_SComplex 1)); by (dtac SComplex_add 1 THEN assume_tac 1); by (dtac CInfinitesimal_add 1 THEN assume_tac 1); @@ -1268,7 +1268,7 @@ by (forw_inst_tac [("x","ea"),("y","x")] CInfinitesimal_CFinite_mult 2); by (dtac CInfinitesimal_mult 3); by (auto_tac (claset() addIs [CInfinitesimal_add], - simpset() addsimps hcomplex_add_ac @ hcomplex_mult_ac)); + simpset() addsimps add_ac @ mult_ac)); qed "lemma_stc_mult"; Goal "[| x: CFinite; y: CFinite |] \ @@ -1282,7 +1282,7 @@ by (thin_tac "x = stc x + e" 1); by (thin_tac "y = stc y + ea" 1); by (asm_full_simp_tac (simpset() addsimps - [hcomplex_add_mult_distrib,hcomplex_add_mult_distrib2]) 1); + [hcomplex_add_mult_distrib,right_distrib]) 1); by (REPEAT(dtac stc_SComplex 1)); by (full_simp_tac (simpset() addsimps [hcomplex_add_assoc]) 1); by (rtac stc_CInfinitesimal_add_SComplex 1); diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Complex/NSComplex.thy Thu Jan 01 21:47:07 2004 +0100 @@ -6,12 +6,38 @@ theory NSComplex = NSInduct: +(*for Ring_and_Field?*) +declare field_mult_eq_0_iff [simp] + (* Move to one of the hyperreal theories *) lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})" apply (induct_tac "m") apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc) done +(* not proved already? strange! *) +lemma hypreal_of_nat_le_iff: + "(hypreal_of_nat n <= hypreal_of_nat m) = (n <= m)" +apply (unfold hypreal_le_def) +apply auto +done +declare hypreal_of_nat_le_iff [simp] + +lemma hypreal_of_nat_ge_zero: "0 <= hypreal_of_nat n" +apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] + del: hypreal_of_nat_zero) +done +declare hypreal_of_nat_ge_zero [simp] + +declare hypreal_of_nat_ge_zero [THEN hrabs_eqI1, simp] + +lemma hypreal_of_hypnat_ge_zero: "0 <= hypreal_of_hypnat n" +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (simp (no_asm_simp) add: hypreal_of_hypnat hypreal_zero_num hypreal_le) +done +declare hypreal_of_hypnat_ge_zero [simp] +declare hypreal_of_hypnat_ge_zero [THEN hrabs_eqI1, simp] + constdefs hcomplexrel :: "((nat=>complex)*(nat=>complex)) set" "hcomplexrel == {p. EX X Y. p = ((X::nat=>complex),Y) & @@ -232,7 +258,8 @@ apply (auto , ultra) done -lemma hcomplex_hRe_hIm_cancel_iff: "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" +lemma hcomplex_hRe_hIm_cancel_iff: + "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" apply (rule_tac z = "z" in eq_Abs_hcomplex) apply (rule_tac z = "w" in eq_Abs_hcomplex) apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff) @@ -293,34 +320,22 @@ Abs_hcomplex(hcomplexrel``{%n. X n + Y n})" apply (unfold hcomplex_add_def) apply (rule_tac f = "Abs_hcomplex" in arg_cong) -apply auto -apply (ultra) +apply (auto, ultra) done lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z" apply (rule_tac z = "z" in eq_Abs_hcomplex) apply (rule_tac z = "w" in eq_Abs_hcomplex) -apply (simp (no_asm_simp) add: complex_add_commute hcomplex_add) +apply (simp add: complex_add_commute hcomplex_add) done lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)" apply (rule_tac z = "z1" in eq_Abs_hcomplex) apply (rule_tac z = "z2" in eq_Abs_hcomplex) apply (rule_tac z = "z3" in eq_Abs_hcomplex) -apply (simp (no_asm_simp) add: hcomplex_add complex_add_assoc) +apply (simp add: hcomplex_add complex_add_assoc) done -(*For AC rewriting*) -lemma hcomplex_add_left_commute: "(x::hcomplex)+(y+z)=y+(x+z)" -apply (rule hcomplex_add_commute [THEN trans]) -apply (rule hcomplex_add_assoc [THEN trans]) -apply (rule hcomplex_add_commute [THEN arg_cong]) -done - -(* hcomplex addition is an AC operator *) -lemmas hcomplex_add_ac = hcomplex_add_assoc hcomplex_add_commute - hcomplex_add_left_commute - lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z" apply (unfold hcomplex_zero_def) apply (rule_tac z = "z" in eq_Abs_hcomplex) @@ -328,9 +343,8 @@ done lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z" -apply (simp (no_asm) add: hcomplex_add_zero_left hcomplex_add_commute) +apply (simp add: hcomplex_add_zero_left hcomplex_add_commute) done -declare hcomplex_add_zero_left [simp] hcomplex_add_zero_right [simp] lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)" apply (rule_tac z = "x" in eq_Abs_hcomplex) @@ -350,7 +364,6 @@ lemma hcomplex_minus_congruent: "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})" - apply (unfold congruent_def) apply safe apply (ultra+) @@ -361,24 +374,24 @@ Abs_hcomplex(hcomplexrel `` {%n. -(X n)})" apply (unfold hcomplex_minus_def) apply (rule_tac f = "Abs_hcomplex" in arg_cong) -apply (auto , ultra) +apply (auto, ultra) done lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)" apply (rule_tac z = "z" in eq_Abs_hcomplex) apply (auto simp add: hcomplex_add hcomplex_minus hcomplex_zero_def) done -declare hcomplex_add_minus_left [simp] + subsection{*Multiplication for Nonstandard Complex Numbers*} lemma hcomplex_mult: - "Abs_hcomplex(hcomplexrel``{%n. X n}) * Abs_hcomplex(hcomplexrel``{%n. Y n}) = + "Abs_hcomplex(hcomplexrel``{%n. X n}) * + Abs_hcomplex(hcomplexrel``{%n. Y n}) = Abs_hcomplex(hcomplexrel``{%n. X n * Y n})" - apply (unfold hcomplex_mult_def) apply (rule_tac f = "Abs_hcomplex" in arg_cong) -apply (auto , ultra) +apply (auto, ultra) done lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w" @@ -399,16 +412,15 @@ apply (rule_tac z = "z" in eq_Abs_hcomplex) apply (auto simp add: hcomplex_mult) done -declare hcomplex_mult_one_left [simp] lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0" apply (unfold hcomplex_zero_def) apply (rule_tac z = "z" in eq_Abs_hcomplex) apply (auto simp add: hcomplex_mult) done -declare hcomplex_mult_zero_left [simp] -lemma hcomplex_add_mult_distrib: "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)" +lemma hcomplex_add_mult_distrib: + "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)" apply (rule_tac z = "z1" in eq_Abs_hcomplex) apply (rule_tac z = "z2" in eq_Abs_hcomplex) apply (rule_tac z = "w" in eq_Abs_hcomplex) @@ -430,7 +442,7 @@ Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})" apply (unfold hcinv_def) apply (rule_tac f = "Abs_hcomplex" in arg_cong) -apply (auto , ultra) +apply (auto, ultra) done lemma hcomplex_mult_inv_left: @@ -443,7 +455,6 @@ apply (drule complex_mult_inv_left) apply auto done -declare hcomplex_mult_inv_left [simp] subsection {* The Field of Nonstandard Complex Numbers *} @@ -455,9 +466,9 @@ show "z + w = w + z" by (simp add: hcomplex_add_commute) show "0 + z = z" - by (simp) + by (simp add: hcomplex_add_zero_left) show "-z + z = 0" - by (simp) + by (simp add: hcomplex_add_minus_left) show "z - w = z + -w" by (simp add: hcomplex_diff_def) show "(u * v) * w = u * (v * w)" @@ -465,7 +476,7 @@ show "z * w = w * z" by (simp add: hcomplex_mult_commute) show "1 * z = z" - by (simp) + by (simp add: hcomplex_mult_one_left) show "0 \ (1::hcomplex)" by (rule hcomplex_zero_not_eq_one) show "(u + v) * w = u * w + v * w" @@ -478,12 +489,11 @@ qed lemma HCOMPLEX_INVERSE_ZERO: "inverse (0::hcomplex) = 0" -apply (unfold hcomplex_zero_def) -apply (auto simp add: hcomplex_inverse) +apply (simp add: hcomplex_zero_def hcomplex_inverse) done lemma HCOMPLEX_DIVISION_BY_ZERO: "a / (0::hcomplex) = 0" -apply (simp (no_asm) add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO) +apply (simp add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO) done instance hcomplex :: division_by_zero @@ -493,9 +503,6 @@ show "x/0 = 0" by (rule HCOMPLEX_DIVISION_BY_ZERO) qed -lemma hcomplex_mult_left_cancel: "(c::hcomplex) ~= (0::hcomplex) ==> (c*a=c*b) = (a=b)" -by (simp add: field_mult_cancel_left) - subsection{*More Minus Laws*} lemma inj_hcomplex_minus: "inj(%z::hcomplex. -z)" @@ -520,49 +527,13 @@ apply (simp add: minus_equation_iff [of x y]) done -lemma hcomplex_minus_add_distrib: "-(x + y) = -x + -(y::hcomplex)" -apply (rule Ring_and_Field.minus_add_distrib) -done - -lemma hcomplex_add_left_cancel: "((x::hcomplex) + y = x + z) = (y = z)" -apply (rule Ring_and_Field.add_left_cancel) -done -declare hcomplex_add_left_cancel [iff] - -lemma hcomplex_add_right_cancel: "(y + (x::hcomplex)= z + x) = (y = z)" -apply (rule Ring_and_Field.add_right_cancel) -done -declare hcomplex_add_right_cancel [iff] subsection{*More Multiplication Laws*} -lemma hcomplex_mult_left_commute: "(x::hcomplex) * (y * z) = y * (x * z)" -apply (rule Ring_and_Field.mult_left_commute) -done - -lemmas hcomplex_mult_ac = hcomplex_mult_assoc hcomplex_mult_commute - hcomplex_mult_left_commute - lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z" apply (rule Ring_and_Field.mult_1_right) done -lemma hcomplex_mult_zero_right: "z * (0::hcomplex) = 0" -apply (rule Ring_and_Field.mult_right_zero) -done - -lemma hcomplex_minus_mult_eq1: "-(x * y) = -x * (y::hcomplex)" -apply (rule Ring_and_Field.minus_mult_left) -done - -declare hcomplex_minus_mult_eq1 [symmetric, simp] - -lemma hcomplex_minus_mult_eq2: "-(x * y) = x * -(y::hcomplex)" -apply (rule Ring_and_Field.minus_mult_right) -done - -declare hcomplex_minus_mult_eq2 [symmetric, simp] - lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z" apply (simp (no_asm)) done @@ -574,26 +545,13 @@ done declare hcomplex_mult_minus_one_right [simp] -lemma hcomplex_add_mult_distrib2: "(w::hcomplex) * (z1 + z2) = (w * z1) + (w * z2)" -apply (rule Ring_and_Field.right_distrib) -done - -lemma hcomplex_mult_right_cancel: "(c::hcomplex) ~= (0::hcomplex) ==> (a*c=b*c) = (a=b)" -apply (simp add: Ring_and_Field.field_mult_cancel_right); -done +lemma hcomplex_mult_left_cancel: + "(c::hcomplex) ~= (0::hcomplex) ==> (c*a=c*b) = (a=b)" +by (simp add: field_mult_cancel_left) -lemma hcomplex_inverse_not_zero: "z ~= (0::hcomplex) ==> inverse(z) ~= 0" -apply (simp add: ); -done - -lemma hcomplex_mult_not_zero: "[| x ~= (0::hcomplex); y ~= 0 |] ==> x * y ~= 0" -apply (simp add: Ring_and_Field.field_mult_eq_0_iff); -done - -lemmas hcomplex_mult_not_zeroE = hcomplex_mult_not_zero [THEN notE, standard] - -lemma hcomplex_minus_inverse: "inverse(-x) = -inverse(x::hcomplex)" -apply (rule Ring_and_Field.inverse_minus_eq) +lemma hcomplex_mult_right_cancel: + "(c::hcomplex) ~= (0::hcomplex) ==> (a*c=b*c) = (a=b)" +apply (simp add: Ring_and_Field.field_mult_cancel_right); done @@ -633,22 +591,26 @@ apply (auto simp add: hcomplex_of_hypreal) done -lemma hcomplex_of_hypreal_cancel_iff: "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" +lemma hcomplex_of_hypreal_cancel_iff: + "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" apply (auto dest: inj_hcomplex_of_hypreal [THEN injD]) done declare hcomplex_of_hypreal_cancel_iff [iff] -lemma hcomplex_of_hypreal_minus: "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x" +lemma hcomplex_of_hypreal_minus: + "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (auto simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus) done -lemma hcomplex_of_hypreal_inverse: "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)" +lemma hcomplex_of_hypreal_inverse: + "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (auto simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse) done -lemma hcomplex_of_hypreal_add: "hcomplex_of_hypreal x + hcomplex_of_hypreal y = +lemma hcomplex_of_hypreal_add: + "hcomplex_of_hypreal x + hcomplex_of_hypreal y = hcomplex_of_hypreal (x + y)" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (rule_tac z = "y" in eq_Abs_hypreal) @@ -662,18 +624,20 @@ apply (auto simp add: hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def) done -lemma hcomplex_of_hypreal_mult: "hcomplex_of_hypreal x * hcomplex_of_hypreal y = +lemma hcomplex_of_hypreal_mult: + "hcomplex_of_hypreal x * hcomplex_of_hypreal y = hcomplex_of_hypreal (x * y)" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult) +apply (auto simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult + complex_of_real_mult) done lemma hcomplex_of_hypreal_divide: "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)" apply (unfold hcomplex_divide_def) apply (case_tac "y=0") -apply (simp (no_asm_simp) add: HYPREAL_DIVISION_BY_ZERO HYPREAL_INVERSE_ZERO HCOMPLEX_INVERSE_ZERO) +apply (simp) apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric]) apply (simp (no_asm) add: hypreal_divide_def) done @@ -722,7 +686,7 @@ apply (unfold hcmod_def) apply (rule_tac f = "Abs_hypreal" in arg_cong) -apply (auto , ultra) +apply (auto, ultra) done lemma hcmod_zero [simp]: @@ -744,7 +708,8 @@ done declare hcmod_hcomplex_of_hypreal [simp] -lemma hcomplex_of_hypreal_abs: "hcomplex_of_hypreal (abs x) = +lemma hcomplex_of_hypreal_abs: + "hcomplex_of_hypreal (abs x) = hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))" apply (simp (no_asm)) done @@ -757,7 +722,7 @@ Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})" apply (unfold hcnj_def) apply (rule_tac f = "Abs_hcomplex" in arg_cong) -apply (auto , ultra) +apply (auto, ultra) done lemma inj_hcnj: "inj hcnj" @@ -778,7 +743,8 @@ done declare hcomplex_hcnj_hcnj [simp] -lemma hcomplex_hcnj_hcomplex_of_hypreal: "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x" +lemma hcomplex_hcnj_hcomplex_of_hypreal: + "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (auto simp add: hcnj hcomplex_of_hypreal) done @@ -864,42 +830,14 @@ done declare hcomplex_hcnj_zero_iff [iff] -lemma hcomplex_mult_hcnj: "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)" +lemma hcomplex_mult_hcnj: + "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)" apply (rule_tac z = "z" in eq_Abs_hcomplex) apply (auto simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj numeral_2_eq_2) done (*---------------------------------------------------------------------------*) -(* some algebra etc. *) -(*---------------------------------------------------------------------------*) - -lemma hcomplex_mult_zero_iff: "(x*y = (0::hcomplex)) = (x = 0 | y = 0)" -apply auto -apply (auto intro: ccontr dest: hcomplex_mult_not_zero) -done -declare hcomplex_mult_zero_iff [simp] - -lemma hcomplex_add_left_cancel_zero: "(x + y = x) = (y = (0::hcomplex))" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_add hcomplex_zero_def) -done -declare hcomplex_add_left_cancel_zero [simp] - -lemma hcomplex_diff_mult_distrib: - "((z1::hcomplex) - z2) * w = (z1 * w) - (z2 * w)" -apply (unfold hcomplex_diff_def) -apply (simp (no_asm) add: hcomplex_add_mult_distrib) -done - -lemma hcomplex_diff_mult_distrib2: - "(w::hcomplex) * (z1 - z2) = (w * z1) - (w * z2)" -apply (unfold hcomplex_diff_def) -apply (simp (no_asm) add: hcomplex_add_mult_distrib2) -done - -(*---------------------------------------------------------------------------*) (* More theorems about hcmod *) (*---------------------------------------------------------------------------*) @@ -909,36 +847,14 @@ done declare hcomplex_hcmod_eq_zero_cancel [simp] -(* not proved already? strange! *) -lemma hypreal_of_nat_le_iff: - "(hypreal_of_nat n <= hypreal_of_nat m) = (n <= m)" -apply (unfold hypreal_le_def) -apply auto -done -declare hypreal_of_nat_le_iff [simp] - -lemma hypreal_of_nat_ge_zero: "0 <= hypreal_of_nat n" -apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] - del: hypreal_of_nat_zero) -done -declare hypreal_of_nat_ge_zero [simp] - -declare hypreal_of_nat_ge_zero [THEN hrabs_eqI1, simp] - -lemma hypreal_of_hypnat_ge_zero: "0 <= hypreal_of_hypnat n" -apply (rule_tac z = "n" in eq_Abs_hypnat) -apply (simp (no_asm_simp) add: hypreal_of_hypnat hypreal_zero_num hypreal_le) -done -declare hypreal_of_hypnat_ge_zero [simp] - -declare hypreal_of_hypnat_ge_zero [THEN hrabs_eqI1, simp] - -lemma hcmod_hcomplex_of_hypreal_of_nat: "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n" +lemma hcmod_hcomplex_of_hypreal_of_nat: + "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n" apply auto done declare hcmod_hcomplex_of_hypreal_of_nat [simp] -lemma hcmod_hcomplex_of_hypreal_of_hypnat: "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n" +lemma hcmod_hcomplex_of_hypreal_of_hypnat: + "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n" apply auto done declare hcmod_hcomplex_of_hypreal_of_hypnat [simp] @@ -1025,7 +941,8 @@ apply (auto simp add: hcmod hcomplex_diff complex_mod_diff_commute) done -lemma hcmod_add_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s" +lemma hcmod_add_less: + "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s" apply (rule_tac z = "x" in eq_Abs_hcomplex) apply (rule_tac z = "y" in eq_Abs_hcomplex) apply (rule_tac z = "r" in eq_Abs_hypreal) @@ -1035,7 +952,8 @@ apply (auto intro: complex_mod_add_less) done -lemma hcmod_mult_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s" +lemma hcmod_mult_less: + "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s" apply (rule_tac z = "x" in eq_Abs_hcomplex) apply (rule_tac z = "y" in eq_Abs_hcomplex) apply (rule_tac z = "r" in eq_Abs_hypreal) @@ -1062,10 +980,11 @@ Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})" apply (unfold hcpow_def) apply (rule_tac f = "Abs_hcomplex" in arg_cong) -apply (auto , ultra) +apply (auto, ultra) done -lemma hcomplex_of_hypreal_hyperpow: "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" +lemma hcomplex_of_hypreal_hyperpow: + "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (rule_tac z = "n" in eq_Abs_hypnat) apply (auto simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow) @@ -1082,12 +1001,14 @@ apply (auto simp add: hcpow hyperpow hcmod complex_mod_complexpow) done -lemma hcomplexpow_minus: "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))" +lemma hcomplexpow_minus: + "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))" apply (induct_tac "n") apply auto done -lemma hcpow_minus: "(-x::hcomplex) hcpow n = +lemma hcpow_minus: + "(-x::hcomplex) hcpow n = (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))" apply (rule_tac z = "x" in eq_Abs_hcomplex) apply (rule_tac z = "n" in eq_Abs_hypnat) @@ -1129,7 +1050,7 @@ lemma hcomplexpow_mult: "((r::hcomplex) * s) ^ n = (r ^ n) * (s ^ n)" apply (induct_tac "n") -apply (auto simp add: hcomplex_mult_ac) +apply (auto simp add: mult_ac) done lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)" @@ -1159,9 +1080,10 @@ done declare hcpow_zero2 [simp] -lemma hcomplexpow_not_zero [rule_format (no_asm)]: "r ~= (0::hcomplex) --> r ^ n ~= 0" +lemma hcomplexpow_not_zero [rule_format (no_asm)]: + "r ~= (0::hcomplex) --> r ^ n ~= 0" apply (induct_tac "n") -apply (auto simp add: hcomplex_mult_not_zero) +apply (auto) done declare hcomplexpow_not_zero [simp] declare hcomplexpow_not_zero [intro] @@ -1209,7 +1131,8 @@ apply auto done -lemma hcomplex_mult_not_eq_zero_iff: "(x * y ~= (0::hcomplex)) = (x ~= 0 & y ~= 0)" +lemma hcomplex_mult_not_eq_zero_iff: + "(x * y ~= (0::hcomplex)) = (x ~= 0 & y ~= 0)" apply auto done declare hcomplex_mult_not_eq_zero_iff [iff] @@ -1229,7 +1152,7 @@ Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})" apply (unfold hsgn_def) apply (rule_tac f = "Abs_hcomplex" in arg_cong) -apply (auto , ultra) +apply (auto, ultra) done lemma hsgn_zero: "hsgn 0 = 0" @@ -1255,7 +1178,8 @@ apply (auto simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq) done -lemma lemma_hypreal_P_EX2: "(EX (x::hypreal) y. P x y) = +lemma lemma_hypreal_P_EX2: + "(EX (x::hypreal) y. P x y) = (EX f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))" apply auto apply (rule_tac z = "x" in eq_Abs_hypreal) @@ -1263,36 +1187,41 @@ apply auto done -lemma complex_split2: "ALL (n::nat). EX x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)" +lemma complex_split2: + "ALL (n::nat). EX x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)" apply (blast intro: complex_split) done (* Interesting proof! *) -lemma hcomplex_split: "EX x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)" +lemma hcomplex_split: + "EX x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)" apply (rule_tac z = "z" in eq_Abs_hcomplex) apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult) apply (cut_tac z = "x" in complex_split2) -apply (drule choice , safe)+ +apply (drule choice, safe)+ apply (rule_tac x = "f" in exI) apply (rule_tac x = "fa" in exI) apply auto done -lemma hRe_hcomplex_i: "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x" +lemma hRe_hcomplex_i: + "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (rule_tac z = "y" in eq_Abs_hypreal) apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) done declare hRe_hcomplex_i [simp] -lemma hIm_hcomplex_i: "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y" +lemma hIm_hcomplex_i: + "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (rule_tac z = "y" in eq_Abs_hypreal) apply (auto simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) done declare hIm_hcomplex_i [simp] -lemma hcmod_i: "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = +lemma hcmod_i: + "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = ( *f* sqrt) (x ^ 2 + y ^ 2)" apply (rule_tac z = "x" in eq_Abs_hypreal) apply (rule_tac z = "y" in eq_Abs_hypreal) @@ -1325,52 +1254,60 @@ apply (ultra) done -lemma hcomplex_eq_cancel_iff: "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = +lemma hcomplex_eq_cancel_iff: + "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))" apply (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq) done declare hcomplex_eq_cancel_iff [simp] -lemma hcomplex_eq_cancel_iffA: "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = +lemma hcomplex_eq_cancel_iffA: + "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii ) = ((xa = xb) & (ya = yb))" apply (auto simp add: hcomplex_mult_commute) done declare hcomplex_eq_cancel_iffA [iff] -lemma hcomplex_eq_cancel_iffB: "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = +lemma hcomplex_eq_cancel_iffB: + "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))" apply (auto simp add: hcomplex_mult_commute) done declare hcomplex_eq_cancel_iffB [iff] -lemma hcomplex_eq_cancel_iffC: "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = +lemma hcomplex_eq_cancel_iffC: + "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))" apply (auto simp add: hcomplex_mult_commute) done declare hcomplex_eq_cancel_iffC [iff] -lemma hcomplex_eq_cancel_iff2: "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = +lemma hcomplex_eq_cancel_iff2: + "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = hcomplex_of_hypreal xa) = (x = xa & y = 0)" apply (cut_tac xa = "x" and ya = "y" and xb = "xa" and yb = "0" in hcomplex_eq_cancel_iff) apply (simp del: hcomplex_eq_cancel_iff) done declare hcomplex_eq_cancel_iff2 [simp] -lemma hcomplex_eq_cancel_iff2a: "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = +lemma hcomplex_eq_cancel_iff2a: + "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = hcomplex_of_hypreal xa) = (x = xa & y = 0)" apply (auto simp add: hcomplex_mult_commute) done declare hcomplex_eq_cancel_iff2a [simp] -lemma hcomplex_eq_cancel_iff3: "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = +lemma hcomplex_eq_cancel_iff3: + "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)" apply (cut_tac xa = "x" and ya = "y" and xb = "0" and yb = "ya" in hcomplex_eq_cancel_iff) apply (simp del: hcomplex_eq_cancel_iff) done declare hcomplex_eq_cancel_iff3 [simp] -lemma hcomplex_eq_cancel_iff3a: "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = +lemma hcomplex_eq_cancel_iff3a: + "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)" apply (auto simp add: hcomplex_mult_commute) done @@ -1410,12 +1347,14 @@ done declare hIm_hsgn [simp] -lemma real_two_squares_add_zero_iff: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)" +lemma real_two_squares_add_zero_iff: + "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)" apply (auto intro: real_sum_squares_cancel) done declare real_two_squares_add_zero_iff [simp] -lemma hcomplex_inverse_complex_split: "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = +lemma hcomplex_inverse_complex_split: + "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) - iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))" apply (rule_tac z = "x" in eq_Abs_hypreal) @@ -1460,24 +1399,27 @@ apply (unfold harg_def) apply (rule_tac f = "Abs_hypreal" in arg_cong) -apply (auto , ultra) +apply (auto, ultra) done -lemma cos_harg_i_mult_zero: "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" +lemma cos_harg_i_mult_zero: + "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" apply (rule_tac z = "y" in eq_Abs_hypreal) apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg) apply (ultra) done declare cos_harg_i_mult_zero [simp] -lemma cos_harg_i_mult_zero2: "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" +lemma cos_harg_i_mult_zero2: + "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" apply (rule_tac z = "y" in eq_Abs_hypreal) apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg) apply (ultra) done declare cos_harg_i_mult_zero2 [simp] -lemma hcomplex_of_hypreal_not_zero_iff: "(hcomplex_of_hypreal y ~= 0) = (y ~= 0)" +lemma hcomplex_of_hypreal_not_zero_iff: + "(hcomplex_of_hypreal y ~= 0) = (y ~= 0)" apply (rule_tac z = "y" in eq_Abs_hypreal) apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def) done @@ -1489,7 +1431,8 @@ done declare hcomplex_of_hypreal_zero_iff [simp] -lemma cos_harg_i_mult_zero3: "y ~= 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" +lemma cos_harg_i_mult_zero3: + "y ~= 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" apply (cut_tac x = "y" and y = "0" in hypreal_linear) apply auto done @@ -1499,7 +1442,8 @@ (* Polar form for nonstandard complex numbers *) (*---------------------------------------------------------------------------*) -lemma complex_split_polar2: "ALL n. EX r a. (z n) = complex_of_real r * +lemma complex_split_polar2: + "ALL n. EX r a. (z n) = complex_of_real r * (complex_of_real(cos a) + ii * complex_of_real(sin a))" apply (blast intro: complex_split_polar) done @@ -1510,7 +1454,7 @@ apply (rule_tac z = "z" in eq_Abs_hcomplex) apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult) apply (cut_tac z = "x" in complex_split_polar2) -apply (drule choice , safe)+ +apply (drule choice, safe)+ apply (rule_tac x = "f" in exI) apply (rule_tac x = "fa" in exI) apply auto @@ -1545,10 +1489,11 @@ apply (rule hcomplex_split_polar) done -lemma hRe_hcomplex_polar: "hRe(hcomplex_of_hypreal r * +lemma hRe_hcomplex_polar: + "hRe(hcomplex_of_hypreal r * (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a" -apply (auto simp add: hcomplex_add_mult_distrib2 hcomplex_of_hypreal_mult hcomplex_mult_ac) +apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) done declare hRe_hcomplex_polar [simp] @@ -1558,10 +1503,11 @@ done declare hRe_hrcis [simp] -lemma hIm_hcomplex_polar: "hIm(hcomplex_of_hypreal r * +lemma hIm_hcomplex_polar: + "hIm(hcomplex_of_hypreal r * (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a" -apply (auto simp add: hcomplex_add_mult_distrib2 hcomplex_of_hypreal_mult hcomplex_mult_ac) +apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) done declare hIm_hcomplex_polar [simp] @@ -1571,7 +1517,8 @@ done declare hIm_hrcis [simp] -lemma hcmod_complex_polar: "hcmod (hcomplex_of_hypreal r * +lemma hcmod_complex_polar: + "hcmod (hcomplex_of_hypreal r * (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r" apply (rule_tac z = "r" in eq_Abs_hypreal) @@ -1656,7 +1603,8 @@ apply (auto simp add: hcis_hypreal_of_nat_Suc_mult) done -lemma hcis_hypreal_of_hypnat_Suc_mult: "hcis (hypreal_of_hypnat (n + 1) * a) = +lemma hcis_hypreal_of_hypnat_Suc_mult: + "hcis (hypreal_of_hypnat (n + 1) * a) = hcis a * hcis (hypreal_of_hypnat n * a)" apply (rule_tac z = "a" in eq_Abs_hypreal) apply (rule_tac z = "n" in eq_Abs_hypnat) @@ -1708,19 +1656,23 @@ done declare hIm_hcis [simp] -lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" +lemma cos_n_hRe_hcis_pow_n: + "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" apply (auto simp add: NSDeMoivre) done -lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" +lemma sin_n_hIm_hcis_pow_n: + "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" apply (auto simp add: NSDeMoivre) done -lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)" +lemma cos_n_hRe_hcis_hcpow_n: + "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)" apply (auto simp add: NSDeMoivre_ext) done -lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" +lemma sin_n_hIm_hcis_hcpow_n: + "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" apply (auto simp add: NSDeMoivre_ext) done @@ -1755,7 +1707,8 @@ done declare hcomplex_of_complex_eq_iff [simp] -lemma hcomplex_of_complex_minus: "hcomplex_of_complex (-r) = - hcomplex_of_complex r" +lemma hcomplex_of_complex_minus: + "hcomplex_of_complex (-r) = - hcomplex_of_complex r" apply (unfold hcomplex_of_complex_def) apply (auto simp add: hcomplex_minus) done @@ -1777,7 +1730,8 @@ apply (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def) done -lemma hcomplex_of_complex_inverse: "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)" +lemma hcomplex_of_complex_inverse: + "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)" apply (case_tac "r=0") apply (simp (no_asm_simp) add: COMPLEX_INVERSE_ZERO HCOMPLEX_INVERSE_ZERO hcomplex_of_complex_zero COMPLEX_DIVIDE_ZERO) apply (rule_tac c1 = "hcomplex_of_complex r" in hcomplex_mult_left_cancel [THEN iffD1]) @@ -1787,7 +1741,8 @@ done declare hcomplex_of_complex_inverse [simp] -lemma hcomplex_of_complex_divide: "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2" +lemma hcomplex_of_complex_divide: + "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2" apply (simp (no_asm) add: hcomplex_divide_def complex_divide_def) done declare hcomplex_of_complex_divide [simp] @@ -1848,7 +1803,6 @@ val hcomplex_add = thm"hcomplex_add"; val hcomplex_add_commute = thm"hcomplex_add_commute"; val hcomplex_add_assoc = thm"hcomplex_add_assoc"; -val hcomplex_add_left_commute = thm"hcomplex_add_left_commute"; val hcomplex_add_zero_left = thm"hcomplex_add_zero_left"; val hcomplex_add_zero_right = thm"hcomplex_add_zero_right"; val hRe_add = thm"hRe_add"; @@ -1860,25 +1814,17 @@ val hRe_minus = thm"hRe_minus"; val hIm_minus = thm"hIm_minus"; val hcomplex_add_minus_eq_minus = thm"hcomplex_add_minus_eq_minus"; -val hcomplex_minus_add_distrib = thm"hcomplex_minus_add_distrib"; -val hcomplex_add_left_cancel = thm"hcomplex_add_left_cancel"; -val hcomplex_add_right_cancel = thm"hcomplex_add_right_cancel"; val hcomplex_diff = thm"hcomplex_diff"; val hcomplex_diff_eq_eq = thm"hcomplex_diff_eq_eq"; val hcomplex_mult = thm"hcomplex_mult"; val hcomplex_mult_commute = thm"hcomplex_mult_commute"; val hcomplex_mult_assoc = thm"hcomplex_mult_assoc"; -val hcomplex_mult_left_commute = thm"hcomplex_mult_left_commute"; val hcomplex_mult_one_left = thm"hcomplex_mult_one_left"; val hcomplex_mult_one_right = thm"hcomplex_mult_one_right"; val hcomplex_mult_zero_left = thm"hcomplex_mult_zero_left"; -val hcomplex_mult_zero_right = thm"hcomplex_mult_zero_right"; -val hcomplex_minus_mult_eq1 = thm"hcomplex_minus_mult_eq1"; -val hcomplex_minus_mult_eq2 = thm"hcomplex_minus_mult_eq2"; val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one"; val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right"; val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib"; -val hcomplex_add_mult_distrib2 = thm"hcomplex_add_mult_distrib2"; val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one"; val hcomplex_inverse = thm"hcomplex_inverse"; val HCOMPLEX_INVERSE_ZERO = thm"HCOMPLEX_INVERSE_ZERO"; @@ -1886,10 +1832,6 @@ val hcomplex_mult_inv_left = thm"hcomplex_mult_inv_left"; val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel"; val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel"; -val hcomplex_inverse_not_zero = thm"hcomplex_inverse_not_zero"; -val hcomplex_mult_not_zero = thm"hcomplex_mult_not_zero"; -val hcomplex_mult_not_zeroE = thm"hcomplex_mult_not_zeroE"; -val hcomplex_minus_inverse = thm"hcomplex_minus_inverse"; val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib"; val hcomplex_of_hypreal = thm"hcomplex_of_hypreal"; val inj_hcomplex_of_hypreal = thm"inj_hcomplex_of_hypreal"; @@ -1928,10 +1870,6 @@ val hcomplex_hcnj_zero = thm"hcomplex_hcnj_zero"; val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff"; val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj"; -val hcomplex_mult_zero_iff = thm"hcomplex_mult_zero_iff"; -val hcomplex_add_left_cancel_zero = thm"hcomplex_add_left_cancel_zero"; -val hcomplex_diff_mult_distrib = thm"hcomplex_diff_mult_distrib"; -val hcomplex_diff_mult_distrib2 = thm"hcomplex_diff_mult_distrib2"; val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel"; val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff"; val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero"; @@ -2065,9 +2003,6 @@ val hRe_hcomplex_of_complex = thm"hRe_hcomplex_of_complex"; val hIm_hcomplex_of_complex = thm"hIm_hcomplex_of_complex"; val hcmod_hcomplex_of_complex = thm"hcmod_hcomplex_of_complex"; - -val hcomplex_add_ac = thms"hcomplex_add_ac"; -val hcomplex_mult_ac = thms"hcomplex_mult_ac"; *} end diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Complex/NSComplexArith.thy --- a/src/HOL/Complex/NSComplexArith.thy Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Complex/NSComplexArith.thy Thu Jan 01 21:47:07 2004 +0100 @@ -14,6 +14,6 @@ by simp lemma hcomplex_minus1_divide [simp]: "-1/(x::hcomplex) = - (1/x)" -by (simp add: hcomplex_divide_def hcomplex_minus_inverse) +by (simp add: hcomplex_divide_def inverse_minus_eq) end diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Complex/NSComplexBin.ML --- a/src/HOL/Complex/NSComplexBin.ML Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Complex/NSComplexBin.ML Thu Jan 01 21:47:07 2004 +0100 @@ -152,7 +152,7 @@ Goal "number_of v + (c - number_of w) = \ \ number_of (bin_add v (bin_minus w)) + (c::hcomplex)"; -by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_def]@ hcomplex_add_ac)); +by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_def]@ add_ac)); qed "hcomplex_add_number_of_diff2"; Addsimps [hcomplex_add_number_of_left, hcomplex_mult_number_of_left, @@ -171,7 +171,7 @@ Goal "i*u + (j*u + k) = (i+j)*u + (k::hcomplex)"; by (asm_simp_tac (simpset() addsimps [hcomplex_add_mult_distrib] - @ hcomplex_add_ac) 1); + @ add_ac) 1); qed "left_hcomplex_add_mult_distrib"; (** For cancel_numerals **) @@ -188,7 +188,7 @@ Goal "!!i::hcomplex. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; by (auto_tac (claset(), simpset() addsimps [hcomplex_add_mult_distrib, - hcomplex_diff_def] @ hcomplex_add_ac)); + hcomplex_diff_def] @ add_ac)); by (asm_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 1); by (simp_tac (simpset() addsimps [hcomplex_add_assoc]) 1); qed "hcomplex_eq_add_iff1"; @@ -309,29 +309,27 @@ (*To let us treat subtraction as addition*) -val diff_simps = [hcomplex_diff_def, hcomplex_minus_add_distrib, - minus_minus]; +val diff_simps = [hcomplex_diff_def, minus_add_distrib, minus_minus]; (*push the unary minus down: - x * y = x * - y *) val hcomplex_minus_mult_eq_1_to_2 = - [hcomplex_minus_mult_eq1 RS sym, hcomplex_minus_mult_eq2] MRS trans + [minus_mult_left RS sym, minus_mult_right] MRS trans |> standard; (*to extract again any uncancelled minuses*) val hcomplex_minus_from_mult_simps = - [minus_minus, hcomplex_minus_mult_eq1 RS sym, - hcomplex_minus_mult_eq2 RS sym]; + [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym]; (*combine unary minus with numeric literals, however nested within a product*) val hcomplex_mult_minus_simps = - [hcomplex_mult_assoc, hcomplex_minus_mult_eq1, hcomplex_minus_mult_eq_1_to_2]; + [hcomplex_mult_assoc, minus_mult_left, hcomplex_minus_mult_eq_1_to_2]; (*Final simplification: cancel + and * *) val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq - [hcomplex_add_zero_left, hcomplex_add_zero_right, - hcomplex_mult_zero_left, hcomplex_mult_zero_right, hcomplex_mult_one_left, - hcomplex_mult_one_right]; + [add_zero_left, add_zero_right, + mult_left_zero, mult_right_zero, mult_1, + mult_1_right]; val prep_simproc = Complex_Numeral_Simprocs.prep_simproc; @@ -346,11 +344,11 @@ val trans_tac = Real_Numeral_Simprocs.trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - hcomplex_minus_simps@hcomplex_add_ac)) + hcomplex_minus_simps@add_ac)) THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hcomplex_mult_minus_simps)) THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps@ - hcomplex_add_ac@hcomplex_mult_ac)) + add_ac@mult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) val simplify_meta_eq = simplify_meta_eq end; @@ -386,10 +384,10 @@ val trans_tac = Real_Numeral_Simprocs.trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - hcomplex_minus_simps@hcomplex_add_ac)) + hcomplex_minus_simps@add_ac)) THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hcomplex_mult_minus_simps)) THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps@ - hcomplex_add_ac@hcomplex_mult_ac)) + add_ac@mult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps)) val simplify_meta_eq = simplify_meta_eq @@ -501,7 +499,7 @@ val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) val T = HComplex_Numeral_Simprocs.hcomplexT val plus = Const ("op *", [T,T] ---> T) - val add_ac = hcomplex_mult_ac + val add_ac = mult_ac end; structure HComplex_Times_Assoc = Assoc_Fold (HComplex_Times_Assoc_Data); diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Complex/hcomplex_arith.ML --- a/src/HOL/Complex/hcomplex_arith.ML Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Complex/hcomplex_arith.ML Thu Jan 01 21:47:07 2004 +0100 @@ -19,7 +19,7 @@ val trans_tac = Real_Numeral_Simprocs.trans_tac val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps @ mult_1s)) THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hcomplex_mult_minus_simps)) - THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_mult_ac)) + THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps rel_hcomplex_number_of@bin_simps)) val simplify_meta_eq = simplify_meta_eq @@ -107,7 +107,7 @@ val dest_coeff = dest_coeff val find_first = find_first [] val trans_tac = Real_Numeral_Simprocs.trans_tac - val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hcomplex_mult_ac)) + val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac)) end; diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/IsaMakefile Thu Jan 01 21:47:07 2004 +0100 @@ -139,7 +139,7 @@ Real/Complex_Numbers.thy \ Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \ Real/PRat.ML Real/PRat.thy \ - Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \ + Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \ Real/ROOT.ML Real/Real.thy \ Real/RealArith0.thy Real/real_arith0.ML \ Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \ diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Real/PRat.ML --- a/src/HOL/Real/PRat.ML Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Real/PRat.ML Thu Jan 01 21:47:07 2004 +0100 @@ -482,9 +482,9 @@ by (asm_full_simp_tac (simpset() addsimps pnat_mult_ac) 1); qed "prat_linear"; -Goal "!!(q1::prat). [| q1 < q2 ==> P; q1 = q2 ==> P; \ -\ q2 < q1 ==> P |] ==> P"; -by (cut_inst_tac [("q1.0","q1"),("q2.0","q2")] prat_linear 1); +Goal "!!(x::prat). [| x < y ==> P; x = y ==> P; \ +\ y < x ==> P |] ==> P"; +by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1); by Auto_tac; qed "prat_linear_less2"; @@ -510,7 +510,7 @@ qed "lemma2_qinv_prat_less"; Goal "q1 < q2 ==> qinv (q2) < qinv (q1)"; -by (res_inst_tac [("q2.0","qinv q1"), ("q1.0","qinv q2")] prat_linear_less2 1); +by (res_inst_tac [("y","qinv q1"), ("x","qinv q2")] prat_linear_less2 1); by (auto_tac (claset() addEs [lemma1_qinv_prat_less, lemma2_qinv_prat_less],simpset())); qed "qinv_prat_less"; diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Real/PReal.ML --- a/src/HOL/Real/PReal.ML Thu Jan 01 10:06:32 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1244 +0,0 @@ -(* Title : HOL/Real/PReal.ML - ID : $Id$ - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : The positive reals as Dedekind sections of positive - rationals. Fundamentals of Abstract Analysis - [Gleason- p. 121] provides some of the definitions. -*) - -Goal "inj_on Abs_preal preal"; -by (rtac inj_on_inverseI 1); -by (etac Abs_preal_inverse 1); -qed "inj_on_Abs_preal"; - -Addsimps [inj_on_Abs_preal RS inj_on_iff]; - -Goal "inj(Rep_preal)"; -by (rtac inj_inverseI 1); -by (rtac Rep_preal_inverse 1); -qed "inj_Rep_preal"; - -Goalw [preal_def] "{} ~: preal"; -by (Fast_tac 1); -qed "empty_not_mem_preal"; - -(* {} : preal ==> P *) -bind_thm ("empty_not_mem_prealE", empty_not_mem_preal RS notE); - -Addsimps [empty_not_mem_preal]; - -Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} : preal"; -by (rtac preal_1 1); -qed "one_set_mem_preal"; - -Addsimps [one_set_mem_preal]; - -Goalw [preal_def] "x : preal ==> {} < x"; -by (Fast_tac 1); -qed "preal_psubset_empty"; - -Goal "{} < Rep_preal x"; -by (rtac (Rep_preal RS preal_psubset_empty) 1); -qed "Rep_preal_psubset_empty"; - -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])); -qed "mem_Rep_preal_Ex"; - -Goalw [preal_def] - "[| {} < A; A < UNIV; \ -\ (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; \ -\ 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 & \ -\ (ALL y: A. ((ALL z. z < y --> z: A) & \ -\ (EX u: A. y < u)))"; -by (Fast_tac 1); -qed "prealE_lemma"; - - -AddSIs [prealI1,prealI2]; - -Addsimps [Abs_preal_inverse]; - - -Goalw [preal_def] "A : preal ==> {} < A"; -by (Fast_tac 1); -qed "prealE_lemma1"; - -Goalw [preal_def] "A : preal ==> A < UNIV"; -by (Fast_tac 1); -qed "prealE_lemma2"; - -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 |] ==> (ALL z. z < y --> z: A)"; -by (fast_tac (claset() addSDs [prealE_lemma3]) 1); -qed "prealE_lemma3a"; - -Goal "[| A : preal; y: A; z < y |] ==> z: A"; -by (fast_tac (claset() addSDs [prealE_lemma3a]) 1); -qed "prealE_lemma3b"; - -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 |] ==> EX u: A. y < u"; -by (fast_tac (claset() addSDs [prealE_lemma4]) 1); -qed "prealE_lemma4a"; - -Goal "EX x. x~: Rep_preal X"; -by (cut_inst_tac [("x","X")] Rep_preal 1); -by (dtac prealE_lemma2 1); -by (auto_tac (claset(),simpset() addsimps [psubset_def])); -qed "not_mem_Rep_preal_Ex"; - -(** preal_of_prat: the injection from prat to preal **) -(** A few lemmas **) - -Goal "{xa::prat. xa < y} : preal"; -by (cut_facts_tac [qless_Ex] 1); -by (auto_tac (claset() addIs[prat_less_trans] - addSEs [prat_less_irrefl], - simpset())); -by (blast_tac (claset() addDs [prat_dense]) 1); -qed "lemma_prat_less_set_mem_preal"; - -Goal "!!(x::prat). {xa. xa < x} = {x. x < y} ==> x = y"; -by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1); -by Safe_tac; -by (dtac prat_dense 2 THEN etac exE 2); -by (dtac prat_dense 1 THEN etac exE 1); -by (blast_tac (claset() addDs [prat_less_not_sym]) 1); -by (blast_tac (claset() addDs [prat_less_not_sym]) 1); -qed "lemma_prat_set_eq"; - -Goal "inj(preal_of_prat)"; -by (rtac injI 1); -by (rewtac preal_of_prat_def); -by (dtac (inj_on_Abs_preal RS inj_onD) 1); -by (rtac lemma_prat_less_set_mem_preal 1); -by (rtac lemma_prat_less_set_mem_preal 1); -by (etac lemma_prat_set_eq 1); -qed "inj_preal_of_prat"; - - (*** theorems for ordering ***) -(* prove introduction and elimination rules for preal_less *) - -(* A positive fraction not in a positive real is an upper bound *) -(* Gleason p. 122 - Remark (1) *) - -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 (fast_tac (claset() addIs [not_less_not_eq_prat_less] addss simpset()) 1); -qed "not_in_preal_ub"; - -(* preal_less is a strong order i.e nonreflexive and transitive *) - -Goalw [preal_less_def] "~ (x::preal) < x"; -by (simp_tac (simpset() addsimps [psubset_def]) 1); -qed "preal_less_not_refl"; - -(*** y < y ==> P ***) -bind_thm("preal_less_irrefl", preal_less_not_refl RS notE); - -Goal "!!(x::preal). x < y ==> x ~= y"; -by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl])); -qed "preal_not_refl2"; - -Goalw [preal_less_def] "!!(x::preal). [| x < y; y < z |] ==> x < z"; -by (auto_tac (claset() addDs [subsetD,equalityI], - simpset() addsimps [psubset_def])); -qed "preal_less_trans"; - -Goal "!! (q1::preal). q1 < q2 ==> ~ q2 < q1"; -by (rtac notI 1); -by (dtac preal_less_trans 1 THEN assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [preal_less_not_refl]) 1); -qed "preal_less_not_sym"; - -(* [| x < y; ~P ==> y < x |] ==> P *) -bind_thm ("preal_less_asym", preal_less_not_sym RS contrapos_np); - -Goalw [preal_less_def] - "(r1::preal) < r2 | r1 = r2 | r2 < r1"; -by (auto_tac (claset() addSDs [inj_Rep_preal RS injD], - simpset() addsimps [psubset_def])); -by (rtac prealE_lemma3b 1 THEN rtac Rep_preal 1); -by (assume_tac 1); -by (fast_tac (claset() addDs [not_in_preal_ub]) 1); -qed "preal_linear"; - -Goal "!!(r1::preal). [| r1 < r2 ==> P; r1 = r2 ==> P; \ -\ r2 < r1 ==> P |] ==> P"; -by (cut_inst_tac [("r1.0","r1"),("r2.0","r2")] preal_linear 1); -by Auto_tac; -qed "preal_linear_less2"; - - (*** Properties of addition ***) - -Goalw [preal_add_def] "(x::preal) + y = y + x"; -by (res_inst_tac [("f","Abs_preal")] arg_cong 1); -by (blast_tac (claset() addIs [prat_add_commute RS subst]) 1); -qed "preal_add_commute"; - -(** addition of two positive reals gives a positive real **) -(** lemmas for proving positive reals addition set in preal **) - -(** Part 1 of Dedekind sections def **) -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], simpset())); -qed "preal_add_set_not_empty"; - -(** Part 2 of Dedekind sections def **) -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)); -by (REPEAT(dtac not_in_preal_ub 1)); -by (res_inst_tac [("x","x+xa")] exI 1); -by (Auto_tac THEN (REPEAT(etac ballE 1)) THEN Auto_tac); -by (dtac prat_add_less_mono 1); -by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl])); -qed "preal_not_mem_add_set_Ex"; - -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 Auto_tac; -qed "preal_add_set_not_prat_set"; - -(** Part 3 of Dedekind sections def **) -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 (Suc 0))")] - prat_mult_less2_mono1 1); -by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat (Suc 0))")] - prat_mult_less2_mono1 1); -by (Asm_full_simp_tac 1); -by (REPEAT(dtac (Rep_preal RS prealE_lemma3a) 1)); -by (REPEAT(etac allE 1)); -by Auto_tac; -by (REPEAT(rtac bexI 1)); -by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2 - RS sym,prat_add_assoc RS sym,prat_mult_assoc])); -qed "preal_add_set_lemma3"; - -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. 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); -by (rtac preal_add_set_lemma3 1); -by (rtac preal_add_set_lemma4 1); -qed "preal_mem_add_set"; - -Goalw [preal_add_def] "((x::preal) + y) + z = x + (y + z)"; -by (res_inst_tac [("f","Abs_preal")] arg_cong 1); -by (simp_tac (simpset() addsimps [preal_mem_add_set RS Abs_preal_inverse]) 1); -by (auto_tac (claset(),simpset() addsimps prat_add_ac)); -by (rtac bexI 1); -by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_add_ac)); -qed "preal_add_assoc"; - -Goal "(z1::preal) + (z2 + z3) = z2 + (z1 + z3)"; -by(rtac ([preal_add_assoc,preal_add_commute] MRS - read_instantiate[("f","op +")](thm"mk_left_commute")) 1); -qed "preal_add_left_commute"; - -(* Positive Reals addition is an AC operator *) -bind_thms ("preal_add_ac", [preal_add_assoc, preal_add_commute, preal_add_left_commute]); - - (*** Properties of multiplication ***) - -(** Proofs essentially same as for addition **) - -Goalw [preal_mult_def] "(x::preal) * y = y * x"; -by (res_inst_tac [("f","Abs_preal")] arg_cong 1); -by (blast_tac (claset() addIs [prat_mult_commute RS subst]) 1); -qed "preal_mult_commute"; - -(** multiplication of two positive reals gives a positive real **) -(** lemmas for proving positive reals multiplication set in preal **) - -(** Part 1 of Dedekind sections def **) -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], simpset())); -qed "preal_mult_set_not_empty"; - -(** Part 2 of Dedekind sections def **) -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)); -by (REPEAT(dtac not_in_preal_ub 1)); -by (res_inst_tac [("x","x*xa")] exI 1); -by (Auto_tac THEN (REPEAT(etac ballE 1)) THEN Auto_tac ); -by (dtac prat_mult_less_mono 1); -by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl])); -qed "preal_not_mem_mult_set_Ex"; - -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 Auto_tac; -qed "preal_mult_set_not_prat_set"; - -(** Part 3 of Dedekind sections def **) -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); -by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1); -by (dtac (Rep_preal RS prealE_lemma3a) 1); -by (etac allE 1); -by (REPEAT(rtac bexI 1)); -by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc])); -qed "preal_mult_set_lemma3"; - -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. 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); -by (rtac preal_mult_set_lemma3 1); -by (rtac preal_mult_set_lemma4 1); -qed "preal_mem_mult_set"; - -Goalw [preal_mult_def] "((x::preal) * y) * z = x * (y * z)"; -by (res_inst_tac [("f","Abs_preal")] arg_cong 1); -by (simp_tac (simpset() addsimps [preal_mem_mult_set RS Abs_preal_inverse]) 1); -by (auto_tac (claset(),simpset() addsimps prat_mult_ac)); -by (rtac bexI 1); -by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_mult_ac)); -qed "preal_mult_assoc"; - -Goal "(z1::preal) * (z2 * z3) = z2 * (z1 * z3)"; -by(rtac ([preal_mult_assoc,preal_mult_commute] MRS - read_instantiate[("f","op *")](thm"mk_left_commute")) 1); -qed "preal_mult_left_commute"; - -(* Positive Reals multiplication is an AC operator *) -bind_thms ("preal_mult_ac", [preal_mult_assoc, - preal_mult_commute, - preal_mult_left_commute]); - -(* Positive Real 1 is the multiplicative identity element *) -(* long *) -Goalw [preal_of_prat_def,preal_mult_def] - "(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) * z = z"; -by (rtac (Rep_preal_inverse RS subst) 1); -by (res_inst_tac [("f","Abs_preal")] arg_cong 1); -by (rtac (one_set_mem_preal RS Abs_preal_inverse RS ssubst) 1); -by (auto_tac(claset(),simpset() addsimps [Rep_preal_inverse])); -by (EVERY1[dtac (Rep_preal RS prealE_lemma4a),etac bexE]); -by (dtac prat_mult_less_mono 1); -by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3a],simpset())); -by (EVERY1[forward_tac [Rep_preal RS prealE_lemma4a],etac bexE]); -by (forw_inst_tac [("x","qinv(u)"),("q1.0","x")] - prat_mult_less2_mono1 1); -by (rtac exI 1 THEN Auto_tac THEN res_inst_tac [("x","u")] bexI 1); -by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc])); -qed "preal_mult_1"; - -Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) = z"; -by (rtac (preal_mult_commute RS subst) 1); -by (rtac preal_mult_1 1); -qed "preal_mult_1_right"; - -(** Lemmas **) - -Goal "(z::preal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"; -by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); -qed "preal_add_assoc_cong"; - -Goal "(z::preal) + (v + w) = v + (z + w)"; -by (REPEAT (ares_tac [preal_add_commute RS preal_add_assoc_cong] 1)); -qed "preal_add_assoc_swap"; - -(** Distribution of multiplication across addition **) -(** lemmas for the proof **) - - (** lemmas **) -Goalw [preal_add_def] - "z: Rep_preal(R+S) ==> \ -\ 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] - "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)) = (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) ==> \ -\ 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] - "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)) = (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"; - -(** More lemmas for preal_add_mult_distrib2 **) - -Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \ -\ Rep_preal w; yb: Rep_preal w |] ==> \ -\ xb * ya + xc * yb: Rep_preal (z1 * w + z2 * w)"; -by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1); -qed "lemma_add_mult_mem_Rep_preal"; - -Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \ -\ Rep_preal w; yb: Rep_preal w |] ==> \ -\ yb*(xb + xc): Rep_preal (w*(z1 + z2))"; -by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1); -qed "lemma_add_mult_mem_Rep_preal1"; - -Goal "x: Rep_preal (w * z1 + w * z2) ==> \ -\ x: Rep_preal (w * (z1 + z2))"; -by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD], - simpset())); -by (forw_inst_tac [("ya","xa"),("yb","xb"),("xb","ya"),("xc","yb")] - lemma_add_mult_mem_Rep_preal1 1); -by Auto_tac; -by (res_inst_tac [("q1.0","xa"),("q2.0","xb")] prat_linear_less2 1); -by (dres_inst_tac [("b","ya"),("c","yb")] lemma_prat_add_mult_mono 1); -by (rtac (Rep_preal RS prealE_lemma3b) 1); -by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2])); -by (dres_inst_tac [("ya","xb"),("yb","xa"),("xc","ya"),("xb","yb")] - lemma_add_mult_mem_Rep_preal1 1); -by Auto_tac; -by (dres_inst_tac [("b","yb"),("c","ya")] lemma_prat_add_mult_mono 1); -by (rtac (Rep_preal RS prealE_lemma3b) 1); -by (thin_tac "xb * ya + xb * yb : Rep_preal (w * (z1 + z2))" 1); -by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib, - prat_add_commute] @ preal_add_ac )); -qed "lemma_preal_add_mult_distrib"; - -Goal "x: Rep_preal (w * (z1 + z2)) ==> \ -\ x: Rep_preal (w * z1 + w * z2)"; -by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD] - addSIs [bexI,mem_Rep_preal_addI,mem_Rep_preal_multI], - simpset() addsimps [prat_add_mult_distrib2])); -qed "lemma_preal_add_mult_distrib2"; - -Goal "(w * ((z1::preal) + z2)) = (w * z1) + (w * z2)"; -by (rtac (inj_Rep_preal RS injD) 1); -by (fast_tac (claset() addIs [lemma_preal_add_mult_distrib, - lemma_preal_add_mult_distrib2]) 1); -qed "preal_add_mult_distrib2"; - -Goal "(((z1::preal) + z2) * w) = (z1 * w) + (z2 * w)"; -by (simp_tac (simpset() addsimps [preal_mult_commute, - preal_add_mult_distrib2]) 1); -qed "preal_add_mult_distrib"; - -(*** Prove existence of inverse ***) -(*** Inverse is a positive real ***) - -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 "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); -by (Fast_tac 1); -qed "lemma_preal_mem_inv_set_ex"; - -(** Part 1 of Dedekind sections def **) -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], simpset())); -qed "preal_inv_set_not_empty"; - -(** Part 2 of Dedekind sections def **) -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 "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; -by (EVERY1[etac allE, etac exE, etac conjE]); -by (dtac qinv_prat_less 1 THEN dtac not_in_preal_ub 1); -by (eres_inst_tac [("x","qinv y")] ballE 1); -by (dtac prat_less_trans 1); -by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl])); -qed "preal_not_mem_inv_set_Ex"; - -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 Auto_tac; -qed "preal_inv_set_not_prat_set"; - -(** Part 3 of Dedekind sections def **) -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 "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. 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); -by (rtac preal_inv_set_lemma3 1); -by (rtac preal_inv_set_lemma4 1); -qed "preal_mem_inv_set"; - -(*more lemmas for inverse *) -Goal "x: Rep_preal(pinv(A)*A) ==> \ -\ x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"; -by (auto_tac (claset() addSDs [mem_Rep_preal_multD], - simpset() addsimps [pinv_def,preal_of_prat_def] )); -by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1); -by (auto_tac (claset() addSDs [not_in_preal_ub],simpset())); -by (dtac prat_mult_less_mono 1 THEN Blast_tac 1); -by (auto_tac (claset(),simpset())); -qed "preal_mem_mult_invD"; - -(*** Gleason's Lemma 9-3.4 p 122 ***) -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 (induct_thm_tac pnat_induct "p" 1); -by (auto_tac (claset(),simpset() addsimps [pnat_one_def, - pSuc_is_plus_one,prat_add_mult_distrib, - prat_of_pnat_add,prat_add_assoc RS sym])); -qed "lemma1_gleason9_34"; - -Goal "Abs_prat (ratrel `` {(y, z)}) < xb + \ -\ Abs_prat (ratrel `` {(x*y, Abs_pnat (Suc 0))})*Abs_prat (ratrel `` {(w, x)})"; -by (res_inst_tac [("j","Abs_prat (ratrel `` {(x * y, Abs_pnat (Suc 0))}) *\ -\ Abs_prat (ratrel `` {(w, x)})")] prat_le_less_trans 1); -by (rtac prat_self_less_add_right 2); -by (auto_tac (claset() addIs [lemma_Abs_prat_le3], - simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc])); -qed "lemma1b_gleason9_34"; - -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); -by (res_inst_tac [("z","x")] eq_Abs_prat 1); -by (res_inst_tac [("z","xa")] eq_Abs_prat 1); -by (dres_inst_tac [("p","y*xb")] lemma1_gleason9_34 1); -by (etac bexE 1); -by (cut_inst_tac [("x","y"),("y","xb"),("w","xaa"), - ("z","ya"),("xb","xba")] lemma1b_gleason9_34 1); -by (dres_inst_tac [("x","xba + prat_of_pnat (y * xb) * x")] bspec 1); -by (auto_tac (claset() addIs [prat_less_asym], - simpset() addsimps [prat_of_pnat_def])); -qed "lemma_gleason9_34a"; - -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"; - -(*** Gleason's Lemma 9-3.6 ***) -(* lemmas for Gleason 9-3.6 *) -(* *) -(******************************) - -Goal "r + r*qinv(xa)*Q3 = r*qinv(xa)*(xa + Q3)"; -by (full_simp_tac (simpset() addsimps [prat_add_mult_distrib2, - prat_mult_assoc]) 1); -qed "lemma1_gleason9_36"; - -Goal "r*qinv(xa)*(xa*x) = r*x"; -by (full_simp_tac (simpset() addsimps prat_mult_ac) 1); -qed "lemma2_gleason9_36"; -(******) - -(*** FIXME: long! ***) -Goal "prat_of_pnat 1 < 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); -by (dres_inst_tac [("x","xa")] prat_self_less_mult_right 1); -by (etac prat_lessE 1); -by (cut_inst_tac [("R","A"),("x","Q3")] lemma_gleason9_34 1); -by (dtac sym 1 THEN Auto_tac ); -by (ftac not_in_preal_ub 1); -by (dres_inst_tac [("x","xa + Q3")] bspec 1 THEN assume_tac 1); -by (dtac prat_add_right_less_cancel 1); -by (dres_inst_tac [("x","qinv(xa)*Q3")] prat_mult_less2_mono1 1); -by (dres_inst_tac [("x","r")] prat_add_less2_mono2 1); -by (asm_full_simp_tac (simpset() addsimps - [prat_mult_assoc RS sym,lemma1_gleason9_36]) 1); -by (dtac sym 1); -by (auto_tac (claset(),simpset() addsimps [lemma2_gleason9_36])); -by (res_inst_tac [("x","r")] bexI 1); -by (rtac notI 1); -by (dres_inst_tac [("y","r*x")] (Rep_preal RS prealE_lemma3b) 1); -by Auto_tac; -qed "lemma_gleason9_36"; - -Goal "prat_of_pnat (Abs_pnat (Suc 0)) < x ==> \ -\ 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"; - -(*** Part 2 of existence of inverse ***) -Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) \ -\ ==> x: Rep_preal(pinv(A)*A)"; -by (auto_tac (claset() addSIs [mem_Rep_preal_multI], - simpset() addsimps [pinv_def,preal_of_prat_def] )); -by (rtac (preal_mem_inv_set RS Abs_preal_inverse RS ssubst) 1); -by (dtac prat_qinv_gt_1 1); -by (dres_inst_tac [("A","A")] lemma_gleason9_36a 1); -by Auto_tac; -by (dtac (Rep_preal RS prealE_lemma4a) 1); -by (Auto_tac THEN dtac qinv_prat_less 1); -by (res_inst_tac [("x","qinv(u)*x")] exI 1); -by (rtac conjI 1); -by (res_inst_tac [("x","qinv(r)*x")] exI 1); -by (auto_tac (claset() addIs [prat_mult_less2_mono1], - simpset() addsimps [qinv_mult_eq,qinv_qinv])); -by (res_inst_tac [("x","u")] bexI 1); -by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc, - prat_mult_left_commute])); -qed "preal_mem_mult_invI"; - -Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"; -by (rtac (inj_Rep_preal RS injD) 1); -by (fast_tac (claset() addDs [preal_mem_mult_invD,preal_mem_mult_invI]) 1); -qed "preal_mult_inv"; - -Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"; -by (rtac (preal_mult_commute RS subst) 1); -by (rtac preal_mult_inv 1); -qed "preal_mult_inv_right"; - -val [prem] = Goal - "(!!u. z = Abs_preal(u) ==> P) ==> P"; -by (cut_inst_tac [("x1","z")] - (rewrite_rule [preal_def] (Rep_preal RS Abs_preal_inverse)) 1); -by (res_inst_tac [("u","Rep_preal z")] prem 1); -by (dtac (inj_Rep_preal RS injD) 1); -by (Asm_simp_tac 1); -qed "eq_Abs_preal"; - -(*** Lemmas/Theorem(s) need lemma_gleason9_34 ***) -Goal "Rep_preal (R1) <= Rep_preal(R1 + R2)"; -by (cut_inst_tac [("X","R2")] mem_Rep_preal_Ex 1); -by (auto_tac (claset() addSIs [bexI] addIs [(Rep_preal RS prealE_lemma3b), - prat_self_less_add_left,mem_Rep_preal_addI],simpset())); -qed "Rep_preal_self_subset"; - -Goal "~ Rep_preal (R1 + R2) <= Rep_preal(R1)"; -by (cut_inst_tac [("X","R2")] mem_Rep_preal_Ex 1); -by (etac exE 1); -by (cut_inst_tac [("R","R1")] lemma_gleason9_34 1); -by (auto_tac (claset() addIs [mem_Rep_preal_addI],simpset())); -qed "Rep_preal_sum_not_subset"; - -Goal "Rep_preal (R1 + R2) ~= Rep_preal(R1)"; -by (rtac notI 1); -by (etac equalityE 1); -by (asm_full_simp_tac (simpset() addsimps [Rep_preal_sum_not_subset]) 1); -qed "Rep_preal_sum_not_eq"; - -(*** at last --- Gleason prop. 9-3.5(iii) p. 123 ***) -Goalw [preal_less_def,psubset_def] "(R1::preal) < R1 + R2"; -by (simp_tac (simpset() addsimps [Rep_preal_self_subset, - Rep_preal_sum_not_eq RS not_sym]) 1); -qed "preal_self_less_add_left"; - -Goal "(R1::preal) < R2 + R1"; -by (simp_tac (simpset() addsimps [preal_add_commute,preal_self_less_add_left]) 1); -qed "preal_self_less_add_right"; - -(*** Properties of <= ***) - -Goalw [preal_le_def,psubset_def,preal_less_def] - "z<=w ==> ~(w<(z::preal))"; -by (auto_tac (claset() addDs [equalityI],simpset())); -qed "preal_leD"; - -bind_thm ("preal_leE", make_elim preal_leD); - -Goalw [preal_le_def,psubset_def,preal_less_def] - "~ z <= w ==> w<(z::preal)"; -by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1); -by (auto_tac (claset(),simpset() addsimps [preal_less_def,psubset_def])); -qed "not_preal_leE"; - -Goal "~(w < z) ==> z <= (w::preal)"; -by (fast_tac (claset() addIs [not_preal_leE]) 1); -qed "preal_leI"; - -Goal "(~(w < z)) = (z <= (w::preal))"; -by (fast_tac (claset() addSIs [preal_leI,preal_leD]) 1); -qed "preal_less_le_iff"; - -Goalw [preal_le_def,preal_less_def,psubset_def] - "z < w ==> z <= (w::preal)"; -by (Fast_tac 1); -qed "preal_less_imp_le"; - -Goalw [preal_le_def,preal_less_def,psubset_def] - "!!(x::preal). x <= y ==> x < y | x = y"; -by (auto_tac (claset() addIs [inj_Rep_preal RS injD],simpset())); -qed "preal_le_imp_less_or_eq"; - -Goalw [preal_le_def,preal_less_def,psubset_def] - "!!(x::preal). x < y | x = y ==> x <=y"; -by Auto_tac; -qed "preal_less_or_eq_imp_le"; - -Goalw [preal_le_def] "w <= (w::preal)"; -by (Simp_tac 1); -qed "preal_le_refl"; - -Goal "[| i <= j; j <= k |] ==> i <= (k::preal)"; -by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq, - rtac preal_less_or_eq_imp_le, - fast_tac (claset() addIs [preal_less_trans])]); -qed "preal_le_trans"; - -Goal "[| z <= w; w <= z |] ==> z = (w::preal)"; -by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq, - fast_tac (claset() addEs [preal_less_irrefl,preal_less_asym])]); -qed "preal_le_anti_sym"; - -Goal "!!w::preal. (w ~= z) = (w ?D. A + D = B ****) -(**** Gleason prop. 9-3.5(iv) p. 123 ****) -(**** Define the D required and show that it is a positive real ****) - -(* useful lemmas - proved elsewhere? *) -Goalw [psubset_def] "A < B ==> EX x. x ~: A & x : B"; -by Auto_tac; -qed "lemma_psubset_mem"; - -Goalw [psubset_def] "~ (A::'a set) < A"; -by (Fast_tac 1); -qed "lemma_psubset_not_refl"; - -Goalw [psubset_def] "!!(A::'a set). [| A < B; B < C |] ==> A < C"; -by (auto_tac (claset() addDs [subset_antisym],simpset())); -qed "psubset_trans"; - -Goalw [psubset_def] "!!(A::'a set). [| A <= B; B < C |] ==> A < C"; -by (auto_tac (claset() addDs [subset_antisym],simpset())); -qed "subset_psubset_trans"; - -Goalw [psubset_def] "!!(A::'a set). [| A < B; B <= C |] ==> A < C"; -by (auto_tac (claset() addDs [subset_antisym],simpset())); -qed "subset_psubset_trans2"; - -Goalw [psubset_def] "!!(A::'a set). [| A < B; c : A |] ==> c : B"; -by (auto_tac (claset() addDs [subsetD],simpset())); -qed "psubsetD"; - -(** Part 1 of Dedekind sections def **) -Goalw [preal_less_def] - "A < 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])); -qed "lemma_ex_mem_less_left_add1"; - -Goal "A < 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], simpset())); -qed "preal_less_set_not_empty"; - -(** Part 2 of Dedekind sections def **) -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); -by Auto_tac; -by (cut_inst_tac [("x","x"),("y","n")] prat_self_less_add_right 1); -by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset())); -qed "lemma_ex_not_mem_less_left_add1"; - -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 Auto_tac; -qed "preal_less_set_not_prat_set"; - -(** Part 3 of Dedekind sections def **) -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 ==> 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])); -qed "preal_less_set_lemma4"; - -Goal - "!! (A::preal). A < B ==> \ -\ {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); -by (rtac preal_less_set_lemma3 2); -by (rtac preal_less_set_lemma4 3); -by Auto_tac; -qed "preal_mem_less_set"; - -(** proving that A + D <= B **) -Goalw [preal_le_def] - "!! (A::preal). A < 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 [ - preal_mem_less_set RS Abs_preal_inverse])); -by (dtac not_in_preal_ub 1); -by (dtac bspec 1 THEN assume_tac 1); -by (dres_inst_tac [("x","y")] prat_add_less2_mono1 1); -by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma3b) 1); -by Auto_tac; -qed "preal_less_add_left_subsetI"; - -(** proving that B <= A + D --- trickier **) -(** lemma **) -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. 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); -by (dtac lemma_sum_mem_Rep_preal_ex 1); -by (etac exE 1); -by (cut_inst_tac [("R","A"),("x","e")] lemma_gleason9_34 1 THEN etac bexE 1); -by (dtac not_in_preal_ub 1 THEN dtac bspec 1 THEN assume_tac 1); -by (etac prat_lessE 1); -by (res_inst_tac [("x","r")] bexI 1); -by (res_inst_tac [("x","Q3")] bexI 1); -by (cut_facts_tac [Rep_preal_self_subset] 4); -by (auto_tac (claset(),simpset() addsimps [ - preal_mem_less_set RS Abs_preal_inverse])); -by (res_inst_tac [("x","r+e")] exI 1); -by (asm_full_simp_tac (simpset() addsimps prat_add_ac) 1); -qed "preal_less_add_left_subsetI2"; - -(*** required proof ***) -Goal "!! (A::preal). A < 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 ==> EX D. A + D = B"; -by (fast_tac (claset() addDs [preal_less_add_left]) 1); -qed "preal_less_add_left_Ex"; - -Goal "!!(A::preal). A < B ==> A + C < B + C"; -by (auto_tac (claset() addSDs [preal_less_add_left_Ex], - simpset() addsimps [preal_add_assoc])); -by (res_inst_tac [("y1","D")] (preal_add_commute RS subst) 1); -by (auto_tac (claset() addIs [preal_self_less_add_left], - simpset() addsimps [preal_add_assoc RS sym])); -qed "preal_add_less2_mono1"; - -Goal "!!(A::preal). A < B ==> C + A < C + B"; -by (auto_tac (claset() addIs [preal_add_less2_mono1], - simpset() addsimps [preal_add_commute])); -qed "preal_add_less2_mono2"; - -Goal - "!!(q1::preal). q1 < q2 ==> q1 * x < q2 * x"; -by (dtac preal_less_add_left_Ex 1); -by (auto_tac (claset(),simpset() addsimps [preal_add_mult_distrib, - preal_self_less_add_left])); -qed "preal_mult_less_mono1"; - -Goal "!!(q1::preal). q1 < q2 ==> x * q1 < x * q2"; -by (auto_tac (claset() addDs [preal_mult_less_mono1], - simpset() addsimps [preal_mult_commute])); -qed "preal_mult_left_less_mono1"; - -Goal "!!(q1::preal). q1 <= q2 ==> x * q1 <= x * q2"; -by (dtac preal_le_imp_less_or_eq 1); -by (Step_tac 1); -by (auto_tac (claset() addSIs [preal_le_refl, - preal_less_imp_le,preal_mult_left_less_mono1],simpset())); -qed "preal_mult_left_le_mono1"; - -Goal "!!(q1::preal). q1 <= q2 ==> q1 * x <= q2 * x"; -by (auto_tac (claset() addDs [preal_mult_left_le_mono1], - simpset() addsimps [preal_mult_commute])); -qed "preal_mult_le_mono1"; - -Goal "!!(q1::preal). q1 <= q2 ==> x + q1 <= x + q2"; -by (dtac preal_le_imp_less_or_eq 1); -by (Step_tac 1); -by (auto_tac (claset() addSIs [preal_le_refl, - preal_less_imp_le,preal_add_less2_mono1], - simpset() addsimps [preal_add_commute])); -qed "preal_add_left_le_mono1"; - -Goal "!!(q1::preal). q1 <= q2 ==> q1 + x <= q2 + x"; -by (auto_tac (claset() addDs [preal_add_left_le_mono1], - simpset() addsimps [preal_add_commute])); -qed "preal_add_le_mono1"; - -Goal "!!(A::preal). A + C < B + C ==> A < B"; -by (cut_facts_tac [preal_linear] 1); -by (auto_tac (claset() addEs [preal_less_irrefl],simpset())); -by (dres_inst_tac [("A","B"),("C","C")] preal_add_less2_mono1 1); -by (fast_tac (claset() addDs [preal_less_trans] - addEs [preal_less_irrefl]) 1); -qed "preal_add_right_less_cancel"; - -Goal "!!(A::preal). C + A < C + B ==> A < B"; -by (auto_tac (claset() addEs [preal_add_right_less_cancel], - simpset() addsimps [preal_add_commute])); -qed "preal_add_left_less_cancel"; - -Goal "((A::preal) + C < B + C) = (A < B)"; -by (REPEAT(ares_tac [iffI,preal_add_less2_mono1, - preal_add_right_less_cancel] 1)); -qed "preal_add_less_iff1"; - -Addsimps [preal_add_less_iff1]; - -Goal "(C + (A::preal) < C + B) = (A < B)"; -by (REPEAT(ares_tac [iffI,preal_add_less2_mono2, - preal_add_left_less_cancel] 1)); -qed "preal_add_less_iff2"; - -Addsimps [preal_add_less_iff2]; - -Goal "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)"; -by (auto_tac (claset() addSDs [preal_less_add_left_Ex], - simpset() addsimps preal_add_ac)); -by (rtac (preal_add_assoc RS subst) 1); -by (rtac preal_self_less_add_right 1); -qed "preal_add_less_mono"; - -Goal "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)"; -by (auto_tac (claset() addSDs [preal_less_add_left_Ex], - simpset() addsimps [preal_add_mult_distrib, - preal_add_mult_distrib2,preal_self_less_add_left, - preal_add_assoc] @ preal_mult_ac)); -qed "preal_mult_less_mono"; - -Goal "!!(A::preal). A + C = B + C ==> A = B"; -by (cut_facts_tac [preal_linear] 1); -by Auto_tac; -by (ALLGOALS(dres_inst_tac [("C","C")] preal_add_less2_mono1)); -by (auto_tac (claset() addEs [preal_less_irrefl],simpset())); -qed "preal_add_right_cancel"; - -Goal "!!(A::preal). C + A = C + B ==> A = B"; -by (auto_tac (claset() addIs [preal_add_right_cancel], - simpset() addsimps [preal_add_commute])); -qed "preal_add_left_cancel"; - -Goal "(C + A = C + B) = ((A::preal) = B)"; -by (fast_tac (claset() addIs [preal_add_left_cancel]) 1); -qed "preal_add_left_cancel_iff"; - -Goal "(A + C = B + C) = ((A::preal) = B)"; -by (fast_tac (claset() addIs [preal_add_right_cancel]) 1); -qed "preal_add_right_cancel_iff"; - -Addsimps [preal_add_left_cancel_iff,preal_add_right_cancel_iff]; - -(*** Completeness of preal ***) - -(*** prove that supremum is a cut ***) -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 "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], simpset())); -qed "preal_sup_set_not_empty"; - -(** Part 2 of Dedekind sections def **) -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); -by (res_inst_tac [("x","x")] exI 1); -by (auto_tac (claset() addSDs [bspec],simpset())); -qed "preal_sup_not_mem_Ex"; - -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); -by (res_inst_tac [("x","x")] exI 1); -by (auto_tac (claset() addSDs [bspec],simpset())); -qed "preal_sup_not_mem_Ex1"; - -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())); -qed "preal_sup_set_not_prat_set"; - -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())); -qed "preal_sup_set_not_prat_set1"; - -(** Part 3 of Dedekind sections def **) -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 "[|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 "[|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 "[|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 "[|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); -by (rtac preal_sup_set_lemma3 3); -by (rtac preal_sup_set_lemma4 5); -by Auto_tac; -qed "preal_sup"; - -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); -by (rtac preal_sup_set_lemma3_1 3); -by (rtac preal_sup_set_lemma4_1 5); -by Auto_tac; -qed "preal_sup1"; - -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] "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 "[| 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 "[| 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] "[| 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); -by (assume_tac 2); -by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def])); -qed "psup_le_ub"; - -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); -by (assume_tac 2); -by (auto_tac (claset() addSDs [bspec], - simpset() addsimps [preal_less_def,psubset_def,preal_le_def])); -qed "psup_le_ub1"; - -(** supremum property **) -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(), simpset() addsimps [psup_def,preal_less_def])); -by (cut_inst_tac [("r1.0","Xa"),("r2.0","Ya")] preal_linear 1); -by (auto_tac (claset() addDs [psubsetD],simpset() addsimps [preal_less_def])); -qed "preal_complete"; - -(****)(****)(****)(****)(****)(****)(****)(****)(****)(****) - (****** Embedding ******) -(*** mapping from prat into preal ***) - -Goal "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1"; -by (dres_inst_tac [("x","z1 * qinv (z1 + z2)")] prat_mult_less2_mono1 1); -by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1); -qed "lemma_preal_rat_less"; - -Goal "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2"; -by (stac prat_add_commute 1); -by (dtac (prat_add_commute RS subst) 1); -by (etac lemma_preal_rat_less 1); -qed "lemma_preal_rat_less2"; - -Goalw [preal_of_prat_def,preal_add_def] - "preal_of_prat ((z1::prat) + z2) = \ -\ preal_of_prat z1 + preal_of_prat z2"; -by (res_inst_tac [("f","Abs_preal")] arg_cong 1); -by (auto_tac (claset() addIs [prat_add_less_mono], - simpset() addsimps [lemma_prat_less_set_mem_preal RS Abs_preal_inverse])); -by (res_inst_tac [("x","x*z1*qinv(z1+z2)")] exI 1 THEN rtac conjI 1); -by (etac lemma_preal_rat_less 1); -by (res_inst_tac [("x","x*z2*qinv(z1+z2)")] exI 1 THEN rtac conjI 1); -by (etac lemma_preal_rat_less2 1); -by (asm_full_simp_tac (simpset() addsimps [prat_add_mult_distrib RS sym, - prat_add_mult_distrib2 RS sym] @ prat_mult_ac) 1); -qed "preal_of_prat_add"; - -Goal "x < xa ==> x*z1*qinv(xa) < z1"; -by (dres_inst_tac [("x","z1 * qinv xa")] prat_mult_less2_mono1 1); -by (dtac (prat_mult_left_commute RS subst) 1); -by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1); -qed "lemma_preal_rat_less3"; - -Goal "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2"; -by (dres_inst_tac [("x","z2 * qinv(z1*z2)")] prat_mult_less2_mono1 1); -by (dtac (prat_mult_left_commute RS subst) 1); -by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1); -qed "lemma_preal_rat_less4"; - -Goalw [preal_of_prat_def,preal_mult_def] - "preal_of_prat ((z1::prat) * z2) = \ -\ preal_of_prat z1 * preal_of_prat z2"; -by (res_inst_tac [("f","Abs_preal")] arg_cong 1); -by (auto_tac (claset() addIs [prat_mult_less_mono], - simpset() addsimps [lemma_prat_less_set_mem_preal RS Abs_preal_inverse])); -by (dtac prat_dense 1); -by (Step_tac 1); -by (res_inst_tac [("x","x*z1*qinv(xa)")] exI 1 THEN rtac conjI 1); -by (etac lemma_preal_rat_less3 1); -by (res_inst_tac [("x"," xa*z2*qinv(z1*z2)")] exI 1 THEN rtac conjI 1); -by (etac lemma_preal_rat_less4 1); -by (asm_full_simp_tac (simpset() - addsimps [qinv_mult_eq RS sym] @ prat_mult_ac) 1); -by (asm_full_simp_tac (simpset() - addsimps [prat_mult_assoc RS sym]) 1); -qed "preal_of_prat_mult"; - -Goalw [preal_of_prat_def,preal_less_def] - "(preal_of_prat p < preal_of_prat q) = (p < q)"; -by (auto_tac (claset() addSDs [lemma_prat_set_eq] addEs [prat_less_trans], - simpset() addsimps [lemma_prat_less_set_mem_preal, - psubset_def,prat_less_not_refl])); -by (res_inst_tac [("q1.0","p"),("q2.0","q")] prat_linear_less2 1); -by (auto_tac (claset() addIs [prat_less_irrefl],simpset())); -qed "preal_of_prat_less_iff"; - -Addsimps [preal_of_prat_less_iff]; diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Real/PReal.thy --- a/src/HOL/Real/PReal.thy Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Real/PReal.thy Thu Jan 01 21:47:07 2004 +0100 @@ -3,41 +3,1303 @@ Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Description : The positive reals as Dedekind sections of positive - rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] + rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] provides some of the definitions. *) -PReal = PRat + +theory PReal = PRat: typedef preal = "{A::prat set. {} < A & A < UNIV & - (!y: A. ((!z. z < y --> z: A) & - (? u: A. y < u)))}" (preal_1) -instance - preal :: {ord, plus, times} + (\y \ A. ((\z. z < y --> z \ A) & + (\u \ A. y < u)))}" +apply (rule exI) +apply (rule preal_1) +done + + +instance preal :: ord .. +instance preal :: plus .. +instance preal :: times .. + constdefs - preal_of_prat :: prat => preal + preal_of_prat :: "prat => preal" "preal_of_prat q == Abs_preal({x::prat. x < q})" - pinv :: preal => preal - "pinv(R) == Abs_preal({w. ? y. w < y & qinv y ~: Rep_preal(R)})" + pinv :: "preal => preal" + "pinv(R) == Abs_preal({w. \y. w < y & qinv y \ Rep_preal(R)})" - psup :: preal set => preal - "psup(P) == Abs_preal({w. ? X: P. w: Rep_preal(X)})" + psup :: "preal set => preal" + "psup(P) == Abs_preal({w. \X \ P. w \ Rep_preal(X)})" -defs +defs (overloaded) - preal_add_def - "R + S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x + y})" + preal_add_def: + "R + S == Abs_preal({w. \x \ Rep_preal(R). \y \ Rep_preal(S). w = x + y})" - preal_mult_def - "R * S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x * y})" + preal_mult_def: + "R * S == Abs_preal({w. \x \ Rep_preal(R). \y \ Rep_preal(S). w = x * y})" - preal_less_def + preal_less_def: "R < (S::preal) == Rep_preal(R) < Rep_preal(S)" - preal_le_def - "R <= (S::preal) == Rep_preal(R) <= Rep_preal(S)" - + preal_le_def: + "R \ (S::preal) == Rep_preal(R) \ Rep_preal(S)" + + +lemma inj_on_Abs_preal: "inj_on Abs_preal preal" +apply (rule inj_on_inverseI) +apply (erule Abs_preal_inverse) +done + +declare inj_on_Abs_preal [THEN inj_on_iff, simp] + +lemma inj_Rep_preal: "inj(Rep_preal)" +apply (rule inj_on_inverseI) +apply (rule Rep_preal_inverse) +done + +lemma empty_not_mem_preal [simp]: "{} \ preal" +by (unfold preal_def, fast) + +lemma one_set_mem_preal: "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} \ preal" +apply (unfold preal_def) +apply (rule preal_1) +done + +declare one_set_mem_preal [simp] + +lemma preal_psubset_empty: "x \ preal ==> {} < x" +by (unfold preal_def, fast) + +lemma Rep_preal_psubset_empty: "{} < Rep_preal x" +by (rule Rep_preal [THEN preal_psubset_empty]) + +lemma mem_Rep_preal_Ex: "\x. x \ Rep_preal X" +apply (cut_tac x = X in Rep_preal_psubset_empty) +apply (auto intro: equals0I [symmetric] simp add: psubset_def) +done + +lemma prealI1: + "[| {} < A; A < UNIV; + (\y \ A. ((\z. z < y --> z \ A) & + (\u \ A. y < u))) |] ==> A \ preal" +apply (unfold preal_def, fast) +done + +lemma prealI2: + "[| {} < A; A < UNIV; + \y \ A. (\z. z < y --> z \ A); + \y \ A. (\u \ A. y < u) |] ==> A \ preal" + +apply (unfold preal_def, best) +done + +lemma prealE_lemma: + "A \ preal ==> {} < A & A < UNIV & + (\y \ A. ((\z. z < y --> z \ A) & + (\u \ A. y < u)))" +apply (unfold preal_def, fast) +done + +declare prealI1 [intro!] prealI2 [intro!] + +declare Abs_preal_inverse [simp] + + +lemma prealE_lemma1: "A \ preal ==> {} < A" +by (unfold preal_def, fast) + +lemma prealE_lemma2: "A \ preal ==> A < UNIV" +by (unfold preal_def, fast) + +lemma prealE_lemma3: "A \ preal ==> \y \ A. (\z. z < y --> z \ A)" +by (unfold preal_def, fast) + +lemma prealE_lemma3a: "[| A \ preal; y \ A |] ==> (\z. z < y --> z \ A)" +by (fast dest!: prealE_lemma3) + +lemma prealE_lemma3b: "[| A \ preal; y \ A; z < y |] ==> z \ A" +by (fast dest!: prealE_lemma3a) + +lemma prealE_lemma4: "A \ preal ==> \y \ A. (\u \ A. y < u)" +by (unfold preal_def, fast) + +lemma prealE_lemma4a: "[| A \ preal; y \ A |] ==> \u \ A. y < u" +by (fast dest!: prealE_lemma4) + +lemma not_mem_Rep_preal_Ex: "\x. x\ Rep_preal X" +apply (cut_tac x = X in Rep_preal) +apply (drule prealE_lemma2) +apply (auto simp add: psubset_def) +done + + +subsection{*@{term preal_of_prat}: the Injection from prat to preal*} + +text{*A few lemmas*} + +lemma lemma_prat_less_set_mem_preal: "{u::prat. u < y} \ preal" +apply (cut_tac qless_Ex) +apply (auto intro: prat_less_trans elim!: prat_less_irrefl) +apply (blast dest: prat_dense) +done + +lemma lemma_prat_set_eq: "{u::prat. u < x} = {x. x < y} ==> x = y" +apply (insert prat_linear [of x y], safe) +apply (drule_tac [2] prat_dense, erule_tac [2] exE) +apply (drule prat_dense, erule exE) +apply (blast dest: prat_less_not_sym) +apply (blast dest: prat_less_not_sym) +done + +lemma inj_preal_of_prat: "inj(preal_of_prat)" +apply (rule inj_onI) +apply (unfold preal_of_prat_def) +apply (drule inj_on_Abs_preal [THEN inj_onD]) +apply (rule lemma_prat_less_set_mem_preal) +apply (rule lemma_prat_less_set_mem_preal) +apply (erule lemma_prat_set_eq) +done + + +subsection{*Theorems for Ordering*} + +text{*A positive fraction not in a positive real is an upper bound. + Gleason p. 122 - Remark (1)*} + +lemma not_in_preal_ub: "x \ Rep_preal(R) ==> \y \ Rep_preal(R). y < x" +apply (cut_tac x1 = R in Rep_preal [THEN prealE_lemma]) +apply (blast intro: not_less_not_eq_prat_less) +done + + +text{*@{text preal_less} is a strict order: nonreflexive and transitive *} + +lemma preal_less_not_refl: "~ (x::preal) < x" +apply (unfold preal_less_def) +apply (simp (no_asm) add: psubset_def) +done + +lemmas preal_less_irrefl = preal_less_not_refl [THEN notE, standard] + +lemma preal_not_refl2: "!!(x::preal). x < y ==> x \ y" +by (auto simp add: preal_less_not_refl) + +lemma preal_less_trans: "!!(x::preal). [| x < y; y < z |] ==> x < z" +apply (unfold preal_less_def) +apply (auto dest: subsetD equalityI simp add: psubset_def) +done + +lemma preal_less_not_sym: "!! (q1::preal). q1 < q2 ==> ~ q2 < q1" +apply (rule notI) +apply (drule preal_less_trans, assumption) +apply (simp add: preal_less_not_refl) +done + +(* [| x < y; ~P ==> y < x |] ==> P *) +lemmas preal_less_asym = preal_less_not_sym [THEN contrapos_np, standard] + +lemma preal_linear: + "(x::preal) < y | x = y | y < x" +apply (unfold preal_less_def) +apply (auto dest!: inj_Rep_preal [THEN injD] simp add: psubset_def) +apply (rule prealE_lemma3b, rule Rep_preal, assumption) +apply (fast dest: not_in_preal_ub) +done + + +subsection{*Properties of Addition*} + +lemma preal_add_commute: "(x::preal) + y = y + x" +apply (unfold preal_add_def) +apply (rule_tac f = Abs_preal in arg_cong) +apply (blast intro: prat_add_commute [THEN subst]) +done + +text{*Addition of two positive reals gives a positive real*} + +text{*Lemmas for proving positive reals addition set in @{typ preal}*} + +text{*Part 1 of Dedekind sections definition*} +lemma preal_add_set_not_empty: + "{} < {w. \x \ Rep_preal R. \y \ Rep_preal S. w = x + y}" +apply (cut_tac mem_Rep_preal_Ex mem_Rep_preal_Ex) +apply (auto intro!: psubsetI) +done + +text{*Part 2 of Dedekind sections definition*} +lemma preal_not_mem_add_set_Ex: + "\q. q \ {w. \x \ Rep_preal R. \y \ Rep_preal S. w = x + y}" +apply (cut_tac X = R in not_mem_Rep_preal_Ex) +apply (cut_tac X = S in not_mem_Rep_preal_Ex, clarify) +apply (drule not_in_preal_ub)+ +apply (rule_tac x = "x+xa" in exI) +apply (auto dest!: bspec) +apply (drule prat_add_less_mono) +apply (auto simp add: prat_less_not_refl) +done + +lemma preal_add_set_not_prat_set: + "{w. \x \ Rep_preal R. \y \ Rep_preal S. w = x + y} < UNIV" +apply (auto intro!: psubsetI) +apply (cut_tac R = R and S = S in preal_not_mem_add_set_Ex, auto) +done + +text{*Part 3 of Dedekind sections definition*} +lemma preal_add_set_lemma3: + "\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}" +apply auto +apply (frule prat_mult_qinv_less_1) +apply (frule_tac x = x + in prat_mult_less2_mono1 [of _ "prat_of_pnat (Abs_pnat (Suc 0))"]) +apply (frule_tac x = ya + in prat_mult_less2_mono1 [of _ "prat_of_pnat (Abs_pnat (Suc 0))"]) +apply simp +apply (drule Rep_preal [THEN prealE_lemma3a])+ +apply (erule allE)+ +apply auto +apply (rule bexI)+ +apply (auto simp add: prat_add_mult_distrib2 [symmetric] + prat_add_assoc [symmetric] prat_mult_assoc) +done + +lemma preal_add_set_lemma4: + "\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" +apply auto +apply (drule Rep_preal [THEN prealE_lemma4a]) +apply (auto intro: prat_add_less2_mono1) +done + +lemma preal_mem_add_set: + "{w. \x \ Rep_preal R. \y \ Rep_preal S. w = x + y} \ preal" +apply (rule prealI2) +apply (rule preal_add_set_not_empty) +apply (rule preal_add_set_not_prat_set) +apply (rule preal_add_set_lemma3) +apply (rule preal_add_set_lemma4) +done + +lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)" +apply (unfold preal_add_def) +apply (rule_tac f = Abs_preal in arg_cong) +apply (simp (no_asm) add: preal_mem_add_set [THEN Abs_preal_inverse]) +apply (auto simp add: prat_add_ac) +apply (rule bexI) +apply (auto intro!: exI simp add: prat_add_ac) +done + +lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)" + apply (rule mk_left_commute [of "op +"]) + apply (rule preal_add_assoc) + apply (rule preal_add_commute) + done + +(* Positive Reals addition is an AC operator *) +lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute + + +subsection{*Properties of Multiplication*} + +text{*Proofs essentially same as for addition*} + +lemma preal_mult_commute: "(x::preal) * y = y * x" +apply (unfold preal_mult_def) +apply (rule_tac f = Abs_preal in arg_cong) +apply (blast intro: prat_mult_commute [THEN subst]) +done + +text{*Multiplication of two positive reals gives a positive real.} + +text{*Lemmas for proving positive reals multiplication set in @{typ preal}*} + +text{*Part 1 of Dedekind sections definition*} +lemma preal_mult_set_not_empty: + "{} < {w. \x \ Rep_preal R. \y \ Rep_preal S. w = x * y}" +apply (cut_tac mem_Rep_preal_Ex mem_Rep_preal_Ex) +apply (auto intro!: psubsetI) +done + +text{*Part 2 of Dedekind sections definition*} +lemma preal_not_mem_mult_set_Ex: + "\q. q \ {w. \x \ Rep_preal R. \y \ Rep_preal S. w = x * y}" +apply (cut_tac X = R in not_mem_Rep_preal_Ex) +apply (cut_tac X = S in not_mem_Rep_preal_Ex) +apply (erule exE)+ +apply (drule not_in_preal_ub)+ +apply (rule_tac x = "x*xa" in exI) +apply (auto, (erule ballE)+, auto) +apply (drule prat_mult_less_mono) +apply (auto simp add: prat_less_not_refl) +done + +lemma preal_mult_set_not_prat_set: + "{w. \x \ Rep_preal R. \y \ Rep_preal S. w = x * y} < UNIV" +apply (auto intro!: psubsetI) +apply (cut_tac R = R and S = S in preal_not_mem_mult_set_Ex, auto) +done + +text{*Part 3 of Dedekind sections definition*} +lemma preal_mult_set_lemma3: + "\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}" +apply auto +apply (frule_tac x = "qinv (ya)" in prat_mult_left_less2_mono1) +apply (simp add: prat_mult_ac) +apply (drule Rep_preal [THEN prealE_lemma3a]) +apply (erule allE) +apply (rule bexI)+ +apply (auto simp add: prat_mult_assoc) +done + +lemma preal_mult_set_lemma4: + "\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" +apply auto +apply (drule Rep_preal [THEN prealE_lemma4a]) +apply (auto intro: prat_mult_less2_mono1) +done + +lemma preal_mem_mult_set: + "{w. \x \ Rep_preal R. \y \ Rep_preal S. w = x * y} \ preal" +apply (rule prealI2) +apply (rule preal_mult_set_not_empty) +apply (rule preal_mult_set_not_prat_set) +apply (rule preal_mult_set_lemma3) +apply (rule preal_mult_set_lemma4) +done + +lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)" +apply (unfold preal_mult_def) +apply (rule_tac f = Abs_preal in arg_cong) +apply (simp (no_asm) add: preal_mem_mult_set [THEN Abs_preal_inverse]) +apply (auto simp add: prat_mult_ac) +apply (rule bexI) +apply (auto intro!: exI simp add: prat_mult_ac) +done + +lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)" + apply (rule mk_left_commute [of "op *"]) + apply (rule preal_mult_assoc) + apply (rule preal_mult_commute) + done + +(* Positive Reals multiplication is an AC operator *) +lemmas preal_mult_ac = + preal_mult_assoc preal_mult_commute preal_mult_left_commute + +(* Positive Real 1 is the multiplicative identity element *) +(* long *) +lemma preal_mult_1: + "(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) * z = z" +apply (unfold preal_of_prat_def preal_mult_def) +apply (rule Rep_preal_inverse [THEN subst]) +apply (rule_tac f = Abs_preal in arg_cong) +apply (rule one_set_mem_preal [THEN Abs_preal_inverse, THEN ssubst]) +apply (auto simp add: Rep_preal_inverse) +apply (drule Rep_preal [THEN prealE_lemma4a]) +apply (erule bexE) +apply (drule prat_mult_less_mono) +apply (auto dest: Rep_preal [THEN prealE_lemma3a]) +apply (frule Rep_preal [THEN prealE_lemma4a]) +apply (erule bexE) +apply (frule_tac x = "qinv (u)" in prat_mult_less2_mono1) +apply (rule exI, auto, rule_tac x = u in bexI) +apply (auto simp add: prat_mult_assoc) +done + +lemma preal_mult_1_right: + "z * (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) = z" +apply (rule preal_mult_commute [THEN subst]) +apply (rule preal_mult_1) +done + + +subsection{*Distribution of Multiplication across Addition*} + +lemma mem_Rep_preal_addD: + "z \ Rep_preal(R+S) ==> + \x \ Rep_preal(R). \y \ Rep_preal(S). z = x + y" +apply (unfold preal_add_def) +apply (drule preal_mem_add_set [THEN Abs_preal_inverse, THEN subst], fast) +done + +lemma mem_Rep_preal_addI: + "\x \ Rep_preal(R). \y \ Rep_preal(S). z = x + y + ==> z \ Rep_preal(R+S)" +apply (unfold preal_add_def) +apply (rule preal_mem_add_set [THEN Abs_preal_inverse, THEN ssubst], fast) +done + +lemma mem_Rep_preal_add_iff: + "(z \ Rep_preal(R+S)) = (\x \ Rep_preal(R). + \y \ Rep_preal(S). z = x + y)" +apply (fast intro!: mem_Rep_preal_addD mem_Rep_preal_addI) +done + +lemma mem_Rep_preal_multD: + "z \ Rep_preal(R*S) ==> + \x \ Rep_preal(R). \y \ Rep_preal(S). z = x * y" +apply (unfold preal_mult_def) +apply (drule preal_mem_mult_set [THEN Abs_preal_inverse, THEN subst], fast) +done + +lemma mem_Rep_preal_multI: + "\x \ Rep_preal(R). \y \ Rep_preal(S). z = x * y + ==> z \ Rep_preal(R*S)" +apply (unfold preal_mult_def) +apply (rule preal_mem_mult_set [THEN Abs_preal_inverse, THEN ssubst], fast) +done + +lemma mem_Rep_preal_mult_iff: + "(z \ Rep_preal(R*S)) = + (\x \ Rep_preal(R). \y \ Rep_preal(S). z = x * y)" +by (fast intro!: mem_Rep_preal_multD mem_Rep_preal_multI) + +lemma lemma_add_mult_mem_Rep_preal: + "[| xb \ Rep_preal z1; xc \ Rep_preal z2; ya: + Rep_preal w; yb \ Rep_preal w |] ==> + xb * ya + xc * yb \ Rep_preal (z1 * w + z2 * w)" +by (fast intro: mem_Rep_preal_addI mem_Rep_preal_multI) + +lemma lemma_add_mult_mem_Rep_preal1: + "[| xb \ Rep_preal z1; xc \ Rep_preal z2; ya: + Rep_preal w; yb \ Rep_preal w |] ==> + yb*(xb + xc) \ Rep_preal (w*(z1 + z2))" +by (fast intro: mem_Rep_preal_addI mem_Rep_preal_multI) + +lemma lemma_preal_add_mult_distrib: + "x \ Rep_preal (w * z1 + w * z2) ==> + x \ Rep_preal (w * (z1 + z2))" +apply (auto dest!: mem_Rep_preal_addD mem_Rep_preal_multD) +apply (frule_tac ya = xa and yb = xb and xb = ya and xc = yb in lemma_add_mult_mem_Rep_preal1, auto) +apply (rule_tac x = xa and y = xb in prat_linear_less2) +apply (drule_tac b = ya and c = yb in lemma_prat_add_mult_mono) +apply (rule Rep_preal [THEN prealE_lemma3b]) +apply (auto simp add: prat_add_mult_distrib2) +apply (drule_tac ya = xb and yb = xa and xc = ya and xb = yb in lemma_add_mult_mem_Rep_preal1, auto) +apply (drule_tac b = yb and c = ya in lemma_prat_add_mult_mono) +apply (rule Rep_preal [THEN prealE_lemma3b]) +apply (erule_tac V = "xb * ya + xb * yb \ Rep_preal (w * (z1 + z2))" in thin_rl) +apply (auto simp add: prat_add_mult_distrib prat_add_commute preal_add_ac) +done + +lemma lemma_preal_add_mult_distrib2: + "x \ Rep_preal (w * (z1 + z2)) ==> + x \ Rep_preal (w * z1 + w * z2)" +by (auto dest!: mem_Rep_preal_addD mem_Rep_preal_multD + intro!: bexI mem_Rep_preal_addI mem_Rep_preal_multI + simp add: prat_add_mult_distrib2) + +lemma preal_add_mult_distrib2: "(w * ((z1::preal) + z2)) = (w * z1) + (w * z2)" +apply (rule inj_Rep_preal [THEN injD]) +apply (fast intro: lemma_preal_add_mult_distrib lemma_preal_add_mult_distrib2) +done + +lemma preal_add_mult_distrib: "(((z1::preal) + z2) * w) = (z1 * w) + (z2 * w)" +apply (simp (no_asm) add: preal_mult_commute preal_add_mult_distrib2) +done + + +subsection{*Existence of Inverse, a Positive Real*} + +lemma qinv_not_mem_Rep_preal_Ex: "\y. qinv(y) \ Rep_preal X" +apply (cut_tac X = X in not_mem_Rep_preal_Ex) +apply (erule exE, cut_tac x = x in prat_as_inverse_ex, auto) +done + +lemma lemma_preal_mem_inv_set_ex: + "\q. q \ {x. \y. x < y & qinv y \ Rep_preal A}" +apply (cut_tac X = A in qinv_not_mem_Rep_preal_Ex, auto) +apply (cut_tac y = y in qless_Ex, fast) +done + +text{*Part 1 of Dedekind sections definition*} +lemma preal_inv_set_not_empty: "{} < {x. \y. x < y & qinv y \ Rep_preal A}" +apply (cut_tac lemma_preal_mem_inv_set_ex) +apply (auto intro!: psubsetI) +done + +text{*Part 2 of Dedekind sections definition*} +lemma qinv_mem_Rep_preal_Ex: "\y. qinv(y) \ Rep_preal X" +apply (cut_tac X = X in mem_Rep_preal_Ex) +apply (erule exE, cut_tac x = x in prat_as_inverse_ex, auto) +done + +lemma preal_not_mem_inv_set_Ex: + "\x. x \ {x. \y. x < y & qinv y \ Rep_preal A}" +apply (rule ccontr) +apply (cut_tac X = A in qinv_mem_Rep_preal_Ex, auto) +apply (erule allE, clarify) +apply (drule qinv_prat_less, drule not_in_preal_ub) +apply (erule_tac x = "qinv y" in ballE) +apply (drule prat_less_trans) +apply (auto simp add: prat_less_not_refl) +done + +lemma preal_inv_set_not_prat_set: + "{x. \y. x < y & qinv y \ Rep_preal A} < UNIV" +apply (auto intro!: psubsetI) +apply (cut_tac A = A in preal_not_mem_inv_set_Ex, auto) +done + +text{*Part 3 of Dedekind sections definition*} +lemma preal_inv_set_lemma3: + "\y \ {x. \y. x < y & qinv y \ Rep_preal A}. + \z. z < y --> z \ {x. \y. x < y & qinv y \ Rep_preal A}" +apply auto +apply (rule_tac x = ya in exI) +apply (auto intro: prat_less_trans) +done + +lemma preal_inv_set_lemma4: + "\y \ {x. \y. x < y & qinv y \ Rep_preal A}. + Bex {x. \y. x < y & qinv y \ Rep_preal A} (op < y)" +by (blast dest: prat_dense) + +lemma preal_mem_inv_set: "{x. \y. x < y & qinv(y) \ Rep_preal(A)} \ preal" +apply (rule prealI2) +apply (rule preal_inv_set_not_empty) +apply (rule preal_inv_set_not_prat_set) +apply (rule preal_inv_set_lemma3) +apply (rule preal_inv_set_lemma4) +done + +(*more lemmas for inverse *) +lemma preal_mem_mult_invD: + "x \ Rep_preal(pinv(A)*A) ==> + x \ Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))" +apply (auto dest!: mem_Rep_preal_multD simp add: pinv_def preal_of_prat_def) +apply (drule preal_mem_inv_set [THEN Abs_preal_inverse, THEN subst]) +apply (auto dest!: not_in_preal_ub) +apply (drule prat_mult_less_mono, blast, auto) +done + +subsection{*Gleason's Lemma 9-3.4, page 122*} + +lemma lemma1_gleason9_34: + "\xa \ Rep_preal(A). xa + x \ Rep_preal(A) ==> + \xb \ Rep_preal(A). xb + (prat_of_pnat p)*x \ Rep_preal(A)" +apply (cut_tac mem_Rep_preal_Ex) +apply (induct_tac "p" rule: pnat_induct) +apply (auto simp add: pnat_one_def pSuc_is_plus_one prat_add_mult_distrib + prat_of_pnat_add prat_add_assoc [symmetric]) +done + +lemma lemma1b_gleason9_34: + "Abs_prat (ratrel `` {(y, z)}) < + xb + + Abs_prat (ratrel `` {(x*y, Abs_pnat (Suc 0))}) * + Abs_prat (ratrel `` {(w, x)})" +apply (rule_tac j = + "Abs_prat (ratrel `` + { (x * y, Abs_pnat (Suc 0))}) * Abs_prat (ratrel `` {(w, x)})" + in prat_le_less_trans) +apply (rule_tac [2] prat_self_less_add_right) +apply (auto intro: lemma_Abs_prat_le3 + simp add: prat_mult pre_lemma_gleason9_34b pnat_mult_assoc) +done + +lemma lemma_gleason9_34a: + "\xa \ Rep_preal(A). xa + x \ Rep_preal(A) ==> False" +apply (cut_tac X = A in not_mem_Rep_preal_Ex) +apply (erule exE) +apply (drule not_in_preal_ub) +apply (rule_tac z = x in eq_Abs_prat) +apply (rule_tac z = xa in eq_Abs_prat) +apply (drule_tac p = "y*xb" in lemma1_gleason9_34) +apply (erule bexE) +apply (cut_tac x = y and y = xb and w = xaa and z = ya and xb = xba in lemma1b_gleason9_34) +apply (drule_tac x = "xba + prat_of_pnat (y * xb) * x" in bspec) +apply (auto intro: prat_less_asym simp add: prat_of_pnat_def) +done + +lemma lemma_gleason9_34: "\r \ Rep_preal(R). r + x \ Rep_preal(R)" +apply (rule ccontr) +apply (blast intro: lemma_gleason9_34a) +done + + +subsection{*Gleason's Lemma 9-3.6*} + +lemma lemma1_gleason9_36: "r + r*qinv(xa)*Q3 = r*qinv(xa)*(xa + Q3)" +apply (simp (no_asm_use) add: prat_add_mult_distrib2 prat_mult_assoc) +done + +lemma lemma2_gleason9_36: "r*qinv(xa)*(xa*x) = r*x" +apply (simp (no_asm_use) add: prat_mult_ac) +done + +(*** FIXME: long! ***) +lemma lemma_gleason9_36: + "prat_of_pnat 1 < x ==> \r \ Rep_preal(A). r*x \ Rep_preal(A)" +apply (rule_tac X1 = A in mem_Rep_preal_Ex [THEN exE]) +apply (rule_tac Q = "xa*x \ Rep_preal (A) " in excluded_middle [THEN disjE]) +apply fast +apply (drule_tac x = xa in prat_self_less_mult_right) +apply (erule prat_lessE) +apply (cut_tac R = A and x = Q3 in lemma_gleason9_34) +apply (drule sym, auto) +apply (frule not_in_preal_ub) +apply (drule_tac x = "xa + Q3" in bspec, assumption) +apply (drule prat_add_right_less_cancel) +apply (drule_tac x = "qinv (xa) *Q3" in prat_mult_less2_mono1) +apply (drule_tac x = r in prat_add_less2_mono2) +apply (simp add: prat_mult_assoc [symmetric] lemma1_gleason9_36) +apply (drule sym) +apply (auto simp add: lemma2_gleason9_36) +apply (rule_tac x = r in bexI) +apply (rule notI) +apply (drule_tac y = "r*x" in Rep_preal [THEN prealE_lemma3b], auto) +done + +lemma lemma_gleason9_36a: + "prat_of_pnat (Abs_pnat (Suc 0)) < x ==> + \r \ Rep_preal(A). r*x \ Rep_preal(A)" +apply (rule lemma_gleason9_36) +apply (simp (no_asm_simp) add: pnat_one_def) +done + + +subsection{*Existence of Inverse: Part 2*} +lemma preal_mem_mult_invI: + "x \ Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) + ==> x \ Rep_preal(pinv(A)*A)" +apply (auto intro!: mem_Rep_preal_multI simp add: pinv_def preal_of_prat_def) +apply (rule preal_mem_inv_set [THEN Abs_preal_inverse, THEN ssubst]) +apply (drule prat_qinv_gt_1) +apply (drule_tac A = A in lemma_gleason9_36a, auto) +apply (drule Rep_preal [THEN prealE_lemma4a]) +apply (auto, drule qinv_prat_less) +apply (rule_tac x = "qinv (u) *x" in exI) +apply (rule conjI) +apply (rule_tac x = "qinv (r) *x" in exI) +apply (auto intro: prat_mult_less2_mono1 simp add: qinv_mult_eq qinv_qinv) +apply (rule_tac x = u in bexI) +apply (auto simp add: prat_mult_assoc prat_mult_left_commute) +done + +lemma preal_mult_inv: + "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))" +apply (rule inj_Rep_preal [THEN injD]) +apply (fast dest: preal_mem_mult_invD preal_mem_mult_invI) +done + +lemma preal_mult_inv_right: + "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))" +apply (rule preal_mult_commute [THEN subst]) +apply (rule preal_mult_inv) +done + + +text{*Theorems needing @{text lemma_gleason9_34}*} + +lemma Rep_preal_self_subset: "Rep_preal (R1) \ Rep_preal(R1 + R2)" +apply (cut_tac X = R2 in mem_Rep_preal_Ex) +apply (auto intro!: bexI + intro: Rep_preal [THEN prealE_lemma3b] prat_self_less_add_left + mem_Rep_preal_addI) +done + +lemma Rep_preal_sum_not_subset: "~ Rep_preal (R1 + R2) \ Rep_preal(R1)" +apply (cut_tac X = R2 in mem_Rep_preal_Ex) +apply (erule exE) +apply (cut_tac R = R1 in lemma_gleason9_34) +apply (auto intro: mem_Rep_preal_addI) +done + +lemma Rep_preal_sum_not_eq: "Rep_preal (R1 + R2) \ Rep_preal(R1)" +apply (rule notI) +apply (erule equalityE) +apply (simp add: Rep_preal_sum_not_subset) +done + +text{*at last, Gleason prop. 9-3.5(iii) page 123*} +lemma preal_self_less_add_left: "(R1::preal) < R1 + R2" +apply (unfold preal_less_def psubset_def) +apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym]) +done + +lemma preal_self_less_add_right: "(R1::preal) < R2 + R1" +apply (simp add: preal_add_commute preal_self_less_add_left) +done + + +subsection{*The @{text "\"} Ordering*} + +lemma preal_less_le_iff: "(~(w < z)) = (z \ (w::preal))" +apply (unfold preal_le_def psubset_def preal_less_def) +apply (insert preal_linear [of w z]) +apply (auto simp add: preal_less_def psubset_def) +done + +lemma preal_le_iff_less_or_eq: + "((x::preal) \ y) = (x < y | x = y)" +apply (unfold preal_le_def preal_less_def psubset_def) +apply (auto intro: inj_Rep_preal [THEN injD]) +done + +lemma preal_le_refl: "w \ (w::preal)" +apply (simp add: preal_le_def) +done + +lemma preal_le_trans: "[| i \ j; j \ k |] ==> i \ (k::preal)" +apply (simp add: preal_le_iff_less_or_eq) +apply (blast intro: preal_less_trans) +done + +lemma preal_le_anti_sym: "[| z \ w; w \ z |] ==> z = (w::preal)" +apply (simp add: preal_le_iff_less_or_eq) +apply (blast intro: preal_less_asym) +done + +lemma preal_neq_iff: "(w \ z) = (w z & w \ z)" +apply (simp (no_asm) add: preal_less_le_iff [symmetric] preal_neq_iff) +apply (blast elim!: preal_less_asym) +done + +instance preal :: order +proof qed + (assumption | + rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+ + +lemma preal_le_linear: "x <= y | y <= (x::preal)" +apply (insert preal_linear [of x y]) +apply (auto simp add: order_less_le) +done + +instance preal :: linorder + by (intro_classes, rule preal_le_linear) + + +subsection{*Gleason prop. 9-3.5(iv), page 123*} + +text{*Proving @{term "A < B ==> \D. A + D = B"}*} + +text{*Define the claimed D and show that it is a positive real*} + +text{*Part 1 of Dedekind sections definition*} +lemma lemma_ex_mem_less_left_add1: + "A < B ==> + \q. q \ {d. \n. n \ Rep_preal(A) & n + d \ Rep_preal(B)}" +apply (unfold preal_less_def psubset_def) +apply (clarify) +apply (drule_tac x1 = B in Rep_preal [THEN prealE_lemma4a]) +apply (auto simp add: prat_less_def) +done + +lemma preal_less_set_not_empty: + "A < B ==> {} < {d. \n. n \ Rep_preal(A) & n + d \ Rep_preal(B)}" +apply (drule lemma_ex_mem_less_left_add1) +apply (auto intro!: psubsetI) +done + +text{*Part 2 of Dedekind sections definition*} +lemma lemma_ex_not_mem_less_left_add1: + "\q. q \ {d. \n. n \ Rep_preal(A) & n + d \ Rep_preal(B)}" +apply (cut_tac X = B in not_mem_Rep_preal_Ex) +apply (erule exE) +apply (rule_tac x = x in exI, auto) +apply (cut_tac x = x and y = n in prat_self_less_add_right) +apply (auto dest: Rep_preal [THEN prealE_lemma3b]) +done + +lemma preal_less_set_not_prat_set: + "{d. \n. n \ Rep_preal(A) & n + d \ Rep_preal(B)} < UNIV" +apply (auto intro!: psubsetI) +apply (cut_tac A = A and B = B in lemma_ex_not_mem_less_left_add1, auto) +done + +text{*Part 3 of Dedekind sections definition*} +lemma preal_less_set_lemma3: + "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)}" +apply auto +apply (drule_tac x = n in prat_add_less2_mono2) +apply (drule Rep_preal [THEN prealE_lemma3b], auto) +done + +lemma preal_less_set_lemma4: + "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)" +apply auto +apply (drule Rep_preal [THEN prealE_lemma4a]) +apply (auto simp add: prat_less_def prat_add_assoc) +done + +lemma preal_mem_less_set: + "!! (A::preal). A < B ==> + {d. \n. n \ Rep_preal(A) & n + d \ Rep_preal(B)}: preal" +apply (rule prealI2) +apply (rule preal_less_set_not_empty) +apply (rule_tac [2] preal_less_set_not_prat_set) +apply (rule_tac [2] preal_less_set_lemma3) +apply (rule_tac [3] preal_less_set_lemma4, auto) +done + +text{*proving that @{term "A + D \ B"}*} +lemma preal_less_add_left_subsetI: + "!! (A::preal). A < B ==> + A + Abs_preal({d. \n. n \ Rep_preal(A) & n + d \ Rep_preal(B)}) \ B" +apply (unfold preal_le_def) +apply (rule subsetI) +apply (drule mem_Rep_preal_addD) +apply (auto simp add: preal_mem_less_set [THEN Abs_preal_inverse]) +apply (drule not_in_preal_ub) +apply (drule bspec, assumption) +apply (drule_tac x = y in prat_add_less2_mono1) +apply (drule_tac x1 = B in Rep_preal [THEN prealE_lemma3b], auto) +done + +subsection{*proving that @{term "B \ A + D"} --- trickier*} + +lemma lemma_sum_mem_Rep_preal_ex: + "x \ Rep_preal(B) ==> \e. x + e \ Rep_preal(B)" +apply (drule Rep_preal [THEN prealE_lemma4a]) +apply (auto simp add: prat_less_def) +done + +lemma preal_less_add_left_subsetI2: + "!! (A::preal). A < B ==> + B \ A + Abs_preal({d. \n. n \ Rep_preal(A) & n + d \ Rep_preal(B)})" +apply (unfold preal_le_def) +apply (rule subsetI) +apply (rule_tac Q = "x \ Rep_preal (A) " in excluded_middle [THEN disjE]) +apply (rule mem_Rep_preal_addI) +apply (drule lemma_sum_mem_Rep_preal_ex) +apply (erule exE) +apply (cut_tac R = A and x = e in lemma_gleason9_34, erule bexE) +apply (drule not_in_preal_ub, drule bspec, assumption) +apply (erule prat_lessE) +apply (rule_tac x = r in bexI) +apply (rule_tac x = Q3 in bexI) +apply (cut_tac [4] Rep_preal_self_subset) +apply (auto simp add: preal_mem_less_set [THEN Abs_preal_inverse]) +apply (rule_tac x = "r+e" in exI) +apply (simp add: prat_add_ac) +done + +(*** required proof ***) +lemma preal_less_add_left: + "!! (A::preal). A < B ==> + A + Abs_preal({d. \n. n \ Rep_preal(A) & n + d \ Rep_preal(B)}) = B" +apply (blast intro: preal_le_anti_sym preal_less_add_left_subsetI preal_less_add_left_subsetI2) +done + +lemma preal_less_add_left_Ex: "!! (A::preal). A < B ==> \D. A + D = B" +by (fast dest: preal_less_add_left) + +lemma preal_add_less2_mono1: "!!(A::preal). A < B ==> A + C < B + C" +apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_assoc) +apply (rule_tac y1 = D in preal_add_commute [THEN subst]) +apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric]) +done + +lemma preal_add_less2_mono2: "!!(A::preal). A < B ==> C + A < C + B" +by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute) + +lemma preal_mult_less_mono1: + "!!(q1::preal). q1 < q2 ==> q1 * x < q2 * x" +apply (drule preal_less_add_left_Ex) +apply (auto simp add: preal_add_mult_distrib preal_self_less_add_left) +done + +lemma preal_mult_left_less_mono1: "!!(q1::preal). q1 < q2 ==> x * q1 < x * q2" +by (auto dest: preal_mult_less_mono1 simp add: preal_mult_commute) + +lemma preal_mult_left_le_mono1: "!!(q1::preal). q1 \ q2 ==> x * q1 \ x * q2" +apply (simp add: preal_le_iff_less_or_eq) +apply (blast intro!: preal_mult_left_less_mono1) +done + +lemma preal_mult_le_mono1: "!!(q1::preal). q1 \ q2 ==> q1 * x \ q2 * x" +by (auto dest: preal_mult_left_le_mono1 simp add: preal_mult_commute) + +lemma preal_add_left_le_mono1: "!!(q1::preal). q1 \ q2 ==> x + q1 \ x + q2" +apply (simp add: preal_le_iff_less_or_eq) +apply (auto intro!: preal_add_less2_mono1 simp add: preal_add_commute) +done + +lemma preal_add_le_mono1: "!!(q1::preal). q1 \ q2 ==> q1 + x \ q2 + x" +by (auto dest: preal_add_left_le_mono1 simp add: preal_add_commute) + +lemma preal_add_right_less_cancel: "!!(A::preal). A + C < B + C ==> A < B" +apply (cut_tac preal_linear) +apply (auto elim: preal_less_irrefl) +apply (drule_tac A = B and C = C in preal_add_less2_mono1) +apply (fast dest: preal_less_trans elim: preal_less_irrefl) +done + +lemma preal_add_left_less_cancel: "!!(A::preal). C + A < C + B ==> A < B" +by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute) + +lemma preal_add_less_iff1 [simp]: "((A::preal) + C < B + C) = (A < B)" +by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel) + +lemma preal_add_less_iff2 [simp]: "(C + (A::preal) < C + B) = (A < B)" +by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel) + +lemma preal_add_less_mono: + "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)" +apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_ac) +apply (rule preal_add_assoc [THEN subst]) +apply (rule preal_self_less_add_right) +done + +lemma preal_mult_less_mono: + "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)" +apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_mult_distrib preal_add_mult_distrib2 preal_self_less_add_left preal_add_assoc preal_mult_ac) +done + +lemma preal_add_right_cancel: "(A::preal) + C = B + C ==> A = B" +apply (cut_tac preal_linear [of A B], safe) +apply (drule_tac [!] C = C in preal_add_less2_mono1) +apply (auto elim: preal_less_irrefl) +done + +lemma preal_add_left_cancel: "!!(A::preal). C + A = C + B ==> A = B" +by (auto intro: preal_add_right_cancel simp add: preal_add_commute) + +lemma preal_add_left_cancel_iff [simp]: "(C + A = C + B) = ((A::preal) = B)" +by (fast intro: preal_add_left_cancel) + +lemma preal_add_right_cancel_iff [simp]: "(A + C = B + C) = ((A::preal) = B)" +by (fast intro: preal_add_right_cancel) + + + +subsection{*Completeness of type @{typ preal}*} + +text{*Prove that supremum is a cut*} + +lemma preal_sup_mem_Ex: + "\X. X \ P ==> \q. q \ {w. \X. X \ P & w \ Rep_preal X}" +apply safe +apply (cut_tac X = X in mem_Rep_preal_Ex, auto) +done + +text{*Part 1 of Dedekind sections definition*} +lemma preal_sup_set_not_empty: + "\(X::preal). X \ P ==> + {} < {w. \X \ P. w \ Rep_preal X}" +apply (drule preal_sup_mem_Ex) +apply (auto intro!: psubsetI) +done + +text{*Part 2 of Dedekind sections definition*} +lemma preal_sup_not_mem_Ex: + "\Y. (\X \ P. X < Y) + ==> \q. q \ {w. \X. X \ P & w \ Rep_preal(X)}" +apply (unfold preal_less_def) +apply (auto simp add: psubset_def) +apply (cut_tac X = Y in not_mem_Rep_preal_Ex) +apply (erule exE) +apply (rule_tac x = x in exI) +apply (auto dest!: bspec) +done + +lemma preal_sup_not_mem_Ex1: + "\Y. (\X \ P. X \ Y) + ==> \q. q \ {w. \X. X \ P & w \ Rep_preal(X)}" +apply (unfold preal_le_def, safe) +apply (cut_tac X = Y in not_mem_Rep_preal_Ex) +apply (erule exE) +apply (rule_tac x = x in exI) +apply (auto dest!: bspec) +done + +lemma preal_sup_set_not_prat_set: + "\Y. (\X \ P. X < Y) ==> {w. \X \ P. w \ Rep_preal(X)} < UNIV" +apply (drule preal_sup_not_mem_Ex) +apply (auto intro!: psubsetI) +done + +lemma preal_sup_set_not_prat_set1: + "\Y. (\X \ P. X \ Y) ==> {w. \X \ P. w \ Rep_preal(X)} < UNIV" +apply (drule preal_sup_not_mem_Ex1) +apply (auto intro!: psubsetI) +done + +text{*Part 3 of Dedekind sections definition*} +lemma preal_sup_set_lemma3: + "[|\(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}" +apply (auto elim: Rep_preal [THEN prealE_lemma3b]) +done + +lemma preal_sup_set_lemma3_1: + "[|\(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}" +apply (auto elim: Rep_preal [THEN prealE_lemma3b]) +done + +lemma preal_sup_set_lemma4: + "[|\(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)" +apply (blast dest: Rep_preal [THEN prealE_lemma4a]) +done + +lemma preal_sup_set_lemma4_1: + "[|\(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)" +apply (blast dest: Rep_preal [THEN prealE_lemma4a]) +done + +lemma preal_sup: + "[|\(X::preal). X \ P; \Y. (\X \ P. X < Y) |] + ==> {w. \X \ P. w \ Rep_preal(X)}: preal" +apply (rule prealI2) +apply (rule preal_sup_set_not_empty) +apply (rule_tac [2] preal_sup_set_not_prat_set) +apply (rule_tac [3] preal_sup_set_lemma3) +apply (rule_tac [5] preal_sup_set_lemma4, auto) +done + +lemma preal_sup1: + "[|\(X::preal). X \ P; \Y. (\X \ P. X \ Y) |] + ==> {w. \X \ P. w \ Rep_preal(X)}: preal" +apply (rule prealI2) +apply (rule preal_sup_set_not_empty) +apply (rule_tac [2] preal_sup_set_not_prat_set1) +apply (rule_tac [3] preal_sup_set_lemma3_1) +apply (rule_tac [5] preal_sup_set_lemma4_1, auto) +done + +lemma preal_psup_leI: "\Y. (\X \ P. X < Y) ==> \x \ P. x \ psup P" +apply (unfold psup_def) +apply (auto simp add: preal_le_def) +apply (rule preal_sup [THEN Abs_preal_inverse, THEN ssubst], auto) +done + +lemma preal_psup_leI2: "\Y. (\X \ P. X \ Y) ==> \x \ P. x \ psup P" +apply (unfold psup_def) +apply (auto simp add: preal_le_def) +apply (rule preal_sup1 [THEN Abs_preal_inverse, THEN ssubst]) +apply (auto simp add: preal_le_def) +done + +lemma preal_psup_leI2b: + "[| \Y. (\X \ P. X < Y); x \ P |] ==> x \ psup P" +apply (blast dest!: preal_psup_leI) +done + +lemma preal_psup_leI2a: + "[| \Y. (\X \ P. X \ Y); x \ P |] ==> x \ psup P" +apply (blast dest!: preal_psup_leI2) +done + +lemma psup_le_ub: "[| \X. X \ P; \X \ P. X < Y |] ==> psup P \ Y" +apply (unfold psup_def) +apply (auto simp add: preal_le_def) +apply (drule preal_sup [OF exI exI, THEN Abs_preal_inverse, THEN subst]) +apply (rotate_tac [2] 1) +prefer 2 apply assumption +apply (auto dest!: bspec simp add: preal_less_def psubset_def) +done + +lemma psup_le_ub1: "[| \X. X \ P; \X \ P. X \ Y |] ==> psup P \ Y" +apply (unfold psup_def) +apply (auto simp add: preal_le_def) +apply (drule preal_sup1 [OF exI exI, THEN Abs_preal_inverse, THEN subst]) +apply (rotate_tac [2] 1) +prefer 2 apply assumption +apply (auto dest!: bspec simp add: preal_less_def psubset_def preal_le_def) +done + +text{*Supremum property*} +lemma preal_complete: + "[|\(X::preal). X \ P; \Y. (\X \ P. X < Y) |] + ==> (\Y. (\X \ P. Y < X) = (Y < psup P))" +apply (frule preal_sup [THEN Abs_preal_inverse], fast) +apply (auto simp add: psup_def preal_less_def) +apply (cut_tac x = Xa and y = Ya in preal_linear) +apply (auto dest: psubsetD simp add: preal_less_def) +done + + +subsection{*The Embadding from @{typ prat} into @{typ preal}*} + +lemma lemma_preal_rat_less: "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1" +apply (drule_tac x = "z1 * qinv (z1 + z2) " in prat_mult_less2_mono1) +apply (simp add: prat_mult_ac) +done + +lemma lemma_preal_rat_less2: "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2" +apply (subst prat_add_commute) +apply (drule prat_add_commute [THEN subst]) +apply (erule lemma_preal_rat_less) +done + +lemma preal_of_prat_add: + "preal_of_prat ((z1::prat) + z2) = + preal_of_prat z1 + preal_of_prat z2" +apply (unfold preal_of_prat_def preal_add_def) +apply (rule_tac f = Abs_preal in arg_cong) +apply (auto intro: prat_add_less_mono + simp add: lemma_prat_less_set_mem_preal [THEN Abs_preal_inverse]) +apply (rule_tac x = "x*z1*qinv (z1+z2) " in exI, rule conjI) +apply (erule lemma_preal_rat_less) +apply (rule_tac x = "x*z2*qinv (z1+z2) " in exI, rule conjI) +apply (erule lemma_preal_rat_less2) +apply (simp add: prat_add_mult_distrib [symmetric] + prat_add_mult_distrib2 [symmetric] prat_mult_ac) +done + +lemma lemma_preal_rat_less3: "x < xa ==> x*z1*qinv(xa) < z1" +apply (drule_tac x = "z1 * qinv xa" in prat_mult_less2_mono1) +apply (drule prat_mult_left_commute [THEN subst]) +apply (simp add: prat_mult_ac) +done + +lemma lemma_preal_rat_less4: "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2" +apply (drule_tac x = "z2 * qinv (z1*z2) " in prat_mult_less2_mono1) +apply (drule prat_mult_left_commute [THEN subst]) +apply (simp add: prat_mult_ac) +done + +lemma preal_of_prat_mult: + "preal_of_prat ((z1::prat) * z2) = + preal_of_prat z1 * preal_of_prat z2" +apply (unfold preal_of_prat_def preal_mult_def) +apply (rule_tac f = Abs_preal in arg_cong) +apply (auto intro: prat_mult_less_mono + simp add: lemma_prat_less_set_mem_preal [THEN Abs_preal_inverse]) +apply (drule prat_dense, safe) +apply (rule_tac x = "x*z1*qinv (xa) " in exI, rule conjI) +apply (erule lemma_preal_rat_less3) +apply (rule_tac x = " xa*z2*qinv (z1*z2) " in exI, rule conjI) +apply (erule lemma_preal_rat_less4) +apply (simp add: qinv_mult_eq [symmetric] prat_mult_ac) +apply (simp add: prat_mult_assoc [symmetric]) +done + +lemma preal_of_prat_less_iff [simp]: + "(preal_of_prat p < preal_of_prat q) = (p < q)" +apply (unfold preal_of_prat_def preal_less_def) +apply (auto dest!: lemma_prat_set_eq elim: prat_less_trans + simp add: lemma_prat_less_set_mem_preal psubset_def prat_less_not_refl) +apply (rule_tac x = p and y = q in prat_linear_less2) +apply (auto intro: prat_less_irrefl) +done + + +ML +{* +val inj_on_Abs_preal = thm"inj_on_Abs_preal"; +val inj_Rep_preal = thm"inj_Rep_preal"; +val empty_not_mem_preal = thm"empty_not_mem_preal"; +val one_set_mem_preal = thm"one_set_mem_preal"; +val preal_psubset_empty = thm"preal_psubset_empty"; +val mem_Rep_preal_Ex = thm"mem_Rep_preal_Ex"; +val inj_preal_of_prat = thm"inj_preal_of_prat"; +val not_in_preal_ub = thm"not_in_preal_ub"; +val preal_less_not_refl = thm"preal_less_not_refl"; +val preal_less_trans = thm"preal_less_trans"; +val preal_less_not_sym = thm"preal_less_not_sym"; +val preal_linear = thm"preal_linear"; +val preal_add_commute = thm"preal_add_commute"; +val preal_add_set_not_empty = thm"preal_add_set_not_empty"; +val preal_not_mem_add_set_Ex = thm"preal_not_mem_add_set_Ex"; +val preal_add_set_not_prat_set = thm"preal_add_set_not_prat_set"; +val preal_mem_add_set = thm"preal_mem_add_set"; +val preal_add_assoc = thm"preal_add_assoc"; +val preal_add_left_commute = thm"preal_add_left_commute"; +val preal_mult_commute = thm"preal_mult_commute"; +val preal_mult_set_not_empty = thm"preal_mult_set_not_empty"; +val preal_not_mem_mult_set_Ex = thm"preal_not_mem_mult_set_Ex"; +val preal_mult_set_not_prat_set = thm"preal_mult_set_not_prat_set"; +val preal_mem_mult_set = thm"preal_mem_mult_set"; +val preal_mult_assoc = thm"preal_mult_assoc"; +val preal_mult_left_commute = thm"preal_mult_left_commute"; +val preal_mult_1 = thm"preal_mult_1"; +val preal_mult_1_right = thm"preal_mult_1_right"; +val mem_Rep_preal_addD = thm"mem_Rep_preal_addD"; +val mem_Rep_preal_addI = thm"mem_Rep_preal_addI"; +val mem_Rep_preal_add_iff = thm"mem_Rep_preal_add_iff"; +val mem_Rep_preal_multD = thm"mem_Rep_preal_multD"; +val mem_Rep_preal_multI = thm"mem_Rep_preal_multI"; +val mem_Rep_preal_mult_iff = thm"mem_Rep_preal_mult_iff"; +val preal_add_mult_distrib2 = thm"preal_add_mult_distrib2"; +val preal_add_mult_distrib = thm"preal_add_mult_distrib"; +val qinv_not_mem_Rep_preal_Ex = thm"qinv_not_mem_Rep_preal_Ex"; +val preal_inv_set_not_empty = thm"preal_inv_set_not_empty"; +val qinv_mem_Rep_preal_Ex = thm"qinv_mem_Rep_preal_Ex"; +val preal_not_mem_inv_set_Ex = thm"preal_not_mem_inv_set_Ex"; +val preal_inv_set_not_prat_set = thm"preal_inv_set_not_prat_set"; +val preal_mem_inv_set = thm"preal_mem_inv_set"; +val preal_mem_mult_invD = thm"preal_mem_mult_invD"; +val preal_mem_mult_invI = thm"preal_mem_mult_invI"; +val preal_mult_inv = thm"preal_mult_inv"; +val preal_mult_inv_right = thm"preal_mult_inv_right"; +val Rep_preal_self_subset = thm"Rep_preal_self_subset"; +val Rep_preal_sum_not_subset = thm"Rep_preal_sum_not_subset"; +val Rep_preal_sum_not_eq = thm"Rep_preal_sum_not_eq"; +val preal_self_less_add_left = thm"preal_self_less_add_left"; +val preal_self_less_add_right = thm"preal_self_less_add_right"; +val preal_less_le_iff = thm"preal_less_le_iff"; +val preal_le_refl = thm"preal_le_refl"; +val preal_le_trans = thm"preal_le_trans"; +val preal_le_anti_sym = thm"preal_le_anti_sym"; +val preal_neq_iff = thm"preal_neq_iff"; +val preal_less_le = thm"preal_less_le"; +val psubset_trans = thm"psubset_trans"; +val preal_less_set_not_empty = thm"preal_less_set_not_empty"; +val preal_less_set_not_prat_set = thm"preal_less_set_not_prat_set"; +val preal_mem_less_set = thm"preal_mem_less_set"; +val preal_less_add_left_subsetI = thm"preal_less_add_left_subsetI"; +val preal_less_add_left_subsetI2 = thm"preal_less_add_left_subsetI2"; +val preal_less_add_left = thm"preal_less_add_left"; +val preal_less_add_left_Ex = thm"preal_less_add_left_Ex"; +val preal_add_less2_mono1 = thm"preal_add_less2_mono1"; +val preal_add_less2_mono2 = thm"preal_add_less2_mono2"; +val preal_mult_less_mono1 = thm"preal_mult_less_mono1"; +val preal_mult_left_less_mono1 = thm"preal_mult_left_less_mono1"; +val preal_mult_left_le_mono1 = thm"preal_mult_left_le_mono1"; +val preal_mult_le_mono1 = thm"preal_mult_le_mono1"; +val preal_add_left_le_mono1 = thm"preal_add_left_le_mono1"; +val preal_add_le_mono1 = thm"preal_add_le_mono1"; +val preal_add_right_less_cancel = thm"preal_add_right_less_cancel"; +val preal_add_left_less_cancel = thm"preal_add_left_less_cancel"; +val preal_add_less_iff1 = thm"preal_add_less_iff1"; +val preal_add_less_iff2 = thm"preal_add_less_iff2"; +val preal_add_less_mono = thm"preal_add_less_mono"; +val preal_mult_less_mono = thm"preal_mult_less_mono"; +val preal_add_right_cancel = thm"preal_add_right_cancel"; +val preal_add_left_cancel = thm"preal_add_left_cancel"; +val preal_add_left_cancel_iff = thm"preal_add_left_cancel_iff"; +val preal_add_right_cancel_iff = thm"preal_add_right_cancel_iff"; +val preal_sup_mem_Ex = thm"preal_sup_mem_Ex"; +val preal_sup_set_not_empty = thm"preal_sup_set_not_empty"; +val preal_sup_not_mem_Ex = thm"preal_sup_not_mem_Ex"; +val preal_sup_not_mem_Ex1 = thm"preal_sup_not_mem_Ex1"; +val preal_sup_set_not_prat_set = thm"preal_sup_set_not_prat_set"; +val preal_sup_set_not_prat_set1 = thm"preal_sup_set_not_prat_set1"; +val preal_sup = thm"preal_sup"; +val preal_sup1 = thm"preal_sup1"; +val preal_psup_leI = thm"preal_psup_leI"; +val preal_psup_leI2 = thm"preal_psup_leI2"; +val preal_psup_leI2b = thm"preal_psup_leI2b"; +val preal_psup_leI2a = thm"preal_psup_leI2a"; +val psup_le_ub = thm"psup_le_ub"; +val psup_le_ub1 = thm"psup_le_ub1"; +val preal_complete = thm"preal_complete"; +val preal_of_prat_add = thm"preal_of_prat_add"; +val preal_of_prat_mult = thm"preal_of_prat_mult"; + +val preal_add_ac = thms"preal_add_ac"; +val preal_mult_ac = thms"preal_mult_ac"; +*} + end - diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Real/RealDef.thy Thu Jan 01 21:47:07 2004 +0100 @@ -7,26 +7,6 @@ theory RealDef = PReal: -(*MOVE TO THEORY PREAL*) -instance preal :: order -proof qed - (assumption | - rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+ - -instance preal :: order - by (intro_classes, - (assumption | - rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+) - -lemma preal_le_linear: "x <= y | y <= (x::preal)" -apply (insert preal_linear [of x y]) -apply (auto simp add: order_less_le) -done - -instance preal :: linorder - by (intro_classes, rule preal_le_linear) - - constdefs realrel :: "((preal * preal) * (preal * preal)) set" "realrel == {p. \x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" @@ -781,8 +761,8 @@ lemma real_of_preal_le_iff: "(real_of_preal m1 \ real_of_preal m2) = (m1 \ m2)" -apply (auto intro!: preal_leI simp add: linorder_not_less [symmetric]) -done +by (auto intro!: preal_le_iff_less_or_eq [THEN iffD1] + simp add: linorder_not_less [symmetric]) subsection{*Monotonicity of Addition*} @@ -797,11 +777,15 @@ lemma real_less_add_positive_left_Ex: "R < S ==> \T::real. 0 < T & R + T = S" apply (rule_tac x = R in real_of_preal_trichotomyE) apply (rule_tac [!] x = S in real_of_preal_trichotomyE) -apply (auto dest!: preal_less_add_left_Ex simp add: real_of_preal_not_minus_gt_all real_of_preal_add real_of_preal_not_less_zero real_less_not_refl real_of_preal_not_minus_gt_zero real_of_preal_minus_less_rev_iff) +apply (auto dest!: preal_less_add_left_Ex + simp add: real_of_preal_not_minus_gt_all real_of_preal_add + real_of_preal_not_less_zero real_less_not_refl + real_of_preal_not_minus_gt_zero real_of_preal_minus_less_rev_iff) apply (rule real_of_preal_zero_less) apply (rule_tac [1] x = "real_of_preal m+real_of_preal ma" in exI) apply (rule_tac [2] x = "real_of_preal D" in exI) -apply (auto simp add: real_of_preal_minus_less_rev_iff real_of_preal_zero_less real_of_preal_sum_zero_less real_add_assoc) +apply (auto simp add: real_of_preal_minus_less_rev_iff real_of_preal_zero_less + real_of_preal_sum_zero_less real_add_assoc) apply (simp add: real_add_assoc [symmetric]) done diff -r 6137d24eef79 -r 9c0b5e081037 src/HOL/Set.thy --- a/src/HOL/Set.thy Thu Jan 01 10:06:32 2004 +0100 +++ b/src/HOL/Set.thy Thu Jan 01 21:47:07 2004 +0100 @@ -868,6 +868,16 @@ lemma psubset_imp_subset: "A \ B ==> A \ B" by (simp add: psubset_eq) +lemma psubset_trans: "[| A \ B; B \ C |] ==> A \ C" +apply (unfold psubset_def) +apply (auto dest: subset_antisym) +done + +lemma psubsetD: "[| A \ B; c \ A |] ==> c \ B" +apply (unfold psubset_def) +apply (auto dest: subsetD) +done + lemma psubset_subset_trans: "A \ B ==> B \ C ==> A \ C" by (auto simp add: psubset_eq)