doc-src/TutorialI/Inductive/Advanced.tex
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10475 77fafa07fc8f
permissions -rw-r--r--
*** empty log message ***
paulson@10468
     1
paulson@10475
     2
This section describes advanced features of inductive definitions. 
paulson@10468
     3
The premises of introduction rules may contain universal quantifiers and
paulson@10468
     4
monotonic functions.  Theorems may be proved by rule inversion.
paulson@10468
     5
paulson@10468
     6
\subsection{Universal quantifiers in introduction rules}
paulson@10468
     7
\label{sec:gterm-datatype}
paulson@10468
     8
paulson@10475
     9
As a running example, this section develops the theory of \textbf{ground
paulson@10475
    10
terms}: terms constructed from constant and function 
paulson@10475
    11
symbols but not variables. To simplify matters further, we regard a
paulson@10475
    12
constant as a function applied to the null argument  list.  Let us declare a
paulson@10475
    13
datatype \isa{gterm} for the type of ground  terms. It is a type constructor
paulson@10475
    14
whose argument is a type of  function symbols. 
paulson@10468
    15
\begin{isabelle}
paulson@10468
    16
\isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list"
paulson@10468
    17
\end{isabelle}
paulson@10468
    18
To try it out, we declare a datatype of some integer operations: 
paulson@10468
    19
integer constants, the unary minus operator and the addition 
paulson@10468
    20
operator. 
paulson@10468
    21
\begin{isabelle}
paulson@10468
    22
\isacommand{datatype}\ integer_op\ =\ Number\ int\ |\ UnaryMinus\ |\ Plus
paulson@10468
    23
\end{isabelle}
paulson@10468
    24
Now the type \isa{integer\_op gterm} denotes the ground 
paulson@10468
    25
terms built over those symbols.
paulson@10468
    26
paulson@10468
    27
The type constructor \texttt{gterm} can be generalized to a function 
paulson@10468
    28
over sets.  It returns 
paulson@10468
    29
the set of ground terms that can be formed over a set \isa{F} of function symbols. For
paulson@10468
    30
example,  we could consider the set of ground terms formed from the finite 
paulson@10468
    31
set {\isa{\{Number 2, UnaryMinus, Plus\}}}.
paulson@10468
    32
paulson@10468
    33
This concept is inductive. If we have a list \isa{args} of ground terms 
paulson@10468
    34
over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we 
paulson@10468
    35
can apply \isa{f} to  \isa{args} to obtain another ground term. 
paulson@10468
    36
The only difficulty is that the argument list may be of any length. Hitherto, 
paulson@10468
    37
each rule in an inductive definition referred to the inductively 
paulson@10468
    38
defined set a fixed number of times, typically once or twice. 
paulson@10468
    39
A universal quantifier in the premise of the introduction rule 
paulson@10468
    40
expresses that every element of \isa{args} belongs
paulson@10468
    41
to our inductively defined set: is a ground term 
paulson@10468
    42
over~\isa{F}.  The function {\isa{set}} denotes the set of elements in a given 
paulson@10468
    43
list. 
paulson@10468
    44
\begin{isabelle}
paulson@10468
    45
\isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
paulson@10468
    46
\isacommand{inductive}\ "gterms\ F"\isanewline
paulson@10468
    47
\isakeyword{intros}\isanewline
paulson@10468
    48
step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ gterms\ F;\ \ f\ \isasymin \ F\isasymrbrakk \isanewline
paulson@10468
    49
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ gterms\
paulson@10468
    50
F"
paulson@10468
    51
\end{isabelle}
paulson@10468
    52
paulson@10468
    53
To demonstrate a proof from this definition, let us 
paulson@10468
    54
show that the function \isa{gterms}
paulson@10468
    55
is \textbf{monotonic}.  We shall need this concept shortly.
paulson@10468
    56
\begin{isabelle}
paulson@10468
    57
\isacommand{lemma}\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline
paulson@10468
    58
\isacommand{apply}\ clarify\isanewline
paulson@10468
    59
\isacommand{apply}\ (erule\ gterms.induct)\isanewline
paulson@10468
    60
\isacommand{apply}\ blast\isanewline
paulson@10468
    61
\isacommand{done}
paulson@10468
    62
\end{isabelle}
paulson@10468
    63
Intuitively, this theorem says that
paulson@10468
    64
enlarging the set of function symbols enlarges the set of ground 
paulson@10468
    65
terms. The proof is a trivial rule induction.
paulson@10468
    66
First we use the \isa{clarify} method to assume the existence of an element of
paulson@10468
    67
\isa{terms~F}.  (We could have used \isa{intro subsetI}.)  We then
paulson@10468
    68
apply rule induction. Here is the resulting subgoal: 
paulson@10468
    69
\begin{isabelle}
paulson@10468
    70
1.\ \isasymAnd x\ f\ args.\isanewline
paulson@10468
    71
\ \ \ \ \ \ \isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline
paulson@10468
    72
\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G%
paulson@10468
    73
\end{isabelle}
paulson@10468
    74
%
paulson@10468
    75
The assumptions state that \isa{f} belongs 
paulson@10468
    76
to~\isa{F}, which is included in~\isa{G}, and that every element of the list \isa{args} is
paulson@10468
    77
a ground term over~\isa{G}.  The \isa{blast} method finds this chain of reasoning easily.  
paulson@10468
    78
paulson@10468
    79
\textit{Remark}: why do we call this function \isa{gterms} instead 
paulson@10468
    80
of {\isa{gterm}}? Isabelle maintains separate name spaces for types 
paulson@10468
    81
and constants, so there is no danger of confusion. However, name 
paulson@10468
    82
clashes could arise in the theorems that Isabelle generates. 
paulson@10468
    83
Our choice of names keeps {\isa{gterms.induct}} separate from {\isa{gterm.induct}}.
paulson@10468
    84
paulson@10468
    85
\subsection{Rule inversion}\label{sec:rule-inversion}
paulson@10468
    86
paulson@10468
    87
Case analysis on an inductive definition is called \textbf{rule inversion}. 
paulson@10468
    88
It is frequently used in proofs about operational semantics.  It can be
paulson@10468
    89
highly effective when it is applied automatically.  Let us look at how rule
paulson@10468
    90
inversion is done in Isabelle.
paulson@10468
    91
paulson@10468
    92
Recall that \isa{even} is the minimal set closed under these two rules:
paulson@10468
    93
\begin{isabelle}
paulson@10468
    94
0\ \isasymin \ even\isanewline
paulson@10468
    95
n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin
paulson@10468
    96
\ even
paulson@10468
    97
\end{isabelle}
paulson@10468
    98
Minimality means that \isa{even} contains only the elements that these
paulson@10468
    99
rules force it to contain.  If we are told that \isa{a}
paulson@10468
   100
belongs to
paulson@10468
   101
\isa{even} then there are only two possibilities.  Either \isa{a} is \isa{0}
paulson@10468
   102
or else \isa{a} has the form \isa{Suc(Suc~n)}, for an arbitrary \isa{n}
paulson@10468
   103
that belongs to
paulson@10468
   104
\isa{even}.  That is the gist of the \isa{cases} rule, which Isabelle proves
paulson@10468
   105
for us when it accepts an inductive definition:
paulson@10468
   106
\begin{isabelle}
paulson@10468
   107
\isasymlbrakk a\ \isasymin \ even;\isanewline
paulson@10468
   108
\ a\ =\ 0\ \isasymLongrightarrow \ P;\isanewline
paulson@10468
   109
\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc(Suc\ n);\ n\ \isasymin \
paulson@10468
   110
even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \
paulson@10468
   111
\isasymLongrightarrow \ P
paulson@10468
   112
\rulename{even.cases}
paulson@10468
   113
\end{isabelle}
paulson@10468
   114
paulson@10468
   115
This general rule is less useful than instances of it for
paulson@10468
   116
specific patterns.  For example, if \isa{a} has the form
paulson@10468
   117
\isa{Suc(Suc~n)} then the first case becomes irrelevant, while the second
paulson@10468
   118
case tells us that \isa{n} belongs to \isa{even}.  Isabelle will generate
paulson@10468
   119
this instance for us:
paulson@10468
   120
\begin{isabelle}
paulson@10468
   121
\isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]:
paulson@10468
   122
\ "Suc(Suc\ n)\ \isasymin \ even"
paulson@10468
   123
\end{isabelle}
paulson@10468
   124
The \isacommand{inductive\_cases} command generates an instance of the
paulson@10468
   125
\isa{cases} rule for the supplied pattern and gives it the supplied name:
paulson@10468
   126
%
paulson@10468
   127
\begin{isabelle}
paulson@10468
   128
\isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\
paulson@10468
   129
\isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
paulson@10468
   130
\rulename{Suc_Suc_cases}
paulson@10468
   131
\end{isabelle}
paulson@10468
   132
%
paulson@10468
   133
Applying this as an elimination rule yields one case where \isa{even.cases}
paulson@10468
   134
would yield two.  Rule inversion works well when the conclusions of the
paulson@10468
   135
introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}
paulson@10468
   136
(list `cons'); freeness reasoning discards all but one or two cases.
paulson@10468
   137
paulson@10468
   138
In the \isacommand{inductive\_cases} command we supplied an
paulson@10468
   139
attribute, \isa{elim!}, indicating that this elimination rule can be applied
paulson@10468
   140
aggressively.  The original
paulson@10468
   141
\isa{cases} rule would loop if used in that manner because the
paulson@10468
   142
pattern~\isa{a} matches everything.
paulson@10468
   143
paulson@10468
   144
The rule \isa{Suc_Suc_cases} is equivalent to the following implication:
paulson@10468
   145
\begin{isabelle}
paulson@10468
   146
Suc (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \
paulson@10468
   147
even
paulson@10468
   148
\end{isabelle}
paulson@10468
   149
%
paulson@10468
   150
In \S\ref{sec:gen-rule-induction} we devoted some effort to proving precisely
paulson@10468
   151
this result.  Yet we could have obtained it by a one-line declaration. 
paulson@10468
   152
This example also justifies the terminology \textbf{rule inversion}: the new
paulson@10468
   153
rule inverts the introduction rule \isa{even.step}.
paulson@10468
   154
paulson@10468
   155
For one-off applications of rule inversion, use the \isa{ind_cases} method. 
paulson@10468
   156
Here is an example:
paulson@10468
   157
\begin{isabelle}
paulson@10468
   158
\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")
paulson@10468
   159
\end{isabelle}
paulson@10468
   160
The specified instance of the \isa{cases} rule is generated, applied, and
paulson@10468
   161
discarded.
paulson@10468
   162
paulson@10468
   163
\medskip
paulson@10468
   164
Let us try rule inversion on our ground terms example:
paulson@10468
   165
\begin{isabelle}
paulson@10468
   166
\isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
paulson@10468
   167
\isasymin\ gterms\ F"
paulson@10468
   168
\end{isabelle}
paulson@10468
   169
%
paulson@10468
   170
Here is the result.  No cases are discarded (there was only one to begin
paulson@10468
   171
with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}.
paulson@10468
   172
It can be applied repeatedly as an elimination rule without looping, so we
paulson@10468
   173
have given the
paulson@10468
   174
\isa{elim!}\ attribute. 
paulson@10468
   175
\begin{isabelle}
paulson@10468
   176
\isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\isanewline
paulson@10468
   177
\ \isasymlbrakk
paulson@10468
   178
\isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin
paulson@10468
   179
\ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk\isanewline
paulson@10468
   180
\isasymLongrightarrow \ P%
paulson@10468
   181
\rulename{gterm_Apply_elim}
paulson@10468
   182
\end{isabelle}
paulson@10468
   183
paulson@10468
   184
This rule replaces an assumption about \isa{Apply\ f\ args} by 
paulson@10468
   185
assumptions about \isa{f} and~\isa{args}.  Here is a proof in which this
paulson@10468
   186
inference is essential.  We show that if \isa{t} is a ground term over both
paulson@10468
   187
of the sets
paulson@10468
   188
\isa{F} and~\isa{G} then it is also a ground term over their intersection,
paulson@10468
   189
\isa{F\isasyminter G}.
paulson@10468
   190
\begin{isabelle}
paulson@10468
   191
\isacommand{lemma}\ gterms_IntI\ [rule_format]:\isanewline
paulson@10468
   192
\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline
paulson@10468
   193
\isacommand{apply}\ (erule\ gterms.induct)\isanewline
paulson@10468
   194
\isacommand{apply}\ blast\isanewline
paulson@10468
   195
\isacommand{done}
paulson@10468
   196
\end{isabelle}
paulson@10468
   197
%
paulson@10468
   198
The proof begins with rule induction over the definition of
paulson@10468
   199
\isa{gterms}, which leaves a single subgoal:  
paulson@10468
   200
\begin{isabelle}
paulson@10468
   201
1.\ \isasymAnd args\ f.\isanewline
paulson@10468
   202
\ \ \ \ \ \ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand\isanewline
paulson@10468
   203
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline
paulson@10468
   204
\ \ \ \ \ \ \ f\ \isasymin \ F\isasymrbrakk \isanewline
paulson@10468
   205
\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G)
paulson@10468
   206
\end{isabelle}
paulson@10468
   207
%
paulson@10468
   208
The induction hypothesis states that every element of \isa{args} belongs to 
paulson@10468
   209
\isa{gterms\ (F\ \isasyminter \ G)} --- provided it already belongs to
paulson@10468
   210
\isa{gterms\ G}.  How do we meet that condition?  
paulson@10468
   211
paulson@10468
   212
By assuming (as we may) the formula \isa{Apply\ f\ args\ \isasymin \ gterms\
paulson@10468
   213
G}.  Rule inversion, in the form of \isa{gterm_Apply_elim}, infers that every
paulson@10468
   214
element of \isa{args} belongs to 
paulson@10468
   215
\isa{gterms~G}.  It also yields \isa{f\ \isasymin \ G}, which will allow us
paulson@10468
   216
to conclude \isa{f\ \isasymin \ F\ \isasyminter \ G}.  All of this reasoning
paulson@10468
   217
is done by \isa{blast}.
paulson@10468
   218
paulson@10468
   219
\medskip
paulson@10468
   220
paulson@10468
   221
To summarize, every inductive definition produces a \isa{cases} rule.  The
paulson@10468
   222
\isacommand{inductive\_cases} command stores an instance of the \isa{cases}
paulson@10468
   223
rule for a given pattern.  Within a proof, the \isa{ind_cases} method
paulson@10468
   224
applies an instance of the \isa{cases}
paulson@10468
   225
rule.
paulson@10468
   226
paulson@10468
   227
paulson@10468
   228
\subsection{Continuing the `ground terms' example}
paulson@10468
   229
paulson@10468
   230
Call a term \textbf{well-formed} if each symbol occurring in it has 
paulson@10468
   231
the correct number of arguments. To formalize this concept, we 
paulson@10468
   232
introduce a function mapping each symbol to its arity, a natural 
paulson@10468
   233
number. 
paulson@10468
   234
paulson@10468
   235
Let us define the set of well-formed ground terms. 
paulson@10468
   236
Suppose we are given a function called \isa{arity}, specifying the arities to be used.
paulson@10468
   237
In the inductive step, we have a list \isa{args} of such terms and a function 
paulson@10468
   238
symbol~\isa{f}. If the length of the list matches the function's arity 
paulson@10468
   239
then applying \isa{f} to \isa{args} yields a well-formed term. 
paulson@10468
   240
\begin{isabelle}
paulson@10468
   241
\isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
paulson@10468
   242
\isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline
paulson@10468
   243
\isakeyword{intros}\isanewline
paulson@10468
   244
step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ well_formed_gterm\ arity;\ \ \isanewline
paulson@10468
   245
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
paulson@10468
   246
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm\
paulson@10468
   247
arity"
paulson@10468
   248
\end{isabelle}
paulson@10468
   249
%
paulson@10468
   250
The inductive definition neatly captures the reasoning above.
paulson@10468
   251
It is just an elaboration of the previous one, consisting of a single 
paulson@10468
   252
introduction rule. The universal quantification over the
paulson@10468
   253
\isa{set} of arguments expresses that all of them are well-formed.
paulson@10468
   254
paulson@10468
   255
\subsection{Alternative definition using a monotonic function}
paulson@10468
   256
paulson@10468
   257
An inductive definition may refer to the inductively defined 
paulson@10468
   258
set through an arbitrary monotonic function.  To demonstrate this
paulson@10468
   259
powerful feature, let us
paulson@10468
   260
change the  inductive definition above, replacing the
paulson@10468
   261
quantifier by a use of the function \isa{lists}. This
paulson@10468
   262
function, from the Isabelle library, is analogous to the
paulson@10468
   263
function \isa{gterms} declared above. If \isa{A} is a set then
paulson@10468
   264
{\isa{lists A}} is the set of lists whose elements belong to
paulson@10468
   265
\isa{A}.  
paulson@10468
   266
paulson@10468
   267
In the inductive definition of well-formed terms, examine the one
paulson@10468
   268
introduction rule.  The first premise states that \isa{args} belongs to
paulson@10468
   269
the \isa{lists} of well-formed terms.  This formulation is more
paulson@10468
   270
direct, if more obscure, than using a universal quantifier.
paulson@10468
   271
\begin{isabelle}
paulson@10468
   272
\isacommand{consts}\ well_formed_gterm'\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
paulson@10468
   273
\isacommand{inductive}\ "well_formed_gterm'\ arity"\isanewline
paulson@10468
   274
\isakeyword{intros}\isanewline
paulson@10468
   275
step[intro!]:\ "\isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity);\ \ \isanewline
paulson@10468
   276
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
paulson@10468
   277
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline
paulson@10468
   278
\isakeyword{monos}\ lists_mono
paulson@10468
   279
\end{isabelle}
paulson@10468
   280
paulson@10468
   281
We must cite the theorem \isa{lists_mono} in order to justify 
paulson@10468
   282
using the function \isa{lists}. 
paulson@10468
   283
\begin{isabelle}
paulson@10468
   284
A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq
paulson@10468
   285
\ lists\ B\rulename{lists_mono}
paulson@10468
   286
\end{isabelle}
paulson@10468
   287
%
paulson@10468
   288
Why must the function be monotonic?  An inductive definition describes
paulson@10468
   289
an iterative construction: each element of the set is constructed by a
paulson@10468
   290
finite number of introduction rule applications.  For example, the
paulson@10468
   291
elements of \isa{even} are constructed by finitely many applications of
paulson@10468
   292
the rules 
paulson@10468
   293
\begin{isabelle}
paulson@10468
   294
0\ \isasymin \ even\isanewline
paulson@10468
   295
n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin
paulson@10468
   296
\ even
paulson@10468
   297
\end{isabelle}
paulson@10468
   298
All references to a set in its
paulson@10468
   299
inductive definition must be positive.  Applications of an
paulson@10468
   300
introduction rule cannot invalidate previous applications, allowing the
paulson@10468
   301
construction process to converge.
paulson@10468
   302
The following pair of rules do not constitute an inductive definition:
paulson@10468
   303
\begin{isabelle}
paulson@10468
   304
0\ \isasymin \ even\isanewline
paulson@10468
   305
n\ \isasymnotin \ even\ \isasymLongrightarrow \ (Suc\ n)\ \isasymin
paulson@10468
   306
\ even
paulson@10468
   307
\end{isabelle}
paulson@10468
   308
%
paulson@10468
   309
Showing that 4 is even using these rules requires showing that 3 is not
paulson@10468
   310
even.  It is far from trivial to show that this set of rules
paulson@10468
   311
characterizes the even numbers.  
paulson@10468
   312
paulson@10468
   313
Even with its use of the function \isa{lists}, the premise of our
paulson@10468
   314
introduction rule is positive:
paulson@10468
   315
\begin{isabelle}
paulson@10468
   316
args\ \isasymin \ lists\ (well_formed_gterm'\ arity)
paulson@10468
   317
\end{isabelle}
paulson@10468
   318
To apply the rule we construct a list \isa{args} of previously
paulson@10468
   319
constructed well-formed terms.  We obtain a
paulson@10468
   320
new term, \isa{Apply\ f\ args}.  Because \isa{lists} is monotonic,
paulson@10468
   321
applications of the rule remain valid as new terms are constructed.
paulson@10468
   322
Further lists of well-formed
paulson@10468
   323
terms become available and none are taken away.
paulson@10468
   324
paulson@10468
   325
paulson@10468
   326
\subsection{A proof of equivalence}
paulson@10468
   327
paulson@10468
   328
We naturally hope that these two inductive definitions of `well-formed' 
paulson@10468
   329
coincide.  The equality can be proved by separate inclusions in 
paulson@10468
   330
each direction.  Each is a trivial rule induction. 
paulson@10468
   331
\begin{isabelle}
paulson@10468
   332
\isacommand{lemma}\ "well_formed_gterm\ arity\ \isasymsubseteq \ well_formed_gterm'\ arity"\isanewline
paulson@10468
   333
\isacommand{apply}\ clarify\isanewline
paulson@10468
   334
\isacommand{apply}\ (erule\ well_formed_gterm.induct)\isanewline
paulson@10468
   335
\isacommand{apply}\ auto\isanewline
paulson@10468
   336
\isacommand{done}
paulson@10468
   337
\end{isabelle}
paulson@10468
   338
paulson@10468
   339
The \isa{clarify} method gives
paulson@10468
   340
us an element of \isa{well_formed_gterm\ arity} on which to perform 
paulson@10468
   341
induction.  The resulting subgoal can be proved automatically:
paulson@10468
   342
\begin{isabelle}
paulson@10468
   343
{\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
paulson@10468
   344
\ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
paulson@10468
   345
\ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
paulson@10468
   346
\ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
paulson@10468
   347
\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
paulson@10468
   348
\end{isabelle}
paulson@10468
   349
%
paulson@10468
   350
This proof resembles the one given in
paulson@10468
   351
\S\ref{sec:gterm-datatype} above, especially in the form of the
paulson@10468
   352
induction hypothesis.  Next, we consider the opposite inclusion:
paulson@10468
   353
\begin{isabelle}
paulson@10468
   354
\isacommand{lemma}\ "well_formed_gterm'\ arity\ \isasymsubseteq \ well_formed_gterm\ arity"\isanewline
paulson@10468
   355
\isacommand{apply}\ clarify\isanewline
paulson@10468
   356
\isacommand{apply}\ (erule\ well_formed_gterm'.induct)\isanewline
paulson@10468
   357
\isacommand{apply}\ auto\isanewline
paulson@10468
   358
\isacommand{done}
paulson@10468
   359
\end{isabelle}
paulson@10468
   360
%
paulson@10468
   361
The proof script is identical, but the subgoal after applying induction may
paulson@10468
   362
be surprising:
paulson@10468
   363
\begin{isabelle}
paulson@10468
   364
1.\ \isasymAnd x\ args\ f.\isanewline
paulson@10468
   365
\ \ \ \ \ \ \isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity\ \isasyminter\isanewline
paulson@10468
   366
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacharbraceleft u.\ u\ \isasymin \ well_formed_gterm\ arity\isacharbraceright );\isanewline
paulson@10468
   367
\ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
paulson@10468
   368
\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity%
paulson@10468
   369
\end{isabelle}
paulson@10468
   370
The induction hypothesis contains an application of \isa{lists}.  Using a
paulson@10468
   371
monotonic function in the inductive definition always has this effect.  The
paulson@10468
   372
subgoal may look uninviting, but fortunately a useful rewrite rule concerning
paulson@10468
   373
\isa{lists} is available:
paulson@10468
   374
\begin{isabelle}
paulson@10468
   375
lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B
paulson@10468
   376
\rulename{lists_Int_eq}
paulson@10468
   377
\end{isabelle}
paulson@10468
   378
%
paulson@10468
   379
Thanks to this default simplification rule, the induction hypothesis 
paulson@10468
   380
is quickly replaced by its two parts:
paulson@10468
   381
\begin{isabelle}
paulson@10468
   382
\ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm'\ arity)\isanewline
paulson@10468
   383
\ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm\ arity)
paulson@10468
   384
\end{isabelle}
paulson@10468
   385
Invoking the rule \isa{well_formed_gterm.step} completes the proof.  The
paulson@10468
   386
call to
paulson@10468
   387
\isa{auto} does all this work.
paulson@10468
   388
paulson@10468
   389
This example is typical of how monotonic functions can be used.  In
paulson@10468
   390
particular, a rewrite rule analogous to \isa{lists_Int_eq} holds in most
paulson@10468
   391
cases.  Monotonicity implies one direction of this set equality; we have
paulson@10468
   392
this theorem:
paulson@10468
   393
\begin{isabelle}
paulson@10468
   394
mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \
paulson@10468
   395
f\ A\ \isasyminter \ f\ B%
paulson@10468
   396
\rulename{mono_Int}
paulson@10468
   397
\end{isabelle}
paulson@10468
   398
paulson@10468
   399
paulson@10468
   400
To summarize: a universal quantifier in an introduction rule 
paulson@10468
   401
lets it refer to any number of instances of 
paulson@10468
   402
the inductively defined set.  A monotonic function in an introduction 
paulson@10468
   403
rule lets it refer to constructions over the inductively defined 
paulson@10468
   404
set.  Each element of an inductively defined set is created 
paulson@10468
   405
through finitely many applications of the introduction rules.  So each rule
paulson@10468
   406
must be positive, and never can it refer to \textit{infinitely} many
paulson@10468
   407
previous instances of the inductively defined set. 
paulson@10468
   408
paulson@10468
   409
paulson@10468
   410
paulson@10468
   411
\begin{exercise}
paulson@10468
   412
Prove this theorem, one direction of which was proved in
paulson@10468
   413
\S\ref{sec:rule-inversion} above.
paulson@10468
   414
\begin{isabelle}
paulson@10468
   415
\isacommand{lemma}\ gterms_Int_eq\ [simp]:\ "gterms\ (F\isasyminter G)\ =\
paulson@10468
   416
gterms\ F\ \isasyminter \ gterms\ G"\isanewline
paulson@10468
   417
\end{isabelle}
paulson@10468
   418
\end{exercise}
paulson@10468
   419
paulson@10468
   420
paulson@10468
   421
\begin{exercise}
paulson@10468
   422
A function mapping function symbols to their 
paulson@10468
   423
types is called a \textbf{signature}.  Given a type 
paulson@10468
   424
ranging over type symbols, we can represent a function's type by a
paulson@10468
   425
list of argument types paired with the result type. 
paulson@10468
   426
Complete this inductive definition:
paulson@10468
   427
\begin{isabelle}
paulson@10468
   428
\isacommand{consts}\ well_typed_gterm::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
paulson@10468
   429
\isacommand{inductive}\ "well_typed_gterm\ sig"\isanewline
paulson@10468
   430
\end{isabelle}
paulson@10468
   431
\end{exercise}