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}(cases~{"}as{"},~auto)\isacommand{.}% |
47 \isacommand{apply}(case\_tac~as,~auto)\isacommand{.}% |
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}% |
91 guided by the intuition that simplification of \isa{lookup} might be easier |
91 guided by the intuition that simplification of \isa{lookup} might be easier |
92 if \isa{update} has already been simplified, which can only happen if |
92 if \isa{update} has already been simplified, which can only happen if |
93 \isa{as} is instantiated. |
93 \isa{as} is instantiated. |
94 The start of the proof is completely conventional:% |
94 The start of the proof is completely conventional:% |
95 \end{isamarkuptxt}% |
95 \end{isamarkuptxt}% |
96 \isacommand{apply}(induct\_tac~{"}as{"},~auto)% |
96 \isacommand{apply}(induct\_tac~as,~auto)% |
97 \begin{isamarkuptxt}% |
97 \begin{isamarkuptxt}% |
98 \noindent |
98 \noindent |
99 Unfortunately, this time we are left with three intimidating looking subgoals: |
99 Unfortunately, this time we are left with three intimidating looking subgoals: |
100 \begin{isabellepar}% |
100 \begin{isabellepar}% |
101 ~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline |
101 ~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline |
110 \isacommand{apply}(auto)\isacommand{.}% |
110 \isacommand{apply}(auto)\isacommand{.}% |
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]}. Individual |
115 applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual |
116 subgoal number are also allowed. |
116 subgoal numbers are also allowed. |
117 |
117 |
118 This proof may look surprisingly straightforward. However, note that this |
118 This proof may look surprisingly straightforward. However, note that this |
119 comes at a cost: the proof script is unreadable because the |
119 comes at a cost: the proof script is unreadable because the |
120 intermediate proof states are invisible, and we rely on the (possibly |
120 intermediate proof states are invisible, and we rely on the (possibly |
121 brittle) magic of \isa{auto} (after the induction) to split the remaining |
121 brittle) magic of \isa{auto} (after the induction) to split the remaining |