equal
deleted
inserted
replaced
89 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}% |
89 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}% |
90 \begin{isamarkuptxt}% |
90 \begin{isamarkuptxt}% |
91 \noindent |
91 \noindent |
92 The resulting 8 goals (one for each constructor) are proved in one fell swoop:% |
92 The resulting 8 goals (one for each constructor) are proved in one fell swoop:% |
93 \end{isamarkuptxt}% |
93 \end{isamarkuptxt}% |
94 \isacommand{by}\ simp\_all% |
94 \isacommand{by}\ simp{\isacharunderscore}all% |
95 \begin{isamarkuptext}% |
95 \begin{isamarkuptext}% |
96 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
96 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
97 an inductive proof expects a goal of the form |
97 an inductive proof expects a goal of the form |
98 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
98 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
99 where each variable $x@i$ is of type $\tau@i$. Induction is started by |
99 where each variable $x@i$ is of type $\tau@i$. Induction is started by |