doc-src/Exercises/2001/a3/Trie2.thy

Removed ~10000 hack in function idx that can lead to inconsistencies
when unifying terms with a large number of abstractions.

(*<*)
theory Trie2 = Main:
(*>*)

text {* Die above definition of @{term update} has the disadvantage
that it often creates junk: each association list it passes through is
extended at the left end with a new (letter,value) pair without
removing any old association of that letter which may already be
present.  Logically, such cleaning up is unnecessary because @{term
assoc} always searches the list from the left. However, it constitutes
a space leak: the old associations cannot be garbage collected because
physically they are still reachable. This problem can be solved by
means of a function *}

consts overwrite :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b) list \<Rightarrow> ('a * 'b) list"

text {* that does not just add new pairs at the front but replaces old
associations by new pairs if possible.

Define @{term overwrite}, modify @{term modify} to employ @{term
overwrite}, and show the same relationship between @{term modify} and
@{term lookup} as before. *}

(*<*)
end;
(*>*)