Homework 01

Definitions File

theory Defs
  imports Main
begin

text ‹Definitions and lemmas from the tutorial›

fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
"snoc [] x = [x]" |
"snoc (y # ys) x = y # (snoc ys x)"

fun reverse :: "'a list ⇒ 'a list" where
"reverse [] = []" |
"reverse (x # xs) = snoc (reverse xs) x"

lemma reverse_snoc: "reverse (snoc xs y) = y # reverse xs"
by (induct xs) auto

theorem reverse_reverse: "reverse (reverse xs) = xs"
  by (induct xs) (auto simp add: reverse_snoc)

end

Template File

theory Submission
  imports Defs
begin

fun list_sum :: "nat list ⇒ nat" where
  "list_sum _ = undefined"

theorem list_sum_reverse:
  "list_sum (reverse xs) = list_sum xs"
  sorry

fun upto :: "nat ⇒ nat list" where
  "upto _ = undefined"

theorem gauss:
  "list_sum (upto n) = n * (n + 1) div 2"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem list_sum_reverse:
  "list_sum (reverse xs) = list_sum xs"
  by (rule Submission.list_sum_reverse)

theorem gauss:
  "list_sum (upto n) = n * (n + 1) div 2"
  by (rule Submission.gauss)

end