Example 1.4 (Scott 1981, PRG-19, §1)

Scott's third worked example: the binary tree of depth 2. Tokens are the finite binary sequences of length ≤ 2, Δ = {Λ, 0, 1, 00, 01, 10, 11}, and the neighbourhoods are the subtrees rooted at each node:

𝒟 = {Δ, {0,00,01}, {1,10,11}, {00}, {01}, {10}, {11}}.

We encode the seven tokens as Fin 7:

token	Λ	0	1	00	01	10	11
Fin 7	0	1	2	3	4	5	6

so left = {0,00,01} = {1,3,4}, right = {1,10,11} = {2,5,6}, and the four leaves are the singletons {3}, {4}, {5}, {6}.

We build the neighbourhood system (Definition 1.1) and classify its domain elements (Definition 1.6): there are exactly seven filters. Unlike Example 1.3's linear chain, this is the first example with branching — at the partial elements elemZero/elemOne one has a choice of how to refine toward one of the four total (leaf) elements.

This is a concrete finite computation (fin_cases/simp); footprint [propext, Classical.choice, Quot.sound] — same as Examples 1.2/1.3.

@[reducible, inline]

abbrev Domain.Neighborhood.Example14.Token : Type

Tokens for Example 1.4: the binary tree Δ = {Λ,0,1,00,01,10,11}, encoded as Fin 7 (Λ=0, 0=1, 1=2, 00=3, 01=4, 10=5, 11=6).

Equations

• Domain.Neighborhood.Example14.Token = Fin 7

def Domain.Neighborhood.Example14.master : Set Token

The master neighbourhood Δ (the whole tree).

Equations

• Domain.Neighborhood.Example14.master = Set.univ

def Domain.Neighborhood.Example14.left : Set Token

The left subtree {0, 00, 01} = {1, 3, 4}.

Equations

• Domain.Neighborhood.Example14.left = {1, 3, 4}

def Domain.Neighborhood.Example14.right : Set Token

The right subtree {1, 10, 11} = {2, 5, 6}.

Equations

• Domain.Neighborhood.Example14.right = {2, 5, 6}

def Domain.Neighborhood.Example14.leaf00 : Set Token

The leaf {00} = {3}.

Equations

• Domain.Neighborhood.Example14.leaf00 = {3}

def Domain.Neighborhood.Example14.leaf01 : Set Token

The leaf {01} = {4}.

Equations

• Domain.Neighborhood.Example14.leaf01 = {4}

def Domain.Neighborhood.Example14.leaf10 : Set Token

The leaf {10} = {5}.

Equations

• Domain.Neighborhood.Example14.leaf10 = {5}

def Domain.Neighborhood.Example14.leaf11 : Set Token

The leaf {11} = {6}.

Equations

• Domain.Neighborhood.Example14.leaf11 = {6}

def Domain.Neighborhood.Example14.memSet : Set (Set Token)

The seven neighbourhoods of Example 1.4.

Equations

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

def Domain.Neighborhood.Example14.mem (X : Set Token) : Prop

Membership in the neighbourhood system 𝒟 of Example 1.4.

Equations

• Domain.Neighborhood.Example14.mem X = (X ∈ Domain.Neighborhood.Example14.memSet)

theorem Domain.Neighborhood.Example14.mem_master : mem master

theorem Domain.Neighborhood.Example14.mem_left : mem left

theorem Domain.Neighborhood.Example14.mem_right : mem right

theorem Domain.Neighborhood.Example14.mem_leaf00 : mem leaf00

theorem Domain.Neighborhood.Example14.mem_leaf01 : mem leaf01

theorem Domain.Neighborhood.Example14.mem_leaf10 : mem leaf10

theorem Domain.Neighborhood.Example14.mem_leaf11 : mem leaf11

theorem Domain.Neighborhood.Example14.mem_iff (X : Set Token) : mem X ↔ X = master ∨ X = left ∨ X = right ∨ X = leaf00 ∨ X = leaf01 ∨ X = leaf10 ∨ X = leaf11

A neighbourhood of Example 1.4 is exactly one of the seven.

theorem Domain.Neighborhood.Example14.not_mem_empty : ¬mem ∅

Distinctness of neighbourhoods (only the pairs needed below).

Nested-subset facts.

"Which neighbourhoods contain a given one" (upward classification).

Intersections.

def Domain.Neighborhood.Example14.neighborhoodSystem : NeighborhoodSystem Token

Example 1.4. The binary-tree neighbourhood system on Δ = {Λ,0,1,00,01,10,11}.

Equations

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

def Domain.Neighborhood.Example14.neighborhoodSystem.bot : neighborhoodSystem.Element

The bottom element ⊥ = {Δ} (node Λ).

Equations

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

def Domain.Neighborhood.Example14.neighborhoodSystem.elemZero : neighborhoodSystem.Element

The partial element {Δ, left} (node 0): the left branch is decided.

Equations

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

def Domain.Neighborhood.Example14.neighborhoodSystem.elemOne : neighborhoodSystem.Element

The partial element {Δ, right} (node 1): the right branch is decided.

Equations

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

def Domain.Neighborhood.Example14.neighborhoodSystem.elem00 : neighborhoodSystem.Element

The total element {Δ, left, leaf00} (leaf 00).

Equations

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

@[simp]

theorem Domain.Neighborhood.Example14.neighborhoodSystem.elem00_mem_leaf00 : elem00.mem leaf00

def Domain.Neighborhood.Example14.neighborhoodSystem.elem01 : neighborhoodSystem.Element

The total element {Δ, left, leaf01} (leaf 01).

Equations

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

def Domain.Neighborhood.Example14.neighborhoodSystem.elem10 : neighborhoodSystem.Element

The total element {Δ, right, leaf10} (leaf 10).

Equations

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

def Domain.Neighborhood.Example14.neighborhoodSystem.elem11 : neighborhoodSystem.Element

The total element {Δ, right, leaf11} (leaf 11).

Equations

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

Filter classification: the seven elements.

theorem Domain.Neighborhood.Example14.neighborhoodSystem.element_classification (x : neighborhoodSystem.Element) : x = bot ∨ x = elemZero ∨ x = elemOne ∨ x = elem00 ∨ x = elem01 ∨ x = elem10 ∨ x = elem11

Example 1.4 classification. Every filter is one of the seven: the bottom ⊥, the two branch partials elemZero/elemOne, or one of the four total leaf elements.

The approximation order (Definition 1.8): a branching tree.

theorem Domain.Neighborhood.Example14.neighborhoodSystem.bot_lt_elemZero : bot < elemZero

theorem Domain.Neighborhood.Example14.neighborhoodSystem.bot_lt_elemOne : bot < elemOne

theorem Domain.Neighborhood.Example14.neighborhoodSystem.elemZero_lt_elem00 : elemZero < elem00

theorem Domain.Neighborhood.Example14.neighborhoodSystem.elemZero_lt_elem01 : elemZero < elem01

theorem Domain.Neighborhood.Example14.neighborhoodSystem.elemOne_lt_elem10 : elemOne < elem10

theorem Domain.Neighborhood.Example14.neighborhoodSystem.elemOne_lt_elem11 : elemOne < elem11

theorem Domain.Neighborhood.Example14.neighborhoodSystem.elem00_maximal (x : neighborhoodSystem.Element) (h : elem00 ≤ x) : x = elem00

theorem Domain.Neighborhood.Example14.neighborhoodSystem.elem01_maximal (x : neighborhoodSystem.Element) (h : elem01 ≤ x) : x = elem01

theorem Domain.Neighborhood.Example14.neighborhoodSystem.elem10_maximal (x : neighborhoodSystem.Element) (h : elem10 ≤ x) : x = elem10

theorem Domain.Neighborhood.Example14.neighborhoodSystem.elem11_maximal (x : neighborhoodSystem.Element) (h : elem11 ≤ x) : x = elem11