equal
deleted
inserted
replaced
62 \attrdx{rule_format} (\S\ref{sec:forward}) convert the |
62 \attrdx{rule_format} (\S\ref{sec:forward}) convert the |
63 result to the usual \isa{{\isasymLongrightarrow}} form:% |
63 result to the usual \isa{{\isasymLongrightarrow}} form:% |
64 \end{isamarkuptxt}% |
64 \end{isamarkuptxt}% |
65 \isamarkuptrue% |
65 \isamarkuptrue% |
66 \isamarkupfalse% |
66 \isamarkupfalse% |
67 \isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline |
67 \isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isamarkupfalse% |
68 \isamarkupfalse% |
|
69 \isamarkupfalse% |
68 \isamarkupfalse% |
70 % |
69 % |
71 \begin{isamarkuptxt}% |
70 \begin{isamarkuptxt}% |
72 \noindent |
71 \noindent |
73 This time, induction leaves us with a trivial base case: |
72 This time, induction leaves us with a trivial base case: |
245 \noindent |
244 \noindent |
246 The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. |
245 The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. |
247 We could have included this derivation in the original statement of the lemma:% |
246 We could have included this derivation in the original statement of the lemma:% |
248 \end{isamarkuptext}% |
247 \end{isamarkuptext}% |
249 \isamarkuptrue% |
248 \isamarkuptrue% |
250 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isanewline |
249 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isamarkupfalse% |
251 \isamarkupfalse% |
|
252 \isamarkupfalse% |
250 \isamarkupfalse% |
253 % |
251 % |
254 \begin{isamarkuptext}% |
252 \begin{isamarkuptext}% |
255 \begin{exercise} |
253 \begin{exercise} |
256 From the axiom and lemma for \isa{f}, show that \isa{f} is the |
254 From the axiom and lemma for \isa{f}, show that \isa{f} is the |