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)


consts lmax :: "nat list \<Rightarrow> nat"

consts contains :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

fun lmax :: "nat list \<Rightarrow> nat"  where
  "lmax _ = undefined"

lemma max_greater: "x \<in> set xs \<Longrightarrow> x\<le>lmax xs"
  sorry

lemma lmax_reverse: "lmax (reverse xs) = lmax xs"
  sorry

fun contains :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"  where
  "contains _ = undefined"

lemma contains_reverse: "contains a (reverse xs) = contains a xs"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma max_greater: "x \<in> set xs \<Longrightarrow> x\<le>lmax xs"
  by (rule Submission.max_greater)

lemma lmax_reverse: "lmax (reverse xs) = lmax xs"
  by (rule Submission.lmax_reverse)

lemma contains_reverse: "contains a (reverse xs) = contains a xs"
  by (rule Submission.contains_reverse)

end