Homework 1

Definitions File

theory Defs
  imports Main
begin


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


end

Template File

theory Submission
  imports Defs
begin

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

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

lemma find_pfx_append:
  "(find_pfx (xs1 @ [x] @ xs2) x) = (find_pfx (xs1 @ [x]) x)"
  sorry

lemma last_find_pfx_val:
  "last (find_pfx (xs @ [x]) x) = x"
  sorry

lemma pfx_append_same: "x \<in> set xs \<Longrightarrow> find_pfx (xs @ xs) x = find_pfx xs x"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma find_pfx_append: "(find_pfx (xs1 @ [x] @ xs2) x) = (find_pfx (xs1 @ [x]) x)"
  by (rule Submission.find_pfx_append)

lemma last_find_pfx_val: "last (find_pfx (xs @ [x]) x) = x"
  by (rule Submission.last_find_pfx_val)

lemma pfx_append_same: "x \<in> set xs \<Longrightarrow> find_pfx (xs @ xs) x = find_pfx xs x"
  by (rule Submission.pfx_append_same)

end