Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: HyperNat.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Nonstandard_Analysis/HyperNat.thy
    Author:     Jacques D. Fleuriot
    Copyright:  1998  University of Cambridge

Converted to Isar and polished by lcp
*)

section \<open>Hypernatural numbers\<close>

theory HyperNat
  imports StarDef
begin

type_synonym hypnat = "nat star"

abbreviation hypnat_of_nat :: "nat \ nat star"
  where "hypnat_of_nat \ star_of"

definition hSuc :: "hypnat \ hypnat"
  where hSuc_def [transfer_unfold]: "hSuc = *f* Suc"

subsection \<open>Properties Transferred from Naturals\<close>

lemma hSuc_not_zero [iff]: "\m. hSuc m \ 0"
  by transfer (rule Suc_not_Zero)

lemma zero_not_hSuc [iff]: "\m. 0 \ hSuc m"
  by transfer (rule Zero_not_Suc)

lemma hSuc_hSuc_eq [iff]: "\m n. hSuc m = hSuc n \ m = n"
  by transfer (rule nat.inject)

lemma zero_less_hSuc [iff]: "\n. 0 < hSuc n"
  by transfer (rule zero_less_Suc)

lemma hypnat_minus_zero [simp]: "\z::hypnat. z - z = 0"
  by transfer (rule diff_self_eq_0)

lemma hypnat_diff_0_eq_0 [simp]: "\n::hypnat. 0 - n = 0"
  by transfer (rule diff_0_eq_0)

lemma hypnat_add_is_0 [iff]: "\m n::hypnat. m + n = 0 \ m = 0 \ n = 0"
  by transfer (rule add_is_0)

lemma hypnat_diff_diff_left: "\i j k::hypnat. i - j - k = i - (j + k)"
  by transfer (rule diff_diff_left)

lemma hypnat_diff_commute: "\i j k::hypnat. i - j - k = i - k - j"
  by transfer (rule diff_commute)

lemma hypnat_diff_add_inverse [simp]: "\m n::hypnat. n + m - n = m"
  by transfer (rule diff_add_inverse)

lemma hypnat_diff_add_inverse2 [simp]:  "\m n::hypnat. m + n - n = m"
  by transfer (rule diff_add_inverse2)

lemma hypnat_diff_cancel [simp]: "\k m n::hypnat. (k + m) - (k + n) = m - n"
  by transfer (rule diff_cancel)

lemma hypnat_diff_cancel2 [simp]: "\k m n::hypnat. (m + k) - (n + k) = m - n"
  by transfer (rule diff_cancel2)

lemma hypnat_diff_add_0 [simp]: "\m n::hypnat. n - (n + m) = 0"
  by transfer (rule diff_add_0)

lemma hypnat_diff_mult_distrib: "\k m n::hypnat. (m - n) * k = (m * k) - (n * k)"
  by transfer (rule diff_mult_distrib)

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

lemma hypnat_le_zero_cancel [iff]: "\n::hypnat. n \ 0 \ n = 0"
  by transfer (rule le_0_eq)

lemma hypnat_mult_is_0 [simp]: "\m n::hypnat. m * n = 0 \ m = 0 \ n = 0"
  by transfer (rule mult_is_0)

lemma hypnat_diff_is_0_eq [simp]: "\m n::hypnat. m - n = 0 \ m \ n"
  by transfer (rule diff_is_0_eq)

lemma hypnat_not_less0 [iff]: "\n::hypnat. \ n < 0"
  by transfer (rule not_less0)

lemma hypnat_less_one [iff]: "\n::hypnat. n < 1 \ n = 0"
  by transfer (rule less_one)

lemma hypnat_add_diff_inverse: "\m n::hypnat. \ m < n \ n + (m - n) = m"
  by transfer (rule add_diff_inverse)

lemma hypnat_le_add_diff_inverse [simp]: "\m n::hypnat. n \ m \ n + (m - n) = m"
  by transfer (rule le_add_diff_inverse)

lemma hypnat_le_add_diff_inverse2 [simp]: "\m n::hypnat. n \ m \ (m - n) + n = m"
  by transfer (rule le_add_diff_inverse2)

declare hypnat_le_add_diff_inverse2 [OF order_less_imp_le]

lemma hypnat_le0 [iff]: "\n::hypnat. 0 \ n"
  by transfer (rule le0)

lemma hypnat_le_add1 [simp]: "\x n::hypnat. x \ x + n"
  by transfer (rule le_add1)

lemma hypnat_add_self_le [simp]: "\x n::hypnat. x \ n + x"
  by transfer (rule le_add2)

lemma hypnat_add_one_self_less [simp]: "x < x + 1" for x :: hypnat
  by (fact less_add_one)

lemma hypnat_neq0_conv [iff]: "\n::hypnat. n \ 0 \ 0 < n"
  by transfer (rule neq0_conv)

lemma hypnat_gt_zero_iff: "0 < n \ 1 \ n" for n :: hypnat
  by (auto simp add: linorder_not_less [symmetric])

lemma hypnat_gt_zero_iff2: "0 < n \ (\m. n = m + 1)" for n :: hypnat
  by (auto intro!: add_nonneg_pos exI[of _ "n - 1"] simp: hypnat_gt_zero_iff)

lemma hypnat_add_self_not_less: "\ x + y < x" for x y :: hypnat
  by (simp add: linorder_not_le [symmetric] add.commute [of x])

lemma hypnat_diff_split: "P (a - b) \ (a < b \ P 0) \ (\d. a = b + d \ P d)"
  for a b :: hypnat
  \<comment> \<open>elimination of \<open>-\<close> on \<open>hypnat\<close>\<close>
proof (cases "a < b" rule: case_split)
  case True
  then show ?thesis
    by (auto simp add: hypnat_add_self_not_less order_less_imp_le hypnat_diff_is_0_eq [THEN iffD2])
next
  case False
  then show ?thesis
    by (auto simp add: linorder_not_less dest: order_le_less_trans)
qed

subsection \<open>Properties of the set of embedded natural numbers\<close>

lemma of_nat_eq_star_of [simp]: "of_nat = star_of"
proof
  show "of_nat n = star_of n" for n
    by transfer simp
qed

lemma Nats_eq_Standard: "(Nats :: nat star set) = Standard"
  by (auto simp: Nats_def Standard_def)

lemma hypnat_of_nat_mem_Nats [simp]: "hypnat_of_nat n \ Nats"
  by (simp add: Nats_eq_Standard)

lemma hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) = 1"
  by transfer simp

lemma hypnat_of_nat_Suc [simp]: "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1"
  by transfer simp

lemma of_nat_eq_add:
  fixes d::hypnat
  shows "of_nat m = of_nat n + d \ d \ range of_nat"
proof (induct n arbitrary: d)
  case (Suc n)
  then show ?case
    by (metis Nats_def Nats_eq_Standard Standard_simps(4) hypnat_diff_add_inverse of_nat_in_Nats)
qed auto

lemma Nats_diff [simp]: "a \ Nats \ b \ Nats \ a - b \ Nats" for a b :: hypnat
  by (simp add: Nats_eq_Standard)

subsection \<open>Infinite Hypernatural Numbers -- \<^term>\<open>HNatInfinite\<close>\<close>

text \<open>The set of infinite hypernatural numbers.\<close>
definition HNatInfinite :: "hypnat set"
  where "HNatInfinite = {n. n \ Nats}"

lemma Nats_not_HNatInfinite_iff: "x \ Nats \ x \ HNatInfinite"
  by (simp add: HNatInfinite_def)

lemma HNatInfinite_not_Nats_iff: "x \ HNatInfinite \ x \ Nats"
  by (simp add: HNatInfinite_def)

lemma star_of_neq_HNatInfinite: "N \ HNatInfinite \ star_of n \ N"
  by (auto simp add: HNatInfinite_def Nats_eq_Standard)

lemma star_of_Suc_lessI: "\N. star_of n < N \ star_of (Suc n) \ N \ star_of (Suc n) < N"
  by transfer (rule Suc_lessI)

lemma star_of_less_HNatInfinite:
  assumes N: "N \ HNatInfinite"
  shows "star_of n < N"
proof (induct n)
  case 0
  from N have "star_of 0 \ N"
    by (rule star_of_neq_HNatInfinite)
  then show ?case by simp
next
  case (Suc n)
  from N have "star_of (Suc n) \ N"
    by (rule star_of_neq_HNatInfinite)
  with Suc show ?case
    by (rule star_of_Suc_lessI)
qed

lemma star_of_le_HNatInfinite: "N \ HNatInfinite \ star_of n \ N"
  by (rule star_of_less_HNatInfinite [THEN order_less_imp_le])

subsubsection \<open>Closure Rules\<close>

lemma Nats_less_HNatInfinite: "x \ Nats \ y \ HNatInfinite \ x < y"
  by (auto simp add: Nats_def star_of_less_HNatInfinite)

lemma Nats_le_HNatInfinite: "x \ Nats \ y \ HNatInfinite \ x \ y"
  by (rule Nats_less_HNatInfinite [THEN order_less_imp_le])

lemma zero_less_HNatInfinite: "x \ HNatInfinite \ 0 < x"
  by (simp add: Nats_less_HNatInfinite)

lemma one_less_HNatInfinite: "x \ HNatInfinite \ 1 < x"
  by (simp add: Nats_less_HNatInfinite)

lemma one_le_HNatInfinite: "x \ HNatInfinite \ 1 \ x"
  by (simp add: Nats_le_HNatInfinite)

lemma zero_not_mem_HNatInfinite [simp]: "0 \ HNatInfinite"
  by (simp add: HNatInfinite_def)

lemma Nats_downward_closed: "x \ Nats \ y \ x \ y \ Nats" for x y :: hypnat
  using HNatInfinite_not_Nats_iff Nats_le_HNatInfinite by fastforce

lemma HNatInfinite_upward_closed: "x \ HNatInfinite \ x \ y \ y \ HNatInfinite"
  using HNatInfinite_not_Nats_iff Nats_downward_closed by blast

lemma HNatInfinite_add: "x \ HNatInfinite \ x + y \ HNatInfinite"
  using HNatInfinite_upward_closed hypnat_le_add1 by blast

lemma HNatInfinite_diff: "\x \ HNatInfinite; y \ Nats\ \ x - y \ HNatInfinite"
  by (metis HNatInfinite_not_Nats_iff Nats_add Nats_le_HNatInfinite le_add_diff_inverse)

lemma HNatInfinite_is_Suc: "x \ HNatInfinite \ \y. x = y + 1" for x :: hypnat
  using hypnat_gt_zero_iff2 zero_less_HNatInfinite by blast

subsection \<open>Existence of an infinite hypernatural number\<close>

text \<open>\<open>\<omega>\<close> is in fact an infinite hypernatural number = \<open>[<1, 2, 3, \<dots>>]\<close>\<close>
definition whn :: hypnat
  where hypnat_omega_def: "whn = star_n (\n::nat. n)"

lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \ whn"
  by (simp add: FreeUltrafilterNat.singleton' hypnat_omega_def star_of_def star_n_eq_iff)

lemma whn_neq_hypnat_of_nat: "whn \ hypnat_of_nat n"
  by (simp add: FreeUltrafilterNat.singleton hypnat_omega_def star_of_def star_n_eq_iff)

lemma whn_not_Nats [simp]: "whn \ Nats"
  by (simp add: Nats_def image_def whn_neq_hypnat_of_nat)

lemma HNatInfinite_whn [simp]: "whn \ HNatInfinite"
  by (simp add: HNatInfinite_def)

lemma lemma_unbounded_set [simp]: "eventually (\n::nat. m < n) \"
  by (rule filter_leD[OF FreeUltrafilterNat.le_cofinite])
     (auto simp add: cofinite_eq_sequentially eventually_at_top_dense)

lemma hypnat_of_nat_eq: "hypnat_of_nat m = star_n (\n::nat. m)"
  by (simp add: star_of_def)

lemma SHNat_eq: "Nats = {n. \N. n = hypnat_of_nat N}"
  by (simp add: Nats_def image_def)

lemma Nats_less_whn: "n \ Nats \ n < whn"
  by (simp add: Nats_less_HNatInfinite)

lemma Nats_le_whn: "n \ Nats \ n \ whn"
  by (simp add: Nats_le_HNatInfinite)

lemma hypnat_of_nat_less_whn [simp]: "hypnat_of_nat n < whn"
  by (simp add: Nats_less_whn)

lemma hypnat_of_nat_le_whn [simp]: "hypnat_of_nat n \ whn"
  by (simp add: Nats_le_whn)

lemma hypnat_zero_less_hypnat_omega [simp]: "0 < whn"
  by (simp add: Nats_less_whn)

lemma hypnat_one_less_hypnat_omega [simp]: "1 < whn"
  by (simp add: Nats_less_whn)

subsubsection \<open>Alternative characterization of the set of infinite hypernaturals\<close>

text \<open>\<^term>\<open>HNatInfinite = {N. \<forall>n \<in> Nats. n < N}\<close>\<close>

text\<open>unused, but possibly interesting\<close>
lemma HNatInfinite_FreeUltrafilterNat_eventually:
  assumes "\k::nat. eventually (\n. f n \ k) \"
  shows "eventually (\n. m < f n) \"
proof (induct m)
  case 0
  then show ?case
    using assms eventually_mono by fastforce
next
  case (Suc m)
  then show ?case
    using assms [of "Suc m"] eventually_elim2 by fastforce
qed

lemma HNatInfinite_iff: "HNatInfinite = {N. \n \ Nats. n < N}"
  using HNatInfinite_def Nats_less_HNatInfinite by auto

subsubsection \<open>Alternative Characterization of \<^term>\<open>HNatInfinite\<close> using Free Ultrafilter\<close>

lemma HNatInfinite_FreeUltrafilterNat:
  "star_n X \ HNatInfinite \ \u. eventually (\n. u < X n) \"
  by (metis (full_types) starP2_star_of starP_star_n star_less_def star_of_less_HNatInfinite)

lemma FreeUltrafilterNat_HNatInfinite:
  "\u. eventually (\n. u < X n) \ \ star_n X \ HNatInfinite"
  by (auto simp add: star_less_def starP2_star_n HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)

lemma HNatInfinite_FreeUltrafilterNat_iff:
  "(star_n X \ HNatInfinite) = (\u. eventually (\n. u < X n) \)"
  by (rule iffI [OF HNatInfinite_FreeUltrafilterNat FreeUltrafilterNat_HNatInfinite])

subsection \<open>Embedding of the Hypernaturals into other types\<close>

definition of_hypnat :: "hypnat \ 'a::semiring_1_cancel star"
  where of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"

lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
  by transfer (rule of_nat_0)

lemma of_hypnat_1 [simp]: "of_hypnat 1 = 1"
  by transfer (rule of_nat_1)

lemma of_hypnat_hSuc: "\m. of_hypnat (hSuc m) = 1 + of_hypnat m"
  by transfer (rule of_nat_Suc)

lemma of_hypnat_add [simp]: "\m n. of_hypnat (m + n) = of_hypnat m + of_hypnat n"
  by transfer (rule of_nat_add)

lemma of_hypnat_mult [simp]: "\m n. of_hypnat (m * n) = of_hypnat m * of_hypnat n"
  by transfer (rule of_nat_mult)

lemma of_hypnat_less_iff [simp]:
  "\m n. of_hypnat m < (of_hypnat n::'a::linordered_semidom star) \ m < n"
  by transfer (rule of_nat_less_iff)

lemma of_hypnat_0_less_iff [simp]:
  "\n. 0 < (of_hypnat n::'a::linordered_semidom star) \ 0 < n"
  by transfer (rule of_nat_0_less_iff)

lemma of_hypnat_less_0_iff [simp]: "\m. \ (of_hypnat m::'a::linordered_semidom star) < 0"
  by transfer (rule of_nat_less_0_iff)

lemma of_hypnat_le_iff [simp]:
  "\m n. of_hypnat m \ (of_hypnat n::'a::linordered_semidom star) \ m \ n"
  by transfer (rule of_nat_le_iff)

lemma of_hypnat_0_le_iff [simp]: "\n. 0 \ (of_hypnat n::'a::linordered_semidom star)"
  by transfer (rule of_nat_0_le_iff)

lemma of_hypnat_le_0_iff [simp]: "\m. (of_hypnat m::'a::linordered_semidom star) \ 0 \ m = 0"
  by transfer (rule of_nat_le_0_iff)

lemma of_hypnat_eq_iff [simp]:
  "\m n. of_hypnat m = (of_hypnat n::'a::linordered_semidom star) \ m = n"
  by transfer (rule of_nat_eq_iff)

lemma of_hypnat_eq_0_iff [simp]: "\m. (of_hypnat m::'a::linordered_semidom star) = 0 \ m = 0"
  by transfer (rule of_nat_eq_0_iff)

lemma HNatInfinite_of_hypnat_gt_zero:
  "N \ HNatInfinite \ (0::'a::linordered_semidom star) < of_hypnat N"
  by (rule ccontr) (simp add: linorder_not_less)

end

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.