Example 4.3 (Scott 1981, PRG-19, §4) — the natural-number domain N

Scott's "THE domain of integers" (pages 57–61). The tokens are ℕ, and the neighbourhoods are

N = {{n} ∣ n ∈ ℕ} ∪ {ℕ}

— a flat domain: the singletons {n} are the finite total elements and the whole space ℕ is the least-informative neighbourhood Δ = ⊥. We build N by the nested-or-disjoint criterion (ofNestedOrDisjoint): any two neighbourhoods are nested (one is ℕ) or disjoint (distinct singletons).

The (ideal) elements of |N| are exactly: the bottom ⊥ = {ℕ} ("undefined"), and for each n the total element n̂ = ↑{n} = {{n}, ℕ} (natElem n). Scott then equips N with the structure maps

• succ, pred : N → N (succMap, predMap)
• zero : N → T (zeroMap, into the truth domain T of Example 1.2),

making ⟨N, 0, succ, pred, zero⟩ "THE domain of integers". All three are strict approximable maps determined by their action on the finite total elements:

• succ(n̂) = (n+1)^, succ(⊥) = ⊥;
• pred((n+1)^) = n̂, pred(0̂) = ⊥, pred(⊥) = ⊥;
• zero(0̂) = true, zero((n+1)^) = false, zero(⊥) = ⊥.

We capture the common shape — a map N → V sending n̂ ↦ val n and ⊥ ↦ ⊥ — once and for all in the combinator constLiftN, whose computation rules constLiftN_natElem/constLiftN_bot give all of the displayed equations uniformly. The data (N, constLiftN, succMap, predMap) is choice-free (#print axioms ⊆ {propext, Quot.sound}); zeroMap inherits Classical.choice structurally from the truth domain T of Example 1.2 exactly as Example23.parityMap does.

The neighbourhood system N.

def Domain.Neighborhood.Example43.memN (X : Set ℕ) : Prop

Membership in Scott's natural-number system: a neighbourhood is the whole space ℕ or a singleton {n}.

Equations

• Domain.Neighborhood.Example43.memN X = (X = Set.univ ∨ ∃ (n : ℕ), X = {n})

theorem Domain.Neighborhood.Example43.memN_univ : memN Set.univ

theorem Domain.Neighborhood.Example43.memN_singleton (n : ℕ) : memN {n}

theorem Domain.Neighborhood.Example43.univ_ne_singleton (n : ℕ) : Set.univ ≠ {n}

ℕ is not a singleton (a witness n+1 ≠ n).

theorem Domain.Neighborhood.Example43.singleton_ne_univ (n : ℕ) : {n} ≠ Set.univ

{n} ≠ ℕ (the symmetric form).

theorem Domain.Neighborhood.Example43.singleton_nat_inj {n m : ℕ} (h : {n} = {m}) : n = m

Singletons of naturals are one-one as sets.

theorem Domain.Neighborhood.Example43.nestedOrDisjoint : NestedOrDisjoint memN

Any two neighbourhoods of N are nested or disjoint: ℕ contains every singleton, and two distinct singletons are disjoint.

def Domain.Neighborhood.Example43.N : NeighborhoodSystem ℕ

Example 4.3 (Scott 1981, PRG-19). The natural-number neighbourhood system N on Δ = ℕ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Domain.Neighborhood.Example43.N_mem {X : Set ℕ} : N.mem X ↔ memN X

@[simp]

theorem Domain.Neighborhood.Example43.N_master : N.master = Set.univ

theorem Domain.Neighborhood.Example43.N_bot_mem {X : Set ℕ} : N.bot.mem X ↔ X = Set.univ

⊥ ∈ N reads: a neighbourhood lies in ⊥ iff it is the whole space ℕ.

The total elements n̂.

def Domain.Neighborhood.Example43.natElem (n : ℕ) : N.Element

Scott's total element n̂ = ↑{n} = {{n}, ℕ}, the principal filter of the singleton {n}.

Equations

• Domain.Neighborhood.Example43.natElem n = Domain.Neighborhood.Example43.N.principal ⋯

theorem Domain.Neighborhood.Example43.mem_natElem_iff {n : ℕ} {Y : Set ℕ} : (natElem n).mem Y ↔ Y = Set.univ ∨ Y = {n}

A neighbourhood belongs to n̂ iff it is ℕ (the master) or the singleton {n}.

def Domain.Neighborhood.Example43.zeroElt : N.Element

Scott's 0 ∈ |N|, the distinguished zero of the structured domain.

Equations

• Domain.Neighborhood.Example43.zeroElt = Domain.Neighborhood.Example43.natElem 0

The strict lifting combinator n̂ ↦ val n, ⊥ ↦ ⊥.

def Domain.Neighborhood.Example43.constLiftN {β : Type u_1} (V : NeighborhoodSystem β) (val : ℕ → V.Element) : ApproximableMap N V

The strict approximable map N → V determined by a choice of value val n ∈ |V| for each n: it sends the total element n̂ to val n and the bottom ⊥ to ⊥. The relation X f Y holds when either X = Δ_N forces the blunt output Y = Δ_V (the strict ⊥ ↦ ⊥ clause), or X = {n} and Y is a neighbourhood of val n.

Definition 2.1 checks uniformly: (i) Δ_N f Δ_V; (ii) intersect outputs — distinct inputs are impossible (ℕ ≠ {n}, singletons are one-one), so both outputs come from the same val n and inter_mem of the filter val n applies; (iii) sharpening {n} ⊆ X keeps the input a singleton {n}, and up_mem of val n widens the output, while a blunt input Δ_N forces Δ_V.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.Example43.constLiftN_natElem {β : Type u_1} (V : NeighborhoodSystem β) (val : ℕ → V.Element) (n : ℕ) : (constLiftN V val).toElementMap (natElem n) = val n

Computation on the total elements. f(n̂) = val n.

theorem Domain.Neighborhood.Example43.constLiftN_bot {β : Type u_1} (V : NeighborhoodSystem β) (val : ℕ → V.Element) : (constLiftN V val).toElementMap N.bot = V.bot

Computation on bottom (strictness). f(⊥) = ⊥.

The successor map succ : N → N.

def Domain.Neighborhood.Example43.succMap : ApproximableMap N N

Example 4.3 — succ. succ(n) = n + 1, strict (succ(⊥) = ⊥).

Equations

• Domain.Neighborhood.Example43.succMap = Domain.Neighborhood.Example43.constLiftN Domain.Neighborhood.Example43.N fun (n : ℕ) => Domain.Neighborhood.Example43.natElem (n + 1)

theorem Domain.Neighborhood.Example43.succMap_natElem (n : ℕ) : succMap.toElementMap (natElem n) = natElem (n + 1)

succ(n̂) = (n+1)^.

theorem Domain.Neighborhood.Example43.succMap_bot : succMap.toElementMap N.bot = N.bot

succ(⊥) = ⊥.

The predecessor map pred : N → N.

def Domain.Neighborhood.Example43.predVal : ℕ → N.Element

The value table for pred: pred(0) = ⊥, pred(k+1) = k.

Equations

• Domain.Neighborhood.Example43.predVal 0 = Domain.Neighborhood.Example43.N.bot
• Domain.Neighborhood.Example43.predVal k.succ = Domain.Neighborhood.Example43.natElem k

def Domain.Neighborhood.Example43.predMap : ApproximableMap N N

Example 4.3 — pred. pred(0) = ⊥, pred(n+1) = n, strict (pred(⊥) = ⊥).

Equations

• Domain.Neighborhood.Example43.predMap = Domain.Neighborhood.Example43.constLiftN Domain.Neighborhood.Example43.N Domain.Neighborhood.Example43.predVal

theorem Domain.Neighborhood.Example43.predMap_natElem_succ (k : ℕ) : predMap.toElementMap (natElem (k + 1)) = natElem k

pred((n+1)^) = n̂.

theorem Domain.Neighborhood.Example43.predMap_natElem_zero : predMap.toElementMap (natElem 0) = N.bot

pred(0̂) = ⊥: predecessor of zero is undefined.

theorem Domain.Neighborhood.Example43.predMap_bot : predMap.toElementMap N.bot = N.bot

pred(⊥) = ⊥.

The test map zero : N → T.

@[reducible, inline]

abbrev Domain.Neighborhood.Example43.T : NeighborhoodSystem Example12.Token

The two-token truth domain T of Example 1.2 (= Example23.T).

Equations

• Domain.Neighborhood.Example43.T = Domain.Neighborhood.Example23.T

def Domain.Neighborhood.Example43.zeroVal : ℕ → T.Element

The value table for zero: zero(0) = true, zero(n+1) = false.

Equations

• Domain.Neighborhood.Example43.zeroVal 0 = Domain.Neighborhood.Example23.trueElt
• Domain.Neighborhood.Example43.zeroVal k.succ = Domain.Neighborhood.Example23.falseElt

def Domain.Neighborhood.Example43.zeroMap : ApproximableMap N T

Example 4.3 — zero. zero(0) = true, zero(n+1) = false, strict (zero(⊥) = ⊥).

Equations

• Domain.Neighborhood.Example43.zeroMap = Domain.Neighborhood.Example43.constLiftN Domain.Neighborhood.Example43.T Domain.Neighborhood.Example43.zeroVal

theorem Domain.Neighborhood.Example43.zeroMap_natElem_zero : zeroMap.toElementMap (natElem 0) = Example23.trueElt

zero(0̂) = true.

theorem Domain.Neighborhood.Example43.zeroMap_natElem_succ (n : ℕ) : zeroMap.toElementMap (natElem (n + 1)) = Example23.falseElt

zero((n+1)^) = false.

theorem Domain.Neighborhood.Example43.zeroMap_bot : zeroMap.toElementMap N.bot = T.bot

zero(⊥) = ⊥.

pred undoes succ.

theorem Domain.Neighborhood.Example43.predMap_succMap_natElem (n : ℕ) : predMap.toElementMap (succMap.toElementMap (natElem n)) = natElem n

pred(succ(n̂)) = n̂: the predecessor undoes the successor on total elements. (A sample of the "recursion" reasoning Scott highlights; cf. the iterated-summation example.)