section \Solutions for Session 3\ theory Solutions03 imports Main begin subsection \Exercise 1\ text \ Prove the following statement only using @{method rule}: \ lemma mt: "A \ B \ \ B \ \ A" proof - assume "A \ B" and "\ B" show "\ A" proof assume "A" from \A \ B\ and \A\ have "B" .. from \\ B\ and \B\ show False .. qed qed subsection \Exercise 2\ text \ Prove the statement below (which might be useful for later exercises) only using @{method rule} together with facts from the following list: \ thm ccontr \ \classical contradiction / proof by contradiction\ thm allI \ \\ introduction\ thm exI \ \\ introduction\ thm notE \ \\ elimination\ lemma not_all_imp_ex_not: "\ (\x. P x) \ \x. \ P x" proof - assume "\ (\x. P x)" show "\x. \ P x" proof (rule ccontr) assume "\ (\x. \ P x)" have "\x. P x" proof (rule allI) fix x show "P x" proof (rule ccontr) assume "\ P x" then have "\x. \ P x" by (rule exI) from \\ (\x. \ P x)\ and this show False by (rule notE) qed qed from \\ (\x. P x)\ and this show False by (rule notE) qed qed subsection \Exercise 3\ text \ Prove the inequalities below by induction. The following facts may be useful: \ thm less_Suc_eq thm power2_eq_square lemma mult2_power2_leq: "n > 2 \ 2*n + 1 \ 2^n" by (induction n) (auto simp: less_Suc_eq) lemma square_power2_less: "n \ 5 \ n ^ 2 < 2 ^ n" proof (induction n) case (Suc n) show "Suc n ^ 2 < 2 ^ Suc n" proof (cases "5 \ n") case True from this and Suc have IH: "n^2 < 2^n" by auto have "(Suc n) ^ 2 = n^2 + 2*n + 1" by (auto simp: power2_eq_square) from this and IH have *: "Suc n ^ 2 < 2^n + 2*n + 1" by auto from True and mult2_power2_leq have "2^n + 2*n + 1 \ 2*2^n" by auto from this and * show ?thesis by auto next case False from Suc and this show ?thesis by (cases "n = 4") (auto) qed qed auto subsection \Exercise 4\ text \ Recall the function \prefixes\ from the slides. \ fun prefixes :: "'a list \ 'a list list" where "prefixes [] = [[]]" | "prefixes (x # xs) = [] # map ((#) x) (prefixes xs)" text \ Implement a recursive function \is_prefix\ that checks whether the first of two given lists is a prefix of the second one. Then prove the following equivalence (where @{term "(\)"} is set membership and @{const set} gives us the set of all elements in a list): \ fun is_prefix :: "'a list \ 'a list \ bool" where "is_prefix [] ys = True" | "is_prefix (x # xs) (y # ys) = (if x = y then is_prefix xs ys else False)" | "is_prefix _ _ = False" lemma Nil_in_prefixes: "[] \ set (prefixes xs)" by (induction xs) auto lemma "xs \ set (prefixes ys) \ is_prefix xs ys" proof (induction xs arbitrary: ys) case (Cons x xs) then show ?case by (cases ys) auto qed (auto simp: Nil_in_prefixes) subsection \Exercise 5\ text \ Consider a stream of bits (i.e., values which are either zero or one) that is modeled by a successor function \succ :: 'a \ 'a\ together with a predicate \ONE :: 'a \ bool\ First prove the following statement informally with pen and paper: If every zero is directly followed by a one, then there is a one whose next next bit is a one again. Then, prove its formal specification below only using @{method cases} for case analysis and @{method rule}. \ lemma "\x. \ ONE x \ ONE (succ x) \ \x. ONE x \ ONE (succ (succ x))" proof - assume *: "\x. \ ONE x \ ONE (succ x)" show "\x. ONE x \ ONE (succ (succ x))" proof (cases "\x. ONE (succ x)") case True \ \Every successor is one.\ fix x \ \Take an arbitrary bit.\ from True have 1: "ONE (succ x)" by (rule spec) from True have 2: "ONE (succ (succ (succ x)))" by (rule spec) from 1 and 2 have "ONE (succ x) \ ONE (succ (succ (succ x)))" by (rule conjI) then show ?thesis by (rule exI) next case False \ \There is a bit with a zero successor.\ then have "\x. \ ONE (succ x)" by (rule not_all_imp_ex_not) then show ?thesis proof fix x assume 1: "\ ONE (succ x)" from * have "\ ONE (succ x) \ ONE (succ (succ x))" by (rule spec) from this and 1 have 2: "ONE (succ (succ x))" by (rule mp) from * have "\ ONE x \ ONE (succ x)" by (rule spec) from this and 1 have "\ \ ONE x" by (rule mt) then have "ONE x" by (rule notnotD) from this and 2 have "ONE x \ ONE (succ (succ x))" by (rule conjI) then show ?thesis by (rule exI) qed qed qed end