--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 26 15:55:22 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 26 16:10:22 2011 +0100
@@ -24,7 +24,7 @@
\end{rail}
\begin{description}
-
+
\item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}
axiomatizes a Gordon/HOL-style type definition in the background
theory of the current context, depending on a non-emptiness result
@@ -36,7 +36,7 @@
multiple interpretations in target contexts. Thus the established
bijection between the representing set @{text A} and the new type
@{text t} may semantically depend on local assumptions.
-
+
By default, @{command (HOL) "typedef"} defines both a type @{text t}
and a set (term constant) of the same name, unless an alternative
base name is given in parentheses, or the ``@{text "(open)"}''
@@ -44,7 +44,7 @@
altogether. The injection from type to set is called @{text Rep_t},
its inverse @{text Abs_t} --- this may be changed via an explicit
@{keyword (HOL) "morphisms"} declaration.
-
+
Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text
Abs_t_inverse} provide the most basic characterization as a
corresponding injection/surjection pair (in both directions). Rules
@@ -55,7 +55,7 @@
@{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views
on surjectivity; these are already declared as set or type rules for
the generic @{method cases} and @{method induct} methods.
-
+
An alternative name for the set definition (and other derived
entities) may be specified in parentheses; the default is to use
@{text t} as indicated before.
@@ -77,7 +77,7 @@
\end{rail}
\begin{description}
-
+
\item @{attribute (HOL) split_format}\ @{text "(complete)"} causes
arguments in function applications to be represented canonically
according to their tuple type structure.
@@ -140,7 +140,7 @@
``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}
element. In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation
for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}.
-
+
\medskip Two key observations make extensible records in a simply
typed language like HOL work out:
@@ -261,7 +261,7 @@
\medskip
\begin{tabular}{lll}
@{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
- @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow>
+ @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow>
\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
@{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
@@ -299,13 +299,13 @@
@{text t} is a record type as specified above.
\begin{enumerate}
-
+
\item Standard conversions for selectors or updates applied to
record constructor terms are made part of the default Simplifier
context; thus proofs by reduction of basic operations merely require
the @{method simp} method without further arguments. These rules
are available as @{text "t.simps"}, too.
-
+
\item Selectors applied to updated records are automatically reduced
by an internal simplification procedure, which is also part of the
standard Simplifier setup.
@@ -325,7 +325,7 @@
induct} format (cf.\ the generic proof methods of the same name,
\secref{sec:cases-induct}). Several variations are available, for
fixed records, record schemes, more parts etc.
-
+
The generic proof methods are sufficiently smart to pick the most
sensible rule according to the type of the indicated record
expression: users just need to apply something like ``@{text "(cases
@@ -614,7 +614,7 @@
The mandatory @{text mode} argument specifies the mode of operation
of the command, which directly corresponds to a complete partial
order on the result type. By default, the following modes are
- defined:
+ defined:
\begin{description}
\item @{text option} defines functions that map into the @{type
@@ -623,7 +623,7 @@
None} is returned by a recursive call, then the overall result
must also be @{term None}. This is best achieved through the use of
the monadic operator @{const "Option.bind"}.
-
+
\item @{text tailrec} defines functions with an arbitrary result
type and uses the slightly degenerated partial order where @{term
"undefined"} is the bottom element. Now, monotonicity requires that
@@ -671,7 +671,7 @@
\end{rail}
\begin{description}
-
+
\item @{command (HOL) "recdef"} defines general well-founded
recursive functions (using the TFL package), see also
\cite{isabelle-HOL}. The ``@{text "(permissive)"}'' option tells
@@ -682,12 +682,12 @@
declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
context of the Simplifier (cf.\ \secref{sec:simplifier}) and
Classical reasoner (cf.\ \secref{sec:classical}).
-
+
\item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the
proof for leftover termination condition number @{text i} (default
1) as generated by a @{command (HOL) "recdef"} definition of
constant @{text c}.
-
+
Note that in most cases, @{command (HOL) "recdef"} is able to finish
its internal proofs without manual intervention.
@@ -984,7 +984,7 @@
\item[@{text eval}] takes a term or a list of terms and evaluates
these terms under the variable assignment found by quickcheck.
-
+
\item[@{text iterations}] sets how many sets of assignments are
generated for each particular size.
@@ -1060,7 +1060,7 @@
induct} method, @{method induct_tac} does not handle structured rule
statements, only the compact object-logic conclusion of the subgoal
being addressed.
-
+
\item @{method (HOL) ind_cases} and @{command (HOL)
"inductive_cases"} provide an interface to the internal @{ML_text
mk_cases} operation. Rules are simplified in an unrestricted
@@ -1224,7 +1224,7 @@
Serializers take an optional list of arguments in parentheses. For
\emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
explicit module signatures.
-
+
For \emph{Haskell} a module name prefix may be given using the
``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
@@ -1318,7 +1318,7 @@
@{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
@{attribute_def (HOL) code} & : & @{text attribute} \\
\end{matharray}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 26 15:55:22 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 26 16:10:22 2011 +0100
@@ -44,7 +44,7 @@
\end{rail}
\begin{description}
-
+
\item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{22}{\isachardoublequote}}}
axiomatizes a Gordon/HOL-style type definition in the background
theory of the current context, depending on a non-emptiness result
@@ -56,7 +56,7 @@
multiple interpretations in target contexts. Thus the established
bijection between the representing set \isa{A} and the new type
\isa{t} may semantically depend on local assumptions.
-
+
By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t}
and a set (term constant) of the same name, unless an alternative
base name is given in parentheses, or the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}''
@@ -64,7 +64,7 @@
altogether. The injection from type to set is called \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t},
its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t} --- this may be changed via an explicit
\hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration.
-
+
Theorems \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t}, \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse}, and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse} provide the most basic characterization as a
corresponding injection/surjection pair (in both directions). Rules
\isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} provide a slightly
@@ -74,7 +74,7 @@
\isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}cases}/\isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views
on surjectivity; these are already declared as set or type rules for
the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.
-
+
An alternative name for the set definition (and other derived
entities) may be specified in parentheses; the default is to use
\isa{t} as indicated before.
@@ -98,7 +98,7 @@
\end{rail}
\begin{description}
-
+
\item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}complete{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} causes
arguments in function applications to be represented canonically
according to their tuple type structure.
@@ -163,7 +163,7 @@
``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' is properly terminated by the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ unit{\isaliteral{22}{\isachardoublequote}}}
element. In fact, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is just an abbreviation
for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.
-
+
\medskip Two key observations make extensible records in a simply
typed language like HOL work out:
@@ -312,13 +312,13 @@
\isa{t} is a record type as specified above.
\begin{enumerate}
-
+
\item Standard conversions for selectors or updates applied to
record constructor terms are made part of the default Simplifier
context; thus proofs by reduction of basic operations merely require
the \hyperlink{method.simp}{\mbox{\isa{simp}}} method without further arguments. These rules
are available as \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, too.
-
+
\item Selectors applied to updated records are automatically reduced
by an internal simplification procedure, which is also part of the
standard Simplifier setup.
@@ -335,7 +335,7 @@
constructor terms are provided both in \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} format (cf.\ the generic proof methods of the same name,
\secref{sec:cases-induct}). Several variations are available, for
fixed records, record schemes, more parts etc.
-
+
The generic proof methods are sufficiently smart to pick the most
sensible rule according to the type of the indicated record
expression: users just need to apply something like ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}cases\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' to a certain proof problem.
@@ -626,14 +626,14 @@
The mandatory \isa{mode} argument specifies the mode of operation
of the command, which directly corresponds to a complete partial
order on the result type. By default, the following modes are
- defined:
+ defined:
\begin{description}
\item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
must also be \isa{None}. This is best achieved through the use of
the monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}.
-
+
\item \isa{tailrec} defines functions with an arbitrary result
type and uses the slightly degenerated partial order where \isa{{\isaliteral{22}{\isachardoublequote}}undefined{\isaliteral{22}{\isachardoublequote}}} is the bottom element. Now, monotonicity requires that
if \isa{undefined} is returned by a recursive call, then the
@@ -680,7 +680,7 @@
\end{rail}
\begin{description}
-
+
\item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
recursive functions (using the TFL package), see also
\cite{isabelle-HOL}. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells
@@ -690,12 +690,12 @@
declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
context of the Simplifier (cf.\ \secref{sec:simplifier}) and
Classical reasoner (cf.\ \secref{sec:classical}).
-
+
\item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} recommences the
proof for leftover termination condition number \isa{i} (default
1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
constant \isa{c}.
-
+
Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
its internal proofs without manual intervention.
@@ -1000,6 +1000,9 @@
\item[\isa{size}] specifies the maximum size of the search space
for assignment values.
+ \item[\isa{eval}] takes a term or a list of terms and evaluates
+ these terms under the variable assignment found by quickcheck.
+
\item[\isa{iterations}] sets how many sets of assignments are
generated for each particular size.
@@ -1074,7 +1077,7 @@
methods (see \secref{sec:cases-induct}). Unlike the \hyperlink{method.induct}{\mbox{\isa{induct}}} method, \hyperlink{method.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}} does not handle structured rule
statements, only the compact object-logic conclusion of the subgoal
being addressed.
-
+
\item \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}} provide an interface to the internal \verb|mk_cases| operation. Rules are simplified in an unrestricted
forward manner.
@@ -1235,7 +1238,7 @@
Serializers take an optional list of arguments in parentheses. For
\emph{SML} and \emph{OCaml}, ``\isa{no{\isaliteral{5F}{\isacharunderscore}}signatures}`` omits
explicit module signatures.
-
+
For \emph{Haskell} a module name prefix may be given using the
``\isa{{\isaliteral{22}{\isachardoublequote}}root{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}'' argument; ``\isa{string{\isaliteral{5F}{\isacharunderscore}}classes}'' adds a
``\verb|deriving (Read, Show)|'' clause to each appropriate
@@ -1327,7 +1330,7 @@
\indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
\end{matharray}