equal
deleted
inserted
replaced
3 \def\isabellecontext{Nested{\isadigit{2}}}% |
3 \def\isabellecontext{Nested{\isadigit{2}}}% |
4 \isanewline |
4 \isanewline |
5 \isamarkupfalse% |
5 \isamarkupfalse% |
6 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline |
6 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline |
7 \isamarkupfalse% |
7 \isamarkupfalse% |
8 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% |
8 \isamarkupfalse% |
9 \isamarkupfalse% |
9 \isamarkupfalse% |
10 % |
10 % |
11 \begin{isamarkuptext}% |
11 \begin{isamarkuptext}% |
12 \noindent |
12 \noindent |
13 By making this theorem a simplification rule, \isacommand{recdef} |
13 By making this theorem a simplification rule, \isacommand{recdef} |
18 \isa{trev}:% |
18 \isa{trev}:% |
19 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |
20 \isamarkuptrue% |
20 \isamarkuptrue% |
21 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline |
21 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline |
22 \isamarkupfalse% |
22 \isamarkupfalse% |
23 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}\ trev{\isachardot}induct{\isacharparenright}\isamarkupfalse% |
23 \isamarkupfalse% |
24 % |
|
25 \begin{isamarkuptxt}% |
|
26 \begin{isabelle}% |
|
27 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x\isanewline |
|
28 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}f\ ts{\isachardot}\isanewline |
|
29 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymforall}x{\isachardot}\ x\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ x{\isacharparenright}\ {\isacharequal}\ x\ {\isasymLongrightarrow}\isanewline |
|
30 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts% |
|
31 \end{isabelle} |
|
32 Both the base case and the induction step fall to simplification:% |
|
33 \end{isamarkuptxt}% |
|
34 \isamarkuptrue% |
24 \isamarkuptrue% |
35 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse% |
25 \isamarkupfalse% |
36 % |
26 % |
37 \begin{isamarkuptext}% |
27 \begin{isamarkuptext}% |
38 \noindent |
28 \noindent |
39 If the proof of the induction step mystifies you, we recommend that you go through |
29 If the proof of the induction step mystifies you, we recommend that you go through |
40 the chain of simplification steps in detail; you will probably need the help of |
30 the chain of simplification steps in detail; you will probably need the help of |