theory sol01 imports Main begin text {* \ExerciseSheet{1}{16.~10.~2012} *} 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} 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::nat) * (5 + 3)" 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 (induct xs) apply auto done text {* \Exercise{Adding elements to the end of a list} *} text {* Recall the definition of lists from the lecture. 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 (induct xs) apply auto oops lemma reverse_snoc: "reverse (snoc xs y) = y # reverse xs" by (induct xs) auto theorem "reverse (reverse xs) = xs" by (induct xs) (auto simp add: reverse_snoc) 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 (induct xs) auto lemma "reverse' (reverse' xs) = xs" by (simp add: rev_append_lemma) end