Homework 10

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