Homework 10

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