(*<*)
theory tmpl07
imports
Complex_Main
"~~/src/HOL/Library/Tree"
begin
(*>*)
text {* \ExerciseSheet{7}{9.~6.~2017} *}
text \\Exercise{Round wrt.\ Binary Search Tree}
The distance between two integers \x\ and \y\ is @{term \abs (x-y)\}.
\<^enum> Define a function \round :: int tree \ int \ int option\, such that
\round t x\ returns an element of a {\bf binary search tree} \t\ with minimum
distance to \x\, and \None\ if and only if \t\ is empty.
Define your function such that it does no unnecessary recursions
into branches of the tree that are known to not contain a minimum distance
element.
\<^enum> Specify and prove that your function is correct.
Note: You are required to phrase the correctness properties yourself!
Hint: Specify 3 properties:
\<^item> None is returned only for the empty tree.
\<^item> Only elements of the tree are returned.
\<^item> The returned element has minimum distance.
\<^enum> Estimate the time of your round function to be linear in the height of the tree
\
fun round :: "int tree \ int \ int option"
where "round _ _ = undefined"
fun t_round :: "int tree \ int \ nat"
where "t_round _ _ = undefined"
text \
\Homework{Cost for \remdups\}{16.~6.~2017}
The following function removes all duplicates from a list.
It uses the auxiliary function \member\ to determine
whether an element is contained in a list.
\
fun member :: "'a \ 'a list \ bool" where
"member x [] \ False"
| "member x (y#ys) \ (if x=y then True else member x ys)"
fun rem_dups :: "'a list \ 'a list" where
"rem_dups [] = []" |
"rem_dups (x # xs) = (if member x xs then rem_dups xs else x # rem_dups xs)"
text \
Show that this function is equal to the HOL standard function @{const \remdups\}
\
lemma rem_dups_correct: "rem_dups xs = remdups xs" sorry
text \Define the timing functions for @{const \member\} and @{const rem_dups},
as described on the slides:\
fun t_member :: "'a \ 'a list \ nat"
where "t_member _ _ = undefined"
fun t_rem_dups :: "'a list \ nat"
where "t_rem_dups _ = undefined"
text \Estimate \t_rem_dups xs\ to be quadratic in the length of \xs\.
Hint: The estimate @{term \(length xs + 1)\<^sup>2\} should work.
\
lemma "t_rem_dups xs \ (length xs+1)\<^sup>2" sorry
(*<*)
end
(*>*)