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