1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Nested{\isadigit{2}}}% |
3 \def\isabellecontext{Nested{\isadigit{2}}}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
4 \isanewline |
15 \isanewline |
|
16 % |
|
17 \endisadelimtheory |
5 \isamarkupfalse% |
18 \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 |
19 \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 |
|
20 % |
|
21 \isadelimproof |
|
22 % |
|
23 \endisadelimproof |
|
24 % |
|
25 \isatagproof |
7 \isamarkupfalse% |
26 \isamarkupfalse% |
8 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% |
27 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}% |
9 \isamarkupfalse% |
28 \endisatagproof |
|
29 {\isafoldproof}% |
|
30 % |
|
31 \isadelimproof |
|
32 % |
|
33 \endisadelimproof |
|
34 \isamarkuptrue% |
10 % |
35 % |
11 \begin{isamarkuptext}% |
36 \begin{isamarkuptext}% |
12 \noindent |
37 \noindent |
13 By making this theorem a simplification rule, \isacommand{recdef} |
38 By making this theorem a simplification rule, \isacommand{recdef} |
14 applies it automatically and the definition of \isa{trev} |
39 applies it automatically and the definition of \isa{trev} |
15 succeeds now. As a reward for our effort, we can now prove the desired |
40 succeeds now. As a reward for our effort, we can now prove the desired |
16 lemma directly. We no longer need the verbose |
41 lemma directly. We no longer need the verbose |
17 induction schema for type \isa{term} and can use the simpler one arising from |
42 induction schema for type \isa{term} and can use the simpler one arising from |
18 \isa{trev}:% |
43 \isa{trev}:% |
19 \end{isamarkuptext}% |
44 \end{isamarkuptext}% |
20 \isamarkuptrue% |
45 \isamarkupfalse% |
21 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline |
46 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline |
|
47 % |
|
48 \isadelimproof |
|
49 % |
|
50 \endisadelimproof |
|
51 % |
|
52 \isatagproof |
22 \isamarkupfalse% |
53 \isamarkupfalse% |
23 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}\ trev{\isachardot}induct{\isacharparenright}\isamarkupfalse% |
54 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}\ trev{\isachardot}induct{\isacharparenright}\isamarkuptrue% |
24 % |
55 % |
25 \begin{isamarkuptxt}% |
56 \begin{isamarkuptxt}% |
26 \begin{isabelle}% |
57 \begin{isabelle}% |
27 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x\isanewline |
58 \ {\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 |
59 \ {\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 |
60 \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% |
61 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts% |
31 \end{isabelle} |
62 \end{isabelle} |
32 Both the base case and the induction step fall to simplification:% |
63 Both the base case and the induction step fall to simplification:% |
33 \end{isamarkuptxt}% |
64 \end{isamarkuptxt}% |
|
65 \isamarkupfalse% |
|
66 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}% |
|
67 \endisatagproof |
|
68 {\isafoldproof}% |
|
69 % |
|
70 \isadelimproof |
|
71 % |
|
72 \endisadelimproof |
34 \isamarkuptrue% |
73 \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% |
|
36 % |
74 % |
37 \begin{isamarkuptext}% |
75 \begin{isamarkuptext}% |
38 \noindent |
76 \noindent |
39 If the proof of the induction step mystifies you, we recommend that you go through |
77 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 |
78 the chain of simplification steps in detail; you will probably need the help of |
74 rules for other higher-order functions on lists are similar. If you get |
112 rules for other higher-order functions on lists are similar. If you get |
75 into a situation where you need to supply \isacommand{recdef} with new |
113 into a situation where you need to supply \isacommand{recdef} with new |
76 congruence rules, you can append a hint after the end of |
114 congruence rules, you can append a hint after the end of |
77 the recursion equations:\cmmdx{hints}% |
115 the recursion equations:\cmmdx{hints}% |
78 \end{isamarkuptext}% |
116 \end{isamarkuptext}% |
79 \isamarkuptrue% |
117 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkuptrue% |
80 \isamarkupfalse% |
|
81 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse% |
|
82 % |
118 % |
83 \begin{isamarkuptext}% |
119 \begin{isamarkuptext}% |
84 \noindent |
120 \noindent |
85 Or you can declare them globally |
121 Or you can declare them globally |
86 by giving them the \attrdx{recdef_cong} attribute:% |
122 by giving them the \attrdx{recdef_cong} attribute:% |
87 \end{isamarkuptext}% |
123 \end{isamarkuptext}% |
88 \isamarkuptrue% |
124 \isamarkupfalse% |
89 \isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}\isamarkupfalse% |
125 \isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}\isamarkuptrue% |
90 % |
126 % |
91 \begin{isamarkuptext}% |
127 \begin{isamarkuptext}% |
92 The \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are |
128 The \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are |
93 intentionally kept apart because they control different activities, namely |
129 intentionally kept apart because they control different activities, namely |
94 simplification and making recursive definitions. |
130 simplification and making recursive definitions. |
95 %The simplifier's congruence rules cannot be used by recdef. |
131 %The simplifier's congruence rules cannot be used by recdef. |
96 %For example the weak congruence rules for if and case would prevent |
132 %For example the weak congruence rules for if and case would prevent |
97 %recdef from generating sensible termination conditions.% |
133 %recdef from generating sensible termination conditions.% |
98 \end{isamarkuptext}% |
134 \end{isamarkuptext}% |
99 \isamarkuptrue% |
135 % |
100 \isamarkupfalse% |
136 \isadelimtheory |
|
137 % |
|
138 \endisadelimtheory |
|
139 % |
|
140 \isatagtheory |
|
141 % |
|
142 \endisatagtheory |
|
143 {\isafoldtheory}% |
|
144 % |
|
145 \isadelimtheory |
|
146 % |
|
147 \endisadelimtheory |
101 \end{isabellebody}% |
148 \end{isabellebody}% |
102 %%% Local Variables: |
149 %%% Local Variables: |
103 %%% mode: latex |
150 %%% mode: latex |
104 %%% TeX-master: "root" |
151 %%% TeX-master: "root" |
105 %%% End: |
152 %%% End: |