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.

Week 10 homework

Week 10 homework

Resources

Definitions File

```theory Defs
imports Main
begin

lemma [simp]: "(\<forall>x. x \<noteq> y) = False"
by blast

hide_const (open) insert

declare Let_def[simp]

subsection "Trie"

datatype trie = Leaf | Node bool "trie * trie"

fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
"isin Leaf ks = False" |
"isin (Node b (l,r)) ks =
(case ks of
[] \<Rightarrow> b |
k#ks \<Rightarrow> isin (if k then r else l) ks)"

fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
"insert [] Leaf = Node True (Leaf,Leaf)" |
"insert [] (Node b lr) = Node True lr" |
"insert (k#ks) Leaf =
Node False (if k then (Leaf, insert ks Leaf)
else (insert ks Leaf, Leaf))" |
"insert (k#ks) (Node b (l,r)) =
Node b (if k then (l, insert ks r)
else (insert ks l, r))"

lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)"
apply(induction as t arbitrary: bs rule: insert.induct)
apply (auto split: list.splits)
done

text \<open>A simple implementation of delete; does not shrink the trie!\<close>

fun delete :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
"delete ks Leaf = Leaf" |
"delete ks (Node b (l,r)) =
(case ks of
[] \<Rightarrow> Node False (l,r) |
k#ks' \<Rightarrow> Node b (if k then (l, delete ks' r) else (delete ks' l, r)))"

lemma "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)"
apply(induction as t arbitrary: bs rule: delete.induct)
apply (auto split: list.splits)
done

fun node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
"node b lr = (if \<not> b \<and> lr = (Leaf,Leaf) then Leaf else Node b lr)"

fun delete2 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
"delete2 ks Leaf = Leaf" |
"delete2 ks (Node b (l,r)) =
(case ks of
[] \<Rightarrow> node False (l,r) |
k#ks' \<Rightarrow> node b (if k then (l, delete2 ks' r) else (delete2 ks' l, r)))"

lemma "isin (delete2 as t) bs = isin (delete as t) bs"
apply(induction as t arbitrary: bs rule: delete2.induct)
apply simp
apply (force split: list.splits)
done

fun union :: "trie \<Rightarrow> trie \<Rightarrow> trie" where
"union Leaf t = t"
| "union t Leaf = t"
| "union (Node v (l,r)) (Node v' (l',r')) = (
Node (v \<or> v') (union l l', union r r'))"

lemma [simp]: "union t Leaf = t" by (cases t) auto

lemma "isin (union a b) x = isin a x \<or> isin b x"
apply (induction a b arbitrary: x rule: union.induct)
apply (auto split: list.split)
done

datatype iptrie = IPLeaf | IPUnary bool iptrie | IPBinary bool "iptrie * iptrie"

fun iptrie_\<alpha> :: "iptrie \<Rightarrow> trie" where
"iptrie_\<alpha> IPLeaf = Leaf"
| "iptrie_\<alpha> (IPUnary x t) = (
if x then Node False (Leaf, iptrie_\<alpha> t)
else Node False (iptrie_\<alpha> t, Leaf))"
| "iptrie_\<alpha> (IPBinary v (l,r)) = Node v (iptrie_\<alpha> l, iptrie_\<alpha> r)"

end```

Template File

```theory Submission
imports Defs
begin

fun ipisin :: "iptrie \<Rightarrow> bool list \<Rightarrow> bool" where
"ipisin _ = undefined"

lemma isin_refine: "ipisin t xs = isin (iptrie_\<alpha> t) xs"
sorry

fun ipunion :: "iptrie \<Rightarrow> iptrie \<Rightarrow> iptrie" where
"ipunion _ = undefined"

lemma union_refine: "iptrie_\<alpha> (ipunion t1 t2) = union (iptrie_\<alpha> t1) (iptrie_\<alpha> t2)"
sorry

fun ipdelete :: "bool list \<Rightarrow> iptrie \<Rightarrow> iptrie" where
"ipdelete _ = undefined"

lemma delete_refine: "iptrie_\<alpha> (ipdelete ks t) = delete ks (iptrie_\<alpha> t)"
sorry

fun shrink_unary where
"shrink_unary _ = undefined"

fun shrink_binary where
"shrink_binary _ = undefined"

fun ipdelete2 :: "bool list \<Rightarrow> iptrie \<Rightarrow> iptrie" where
"ipdelete2 _ = undefined"

lemma delete2_refine: "iptrie_\<alpha> (ipdelete2 ks t) = delete2 ks (iptrie_\<alpha> t)"
sorry

end```

Check File

```theory Check
imports "Submission"
begin

lemma isin_refine: "ipisin t xs = isin (iptrie_\<alpha> t) xs"
by(rule isin_refine)

lemma union_refine: "iptrie_\<alpha> (ipunion t1 t2) = union (iptrie_\<alpha> t1) (iptrie_\<alpha> t2)"
by(rule union_refine)

lemma delete_refine: "iptrie_\<alpha> (ipdelete ks t) = delete ks (iptrie_\<alpha> t)"
by(rule delete_refine)

lemma delete2_refine: "iptrie_\<alpha> (ipdelete2 ks t) = delete2 ks (iptrie_\<alpha> t)"
by(rule delete2_refine)

end```

Terms and Conditions