I agree 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.

Download Files
### Definitions File

### Template File

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

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

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