theory Hw01_Comments imports Main begin text \This file contains the solution for homework 1, and some comments on the solution variants I saw during correction:\ fun snoc :: "'a list \ 'a \ 'a list" where "snoc [] x = [x]" | "snoc (y # ys) x = y # (snoc ys x)" fun reverse :: "'a list \ 'a list" where "reverse [] = []" | "reverse (x # xs) = snoc (reverse xs) x" text \Here, the most common solution was the following:\ fun lsum :: "nat list \ nat" where "lsum [] = 0" | "lsum (x#xs) = x + lsum xs" text \This was also solved by most people, using the straightforward approach\ lemma "lsum (reverse xs) = lsum xs" apply (induction xs) apply auto (** here, you see in the remaining subgoal: lsum (snoc (reverse xs) a) = ... and you would like to rewrite it to a + lsum (snoc ...) to apply the induction hypothesis. So, prove the following auxiliary lemma: **) oops lemma aux: "lsum (snoc xs x) = x + lsum xs" by (induction xs) auto text \Now, the proof goes through:\ lemma "lsum (reverse xs) = lsum xs" by (induction xs) (auto simp: aux) text \Some stated the auxiliary lemma directed in the other way, i.e., @{term "x + lsum xs = lsum (snoc xs x)"}. While this works for this part, it will cause trouble when proving Gauss: Adding this lemma to the simplifier, instructs the simplifier to rewrite all additions to an lsum to a "snoc". Thus, there is no chance to apply lemmas about addition ... \ text \This was solved by most people like this: \ fun nlist :: "nat \ nat list" where "nlist 0 = []" | "nlist (Suc n) = snoc (nlist n) (Suc n)" lemma "lsum (nlist n) = n * (n+1) div 2" by (induction n) (auto simp: aux) text \Some people discovered list-comprehension syntax: \ definition "nlist' n \ [1..Then, an auxiliary lemma about lsum and list concatenation is required:\ lemma aux2: "lsum (xs@ys) = lsum xs + lsum ys" by (induction xs) auto lemma "lsum (nlist' n) = n * (n+1) div 2" unfolding nlist'_def by (induction n) (auto simp: aux2) end