FDS Week 10 Homework 1

Definitions File

theory Defs
  imports Main
begin

  datatype trie = LeafF | LeafT | Node "trie * trie"

end

Template File

theory Template
  imports Defs
begin

fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
  "isin _ _ = undefined"

fun ins :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
  "ins _ _ = undefined"

fun delete2 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
"delete2 _ _ = undefined"

fun is_trie :: "nat \<Rightarrow> trie \<Rightarrow> bool" where
  "is_trie _ _ = undefined"

lemma isin_correct:
  "\<lbrakk> is_trie n t; length as = n \<rbrakk> \<Longrightarrow> isin (ins as t) bs = (as = bs \<or> isin t bs) \<and> is_trie n (ins as t)"
  sorry

lemma delete2_correct:
  "is_trie n t \<Longrightarrow> isin (delete2 as t) bs = (as\<noteq>bs \<and> isin t bs) \<and> (is_trie n (delete2 as t))"
  sorry

end

Check File

theory Check
  imports Template
begin

lemma isin_correct:
  "\<lbrakk> is_trie n t; length as = n \<rbrakk> \<Longrightarrow> isin (ins as t) bs = (as = bs \<or> isin t bs) \<and> is_trie n (ins as t)"
  by(rule isin_correct)

lemma delete2_correct:
  "is_trie n t \<Longrightarrow> isin (delete2 as t) bs = (as\<noteq>bs \<and> isin t bs) \<and> (is_trie n (delete2 as t))"
  by(rule delete2_correct)

end