Week 10 homework

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