--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Feb 02 16:07:25 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Feb 02 16:38:15 2012 +0100
@@ -60,11 +60,20 @@
section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}
-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.
+text {*
+ \begin{matharray}{rcl}
+ @{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{attribute_def (HOL) mono} & : & @{text attribute} \\
+ \end{matharray}
+
+ 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 \emph{coinductive definition} specifies the greatest
predicate or set @{text R} that is consistent with given rules:
@@ -86,14 +95,6 @@
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"} \\
- @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{attribute_def (HOL) mono} & : & @{text attribute} \\
- \end{matharray}
-
@{rail "
(@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
@@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
@@ -626,15 +627,15 @@
subsection {* Old-style recursive function definitions (TFL) *}
text {*
- The old TFL commands @{command (HOL) "recdef"} and @{command (HOL)
- "recdef_tc"} for defining recursive are mostly obsolete; @{command
- (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
-
\begin{matharray}{rcl}
@{command_def (HOL) "recdef"} & : & @{text "theory \<rightarrow> theory)"} \\
@{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
\end{matharray}
+ The old TFL commands @{command (HOL) "recdef"} and @{command (HOL)
+ "recdef_tc"} for defining recursive are mostly obsolete; @{command
+ (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
+
@{rail "
@@{command (HOL) recdef} ('(' @'permissive' ')')? \\
@{syntax name} @{syntax term} (@{syntax prop} +) hints?
@@ -1057,8 +1058,13 @@
section {* Typedef axiomatization \label{sec:hol-typedef} *}
-text {* A Gordon/HOL-style type definition is a certain axiom scheme
- that identifies a new type with a subset of an existing type. More
+text {*
+ \begin{matharray}{rcl}
+ @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
+ \end{matharray}
+
+ A Gordon/HOL-style type definition is a certain axiom scheme that
+ identifies a new type with a subset of an existing type. More
precisely, the new type is defined by exhibiting an existing type
@{text \<tau>}, a set @{text "A :: \<tau> set"}, and a theorem that proves
@{prop "\<exists>x. x \<in> A"}. Thus @{text A} is a non-empty subset of @{text
@@ -1078,10 +1084,6 @@
type_synonym} from Isabelle/Pure merely introduces syntactic
abbreviations, without any logical significance.
- \begin{matharray}{rcl}
- @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- \end{matharray}
-
@{rail "
@@{command (HOL) typedef} alt_name? abs_type '=' rep_set
;
@@ -1251,12 +1253,6 @@
section {* Quotient types *}
text {*
- The quotient package defines a new quotient type given a raw type
- and a partial equivalence relation.
- It also includes automation for transporting definitions and theorems.
- It can automatically produce definitions and theorems on the quotient type,
- given the corresponding constants and facts on the raw type.
-
\begin{matharray}{rcl}
@{command_def (HOL) "quotient_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
@{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
@@ -1265,6 +1261,12 @@
@{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\
\end{matharray}
+ The quotient package defines a new quotient type given a raw type
+ and a partial equivalence relation. It also includes automation for
+ transporting definitions and theorems. It can automatically produce
+ definitions and theorems on the quotient type, given the
+ corresponding constants and facts on the raw type.
+
@{rail "
@@{command (HOL) quotient_type} (spec + @'and');
@@ -1282,21 +1284,24 @@
\begin{description}
- \item @{command (HOL) "quotient_type"} defines quotient types. The injection from a quotient type
- to a raw type is called @{text rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL)
+ \item @{command (HOL) "quotient_type"} defines quotient types. The
+ injection from a quotient type to a raw type is called @{text
+ rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL)
"morphisms"} specification provides alternative names.
- \item @{command (HOL) "quotient_definition"} defines a constant on the quotient type.
+ \item @{command (HOL) "quotient_definition"} defines a constant on
+ the quotient type.
- \item @{command (HOL) "print_quotmaps"} prints quotient map functions.
+ \item @{command (HOL) "print_quotmaps"} prints quotient map
+ functions.
\item @{command (HOL) "print_quotients"} prints quotients.
\item @{command (HOL) "print_quotconsts"} prints quotient constants.
\end{description}
+*}
-*}
section {* Coercive subtyping *}
@@ -1307,6 +1312,11 @@
@{attribute_def (HOL) coercion_map} & : & @{text attribute} \\
\end{matharray}
+ Coercive subtyping allows the user to omit explicit type
+ conversions, also called \emph{coercions}. Type inference will add
+ them as necessary when parsing a term. See
+ \cite{traytel-berghofer-nipkow-2011} for details.
+
@{rail "
@@{attribute (HOL) coercion} (@{syntax term})?
;
@@ -1316,44 +1326,35 @@
;
"}
- Coercive subtyping allows the user to omit explicit type conversions,
- also called \emph{coercions}. Type inference will add them as
- necessary when parsing a term. See
- \cite{traytel-berghofer-nipkow-2011} for details.
-
\begin{description}
\item @{attribute (HOL) "coercion"}~@{text "f"} registers a new
- coercion function @{text "f :: \<sigma>\<^isub>1 \<Rightarrow>
- \<sigma>\<^isub>2"} where @{text "\<sigma>\<^isub>1"} and @{text
- "\<sigma>\<^isub>2"} are nullary type constructors. Coercions are
- composed by the inference algorithm if needed. Note that the type
- inference algorithm is complete only if the registered coercions form
- a lattice.
+ coercion function @{text "f :: \<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2"} where @{text "\<sigma>\<^isub>1"} and
+ @{text "\<sigma>\<^isub>2"} are type constructors without arguments. Coercions are
+ composed by the inference algorithm if needed. Note that the type
+ inference algorithm is complete only if the registered coercions
+ form a lattice.
-
- \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a new
- map function to lift coercions through type constructors. The function
- @{text "map"} must conform to the following type pattern
+ \item @{attribute (HOL) "coercion_map"}~@{text "map"} registers a
+ new map function to lift coercions through type constructors. The
+ function @{text "map"} must conform to the following type pattern
\begin{matharray}{lll}
@{text "map"} & @{text "::"} &
@{text "f\<^isub>1 \<Rightarrow> \<dots> \<Rightarrow> f\<^isub>n \<Rightarrow> (\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n) t \<Rightarrow> (\<beta>\<^isub>1, \<dots>, \<beta>\<^isub>n) t"} \\
\end{matharray}
- where @{text "t"} is a type constructor and @{text "f\<^isub>i"} is of
- type @{text "\<alpha>\<^isub>i \<Rightarrow> \<beta>\<^isub>i"} or
- @{text "\<beta>\<^isub>i \<Rightarrow> \<alpha>\<^isub>i"}.
- Registering a map function overwrites any existing map function for
- this particular type constructor.
-
+ where @{text "t"} is a type constructor and @{text "f\<^isub>i"} is of type
+ @{text "\<alpha>\<^isub>i \<Rightarrow> \<beta>\<^isub>i"} or @{text "\<beta>\<^isub>i \<Rightarrow> \<alpha>\<^isub>i"}. Registering a map function
+ overwrites any existing map function for this particular type
+ constructor.
\item @{attribute (HOL) "coercion_enabled"} enables the coercion
inference algorithm.
\end{description}
+*}
-*}
section {* Arithmetic proof support *}
@@ -1364,18 +1365,22 @@
@{attribute_def (HOL) arith_split} & : & @{text attribute} \\
\end{matharray}
- The @{method (HOL) arith} method decides linear arithmetic problems
- (on types @{text nat}, @{text int}, @{text real}). Any current
- facts are inserted into the goal before running the procedure.
+ \begin{description}
- The @{attribute (HOL) arith} attribute declares facts that are
- always supplied to the arithmetic provers implicitly.
+ \item @{method (HOL) arith} decides linear arithmetic problems (on
+ types @{text nat}, @{text int}, @{text real}). Any current facts
+ are inserted into the goal before running the procedure.
- The @{attribute (HOL) arith_split} attribute declares case split
+ \item @{attribute (HOL) arith} declares facts that are supplied to
+ the arithmetic provers implicitly.
+
+ \item @{attribute (HOL) arith_split} attribute declares case split
rules to be expanded before @{method (HOL) arith} is invoked.
- Note that a simpler (but faster) arithmetic prover is
- already invoked by the Simplifier.
+ \end{description}
+
+ Note that a simpler (but faster) arithmetic prover is already
+ invoked by the Simplifier.
*}
@@ -1390,10 +1395,12 @@
@@{method (HOL) iprover} ( @{syntax rulemod} * )
"}
- The @{method (HOL) iprover} method performs intuitionistic proof
- search, depending on specifically declared rules from the context,
- or given as explicit arguments. Chained facts are inserted into the
- goal before commencing proof search.
+ \begin{description}
+
+ \item @{method (HOL) iprover} performs intuitionistic proof search,
+ depending on specifically declared rules from the context, or given
+ as explicit arguments. Chained facts are inserted into the goal
+ before commencing proof search.
Rules need to be classified as @{attribute (Pure) intro},
@{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
@@ -1403,8 +1410,11 @@
single-step @{method (Pure) rule} method still observes these). An
explicit weight annotation may be given as well; otherwise the
number of rule premises will be taken into account here.
+
+ \end{description}
*}
+
section {* Model Elimination and Resolution *}
text {*
@@ -1417,22 +1427,28 @@
@@{method (HOL) meson} @{syntax thmrefs}?
;
- @@{method (HOL) metis} ( '(' ('partial_types' | 'full_types' | 'no_types'
- | @{syntax name}) ')' )? @{syntax thmrefs}?
+ @@{method (HOL) metis}
+ ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
+ @{syntax thmrefs}?
"}
- The @{method (HOL) meson} method implements Loveland's model elimination
- procedure \cite{loveland-78}. See @{file "~~/src/HOL/ex/Meson_Test.thy"} for
- examples.
+ \begin{description}
+
+ \item @{method (HOL) meson} implements Loveland's model elimination
+ procedure \cite{loveland-78}. See @{file
+ "~~/src/HOL/ex/Meson_Test.thy"} for examples.
- The @{method (HOL) metis} method combines ordered resolution and ordered
- paramodulation to find first-order (or mildly higher-order) proofs. The first
- optional argument specifies a type encoding; see the Sledgehammer manual
- \cite{isabelle-sledgehammer} for details. The @{file
- "~~/src/HOL/Metis_Examples"} directory contains several small theories
- developed to a large extent using Metis.
+ \item @{method (HOL) metis} combines ordered resolution and ordered
+ paramodulation to find first-order (or mildly higher-order) proofs.
+ The first optional argument specifies a type encoding; see the
+ Sledgehammer manual \cite{isabelle-sledgehammer} for details. The
+ directory @{file "~~/src/HOL/Metis_Examples"} contains several small
+ theories developed to a large extent using @{method (HOL) metis}.
+
+ \end{description}
*}
+
section {* Coherent Logic *}
text {*
@@ -1444,11 +1460,14 @@
@@{method (HOL) coherent} @{syntax thmrefs}?
"}
- The @{method (HOL) coherent} method solves problems of
- \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
- applications in confluence theory, lattice theory and projective
- geometry. See @{file "~~/src/HOL/ex/Coherent.thy"} for some
- examples.
+ \begin{description}
+
+ \item @{method (HOL) coherent} solves problems of \emph{Coherent
+ Logic} \cite{Bezem-Coquand:2005}, which covers applications in
+ confluence theory, lattice theory and projective geometry. See
+ @{file "~~/src/HOL/ex/Coherent.thy"} for some examples.
+
+ \end{description}
*}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 02 16:07:25 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 02 16:38:15 2012 +0100
@@ -83,11 +83,19 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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.
+\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}}} \\
+ \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
+ \end{matharray}
+
+ 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 \emph{coinductive definition} specifies the greatest
predicate or set \isa{R} that is consistent with given rules:
@@ -109,14 +117,6 @@
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}}} \\
- \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
- \end{matharray}
-
\begin{railoutput}
\rail@begin{10}{}
\rail@bar
@@ -881,13 +881,13 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}} for defining recursive are mostly obsolete; \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} or \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} should be used instead.
-
- \begin{matharray}{rcl}
+\begin{matharray}{rcl}
\indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
\end{matharray}
+ The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}} for defining recursive are mostly obsolete; \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} or \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} should be used instead.
+
\begin{railoutput}
\rail@begin{5}{}
\rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
@@ -1487,8 +1487,12 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A Gordon/HOL-style type definition is a certain axiom scheme
- that identifies a new type with a subset of an existing type. More
+\begin{matharray}{rcl}
+ \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+ \end{matharray}
+
+ A Gordon/HOL-style type definition is a certain axiom scheme that
+ identifies a new type with a subset of an existing type. More
precisely, the new type is defined by exhibiting an existing type
\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, a set \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ set{\isaliteral{22}{\isachardoublequote}}}, and a theorem that proves
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequote}}}. Thus \isa{A} is a non-empty subset of \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, and the new type denotes this subset. New functions are
@@ -1506,10 +1510,6 @@
of HOL models by construction. Note that \indexref{}{command}{type\_synonym}\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}} from Isabelle/Pure merely introduces syntactic
abbreviations, without any logical significance.
- \begin{matharray}{rcl}
- \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
- \end{matharray}
-
\begin{railoutput}
\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
@@ -1768,13 +1768,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The quotient package defines a new quotient type given a raw type
- and a partial equivalence relation.
- It also includes automation for transporting definitions and theorems.
- It can automatically produce definitions and theorems on the quotient type,
- given the corresponding constants and facts on the raw type.
-
- \begin{matharray}{rcl}
+\begin{matharray}{rcl}
\indexdef{HOL}{command}{quotient\_type}\hypertarget{command.HOL.quotient-type}{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
\indexdef{HOL}{command}{quotient\_definition}\hypertarget{command.HOL.quotient-definition}{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
\indexdef{HOL}{command}{print\_quotmaps}\hypertarget{command.HOL.print-quotmaps}{\hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\
@@ -1782,6 +1776,12 @@
\indexdef{HOL}{command}{print\_quotconsts}\hypertarget{command.HOL.print-quotconsts}{\hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\
\end{matharray}
+ The quotient package defines a new quotient type given a raw type
+ and a partial equivalence relation. It also includes automation for
+ transporting definitions and theorems. It can automatically produce
+ definitions and theorems on the quotient type, given the
+ corresponding constants and facts on the raw type.
+
\begin{railoutput}
\rail@begin{2}{}
\rail@term{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
@@ -1851,12 +1851,14 @@
\begin{description}
- \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. The injection from a quotient type
- to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.
+ \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. The
+ injection from a quotient type to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.
- \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type.
+ \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on
+ the quotient type.
- \item \hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}} prints quotient map functions.
+ \item \hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}} prints quotient map
+ functions.
\item \hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}} prints quotients.
@@ -1877,6 +1879,11 @@
\indexdef{HOL}{attribute}{coercion\_map}\hypertarget{attribute.HOL.coercion-map}{\hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}} & : & \isa{attribute} \\
\end{matharray}
+ Coercive subtyping allows the user to omit explicit type
+ conversions, also called \emph{coercions}. Type inference will add
+ them as necessary when parsing a term. See
+ \cite{traytel-berghofer-nipkow-2011} for details.
+
\begin{railoutput}
\rail@begin{2}{}
\rail@term{\hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}}[]
@@ -1898,35 +1905,28 @@
\end{railoutput}
- Coercive subtyping allows the user to omit explicit type conversions,
- also called \emph{coercions}. Type inference will add them as
- necessary when parsing a term. See
- \cite{traytel-berghofer-nipkow-2011} for details.
-
\begin{description}
\item \hyperlink{attribute.HOL.coercion}{\mbox{\isa{coercion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} registers a new
- coercion function \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} where \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} are nullary type constructors. Coercions are
- composed by the inference algorithm if needed. Note that the type
- inference algorithm is complete only if the registered coercions form
- a lattice.
+ coercion function \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} where \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} and
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} are type constructors without arguments. Coercions are
+ composed by the inference algorithm if needed. Note that the type
+ inference algorithm is complete only if the registered coercions
+ form a lattice.
-
- \item \hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}~\isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} registers a new
- map function to lift coercions through type constructors. The function
- \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} must conform to the following type pattern
+ \item \hyperlink{attribute.HOL.coercion-map}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}map}}}~\isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} registers a
+ new map function to lift coercions through type constructors. The
+ function \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} must conform to the following type pattern
\begin{matharray}{lll}
\isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
\isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ f\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} \\
\end{matharray}
- where \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is a type constructor and \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} is of
- type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} or
- \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}.
- Registering a map function overwrites any existing map function for
- this particular type constructor.
-
+ where \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is a type constructor and \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} is of type
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}. Registering a map function
+ overwrites any existing map function for this particular type
+ constructor.
\item \hyperlink{attribute.HOL.coercion-enabled}{\mbox{\isa{coercion{\isaliteral{5F}{\isacharunderscore}}enabled}}} enables the coercion
inference algorithm.
@@ -1946,18 +1946,22 @@
\indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}}} & : & \isa{attribute} \\
\end{matharray}
- The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems
- (on types \isa{nat}, \isa{int}, \isa{real}). Any current
- facts are inserted into the goal before running the procedure.
+ \begin{description}
- The \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} attribute declares facts that are
- always supplied to the arithmetic provers implicitly.
+ \item \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} decides linear arithmetic problems (on
+ types \isa{nat}, \isa{int}, \isa{real}). Any current facts
+ are inserted into the goal before running the procedure.
- The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}} attribute declares case split
+ \item \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} declares facts that are supplied to
+ the arithmetic provers implicitly.
+
+ \item \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}} attribute declares case split
rules to be expanded before \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} is invoked.
- Note that a simpler (but faster) arithmetic prover is
- already invoked by the Simplifier.%
+ \end{description}
+
+ Note that a simpler (but faster) arithmetic prover is already
+ invoked by the Simplifier.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1981,10 +1985,12 @@
\end{railoutput}
- The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
- search, depending on specifically declared rules from the context,
- or given as explicit arguments. Chained facts are inserted into the
- goal before commencing proof search.
+ \begin{description}
+
+ \item \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} performs intuitionistic proof search,
+ depending on specifically declared rules from the context, or given
+ as explicit arguments. Chained facts are inserted into the goal
+ before commencing proof search.
Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
@@ -1993,7 +1999,9 @@
Rules declared with ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' are ignored in proof search (the
single-step \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method still observes these). An
explicit weight annotation may be given as well; otherwise the
- number of rule premises will be taken into account here.%
+ number of rule premises will be taken into account here.
+
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -2039,15 +2047,19 @@
\end{railoutput}
- The \hyperlink{method.HOL.meson}{\mbox{\isa{meson}}} method implements Loveland's model elimination
- procedure \cite{loveland-78}. See \verb|~~/src/HOL/ex/Meson_Test.thy| for
- examples.
+ \begin{description}
+
+ \item \hyperlink{method.HOL.meson}{\mbox{\isa{meson}}} implements Loveland's model elimination
+ procedure \cite{loveland-78}. See \verb|~~/src/HOL/ex/Meson_Test.thy| for examples.
- The \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}} method combines ordered resolution and ordered
- paramodulation to find first-order (or mildly higher-order) proofs. The first
- optional argument specifies a type encoding; see the Sledgehammer manual
- \cite{isabelle-sledgehammer} for details. The \verb|~~/src/HOL/Metis_Examples| directory contains several small theories
- developed to a large extent using Metis.%
+ \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}} combines ordered resolution and ordered
+ paramodulation to find first-order (or mildly higher-order) proofs.
+ The first optional argument specifies a type encoding; see the
+ Sledgehammer manual \cite{isabelle-sledgehammer} for details. The
+ directory \verb|~~/src/HOL/Metis_Examples| contains several small
+ theories developed to a large extent using \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}.
+
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -2071,11 +2083,14 @@
\end{railoutput}
- The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
- \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
- applications in confluence theory, lattice theory and projective
- geometry. See \verb|~~/src/HOL/ex/Coherent.thy| for some
- examples.%
+ \begin{description}
+
+ \item \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} solves problems of \emph{Coherent
+ Logic} \cite{Bezem-Coquand:2005}, which covers applications in
+ confluence theory, lattice theory and projective geometry. See
+ \verb|~~/src/HOL/ex/Coherent.thy| for some examples.
+
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%