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

theory Solutions04
  imports Demo04
begin

subsection \<open>Exercise 1\<close>

text \<open>
Prove that @{const Demo04.add} is associative and commutative.
\<close>
lemma add_Suc_left [simp]:
  "add (Suc x) y = Suc (add x y)"
  by (induction y) (simp_all only: add.simps)

lemma add_assoc [simp]: "add (add x y) z = add x (add y z)" by (induction y) simp_all

lemma add_commute: "add x y = add y x" by (induction y) simp_all


subsection \<open>Exercise 2\<close>

text \<open>
Prove that @{const Demo04.mul} can also be computed via recursion on its first argument.
\<close>
lemma mul0_left [simp]: "mul 0 y = 0" by (induction y) simp_all

lemma mul_Suc_left [simp]: "mul (Suc x) y = add y (mul x y)" by (induction y) simp_all


subsection \<open>Exercise 3\<close>

text \<open>
Define a recursive function \<open>div2\<close> that computes "division by 2" and prove that

  \<open>m + n/2 = (2m + n)/2\<close>
\<close>

fun div2 :: "nat \<Rightarrow> nat"
  where
    "div2 0 = 0"
  | "div2 (Suc 0) = 0"
  | "div2 (Suc (Suc x)) = Suc (div2 x)"

lemma div2_add_self [simp]: "div2 (add m m) = m"
  by (induction m) simp_all

lemma div2_Suc_add_self [simp]: "div2 (Suc (add m m)) = m"
  by (induction m) simp_all

lemma add_div2:
  "add m (div2 n) = div2 (add (mul (Suc (Suc 0)) m) n)"
  by (induction m) simp_all


subsection \<open>Exercise 4\<close>

text \<open>
Only using @{const Demo04.add} and @{const Demo04.mul}, define a function \<open>sum\<close> such that

  \<open>sum n = 0 + 1 + 2 + \<cdots> + n\<close>

and prove Gauss's equation.
\<close>
fun sum :: "nat \<Rightarrow> nat"
  where
    "sum 0 = 0"
  | "sum (Suc n) = add (Suc n) (sum n)"

lemma
  "sum n = div2 (mul n (Suc n))"
proof (induction n)
  case 0
  have "sum 0 = 0" unfolding sum.simps ..
  also have "\<dots> = div2 (mul 0 (Suc 0))" unfolding mul0_left and div2.simps ..
  finally show ?case .
next
  case IH: (Suc n)
  have "sum (Suc n) = add (Suc n) (sum n)" unfolding sum.simps ..
  also have "\<dots> = add (Suc n) (div2 (mul n (Suc n)))" unfolding IH ..
  also have "\<dots> = add (Suc n) (div2 (add (mul n n) n))" unfolding mul.simps ..
  also have "\<dots> = div2 (add (mul (Suc (Suc 0)) (Suc n)) (add (mul n n) n))" unfolding add_div2 ..
  finally show ?case by (simp add: add_commute)
qed

end