(*<*)
theory hwsol02
imports
"~~/src/HOL/IMP/AExp"
"~~/src/HOL/IMP/BExp"
begin
(*>*)
text \\NumHomework{Conditionals}{27. Oct. 2015}
We define a representation of Boolean expressions that only use
conditionals as connective.
\
datatype cexp = Cond cexp cexp cexp | Bc' bool | Less' aexp aexp
text \The semantics of @{term "Cond b t e"} is if $b$ holds, then
evaluate $t$, else evaluate $e$.
Define the semantics:\
fun cval :: "cexp \ state \ bool"
(*<*)
where
"cval (Cond b t e) \ = (if cval b \ then cval t \ else cval e \)"
| "cval (Bc' b) \ = b"
| "cval (Less' a1 a2) \ \ aval a1 \ < aval a2 \"
(*>*)
text \Define conversions from @{typ bexp} to @{typ cexp} and back.
Show that your conversions preserve the semantics:\
fun b2c :: "bexp \ cexp"
(*<*)
where
"b2c (Bc b) = Bc' b"
| "b2c (Not b) = Cond (b2c b) (Bc' False) (Bc' True)"
| "b2c (And b1 b2) = Cond (b2c b1) (b2c b2) (Bc' False)"
| "b2c (Less a1 a2) = Less' a1 a2"
(*>*)
lemma "cval (b2c b) \ = bval b \"
(*<*)
by (induction b) auto
(*>*)
fun c2b :: "cexp \ bexp"
(*<*)
where
"c2b (Bc' b) = Bc b"
| "c2b (Less' a1 a2) = Less a1 a2"
| "c2b (Cond b t e) = Not (And (Not (And (c2b b) (c2b t))) (Not (And (Not (c2b b)) (c2b e))))"
(*>*)
lemma "bval (c2b c) \ = cval c \"
(*<*)
by (induction c) auto
(*>*)
text \\NumHomework{Heaps}{27. Oct. 2015}
A (min) heap is a binary tree with node labels,
such that every node is less than or equal to its successors.
We model heaps by the following datatype:
\
datatype heap = Leaf | Node nat heap heap
text \
Define a function to check the heap property.
Hint: The following function may save you some case distinctions:
\
fun le :: "nat \ heap \ bool" where
"le n Leaf \ True"
| "le n (Node m _ _) \ n\m"
fun heap_invar :: "heap \ bool" where
(*<*)
"heap_invar Leaf \ True"
| "heap_invar (Node a h1 h2) \ heap_invar h1 \ heap_invar h2 \ le a h1 \ le a h2"
(*>*)
text \Define a function to return the minimal value of a non-empty heap.
Set the case for an empty heap to undefined.\
fun get_min :: "heap \ nat" where
"get_min Leaf = undefined"
(*<*)
| "get_min (Node a h1 h2) = a"
(*>*)
text \The following function maps a heap to the set of its elements.\
fun heap_set where
"heap_set Leaf = {}"
| "heap_set (Node a h1 h2) = insert a (heap_set h1 \ heap_set h2)"
text \Note that @{term "insert x s"} inserts element $x$ to set $s$.
To get the @{text \} symbol, type $\backslash union$, or use the symbols panel!\
text \Show that @{const get_min} actually returns an element from the heap\
lemma get_min_correct1: "h\Leaf \ get_min h \heap_set h"
(*<*)
by (induction h) auto
(*>*)
text \Show that @{const get_min} returns an element smaller or equal to the elements of the heap\
(*<*)
lemma aux:
assumes "heap_invar h"
and "(le a h)"
and "b\heap_set h"
shows"a\b"
using assms
apply (induction h arbitrary: a)
apply auto
using dual_order.trans apply blast+ (* Sledgehammer find this *)
done
(*>*)
lemma get_min_correct2: "h\Leaf \ heap_invar h \ b\heap_set h \ get_min h\b"
(*<*)
apply (cases h)
by (auto simp: aux)
(*>*)
text \Hint: You may need an auxiliary lemma about @{const le}.\
text \As a {\bfseries bonus exercise} for 5 bonus points,
implement a function that merges two heaps, and show that
it preserves the heap-property and that the set of elements on the new
heap is the union of elements in the old heaps. You need not
consider balancedness of heaps!
\
text \Note: Bonus points count on your side, but not on the total
number of reachable points, when we compute the ratio of points
that you scored in the homework, which will be 40% of the final grade. \
text \It may happen that the function package cannot prove termination of
your function by default. In this case, use the following template, which
makes use of the size-change termination prover, which should be able to
prove termination.\
function merge :: "heap \ heap \ heap"
where
-- \Function equations as usual\
(*<*)
"merge h Leaf = h"
| "merge Leaf h = h"
| "merge (Node a h1 h2) (Node b h3 h4) = (
if a\b then Node a (merge h1 h2) (Node b h3 h4)
else Node b (merge h3 h4) (Node a h1 h2)
)"
(*>*)
by pat_completeness auto
termination by size_change
(*<*)
lemma le_merge[simp]: "le a (merge h1 h2) \ le a h1 \ le a h2"
apply (cases "(h1,h2)" rule: merge.cases)
apply auto
done
(*>*)
lemma merge_correct1: "\heap_invar h1; heap_invar h2\ \ heap_invar (merge h1 h2)"
(*<*)
by (induction h1 h2 rule: merge.induct) auto
(*>*)
lemma merge_correct2: "heap_set (merge h1 h2) = heap_set h1 \ heap_set h2"
(*<*)
by (induction h1 h2 rule: merge.induct) auto
(*>*)
(*<*)
end
(*>*)