--- a/doc-src/HOL/HOL.tex Thu May 26 15:56:39 2011 +0200
+++ b/doc-src/HOL/HOL.tex Thu May 26 21:39:02 2011 +0200
@@ -2128,186 +2128,6 @@
\index{*recdef|)}
-\section{Inductive and coinductive definitions}
-\index{*inductive|(}
-\index{*coinductive|(}
-
-An {\bf inductive definition} specifies the least set~$R$ closed under given
-rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For
-example, a structural operational semantics is an inductive definition of an
-evaluation relation. Dually, a {\bf coinductive definition} specifies the
-greatest set~$R$ consistent with given rules. (Every element of~$R$ can be
-seen as arising by applying a rule to elements of~$R$.) An important example
-is using bisimulation relations to formalise equivalence of processes and
-infinite data structures.
-
-A theory file may contain any number of inductive and coinductive
-definitions. They may be intermixed with other declarations; in
-particular, the (co)inductive sets {\bf must} be declared separately as
-constants, and may have mixfix syntax or be subject to syntax translations.
-
-Each (co)inductive definition adds definitions to the theory and also
-proves some theorems. Each definition creates an \ML\ structure, which is a
-substructure of the main theory structure.
-
-This package is related to the ZF one, described in a separate
-paper,%
-\footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
- distributed with Isabelle.} %
-which you should refer to in case of difficulties. The package is simpler
-than ZF's thanks to HOL's extra-logical automatic type-checking. The types of
-the (co)inductive sets determine the domain of the fixedpoint definition, and
-the package does not have to use inference rules for type-checking.
-
-
-\subsection{The result structure}
-Many of the result structure's components have been discussed in the paper;
-others are self-explanatory.
-\begin{description}
-\item[\tt defs] is the list of definitions of the recursive sets.
-
-\item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
-
-\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
-the recursive sets, in the case of mutual recursion).
-
-\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
-the recursive sets. The rules are also available individually, using the
-names given them in the theory file.
-
-\item[\tt elims] is the list of elimination rule. This is for compatibility
- with ML scripts; within the theory the name is \texttt{cases}.
-
-\item[\tt elim] is the head of the list \texttt{elims}. This is for
- compatibility only.
-
-\item[\tt mk_cases] is a function to create simplified instances of {\tt
-elim} using freeness reasoning on underlying datatypes.
-\end{description}
-
-For an inductive definition, the result structure contains the
-rule \texttt{induct}. For a
-coinductive definition, it contains the rule \verb|coinduct|.
-
-Figure~\ref{def-result-fig} summarises the two result signatures,
-specifying the types of all these components.
-
-\begin{figure}
-\begin{ttbox}
-sig
-val defs : thm list
-val mono : thm
-val unfold : thm
-val intrs : thm list
-val elims : thm list
-val elim : thm
-val mk_cases : string -> thm
-{\it(Inductive definitions only)}
-val induct : thm
-{\it(coinductive definitions only)}
-val coinduct : thm
-end
-\end{ttbox}
-\hrule
-\caption{The {\ML} result of a (co)inductive definition} \label{def-result-fig}
-\end{figure}
-
-\subsection{The syntax of a (co)inductive definition}
-An inductive definition has the form
-\begin{ttbox}
-inductive {\it inductive sets}
- intrs {\it introduction rules}
- monos {\it monotonicity theorems}
-\end{ttbox}
-A coinductive definition is identical, except that it starts with the keyword
-\texttt{coinductive}.
-
-The \texttt{monos} section is optional; if present it is specified by a list
-of identifiers.
-
-\begin{itemize}
-\item The \textit{inductive sets} are specified by one or more strings.
-
-\item The \textit{introduction rules} specify one or more introduction rules in
- the form \textit{ident\/}~\textit{string}, where the identifier gives the name of
- the rule in the result structure.
-
-\item The \textit{monotonicity theorems} are required for each operator
- applied to a recursive set in the introduction rules. There {\bf must}
- be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
- premise $t\in M(R@i)$ in an introduction rule!
-
-\item The \textit{constructor definitions} contain definitions of constants
- appearing in the introduction rules. In most cases it can be omitted.
-\end{itemize}
-
-
-\subsection{*Monotonicity theorems}
-
-Each theory contains a default set of theorems that are used in monotonicity
-proofs. New rules can be added to this set via the \texttt{mono} attribute.
-Theory \texttt{Inductive} shows how this is done. In general, the following
-monotonicity theorems may be added:
-\begin{itemize}
-\item Theorems of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for proving
- monotonicity of inductive definitions whose introduction rules have premises
- involving terms such as $t\in M(R@i)$.
-\item Monotonicity theorems for logical operators, which are of the general form
- $\List{\cdots \to \cdots;~\ldots;~\cdots \to \cdots} \Imp
- \cdots \to \cdots$.
- For example, in the case of the operator $\lor$, the corresponding theorem is
- \[
- \infer{P@1 \lor P@2 \to Q@1 \lor Q@2}
- {P@1 \to Q@1 & P@2 \to Q@2}
- \]
-\item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g.
- \[
- (\lnot \lnot P) ~=~ P \qquad\qquad
- (\lnot (P \land Q)) ~=~ (\lnot P \lor \lnot Q)
- \]
-\item Equations for reducing complex operators to more primitive ones whose
- monotonicity can easily be proved, e.g.
- \[
- (P \to Q) ~=~ (\lnot P \lor Q) \qquad\qquad
- \mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \to P~x
- \]
-\end{itemize}
-
-\subsection{Example of an inductive definition}
-Two declarations, included in a theory file, define the finite powerset
-operator. First we declare the constant~\texttt{Fin}. Then we declare it
-inductively, with two introduction rules:
-\begin{ttbox}
-consts Fin :: 'a set => 'a set set
-inductive "Fin A"
- intrs
- emptyI "{\ttlbrace}{\ttrbrace} : Fin A"
- insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A"
-\end{ttbox}
-The resulting theory structure contains a substructure, called~\texttt{Fin}.
-It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs},
-and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction
-rule is \texttt{Fin.induct}.
-
-For another example, here is a theory file defining the accessible part of a
-relation. The paper \cite{paulson-CADE} discusses a ZF version of this
-example in more detail.
-\begin{ttbox}
-Acc = WF + Inductive +
-
-consts acc :: "('a * 'a)set => 'a set" (* accessible part *)
-
-inductive "acc r"
- intrs
- accI "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
-
-end
-\end{ttbox}
-The Isabelle distribution contains many other inductive definitions.
-
-\index{*coinductive|)} \index{*inductive|)}
-
-
\section{Example: Cantor's Theorem}\label{sec:hol-cantor}
Cantor's Theorem states that every set has more subsets than it has
elements. It has become a favourite example in higher-order logic since
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 26 15:56:39 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 26 21:39:02 2011 +0200
@@ -6,28 +6,31 @@
section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}
-text {*
- An \textbf{inductive definition} specifies the least predicate (or
- set) @{text R} closed under given rules: applying a rule to elements
- of @{text R} yields a result within @{text R}. For example, a
- structural operational semantics is an inductive definition of an
- evaluation relation.
+text {* An \emph{inductive definition} specifies the least predicate
+ or set @{text R} closed under given rules: applying a rule to
+ elements of @{text R} yields a result within @{text R}. For
+ example, a structural operational semantics is an inductive
+ definition of an evaluation relation.
- Dually, a \textbf{coinductive definition} specifies the greatest
- predicate~/ set @{text R} that is consistent with given rules: every
- element of @{text R} can be seen as arising by applying a rule to
- elements of @{text R}. An important example is using bisimulation
- relations to formalise equivalence of processes and infinite data
- structures.
-
- \medskip The HOL package is related to the ZF one, which is
- described in a separate paper,\footnote{It appeared in CADE
- \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
- which you should refer to in case of difficulties. The package is
- simpler than that of ZF thanks to implicit type-checking in HOL.
- The types of the (co)inductive predicates (or sets) determine the
- domain of the fixedpoint definition, and the package does not have
- to use inference rules for type-checking.
+ Dually, a \emph{coinductive definition} specifies the greatest
+ predicate or set @{text R} that is consistent with given rules:
+ every element of @{text R} can be seen as arising by applying a rule
+ to elements of @{text R}. An important example is using
+ bisimulation relations to formalise equivalence of processes and
+ infinite data structures.
+
+ Both inductive and coinductive definitions are based on the
+ Knaster-Tarski fixed-point theorem for complete lattices. The
+ collection of introduction rules given by the user determines a
+ functor on subsets of set-theoretic relations. The required
+ monotonicity of the recursion scheme is proven as a prerequisite to
+ the fixed-point definition and the resulting consequences. This
+ works by pushing inclusion through logical connectives and any other
+ operator that might be wrapped around recursive occurrences of the
+ defined relation: there must be a monotonicity theorem of the form
+ @{text "A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B"}, for each premise @{text "\<M> R t"} in an
+ introduction rule. The default rule declarations of Isabelle/HOL
+ already take care of most common situations.
\begin{matharray}{rcl}
@{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@@ -40,8 +43,9 @@
@{rail "
(@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
@@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
- @{syntax target}? @{syntax \"fixes\"} (@'for' @{syntax \"fixes\"})? \\
- (@'where' clauses)? (@'monos' @{syntax thmrefs})?
+ @{syntax target}? \\
+ @{syntax \"fixes\"} (@'for' @{syntax \"fixes\"})? (@'where' clauses)? \\
+ (@'monos' @{syntax thmrefs})?
;
clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
;
@@ -51,23 +55,34 @@
\begin{description}
\item @{command (HOL) "inductive"} and @{command (HOL)
- "coinductive"} define (co)inductive predicates from the
- introduction rules given in the @{keyword "where"} part. The
- optional @{keyword "for"} part contains a list of parameters of the
- (co)inductive predicates that remain fixed throughout the
- definition. The optional @{keyword "monos"} section contains
+ "coinductive"} define (co)inductive predicates from the introduction
+ rules.
+
+ The propositions given as @{text "clauses"} in the @{keyword
+ "where"} part are either rules of the usual @{text "\<And>/\<Longrightarrow>"} format
+ (with arbitrary nesting), or equalities using @{text "\<equiv>"}. The
+ latter specifies extra-logical abbreviations in the sense of
+ @{command_ref abbreviation}. Introducing abstract syntax
+ simultaneously with the actual introduction rules is occasionally
+ useful for complex specifications.
+
+ The optional @{keyword "for"} part contains a list of parameters of
+ the (co)inductive predicates that remain fixed throughout the
+ definition, in contrast to arguments of the relation that may vary
+ in each occurrence within the given @{text "clauses"}.
+
+ The optional @{keyword "monos"} declaration contains additional
\emph{monotonicity theorems}, which are required for each operator
- applied to a recursive set in the introduction rules. There
- \emph{must} be a theorem of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"},
- for each premise @{text "M R\<^sub>i t"} in an introduction rule!
+ applied to a recursive set in the introduction rules.
\item @{command (HOL) "inductive_set"} and @{command (HOL)
- "coinductive_set"} are wrappers for to the previous commands,
- allowing the definition of (co)inductive sets.
+ "coinductive_set"} are wrappers for to the previous commands for
+ native HOL predicates. This allows to define (co)inductive sets,
+ where multiple arguments are simulated via tuples.
- \item @{attribute (HOL) mono} declares monotonicity rules. These
- rule are involved in the automated monotonicity proof of @{command
- (HOL) "inductive"}.
+ \item @{attribute (HOL) mono} declares monotonicity rules in the
+ context. These rule are involved in the automated monotonicity
+ proof of the above inductive and coinductive definitions.
\end{description}
*}
@@ -75,9 +90,8 @@
subsection {* Derived rules *}
-text {*
- Each (co)inductive definition @{text R} adds definitions to the
- theory and also proves some theorems:
+text {* A (co)inductive definition of @{text R} provides the following
+ main theorems:
\begin{description}
@@ -104,18 +118,17 @@
subsection {* Monotonicity theorems *}
-text {*
- Each theory contains a default set of theorems that are used in
- monotonicity proofs. New rules can be added to this set via the
- @{attribute (HOL) mono} attribute. The HOL theory @{text Inductive}
- shows how this is done. In general, the following monotonicity
- theorems may be added:
+text {* The context maintains a default set of theorems that are used
+ in monotonicity proofs. New rules can be declared via the
+ @{attribute (HOL) mono} attribute. See the main Isabelle/HOL
+ sources for some examples. The general format of such monotonicity
+ theorems is as follows:
\begin{itemize}
- \item Theorems of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"}, for proving
+ \item Theorems of the form @{text "A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B"}, for proving
monotonicity of inductive definitions whose introduction rules have
- premises involving terms such as @{text "M R\<^sub>i t"}.
+ premises involving terms such as @{text "\<M> R t"}.
\item Monotonicity theorems for logical operators, which are of the
general form @{text "(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>"}. For example, in
@@ -139,9 +152,43 @@
\]
\end{itemize}
+*}
- %FIXME: Example of an inductive definition
-*}
+subsubsection {* Examples *}
+
+text {* The finite powerset operator can be defined inductively like this: *}
+
+inductive_set Fin :: "'a set \<Rightarrow> 'a set set" for A :: "'a set"
+where
+ empty: "{} \<in> Fin A"
+| insert: "a \<in> A \<Longrightarrow> B \<in> Fin A \<Longrightarrow> insert a B \<in> Fin A"
+
+text {* The accessible part of a relation is defined as follows: *}
+
+inductive acc :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
+where acc: "(\<And>y. y \<prec> x \<Longrightarrow> acc r y) \<Longrightarrow> acc r x"
+
+text {* Common logical connectives can be easily characterized as
+non-recursive inductive definitions with parameters, but without
+arguments. *}
+
+inductive AND for A B :: bool
+where "A \<Longrightarrow> B \<Longrightarrow> AND A B"
+
+inductive OR for A B :: bool
+where "A \<Longrightarrow> OR A B"
+ | "B \<Longrightarrow> OR A B"
+
+inductive EXISTS for B :: "'a \<Rightarrow> bool"
+where "B a \<Longrightarrow> EXISTS B"
+
+text {* Here the @{text "cases"} or @{text "induct"} rules produced by
+ the @{command inductive} package coincide with the expected
+ elimination rules for Natural Deduction. Already in the original
+ article by Gerhard Gentzen \cite{Gentzen:1935} there is a hint that
+ each connective can be characterized by its introductions, and the
+ elimination can be constructed systematically. *}
section {* Recursive functions \label{sec:recursion} *}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 26 15:56:39 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 26 21:39:02 2011 +0200
@@ -27,27 +27,31 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-An \textbf{inductive definition} specifies the least predicate (or
- set) \isa{R} closed under given rules: applying a rule to elements
- of \isa{R} yields a result within \isa{R}. For example, a
- structural operational semantics is an inductive definition of an
- evaluation relation.
+An \emph{inductive definition} specifies the least predicate
+ or set \isa{R} closed under given rules: applying a rule to
+ elements of \isa{R} yields a result within \isa{R}. For
+ example, a structural operational semantics is an inductive
+ definition of an evaluation relation.
- Dually, a \textbf{coinductive definition} specifies the greatest
- predicate~/ set \isa{R} that is consistent with given rules: every
- element of \isa{R} can be seen as arising by applying a rule to
- elements of \isa{R}. An important example is using bisimulation
- relations to formalise equivalence of processes and infinite data
- structures.
-
- \medskip The HOL package is related to the ZF one, which is
- described in a separate paper,\footnote{It appeared in CADE
- \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
- which you should refer to in case of difficulties. The package is
- simpler than that of ZF thanks to implicit type-checking in HOL.
- The types of the (co)inductive predicates (or sets) determine the
- domain of the fixedpoint definition, and the package does not have
- to use inference rules for type-checking.
+ Dually, a \emph{coinductive definition} specifies the greatest
+ predicate or set \isa{R} that is consistent with given rules:
+ every element of \isa{R} can be seen as arising by applying a rule
+ to elements of \isa{R}. An important example is using
+ bisimulation relations to formalise equivalence of processes and
+ infinite data structures.
+
+ Both inductive and coinductive definitions are based on the
+ Knaster-Tarski fixed-point theorem for complete lattices. The
+ collection of introduction rules given by the user determines a
+ functor on subsets of set-theoretic relations. The required
+ monotonicity of the recursion scheme is proven as a prerequisite to
+ the fixed-point definition and the resulting consequences. This
+ works by pushing inclusion through logical connectives and any other
+ operator that might be wrapped around recursive occurrences of the
+ defined relation: there must be a monotonicity theorem of the form
+ \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ B{\isaliteral{22}{\isachardoublequote}}}, for each premise \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4D3E}{\isasymM}}\ R\ t{\isaliteral{22}{\isachardoublequote}}} in an
+ introduction rule. The default rule declarations of Isabelle/HOL
+ already take care of most common situations.
\begin{matharray}{rcl}
\indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
@@ -58,7 +62,7 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{7}{}
+\rail@begin{10}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
\rail@nextbar{1}
@@ -72,20 +76,21 @@
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
\rail@endbar
+\rail@cr{5}
\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
\rail@bar
-\rail@nextbar{1}
+\rail@nextbar{6}
\rail@term{\isa{\isakeyword{for}}}[]
\rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
\rail@endbar
-\rail@cr{5}
\rail@bar
\rail@nextbar{6}
\rail@term{\isa{\isakeyword{where}}}[]
\rail@nont{\isa{clauses}}[]
\rail@endbar
+\rail@cr{8}
\rail@bar
-\rail@nextbar{6}
+\rail@nextbar{9}
\rail@term{\isa{\isakeyword{monos}}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@endbar
@@ -115,21 +120,32 @@
\begin{description}
- \item \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}} define (co)inductive predicates from the
- introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part. The
- optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the
- (co)inductive predicates that remain fixed throughout the
- definition. The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains
+ \item \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}} define (co)inductive predicates from the introduction
+ rules.
+
+ The propositions given as \isa{{\isaliteral{22}{\isachardoublequote}}clauses{\isaliteral{22}{\isachardoublequote}}} in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part are either rules of the usual \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} format
+ (with arbitrary nesting), or equalities using \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}}. The
+ latter specifies extra-logical abbreviations in the sense of
+ \indexref{}{command}{abbreviation}\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}. Introducing abstract syntax
+ simultaneously with the actual introduction rules is occasionally
+ useful for complex specifications.
+
+ The optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of
+ the (co)inductive predicates that remain fixed throughout the
+ definition, in contrast to arguments of the relation that may vary
+ in each occurrence within the given \isa{{\isaliteral{22}{\isachardoublequote}}clauses{\isaliteral{22}{\isachardoublequote}}}.
+
+ The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} declaration contains additional
\emph{monotonicity theorems}, which are required for each operator
- applied to a recursive set in the introduction rules. There
- \emph{must} be a theorem of the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ M\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ M\ B{\isaliteral{22}{\isachardoublequote}}},
- for each premise \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}} in an introduction rule!
+ applied to a recursive set in the introduction rules.
- \item \hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}} are wrappers for to the previous commands,
- allowing the definition of (co)inductive sets.
+ \item \hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}} are wrappers for to the previous commands for
+ native HOL predicates. This allows to define (co)inductive sets,
+ where multiple arguments are simulated via tuples.
- \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules. These
- rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}.
+ \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules in the
+ context. These rule are involved in the automated monotonicity
+ proof of the above inductive and coinductive definitions.
\end{description}%
\end{isamarkuptext}%
@@ -140,8 +156,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Each (co)inductive definition \isa{R} adds definitions to the
- theory and also proves some theorems:
+A (co)inductive definition of \isa{R} provides the following
+ main theorems:
\begin{description}
@@ -170,17 +186,17 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Each theory contains a default set of theorems that are used in
- monotonicity proofs. New rules can be added to this set via the
- \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute. The HOL theory \isa{Inductive}
- shows how this is done. In general, the following monotonicity
- theorems may be added:
+The context maintains a default set of theorems that are used
+ in monotonicity proofs. New rules can be declared via the
+ \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute. See the main Isabelle/HOL
+ sources for some examples. The general format of such monotonicity
+ theorems is as follows:
\begin{itemize}
- \item Theorems of the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ M\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ M\ B{\isaliteral{22}{\isachardoublequote}}}, for proving
+ \item Theorems of the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{5C3C4D3E}{\isasymM}}\ B{\isaliteral{22}{\isachardoublequote}}}, for proving
monotonicity of inductive definitions whose introduction rules have
- premises involving terms such as \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}}.
+ premises involving terms such as \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4D3E}{\isasymM}}\ R\ t{\isaliteral{22}{\isachardoublequote}}}.
\item Monotonicity theorems for logical operators, which are of the
general form \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}. For example, in
@@ -203,9 +219,56 @@
\isa{{\isaliteral{22}{\isachardoublequote}}Ball\ A\ P\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequote}}}
\]
- \end{itemize}
-
- %FIXME: Example of an inductive definition%
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The finite powerset operator can be defined inductively like this:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse%
+\ Fin\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{for}\ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+\ \ empty{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Fin\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ insert{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Fin\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ insert\ a\ B\ {\isaliteral{5C3C696E3E}{\isasymin}}\ Fin\ A{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+The accessible part of a relation is defined as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive}\isamarkupfalse%
+\ acc\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{for}\ r\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C707265633E}{\isasymprec}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\isakeyword{where}\ acc{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}y{\isaliteral{2E}{\isachardot}}\ y\ {\isaliteral{5C3C707265633E}{\isasymprec}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ acc\ r\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ acc\ r\ x{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+Common logical connectives can be easily characterized as
+non-recursive inductive definitions with parameters, but without
+arguments.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive}\isamarkupfalse%
+\ AND\ \isakeyword{for}\ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\isanewline
+\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ AND\ A\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+\isacommand{inductive}\isamarkupfalse%
+\ OR\ \isakeyword{for}\ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\isanewline
+\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ OR\ A\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ OR\ A\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+\isacommand{inductive}\isamarkupfalse%
+\ EXISTS\ \isakeyword{for}\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ EXISTS\ B{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+Here the \isa{{\isaliteral{22}{\isachardoublequote}}cases{\isaliteral{22}{\isachardoublequote}}} or \isa{{\isaliteral{22}{\isachardoublequote}}induct{\isaliteral{22}{\isachardoublequote}}} rules produced by
+ the \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} package coincide with the expected
+ elimination rules for Natural Deduction. Already in the original
+ article by Gerhard Gentzen \cite{Gentzen:1935} there is a hint that
+ each connective can be characterized by its introductions, and the
+ elimination can be constructed systematically.%
\end{isamarkuptext}%
\isamarkuptrue%
%