Homework 1

Definitions File

theory Defs
  imports Main
begin

declare [[names_short]]

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"


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


end

Template File

theory Submission
  imports Defs
begin

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

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

theorem double_len: "length (double xs) = 2 * length xs"
  sorry

theorem reverse_double: "reverse (double xs) = double (reverse xs)"
  sorry

theorem rev_double: "rev (double xs) = double (rev xs)"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem double_len: "length (double xs) = 2 * length xs"
  by (rule Submission.double_len)

theorem reverse_double: "reverse (double xs) = double (reverse xs)"
  by (rule Submission.reverse_double)

theorem rev_double: "rev (double xs) = double (rev xs)"
  by (rule Submission.rev_double)

end