Documentation

WeightedNetKAT.Approximate

@[implicit_reducible]

instance WeightedNetKAT.instZeroPol {𝒮 : Type u_2} {F : Type u_3} {N : Type u_4} :

Zero Pol[F,N,𝒮]

Equations

WeightedNetKAT.instZeroPol = { zero := wnk_pol {false } }

@[implicit_reducible]

instance WeightedNetKAT.instAddPol {𝒮 : Type u_2} {F : Type u_3} {N : Type u_4} :

Add Pol[F,N,𝒮]

Equations

WeightedNetKAT.instAddPol = { add := fun (p q : Pol[F,N,𝒮]) => wnk_pol {~p ⨁ ~q} }

@[simp]

theorem WeightedNetKAT.Pol.zero_def {𝒮 : Type u_2} {F : Type u_3} {N : Type u_4} :

0 = wnk_pol {false }

@[simp]

theorem WeightedNetKAT.Pol.add_def {𝒮 : Type u_2} {F : Type u_3} {N : Type u_4} (p q : Pol[F,N,𝒮]) :

p + q = wnk_pol {~p ⨁ ~q}

@[simp]

theorem WeightedNetKAT.Pol.instAdd_sem {𝒮 : Type u_2} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type u_3} [Listed F] [DecidableEq F] {N : Type u_4} [DecidableEq N] (p q : Pol[F,N,𝒮]) :

(p + q).sem = p.sem + q.sem

@[simp]

theorem WeightedNetKAT.Pol.instZero_sem {𝒮 : Type u_2} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type u_3} [Listed F] [DecidableEq F] {N : Type u_4} [DecidableEq N] :

sem 0 = 0

noncomputable def WeightedNetKAT.Pol.approx_n {𝒮 : Type u_2} {F : Type u_3} {N : Type u_4} (p : Pol[F,N,𝒮]) (n : ℕ) :

Equations

(WeightedNetKAT.Pol.Filter t).approx_n n = WeightedNetKAT.Pol.Filter t
wnk_pol {~f ← ~n_1}.approx_n n = wnk_pol {~f ← ~n_1}
wnk_pol {dup }.approx_n n = wnk_pol {dup }
wnk_pol {~p_2; ~q}.approx_n n = wnk_pol {~(p_2.approx_n n); ~(q.approx_n n)}
wnk_pol {~w ⨀ ~p_2}.approx_n n = wnk_pol {~w ⨀ ~(p_2.approx_n n)}
wnk_pol {~p_2 ⨁ ~q}.approx_n n = wnk_pol {~(p_2.approx_n n) ⨁ ~(q.approx_n n)}
wnk_pol {~p_2*}.approx_n n = (List.map (fun (x : ℕ) => p_2.approx_n n ^ x) (List.range n)).sum

Instances For

@[irreducible]

noncomputable def WeightedNetKAT.Pol.sem_n {𝒮 : Type u_2} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type u_3} [Listed F] [DecidableEq F] {N : Type u_4} [DecidableEq N] (p : Pol[F,N,𝒮]) (n : ℕ) :

Pk[F,N] × List Pk[F,N] → Pk[F,N] × List Pk[F,N] →c 𝒮

Equations

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

Instances For

theorem WeightedNetKAT.Pol.approx_n_sem {𝒮 : Type u_2} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type u_3} [Listed F] [DecidableEq F] {N : Type u_4} [DecidableEq N] (p : Pol[F,N,𝒮]) (n : ℕ) :

(p.approx_n n).sem = p.sem_n n

theorem WeightedNetKAT.Pol.sem_n_mono {𝒮 : Type u_2} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {F : Type u_3} [Listed F] [DecidableEq F] {N : Type u_4} [DecidableEq N] (p : Pol[F,N,𝒮]) :

Monotone p.sem_n

theorem WeightedNetKAT.Pol.iter_m_sem_eq_ωSup_sem_n {𝒮 : Type u_2} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {F : Type u_3} [Listed F] [DecidableEq F] {N : Type u_4} [DecidableEq N] [Fintype N] {p : Pol[F,N,𝒮]} (h : p.sem = OmegaCompletePartialOrder.ωSup { toFun := p.sem_n, monotone' := ⋯ }) (m : ℕ) :

(p.iter m).sem = OmegaCompletePartialOrder.ωSup { toFun := fun (n : ℕ) => (p.iter m).sem_n n, monotone' := ⋯ }

theorem WeightedNetKAT.Pol.sem_n_approx {𝒮 : Type u_2} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {F : Type u_3} [Listed F] [DecidableEq F] {N : Type u_4} [DecidableEq N] [Fintype N] (p : Pol[F,N,𝒮]) :

p.sem = OmegaCompletePartialOrder.ωSup { toFun := p.sem_n, monotone' := ⋯ }

theorem WeightedNetKAT.Pol.sem_n_lowerBounds {𝒮 : Type u_2} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {F : Type u_3} [Listed F] [DecidableEq F] {N : Type u_4} [DecidableEq N] [Fintype N] (p : Pol[F,N,𝒮]) (n : ℕ) :

p.sem_n n ≤ p.sem