79 Before we start on any proofs about \isa{update} we tell the simplifier to |
79 Before we start on any proofs about \isa{update} we tell the simplifier to |
80 expand all \isa{let}s and to split all \isa{case}-constructs over |
80 expand all \isa{let}s and to split all \isa{case}-constructs over |
81 options: |
81 options: |
82 *}; |
82 *}; |
83 |
83 |
84 theorems [simp] = Let_def; |
84 lemmas [simp] = Let_def; |
85 theorems [split] = option.split; |
85 lemmas [split] = option.split; |
86 |
86 |
87 text{*\noindent |
87 text{*\noindent |
88 The reason becomes clear when looking (probably after a failed proof |
88 The reason becomes clear when looking (probably after a failed proof |
89 attempt) at the body of \isa{update}: it contains both |
89 attempt) at the body of \isa{update}: it contains both |
90 \isa{let} and a case distinction over type \isa{option}. |
90 \isa{let} and a case distinction over type \isa{option}. |
103 guided by the intuition that simplification of \isa{lookup} might be easier |
103 guided by the intuition that simplification of \isa{lookup} might be easier |
104 if \isa{update} has already been simplified, which can only happen if |
104 if \isa{update} has already been simplified, which can only happen if |
105 \isa{as} is instantiated. |
105 \isa{as} is instantiated. |
106 The start of the proof is completely conventional: |
106 The start of the proof is completely conventional: |
107 *}; |
107 *}; |
108 |
|
109 apply(induct_tac as, auto); |
108 apply(induct_tac as, auto); |
110 |
109 |
111 txt{*\noindent |
110 txt{*\noindent |
112 Unfortunately, this time we are left with three intimidating looking subgoals: |
111 Unfortunately, this time we are left with three intimidating looking subgoals: |
113 \begin{isabellepar}% |
112 \begin{isabellepar}% |
117 \end{isabellepar}% |
116 \end{isabellepar}% |
118 Clearly, if we want to make headway we have to instantiate \isa{bs} as |
117 Clearly, if we want to make headway we have to instantiate \isa{bs} as |
119 well now. It turns out that instead of induction, case distinction |
118 well now. It turns out that instead of induction, case distinction |
120 suffices: |
119 suffices: |
121 *}; |
120 *}; |
122 |
121 by(case_tac[!] bs, auto); |
123 apply(case_tac[!] bs); |
|
124 by(auto); |
|
125 |
122 |
126 text{*\noindent |
123 text{*\noindent |
127 Both \isaindex{case_tac} and \isaindex{induct_tac} |
124 All methods ending in \isa{tac} take an optional first argument that |
128 take an optional first argument that specifies the range of subgoals they are |
125 specifies the range of subgoals they are applied to, where \isa{[!]} means all |
129 applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual |
126 subgoals, i.e.\ \isa{[1-3]} in our case. Individual subgoal numbers, |
130 subgoal numbers are also allowed. |
127 e.g. \isa{[2]} are also allowed. |
131 |
128 |
132 This proof may look surprisingly straightforward. However, note that this |
129 This proof may look surprisingly straightforward. However, note that this |
133 comes at a cost: the proof script is unreadable because the |
130 comes at a cost: the proof script is unreadable because the |
134 intermediate proof states are invisible, and we rely on the (possibly |
131 intermediate proof states are invisible, and we rely on the (possibly |
135 brittle) magic of \isa{auto} (after the induction) to split the remaining |
132 brittle) magic of \isa{auto} (after the induction) to split the remaining |