Quellcode-Bibliothek Discrete_Topology.thy Sprache: Isabelle

(*  Title:      HOL/Probability/Discrete_Topology.thy
    Author:     Fabian Immler, TU München
*)

theory Discrete_Topology
imports "HOL-Analysis.Analysis"
begin

text \<open>Copy of discrete types with discrete topology. This space is polish.\<close>

typedef 'a discrete = "UNIV::'a set"
morphisms of_discrete discrete
..

instantiation discrete :: (type) metric_space
begin

definition dist_discrete :: "'a discrete \ 'a discrete \ real"
  where "dist_discrete n m = (if n = m then 0 else 1)"

definition uniformity_discrete :: "('a discrete \ 'a discrete) filter" where
  "(uniformity::('a discrete \ 'a discrete) filter) = (INF e\{0 <..}. principal {(x, y). dist x y < e})"

definition "open_discrete" :: "'a discrete set \ bool" where
  "(open::'a discrete set \ bool) U \ (\x\U. eventually (\(x', y). x' = x \ y \ U) uniformity)"

instance proof qed (auto simp: uniformity_discrete_def open_discrete_def dist_discrete_def intro: exI[where x=1])
end

lemma open_discrete: "open (S :: 'a discrete set)"
  unfolding open_dist dist_discrete_def by (auto intro!: exI[of _ "1 / 2"])

instance discrete :: (type) complete_space
proof
  fix X::"nat\'a discrete"
  assume "Cauchy X"
  then obtain n where "\m\n. X n = X m"
    by (force simp: dist_discrete_def Cauchy_def split: if_split_asm dest:spec[where x=1])
  thus "convergent X"
    by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n])
       (simp add: dist_discrete_def)
qed

instance discrete :: (countable) countable
proof
  have "inj (\c::'a discrete. to_nat (of_discrete c))"
    by (simp add: inj_on_def of_discrete_inject)
  thus "\f::'a discrete \ nat. inj f" by blast
qed

instance discrete :: (countable) second_countable_topology
proof
  let ?B = "range (\n::'a discrete. {n})"
  have "\S. generate_topology ?B (\x\S. {x})"
    by (intro generate_topology_Union) (auto intro: generate_topology.intros)
  then have "open = generate_topology ?B"
    by (auto intro!: ext simp: open_discrete)
  moreover have "countable ?B" by simp
  ultimately show "\B::'a discrete set set. countable B \ open = generate_topology B" by blast
qed

instance discrete :: (countable) polish_space ..

end

quality100%

¤ 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.0.11Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.