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

### Definitions File

```theory Defs
imports "HOL-Data_Structures.Tries_Binary"
begin

fun is_some where
"is_some (Some _) = True"
| "is_some None = False"

datatype 'a trieIP = LfIP
| UnIP bool "'a trieIP"
| NdIP "'a option" "'a trieIP * 'a trieIP"

consts keys :: "'a trieIP \<Rightarrow> trie"

consts lookupIP :: "'a trieIP \<Rightarrow> bool list \<rightharpoonup> 'a"

consts updateIP :: "bool list \<Rightarrow> 'a \<Rightarrow> 'a trieIP \<Rightarrow> 'a trieIP"

consts delete0IP :: "bool list \<Rightarrow> 'a trieIP \<Rightarrow> 'a trieIP"

consts deleteIP :: "bool list \<Rightarrow> 'a trieIP \<Rightarrow> 'a trieIP"

end```

### Template File

```theory Submission
imports Defs
begin

fun keys :: "'a trieIP \<Rightarrow> trie"  where
"keys _ = undefined"

fun lookupIP :: "'a trieIP \<Rightarrow> bool list \<rightharpoonup> 'a"  where
"lookupIP _ = undefined"

theorem lookup_keys: "isin (keys t) ks \<longleftrightarrow> is_some (lookupIP t ks)"
sorry

fun updateIP :: "bool list \<Rightarrow> 'a \<Rightarrow> 'a trieIP \<Rightarrow> 'a trieIP"  where
"updateIP _ = undefined"

theorem update_set: "x \<in> set_trieIP (updateIP ks x t)"
sorry

theorem update_lookup: "lookupIP (updateIP ks x t) ks = Some x"
sorry

fun delete0IP :: "bool list \<Rightarrow> 'a trieIP \<Rightarrow> 'a trieIP"  where
"delete0IP _ = undefined"

lemma delete0_keys: "keys (delete0IP ks t) = delete0 ks (keys t)"
sorry

fun deleteIP :: "bool list \<Rightarrow> 'a trieIP \<Rightarrow> 'a trieIP"  where
"deleteIP _ = undefined"

lemma delete_keys: "keys (deleteIP ks t) = delete ks (keys t)"
sorry

end```

### Check File

```theory Check
imports Submission
begin

theorem lookup_keys: "isin (keys t) ks \<longleftrightarrow> is_some (lookupIP t ks)"
by (rule Submission.lookup_keys)

theorem update_set: "x \<in> set_trieIP (updateIP ks x t)"
by (rule Submission.update_set)

theorem update_lookup: "lookupIP (updateIP ks x t) ks = Some x"
by (rule Submission.update_lookup)

lemma delete0_keys: "keys (delete0IP ks t) = delete0 ks (keys t)"
by (rule Submission.delete0_keys)

lemma delete_keys: "keys (deleteIP ks t) = delete ks (keys t)"
by (rule Submission.delete_keys)

end```

Terms and Conditions