Homework 2

Definitions File

theory Defs
  imports Main
begin

fun contains :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" where
  "contains x [] = False"
| "contains x (y#ys) \<longleftrightarrow> x=y \<or> contains x ys"

lemma contains_append[simp]: "contains a (xs@[b]) = (contains a xs \<or> a = b)"
  by (induction xs) auto

lemma contains_rev: "contains a (rev xs) = contains a xs"
  by (induction xs) auto


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

consts length_fold :: "'a list \<Rightarrow> nat"

consts length_foldr :: "'a list \<Rightarrow> nat"

consts slice :: "'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list"


end

Template File

theory Submission
  imports Defs
begin

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

lemma ldistinct_rev: "ldistinct (rev xs) = ldistinct xs"
  sorry

thm fold.simps
thm foldr.simps

definition length_fold :: "'a list \<Rightarrow> nat"  where
  "length_fold _ = undefined"

definition length_foldr :: "'a list \<Rightarrow> nat"  where
  "length_foldr _ = undefined"

lemma length_fold: "length_fold xs = length xs"
  sorry

lemma length_foldr: "length_foldr xs = length xs"
  sorry

fun slice :: "'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list"  where
  "slice _ = undefined"

value "slice [0,1,2,3,4,5,6::int] 2 3 = [2,3,4]" text \<open>(In range)\<close>
value "slice [0,1,2,3,4,5,6::int] 2 10 = [2,3,4,5,6]" text \<open>(Length out of range)\<close>
value "slice [0,1,2,3,4,5,6::int] 10 10 = []" text \<open>(Start index out of range)\<close>

lemma slice_append: "slice xs s l1 @ slice xs (s+l1) l2 = slice xs s (l1+l2)"
  sorry

lemma ldistinct_slice: "ldistinct xs \<Longrightarrow> ldistinct (slice xs s l)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma ldistinct_rev: "ldistinct (rev xs) = ldistinct xs"
  by (rule Submission.ldistinct_rev)

lemma length_fold: "length_fold xs = length xs"
  by (rule Submission.length_fold)

lemma length_foldr: "length_foldr xs = length xs"
  by (rule Submission.length_foldr)

lemma slice_append: "slice xs s l1 @ slice xs (s+l1) l2 = slice xs s (l1+l2)"
  by (rule Submission.slice_append)

lemma ldistinct_slice: "ldistinct xs \<Longrightarrow> ldistinct (slice xs s l)"
  by (rule Submission.ldistinct_slice)

end