equal
deleted
inserted
replaced
363 definition |
363 definition |
364 EQ_TRUE |
364 EQ_TRUE |
365 where |
365 where |
366 "EQ_TRUE X \<equiv> (X = True)" |
366 "EQ_TRUE X \<equiv> (X = True)" |
367 |
367 |
368 lemma test: |
368 schematic_lemma test: |
369 shows "EQ_TRUE ?X" |
369 shows "EQ_TRUE ?X" |
370 unfolding EQ_TRUE_def |
370 unfolding EQ_TRUE_def |
371 by (rule refl) |
371 by (rule refl) |
372 |
372 |
373 text {* |
373 text {* |
374 Although Isabelle issues a warning message when stating goals involving |
374 By using \isacommand{schematic\_lemma} it is possible to prove lemmas including |
375 meta-variables, it is possible to prove this theorem. The reason for the warning |
375 meta-variables on the user level. However, the proved theorem is not @{text "EQ_TRUE ?X"}, |
376 message is that the proved theorem is not @{text "EQ_TRUE ?X"}, as one might |
376 as one might expect, but @{thm test}. We can test this with: |
377 expect, but @{thm test}. We can test this with: |
|
378 |
377 |
379 \begin{isabelle} |
378 \begin{isabelle} |
380 \isacommand{thm}~@{thm [source] test}\\ |
379 \isacommand{thm}~@{thm [source] test}\\ |
381 @{text ">"}~@{thm test} |
380 @{text ">"}~@{thm test} |
382 \end{isabelle} |
381 \end{isabelle} |
388 \begin{readmore} |
387 \begin{readmore} |
389 For more information about the internals of goals see \isccite{sec:tactical-goals}. |
388 For more information about the internals of goals see \isccite{sec:tactical-goals}. |
390 \end{readmore} |
389 \end{readmore} |
391 |
390 |
392 *} |
391 *} |
|
392 |
393 |
393 |
394 section {* Simple Tactics\label{sec:simpletacs} *} |
394 section {* Simple Tactics\label{sec:simpletacs} *} |
395 |
395 |
396 text {* |
396 text {* |
397 In this section we will introduce more of the simple tactics in Isabelle. The |
397 In this section we will introduce more of the simple tactics in Isabelle. The |
566 in Section~\ref{sec:printing} for extracting strings from @{ML_type cterm}s |
566 in Section~\ref{sec:printing} for extracting strings from @{ML_type cterm}s |
567 and @{ML_type thm}s.\label{fig:sptac}} |
567 and @{ML_type thm}s.\label{fig:sptac}} |
568 \end{figure} |
568 \end{figure} |
569 *} |
569 *} |
570 |
570 |
571 lemma |
571 schematic_lemma |
572 shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x" |
572 shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x" |
573 apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *}) |
573 apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *}) |
574 |
574 |
575 txt {* |
575 txt {* |
576 The tactic produces the following printout: |
576 The tactic produces the following printout: |