Homework 1

Definitions File

theory Defs
  imports Main
begin

fun snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where
  "snoc [] x = [x]" |
  "snoc (y # ys) x = y # (snoc ys x)"

fun reverse :: "'a list \<Rightarrow> '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 xs) = xs"
  by (induct xs) (auto simp add: reverse_snoc)

fun count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
  "count [] _ = 0" |
  "count (x # xs) y = (if x = y then Suc (count xs y) else count xs y)"


consts oddsum :: "nat \<Rightarrow> nat"

consts spread :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"


end

Template File

theory Submission
  imports Defs
begin

fun oddsum :: "nat \<Rightarrow> nat"  where
  "oddsum _ = 0"

value "oddsum 3 = 5 + 3 + 1 + 0"
value "oddsum 7 = 49"
value "oddsum 1 = 1"

lemma oddsum_is_square: "oddsum n = n * n"
  sorry

lemma oddsum_mult: "oddsum (n*m) = oddsum n * oddsum m"
  sorry

fun spread :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  where
  "spread _ _ = []"

value "spread (0::nat) [1,2,3] = [1,0,2,0,3,0]"

lemma count_spread: "count (spread a xs) a = count xs a + length xs"
  sorry

lemma spread_reverse_snoc: "snoc (reverse (spread a xs)) a = a # spread a (reverse xs)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma oddsum_is_square: "oddsum n = n * n"
  by (rule Submission.oddsum_is_square)

lemma oddsum_mult: "oddsum (n*m) = oddsum n * oddsum m"
  by (rule Submission.oddsum_mult)

lemma count_spread: "count (spread a xs) a = count xs a + length xs"
  by (rule Submission.count_spread)

lemma spread_reverse_snoc: "snoc (reverse (spread a xs)) a = a # spread a (reverse xs)"
  by (rule Submission.spread_reverse_snoc)

end