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