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