57 a name, @{text add_02}. Properties of recursively defined functions |
57 a name, @{text add_02}. Properties of recursively defined functions |
58 need to be established by induction in most cases. |
58 need to be established by induction in most cases. |
59 Command \isacom{apply}@{text"(induction m)"} instructs Isabelle to |
59 Command \isacom{apply}@{text"(induction m)"} instructs Isabelle to |
60 start a proof by induction on @{text m}. In response, it will show the |
60 start a proof by induction on @{text m}. In response, it will show the |
61 following proof state\ifsem\footnote{See page \pageref{proof-state} for how to |
61 following proof state\ifsem\footnote{See page \pageref{proof-state} for how to |
62 display the proof state}\fi: |
62 display the proof state.}\fi: |
63 @{subgoals[display,indent=0]} |
63 @{subgoals[display,indent=0]} |
64 The numbered lines are known as \emph{subgoals}. |
64 The numbered lines are known as \emph{subgoals}. |
65 The first subgoal is the base case, the second one the induction step. |
65 The first subgoal is the base case, the second one the induction step. |
66 The prefix @{text"\<And>m."} is Isabelle's way of saying ``for an arbitrary but fixed @{text m}''. The @{text"\<Longrightarrow>"} separates assumptions from the conclusion. |
66 The prefix @{text"\<And>m."} is Isabelle's way of saying ``for an arbitrary but fixed @{text m}''. The @{text"\<Longrightarrow>"} separates assumptions from the conclusion. |
67 The command \isacom{apply}@{text"(auto)"} instructs Isabelle to try |
67 The command \isacom{apply}@{text"(auto)"} instructs Isabelle to try |