Exercise 6.21 (Scott 1981, PRG-19, §6) — the separated sum ⊕ and product ⊗

EXERCISE 6.21. Do the same as 6.19 and 6.20 when the functors are also allowed to be generated by the operations D₀ ⊕ D₁ = {{Λ} ∪ 0Δ₀ ∪ 1Δ₁} ∪ {0X ∣ X ∈ D₀ ∖ {Δ₀}} ∪ {1Y ∣ Y ∈ D₁ ∖ {Δ₁}}, D₀ ⊗ D₁ = {{Λ} ∪ 0Δ₀ ∪ 1Δ₁} ∪ {{Λ} ∪ 0X ∪ 1Y ∣ X ∈ D₀ ∖ {Δ₀} and Y ∈ D₁ ∖ {Δ₁}}. Generalize all of +, ×, ⊕, ⊗ to combinations of several terms, not just the binary sums and products.

This module extends Exercise 6.19 Part B (Exercise619PartB.lean) with the two coalesced operations. The difference from the separated sum +/product × of 6.19 is that ⊕/⊗ delete the improper tagged copies 0Δ₀ and 1Δ₁: in domain terms this identifies the two bottoms (⊕ is the coalesced sum, ⊗ the smash product), whereas +/× keep them apart. Both share the same master {Λ} ∪ 0Δ₀ ∪ 1Δ₁ as +/×.

Contents (this stage: objects)

• oplusTok/otimesTok — the two token-level systems over Str = {0,1}*, each ∅-free.
• ScottSys.oplus/ScottSys.otimes — the same, repackaged as objects of Scott's category.

Everything is choice-free (#print axioms ⊆ {propext, Quot.sound}).

The coalesced sum D₀ ⊕ D₁ over {0,1}*

D₀ ⊕ D₁ = {M} ∪ {0X ∣ X ∈ 𝒟₀, X ≠ Δ₀} ∪ {1Y ∣ Y ∈ 𝒟₁, Y ≠ Δ₁}, where M = {Λ} ∪ 0Δ₀ ∪ 1Δ₁ is the shared sumTokMaster.

theorem Domain.Neighborhood.Exercise619.inter_ne_of_ne_left {X X' Δ : Set ExampleB.Str} (hX : X ⊆ Δ) (hne : X ≠ Δ) : X ∩ X' ≠ Δ

If X ⊆ Δ and X ≠ Δ, then any intersection X ∩ X' is still ≠ Δ (it is ⊆ X ⊊ Δ).

theorem Domain.Neighborhood.Exercise619.inter_ne_of_ne_right {X X' Δ : Set ExampleB.Str} (hX' : X' ⊆ Δ) (hne : X' ≠ Δ) : X ∩ X' ≠ Δ

def Domain.Neighborhood.Exercise619.oplusTok (D₀ D₁ : NeighborhoodSystem ExampleB.Str) (h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty) (h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty) : NeighborhoodSystem ExampleB.Str

Exercise 6.21 — the coalesced sum system 𝒟₀ ⊕ 𝒟₁ over {0,1}*. As sumTok, but the improper copies 0Δ₀, 1Δ₁ are removed (X ≠ Δ₀, Y ≠ Δ₁), so the two bottoms are identified.

Equations

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

theorem Domain.Neighborhood.Exercise619.oplusTok_nonempty {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} (W : Set ExampleB.Str) : (oplusTok D₀ D₁ h₀ h₁).mem W → W.Nonempty

The smash product D₀ ⊗ D₁ over {0,1}*

D₀ ⊗ D₁ = {M} ∪ {{Λ} ∪ 0X ∪ 1Y ∣ X ∈ 𝒟₀, X ≠ Δ₀, Y ∈ 𝒟₁, Y ≠ Δ₁}, where again M = {Λ} ∪ 0Δ₀ ∪ 1Δ₁ = prodTokNbhd Δ₀ Δ₁. The improper rectangles touching a top coordinate (other than the full top M) are removed.

def Domain.Neighborhood.Exercise619.otimesTok (D₀ D₁ : NeighborhoodSystem ExampleB.Str) : NeighborhoodSystem ExampleB.Str

Exercise 6.21 — the smash product system 𝒟₀ ⊗ 𝒟₁ over {0,1}*. As prodTok, but proper rectangles must avoid both top coordinates (X ≠ Δ₀, Y ≠ Δ₁); the full top M = prodTokNbhd Δ₀ Δ₁ is kept as the master.

Equations

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

theorem Domain.Neighborhood.Exercise619.otimesTok_nonempty {D₀ D₁ : NeighborhoodSystem ExampleB.Str} (W : Set ExampleB.Str) : (otimesTok D₀ D₁).mem W → W.Nonempty

Repackaged as objects of Scott's category

def Domain.Neighborhood.Exercise619.ScottSys.oplus (A₀ A₁ : ScottSys) : ScottSys

The coalesced sum object 𝒟₀ ⊕ 𝒟₁.

Equations

• A₀.oplus A₁ = { sys := Domain.Neighborhood.Exercise619.oplusTok A₀.sys A₁.sys ⋯ ⋯, ne := ⋯ }

def Domain.Neighborhood.Exercise619.ScottSys.otimes (A₀ A₁ : ScottSys) : ScottSys

The smash product object 𝒟₀ ⊗ 𝒟₁.

Equations

• A₀.otimes A₁ = { sys := Domain.Neighborhood.Exercise619.otimesTok A₀.sys A₁.sys, ne := ⋯ }

Membership inversions

theorem Domain.Neighborhood.Exercise619.oplusTok_mem_master {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} : (oplusTok D₀ D₁ h₀ h₁).mem (sumTokMaster D₀ D₁)

theorem Domain.Neighborhood.Exercise619.oplusTok_mem_embF {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {X : Set ExampleB.Str} (hX : D₀.mem X) (hXne : X ≠ D₀.master) : (oplusTok D₀ D₁ h₀ h₁).mem (Example62.embBit false X)

theorem Domain.Neighborhood.Exercise619.oplusTok_mem_embT {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {Y : Set ExampleB.Str} (hY : D₁.mem Y) (hYne : Y ≠ D₁.master) : (oplusTok D₀ D₁ h₀ h₁).mem (Example62.embBit true Y)

theorem Domain.Neighborhood.Exercise619.oplusTok_mem_embF_inv {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {W : Set ExampleB.Str} (h : (oplusTok D₀ D₁ h₀ h₁).mem (Example62.embBit false W)) : D₀.mem W

theorem Domain.Neighborhood.Exercise619.oplusTok_mem_embT_inv {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {W : Set ExampleB.Str} (h : (oplusTok D₀ D₁ h₀ h₁).mem (Example62.embBit true W)) : D₁.mem W

theorem Domain.Neighborhood.Exercise619.otimesTok_mem_master {D₀ D₁ : NeighborhoodSystem ExampleB.Str} : (otimesTok D₀ D₁).mem (prodTokNbhd D₀.master D₁.master)

theorem Domain.Neighborhood.Exercise619.otimesTok_mem_prod {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {X Y : Set ExampleB.Str} (hX : D₀.mem X) (hY : D₁.mem Y) (hXne : X ≠ D₀.master) (hYne : Y ≠ D₁.master) : (otimesTok D₀ D₁).mem (prodTokNbhd X Y)

theorem Domain.Neighborhood.Exercise619.otimesTok_mem_prod_inv {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {X Y : Set ExampleB.Str} (h : (otimesTok D₀ D₁).mem (prodTokNbhd X Y)) (hX : X ≠ D₀.master) : D₀.mem X ∧ D₁.mem Y

Monotone on domains: ◁ is carried componentwise

theorem Domain.Neighborhood.Exercise619.oplusTok_subsystem {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : (A₀.oplus A₁).sys ◁ (B₀.oplus B₁).sys

The coalesced sum carries the subsystem relation componentwise.

theorem Domain.Neighborhood.Exercise619.otimesTok_subsystem {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : (A₀.otimes A₁).sys ◁ (B₀.otimes B₁).sys

The smash product carries the subsystem relation componentwise.

The functorial action of the coalesced sum on (strict) maps

The relation has the same shape as sumMapTok but with two changes forced by coalescence: proper tagged copies require the components to be proper (X ≠ Δ₀, X' ≠ Δ₀'), and the master/collapse row (W ∈ 𝒟₀⊕𝒟₁ ∧ W' = M) sends every neighbourhood to the top M (which is always valid, the top being the least informative output, and is exactly what handles f₀(X) = Δ₀' collapsing back to the shared bottom).

def Domain.Neighborhood.Exercise619.oplusMapTok {A₀ A₁ B₀ B₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) : ApproximableMap (A₀.oplus A₁).sys (B₀.oplus B₁).sys

f₀ ⊕ f₁, the action of the coalesced sum on maps.

Equations

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

theorem Domain.Neighborhood.Exercise619.oplusMapTok_isStrict {A₀ A₁ B₀ B₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) : Exercise510.IsStrict (oplusMapTok f₀ f₁)

oplusMapTok is always strict.

theorem Domain.Neighborhood.Exercise619.oplusMapTok_id {A₀ A₁ : ScottSys} : oplusMapTok (ApproximableMap.idMap A₀.sys) (ApproximableMap.idMap A₁.sys) = ApproximableMap.idMap (A₀.oplus A₁).sys

(I ⊕ I) = I.

theorem Domain.Neighborhood.Exercise619.oplusMapTok_comp {A₀ A₁ B₀ B₁ C₀ C₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) {g₀ : ApproximableMap B₀.sys C₀.sys} {g₁ : ApproximableMap B₁.sys C₁.sys} (hg₀ : Exercise510.IsStrict g₀) (hg₁ : Exercise510.IsStrict g₁) : oplusMapTok (g₀.comp f₀) (g₁.comp f₁) = (oplusMapTok g₀ g₁).comp (oplusMapTok f₀ f₁)

(g₀ ∘ f₀) ⊕ (g₁ ∘ f₁) = (g₀ ⊕ g₁) ∘ (f₀ ⊕ f₁) for strict g₀, g₁. (Strictness of the outer maps is exactly what prevents an intermediate top f₀(X) = Δ₀' from being re-expanded — that is the categorical reason ⊕ is a functor only on the strict-map category Scott restricts to.)

theorem Domain.Neighborhood.Exercise619.oplusMapTok_mono {A₀ A₁ B₀ B₁ : ScottSys} {f₀ f₀' : ApproximableMap A₀.sys B₀.sys} {f₁ f₁' : ApproximableMap A₁.sys B₁.sys} (h0 : f₀ ≤ f₀') (h1 : f₁ ≤ f₁') : oplusMapTok f₀ f₁ ≤ oplusMapTok f₀' f₁'

oplusMapTok is monotone in both arguments.

The functorial action of the smash product on (strict) maps

As prodMapTok, but proper rectangles require both components proper, and a master/collapse row absorbs a boundary hit f₀(X) = Δ₀' (or f₁(Y) = Δ₁') into the top M.

def Domain.Neighborhood.Exercise619.otimesMapTok {A₀ A₁ B₀ B₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) : ApproximableMap (A₀.otimes A₁).sys (B₀.otimes B₁).sys

f₀ ⊗ f₁, the action of the smash product on maps.

Equations

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

theorem Domain.Neighborhood.Exercise619.otimesMapTok_isStrict {A₀ A₁ B₀ B₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) : Exercise510.IsStrict (otimesMapTok f₀ f₁)

otimesMapTok is always strict.

theorem Domain.Neighborhood.Exercise619.otimesMapTok_id {A₀ A₁ : ScottSys} : otimesMapTok (ApproximableMap.idMap A₀.sys) (ApproximableMap.idMap A₁.sys) = ApproximableMap.idMap (A₀.otimes A₁).sys

(I ⊗ I) = I.

theorem Domain.Neighborhood.Exercise619.otimesMapTok_comp {A₀ A₁ B₀ B₁ C₀ C₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) {g₀ : ApproximableMap B₀.sys C₀.sys} {g₁ : ApproximableMap B₁.sys C₁.sys} (hg₀ : Exercise510.IsStrict g₀) (hg₁ : Exercise510.IsStrict g₁) : otimesMapTok (g₀.comp f₀) (g₁.comp f₁) = (otimesMapTok g₀ g₁).comp (otimesMapTok f₀ f₁)

(g₀ ∘ f₀) ⊗ (g₁ ∘ f₁) = (g₀ ⊗ g₁) ∘ (f₀ ⊗ f₁) for strict g₀, g₁.

theorem Domain.Neighborhood.Exercise619.otimesMapTok_mono {A₀ A₁ B₀ B₁ : ScottSys} {f₀ f₀' : ApproximableMap A₀.sys B₀.sys} {f₁ f₁' : ApproximableMap A₁.sys B₁.sys} (h0 : f₀ ≤ f₀') (h1 : f₁ ≤ f₁') : otimesMapTok f₀ f₁ ≤ otimesMapTok f₀' f₁'

otimesMapTok is monotone in both arguments.

The extended functor-expression algebra GExpr

Scott's "do the same as 6.19 and 6.20 when the functors are also allowed to be generated by the operations ⊕, ⊗": the closed family of constructs is enlarged from FExpr (constants, identity, +, ×) to also include the coalesced ⊕ and the smash ⊗. The functor laws and the on-maps/on-domains continuity properties are re-established by induction; the ⊕/⊗ composition law carries the strictness hypothesis (Scott's category is the strict-map category, and that is exactly what makes ⊕/⊗ functorial).

inductive Domain.Neighborhood.Exercise619.GExpr : Type

The extended functor-expression algebra (constants, identity, +, ×, ⊕, ⊗).

• const : ScottSys → GExpr

  The constant functor T(X) = 𝒟.

• var : GExpr

  The identity functor T(X) = X.

• sum : GExpr → GExpr → GExpr

  The separated sum T₀(X) + T₁(X).

• prod : GExpr → GExpr → GExpr

  The separated product T₀(X) × T₁(X).

• oplus : GExpr → GExpr → GExpr

  The coalesced sum T₀(X) ⊕ T₁(X).

• otimes : GExpr → GExpr → GExpr

  The smash product T₀(X) ⊗ T₁(X).

def Domain.Neighborhood.Exercise619.GExpr.obj : GExpr → ScottSys → ScottSys

The action of T on objects.

Equations

• (Domain.Neighborhood.Exercise619.GExpr.const D).obj x✝ = D
• Domain.Neighborhood.Exercise619.GExpr.var.obj x✝ = x✝
• (a.sum b).obj x✝ = (a.obj x✝).sum (b.obj x✝)
• (a.prod b).obj x✝ = (a.obj x✝).prod (b.obj x✝)
• (a.oplus b).obj x✝ = (a.obj x✝).oplus (b.obj x✝)
• (a.otimes b).obj x✝ = (a.obj x✝).otimes (b.obj x✝)

def Domain.Neighborhood.Exercise619.GExpr.map (T : GExpr) {X Y : ScottSys} : ApproximableMap X.sys Y.sys → ApproximableMap (T.obj X).sys (T.obj Y).sys

The action of T on maps.

Equations

• (Domain.Neighborhood.Exercise619.GExpr.const D).map x✝ = Domain.Neighborhood.ApproximableMap.idMap D.sys
• Domain.Neighborhood.Exercise619.GExpr.var.map x✝ = x✝
• (a.sum b).map x✝ = Domain.Neighborhood.Exercise619.sumMapTok (a.map x✝) (b.map x✝)
• (a.prod b).map x✝ = Domain.Neighborhood.Exercise619.prodMapTok (a.map x✝) (b.map x✝)
• (a.oplus b).map x✝ = Domain.Neighborhood.Exercise619.oplusMapTok (a.map x✝) (b.map x✝)
• (a.otimes b).map x✝ = Domain.Neighborhood.Exercise619.otimesMapTok (a.map x✝) (b.map x✝)

theorem Domain.Neighborhood.Exercise619.GExpr.map_isStrict (T : GExpr) {X Y : ScottSys} (f : ApproximableMap X.sys Y.sys) : Exercise510.IsStrict f → Exercise510.IsStrict (T.map f)

Every T preserves strictness.

theorem Domain.Neighborhood.Exercise619.GExpr.map_id (T : GExpr) (X : ScottSys) : T.map (ApproximableMap.idMap X.sys) = ApproximableMap.idMap (T.obj X).sys

Functor law 1 — T(I_X) = I_{T(X)}.

theorem Domain.Neighborhood.Exercise619.GExpr.map_comp (T : GExpr) {X Y Z : ScottSys} (f : ApproximableMap X.sys Y.sys) {g : ApproximableMap Y.sys Z.sys} : Exercise510.IsStrict g → T.map (g.comp f) = (T.map g).comp (T.map f)

Functor law 2 — T(g ∘ f) = T(g) ∘ T(f) for strict g. Together with map_id, these are all functors of the strict-map category. The strictness of g is needed (and only) for the coalesced ⊕/⊗, whose composition law oplusMapTok_comp/otimesMapTok_comp requires it.

theorem Domain.Neighborhood.Exercise619.GExpr.map_mono (T : GExpr) {X Y : ScottSys} {f f' : ApproximableMap X.sys Y.sys} : f ≤ f' → T.map f ≤ T.map f'

λf. T(f) is monotone (the order half of continuous on maps).

theorem Domain.Neighborhood.Exercise619.GExpr.obj_subsystem (T : GExpr) {X Y : ScottSys} : X.sys ◁ Y.sys → (T.obj X).sys ◁ (T.obj Y).sys

λX. T(X) is monotone on domains.

Continuous on domains

theorem Domain.Neighborhood.Exercise619.GExpr.obj_continuous_mp (T : GExpr) {ℱ : Set ScottSys} {U : ScottSys} : DirectedOn (fun (a b : ScottSys) => a.sys ◁ b.sys) ℱ → ℱ.Nonempty → (∀ D ∈ ℱ, D.sys ◁ U.sys) → (∀ (X : Set ExampleB.Str), U.sys.mem X ↔ ∃ D ∈ ℱ, D.sys.mem X) → ∀ {W : Set ExampleB.Str}, (T.obj U).sys.mem W → ∃ D ∈ ℱ, (T.obj D).sys.mem W

Forward direction of continuity on domains for GExpr.

theorem Domain.Neighborhood.Exercise619.GExpr.obj_continuous (T : GExpr) {ℱ : Set ScottSys} {U : ScottSys} (hdir : DirectedOn (fun (a b : ScottSys) => a.sys ◁ b.sys) ℱ) (hne : ℱ.Nonempty) (hsub : ∀ D ∈ ℱ, D.sys ◁ U.sys) (hU : ∀ (X : Set ExampleB.Str), U.sys.mem X ↔ ∃ D ∈ ℱ, D.sys.mem X) (W : Set ExampleB.Str) : (T.obj U).sys.mem W ↔ ∃ D ∈ ℱ, (T.obj D).sys.mem W

λD. T(D) is continuous on domains.

Continuous on maps

theorem Domain.Neighborhood.Exercise619.GExpr.map_continuous_mp (T : GExpr) {I : Type} {X Y : ScottSys} {g : I → ApproximableMap X.sys Y.sys} {f : ApproximableMap X.sys Y.sys} [Nonempty I] : (∀ (i j : I), ∃ (k : I), g i ≤ g k ∧ g j ≤ g k) → (∀ (A B : Set ExampleB.Str), f.rel A B ↔ ∃ (i : I), (g i).rel A B) → ∀ {A B : Set ExampleB.Str}, (T.map f).rel A B → ∃ (i : I), (T.map (g i)).rel A B

Forward direction of continuity on maps for GExpr.

theorem Domain.Neighborhood.Exercise619.GExpr.map_continuous (T : GExpr) {I : Type} [Nonempty I] {X Y : ScottSys} (g : I → ApproximableMap X.sys Y.sys) (f : ApproximableMap X.sys Y.sys) (hdir : ∀ (i j : I), ∃ (k : I), g i ≤ g k ∧ g j ≤ g k) (hf : ∀ (A B : Set ExampleB.Str), f.rel A B ↔ ∃ (i : I), (g i).rel A B) (A B : Set ExampleB.Str) : (T.map f).rel A B ↔ ∃ (i : I), (T.map (g i)).rel A B

λf. T(f) is continuous on maps.

Exercise 6.20 for the extended algebra — λΓ. tok(T({Γ})) is continuous,

so a fixed point exists

The masters of ⊕/⊗ coincide with those of +/× (all four equal {Λ} ∪ 0Δ₀ ∪ 1Δ₁), so the token-level recursion gFun has the same tagged-union body in all four binary cases. The 6.20 argument (continuity of λΓ. tok(T({Γ})) and existence of Γ = tok(T({Γ})), whence {Γ} ◁ T({Γ}) and Theorem 6.14 applies) goes through verbatim, reusing the generic helpers singletonSys, insertTag_mono, insertTag_continuous of Exercise 6.19 Part B.

def Domain.Neighborhood.Exercise619.gFun : GExpr → Set ExampleB.Str → Set ExampleB.Str

The token-level master recursion for GExpr. All four binary operations share the same body (sumTokMaster = prodTokNbhd on masters).

Equations

• One or more equations did not get rendered due to their size.
• Domain.Neighborhood.Exercise619.gFun (Domain.Neighborhood.Exercise619.GExpr.const C) x✝ = C.sys.master
• Domain.Neighborhood.Exercise619.gFun Domain.Neighborhood.Exercise619.GExpr.var x✝ = x✝

theorem Domain.Neighborhood.Exercise619.gFun_eq_master (T : GExpr) {Γ : Set ExampleB.Str} (h : Γ.Nonempty) : gFun T Γ = (T.obj (singletonSys Γ h)).sys.master

gFun T Γ = tok(T({Γ})).

theorem Domain.Neighborhood.Exercise619.gFun_mono (T : GExpr) {Γ Γ' : Set ExampleB.Str} (h : Γ ⊆ Γ') : gFun T Γ ⊆ gFun T Γ'

λΓ. tok(T({Γ})) is monotone.

theorem Domain.Neighborhood.Exercise619.gFun_continuous (T : GExpr) {ℱ : Set (Set ExampleB.Str)} {U : Set ExampleB.Str} (_hdir : DirectedOn (fun (x1 x2 : Set ExampleB.Str) => x1 ⊆ x2) ℱ) (hne : ℱ.Nonempty) (hU : ∀ (w : ExampleB.Str), w ∈ U ↔ ∃ Γ ∈ ℱ, w ∈ Γ) (w : ExampleB.Str) : w ∈ gFun T U ↔ ∃ Γ ∈ ℱ, w ∈ gFun T Γ

λΓ. tok(T({Γ})) is continuous on {Γ ∣ Λ ∈ Γ}.

def Domain.Neighborhood.Exercise619.GExpr.RootedConst : GExpr → Prop

Λ ∈ tok(C) for every constant C occurring in T.

Equations

• (Domain.Neighborhood.Exercise619.GExpr.const C).RootedConst = ([] ∈ C.sys.master)
• Domain.Neighborhood.Exercise619.GExpr.var.RootedConst = True
• (a.sum b).RootedConst = (a.RootedConst ∧ b.RootedConst)
• (a.prod b).RootedConst = (a.RootedConst ∧ b.RootedConst)
• (a.oplus b).RootedConst = (a.RootedConst ∧ b.RootedConst)
• (a.otimes b).RootedConst = (a.RootedConst ∧ b.RootedConst)

theorem Domain.Neighborhood.Exercise619.gFun_nil_mem (T : GExpr) : T.RootedConst → ∀ {Γ : Set ExampleB.Str}, [] ∈ Γ → [] ∈ gFun T Γ

def Domain.Neighborhood.Exercise619.gIter (T : GExpr) : ℕ → Set ExampleB.Str

The Kleene iteration gFunⁿ({Λ}).

Equations

• Domain.Neighborhood.Exercise619.gIter T 0 = {[]}
• Domain.Neighborhood.Exercise619.gIter T n.succ = Domain.Neighborhood.Exercise619.gFun T (Domain.Neighborhood.Exercise619.gIter T n)

theorem Domain.Neighborhood.Exercise619.nil_mem_gIter (T : GExpr) (hT : T.RootedConst) (n : ℕ) : [] ∈ gIter T n

theorem Domain.Neighborhood.Exercise619.gIter_mono_step (T : GExpr) (hT : T.RootedConst) (n : ℕ) : gIter T n ⊆ gIter T (n + 1)

theorem Domain.Neighborhood.Exercise619.gIter_mono (T : GExpr) (hT : T.RootedConst) {m n : ℕ} (hmn : m ≤ n) : gIter T m ⊆ gIter T n

theorem Domain.Neighborhood.Exercise619.gFun_iter_fixed (T : GExpr) (hT : T.RootedConst) : gFun T (⋃ (n : ℕ), gIter T n) = ⋃ (n : ℕ), gIter T n

The Kleene union is a fixed point of λΓ. tok(T({Γ})).

theorem Domain.Neighborhood.Exercise619.gExists_tok_fixedPoint (T : GExpr) (hT : T.RootedConst) : ∃ (Γ : Set ExampleB.Str), [] ∈ Γ ∧ gFun T Γ = Γ

Exercise 6.21/6.20 (token level). For any GExpr T whose constants contain Λ, there is a set Γ with Λ ∈ Γ and Γ = tok(T({Γ})).

theorem Domain.Neighborhood.Exercise619.gExists_singleton_subsystem (T : GExpr) (hT : T.RootedConst) : ∃ (Γ : Set ExampleB.Str) (h : Γ.Nonempty), (singletonSys Γ h).sys ◁ (T.obj (singletonSys Γ h)).sys

Exercise 6.21/6.20 (object level): {Γ} ◁ T({Γ}), so Theorem 6.14 applies for any construct T built from constants, identity, +, ×, ⊕, ⊗.

Generalizing +, ×, ⊕, ⊗ to combinations of several terms

Generalize all of +, ×, ⊕, ⊗ to combinations of several terms, not just the binary sums and products.

Because GExpr is closed under the binary operations, every finite combination of several terms T₀ ⋆ T₁ ⋆ ⋯ ⋆ Tₙ (for any ⋆ ∈ {+, ×, ⊕, ⊗}, in any nesting) is itself a GExpr — so the results already proved (map_id, map_comp, map_mono, map_continuous, obj_subsystem, obj_continuous, and the 6.20 fixed point gExists_singleton_subsystem) apply to all of them with no further work. The naryOp fold below packages the common right-nested n-ary constructs ⋆(a, [b, c, …]) = a ⋆ (b ⋆ (c ⋆ ⋯)) explicitly, and naryOp_rootedConst shows the Λ ∈ tok side-condition (needed for the 6.20 fixed point) is preserved, so every n-ary construct also has a solution Γ = tok(T({Γ})).

def Domain.Neighborhood.Exercise619.GExpr.naryOp (op : GExpr → GExpr → GExpr) (a : GExpr) : List GExpr → GExpr

Right-nested n-ary fold of a binary construct-operation op over a non-empty list a, l…. With op = .sum/.prod/.oplus/.otimes this is the n-ary +/×/⊕/⊗.

Equations

• Domain.Neighborhood.Exercise619.GExpr.naryOp op a [] = a
• Domain.Neighborhood.Exercise619.GExpr.naryOp op a (b :: l) = op a (Domain.Neighborhood.Exercise619.GExpr.naryOp op b l)

def Domain.Neighborhood.Exercise619.GExpr.narySum : GExpr → List GExpr → GExpr

n-ary separated sum T₀ + T₁ + ⋯ + Tₙ.

Equations

• Domain.Neighborhood.Exercise619.GExpr.narySum = Domain.Neighborhood.Exercise619.GExpr.naryOp Domain.Neighborhood.Exercise619.GExpr.sum

def Domain.Neighborhood.Exercise619.GExpr.naryProd : GExpr → List GExpr → GExpr

n-ary separated product T₀ × T₁ × ⋯ × Tₙ.

Equations

• Domain.Neighborhood.Exercise619.GExpr.naryProd = Domain.Neighborhood.Exercise619.GExpr.naryOp Domain.Neighborhood.Exercise619.GExpr.prod

def Domain.Neighborhood.Exercise619.GExpr.naryOplus : GExpr → List GExpr → GExpr

n-ary coalesced sum T₀ ⊕ T₁ ⊕ ⋯ ⊕ Tₙ.

Equations

• Domain.Neighborhood.Exercise619.GExpr.naryOplus = Domain.Neighborhood.Exercise619.GExpr.naryOp Domain.Neighborhood.Exercise619.GExpr.oplus

def Domain.Neighborhood.Exercise619.GExpr.naryOtimes : GExpr → List GExpr → GExpr

n-ary smash product T₀ ⊗ T₁ ⊗ ⋯ ⊗ Tₙ.

Equations

• Domain.Neighborhood.Exercise619.GExpr.naryOtimes = Domain.Neighborhood.Exercise619.GExpr.naryOp Domain.Neighborhood.Exercise619.GExpr.otimes

theorem Domain.Neighborhood.Exercise619.GExpr.naryOp_rootedConst {op : GExpr → GExpr → GExpr} (hop : ∀ (x y : GExpr), (op x y).RootedConst ↔ x.RootedConst ∧ y.RootedConst) (a : GExpr) (l : List GExpr) : a.RootedConst → (∀ b ∈ l, b.RootedConst) → (naryOp op a l).RootedConst

The Λ ∈ tok side-condition is preserved by any n-ary fold whose binary operation preserves it (all four of +, ×, ⊕, ⊗ do, definitionally).

theorem Domain.Neighborhood.Exercise619.narySum_singleton_subsystem (a : GExpr) (l : List GExpr) (ha : a.RootedConst) (hl : ∀ b ∈ l, b.RootedConst) : ∃ (Γ : Set ExampleB.Str) (h : Γ.Nonempty), (singletonSys Γ h).sys ◁ ((a.narySum l).obj (singletonSys Γ h)).sys

Every n-ary construct has a solution Γ = tok(T({Γ})) (so {Γ} ◁ T({Γ}) and 6.14 applies), illustrated for the n-ary separated sum; identical for naryProd/naryOplus/naryOtimes.

theorem Domain.Neighborhood.Exercise619.naryOplus_singleton_subsystem (a : GExpr) (l : List GExpr) (ha : a.RootedConst) (hl : ∀ b ∈ l, b.RootedConst) : ∃ (Γ : Set ExampleB.Str) (h : Γ.Nonempty), (singletonSys Γ h).sys ◁ ((a.naryOplus l).obj (singletonSys Γ h)).sys

theorem Domain.Neighborhood.Exercise619.naryProd_singleton_subsystem (a : GExpr) (l : List GExpr) (ha : a.RootedConst) (hl : ∀ b ∈ l, b.RootedConst) : ∃ (Γ : Set ExampleB.Str) (h : Γ.Nonempty), (singletonSys Γ h).sys ◁ ((a.naryProd l).obj (singletonSys Γ h)).sys

theorem Domain.Neighborhood.Exercise619.naryOtimes_singleton_subsystem (a : GExpr) (l : List GExpr) (ha : a.RootedConst) (hl : ∀ b ∈ l, b.RootedConst) : ∃ (Γ : Set ExampleB.Str) (h : Γ.Nonempty), (singletonSys Γ h).sys ◁ ((a.naryOtimes l).obj (singletonSys Γ h)).sys