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