--- a/src/HOL/Hyperreal/HLog.thy Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HLog.thy Mon Mar 15 10:46:19 2004 +0100
@@ -32,22 +32,19 @@
by (simp add: powhr_def starfun hypreal_mult powr_def)
lemma powhr_one_eq_one [simp]: "1 powhr a = 1"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
apply (simp add: powhr hypreal_one_num)
done
lemma powhr_mult:
"[| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases y, cases a)
apply (simp add: powhr hypreal_zero_num hypreal_mult hypreal_less, ultra)
apply (simp add: powr_mult)
done
lemma powhr_gt_zero [simp]: "0 < x powhr a"
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of x])
+apply (cases a, cases x)
apply (simp add: hypreal_zero_def powhr hypreal_less hypreal_zero_num)
done
@@ -61,37 +58,28 @@
lemma powhr_divide:
"[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases y, cases a)
apply (simp add: powhr hypreal_divide hypreal_zero_num hypreal_less, ultra)
apply (simp add: powr_divide)
done
lemma powhr_add: "x powhr (a + b) = (x powhr a) * (x powhr b)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of b])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases b, cases a)
apply (simp add: powhr hypreal_add hypreal_mult powr_add)
done
lemma powhr_powhr: "(x powhr a) powhr b = x powhr (a * b)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of b])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases b, cases a)
apply (simp add: powhr hypreal_mult powr_powr)
done
lemma powhr_powhr_swap: "(x powhr a) powhr b = (x powhr b) powhr a"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of b])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases b, cases a)
apply (simp add: powhr powr_powr_swap)
done
lemma powhr_minus: "x powhr (-a) = inverse (x powhr a)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases a)
apply (simp add: powhr hypreal_minus hypreal_inverse hypreal_less powr_minus)
done
@@ -99,16 +87,12 @@
by (simp add: divide_inverse powhr_minus)
lemma powhr_less_mono: "[| a < b; 1 < x |] ==> x powhr a < x powhr b"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of b])
+apply (cases x, cases a, cases b)
apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
done
lemma powhr_less_cancel: "[| x powhr a < x powhr b; 1 < x |] ==> a < b"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of b])
+apply (cases x, cases a, cases b)
apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
done
@@ -128,21 +112,19 @@
done
lemma hlog_starfun_ln: "( *f* ln) x = hlog (( *f* exp) 1) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hlog log_ln hypreal_one_num)
done
lemma powhr_hlog_cancel [simp]:
"[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases a)
apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
done
lemma hlog_powhr_cancel [simp]:
"[| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases y, cases a)
apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
apply (auto intro: log_powr_cancel)
done
@@ -150,33 +132,27 @@
lemma hlog_mult:
"[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]
==> hlog a (x * y) = hlog a x + hlog a y"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases y, cases a)
apply (simp add: hlog powhr hypreal_zero_num hypreal_one_num hypreal_less hypreal_add hypreal_mult, ultra)
apply (simp add: log_mult)
done
lemma hlog_as_starfun:
"[| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
+apply (cases x, cases a)
apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_divide log_def)
done
lemma hlog_eq_div_starfun_ln_mult_hlog:
"[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]
==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of b])
+apply (cases x, cases a, cases b)
apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_less hypreal_divide hypreal_mult, ultra)
apply (auto dest: log_eq_div_ln_mult_log)
done
lemma powhr_as_starfun: "x powhr a = ( *f* exp) (a * ( *f* ln) x)"
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of x])
+apply (cases a, cases x)
apply (simp add: powhr starfun hypreal_mult powr_def)
done
@@ -202,12 +178,12 @@
by (rule hlog_as_starfun, auto)
lemma hlog_one [simp]: "hlog a 1 = 0"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
apply (simp add: hypreal_one_num hypreal_zero_num hlog)
done
lemma hlog_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
-apply (rule eq_Abs_hypreal [of a])
+apply (cases a)
apply (simp add: hypreal_one_num hypreal_zero_num hlog hypreal_less, ultra)
apply (auto intro: log_eq_one)
done
@@ -224,9 +200,7 @@
lemma hlog_less_cancel_iff [simp]:
"[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
-apply (rule eq_Abs_hypreal [of a])
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases a, cases x, cases y)
apply (auto simp add: hlog hypreal_less hypreal_zero_num hypreal_one_num, ultra+)
done
--- a/src/HOL/Hyperreal/HSeries.thy Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy Mon Mar 15 10:46:19 2004 +0100
@@ -36,7 +36,7 @@
text{*Base case in definition of @{term sumr}*}
lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
-apply (rule eq_Abs_hypnat [of m])
+apply (cases m)
apply (simp add: hypnat_zero_def sumhr symmetric hypreal_zero_def)
done
@@ -44,48 +44,43 @@
lemma sumhr_if:
"sumhr(m,n+1,f) =
(if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *fNat* f) n)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (auto simp add: hypnat_one_def sumhr hypnat_add hypnat_le starfunNat
hypreal_add hypreal_zero_def, ultra+)
done
lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (simp add: hypnat_one_def sumhr hypnat_add hypreal_zero_def)
done
lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (simp add: sumhr hypreal_zero_def)
done
lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *fNat* f) m"
-apply (rule eq_Abs_hypnat [of m])
+apply (cases m)
apply (simp add: sumhr hypnat_one_def hypnat_add starfunNat)
done
lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of k])
+apply (cases m, cases k)
apply (simp add: sumhr hypnat_add hypreal_zero_def)
done
lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: sumhr hypreal_add sumr_add)
done
lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: sumhr hypreal_of_real_def hypreal_mult sumr_mult)
done
lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypnat [of p])
+apply (cases n, cases p)
apply (auto elim!: FreeUltrafilterNat_subset simp
add: hypnat_zero_def sumhr hypreal_add hypnat_less sumr_split_add)
done
@@ -94,8 +89,7 @@
by (drule_tac f1 = f in sumhr_split_add [symmetric], simp)
lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypnat [of m])
+apply (cases n, cases m)
apply (simp add: sumhr hypreal_le hypreal_hrabs sumr_rabs)
done
@@ -109,35 +103,32 @@
done
lemma sumhr_const: "sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat hypreal_mult)
done
lemma sumhr_add_mult_const:
"sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) =
sumhr(0,n,%i. f i + -r)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat
hypreal_mult hypreal_add hypreal_minus sumr_add [symmetric])
done
lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (auto elim: FreeUltrafilterNat_subset
simp add: sumhr hypnat_less hypreal_zero_def)
done
lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: sumhr hypreal_minus sumr_minus)
done
lemma sumhr_shift_bounds:
"sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: sumhr hypnat_add sumr_shift_bounds hypnat_of_nat_eq)
done
@@ -169,7 +160,7 @@
hypnat_of_nat_eq hypreal_of_real_def hypreal_mult)
lemma starfunNat_sumr: "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"
-apply (rule eq_Abs_hypnat [of N])
+apply (cases N)
apply (simp add: hypnat_zero_def starfunNat sumhr)
done
--- a/src/HOL/Hyperreal/HTranscendental.thy Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy Mon Mar 15 10:46:19 2004 +0100
@@ -33,14 +33,14 @@
by (simp add: starfun hypreal_one_num)
lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow
real_sqrt_pow2_iff
simp del: hpowr_Suc realpow_Suc)
done
lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (auto intro: FreeUltrafilterNat_subset real_sqrt_gt_zero_pow2
simp add: hypreal_less starfun hrealpow hypreal_zero_num
simp del: hpowr_Suc realpow_Suc)
@@ -62,8 +62,7 @@
lemma hypreal_sqrt_mult_distrib:
"[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
apply (auto intro: real_sqrt_mult_distrib)
done
@@ -101,7 +100,7 @@
done
lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
apply (auto intro: real_sqrt_gt_zero)
done
@@ -110,7 +109,7 @@
by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
lemma hypreal_sqrt_hrabs [simp]: "( *f* sqrt)(x ^ 2) = abs(x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
done
@@ -122,7 +121,7 @@
lemma hypreal_sqrt_hyperpow_hrabs [simp]:
"( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
done
@@ -142,8 +141,7 @@
done
lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
apply (simp add: starfun hypreal_add hrealpow hypreal_le
del: hpowr_Suc realpow_Suc)
done
@@ -274,8 +272,7 @@
by (auto intro: STAR_exp_Infinitesimal)
lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (cases x, cases y)
apply (simp add: starfun hypreal_add hypreal_mult exp_add)
done
@@ -293,7 +290,7 @@
done
lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
done
@@ -306,7 +303,7 @@
done
lemma starfun_exp_minus: "( *f* exp) (-x) = inverse(( *f* exp) x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
done
@@ -320,7 +317,7 @@
done
lemma starfun_exp_gt_one [simp]: "0 < x ==> 1 < ( *f* exp) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
done
@@ -338,12 +335,12 @@
lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun)
done
lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hypreal_zero_num hypreal_less)
done
@@ -351,22 +348,22 @@
by (auto simp add: starfun)
lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
done
lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
done
lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
done
lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
apply (auto dest: ln_not_eq_zero)
done
@@ -379,13 +376,13 @@
done
lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
apply (simp add: ln_inverse)
done
lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
apply (rule_tac x = "exp u" in exI)
@@ -433,7 +430,7 @@
done
lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
apply (auto intro: ln_less_zero)
done
--- a/src/HOL/Hyperreal/HyperDef.thy Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Mon Mar 15 10:46:19 2004 +0100
@@ -2,9 +2,11 @@
ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
- Description : Construction of hyperreals using ultrafilters
+ Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)
+header{*Construction of Hyperreals Using Ultrafilters*}
+
theory HyperDef = Filter + Real
files ("fuf.ML"): (*Warning: file fuf.ML refers to the name Hyperdef!*)
@@ -233,19 +235,17 @@
text{*Proving that @{term hyprel} is an equivalence relation*}
lemma hyprel_iff: "((X,Y) \<in> hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)"
-by (unfold hyprel_def, fast)
+by (simp add: hyprel_def)
lemma hyprel_refl: "(x,x) \<in> hyprel"
-apply (unfold hyprel_def)
-apply (auto simp add: FreeUltrafilterNat_Nat_set)
-done
+by (simp add: hyprel_def)
lemma hyprel_sym [rule_format (no_asm)]: "(x,y) \<in> hyprel --> (y,x) \<in> hyprel"
by (simp add: hyprel_def eq_commute)
lemma hyprel_trans:
"[|(x,y) \<in> hyprel; (y,z) \<in> hyprel|] ==> (x,z) \<in> hyprel"
-by (unfold hyprel_def, auto, ultra)
+by (simp add: hyprel_def, ultra)
lemma equiv_hyprel: "equiv UNIV hyprel"
apply (simp add: equiv_def refl_def sym_def trans_def hyprel_refl)
@@ -257,7 +257,7 @@
eq_equiv_class_iff [OF equiv_hyprel UNIV_I UNIV_I, simp]
lemma hyprel_in_hypreal [simp]: "hyprel``{x}:hypreal"
-by (unfold hypreal_def hyprel_def quotient_def, blast)
+by (simp add: hypreal_def hyprel_def quotient_def, blast)
lemma inj_on_Abs_hypreal: "inj_on Abs_hypreal hypreal"
apply (rule inj_on_inverseI)
@@ -279,12 +279,10 @@
done
lemma lemma_hyprel_refl [simp]: "x \<in> hyprel `` {x}"
-apply (unfold hyprel_def, safe)
-apply (auto intro!: FreeUltrafilterNat_Nat_set)
-done
+by (simp add: hyprel_def)
lemma hypreal_empty_not_mem [simp]: "{} \<notin> hypreal"
-apply (unfold hypreal_def)
+apply (simp add: hypreal_def)
apply (auto elim!: quotientE equalityCE)
done
@@ -297,53 +295,47 @@
lemma inj_hypreal_of_real: "inj(hypreal_of_real)"
apply (rule inj_onI)
-apply (unfold hypreal_of_real_def)
-apply (drule inj_on_Abs_hypreal [THEN inj_onD])
-apply (rule hyprel_in_hypreal)+
-apply (drule eq_equiv_class)
-apply (rule equiv_hyprel)
-apply (simp_all add: split: split_if_asm)
+apply (simp add: hypreal_of_real_def split: split_if_asm)
done
lemma eq_Abs_hypreal:
- "(!!x y. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
+ "(!!x. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
apply (rule_tac x1=z in Rep_hypreal [unfolded hypreal_def, THEN quotientE])
apply (drule_tac f = Abs_hypreal in arg_cong)
apply (force simp add: Rep_hypreal_inverse)
done
+theorem hypreal_cases [case_names Abs_hypreal, cases type: hypreal]:
+ "(!!x. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
+by (rule eq_Abs_hypreal [of z], blast)
+
subsection{*Hyperreal Addition*}
lemma hypreal_add_congruent2:
"congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})"
-apply (unfold congruent2_def, auto, ultra)
+apply (simp add: congruent2_def, auto, ultra)
done
lemma hypreal_add:
"Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) =
Abs_hypreal(hyprel``{%n. X n + Y n})"
-apply (unfold hypreal_add_def)
+apply (simp add: hypreal_add_def)
apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_add_congruent2])
done
lemma hypreal_add_commute: "(z::hypreal) + w = w + z"
-apply (rule eq_Abs_hypreal [of z])
-apply (rule eq_Abs_hypreal [of w])
+apply (cases z, cases w)
apply (simp add: add_ac hypreal_add)
done
lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"
-apply (rule eq_Abs_hypreal [of z1])
-apply (rule eq_Abs_hypreal [of z2])
-apply (rule eq_Abs_hypreal [of z3])
+apply (cases z1, cases z2, cases z3)
apply (simp add: hypreal_add real_add_assoc)
done
lemma hypreal_add_zero_left: "(0::hypreal) + z = z"
-apply (rule eq_Abs_hypreal [of z])
-apply (simp add: hypreal_zero_def hypreal_add)
-done
+by (cases z, simp add: hypreal_zero_def hypreal_add)
instance hypreal :: plus_ac0
by (intro_classes,
@@ -362,7 +354,7 @@
lemma hypreal_minus:
"- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"
-apply (unfold hypreal_minus_def)
+apply (simp add: hypreal_minus_def)
apply (rule_tac f = Abs_hypreal in arg_cong)
apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse]
UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent])
@@ -375,7 +367,7 @@
done
lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)"
-apply (unfold hypreal_zero_def)
+apply (simp add: hypreal_zero_def)
apply (rule_tac z = z in eq_Abs_hypreal)
apply (simp add: hypreal_minus hypreal_add)
done
@@ -388,62 +380,55 @@
lemma hypreal_mult_congruent2:
"congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})"
-apply (unfold congruent2_def, auto, ultra)
+apply (simp add: congruent2_def, auto, ultra)
done
lemma hypreal_mult:
"Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) =
Abs_hypreal(hyprel``{%n. X n * Y n})"
-apply (unfold hypreal_mult_def)
+apply (simp add: hypreal_mult_def)
apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_mult_congruent2])
done
lemma hypreal_mult_commute: "(z::hypreal) * w = w * z"
-apply (rule eq_Abs_hypreal [of z])
-apply (rule eq_Abs_hypreal [of w])
+apply (cases z, cases w)
apply (simp add: hypreal_mult mult_ac)
done
lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"
-apply (rule eq_Abs_hypreal [of z1])
-apply (rule eq_Abs_hypreal [of z2])
-apply (rule eq_Abs_hypreal [of z3])
+apply (cases z1, cases z2, cases z3)
apply (simp add: hypreal_mult mult_assoc)
done
lemma hypreal_mult_1: "(1::hypreal) * z = z"
-apply (unfold hypreal_one_def)
+apply (simp add: hypreal_one_def)
apply (rule_tac z = z in eq_Abs_hypreal)
apply (simp add: hypreal_mult)
done
lemma hypreal_add_mult_distrib:
"((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"
-apply (rule eq_Abs_hypreal [of z1])
-apply (rule eq_Abs_hypreal [of z2])
-apply (rule eq_Abs_hypreal [of w])
+apply (cases z1, cases z2, cases w)
apply (simp add: hypreal_mult hypreal_add left_distrib)
done
text{*one and zero are distinct*}
lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)"
-apply (unfold hypreal_zero_def hypreal_one_def)
-apply (auto simp add: real_zero_not_eq_one)
-done
+by (simp add: hypreal_zero_def hypreal_one_def)
subsection{*Multiplicative Inverse on @{typ hypreal} *}
lemma hypreal_inverse_congruent:
"congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})"
-apply (unfold congruent_def)
+apply (simp add: congruent_def)
apply (auto, ultra)
done
lemma hypreal_inverse:
"inverse (Abs_hypreal(hyprel``{%n. X n})) =
Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})"
-apply (unfold hypreal_inverse_def)
+apply (simp add: hypreal_inverse_def)
apply (rule_tac f = Abs_hypreal in arg_cong)
apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse]
UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent])
@@ -451,8 +436,8 @@
lemma hypreal_mult_inverse:
"x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
-apply (unfold hypreal_one_def hypreal_zero_def)
-apply (rule eq_Abs_hypreal [of x])
+apply (simp add: hypreal_one_def hypreal_zero_def)
+apply (cases x)
apply (simp add: hypreal_inverse hypreal_mult)
apply (drule FreeUltrafilterNat_Compl_mem)
apply (blast intro!: right_inverse FreeUltrafilterNat_subset)
@@ -492,25 +477,22 @@
lemma hypreal_le:
"(Abs_hypreal(hyprel``{%n. X n}) \<le> Abs_hypreal(hyprel``{%n. Y n})) =
({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-apply (unfold hypreal_le_def)
+apply (simp add: hypreal_le_def)
apply (auto intro!: lemma_hyprel_refl, ultra)
done
lemma hypreal_le_refl: "w \<le> (w::hypreal)"
-apply (rule eq_Abs_hypreal [of w])
+apply (cases w)
apply (simp add: hypreal_le)
done
lemma hypreal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypreal)"
-apply (rule eq_Abs_hypreal [of i])
-apply (rule eq_Abs_hypreal [of j])
-apply (rule eq_Abs_hypreal [of k])
+apply (cases i, cases j, cases k)
apply (simp add: hypreal_le, ultra)
done
lemma hypreal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypreal)"
-apply (rule eq_Abs_hypreal [of z])
-apply (rule eq_Abs_hypreal [of w])
+apply (cases z, cases w)
apply (simp add: hypreal_le, ultra)
done
@@ -526,8 +508,7 @@
(* Axiom 'linorder_linear' of class 'linorder': *)
lemma hypreal_le_linear: "(z::hypreal) \<le> w | w \<le> z"
-apply (rule eq_Abs_hypreal [of z])
-apply (rule eq_Abs_hypreal [of w])
+apply (cases z, cases w)
apply (auto simp add: hypreal_le, ultra)
done
@@ -538,16 +519,12 @@
by (auto simp add: order_less_irrefl)
lemma hypreal_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypreal)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of z])
+apply (cases x, cases y, cases z)
apply (auto simp add: hypreal_le hypreal_add)
done
lemma hypreal_mult_less_mono2: "[| (0::hypreal)<z; x<y |] ==> z*x<z*y"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (rule eq_Abs_hypreal [of z])
+apply (cases x, cases y, cases z)
apply (auto simp add: hypreal_zero_def hypreal_le hypreal_mult
linorder_not_le [symmetric], ultra)
done
@@ -630,25 +607,25 @@
lemma hypreal_of_real_add [simp]:
"hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
-apply (unfold hypreal_of_real_def)
+apply (simp add: hypreal_of_real_def)
apply (simp add: hypreal_add left_distrib)
done
lemma hypreal_of_real_mult [simp]:
"hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z"
-apply (unfold hypreal_of_real_def)
+apply (simp add: hypreal_of_real_def)
apply (simp add: hypreal_mult right_distrib)
done
lemma hypreal_of_real_one [simp]: "hypreal_of_real 1 = (1::hypreal)"
-by (unfold hypreal_of_real_def hypreal_one_def, simp)
+by (simp add: hypreal_of_real_def hypreal_one_def)
lemma hypreal_of_real_zero [simp]: "hypreal_of_real 0 = 0"
-by (unfold hypreal_of_real_def hypreal_zero_def, simp)
+by (simp add: hypreal_of_real_def hypreal_zero_def)
lemma hypreal_of_real_le_iff [simp]:
"(hypreal_of_real w \<le> hypreal_of_real z) = (w \<le> z)"
-apply (unfold hypreal_le_def hypreal_of_real_def, auto)
+apply (simp add: hypreal_le_def hypreal_of_real_def, auto)
apply (rule_tac [2] x = "%n. w" in exI, safe)
apply (rule_tac [3] x = "%n. z" in exI, auto)
apply (rule FreeUltrafilterNat_P, ultra)
@@ -713,7 +690,7 @@
by (simp add: hypreal_one_def [THEN meta_eq_to_obj_eq, symmetric])
lemma hypreal_omega_gt_zero [simp]: "0 < omega"
-apply (unfold omega_def)
+apply (simp add: omega_def)
apply (auto simp add: hypreal_less hypreal_zero_num)
done
@@ -738,9 +715,7 @@
subsection{*Existence of Infinite Hyperreal Number*}
lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal"
-apply (unfold omega_def)
-apply (rule Rep_hypreal)
-done
+by (simp add: omega_def)
text{*Existence of infinite number not corresponding to any real number.
Use assumption that member @{term FreeUltrafilterNat} is not finite.*}
@@ -757,7 +732,7 @@
lemma not_ex_hypreal_of_real_eq_omega:
"~ (\<exists>x. hypreal_of_real x = omega)"
-apply (unfold omega_def hypreal_of_real_def)
+apply (simp add: omega_def hypreal_of_real_def)
apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric]
lemma_finite_omega_set [THEN FreeUltrafilterNat_finite])
done
@@ -778,7 +753,7 @@
lemma not_ex_hypreal_of_real_eq_epsilon:
"~ (\<exists>x. hypreal_of_real x = epsilon)"
-apply (unfold epsilon_def hypreal_of_real_def)
+apply (simp add: epsilon_def hypreal_of_real_def)
apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
done
@@ -786,7 +761,7 @@
by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto)
lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
-by (unfold epsilon_def hypreal_zero_def, auto)
+by (simp add: epsilon_def hypreal_zero_def)
lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
by (simp add: hypreal_inverse omega_def epsilon_def)
--- a/src/HOL/Hyperreal/HyperNat.thy Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Mon Mar 15 10:46:19 2004 +0100
@@ -63,19 +63,18 @@
lemma hypnatrel_iff:
"((X,Y) \<in> hypnatrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
-apply (unfold hypnatrel_def, fast)
+apply (simp add: hypnatrel_def)
done
lemma hypnatrel_refl: "(x,x) \<in> hypnatrel"
-by (unfold hypnatrel_def, auto)
+by (simp add: hypnatrel_def)
lemma hypnatrel_sym: "(x,y) \<in> hypnatrel ==> (y,x) \<in> hypnatrel"
by (auto simp add: hypnatrel_def eq_commute)
lemma hypnatrel_trans [rule_format (no_asm)]:
"(x,y) \<in> hypnatrel --> (y,z) \<in> hypnatrel --> (x,z) \<in> hypnatrel"
-apply (unfold hypnatrel_def, auto, ultra)
-done
+by (auto simp add: hypnatrel_def, ultra)
lemma equiv_hypnatrel:
"equiv UNIV hypnatrel"
@@ -88,7 +87,7 @@
eq_equiv_class_iff [OF equiv_hypnatrel UNIV_I UNIV_I, simp]
lemma hypnatrel_in_hypnat [simp]: "hypnatrel``{x}:hypnat"
-by (unfold hypnat_def hypnatrel_def quotient_def, blast)
+by (simp add: hypnat_def hypnatrel_def quotient_def, blast)
lemma inj_on_Abs_hypnat: "inj_on Abs_hypnat hypnat"
apply (rule inj_on_inverseI)
@@ -114,7 +113,7 @@
declare lemma_hypnatrel_refl [simp]
lemma hypnat_empty_not_mem: "{} \<notin> hypnat"
-apply (unfold hypnat_def)
+apply (simp add: hypnat_def)
apply (auto elim!: quotientE equalityCE)
done
@@ -133,11 +132,15 @@
apply (force simp add: Rep_hypnat_inverse)
done
+theorem hypnat_cases [case_names Abs_hypnat, cases type: hypnat]:
+ "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
+by (rule eq_Abs_hypnat [of z], blast)
+
subsection{*Hypernat Addition*}
lemma hypnat_add_congruent2:
"congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
-apply (unfold congruent2_def, auto, ultra)
+apply (simp add: congruent2_def, auto, ultra)
done
lemma hypnat_add:
@@ -146,20 +149,17 @@
by (simp add: hypnat_add_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_add_congruent2])
lemma hypnat_add_commute: "(z::hypnat) + w = w + z"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
apply (simp add: add_ac hypnat_add)
done
lemma hypnat_add_assoc: "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)"
-apply (rule eq_Abs_hypnat [of z1])
-apply (rule eq_Abs_hypnat [of z2])
-apply (rule eq_Abs_hypnat [of z3])
+apply (cases z1, cases z2, cases z3)
apply (simp add: hypnat_add nat_add_assoc)
done
lemma hypnat_add_zero_left: "(0::hypnat) + z = z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: hypnat_zero_def hypnat_add)
done
@@ -174,7 +174,7 @@
lemma hypnat_minus_congruent2:
"congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
-apply (unfold congruent2_def, auto, ultra)
+apply (simp add: congruent2_def, auto, ultra)
done
lemma hypnat_minus:
@@ -183,29 +183,26 @@
by (simp add: hypnat_minus_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_minus_congruent2])
lemma hypnat_minus_zero: "z - z = (0::hypnat)"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: hypnat_zero_def hypnat_minus)
done
lemma hypnat_diff_0_eq_0: "(0::hypnat) - n = 0"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (simp add: hypnat_minus hypnat_zero_def)
done
declare hypnat_minus_zero [simp] hypnat_diff_0_eq_0 [simp]
lemma hypnat_add_is_0: "(m+n = (0::hypnat)) = (m=0 & n=0)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (auto intro: FreeUltrafilterNat_subset dest: FreeUltrafilterNat_Int simp add: hypnat_zero_def hypnat_add)
done
declare hypnat_add_is_0 [iff]
lemma hypnat_diff_diff_left: "(i::hypnat) - j - k = i - (j+k)"
-apply (rule eq_Abs_hypnat [of i])
-apply (rule eq_Abs_hypnat [of j])
-apply (rule eq_Abs_hypnat [of k])
+apply (cases i, cases j, cases k)
apply (simp add: hypnat_minus hypnat_add diff_diff_left)
done
@@ -213,23 +210,19 @@
by (simp add: hypnat_diff_diff_left hypnat_add_commute)
lemma hypnat_diff_add_inverse: "((n::hypnat) + m) - n = m"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: hypnat_minus hypnat_add)
done
declare hypnat_diff_add_inverse [simp]
lemma hypnat_diff_add_inverse2: "((m::hypnat) + n) - n = m"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: hypnat_minus hypnat_add)
done
declare hypnat_diff_add_inverse2 [simp]
lemma hypnat_diff_cancel: "((k::hypnat) + m) - (k+n) = m - n"
-apply (rule eq_Abs_hypnat [of k])
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases k, cases m, cases n)
apply (simp add: hypnat_minus hypnat_add)
done
declare hypnat_diff_cancel [simp]
@@ -239,8 +232,7 @@
declare hypnat_diff_cancel2 [simp]
lemma hypnat_diff_add_0: "(n::hypnat) - (n+m) = (0::hypnat)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: hypnat_zero_def hypnat_minus hypnat_add)
done
declare hypnat_diff_add_0 [simp]
@@ -250,7 +242,7 @@
lemma hypnat_mult_congruent2:
"congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
-by (unfold congruent2_def, auto, ultra)
+by (simp add: congruent2_def, auto, ultra)
lemma hypnat_mult:
"Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) =
@@ -258,27 +250,22 @@
by (simp add: hypnat_mult_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_mult_congruent2])
lemma hypnat_mult_commute: "(z::hypnat) * w = w * z"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
apply (simp add: hypnat_mult mult_ac)
done
lemma hypnat_mult_assoc: "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)"
-apply (rule eq_Abs_hypnat [of z1])
-apply (rule eq_Abs_hypnat [of z2])
-apply (rule eq_Abs_hypnat [of z3])
+apply (cases z1, cases z2, cases z3)
apply (simp add: hypnat_mult mult_assoc)
done
lemma hypnat_mult_1: "(1::hypnat) * z = z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: hypnat_mult hypnat_one_def)
done
lemma hypnat_diff_mult_distrib: "((m::hypnat) - n) * k = (m * k) - (n * k)"
-apply (rule eq_Abs_hypnat [of k])
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases k, cases m, cases n)
apply (simp add: hypnat_mult hypnat_minus diff_mult_distrib)
done
@@ -286,9 +273,7 @@
by (simp add: hypnat_diff_mult_distrib hypnat_mult_commute [of k])
lemma hypnat_add_mult_distrib: "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)"
-apply (rule eq_Abs_hypnat [of z1])
-apply (rule eq_Abs_hypnat [of z2])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z1, cases z2, cases w)
apply (simp add: hypnat_mult hypnat_add add_mult_distrib)
done
@@ -324,25 +309,22 @@
lemma hypnat_le:
"(Abs_hypnat(hypnatrel``{%n. X n}) \<le> Abs_hypnat(hypnatrel``{%n. Y n})) =
({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-apply (unfold hypnat_le_def)
+apply (simp add: hypnat_le_def)
apply (auto intro!: lemma_hypnatrel_refl, ultra)
done
lemma hypnat_le_refl: "w \<le> (w::hypnat)"
-apply (rule eq_Abs_hypnat [of w])
+apply (cases w)
apply (simp add: hypnat_le)
done
lemma hypnat_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypnat)"
-apply (rule eq_Abs_hypnat [of i])
-apply (rule eq_Abs_hypnat [of j])
-apply (rule eq_Abs_hypnat [of k])
+apply (cases i, cases j, cases k)
apply (simp add: hypnat_le, ultra)
done
lemma hypnat_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypnat)"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
apply (simp add: hypnat_le, ultra)
done
@@ -357,8 +339,7 @@
(* Axiom 'linorder_linear' of class 'linorder': *)
lemma hypnat_le_linear: "(z::hypnat) \<le> w | w \<le> z"
-apply (rule eq_Abs_hypnat [of z])
-apply (rule eq_Abs_hypnat [of w])
+apply (cases z, cases w)
apply (auto simp add: hypnat_le, ultra)
done
@@ -366,16 +347,12 @@
by (intro_classes, rule hypnat_le_linear)
lemma hypnat_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypnat)"
-apply (rule eq_Abs_hypnat [of x])
-apply (rule eq_Abs_hypnat [of y])
-apply (rule eq_Abs_hypnat [of z])
+apply (cases x, cases y, cases z)
apply (auto simp add: hypnat_le hypnat_add)
done
lemma hypnat_mult_less_mono2: "[| (0::hypnat)<z; x<y |] ==> z*x<z*y"
-apply (rule eq_Abs_hypnat [of x])
-apply (rule eq_Abs_hypnat [of y])
-apply (rule eq_Abs_hypnat [of z])
+apply (cases x, cases y, cases z)
apply (simp add: hypnat_zero_def hypnat_mult linorder_not_le [symmetric])
apply (auto simp add: hypnat_le, ultra)
done
@@ -396,19 +373,17 @@
qed
lemma hypnat_le_zero_cancel [iff]: "(n \<le> (0::hypnat)) = (n = 0)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (simp add: hypnat_zero_def hypnat_le)
done
lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (auto simp add: hypnat_zero_def hypnat_mult, ultra+)
done
lemma hypnat_diff_is_0_eq [simp]: "((m::hypnat) - n = 0) = (m \<le> n)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: hypnat_le hypnat_minus hypnat_zero_def)
done
@@ -424,19 +399,18 @@
done
lemma hypnat_not_less0 [iff]: "~ n < (0::hypnat)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (auto simp add: hypnat_zero_def hypnat_less)
done
lemma hypnat_less_one [iff]:
"(n < (1::hypnat)) = (n=0)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (auto simp add: hypnat_zero_def hypnat_one_def hypnat_less)
done
lemma hypnat_add_diff_inverse: "~ m<n ==> n+(m-n) = (m::hypnat)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: hypnat_minus hypnat_add hypnat_less split: nat_diff_split, ultra)
done
@@ -484,7 +458,7 @@
next
case False
thus ?thesis
- by (auto simp add: linorder_not_less dest: order_le_less_trans);
+ by (auto simp add: linorder_not_less dest: order_le_less_trans)
qed
@@ -563,15 +537,13 @@
done
lemma Nats_diff [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> (a-b :: hypnat) \<in> Nats"
-apply (auto simp add: of_nat_eq_add Nats_def split: hypnat_diff_split)
-done
+by (auto simp add: of_nat_eq_add Nats_def split: hypnat_diff_split)
lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
apply (insert finite_atMost [of m])
apply (simp add: atMost_def)
apply (drule FreeUltrafilterNat_finite)
-apply (drule FreeUltrafilterNat_Compl_mem)
-apply ultra
+apply (drule FreeUltrafilterNat_Compl_mem, ultra)
done
lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
@@ -581,7 +553,7 @@
lemma hypnat_of_nat_eq:
"hypnat_of_nat m = Abs_hypnat(hypnatrel``{%n::nat. m})"
apply (induct m)
-apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add);
+apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add)
done
lemma SHNat_eq: "Nats = {n. \<exists>N. n = hypnat_of_nat N}"
@@ -599,8 +571,7 @@
(* Infinite hypernatural not in embedded Nats *)
lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
-apply (blast dest: hypnat_omega_gt_SHNat)
-done
+by (blast dest: hypnat_omega_gt_SHNat)
lemma hypnat_of_nat_less_whn [simp]: "hypnat_of_nat n < whn"
apply (insert hypnat_omega_gt_SHNat [of "hypnat_of_nat n"])
@@ -657,7 +628,7 @@
lemma HNatInfinite_FreeUltrafilterNat:
"x \<in> HNatInfinite
==> \<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
apply (rule bexI [OF _ lemma_hypnatrel_refl], clarify)
apply (auto simp add: hypnat_of_nat_def hypnat_less)
@@ -666,7 +637,7 @@
lemma FreeUltrafilterNat_HNatInfinite:
"\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat
==> x \<in> HNatInfinite"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
apply (drule spec, ultra, auto)
done
@@ -708,8 +679,7 @@
lemma HNatInfinite_SHNat_add:
"[| x \<in> HNatInfinite; y \<in> Nats |] ==> x + y \<in> HNatInfinite"
apply (auto simp add: HNatInfinite_not_Nats_iff)
-apply (drule_tac a = "x + y" in Nats_diff)
-apply (auto );
+apply (drule_tac a = "x + y" in Nats_diff, auto)
done
lemma HNatInfinite_Nats_imp_less: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> y < x"
@@ -764,8 +734,7 @@
lemma hypreal_of_hypnat_inject [simp]:
"(hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (auto simp add: hypreal_of_hypnat)
done
@@ -777,22 +746,19 @@
lemma hypreal_of_hypnat_add [simp]:
"hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: hypreal_of_hypnat hypreal_add hypnat_add real_of_nat_add)
done
lemma hypreal_of_hypnat_mult [simp]:
"hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: hypreal_of_hypnat hypreal_mult hypnat_mult real_of_nat_mult)
done
lemma hypreal_of_hypnat_less_iff [simp]:
"(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypnat [of n])
+apply (cases m, cases n)
apply (simp add: hypreal_of_hypnat hypreal_less hypnat_less)
done
@@ -801,13 +767,13 @@
declare hypreal_of_hypnat_eq_zero_iff [simp]
lemma hypreal_of_hypnat_ge_zero [simp]: "0 \<le> hypreal_of_hypnat n"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (simp add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
done
lemma HNatInfinite_inverse_Infinitesimal [simp]:
"n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (auto simp add: hypreal_of_hypnat hypreal_inverse
HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
--- a/src/HOL/Hyperreal/HyperPow.thy Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy Mon Mar 15 10:46:19 2004 +0100
@@ -146,78 +146,62 @@
lemma hyperpow_not_zero [rule_format (no_asm)]:
"r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
-apply (simp (no_asm) add: hypreal_zero_def)
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
+apply (simp (no_asm) add: hypreal_zero_def, cases n, cases r)
apply (auto simp add: hyperpow)
apply (drule FreeUltrafilterNat_Compl_mem, ultra)
done
lemma hyperpow_inverse:
"r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
-apply (simp (no_asm) add: hypreal_zero_def)
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
+apply (simp (no_asm) add: hypreal_zero_def, cases n, cases r)
apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
apply (rule FreeUltrafilterNat_subset)
apply (auto dest: realpow_not_zero intro: power_inverse)
done
lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
+apply (cases n, cases r)
apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
done
lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypnat [of m])
-apply (rule eq_Abs_hypreal [of r])
+apply (cases n, cases m, cases r)
apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
done
lemma hyperpow_one: "r pow (1::hypnat) = r"
-apply (unfold hypnat_one_def)
-apply (rule eq_Abs_hypreal [of r])
+apply (unfold hypnat_one_def, cases r)
apply (auto simp add: hyperpow)
done
declare hyperpow_one [simp]
lemma hyperpow_two:
"r pow ((1::hypnat) + (1::hypnat)) = r * r"
-apply (unfold hypnat_one_def)
-apply (rule eq_Abs_hypreal [of r])
+apply (unfold hypnat_one_def, cases r)
apply (auto simp add: hyperpow hypnat_add hypreal_mult)
done
lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
-apply (simp add: hypreal_zero_def)
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
+apply (simp add: hypreal_zero_def, cases n, cases r)
apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
simp add: hyperpow hypreal_less hypreal_le)
done
lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
-apply (simp add: hypreal_zero_def)
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
+apply (simp add: hypreal_zero_def, cases n, cases r)
apply (auto elim!: FreeUltrafilterNat_subset zero_le_power
simp add: hyperpow hypreal_le)
done
lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
-apply (simp add: hypreal_zero_def)
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
+apply (simp add: hypreal_zero_def, cases n, cases x, cases y)
apply (auto simp add: hyperpow hypreal_le hypreal_less)
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
apply (auto intro: power_mono)
done
lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (auto simp add: hypreal_one_def hyperpow)
done
declare hyperpow_eq_one [simp]
@@ -225,15 +209,13 @@
lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
apply simp
-apply (rule eq_Abs_hypnat [of n])
+apply (cases n)
apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
done
declare hrabs_hyperpow_minus_one [simp]
lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypreal [of r])
-apply (rule eq_Abs_hypreal [of s])
+apply (cases n, cases r, cases s)
apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
done
@@ -272,8 +254,7 @@
"-1 pow ((1 + 1)*n) = (1::hypreal)"
apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
apply simp
-apply (simp only: hypreal_one_def)
-apply (rule eq_Abs_hypnat [of n])
+apply (simp only: hypreal_one_def, cases n)
apply (auto simp add: nat_mult_2 [symmetric] hyperpow hypnat_add hypreal_minus
left_distrib)
done
@@ -281,9 +262,7 @@
lemma hyperpow_less_le:
"[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-apply (rule eq_Abs_hypnat [of n])
-apply (rule eq_Abs_hypnat [of N])
-apply (rule eq_Abs_hypreal [of r])
+apply (cases n, cases N, cases r)
apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less
hypreal_zero_def hypreal_one_def)
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
@@ -338,7 +317,7 @@
lemma hrealpow_hyperpow_Infinitesimal_iff:
"(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
done
--- a/src/HOL/Hyperreal/NSA.thy Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Mon Mar 15 10:46:19 2004 +0100
@@ -1848,7 +1848,7 @@
lemma HFinite_FreeUltrafilterNat:
"x \<in> HFinite
==> \<exists>X \<in> Rep_hypreal x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x]
hypreal_less SReal_iff hypreal_minus hypreal_of_real_def)
apply (rule_tac x=x in bexI)
@@ -1859,7 +1859,7 @@
"\<exists>X \<in> Rep_hypreal x.
\<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
==> x \<in> HFinite"
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x])
apply (rule_tac x = "hypreal_of_real u" in bexI)
apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def, ultra+)
@@ -1954,7 +1954,7 @@
\<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat"
apply (simp add: Infinitesimal_def)
apply (auto simp add: abs_less_iff minus_less_iff [of x])
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (auto, rule bexI [OF _ lemma_hyprel_refl], safe)
apply (drule hypreal_of_real_less_iff [THEN iffD2])
apply (drule_tac x = "hypreal_of_real u" in bspec, auto)
@@ -1966,7 +1966,7 @@
\<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
==> x \<in> Infinitesimal"
apply (simp add: Infinitesimal_def)
-apply (rule eq_Abs_hypreal [of x])
+apply (cases x)
apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x])
apply (auto simp add: SReal_iff)
apply (drule_tac [!] x=y in spec)
--- a/src/HOL/Hyperreal/NatStar.thy Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy Mon Mar 15 10:46:19 2004 +0100
@@ -213,13 +213,13 @@
lemma starfunNat_mult:
"( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat hypreal_mult)
done
lemma starfunNat2_mult:
"( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat2 hypnat_mult)
done
@@ -227,19 +227,19 @@
lemma starfunNat_add:
"( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat hypreal_add)
done
lemma starfunNat2_add:
"( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat2 hypnat_add)
done
lemma starfunNat2_minus:
"( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat2 hypnat_minus)
done
@@ -285,23 +285,23 @@
text{*NS extension of constant function*}
lemma starfunNat_const_fun [simp]: "( *fNat* (%x. k)) z = hypreal_of_real k"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat hypreal_of_real_def)
done
lemma starfunNat2_const_fun [simp]: "( *fNat2* (%x. k)) z = hypnat_of_nat k"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat2 hypnat_of_nat_eq)
done
lemma starfunNat_minus: "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
apply (simp add: starfunNat hypreal_minus)
done
lemma starfunNat_inverse:
"inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
apply (simp add: starfunNat hypreal_inverse)
done
@@ -346,27 +346,27 @@
lemma starfunNat_shift_one:
"( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))"
-apply (rule eq_Abs_hypnat [of N])
+apply (cases N)
apply (simp add: starfunNat hypnat_one_def hypnat_add)
done
text{*Nonstandard extension with absolute value*}
lemma starfunNat_rabs: "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)"
-apply (rule eq_Abs_hypnat [of N])
+apply (cases N)
apply (simp add: starfunNat hypreal_hrabs)
done
text{*The hyperpow function as a nonstandard extension of realpow*}
lemma starfunNat_pow: "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
-apply (rule eq_Abs_hypnat [of N])
+apply (cases N)
apply (simp add: hyperpow hypreal_of_real_def starfunNat)
done
lemma starfunNat_pow2:
"( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m"
-apply (rule eq_Abs_hypnat [of N])
+apply (cases N)
apply (simp add: hyperpow hypnat_of_nat_eq starfunNat)
done
@@ -411,7 +411,7 @@
lemma starfunNat_n_mult:
"( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat_n hypreal_mult)
done
@@ -419,7 +419,7 @@
lemma starfunNat_n_add:
"( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat_n hypreal_add)
done
@@ -427,7 +427,7 @@
lemma starfunNat_n_add_minus:
"( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat_n hypreal_minus hypreal_add)
done
@@ -436,12 +436,12 @@
lemma starfunNat_n_const_fun [simp]:
"( *fNatn* (%i x. k)) z = hypreal_of_real k"
-apply (rule eq_Abs_hypnat [of z])
+apply (cases z)
apply (simp add: starfunNat_n hypreal_of_real_def)
done
lemma starfunNat_n_minus: "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x"
-apply (rule eq_Abs_hypnat [of x])
+apply (cases x)
apply (simp add: starfunNat_n hypreal_minus)
done
--- a/src/HOL/Hyperreal/Star.thy Mon Mar 15 10:46:01 2004 +0100
+++ b/src/HOL/Hyperreal/Star.thy Mon Mar 15 10:46:19 2004 +0100
@@ -1,8 +1,7 @@
(* Title : Star.thy
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
- Description : defining *-transforms in NSA which extends sets of reals,
- and real=>real functions
+ Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
*)
header{*Star-Transforms in Non-Standard Analysis*}
@@ -12,30 +11,30 @@
constdefs
(* nonstandard extension of sets *)
starset :: "real set => hypreal set" ("*s* _" [80] 80)
- "*s* A == {x. ALL X: Rep_hypreal(x). {n::nat. X n : A}: FreeUltrafilterNat}"
+ "*s* A == {x. \<forall>X \<in> Rep_hypreal(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}"
(* internal sets *)
starset_n :: "(nat => real set) => hypreal set" ("*sn* _" [80] 80)
- "*sn* As == {x. ALL X: Rep_hypreal(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"
+ "*sn* As == {x. \<forall>X \<in> Rep_hypreal(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"
InternalSets :: "hypreal set set"
- "InternalSets == {X. EX As. X = *sn* As}"
+ "InternalSets == {X. \<exists>As. X = *sn* As}"
(* nonstandard extension of function *)
is_starext :: "[hypreal => hypreal, real => real] => bool"
- "is_starext F f == (ALL x y. EX X: Rep_hypreal(x). EX Y: Rep_hypreal(y).
+ "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_hypreal(x). \<exists>Y \<in> Rep_hypreal(y).
((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
starfun :: "(real => real) => hypreal => hypreal" ("*f* _" [80] 80)
- "*f* f == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel``{%n. f(X n)}))"
+ "*f* f == (%x. Abs_hypreal(\<Union>X \<in> Rep_hypreal(x). hyprel``{%n. f(X n)}))"
(* internal functions *)
starfun_n :: "(nat => (real => real)) => hypreal => hypreal"
("*fn* _" [80] 80)
- "*fn* F == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel``{%n. (F n)(X n)}))"
+ "*fn* F == (%x. Abs_hypreal(\<Union>X \<in> Rep_hypreal(x). hyprel``{%n. (F n)(X n)}))"
InternalFuns :: "(hypreal => hypreal) set"
- "InternalFuns == {X. EX F. X = *fn* F}"
+ "InternalFuns == {X. \<exists>F. X = *fn* F}"
@@ -47,7 +46,7 @@
referee for the JCM Paper: let f(x) be least y such
that Q(x,y)
*)
-lemma no_choice: "ALL x. EX y. Q x y ==> EX (f :: nat => nat). ALL x. Q x (f x)"
+lemma no_choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>(f :: nat => nat). \<forall>x. Q x (f x)"
apply (rule_tac x = "%x. LEAST y. Q x y" in exI)
apply (blast intro: LeastI)
done
@@ -57,20 +56,15 @@
------------------------------------------------------------*)
lemma STAR_real_set: "*s*(UNIV::real set) = (UNIV::hypreal set)"
-
-apply (unfold starset_def, auto)
-done
+by (simp add: starset_def)
declare STAR_real_set [simp]
lemma STAR_empty_set: "*s* {} = {}"
-apply (unfold starset_def, safe)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (drule_tac x = "%n. xa n" in bspec, auto)
-done
+by (simp add: starset_def)
declare STAR_empty_set [simp]
lemma STAR_Un: "*s* (A Un B) = *s* A Un *s* B"
-apply (unfold starset_def, auto)
+apply (auto simp add: starset_def)
prefer 3 apply (blast intro: FreeUltrafilterNat_subset)
prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
apply (drule FreeUltrafilterNat_Compl_mem)
@@ -79,7 +73,7 @@
done
lemma STAR_Int: "*s* (A Int B) = *s* A Int *s* B"
-apply (unfold starset_def, auto)
+apply (simp add: starset_def, auto)
prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset)
apply (blast intro: FreeUltrafilterNat_subset)+
done
@@ -98,23 +92,23 @@
by (auto simp add: Diff_eq STAR_Int STAR_Compl)
lemma STAR_subset: "A <= B ==> *s* A <= *s* B"
-apply (unfold starset_def)
+apply (simp add: starset_def)
apply (blast intro: FreeUltrafilterNat_subset)+
done
-lemma STAR_mem: "a : A ==> hypreal_of_real a : *s* A"
-apply (unfold starset_def hypreal_of_real_def)
+lemma STAR_mem: "a \<in> A ==> hypreal_of_real a : *s* A"
+apply (simp add: starset_def hypreal_of_real_def)
apply (auto intro: FreeUltrafilterNat_subset)
done
lemma STAR_hypreal_of_real_image_subset: "hypreal_of_real ` A <= *s* A"
-apply (unfold starset_def)
+apply (simp add: starset_def)
apply (auto simp add: hypreal_of_real_def)
apply (blast intro: FreeUltrafilterNat_subset)
done
lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
-apply (unfold starset_def)
+apply (simp add: starset_def)
apply (auto simp add: hypreal_of_real_def SReal_def)
apply (simp add: hypreal_of_real_def [symmetric])
apply (rule imageI, rule ccontr)
@@ -123,21 +117,21 @@
prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
done
-lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A ==> ALL y: A. x \<noteq> hypreal_of_real y"
+lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A ==> \<forall>y \<in> A. x \<noteq> hypreal_of_real y"
by auto
lemma lemma_Compl_eq: "- {n. X n = xa} = {n. X n \<noteq> xa}"
by auto
lemma STAR_real_seq_to_hypreal:
- "ALL n. (X n) \<notin> M
+ "\<forall>n. (X n) \<notin> M
==> Abs_hypreal(hyprel``{X}) \<notin> *s* M"
-apply (unfold starset_def)
-apply (auto, rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (simp add: starset_def)
+apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
done
lemma STAR_singleton: "*s* {x} = {hypreal_of_real x}"
-apply (unfold starset_def)
+apply (simp add: starset_def)
apply (auto simp add: hypreal_of_real_def)
apply (rule_tac z = xa in eq_Abs_hypreal)
apply (auto intro: FreeUltrafilterNat_subset)
@@ -157,11 +151,8 @@
sequence) as a special case of an internal set
-----------------------------------------------------------------*)
-lemma starset_n_starset:
- "ALL n. (As n = A) ==> *sn* As = *s* A"
-
-apply (unfold starset_n_def starset_def, auto)
-done
+lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
+by (simp add: starset_n_def starset_def)
(*----------------------------------------------------------------*)
@@ -173,11 +164,8 @@
(* constant sequence) as a special case of an internal function *)
(*----------------------------------------------------------------*)
-lemma starfun_n_starfun:
- "ALL n. (F n = f) ==> *fn* F = *f* f"
-
-apply (unfold starfun_n_def starfun_def, auto)
-done
+lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f"
+by (simp add: starfun_n_def starfun_def)
(*
@@ -193,7 +181,7 @@
lemma hrabs_is_starext_rabs: "is_starext abs abs"
-apply (unfold is_starext_def, safe)
+apply (simp add: is_starext_def, safe)
apply (rule_tac z = x in eq_Abs_hypreal)
apply (rule_tac z = y in eq_Abs_hypreal, auto)
apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
@@ -202,7 +190,7 @@
apply (arith | ultra)+
done
-lemma Rep_hypreal_FreeUltrafilterNat: "[| X: Rep_hypreal z; Y: Rep_hypreal z |]
+lemma Rep_hypreal_FreeUltrafilterNat: "[| X \<in> Rep_hypreal z; Y \<in> Rep_hypreal z |]
==> {n. X n = Y n} : FreeUltrafilterNat"
apply (rule_tac z = z in eq_Abs_hypreal)
apply (auto, ultra)
@@ -213,12 +201,12 @@
-----------------------------------------------------------------------*)
lemma starfun_congruent: "congruent hyprel (%X. hyprel``{%n. f (X n)})"
-by (unfold congruent_def, auto, ultra)
+by (simp add: congruent_def, auto, ultra)
lemma starfun:
"( *f* f) (Abs_hypreal(hyprel``{%n. X n})) =
Abs_hypreal(hyprel `` {%n. f (X n)})"
-apply (unfold starfun_def)
+apply (simp add: starfun_def)
apply (rule_tac f = Abs_hypreal in arg_cong)
apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse]
UN_equiv_class [OF equiv_hyprel starfun_congruent])
@@ -260,8 +248,7 @@
lemma starfun_diff:
"( *f* f) xa - ( *f* g) xa = ( *f* (%x. f x - g x)) xa"
-apply (unfold hypreal_diff_def real_diff_def)
-apply (rule starfun_add_minus)
+apply (simp add: diff_minus)
done
declare starfun_diff [symmetric, simp]
@@ -276,7 +263,7 @@
done
lemma starfun_o: "( *f* f) o ( *f* g) = ( *f* (f o g))"
-apply (unfold o_def)
+apply (simp add: o_def)
apply (simp (no_asm) add: starfun_o2)
done
@@ -311,7 +298,7 @@
lemma is_starext_starfun: "is_starext ( *f* f) f"
-apply (unfold is_starext_def, auto)
+apply (simp add: is_starext_def, auto)
apply (rule_tac z = x in eq_Abs_hypreal)
apply (rule_tac z = y in eq_Abs_hypreal)
apply (auto intro!: bexI simp add: starfun)
@@ -323,7 +310,7 @@
lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
-apply (unfold is_starext_def)
+apply (simp add: is_starext_def)
apply (rule ext)
apply (rule_tac z = x in eq_Abs_hypreal)
apply (drule_tac x = x in spec)
@@ -394,10 +381,8 @@
done
declare starfun_inverse [symmetric, simp]
-lemma starfun_divide:
- "( *f* f) xa / ( *f* g) xa = ( *f* (%x. f x / g x)) xa"
-apply (unfold hypreal_divide_def real_divide_def, auto)
-done
+lemma starfun_divide: "( *f* f) xa / ( *f* g) xa = ( *f* (%x. f x / g x)) xa"
+by (simp add: divide_inverse)
declare starfun_divide [symmetric, simp]
lemma starfun_inverse2: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
@@ -410,8 +395,8 @@
topology of the reals
------------------------------------------------------------*)
lemma starfun_mem_starset:
- "( *f* f) x : *s* A ==> x : *s* {x. f x : A}"
-apply (unfold starset_def)
+ "( *f* f) x : *s* A ==> x : *s* {x. f x \<in> A}"
+apply (simp add: starset_def)
apply (rule_tac z = x in eq_Abs_hypreal)
apply (auto simp add: starfun)
apply (rename_tac "X")
@@ -438,7 +423,7 @@
lemma STAR_rabs_add_minus:
"*s* {x. abs (x + - y) < r} =
{x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
-apply (unfold starset_def, safe)
+apply (simp add: starset_def, safe)
apply (rule_tac [!] z = x in eq_Abs_hypreal)
apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less, ultra)
done
@@ -446,7 +431,7 @@
lemma STAR_starfun_rabs_add_minus:
"*s* {x. abs (f x + - y) < r} =
{x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"
-apply (unfold starset_def, safe)
+apply (simp add: starset_def, safe)
apply (rule_tac [!] z = x in eq_Abs_hypreal)
apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less starfun, ultra)
done
@@ -457,10 +442,10 @@
move both if possible?
-------------------------------------------------------------------*)
lemma Infinitesimal_FreeUltrafilterNat_iff2:
- "(x:Infinitesimal) =
- (EX X:Rep_hypreal(x).
- ALL m. {n. abs(X n) < inverse(real(Suc m))}
- : FreeUltrafilterNat)"
+ "(x \<in> Infinitesimal) =
+ (\<exists>X \<in> Rep_hypreal(x).
+ \<forall>m. {n. abs(X n) < inverse(real(Suc m))}
+ \<in> FreeUltrafilterNat)"
apply (rule eq_Abs_hypreal [of x])
apply (auto intro!: bexI lemma_hyprel_refl
simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def
@@ -469,7 +454,7 @@
done
lemma approx_FreeUltrafilterNat_iff: "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) =
- (ALL m. {n. abs (X n + - Y n) <
+ (\<forall>m. {n. abs (X n + - Y n) <
inverse(real(Suc m))} : FreeUltrafilterNat)"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])