Homework 10

Definitions File

theory Defs
  imports "HOL-Data_Structures.Tries_Binary"
begin

declare [[names_short]]

datatype trie' = LfF | LfT | NdI "trie' \<times> trie'"


consts is_trie :: "nat \<Rightarrow> trie' \<Rightarrow> bool"

consts isin :: "trie' \<Rightarrow> bool list \<Rightarrow> bool"

consts ins :: "bool list \<Rightarrow> trie' \<Rightarrow> trie'"

consts delete :: "bool list \<Rightarrow> trie' \<Rightarrow> trie'"


end

Template File

theory Submission
  imports Defs
begin

fun is_trie :: "nat \<Rightarrow> trie' \<Rightarrow> bool"  where
  "is_trie _ _ = False"

value "is_trie 42 LfF"
value "is_trie 2 (NdI (LfF,NdI (LfT,LfF)))"
text \<open>Whereas these should be false\<close>
value "is_trie 42 LfT"
value "is_trie 2 (NdI (LfT,NdI (LfT,LfF)))"
value "is_trie 1 (NdI (LfT,NdI (LfF,LfF)))"


fun isin :: "trie' \<Rightarrow> bool list \<Rightarrow> bool"  where
  "isin _ _ = False"

fun ins :: "bool list \<Rightarrow> trie' \<Rightarrow> trie'"  where
  "ins _ _ = LfF"

lemma isin_ins:
    assumes "is_trie n t"
      and "length as = n"
  shows "isin (ins as t) bs = (as = bs \<or> isin t bs) \<and> is_trie n (ins as t)"
  sorry

fun delete :: "bool list \<Rightarrow> trie' \<Rightarrow> trie'"  where
  "delete _ _ = LfF"

lemma isin_delete:
    assumes "is_trie n t"
  shows "isin (delete as t) bs = (as\<noteq>bs \<and> isin t bs) \<and> (is_trie n (delete as t))"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma isin_ins: "(is_trie n t) \<Longrightarrow> (length as = n) \<Longrightarrow> isin (ins as t) bs = (as = bs \<or> isin t bs) \<and> is_trie n (ins as t)"
  by (rule Submission.isin_ins)

lemma isin_delete: "(is_trie n t) \<Longrightarrow> isin (delete as t) bs = (as\<noteq>bs \<and> isin t bs) \<and> (is_trie n (delete as t))"
  by (rule Submission.isin_delete)

end