FDS week 1 homework

Definitions File

theory Defs
  imports Main
begin

end

Template File

theory Submission
  imports Defs
begin

fun find_pfx :: "nat list => nat => nat list" where
 "find_pfx _ _ = undefined"

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 find_pfx_append_2:
  "\<exists>xs2. xs = find_pfx xs x @ xs2"
  sorry

end

Check File

theory Check
  imports Submission
begin

text "Test cases"
lemma  "find_pfx [1::nat,2,3] 2 = [1,2]"
       "find_pfx [] (1::nat) = []"
  by simp+

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 find_pfx_append_2:
  "\<exists>xs2. xs = find_pfx xs x @ xs2"
  by (rule Submission.find_pfx_append_2)


end