doc-src/TutorialI/Inductive/advanced-examples.tex

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

% $Id$
The premises of introduction rules may contain universal quantifiers and
monotone functions.  A universal quantifier lets the rule 
refer to any number of instances of 
the inductively defined set.  A monotone function lets the rule refer
to existing constructions (such as ``list of'') over the inductively defined
set.  The examples below show how to use the additional expressiveness
and how to reason from the resulting definitions.

\subsection{Universal Quantifiers in Introduction Rules}
\label{sec:gterm-datatype}

\index{ground terms example|(}%
\index{quantifiers!and inductive definitions|(}%
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{monotone}.  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{gterms~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}

Call a term \textbf{well-formed} if each symbol occurring in it is applied
to the correct number of arguments.  (This number is called the symbol's
\textbf{arity}.)  We can express well-formedness by
generalizing the inductive definition of
\isa{gterms}.
Suppose we are given a function called \isa{arity}, specifying the arities
of all symbols.  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.
The universal quantification over the
\isa{set} of arguments expresses that all of them are well-formed.%
\index{quantifiers!and inductive definitions|)}


\subsection{Alternative Definition Using a Monotone Function}

\index{monotone functions!and inductive definitions|(}% 
An inductive definition may refer to the
inductively defined  set through an arbitrary monotone 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 cite the theorem \isa{lists_mono} to justify 
using the function \isa{lists}.%
\footnote{This particular theorem is installed by default already, but we
include the \isakeyword{monos} declaration in order to illustrate its syntax.}
\begin{isabelle}
A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq
\ lists\ B\rulenamedx{lists_mono}
\end{isabelle}
%
Why must the function be monotone?  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 monotone,
applications of the rule remain valid as new terms are constructed.
Further lists of well-formed
terms become available and none are taken away.%
\index{monotone functions!and inductive definitions|)} 


\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\_formed\_gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well\_formed\_gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
\ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
\ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well\_formed\_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
monotone function in the inductive definition always has this effect.  The
subgoal may look uninviting, but fortunately 
\isa{lists} distributes over intersection:
\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 monotone functions
\index{monotone functions} can be used.  In particular, many of them
distribute over intersection.  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}


\subsection{Another Example of Rule Inversion}

\index{rule inversion|(}%
Does \isa{gterms} distribute over intersection?  We have proved that this
function is monotone, so \isa{mono_Int} gives one of the inclusions.  The
opposite inclusion asserts 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:\isanewline
\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter
G)"
\end{isabelle}
Attempting this proof, we get the assumption 
\isa{Apply\ f\ args\ \isasymin\ gterms\ G}, which cannot be broken down. 
It looks like a job for rule inversion:
\begin{isabelle}
\commdx{inductive\protect\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
\isasymin\ gterms\ F"
\end{isabelle}
%
Here is the result.
\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}.  
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. 

Now we can prove the other half of that distributive law.
\begin{isabelle}
\isacommand{lemma}\ gterms_IntI\ [rule_format,\ intro!]:\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}
%
To prove this, we assume \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}; hence (by the induction hypothesis) it belongs
to \isa{gterms\ (F\ \isasyminter \ G)}.  Rule inversion also yields
\isa{f\ \isasymin\ G} and hence \isa{f\ \isasymin \ F\ \isasyminter \ G}. 
All of this reasoning is done by \isa{blast}.

\smallskip
Our distributive law is a trivial consequence of previously-proved results:
\begin{isabelle}
\isacommand{theorem}\ gterms_Int_eq\ [simp]:\isanewline
\ \ \ \ \ "gterms\ (F\isasyminter G)\ =\ gterms\ F\ \isasyminter \ gterms\ G"\isanewline
\isacommand{by}\ (blast\ intro!:\ mono_Int\ monoI\ gterms_mono)
\end{isabelle}
\index{rule inversion|)}%
\index{ground terms example|)}


\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}