theorem List.succ_range_map {α : Type} (f : ℕ → α) {n : ℕ} : map f (range (n + 1)) = map f (range n) ++ [f n]

@[reducible, inline]

abbrev WeightedNetKAT.η {ι α : Type} [DecidableEq ι] [Zero α] [One α] (i : ι) : ι →c α

Equations

• WeightedNetKAT.η i = { toFun := Pi.single i 1, countable := ⋯ }

@[simp]

theorem WeightedNetKAT.η_apply {ι α : Type} [DecidableEq ι] [Zero α] [One α] {x y : ι} : (η x) y = if x = y then 1 else 0

def WeightedNetKAT.Pred.orDepth {F N : Type} : Pred[F,N] → ℕ

Equations

• wnk_pred {false}.orDepth = 0
• wnk_pred {true}.orDepth = 0
• wnk_pred {~f = ~n}.orDepth = 0
• wnk_pred {~t ∨ ~u}.orDepth = max t.orDepth u.orDepth + 1
• wnk_pred {~t ∧ ~u}.orDepth = max t.orDepth u.orDepth
• wnk_pred {¬~t}.orDepth = t.orDepth

def WeightedNetKAT.Pred.test {F : Type} [Listed F] {N : Type} (t : Pred[F,N]) (pk : Pk[F,N]) : Prop

Equations

• wnk_pred {false}.test pk = (false = true)
• wnk_pred {true}.test pk = (true = true)
• wnk_pred {~f = ~n}.test pk = (pk f = n)
• wnk_pred {~t_1 ∨ ~u}.test pk = (t_1.test pk ∨ u.test pk)
• wnk_pred {~t_1 ∧ ~u}.test pk = (t_1.test pk ∧ u.test pk)
• wnk_pred {¬~t_1}.test pk = ¬t_1.test pk

@[reducible]

def WeightedNetKAT.Pred.test_decidable {F : Type} [Listed F] {N : Type} [DecidableEq N] {t : Pred[F,N]} : DecidablePred t.test

Equations

• WeightedNetKAT.Pred.test_decidable pk = isFalse ⋯
• WeightedNetKAT.Pred.test_decidable pk = isTrue ⋯
• WeightedNetKAT.Pred.test_decidable pk = if h' : pk f = n then isTrue h' else isFalse h'
• WeightedNetKAT.Pred.test_decidable pk = if h' : t_2.test pk ∨ u.test pk then isTrue h' else isFalse h'
• WeightedNetKAT.Pred.test_decidable pk = if h' : t_2.test pk ∧ u.test pk then isTrue h' else isFalse h'
• WeightedNetKAT.Pred.test_decidable pk = if h' : ¬t_2.test pk then isTrue h' else isFalse h'

@[implicit_reducible]

instance WeightedNetKAT.Pred.test_instDecidable {F : Type} [Listed F] {N : Type} [DecidableEq N] {t : Pred[F,N]} : DecidablePred t.test

Equations

• WeightedNetKAT.Pred.test_instDecidable = WeightedNetKAT.Pred.test_decidable

def WeightedNetKAT.Pred.sem {𝒮 : Type} [Semiring 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] (p : Pred[F,N]) (h : Pk[F,N] × List Pk[F,N]) : Pk[F,N] × List Pk[F,N] →c 𝒮

Equations

• p.sem h = if p.test h.1 then WeightedNetKAT.η h else 0

@[implicit_reducible]

instance WeightedNetKAT.instSubstPk {F : Type} [DecidableEq F] [Listed F] {N : Type} : Subst Pk[F,N] F N

Equations

• WeightedNetKAT.instSubstPk = { subst := fun (pk : Pk[F,N]) (f : F) (n : N) => WeightedNetKAT.Pk.ofFn fun (f' : F) => if f = f' then n else pk f' }

def WeightedNetKAT.Pol.iter {X F N : Type} (p : Pol[F,N,X]) : ℕ → Pol[F,N,X]

Equations

• p.iter 0 = wnk_pol {true}
• p.iter n.succ = wnk_pol {~p; ~(p.iter n)}

@[reducible]

instance WeightedNetKAT.Pol.instHPow {X F N : Type} : HPow Pol[F,N,X] ℕ Pol[F,N,X]

Equations

• WeightedNetKAT.Pol.instHPow = { hPow := fun (p : Pol[F,N,X]) (n : ℕ) => p.iter n }

@[simp]

theorem WeightedNetKAT.Pol.pow_eq_iter {X F N : Type} {p : Pol[F,N,X]} {n : ℕ} : p ^ n = p.iter n

def WeightedNetKAT.Pol.iterDepth {X F N : Type} : Pol[F,N,X] → ℕ

Equations

• (WeightedNetKAT.Pol.Filter t).iterDepth = 0
• wnk_pol {~f ← ~n}.iterDepth = 0
• wnk_pol {dup}.iterDepth = 0
• wnk_pol {~p ⨁ ~q}.iterDepth = max p.iterDepth q.iterDepth
• wnk_pol {~p; ~q}.iterDepth = max p.iterDepth q.iterDepth
• wnk_pol {~w ⨀ ~q}.iterDepth = q.iterDepth
• wnk_pol {~p*}.iterDepth = p.iterDepth + 1

@[simp]

theorem WeightedNetKAT.Pol.iterDepth_iter {X F N : Type} {p : Pol[F,N,X]} {n : ℕ} : (p.iter n).iterDepth = if n = 0 then 0 else p.iterDepth

@[simp]

theorem WeightedNetKAT.Pol.iterDepth_pow {X F N : Type} {p : Pol[F,N,X]} {n : ℕ} : (p ^ n).iterDepth = if n = 0 then 0 else p.iterDepth

@[irreducible]

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

Equations

• (WeightedNetKAT.Pol.Filter t).sem = t.sem
• wnk_pol {~f ← ~n}.sem = fun (x : Pk[F,N] × List Pk[F,N]) => match x with | (π, h) => WeightedNetKAT.η (π[f ↦ n], h)
• wnk_pol {dup}.sem = fun (x : Pk[F,N] × List Pk[F,N]) => match x with | (π, h) => WeightedNetKAT.η (π, π :: h)
• wnk_pol {~p_2; ~q}.sem = fun (h : Pk[F,N] × List Pk[F,N]) => (p_2.sem h).bind q.sem
• wnk_pol {~w ⨀ ~p_2}.sem = fun (h : Pk[F,N] × List Pk[F,N]) => w * p_2.sem h
• wnk_pol {~p_2 ⨁ ~q}.sem = fun (h : Pk[F,N] × List Pk[F,N]) => p_2.sem h + q.sem h
• wnk_pol {~p_2*}.sem = fun (h : Pk[F,N] × List Pk[F,N]) => ω∑ (n : ℕ), (p_2 ^ n).sem h

noncomputable def WeightedNetKAT.Pol.map {𝒮 : Type} [Semiring 𝒮] {F N M : Type} [Semiring M] (p : Pol[F,N,𝒮]) (f : 𝒮 →+* M) : Pol[F,N,M]

Equations

• (WeightedNetKAT.Pol.Filter t).map f = WeightedNetKAT.Pol.Filter t
• wnk_pol {~f_1 ← ~n}.map f = wnk_pol {~f_1 ← ~n}
• wnk_pol {dup}.map f = wnk_pol {dup}
• wnk_pol {~p_2; ~q}.map f = wnk_pol {~(p_2.map f); ~(q.map f)}
• wnk_pol {~w ⨀ ~p_2}.map f = wnk_pol {~(f w) ⨀ ~(p_2.map f)}
• wnk_pol {~p_2 ⨁ ~q}.map f = wnk_pol {~(p_2.map f) ⨁ ~(q.map f)}
• wnk_pol {~p_2*}.map f = wnk_pol {~(p_2.map f)*}

theorem WeightedNetKAT.map_ωSum {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {M : Type} [Semiring M] [OmegaCompletePartialOrder M] [OrderBot M] [IsPositiveOrderedAddMonoid M] {ι : Type} [Countable ι] (g : 𝒮 →+* M) (hg : OmegaCompletePartialOrder.ωScottContinuous ⇑g) (f : ι → 𝒮) : g (ω∑ (i : ι), f i) = ω∑ (i : ι), g (f i)

theorem WeightedNetKAT.Pol.map_sem {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] {M : Type} [Semiring M] [OmegaCompletePartialOrder M] [OrderBot M] [IsPositiveOrderedAddMonoid M] (p : Pol[F,N,𝒮]) (f : 𝒮 →+* M) (hf : OmegaCompletePartialOrder.ωScottContinuous ⇑f) (h h' : Pk[F,N] × List Pk[F,N]) : f ((p.sem h) h') = ((p.map f).sem h) h'

@[simp]

theorem WeightedNetKAT.zero_apply {𝒮 : Type} [Semiring 𝒮] {F : Type} [Listed F] {N : Type} {x : Pk[F,N] × List Pk[F,N]} : OfNat.ofNat 0 x = 0

noncomputable def WeightedNetKAT.Φ {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] (p : Pol[F,N,𝒮]) (d : Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →c 𝒮) : Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →c 𝒮

Equations

• WeightedNetKAT.Φ p d h = WeightedNetKAT.η h + (p.sem h).bind d

theorem WeightedNetKAT.Φ_mono {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] (p : Pol[F,N,𝒮]) : Monotone (Φ p)

theorem WeightedNetKAT.Φ_continuous {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] [OmegaContinuousNonUnitalSemiring 𝒮] (p : Pol[F,N,𝒮]) : OmegaCompletePartialOrder.ωScottContinuous (Φ p)

@[simp]

theorem WeightedNetKAT.𝒲.wZero_le {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [Listed F] {N : Type} (p : Pk[F,N] × List Pk[F,N] →c 𝒮) : 0 ≤ p

@[simp]

theorem WeightedNetKAT.𝒲.Pi_wZero_le {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [Listed F] {N X : Type} (p : X → Pk[F,N] × List Pk[F,N] →c 𝒮) : 0 ≤ p

noncomputable def WeightedNetKAT.Φ_chain {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] (p : Pol[F,N,𝒮]) : OmegaCompletePartialOrder.Chain (Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →c 𝒮)

Equations

• WeightedNetKAT.Φ_chain p = { toFun := fun (n : ℕ) => (WeightedNetKAT.Φ p)^[n] 0, monotone' := ⋯ }

noncomputable def WeightedNetKAT.Φ_ωSup {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] (p : Pol[F,N,𝒮]) : Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →c 𝒮

Equations

• WeightedNetKAT.Φ_ωSup p = OmegaCompletePartialOrder.ωSup (WeightedNetKAT.Φ_chain p)

def WeightedNetKAT.IsLfp {α : Type} [OmegaCompletePartialOrder α] (f : α → α) (p : α) : Prop

Equations

• WeightedNetKAT.IsLfp f p = (f p = p ∧ ∀ (p' : α), f p' = p' → p ≤ p')

theorem WeightedNetKAT.IsLfp_unique {α : Type} [OmegaCompletePartialOrder α] {f : α → α} {p₁ p₂ : α} (h₁ : IsLfp f p₁) (h₂ : IsLfp f p₂) : p₁ = p₂

theorem WeightedNetKAT.Pol.Φ_ωSup_isLfp {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] [OmegaContinuousNonUnitalSemiring 𝒮] (p : Pol[F,N,𝒮]) : IsLfp (Φ p) (Φ_ωSup p)

theorem WeightedNetKAT.Pol.iter_sem_isLfp {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] [OmegaContinuousNonUnitalSemiring 𝒮] (p : Pol[F,N,𝒮]) : IsLfp (Φ p) wnk_pol {~p*}.sem

theorem WeightedNetKAT.Pol.iter_sem_eq_lfp {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type} [DecidableEq F] [Listed F] {N : Type} [DecidableEq N] [OmegaContinuousNonUnitalSemiring 𝒮] (p : Pol[F,N,𝒮]) : wnk_pol {~p*}.sem = Φ_ωSup p