doc-src/TutorialI/Inductive/document/Advanced.tex
author paulson
Mon, 12 Nov 2001 10:56:38 +0100
changeset 12156 d2758965362e
parent 11866 fbd097aec213
child 14379 ea10a8c3e9cf
permissions -rw-r--r--
new-style numerals without leading #, along with generic 0 and 1
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
     1
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
     2
\begin{isabellebody}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
     3
\def\isabellecontext{Advanced}%
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
     4
\isanewline
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
     5
\isacommand{theory}\ Advanced\ {\isacharequal}\ Even{\isacharcolon}\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
     6
\isanewline
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
     7
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
     8
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
     9
\isacommand{datatype}\ {\isacharprime}f\ gterm\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequote}{\isacharprime}f\ gterm\ list{\isachardoublequote}\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    10
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    11
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    12
\isacommand{datatype}\ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    13
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    14
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    15
\isacommand{consts}\ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    16
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    17
\isacommand{inductive}\ {\isachardoublequote}gterms\ F{\isachardoublequote}\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    18
\isakeyword{intros}\isanewline
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    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
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    20
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequote}\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    21
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    22
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    23
\isacommand{lemma}\ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequote}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    24
\isamarkupfalse%
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    25
\isacommand{apply}\ clarify\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    26
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    27
\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    28
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    29
\begin{isamarkuptxt}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    30
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    31
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    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
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    33
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    34
\end{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    35
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    36
\isamarkuptrue%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    37
\isacommand{apply}\ blast\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    38
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    39
\isacommand{done}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    40
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    41
\begin{isamarkuptext}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    42
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    43
\ \ \ \ \ {\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%
11173
094b76968484 revisions in response to comments by Tobias
paulson
parents: 10950
diff changeset
    44
\end{isabelle}
094b76968484 revisions in response to comments by Tobias
paulson
parents: 10950
diff changeset
    45
\rulename{even.cases}
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    46
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    47
Just as a demo I include
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    48
the two forms that Markus has made available. First the one for binding the
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    49
result to a name%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    50
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    51
\isamarkuptrue%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    52
\isacommand{inductive{\isacharunderscore}cases}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    53
\ \ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}\isanewline
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
    54
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    55
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    56
\isacommand{thm}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    57
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    58
\begin{isamarkuptext}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    59
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    60
\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    61
\end{isabelle}
11173
094b76968484 revisions in response to comments by Tobias
paulson
parents: 10950
diff changeset
    62
\rulename{Suc_Suc_cases}
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    63
10457
dd669bda2b0c updated;
wenzelm
parents: 10365
diff changeset
    64
and now the one for local usage:%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    65
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    66
\isamarkuptrue%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    67
\isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    68
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    69
\isacommand{apply}\ {\isacharparenleft}ind{\isacharunderscore}cases\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}{\isacharparenright}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    70
\isamarkupfalse%
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    71
\isacommand{oops}\isanewline
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    72
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    73
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    74
\isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    75
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    76
\begin{isamarkuptext}%
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    77
this is what we get:
10457
dd669bda2b0c updated;
wenzelm
parents: 10365
diff changeset
    78
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    79
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    80
\ \ \ \ \ {\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
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
    81
\end{isabelle}
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    82
\rulename{gterm_Apply_elim}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    83
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    84
\isamarkuptrue%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    85
\isacommand{lemma}\ gterms{\isacharunderscore}IntI\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    86
\ \ \ \ \ {\isachardoublequote}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    87
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    88
\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    89
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    90
\begin{isamarkuptxt}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    91
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    92
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    93
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    94
\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
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    95
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    96
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    97
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    98
\end{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
    99
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   100
\isamarkuptrue%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   101
\isacommand{apply}\ blast\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   102
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   103
\isacommand{done}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   104
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   105
\begin{isamarkuptext}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   106
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   107
\ \ \ \ \ mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B%
11173
094b76968484 revisions in response to comments by Tobias
paulson
parents: 10950
diff changeset
   108
\end{isabelle}
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   109
\rulename{mono_Int}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   110
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   111
\isamarkuptrue%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   112
\isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   113
\ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   114
\isamarkupfalse%
12156
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11866
diff changeset
   115
\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isamarkupfalse%
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11866
diff changeset
   116
%
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11866
diff changeset
   117
\begin{isamarkuptext}%
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11866
diff changeset
   118
the following declaration isn't actually used%
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11866
diff changeset
   119
\end{isamarkuptext}%
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11866
diff changeset
   120
\isamarkuptrue%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   121
\isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   122
\isamarkupfalse%
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   123
\isacommand{primrec}\isanewline
11708
d27253c4594f *** empty log message ***
wenzelm
parents: 11187
diff changeset
   124
{\isachardoublequote}integer{\isacharunderscore}arity\ {\isacharparenleft}Number\ n{\isacharparenright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
d27253c4594f *** empty log message ***
wenzelm
parents: 11187
diff changeset
   125
{\isachardoublequote}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
d27253c4594f *** empty log message ***
wenzelm
parents: 11187
diff changeset
   126
{\isachardoublequote}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{2}}{\isachardoublequote}\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   127
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   128
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   129
\isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   130
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   131
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   132
\isakeyword{intros}\isanewline
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   133
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   134
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   135
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   136
\isanewline
a17cf465d29a auto generated
paulson
parents:
diff changeset
   137
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   138
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   139
\isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   140
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   141
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   142
\isakeyword{intros}\isanewline
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   143
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   144
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   145
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   146
\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   147
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   148
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   149
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   150
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   151
\isacommand{apply}\ clarify\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   152
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   153
\begin{isamarkuptxt}%
10878
b254d5ad6dd4 auto update
paulson
parents: 10696
diff changeset
   154
The situation after clarify
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   155
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   156
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymLongrightarrow}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   157
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   158
\end{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   159
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   160
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   161
\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   162
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   163
\begin{isamarkuptxt}%
10878
b254d5ad6dd4 auto update
paulson
parents: 10696
diff changeset
   164
note the induction hypothesis!
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   165
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   166
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   167
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   168
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   169
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   170
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   171
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   172
\end{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   173
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   174
\isamarkuptrue%
10878
b254d5ad6dd4 auto update
paulson
parents: 10696
diff changeset
   175
\isacommand{apply}\ auto\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   176
\isamarkupfalse%
10878
b254d5ad6dd4 auto update
paulson
parents: 10696
diff changeset
   177
\isacommand{done}\isanewline
b254d5ad6dd4 auto update
paulson
parents: 10696
diff changeset
   178
\isanewline
b254d5ad6dd4 auto update
paulson
parents: 10696
diff changeset
   179
\isanewline
b254d5ad6dd4 auto update
paulson
parents: 10696
diff changeset
   180
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   181
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   182
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   183
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   184
\isacommand{apply}\ clarify\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   185
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   186
\begin{isamarkuptxt}%
10878
b254d5ad6dd4 auto update
paulson
parents: 10696
diff changeset
   187
The situation after clarify
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   188
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   189
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymLongrightarrow}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   190
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   191
\end{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   192
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   193
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   194
\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   195
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   196
\begin{isamarkuptxt}%
10878
b254d5ad6dd4 auto update
paulson
parents: 10696
diff changeset
   197
note the induction hypothesis!
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   198
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   199
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   200
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   201
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   202
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   203
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   204
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   205
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   206
\end{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   207
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   208
\isamarkuptrue%
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   209
\isacommand{apply}\ auto\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   210
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   211
\isacommand{done}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   212
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   213
\begin{isamarkuptext}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   214
\begin{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   215
\ \ \ \ \ lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   216
\end{isabelle}%
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   217
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   218
\isamarkuptrue%
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   219
%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   220
\begin{isamarkuptext}%
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   221
the rest isn't used: too complicated.  OK for an exercise though.%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   222
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   223
\isamarkuptrue%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   224
\isacommand{consts}\ integer{\isacharunderscore}signature\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}integer{\isacharunderscore}op\ {\isacharasterisk}\ {\isacharparenleft}unit\ list\ {\isacharasterisk}\ unit{\isacharparenright}{\isacharparenright}\ set{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   225
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   226
\isacommand{inductive}\ {\isachardoublequote}integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   227
\isakeyword{intros}\isanewline
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   228
Number{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isacharparenleft}Number\ n{\isacharcomma}\ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   229
UnaryMinus{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}UnaryMinus{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   230
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
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   231
\isanewline
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   232
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   233
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   234
\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
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   235
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   236
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   237
\isakeyword{intros}\isanewline
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   238
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   239
\ \ \ \ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}pair\ {\isasymin}\ set\ args{\isachardot}\ pair\ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isacharsemicolon}\ \isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   240
\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   241
\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   242
\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   243
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   244
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   245
\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
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   246
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   247
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   248
\isakeyword{intros}\isanewline
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   249
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   250
\ \ \ \ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists{\isacharparenleft}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isacharparenright}{\isacharsemicolon}\ \isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   251
\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   252
\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   253
\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   254
\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   255
\isanewline
a17cf465d29a auto generated
paulson
parents:
diff changeset
   256
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   257
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   258
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   259
\isamarkupfalse%
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   260
\isacommand{apply}\ clarify\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   261
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   262
\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   263
\isamarkupfalse%
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   264
\isacommand{apply}\ auto\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   265
\isamarkupfalse%
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   266
\isacommand{done}\isanewline
a17cf465d29a auto generated
paulson
parents:
diff changeset
   267
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   268
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   269
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   270
\isamarkupfalse%
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   271
\isacommand{apply}\ clarify\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   272
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   273
\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   274
\isamarkupfalse%
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   275
\isacommand{apply}\ auto\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   276
\isamarkupfalse%
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   277
\isacommand{done}\isanewline
a17cf465d29a auto generated
paulson
parents:
diff changeset
   278
\isanewline
10469
7813f5ccfb18 auto update
paulson
parents: 10457
diff changeset
   279
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   280
\isamarkupfalse%
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   281
\isacommand{end}\isanewline
a17cf465d29a auto generated
paulson
parents:
diff changeset
   282
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   283
\isamarkupfalse%
11187
c6e49929e544 auto-update
paulson
parents: 11173
diff changeset
   284
\end{isabellebody}%
10365
a17cf465d29a auto generated
paulson
parents:
diff changeset
   285
%%% Local Variables:
a17cf465d29a auto generated
paulson
parents:
diff changeset
   286
%%% mode: latex
a17cf465d29a auto generated
paulson
parents:
diff changeset
   287
%%% TeX-master: "root"
a17cf465d29a auto generated
paulson
parents:
diff changeset
   288
%%% End: