(*<*) theory sol01 imports Main begin (*>*) text {* \ExerciseSheet{1}{25.~10.~2016} *} 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 (*>*)