1.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Sun Oct 21 19:48:19 2001 +0200
1.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Sun Oct 21 19:49:29 2001 +0200
1.3 @@ -5,19 +5,27 @@
1.4 \isacommand{theory}\ Advanced\ {\isacharequal}\ Even{\isacharcolon}\isanewline
1.5 \isanewline
1.6 \isanewline
1.7 +\isamarkupfalse%
1.8 \isacommand{datatype}\ {\isacharprime}f\ gterm\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequote}{\isacharprime}f\ gterm\ list{\isachardoublequote}\isanewline
1.9 \isanewline
1.10 +\isamarkupfalse%
1.11 \isacommand{datatype}\ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus\isanewline
1.12 \isanewline
1.13 +\isamarkupfalse%
1.14 \isacommand{consts}\ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
1.15 +\isamarkupfalse%
1.16 \isacommand{inductive}\ {\isachardoublequote}gterms\ F{\isachardoublequote}\isanewline
1.17 \isakeyword{intros}\isanewline
1.18 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
1.19 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequote}\isanewline
1.20 \isanewline
1.21 +\isamarkupfalse%
1.22 \isacommand{lemma}\ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequote}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequote}\isanewline
1.23 +\isamarkupfalse%
1.24 \isacommand{apply}\ clarify\isanewline
1.25 -\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}%
1.26 +\isamarkupfalse%
1.27 +\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isamarkupfalse%
1.28 +%
1.29 \begin{isamarkuptxt}%
1.30 \begin{isabelle}%
1.31 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
1.32 @@ -25,8 +33,11 @@
1.33 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G%
1.34 \end{isabelle}%
1.35 \end{isamarkuptxt}%
1.36 +\isamarkuptrue%
1.37 \isacommand{apply}\ blast\isanewline
1.38 -\isacommand{done}%
1.39 +\isamarkupfalse%
1.40 +\isacommand{done}\isamarkupfalse%
1.41 +%
1.42 \begin{isamarkuptext}%
1.43 \begin{isabelle}%
1.44 \ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
1.45 @@ -37,10 +48,13 @@
1.46 the two forms that Markus has made available. First the one for binding the
1.47 result to a name%
1.48 \end{isamarkuptext}%
1.49 +\isamarkuptrue%
1.50 \isacommand{inductive{\isacharunderscore}cases}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline
1.51 \ \ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}\isanewline
1.52 \isanewline
1.53 -\isacommand{thm}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases%
1.54 +\isamarkupfalse%
1.55 +\isacommand{thm}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\isamarkupfalse%
1.56 +%
1.57 \begin{isamarkuptext}%
1.58 \begin{isabelle}%
1.59 \ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
1.60 @@ -49,11 +63,16 @@
1.61
1.62 and now the one for local usage:%
1.63 \end{isamarkuptext}%
1.64 +\isamarkuptrue%
1.65 \isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
1.66 +\isamarkupfalse%
1.67 \isacommand{apply}\ {\isacharparenleft}ind{\isacharunderscore}cases\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}{\isacharparenright}\isanewline
1.68 +\isamarkupfalse%
1.69 \isacommand{oops}\isanewline
1.70 \isanewline
1.71 -\isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}%
1.72 +\isamarkupfalse%
1.73 +\isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}\isamarkupfalse%
1.74 +%
1.75 \begin{isamarkuptext}%
1.76 this is what we get:
1.77
1.78 @@ -62,9 +81,12 @@
1.79 \end{isabelle}
1.80 \rulename{gterm_Apply_elim}%
1.81 \end{isamarkuptext}%
1.82 +\isamarkuptrue%
1.83 \isacommand{lemma}\ gterms{\isacharunderscore}IntI\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline
1.84 \ \ \ \ \ {\isachardoublequote}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequote}\isanewline
1.85 -\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}%
1.86 +\isamarkupfalse%
1.87 +\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isamarkupfalse%
1.88 +%
1.89 \begin{isamarkuptxt}%
1.90 \begin{isabelle}%
1.91 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline
1.92 @@ -75,26 +97,35 @@
1.93 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}%
1.94 \end{isabelle}%
1.95 \end{isamarkuptxt}%
1.96 +\isamarkuptrue%
1.97 \isacommand{apply}\ blast\isanewline
1.98 -\isacommand{done}%
1.99 +\isamarkupfalse%
1.100 +\isacommand{done}\isamarkupfalse%
1.101 +%
1.102 \begin{isamarkuptext}%
1.103 \begin{isabelle}%
1.104 \ \ \ \ \ mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B%
1.105 \end{isabelle}
1.106 \rulename{mono_Int}%
1.107 \end{isamarkuptext}%
1.108 +\isamarkuptrue%
1.109 \isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
1.110 \ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline
1.111 +\isamarkupfalse%
1.112 \isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isanewline
1.113 \isanewline
1.114 \isanewline
1.115 +\isamarkupfalse%
1.116 \isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
1.117 +\isamarkupfalse%
1.118 \isacommand{primrec}\isanewline
1.119 {\isachardoublequote}integer{\isacharunderscore}arity\ {\isacharparenleft}Number\ n{\isacharparenright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
1.120 {\isachardoublequote}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
1.121 {\isachardoublequote}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{2}}{\isachardoublequote}\isanewline
1.122 \isanewline
1.123 +\isamarkupfalse%
1.124 \isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
1.125 +\isamarkupfalse%
1.126 \isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
1.127 \isakeyword{intros}\isanewline
1.128 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline
1.129 @@ -102,7 +133,9 @@
1.130 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
1.131 \isanewline
1.132 \isanewline
1.133 +\isamarkupfalse%
1.134 \isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
1.135 +\isamarkupfalse%
1.136 \isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
1.137 \isakeyword{intros}\isanewline
1.138 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline
1.139 @@ -110,8 +143,11 @@
1.140 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
1.141 \isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline
1.142 \isanewline
1.143 +\isamarkupfalse%
1.144 \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
1.145 -\isacommand{apply}\ clarify%
1.146 +\isamarkupfalse%
1.147 +\isacommand{apply}\ clarify\isamarkupfalse%
1.148 +%
1.149 \begin{isamarkuptxt}%
1.150 The situation after clarify
1.151 \begin{isabelle}%
1.152 @@ -119,7 +155,9 @@
1.153 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
1.154 \end{isabelle}%
1.155 \end{isamarkuptxt}%
1.156 -\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}%
1.157 +\isamarkuptrue%
1.158 +\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isamarkupfalse%
1.159 +%
1.160 \begin{isamarkuptxt}%
1.161 note the induction hypothesis!
1.162 \begin{isabelle}%
1.163 @@ -131,13 +169,18 @@
1.164 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
1.165 \end{isabelle}%
1.166 \end{isamarkuptxt}%
1.167 +\isamarkuptrue%
1.168 \isacommand{apply}\ auto\isanewline
1.169 +\isamarkupfalse%
1.170 \isacommand{done}\isanewline
1.171 \isanewline
1.172 \isanewline
1.173 \isanewline
1.174 +\isamarkupfalse%
1.175 \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
1.176 -\isacommand{apply}\ clarify%
1.177 +\isamarkupfalse%
1.178 +\isacommand{apply}\ clarify\isamarkupfalse%
1.179 +%
1.180 \begin{isamarkuptxt}%
1.181 The situation after clarify
1.182 \begin{isabelle}%
1.183 @@ -145,7 +188,9 @@
1.184 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
1.185 \end{isabelle}%
1.186 \end{isamarkuptxt}%
1.187 -\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}%
1.188 +\isamarkuptrue%
1.189 +\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isamarkupfalse%
1.190 +%
1.191 \begin{isamarkuptxt}%
1.192 note the induction hypothesis!
1.193 \begin{isabelle}%
1.194 @@ -158,18 +203,24 @@
1.195 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
1.196 \end{isabelle}%
1.197 \end{isamarkuptxt}%
1.198 +\isamarkuptrue%
1.199 \isacommand{apply}\ auto\isanewline
1.200 -\isacommand{done}%
1.201 +\isamarkupfalse%
1.202 +\isacommand{done}\isamarkupfalse%
1.203 +%
1.204 \begin{isamarkuptext}%
1.205 \begin{isabelle}%
1.206 \ \ \ \ \ lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B%
1.207 \end{isabelle}%
1.208 \end{isamarkuptext}%
1.209 +\isamarkuptrue%
1.210 %
1.211 \begin{isamarkuptext}%
1.212 the rest isn't used: too complicated. OK for an exercise though.%
1.213 \end{isamarkuptext}%
1.214 +\isamarkuptrue%
1.215 \isacommand{consts}\ integer{\isacharunderscore}signature\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}integer{\isacharunderscore}op\ {\isacharasterisk}\ {\isacharparenleft}unit\ list\ {\isacharasterisk}\ unit{\isacharparenright}{\isacharparenright}\ set{\isachardoublequote}\isanewline
1.216 +\isamarkupfalse%
1.217 \isacommand{inductive}\ {\isachardoublequote}integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
1.218 \isakeyword{intros}\isanewline
1.219 Number{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isacharparenleft}Number\ n{\isacharcomma}\ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
1.220 @@ -177,7 +228,9 @@
1.221 Plus{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}Plus{\isacharcomma}\ \ \ \ \ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharcomma}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
1.222 \isanewline
1.223 \isanewline
1.224 +\isamarkupfalse%
1.225 \isacommand{consts}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequote}\isanewline
1.226 +\isamarkupfalse%
1.227 \isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
1.228 \isakeyword{intros}\isanewline
1.229 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline
1.230 @@ -186,7 +239,9 @@
1.231 \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline
1.232 \ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
1.233 \isanewline
1.234 +\isamarkupfalse%
1.235 \isacommand{consts}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequote}\isanewline
1.236 +\isamarkupfalse%
1.237 \isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
1.238 \isakeyword{intros}\isanewline
1.239 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline
1.240 @@ -197,21 +252,33 @@
1.241 \isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline
1.242 \isanewline
1.243 \isanewline
1.244 +\isamarkupfalse%
1.245 \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
1.246 +\isamarkupfalse%
1.247 \isacommand{apply}\ clarify\isanewline
1.248 +\isamarkupfalse%
1.249 \isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isanewline
1.250 +\isamarkupfalse%
1.251 \isacommand{apply}\ auto\isanewline
1.252 +\isamarkupfalse%
1.253 \isacommand{done}\isanewline
1.254 \isanewline
1.255 +\isamarkupfalse%
1.256 \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
1.257 +\isamarkupfalse%
1.258 \isacommand{apply}\ clarify\isanewline
1.259 +\isamarkupfalse%
1.260 \isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isanewline
1.261 +\isamarkupfalse%
1.262 \isacommand{apply}\ auto\isanewline
1.263 +\isamarkupfalse%
1.264 \isacommand{done}\isanewline
1.265 \isanewline
1.266 \isanewline
1.267 +\isamarkupfalse%
1.268 \isacommand{end}\isanewline
1.269 \isanewline
1.270 +\isamarkupfalse%
1.271 \end{isabellebody}%
1.272 %%% Local Variables:
1.273 %%% mode: latex