equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Nested{\isadigit{2}}}% |
3 \def\isabellecontext{Nested{\isadigit{2}}}% |
|
4 \isanewline |
4 \isanewline |
5 \isanewline |
5 \isamarkupfalse% |
6 \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 |
7 \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% |
8 \isamarkupfalse% |
8 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% |
9 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% |
76 congruence rules, you can append a hint after the end of |
77 congruence rules, you can append a hint after the end of |
77 the recursion equations:\cmmdx{hints}% |
78 the recursion equations:\cmmdx{hints}% |
78 \end{isamarkuptext}% |
79 \end{isamarkuptext}% |
79 \isamarkuptrue% |
80 \isamarkuptrue% |
80 \isamarkupfalse% |
81 \isamarkupfalse% |
|
82 \isanewline |
81 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse% |
83 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse% |
82 % |
84 % |
83 \begin{isamarkuptext}% |
85 \begin{isamarkuptext}% |
84 \noindent |
86 \noindent |
85 Or you can declare them globally |
87 Or you can declare them globally |
95 %The simplifier's congruence rules cannot be used by recdef. |
97 %The simplifier's congruence rules cannot be used by recdef. |
96 %For example the weak congruence rules for if and case would prevent |
98 %For example the weak congruence rules for if and case would prevent |
97 %recdef from generating sensible termination conditions.% |
99 %recdef from generating sensible termination conditions.% |
98 \end{isamarkuptext}% |
100 \end{isamarkuptext}% |
99 \isamarkuptrue% |
101 \isamarkuptrue% |
|
102 \isanewline |
100 \isamarkupfalse% |
103 \isamarkupfalse% |
101 \end{isabellebody}% |
104 \end{isabellebody}% |
102 %%% Local Variables: |
105 %%% Local Variables: |
103 %%% mode: latex |
106 %%% mode: latex |
104 %%% TeX-master: "root" |
107 %%% TeX-master: "root" |