FDS Week 1 Homework

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" (*>*)

end

Template File

theory Template
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 max_reverse: "lmax (reverse xs) = lmax xs"
  sorry

end

Check File

theory Check
imports Submission
begin

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

lemma max_reverse: "lmax (reverse xs) = lmax xs"
  by (rule max_reverse)


end