equal
deleted
inserted
replaced
137 @{const_typ card}\index{card@@{const card}} & is the cardinality of a finite set\\ |
137 @{const_typ card}\index{card@@{const card}} & is the cardinality of a finite set\\ |
138 & and is @{text 0} for all infinite sets\\ |
138 & and is @{text 0} for all infinite sets\\ |
139 @{thm image_def}\index{$IMP042@@{term"f ` A"}} & is the image of a function over a set |
139 @{thm image_def}\index{$IMP042@@{term"f ` A"}} & is the image of a function over a set |
140 \end{tabular} |
140 \end{tabular} |
141 \end{center} |
141 \end{center} |
142 See \cite{Nipkow-Main} for the wealth of further predefined functions in theory |
142 See @{cite "Nipkow-Main"} for the wealth of further predefined functions in theory |
143 @{theory Main}. |
143 @{theory Main}. |
144 |
144 |
145 |
145 |
146 \subsection*{Exercises} |
146 \subsection*{Exercises} |
147 |
147 |
397 \[ |
397 \[ |
398 \inferrule*[right=\mbox{@{text iffI}}]{\mbox{@{text"?P \<Longrightarrow> ?Q"}} \\ \mbox{@{text"?Q \<Longrightarrow> ?P"}}} |
398 \inferrule*[right=\mbox{@{text iffI}}]{\mbox{@{text"?P \<Longrightarrow> ?Q"}} \\ \mbox{@{text"?Q \<Longrightarrow> ?P"}}} |
399 {\mbox{@{text"?P = ?Q"}}} |
399 {\mbox{@{text"?P = ?Q"}}} |
400 \] |
400 \] |
401 These rules are part of the logical system of \concept{natural deduction} |
401 These rules are part of the logical system of \concept{natural deduction} |
402 (e.g., \cite{HuthRyan}). Although we intentionally de-emphasize the basic rules |
402 (e.g., @{cite HuthRyan}). Although we intentionally de-emphasize the basic rules |
403 of logic in favour of automatic proof methods that allow you to take bigger |
403 of logic in favour of automatic proof methods that allow you to take bigger |
404 steps, these rules are helpful in locating where and why automation fails. |
404 steps, these rules are helpful in locating where and why automation fails. |
405 When applied backwards, these rules decompose the goal: |
405 When applied backwards, these rules decompose the goal: |
406 \begin{itemize} |
406 \begin{itemize} |
407 \item @{thm[source] conjI} and @{thm[source]iffI} split the goal into two subgoals, |
407 \item @{thm[source] conjI} and @{thm[source]iffI} split the goal into two subgoals, |
484 |
484 |
485 %\subsection{Finding Theorems} |
485 %\subsection{Finding Theorems} |
486 % |
486 % |
487 %Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current |
487 %Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current |
488 %theory. Search criteria include pattern matching on terms and on names. |
488 %theory. Search criteria include pattern matching on terms and on names. |
489 %For details see the Isabelle/Isar Reference Manual~\cite{IsarRef}. |
489 %For details see the Isabelle/Isar Reference Manual~@{cite IsarRef}. |
490 %\bigskip |
490 %\bigskip |
491 |
491 |
492 \begin{warn} |
492 \begin{warn} |
493 To ease readability we will drop the question marks |
493 To ease readability we will drop the question marks |
494 in front of unknowns from now on. |
494 in front of unknowns from now on. |