equal
deleted
inserted
replaced
42 As a first simple property we prove that looking up a string in the empty |
42 As a first simple property we prove that looking up a string in the empty |
43 trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely |
43 trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely |
44 distinguishes the two cases whether the search string is empty or not:% |
44 distinguishes the two cases whether the search string is empty or not:% |
45 \end{isamarkuptext}% |
45 \end{isamarkuptext}% |
46 \isacommand{lemma}~[simp]:~{"}lookup~(Trie~None~[])~as~=~None{"}\isanewline |
46 \isacommand{lemma}~[simp]:~{"}lookup~(Trie~None~[])~as~=~None{"}\isanewline |
47 \isacommand{apply}(case\_tac~as,~auto)\isacommand{.}% |
47 \isacommand{by}(case\_tac~as,~auto)% |
48 \begin{isamarkuptext}% |
48 \begin{isamarkuptext}% |
49 Things begin to get interesting with the definition of an update function |
49 Things begin to get interesting with the definition of an update function |
50 that adds a new (string,value) pair to a trie, overwriting the old value |
50 that adds a new (string,value) pair to a trie, overwriting the old value |
51 associated with that string:% |
51 associated with that string:% |
52 \end{isamarkuptext}% |
52 \end{isamarkuptext}% |
105 Clearly, if we want to make headway we have to instantiate \isa{bs} as |
105 Clearly, if we want to make headway we have to instantiate \isa{bs} as |
106 well now. It turns out that instead of induction, case distinction |
106 well now. It turns out that instead of induction, case distinction |
107 suffices:% |
107 suffices:% |
108 \end{isamarkuptxt}% |
108 \end{isamarkuptxt}% |
109 \isacommand{apply}(case\_tac[!]~bs)\isanewline |
109 \isacommand{apply}(case\_tac[!]~bs)\isanewline |
110 \isacommand{apply}(auto)\isacommand{.}% |
110 \isacommand{by}(auto)% |
111 \begin{isamarkuptext}% |
111 \begin{isamarkuptext}% |
112 \noindent |
112 \noindent |
113 Both \isaindex{case_tac} and \isaindex{induct_tac} |
113 Both \isaindex{case_tac} and \isaindex{induct_tac} |
114 take an optional first argument that specifies the range of subgoals they are |
114 take an optional first argument that specifies the range of subgoals they are |
115 applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual |
115 applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual |