65 The most obvious approach is the brute force expansion of \isa{split}:% |
65 The most obvious approach is the brute force expansion of \isa{split}:% |
66 \end{isamarkuptext}% |
66 \end{isamarkuptext}% |
67 \isamarkuptrue% |
67 \isamarkuptrue% |
68 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}x{\isacharparenright}\ p\ {\isacharequal}\ fst\ p{\isachardoublequote}\isanewline |
68 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}x{\isacharparenright}\ p\ {\isacharequal}\ fst\ p{\isachardoublequote}\isanewline |
69 \isamarkupfalse% |
69 \isamarkupfalse% |
70 \isamarkupfalse% |
70 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
71 % |
71 % |
72 \begin{isamarkuptext}% |
72 \begin{isamarkuptext}% |
73 This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the |
73 This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the |
74 proof, as it does above. But if it does not, you end up with exactly what |
74 proof, as it does above. But if it does not, you end up with exactly what |
75 we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this |
75 we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this |
88 \index{*split (method)}% |
88 \index{*split (method)}% |
89 \end{isamarkuptext}% |
89 \end{isamarkuptext}% |
90 \isamarkuptrue% |
90 \isamarkuptrue% |
91 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}y{\isacharparenright}\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline |
91 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}y{\isacharparenright}\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline |
92 \isamarkupfalse% |
92 \isamarkupfalse% |
93 \isamarkupfalse% |
93 \isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}split{\isacharparenright}\isamarkupfalse% |
94 \isamarkuptrue% |
94 % |
95 \isanewline |
95 \begin{isamarkuptxt}% |
96 \isamarkupfalse% |
96 \begin{isabelle}% |
97 \isamarkupfalse% |
97 \ {\isadigit{1}}{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymlongrightarrow}\ y\ {\isacharequal}\ snd\ p% |
98 \isamarkupfalse% |
98 \end{isabelle} |
|
99 This subgoal is easily proved by simplification. Thus we could have combined |
|
100 simplification and splitting in one command that proves the goal outright:% |
|
101 \end{isamarkuptxt}% |
|
102 \isamarkuptrue% |
|
103 \isamarkupfalse% |
|
104 \isamarkupfalse% |
|
105 \isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ split{\isacharunderscore}split{\isacharparenright}\isamarkupfalse% |
99 % |
106 % |
100 \begin{isamarkuptext}% |
107 \begin{isamarkuptext}% |
101 Let us look at a second example:% |
108 Let us look at a second example:% |
102 \end{isamarkuptext}% |
109 \end{isamarkuptext}% |
103 \isamarkuptrue% |
110 \isamarkuptrue% |
104 \isacommand{lemma}\ {\isachardoublequote}let\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ p\ in\ fst\ p\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
111 \isacommand{lemma}\ {\isachardoublequote}let\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ p\ in\ fst\ p\ {\isacharequal}\ x{\isachardoublequote}\isanewline |
105 \isamarkupfalse% |
112 \isamarkupfalse% |
106 \isamarkupfalse% |
113 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
|
114 % |
|
115 \begin{isamarkuptxt}% |
|
116 \begin{isabelle}% |
|
117 \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ fst\ p\ {\isacharequal}\ x{\isacharparenright}\ p% |
|
118 \end{isabelle} |
|
119 A paired \isa{let} reduces to a paired $\lambda$-abstraction, which |
|
120 can be split as above. The same is true for paired set comprehension:% |
|
121 \end{isamarkuptxt}% |
107 \isamarkuptrue% |
122 \isamarkuptrue% |
108 \isamarkupfalse% |
123 \isamarkupfalse% |
109 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline |
124 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline |
110 \isamarkupfalse% |
125 \isamarkupfalse% |
111 \isamarkupfalse% |
126 \isacommand{apply}\ simp\isamarkupfalse% |
|
127 % |
|
128 \begin{isamarkuptxt}% |
|
129 \begin{isabelle}% |
|
130 \ {\isadigit{1}}{\isachardot}\ split\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p% |
|
131 \end{isabelle} |
|
132 Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split} |
|
133 as above. If you are worried about the strange form of the premise: |
|
134 \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}. |
|
135 The same proof procedure works for% |
|
136 \end{isamarkuptxt}% |
112 \isamarkuptrue% |
137 \isamarkuptrue% |
113 \isamarkupfalse% |
138 \isamarkupfalse% |
114 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isamarkupfalse% |
139 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isamarkupfalse% |
|
140 % |
|
141 \begin{isamarkuptxt}% |
|
142 \noindent |
|
143 except that we now have to use \isa{split{\isacharunderscore}split{\isacharunderscore}asm}, because |
|
144 \isa{split} occurs in the assumptions. |
|
145 |
|
146 However, splitting \isa{split} is not always a solution, as no \isa{split} |
|
147 may be present in the goal. Consider the following function:% |
|
148 \end{isamarkuptxt}% |
115 \isamarkuptrue% |
149 \isamarkuptrue% |
116 \isamarkupfalse% |
150 \isamarkupfalse% |
117 \isacommand{consts}\ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequote}\isanewline |
151 \isacommand{consts}\ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequote}\isanewline |
118 \isamarkupfalse% |
152 \isamarkupfalse% |
119 \isacommand{primrec}\isanewline |
153 \isacommand{primrec}\isanewline |
124 Note that the above \isacommand{primrec} definition is admissible |
158 Note that the above \isacommand{primrec} definition is admissible |
125 because \isa{{\isasymtimes}} is a datatype. When we now try to prove% |
159 because \isa{{\isasymtimes}} is a datatype. When we now try to prove% |
126 \end{isamarkuptext}% |
160 \end{isamarkuptext}% |
127 \isamarkuptrue% |
161 \isamarkuptrue% |
128 \isacommand{lemma}\ {\isachardoublequote}swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p{\isachardoublequote}\isamarkupfalse% |
162 \isacommand{lemma}\ {\isachardoublequote}swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p{\isachardoublequote}\isamarkupfalse% |
129 \isamarkuptrue% |
163 % |
130 \isamarkupfalse% |
164 \begin{isamarkuptxt}% |
|
165 \noindent |
|
166 simplification will do nothing, because the defining equation for \isa{Pairs{\isachardot}swap} |
|
167 expects a pair. Again, we need to turn \isa{p} into a pair first, but this |
|
168 time there is no \isa{split} in sight. In this case the only thing we can do |
|
169 is to split the term by hand:% |
|
170 \end{isamarkuptxt}% |
|
171 \isamarkuptrue% |
|
172 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ p{\isacharparenright}\isamarkupfalse% |
|
173 % |
|
174 \begin{isamarkuptxt}% |
|
175 \noindent |
|
176 \begin{isabelle}% |
|
177 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ Pairs{\isachardot}swap\ {\isacharparenleft}Pairs{\isachardot}swap\ p{\isacharparenright}\ {\isacharequal}\ p% |
|
178 \end{isabelle} |
|
179 Again, \methdx{case_tac} is applicable because \isa{{\isasymtimes}} is a datatype. |
|
180 The subgoal is easily proved by \isa{simp}. |
|
181 |
|
182 Splitting by \isa{case{\isacharunderscore}tac} also solves the previous examples and may thus |
|
183 appear preferable to the more arcane methods introduced first. However, see |
|
184 the warning about \isa{case{\isacharunderscore}tac} in \S\ref{sec:struct-ind-case}. |
|
185 |
|
186 In case the term to be split is a quantified variable, there are more options. |
|
187 You can split \emph{all} \isa{{\isasymAnd}}-quantified variables in a goal |
|
188 with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:% |
|
189 \end{isamarkuptxt}% |
131 \isamarkuptrue% |
190 \isamarkuptrue% |
132 \isamarkupfalse% |
191 \isamarkupfalse% |
133 \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline |
192 \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline |
134 \isamarkupfalse% |
193 \isamarkupfalse% |
135 \isamarkupfalse% |
194 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% |
136 \isamarkuptrue% |
195 % |
137 \isamarkupfalse% |
196 \begin{isamarkuptxt}% |
138 \isamarkupfalse% |
197 \noindent |
|
198 \begin{isabelle}% |
|
199 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\isanewline |
|
200 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Pairs{\isachardot}swap\ {\isacharparenleft}Pairs{\isachardot}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\isanewline |
|
201 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}% |
|
202 \end{isabelle}% |
|
203 \end{isamarkuptxt}% |
|
204 \isamarkuptrue% |
|
205 \isacommand{apply}\ simp\isanewline |
|
206 \isamarkupfalse% |
|
207 \isacommand{done}\isamarkupfalse% |
139 % |
208 % |
140 \begin{isamarkuptext}% |
209 \begin{isamarkuptext}% |
141 \noindent |
210 \noindent |
142 Note that we have intentionally included only \isa{split{\isacharunderscore}paired{\isacharunderscore}all} |
211 Note that we have intentionally included only \isa{split{\isacharunderscore}paired{\isacharunderscore}all} |
143 in the first simplification step, and then we simplify again. |
212 in the first simplification step, and then we simplify again. |
148 The following command could fail (here it does not) |
217 The following command could fail (here it does not) |
149 where two separate \isa{simp} applications succeed.% |
218 where two separate \isa{simp} applications succeed.% |
150 \end{isamarkuptext}% |
219 \end{isamarkuptext}% |
151 \isamarkuptrue% |
220 \isamarkuptrue% |
152 \isamarkupfalse% |
221 \isamarkupfalse% |
153 \isamarkupfalse% |
222 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% |
154 \isamarkupfalse% |
223 \isamarkupfalse% |
155 % |
224 % |
156 \begin{isamarkuptext}% |
225 \begin{isamarkuptext}% |
157 \noindent |
226 \noindent |
158 Finally, the simplifier automatically splits all \isa{{\isasymforall}} and |
227 Finally, the simplifier automatically splits all \isa{{\isasymforall}} and |
159 \isa{{\isasymexists}}-quantified variables:% |
228 \isa{{\isasymexists}}-quantified variables:% |
160 \end{isamarkuptext}% |
229 \end{isamarkuptext}% |
161 \isamarkuptrue% |
230 \isamarkuptrue% |
162 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}p{\isachardot}\ {\isasymexists}q{\isachardot}\ swap\ p\ {\isacharequal}\ swap\ q{\isachardoublequote}\isanewline |
231 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}p{\isachardot}\ {\isasymexists}q{\isachardot}\ swap\ p\ {\isacharequal}\ swap\ q{\isachardoublequote}\isanewline |
163 \isamarkupfalse% |
232 \isamarkupfalse% |
164 \isamarkupfalse% |
233 \isacommand{by}\ simp\isamarkupfalse% |
165 % |
234 % |
166 \begin{isamarkuptext}% |
235 \begin{isamarkuptext}% |
167 \noindent |
236 \noindent |
168 To turn off this automatic splitting, just disable the |
237 To turn off this automatic splitting, just disable the |
169 responsible simplification rules: |
238 responsible simplification rules: |