section \<open>Solutions for Session 3\<close>

theory Solutions03
  imports Main
begin

subsection \<open>Exercise 1\<close>

text \<open>
Prove the following statement only using @{method rule}:
\<close>
lemma mt:
  "A \<longrightarrow> B \<Longrightarrow> \<not> B \<Longrightarrow> \<not> A"
proof -
  assume "A \<longrightarrow> B" and "\<not> B"
  show "\<not> A"
  proof
    assume "A"
    from \<open>A \<longrightarrow> B\<close> and \<open>A\<close> have "B" ..
    from \<open>\<not> B\<close> and \<open>B\<close> show False ..
  qed
qed


subsection \<open>Exercise 2\<close>

text \<open>
Prove the statement below (which might be useful for later exercises) only using
@{method rule} together with facts from the following list:
\<close>
thm ccontr \<comment> \<open>classical contradiction / proof by contradiction\<close>
thm allI \<comment> \<open>\<forall> introduction\<close>
thm exI \<comment> \<open>\<exists> introduction\<close>
thm notE \<comment> \<open>\<not> elimination\<close>

lemma not_all_imp_ex_not:
  "\<not> (\<forall>x. P x) \<Longrightarrow> \<exists>x. \<not> P x"
proof -
  assume "\<not> (\<forall>x. P x)"
  show "\<exists>x. \<not> P x"
  proof (rule ccontr)
    assume "\<not> (\<exists>x. \<not> P x)"
    have "\<forall>x. P x"
    proof (rule allI)
      fix x
      show "P x"
      proof (rule ccontr)
        assume "\<not> P x"
        then have "\<exists>x. \<not> P x" by (rule exI)
        from \<open>\<not> (\<exists>x. \<not> P x)\<close> and this
        show False by (rule notE)
      qed
    qed
    from \<open>\<not> (\<forall>x. P x)\<close> and this
    show False by (rule notE)
  qed
qed


subsection \<open>Exercise 3\<close>

text \<open>
Prove the inequalities below by induction.
The following facts may be useful:
\<close>
thm less_Suc_eq
thm power2_eq_square

lemma mult2_power2_leq: "n > 2 \<Longrightarrow> 2*n + 1 \<le> 2^n"
  by (induction n) (auto simp: less_Suc_eq)

lemma square_power2_less: "n \<ge> 5 \<Longrightarrow> n ^ 2 < 2 ^ n"
proof (induction n)
  case (Suc n)
  show "Suc n ^ 2 < 2 ^ Suc n"
  proof (cases "5 \<le> 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 \<le> 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 \<open>Exercise 4\<close>

text \<open>
Recall the function \<open>prefixes\<close> from the slides.
\<close>
fun prefixes :: "'a list \<Rightarrow> 'a list list"
  where
    "prefixes [] = [[]]"
  | "prefixes (x # xs) = [] # map ((#) x) (prefixes xs)"

text \<open>
Implement a recursive function \<open>is_prefix\<close> that checks whether the first of
two given lists is a prefix of the second one.

Then prove the following equivalence (where @{term "(\<in>)"} is set membership
and @{const set} gives us the set of all elements in a list):
\<close>
fun is_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> 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: "[] \<in> set (prefixes xs)"
  by (induction xs) auto

lemma
  "xs \<in> set (prefixes ys) \<longleftrightarrow> 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 \<open>Exercise 5\<close>

text \<open>
Consider a stream of bits (i.e., values which are either zero or one) that is modeled
by a successor function \<open>succ :: 'a \<Rightarrow> 'a\<close> together with a predicate \<open>ONE :: 'a \<Rightarrow> bool\<close>

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}.
\<close>
lemma
  "\<forall>x. \<not> ONE x \<longrightarrow> ONE (succ x) \<Longrightarrow> \<exists>x. ONE x \<and> ONE (succ (succ x))"
proof -
  assume *: "\<forall>x. \<not> ONE x \<longrightarrow> ONE (succ x)"
  show "\<exists>x. ONE x \<and> ONE (succ (succ x))"
  proof (cases "\<forall>x. ONE (succ x)")
    case True \<comment> \<open>Every successor is one.\<close>
    fix x \<comment> \<open>Take an arbitrary bit.\<close>
    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) \<and> ONE (succ (succ (succ x)))" by (rule conjI)
    then show ?thesis by (rule exI)
  next
    case False \<comment> \<open>There is a bit with a zero successor.\<close>
    then have "\<exists>x. \<not> ONE (succ x)" by (rule not_all_imp_ex_not)
    then show ?thesis
    proof
      fix x assume 1: "\<not> ONE (succ x)"
      from * have "\<not> ONE (succ x) \<longrightarrow> ONE (succ (succ x))" by (rule spec)
      from this and 1 have 2: "ONE (succ (succ x))" by (rule mp)
      from * have "\<not> ONE x \<longrightarrow> ONE (succ x)" by (rule spec)
      from this and 1 have "\<not> \<not> ONE x" by (rule mt)
      then have "ONE x" by (rule notnotD)
      from this and 2 have "ONE x \<and> ONE (succ (succ x))" by (rule conjI)
      then show ?thesis by (rule exI)
    qed
  qed
qed

end