author | wenzelm |
Mon, 29 Aug 2005 11:44:23 +0200 | |
changeset 17181 | 5f42dd5e6570 |
parent 17175 | 1eced27ee0e1 |
child 17187 | 45bee2f6e61f |
permissions | -rw-r--r-- |
10365 | 1 |
% |
11187 | 2 |
\begin{isabellebody}% |
3 |
\def\isabellecontext{Advanced}% |
|
17181 | 4 |
\isamarkupfalse% |
17056 | 5 |
% |
6 |
\isadelimtheory |
|
10365 | 7 |
\isanewline |
17056 | 8 |
% |
9 |
\endisadelimtheory |
|
10 |
% |
|
11 |
\isatagtheory |
|
17175 | 12 |
\isacommand{theory}\isamarkupfalse% |
13 |
\ Advanced\ \isakeyword{imports}\ Even\ \isakeyword{begin}% |
|
17056 | 14 |
\endisatagtheory |
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
\isanewline |
|
19 |
% |
|
20 |
\endisadelimtheory |
|
10469 | 21 |
\isanewline |
22 |
\isanewline |
|
17175 | 23 |
\isacommand{datatype}\isamarkupfalse% |
24 |
\ {\isacharprime}f\ gterm\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequoteopen}{\isacharprime}f\ gterm\ list{\isachardoublequoteclose}\isanewline |
|
10469 | 25 |
\isanewline |
17175 | 26 |
\isacommand{datatype}\isamarkupfalse% |
27 |
\ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus\isanewline |
|
10469 | 28 |
\isanewline |
17175 | 29 |
\isacommand{consts}\isamarkupfalse% |
30 |
\ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline |
|
31 |
\isacommand{inductive}\isamarkupfalse% |
|
32 |
\ {\isachardoublequoteopen}gterms\ F{\isachardoublequoteclose}\isanewline |
|
10469 | 33 |
\isakeyword{intros}\isanewline |
17175 | 34 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline |
35 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequoteclose}\isanewline |
|
10469 | 36 |
\isanewline |
17175 | 37 |
\isacommand{lemma}\isamarkupfalse% |
38 |
\ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequoteopen}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequoteclose}\isanewline |
|
17056 | 39 |
% |
40 |
\isadelimproof |
|
41 |
% |
|
42 |
\endisadelimproof |
|
43 |
% |
|
44 |
\isatagproof |
|
17175 | 45 |
\isacommand{apply}\isamarkupfalse% |
46 |
\ clarify\isanewline |
|
47 |
\isacommand{apply}\isamarkupfalse% |
|
48 |
\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}% |
|
16069 | 49 |
\begin{isamarkuptxt}% |
50 |
\begin{isabelle}% |
|
51 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline |
|
52 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline |
|
53 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G% |
|
54 |
\end{isabelle}% |
|
55 |
\end{isamarkuptxt}% |
|
17175 | 56 |
\isamarkuptrue% |
57 |
\isacommand{apply}\isamarkupfalse% |
|
58 |
\ blast\isanewline |
|
59 |
\isacommand{done}\isamarkupfalse% |
|
60 |
% |
|
17056 | 61 |
\endisatagproof |
62 |
{\isafoldproof}% |
|
63 |
% |
|
64 |
\isadelimproof |
|
65 |
% |
|
66 |
\endisadelimproof |
|
11866 | 67 |
% |
11187 | 68 |
\begin{isamarkuptext}% |
69 |
\begin{isabelle}% |
|
14470 | 70 |
\ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\isanewline |
71 |
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P% |
|
11173 | 72 |
\end{isabelle} |
73 |
\rulename{even.cases} |
|
10469 | 74 |
|
75 |
Just as a demo I include |
|
76 |
the two forms that Markus has made available. First the one for binding the |
|
77 |
result to a name% |
|
11187 | 78 |
\end{isamarkuptext}% |
17175 | 79 |
\isamarkuptrue% |
80 |
\isacommand{inductive{\isacharunderscore}cases}\isamarkupfalse% |
|
81 |
\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline |
|
82 |
\ \ {\isachardoublequoteopen}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline |
|
10365 | 83 |
\isanewline |
17175 | 84 |
\isacommand{thm}\isamarkupfalse% |
85 |
\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases% |
|
11187 | 86 |
\begin{isamarkuptext}% |
87 |
\begin{isabelle}% |
|
14470 | 88 |
\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% |
11187 | 89 |
\end{isabelle} |
11173 | 90 |
\rulename{Suc_Suc_cases} |
10469 | 91 |
|
10457 | 92 |
and now the one for local usage:% |
11187 | 93 |
\end{isamarkuptext}% |
17175 | 94 |
\isamarkuptrue% |
95 |
\isacommand{lemma}\isamarkupfalse% |
|
96 |
\ {\isachardoublequoteopen}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequoteclose}\isanewline |
|
17056 | 97 |
% |
98 |
\isadelimproof |
|
99 |
% |
|
100 |
\endisadelimproof |
|
101 |
% |
|
102 |
\isatagproof |
|
17175 | 103 |
\isacommand{apply}\isamarkupfalse% |
104 |
\ {\isacharparenleft}ind{\isacharunderscore}cases\ {\isachardoublequoteopen}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}{\isacharparenright}\isanewline |
|
105 |
\isacommand{oops}\isamarkupfalse% |
|
106 |
% |
|
17056 | 107 |
\endisatagproof |
108 |
{\isafoldproof}% |
|
109 |
% |
|
110 |
\isadelimproof |
|
111 |
\isanewline |
|
112 |
% |
|
113 |
\endisadelimproof |
|
15481 | 114 |
\isanewline |
17175 | 115 |
\isacommand{inductive{\isacharunderscore}cases}\isamarkupfalse% |
116 |
\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequoteclose}% |
|
11187 | 117 |
\begin{isamarkuptext}% |
10469 | 118 |
this is what we get: |
10457 | 119 |
|
11187 | 120 |
\begin{isabelle}% |
121 |
\ \ \ \ \ {\isasymlbrakk}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% |
|
10469 | 122 |
\end{isabelle} |
11187 | 123 |
\rulename{gterm_Apply_elim}% |
124 |
\end{isamarkuptext}% |
|
17175 | 125 |
\isamarkuptrue% |
126 |
\isacommand{lemma}\isamarkupfalse% |
|
127 |
\ gterms{\isacharunderscore}IntI\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline |
|
128 |
\ \ \ \ \ {\isachardoublequoteopen}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
17056 | 129 |
% |
130 |
\isadelimproof |
|
131 |
% |
|
132 |
\endisadelimproof |
|
133 |
% |
|
134 |
\isatagproof |
|
17175 | 135 |
\isacommand{apply}\isamarkupfalse% |
136 |
\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}% |
|
16069 | 137 |
\begin{isamarkuptxt}% |
138 |
\begin{isabelle}% |
|
139 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline |
|
140 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline |
|
141 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
|
142 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline |
|
143 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline |
|
144 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}% |
|
145 |
\end{isabelle}% |
|
146 |
\end{isamarkuptxt}% |
|
17175 | 147 |
\isamarkuptrue% |
148 |
\isacommand{apply}\isamarkupfalse% |
|
149 |
\ blast\isanewline |
|
150 |
\isacommand{done}\isamarkupfalse% |
|
151 |
% |
|
17056 | 152 |
\endisatagproof |
153 |
{\isafoldproof}% |
|
154 |
% |
|
155 |
\isadelimproof |
|
156 |
% |
|
157 |
\endisadelimproof |
|
11866 | 158 |
% |
11187 | 159 |
\begin{isamarkuptext}% |
160 |
\begin{isabelle}% |
|
161 |
\ \ \ \ \ mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B% |
|
11173 | 162 |
\end{isabelle} |
11187 | 163 |
\rulename{mono_Int}% |
164 |
\end{isamarkuptext}% |
|
17175 | 165 |
\isamarkuptrue% |
166 |
\isacommand{lemma}\isamarkupfalse% |
|
167 |
\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
|
168 |
\ \ \ \ \ {\isachardoublequoteopen}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequoteclose}\isanewline |
|
17056 | 169 |
% |
170 |
\isadelimproof |
|
171 |
% |
|
172 |
\endisadelimproof |
|
173 |
% |
|
174 |
\isatagproof |
|
17175 | 175 |
\isacommand{by}\isamarkupfalse% |
176 |
\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}% |
|
17056 | 177 |
\endisatagproof |
178 |
{\isafoldproof}% |
|
179 |
% |
|
180 |
\isadelimproof |
|
181 |
% |
|
182 |
\endisadelimproof |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11866
diff
changeset
|
183 |
% |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11866
diff
changeset
|
184 |
\begin{isamarkuptext}% |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11866
diff
changeset
|
185 |
the following declaration isn't actually used% |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11866
diff
changeset
|
186 |
\end{isamarkuptext}% |
17175 | 187 |
\isamarkuptrue% |
188 |
\isacommand{consts}\isamarkupfalse% |
|
189 |
\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline |
|
190 |
\isacommand{primrec}\isamarkupfalse% |
|
191 |
\isanewline |
|
192 |
{\isachardoublequoteopen}integer{\isacharunderscore}arity\ {\isacharparenleft}Number\ n{\isacharparenright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline |
|
193 |
{\isachardoublequoteopen}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline |
|
194 |
{\isachardoublequoteopen}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline |
|
10469 | 195 |
\isanewline |
17175 | 196 |
\isacommand{consts}\isamarkupfalse% |
197 |
\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline |
|
198 |
\isacommand{inductive}\isamarkupfalse% |
|
199 |
\ {\isachardoublequoteopen}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequoteclose}\isanewline |
|
10365 | 200 |
\isakeyword{intros}\isanewline |
17175 | 201 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline |
11187 | 202 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline |
17175 | 203 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequoteclose}\isanewline |
10365 | 204 |
\isanewline |
205 |
\isanewline |
|
17175 | 206 |
\isacommand{consts}\isamarkupfalse% |
207 |
\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline |
|
208 |
\isacommand{inductive}\isamarkupfalse% |
|
209 |
\ {\isachardoublequoteopen}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequoteclose}\isanewline |
|
10365 | 210 |
\isakeyword{intros}\isanewline |
17175 | 211 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline |
11187 | 212 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline |
17175 | 213 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequoteclose}\isanewline |
11187 | 214 |
\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline |
10469 | 215 |
\isanewline |
17175 | 216 |
\isacommand{lemma}\isamarkupfalse% |
217 |
\ {\isachardoublequoteopen}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequoteclose}\isanewline |
|
17056 | 218 |
% |
219 |
\isadelimproof |
|
220 |
% |
|
221 |
\endisadelimproof |
|
222 |
% |
|
223 |
\isatagproof |
|
17175 | 224 |
\isacommand{apply}\isamarkupfalse% |
225 |
\ clarify% |
|
16069 | 226 |
\begin{isamarkuptxt}% |
227 |
The situation after clarify |
|
228 |
\begin{isabelle}% |
|
229 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymLongrightarrow}\isanewline |
|
230 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% |
|
231 |
\end{isabelle}% |
|
232 |
\end{isamarkuptxt}% |
|
17175 | 233 |
\isamarkuptrue% |
234 |
\isacommand{apply}\isamarkupfalse% |
|
235 |
\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}% |
|
16069 | 236 |
\begin{isamarkuptxt}% |
237 |
note the induction hypothesis! |
|
238 |
\begin{isabelle}% |
|
239 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline |
|
240 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline |
|
241 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\isanewline |
|
242 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline |
|
243 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline |
|
244 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% |
|
245 |
\end{isabelle}% |
|
246 |
\end{isamarkuptxt}% |
|
17175 | 247 |
\isamarkuptrue% |
248 |
\isacommand{apply}\isamarkupfalse% |
|
249 |
\ auto\isanewline |
|
250 |
\isacommand{done}\isamarkupfalse% |
|
251 |
% |
|
17056 | 252 |
\endisatagproof |
253 |
{\isafoldproof}% |
|
254 |
% |
|
255 |
\isadelimproof |
|
256 |
\isanewline |
|
257 |
% |
|
258 |
\endisadelimproof |
|
15481 | 259 |
\isanewline |
10878 | 260 |
\isanewline |
261 |
\isanewline |
|
17175 | 262 |
\isacommand{lemma}\isamarkupfalse% |
263 |
\ {\isachardoublequoteopen}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequoteclose}\isanewline |
|
17056 | 264 |
% |
265 |
\isadelimproof |
|
266 |
% |
|
267 |
\endisadelimproof |
|
268 |
% |
|
269 |
\isatagproof |
|
17175 | 270 |
\isacommand{apply}\isamarkupfalse% |
271 |
\ clarify% |
|
16069 | 272 |
\begin{isamarkuptxt}% |
273 |
The situation after clarify |
|
274 |
\begin{isabelle}% |
|
275 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymLongrightarrow}\isanewline |
|
276 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% |
|
277 |
\end{isabelle}% |
|
278 |
\end{isamarkuptxt}% |
|
17175 | 279 |
\isamarkuptrue% |
280 |
\isacommand{apply}\isamarkupfalse% |
|
281 |
\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}% |
|
16069 | 282 |
\begin{isamarkuptxt}% |
283 |
note the induction hypothesis! |
|
284 |
\begin{isabelle}% |
|
285 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline |
|
286 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline |
|
287 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline |
|
288 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline |
|
289 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline |
|
290 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline |
|
291 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% |
|
292 |
\end{isabelle}% |
|
293 |
\end{isamarkuptxt}% |
|
17175 | 294 |
\isamarkuptrue% |
295 |
\isacommand{apply}\isamarkupfalse% |
|
296 |
\ auto\isanewline |
|
297 |
\isacommand{done}\isamarkupfalse% |
|
298 |
% |
|
17056 | 299 |
\endisatagproof |
300 |
{\isafoldproof}% |
|
301 |
% |
|
302 |
\isadelimproof |
|
303 |
% |
|
304 |
\endisadelimproof |
|
11866 | 305 |
% |
11187 | 306 |
\begin{isamarkuptext}% |
307 |
\begin{isabelle}% |
|
308 |
\ \ \ \ \ lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B% |
|
309 |
\end{isabelle}% |
|
310 |
\end{isamarkuptext}% |
|
11866 | 311 |
\isamarkuptrue% |
10469 | 312 |
% |
11187 | 313 |
\begin{isamarkuptext}% |
10469 | 314 |
the rest isn't used: too complicated. OK for an exercise though.% |
11187 | 315 |
\end{isamarkuptext}% |
17175 | 316 |
\isamarkuptrue% |
317 |
\isacommand{consts}\isamarkupfalse% |
|
318 |
\ integer{\isacharunderscore}signature\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}integer{\isacharunderscore}op\ {\isacharasterisk}\ {\isacharparenleft}unit\ list\ {\isacharasterisk}\ unit{\isacharparenright}{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline |
|
319 |
\isacommand{inductive}\isamarkupfalse% |
|
320 |
\ {\isachardoublequoteopen}integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline |
|
10365 | 321 |
\isakeyword{intros}\isanewline |
17175 | 322 |
Number{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}Number\ n{\isacharcomma}\ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline |
323 |
UnaryMinus{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}UnaryMinus{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline |
|
324 |
Plus{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}Plus{\isacharcomma}\ \ \ \ \ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharcomma}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline |
|
10469 | 325 |
\isanewline |
326 |
\isanewline |
|
17175 | 327 |
\isacommand{consts}\isamarkupfalse% |
328 |
\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequoteclose}\isanewline |
|
329 |
\isacommand{inductive}\isamarkupfalse% |
|
330 |
\ {\isachardoublequoteopen}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequoteclose}\isanewline |
|
10469 | 331 |
\isakeyword{intros}\isanewline |
11187 | 332 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline |
17175 | 333 |
\ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}pair\ {\isasymin}\ set\ args{\isachardot}\ pair\ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isacharsemicolon}\ \isanewline |
11187 | 334 |
\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline |
335 |
\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline |
|
17175 | 336 |
\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequoteclose}\isanewline |
10469 | 337 |
\isanewline |
17175 | 338 |
\isacommand{consts}\isamarkupfalse% |
339 |
\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequoteclose}\isanewline |
|
340 |
\isacommand{inductive}\isamarkupfalse% |
|
341 |
\ {\isachardoublequoteopen}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequoteclose}\isanewline |
|
10469 | 342 |
\isakeyword{intros}\isanewline |
11187 | 343 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline |
17175 | 344 |
\ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}args\ {\isasymin}\ lists{\isacharparenleft}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isacharparenright}{\isacharsemicolon}\ \isanewline |
11187 | 345 |
\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline |
346 |
\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline |
|
17175 | 347 |
\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequoteclose}\isanewline |
11187 | 348 |
\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline |
10365 | 349 |
\isanewline |
350 |
\isanewline |
|
17175 | 351 |
\isacommand{lemma}\isamarkupfalse% |
352 |
\ {\isachardoublequoteopen}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequoteclose}\isanewline |
|
17056 | 353 |
% |
354 |
\isadelimproof |
|
355 |
% |
|
356 |
\endisadelimproof |
|
357 |
% |
|
358 |
\isatagproof |
|
17175 | 359 |
\isacommand{apply}\isamarkupfalse% |
360 |
\ clarify\isanewline |
|
361 |
\isacommand{apply}\isamarkupfalse% |
|
362 |
\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isanewline |
|
363 |
\isacommand{apply}\isamarkupfalse% |
|
364 |
\ auto\isanewline |
|
365 |
\isacommand{done}\isamarkupfalse% |
|
366 |
% |
|
17056 | 367 |
\endisatagproof |
368 |
{\isafoldproof}% |
|
369 |
% |
|
370 |
\isadelimproof |
|
371 |
\isanewline |
|
372 |
% |
|
373 |
\endisadelimproof |
|
15481 | 374 |
\isanewline |
17175 | 375 |
\isacommand{lemma}\isamarkupfalse% |
376 |
\ {\isachardoublequoteopen}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequoteclose}\isanewline |
|
17056 | 377 |
% |
378 |
\isadelimproof |
|
379 |
% |
|
380 |
\endisadelimproof |
|
381 |
% |
|
382 |
\isatagproof |
|
17175 | 383 |
\isacommand{apply}\isamarkupfalse% |
384 |
\ clarify\isanewline |
|
385 |
\isacommand{apply}\isamarkupfalse% |
|
386 |
\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isanewline |
|
387 |
\isacommand{apply}\isamarkupfalse% |
|
388 |
\ auto\isanewline |
|
389 |
\isacommand{done}\isamarkupfalse% |
|
390 |
% |
|
17056 | 391 |
\endisatagproof |
392 |
{\isafoldproof}% |
|
393 |
% |
|
394 |
\isadelimproof |
|
15481 | 395 |
\isanewline |
17056 | 396 |
% |
397 |
\endisadelimproof |
|
10365 | 398 |
\isanewline |
17056 | 399 |
% |
400 |
\isadelimtheory |
|
401 |
\isanewline |
|
402 |
% |
|
403 |
\endisadelimtheory |
|
404 |
% |
|
405 |
\isatagtheory |
|
17175 | 406 |
\isacommand{end}\isamarkupfalse% |
407 |
% |
|
17056 | 408 |
\endisatagtheory |
409 |
{\isafoldtheory}% |
|
410 |
% |
|
411 |
\isadelimtheory |
|
10365 | 412 |
\isanewline |
17056 | 413 |
% |
414 |
\endisadelimtheory |
|
415 |
\isanewline |
|
11187 | 416 |
\end{isabellebody}% |
10365 | 417 |
%%% Local Variables: |
418 |
%%% mode: latex |
|
419 |
%%% TeX-master: "root" |
|
420 |
%%% End: |