--- 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) \\<Longrightarrow> (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]
--- 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 \<noteq> (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 \<noteq> 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
--- 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];
--- 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);
--- 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 \<noteq> (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
--- 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
--- 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);
--- 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;
--- 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 \
--- 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";
--- 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<z | z<w)";
-by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
-by (auto_tac (claset() addEs [preal_less_irrefl], simpset()));
-qed "preal_neq_iff";
-
-(* Axiom 'order_less_le' of class 'order': *)
-Goal "((w::preal) < z) = (w <= z & w ~= z)";
-by (simp_tac (simpset() addsimps [preal_less_le_iff RS sym, preal_neq_iff]) 1);
-by (blast_tac (claset() addSEs [preal_less_asym]) 1);
-qed "preal_less_le";
-
-
-(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
-
-(**** Set up all lemmas for proving A < B ==> ?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];
--- 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}
+ (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
+ (\<exists>u \<in> 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. \<exists>y. w < y & qinv y \<notin> 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. \<exists>X \<in> P. w \<in> 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. \<exists>x \<in> Rep_preal(R). \<exists>y \<in> 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. \<exists>x \<in> Rep_preal(R). \<exists>y \<in> 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 \<le> (S::preal) == Rep_preal(R) \<subseteq> 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]: "{} \<notin> preal"
+by (unfold preal_def, fast)
+
+lemma one_set_mem_preal: "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} \<in> preal"
+apply (unfold preal_def)
+apply (rule preal_1)
+done
+
+declare one_set_mem_preal [simp]
+
+lemma preal_psubset_empty: "x \<in> 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: "\<exists>x. x \<in> 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;
+ (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
+ (\<exists>u \<in> A. y < u))) |] ==> A \<in> preal"
+apply (unfold preal_def, fast)
+done
+
+lemma prealI2:
+ "[| {} < A; A < UNIV;
+ \<forall>y \<in> A. (\<forall>z. z < y --> z \<in> A);
+ \<forall>y \<in> A. (\<exists>u \<in> A. y < u) |] ==> A \<in> preal"
+
+apply (unfold preal_def, best)
+done
+
+lemma prealE_lemma:
+ "A \<in> preal ==> {} < A & A < UNIV &
+ (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
+ (\<exists>u \<in> A. y < u)))"
+apply (unfold preal_def, fast)
+done
+
+declare prealI1 [intro!] prealI2 [intro!]
+
+declare Abs_preal_inverse [simp]
+
+
+lemma prealE_lemma1: "A \<in> preal ==> {} < A"
+by (unfold preal_def, fast)
+
+lemma prealE_lemma2: "A \<in> preal ==> A < UNIV"
+by (unfold preal_def, fast)
+
+lemma prealE_lemma3: "A \<in> preal ==> \<forall>y \<in> A. (\<forall>z. z < y --> z \<in> A)"
+by (unfold preal_def, fast)
+
+lemma prealE_lemma3a: "[| A \<in> preal; y \<in> A |] ==> (\<forall>z. z < y --> z \<in> A)"
+by (fast dest!: prealE_lemma3)
+
+lemma prealE_lemma3b: "[| A \<in> preal; y \<in> A; z < y |] ==> z \<in> A"
+by (fast dest!: prealE_lemma3a)
+
+lemma prealE_lemma4: "A \<in> preal ==> \<forall>y \<in> A. (\<exists>u \<in> A. y < u)"
+by (unfold preal_def, fast)
+
+lemma prealE_lemma4a: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
+by (fast dest!: prealE_lemma4)
+
+lemma not_mem_Rep_preal_Ex: "\<exists>x. x\<notin> 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} \<in> 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 \<notin> Rep_preal(R) ==> \<forall>y \<in> 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 \<noteq> 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. \<exists>x \<in> Rep_preal R. \<exists>y \<in> 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:
+ "\<exists>q. q \<notin> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> 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. \<exists>x \<in> Rep_preal R. \<exists>y \<in> 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:
+ "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}.
+ \<forall>z. z < y --> z \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> 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:
+ "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}.
+ \<exists>u \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> 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. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y} \<in> 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. \<exists>x \<in> Rep_preal R. \<exists>y \<in> 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:
+ "\<exists>q. q \<notin> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> 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. \<exists>x \<in> Rep_preal R. \<exists>y \<in> 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:
+ "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}.
+ \<forall>z. z < y --> z \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> 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:
+ "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}.
+ \<exists>u \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> 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. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y} \<in> 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 \<in> Rep_preal(R+S) ==>
+ \<exists>x \<in> Rep_preal(R). \<exists>y \<in> 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:
+ "\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x + y
+ ==> z \<in> 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 \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal(R).
+ \<exists>y \<in> Rep_preal(S). z = x + y)"
+apply (fast intro!: mem_Rep_preal_addD mem_Rep_preal_addI)
+done
+
+lemma mem_Rep_preal_multD:
+ "z \<in> Rep_preal(R*S) ==>
+ \<exists>x \<in> Rep_preal(R). \<exists>y \<in> 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:
+ "\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x * y
+ ==> z \<in> 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 \<in> Rep_preal(R*S)) =
+ (\<exists>x \<in> Rep_preal(R). \<exists>y \<in> 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 \<in> Rep_preal z1; xc \<in> Rep_preal z2; ya:
+ Rep_preal w; yb \<in> Rep_preal w |] ==>
+ xb * ya + xc * yb \<in> 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 \<in> Rep_preal z1; xc \<in> Rep_preal z2; ya:
+ Rep_preal w; yb \<in> Rep_preal w |] ==>
+ yb*(xb + xc) \<in> Rep_preal (w*(z1 + z2))"
+by (fast intro: mem_Rep_preal_addI mem_Rep_preal_multI)
+
+lemma lemma_preal_add_mult_distrib:
+ "x \<in> Rep_preal (w * z1 + w * z2) ==>
+ x \<in> 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 \<in> 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 \<in> Rep_preal (w * (z1 + z2)) ==>
+ x \<in> 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: "\<exists>y. qinv(y) \<notin> 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:
+ "\<exists>q. q \<in> {x. \<exists>y. x < y & qinv y \<notin> 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. \<exists>y. x < y & qinv y \<notin> 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: "\<exists>y. qinv(y) \<in> 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:
+ "\<exists>x. x \<notin> {x. \<exists>y. x < y & qinv y \<notin> 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. \<exists>y. x < y & qinv y \<notin> 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:
+ "\<forall>y \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}.
+ \<forall>z. z < y --> z \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}"
+apply auto
+apply (rule_tac x = ya in exI)
+apply (auto intro: prat_less_trans)
+done
+
+lemma preal_inv_set_lemma4:
+ "\<forall>y \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}.
+ Bex {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A} (op < y)"
+by (blast dest: prat_dense)
+
+lemma preal_mem_inv_set: "{x. \<exists>y. x < y & qinv(y) \<notin> Rep_preal(A)} \<in> 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 \<in> Rep_preal(pinv(A)*A) ==>
+ x \<in> 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:
+ "\<forall>xa \<in> Rep_preal(A). xa + x \<in> Rep_preal(A) ==>
+ \<exists>xb \<in> Rep_preal(A). xb + (prat_of_pnat p)*x \<in> 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:
+ "\<forall>xa \<in> Rep_preal(A). xa + x \<in> 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: "\<exists>r \<in> Rep_preal(R). r + x \<notin> 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 ==> \<exists>r \<in> Rep_preal(A). r*x \<notin> Rep_preal(A)"
+apply (rule_tac X1 = A in mem_Rep_preal_Ex [THEN exE])
+apply (rule_tac Q = "xa*x \<in> 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 ==>
+ \<exists>r \<in> Rep_preal(A). r*x \<notin> 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 \<in> Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))
+ ==> x \<in> 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) \<subseteq> 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) \<subseteq> 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) \<noteq> 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 "\<le>"} Ordering*}
+
+lemma preal_less_le_iff: "(~(w < z)) = (z \<le> (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) \<le> 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 \<le> (w::preal)"
+apply (simp add: preal_le_def)
+done
+
+lemma preal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::preal)"
+apply (simp add: preal_le_iff_less_or_eq)
+apply (blast intro: preal_less_trans)
+done
+
+lemma preal_le_anti_sym: "[| z \<le> w; w \<le> 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 \<noteq> z) = (w<z | z < (w::preal))"
+apply (insert preal_linear [of w z])
+apply (auto elim: preal_less_irrefl)
+done
+
+(* Axiom 'order_less_le' of class 'order': *)
+lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> 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 ==> \<exists>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 ==>
+ \<exists>q. q \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> 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. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> 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:
+ "\<exists>q. q \<notin> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> 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. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> 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 ==> \<forall>y \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}.
+ \<forall>z. z < y --> z \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> 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 ==> \<forall>y \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}.
+ Bex {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> 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. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> 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 \<le> B"}*}
+lemma preal_less_add_left_subsetI:
+ "!! (A::preal). A < B ==>
+ A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}) \<le> 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 \<le> A + D"} --- trickier*}
+
+lemma lemma_sum_mem_Rep_preal_ex:
+ "x \<in> Rep_preal(B) ==> \<exists>e. x + e \<in> 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 \<le> A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)})"
+apply (unfold preal_le_def)
+apply (rule subsetI)
+apply (rule_tac Q = "x \<in> 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. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> 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 ==> \<exists>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 \<le> q2 ==> x * q1 \<le> 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 \<le> q2 ==> q1 * x \<le> q2 * x"
+by (auto dest: preal_mult_left_le_mono1 simp add: preal_mult_commute)
+
+lemma preal_add_left_le_mono1: "!!(q1::preal). q1 \<le> q2 ==> x + q1 \<le> 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 \<le> q2 ==> q1 + x \<le> 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:
+ "\<exists>X. X \<in> P ==> \<exists>q. q \<in> {w. \<exists>X. X \<in> P & w \<in> 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:
+ "\<exists>(X::preal). X \<in> P ==>
+ {} < {w. \<exists>X \<in> P. w \<in> 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:
+ "\<exists>Y. (\<forall>X \<in> P. X < Y)
+ ==> \<exists>q. q \<notin> {w. \<exists>X. X \<in> P & w \<in> 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:
+ "\<exists>Y. (\<forall>X \<in> P. X \<le> Y)
+ ==> \<exists>q. q \<notin> {w. \<exists>X. X \<in> P & w \<in> 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:
+ "\<exists>Y. (\<forall>X \<in> P. X < Y) ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)} < UNIV"
+apply (drule preal_sup_not_mem_Ex)
+apply (auto intro!: psubsetI)
+done
+
+lemma preal_sup_set_not_prat_set1:
+ "\<exists>Y. (\<forall>X \<in> P. X \<le> Y) ==> {w. \<exists>X \<in> P. w \<in> 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:
+ "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
+ ==> \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
+ \<forall>z. z < y --> z \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
+apply (auto elim: Rep_preal [THEN prealE_lemma3b])
+done
+
+lemma preal_sup_set_lemma3_1:
+ "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
+ ==> \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
+ \<forall>z. z < y --> z \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
+apply (auto elim: Rep_preal [THEN prealE_lemma3b])
+done
+
+lemma preal_sup_set_lemma4:
+ "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
+ ==> \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
+ Bex {w. \<exists>X \<in> P. w \<in> Rep_preal X} (op < y)"
+apply (blast dest: Rep_preal [THEN prealE_lemma4a])
+done
+
+lemma preal_sup_set_lemma4_1:
+ "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
+ ==> \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
+ Bex {w. \<exists>X \<in> P. w \<in> Rep_preal X} (op < y)"
+apply (blast dest: Rep_preal [THEN prealE_lemma4a])
+done
+
+lemma preal_sup:
+ "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
+ ==> {w. \<exists>X \<in> P. w \<in> 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:
+ "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
+ ==> {w. \<exists>X \<in> P. w \<in> 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: "\<exists>Y. (\<forall>X \<in> P. X < Y) ==> \<forall>x \<in> P. x \<le> 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: "\<exists>Y. (\<forall>X \<in> P. X \<le> Y) ==> \<forall>x \<in> P. x \<le> 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:
+ "[| \<exists>Y. (\<forall>X \<in> P. X < Y); x \<in> P |] ==> x \<le> psup P"
+apply (blast dest!: preal_psup_leI)
+done
+
+lemma preal_psup_leI2a:
+ "[| \<exists>Y. (\<forall>X \<in> P. X \<le> Y); x \<in> P |] ==> x \<le> psup P"
+apply (blast dest!: preal_psup_leI2)
+done
+
+lemma psup_le_ub: "[| \<exists>X. X \<in> P; \<forall>X \<in> P. X < Y |] ==> psup P \<le> 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: "[| \<exists>X. X \<in> P; \<forall>X \<in> P. X \<le> Y |] ==> psup P \<le> 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:
+ "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
+ ==> (\<forall>Y. (\<exists>X \<in> 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
-
--- 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. \<exists>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 \<le> real_of_preal m2) = (m1 \<le> 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 ==> \<exists>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
--- 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 \<subset> B ==> A \<subseteq> B"
by (simp add: psubset_eq)
+lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
+apply (unfold psubset_def)
+apply (auto dest: subset_antisym)
+done
+
+lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
+apply (unfold psubset_def)
+apply (auto dest: subsetD)
+done
+
lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
by (auto simp add: psubset_eq)