Cookies disclaimer

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.

Homework 10

This is the task corresponding to homework 10.

Resources

Download Files

Definitions File

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

Template File

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

Check File

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

Terms and Conditions