def WeightedNetKAT.Pk? (F N : Type) [Listed F] : Type

Pk? is the set of complete tests.

Equations

• WeightedNetKAT.Pk? F N = Pk[F,N]

def WeightedNetKAT.Pk! (F N : Type) [Listed F] : Type

Pk! is the set of all complete assignments.

Equations

• WeightedNetKAT.Pk! F N = Pk[F,N]

def WeightedNetKAT.GS (F N : Type) [Listed F] : Type

The language of guarded strings.

Isomorphically defined as Pk? ⬝ (Pk! ⬝ dup)* ⬝ Pk!.

Equations

• WeightedNetKAT.GS F N = (Pk[F,N] × List Pk[F,N] × Pk[F,N])

def WeightedNetKAT.«termGS[_,_]» : Lean.ParserDescr

Equations

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

@[implicit_reducible]

instance WeightedNetKAT.instDecidableEqGS {F N : Type} [Listed F] [DecidableEq F] [DecidableEq N] : DecidableEq (GS F N)

Equations

• WeightedNetKAT.instDecidableEqGS = instDecidableEqProd

instance WeightedNetKAT.instCountableGSOfListedOfDecidableEq {F N : Type} [Listed F] [Listed N] [DecidableEq N] : Countable (GS F N)

def WeightedNetKAT.«termGs[_;_]» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«termGs[_;_;Dup;_]» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«termGs[_;_;Dup;_;Dup;_]» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«termGs[_;_;Dup;_;Dup;_;Dup;_]» : Lean.ParserDescr

Equations

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

class WeightedNetKAT.Concat (α : Type u_1) (β : outParam (Type u_2)) : Type (max u_1 u_2)

• concat : α → α → β

  Concatenation ♢

def WeightedNetKAT.«term_♢_» : Lean.TrailingParserDescr

Concatenation ♢

Equations

• WeightedNetKAT.«term_♢_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_♢_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ♢ ") (Lean.ParserDescr.cat `term 71))

class WeightedNetKAT.ConcatAssoc (α : Type u_1) [Concat α α] : Prop

• concat_assoc (a b c : α) : a ♢ b ♢ c = a ♢ (b ♢ c)

@[implicit_reducible]

instance WeightedNetKAT.instConcatGSOption {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] : Concat (GS F N) (Option (GS F N))

Equations

• WeightedNetKAT.instConcatGSOption = { concat := fun (x x_1 : WeightedNetKAT.GS F N) => match x, x_1 with | (α, x, β), (γ, y, ξ) => if β = γ then some (α, x ++ y, ξ) else none }

def WeightedNetKAT.GS.splitAtJoined {F : Type} [Listed F] {N : Type} (g : GS F N) (n : ℕ) (γ : Pk[F,N]) : GS F N × GS F N

Equations

• WeightedNetKAT.GS.splitAtJoined (g₀, g_2, gₙ) n γ = match List.splitAt n g_2 with | (l, r) => ((g₀, l, γ), γ, r, gₙ)

@[implicit_reducible]

instance WeightedNetKAT.instConcatCountsuppGS {F : Type} [Listed F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] : Concat (GS F N →c 𝒮) (GS F N →c 𝒮)

Equations

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

theorem WeightedNetKAT.G.concat_apply {F : Type} [Listed F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] {L R : GS F N →c 𝒮} {xₙ : GS F N} : (L ♢ R) xₙ = ∑ i ∈ ..=‖xₙ.2.1‖, ∑ γ : Pk[F,N], L (xₙ.splitAtJoined i γ).1 * R (xₙ.splitAtJoined i γ).2

theorem WeightedNetKAT.G.concat_eq_ωSum {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {L R : GS F N →c 𝒮} {xₙ : GS F N} : (L ♢ R) xₙ = ω∑ (x : ↑L.support) (y : ↑R.support), if ↑x ♢ ↑y = some xₙ then L ↑x * R ↑y else 0

@[simp]

theorem WeightedNetKAT.GS.mk_eq {F : Type} [Listed F] {N : Type} {α β γ δ : Pk[F,N]} {xs : List Pk[F,N]} : (α, [], β) = (γ, xs, δ) ↔ α = γ ∧ xs = [] ∧ β = δ

@[simp]

theorem WeightedNetKAT.GS.mk_one_eq {F : Type} [Listed F] {N : Type} {α κ β γ δ : Pk[F,N]} {xs : List Pk[F,N]} : (α, [κ], β) = (γ, xs, δ) ↔ α = γ ∧ xs = [κ] ∧ β = δ

def WeightedNetKAT.G.ofPk {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] (f : Pk[F,N] → GS F N) : GS F N →c 𝒮

Equations

• WeightedNetKAT.G.ofPk f = { toFun := fun (x : WeightedNetKAT.GS F N) => if ∃ (α : Pk[F,N]), f α = x then 1 else 0, countable := ⋯ }

def WeightedNetKAT.G.ofConst {F : Type} [Listed F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [DecidableEq (GS F N)] (f : GS F N) : GS F N →c 𝒮

Equations

• WeightedNetKAT.G.ofConst f = { toFun := fun (x : WeightedNetKAT.GS F N) => if f = x then 1 else 0, countable := ⋯ }

@[simp]

theorem WeightedNetKAT.G.ofPk_apply {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] (f : Pk[F,N] → GS F N) (x : GS F N) : (ofPk f) x = if ∃ (α : Pk[F,N]), f α = x then 1 else 0

@[simp]

theorem WeightedNetKAT.G.ofConst_apply {F : Type} [Listed F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [DecidableEq (GS F N)] (f x : GS F N) : (ofConst f) x = if f = x then 1 else 0

@[irreducible]

noncomputable def WeightedNetKAT.G {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (p : RPol 𝒮) : GS F N →c 𝒮

Equations

• G⟦~WeightedNetKAT.RPol.Drop⟧ = 0
• G⟦skip⟧ = WeightedNetKAT.G.ofPk fun (α : Pk[F,N]) => (α, [], α)
• G⟦@test ~α⟧ = WeightedNetKAT.G.ofConst (α, [], α)
• G⟦@mod ~π⟧ = WeightedNetKAT.G.ofPk fun (α : Pk[F,N]) => (α, [], π)
• G⟦dup⟧ = WeightedNetKAT.G.ofPk fun (α : Pk[F,N]) => (α, [α], α)
• G⟦~p₁ ⨁ ~p₂⟧ = G⟦~p₁⟧ + G⟦~p₂⟧
• G⟦~p₁; ~p₂⟧ = G⟦~p₁⟧ ♢ G⟦~p₂⟧
• G⟦~w ⨀ ~p₁⟧ = w * G⟦~p₁⟧
• G⟦~p₁*⟧ = ω∑ (n : ℕ), G⟦~(p₁ ^ n)⟧

def WeightedNetKAT.«termG⟦_⟧» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.G.unexpander : Lean.PrettyPrinter.Unexpander

Equations

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

@[simp]

theorem WeightedNetKAT.G.skip_eq {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {gs : GS F N} : G⟦skip⟧ gs = if gs.1 = gs.2.2 ∧ gs.2.1 = [] then 1 else 0

@[simp]

theorem WeightedNetKAT.G.test_eq {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {gs : GS F N} {π : Pk[F,N]} : G⟦@test ~π⟧ gs = if gs.1 = gs.2.2 ∧ gs.1 = π ∧ gs.2.1 = [] then 1 else 0

@[simp]

theorem WeightedNetKAT.G.mod_eq {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {gs : GS F N} {π : Pk[F,N]} : G⟦@mod ~π⟧ gs = if gs.2.2 = π ∧ gs.2.1 = [] then 1 else 0

@[simp]

theorem WeightedNetKAT.G.dup_eq {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {gs : GS F N} : G⟦dup⟧ gs = if gs.2.2 = gs.1 ∧ gs.2.1 = [gs.1] then 1 else 0

@[simp]

theorem WeightedNetKAT.G.skip_concat {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {x : GS F N →c 𝒮} : G⟦skip⟧ ♢ x = x

@[simp]

theorem WeightedNetKAT.G.concat_skip {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {x : GS F N →c 𝒮} : x ♢ G⟦skip⟧ = x

@[simp]

theorem WeightedNetKAT.G.seq_skip {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {p : RPol 𝒮} : G⟦~p; skip⟧ = G⟦~p⟧

theorem WeightedNetKAT.G.iter_succ {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (p₁ : RPol 𝒮) (n : ℕ) : G⟦~(p₁.iter (n + 1))⟧ = (fun (x : GS F N →c 𝒮) => G⟦~p₁⟧ ♢ x)^[n] G⟦~p₁⟧

theorem WeightedNetKAT.G.iter {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (p₁ : RPol 𝒮) (n : ℕ) : G⟦~(p₁.iter n)⟧ = (fun (x : GS F N →c 𝒮) => G⟦~p₁⟧ ♢ x)^[n] G⟦skip⟧

@[implicit_reducible]

noncomputable instance WeightedNetKAT.GS.instHPowCountsuppNat {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : HPow (GS F N →c 𝒮) ℕ (GS F N →c 𝒮)

Equations

• WeightedNetKAT.GS.instHPowCountsuppNat = { hPow := fun (s : WeightedNetKAT.GS F N →c 𝒮) (n : ℕ) => (fun (x : WeightedNetKAT.GS F N →c 𝒮) => s ♢ x)^[n] G⟦skip⟧ }

instance WeightedNetKAT.GS.instConcatAssocCountsupp {F : Type} [Listed F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] : ConcatAssoc (GS F N →c 𝒮)

@[simp]

theorem WeightedNetKAT.GS.pow_zero {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (M : GS F N →c 𝒮) : M ^ 0 = G⟦skip⟧

@[simp]

theorem WeightedNetKAT.GS.pow_one {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (M : GS F N →c 𝒮) : M ^ 1 = M

theorem WeightedNetKAT.GS.pow_succ {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (M : GS F N →c 𝒮) {n : ℕ} : M ^ (n + 1) = M ♢ M ^ n

theorem WeightedNetKAT.GS.pow_succ' {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (M : GS F N →c 𝒮) {n : ℕ} : M ^ (n + 1) = M ^ n ♢ M

theorem WeightedNetKAT.GS.pow_add {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (M : GS F N →c 𝒮) {n m : ℕ} : M ^ (n + m) = M ^ n ♢ M ^ m

def WeightedNetKAT.GS.pks {F : Type} [Listed F] {N : Type} (s : GS F N) : List Pk[F,N]

Equations

• s.pks = s.1 :: s.2.1 ++ [s.2.2]

def WeightedNetKAT.GS.H {F : Type} [Listed F] {N : Type} (s : GS F N) : Pk[F,N] × List Pk[F,N]

Equations

• s.H = (s.2.2, s.2.1.reverse)

def WeightedNetKAT.GS.toRPol {F : Type} [Listed F] {N 𝒮 : Type} (g : GS F N) : RPol 𝒮

Equations

• g.toRPol = wnk_rpol {@test ~g.1; ~(List.foldr (fun (x : Pk[F,N]) (y : WeightedNetKAT.RPol 𝒮) => wnk_rpol {@mod ~x; dup; ~y}) wnk_rpol {@mod ~g.2.2} g.2.1)}

noncomputable def WeightedNetKAT.GS.sem {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (g : GS F N) : Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →c 𝒮

Equations

• g.sem = g.toRPol.sem

theorem WeightedNetKAT.GS.sem_eq {F : Type} [Listed F] [DecidableEq F] {N : Type} [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (g : GS F N) (h : Pk[F,N] × List Pk[F,N]) : g.sem h = if g.1 = h.1 then η (g.H.1, g.H.2 ++ h.2) else 0

noncomputable def WeightedNetKAT.RPol.sem_G_theorem {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (p : RPol 𝒮) : Prop

Equations

• p.sem_G_theorem = (p.sem = fun (h : Pk[F,N] × List Pk[F,N]) => ω∑ (x : ↑G⟦~p⟧.support), G⟦~p⟧ ↑x * (↑x).sem h)

theorem WeightedNetKAT.RPol.sem_G.Drop {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : RPol.Drop.sem_G_theorem

theorem WeightedNetKAT.RPol.sem_G.Skip {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : wnk_rpol {skip}.sem_G_theorem

theorem WeightedNetKAT.RPol.sem_G.Test {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {π₀ : Pk[F,N]} : wnk_rpol {@test ~π₀}.sem_G_theorem

theorem WeightedNetKAT.RPol.sem_G.Mod {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {γ : Pk[F,N]} : wnk_rpol {@mod ~γ}.sem_G_theorem

theorem WeightedNetKAT.RPol.sem_G.Dup {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : wnk_rpol {dup}.sem_G_theorem

theorem WeightedNetKAT.RPol.sem_G.Seq {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p₁ p₂ : RPol 𝒮} (ih₁ : p₁.sem_G_theorem) (ih₂ : p₂.sem_G_theorem) : wnk_rpol {~p₁; ~p₂}.sem_G_theorem

theorem WeightedNetKAT.RPol.sem_G.Add {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p₁ p₂ : RPol 𝒮} (ih₁ : p₁.sem_G_theorem) (ih₂ : p₂.sem_G_theorem) : wnk_rpol {~p₁ ⨁ ~p₂}.sem_G_theorem

theorem WeightedNetKAT.RPol.sem_G.Weight {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {w : 𝒮} {p₁ : RPol 𝒮} (ih : p₁.sem_G_theorem) : wnk_rpol {~w ⨀ ~p₁}.sem_G_theorem

theorem WeightedNetKAT.RPol.sem_G.Iter {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p₁ : RPol 𝒮} (ih : p₁.sem_G_theorem) : wnk_rpol {~p₁*}.sem_G_theorem

theorem WeightedNetKAT.RPol.sem_G {F : Type} [Listed F] [DecidableEq F] {N : Type} [Listed N] [DecidableEq N] {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] (p : RPol 𝒮) : p.sem = fun (h : Pk[F,N] × List Pk[F,N]) => ω∑ (x : ↑G⟦~p⟧.support), G⟦~p⟧ ↑x * (↑x).sem h