% $Id$

This section describes advanced features of inductive definitions. 

The premises of introduction rules may contain universal quantifiers and

monotonic functions.  Theorems may be proved by rule inversion.

\subsection{Universal Quantifiers in Introduction Rules}

\label{sec:gterm-datatype}

As a running example, this section develops the theory of \textbf{ground

terms}: terms constructed from constant and function 

symbols but not variables. To simplify matters further, we regard a

constant as a function applied to the null argument  list.  Let us declare a

datatype \isa{gterm} for the type of ground  terms. It is a type constructor

whose argument is a type of  function symbols. 

\begin{isabelle}

\isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list"

\end{isabelle}

To try it out, we declare a datatype of some integer operations: 

integer constants, the unary minus operator and the addition 

operator. 

\begin{isabelle}

\isacommand{datatype}\ integer_op\ =\ Number\ int\ |\ UnaryMinus\ |\ Plus

\end{isabelle}

Now the type \isa{integer\_op gterm} denotes the ground 

terms built over those symbols.

The type constructor \texttt{gterm} can be generalized to a function 

over sets.  It returns 

the set of ground terms that can be formed over a set \isa{F} of function symbols. For

example,  we could consider the set of ground terms formed from the finite 

set \isa{\isacharbraceleft Number 2, UnaryMinus,

Plus\isacharbraceright}.

This concept is inductive. If we have a list \isa{args} of ground terms 

over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we 

can apply \isa{f} to  \isa{args} to obtain another ground term. 

The only difficulty is that the argument list may be of any length. Hitherto, 

each rule in an inductive definition referred to the inductively 

defined set a fixed number of times, typically once or twice. 

A universal quantifier in the premise of the introduction rule 

expresses that every element of \isa{args} belongs

to our inductively defined set: is a ground term 

over~\isa{F}.  The function {\isa{set}} denotes the set of elements in a given 

list. 

\begin{isabelle}

\isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline

\isacommand{inductive}\ "gterms\ F"\isanewline

\isakeyword{intros}\isanewline

step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ gterms\ F;\ \ f\ \isasymin \ F\isasymrbrakk \isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ gterms\

F"

\end{isabelle}

To demonstrate a proof from this definition, let us 

show that the function \isa{gterms}

is \textbf{monotonic}.  We shall need this concept shortly.

\begin{isabelle}

\isacommand{lemma}\ gterms_mono:\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline

\isacommand{apply}\ clarify\isanewline

\isacommand{apply}\ (erule\ gterms.induct)\isanewline

\isacommand{apply}\ blast\isanewline

\isacommand{done}

\end{isabelle}

Intuitively, this theorem says that

enlarging the set of function symbols enlarges the set of ground 

terms. The proof is a trivial rule induction.

First we use the \isa{clarify} method to assume the existence of an element of

\isa{terms~F}.  (We could have used \isa{intro subsetI}.)  We then

apply rule induction. Here is the resulting subgoal: 

\begin{isabelle}

\ 1.\ \isasymAnd x\ args\ f.\isanewline

\ \ \ \ \ \ \ \isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline

\ \ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G%

\end{isabelle}

%

The assumptions state that \isa{f} belongs 

to~\isa{F}, which is included in~\isa{G}, and that every element of the list \isa{args} is

a ground term over~\isa{G}.  The \isa{blast} method finds this chain of reasoning easily.  

\begin{warn}

Why do we call this function \isa{gterms} instead 

of {\isa{gterm}}?  A constant may have the same name as a type.  However,

name  clashes could arise in the theorems that Isabelle generates. 

Our choice of names keeps {\isa{gterms.induct}} separate from 

{\isa{gterm.induct}}.

\end{warn}

\subsection{Rule Inversion}\label{sec:rule-inversion}

Case analysis on an inductive definition is called \textbf{rule inversion}. 

It is frequently used in proofs about operational semantics.  It can be

highly effective when it is applied automatically.  Let us look at how rule

inversion is done in Isabelle.

Recall that \isa{even} is the minimal set closed under these two rules:

\begin{isabelle}

0\ \isasymin \ even\isanewline

n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin

\ even

\end{isabelle}

Minimality means that \isa{even} contains only the elements that these

rules force it to contain.  If we are told that \isa{a}

belongs to

\isa{even} then there are only two possibilities.  Either \isa{a} is \isa{0}

or else \isa{a} has the form \isa{Suc(Suc~n)}, for an arbitrary \isa{n}

that belongs to

\isa{even}.  That is the gist of the \isa{cases} rule, which Isabelle proves

for us when it accepts an inductive definition:

\begin{isabelle}

\isasymlbrakk a\ \isasymin \ even;\isanewline

\ a\ =\ 0\ \isasymLongrightarrow \ P;\isanewline

\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc(Suc\ n);\ n\ \isasymin \

even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \

\isasymLongrightarrow \ P

\rulename{even.cases}

\end{isabelle}

This general rule is less useful than instances of it for

specific patterns.  For example, if \isa{a} has the form

\isa{Suc(Suc~n)} then the first case becomes irrelevant, while the second

case tells us that \isa{n} belongs to \isa{even}.  Isabelle will generate

this instance for us:

\begin{isabelle}

\isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]:

\ "Suc(Suc\ n)\ \isasymin \ even"

\end{isabelle}

The \isacommand{inductive\_cases} command generates an instance of the

\isa{cases} rule for the supplied pattern and gives it the supplied name:

%

\begin{isabelle}

\isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\

\isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%

\rulename{Suc_Suc_cases}

\end{isabelle}

%

Applying this as an elimination rule yields one case where \isa{even.cases}

would yield two.  Rule inversion works well when the conclusions of the

introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}

(list ``cons''); freeness reasoning discards all but one or two cases.

In the \isacommand{inductive\_cases} command we supplied an

attribute, \isa{elim!}, indicating that this elimination rule can be applied

aggressively.  The original

\isa{cases} rule would loop if used in that manner because the

pattern~\isa{a} matches everything.

The rule \isa{Suc_Suc_cases} is equivalent to the following implication:

\begin{isabelle}

Suc (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \

even

\end{isabelle}

%

In {\S}\ref{sec:gen-rule-induction} we devoted some effort to proving precisely

this result.  Yet we could have obtained it by a one-line declaration. 

This example also justifies the terminology \textbf{rule inversion}: the new

rule inverts the introduction rule \isa{even.step}.

For one-off applications of rule inversion, use the \isa{ind_cases} method. 

Here is an example:

\begin{isabelle}

\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")

\end{isabelle}

The specified instance of the \isa{cases} rule is generated, applied, and

discarded.

\medskip

Let us try rule inversion on our ground terms example:

\begin{isabelle}

\isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\

\isasymin\ gterms\ F"

\end{isabelle}

%

Here is the result.  No cases are discarded (there was only one to begin

with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}.

It can be applied repeatedly as an elimination rule without looping, so we

have given the

\isa{elim!}\ attribute. 

\begin{isabelle}

\isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\isanewline

\ \isasymlbrakk

\isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin

\ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk\isanewline

\isasymLongrightarrow \ P%

\rulename{gterm_Apply_elim}

\end{isabelle}

This rule replaces an assumption about \isa{Apply\ f\ args} by 

assumptions about \isa{f} and~\isa{args}.  Here is a proof in which this

inference is essential.  We show that if \isa{t} is a ground term over both

of the sets

\isa{F} and~\isa{G} then it is also a ground term over their intersection,

\isa{F\isasyminter G}.

\begin{isabelle}

\isacommand{lemma}\ gterms_IntI\ [rule_format]:\isanewline

\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline

\isacommand{apply}\ (erule\ gterms.induct)\isanewline

\isacommand{apply}\ blast\isanewline

\isacommand{done}

\end{isabelle}

%

The proof begins with rule induction over the definition of

\isa{gterms}, which leaves a single subgoal:  

\begin{isabelle}

1.\ \isasymAnd args\ f.\isanewline

\ \ \ \ \ \ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline

\ \ \ \ \ \ \ f\ \isasymin \ F\isasymrbrakk \isanewline

\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G)

\end{isabelle}

%

The induction hypothesis states that every element of \isa{args} belongs to 

\isa{gterms\ (F\ \isasyminter \ G)} --- provided it already belongs to

\isa{gterms\ G}.  How do we meet that condition?  

By assuming (as we may) the formula \isa{Apply\ f\ args\ \isasymin \ gterms\

G}.  Rule inversion, in the form of \isa{gterm_Apply_elim}, infers that every

element of \isa{args} belongs to 

\isa{gterms~G}.  It also yields \isa{f\ \isasymin \ G}, which will allow us

to conclude \isa{f\ \isasymin \ F\ \isasyminter \ G}.  All of this reasoning

is done by \isa{blast}.

\medskip

To summarize, every inductive definition produces a \isa{cases} rule.  The

\isacommand{inductive\_cases} command stores an instance of the \isa{cases}

rule for a given pattern.  Within a proof, the \isa{ind_cases} method

applies an instance of the \isa{cases}

rule.

\subsection{Continuing the Ground Terms Example}

Call a term \textbf{well-formed} if each symbol occurring in it has 

the correct number of arguments. To formalize this concept, we 

introduce a function mapping each symbol to its \textbf{arity}, a natural 

number. 

Let us define the set of well-formed ground terms. 

Suppose we are given a function called \isa{arity}, specifying the arities to be used.

In the inductive step, we have a list \isa{args} of such terms and a function 

symbol~\isa{f}. If the length of the list matches the function's arity 

then applying \isa{f} to \isa{args} yields a well-formed term. 

\begin{isabelle}

\isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline

\isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline

\isakeyword{intros}\isanewline

step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ well_formed_gterm\ arity;\ \ \isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm\

arity"

\end{isabelle}

%

The inductive definition neatly captures the reasoning above.

It is just an elaboration of the previous one, consisting of a single 

introduction rule. The universal quantification over the

\isa{set} of arguments expresses that all of them are well-formed.

\subsection{Alternative Definition Using a Monotonic Function}

An inductive definition may refer to the inductively defined 

set through an arbitrary monotonic function.  To demonstrate this

powerful feature, let us

change the  inductive definition above, replacing the

quantifier by a use of the function \isa{lists}. This

function, from the Isabelle theory of lists, is analogous to the

function \isa{gterms} declared above: if \isa{A} is a set then

{\isa{lists A}} is the set of lists whose elements belong to

\isa{A}.  

In the inductive definition of well-formed terms, examine the one

introduction rule.  The first premise states that \isa{args} belongs to

the \isa{lists} of well-formed terms.  This formulation is more

direct, if more obscure, than using a universal quantifier.

\begin{isabelle}

\isacommand{consts}\ well_formed_gterm'\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline

\isacommand{inductive}\ "well_formed_gterm'\ arity"\isanewline

\isakeyword{intros}\isanewline

step[intro!]:\ "\isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity);\ \ \isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline

\isakeyword{monos}\ lists_mono

\end{isabelle}

We must cite the theorem \isa{lists_mono} in order to justify 

using the function \isa{lists}. 

\begin{isabelle}

A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq

\ lists\ B\rulename{lists_mono}

\end{isabelle}

%

Why must the function be monotonic?  An inductive definition describes

an iterative construction: each element of the set is constructed by a

finite number of introduction rule applications.  For example, the

elements of \isa{even} are constructed by finitely many applications of

the rules 

\begin{isabelle}

0\ \isasymin \ even\isanewline

n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin

\ even

\end{isabelle}

All references to a set in its

inductive definition must be positive.  Applications of an

introduction rule cannot invalidate previous applications, allowing the

construction process to converge.

The following pair of rules do not constitute an inductive definition:

\begin{isabelle}

0\ \isasymin \ even\isanewline

n\ \isasymnotin \ even\ \isasymLongrightarrow \ (Suc\ n)\ \isasymin

\ even

\end{isabelle}

%

Showing that 4 is even using these rules requires showing that 3 is not

even.  It is far from trivial to show that this set of rules

characterizes the even numbers.  

Even with its use of the function \isa{lists}, the premise of our

introduction rule is positive:

\begin{isabelle}

args\ \isasymin \ lists\ (well_formed_gterm'\ arity)

\end{isabelle}

To apply the rule we construct a list \isa{args} of previously

constructed well-formed terms.  We obtain a

new term, \isa{Apply\ f\ args}.  Because \isa{lists} is monotonic,

applications of the rule remain valid as new terms are constructed.

Further lists of well-formed

terms become available and none are taken away.

\subsection{A Proof of Equivalence}

We naturally hope that these two inductive definitions of ``well-formed'' 

coincide.  The equality can be proved by separate inclusions in 

each direction.  Each is a trivial rule induction. 

\begin{isabelle}

\isacommand{lemma}\ "well_formed_gterm\ arity\ \isasymsubseteq \ well_formed_gterm'\ arity"\isanewline

\isacommand{apply}\ clarify\isanewline

\isacommand{apply}\ (erule\ well_formed_gterm.induct)\isanewline

\isacommand{apply}\ auto\isanewline

\isacommand{done}

\end{isabelle}

The \isa{clarify} method gives

us an element of \isa{well_formed_gterm\ arity} on which to perform 

induction.  The resulting subgoal can be proved automatically:

\begin{isabelle}

{\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline

\ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline

\ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline

\ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline

\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%

\end{isabelle}

%

This proof resembles the one given in

{\S}\ref{sec:gterm-datatype} above, especially in the form of the

induction hypothesis.  Next, we consider the opposite inclusion:

\begin{isabelle}

\isacommand{lemma}\ "well_formed_gterm'\ arity\ \isasymsubseteq \ well_formed_gterm\ arity"\isanewline

\isacommand{apply}\ clarify\isanewline

\isacommand{apply}\ (erule\ well_formed_gterm'.induct)\isanewline

\isacommand{apply}\ auto\isanewline

\isacommand{done}

\end{isabelle}

%

The proof script is identical, but the subgoal after applying induction may

be surprising:

\begin{isabelle}

1.\ \isasymAnd x\ args\ f.\isanewline

\ \ \ \ \ \ \isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity\ \isasyminter\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacharbraceleft u.\ u\ \isasymin \ well_formed_gterm\ arity\isacharbraceright );\isanewline

\ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline

\ \ \ \ \ \ \isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity%

\end{isabelle}

The induction hypothesis contains an application of \isa{lists}.  Using a

monotonic function in the inductive definition always has this effect.  The

subgoal may look uninviting, but fortunately a useful rewrite rule concerning

\isa{lists} is available:

\begin{isabelle}

lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B

\rulename{lists_Int_eq}

\end{isabelle}

%

Thanks to this default simplification rule, the induction hypothesis 

is quickly replaced by its two parts:

\begin{isabelle}

\ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm'\ arity)\isanewline

\ \ \ \ \ \ \ args\ \isasymin \ lists\ (well_formed_gterm\ arity)

\end{isabelle}

Invoking the rule \isa{well_formed_gterm.step} completes the proof.  The

call to

\isa{auto} does all this work.

This example is typical of how monotonic functions can be used.  In

particular, a rewrite rule analogous to \isa{lists_Int_eq} holds in most

cases.  Monotonicity implies one direction of this set equality; we have

this theorem:

\begin{isabelle}

mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \

f\ A\ \isasyminter \ f\ B%

\rulename{mono_Int}

\end{isabelle}

To summarize: a universal quantifier in an introduction rule 

lets it refer to any number of instances of 

the inductively defined set.  A monotonic function in an introduction 

rule lets it refer to constructions over the inductively defined 

set.  Each element of an inductively defined set is created 

through finitely many applications of the introduction rules.  So each rule

must be positive, and never can it refer to \textit{infinitely} many

previous instances of the inductively defined set. 

\begin{exercise}

Prove this theorem, one direction of which was proved in

{\S}\ref{sec:rule-inversion} above.

\begin{isabelle}

\isacommand{lemma}\ gterms_Int_eq\ [simp]:\ "gterms\ (F\isasyminter G)\ =\

gterms\ F\ \isasyminter \ gterms\ G"\isanewline

\end{isabelle}

\end{exercise}

\begin{exercise}

A function mapping function symbols to their 

types is called a \textbf{signature}.  Given a type 

ranging over type symbols, we can represent a function's type by a

list of argument types paired with the result type. 

Complete this inductive definition:

\begin{isabelle}

\isacommand{consts}\ well_typed_gterm::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline

\isacommand{inductive}\ "well_typed_gterm\ sig"\isanewline

\end{isabelle}

\end{exercise}