# HG changeset patch # User wenzelm # Date 1306438742 -7200 # Node ID 68bc69bdce8828d243bd6c45c04ef4305daed3aa # Parent a5bbc11474f9c3b41f39a3889f3474d62ca8f198 updated and re-unified (co)inductive definitions in HOL; modernized examples; diff -r a5bbc11474f9 -r 68bc69bdce88 doc-src/HOL/HOL.tex --- 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 diff -r a5bbc11474f9 -r 68bc69bdce88 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 \ B \ \ A \ \ B"}, for each premise @{text "\ 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 \ 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 "\/\"} format + (with arbitrary nesting), or equalities using @{text "\"}. 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 \ B \ M A \ 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 \ B \ M A \ M B"}, for proving + \item Theorems of the form @{text "A \ B \ \ A \ \ 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 "\ R t"}. \item Monotonicity theorems for logical operators, which are of the general form @{text "(\ \ \) \ \ (\ \ \) \ \ \ \"}. 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 \ 'a set set" for A :: "'a set" +where + empty: "{} \ Fin A" +| insert: "a \ A \ B \ Fin A \ insert a B \ Fin A" + +text {* The accessible part of a relation is defined as follows: *} + +inductive acc :: "('a \ 'a \ bool) \ 'a \ bool" + for r :: "'a \ 'a \ bool" (infix "\" 50) +where acc: "(\y. y \ x \ acc r y) \ 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 \ B \ AND A B" + +inductive OR for A B :: bool +where "A \ OR A B" + | "B \ OR A B" + +inductive EXISTS for B :: "'a \ bool" +where "B a \ 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} *} diff -r a5bbc11474f9 -r 68bc69bdce88 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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% %