(*<*)
theory tmpl09
imports "../../Material/Thys/Trie1"
begin
(*>*)
text {* \ExerciseSheet{9}{23.~6.~2017} *}
text \\Exercise{Union Function on Tries}
Define a function to merge two tries and show its correctness
\
fun union :: "trie \ trie \ trie"
where "union _ _ = undefined"
lemma "isin (union a b) x = isin a x \ isin b x"
sorry
text \
\Exercise{Intermediate Abstraction Level for Patricia Tries}
We introduce an abstraction level in between tries and Patricia tries:
A node with only a single non-leaf successor is represented as an unary node.
Via unary nodes, this implementation already introduces a notion of common prefix,
but does not yet summarize runs of multiple prefixes into a list.
\
datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
fun abs_itrie :: "itrie \ trie" -- \Abstraction to tries\
where
"abs_itrie LeafI = Leaf"
| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"
text \Refine the union function to intermediate tries\
fun unionI :: "itrie \ itrie \ itrie"
where "unionI _ _ = undefined"
text \Next, we define an abstraction function from Patricia tries to intermediate tries.
Note that we need to install a custom measure function to get the termination proof through!
\
fun size1P :: "ptrie \ nat" where
"size1P LeafP = 0"
| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial)
fun absI_ptrie :: "ptrie \ itrie" where
"absI_ptrie LeafP = LeafI"
| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
text \Warmup: Show that abstracting Patricia tries over intermediate
tries to tries is the same as abstracting directly to tries.\
lemma "abs_itrie o absI_ptrie = abs_ptrie"
sorry
text \Refine the union function to Patricia tries.
Hint: First figure out how a Patricia trie that
correspond to a leaf/unary/binary node looks like.
Then translate @{const \unionI\} equation by equation!
More precisely, try to find terms \unaryP\ and \binaryP\ such that
@{term [display] "absI_ptrie (unaryP k t) = UnaryI k (absI_ptrie t)"}
@{term [display] "absI_ptrie (binaryP v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"}
You will encounter a small problem with \unaryP\. Which one?
\
fun unionP :: "ptrie \ ptrie \ ptrie"
where "unionP _ _ = undefined"
lemma "absI_ptrie (unionP t\<^sub>1 t\<^sub>2) = unionI (absI_ptrie t\<^sub>1) (absI_ptrie t\<^sub>2)"
sorry
text \
\NumHomework{Shrunk Trees}{30.~6.~2017}
Have a look at the @{const delete2} function for tries. It maintains a
``shrunk'' - property on tries. Identify this property, define a predicate
for it, and show that it is indeed maintained by empty, insert, and delete2!
\
fun shrunk :: "trie \ bool" where "shrunk _ = undefined"
lemma "shrunk Leaf" sorry
lemma "shrunk t \ shrunk (insert ks t)" sorry
lemma "shrunk t \ shrunk (delete2 ks t)" sorry
text \
\NumHomework{Refining Delete}{30.~6.~2017}
Refine the delete function to intermediate tries and further down
to Patricia tries.
\
fun deleteI :: "bool list \ itrie \ itrie" where
"deleteI _ _ = undefined"
lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)" sorry
fun pdelete :: "bool list \ ptrie \ ptrie"
where
"pdelete _ _ = undefined"
lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)" sorry
(*<*)
end
(*>*)