fun isin :: "'a trie \ 'a list \ bool" where "isin (Nd b m) [] = b" | "isin (Nd b m) (k # xs) = (case m k of None \ False | Some t \ isin t xs)"
fun insert :: "'a list \ 'a trie \ 'a trie" where "insert [] (Nd b m) = Nd True m" | "insert (x#xs) (Nd b m) =
(let s = (case m x of None \<Rightarrow> empty | Some t \<Rightarrow> t) in Nd b (m(x := Some(insert xs s))))"
fun delete :: "'a list \ 'a trie \ 'a trie" where "delete [] (Nd b m) = Nd False m" | "delete (x#xs) (Nd b m) = Nd b
(case m x of
None \<Rightarrow> m |
Some t \<Rightarrow> m(x := Some(delete xs t)))"
text\<open>Use (a tuned version of) @{const isin} as an abstraction function:\<close>
lemma isin_case: "isin (Nd b m) xs =
(case xs of
[] \<Rightarrow> b |
x # ys \<Rightarrow> (case m x of None \<Rightarrow> False | Some t \<Rightarrow> isin t ys))" by(cases xs)auto
definition set_trie :: "'a trie \ 'a list set" where
[simp]: "set_trie t = {xs. isin t xs}"
lemma isin_set_trie: "isin t xs = (xs \ set_trie t)" by simp
lemma set_trie_insert: "set_trie (insert xs t) = set_trie t \ {xs}" by (induction xs t rule: insert.induct)
(auto simp: isin_case split!: if_splits option.splits list.splits)
lemma set_trie_delete: "set_trie (delete xs t) = set_trie t - {xs}" by (induction xs t rule: delete.induct)
(auto simp: isin_case split!: if_splits option.splits list.splits)
interpretation S: Set where empty = empty and isin = isin and insert = insert and delete = delete and set = set_trie and invar = "\_. True" proof (standard, goal_cases) case 1 show ?caseby (simp add: isin_case split: list.split) next case 2 show ?caseby(rule isin_set_trie) next case 3 show ?caseby(rule set_trie_insert) next case 4 show ?caseby(rule set_trie_delete) qed (rule TrueI)+
end
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
