equal
deleted
inserted
replaced
50 trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely |
50 trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely |
51 distinguishes the two cases whether the search string is empty or not: |
51 distinguishes the two cases whether the search string is empty or not: |
52 *}; |
52 *}; |
53 |
53 |
54 lemma [simp]: "lookup (Trie None []) as = None"; |
54 lemma [simp]: "lookup (Trie None []) as = None"; |
55 by(case_tac as, auto); |
55 by(case_tac as, simp_all); |
56 |
56 |
57 text{* |
57 text{* |
58 Things begin to get interesting with the definition of an update function |
58 Things begin to get interesting with the definition of an update function |
59 that adds a new (string,value) pair to a trie, overwriting the old value |
59 that adds a new (string,value) pair to a trie, overwriting the old value |
60 associated with that string: |
60 associated with that string: |
127 e.g. \isa{[2]} are also allowed. |
127 e.g. \isa{[2]} are also allowed. |
128 |
128 |
129 This proof may look surprisingly straightforward. However, note that this |
129 This proof may look surprisingly straightforward. However, note that this |
130 comes at a cost: the proof script is unreadable because the |
130 comes at a cost: the proof script is unreadable because the |
131 intermediate proof states are invisible, and we rely on the (possibly |
131 intermediate proof states are invisible, and we rely on the (possibly |
132 brittle) magic of \isa{auto} (after the induction) to split the remaining |
132 brittle) magic of \isa{auto} (\isa{simp\_all} will not do---try it) to split the subgoals |
133 goals up in such a way that case distinction on \isa{bs} makes sense and |
133 of the induction up in such a way that case distinction on \isa{bs} makes sense and |
134 solves the proof. Part~\ref{Isar} shows you how to write readable and stable |
134 solves the proof. Part~\ref{Isar} shows you how to write readable and stable |
135 proofs. |
135 proofs. |
136 *}; |
136 *}; |
137 |
137 |
138 (*<*) |
138 (*<*) |