equal
deleted
inserted
replaced
41 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ {\isachardoublequote}T{\isachardoublequote}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% |
41 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ {\isachardoublequote}T{\isachardoublequote}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% |
42 \begin{isamarkuptext}% |
42 \begin{isamarkuptext}% |
43 \noindent |
43 \noindent |
44 but it is worth taking a look at the proof state after the induction step |
44 but it is worth taking a look at the proof state after the induction step |
45 to understand what the presence of the function type entails: |
45 to understand what the presence of the function type entails: |
46 \begin{isabellepar}% |
46 \begin{isabelle} |
47 ~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline |
47 ~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline |
48 ~2.~{\isasymAnd}a~F.\isanewline |
48 ~2.~{\isasymAnd}a~F.\isanewline |
49 ~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline |
49 ~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline |
50 ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)% |
50 ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)% |
51 \end{isabellepar}%% |
51 \end{isabelle}% |
52 \end{isamarkuptext}% |
52 \end{isamarkuptext}% |
53 \end{isabellebody}% |
53 \end{isabellebody}% |
54 %%% Local Variables: |
54 %%% Local Variables: |
55 %%% mode: latex |
55 %%% mode: latex |
56 %%% TeX-master: "root" |
56 %%% TeX-master: "root" |