# Theory Examples

section ‹Examples\label{sec:examples}›

theory Examples
imports Prefix_Free_Code_Combinators
begin

text ‹The following introduces a few examples for encoders:›

begin ✐‹tag visible›
define example1 where "example1 = N⇩e ×⇩e N⇩e"

text ‹This is an encoder for a pair of natural numbers using exponential Golomb codes.›

text ‹Given a pair it is possible to estimate the number of bits necessary to
encode it using the @{term "bit_count"} lemmas.›

have "bit_count (example1 (0,1)) = 4"

text ‹Note that a finite bit count automatically implies that the encoded element is in the domain
of the encoding function. This means usually it is possible to establish a bound on the size of
the datastructure and verify that the value is encodable simultaneously.›

hence "(0,1) ∈ dom example1"
by (intro bit_count_finite_imp_dom, simp)

define example2
where "example2 = [0..<42] →⇩e Nb⇩e 314"

text ‹The second example illustrates the use of the combinator @{term "(→⇩e)"}, which allows
encoding functions with a known finite encodable domain, here we assume the values are smaller
than @{term "314"} on the domain @{term "{..<42}"}.›

have "bit_count (example2 f) = 42*9" (is "?lhs = ?rhs")
if a:"f ∈ {0..<42} →⇩E {0..<314}" for f
proof -
have "?lhs = (∑x←[0..<42]. bit_count (Nb⇩e 314 (f x)))"
using a by (simp add:example2_def fun_bit_count PiE_def)
also have "... = (∑x←[0..<42]. ereal (floorlog 2 313))"
using a Pi_def PiE_def bounded_nat_bit_count
by (intro arg_cong[where f="sum_list"] map_cong, auto)
also have "... = ?rhs"
finally show ?thesis by simp
qed

define example3
where "example3 = N⇩e ⋈⇩e (λn. [0..<42] →⇩e Nb⇩e n)"

text ‹The third example is more complex and illustrates the use of dependent encoders, consider
a function with domain @{term "{..<(42::nat)}"} whose values are natural numbers in the interval
@{term "{..<n::nat}"}. Let us assume the bound is not known in advance and needs to be encoded
as well. This can be done using a dependent product encoding, where the first component encodes
the bound and the second component is an encoder parameterized by that value.›

end

end