author huffman Fri, 16 Sep 2005 02:20:50 +0200 changeset 17433 4cf2e7980529 parent 17432 835647238122 child 17434 c2efacfe8ab8
rearranged
```--- a/src/HOL/Hyperreal/HyperNat.thy	Fri Sep 16 01:42:57 2005 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Fri Sep 16 02:20:50 2005 +0200
@@ -5,7 +5,7 @@
Converted to Isar and polished by lcp
*)

theory HyperNat
imports Star
@@ -16,11 +16,7 @@
syntax hypnat_of_nat :: "nat => nat star"
translations "hypnat_of_nat" => "star_of :: nat => nat star"

-consts whn :: hypnat
-
-defs
-  (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
-  hypnat_omega_def:  "whn == star_n (%n::nat. n)"
+subsection{*Properties Transferred from Naturals*}

lemma hypnat_minus_zero [simp]: "!!z. z - z = (0::hypnat)"
by transfer (rule diff_self_eq_0)
@@ -52,17 +48,12 @@
lemma hypnat_diff_add_0 [simp]: "!!m n. (n::hypnat) - (n+m) = (0::hypnat)"

-
-subsection{*Hyperreal Multiplication*}
-
lemma hypnat_diff_mult_distrib: "!!k m n. ((m::hypnat) - n) * k = (m * k) - (n * k)"
by transfer (rule diff_mult_distrib)

lemma hypnat_diff_mult_distrib2: "!!k m n. (k::hypnat) * (m - n) = (k * m) - (k * n)"
by transfer (rule diff_mult_distrib2)

-subsection{*Properties of The @{text "\<le>"} Relation*}
-
lemma hypnat_le_zero_cancel [iff]: "!!n. (n \<le> (0::hypnat)) = (n = 0)"
by transfer (rule le_0_eq)

@@ -72,10 +63,6 @@
lemma hypnat_diff_is_0_eq [simp]: "!!m n. ((m::hypnat) - n = 0) = (m \<le> n)"
by transfer (rule diff_is_0_eq)

-
-
-subsection{*Theorems for Ordering*}
-
lemma hypnat_not_less0 [iff]: "!!n. ~ n < (0::hypnat)"
by transfer (rule not_less0)

@@ -103,8 +90,8 @@
lemma hypnat_add_one_self_less [simp]: "(x::hypnat) < x + (1::hypnat)"
by (insert add_strict_left_mono [OF zero_less_one], auto)

-lemma hypnat_neq0_conv [iff]: "(n \<noteq> 0) = (0 < (n::hypnat))"
+lemma hypnat_neq0_conv [iff]: "!!n. (n \<noteq> 0) = (0 < (n::hypnat))"
+by transfer (rule neq0_conv)

lemma hypnat_gt_zero_iff: "((0::hypnat) < n) = ((1::hypnat) \<le> n)"
by (auto simp add: linorder_not_less [symmetric])
@@ -133,16 +120,7 @@
by (auto simp add: linorder_not_less dest: order_le_less_trans)
qed

-
-subsection{*The Embedding @{term hypnat_of_nat} Preserves @{text
-comm_ring_1} and Order Properties*}
-
-constdefs
-
-  (* the set of infinite hypernatural numbers *)
-  HNatInfinite :: "hypnat set"
-  "HNatInfinite == {n. n \<notin> Nats}"
-
+subsection{*Properties of the set of embedded natural numbers*}

lemma hypnat_of_nat_def: "hypnat_of_nat m == of_nat m"
by (transfer, simp)
@@ -154,16 +132,6 @@
"hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)"

-
-subsection{*Existence of an infinite hypernatural number*}
-
-text{*Existence of infinite number not corresponding to any natural number
-follows because member @{term FreeUltrafilterNat} is not finite.
-See @{text HyperDef.thy} for similar argument.*}
-
-
-subsection{*Properties of the set of embedded natural numbers*}
-
"\<forall>d::hypnat. of_nat m = of_nat n + d --> d \<in> range of_nat"
apply (induct n)
@@ -175,6 +143,21 @@
lemma Nats_diff [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> (a-b :: hypnat) \<in> Nats"

+
+
+subsection{*Existence of an infinite hypernatural number*}
+
+consts whn :: hypnat
+
+defs
+  (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
+  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.
+See @{text HyperDef.thy} for similar argument.*}
+
+
lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
apply (insert finite_atMost [of m])
@@ -217,6 +200,12 @@

subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}

+constdefs
+
+  (* the set of infinite hypernatural numbers *)
+  HNatInfinite :: "hypnat set"
+  "HNatInfinite == {n. n \<notin> Nats}"
+
lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"

@@ -227,7 +216,7 @@

-subsection{*Alternative characterization of the set of infinite hypernaturals*}
+subsubsection{*Alternative characterization of the set of infinite hypernaturals*}

text{* @{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}

@@ -250,7 +239,7 @@
done

-subsection{*Alternative Characterization of @{term HNatInfinite} using
+subsubsection{*Alternative Characterization of @{term HNatInfinite} using
Free Ultrafilter*}

lemma HNatInfinite_FreeUltrafilterNat:
@@ -294,7 +283,7 @@
by (blast intro: order_less_imp_le HNatInfinite_gt_one)

-subsection{*Closure Rules*}
+subsubsection{*Closure Rules*}