# HG changeset patch
# User huffman
# Date 1126830050 -7200
# Node ID 4cf2e7980529ec1078e89faf44c6630af0920eb3
# Parent  835647238122bc8e10c685d3c45aede386f37824
rearranged

diff -r 835647238122 -r 4cf2e7980529 src/HOL/Hyperreal/HyperNat.thy
--- 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    
 *)
 
-header{*Construction of Hypernaturals using Ultrafilters*}
+header{*Hypernatural numbers*}
 
 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)"
 by transfer (rule diff_add_0)
 
-
-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))"
-by (simp add: order_less_le)
+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)"
 by (simp add: hypnat_of_nat_def)
 
-
-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*}
-
 lemma of_nat_eq_add [rule_format]:
      "\<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"
 by (auto simp add: of_nat_eq_add Nats_def split: hypnat_diff_split)
 
+
+
+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]) 
 apply (simp add: atMost_def) 
@@ -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"
 by (simp add: HNatInfinite_def)
 
@@ -227,7 +216,7 @@
 by (simp add: HNatInfinite_def)
 
 
-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*}
 
 lemma HNatInfinite_add:
      "[| x \<in> HNatInfinite; y \<in> HNatInfinite |] ==> x + y \<in> HNatInfinite"