theory Solutions_ExerciseSession_1 imports "~~/src/HOL/Library/BNF_Corec" begin (* 1. To be done by the lecturer in class: *) (* Define the reveres operator "rvs" on lists (ignore the existing ones) and prove that it is involutive: rvs (rvs xs) = xs *) (* To define rvs, we first define app (append): *) primrec app :: "'a list \ 'a list \ 'a list" where "app [] ys = ys" | "app (x # xs) ys = x # (app xs ys)" primrec rvs :: "'a list \ 'a list" where "rvs [] = []" | "rvs (x # xs) = app (rvs xs) [x]" (* Testing: *) value "rvs [1,2,3::nat]" (* Fully automatic: *) lemma app_assoc: "app (app xs ys) zs = app xs (app ys zs)" by (induct xs) auto lemma app_Nil[simp]: "app xs [] = xs" by (induct xs) auto (* Apply style: *) lemma rvs_app: "rvs (app xs ys) = app (rvs ys) (rvs xs)" apply(induct xs) subgoal by simp subgoal for x xs by (simp add: app_assoc) . lemma rvs_rvs[simp]: "rvs (rvs xs) = xs" apply(induction xs) subgoal apply simp . subgoal for x xs by (simp add: rvs_app) . (* *) (* 2. To be done by the students: *) (* Define addition on natural numbers recursively in two different ways: -- by recursion on the first argument -- by recursion on the second argument and prove that the two versions coincide. Also, prove that these operators are commutative. (Ignore the existing operator +.) *) fun add :: "nat \ nat \ nat" where "add m 0 = m" |"add m (Suc n) = Suc (add m n)" primrec add2 :: "nat \ nat \ nat" where "add2 0 n = n" | "add2 (Suc m) n = Suc (add2 m n)" (* Suffices to prove that one of the two (say, add) satisfies the eqautions that uniquely identify the other (say, add2): *) lemma add_0[simp]: "add 0 n = n" by (induct n) auto lemma add_Suc[simp]: "add (Suc m) n = Suc (add m n)" by (induct n) auto (* ... and then their inductive proof of their equality is immediate: *) lemma add_add2: "add m n = add2 m n" by (induct m) auto lemma add_comm: "add m n = add n m" by (induct m) auto (* 3. To be done by the lecturer together with the students (if time allows): Define some of the examples from Lecture 1. *) fun f :: "nat \ nat" where "f x = (if x = 0 then 1 else f(x - 1) * 2)" lemma "f x = 2 ^ x" by (induct x) auto (* *) declare [[names_short]] codatatype stream = Cons (hd: nat) (tl: stream) primcorec zeros :: stream where "zeros = Cons 0 zeros" corec zzeros :: stream where "zzeros = Cons 0 (Cons 0 zzeros)" lemma tl_zzeros[simp]: "hd zzeros = 0" "tl zzeros = Cons 0 zzeros" apply(subst zzeros.code,simp)+ . lemma "zeros = zzeros" proof- {fix xs ys assume "xs = zeros \ ys \ {zzeros, Cons 0 zzeros}" hence "xs = ys" by (coinduct rule: stream.coinduct) auto } thus ?thesis by auto qed corec (friend) plus :: "stream \ stream \ stream" where "plus xs ys = Cons ((hd xs) + (hd ys)) (plus (tl xs) (tl ys))" corec ff :: "stream \ stream \ stream" where "ff xs ys = Cons (hd xs + hd ys) (plus (ff xs zeros) (ff (tl xs) ys))" corec collatz :: "nat \ stream" where "collatz n = (if n \ {0,1} then zeros else if even n then collatz (n div 2) else Cons n (collatz (3 * n + 1)))" end