--- a/doc-src/TutorialI/Inductive/Advanced.thy Wed Feb 21 12:07:00 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Advanced.thy Wed Feb 21 12:57:55 2001 +0100
@@ -56,7 +56,7 @@
\rulename{gterm_Apply_elim}
*}
-lemma gterms_IntI [rule_format]:
+lemma gterms_IntI [rule_format, intro!]:
"t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
apply (erule gterms.induct)
txt{*
@@ -73,10 +73,7 @@
lemma gterms_Int_eq [simp]:
"gterms (F\<inter>G) = gterms F \<inter> gterms G"
-apply (rule equalityI)
-apply (blast intro!: mono_Int monoI gterms_mono)
-apply (blast intro!: gterms_IntI)
-done
+by (blast intro!: mono_Int monoI gterms_mono)
consts integer_arity :: "integer_op \<Rightarrow> nat"
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex Wed Feb 21 12:07:00 2001 +0100
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Wed Feb 21 12:57:55 2001 +0100
@@ -1,7 +1,11 @@
% $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.
+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}
@@ -40,7 +44,7 @@
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
+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
@@ -53,7 +57,7 @@
To demonstrate a proof from this definition, let us
show that the function \isa{gterms}
-is \textbf{monotonic}. We shall need this concept shortly.
+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
@@ -85,162 +89,16 @@
{\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 some suitable \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.
+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
@@ -252,14 +110,14 @@
\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
+The universal quantification over the
\isa{set} of arguments expresses that all of them are well-formed.
-\subsection{Alternative Definition Using a Monotonic Function}
+
+\subsection{Alternative Definition Using a monotone Function}
An inductive definition may refer to the inductively defined
-set through an arbitrary monotonic function. To demonstrate this
+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
@@ -289,7 +147,7 @@
\ lists\ B\rulename{lists_mono}
\end{isabelle}
%
-Why must the function be monotonic? An inductive definition describes
+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
@@ -321,7 +179,7 @@
\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,
+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.
@@ -372,9 +230,9 @@
\ \ \ \ \ \ \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:
+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}
@@ -390,10 +248,9 @@
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:
+This example is typical of how 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%
@@ -401,15 +258,76 @@
\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.
+\subsection{Another Example of 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}.
+
+Attempting this proof, we get the assumption
+\isa{Apply\ f\ args\ \isasymin\ gterms\ F}, which cannot be broken down.
+It looks like a job for rule inversion:
+\begin{isabelle}
+\isacommand{inductive\_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}
+The \isa{intro!}\ attribute of \isa{gterms_IntI} makes it available for
+this proof.
\begin{exercise}
--- a/doc-src/TutorialI/Inductive/document/Advanced.tex Wed Feb 21 12:07:00 2001 +0100
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Wed Feb 21 12:57:55 2001 +0100
@@ -1,221 +1,218 @@
%
-\begin{isabellebody}%
-\def\isabellecontext{Advanced}%
+\begin{isabelle}
+\def\isabellecontext{Advanced}
\isanewline
-\isacommand{theory}\ Advanced\ {\isacharequal}\ Even{\isacharcolon}\isanewline
+\isacommand{theory}\ Advanced\ =\ Even:\isanewline
\isanewline
\isanewline
-\isacommand{datatype}\ {\isacharprime}f\ gterm\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequote}{\isacharprime}f\ gterm\ list{\isachardoublequote}\isanewline
+\isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list"\isanewline
\isanewline
-\isacommand{datatype}\ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus\isanewline
+\isacommand{datatype}\ integer_op\ =\ Number\ int\ |\ UnaryMinus\ |\ Plus\isanewline
\isanewline
-\isacommand{consts}\ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
-\isacommand{inductive}\ {\isachardoublequote}gterms\ F{\isachardoublequote}\isanewline
+\isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
+\isacommand{inductive}\ "gterms\ F"\isanewline
\isakeyword{intros}\isanewline
-step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequote}\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"\isanewline
\isanewline
-\isacommand{lemma}\ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequote}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequote}\isanewline
+\isacommand{lemma}\ gterms_mono:\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline
\isacommand{apply}\ clarify\isanewline
-\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}%
-\begin{isamarkuptxt}%
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
-\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
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G%
-\end{isabelle}%
-\end{isamarkuptxt}%
+\isacommand{apply}\ (erule\ gterms.induct)
+\begin{isamarkuptxt}
+\begin{isabelle}
+\ 1.\ \isasymAnd x\ args\ f.\isanewline
+\isaindent{\ 1.\ \ \ \ }\isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline
+\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G%
+\end{isabelle}
+\end{isamarkuptxt}
\isacommand{apply}\ blast\isanewline
-\isacommand{done}%
-\begin{isamarkuptext}%
-\begin{isabelle}%
-\ \ \ \ \ {\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%
+\isacommand{done}
+\begin{isamarkuptext}
+\begin{isabelle}
+\ \ \ \ \ \isasymlbrakk a\ \isasymin \ even;\ a\ =\ 0\ \isasymLongrightarrow \ P;\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc\ (Suc\ n);\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
+\rulename{even.cases}
\end{isabelle}
-\rulename{even.cases}
Just as a demo I include
the two forms that Markus has made available. First the one for binding the
result to a name%
-\end{isamarkuptext}%
-\isacommand{inductive{\isacharunderscore}cases}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}\isanewline
+\end{isamarkuptext}
+\isacommand{inductive_cases}\ Suc_Suc_cases\ [elim!]:\isanewline
+\ \ "Suc(Suc\ n)\ \isasymin \ even"\isanewline
\isanewline
-\isacommand{thm}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases%
-\begin{isamarkuptext}%
-\begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
+\isacommand{thm}\ Suc_Suc_cases%
+\begin{isamarkuptext}
+\begin{isabelle}
+\ \ \ \ \ \isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
+\rulename{Suc_Suc_cases}
\end{isabelle}
-\rulename{Suc_Suc_cases}
and now the one for local usage:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
-\isacommand{apply}\ {\isacharparenleft}ind{\isacharunderscore}cases\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}{\isacharparenright}\isanewline
+\end{isamarkuptext}
+\isacommand{lemma}\ "Suc(Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ P\ n"\isanewline
+\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")\isanewline
\isacommand{oops}\isanewline
\isanewline
-\isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}%
-\begin{isamarkuptext}%
+\isacommand{inductive_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\ \isasymin \ gterms\ F"
+\begin{isamarkuptext}
this is what we get:
-\begin{isabelle}%
-\ \ \ \ \ {\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%
+\begin{isabelle}
+\ \ \ \ \ \isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin \ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
+\rulename{gterm_Apply_elim}
\end{isabelle}
-\rulename{gterm_Apply_elim}%
-\end{isamarkuptext}%
-\isacommand{lemma}\ gterms{\isacharunderscore}IntI\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ \ \ \ {\isachardoublequote}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}%
-\begin{isamarkuptxt}%
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
-\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
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}%
-\end{isabelle}%
-\end{isamarkuptxt}%
+\end{isamarkuptext}
+\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)
+\begin{isamarkuptxt}
+\begin{isabelle}
+\ 1.\ \isasymAnd args\ f.\isanewline
+\isaindent{\ 1.\ \ \ \ }\isasymlbrakk \isasymforall t\isasymin set\ args.\isanewline
+\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ gterms\ F\ \isasymand \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline
+\isaindent{\ 1.\ \ \ \ \ \ \ }f\ \isasymin \ F\isasymrbrakk \isanewline
+\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \isanewline
+\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G)
+\end{isabelle}
+\end{isamarkuptxt}
\isacommand{apply}\ blast\isanewline
-\isacommand{done}%
-\begin{isamarkuptext}%
-\begin{isabelle}%
-\ \ \ \ \ mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B%
+\isacommand{done}
+\begin{isamarkuptext}
+\begin{isabelle}
+\ \ \ \ \ mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \ f\ A\ \isasyminter \ f\ B%
+\rulename{mono_Int}
\end{isabelle}
-\rulename{mono_Int}%
-\end{isamarkuptext}%
-\isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline
-\isacommand{apply}\ {\isacharparenleft}rule\ equalityI{\isacharparenright}\isanewline
-\isacommand{apply}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isanewline
-\isacommand{apply}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ gterms{\isacharunderscore}IntI{\isacharparenright}\isanewline
-\isacommand{done}\isanewline
+\end{isamarkuptext}
+\isacommand{lemma}\ gterms_Int_eq\ [simp]:\isanewline
+\ \ \ \ \ "gterms\ (F\isasyminter G)\ =\ gterms\ F\ \isasyminter \ gterms\ G"\isanewline
+\isacommand{by}\ (blast\ intro!:\ mono_Int\ monoI\ gterms_mono)\isanewline
\isanewline
\isanewline
-\isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{consts}\ integer_arity\ ::\ "integer_op\ \isasymRightarrow \ nat"\isanewline
\isacommand{primrec}\isanewline
-{\isachardoublequote}integer{\isacharunderscore}arity\ {\isacharparenleft}Number\ n{\isacharparenright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharhash}{\isadigit{0}}{\isachardoublequote}\isanewline
-{\isachardoublequote}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}\isanewline
-{\isachardoublequote}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharhash}{\isadigit{2}}{\isachardoublequote}\isanewline
+"integer_arity\ (Number\ n)\ \ \ \ \ \ \ \ =\ \#0"\isanewline
+"integer_arity\ UnaryMinus\ \ \ \ \ \ \ \ =\ \#1"\isanewline
+"integer_arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ =\ \#2"\isanewline
\isanewline
-\isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
-\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
+\isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
+\isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline
\isakeyword{intros}\isanewline
-step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\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"\isanewline
\isanewline
\isanewline
-\isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
-\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
+\isacommand{consts}\ well_formed_gterm'\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
+\isacommand{inductive}\ "well_formed_gterm'\ arity"\isanewline
\isakeyword{intros}\isanewline
-step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
-\isakeyword{monos}\ lists{\isacharunderscore}mono\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\isanewline
\isanewline
-\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
+\isacommand{lemma}\ "well_formed_gterm\ arity\ \isasymsubseteq \ well_formed_gterm'\ arity"\isanewline
\isacommand{apply}\ clarify%
-\begin{isamarkuptxt}%
+\begin{isamarkuptxt}
The situation after clarify
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymLongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
-\end{isabelle}%
-\end{isamarkuptxt}%
-\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}%
-\begin{isamarkuptxt}%
+\begin{isabelle}
+\ 1.\ \isasymAnd x.\ x\ \isasymin \ well_formed_gterm\ arity\ \isasymLongrightarrow \isanewline
+\isaindent{\ 1.\ \isasymAnd x.\ }x\ \isasymin \ well_formed_gterm'\ arity%
+\end{isabelle}
+\end{isamarkuptxt}
+\isacommand{apply}\ (erule\ well_formed_gterm.induct)
+\begin{isamarkuptxt}
note the induction hypothesis!
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
-\end{isabelle}%
-\end{isamarkuptxt}%
+\begin{isabelle}
+\ 1.\ \isasymAnd x\ args\ f.\isanewline
+\isaindent{\ 1.\ \ \ \ }\isasymlbrakk \isasymforall t\isasymin set\ args.\isanewline
+\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ well_formed_gterm\ arity\ \isasymand \isanewline
+\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ well_formed_gterm'\ arity;\isanewline
+\isaindent{\ 1.\ \ \ \ \ \ \ }length\ args\ =\ arity\ f\isasymrbrakk \isanewline
+\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm'\ arity%
+\end{isabelle}
+\end{isamarkuptxt}
\isacommand{apply}\ auto\isanewline
\isacommand{done}\isanewline
\isanewline
\isanewline
\isanewline
-\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
+\isacommand{lemma}\ "well_formed_gterm'\ arity\ \isasymsubseteq \ well_formed_gterm\ arity"\isanewline
\isacommand{apply}\ clarify%
-\begin{isamarkuptxt}%
+\begin{isamarkuptxt}
The situation after clarify
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymLongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
-\end{isabelle}%
-\end{isamarkuptxt}%
-\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}%
-\begin{isamarkuptxt}%
+\begin{isabelle}
+\ 1.\ \isasymAnd x.\ x\ \isasymin \ well_formed_gterm'\ arity\ \isasymLongrightarrow \isanewline
+\isaindent{\ 1.\ \isasymAnd x.\ }x\ \isasymin \ well_formed_gterm\ arity%
+\end{isabelle}
+\end{isamarkuptxt}
+\isacommand{apply}\ (erule\ well_formed_gterm'.induct)
+\begin{isamarkuptxt}
note the induction hypothesis!
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
-\end{isabelle}%
-\end{isamarkuptxt}%
+\begin{isabelle}
+\ 1.\ \isasymAnd x\ args\ f.\isanewline
+\isaindent{\ 1.\ \ \ \ }\isasymlbrakk args\isanewline
+\isaindent{\ 1.\ \ \ \ \isasymlbrakk }\isasymin \ lists\isanewline
+\isaindent{\ 1.\ \ \ \ \isasymlbrakk \isasymin \ \ }(well_formed_gterm'\ arity\ \isasyminter \isanewline
+\isaindent{\ 1.\ \ \ \ \isasymlbrakk \isasymin \ \ (}\isacharbraceleft x.\ x\ \isasymin \ well_formed_gterm\ arity\isacharbraceright );\isanewline
+\isaindent{\ 1.\ \ \ \ \ \ \ }length\ args\ =\ arity\ f\isasymrbrakk \isanewline
+\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity%
+\end{isabelle}
+\end{isamarkuptxt}
\isacommand{apply}\ auto\isanewline
-\isacommand{done}%
-\begin{isamarkuptext}%
-\begin{isabelle}%
-\ \ \ \ \ lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B%
-\end{isabelle}%
-\end{isamarkuptext}%
+\isacommand{done}
+\begin{isamarkuptext}
+\begin{isabelle}
+\ \ \ \ \ lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B%
+\end{isabelle}
+\end{isamarkuptext}
%
-\begin{isamarkuptext}%
+\begin{isamarkuptext}
the rest isn't used: too complicated. OK for an exercise though.%
-\end{isamarkuptext}%
-\isacommand{consts}\ integer{\isacharunderscore}signature\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}integer{\isacharunderscore}op\ {\isacharasterisk}\ {\isacharparenleft}unit\ list\ {\isacharasterisk}\ unit{\isacharparenright}{\isacharparenright}\ set{\isachardoublequote}\isanewline
-\isacommand{inductive}\ {\isachardoublequote}integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
+\end{isamarkuptext}
+\isacommand{consts}\ integer_signature\ ::\ "(integer_op\ *\ (unit\ list\ *\ unit))\ set"\isanewline
+\isacommand{inductive}\ "integer_signature"\isanewline
\isakeyword{intros}\isanewline
-Number{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isacharparenleft}Number\ n{\isacharcomma}\ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
-UnaryMinus{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}UnaryMinus{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
-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
+Number:\ \ \ \ \ "(Number\ n,\ \ \ ([],\ ()))\ \isasymin \ integer_signature"\isanewline
+UnaryMinus:\ "(UnaryMinus,\ ([()],\ ()))\ \isasymin \ integer_signature"\isanewline
+Plus:\ \ \ \ \ \ \ "(Plus,\ \ \ \ \ \ \ ([(),()],\ ()))\ \isasymin \ integer_signature"\isanewline
\isanewline
\isanewline
-\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
-\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
+\isacommand{consts}\ well_typed_gterm\ ::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
+\isacommand{inductive}\ "well_typed_gterm\ sig"\isanewline
\isakeyword{intros}\isanewline
-step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline
-\ \ \ \ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}pair\ {\isasymin}\ set\ args{\isachardot}\ pair\ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isacharsemicolon}\ \isanewline
-\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline
-\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline
-\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
+step[intro!]:\ \isanewline
+\ \ \ \ "\isasymlbrakk \isasymforall pair\ \isasymin \ set\ args.\ pair\ \isasymin \ well_typed_gterm\ sig;\ \isanewline
+\ \ \ \ \ \ sig\ f\ =\ (map\ snd\ args,\ rtype)\isasymrbrakk \isanewline
+\ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ (map\ fst\ args),\ rtype)\ \isanewline
+\ \ \ \ \ \ \ \ \ \isasymin \ well_typed_gterm\ sig"\isanewline
\isanewline
-\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
-\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
+\isacommand{consts}\ well_typed_gterm'\ ::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
+\isacommand{inductive}\ "well_typed_gterm'\ sig"\isanewline
\isakeyword{intros}\isanewline
-step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline
-\ \ \ \ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists{\isacharparenleft}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isacharparenright}{\isacharsemicolon}\ \isanewline
-\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline
-\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline
-\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
-\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline
+step[intro!]:\ \isanewline
+\ \ \ \ "\isasymlbrakk args\ \isasymin \ lists(well_typed_gterm'\ sig);\ \isanewline
+\ \ \ \ \ \ sig\ f\ =\ (map\ snd\ args,\ rtype)\isasymrbrakk \isanewline
+\ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ (map\ fst\ args),\ rtype)\ \isanewline
+\ \ \ \ \ \ \ \ \ \isasymin \ well_typed_gterm'\ sig"\isanewline
+\isakeyword{monos}\ lists_mono\isanewline
\isanewline
\isanewline
-\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
+\isacommand{lemma}\ "well_typed_gterm\ sig\ \isasymsubseteq \ well_typed_gterm'\ sig"\isanewline
\isacommand{apply}\ clarify\isanewline
-\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isanewline
+\isacommand{apply}\ (erule\ well_typed_gterm.induct)\isanewline
\isacommand{apply}\ auto\isanewline
\isacommand{done}\isanewline
\isanewline
-\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
+\isacommand{lemma}\ "well_typed_gterm'\ sig\ \isasymsubseteq \ well_typed_gterm\ sig"\isanewline
\isacommand{apply}\ clarify\isanewline
-\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isanewline
+\isacommand{apply}\ (erule\ well_typed_gterm'.induct)\isanewline
\isacommand{apply}\ auto\isanewline
\isacommand{done}\isanewline
\isanewline
\isanewline
\isacommand{end}\isanewline
\isanewline
-\end{isabellebody}%
+\end{isabelle}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Inductive/even-example.tex Wed Feb 21 12:07:00 2001 +0100
+++ b/doc-src/TutorialI/Inductive/even-example.tex Wed Feb 21 12:57:55 2001 +0100
@@ -24,12 +24,11 @@
An inductive definition consists of introduction rules. The first one
above states that 0 is even; the second states that if $n$ is even, then so
-is
-$n+2$. Given this declaration, Isabelle generates a fixed point definition
-for \isa{even} and proves theorems about it. These theorems include the
-introduction rules specified in the declaration, an elimination rule for case
-analysis and an induction rule. We can refer to these theorems by
-automatically-generated names. Here are two examples:
+is~$n+2$. Given this declaration, Isabelle generates a fixed point
+definition for \isa{even} and proves theorems about it. These theorems
+include the introduction rules specified in the declaration, an elimination
+rule for case analysis and an induction rule. We can refer to these
+theorems by automatically-generated names. Here are two examples:
%
\begin{isabelle}
0\ \isasymin \ even
@@ -217,5 +216,92 @@
\isacommand{by}\ (blast\ dest:\ Suc_Suc_even_imp_even)
\end{isabelle}
-The even numbers example has shown how inductive definitions can be used.
-Later examples will show that they are actually worth using.
+
+\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/HOL\@.
+
+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 some suitable \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}
+%
+Just above we devoted some effort to reaching precisely
+this result. Yet we could have obtained it by a one-line declaration,
+dispensing with the lemma \isa{even_imp_even_minus_2}.
+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, then applied
+as an elimination rule.
+
+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.
+
+The even numbers example has shown how inductive definitions can be
+used. Later examples will show that they are actually worth using.