--- a/src/HOL/Hyperreal/HyperDef.thy Tue Dec 12 07:13:06 2006 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Tue Dec 12 07:46:40 2006 +0100
@@ -19,12 +19,14 @@
"hypreal_of_real == star_of"
definition
- omega :: hypreal where -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
- "omega = star_n (%n. real (Suc n))"
+ omega :: hypreal where
+ -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
+ "omega = star_n (\<lambda>n. real (Suc n))"
definition
- epsilon :: hypreal where -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
- "epsilon = star_n (%n. inverse (real (Suc n)))"
+ epsilon :: hypreal where
+ -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
+ "epsilon = star_n (\<lambda>n. inverse (real (Suc n)))"
notation (xsymbols)
omega ("\<omega>") and
@@ -42,31 +44,31 @@
defs (overloaded)
star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
-lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> r *# x \<in> Standard"
+lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard"
by (simp add: star_scaleR_def)
-lemma star_of_scaleR [simp]: "star_of (r *# x) = r *# star_of x"
+lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)"
by transfer (rule refl)
instance star :: (real_vector) real_vector
proof
fix a b :: real
- show "\<And>x y::'a star. a *# (x + y) = a *# x + a *# y"
+ show "\<And>x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y"
by transfer (rule scaleR_right_distrib)
- show "\<And>x::'a star. (a + b) *# x = a *# x + b *# x"
+ show "\<And>x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x"
by transfer (rule scaleR_left_distrib)
- show "\<And>x::'a star. a *# b *# x = (a * b) *# x"
+ show "\<And>x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x"
by transfer (rule scaleR_scaleR)
- show "\<And>x::'a star. 1 *# x = x"
+ show "\<And>x::'a star. scaleR 1 x = x"
by transfer (rule scaleR_one)
qed
instance star :: (real_algebra) real_algebra
proof
fix a :: real
- show "\<And>x y::'a star. a *# x * y = a *# (x * y)"
+ show "\<And>x y::'a star. scaleR a x * y = scaleR a (x * y)"
by transfer (rule mult_scaleR_left)
- show "\<And>x y::'a star. x * a *# y = a *# (x * y)"
+ show "\<And>x y::'a star. x * scaleR a y = scaleR a (x * y)"
by transfer (rule mult_scaleR_right)
qed
@@ -117,52 +119,47 @@
by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.filter])
lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat"
-by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.finite])
+by (rule FreeUltrafilterNat.finite)
lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x"
-thm FreeUltrafilterNat_mem
-thm freeultrafilter.infinite
-thm FreeUltrafilterNat_mem [THEN freeultrafilter.infinite]
-by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.infinite])
+by (rule FreeUltrafilterNat.infinite)
-lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.empty])
+lemma FreeUltrafilterNat_empty: "{} \<notin> FreeUltrafilterNat"
+by (rule FreeUltrafilterNat.empty)
lemma FreeUltrafilterNat_Int:
"[| X \<in> FreeUltrafilterNat; Y \<in> FreeUltrafilterNat |]
==> X Int Y \<in> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.Int])
+by (rule FreeUltrafilterNat.Int)
lemma FreeUltrafilterNat_subset:
"[| X \<in> FreeUltrafilterNat; X \<subseteq> Y |]
==> Y \<in> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.subset])
+by (rule FreeUltrafilterNat.subset)
lemma FreeUltrafilterNat_Compl:
"X \<in> FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat"
-apply (erule contrapos_pn)
-apply (erule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD2])
-done
+by (rule FreeUltrafilterNat.memD)
lemma FreeUltrafilterNat_Compl_mem:
- "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
-by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD1])
+ "X \<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
+by (rule FreeUltrafilterNat.not_memD)
lemma FreeUltrafilterNat_Compl_iff1:
"(X \<notin> FreeUltrafilterNat) = (-X \<in> FreeUltrafilterNat)"
-by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff])
+by (rule FreeUltrafilterNat.not_mem_iff)
lemma FreeUltrafilterNat_Compl_iff2:
"(X \<in> FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
-apply (drule FreeUltrafilterNat_finite)
-apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
+apply (drule FreeUltrafilterNat.finite)
+apply (simp add: FreeUltrafilterNat.not_mem_iff)
done
-lemma FreeUltrafilterNat_UNIV [iff]: "UNIV \<in> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.UNIV])
+lemma FreeUltrafilterNat_UNIV: "UNIV \<in> FreeUltrafilterNat"
+by (rule FreeUltrafilterNat.UNIV)
lemma FreeUltrafilterNat_Nat_set_refl [intro]:
"{n. P(n) = P(n)} \<in> FreeUltrafilterNat"
@@ -202,7 +199,7 @@
subsection{*Properties of @{term starrel}*}
text{*Proving that @{term starrel} is an equivalence relation*}
-
+(*
lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
by (rule StarDef.starrel_iff)
@@ -219,21 +216,11 @@
lemma equiv_starrel: "equiv UNIV starrel"
by (rule StarDef.equiv_starrel)
-(* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *)
lemmas equiv_starrel_iff =
eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I, simp]
-lemma starrel_in_hypreal [simp]: "starrel``{x}:star"
-by (simp add: star_def starrel_def quotient_def, blast)
-
-declare Abs_star_inject [simp] Abs_star_inverse [simp]
-declare equiv_starrel [THEN eq_equiv_class_iff, simp]
-
lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel]
-lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
-by (simp add: starrel_def)
-
lemma hypreal_empty_not_mem [simp]: "{} \<notin> star"
apply (simp add: star_def)
apply (auto elim!: quotientE equalityCE)
@@ -241,6 +228,16 @@
lemma Rep_hypreal_nonempty [simp]: "Rep_star x \<noteq> {}"
by (insert Rep_star [of x], auto)
+*)
+
+lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
+by (simp add: starrel_def)
+
+lemma starrel_in_hypreal [simp]: "starrel``{x}:star"
+by (simp add: star_def starrel_def quotient_def, blast)
+
+declare Abs_star_inject [simp] Abs_star_inverse [simp]
+declare equiv_starrel [THEN eq_equiv_class_iff, simp]
subsection{*@{term hypreal_of_real}:
the Injection from @{typ real} to @{typ hypreal}*}
--- a/src/HOL/Hyperreal/HyperNat.thy Tue Dec 12 07:13:06 2006 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Tue Dec 12 07:46:40 2006 +0100
@@ -258,10 +258,12 @@
hypnat_omega_def: "whn = star_n (%n::nat. n)"
lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \<noteq> whn"
-by (simp add: hypnat_omega_def star_of_def star_n_eq_iff FUFNat.finite)
+by (simp add: hypnat_omega_def star_of_def star_n_eq_iff
+ FreeUltrafilterNat.finite)
lemma whn_neq_hypnat_of_nat: "whn \<noteq> hypnat_of_nat n"
-by (simp add: hypnat_omega_def star_of_def star_n_eq_iff FUFNat.finite)
+by (simp add: hypnat_omega_def star_of_def star_n_eq_iff
+ FreeUltrafilterNat.finite)
lemma whn_not_Nats [simp]: "whn \<notin> Nats"
by (simp add: Nats_def image_def whn_neq_hypnat_of_nat)
@@ -373,32 +375,32 @@
lemma hypreal_of_hypnat_inject [simp]:
"!!m n. (hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
-by (transfer, simp)
+by transfer (rule real_of_nat_inject)
lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
-by (simp add: star_n_zero_num hypreal_of_hypnat)
+by transfer (rule real_of_nat_zero)
lemma hypreal_of_hypnat_one: "hypreal_of_hypnat (1::hypnat) = 1"
-by (simp add: star_n_one_num hypreal_of_hypnat)
+by transfer simp
lemma hypreal_of_hypnat_add [simp]:
"!!m n. hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
-by (transfer, rule real_of_nat_add)
+by transfer (rule real_of_nat_add)
lemma hypreal_of_hypnat_mult [simp]:
"!!m n. hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
-by (transfer, rule real_of_nat_mult)
+by transfer (rule real_of_nat_mult)
lemma hypreal_of_hypnat_less_iff [simp]:
"!!m n. (hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
-by (transfer, simp)
+by transfer (rule real_of_nat_less_iff)
lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)"
by (simp add: hypreal_of_hypnat_zero [symmetric])
declare hypreal_of_hypnat_eq_zero_iff [simp]
lemma hypreal_of_hypnat_ge_zero [simp]: "!!n. 0 \<le> hypreal_of_hypnat n"
-by (transfer, simp)
+by transfer (rule real_of_nat_ge_zero)
lemma HNatInfinite_inverse_Infinitesimal [simp]:
"n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
--- a/src/HOL/Hyperreal/StarDef.thy Tue Dec 12 07:13:06 2006 +0100
+++ b/src/HOL/Hyperreal/StarDef.thy Tue Dec 12 07:46:40 2006 +0100
@@ -16,21 +16,22 @@
FreeUltrafilterNat :: "nat set set" ("\<U>") where
"\<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
+lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
+apply (unfold FreeUltrafilterNat_def)
+apply (rule someI_ex)
+apply (rule freeultrafilter_Ex)
+apply (rule nat_infinite)
+done
-interpretation FUFNat: freeultrafilter [FreeUltrafilterNat]
- using freeultrafilter_FUFNat by (simp_all add: freeultrafilter_def)
+interpretation FreeUltrafilterNat: freeultrafilter [FreeUltrafilterNat]
+by (rule freeultrafilter_FreeUltrafilterNat)
text {* This rule takes the place of the old ultra tactic *}
lemma ultra:
"\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
-by (simp add: Collect_imp_eq FUFNat.F.Un_iff FUFNat.F.Compl_iff)
+by (simp add: Collect_imp_eq
+ FreeUltrafilterNat.Un_iff FreeUltrafilterNat.Compl_iff)
subsection {* Definition of @{text star} type constructor *}
@@ -94,26 +95,26 @@
lemma transfer_ex [transfer_intro]:
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
\<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
-by (simp only: ex_star_eq FUFNat.F.Collect_ex)
+by (simp only: ex_star_eq FreeUltrafilterNat.Collect_ex)
lemma transfer_all [transfer_intro]:
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
\<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
-by (simp only: all_star_eq FUFNat.F.Collect_all)
+by (simp only: all_star_eq FreeUltrafilterNat.Collect_all)
lemma transfer_not [transfer_intro]:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
-by (simp only: FUFNat.F.Collect_not)
+by (simp only: FreeUltrafilterNat.Collect_not)
lemma transfer_conj [transfer_intro]:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
\<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
-by (simp only: FUFNat.F.Collect_conj)
+by (simp only: FreeUltrafilterNat.Collect_conj)
lemma transfer_disj [transfer_intro]:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
\<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
-by (simp only: FUFNat.F.Collect_disj)
+by (simp only: FreeUltrafilterNat.Collect_disj)
lemma transfer_imp [transfer_intro]:
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>