329 @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible |
329 @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible |
330 as an @{text #}). This wrapper prevents that premises of @{text C} are |
330 as an @{text #}). This wrapper prevents that premises of @{text C} are |
331 misinterpreted as open subgoals. While tactics can operate on the subgoals |
331 misinterpreted as open subgoals. While tactics can operate on the subgoals |
332 (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion |
332 (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion |
333 @{term C} intact, with the exception of possibly instantiating schematic |
333 @{term C} intact, with the exception of possibly instantiating schematic |
334 variables. If you use the predefined tactics, which we describe in the next |
334 variables. The instantiations of schematic variables can even be observed |
335 section, this will always be the case. |
335 on the user level. For this consider the following definition and proof. |
|
336 *} |
|
337 |
|
338 definition |
|
339 EQ_TRUE |
|
340 where |
|
341 "EQ_TRUE X \<equiv> (X = True)" |
|
342 |
|
343 lemma test: |
|
344 shows "EQ_TRUE ?X" |
|
345 unfolding EQ_TRUE_def |
|
346 by (rule refl) |
|
347 |
|
348 text {* |
|
349 Although Isabelle issues a warning message when stating goals involving |
|
350 meta-variables, it is possible to prove this theorem. The reason for the warning |
|
351 message is that the proved theorem is not @{text "EQ_TRUE ?X"}, as one might |
|
352 expect, but @{thm test}: |
|
353 |
|
354 \begin{isabelle} |
|
355 \isacommand{thm}~@{thm [source] test}\\ |
|
356 @{text ">"}~@{thm test} |
|
357 \end{isabelle} |
336 |
358 |
337 \begin{readmore} |
359 \begin{readmore} |
338 For more information about the internals of goals see \isccite{sec:tactical-goals}. |
360 For more information about the internals of goals see \isccite{sec:tactical-goals}. |
339 \end{readmore} |
361 \end{readmore} |
340 |
362 |