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.
theory Defs imports "HOL-Data_Structures.Set_Specs" begin declare [[names_short]] declare Let_def[simp] datatype trie = LfR | LfA | Nd bool "trie * trie" (* Magic incantation, just ignore*) datatype_compat trie definition empty_trie :: trie where [simp]: "empty_trie = LfR" fun invar where "invar LfR = True" | "invar LfA = True" | "invar (Nd b (l,r)) = (invar l \<and> invar r \<and> (l = LfR \<and> r = LfR \<longrightarrow> b) \<and> (l = LfA \<and> r = LfA \<longrightarrow> \<not> b))" consts isin_trie :: "trie \<Rightarrow> bool list \<Rightarrow> bool" consts set_trie :: "trie \<Rightarrow> bool list set" consts node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" consts insert_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" consts delete_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" end
theory Submission
imports Defs
begin
fun isin_trie :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
"isin_trie _ _ = False"
definition set_trie :: "trie \<Rightarrow> bool list set" where
"set_trie t = {xs. isin_trie t xs}"
definition node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
"node _ _ = LfR"
fun insert_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
"insert_trie _ _ = LfR"
fun delete_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
"delete_trie _ _ = LfR"
lemma set_trie_insert_trie: "set_trie(insert_trie xs t) = set_trie t \<union> {xs}"
sorry
lemma set_trie_delete_trie: "set_trie(delete_trie xs t) = set_trie t - {xs}"
sorry
lemma invar_insert_trie: "invar t \<Longrightarrow> invar(insert_trie xs t)"
sorry
lemma invar_delete_trie: "invar t \<Longrightarrow> invar(delete_trie xs t)"
sorry
interpretation S: Set
where empty = empty_trie and isin = isin_trie and insert = insert_trie and delete = delete_trie
and set = set_trie and invar = invar
sorry
end
theory Check
imports Submission
begin
lemma set_trie_insert_trie: "set_trie(insert_trie xs t) = set_trie t \<union> {xs}"
by (rule Submission.set_trie_insert_trie)
lemma set_trie_delete_trie: "set_trie(delete_trie xs t) = set_trie t - {xs}"
by (rule Submission.set_trie_delete_trie)
lemma invar_insert_trie: "invar t \<Longrightarrow> invar(insert_trie xs t)"
by (rule Submission.invar_insert_trie)
lemma invar_delete_trie: "invar t \<Longrightarrow> invar(delete_trie xs t)"
by (rule Submission.invar_delete_trie)
end