equal
deleted
inserted
replaced
52 \end{isamarkuptxt}% |
52 \end{isamarkuptxt}% |
53 \isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}% |
53 \isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}% |
54 \begin{isamarkuptext}% |
54 \begin{isamarkuptext}% |
55 \noindent |
55 \noindent |
56 This time, induction leaves us with the following base case |
56 This time, induction leaves us with the following base case |
|
57 %{goals[goals_limit=1,display]} |
57 \begin{isabelle} |
58 \begin{isabelle} |
58 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] |
59 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] |
59 \end{isabelle} |
60 \end{isabelle} |
60 which is trivial, and \isa{auto} finishes the whole proof. |
61 which is trivial, and \isa{auto} finishes the whole proof. |
61 |
62 |