author huffman Tue, 12 Dec 2006 07:46:40 +0100 changeset 21787 9edd495b6330 parent 21786 66da6af2b0c9 child 21788 d460465a9f97
 src/HOL/Hyperreal/HyperDef.thy file | annotate | diff | comparison | revisions src/HOL/Hyperreal/HyperNat.thy file | annotate | diff | comparison | revisions src/HOL/Hyperreal/StarDef.thy file | annotate | diff | comparison | revisions
```--- 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 @@
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"

-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 (drule FreeUltrafilterNat.finite)
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}"
-
lemma hypreal_empty_not_mem [simp]: "{} \<notin> star"
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}"
+
+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 transfer (rule real_of_nat_zero)

lemma hypreal_of_hypnat_one: "hypreal_of_hypnat (1::hypnat) = 1"
+by transfer simp

"!!m n. hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"

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)"
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)
+    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>```