Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 10

This is the task corresponding to homework 10.

## Resources

### 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```

Terms and Conditions