(*<*)
theory sol01
imports Main
begin
(*>*)
text {* \ExerciseSheet{1}{15.~10.~2013} *}
text {*
Before beginning to solve the exercises, open a new theory file
named \texttt{Ex01.thy} and write the the following three lines
at the top of this file.
*}
text {*
\textbf{theory} \textit{Ex01}
\textbf{imports} \textit{Main}
\textbf{begin}
*}
text {* \Exercise{Calculating with natural numbers and integers}
Use the \textbf{value} command to turn Isabelle into
a fancy calculator and evaluate the following natural
number expressions:
*}
(*<*)value(*>*) "2 + (2::nat)" (*<*)value(*>*) "(2::int) * (5 + 3)" (*<*)value(*>*) "(3::int) * 4 - 2 * (7 + 1)" text {**}
(*<*)value(*>*) "(3::nat) * 4 - 2 * (7 + 1)"
text {*
Can you explain the last result?
*}
text {* \Exercise{Natural number laws}
Formulate and prove the well-known laws of commutativity and
associativity for addition of natural numbers.
*}
(*<*)
lemma "x + y = y + (x::nat)"
apply auto
done
lemma "x + (y + z) = (x + y) + (z::nat)"
apply auto
done
(*>*)
text {* \Exercise{Counting elements of a list} *}
text {*
Define a function which counts the number of occurrences of
a particular element in a list.
*}
fun count :: "'a list \ 'a \ nat" (*<*) where
"count [] _ = 0" |
"count (x # xs) y = (if x = y then Suc (count xs y) else count xs y)" (*>*)
text {*
Test your definition of @{term count} on some examples and
prove that the results are indeed correct.
*}
(*<*)
value "count [] (3::nat)"
value "count [3, 2] (3::nat)"
value "count [3, 3] (3::nat)"
(*>*)
text {*
Prove the following inequality (and additional lemmas, if
necessary) about the relation between @{term count} and
@{term length}, the function returning the length of a list.
*}
theorem "count xs x \ length xs"
(*<*)
apply (induction xs)
apply auto
done
(*>*)
text {* \Exercise{Adding elements to the end of a list} *}
text {*
Define a
function @{text snoc} that appends an element at the right
end of a list. Do not use the existing append operator
@{text "@"} for lists.
*}
fun snoc :: "'a list \ 'a \ 'a list" (*<*) where
"snoc [] x = [x]" |
"snoc (y # ys) x = y # (snoc ys x)" (*>*)
text {*
Convince yourself on some test cases that your definition
of @{term snoc} behaves as expected, for example run:
*}
value "snoc [] c"
text {*
Also prove that your test cases are indeed correct,
for instance show:
*}
lemma "snoc [] c = [c]"
(*<*)
apply auto
done
(*>*)
text {*
Next define a function @{text reverse} that reverses the
order of elements in a list. (Do not use the existing
function @{term rev} from the library.) Hint: Define
the reverse of @{text "x # xs"} using the @{term snoc}
function.
*}
fun reverse :: "'a list \ 'a list" (*<*) where
"reverse [] = []" |
"reverse (x # xs) = snoc (reverse xs) x" (*>*)
text {*
Demonstrate that your definition is correct by running some
test cases, and proving that those test cases are correct.
For example:
*}
value "reverse [a, b, c]"
lemma "reverse [a, b, c] = [c, b, a]"
(*<*)
apply auto
done
(*>*)
text {*
Prove the following theorem. Hint: You need to find an
additional lemma relating @{text reverse} and @{text snoc} to prove it.
*}
theorem "reverse (reverse xs) = xs"
(*<*)
apply (induction xs)
apply auto
oops
lemma reverse_snoc: "reverse (snoc xs y) = y # reverse xs"
by (induction xs) auto
theorem "reverse (reverse xs) = xs"
by (induction xs) (auto simp add: reverse_snoc)
(*>*)
(*<*)
text {* Of course, our definitions can also be expressed by functions
predefined in HOL: *}
lemma snoc_append_conv: "snoc xs x = xs@[x]"
by (induction xs) auto
lemma reverse_rev_conv: "reverse x = rev x"
by (induction x) (auto simp: snoc_append_conv)
find_theorems "rev (rev _) = _"
thm rev_rev_ident (* This one happens to be in the default simpset! *)
theorem "reverse (reverse xs) = xs" by (simp add: reverse_rev_conv)
(*>*)
(*<*)
text {*
Just in case anyone tries the tail-recursive definition:
*}
fun rev_append where
"rev_append ys [] = ys" |
"rev_append ys (x # xs) = rev_append (x # ys) xs"
fun reverse' where "reverse' xs = rev_append [] xs"
lemma rev_append_lemma:
"\ys. rev_append [] (rev_append ys xs) = rev_append xs ys"
by (induction xs) auto
lemma "reverse' (reverse' xs) = xs"
by (simp add: rev_append_lemma)
(*>*)
(*<*)
end
(*>*)