--- a/src/HOL/Complex/CLim.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/CLim.thy Fri Jun 02 23:22:29 2006 +0200
@@ -33,79 +33,79 @@
apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto)
done
-constdefs
+definition
CLIM :: "[complex=>complex,complex,complex] => bool"
("((_)/ -- (_)/ --C> (_))" [60, 0, 60] 60)
- "f -- a --C> L ==
- \<forall>r. 0 < r -->
+ "f -- a --C> L =
+ (\<forall>r. 0 < r -->
(\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s)
- --> cmod(f x - L) < r)))"
+ --> cmod(f x - L) < r))))"
NSCLIM :: "[complex=>complex,complex,complex] => bool"
("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60)
- "f -- a --NSC> L == (\<forall>x. (x \<noteq> hcomplex_of_complex a &
+ "f -- a --NSC> L = (\<forall>x. (x \<noteq> hcomplex_of_complex a &
x @c= hcomplex_of_complex a
--> ( *f* f) x @c= hcomplex_of_complex L))"
(* f: C --> R *)
CRLIM :: "[complex=>real,complex,real] => bool"
("((_)/ -- (_)/ --CR> (_))" [60, 0, 60] 60)
- "f -- a --CR> L ==
- \<forall>r. 0 < r -->
+ "f -- a --CR> L =
+ (\<forall>r. 0 < r -->
(\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s)
- --> abs(f x - L) < r)))"
+ --> abs(f x - L) < r))))"
NSCRLIM :: "[complex=>real,complex,real] => bool"
("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60)
- "f -- a --NSCR> L == (\<forall>x. (x \<noteq> hcomplex_of_complex a &
+ "f -- a --NSCR> L = (\<forall>x. (x \<noteq> hcomplex_of_complex a &
x @c= hcomplex_of_complex a
--> ( *f* f) x @= hypreal_of_real L))"
isContc :: "[complex=>complex,complex] => bool"
- "isContc f a == (f -- a --C> (f a))"
+ "isContc f a = (f -- a --C> (f a))"
(* NS definition dispenses with limit notions *)
isNSContc :: "[complex=>complex,complex] => bool"
- "isNSContc f a == (\<forall>y. y @c= hcomplex_of_complex a -->
+ "isNSContc f a = (\<forall>y. y @c= hcomplex_of_complex a -->
( *f* f) y @c= hcomplex_of_complex (f a))"
isContCR :: "[complex=>real,complex] => bool"
- "isContCR f a == (f -- a --CR> (f a))"
+ "isContCR f a = (f -- a --CR> (f a))"
(* NS definition dispenses with limit notions *)
isNSContCR :: "[complex=>real,complex] => bool"
- "isNSContCR f a == (\<forall>y. y @c= hcomplex_of_complex a -->
+ "isNSContCR f a = (\<forall>y. y @c= hcomplex_of_complex a -->
( *f* f) y @= hypreal_of_real (f a))"
(* differentiation: D is derivative of function f at x *)
cderiv:: "[complex=>complex,complex,complex] => bool"
("(CDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
- "CDERIV f x :> D == ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"
+ "CDERIV f x :> D = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"
nscderiv :: "[complex=>complex,complex,complex] => bool"
("(NSCDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
- "NSCDERIV f x :> D == (\<forall>h \<in> CInfinitesimal - {0}.
+ "NSCDERIV f x :> D = (\<forall>h \<in> CInfinitesimal - {0}.
(( *f* f)(hcomplex_of_complex x + h)
- hcomplex_of_complex (f x))/h @c= hcomplex_of_complex D)"
cdifferentiable :: "[complex=>complex,complex] => bool"
(infixl "cdifferentiable" 60)
- "f cdifferentiable x == (\<exists>D. CDERIV f x :> D)"
+ "f cdifferentiable x = (\<exists>D. CDERIV f x :> D)"
NSCdifferentiable :: "[complex=>complex,complex] => bool"
(infixl "NSCdifferentiable" 60)
- "f NSCdifferentiable x == (\<exists>D. NSCDERIV f x :> D)"
+ "f NSCdifferentiable x = (\<exists>D. NSCDERIV f x :> D)"
isUContc :: "(complex=>complex) => bool"
- "isUContc f == (\<forall>r. 0 < r -->
+ "isUContc f = (\<forall>r. 0 < r -->
(\<exists>s. 0 < s & (\<forall>x y. cmod(x - y) < s
--> cmod(f x - f y) < r)))"
isNSUContc :: "(complex=>complex) => bool"
- "isNSUContc f == (\<forall>x y. x @c= y --> ( *f* f) x @c= ( *f* f) y)"
+ "isNSUContc f = (\<forall>x y. x @c= y --> ( *f* f) x @c= ( *f* f) y)"
@@ -1020,156 +1020,4 @@
==> NSCDERIV f x :> l"
by (auto simp add: NSCDERIV_iff2 isNSContc_def cstarfun_if_eq);
-
-ML
-{*
-val complex_add_minus_iff = thm "complex_add_minus_iff";
-val complex_add_eq_0_iff = thm "complex_add_eq_0_iff";
-val NSCLIM_NSCRLIM_Re = thm "NSCLIM_NSCRLIM_Re";
-val NSCLIM_NSCRLIM_Im = thm "NSCLIM_NSCRLIM_Im";
-val CLIM_NSCLIM = thm "CLIM_NSCLIM";
-val eq_Abs_star_ALL = thm "eq_Abs_star_ALL";
-val lemma_CLIM = thm "lemma_CLIM";
-val lemma_skolemize_CLIM2 = thm "lemma_skolemize_CLIM2";
-val lemma_csimp = thm "lemma_csimp";
-val NSCLIM_CLIM = thm "NSCLIM_CLIM";
-val CLIM_NSCLIM_iff = thm "CLIM_NSCLIM_iff";
-val CRLIM_NSCRLIM = thm "CRLIM_NSCRLIM";
-val lemma_CRLIM = thm "lemma_CRLIM";
-val lemma_skolemize_CRLIM2 = thm "lemma_skolemize_CRLIM2";
-val lemma_crsimp = thm "lemma_crsimp";
-val NSCRLIM_CRLIM = thm "NSCRLIM_CRLIM";
-val CRLIM_NSCRLIM_iff = thm "CRLIM_NSCRLIM_iff";
-val CLIM_CRLIM_Re = thm "CLIM_CRLIM_Re";
-val CLIM_CRLIM_Im = thm "CLIM_CRLIM_Im";
-val CLIM_cnj = thm "CLIM_cnj";
-val CLIM_cnj_iff = thm "CLIM_cnj_iff";
-val NSCLIM_add = thm "NSCLIM_add";
-val CLIM_add = thm "CLIM_add";
-val NSCLIM_mult = thm "NSCLIM_mult";
-val CLIM_mult = thm "CLIM_mult";
-val NSCLIM_const = thm "NSCLIM_const";
-val CLIM_const = thm "CLIM_const";
-val NSCLIM_minus = thm "NSCLIM_minus";
-val CLIM_minus = thm "CLIM_minus";
-val NSCLIM_diff = thm "NSCLIM_diff";
-val CLIM_diff = thm "CLIM_diff";
-val NSCLIM_inverse = thm "NSCLIM_inverse";
-val CLIM_inverse = thm "CLIM_inverse";
-val NSCLIM_zero = thm "NSCLIM_zero";
-val CLIM_zero = thm "CLIM_zero";
-val NSCLIM_zero_cancel = thm "NSCLIM_zero_cancel";
-val CLIM_zero_cancel = thm "CLIM_zero_cancel";
-val NSCLIM_not_zero = thm "NSCLIM_not_zero";
-val NSCLIM_not_zeroE = thms "NSCLIM_not_zeroE";
-val CLIM_not_zero = thm "CLIM_not_zero";
-val NSCLIM_const_eq = thm "NSCLIM_const_eq";
-val CLIM_const_eq = thm "CLIM_const_eq";
-val NSCLIM_unique = thm "NSCLIM_unique";
-val CLIM_unique = thm "CLIM_unique";
-val NSCLIM_mult_zero = thm "NSCLIM_mult_zero";
-val CLIM_mult_zero = thm "CLIM_mult_zero";
-val NSCLIM_self = thm "NSCLIM_self";
-val CLIM_self = thm "CLIM_self";
-val NSCLIM_NSCRLIM_iff = thm "NSCLIM_NSCRLIM_iff";
-val CLIM_CRLIM_iff = thm "CLIM_CRLIM_iff";
-val NSCLIM_NSCRLIM_iff2 = thm "NSCLIM_NSCRLIM_iff2";
-val NSCLIM_NSCRLIM_Re_Im_iff = thm "NSCLIM_NSCRLIM_Re_Im_iff";
-val CLIM_CRLIM_Re_Im_iff = thm "CLIM_CRLIM_Re_Im_iff";
-val isNSContcD = thm "isNSContcD";
-val isNSContc_NSCLIM = thm "isNSContc_NSCLIM";
-val NSCLIM_isNSContc = thm "NSCLIM_isNSContc";
-val isNSContc_NSCLIM_iff = thm "isNSContc_NSCLIM_iff";
-val isNSContc_CLIM_iff = thm "isNSContc_CLIM_iff";
-val isNSContc_isContc_iff = thm "isNSContc_isContc_iff";
-val isContc_isNSContc = thm "isContc_isNSContc";
-val isNSContc_isContc = thm "isNSContc_isContc";
-val NSCLIM_h_iff = thm "NSCLIM_h_iff";
-val NSCLIM_isContc_iff = thm "NSCLIM_isContc_iff";
-val CLIM_isContc_iff = thm "CLIM_isContc_iff";
-val isContc_iff = thm "isContc_iff";
-val isContc_add = thm "isContc_add";
-val isContc_mult = thm "isContc_mult";
-val isContc_o = thm "isContc_o";
-val isContc_o2 = thm "isContc_o2";
-val isNSContc_minus = thm "isNSContc_minus";
-val isContc_minus = thm "isContc_minus";
-val isContc_inverse = thm "isContc_inverse";
-val isNSContc_inverse = thm "isNSContc_inverse";
-val isContc_diff = thm "isContc_diff";
-val isContc_const = thm "isContc_const";
-val isNSContc_const = thm "isNSContc_const";
-val isNSContCRD = thm "isNSContCRD";
-val isNSContCR_NSCRLIM = thm "isNSContCR_NSCRLIM";
-val NSCRLIM_isNSContCR = thm "NSCRLIM_isNSContCR";
-val isNSContCR_NSCRLIM_iff = thm "isNSContCR_NSCRLIM_iff";
-val isNSContCR_CRLIM_iff = thm "isNSContCR_CRLIM_iff";
-val isNSContCR_isContCR_iff = thm "isNSContCR_isContCR_iff";
-val isContCR_isNSContCR = thm "isContCR_isNSContCR";
-val isNSContCR_isContCR = thm "isNSContCR_isContCR";
-val isNSContCR_cmod = thm "isNSContCR_cmod";
-val isContCR_cmod = thm "isContCR_cmod";
-val isContc_isContCR_Re = thm "isContc_isContCR_Re";
-val isContc_isContCR_Im = thm "isContc_isContCR_Im";
-val CDERIV_iff = thm "CDERIV_iff";
-val CDERIV_NSC_iff = thm "CDERIV_NSC_iff";
-val CDERIVD = thm "CDERIVD";
-val NSC_DERIVD = thm "NSC_DERIVD";
-val CDERIV_unique = thm "CDERIV_unique";
-val NSCDeriv_unique = thm "NSCDeriv_unique";
-val CDERIV_CLIM_iff = thm "CDERIV_CLIM_iff";
-val CDERIV_iff2 = thm "CDERIV_iff2";
-val NSCDERIV_NSCLIM_iff = thm "NSCDERIV_NSCLIM_iff";
-val NSCDERIV_NSCLIM_iff2 = thm "NSCDERIV_NSCLIM_iff2";
-val NSCDERIV_iff2 = thm "NSCDERIV_iff2";
-val NSCDERIV_CDERIV_iff = thm "NSCDERIV_CDERIV_iff";
-val NSCDERIV_isNSContc = thm "NSCDERIV_isNSContc";
-val CDERIV_isContc = thm "CDERIV_isContc";
-val NSCDERIV_const = thm "NSCDERIV_const";
-val CDERIV_const = thm "CDERIV_const";
-val NSCDERIV_add = thm "NSCDERIV_add";
-val CDERIV_add = thm "CDERIV_add";
-val lemma_nscderiv1 = thm "lemma_nscderiv1";
-val lemma_nscderiv2 = thm "lemma_nscderiv2";
-val NSCDERIV_mult = thm "NSCDERIV_mult";
-val CDERIV_mult = thm "CDERIV_mult";
-val NSCDERIV_cmult = thm "NSCDERIV_cmult";
-val CDERIV_cmult = thm "CDERIV_cmult";
-val NSCDERIV_minus = thm "NSCDERIV_minus";
-val CDERIV_minus = thm "CDERIV_minus";
-val NSCDERIV_add_minus = thm "NSCDERIV_add_minus";
-val CDERIV_add_minus = thm "CDERIV_add_minus";
-val NSCDERIV_diff = thm "NSCDERIV_diff";
-val CDERIV_diff = thm "CDERIV_diff";
-val NSCDERIV_zero = thm "NSCDERIV_zero";
-val NSCDERIV_capprox = thm "NSCDERIV_capprox";
-val NSCDERIVD1 = thm "NSCDERIVD1";
-val NSCDERIVD2 = thm "NSCDERIVD2";
-val lemma_complex_chain = thm "lemma_complex_chain";
-val NSCDERIV_chain = thm "NSCDERIV_chain";
-val CDERIV_chain = thm "CDERIV_chain";
-val CDERIV_chain2 = thm "CDERIV_chain2";
-val NSCDERIV_Id = thm "NSCDERIV_Id";
-val CDERIV_Id = thm "CDERIV_Id";
-val isContc_Id = thms "isContc_Id";
-val CDERIV_cmult_Id = thm "CDERIV_cmult_Id";
-val NSCDERIV_cmult_Id = thm "NSCDERIV_cmult_Id";
-val CDERIV_pow = thm "CDERIV_pow";
-val NSCDERIV_pow = thm "NSCDERIV_pow";
-val lemma_CDERIV_subst = thm "lemma_CDERIV_subst";
-val CInfinitesimal_add_not_zero = thm "CInfinitesimal_add_not_zero";
-val NSCDERIV_inverse = thm "NSCDERIV_inverse";
-val CDERIV_inverse = thm "CDERIV_inverse";
-val CDERIV_inverse_fun = thm "CDERIV_inverse_fun";
-val NSCDERIV_inverse_fun = thm "NSCDERIV_inverse_fun";
-val lemma_complex_mult_inverse_squared = thm "lemma_complex_mult_inverse_squared";
-val CDERIV_quotient = thm "CDERIV_quotient";
-val NSCDERIV_quotient = thm "NSCDERIV_quotient";
-val CLIM_equal = thm "CLIM_equal";
-val CLIM_trans = thm "CLIM_trans";
-val CARAT_CDERIV = thm "CARAT_CDERIV";
-val CARAT_NSCDERIV = thm "CARAT_NSCDERIV";
-val CARAT_CDERIVD = thm "CARAT_CDERIVD";
-*}
-
end
--- a/src/HOL/Complex/CSeries.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/CSeries.thy Fri Jun 02 23:22:29 2006 +0200
@@ -15,18 +15,18 @@
sumc_Suc: "sumc m (Suc n) f = (if n < m then 0 else sumc m n f + f(n))"
(*
-constdefs
+definition
needs convergence of complex sequences
csums :: [nat=>complex,complex] => bool (infixr 80)
- "f sums s == (%n. sumr 0 n f) ----C> s"
+ "f sums s = (%n. sumr 0 n f) ----C> s"
csummable :: (nat=>complex) => bool
- "csummable f == (EX s. f csums s)"
+ "csummable f = (EX s. f csums s)"
csuminf :: (nat=>complex) => complex
- "csuminf f == (@s. f csums s)"
+ "csuminf f = (@s. f csums s)"
*)
lemma sumc_Suc_zero [simp]: "sumc (Suc n) n f = 0"
@@ -173,34 +173,5 @@
apply (auto simp add: sumc_split_add add_commute)
done
-ML
-{*
-val sumc_Suc_zero = thm "sumc_Suc_zero";
-val sumc_eq_bounds = thm "sumc_eq_bounds";
-val sumc_Suc_eq = thm "sumc_Suc_eq";
-val sumc_add_lbound_zero = thm "sumc_add_lbound_zero";
-val sumc_add = thm "sumc_add";
-val sumc_mult = thm "sumc_mult";
-val sumc_split_add = thm "sumc_split_add";
-val sumc_split_add_minus = thm "sumc_split_add_minus";
-val sumc_cmod = thm "sumc_cmod";
-val sumc_fun_eq = thm "sumc_fun_eq";
-val sumc_const = thm "sumc_const";
-val sumc_add_mult_const = thm "sumc_add_mult_const";
-val sumc_diff_mult_const = thm "sumc_diff_mult_const";
-val sumc_less_bounds_zero = thm "sumc_less_bounds_zero";
-val sumc_minus = thm "sumc_minus";
-val sumc_shift_bounds = thm "sumc_shift_bounds";
-val sumc_minus_one_complexpow_zero = thm "sumc_minus_one_complexpow_zero";
-val sumc_interval_const = thm "sumc_interval_const";
-val sumc_interval_const2 = thm "sumc_interval_const2";
-val sumr_cmod_ge_zero = thm "sumr_cmod_ge_zero";
-val rabs_sumc_cmod_cancel = thm "rabs_sumc_cmod_cancel";
-val sumc_one_lb_complexpow_zero = thm "sumc_one_lb_complexpow_zero";
-val sumc_diff = thm "sumc_diff";
-val sumc_subst = thm "sumc_subst";
-val sumc_group = thm "sumc_group";
-*}
-
end
--- a/src/HOL/Complex/CStar.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/CStar.thy Fri Jun 02 23:22:29 2006 +0200
@@ -36,10 +36,6 @@
"( *f* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)"
by auto
-(*
-Goal "( *fNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N"
-*)
-
lemma starfunC_hcpow: "( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"
apply (cases Z)
apply (simp add: hcpow starfun hypnat_of_nat_eq)
@@ -93,21 +89,4 @@
"x @c= hcomplex_of_complex a ==> ( *f* (%x. x)) x @c= hcomplex_of_complex a"
by simp
-ML
-{*
-val STARC_SComplex_subset = thm "STARC_SComplex_subset";
-val STARC_hcomplex_of_complex_Int = thm "STARC_hcomplex_of_complex_Int";
-val lemma_not_hcomplexA = thm "lemma_not_hcomplexA";
-val starfun_capprox = thm "starfun_capprox";
-val starfunC_hcpow = thm "starfunC_hcpow";
-val starfun_mult_CFinite_capprox = thm "starfun_mult_CFinite_capprox";
-val starfun_add_capprox = thm "starfun_add_capprox";
-val starfunCR_cmod = thm "starfunCR_cmod";
-val starfun_inverse_inverse = thm "starfun_inverse_inverse";
-val starfun_n_diff = thm "starfun_n_diff";
-val starfunC_eq_Re_Im_iff = thm "starfunC_eq_Re_Im_iff";
-val starfunC_approx_Re_Im_iff = thm "starfunC_approx_Re_Im_iff";
-val starfunC_Idfun_capprox = thm "starfunC_Idfun_capprox";
-*}
-
end
--- a/src/HOL/Complex/Complex.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/Complex.thy Fri Jun 02 23:22:29 2006 +0200
@@ -27,30 +27,30 @@
lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
by (induct z) simp
-constdefs
+definition
(*----------- modulus ------------*)
cmod :: "complex => real"
- "cmod z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)"
+ "cmod z = sqrt(Re(z) ^ 2 + Im(z) ^ 2)"
(*----- injection from reals -----*)
complex_of_real :: "real => complex"
- "complex_of_real r == Complex r 0"
+ "complex_of_real r = Complex r 0"
(*------- complex conjugate ------*)
cnj :: "complex => complex"
- "cnj z == Complex (Re z) (-Im z)"
+ "cnj z = Complex (Re z) (-Im z)"
(*------------ Argand -------------*)
sgn :: "complex => complex"
- "sgn z == z / complex_of_real(cmod z)"
+ "sgn z = z / complex_of_real(cmod z)"
arg :: "complex => real"
- "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi"
+ "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)"
defs (overloaded)
@@ -81,19 +81,19 @@
complex_divide_def: "w / (z::complex) == w * inverse z"
-constdefs
+definition
(* abbreviation for (cos a + i sin a) *)
cis :: "real => complex"
- "cis a == Complex (cos a) (sin a)"
+ "cis a = Complex (cos a) (sin a)"
(* abbreviation for r*(cos a + i sin a) *)
rcis :: "[real, real] => complex"
- "rcis r a == complex_of_real r * cis a"
+ "rcis r a = complex_of_real r * cis a"
(* e ^ (x + iy) *)
expi :: "complex => complex"
- "expi z == complex_of_real(exp (Re z)) * cis (Im z)"
+ "expi z = complex_of_real(exp (Re z)) * cis (Im z)"
lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w"
@@ -838,16 +838,16 @@
lemma complex_of_real_of_nat [simp]: "complex_of_real (of_nat n) = of_nat n"
-by (induct n, simp_all)
+ by (induct n) simp_all
lemma complex_of_real_of_int [simp]: "complex_of_real (of_int z) = of_int z"
proof (cases z)
case (1 n)
- thus ?thesis by simp
+ thus ?thesis by simp
next
case (2 n)
- thus ?thesis
- by (simp only: of_int_minus complex_of_real_minus, simp)
+ thus ?thesis
+ by (simp only: of_int_minus complex_of_real_minus, simp)
qed
@@ -914,163 +914,6 @@
test "a*(b*c)/(y*z) = d*(b::complex)*(x*a)/z";
*)
-
-ML
-{*
-val complex_zero_def = thm"complex_zero_def";
-val complex_one_def = thm"complex_one_def";
-val complex_minus_def = thm"complex_minus_def";
-val complex_divide_def = thm"complex_divide_def";
-val complex_mult_def = thm"complex_mult_def";
-val complex_add_def = thm"complex_add_def";
-val complex_of_real_def = thm"complex_of_real_def";
-val i_def = thm"i_def";
-val expi_def = thm"expi_def";
-val cis_def = thm"cis_def";
-val rcis_def = thm"rcis_def";
-val cmod_def = thm"cmod_def";
-val cnj_def = thm"cnj_def";
-val sgn_def = thm"sgn_def";
-val arg_def = thm"arg_def";
-val complexpow_0 = thm"complexpow_0";
-val complexpow_Suc = thm"complexpow_Suc";
-
-val Re = thm"Re";
-val Im = thm"Im";
-val complex_Re_Im_cancel_iff = thm"complex_Re_Im_cancel_iff";
-val complex_Re_zero = thm"complex_Re_zero";
-val complex_Im_zero = thm"complex_Im_zero";
-val complex_Re_one = thm"complex_Re_one";
-val complex_Im_one = thm"complex_Im_one";
-val complex_Re_i = thm"complex_Re_i";
-val complex_Im_i = thm"complex_Im_i";
-val Re_complex_of_real = thm"Re_complex_of_real";
-val Im_complex_of_real = thm"Im_complex_of_real";
-val complex_minus = thm"complex_minus";
-val complex_Re_minus = thm"complex_Re_minus";
-val complex_Im_minus = thm"complex_Im_minus";
-val complex_add = thm"complex_add";
-val complex_Re_add = thm"complex_Re_add";
-val complex_Im_add = thm"complex_Im_add";
-val complex_add_commute = thm"complex_add_commute";
-val complex_add_assoc = thm"complex_add_assoc";
-val complex_add_zero_left = thm"complex_add_zero_left";
-val complex_add_zero_right = thm"complex_add_zero_right";
-val complex_diff = thm"complex_diff";
-val complex_mult = thm"complex_mult";
-val complex_mult_one_left = thm"complex_mult_one_left";
-val complex_mult_one_right = thm"complex_mult_one_right";
-val complex_inverse = thm"complex_inverse";
-val complex_of_real_one = thm"complex_of_real_one";
-val complex_of_real_zero = thm"complex_of_real_zero";
-val complex_of_real_eq_iff = thm"complex_of_real_eq_iff";
-val complex_of_real_minus = thm"complex_of_real_minus";
-val complex_of_real_inverse = thm"complex_of_real_inverse";
-val complex_of_real_add = thm"complex_of_real_add";
-val complex_of_real_diff = thm"complex_of_real_diff";
-val complex_of_real_mult = thm"complex_of_real_mult";
-val complex_of_real_divide = thm"complex_of_real_divide";
-val complex_of_real_pow = thm"complex_of_real_pow";
-val complex_mod = thm"complex_mod";
-val complex_mod_zero = thm"complex_mod_zero";
-val complex_mod_one = thm"complex_mod_one";
-val complex_mod_complex_of_real = thm"complex_mod_complex_of_real";
-val complex_of_real_abs = thm"complex_of_real_abs";
-val complex_cnj = thm"complex_cnj";
-val complex_cnj_cancel_iff = thm"complex_cnj_cancel_iff";
-val complex_cnj_cnj = thm"complex_cnj_cnj";
-val complex_cnj_complex_of_real = thm"complex_cnj_complex_of_real";
-val complex_mod_cnj = thm"complex_mod_cnj";
-val complex_cnj_minus = thm"complex_cnj_minus";
-val complex_cnj_inverse = thm"complex_cnj_inverse";
-val complex_cnj_add = thm"complex_cnj_add";
-val complex_cnj_diff = thm"complex_cnj_diff";
-val complex_cnj_mult = thm"complex_cnj_mult";
-val complex_cnj_divide = thm"complex_cnj_divide";
-val complex_cnj_one = thm"complex_cnj_one";
-val complex_cnj_pow = thm"complex_cnj_pow";
-val complex_add_cnj = thm"complex_add_cnj";
-val complex_diff_cnj = thm"complex_diff_cnj";
-val complex_cnj_zero = thm"complex_cnj_zero";
-val complex_cnj_zero_iff = thm"complex_cnj_zero_iff";
-val complex_mult_cnj = thm"complex_mult_cnj";
-val complex_mod_eq_zero_cancel = thm"complex_mod_eq_zero_cancel";
-val complex_mod_complex_of_real_of_nat = thm"complex_mod_complex_of_real_of_nat";
-val complex_mod_minus = thm"complex_mod_minus";
-val complex_mod_mult_cnj = thm"complex_mod_mult_cnj";
-val complex_mod_squared = thm"complex_mod_squared";
-val complex_mod_ge_zero = thm"complex_mod_ge_zero";
-val abs_cmod_cancel = thm"abs_cmod_cancel";
-val complex_mod_mult = thm"complex_mod_mult";
-val complex_mod_add_squared_eq = thm"complex_mod_add_squared_eq";
-val complex_Re_mult_cnj_le_cmod = thm"complex_Re_mult_cnj_le_cmod";
-val complex_Re_mult_cnj_le_cmod2 = thm"complex_Re_mult_cnj_le_cmod2";
-val real_sum_squared_expand = thm"real_sum_squared_expand";
-val complex_mod_triangle_squared = thm"complex_mod_triangle_squared";
-val complex_mod_minus_le_complex_mod = thm"complex_mod_minus_le_complex_mod";
-val complex_mod_triangle_ineq = thm"complex_mod_triangle_ineq";
-val complex_mod_triangle_ineq2 = thm"complex_mod_triangle_ineq2";
-val complex_mod_diff_commute = thm"complex_mod_diff_commute";
-val complex_mod_add_less = thm"complex_mod_add_less";
-val complex_mod_mult_less = thm"complex_mod_mult_less";
-val complex_mod_diff_ineq = thm"complex_mod_diff_ineq";
-val complex_Re_le_cmod = thm"complex_Re_le_cmod";
-val complex_mod_gt_zero = thm"complex_mod_gt_zero";
-val complex_mod_complexpow = thm"complex_mod_complexpow";
-val complex_mod_inverse = thm"complex_mod_inverse";
-val complex_mod_divide = thm"complex_mod_divide";
-val complexpow_i_squared = thm"complexpow_i_squared";
-val complex_i_not_zero = thm"complex_i_not_zero";
-val sgn_zero = thm"sgn_zero";
-val sgn_one = thm"sgn_one";
-val sgn_minus = thm"sgn_minus";
-val sgn_eq = thm"sgn_eq";
-val i_mult_eq = thm"i_mult_eq";
-val i_mult_eq2 = thm"i_mult_eq2";
-val Re_sgn = thm"Re_sgn";
-val Im_sgn = thm"Im_sgn";
-val complex_inverse_complex_split = thm"complex_inverse_complex_split";
-val cos_arg_i_mult_zero = thm"cos_arg_i_mult_zero";
-val complex_of_real_zero_iff = thm"complex_of_real_zero_iff";
-val rcis_Ex = thm"rcis_Ex";
-val Re_rcis = thm"Re_rcis";
-val Im_rcis = thm"Im_rcis";
-val complex_mod_rcis = thm"complex_mod_rcis";
-val complex_mod_sqrt_Re_mult_cnj = thm"complex_mod_sqrt_Re_mult_cnj";
-val complex_Re_cnj = thm"complex_Re_cnj";
-val complex_Im_cnj = thm"complex_Im_cnj";
-val complex_In_mult_cnj_zero = thm"complex_In_mult_cnj_zero";
-val complex_Re_mult = thm"complex_Re_mult";
-val complex_Re_mult_complex_of_real = thm"complex_Re_mult_complex_of_real";
-val complex_Im_mult_complex_of_real = thm"complex_Im_mult_complex_of_real";
-val complex_Re_mult_complex_of_real2 = thm"complex_Re_mult_complex_of_real2";
-val complex_Im_mult_complex_of_real2 = thm"complex_Im_mult_complex_of_real2";
-val cis_rcis_eq = thm"cis_rcis_eq";
-val rcis_mult = thm"rcis_mult";
-val cis_mult = thm"cis_mult";
-val cis_zero = thm"cis_zero";
-val rcis_zero_mod = thm"rcis_zero_mod";
-val rcis_zero_arg = thm"rcis_zero_arg";
-val complex_of_real_minus_one = thm"complex_of_real_minus_one";
-val complex_i_mult_minus = thm"complex_i_mult_minus";
-val cis_real_of_nat_Suc_mult = thm"cis_real_of_nat_Suc_mult";
-val DeMoivre = thm"DeMoivre";
-val DeMoivre2 = thm"DeMoivre2";
-val cis_inverse = thm"cis_inverse";
-val rcis_inverse = thm"rcis_inverse";
-val cis_divide = thm"cis_divide";
-val rcis_divide = thm"rcis_divide";
-val Re_cis = thm"Re_cis";
-val Im_cis = thm"Im_cis";
-val cos_n_Re_cis_pow_n = thm"cos_n_Re_cis_pow_n";
-val sin_n_Im_cis_pow_n = thm"sin_n_Im_cis_pow_n";
-val expi_add = thm"expi_add";
-val expi_zero = thm"expi_zero";
-val complex_Re_mult_eq = thm"complex_Re_mult_eq";
-val complex_Im_mult_eq = thm"complex_Im_mult_eq";
-val complex_expi_Ex = thm"complex_expi_Ex";
-*}
-
end
--- a/src/HOL/Complex/NSCA.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/NSCA.thy Fri Jun 02 23:22:29 2006 +0200
@@ -9,34 +9,34 @@
imports NSComplex
begin
-constdefs
+definition
CInfinitesimal :: "hcomplex set"
- "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
+ "CInfinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
capprox :: "[hcomplex,hcomplex] => bool" (infixl "@c=" 50)
--{*the ``infinitely close'' relation*}
- "x @c= y == (x - y) \<in> CInfinitesimal"
+ "x @c= y = ((x - y) \<in> CInfinitesimal)"
(* standard complex numbers reagarded as an embedded subset of NS complex *)
SComplex :: "hcomplex set"
- "SComplex == {x. \<exists>r. x = hcomplex_of_complex r}"
+ "SComplex = {x. \<exists>r. x = hcomplex_of_complex r}"
CFinite :: "hcomplex set"
- "CFinite == {x. \<exists>r \<in> Reals. hcmod x < r}"
+ "CFinite = {x. \<exists>r \<in> Reals. hcmod x < r}"
CInfinite :: "hcomplex set"
- "CInfinite == {x. \<forall>r \<in> Reals. r < hcmod x}"
+ "CInfinite = {x. \<forall>r \<in> Reals. r < hcmod x}"
stc :: "hcomplex => hcomplex"
--{* standard part map*}
- "stc x == (@r. x \<in> CFinite & r:SComplex & r @c= x)"
+ "stc x = (SOME r. x \<in> CFinite & r:SComplex & r @c= x)"
cmonad :: "hcomplex => hcomplex set"
- "cmonad x == {y. x @c= y}"
+ "cmonad x = {y. x @c= y}"
cgalaxy :: "hcomplex => hcomplex set"
- "cgalaxy x == {y. (x - y) \<in> CFinite}"
+ "cgalaxy x = {y. (x - y) \<in> CFinite}"
@@ -1217,222 +1217,4 @@
"(0 @c= hcomplex_of_complex z) = (z = 0)"
by (simp add: star_of_zero [symmetric] del: star_of_zero)
-
-ML
-{*
-val SComplex_add = thm "SComplex_add";
-val SComplex_mult = thm "SComplex_mult";
-val SComplex_inverse = thm "SComplex_inverse";
-val SComplex_divide = thm "SComplex_divide";
-val SComplex_minus = thm "SComplex_minus";
-val SComplex_minus_iff = thm "SComplex_minus_iff";
-val SComplex_diff = thm "SComplex_diff";
-val SComplex_add_cancel = thm "SComplex_add_cancel";
-val SReal_hcmod_hcomplex_of_complex = thm "SReal_hcmod_hcomplex_of_complex";
-val SReal_hcmod_number_of = thm "SReal_hcmod_number_of";
-val SReal_hcmod_SComplex = thm "SReal_hcmod_SComplex";
-val SComplex_hcomplex_of_complex = thm "SComplex_hcomplex_of_complex";
-val SComplex_number_of = thm "SComplex_number_of";
-val SComplex_divide_number_of = thm "SComplex_divide_number_of";
-val SComplex_UNIV_complex = thm "SComplex_UNIV_complex";
-val SComplex_iff = thm "SComplex_iff";
-val hcomplex_of_complex_image = thm "hcomplex_of_complex_image";
-val inv_hcomplex_of_complex_image = thm "inv_hcomplex_of_complex_image";
-val SComplex_hcomplex_of_complex_image = thm "SComplex_hcomplex_of_complex_image";
-val SComplex_SReal_dense = thm "SComplex_SReal_dense";
-val SComplex_hcmod_SReal = thm "SComplex_hcmod_SReal";
-val SComplex_zero = thm "SComplex_zero";
-val SComplex_one = thm "SComplex_one";
-val CFinite_add = thm "CFinite_add";
-val CFinite_mult = thm "CFinite_mult";
-val CFinite_minus_iff = thm "CFinite_minus_iff";
-val SComplex_subset_CFinite = thm "SComplex_subset_CFinite";
-val HFinite_hcmod_hcomplex_of_complex = thm "HFinite_hcmod_hcomplex_of_complex";
-val CFinite_hcomplex_of_complex = thm "CFinite_hcomplex_of_complex";
-val CFiniteD = thm "CFiniteD";
-val CFinite_hcmod_iff = thm "CFinite_hcmod_iff";
-val CFinite_number_of = thm "CFinite_number_of";
-val CFinite_bounded = thm "CFinite_bounded";
-val CInfinitesimal_zero = thm "CInfinitesimal_zero";
-val hcomplex_sum_of_halves = thm "hcomplex_sum_of_halves";
-val CInfinitesimal_hcmod_iff = thm "CInfinitesimal_hcmod_iff";
-val one_not_CInfinitesimal = thm "one_not_CInfinitesimal";
-val CInfinitesimal_add = thm "CInfinitesimal_add";
-val CInfinitesimal_minus_iff = thm "CInfinitesimal_minus_iff";
-val CInfinitesimal_diff = thm "CInfinitesimal_diff";
-val CInfinitesimal_mult = thm "CInfinitesimal_mult";
-val CInfinitesimal_CFinite_mult = thm "CInfinitesimal_CFinite_mult";
-val CInfinitesimal_CFinite_mult2 = thm "CInfinitesimal_CFinite_mult2";
-val CInfinite_hcmod_iff = thm "CInfinite_hcmod_iff";
-val CInfinite_inverse_CInfinitesimal = thm "CInfinite_inverse_CInfinitesimal";
-val CInfinite_mult = thm "CInfinite_mult";
-val CInfinite_minus_iff = thm "CInfinite_minus_iff";
-val CFinite_sum_squares = thm "CFinite_sum_squares";
-val not_CInfinitesimal_not_zero = thm "not_CInfinitesimal_not_zero";
-val not_CInfinitesimal_not_zero2 = thm "not_CInfinitesimal_not_zero2";
-val CFinite_diff_CInfinitesimal_hcmod = thm "CFinite_diff_CInfinitesimal_hcmod";
-val hcmod_less_CInfinitesimal = thm "hcmod_less_CInfinitesimal";
-val hcmod_le_CInfinitesimal = thm "hcmod_le_CInfinitesimal";
-val CInfinitesimal_interval = thm "CInfinitesimal_interval";
-val CInfinitesimal_interval2 = thm "CInfinitesimal_interval2";
-val not_CInfinitesimal_mult = thm "not_CInfinitesimal_mult";
-val CInfinitesimal_mult_disj = thm "CInfinitesimal_mult_disj";
-val CFinite_CInfinitesimal_diff_mult = thm "CFinite_CInfinitesimal_diff_mult";
-val CInfinitesimal_subset_CFinite = thm "CInfinitesimal_subset_CFinite";
-val CInfinitesimal_hcomplex_of_complex_mult = thm "CInfinitesimal_hcomplex_of_complex_mult";
-val CInfinitesimal_hcomplex_of_complex_mult2 = thm "CInfinitesimal_hcomplex_of_complex_mult2";
-val mem_cinfmal_iff = thm "mem_cinfmal_iff";
-val capprox_minus_iff = thm "capprox_minus_iff";
-val capprox_minus_iff2 = thm "capprox_minus_iff2";
-val capprox_refl = thm "capprox_refl";
-val capprox_sym = thm "capprox_sym";
-val capprox_trans = thm "capprox_trans";
-val capprox_trans2 = thm "capprox_trans2";
-val capprox_trans3 = thm "capprox_trans3";
-val number_of_capprox_reorient = thm "number_of_capprox_reorient";
-val CInfinitesimal_capprox_minus = thm "CInfinitesimal_capprox_minus";
-val capprox_monad_iff = thm "capprox_monad_iff";
-val Infinitesimal_capprox = thm "Infinitesimal_capprox";
-val capprox_add = thm "capprox_add";
-val capprox_minus = thm "capprox_minus";
-val capprox_minus2 = thm "capprox_minus2";
-val capprox_minus_cancel = thm "capprox_minus_cancel";
-val capprox_add_minus = thm "capprox_add_minus";
-val capprox_mult1 = thm "capprox_mult1";
-val capprox_mult2 = thm "capprox_mult2";
-val capprox_mult_subst = thm "capprox_mult_subst";
-val capprox_mult_subst2 = thm "capprox_mult_subst2";
-val capprox_mult_subst_SComplex = thm "capprox_mult_subst_SComplex";
-val capprox_eq_imp = thm "capprox_eq_imp";
-val CInfinitesimal_minus_capprox = thm "CInfinitesimal_minus_capprox";
-val bex_CInfinitesimal_iff = thm "bex_CInfinitesimal_iff";
-val bex_CInfinitesimal_iff2 = thm "bex_CInfinitesimal_iff2";
-val CInfinitesimal_add_capprox = thm "CInfinitesimal_add_capprox";
-val CInfinitesimal_add_capprox_self = thm "CInfinitesimal_add_capprox_self";
-val CInfinitesimal_add_capprox_self2 = thm "CInfinitesimal_add_capprox_self2";
-val CInfinitesimal_add_minus_capprox_self = thm "CInfinitesimal_add_minus_capprox_self";
-val CInfinitesimal_add_cancel = thm "CInfinitesimal_add_cancel";
-val CInfinitesimal_add_right_cancel = thm "CInfinitesimal_add_right_cancel";
-val capprox_add_left_cancel = thm "capprox_add_left_cancel";
-val capprox_add_right_cancel = thm "capprox_add_right_cancel";
-val capprox_add_mono1 = thm "capprox_add_mono1";
-val capprox_add_mono2 = thm "capprox_add_mono2";
-val capprox_add_left_iff = thm "capprox_add_left_iff";
-val capprox_add_right_iff = thm "capprox_add_right_iff";
-val capprox_CFinite = thm "capprox_CFinite";
-val capprox_hcomplex_of_complex_CFinite = thm "capprox_hcomplex_of_complex_CFinite";
-val capprox_mult_CFinite = thm "capprox_mult_CFinite";
-val capprox_mult_hcomplex_of_complex = thm "capprox_mult_hcomplex_of_complex";
-val capprox_SComplex_mult_cancel_zero = thm "capprox_SComplex_mult_cancel_zero";
-val capprox_mult_SComplex1 = thm "capprox_mult_SComplex1";
-val capprox_mult_SComplex2 = thm "capprox_mult_SComplex2";
-val capprox_mult_SComplex_zero_cancel_iff = thm "capprox_mult_SComplex_zero_cancel_iff";
-val capprox_SComplex_mult_cancel = thm "capprox_SComplex_mult_cancel";
-val capprox_SComplex_mult_cancel_iff1 = thm "capprox_SComplex_mult_cancel_iff1";
-val capprox_hcmod_approx_zero = thm "capprox_hcmod_approx_zero";
-val capprox_approx_zero_iff = thm "capprox_approx_zero_iff";
-val capprox_minus_zero_cancel_iff = thm "capprox_minus_zero_cancel_iff";
-val Infinitesimal_hcmod_add_diff = thm "Infinitesimal_hcmod_add_diff";
-val approx_hcmod_add_hcmod = thm "approx_hcmod_add_hcmod";
-val capprox_hcmod_approx = thm "capprox_hcmod_approx";
-val CInfinitesimal_less_SComplex = thm "CInfinitesimal_less_SComplex";
-val SComplex_Int_CInfinitesimal_zero = thm "SComplex_Int_CInfinitesimal_zero";
-val SComplex_CInfinitesimal_zero = thm "SComplex_CInfinitesimal_zero";
-val SComplex_CFinite_diff_CInfinitesimal = thm "SComplex_CFinite_diff_CInfinitesimal";
-val hcomplex_of_complex_CFinite_diff_CInfinitesimal = thm "hcomplex_of_complex_CFinite_diff_CInfinitesimal";
-val hcomplex_of_complex_CInfinitesimal_iff_0 = thm "hcomplex_of_complex_CInfinitesimal_iff_0";
-val number_of_not_CInfinitesimal = thm "number_of_not_CInfinitesimal";
-val capprox_SComplex_not_zero = thm "capprox_SComplex_not_zero";
-val CFinite_diff_CInfinitesimal_capprox = thm "CFinite_diff_CInfinitesimal_capprox";
-val CInfinitesimal_ratio = thm "CInfinitesimal_ratio";
-val SComplex_capprox_iff = thm "SComplex_capprox_iff";
-val number_of_capprox_iff = thm "number_of_capprox_iff";
-val number_of_CInfinitesimal_iff = thm "number_of_CInfinitesimal_iff";
-val hcomplex_of_complex_approx_iff = thm "hcomplex_of_complex_approx_iff";
-val hcomplex_of_complex_capprox_number_of_iff = thm "hcomplex_of_complex_capprox_number_of_iff";
-val capprox_unique_complex = thm "capprox_unique_complex";
-val hcomplex_capproxD1 = thm "hcomplex_capproxD1";
-val hcomplex_capproxD2 = thm "hcomplex_capproxD2";
-val hcomplex_capproxI = thm "hcomplex_capproxI";
-val capprox_approx_iff = thm "capprox_approx_iff";
-val hcomplex_of_hypreal_capprox_iff = thm "hcomplex_of_hypreal_capprox_iff";
-val CFinite_HFinite_Re = thm "CFinite_HFinite_Re";
-val CFinite_HFinite_Im = thm "CFinite_HFinite_Im";
-val HFinite_Re_Im_CFinite = thm "HFinite_Re_Im_CFinite";
-val CFinite_HFinite_iff = thm "CFinite_HFinite_iff";
-val SComplex_Re_SReal = thm "SComplex_Re_SReal";
-val SComplex_Im_SReal = thm "SComplex_Im_SReal";
-val Reals_Re_Im_SComplex = thm "Reals_Re_Im_SComplex";
-val SComplex_SReal_iff = thm "SComplex_SReal_iff";
-val CInfinitesimal_Infinitesimal_iff = thm "CInfinitesimal_Infinitesimal_iff";
-val eq_Abs_star_Bex = thm "eq_Abs_star_Bex";
-val stc_part_Ex = thm "stc_part_Ex";
-val stc_part_Ex1 = thm "stc_part_Ex1";
-val CFinite_Int_CInfinite_empty = thm "CFinite_Int_CInfinite_empty";
-val CFinite_not_CInfinite = thm "CFinite_not_CInfinite";
-val not_CFinite_CInfinite = thm "not_CFinite_CInfinite";
-val CInfinite_CFinite_disj = thm "CInfinite_CFinite_disj";
-val CInfinite_CFinite_iff = thm "CInfinite_CFinite_iff";
-val CFinite_CInfinite_iff = thm "CFinite_CInfinite_iff";
-val CInfinite_diff_CFinite_CInfinitesimal_disj = thm "CInfinite_diff_CFinite_CInfinitesimal_disj";
-val CFinite_inverse = thm "CFinite_inverse";
-val CFinite_inverse2 = thm "CFinite_inverse2";
-val CInfinitesimal_inverse_CFinite = thm "CInfinitesimal_inverse_CFinite";
-val CFinite_not_CInfinitesimal_inverse = thm "CFinite_not_CInfinitesimal_inverse";
-val capprox_inverse = thm "capprox_inverse";
-val hcomplex_of_complex_capprox_inverse = thms "hcomplex_of_complex_capprox_inverse";
-val inverse_add_CInfinitesimal_capprox = thm "inverse_add_CInfinitesimal_capprox";
-val inverse_add_CInfinitesimal_capprox2 = thm "inverse_add_CInfinitesimal_capprox2";
-val inverse_add_CInfinitesimal_approx_CInfinitesimal = thm "inverse_add_CInfinitesimal_approx_CInfinitesimal";
-val CInfinitesimal_square_iff = thm "CInfinitesimal_square_iff";
-val capprox_CFinite_mult_cancel = thm "capprox_CFinite_mult_cancel";
-val capprox_CFinite_mult_cancel_iff1 = thm "capprox_CFinite_mult_cancel_iff1";
-val capprox_cmonad_iff = thm "capprox_cmonad_iff";
-val CInfinitesimal_cmonad_eq = thm "CInfinitesimal_cmonad_eq";
-val mem_cmonad_iff = thm "mem_cmonad_iff";
-val CInfinitesimal_cmonad_zero_iff = thm "CInfinitesimal_cmonad_zero_iff";
-val cmonad_zero_minus_iff = thm "cmonad_zero_minus_iff";
-val cmonad_zero_hcmod_iff = thm "cmonad_zero_hcmod_iff";
-val mem_cmonad_self = thm "mem_cmonad_self";
-val stc_capprox_self = thm "stc_capprox_self";
-val stc_SComplex = thm "stc_SComplex";
-val stc_CFinite = thm "stc_CFinite";
-val stc_SComplex_eq = thm "stc_SComplex_eq";
-val stc_hcomplex_of_complex = thm "stc_hcomplex_of_complex";
-val stc_eq_capprox = thm "stc_eq_capprox";
-val capprox_stc_eq = thm "capprox_stc_eq";
-val stc_eq_capprox_iff = thm "stc_eq_capprox_iff";
-val stc_CInfinitesimal_add_SComplex = thm "stc_CInfinitesimal_add_SComplex";
-val stc_CInfinitesimal_add_SComplex2 = thm "stc_CInfinitesimal_add_SComplex2";
-val CFinite_stc_CInfinitesimal_add = thm "CFinite_stc_CInfinitesimal_add";
-val stc_add = thm "stc_add";
-val stc_number_of = thm "stc_number_of";
-val stc_zero = thm "stc_zero";
-val stc_one = thm "stc_one";
-val stc_minus = thm "stc_minus";
-val stc_diff = thm "stc_diff";
-val lemma_stc_mult = thm "lemma_stc_mult";
-val stc_mult = thm "stc_mult";
-val stc_CInfinitesimal = thm "stc_CInfinitesimal";
-val stc_not_CInfinitesimal = thm "stc_not_CInfinitesimal";
-val stc_inverse = thm "stc_inverse";
-val stc_divide = thm "stc_divide";
-val stc_idempotent = thm "stc_idempotent";
-val CFinite_HFinite_hcomplex_of_hypreal = thm "CFinite_HFinite_hcomplex_of_hypreal";
-val SComplex_SReal_hcomplex_of_hypreal = thm "SComplex_SReal_hcomplex_of_hypreal";
-val stc_hcomplex_of_hypreal = thm "stc_hcomplex_of_hypreal";
-val CInfinitesimal_hcnj_iff = thm "CInfinitesimal_hcnj_iff";
-val CInfinite_HInfinite_iff = thm "CInfinite_HInfinite_iff";
-val hcomplex_split_CInfinitesimal_iff = thm "hcomplex_split_CInfinitesimal_iff";
-val hcomplex_split_CFinite_iff = thm "hcomplex_split_CFinite_iff";
-val hcomplex_split_SComplex_iff = thm "hcomplex_split_SComplex_iff";
-val hcomplex_split_CInfinite_iff = thm "hcomplex_split_CInfinite_iff";
-val hcomplex_split_capprox_iff = thm "hcomplex_split_capprox_iff";
-val complex_seq_to_hcomplex_CInfinitesimal = thm "complex_seq_to_hcomplex_CInfinitesimal";
-val CInfinitesimal_hcomplex_of_hypreal_epsilon = thm "CInfinitesimal_hcomplex_of_hypreal_epsilon";
-val hcomplex_of_complex_approx_zero_iff = thm "hcomplex_of_complex_approx_zero_iff";
-val hcomplex_of_complex_approx_zero_iff2 = thm "hcomplex_of_complex_approx_zero_iff2";
-*}
-
-
end
--- a/src/HOL/Complex/NSComplex.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/NSComplex.thy Fri Jun 02 23:22:29 2006 +0200
@@ -13,66 +13,67 @@
types hcomplex = "complex star"
-syntax hcomplex_of_complex :: "real => real star"
-translations "hcomplex_of_complex" => "star_of :: complex => complex star"
+abbreviation
+ hcomplex_of_complex :: "complex => complex star"
+ "hcomplex_of_complex == star_of"
-constdefs
+definition
(*--- real and Imaginary parts ---*)
hRe :: "hcomplex => hypreal"
- "hRe == *f* Re"
+ "hRe = *f* Re"
hIm :: "hcomplex => hypreal"
- "hIm == *f* Im"
+ "hIm = *f* Im"
(*----------- modulus ------------*)
hcmod :: "hcomplex => hypreal"
- "hcmod == *f* cmod"
+ "hcmod = *f* cmod"
(*------ imaginary unit ----------*)
iii :: hcomplex
- "iii == star_of ii"
+ "iii = star_of ii"
(*------- complex conjugate ------*)
hcnj :: "hcomplex => hcomplex"
- "hcnj == *f* cnj"
+ "hcnj = *f* cnj"
(*------------ Argand -------------*)
hsgn :: "hcomplex => hcomplex"
- "hsgn == *f* sgn"
+ "hsgn = *f* sgn"
harg :: "hcomplex => hypreal"
- "harg == *f* arg"
+ "harg = *f* arg"
(* abbreviation for (cos a + i sin a) *)
hcis :: "hypreal => hcomplex"
- "hcis == *f* cis"
+ "hcis = *f* cis"
(*----- injection from hyperreals -----*)
hcomplex_of_hypreal :: "hypreal => hcomplex"
- "hcomplex_of_hypreal == *f* complex_of_real"
+ "hcomplex_of_hypreal = *f* complex_of_real"
(* abbreviation for r*(cos a + i sin a) *)
hrcis :: "[hypreal, hypreal] => hcomplex"
- "hrcis == *f2* rcis"
+ "hrcis = *f2* rcis"
(*------------ e ^ (x + iy) ------------*)
hexpi :: "hcomplex => hcomplex"
- "hexpi == *f* expi"
+ "hexpi = *f* expi"
HComplex :: "[hypreal,hypreal] => hcomplex"
- "HComplex == *f2* Complex"
+ "HComplex = *f2* Complex"
hcpow :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80)
- "(z::hcomplex) hcpow (n::hypnat) == ( *f2* op ^) z n"
+ "(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n"
lemmas hcomplex_defs [transfer_unfold] =
hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def
@@ -921,158 +922,4 @@
"hIm(number_of v :: hcomplex) = 0"
by (transfer, simp)
-
-ML
-{*
-val iii_def = thm"iii_def";
-
-val hRe = thm"hRe";
-val hIm = thm"hIm";
-val hcomplex_hRe_hIm_cancel_iff = thm"hcomplex_hRe_hIm_cancel_iff";
-val hcomplex_hRe_zero = thm"hcomplex_hRe_zero";
-val hcomplex_hIm_zero = thm"hcomplex_hIm_zero";
-val hcomplex_hRe_one = thm"hcomplex_hRe_one";
-val hcomplex_hIm_one = thm"hcomplex_hIm_one";
-val inj_hcomplex_of_complex = thm"inj_hcomplex_of_complex";
-val hcomplex_of_complex_i = thm"hcomplex_of_complex_i";
-val star_n_add = thm"star_n_add";
-val hRe_add = thm"hRe_add";
-val hIm_add = thm"hIm_add";
-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_diff_eq_eq = thm"hcomplex_diff_eq_eq";
-val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one";
-val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right";
-val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel";
-val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel";
-val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib";
-val hcomplex_of_hypreal = thm"hcomplex_of_hypreal";
-val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff";
-val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus";
-val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse";
-val hcomplex_of_hypreal_add = thm"hcomplex_of_hypreal_add";
-val hcomplex_of_hypreal_diff = thm"hcomplex_of_hypreal_diff";
-val hcomplex_of_hypreal_mult = thm"hcomplex_of_hypreal_mult";
-val hcomplex_of_hypreal_divide = thm"hcomplex_of_hypreal_divide";
-val hcomplex_of_hypreal_one = thm"hcomplex_of_hypreal_one";
-val hcomplex_of_hypreal_zero = thm"hcomplex_of_hypreal_zero";
-val hcomplex_of_hypreal_pow = thm"hcomplex_of_hypreal_pow";
-val hRe_hcomplex_of_hypreal = thm"hRe_hcomplex_of_hypreal";
-val hIm_hcomplex_of_hypreal = thm"hIm_hcomplex_of_hypreal";
-val hcomplex_of_hypreal_epsilon_not_zero = thm"hcomplex_of_hypreal_epsilon_not_zero";
-val hcmod = thm"hcmod";
-val hcmod_zero = thm"hcmod_zero";
-val hcmod_one = thm"hcmod_one";
-val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal";
-val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs";
-val hcnj = thm"hcnj";
-val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff";
-val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj";
-val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal";
-val hcomplex_hmod_hcnj = thm"hcomplex_hmod_hcnj";
-val hcomplex_hcnj_minus = thm"hcomplex_hcnj_minus";
-val hcomplex_hcnj_inverse = thm"hcomplex_hcnj_inverse";
-val hcomplex_hcnj_add = thm"hcomplex_hcnj_add";
-val hcomplex_hcnj_diff = thm"hcomplex_hcnj_diff";
-val hcomplex_hcnj_mult = thm"hcomplex_hcnj_mult";
-val hcomplex_hcnj_divide = thm"hcomplex_hcnj_divide";
-val hcnj_one = thm"hcnj_one";
-val hcomplex_hcnj_pow = thm"hcomplex_hcnj_pow";
-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_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel";
-
-val hcmod_hcomplex_of_hypreal_of_nat = thm"hcmod_hcomplex_of_hypreal_of_nat";
-val hcmod_hcomplex_of_hypreal_of_hypnat = thm"hcmod_hcomplex_of_hypreal_of_hypnat";
-val hcmod_minus = thm"hcmod_minus";
-val hcmod_mult_hcnj = thm"hcmod_mult_hcnj";
-val hcmod_ge_zero = thm"hcmod_ge_zero";
-val hrabs_hcmod_cancel = thm"hrabs_hcmod_cancel";
-val hcmod_mult = thm"hcmod_mult";
-val hcmod_add_squared_eq = thm"hcmod_add_squared_eq";
-val hcomplex_hRe_mult_hcnj_le_hcmod = thm"hcomplex_hRe_mult_hcnj_le_hcmod";
-val hcomplex_hRe_mult_hcnj_le_hcmod2 = thm"hcomplex_hRe_mult_hcnj_le_hcmod2";
-val hcmod_triangle_squared = thm"hcmod_triangle_squared";
-val hcmod_triangle_ineq = thm"hcmod_triangle_ineq";
-val hcmod_triangle_ineq2 = thm"hcmod_triangle_ineq2";
-val hcmod_diff_commute = thm"hcmod_diff_commute";
-val hcmod_add_less = thm"hcmod_add_less";
-val hcmod_mult_less = thm"hcmod_mult_less";
-val hcmod_diff_ineq = thm"hcmod_diff_ineq";
-val hcpow = thm"hcpow";
-val hcomplex_of_hypreal_hyperpow = thm"hcomplex_of_hypreal_hyperpow";
-val hcmod_hcomplexpow = thm"hcmod_hcomplexpow";
-val hcmod_hcpow = thm"hcmod_hcpow";
-val hcpow_minus = thm"hcpow_minus";
-val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
-val hcmod_divide = thm"hcmod_divide";
-val hcpow_mult = thm"hcpow_mult";
-val hcpow_zero = thm"hcpow_zero";
-val hcpow_zero2 = thm"hcpow_zero2";
-val hcpow_not_zero = thm"hcpow_not_zero";
-val hcpow_zero_zero = thm"hcpow_zero_zero";
-val hcomplex_i_mult_eq = thm"hcomplex_i_mult_eq";
-val hcomplexpow_i_squared = thm"hcomplexpow_i_squared";
-val hcomplex_i_not_zero = thm"hcomplex_i_not_zero";
-val star_n_divide = thm"star_n_divide";
-val hsgn = thm"hsgn";
-val hsgn_zero = thm"hsgn_zero";
-val hsgn_one = thm"hsgn_one";
-val hsgn_minus = thm"hsgn_minus";
-val hsgn_eq = thm"hsgn_eq";
-val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2";
-val hcmod_i = thm"hcmod_i";
-val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2";
-val hRe_hsgn = thm"hRe_hsgn";
-val hIm_hsgn = thm"hIm_hsgn";
-val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff";
-val hRe_mult_i_eq = thm"hRe_mult_i_eq";
-val hIm_mult_i_eq = thm"hIm_mult_i_eq";
-val hcmod_mult_i = thm"hcmod_mult_i";
-val hcmod_mult_i2 = thm"hcmod_mult_i2";
-val harg = thm"harg";
-val cos_harg_i_mult_zero = thm"cos_harg_i_mult_zero";
-val hcomplex_of_hypreal_zero_iff = thm"hcomplex_of_hypreal_zero_iff";
-val complex_split_polar2 = thm"complex_split_polar2";
-val hcomplex_split_polar = thm"hcomplex_split_polar";
-val hcis = thm"hcis";
-val hcis_eq = thm"hcis_eq";
-val hrcis = thm"hrcis";
-val hrcis_Ex = thm"hrcis_Ex";
-val hRe_hcomplex_polar = thm"hRe_hcomplex_polar";
-val hRe_hrcis = thm"hRe_hrcis";
-val hIm_hcomplex_polar = thm"hIm_hcomplex_polar";
-val hIm_hrcis = thm"hIm_hrcis";
-val hcmod_complex_polar = thm"hcmod_complex_polar";
-val hcmod_hrcis = thm"hcmod_hrcis";
-val hcis_hrcis_eq = thm"hcis_hrcis_eq";
-val hrcis_mult = thm"hrcis_mult";
-val hcis_mult = thm"hcis_mult";
-val hcis_zero = thm"hcis_zero";
-val hrcis_zero_mod = thm"hrcis_zero_mod";
-val hrcis_zero_arg = thm"hrcis_zero_arg";
-val hcomplex_i_mult_minus = thm"hcomplex_i_mult_minus";
-val hcomplex_i_mult_minus2 = thm"hcomplex_i_mult_minus2";
-val hcis_hypreal_of_nat_Suc_mult = thm"hcis_hypreal_of_nat_Suc_mult";
-val NSDeMoivre = thm"NSDeMoivre";
-val hcis_hypreal_of_hypnat_Suc_mult = thm"hcis_hypreal_of_hypnat_Suc_mult";
-val NSDeMoivre_ext = thm"NSDeMoivre_ext";
-val DeMoivre2 = thm"DeMoivre2";
-val DeMoivre2_ext = thm"DeMoivre2_ext";
-val hcis_inverse = thm"hcis_inverse";
-val hrcis_inverse = thm"hrcis_inverse";
-val hRe_hcis = thm"hRe_hcis";
-val hIm_hcis = thm"hIm_hcis";
-val cos_n_hRe_hcis_pow_n = thm"cos_n_hRe_hcis_pow_n";
-val sin_n_hIm_hcis_pow_n = thm"sin_n_hIm_hcis_pow_n";
-val cos_n_hRe_hcis_hcpow_n = thm"cos_n_hRe_hcis_hcpow_n";
-val sin_n_hIm_hcis_hcpow_n = thm"sin_n_hIm_hcis_hcpow_n";
-val hexpi_add = thm"hexpi_add";
-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";
-*}
-
end
--- a/src/HOL/Hyperreal/EvenOdd.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/EvenOdd.thy Fri Jun 02 23:22:29 2006 +0200
@@ -86,24 +86,4 @@
lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
by (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst], simp)
-ML
-{*
-val even_nat_Suc = thm"Parity.even_nat_Suc";
-
-val even_mult_two_ex = thm "even_mult_two_ex";
-val odd_Suc_mult_two_ex = thm "odd_Suc_mult_two_ex";
-val even_add = thm "even_add";
-val odd_add = thm "odd_add";
-val Suc_n_div_2_gt_zero = thm "Suc_n_div_2_gt_zero";
-val div_2_gt_zero = thm "div_2_gt_zero";
-val even_num_iff = thm "even_num_iff";
-val nat_mod_div_trivial = thm "nat_mod_div_trivial";
-val nat_mod_mod_trivial = thm "nat_mod_mod_trivial";
-val mod_Suc_eq_Suc_mod = thm "mod_Suc_eq_Suc_mod";
-val even_even_mod_4_iff = thm "even_even_mod_4_iff";
-val lemma_odd_mod_4_div_2 = thm "lemma_odd_mod_4_div_2";
-val lemma_even_mod_4_div_2 = thm "lemma_even_mod_4_div_2";
-*}
-
end
-
--- a/src/HOL/Hyperreal/Fact.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Fact.thy Fri Jun 02 23:22:29 2006 +0200
@@ -12,65 +12,65 @@
consts fact :: "nat => nat"
primrec
- fact_0: "fact 0 = 1"
- fact_Suc: "fact (Suc n) = (Suc n) * fact n"
+ fact_0: "fact 0 = 1"
+ fact_Suc: "fact (Suc n) = (Suc n) * fact n"
lemma fact_gt_zero [simp]: "0 < fact n"
-by (induct "n", auto)
+ by (induct n) auto
lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
-by simp
+ by simp
lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
-by auto
+ by auto
lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
-by auto
+ by auto
lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
-by simp
+ by simp
lemma fact_ge_one [simp]: "1 \<le> fact n"
-by (induct "n", auto)
+ by (induct n) auto
lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
-apply (drule le_imp_less_or_eq)
-apply (auto dest!: less_imp_Suc_add)
-apply (induct_tac "k", auto)
-done
+ apply (drule le_imp_less_or_eq)
+ apply (auto dest!: less_imp_Suc_add)
+ apply (induct_tac k, auto)
+ done
text{*Note that @{term "fact 0 = fact 1"}*}
lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
-apply (drule_tac m = m in less_imp_Suc_add, auto)
-apply (induct_tac "k", auto)
-done
+ apply (drule_tac m = m in less_imp_Suc_add, auto)
+ apply (induct_tac k, auto)
+ done
lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
-by (auto simp add: positive_imp_inverse_positive)
+ by (auto simp add: positive_imp_inverse_positive)
lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
-by (auto intro: order_less_imp_le)
+ by (auto intro: order_less_imp_le)
lemma fact_diff_Suc [rule_format]:
- "\<forall>m. n < Suc m --> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
-apply (induct n, auto)
-apply (drule_tac x = "m - 1" in spec, auto)
-done
+ "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
+ apply (induct n fixing: m)
+ apply auto
+ apply (drule_tac x = "m - 1" in meta_spec, auto)
+ done
lemma fact_num0 [simp]: "fact 0 = 1"
-by auto
+ by auto
lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
-by (case_tac "m", auto)
+ by (cases m) auto
lemma fact_add_num_eq_if:
- "fact (m+n) = (if (m+n = 0) then 1 else (m+n) * (fact (m + n - 1)))"
-by (case_tac "m+n", auto)
+ "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
+ by (cases "m + n") auto
lemma fact_add_num_eq_if2:
- "fact (m+n) = (if m=0 then fact n else (m+n) * (fact ((m - 1) + n)))"
-by (case_tac "m", auto)
-
+ "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
+ by (cases m) auto
end
--- a/src/HOL/Hyperreal/HLog.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HLog.thy Fri Jun 02 23:22:29 2006 +0200
@@ -18,13 +18,12 @@
by auto
-constdefs
-
- powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80)
- "x powhr a == starfun2 (op powr) x a"
+definition
+ powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80)
+ "x powhr a = starfun2 (op powr) x a"
- hlog :: "[hypreal,hypreal] => hypreal"
- "hlog a x == starfun2 log a x"
+ hlog :: "[hypreal,hypreal] => hypreal"
+ "hlog a x = starfun2 log a x"
declare powhr_def [transfer_unfold]
declare hlog_def [transfer_unfold]
@@ -156,41 +155,4 @@
"[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
by (simp add: linorder_not_less [symmetric])
-
-ML
-{*
-val powhr = thm "powhr";
-val powhr_one_eq_one = thm "powhr_one_eq_one";
-val powhr_mult = thm "powhr_mult";
-val powhr_gt_zero = thm "powhr_gt_zero";
-val powhr_not_zero = thm "powhr_not_zero";
-val powhr_divide = thm "powhr_divide";
-val powhr_add = thm "powhr_add";
-val powhr_powhr = thm "powhr_powhr";
-val powhr_powhr_swap = thm "powhr_powhr_swap";
-val powhr_minus = thm "powhr_minus";
-val powhr_minus_divide = thm "powhr_minus_divide";
-val powhr_less_mono = thm "powhr_less_mono";
-val powhr_less_cancel = thm "powhr_less_cancel";
-val powhr_less_cancel_iff = thm "powhr_less_cancel_iff";
-val powhr_le_cancel_iff = thm "powhr_le_cancel_iff";
-val hlog = thm "hlog";
-val hlog_starfun_ln = thm "hlog_starfun_ln";
-val powhr_hlog_cancel = thm "powhr_hlog_cancel";
-val hlog_powhr_cancel = thm "hlog_powhr_cancel";
-val hlog_mult = thm "hlog_mult";
-val hlog_as_starfun = thm "hlog_as_starfun";
-val hlog_eq_div_starfun_ln_mult_hlog = thm "hlog_eq_div_starfun_ln_mult_hlog";
-val powhr_as_starfun = thm "powhr_as_starfun";
-val HInfinite_powhr = thm "HInfinite_powhr";
-val hlog_hrabs_HInfinite_Infinitesimal = thm "hlog_hrabs_HInfinite_Infinitesimal";
-val hlog_HInfinite_as_starfun = thm "hlog_HInfinite_as_starfun";
-val hlog_one = thm "hlog_one";
-val hlog_eq_one = thm "hlog_eq_one";
-val hlog_inverse = thm "hlog_inverse";
-val hlog_divide = thm "hlog_divide";
-val hlog_less_cancel_iff = thm "hlog_less_cancel_iff";
-val hlog_le_cancel_iff = thm "hlog_le_cancel_iff";
-*}
-
end
--- a/src/HOL/Hyperreal/HSeries.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy Fri Jun 02 23:22:29 2006 +0200
@@ -11,19 +11,19 @@
imports Series
begin
-constdefs
+definition
sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
- "sumhr ==
- %(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N"
+ "sumhr =
+ (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80)
- "f NSsums s == (%n. setsum f {0..<n}) ----NS> s"
+ "f NSsums s = (%n. setsum f {0..<n}) ----NS> s"
NSsummable :: "(nat=>real) => bool"
- "NSsummable f == (\<exists>s. f NSsums s)"
+ "NSsummable f = (\<exists>s. f NSsums s)"
NSsuminf :: "(nat=>real) => real"
- "NSsuminf f == (@s. f NSsums s)"
+ "NSsuminf f = (SOME s. f NSsums s)"
lemma sumhr:
@@ -230,42 +230,4 @@
apply (auto)
done
-ML
-{*
-val sumhr = thm "sumhr";
-val sumhr_zero = thm "sumhr_zero";
-val sumhr_if = thm "sumhr_if";
-val sumhr_Suc_zero = thm "sumhr_Suc_zero";
-val sumhr_eq_bounds = thm "sumhr_eq_bounds";
-val sumhr_Suc = thm "sumhr_Suc";
-val sumhr_add_lbound_zero = thm "sumhr_add_lbound_zero";
-val sumhr_add = thm "sumhr_add";
-val sumhr_mult = thm "sumhr_mult";
-val sumhr_split_add = thm "sumhr_split_add";
-val sumhr_split_diff = thm "sumhr_split_diff";
-val sumhr_hrabs = thm "sumhr_hrabs";
-val sumhr_fun_hypnat_eq = thm "sumhr_fun_hypnat_eq";
-val sumhr_less_bounds_zero = thm "sumhr_less_bounds_zero";
-val sumhr_minus = thm "sumhr_minus";
-val sumhr_shift_bounds = thm "sumhr_shift_bounds";
-val sumhr_hypreal_of_hypnat_omega = thm "sumhr_hypreal_of_hypnat_omega";
-val sumhr_hypreal_omega_minus_one = thm "sumhr_hypreal_omega_minus_one";
-val sumhr_minus_one_realpow_zero = thm "sumhr_minus_one_realpow_zero";
-val sumhr_interval_const = thm "sumhr_interval_const";
-val starfunNat_sumr = thm "starfunNat_sumr";
-val sumhr_hrabs_approx = thm "sumhr_hrabs_approx";
-val sums_NSsums_iff = thm "sums_NSsums_iff";
-val summable_NSsummable_iff = thm "summable_NSsummable_iff";
-val suminf_NSsuminf_iff = thm "suminf_NSsuminf_iff";
-val NSsums_NSsummable = thm "NSsums_NSsummable";
-val NSsummable_NSsums = thm "NSsummable_NSsums";
-val NSsums_unique = thm "NSsums_unique";
-val NSseries_zero = thm "NSseries_zero";
-val NSsummable_NSCauchy = thm "NSsummable_NSCauchy";
-val NSsummable_NSLIMSEQ_zero = thm "NSsummable_NSLIMSEQ_zero";
-val summable_LIMSEQ_zero = thm "summable_LIMSEQ_zero";
-val NSsummable_comparison_test = thm "NSsummable_comparison_test";
-val NSsummable_rabs_comparison_test = thm "NSsummable_rabs_comparison_test";
-*}
-
end
--- a/src/HOL/Hyperreal/HTranscendental.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Fri Jun 02 23:22:29 2006 +0200
@@ -30,18 +30,17 @@
qed
-constdefs
-
+definition
exphr :: "real => hypreal"
--{*define exponential function using standard part *}
- "exphr x == st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
+ "exphr x = st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
sinhr :: "real => hypreal"
- "sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
+ "sinhr x = st(sumhr (0, whn, %n. (if even(n) then 0 else
((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
coshr :: "real => hypreal"
- "coshr x == st(sumhr (0, whn, %n. (if even(n) then
+ "coshr x = st(sumhr (0, whn, %n. (if even(n) then
((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
@@ -616,98 +615,4 @@
simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
done
-ML
-{*
-val STAR_sqrt_zero = thm "STAR_sqrt_zero";
-val STAR_sqrt_one = thm "STAR_sqrt_one";
-val hypreal_sqrt_pow2_iff = thm "hypreal_sqrt_pow2_iff";
-val hypreal_sqrt_gt_zero_pow2 = thm "hypreal_sqrt_gt_zero_pow2";
-val hypreal_sqrt_pow2_gt_zero = thm "hypreal_sqrt_pow2_gt_zero";
-val hypreal_sqrt_not_zero = thm "hypreal_sqrt_not_zero";
-val hypreal_inverse_sqrt_pow2 = thm "hypreal_inverse_sqrt_pow2";
-val hypreal_sqrt_mult_distrib = thm "hypreal_sqrt_mult_distrib";
-val hypreal_sqrt_mult_distrib2 = thm "hypreal_sqrt_mult_distrib2";
-val hypreal_sqrt_approx_zero = thm "hypreal_sqrt_approx_zero";
-val hypreal_sqrt_approx_zero2 = thm "hypreal_sqrt_approx_zero2";
-val hypreal_sqrt_sum_squares = thm "hypreal_sqrt_sum_squares";
-val hypreal_sqrt_sum_squares2 = thm "hypreal_sqrt_sum_squares2";
-val hypreal_sqrt_gt_zero = thm "hypreal_sqrt_gt_zero";
-val hypreal_sqrt_ge_zero = thm "hypreal_sqrt_ge_zero";
-val hypreal_sqrt_hrabs = thm "hypreal_sqrt_hrabs";
-val hypreal_sqrt_hrabs2 = thm "hypreal_sqrt_hrabs2";
-val hypreal_sqrt_hyperpow_hrabs = thm "hypreal_sqrt_hyperpow_hrabs";
-val star_sqrt_HFinite = thm "star_sqrt_HFinite";
-val st_hypreal_sqrt = thm "st_hypreal_sqrt";
-val hypreal_sqrt_sum_squares_ge1 = thm "hypreal_sqrt_sum_squares_ge1";
-val HFinite_hypreal_sqrt = thm "HFinite_hypreal_sqrt";
-val HFinite_hypreal_sqrt_imp_HFinite = thm "HFinite_hypreal_sqrt_imp_HFinite";
-val HFinite_hypreal_sqrt_iff = thm "HFinite_hypreal_sqrt_iff";
-val HFinite_sqrt_sum_squares = thm "HFinite_sqrt_sum_squares";
-val Infinitesimal_hypreal_sqrt = thm "Infinitesimal_hypreal_sqrt";
-val Infinitesimal_hypreal_sqrt_imp_Infinitesimal = thm "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
-val Infinitesimal_hypreal_sqrt_iff = thm "Infinitesimal_hypreal_sqrt_iff";
-val Infinitesimal_sqrt_sum_squares = thm "Infinitesimal_sqrt_sum_squares";
-val HInfinite_hypreal_sqrt = thm "HInfinite_hypreal_sqrt";
-val HInfinite_hypreal_sqrt_imp_HInfinite = thm "HInfinite_hypreal_sqrt_imp_HInfinite";
-val HInfinite_hypreal_sqrt_iff = thm "HInfinite_hypreal_sqrt_iff";
-val HInfinite_sqrt_sum_squares = thm "HInfinite_sqrt_sum_squares";
-val HFinite_exp = thm "HFinite_exp";
-val exphr_zero = thm "exphr_zero";
-val coshr_zero = thm "coshr_zero";
-val STAR_exp_zero_approx_one = thm "STAR_exp_zero_approx_one";
-val STAR_exp_Infinitesimal = thm "STAR_exp_Infinitesimal";
-val STAR_exp_epsilon = thm "STAR_exp_epsilon";
-val STAR_exp_add = thm "STAR_exp_add";
-val exphr_hypreal_of_real_exp_eq = thm "exphr_hypreal_of_real_exp_eq";
-val starfun_exp_ge_add_one_self = thm "starfun_exp_ge_add_one_self";
-val starfun_exp_HInfinite = thm "starfun_exp_HInfinite";
-val starfun_exp_minus = thm "starfun_exp_minus";
-val starfun_exp_Infinitesimal = thm "starfun_exp_Infinitesimal";
-val starfun_exp_gt_one = thm "starfun_exp_gt_one";
-val starfun_ln_exp = thm "starfun_ln_exp";
-val starfun_exp_ln_iff = thm "starfun_exp_ln_iff";
-val starfun_exp_ln_eq = thm "starfun_exp_ln_eq";
-val starfun_ln_less_self = thm "starfun_ln_less_self";
-val starfun_ln_ge_zero = thm "starfun_ln_ge_zero";
-val starfun_ln_gt_zero = thm "starfun_ln_gt_zero";
-val starfun_ln_not_eq_zero = thm "starfun_ln_not_eq_zero";
-val starfun_ln_HFinite = thm "starfun_ln_HFinite";
-val starfun_ln_inverse = thm "starfun_ln_inverse";
-val starfun_exp_HFinite = thm "starfun_exp_HFinite";
-val starfun_exp_add_HFinite_Infinitesimal_approx = thm "starfun_exp_add_HFinite_Infinitesimal_approx";
-val starfun_ln_HInfinite = thm "starfun_ln_HInfinite";
-val starfun_exp_HInfinite_Infinitesimal_disj = thm "starfun_exp_HInfinite_Infinitesimal_disj";
-val starfun_ln_HFinite_not_Infinitesimal = thm "starfun_ln_HFinite_not_Infinitesimal";
-val starfun_ln_Infinitesimal_HInfinite = thm "starfun_ln_Infinitesimal_HInfinite";
-val starfun_ln_less_zero = thm "starfun_ln_less_zero";
-val starfun_ln_Infinitesimal_less_zero = thm "starfun_ln_Infinitesimal_less_zero";
-val starfun_ln_HInfinite_gt_zero = thm "starfun_ln_HInfinite_gt_zero";
-val HFinite_sin = thm "HFinite_sin";
-val STAR_sin_zero = thm "STAR_sin_zero";
-val STAR_sin_Infinitesimal = thm "STAR_sin_Infinitesimal";
-val HFinite_cos = thm "HFinite_cos";
-val STAR_cos_zero = thm "STAR_cos_zero";
-val STAR_cos_Infinitesimal = thm "STAR_cos_Infinitesimal";
-val STAR_tan_zero = thm "STAR_tan_zero";
-val STAR_tan_Infinitesimal = thm "STAR_tan_Infinitesimal";
-val STAR_sin_cos_Infinitesimal_mult = thm "STAR_sin_cos_Infinitesimal_mult";
-val HFinite_pi = thm "HFinite_pi";
-val lemma_split_hypreal_of_real = thm "lemma_split_hypreal_of_real";
-val STAR_sin_Infinitesimal_divide = thm "STAR_sin_Infinitesimal_divide";
-val lemma_sin_pi = thm "lemma_sin_pi";
-val STAR_sin_inverse_HNatInfinite = thm "STAR_sin_inverse_HNatInfinite";
-val Infinitesimal_pi_divide_HNatInfinite = thm "Infinitesimal_pi_divide_HNatInfinite";
-val pi_divide_HNatInfinite_not_zero = thm "pi_divide_HNatInfinite_not_zero";
-val STAR_sin_pi_divide_HNatInfinite_approx_pi = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi";
-val STAR_sin_pi_divide_HNatInfinite_approx_pi2 = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
-val starfunNat_pi_divide_n_Infinitesimal = thm "starfunNat_pi_divide_n_Infinitesimal";
-val STAR_sin_pi_divide_n_approx = thm "STAR_sin_pi_divide_n_approx";
-val NSLIMSEQ_sin_pi = thm "NSLIMSEQ_sin_pi";
-val NSLIMSEQ_cos_one = thm "NSLIMSEQ_cos_one";
-val NSLIMSEQ_sin_cos_pi = thm "NSLIMSEQ_sin_cos_pi";
-val STAR_cos_Infinitesimal_approx = thm "STAR_cos_Infinitesimal_approx";
-val STAR_cos_Infinitesimal_approx2 = thm "STAR_cos_Infinitesimal_approx2";
-*}
-
-
end
--- a/src/HOL/Hyperreal/HyperArith.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy Fri Jun 02 23:22:29 2006 +0200
@@ -23,14 +23,12 @@
"[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
by (simp add: abs_if split: split_if_asm)
-text{*used once in NSA*}
lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
by (blast intro!: order_le_less_trans abs_ge_zero)
lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x"
by (simp add: abs_if)
-(* Needed in Geom.ML *)
lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
by (simp add: abs_if split add: split_if_asm)
@@ -41,9 +39,9 @@
subsection{*Embedding the Naturals into the Hyperreals*}
-constdefs
+definition
hypreal_of_nat :: "nat => hypreal"
- "hypreal_of_nat m == of_nat m"
+ "hypreal_of_nat m = of_nat m"
lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
by (force simp add: hypreal_of_nat_def Nats_def)
@@ -111,24 +109,4 @@
Addsimps [symmetric hypreal_diff_def]
*)
-ML
-{*
-val hypreal_of_nat_def = thm"hypreal_of_nat_def";
-
-val hrabs_add_less = thm "hrabs_add_less";
-val hrabs_disj = thm "hrabs_disj";
-val hrabs_add_lemma_disj = thm "hrabs_add_lemma_disj";
-val hypreal_of_real_hrabs = thm "hypreal_of_real_hrabs";
-val hypreal_of_nat_add = thm "hypreal_of_nat_add";
-val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
-val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
-val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
-val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
-val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";
-val hypreal_of_nat_one = thm "hypreal_of_nat_one";
-val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
-val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
-val hypreal_of_nat = thm"hypreal_of_nat";
-*}
-
end
--- a/src/HOL/Hyperreal/HyperDef.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Fri Jun 02 23:22:29 2006 +0200
@@ -18,21 +18,20 @@
hypreal_of_real :: "real => real star"
"hypreal_of_real == star_of"
-constdefs
-
+definition
omega :: hypreal -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
- "omega == star_n (%n. real (Suc n))"
+ "omega = star_n (%n. real (Suc n))"
epsilon :: hypreal -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
- "epsilon == star_n (%n. inverse (real (Suc n)))"
+ "epsilon = star_n (%n. inverse (real (Suc n)))"
-syntax (xsymbols)
- omega :: hypreal ("\<omega>")
- epsilon :: hypreal ("\<epsilon>")
+const_syntax (xsymbols)
+ omega ("\<omega>")
+ epsilon ("\<epsilon>")
-syntax (HTML output)
- omega :: hypreal ("\<omega>")
- epsilon :: hypreal ("\<epsilon>")
+const_syntax (HTML output)
+ omega ("\<omega>")
+ epsilon ("\<epsilon>")
subsection{*Existence of Free Ultrafilter over the Naturals*}
@@ -302,60 +301,4 @@
lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
by (simp add: epsilon_def omega_def star_n_inverse)
-
-ML
-{*
-val omega_def = thm "omega_def";
-val epsilon_def = thm "epsilon_def";
-
-val FreeUltrafilterNat_Ex = thm "FreeUltrafilterNat_Ex";
-val FreeUltrafilterNat_mem = thm "FreeUltrafilterNat_mem";
-val FreeUltrafilterNat_finite = thm "FreeUltrafilterNat_finite";
-val FreeUltrafilterNat_not_finite = thm "FreeUltrafilterNat_not_finite";
-val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty";
-val FreeUltrafilterNat_Int = thm "FreeUltrafilterNat_Int";
-val FreeUltrafilterNat_subset = thm "FreeUltrafilterNat_subset";
-val FreeUltrafilterNat_Compl = thm "FreeUltrafilterNat_Compl";
-val FreeUltrafilterNat_Compl_mem = thm "FreeUltrafilterNat_Compl_mem";
-val FreeUltrafilterNat_Compl_iff1 = thm "FreeUltrafilterNat_Compl_iff1";
-val FreeUltrafilterNat_Compl_iff2 = thm "FreeUltrafilterNat_Compl_iff2";
-val FreeUltrafilterNat_UNIV = thm "FreeUltrafilterNat_UNIV";
-val FreeUltrafilterNat_Nat_set_refl = thm "FreeUltrafilterNat_Nat_set_refl";
-val FreeUltrafilterNat_P = thm "FreeUltrafilterNat_P";
-val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P";
-val FreeUltrafilterNat_all = thm "FreeUltrafilterNat_all";
-val FreeUltrafilterNat_Un = thm "FreeUltrafilterNat_Un";
-val starrel_iff = thm "starrel_iff";
-val starrel_in_hypreal = thm "starrel_in_hypreal";
-val Abs_star_inverse = thm "Abs_star_inverse";
-val lemma_starrel_refl = thm "lemma_starrel_refl";
-val hypreal_empty_not_mem = thm "hypreal_empty_not_mem";
-val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty";
-val inj_hypreal_of_real = thm "inj_hypreal_of_real";
-(* val eq_Abs_star = thm "eq_Abs_star"; *)
-val star_n_minus = thm "star_n_minus";
-val star_n_add = thm "star_n_add";
-val star_n_diff = thm "star_n_diff";
-val star_n_mult = thm "star_n_mult";
-val star_n_inverse = thm "star_n_inverse";
-val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel";
-val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel";
-val hypreal_not_refl2 = thm "hypreal_not_refl2";
-val star_n_less = thm "star_n_less";
-val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff";
-val star_n_le = thm "star_n_le";
-val star_n_zero_num = thm "star_n_zero_num";
-val star_n_one_num = thm "star_n_one_num";
-val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero";
-
-val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
-val lemma_finite_omega_set = thm"lemma_finite_omega_set";
-val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega";
-val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega";
-val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon";
-val hypreal_of_real_not_eq_epsilon = thm"hypreal_of_real_not_eq_epsilon";
-val hypreal_epsilon_not_zero = thm"hypreal_epsilon_not_zero";
-val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega";
-*}
-
end
--- a/src/HOL/Hyperreal/HyperNat.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Fri Jun 02 23:22:29 2006 +0200
@@ -148,11 +148,10 @@
subsection{*Existence of an infinite hypernatural number*}
-consts whn :: hypnat
-
-defs
+definition
(* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
- hypnat_omega_def: "whn == star_n (%n::nat. n)"
+ whn :: hypnat
+ hypnat_omega_def: "whn = star_n (%n::nat. n)"
text{*Existence of infinite number not corresponding to any natural number
follows because member @{term FreeUltrafilterNat} is not finite.
@@ -201,11 +200,10 @@
subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
-constdefs
-
+definition
(* the set of infinite hypernatural numbers *)
HNatInfinite :: "hypnat set"
- "HNatInfinite == {n. n \<notin> Nats}"
+ "HNatInfinite = {n. n \<notin> Nats}"
lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"
by (simp add: HNatInfinite_def)
@@ -327,9 +325,9 @@
subsection{*Embedding of the Hypernaturals into the Hyperreals*}
text{*Obtained using the nonstandard extension of the naturals*}
-constdefs
+definition
hypreal_of_hypnat :: "hypnat => hypreal"
- "hypreal_of_hypnat == *f* real"
+ "hypreal_of_hypnat = *f* real"
declare hypreal_of_hypnat_def [transfer_unfold]
@@ -384,73 +382,4 @@
apply (simp add: hypreal_of_hypnat_zero [symmetric] linorder_not_less)
done
-
-ML
-{*
-val hypnat_of_nat_def = thm"hypnat_of_nat_def";
-val HNatInfinite_def = thm"HNatInfinite_def";
-val hypreal_of_hypnat_def = thm"hypreal_of_hypnat_def";
-val hypnat_omega_def = thm"hypnat_omega_def";
-
-val starrel_iff = thm "starrel_iff";
-val lemma_starrel_refl = thm "lemma_starrel_refl";
-val hypnat_minus_zero = thm "hypnat_minus_zero";
-val hypnat_diff_0_eq_0 = thm "hypnat_diff_0_eq_0";
-val hypnat_add_is_0 = thm "hypnat_add_is_0";
-val hypnat_diff_diff_left = thm "hypnat_diff_diff_left";
-val hypnat_diff_commute = thm "hypnat_diff_commute";
-val hypnat_diff_add_inverse = thm "hypnat_diff_add_inverse";
-val hypnat_diff_add_inverse2 = thm "hypnat_diff_add_inverse2";
-val hypnat_diff_cancel = thm "hypnat_diff_cancel";
-val hypnat_diff_cancel2 = thm "hypnat_diff_cancel2";
-val hypnat_diff_add_0 = thm "hypnat_diff_add_0";
-val hypnat_diff_mult_distrib = thm "hypnat_diff_mult_distrib";
-val hypnat_diff_mult_distrib2 = thm "hypnat_diff_mult_distrib2";
-val hypnat_mult_is_0 = thm "hypnat_mult_is_0";
-val hypnat_not_less0 = thm "hypnat_not_less0";
-val hypnat_less_one = thm "hypnat_less_one";
-val hypnat_add_diff_inverse = thm "hypnat_add_diff_inverse";
-val hypnat_le_add_diff_inverse = thm "hypnat_le_add_diff_inverse";
-val hypnat_le_add_diff_inverse2 = thm "hypnat_le_add_diff_inverse2";
-val hypnat_le0 = thm "hypnat_le0";
-val hypnat_add_self_le = thm "hypnat_add_self_le";
-val hypnat_add_one_self_less = thm "hypnat_add_one_self_less";
-val hypnat_neq0_conv = thm "hypnat_neq0_conv";
-val hypnat_gt_zero_iff = thm "hypnat_gt_zero_iff";
-val hypnat_gt_zero_iff2 = thm "hypnat_gt_zero_iff2";
-val SHNat_eq = thm"SHNat_eq"
-val hypnat_of_nat_one = thm "hypnat_of_nat_one";
-val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
-val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
-val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
-val hypnat_omega_gt_SHNat = thm "hypnat_omega_gt_SHNat";
-val hypnat_of_nat_less_whn = thm "hypnat_of_nat_less_whn";
-val hypnat_of_nat_le_whn = thm "hypnat_of_nat_le_whn";
-val hypnat_zero_less_hypnat_omega = thm "hypnat_zero_less_hypnat_omega";
-val hypnat_one_less_hypnat_omega = thm "hypnat_one_less_hypnat_omega";
-val HNatInfinite_whn = thm "HNatInfinite_whn";
-val HNatInfinite_iff = thm "HNatInfinite_iff";
-val HNatInfinite_FreeUltrafilterNat = thm "HNatInfinite_FreeUltrafilterNat";
-val FreeUltrafilterNat_HNatInfinite = thm "FreeUltrafilterNat_HNatInfinite";
-val HNatInfinite_FreeUltrafilterNat_iff = thm "HNatInfinite_FreeUltrafilterNat_iff";
-val HNatInfinite_gt_one = thm "HNatInfinite_gt_one";
-val zero_not_mem_HNatInfinite = thm "zero_not_mem_HNatInfinite";
-val HNatInfinite_not_eq_zero = thm "HNatInfinite_not_eq_zero";
-val HNatInfinite_ge_one = thm "HNatInfinite_ge_one";
-val HNatInfinite_add = thm "HNatInfinite_add";
-val HNatInfinite_SHNat_add = thm "HNatInfinite_SHNat_add";
-val HNatInfinite_SHNat_diff = thm "HNatInfinite_SHNat_diff";
-val HNatInfinite_add_one = thm "HNatInfinite_add_one";
-val HNatInfinite_is_Suc = thm "HNatInfinite_is_Suc";
-val HNat_hypreal_of_nat = thm "HNat_hypreal_of_nat";
-val hypreal_of_hypnat = thm "hypreal_of_hypnat";
-val hypreal_of_hypnat_zero = thm "hypreal_of_hypnat_zero";
-val hypreal_of_hypnat_one = thm "hypreal_of_hypnat_one";
-val hypreal_of_hypnat_add = thm "hypreal_of_hypnat_add";
-val hypreal_of_hypnat_mult = thm "hypreal_of_hypnat_mult";
-val hypreal_of_hypnat_less_iff = thm "hypreal_of_hypnat_less_iff";
-val hypreal_of_hypnat_ge_zero = thm "hypreal_of_hypnat_ge_zero";
-val HNatInfinite_inverse_Infinitesimal = thm "HNatInfinite_inverse_Infinitesimal";
-*}
-
end
--- a/src/HOL/Hyperreal/HyperPow.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy Fri Jun 02 23:22:29 2006 +0200
@@ -18,14 +18,11 @@
lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
by (rule power_Suc)
-consts
- "pow" :: "[hypreal,hypnat] => hypreal" (infixr "pow" 80)
-
-defs
-
+definition
(* hypernatural powers of hyperreals *)
+ pow :: "[hypreal,hypnat] => hypreal" (infixr "pow" 80)
hyperpow_def [transfer_unfold]:
- "(R::hypreal) pow (N::hypnat) == ( *f2* op ^) R N"
+ "(R::hypreal) pow (N::hypnat) = ( *f2* op ^) R N"
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
by simp
@@ -235,54 +232,4 @@
"[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow)
-ML
-{*
-val hrealpow_two = thm "hrealpow_two";
-val hrealpow_two_le = thm "hrealpow_two_le";
-val hrealpow_two_le_add_order = thm "hrealpow_two_le_add_order";
-val hrealpow_two_le_add_order2 = thm "hrealpow_two_le_add_order2";
-val hypreal_add_nonneg_eq_0_iff = thm "hypreal_add_nonneg_eq_0_iff";
-val hypreal_three_squares_add_zero_iff = thm "hypreal_three_squares_add_zero_iff";
-val hrealpow_three_squares_add_zero_iff = thm "hrealpow_three_squares_add_zero_iff";
-val hrabs_hrealpow_two = thm "hrabs_hrealpow_two";
-val two_hrealpow_ge_one = thm "two_hrealpow_ge_one";
-val two_hrealpow_gt = thm "two_hrealpow_gt";
-val hrealpow = thm "hrealpow";
-val hrealpow_sum_square_expand = thm "hrealpow_sum_square_expand";
-val power_hypreal_of_real_number_of = thm "power_hypreal_of_real_number_of";
-val hrealpow_HFinite = thm "hrealpow_HFinite";
-val hyperpow = thm "hyperpow";
-val hyperpow_zero = thm "hyperpow_zero";
-val hyperpow_not_zero = thm "hyperpow_not_zero";
-val hyperpow_inverse = thm "hyperpow_inverse";
-val hyperpow_hrabs = thm "hyperpow_hrabs";
-val hyperpow_add = thm "hyperpow_add";
-val hyperpow_one = thm "hyperpow_one";
-val hyperpow_two = thm "hyperpow_two";
-val hyperpow_gt_zero = thm "hyperpow_gt_zero";
-val hyperpow_ge_zero = thm "hyperpow_ge_zero";
-val hyperpow_le = thm "hyperpow_le";
-val hyperpow_eq_one = thm "hyperpow_eq_one";
-val hrabs_hyperpow_minus_one = thm "hrabs_hyperpow_minus_one";
-val hyperpow_mult = thm "hyperpow_mult";
-val hyperpow_two_le = thm "hyperpow_two_le";
-val hrabs_hyperpow_two = thm "hrabs_hyperpow_two";
-val hyperpow_two_hrabs = thm "hyperpow_two_hrabs";
-val hyperpow_two_gt_one = thm "hyperpow_two_gt_one";
-val hyperpow_two_ge_one = thm "hyperpow_two_ge_one";
-val two_hyperpow_ge_one = thm "two_hyperpow_ge_one";
-val hyperpow_minus_one2 = thm "hyperpow_minus_one2";
-val hyperpow_less_le = thm "hyperpow_less_le";
-val hyperpow_SHNat_le = thm "hyperpow_SHNat_le";
-val hyperpow_realpow = thm "hyperpow_realpow";
-val hyperpow_SReal = thm "hyperpow_SReal";
-val hyperpow_zero_HNatInfinite = thm "hyperpow_zero_HNatInfinite";
-val hyperpow_le_le = thm "hyperpow_le_le";
-val hyperpow_Suc_le_self2 = thm "hyperpow_Suc_le_self2";
-val lemma_Infinitesimal_hyperpow = thm "lemma_Infinitesimal_hyperpow";
-val Infinitesimal_hyperpow = thm "Infinitesimal_hyperpow";
-val hrealpow_hyperpow_Infinitesimal_iff = thm "hrealpow_hyperpow_Infinitesimal_iff";
-val Infinitesimal_hrealpow = thm "Infinitesimal_hrealpow";
-*}
-
end
--- a/src/HOL/Hyperreal/Integration.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Fri Jun 02 23:22:29 2006 +0200
@@ -12,43 +12,43 @@
text{*We follow John Harrison in formalizing the Gauge integral.*}
-constdefs
+definition
--{*Partitions and tagged partitions etc.*}
partition :: "[(real*real),nat => real] => bool"
- "partition == %(a,b) D. D 0 = a &
+ "partition = (%(a,b) D. D 0 = a &
(\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
- (\<forall>n \<ge> N. D(n) = b))"
+ (\<forall>n \<ge> N. D(n) = b)))"
psize :: "(nat => real) => nat"
- "psize D == SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
- (\<forall>n \<ge> N. D(n) = D(N))"
+ "psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
+ (\<forall>n \<ge> N. D(n) = D(N)))"
tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
- "tpart == %(a,b) (D,p). partition(a,b) D &
- (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n))"
+ "tpart = (%(a,b) (D,p). partition(a,b) D &
+ (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
--{*Gauges and gauge-fine divisions*}
gauge :: "[real => bool, real => real] => bool"
- "gauge E g == \<forall>x. E x --> 0 < g(x)"
+ "gauge E g = (\<forall>x. E x --> 0 < g(x))"
fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
- "fine == % g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
+ "fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
--{*Riemann sum*}
rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
- "rsum == %(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n))"
+ "rsum = (%(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n)))"
--{*Gauge integrability (definite)*}
- Integral :: "[(real*real),real=>real,real] => bool"
- "Integral == %(a,b) f k. \<forall>e > 0.
+ Integral :: "[(real*real),real=>real,real] => bool"
+ "Integral = (%(a,b) f k. \<forall>e > 0.
(\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
(\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
- \<bar>rsum(D,p) f - k\<bar> < e))"
+ \<bar>rsum(D,p) f - k\<bar> < e)))"
lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0"
--- a/src/HOL/Hyperreal/Lim.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Fri Jun 02 23:22:29 2006 +0200
@@ -14,61 +14,58 @@
text{*Standard and Nonstandard Definitions*}
-constdefs
+definition
LIM :: "[real=>real,real,real] => bool"
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
- "f -- a --> L ==
- \<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
- --> \<bar>f x + -L\<bar> < r"
+ "f -- a --> L =
+ (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
+ --> \<bar>f x + -L\<bar> < r)"
NSLIM :: "[real=>real,real,real] => bool"
("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
- "f -- a --NS> L == (\<forall>x. (x \<noteq> hypreal_of_real a &
+ "f -- a --NS> L = (\<forall>x. (x \<noteq> hypreal_of_real a &
x @= hypreal_of_real a -->
( *f* f) x @= hypreal_of_real L))"
isCont :: "[real=>real,real] => bool"
- "isCont f a == (f -- a --> (f a))"
+ "isCont f a = (f -- a --> (f a))"
isNSCont :: "[real=>real,real] => bool"
--{*NS definition dispenses with limit notions*}
- "isNSCont f a == (\<forall>y. y @= hypreal_of_real a -->
+ "isNSCont f a = (\<forall>y. y @= hypreal_of_real a -->
( *f* f) y @= hypreal_of_real (f a))"
deriv:: "[real=>real,real,real] => bool"
--{*Differentiation: D is derivative of function f at x*}
("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
- "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
+ "DERIV f x :> D = ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
nsderiv :: "[real=>real,real,real] => bool"
("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
- "NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}.
+ "NSDERIV f x :> D = (\<forall>h \<in> Infinitesimal - {0}.
(( *f* f)(hypreal_of_real x + h) +
- hypreal_of_real (f x))/h @= hypreal_of_real D)"
differentiable :: "[real=>real,real] => bool" (infixl "differentiable" 60)
- "f differentiable x == (\<exists>D. DERIV f x :> D)"
+ "f differentiable x = (\<exists>D. DERIV f x :> D)"
NSdifferentiable :: "[real=>real,real] => bool"
(infixl "NSdifferentiable" 60)
- "f NSdifferentiable x == (\<exists>D. NSDERIV f x :> D)"
+ "f NSdifferentiable x = (\<exists>D. NSDERIV f x :> D)"
increment :: "[real=>real,real,hypreal] => hypreal"
- "increment f x h == (@inc. f NSdifferentiable x &
+ "increment f x h = (@inc. f NSdifferentiable x &
inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
isUCont :: "(real=>real) => bool"
- "isUCont f == \<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r"
+ "isUCont f = (\<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r)"
isNSUCont :: "(real=>real) => bool"
- "isNSUCont f == (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+ "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
consts
Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
- --{*Used in the proof of the Bolzano theorem*}
-
-
primrec
"Bolzano_bisect P a b 0 = (a,b)"
"Bolzano_bisect P a b (Suc n) =
@@ -2372,202 +2369,4 @@
thus ?thesis by (fold LIM_def)
qed
-
-
-ML
-{*
-val LIM_def = thm"LIM_def";
-val NSLIM_def = thm"NSLIM_def";
-val isCont_def = thm"isCont_def";
-val isNSCont_def = thm"isNSCont_def";
-val deriv_def = thm"deriv_def";
-val nsderiv_def = thm"nsderiv_def";
-val differentiable_def = thm"differentiable_def";
-val NSdifferentiable_def = thm"NSdifferentiable_def";
-val increment_def = thm"increment_def";
-val isUCont_def = thm"isUCont_def";
-val isNSUCont_def = thm"isNSUCont_def";
-
-val half_gt_zero_iff = thm "half_gt_zero_iff";
-val half_gt_zero = thms "half_gt_zero";
-val abs_diff_triangle_ineq = thm "abs_diff_triangle_ineq";
-val LIM_eq = thm "LIM_eq";
-val LIM_D = thm "LIM_D";
-val LIM_const = thm "LIM_const";
-val LIM_add = thm "LIM_add";
-val LIM_minus = thm "LIM_minus";
-val LIM_add_minus = thm "LIM_add_minus";
-val LIM_diff = thm "LIM_diff";
-val LIM_const_not_eq = thm "LIM_const_not_eq";
-val LIM_const_eq = thm "LIM_const_eq";
-val LIM_unique = thm "LIM_unique";
-val LIM_mult_zero = thm "LIM_mult_zero";
-val LIM_self = thm "LIM_self";
-val LIM_equal = thm "LIM_equal";
-val LIM_trans = thm "LIM_trans";
-val LIM_NSLIM = thm "LIM_NSLIM";
-val NSLIM_LIM = thm "NSLIM_LIM";
-val LIM_NSLIM_iff = thm "LIM_NSLIM_iff";
-val NSLIM_mult = thm "NSLIM_mult";
-val LIM_mult2 = thm "LIM_mult2";
-val NSLIM_add = thm "NSLIM_add";
-val LIM_add2 = thm "LIM_add2";
-val NSLIM_const = thm "NSLIM_const";
-val LIM_const2 = thm "LIM_const2";
-val NSLIM_minus = thm "NSLIM_minus";
-val LIM_minus2 = thm "LIM_minus2";
-val NSLIM_add_minus = thm "NSLIM_add_minus";
-val LIM_add_minus2 = thm "LIM_add_minus2";
-val NSLIM_inverse = thm "NSLIM_inverse";
-val LIM_inverse = thm "LIM_inverse";
-val NSLIM_zero = thm "NSLIM_zero";
-val LIM_zero2 = thm "LIM_zero2";
-val NSLIM_zero_cancel = thm "NSLIM_zero_cancel";
-val LIM_zero_cancel = thm "LIM_zero_cancel";
-val NSLIM_not_zero = thm "NSLIM_not_zero";
-val NSLIM_const_not_eq = thm "NSLIM_const_not_eq";
-val NSLIM_const_eq = thm "NSLIM_const_eq";
-val NSLIM_unique = thm "NSLIM_unique";
-val LIM_unique2 = thm "LIM_unique2";
-val NSLIM_mult_zero = thm "NSLIM_mult_zero";
-val LIM_mult_zero2 = thm "LIM_mult_zero2";
-val NSLIM_self = thm "NSLIM_self";
-val isNSContD = thm "isNSContD";
-val isNSCont_NSLIM = thm "isNSCont_NSLIM";
-val NSLIM_isNSCont = thm "NSLIM_isNSCont";
-val isNSCont_NSLIM_iff = thm "isNSCont_NSLIM_iff";
-val isNSCont_LIM_iff = thm "isNSCont_LIM_iff";
-val isNSCont_isCont_iff = thm "isNSCont_isCont_iff";
-val isCont_isNSCont = thm "isCont_isNSCont";
-val isNSCont_isCont = thm "isNSCont_isCont";
-val NSLIM_h_iff = thm "NSLIM_h_iff";
-val NSLIM_isCont_iff = thm "NSLIM_isCont_iff";
-val LIM_isCont_iff = thm "LIM_isCont_iff";
-val isCont_iff = thm "isCont_iff";
-val isCont_add = thm "isCont_add";
-val isCont_mult = thm "isCont_mult";
-val isCont_o = thm "isCont_o";
-val isCont_o2 = thm "isCont_o2";
-val isNSCont_minus = thm "isNSCont_minus";
-val isCont_minus = thm "isCont_minus";
-val isCont_inverse = thm "isCont_inverse";
-val isNSCont_inverse = thm "isNSCont_inverse";
-val isCont_diff = thm "isCont_diff";
-val isCont_const = thm "isCont_const";
-val isNSCont_const = thm "isNSCont_const";
-val isNSUContD = thm "isNSUContD";
-val isUCont_isCont = thm "isUCont_isCont";
-val isUCont_isNSUCont = thm "isUCont_isNSUCont";
-val isNSUCont_isUCont = thm "isNSUCont_isUCont";
-val DERIV_iff = thm "DERIV_iff";
-val DERIV_NS_iff = thm "DERIV_NS_iff";
-val DERIV_D = thm "DERIV_D";
-val NS_DERIV_D = thm "NS_DERIV_D";
-val DERIV_unique = thm "DERIV_unique";
-val NSDeriv_unique = thm "NSDeriv_unique";
-val differentiableD = thm "differentiableD";
-val differentiableI = thm "differentiableI";
-val NSdifferentiableD = thm "NSdifferentiableD";
-val NSdifferentiableI = thm "NSdifferentiableI";
-val LIM_I = thm "LIM_I";
-val DERIV_LIM_iff = thm "DERIV_LIM_iff";
-val DERIV_iff2 = thm "DERIV_iff2";
-val NSDERIV_NSLIM_iff = thm "NSDERIV_NSLIM_iff";
-val NSDERIV_NSLIM_iff2 = thm "NSDERIV_NSLIM_iff2";
-val NSDERIV_iff2 = thm "NSDERIV_iff2";
-val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff";
-val NSDERIVD5 = thm "NSDERIVD5";
-val NSDERIVD4 = thm "NSDERIVD4";
-val NSDERIVD3 = thm "NSDERIVD3";
-val NSDERIV_DERIV_iff = thm "NSDERIV_DERIV_iff";
-val NSDERIV_isNSCont = thm "NSDERIV_isNSCont";
-val DERIV_isCont = thm "DERIV_isCont";
-val NSDERIV_const = thm "NSDERIV_const";
-val DERIV_const = thm "DERIV_const";
-val NSDERIV_add = thm "NSDERIV_add";
-val DERIV_add = thm "DERIV_add";
-val NSDERIV_mult = thm "NSDERIV_mult";
-val DERIV_mult = thm "DERIV_mult";
-val NSDERIV_cmult = thm "NSDERIV_cmult";
-val DERIV_cmult = thm "DERIV_cmult";
-val NSDERIV_minus = thm "NSDERIV_minus";
-val DERIV_minus = thm "DERIV_minus";
-val NSDERIV_add_minus = thm "NSDERIV_add_minus";
-val DERIV_add_minus = thm "DERIV_add_minus";
-val NSDERIV_diff = thm "NSDERIV_diff";
-val DERIV_diff = thm "DERIV_diff";
-val incrementI = thm "incrementI";
-val incrementI2 = thm "incrementI2";
-val increment_thm = thm "increment_thm";
-val increment_thm2 = thm "increment_thm2";
-val increment_approx_zero = thm "increment_approx_zero";
-val NSDERIV_zero = thm "NSDERIV_zero";
-val NSDERIV_approx = thm "NSDERIV_approx";
-val NSDERIVD1 = thm "NSDERIVD1";
-val NSDERIVD2 = thm "NSDERIVD2";
-val NSDERIV_chain = thm "NSDERIV_chain";
-val DERIV_chain = thm "DERIV_chain";
-val DERIV_chain2 = thm "DERIV_chain2";
-val NSDERIV_Id = thm "NSDERIV_Id";
-val DERIV_Id = thm "DERIV_Id";
-val isCont_Id = thms "isCont_Id";
-val DERIV_cmult_Id = thm "DERIV_cmult_Id";
-val NSDERIV_cmult_Id = thm "NSDERIV_cmult_Id";
-val DERIV_pow = thm "DERIV_pow";
-val NSDERIV_pow = thm "NSDERIV_pow";
-val NSDERIV_inverse = thm "NSDERIV_inverse";
-val DERIV_inverse = thm "DERIV_inverse";
-val DERIV_inverse_fun = thm "DERIV_inverse_fun";
-val NSDERIV_inverse_fun = thm "NSDERIV_inverse_fun";
-val DERIV_quotient = thm "DERIV_quotient";
-val NSDERIV_quotient = thm "NSDERIV_quotient";
-val CARAT_DERIV = thm "CARAT_DERIV";
-val CARAT_NSDERIV = thm "CARAT_NSDERIV";
-val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3";
-val starfun_if_eq = thm "starfun_if_eq";
-val CARAT_DERIVD = thm "CARAT_DERIVD";
-val f_inc_g_dec_Beq_f = thm "f_inc_g_dec_Beq_f";
-val f_inc_g_dec_Beq_g = thm "f_inc_g_dec_Beq_g";
-val f_inc_imp_le_lim = thm "f_inc_imp_le_lim";
-val lim_uminus = thm "lim_uminus";
-val g_dec_imp_lim_le = thm "g_dec_imp_lim_le";
-val Bolzano_bisect_le = thm "Bolzano_bisect_le";
-val Bolzano_bisect_fst_le_Suc = thm "Bolzano_bisect_fst_le_Suc";
-val Bolzano_bisect_Suc_le_snd = thm "Bolzano_bisect_Suc_le_snd";
-val eq_divide_2_times_iff = thm "eq_divide_2_times_iff";
-val Bolzano_bisect_diff = thm "Bolzano_bisect_diff";
-val Bolzano_nest_unique = thms "Bolzano_nest_unique";
-val not_P_Bolzano_bisect = thm "not_P_Bolzano_bisect";
-val not_P_Bolzano_bisect = thm "not_P_Bolzano_bisect";
-val lemma_BOLZANO2 = thm "lemma_BOLZANO2";
-val IVT = thm "IVT";
-val IVT2 = thm "IVT2";
-val IVT_objl = thm "IVT_objl";
-val IVT2_objl = thm "IVT2_objl";
-val isCont_bounded = thm "isCont_bounded";
-val isCont_has_Ub = thm "isCont_has_Ub";
-val isCont_eq_Ub = thm "isCont_eq_Ub";
-val isCont_eq_Lb = thm "isCont_eq_Lb";
-val isCont_Lb_Ub = thm "isCont_Lb_Ub";
-val DERIV_left_inc = thm "DERIV_left_inc";
-val DERIV_left_dec = thm "DERIV_left_dec";
-val DERIV_local_max = thm "DERIV_local_max";
-val DERIV_local_min = thm "DERIV_local_min";
-val DERIV_local_const = thm "DERIV_local_const";
-val Rolle = thm "Rolle";
-val MVT = thm "MVT";
-val DERIV_isconst_end = thm "DERIV_isconst_end";
-val DERIV_isconst1 = thm "DERIV_isconst1";
-val DERIV_isconst2 = thm "DERIV_isconst2";
-val DERIV_isconst_all = thm "DERIV_isconst_all";
-val DERIV_const_ratio_const = thm "DERIV_const_ratio_const";
-val DERIV_const_ratio_const2 = thm "DERIV_const_ratio_const2";
-val real_average_minus_first = thm "real_average_minus_first";
-val real_average_minus_second = thm "real_average_minus_second";
-val DERIV_const_average = thm "DERIV_const_average";
-val isCont_inj_range = thm "isCont_inj_range";
-val isCont_inverse_function = thm "isCont_inverse_function";
-*}
-
-
end
--- a/src/HOL/Hyperreal/Ln.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Ln.thy Fri Jun 02 23:22:29 2006 +0200
@@ -6,7 +6,6 @@
header {* Properties of ln *}
theory Ln
-
imports Transcendental
begin
@@ -14,7 +13,7 @@
inverse(real (fact (n+2))) * (x ^ (n+2)))"
proof -
have "exp x = suminf (%n. inverse(real (fact n)) * (x ^ n))"
- by (unfold exp_def, simp)
+ by (simp add: exp_def)
also from summable_exp have "... = (SUM n : {0..<2}.
inverse(real (fact n)) * (x ^ n)) + suminf (%n.
inverse(real (fact (n+2))) * (x ^ (n+2)))" (is "_ = ?a + _")
@@ -477,4 +476,3 @@
qed
end
-
--- a/src/HOL/Hyperreal/Log.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Log.thy Fri Jun 02 23:22:29 2006 +0200
@@ -10,15 +10,14 @@
imports Transcendental
begin
-constdefs
-
+definition
powr :: "[real,real] => real" (infixr "powr" 80)
--{*exponentation with real exponent*}
- "x powr a == exp(a * ln x)"
+ "x powr a = exp(a * ln x)"
log :: "[real,real] => real"
--{*logarithm of @{term x} to base @{term a}*}
- "log a x == ln x / ln a"
+ "log a x = ln x / ln a"
@@ -273,39 +272,4 @@
finally show "real n powr - s < r" .
qed
-
-
-ML
-{*
-val powr_one_eq_one = thm "powr_one_eq_one";
-val powr_zero_eq_one = thm "powr_zero_eq_one";
-val powr_one_gt_zero_iff = thm "powr_one_gt_zero_iff";
-val powr_mult = thm "powr_mult";
-val powr_gt_zero = thm "powr_gt_zero";
-val powr_not_zero = thm "powr_not_zero";
-val powr_divide = thm "powr_divide";
-val powr_add = thm "powr_add";
-val powr_powr = thm "powr_powr";
-val powr_powr_swap = thm "powr_powr_swap";
-val powr_minus = thm "powr_minus";
-val powr_minus_divide = thm "powr_minus_divide";
-val powr_less_mono = thm "powr_less_mono";
-val powr_less_cancel = thm "powr_less_cancel";
-val powr_less_cancel_iff = thm "powr_less_cancel_iff";
-val powr_le_cancel_iff = thm "powr_le_cancel_iff";
-val log_ln = thm "log_ln";
-val powr_log_cancel = thm "powr_log_cancel";
-val log_powr_cancel = thm "log_powr_cancel";
-val log_mult = thm "log_mult";
-val log_eq_div_ln_mult_log = thm "log_eq_div_ln_mult_log";
-val log_base_10_eq1 = thm "log_base_10_eq1";
-val log_base_10_eq2 = thm "log_base_10_eq2";
-val log_one = thm "log_one";
-val log_eq_one = thm "log_eq_one";
-val log_inverse = thm "log_inverse";
-val log_divide = thm "log_divide";
-val log_less_cancel_iff = thm "log_less_cancel_iff";
-val log_le_cancel_iff = thm "log_le_cancel_iff";
-*}
-
end
--- a/src/HOL/Hyperreal/MacLaurin.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Fri Jun 02 23:22:29 2006 +0200
@@ -31,18 +31,24 @@
text{*A crude tactic to differentiate by proof.*}
ML
{*
+local
+val deriv_rulesI =
+ [thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
+ thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow",
+ thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus",
+ thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow",
+ thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos",
+ thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"];
+
+val DERIV_chain2 = thm "DERIV_chain2";
+
+in
+
exception DERIV_name;
fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
| get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
| get_fun_name _ = raise DERIV_name;
-val deriv_rulesI = [DERIV_Id,DERIV_const,DERIV_cos,DERIV_cmult,
- DERIV_sin, DERIV_exp, DERIV_inverse,DERIV_pow,
- DERIV_add, DERIV_diff, DERIV_mult, DERIV_minus,
- DERIV_inverse_fun,DERIV_quotient,DERIV_fun_pow,
- DERIV_fun_exp,DERIV_fun_sin,DERIV_fun_cos,
- DERIV_Id,DERIV_const,DERIV_cos];
-
val deriv_tac =
SUBGOAL (fn (prem,i) =>
(resolve_tac deriv_rulesI i) ORELSE
@@ -50,6 +56,8 @@
DERIV_chain2) i) handle DERIV_name => no_tac));;
val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));
+
+end
*}
lemma Maclaurin_lemma2:
--- a/src/HOL/Hyperreal/NSA.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Fri Jun 02 23:22:29 2006 +0200
@@ -11,42 +11,41 @@
imports HyperArith "../Real/RComplete"
begin
-constdefs
+definition
Infinitesimal :: "hypreal set"
- "Infinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> abs x < r}"
+ "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> abs x < r}"
HFinite :: "hypreal set"
- "HFinite == {x. \<exists>r \<in> Reals. abs x < r}"
+ "HFinite = {x. \<exists>r \<in> Reals. abs x < r}"
HInfinite :: "hypreal set"
- "HInfinite == {x. \<forall>r \<in> Reals. r < abs x}"
+ "HInfinite = {x. \<forall>r \<in> Reals. r < abs x}"
approx :: "[hypreal, hypreal] => bool" (infixl "@=" 50)
--{*the `infinitely close' relation*}
- "x @= y == (x + -y) \<in> Infinitesimal"
+ "(x @= y) = ((x + -y) \<in> Infinitesimal)"
st :: "hypreal => hypreal"
--{*the standard part of a hyperreal*}
- "st == (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
+ "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
monad :: "hypreal => hypreal set"
- "monad x == {y. x @= y}"
+ "monad x = {y. x @= y}"
galaxy :: "hypreal => hypreal set"
- "galaxy x == {y. (x + -y) \<in> HFinite}"
+ "galaxy x = {y. (x + -y) \<in> HFinite}"
+
+const_syntax (xsymbols)
+ approx (infixl "\<approx>" 50)
+
+const_syntax (HTML output)
+ approx (infixl "\<approx>" 50)
defs (overloaded)
-
- SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
- --{*the standard real numbers as a subset of the hyperreals*}
-
-syntax (xsymbols)
- approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50)
-
-syntax (HTML output)
- approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50)
+ SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
+ --{*the standard real numbers as a subset of the hyperreals*}
@@ -507,101 +506,16 @@
by (blast intro: approx_sym)
-ML
-{*
-val SReal_add = thm "SReal_add";
-val SReal_mult = thm "SReal_mult";
-val SReal_inverse = thm "SReal_inverse";
-val SReal_divide = thm "SReal_divide";
-val SReal_minus = thm "SReal_minus";
-val SReal_minus_iff = thm "SReal_minus_iff";
-val SReal_add_cancel = thm "SReal_add_cancel";
-val SReal_hrabs = thm "SReal_hrabs";
-val SReal_hypreal_of_real = thm "SReal_hypreal_of_real";
-val SReal_number_of = thm "SReal_number_of";
-val Reals_0 = thm "Reals_0";
-val Reals_1 = thm "Reals_1";
-val SReal_divide_number_of = thm "SReal_divide_number_of";
-val SReal_epsilon_not_mem = thm "SReal_epsilon_not_mem";
-val SReal_omega_not_mem = thm "SReal_omega_not_mem";
-val SReal_UNIV_real = thm "SReal_UNIV_real";
-val SReal_iff = thm "SReal_iff";
-val hypreal_of_real_image = thm "hypreal_of_real_image";
-val inv_hypreal_of_real_image = thm "inv_hypreal_of_real_image";
-val SReal_hypreal_of_real_image = thm "SReal_hypreal_of_real_image";
-val SReal_dense = thm "SReal_dense";
-val hypreal_of_real_isUb_iff = thm "hypreal_of_real_isUb_iff";
-val hypreal_of_real_isLub1 = thm "hypreal_of_real_isLub1";
-val hypreal_of_real_isLub2 = thm "hypreal_of_real_isLub2";
-val hypreal_of_real_isLub_iff = thm "hypreal_of_real_isLub_iff";
-val lemma_isUb_hypreal_of_real = thm "lemma_isUb_hypreal_of_real";
-val lemma_isLub_hypreal_of_real = thm "lemma_isLub_hypreal_of_real";
-val lemma_isLub_hypreal_of_real2 = thm "lemma_isLub_hypreal_of_real2";
-val SReal_complete = thm "SReal_complete";
-val HFinite_add = thm "HFinite_add";
-val HFinite_mult = thm "HFinite_mult";
-val HFinite_minus_iff = thm "HFinite_minus_iff";
-val SReal_subset_HFinite = thm "SReal_subset_HFinite";
-val HFinite_hypreal_of_real = thm "HFinite_hypreal_of_real";
-val HFiniteD = thm "HFiniteD";
-val HFinite_hrabs_iff = thm "HFinite_hrabs_iff";
-val HFinite_number_of = thm "HFinite_number_of";
-val HFinite_0 = thm "HFinite_0";
-val HFinite_1 = thm "HFinite_1";
-val HFinite_bounded = thm "HFinite_bounded";
-val InfinitesimalD = thm "InfinitesimalD";
-val Infinitesimal_zero = thm "Infinitesimal_zero";
-val hypreal_sum_of_halves = thm "hypreal_sum_of_halves";
-val Infinitesimal_add = thm "Infinitesimal_add";
-val Infinitesimal_minus_iff = thm "Infinitesimal_minus_iff";
-val Infinitesimal_diff = thm "Infinitesimal_diff";
-val Infinitesimal_mult = thm "Infinitesimal_mult";
-val Infinitesimal_HFinite_mult = thm "Infinitesimal_HFinite_mult";
-val Infinitesimal_HFinite_mult2 = thm "Infinitesimal_HFinite_mult2";
-val HInfinite_inverse_Infinitesimal = thm "HInfinite_inverse_Infinitesimal";
-val HInfinite_mult = thm "HInfinite_mult";
-val HInfinite_add_ge_zero = thm "HInfinite_add_ge_zero";
-val HInfinite_add_ge_zero2 = thm "HInfinite_add_ge_zero2";
-val HInfinite_add_gt_zero = thm "HInfinite_add_gt_zero";
-val HInfinite_minus_iff = thm "HInfinite_minus_iff";
-val HInfinite_add_le_zero = thm "HInfinite_add_le_zero";
-val HInfinite_add_lt_zero = thm "HInfinite_add_lt_zero";
-val HFinite_sum_squares = thm "HFinite_sum_squares";
-val not_Infinitesimal_not_zero = thm "not_Infinitesimal_not_zero";
-val not_Infinitesimal_not_zero2 = thm "not_Infinitesimal_not_zero2";
-val Infinitesimal_hrabs_iff = thm "Infinitesimal_hrabs_iff";
-val HFinite_diff_Infinitesimal_hrabs = thm "HFinite_diff_Infinitesimal_hrabs";
-val hrabs_less_Infinitesimal = thm "hrabs_less_Infinitesimal";
-val hrabs_le_Infinitesimal = thm "hrabs_le_Infinitesimal";
-val Infinitesimal_interval = thm "Infinitesimal_interval";
-val Infinitesimal_interval2 = thm "Infinitesimal_interval2";
-val not_Infinitesimal_mult = thm "not_Infinitesimal_mult";
-val Infinitesimal_mult_disj = thm "Infinitesimal_mult_disj";
-val HFinite_Infinitesimal_not_zero = thm "HFinite_Infinitesimal_not_zero";
-val HFinite_Infinitesimal_diff_mult = thm "HFinite_Infinitesimal_diff_mult";
-val Infinitesimal_subset_HFinite = thm "Infinitesimal_subset_HFinite";
-val Infinitesimal_hypreal_of_real_mult = thm "Infinitesimal_hypreal_of_real_mult";
-val Infinitesimal_hypreal_of_real_mult2 = thm "Infinitesimal_hypreal_of_real_mult2";
-val mem_infmal_iff = thm "mem_infmal_iff";
-val approx_minus_iff = thm "approx_minus_iff";
-val approx_minus_iff2 = thm "approx_minus_iff2";
-val approx_refl = thm "approx_refl";
-val approx_sym = thm "approx_sym";
-val approx_trans = thm "approx_trans";
-val approx_trans2 = thm "approx_trans2";
-val approx_trans3 = thm "approx_trans3";
-val number_of_approx_reorient = thm "number_of_approx_reorient";
-val zero_approx_reorient = thm "zero_approx_reorient";
-val one_approx_reorient = thm "one_approx_reorient";
-
+ML {*
+local
(*** re-orientation, following HOL/Integ/Bin.ML
We re-orient x @=y where x is 0, 1 or a numeral, unless y is as well!
***)
(*reorientation simprules using ==, for the following simproc*)
-val meta_zero_approx_reorient = zero_approx_reorient RS eq_reflection;
-val meta_one_approx_reorient = one_approx_reorient RS eq_reflection;
-val meta_number_of_approx_reorient = number_of_approx_reorient RS eq_reflection
+val meta_zero_approx_reorient = thm "zero_approx_reorient" RS eq_reflection;
+val meta_one_approx_reorient = thm "one_approx_reorient" RS eq_reflection;
+val meta_number_of_approx_reorient = thm "number_of_approx_reorient" RS eq_reflection
(*reorientation simplification procedure: reorients (polymorphic)
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
@@ -616,9 +530,11 @@
| Const("Numeral.number_of", _) $ _ =>
meta_number_of_approx_reorient);
+in
val approx_reorient_simproc =
Bin_Simprocs.prep_simproc
("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
+end;
Addsimprocs [approx_reorient_simproc];
*}
@@ -2147,213 +2063,4 @@
simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_minus
star_n_add star_n_inverse)
-
-ML
-{*
-val Infinitesimal_def = thm"Infinitesimal_def";
-val HFinite_def = thm"HFinite_def";
-val HInfinite_def = thm"HInfinite_def";
-val st_def = thm"st_def";
-val monad_def = thm"monad_def";
-val galaxy_def = thm"galaxy_def";
-val approx_def = thm"approx_def";
-val SReal_def = thm"SReal_def";
-
-val Infinitesimal_approx_minus = thm "Infinitesimal_approx_minus";
-val approx_monad_iff = thm "approx_monad_iff";
-val Infinitesimal_approx = thm "Infinitesimal_approx";
-val approx_add = thm "approx_add";
-val approx_minus = thm "approx_minus";
-val approx_minus2 = thm "approx_minus2";
-val approx_minus_cancel = thm "approx_minus_cancel";
-val approx_add_minus = thm "approx_add_minus";
-val approx_mult1 = thm "approx_mult1";
-val approx_mult2 = thm "approx_mult2";
-val approx_mult_subst = thm "approx_mult_subst";
-val approx_mult_subst2 = thm "approx_mult_subst2";
-val approx_mult_subst_SReal = thm "approx_mult_subst_SReal";
-val approx_eq_imp = thm "approx_eq_imp";
-val Infinitesimal_minus_approx = thm "Infinitesimal_minus_approx";
-val bex_Infinitesimal_iff = thm "bex_Infinitesimal_iff";
-val bex_Infinitesimal_iff2 = thm "bex_Infinitesimal_iff2";
-val Infinitesimal_add_approx = thm "Infinitesimal_add_approx";
-val Infinitesimal_add_approx_self = thm "Infinitesimal_add_approx_self";
-val Infinitesimal_add_approx_self2 = thm "Infinitesimal_add_approx_self2";
-val Infinitesimal_add_minus_approx_self = thm "Infinitesimal_add_minus_approx_self";
-val Infinitesimal_add_cancel = thm "Infinitesimal_add_cancel";
-val Infinitesimal_add_right_cancel = thm "Infinitesimal_add_right_cancel";
-val approx_add_left_cancel = thm "approx_add_left_cancel";
-val approx_add_right_cancel = thm "approx_add_right_cancel";
-val approx_add_mono1 = thm "approx_add_mono1";
-val approx_add_mono2 = thm "approx_add_mono2";
-val approx_add_left_iff = thm "approx_add_left_iff";
-val approx_add_right_iff = thm "approx_add_right_iff";
-val approx_HFinite = thm "approx_HFinite";
-val approx_hypreal_of_real_HFinite = thm "approx_hypreal_of_real_HFinite";
-val approx_mult_HFinite = thm "approx_mult_HFinite";
-val approx_mult_hypreal_of_real = thm "approx_mult_hypreal_of_real";
-val approx_SReal_mult_cancel_zero = thm "approx_SReal_mult_cancel_zero";
-val approx_mult_SReal1 = thm "approx_mult_SReal1";
-val approx_mult_SReal2 = thm "approx_mult_SReal2";
-val approx_mult_SReal_zero_cancel_iff = thm "approx_mult_SReal_zero_cancel_iff";
-val approx_SReal_mult_cancel = thm "approx_SReal_mult_cancel";
-val approx_SReal_mult_cancel_iff1 = thm "approx_SReal_mult_cancel_iff1";
-val approx_le_bound = thm "approx_le_bound";
-val Infinitesimal_less_SReal = thm "Infinitesimal_less_SReal";
-val Infinitesimal_less_SReal2 = thm "Infinitesimal_less_SReal2";
-val SReal_not_Infinitesimal = thm "SReal_not_Infinitesimal";
-val SReal_minus_not_Infinitesimal = thm "SReal_minus_not_Infinitesimal";
-val SReal_Int_Infinitesimal_zero = thm "SReal_Int_Infinitesimal_zero";
-val SReal_Infinitesimal_zero = thm "SReal_Infinitesimal_zero";
-val SReal_HFinite_diff_Infinitesimal = thm "SReal_HFinite_diff_Infinitesimal";
-val hypreal_of_real_HFinite_diff_Infinitesimal = thm "hypreal_of_real_HFinite_diff_Infinitesimal";
-val hypreal_of_real_Infinitesimal_iff_0 = thm "hypreal_of_real_Infinitesimal_iff_0";
-val number_of_not_Infinitesimal = thm "number_of_not_Infinitesimal";
-val one_not_Infinitesimal = thm "one_not_Infinitesimal";
-val approx_SReal_not_zero = thm "approx_SReal_not_zero";
-val HFinite_diff_Infinitesimal_approx = thm "HFinite_diff_Infinitesimal_approx";
-val Infinitesimal_ratio = thm "Infinitesimal_ratio";
-val SReal_approx_iff = thm "SReal_approx_iff";
-val number_of_approx_iff = thm "number_of_approx_iff";
-val hypreal_of_real_approx_iff = thm "hypreal_of_real_approx_iff";
-val hypreal_of_real_approx_number_of_iff = thm "hypreal_of_real_approx_number_of_iff";
-val approx_unique_real = thm "approx_unique_real";
-val hypreal_isLub_unique = thm "hypreal_isLub_unique";
-val hypreal_setle_less_trans = thm "hypreal_setle_less_trans";
-val hypreal_gt_isUb = thm "hypreal_gt_isUb";
-val st_part_Ex = thm "st_part_Ex";
-val st_part_Ex1 = thm "st_part_Ex1";
-val HFinite_Int_HInfinite_empty = thm "HFinite_Int_HInfinite_empty";
-val HFinite_not_HInfinite = thm "HFinite_not_HInfinite";
-val not_HFinite_HInfinite = thm "not_HFinite_HInfinite";
-val HInfinite_HFinite_disj = thm "HInfinite_HFinite_disj";
-val HInfinite_HFinite_iff = thm "HInfinite_HFinite_iff";
-val HFinite_HInfinite_iff = thm "HFinite_HInfinite_iff";
-val HInfinite_diff_HFinite_Infinitesimal_disj = thm "HInfinite_diff_HFinite_Infinitesimal_disj";
-val HFinite_inverse = thm "HFinite_inverse";
-val HFinite_inverse2 = thm "HFinite_inverse2";
-val Infinitesimal_inverse_HFinite = thm "Infinitesimal_inverse_HFinite";
-val HFinite_not_Infinitesimal_inverse = thm "HFinite_not_Infinitesimal_inverse";
-val approx_inverse = thm "approx_inverse";
-val hypreal_of_real_approx_inverse = thm "hypreal_of_real_approx_inverse";
-val inverse_add_Infinitesimal_approx = thm "inverse_add_Infinitesimal_approx";
-val inverse_add_Infinitesimal_approx2 = thm "inverse_add_Infinitesimal_approx2";
-val inverse_add_Infinitesimal_approx_Infinitesimal = thm "inverse_add_Infinitesimal_approx_Infinitesimal";
-val Infinitesimal_square_iff = thm "Infinitesimal_square_iff";
-val HFinite_square_iff = thm "HFinite_square_iff";
-val HInfinite_square_iff = thm "HInfinite_square_iff";
-val approx_HFinite_mult_cancel = thm "approx_HFinite_mult_cancel";
-val approx_HFinite_mult_cancel_iff1 = thm "approx_HFinite_mult_cancel_iff1";
-val approx_hrabs_disj = thm "approx_hrabs_disj";
-val monad_hrabs_Un_subset = thm "monad_hrabs_Un_subset";
-val Infinitesimal_monad_eq = thm "Infinitesimal_monad_eq";
-val mem_monad_iff = thm "mem_monad_iff";
-val Infinitesimal_monad_zero_iff = thm "Infinitesimal_monad_zero_iff";
-val monad_zero_minus_iff = thm "monad_zero_minus_iff";
-val monad_zero_hrabs_iff = thm "monad_zero_hrabs_iff";
-val mem_monad_self = thm "mem_monad_self";
-val approx_subset_monad = thm "approx_subset_monad";
-val approx_subset_monad2 = thm "approx_subset_monad2";
-val mem_monad_approx = thm "mem_monad_approx";
-val approx_mem_monad = thm "approx_mem_monad";
-val approx_mem_monad2 = thm "approx_mem_monad2";
-val approx_mem_monad_zero = thm "approx_mem_monad_zero";
-val Infinitesimal_approx_hrabs = thm "Infinitesimal_approx_hrabs";
-val less_Infinitesimal_less = thm "less_Infinitesimal_less";
-val Ball_mem_monad_gt_zero = thm "Ball_mem_monad_gt_zero";
-val Ball_mem_monad_less_zero = thm "Ball_mem_monad_less_zero";
-val approx_hrabs = thm "approx_hrabs";
-val approx_hrabs_zero_cancel = thm "approx_hrabs_zero_cancel";
-val approx_hrabs_add_Infinitesimal = thm "approx_hrabs_add_Infinitesimal";
-val approx_hrabs_add_minus_Infinitesimal = thm "approx_hrabs_add_minus_Infinitesimal";
-val hrabs_add_Infinitesimal_cancel = thm "hrabs_add_Infinitesimal_cancel";
-val hrabs_add_minus_Infinitesimal_cancel = thm "hrabs_add_minus_Infinitesimal_cancel";
-val Infinitesimal_add_hypreal_of_real_less = thm "Infinitesimal_add_hypreal_of_real_less";
-val Infinitesimal_add_hrabs_hypreal_of_real_less = thm "Infinitesimal_add_hrabs_hypreal_of_real_less";
-val Infinitesimal_add_hrabs_hypreal_of_real_less2 = thm "Infinitesimal_add_hrabs_hypreal_of_real_less2";
-val hypreal_of_real_le_add_Infininitesimal_cancel2 = thm"hypreal_of_real_le_add_Infininitesimal_cancel2";
-val hypreal_of_real_less_Infinitesimal_le_zero = thm "hypreal_of_real_less_Infinitesimal_le_zero";
-val Infinitesimal_add_not_zero = thm "Infinitesimal_add_not_zero";
-val Infinitesimal_square_cancel = thm "Infinitesimal_square_cancel";
-val HFinite_square_cancel = thm "HFinite_square_cancel";
-val Infinitesimal_square_cancel2 = thm "Infinitesimal_square_cancel2";
-val HFinite_square_cancel2 = thm "HFinite_square_cancel2";
-val Infinitesimal_sum_square_cancel = thm "Infinitesimal_sum_square_cancel";
-val HFinite_sum_square_cancel = thm "HFinite_sum_square_cancel";
-val Infinitesimal_sum_square_cancel2 = thm "Infinitesimal_sum_square_cancel2";
-val HFinite_sum_square_cancel2 = thm "HFinite_sum_square_cancel2";
-val Infinitesimal_sum_square_cancel3 = thm "Infinitesimal_sum_square_cancel3";
-val HFinite_sum_square_cancel3 = thm "HFinite_sum_square_cancel3";
-val monad_hrabs_less = thm "monad_hrabs_less";
-val mem_monad_SReal_HFinite = thm "mem_monad_SReal_HFinite";
-val st_approx_self = thm "st_approx_self";
-val st_SReal = thm "st_SReal";
-val st_HFinite = thm "st_HFinite";
-val st_SReal_eq = thm "st_SReal_eq";
-val st_hypreal_of_real = thm "st_hypreal_of_real";
-val st_eq_approx = thm "st_eq_approx";
-val approx_st_eq = thm "approx_st_eq";
-val st_eq_approx_iff = thm "st_eq_approx_iff";
-val st_Infinitesimal_add_SReal = thm "st_Infinitesimal_add_SReal";
-val st_Infinitesimal_add_SReal2 = thm "st_Infinitesimal_add_SReal2";
-val HFinite_st_Infinitesimal_add = thm "HFinite_st_Infinitesimal_add";
-val st_add = thm "st_add";
-val st_number_of = thm "st_number_of";
-val st_minus = thm "st_minus";
-val st_diff = thm "st_diff";
-val st_mult = thm "st_mult";
-val st_Infinitesimal = thm "st_Infinitesimal";
-val st_not_Infinitesimal = thm "st_not_Infinitesimal";
-val st_inverse = thm "st_inverse";
-val st_divide = thm "st_divide";
-val st_idempotent = thm "st_idempotent";
-val Infinitesimal_add_st_less = thm "Infinitesimal_add_st_less";
-val Infinitesimal_add_st_le_cancel = thm "Infinitesimal_add_st_le_cancel";
-val st_le = thm "st_le";
-val st_zero_le = thm "st_zero_le";
-val st_zero_ge = thm "st_zero_ge";
-val st_hrabs = thm "st_hrabs";
-val FreeUltrafilterNat_HFinite = thm "FreeUltrafilterNat_HFinite";
-val HFinite_FreeUltrafilterNat_iff = thm "HFinite_FreeUltrafilterNat_iff";
-val FreeUltrafilterNat_const_Finite = thm "FreeUltrafilterNat_const_Finite";
-val FreeUltrafilterNat_HInfinite = thm "FreeUltrafilterNat_HInfinite";
-val HInfinite_FreeUltrafilterNat_iff = thm "HInfinite_FreeUltrafilterNat_iff";
-val Infinitesimal_FreeUltrafilterNat = thm "Infinitesimal_FreeUltrafilterNat";
-val FreeUltrafilterNat_Infinitesimal = thm "FreeUltrafilterNat_Infinitesimal";
-val Infinitesimal_FreeUltrafilterNat_iff = thm "Infinitesimal_FreeUltrafilterNat_iff";
-val Infinitesimal_hypreal_of_nat_iff = thm "Infinitesimal_hypreal_of_nat_iff";
-val Suc_Un_eq = thm "Suc_Un_eq";
-val finite_nat_segment = thm "finite_nat_segment";
-val finite_real_of_nat_segment = thm "finite_real_of_nat_segment";
-val finite_real_of_nat_less_real = thm "finite_real_of_nat_less_real";
-val finite_real_of_nat_le_real = thm "finite_real_of_nat_le_real";
-val finite_rabs_real_of_nat_le_real = thm "finite_rabs_real_of_nat_le_real";
-val rabs_real_of_nat_le_real_FreeUltrafilterNat = thm "rabs_real_of_nat_le_real_FreeUltrafilterNat";
-val FreeUltrafilterNat_nat_gt_real = thm "FreeUltrafilterNat_nat_gt_real";
-val FreeUltrafilterNat_omega = thm "FreeUltrafilterNat_omega";
-val HInfinite_omega = thm "HInfinite_omega";
-val Infinitesimal_epsilon = thm "Infinitesimal_epsilon";
-val HFinite_epsilon = thm "HFinite_epsilon";
-val epsilon_approx_zero = thm "epsilon_approx_zero";
-val real_of_nat_less_inverse_iff = thm "real_of_nat_less_inverse_iff";
-val finite_inverse_real_of_posnat_gt_real = thm "finite_inverse_real_of_posnat_gt_real";
-val real_of_nat_inverse_le_iff = thm "real_of_nat_inverse_le_iff";
-val real_of_nat_inverse_eq_iff = thm "real_of_nat_inverse_eq_iff";
-val finite_inverse_real_of_posnat_ge_real = thm "finite_inverse_real_of_posnat_ge_real";
-val inverse_real_of_posnat_ge_real_FreeUltrafilterNat = thm "inverse_real_of_posnat_ge_real_FreeUltrafilterNat";
-val FreeUltrafilterNat_inverse_real_of_posnat = thm "FreeUltrafilterNat_inverse_real_of_posnat";
-val real_seq_to_hypreal_Infinitesimal = thm "real_seq_to_hypreal_Infinitesimal";
-val real_seq_to_hypreal_approx = thm "real_seq_to_hypreal_approx";
-val real_seq_to_hypreal_approx2 = thm "real_seq_to_hypreal_approx2";
-val real_seq_to_hypreal_Infinitesimal2 = thm "real_seq_to_hypreal_Infinitesimal2";
-val HInfinite_HFinite_add = thm "HInfinite_HFinite_add";
-val HInfinite_ge_HInfinite = thm "HInfinite_ge_HInfinite";
-val Infinitesimal_inverse_HInfinite = thm "Infinitesimal_inverse_HInfinite";
-val HInfinite_HFinite_not_Infinitesimal_mult = thm "HInfinite_HFinite_not_Infinitesimal_mult";
-val HInfinite_HFinite_not_Infinitesimal_mult2 = thm "HInfinite_HFinite_not_Infinitesimal_mult2";
-val HInfinite_gt_SReal = thm "HInfinite_gt_SReal";
-val HInfinite_gt_zero_gt_one = thm "HInfinite_gt_zero_gt_one";
-val not_HInfinite_one = thm "not_HInfinite_one";
-*}
-
end
--- a/src/HOL/Hyperreal/NatStar.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy Fri Jun 02 23:22:29 2006 +0200
@@ -182,51 +182,12 @@
apply (simp_all add: HNatInfinite_not_eq_zero starfunNat_real_of_nat)
done
-ML
-{*
-val starset_n_Un = thm "starset_n_Un";
-val InternalSets_Un = thm "InternalSets_Un";
-val starset_n_Int = thm "starset_n_Int";
-val InternalSets_Int = thm "InternalSets_Int";
-val starset_n_Compl = thm "starset_n_Compl";
-val InternalSets_Compl = thm "InternalSets_Compl";
-val starset_n_diff = thm "starset_n_diff";
-val InternalSets_diff = thm "InternalSets_diff";
-val NatStar_SHNat_subset = thm "NatStar_SHNat_subset";
-val NatStar_hypreal_of_real_Int = thm "NatStar_hypreal_of_real_Int";
-val starset_starset_n_eq = thm "starset_starset_n_eq";
-val InternalSets_starset_n = thm "InternalSets_starset_n";
-val InternalSets_UNIV_diff = thm "InternalSets_UNIV_diff";
-val starset_n_starset = thm "starset_n_starset";
-val starfun_const_fun = thm "starfun_const_fun";
-val starfun_le_mono = thm "starfun_le_mono";
-val starfun_less_mono = thm "starfun_less_mono";
-val starfun_shift_one = thm "starfun_shift_one";
-val starfun_abs = thm "starfun_abs";
-val starfun_pow = thm "starfun_pow";
-val starfun_pow2 = thm "starfun_pow2";
-val starfun_pow3 = thm "starfun_pow3";
-val starfunNat_real_of_nat = thm "starfunNat_real_of_nat";
-val starfun_inverse_real_of_nat_eq = thm "starfun_inverse_real_of_nat_eq";
-val starfun_n = thm "starfun_n";
-val starfun_n_mult = thm "starfun_n_mult";
-val starfun_n_add = thm "starfun_n_add";
-val starfun_n_add_minus = thm "starfun_n_add_minus";
-val starfun_n_const_fun = thm "starfun_n_const_fun";
-val starfun_n_minus = thm "starfun_n_minus";
-val starfun_n_eq = thm "starfun_n_eq";
-val starfun_eq_iff = thm "starfun_eq_iff";
-val starfunNat_inverse_real_of_nat_Infinitesimal = thm "starfunNat_inverse_real_of_nat_Infinitesimal";
-*}
-
-
subsection{*Nonstandard Characterization of Induction*}
-
-constdefs
+definition
hSuc :: "hypnat => hypnat"
- "hSuc n == n + 1"
+ "hSuc n = n + 1"
lemma starP: "(( *p* P) (star_n X)) = ({n. P (X n)} \<in> FreeUltrafilterNat)"
by (rule starP_star_n)
--- a/src/HOL/Hyperreal/NthRoot.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy Fri Jun 02 23:22:29 2006 +0200
@@ -170,17 +170,4 @@
apply (drule_tac [4] x = y in realpow_less, auto)
done
-ML
-{*
-val nth_realpow_isLub_ex = thm"nth_realpow_isLub_ex";
-val realpow_nth_ge = thm"realpow_nth_ge";
-val less_isLub_not_isUb = thm"less_isLub_not_isUb";
-val not_isUb_less_ex = thm"not_isUb_less_ex";
-val realpow_nth_le = thm"realpow_nth_le";
-val realpow_nth = thm"realpow_nth";
-val realpow_pos_nth = thm"realpow_pos_nth";
-val realpow_pos_nth2 = thm"realpow_pos_nth2";
-val realpow_pos_nth_unique = thm"realpow_pos_nth_unique";
-*}
-
end
--- a/src/HOL/Hyperreal/Poly.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Fri Jun 02 23:22:29 2006 +0200
@@ -81,29 +81,29 @@
text{*Other definitions*}
-constdefs
- poly_minus :: "real list => real list" ("-- _" [80] 80)
- "-- p == (- 1) %* p"
+definition
+ poly_minus :: "real list => real list" ("-- _" [80] 80)
+ "-- p = (- 1) %* p"
- pderiv :: "real list => real list"
- "pderiv p == if p = [] then [] else pderiv_aux 1 (tl p)"
+ pderiv :: "real list => real list"
+ "pderiv p = (if p = [] then [] else pderiv_aux 1 (tl p))"
- divides :: "[real list,real list] => bool" (infixl "divides" 70)
- "p1 divides p2 == \<exists>q. poly p2 = poly(p1 *** q)"
+ divides :: "[real list,real list] => bool" (infixl "divides" 70)
+ "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
- order :: "real => real list => nat"
- --{*order of a polynomial*}
- "order a p == (@n. ([-a, 1] %^ n) divides p &
+ order :: "real => real list => nat"
+ --{*order of a polynomial*}
+ "order a p = (SOME n. ([-a, 1] %^ n) divides p &
~ (([-a, 1] %^ (Suc n)) divides p))"
- degree :: "real list => nat"
+ degree :: "real list => nat"
--{*degree of a polynomial*}
- "degree p == length (pnormalize p)"
+ "degree p = length (pnormalize p)"
- rsquarefree :: "real list => bool"
+ rsquarefree :: "real list => bool"
--{*squarefree polynomials --- NB with respect to real roots only.*}
- "rsquarefree p == poly p \<noteq> poly [] &
- (\<forall>a. (order a p = 0) | (order a p = 1))"
+ "rsquarefree p = (poly p \<noteq> poly [] &
+ (\<forall>a. (order a p = 0) | (order a p = 1)))"
@@ -1026,135 +1026,4 @@
apply (auto intro!: mult_mono simp add: abs_mult, arith)
done
-ML
-{*
-val padd_Nil2 = thm "padd_Nil2";
-val padd_Cons_Cons = thm "padd_Cons_Cons";
-val pminus_Nil = thm "pminus_Nil";
-val pmult_singleton = thm "pmult_singleton";
-val poly_ident_mult = thm "poly_ident_mult";
-val poly_simple_add_Cons = thm "poly_simple_add_Cons";
-val padd_commut = thm "padd_commut";
-val padd_assoc = thm "padd_assoc";
-val poly_cmult_distr = thm "poly_cmult_distr";
-val pmult_by_x = thm "pmult_by_x";
-val poly_add = thm "poly_add";
-val poly_cmult = thm "poly_cmult";
-val poly_minus = thm "poly_minus";
-val poly_mult = thm "poly_mult";
-val poly_exp = thm "poly_exp";
-val poly_add_rzero = thm "poly_add_rzero";
-val poly_mult_assoc = thm "poly_mult_assoc";
-val poly_mult_Nil2 = thm "poly_mult_Nil2";
-val poly_exp_add = thm "poly_exp_add";
-val pderiv_Nil = thm "pderiv_Nil";
-val pderiv_singleton = thm "pderiv_singleton";
-val pderiv_Cons = thm "pderiv_Cons";
-val DERIV_cmult2 = thm "DERIV_cmult2";
-val DERIV_pow2 = thm "DERIV_pow2";
-val lemma_DERIV_poly1 = thm "lemma_DERIV_poly1";
-val lemma_DERIV_poly = thm "lemma_DERIV_poly";
-val DERIV_add_const = thm "DERIV_add_const";
-val poly_DERIV = thm "poly_DERIV";
-val poly_differentiable = thm "poly_differentiable";
-val poly_isCont = thm "poly_isCont";
-val poly_IVT_pos = thm "poly_IVT_pos";
-val poly_IVT_neg = thm "poly_IVT_neg";
-val poly_MVT = thm "poly_MVT";
-val lemma_poly_pderiv_aux_add = thm "lemma_poly_pderiv_aux_add";
-val poly_pderiv_aux_add = thm "poly_pderiv_aux_add";
-val lemma_poly_pderiv_aux_cmult = thm "lemma_poly_pderiv_aux_cmult";
-val poly_pderiv_aux_cmult = thm "poly_pderiv_aux_cmult";
-val poly_pderiv_aux_minus = thm "poly_pderiv_aux_minus";
-val lemma_poly_pderiv_aux_mult1 = thm "lemma_poly_pderiv_aux_mult1";
-val lemma_poly_pderiv_aux_mult = thm "lemma_poly_pderiv_aux_mult";
-val lemma_poly_pderiv_add = thm "lemma_poly_pderiv_add";
-val poly_pderiv_add = thm "poly_pderiv_add";
-val poly_pderiv_cmult = thm "poly_pderiv_cmult";
-val poly_pderiv_minus = thm "poly_pderiv_minus";
-val lemma_poly_mult_pderiv = thm "lemma_poly_mult_pderiv";
-val poly_pderiv_mult = thm "poly_pderiv_mult";
-val poly_pderiv_exp = thm "poly_pderiv_exp";
-val poly_pderiv_exp_prime = thm "poly_pderiv_exp_prime";
-val lemma_poly_linear_rem = thm "lemma_poly_linear_rem";
-val poly_linear_rem = thm "poly_linear_rem";
-val poly_linear_divides = thm "poly_linear_divides";
-val lemma_poly_length_mult = thm "lemma_poly_length_mult";
-val lemma_poly_length_mult2 = thm "lemma_poly_length_mult2";
-val poly_length_mult = thm "poly_length_mult";
-val poly_cmult_length = thm "poly_cmult_length";
-val poly_add_length = thm "poly_add_length";
-val poly_root_mult_length = thm "poly_root_mult_length";
-val poly_mult_not_eq_poly_Nil = thm "poly_mult_not_eq_poly_Nil";
-val poly_mult_eq_zero_disj = thm "poly_mult_eq_zero_disj";
-val poly_normalized_nil = thm "poly_normalized_nil";
-val poly_roots_index_lemma = thm "poly_roots_index_lemma";
-val poly_roots_index_lemma2 = thms "poly_roots_index_lemma2";
-val poly_roots_index_length = thm "poly_roots_index_length";
-val poly_roots_finite_lemma = thm "poly_roots_finite_lemma";
-val real_finite_lemma = thm "real_finite_lemma";
-val poly_roots_finite = thm "poly_roots_finite";
-val poly_entire_lemma = thm "poly_entire_lemma";
-val poly_entire = thm "poly_entire";
-val poly_entire_neg = thm "poly_entire_neg";
-val fun_eq = thm "fun_eq";
-val poly_add_minus_zero_iff = thm "poly_add_minus_zero_iff";
-val poly_add_minus_mult_eq = thm "poly_add_minus_mult_eq";
-val poly_mult_left_cancel = thm "poly_mult_left_cancel";
-val real_mult_zero_disj_iff = thm "real_mult_zero_disj_iff";
-val poly_exp_eq_zero = thm "poly_exp_eq_zero";
-val poly_prime_eq_zero = thm "poly_prime_eq_zero";
-val poly_exp_prime_eq_zero = thm "poly_exp_prime_eq_zero";
-val poly_zero_lemma = thm "poly_zero_lemma";
-val poly_zero = thm "poly_zero";
-val pderiv_aux_iszero = thm "pderiv_aux_iszero";
-val pderiv_aux_iszero_num = thm "pderiv_aux_iszero_num";
-val pderiv_iszero = thm "pderiv_iszero";
-val pderiv_zero_obj = thm "pderiv_zero_obj";
-val pderiv_zero = thm "pderiv_zero";
-val poly_pderiv_welldef = thm "poly_pderiv_welldef";
-val poly_primes = thm "poly_primes";
-val poly_divides_refl = thm "poly_divides_refl";
-val poly_divides_trans = thm "poly_divides_trans";
-val poly_divides_exp = thm "poly_divides_exp";
-val poly_exp_divides = thm "poly_exp_divides";
-val poly_divides_add = thm "poly_divides_add";
-val poly_divides_diff = thm "poly_divides_diff";
-val poly_divides_diff2 = thm "poly_divides_diff2";
-val poly_divides_zero = thm "poly_divides_zero";
-val poly_divides_zero2 = thm "poly_divides_zero2";
-val poly_order_exists_lemma = thm "poly_order_exists_lemma";
-val poly_order_exists = thm "poly_order_exists";
-val poly_one_divides = thm "poly_one_divides";
-val poly_order = thm "poly_order";
-val some1_equalityD = thm "some1_equalityD";
-val order = thm "order";
-val order2 = thm "order2";
-val order_unique = thm "order_unique";
-val order_unique_lemma = thm "order_unique_lemma";
-val order_poly = thm "order_poly";
-val pexp_one = thm "pexp_one";
-val lemma_order_root = thm "lemma_order_root";
-val order_root = thm "order_root";
-val order_divides = thm "order_divides";
-val order_decomp = thm "order_decomp";
-val order_mult = thm "order_mult";
-val lemma_order_pderiv = thm "lemma_order_pderiv";
-val order_pderiv = thm "order_pderiv";
-val poly_squarefree_decomp_order = thm "poly_squarefree_decomp_order";
-val poly_squarefree_decomp_order2 = thm "poly_squarefree_decomp_order2";
-val order_root2 = thm "order_root2";
-val order_pderiv2 = thm "order_pderiv2";
-val rsquarefree_roots = thm "rsquarefree_roots";
-val pmult_one = thm "pmult_one";
-val poly_Nil_zero = thm "poly_Nil_zero";
-val rsquarefree_decomp = thm "rsquarefree_decomp";
-val poly_squarefree_decomp = thm "poly_squarefree_decomp";
-val poly_normalize = thm "poly_normalize";
-val lemma_degree_zero = thm "lemma_degree_zero";
-val degree_zero = thm "degree_zero";
-val poly_roots_finite_set = thm "poly_roots_finite_set";
-val poly_mono = thm "poly_mono";
-*}
-
end
--- a/src/HOL/Hyperreal/SEQ.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Fri Jun 02 23:22:29 2006 +0200
@@ -12,56 +12,55 @@
imports NatStar
begin
-constdefs
+definition
LIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----> (_))" [60, 60] 60)
--{*Standard definition of convergence of sequence*}
- "X ----> L == (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
+ "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
NSLIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----NS> (_))" [60, 60] 60)
--{*Nonstandard definition of convergence of sequence*}
- "X ----NS> L == (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
+ "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
lim :: "(nat => real) => real"
--{*Standard definition of limit using choice operator*}
- "lim X == (@L. (X ----> L))"
+ "lim X = (SOME L. (X ----> L))"
nslim :: "(nat => real) => real"
--{*Nonstandard definition of limit using choice operator*}
- "nslim X == (@L. (X ----NS> L))"
+ "nslim X = (SOME L. (X ----NS> L))"
convergent :: "(nat => real) => bool"
--{*Standard definition of convergence*}
- "convergent X == (\<exists>L. (X ----> L))"
+ "convergent X = (\<exists>L. (X ----> L))"
NSconvergent :: "(nat => real) => bool"
--{*Nonstandard definition of convergence*}
- "NSconvergent X == (\<exists>L. (X ----NS> L))"
+ "NSconvergent X = (\<exists>L. (X ----NS> L))"
Bseq :: "(nat => real) => bool"
--{*Standard definition for bounded sequence*}
- "Bseq X == \<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K"
+ "Bseq X = (\<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K)"
NSBseq :: "(nat=>real) => bool"
--{*Nonstandard definition for bounded sequence*}
- "NSBseq X == (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
+ "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
monoseq :: "(nat=>real)=>bool"
--{*Definition for monotonicity*}
- "monoseq X == (\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+ "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
subseq :: "(nat => nat) => bool"
--{*Definition of subsequence*}
- "subseq f == \<forall>m. \<forall>n>m. (f m) < (f n)"
+ "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
Cauchy :: "(nat => real) => bool"
--{*Standard definition of the Cauchy condition*}
- "Cauchy X == \<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e"
+ "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e)"
NSCauchy :: "(nat => real) => bool"
--{*Nonstandard definition*}
- "NSCauchy X == (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite.
- ( *f* X) M \<approx> ( *f* X) N)"
+ "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
@@ -1195,125 +1194,4 @@
Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
---------------------------------------------------------------***)
-
-ML
-{*
-val Cauchy_def = thm"Cauchy_def";
-val SEQ_Infinitesimal = thm "SEQ_Infinitesimal";
-val LIMSEQ_iff = thm "LIMSEQ_iff";
-val NSLIMSEQ_iff = thm "NSLIMSEQ_iff";
-val LIMSEQ_NSLIMSEQ = thm "LIMSEQ_NSLIMSEQ";
-val NSLIMSEQ_finite_set = thm "NSLIMSEQ_finite_set";
-val Compl_less_set = thm "Compl_less_set";
-val FreeUltrafilterNat_NSLIMSEQ = thm "FreeUltrafilterNat_NSLIMSEQ";
-val HNatInfinite_NSLIMSEQ = thm "HNatInfinite_NSLIMSEQ";
-val NSLIMSEQ_LIMSEQ = thm "NSLIMSEQ_LIMSEQ";
-val LIMSEQ_NSLIMSEQ_iff = thm "LIMSEQ_NSLIMSEQ_iff";
-val NSLIMSEQ_const = thm "NSLIMSEQ_const";
-val LIMSEQ_const = thm "LIMSEQ_const";
-val NSLIMSEQ_add = thm "NSLIMSEQ_add";
-val LIMSEQ_add = thm "LIMSEQ_add";
-val NSLIMSEQ_mult = thm "NSLIMSEQ_mult";
-val LIMSEQ_mult = thm "LIMSEQ_mult";
-val NSLIMSEQ_minus = thm "NSLIMSEQ_minus";
-val LIMSEQ_minus = thm "LIMSEQ_minus";
-val LIMSEQ_minus_cancel = thm "LIMSEQ_minus_cancel";
-val NSLIMSEQ_minus_cancel = thm "NSLIMSEQ_minus_cancel";
-val NSLIMSEQ_add_minus = thm "NSLIMSEQ_add_minus";
-val LIMSEQ_add_minus = thm "LIMSEQ_add_minus";
-val LIMSEQ_diff = thm "LIMSEQ_diff";
-val NSLIMSEQ_diff = thm "NSLIMSEQ_diff";
-val NSLIMSEQ_inverse = thm "NSLIMSEQ_inverse";
-val LIMSEQ_inverse = thm "LIMSEQ_inverse";
-val NSLIMSEQ_mult_inverse = thm "NSLIMSEQ_mult_inverse";
-val LIMSEQ_divide = thm "LIMSEQ_divide";
-val NSLIMSEQ_unique = thm "NSLIMSEQ_unique";
-val LIMSEQ_unique = thm "LIMSEQ_unique";
-val limI = thm "limI";
-val nslimI = thm "nslimI";
-val lim_nslim_iff = thm "lim_nslim_iff";
-val convergentD = thm "convergentD";
-val convergentI = thm "convergentI";
-val NSconvergentD = thm "NSconvergentD";
-val NSconvergentI = thm "NSconvergentI";
-val convergent_NSconvergent_iff = thm "convergent_NSconvergent_iff";
-val NSconvergent_NSLIMSEQ_iff = thm "NSconvergent_NSLIMSEQ_iff";
-val convergent_LIMSEQ_iff = thm "convergent_LIMSEQ_iff";
-val subseq_Suc_iff = thm "subseq_Suc_iff";
-val monoseq_Suc = thm "monoseq_Suc";
-val monoI1 = thm "monoI1";
-val monoI2 = thm "monoI2";
-val mono_SucI1 = thm "mono_SucI1";
-val mono_SucI2 = thm "mono_SucI2";
-val BseqD = thm "BseqD";
-val BseqI = thm "BseqI";
-val Bseq_iff = thm "Bseq_iff";
-val Bseq_iff1a = thm "Bseq_iff1a";
-val NSBseqD = thm "NSBseqD";
-val NSBseqI = thm "NSBseqI";
-val Bseq_NSBseq = thm "Bseq_NSBseq";
-val real_seq_to_hypreal_HInfinite = thm "real_seq_to_hypreal_HInfinite";
-val HNatInfinite_skolem_f = thm "HNatInfinite_skolem_f";
-val NSBseq_Bseq = thm "NSBseq_Bseq";
-val Bseq_NSBseq_iff = thm "Bseq_NSBseq_iff";
-val NSconvergent_NSBseq = thm "NSconvergent_NSBseq";
-val convergent_Bseq = thm "convergent_Bseq";
-val Bseq_isUb = thm "Bseq_isUb";
-val Bseq_isLub = thm "Bseq_isLub";
-val NSBseq_isUb = thm "NSBseq_isUb";
-val NSBseq_isLub = thm "NSBseq_isLub";
-val Bmonoseq_LIMSEQ = thm "Bmonoseq_LIMSEQ";
-val Bmonoseq_NSLIMSEQ = thm "Bmonoseq_NSLIMSEQ";
-val Bseq_mono_convergent = thm "Bseq_mono_convergent";
-val NSBseq_mono_NSconvergent = thm "NSBseq_mono_NSconvergent";
-val convergent_minus_iff = thm "convergent_minus_iff";
-val Bseq_minus_iff = thm "Bseq_minus_iff";
-val Bseq_monoseq_convergent = thm "Bseq_monoseq_convergent";
-val Bseq_iff2 = thm "Bseq_iff2";
-val Bseq_iff3 = thm "Bseq_iff3";
-val BseqI2 = thm "BseqI2";
-val Cauchy_NSCauchy = thm "Cauchy_NSCauchy";
-val NSCauchy_Cauchy = thm "NSCauchy_Cauchy";
-val NSCauchy_Cauchy_iff = thm "NSCauchy_Cauchy_iff";
-val less_Suc_cancel_iff = thm "less_Suc_cancel_iff";
-val SUP_rabs_subseq = thm "SUP_rabs_subseq";
-val Cauchy_Bseq = thm "Cauchy_Bseq";
-val NSCauchy_NSBseq = thm "NSCauchy_NSBseq";
-val NSCauchy_NSconvergent_iff = thm "NSCauchy_NSconvergent_iff";
-val Cauchy_convergent_iff = thm "Cauchy_convergent_iff";
-val NSLIMSEQ_le = thm "NSLIMSEQ_le";
-val LIMSEQ_le = thm "LIMSEQ_le";
-val LIMSEQ_le_const = thm "LIMSEQ_le_const";
-val NSLIMSEQ_le_const = thm "NSLIMSEQ_le_const";
-val LIMSEQ_le_const2 = thm "LIMSEQ_le_const2";
-val NSLIMSEQ_le_const2 = thm "NSLIMSEQ_le_const2";
-val NSLIMSEQ_Suc = thm "NSLIMSEQ_Suc";
-val LIMSEQ_Suc = thm "LIMSEQ_Suc";
-val NSLIMSEQ_imp_Suc = thm "NSLIMSEQ_imp_Suc";
-val LIMSEQ_imp_Suc = thm "LIMSEQ_imp_Suc";
-val LIMSEQ_Suc_iff = thm "LIMSEQ_Suc_iff";
-val NSLIMSEQ_Suc_iff = thm "NSLIMSEQ_Suc_iff";
-val LIMSEQ_rabs_zero = thm "LIMSEQ_rabs_zero";
-val NSLIMSEQ_rabs_zero = thm "NSLIMSEQ_rabs_zero";
-val NSLIMSEQ_imp_rabs = thm "NSLIMSEQ_imp_rabs";
-val LIMSEQ_imp_rabs = thm "LIMSEQ_imp_rabs";
-val LIMSEQ_inverse_zero = thm "LIMSEQ_inverse_zero";
-val NSLIMSEQ_inverse_zero = thm "NSLIMSEQ_inverse_zero";
-val LIMSEQ_inverse_real_of_nat = thm "LIMSEQ_inverse_real_of_nat";
-val NSLIMSEQ_inverse_real_of_nat = thm "NSLIMSEQ_inverse_real_of_nat";
-val LIMSEQ_inverse_real_of_nat_add = thm "LIMSEQ_inverse_real_of_nat_add";
-val NSLIMSEQ_inverse_real_of_nat_add = thm "NSLIMSEQ_inverse_real_of_nat_add";
-val LIMSEQ_inverse_real_of_nat_add_minus = thm "LIMSEQ_inverse_real_of_nat_add_minus";
-val NSLIMSEQ_inverse_real_of_nat_add_minus = thm "NSLIMSEQ_inverse_real_of_nat_add_minus";
-val LIMSEQ_inverse_real_of_nat_add_minus_mult = thm "LIMSEQ_inverse_real_of_nat_add_minus_mult";
-val NSLIMSEQ_inverse_real_of_nat_add_minus_mult = thm "NSLIMSEQ_inverse_real_of_nat_add_minus_mult";
-val NSLIMSEQ_pow = thm "NSLIMSEQ_pow";
-val LIMSEQ_pow = thm "LIMSEQ_pow";
-val Bseq_realpow = thm "Bseq_realpow";
-val monoseq_realpow = thm "monoseq_realpow";
-val convergent_realpow = thm "convergent_realpow";
-val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero";
-*}
-
-
end
--- a/src/HOL/Hyperreal/Series.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy Fri Jun 02 23:22:29 2006 +0200
@@ -16,15 +16,15 @@
declare atLeastLessThan_iff[iff]
declare setsum_op_ivl_Suc[simp]
-constdefs
+definition
sums :: "(nat => real) => real => bool" (infixr "sums" 80)
- "f sums s == (%n. setsum f {0..<n}) ----> s"
+ "f sums s = (%n. setsum f {0..<n}) ----> s"
summable :: "(nat=>real) => bool"
- "summable f == (\<exists>s. f sums s)"
+ "summable f = (\<exists>s. f sums s)"
suminf :: "(nat=>real) => real"
- "suminf f == SOME s. f sums s"
+ "suminf f = (SOME s. f sums s)"
syntax
"_suminf" :: "idt => real => real" ("\<Sum>_. _" [0, 10] 10)
@@ -500,48 +500,4 @@
apply (auto intro: DERIV_add)
done
-ML
-{*
-val sums_def = thm"sums_def";
-val summable_def = thm"summable_def";
-val suminf_def = thm"suminf_def";
-
-val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
-val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero";
-val sumr_group = thm "sumr_group";
-val sums_summable = thm "sums_summable";
-val summable_sums = thm "summable_sums";
-val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf";
-val sums_unique = thm "sums_unique";
-val series_zero = thm "series_zero";
-val sums_mult = thm "sums_mult";
-val sums_divide = thm "sums_divide";
-val sums_diff = thm "sums_diff";
-val suminf_mult = thm "suminf_mult";
-val suminf_mult2 = thm "suminf_mult2";
-val suminf_diff = thm "suminf_diff";
-val sums_minus = thm "sums_minus";
-val sums_group = thm "sums_group";
-val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma";
-val sumr_pos_lt_pair = thm "sumr_pos_lt_pair";
-val series_pos_le = thm "series_pos_le";
-val series_pos_less = thm "series_pos_less";
-val sumr_geometric = thm "sumr_geometric";
-val geometric_sums = thm "geometric_sums";
-val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff";
-val summable_Cauchy = thm "summable_Cauchy";
-val summable_comparison_test = thm "summable_comparison_test";
-val summable_rabs_comparison_test = thm "summable_rabs_comparison_test";
-val summable_le = thm "summable_le";
-val summable_le2 = thm "summable_le2";
-val summable_rabs_cancel = thm "summable_rabs_cancel";
-val summable_rabs = thm "summable_rabs";
-val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma";
-val le_Suc_ex = thm "le_Suc_ex";
-val le_Suc_ex_iff = thm "le_Suc_ex_iff";
-val ratio_test_lemma2 = thm "ratio_test_lemma2";
-val ratio_test = thm "ratio_test";
-val DERIV_sumr = thm "DERIV_sumr";
-*}
-
end
--- a/src/HOL/Hyperreal/Star.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Star.thy Fri Jun 02 23:22:29 2006 +0200
@@ -10,26 +10,24 @@
imports NSA
begin
-constdefs
+definition
(* internal sets *)
- starset_n :: "(nat => 'a set) => 'a star set" ("*sn* _" [80] 80)
- "*sn* As == Iset (star_n As)"
+ starset_n :: "(nat => 'a set) => 'a star set" ("*sn* _" [80] 80)
+ "*sn* As = Iset (star_n As)"
- InternalSets :: "'a star set set"
- "InternalSets == {X. \<exists>As. X = *sn* As}"
+ InternalSets :: "'a star set set"
+ "InternalSets = {X. \<exists>As. X = *sn* As}"
- (* nonstandard extension of function *)
- is_starext :: "['a star => 'a star, 'a => 'a] => bool"
- "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
+ (* nonstandard extension of function *)
+ is_starext :: "['a star => 'a star, 'a => 'a] => bool"
+ "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
- (* internal functions *)
- starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star"
- ("*fn* _" [80] 80)
- "*fn* F == Ifun (star_n F)"
+ (* internal functions *)
+ starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star" ("*fn* _" [80] 80)
+ "*fn* F = Ifun (star_n F)"
- InternalFuns :: "('a star => 'b star) set"
- "InternalFuns == {X. \<exists>F. X = *fn* F}"
-
+ InternalFuns :: "('a star => 'b star) set"
+ "InternalFuns = {X. \<exists>F. X = *fn* F}"
(*--------------------------------------------------------
@@ -353,66 +351,4 @@
apply (auto simp add: starfun star_n_eq_iff)
done
-ML
-{*
-val starset_n_def = thm"starset_n_def";
-val InternalSets_def = thm"InternalSets_def";
-val is_starext_def = thm"is_starext_def";
-val starfun_n_def = thm"starfun_n_def";
-val InternalFuns_def = thm"InternalFuns_def";
-
-val no_choice = thm "no_choice";
-val STAR_UNIV_set = thm "STAR_UNIV_set";
-val STAR_empty_set = thm "STAR_empty_set";
-val STAR_Un = thm "STAR_Un";
-val STAR_Int = thm "STAR_Int";
-val STAR_Compl = thm "STAR_Compl";
-val STAR_mem_Compl = thm "STAR_mem_Compl";
-val STAR_diff = thm "STAR_diff";
-val STAR_subset = thm "STAR_subset";
-val STAR_mem = thm "STAR_mem";
-val STAR_star_of_image_subset = thm "STAR_star_of_image_subset";
-val STAR_hypreal_of_real_Int = thm "STAR_hypreal_of_real_Int";
-val STAR_real_seq_to_hypreal = thm "STAR_real_seq_to_hypreal";
-val STAR_singleton = thm "STAR_singleton";
-val STAR_not_mem = thm "STAR_not_mem";
-val STAR_subset_closed = thm "STAR_subset_closed";
-val starset_n_starset = thm "starset_n_starset";
-val starfun_n_starfun = thm "starfun_n_starfun";
-val hrabs_is_starext_rabs = thm "hrabs_is_starext_rabs";
-val Rep_star_FreeUltrafilterNat = thm "Rep_star_FreeUltrafilterNat";
-val starfun = thm "starfun";
-val starfun_mult = thm "starfun_mult";
-val starfun_add = thm "starfun_add";
-val starfun_minus = thm "starfun_minus";
-val starfun_add_minus = thm "starfun_add_minus";
-val starfun_diff = thm "starfun_diff";
-val starfun_o2 = thm "starfun_o2";
-val starfun_o = thm "starfun_o";
-val starfun_const_fun = thm "starfun_const_fun";
-val starfun_Idfun_approx = thm "starfun_Idfun_approx";
-val starfun_Id = thm "starfun_Id";
-val is_starext_starfun = thm "is_starext_starfun";
-val is_starfun_starext = thm "is_starfun_starext";
-val is_starext_starfun_iff = thm "is_starext_starfun_iff";
-val starfun_eq = thm "starfun_eq";
-val starfun_approx = thm "starfun_approx";
-val starfun_lambda_cancel = thm "starfun_lambda_cancel";
-val starfun_lambda_cancel2 = thm "starfun_lambda_cancel2";
-val starfun_mult_HFinite_approx = thm "starfun_mult_HFinite_approx";
-val starfun_add_approx = thm "starfun_add_approx";
-val starfun_rabs_hrabs = thm "starfun_rabs_hrabs";
-val starfun_inverse_inverse = thm "starfun_inverse_inverse";
-val starfun_inverse = thm "starfun_inverse";
-val starfun_divide = thm "starfun_divide";
-val starfun_inverse2 = thm "starfun_inverse2";
-val starfun_mem_starset = thm "starfun_mem_starset";
-val hypreal_hrabs = thm "hypreal_hrabs";
-val STAR_rabs_add_minus = thm "STAR_rabs_add_minus";
-val STAR_starfun_rabs_add_minus = thm "STAR_starfun_rabs_add_minus";
-val Infinitesimal_FreeUltrafilterNat_iff2 = thm "Infinitesimal_FreeUltrafilterNat_iff2";
-val approx_FreeUltrafilterNat_iff = thm "approx_FreeUltrafilterNat_iff";
-val inj_starfun = thm "inj_starfun";
-*}
-
end
--- a/src/HOL/Hyperreal/StarDef.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/StarDef.thy Fri Jun 02 23:22:29 2006 +0200
@@ -12,19 +12,19 @@
subsection {* A Free Ultrafilter over the Naturals *}
-constdefs
+definition
FreeUltrafilterNat :: "nat set set" ("\<U>")
- "\<U> \<equiv> SOME U. freeultrafilter U"
+ "\<U> = (SOME U. freeultrafilter U)"
lemma freeultrafilter_FUFNat: "freeultrafilter \<U>"
apply (unfold FreeUltrafilterNat_def)
apply (rule someI_ex)
apply (rule freeultrafilter_Ex)
apply (rule nat_infinite)
-done
+ done
interpretation FUFNat: freeultrafilter [FreeUltrafilterNat]
-by (cut_tac [!] freeultrafilter_FUFNat, simp_all add: freeultrafilter_def)
+ using freeultrafilter_FUFNat by (simp_all add: freeultrafilter_def)
text {* This rule takes the place of the old ultra tactic *}
@@ -35,16 +35,16 @@
subsection {* Definition of @{text star} type constructor *}
-constdefs
+definition
starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set"
- "starrel \<equiv> {(X,Y). {n. X n = Y n} \<in> \<U>}"
+ "starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
by (auto intro: quotientI)
-constdefs
+definition
star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star"
- "star_n X \<equiv> Abs_star (starrel `` {X})"
+ "star_n X = Abs_star (starrel `` {X})"
theorem star_cases [case_names star_n, cases type: star]:
"(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P"
@@ -156,9 +156,9 @@
subsection {* Standard elements *}
-constdefs
+definition
star_of :: "'a \<Rightarrow> 'a star"
- "star_of x \<equiv> star_n (\<lambda>n. x)"
+ "star_of x == star_n (\<lambda>n. x)"
text {* Transfer tactic should remove occurrences of @{term star_of} *}
setup {* Transfer.add_const "StarDef.star_of" *}
@@ -170,7 +170,7 @@
subsection {* Internal functions *}
-constdefs
+definition
Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300)
"Ifun f \<equiv> \<lambda>x. Abs_star
(\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
@@ -195,14 +195,14 @@
text {* Nonstandard extensions of functions *}
-constdefs
+definition
starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)"
("*f* _" [80] 80)
- "starfun f \<equiv> \<lambda>x. star_of f \<star> x"
+ "starfun f == \<lambda>x. star_of f \<star> x"
starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
("*f2* _" [80] 80)
- "starfun2 f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y"
+ "starfun2 f == \<lambda>x y. star_of f \<star> x \<star> y"
declare starfun_def [transfer_unfold]
declare starfun2_def [transfer_unfold]
@@ -223,9 +223,9 @@
subsection {* Internal predicates *}
-constdefs
+definition
unstar :: "bool star \<Rightarrow> bool"
- "unstar b \<equiv> b = star_of True"
+ "unstar b = (b = star_of True)"
lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
by (simp add: unstar_def star_of_def star_n_eq_iff)
@@ -240,14 +240,14 @@
"p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
by (simp only: unstar_star_n)
-constdefs
+definition
starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool"
("*p* _" [80] 80)
- "*p* P \<equiv> \<lambda>x. unstar (star_of P \<star> x)"
+ "*p* P = (\<lambda>x. unstar (star_of P \<star> x))"
starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool"
("*p2* _" [80] 80)
- "*p2* P \<equiv> \<lambda>x y. unstar (star_of P \<star> x \<star> y)"
+ "*p2* P = (\<lambda>x y. unstar (star_of P \<star> x \<star> y))"
declare starP_def [transfer_unfold]
declare starP2_def [transfer_unfold]
@@ -268,9 +268,9 @@
subsection {* Internal sets *}
-constdefs
+definition
Iset :: "'a set star \<Rightarrow> 'a star set"
- "Iset A \<equiv> {x. ( *p2* op \<in>) x A}"
+ "Iset A = {x. ( *p2* op \<in>) x A}"
lemma Iset_star_n:
"(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
@@ -309,9 +309,10 @@
by simp
text {* Nonstandard extensions of sets. *}
-constdefs
+
+definition
starset :: "'a set \<Rightarrow> 'a star set" ("*s* _" [80] 80)
- "starset A \<equiv> Iset (star_of A)"
+ "starset A = Iset (star_of A)"
declare starset_def [transfer_unfold]
--- a/src/HOL/Hyperreal/Transcendental.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Fri Jun 02 23:22:29 2006 +0200
@@ -11,44 +11,44 @@
imports NthRoot Fact HSeries EvenOdd Lim
begin
-constdefs
- root :: "[nat,real] => real"
- "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
-
- sqrt :: "real => real"
- "sqrt x == root 2 x"
-
- exp :: "real => real"
- "exp x == \<Sum>n. inverse(real (fact n)) * (x ^ n)"
-
- sin :: "real => real"
- "sin x == \<Sum>n. (if even(n) then 0 else
- ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n"
+definition
+ root :: "[nat,real] => real"
+ "root n x = (SOME u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
+
+ sqrt :: "real => real"
+ "sqrt x = root 2 x"
+
+ exp :: "real => real"
+ "exp x = (\<Sum>n. inverse(real (fact n)) * (x ^ n))"
+
+ sin :: "real => real"
+ "sin x = (\<Sum>n. (if even(n) then 0 else
+ ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
- diffs :: "(nat => real) => nat => real"
- "diffs c == (%n. real (Suc n) * c(Suc n))"
-
- cos :: "real => real"
- "cos x == \<Sum>n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n))
- else 0) * x ^ n"
+ diffs :: "(nat => real) => nat => real"
+ "diffs c = (%n. real (Suc n) * c(Suc n))"
+
+ cos :: "real => real"
+ "cos x = (\<Sum>n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n))
+ else 0) * x ^ n)"
- ln :: "real => real"
- "ln x == (@u. exp u = x)"
-
- pi :: "real"
- "pi == 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
-
- tan :: "real => real"
- "tan x == (sin x)/(cos x)"
-
- arcsin :: "real => real"
- "arcsin y == (@x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
-
- arcos :: "real => real"
- "arcos y == (@x. 0 \<le> x & x \<le> pi & cos x = y)"
+ ln :: "real => real"
+ "ln x = (SOME u. exp u = x)"
+
+ pi :: "real"
+ "pi = 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
+
+ tan :: "real => real"
+ "tan x = (sin x)/(cos x)"
+
+ arcsin :: "real => real"
+ "arcsin y = (SOME x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
+
+ arcos :: "real => real"
+ "arcos y = (SOME x. 0 \<le> x & x \<le> pi & cos x = y)"
- arctan :: "real => real"
- "arctan y == (@x. -(pi/2) < x & x < pi/2 & tan x = y)"
+ arctan :: "real => real"
+ "arctan y = (SOME x. -(pi/2) < x & x < pi/2 & tan x = y)"
lemma real_root_zero [simp]: "root (Suc n) 0 = 0"
@@ -2578,298 +2578,5 @@
apply (drule_tac [3] LIM_fun_gt_zero)
apply force+
done
-
-ML
-{*
-val inverse_unique = thm "inverse_unique";
-val real_root_zero = thm "real_root_zero";
-val real_root_pow_pos = thm "real_root_pow_pos";
-val real_root_pow_pos2 = thm "real_root_pow_pos2";
-val real_root_pos = thm "real_root_pos";
-val real_root_pos2 = thm "real_root_pos2";
-val real_root_pos_pos = thm "real_root_pos_pos";
-val real_root_pos_pos_le = thm "real_root_pos_pos_le";
-val real_root_one = thm "real_root_one";
-val root_2_eq = thm "root_2_eq";
-val real_sqrt_zero = thm "real_sqrt_zero";
-val real_sqrt_one = thm "real_sqrt_one";
-val real_sqrt_pow2_iff = thm "real_sqrt_pow2_iff";
-val real_sqrt_pow2 = thm "real_sqrt_pow2";
-val real_sqrt_abs_abs = thm "real_sqrt_abs_abs";
-val real_pow_sqrt_eq_sqrt_pow = thm "real_pow_sqrt_eq_sqrt_pow";
-val real_pow_sqrt_eq_sqrt_abs_pow2 = thm "real_pow_sqrt_eq_sqrt_abs_pow2";
-val real_sqrt_pow_abs = thm "real_sqrt_pow_abs";
-val not_real_square_gt_zero = thm "not_real_square_gt_zero";
-val real_sqrt_gt_zero = thm "real_sqrt_gt_zero";
-val real_sqrt_ge_zero = thm "real_sqrt_ge_zero";
-val sqrt_eqI = thm "sqrt_eqI";
-val real_sqrt_mult_distrib = thm "real_sqrt_mult_distrib";
-val real_sqrt_mult_distrib2 = thm "real_sqrt_mult_distrib2";
-val real_sqrt_sum_squares_ge_zero = thm "real_sqrt_sum_squares_ge_zero";
-val real_sqrt_sum_squares_mult_ge_zero = thm "real_sqrt_sum_squares_mult_ge_zero";
-val real_sqrt_sum_squares_mult_squared_eq = thm "real_sqrt_sum_squares_mult_squared_eq";
-val real_sqrt_abs = thm "real_sqrt_abs";
-val real_sqrt_abs2 = thm "real_sqrt_abs2";
-val real_sqrt_pow2_gt_zero = thm "real_sqrt_pow2_gt_zero";
-val real_sqrt_not_eq_zero = thm "real_sqrt_not_eq_zero";
-val real_inv_sqrt_pow2 = thm "real_inv_sqrt_pow2";
-val real_sqrt_eq_zero_cancel = thm "real_sqrt_eq_zero_cancel";
-val real_sqrt_eq_zero_cancel_iff = thm "real_sqrt_eq_zero_cancel_iff";
-val real_sqrt_sum_squares_ge1 = thm "real_sqrt_sum_squares_ge1";
-val real_sqrt_sum_squares_ge2 = thm "real_sqrt_sum_squares_ge2";
-val real_sqrt_ge_one = thm "real_sqrt_ge_one";
-val summable_exp = thm "summable_exp";
-val summable_sin = thm "summable_sin";
-val summable_cos = thm "summable_cos";
-val exp_converges = thm "exp_converges";
-val sin_converges = thm "sin_converges";
-val cos_converges = thm "cos_converges";
-val powser_insidea = thm "powser_insidea";
-val powser_inside = thm "powser_inside";
-val diffs_minus = thm "diffs_minus";
-val diffs_equiv = thm "diffs_equiv";
-val less_add_one = thm "less_add_one";
-val termdiffs_aux = thm "termdiffs_aux";
-val termdiffs = thm "termdiffs";
-val exp_fdiffs = thm "exp_fdiffs";
-val sin_fdiffs = thm "sin_fdiffs";
-val sin_fdiffs2 = thm "sin_fdiffs2";
-val cos_fdiffs = thm "cos_fdiffs";
-val cos_fdiffs2 = thm "cos_fdiffs2";
-val DERIV_exp = thm "DERIV_exp";
-val DERIV_sin = thm "DERIV_sin";
-val DERIV_cos = thm "DERIV_cos";
-val exp_zero = thm "exp_zero";
-(* val exp_ge_add_one_self = thm "exp_ge_add_one_self"; *)
-val exp_gt_one = thm "exp_gt_one";
-val DERIV_exp_add_const = thm "DERIV_exp_add_const";
-val DERIV_exp_minus = thm "DERIV_exp_minus";
-val DERIV_exp_exp_zero = thm "DERIV_exp_exp_zero";
-val exp_add_mult_minus = thm "exp_add_mult_minus";
-val exp_mult_minus = thm "exp_mult_minus";
-val exp_mult_minus2 = thm "exp_mult_minus2";
-val exp_minus = thm "exp_minus";
-val exp_add = thm "exp_add";
-val exp_ge_zero = thm "exp_ge_zero";
-val exp_not_eq_zero = thm "exp_not_eq_zero";
-val exp_gt_zero = thm "exp_gt_zero";
-val inv_exp_gt_zero = thm "inv_exp_gt_zero";
-val abs_exp_cancel = thm "abs_exp_cancel";
-val exp_real_of_nat_mult = thm "exp_real_of_nat_mult";
-val exp_diff = thm "exp_diff";
-val exp_less_mono = thm "exp_less_mono";
-val exp_less_cancel = thm "exp_less_cancel";
-val exp_less_cancel_iff = thm "exp_less_cancel_iff";
-val exp_le_cancel_iff = thm "exp_le_cancel_iff";
-val exp_inj_iff = thm "exp_inj_iff";
-val exp_total = thm "exp_total";
-val ln_exp = thm "ln_exp";
-val exp_ln_iff = thm "exp_ln_iff";
-val ln_mult = thm "ln_mult";
-val ln_inj_iff = thm "ln_inj_iff";
-val ln_one = thm "ln_one";
-val ln_inverse = thm "ln_inverse";
-val ln_div = thm "ln_div";
-val ln_less_cancel_iff = thm "ln_less_cancel_iff";
-val ln_le_cancel_iff = thm "ln_le_cancel_iff";
-val ln_realpow = thm "ln_realpow";
-val ln_add_one_self_le_self = thm "ln_add_one_self_le_self";
-val ln_less_self = thm "ln_less_self";
-val ln_ge_zero = thm "ln_ge_zero";
-val ln_gt_zero = thm "ln_gt_zero";
-val ln_less_zero = thm "ln_less_zero";
-val exp_ln_eq = thm "exp_ln_eq";
-val sin_zero = thm "sin_zero";
-val cos_zero = thm "cos_zero";
-val DERIV_sin_sin_mult = thm "DERIV_sin_sin_mult";
-val DERIV_sin_sin_mult2 = thm "DERIV_sin_sin_mult2";
-val DERIV_sin_realpow2 = thm "DERIV_sin_realpow2";
-val DERIV_sin_realpow2a = thm "DERIV_sin_realpow2a";
-val DERIV_cos_cos_mult = thm "DERIV_cos_cos_mult";
-val DERIV_cos_cos_mult2 = thm "DERIV_cos_cos_mult2";
-val DERIV_cos_realpow2 = thm "DERIV_cos_realpow2";
-val DERIV_cos_realpow2a = thm "DERIV_cos_realpow2a";
-val DERIV_cos_realpow2b = thm "DERIV_cos_realpow2b";
-val DERIV_cos_cos_mult3 = thm "DERIV_cos_cos_mult3";
-val DERIV_sin_circle_all = thm "DERIV_sin_circle_all";
-val DERIV_sin_circle_all_zero = thm "DERIV_sin_circle_all_zero";
-val sin_cos_squared_add = thm "sin_cos_squared_add";
-val sin_cos_squared_add2 = thm "sin_cos_squared_add2";
-val sin_cos_squared_add3 = thm "sin_cos_squared_add3";
-val sin_squared_eq = thm "sin_squared_eq";
-val cos_squared_eq = thm "cos_squared_eq";
-val real_gt_one_ge_zero_add_less = thm "real_gt_one_ge_zero_add_less";
-val abs_sin_le_one = thm "abs_sin_le_one";
-val sin_ge_minus_one = thm "sin_ge_minus_one";
-val sin_le_one = thm "sin_le_one";
-val abs_cos_le_one = thm "abs_cos_le_one";
-val cos_ge_minus_one = thm "cos_ge_minus_one";
-val cos_le_one = thm "cos_le_one";
-val DERIV_fun_pow = thm "DERIV_fun_pow";
-val DERIV_fun_exp = thm "DERIV_fun_exp";
-val DERIV_fun_sin = thm "DERIV_fun_sin";
-val DERIV_fun_cos = thm "DERIV_fun_cos";
-val DERIV_intros = thms "DERIV_intros";
-val sin_cos_add = thm "sin_cos_add";
-val sin_add = thm "sin_add";
-val cos_add = thm "cos_add";
-val sin_cos_minus = thm "sin_cos_minus";
-val sin_minus = thm "sin_minus";
-val cos_minus = thm "cos_minus";
-val sin_diff = thm "sin_diff";
-val sin_diff2 = thm "sin_diff2";
-val cos_diff = thm "cos_diff";
-val cos_diff2 = thm "cos_diff2";
-val sin_double = thm "sin_double";
-val cos_double = thm "cos_double";
-val sin_paired = thm "sin_paired";
-val sin_gt_zero = thm "sin_gt_zero";
-val sin_gt_zero1 = thm "sin_gt_zero1";
-val cos_double_less_one = thm "cos_double_less_one";
-val cos_paired = thm "cos_paired";
-val cos_two_less_zero = thm "cos_two_less_zero";
-val cos_is_zero = thm "cos_is_zero";
-val pi_half = thm "pi_half";
-val cos_pi_half = thm "cos_pi_half";
-val pi_half_gt_zero = thm "pi_half_gt_zero";
-val pi_half_less_two = thm "pi_half_less_two";
-val pi_gt_zero = thm "pi_gt_zero";
-val pi_neq_zero = thm "pi_neq_zero";
-val pi_not_less_zero = thm "pi_not_less_zero";
-val pi_ge_zero = thm "pi_ge_zero";
-val minus_pi_half_less_zero = thm "minus_pi_half_less_zero";
-val sin_pi_half = thm "sin_pi_half";
-val cos_pi = thm "cos_pi";
-val sin_pi = thm "sin_pi";
-val sin_cos_eq = thm "sin_cos_eq";
-val minus_sin_cos_eq = thm "minus_sin_cos_eq";
-val cos_sin_eq = thm "cos_sin_eq";
-val sin_periodic_pi = thm "sin_periodic_pi";
-val sin_periodic_pi2 = thm "sin_periodic_pi2";
-val cos_periodic_pi = thm "cos_periodic_pi";
-val sin_periodic = thm "sin_periodic";
-val cos_periodic = thm "cos_periodic";
-val cos_npi = thm "cos_npi";
-val sin_npi = thm "sin_npi";
-val sin_npi2 = thm "sin_npi2";
-val cos_two_pi = thm "cos_two_pi";
-val sin_two_pi = thm "sin_two_pi";
-val sin_gt_zero2 = thm "sin_gt_zero2";
-val sin_less_zero = thm "sin_less_zero";
-val pi_less_4 = thm "pi_less_4";
-val cos_gt_zero = thm "cos_gt_zero";
-val cos_gt_zero_pi = thm "cos_gt_zero_pi";
-val cos_ge_zero = thm "cos_ge_zero";
-val sin_gt_zero_pi = thm "sin_gt_zero_pi";
-val sin_ge_zero = thm "sin_ge_zero";
-val cos_total = thm "cos_total";
-val sin_total = thm "sin_total";
-val reals_Archimedean4 = thm "reals_Archimedean4";
-val cos_zero_lemma = thm "cos_zero_lemma";
-val sin_zero_lemma = thm "sin_zero_lemma";
-val cos_zero_iff = thm "cos_zero_iff";
-val sin_zero_iff = thm "sin_zero_iff";
-val tan_zero = thm "tan_zero";
-val tan_pi = thm "tan_pi";
-val tan_npi = thm "tan_npi";
-val tan_minus = thm "tan_minus";
-val tan_periodic = thm "tan_periodic";
-val add_tan_eq = thm "add_tan_eq";
-val tan_add = thm "tan_add";
-val tan_double = thm "tan_double";
-val tan_gt_zero = thm "tan_gt_zero";
-val tan_less_zero = thm "tan_less_zero";
-val DERIV_tan = thm "DERIV_tan";
-val LIM_cos_div_sin = thm "LIM_cos_div_sin";
-val tan_total_pos = thm "tan_total_pos";
-val tan_total = thm "tan_total";
-val arcsin_pi = thm "arcsin_pi";
-val arcsin = thm "arcsin";
-val sin_arcsin = thm "sin_arcsin";
-val arcsin_bounded = thm "arcsin_bounded";
-val arcsin_lbound = thm "arcsin_lbound";
-val arcsin_ubound = thm "arcsin_ubound";
-val arcsin_lt_bounded = thm "arcsin_lt_bounded";
-val arcsin_sin = thm "arcsin_sin";
-val arcos = thm "arcos";
-val cos_arcos = thm "cos_arcos";
-val arcos_bounded = thm "arcos_bounded";
-val arcos_lbound = thm "arcos_lbound";
-val arcos_ubound = thm "arcos_ubound";
-val arcos_lt_bounded = thm "arcos_lt_bounded";
-val arcos_cos = thm "arcos_cos";
-val arcos_cos2 = thm "arcos_cos2";
-val arctan = thm "arctan";
-val tan_arctan = thm "tan_arctan";
-val arctan_bounded = thm "arctan_bounded";
-val arctan_lbound = thm "arctan_lbound";
-val arctan_ubound = thm "arctan_ubound";
-val arctan_tan = thm "arctan_tan";
-val arctan_zero_zero = thm "arctan_zero_zero";
-val cos_arctan_not_zero = thm "cos_arctan_not_zero";
-val tan_sec = thm "tan_sec";
-val DERIV_sin_add = thm "DERIV_sin_add";
-val cos_2npi = thm "cos_2npi";
-val cos_3over2_pi = thm "cos_3over2_pi";
-val sin_2npi = thm "sin_2npi";
-val sin_3over2_pi = thm "sin_3over2_pi";
-val cos_pi_eq_zero = thm "cos_pi_eq_zero";
-val DERIV_cos_add = thm "DERIV_cos_add";
-val isCont_cos = thm "isCont_cos";
-val isCont_sin = thm "isCont_sin";
-val isCont_exp = thm "isCont_exp";
-val sin_zero_abs_cos_one = thm "sin_zero_abs_cos_one";
-val exp_eq_one_iff = thm "exp_eq_one_iff";
-val cos_one_sin_zero = thm "cos_one_sin_zero";
-val real_root_less_mono = thm "real_root_less_mono";
-val real_root_le_mono = thm "real_root_le_mono";
-val real_root_less_iff = thm "real_root_less_iff";
-val real_root_le_iff = thm "real_root_le_iff";
-val real_root_eq_iff = thm "real_root_eq_iff";
-val real_root_pos_unique = thm "real_root_pos_unique";
-val real_root_mult = thm "real_root_mult";
-val real_root_inverse = thm "real_root_inverse";
-val real_root_divide = thm "real_root_divide";
-val real_sqrt_less_mono = thm "real_sqrt_less_mono";
-val real_sqrt_le_mono = thm "real_sqrt_le_mono";
-val real_sqrt_less_iff = thm "real_sqrt_less_iff";
-val real_sqrt_le_iff = thm "real_sqrt_le_iff";
-val real_sqrt_eq_iff = thm "real_sqrt_eq_iff";
-val real_sqrt_sos_less_one_iff = thm "real_sqrt_sos_less_one_iff";
-val real_sqrt_sos_eq_one_iff = thm "real_sqrt_sos_eq_one_iff";
-val real_divide_square_eq = thm "real_divide_square_eq";
-val real_sqrt_sum_squares_gt_zero1 = thm "real_sqrt_sum_squares_gt_zero1";
-val real_sqrt_sum_squares_gt_zero2 = thm "real_sqrt_sum_squares_gt_zero2";
-val real_sqrt_sum_squares_gt_zero3 = thm "real_sqrt_sum_squares_gt_zero3";
-val real_sqrt_sum_squares_gt_zero3a = thm "real_sqrt_sum_squares_gt_zero3a";
-val cos_x_y_ge_minus_one = thm "cos_x_y_ge_minus_one";
-val cos_x_y_ge_minus_one1a = thm "cos_x_y_ge_minus_one1a";
-val cos_x_y_le_one = thm "cos_x_y_le_one";
-val cos_x_y_le_one2 = thm "cos_x_y_le_one2";
-val cos_abs_x_y_ge_minus_one = thm "cos_abs_x_y_ge_minus_one";
-val cos_abs_x_y_le_one = thm "cos_abs_x_y_le_one";
-val minus_pi_less_zero = thm "minus_pi_less_zero";
-val arcos_ge_minus_pi = thm "arcos_ge_minus_pi";
-val sin_x_y_disj = thm "sin_x_y_disj";
-val cos_x_y_disj = thm "cos_x_y_disj";
-val real_sqrt_divide_less_zero = thm "real_sqrt_divide_less_zero";
-val polar_ex1 = thm "polar_ex1";
-val polar_ex2 = thm "polar_ex2";
-val polar_Ex = thm "polar_Ex";
-val real_sqrt_ge_abs1 = thm "real_sqrt_ge_abs1";
-val real_sqrt_ge_abs2 = thm "real_sqrt_ge_abs2";
-val real_sqrt_two_gt_zero = thm "real_sqrt_two_gt_zero";
-val real_sqrt_two_ge_zero = thm "real_sqrt_two_ge_zero";
-val real_sqrt_two_gt_one = thm "real_sqrt_two_gt_one";
-val STAR_exp_ln = thm "STAR_exp_ln";
-val hypreal_add_Infinitesimal_gt_zero = thm "hypreal_add_Infinitesimal_gt_zero";
-val NSDERIV_exp_ln_one = thm "NSDERIV_exp_ln_one";
-val DERIV_exp_ln_one = thm "DERIV_exp_ln_one";
-val isCont_inv_fun = thm "isCont_inv_fun";
-val isCont_inv_fun_inv = thm "isCont_inv_fun_inv";
-val LIM_fun_gt_zero = thm "LIM_fun_gt_zero";
-val LIM_fun_less_zero = thm "LIM_fun_less_zero";
-val LIM_fun_not_zero = thm "LIM_fun_not_zero";
-*}
end
--- a/src/HOL/Real/ContNotDenum.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/ContNotDenum.thy Fri Jun 02 23:22:29 2006 +0200
@@ -36,8 +36,9 @@
subsection {* Definition *}
-constdefs closed_int :: "real \<Rightarrow> real \<Rightarrow> real set"
- "closed_int x y \<equiv> {z. x \<le> z \<and> z \<le> y}"
+definition
+ closed_int :: "real \<Rightarrow> real \<Rightarrow> real set"
+ "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
subsection {* Properties *}
@@ -48,9 +49,9 @@
{
fix x::real
assume "x \<in> closed_int x1 y1"
- hence "x \<ge> x1 \<and> x \<le> y1" by (unfold closed_int_def, simp)
+ hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
- hence "x \<in> closed_int x0 y0" by (unfold closed_int_def, simp)
+ hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
}
thus ?thesis by auto
qed
@@ -575,4 +576,4 @@
ultimately show False by blast
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Real/Float.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/Float.thy Fri Jun 02 23:22:29 2006 +0200
@@ -5,11 +5,11 @@
theory Float imports Real begin
-constdefs
+definition
pow2 :: "int \<Rightarrow> real"
- "pow2 a == if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a))))"
+ "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
float :: "int * int \<Rightarrow> real"
- "float x == (real (fst x)) * (pow2 (snd x))"
+ "float x = real (fst x) * pow2 (snd x)"
lemma pow2_0[simp]: "pow2 0 = 1"
by (simp add: pow2_def)
@@ -20,7 +20,7 @@
lemma pow2_neg: "pow2 x = inverse (pow2 (-x))"
by (simp add: pow2_def)
-lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
+lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
proof -
have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
have g: "! a b. a - -1 = a + (1::int)" by arith
@@ -30,7 +30,7 @@
apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
apply (auto simp add: h)
apply arith
- done
+ done
show ?thesis
proof (induct a)
case (1 n)
@@ -43,12 +43,12 @@
apply (subst pow2_neg[of "-1 - int n"])
apply (auto simp add: g pos)
done
- qed
+ qed
qed
-
+
lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
proof (induct b)
- case (1 n)
+ case (1 n)
show ?case
proof (induct n)
case 0
@@ -59,10 +59,10 @@
qed
next
case (2 n)
- show ?case
+ show ?case
proof (induct n)
case 0
- show ?case
+ show ?case
apply (auto)
apply (subst pow2_neg[of "a + -1"])
apply (subst pow2_neg[of "-1"])
@@ -73,7 +73,7 @@
apply (simp)
done
case (Suc m)
- have a: "int m - (a + -2) = 1 + (int m - a + 1)" by arith
+ have a: "int m - (a + -2) = 1 + (int m - a + 1)" by arith
have b: "int m - -2 = 1 + (int m + 1)" by arith
show ?case
apply (auto)
@@ -92,14 +92,14 @@
qed
qed
-lemma "float (a, e) + float (b, e) = float (a + b, e)"
+lemma "float (a, e) + float (b, e) = float (a + b, e)"
by (simp add: float_def ring_eq_simps)
-constdefs
+definition
int_of_real :: "real \<Rightarrow> int"
- "int_of_real x == SOME y. real y = x"
+ "int_of_real x = (SOME y. real y = x)"
real_is_int :: "real \<Rightarrow> bool"
- "real_is_int x == ? (u::int). x = real u"
+ "real_is_int x = (EX (u::int). x = real u)"
lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
by (auto simp add: real_is_int_def int_of_real_def)
@@ -110,7 +110,7 @@
lemma pow2_int: "pow2 (int c) = (2::real)^c"
by (simp add: pow2_def)
-lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)"
+lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)"
by (simp add: float_def pow2_int[symmetric] pow2_add[symmetric])
lemma real_is_int_real[simp]: "real_is_int (real (x::int))"
@@ -141,7 +141,7 @@
lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real a = x"
by (auto simp add: real_is_int_def)
-lemma int_of_real_mult:
+lemma int_of_real_mult:
assumes "real_is_int a" "real_is_int b"
shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
proof -
@@ -187,8 +187,8 @@
also have "\<dots> = True" by (simp only: real_is_int_real)
ultimately show ?thesis by auto
qed
-
- {
+
+ {
fix x::int
have "!! y. real_is_int ((number_of::bin\<Rightarrow>real) (Abs_Bin x))"
apply (simp add: number_of_eq)
@@ -205,11 +205,11 @@
assume rn: "(real_is_int (of_int (- (int (Suc n)))))"
have s: "-(int (Suc (Suc n))) = -1 + - (int (Suc n))" by simp
show "real_is_int (of_int (- (int (Suc (Suc n)))))"
- apply (simp only: s of_int_add)
- apply (rule real_is_int_add)
- apply (simp add: neg1)
- apply (simp only: rn)
- done
+ apply (simp only: s of_int_add)
+ apply (rule real_is_int_add)
+ apply (simp add: neg1)
+ apply (simp only: rn)
+ done
qed
}
note Abs_Bin = this
@@ -228,7 +228,7 @@
by (simp add: int_of_real_def)
lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)"
-proof -
+proof -
have 1: "(1::real) = real (1::int)" by auto
show ?thesis by (simp only: 1 int_of_real_real)
qed
@@ -238,9 +238,9 @@
have "real_is_int (number_of b)" by simp
then have uu: "?! u::int. number_of b = real u" by (auto simp add: real_is_int_rep)
then obtain u::int where u:"number_of b = real u" by auto
- have "number_of b = real ((number_of b)::int)"
+ have "number_of b = real ((number_of b)::int)"
by (simp add: number_of_eq real_of_int_def)
- have ub: "number_of b = real ((number_of b)::int)"
+ have ub: "number_of b = real ((number_of b)::int)"
by (simp add: number_of_eq real_of_int_def)
from uu u ub have unb: "u = number_of b"
by blast
@@ -255,10 +255,10 @@
proof -
fix q::int
have a:"b - (-1\<Colon>int) = (1\<Colon>int) + b" by arith
- show "(float (q, (b - (-1\<Colon>int)))) = (float (q, ((1\<Colon>int) + b)))"
+ show "(float (q, (b - (-1\<Colon>int)))) = (float (q, ((1\<Colon>int) + b)))"
by (simp add: a)
qed
-
+
consts
norm_float :: "int*int \<Rightarrow> int*int"
@@ -285,7 +285,7 @@
apply (auto)
done
-ML {* simp_depth_limit := 2 *}
+ML {* simp_depth_limit := 2 *}
recdef norm_float "measure (% (a,b). nat (abs a))"
"norm_float (a,b) = (if (a \<noteq> 0) & (even a) then norm_float (a div 2, b+1) else (if a=0 then (0,0) else (a,b)))"
(hints simp: terminating_norm_float)
@@ -294,23 +294,23 @@
lemma norm_float: "float x = float (norm_float x)"
proof -
{
- fix a b :: int
- have norm_float_pair: "float (a,b) = float (norm_float (a,b))"
+ fix a b :: int
+ have norm_float_pair: "float (a,b) = float (norm_float (a,b))"
proof (induct a b rule: norm_float.induct)
case (1 u v)
- show ?case
+ show ?case
proof cases
- assume u: "u \<noteq> 0 \<and> even u"
- with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2, v + 1))" by auto
- with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
- then show ?thesis
- apply (subst norm_float.simps)
- apply (simp add: ind)
- done
+ assume u: "u \<noteq> 0 \<and> even u"
+ with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2, v + 1))" by auto
+ with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
+ then show ?thesis
+ apply (subst norm_float.simps)
+ apply (simp add: ind)
+ done
next
- assume "~(u \<noteq> 0 \<and> even u)"
- then show ?thesis
- by (simp add: prems float_def)
+ assume "~(u \<noteq> 0 \<and> even u)"
+ then show ?thesis
+ by (simp add: prems float_def)
qed
qed
}
@@ -323,16 +323,16 @@
lemma pow2_int: "pow2 (int n) = 2^n"
by (simp add: pow2_def)
-lemma float_add:
- "float (a1, e1) + float (a2, e2) =
- (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
+lemma float_add:
+ "float (a1, e1) + float (a2, e2) =
+ (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
else float (a1*2^(nat (e1-e2))+a2, e2))"
apply (simp add: float_def ring_eq_simps)
apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
done
lemma float_mult:
- "float (a1, e1) * float (a2, e2) =
+ "float (a1, e1) * float (a2, e2) =
(float (a1 * a2, e1 + e2))"
by (simp add: float_def pow2_add)
@@ -345,7 +345,7 @@
proof -
{
fix y
- have "0 <= y \<Longrightarrow> 0 < pow2 y"
+ have "0 <= y \<Longrightarrow> 0 < pow2 y"
by (induct y, induct_tac n, simp_all add: pow2_add)
}
note helper=this
@@ -360,7 +360,7 @@
lemma zero_le_float:
"(0 <= float (a,b)) = (0 <= a)"
apply (auto simp add: float_def)
- apply (auto simp add: zero_le_mult_iff zero_less_pow2)
+ apply (auto simp add: zero_le_mult_iff zero_less_pow2)
apply (insert zero_less_pow2[of b])
apply (simp_all)
done
@@ -393,7 +393,7 @@
lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1"
by auto
-
+
lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
by simp
@@ -451,19 +451,19 @@
lemma not_true_eq_false: "(~ True) = False" by simp
-lemmas binarith =
+lemmas binarith =
Pls_0_eq Min_1_eq
- bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
+ bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10
- bin_add_BIT_11 bin_minus_Pls bin_minus_Min bin_minus_1
- bin_minus_0 bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
+ bin_add_BIT_11 bin_minus_Pls bin_minus_Min bin_minus_1
+ bin_minus_0 bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
bin_add_Pls_right bin_add_Min_right
lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
by simp
-lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
+lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
by (simp only: iszero_number_of_Pls)
lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
@@ -472,13 +472,13 @@
lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
by simp
-lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
+lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
by simp
lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
by simp
-lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
+lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
by simp
lemma int_neg_number_of_Min: "neg (-1::int)"
@@ -490,9 +490,9 @@
lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
by simp
-lemmas intarithrel =
- int_eq_number_of_eq
- lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_0
+lemmas intarithrel =
+ int_eq_number_of_eq
+ lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_0
lift_bool[OF int_iszero_number_of_1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
int_neg_number_of_BIT int_le_number_of_eq
@@ -512,8 +512,8 @@
lemmas natarith = add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
-lemmas powerarith = nat_number_of zpower_number_of_even
- zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
+lemmas powerarith = nat_number_of zpower_number_of_even
+ zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
zpower_Pls zpower_Min
lemmas floatarith[simplified norm_0_1] = float_add float_mult float_minus float_abs zero_le_float float_pprt float_nprt
@@ -522,4 +522,3 @@
lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false
end
-
--- a/src/HOL/Real/Lubs.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/Lubs.thy Fri Jun 02 23:22:29 2006 +0200
@@ -12,25 +12,25 @@
text{*Thanks to suggestions by James Margetson*}
-constdefs
+definition
setle :: "['a set, 'a::ord] => bool" (infixl "*<=" 70)
- "S *<= x == (ALL y: S. y <= x)"
+ "S *<= x = (ALL y: S. y <= x)"
setge :: "['a::ord, 'a set] => bool" (infixl "<=*" 70)
- "x <=* S == (ALL y: S. x <= y)"
+ "x <=* S = (ALL y: S. x <= y)"
leastP :: "['a =>bool,'a::ord] => bool"
- "leastP P x == (P x & x <=* Collect P)"
+ "leastP P x = (P x & x <=* Collect P)"
isUb :: "['a set, 'a set, 'a::ord] => bool"
- "isUb R S x == S *<= x & x: R"
+ "isUb R S x = (S *<= x & x: R)"
isLub :: "['a set, 'a set, 'a::ord] => bool"
- "isLub R S x == leastP (isUb R S) x"
+ "isLub R S x = leastP (isUb R S) x"
ubs :: "['a set, 'a::ord set] => 'a set"
- "ubs R S == Collect (isUb R S)"
+ "ubs R S = Collect (isUb R S)"
@@ -106,35 +106,4 @@
apply (erule leastPD2)
done
-ML
-{*
-val setle_def = thm "setle_def";
-val setge_def = thm "setge_def";
-val leastP_def = thm "leastP_def";
-val isLub_def = thm "isLub_def";
-val isUb_def = thm "isUb_def";
-val ubs_def = thm "ubs_def";
-
-val setleI = thm "setleI";
-val setleD = thm "setleD";
-val setgeI = thm "setgeI";
-val setgeD = thm "setgeD";
-val leastPD1 = thm "leastPD1";
-val leastPD2 = thm "leastPD2";
-val leastPD3 = thm "leastPD3";
-val isLubD1 = thm "isLubD1";
-val isLubD1a = thm "isLubD1a";
-val isLub_isUb = thm "isLub_isUb";
-val isLubD2 = thm "isLubD2";
-val isLubD3 = thm "isLubD3";
-val isLubI1 = thm "isLubI1";
-val isLubI2 = thm "isLubI2";
-val isUbD = thm "isUbD";
-val isUbD2 = thm "isUbD2";
-val isUbD2a = thm "isUbD2a";
-val isUbI = thm "isUbI";
-val isLub_le_isUb = thm "isLub_le_isUb";
-val isLub_ubs = thm "isLub_ubs";
-*}
-
end
--- a/src/HOL/Real/PReal.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/PReal.thy Fri Jun 02 23:22:29 2006 +0200
@@ -27,11 +27,11 @@
by (auto dest: dense)
-constdefs
+definition
cut :: "rat set => bool"
- "cut A == {} \<subset> A &
- A < {r. 0 < r} &
- (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u)))"
+ "cut A = ({} \<subset> A &
+ A < {r. 0 < r} &
+ (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
lemma cut_of_rat:
@@ -56,24 +56,24 @@
instance preal :: "{ord, plus, minus, times, inverse}" ..
-constdefs
+definition
preal_of_rat :: "rat => preal"
- "preal_of_rat q == Abs_preal({x::rat. 0 < x & x < q})"
+ "preal_of_rat q = Abs_preal({x::rat. 0 < x & x < q})"
psup :: "preal set => preal"
- "psup(P) == Abs_preal(\<Union>X \<in> P. Rep_preal(X))"
+ "psup(P) = Abs_preal(\<Union>X \<in> P. Rep_preal(X))"
add_set :: "[rat set,rat set] => rat set"
- "add_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}"
+ "add_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}"
diff_set :: "[rat set,rat set] => rat set"
- "diff_set A B == {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
+ "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
mult_set :: "[rat set,rat set] => rat set"
- "mult_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}"
+ "mult_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}"
inverse_set :: "rat set => rat set"
- "inverse_set A == {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
+ "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
defs (overloaded)
@@ -163,11 +163,11 @@
Gleason p. 122 - Remark (1)*}
lemma not_in_preal_ub:
- assumes A: "A \<in> preal"
- and notx: "x \<notin> A"
- and y: "y \<in> A"
- and pos: "0 < x"
- shows "y < x"
+ assumes A: "A \<in> preal"
+ and notx: "x \<notin> A"
+ and y: "y \<in> A"
+ and pos: "0 < x"
+ shows "y < x"
proof (cases rule: linorder_cases)
assume "x<y"
with notx show ?thesis
@@ -271,11 +271,11 @@
proof (unfold add_set_def, clarify)
fix x::rat and y::rat
assume A: "A \<in> preal"
- and B: "B \<in> preal"
- and [simp]: "0 < z"
- and zless: "z < x + y"
- and x: "x \<in> A"
- and y: "y \<in> B"
+ and B: "B \<in> preal"
+ and [simp]: "0 < z"
+ and zless: "z < x + y"
+ and x: "x \<in> A"
+ and y: "y \<in> B"
have xpos [simp]: "0<x" by (rule preal_imp_pos [OF A x])
have ypos [simp]: "0<y" by (rule preal_imp_pos [OF B y])
have xypos [simp]: "0 < x+y" by (simp add: pos_add_strict)
@@ -394,16 +394,15 @@
qed
lemma mult_set_not_rat_set:
- assumes A: "A \<in> preal"
- and B: "B \<in> preal"
- shows "mult_set A B < {r. 0 < r}"
+ assumes A: "A \<in> preal"
+ and B: "B \<in> preal"
+ shows "mult_set A B < {r. 0 < r}"
proof
show "mult_set A B \<subseteq> {r. 0 < r}"
by (force simp add: mult_set_def
- intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos_pos)
-next
+ intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos_pos)
show "mult_set A B \<noteq> {r. 0 < r}"
- by (insert preal_not_mem_mult_set_Ex [OF A B], blast)
+ using preal_not_mem_mult_set_Ex [OF A B] by blast
qed
@@ -415,11 +414,11 @@
proof (unfold mult_set_def, clarify)
fix x::rat and y::rat
assume A: "A \<in> preal"
- and B: "B \<in> preal"
- and [simp]: "0 < z"
- and zless: "z < x * y"
- and x: "x \<in> A"
- and y: "y \<in> B"
+ and B: "B \<in> preal"
+ and [simp]: "0 < z"
+ and zless: "z < x * y"
+ and x: "x \<in> A"
+ and y: "y \<in> B"
have [simp]: "0<y" by (rule preal_imp_pos [OF B y])
show "\<exists>x' \<in> A. \<exists>y' \<in> B. z = x' * y'"
proof
@@ -560,10 +559,10 @@
lemma preal_add_mult_distrib_mean:
assumes a: "a \<in> Rep_preal w"
- and b: "b \<in> Rep_preal w"
- and d: "d \<in> Rep_preal x"
- and e: "e \<in> Rep_preal y"
- shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)"
+ and b: "b \<in> Rep_preal w"
+ and d: "d \<in> Rep_preal x"
+ and e: "e \<in> Rep_preal y"
+ shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)"
proof
let ?c = "(a*d + b*e)/(d+e)"
have [simp]: "0<a" "0<b" "0<d" "0<e" "0<d+e"
@@ -690,9 +689,9 @@
lemma Gleason9_34_exists:
assumes A: "A \<in> preal"
- and "\<forall>x\<in>A. x + u \<in> A"
- and "0 \<le> z"
- shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
+ and "\<forall>x\<in>A. x + u \<in> A"
+ and "0 \<le> z"
+ shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
proof (cases z rule: int_cases)
case (nonneg n)
show ?thesis
@@ -717,11 +716,11 @@
fix a::int and b::int
fix c::int and d::int
assume bpos [simp]: "0 < b"
- and dpos [simp]: "0 < d"
- and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A"
- and upos: "0 < Fract c d"
- and ypos: "0 < Fract a b"
- and notin: "Fract a b \<notin> A"
+ and dpos [simp]: "0 < d"
+ and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A"
+ and upos: "0 < Fract c d"
+ and ypos: "0 < Fract a b"
+ and notin: "Fract a b \<notin> A"
have cpos [simp]: "0 < c"
by (simp add: zero_less_Fract_iff [OF dpos, symmetric] upos)
have apos [simp]: "0 < a"
@@ -752,8 +751,8 @@
lemma Gleason9_34:
assumes A: "A \<in> preal"
- and upos: "0 < u"
- shows "\<exists>r \<in> A. r + u \<notin> A"
+ and upos: "0 < u"
+ shows "\<exists>r \<in> A. r + u \<notin> A"
proof (rule ccontr, simp)
assume closed: "\<forall>r\<in>A. r + u \<in> A"
from preal_exists_bound [OF A]
@@ -768,8 +767,8 @@
lemma lemma_gleason9_36:
assumes A: "A \<in> preal"
- and x: "1 < x"
- shows "\<exists>r \<in> A. r*x \<notin> A"
+ and x: "1 < x"
+ shows "\<exists>r \<in> A. r*x \<notin> A"
proof -
from preal_nonempty [OF A]
obtain y where y: "y \<in> A" and ypos: "0<y" ..
@@ -824,9 +823,9 @@
by (simp add: preal_of_rat_def rat_mem_preal)
lemma subset_inverse_mult_lemma:
- assumes xpos: "0 < x" and xless: "x < 1"
- shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R &
- u \<in> Rep_preal R & x = r * u"
+ assumes xpos: "0 < x" and xless: "x < 1"
+ shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R &
+ u \<in> Rep_preal R & x = r * u"
proof -
from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff)
from lemma_gleason9_36 [OF Rep_preal this]
@@ -858,11 +857,11 @@
done
lemma inverse_mult_subset_lemma:
- assumes rpos: "0 < r"
- and rless: "r < y"
- and notin: "inverse y \<notin> Rep_preal R"
- and q: "q \<in> Rep_preal R"
- shows "r*q < 1"
+ assumes rpos: "0 < r"
+ and rless: "r < y"
+ and notin: "inverse y \<notin> Rep_preal R"
+ and q: "q \<in> Rep_preal R"
+ shows "r*q < 1"
proof -
have "q < inverse y" using rpos rless
by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
@@ -961,7 +960,7 @@
done
lemma diff_set_not_rat_set:
- "diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs")
+ "diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs")
proof
show "?lhs \<subseteq> ?rhs" by (auto simp add: diff_set_def)
show "?lhs \<noteq> ?rhs" using diff_set_nonempty by blast
@@ -1007,11 +1006,11 @@
lemma less_add_left_lemma:
assumes Rless: "R < S"
- and a: "a \<in> Rep_preal R"
- and cb: "c + b \<in> Rep_preal S"
- and "c \<notin> Rep_preal R"
- and "0 < b"
- and "0 < c"
+ and a: "a \<in> Rep_preal R"
+ and cb: "c + b \<in> Rep_preal S"
+ and "c \<notin> Rep_preal R"
+ and "0 < b"
+ and "0 < c"
shows "a + b \<in> Rep_preal S"
proof -
have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
@@ -1039,8 +1038,8 @@
lemma less_add_left_lemma2:
assumes Rless: "R < S"
- and x: "x \<in> Rep_preal S"
- and xnot: "x \<notin> Rep_preal R"
+ and x: "x \<in> Rep_preal S"
+ and xnot: "x \<notin> Rep_preal R"
shows "\<exists>u v z. 0 < v & 0 < z & u \<in> Rep_preal R & z \<notin> Rep_preal R &
z + v \<in> Rep_preal S & x = u + v"
proof -
@@ -1216,9 +1215,9 @@
lemma preal_of_rat_add_lemma2:
assumes "u < x + y"
- and "0 < x"
- and "0 < y"
- and "0 < u"
+ and "0 < x"
+ and "0 < y"
+ and "0 < u"
shows "\<exists>v w::rat. w < y & 0 < v & v < x & 0 < w & u = v + w"
proof (intro exI conjI)
show "u * x * inverse(x+y) < x" using prems
@@ -1253,8 +1252,8 @@
lemma preal_of_rat_mult_lemma2:
assumes xless: "x < y * z"
- and xpos: "0 < x"
- and ypos: "0 < y"
+ and xpos: "0 < x"
+ and ypos: "0 < y"
shows "x * z * inverse y * inverse z < (z::rat)"
proof -
have "0 < y * z" using prems by simp
@@ -1270,9 +1269,9 @@
lemma preal_of_rat_mult_lemma3:
assumes uless: "u < x * y"
- and "0 < x"
- and "0 < y"
- and "0 < u"
+ and "0 < x"
+ and "0 < y"
+ and "0 < u"
shows "\<exists>v w::rat. v < x & w < y & 0 < v & 0 < w & u = v * w"
proof -
from dense [OF uless]
@@ -1317,37 +1316,4 @@
"[| 0 < x; 0 < y|] ==> (preal_of_rat x = preal_of_rat y) = (x = y)"
by (simp add: preal_of_rat_le_iff order_eq_iff)
-
-ML
-{*
-val mem_Rep_preal_Ex = thm"mem_Rep_preal_Ex";
-val preal_add_commute = thm"preal_add_commute";
-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_assoc = thm"preal_mult_assoc";
-val preal_mult_left_commute = thm"preal_mult_left_commute";
-val preal_add_mult_distrib2 = thm"preal_add_mult_distrib2";
-val preal_add_mult_distrib = thm"preal_add_mult_distrib";
-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 less_add_left = thm"less_add_left";
-val preal_add_less2_mono1 = thm"preal_add_less2_mono1";
-val preal_add_less2_mono2 = thm"preal_add_less2_mono2";
-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_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_psup_le = thm"preal_psup_le";
-val psup_le_ub = thm"psup_le_ub";
-val preal_complete = thm"preal_complete";
-val preal_of_rat_add = thm"preal_of_rat_add";
-val preal_of_rat_mult = thm"preal_of_rat_mult";
-
-val preal_add_ac = thms"preal_add_ac";
-val preal_mult_ac = thms"preal_mult_ac";
-*}
-
end
--- a/src/HOL/Real/RComplete.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/RComplete.thy Fri Jun 02 23:22:29 2006 +0200
@@ -429,36 +429,22 @@
done
-ML
-{*
-val real_sum_of_halves = thm "real_sum_of_halves";
-val posreal_complete = thm "posreal_complete";
-val real_isLub_unique = thm "real_isLub_unique";
-val posreals_complete = thm "posreals_complete";
-val reals_complete = thm "reals_complete";
-val reals_Archimedean = thm "reals_Archimedean";
-val reals_Archimedean2 = thm "reals_Archimedean2";
-val reals_Archimedean3 = thm "reals_Archimedean3";
-*}
-
-
subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
-constdefs
-
+definition
floor :: "real => int"
- "floor r == (LEAST n::int. r < real (n+1))"
+ "floor r = (LEAST n::int. r < real (n+1))"
ceiling :: "real => int"
- "ceiling r == - floor (- r)"
+ "ceiling r = - floor (- r)"
-syntax (xsymbols)
- floor :: "real => int" ("\<lfloor>_\<rfloor>")
- ceiling :: "real => int" ("\<lceil>_\<rceil>")
+const_syntax (xsymbols)
+ floor ("\<lfloor>_\<rfloor>")
+ ceiling ("\<lceil>_\<rceil>")
-syntax (HTML output)
- floor :: "real => int" ("\<lfloor>_\<rfloor>")
- ceiling :: "real => int" ("\<lceil>_\<rceil>")
+const_syntax (HTML output)
+ floor ("\<lfloor>_\<rfloor>")
+ ceiling ("\<lceil>_\<rceil>")
lemma number_of_less_real_of_int_iff [simp]:
@@ -946,11 +932,11 @@
subsection {* Versions for the natural numbers *}
-constdefs
+definition
natfloor :: "real => nat"
- "natfloor x == nat(floor x)"
+ "natfloor x = nat(floor x)"
natceiling :: "real => nat"
- "natceiling x == nat(ceiling x)"
+ "natceiling x = nat(ceiling x)"
lemma natfloor_zero [simp]: "natfloor 0 = 0"
by (unfold natfloor_def, simp)
@@ -1300,55 +1286,4 @@
by simp
qed
-ML
-{*
-val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff";
-val number_of_less_real_of_int_iff2 = thm "number_of_less_real_of_int_iff2";
-val number_of_le_real_of_int_iff = thm "number_of_le_real_of_int_iff";
-val number_of_le_real_of_int_iff2 = thm "number_of_le_real_of_int_iff2";
-val floor_zero = thm "floor_zero";
-val floor_real_of_nat_zero = thm "floor_real_of_nat_zero";
-val floor_real_of_nat = thm "floor_real_of_nat";
-val floor_minus_real_of_nat = thm "floor_minus_real_of_nat";
-val floor_real_of_int = thm "floor_real_of_int";
-val floor_minus_real_of_int = thm "floor_minus_real_of_int";
-val reals_Archimedean6 = thm "reals_Archimedean6";
-val reals_Archimedean6a = thm "reals_Archimedean6a";
-val reals_Archimedean_6b_int = thm "reals_Archimedean_6b_int";
-val reals_Archimedean_6c_int = thm "reals_Archimedean_6c_int";
-val real_lb_ub_int = thm "real_lb_ub_int";
-val lemma_floor = thm "lemma_floor";
-val real_of_int_floor_le = thm "real_of_int_floor_le";
-(*val floor_le = thm "floor_le";
-val floor_le2 = thm "floor_le2";
-*)
-val lemma_floor2 = thm "lemma_floor2";
-val real_of_int_floor_cancel = thm "real_of_int_floor_cancel";
-val floor_eq = thm "floor_eq";
-val floor_eq2 = thm "floor_eq2";
-val floor_eq3 = thm "floor_eq3";
-val floor_eq4 = thm "floor_eq4";
-val floor_number_of_eq = thm "floor_number_of_eq";
-val real_of_int_floor_ge_diff_one = thm "real_of_int_floor_ge_diff_one";
-val real_of_int_floor_add_one_ge = thm "real_of_int_floor_add_one_ge";
-val ceiling_zero = thm "ceiling_zero";
-val ceiling_real_of_nat = thm "ceiling_real_of_nat";
-val ceiling_real_of_nat_zero = thm "ceiling_real_of_nat_zero";
-val ceiling_floor = thm "ceiling_floor";
-val floor_ceiling = thm "floor_ceiling";
-val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge";
-(*
-val ceiling_le = thm "ceiling_le";
-val ceiling_le2 = thm "ceiling_le2";
-*)
-val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel";
-val ceiling_eq = thm "ceiling_eq";
-val ceiling_eq2 = thm "ceiling_eq2";
-val ceiling_eq3 = thm "ceiling_eq3";
-val ceiling_real_of_int = thm "ceiling_real_of_int";
-val ceiling_number_of_eq = thm "ceiling_number_of_eq";
-val real_of_int_ceiling_diff_one_le = thm "real_of_int_ceiling_diff_one_le";
-val real_of_int_ceiling_le_add_one = thm "real_of_int_ceiling_le_add_one";
-*}
-
end
--- a/src/HOL/Real/Rational.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/Rational.thy Fri Jun 02 23:22:29 2006 +0200
@@ -14,12 +14,12 @@
subsubsection {* Equivalence of fractions *}
-constdefs
+definition
fraction :: "(int \<times> int) set"
- "fraction \<equiv> {x. snd x \<noteq> 0}"
+ "fraction = {x. snd x \<noteq> 0}"
ratrel :: "((int \<times> int) \<times> (int \<times> int)) set"
- "ratrel \<equiv> {(x,y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
+ "ratrel = {(x,y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
lemma fraction_iff [simp]: "(x \<in> fraction) = (snd x \<noteq> 0)"
by (simp add: fraction_def)
@@ -78,9 +78,9 @@
declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp]
-constdefs
+definition
Fract :: "int \<Rightarrow> int \<Rightarrow> rat"
- "Fract a b \<equiv> Abs_Rat (ratrel``{(a,b)})"
+ "Fract a b = Abs_Rat (ratrel``{(a,b)})"
theorem Rat_cases [case_names Fract, cases type: rat]:
"(!!a b. q = Fract a b ==> b \<noteq> 0 ==> C) ==> C"
@@ -455,12 +455,9 @@
--{*the type constraint is essential!*}
instance rat :: number_ring
-by (intro_classes, simp add: rat_number_of_def)
-
-declare diff_rat_def [symmetric]
+ by default (simp add: rat_number_of_def)
use "rat_arith.ML"
-
setup rat_arith_setup
end
--- a/src/HOL/Real/RealDef.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/RealDef.thy Fri Jun 02 23:22:29 2006 +0200
@@ -13,22 +13,21 @@
uses ("real_arith.ML")
begin
-constdefs
+definition
realrel :: "((preal * preal) * (preal * preal)) set"
- "realrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+ "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
typedef (Real) real = "UNIV//realrel"
by (auto simp add: quotient_def)
instance real :: "{ord, zero, one, plus, times, minus, inverse}" ..
-constdefs
+definition
(** these don't use the overloaded "real" function: users don't see them **)
real_of_preal :: "preal => real"
- "real_of_preal m ==
- Abs_Real(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})"
+ "real_of_preal m = Abs_Real(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})"
consts
(*Overloaded constant denoting the Real subset of enclosing
@@ -38,8 +37,8 @@
(*overloaded constant for injecting other types into "real"*)
real :: "'a => real"
-syntax (xsymbols)
- Reals :: "'a set" ("\<real>")
+const_syntax (xsymbols)
+ Reals ("\<real>")
defs (overloaded)
@@ -1018,7 +1017,6 @@
lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
by (force simp add: OrderedGroup.abs_le_iff)
-(*FIXME: used only once, in SEQ.ML*)
lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
by (simp add: abs_if)
@@ -1030,7 +1028,6 @@
apply (auto intro: abs_ge_self [THEN order_trans])
done
-text{*Used only in Hyperreal/Lim.ML*}
lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
apply (simp add: real_add_assoc)
apply (rule_tac a1 = y in add_left_commute [THEN ssubst])
@@ -1038,19 +1035,4 @@
apply (rule abs_triangle_ineq)
done
-
-ML
-{*
-val real_lbound_gt_zero = thm"real_lbound_gt_zero";
-val real_less_half_sum = thm"real_less_half_sum";
-val real_gt_half_sum = thm"real_gt_half_sum";
-
-val abs_interval_iff = thm"abs_interval_iff";
-val abs_le_interval_iff = thm"abs_le_interval_iff";
-val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
-val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
-val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
-*}
-
-
end
--- a/src/HOL/Real/RealPow.thy Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/RealPow.thy Fri Jun 02 23:22:29 2006 +0200
@@ -37,8 +37,7 @@
lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
by simp
-text{*Legacy: weaker version of the theorem @{text power_strict_mono},
-used 6 times in NthRoot and Transcendental*}
+text{*Legacy: weaker version of the theorem @{text power_strict_mono}*}
lemma realpow_less:
"[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
apply (rule power_strict_mono, auto)
@@ -67,11 +66,9 @@
lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
by (insert power_decreasing [of 1 "Suc n" r], simp)
-text{*Used ONCE in Transcendental*}
lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
by (insert power_strict_decreasing [of 0 "Suc n" r], simp)
-text{*Used ONCE in Lim.ML*}
lemma realpow_minus_mult [rule_format]:
"0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
apply (simp split add: nat_diff_split)
@@ -140,7 +137,6 @@
subsection{*Various Other Theorems*}
-text{*Used several times in Hyperreal/Transcendental.ML*}
lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric])
apply (auto dest: real_sum_squares_cancel simp add: add_commute)
@@ -171,7 +167,6 @@
apply (auto simp add: mult_ac)
done
-text{*Used once: in Hyperreal/Transcendental.ML*}
lemma real_mult_inverse_cancel2:
"[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
@@ -272,59 +267,4 @@
apply (auto simp add: realpow_num_eq_if)
done
-
-ML
-{*
-val realpow_0 = thm "realpow_0";
-val realpow_Suc = thm "realpow_Suc";
-
-val realpow_not_zero = thm "realpow_not_zero";
-val realpow_zero_zero = thm "realpow_zero_zero";
-val realpow_two = thm "realpow_two";
-val realpow_less = thm "realpow_less";
-val realpow_two_le = thm "realpow_two_le";
-val abs_realpow_two = thm "abs_realpow_two";
-val realpow_two_abs = thm "realpow_two_abs";
-val two_realpow_ge_one = thm "two_realpow_ge_one";
-val two_realpow_gt = thm "two_realpow_gt";
-val realpow_Suc_le_self = thm "realpow_Suc_le_self";
-val realpow_Suc_less_one = thm "realpow_Suc_less_one";
-val realpow_minus_mult = thm "realpow_minus_mult";
-val realpow_two_mult_inverse = thm "realpow_two_mult_inverse";
-val realpow_two_minus = thm "realpow_two_minus";
-val realpow_two_disj = thm "realpow_two_disj";
-val realpow_real_of_nat = thm "realpow_real_of_nat";
-val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos";
-val realpow_increasing = thm "realpow_increasing";
-val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff";
-val zero_le_realpow_abs = thm "zero_le_realpow_abs";
-val real_of_int_power = thm "real_of_int_power";
-val power_real_number_of = thm "power_real_number_of";
-val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a";
-val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
-val real_squared_diff_one_factored = thm "real_squared_diff_one_factored";
-val real_mult_is_one = thm "real_mult_is_one";
-val real_le_add_half_cancel = thm "real_le_add_half_cancel";
-val real_minus_half_eq = thm "real_minus_half_eq";
-val real_mult_inverse_cancel = thm "real_mult_inverse_cancel";
-val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
-val inverse_real_of_nat_gt_zero = thm "inverse_real_of_nat_gt_zero";
-val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero";
-val real_sum_squares_not_zero = thm "real_sum_squares_not_zero";
-val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2";
-
-val realpow_divide = thm "realpow_divide";
-val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
-val realpow_two_le_add_order = thm "realpow_two_le_add_order";
-val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
-val real_sum_square_gt_zero = thm "real_sum_square_gt_zero";
-val real_sum_square_gt_zero2 = thm "real_sum_square_gt_zero2";
-val real_minus_mult_self_le = thm "real_minus_mult_self_le";
-val realpow_square_minus_le = thm "realpow_square_minus_le";
-val realpow_num_eq_if = thm "realpow_num_eq_if";
-val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow";
-val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono";
-*}
-
-
end