FDS Week 2 Homework

Definitions File

theory Defs
  imports Main
begin


end

Template File

theory Template
  imports Defs
begin

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

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

lemma ldistinct_rev: "ldistinct (rev xs) \<longleftrightarrow> ldistinct xs"
  sorry

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"

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) \<longleftrightarrow> ldistinct xs"
  by (rule ldistinct_rev) 

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

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

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

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

end