--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 02 21:15:15 2012 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 02 21:15:38 2012 +0200
@@ -81,7 +81,7 @@
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
@@ -162,7 +162,7 @@
\item @{text R.simps} is the equation unrolling the fixpoint of the
predicate one step.
-
+
\end{description}
When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are
@@ -1087,7 +1087,7 @@
of HOL models by construction. Note that @{command_ref
type_synonym} from Isabelle/Pure merely introduces syntactic
abbreviations, without any logical significance.
-
+
@{rail "
@@{command (HOL) typedef} alt_name? abs_type '=' rep_set
;
@@ -1254,6 +1254,7 @@
\end{description}
*}
+
section {* Transfer package *}
text {*
@@ -1314,6 +1315,7 @@
*}
+
section {* Lifting package *}
text {*
@@ -1338,67 +1340,75 @@
\begin{description}
- \item @{command (HOL) "setup_lifting"} Sets up the Lifting package to work with
- a user-defined type. The user must provide either a quotient
- theorem @{text "Quotient R Abs Rep T"} or a type_definition theorem
- @{text "type_definition Rep Abs A"}.
- The package configures
- transfer rules for equality and quantifiers on the type, and sets
- up the @{command_def (HOL) "lift_definition"} command to work with the type.
- In the case of a quotient theorem,
- an optional theorem @{text "reflp R"} can be provided as a second argument.
- This allows the package to generate stronger transfer rules.
-
- @{command (HOL) "setup_lifting"} is called automatically if a quotient type
- is defined by the command @{command (HOL) "quotient_type"} from the Quotient package.
-
- If @{command (HOL) "setup_lifting"} is called with a type_definition theorem,
- the abstract type implicitly defined by the theorem is declared as an abstract type in
- the code generator. This allows @{command (HOL) "lift_definition"} to register
- (generated) code certificate theorems as abstract code equations in the code generator.
- The option @{text "no_abs_code"} of the command @{command (HOL) "setup_lifting"}
- can turn off that behavior and causes that code certificate theorems generated
- by @{command (HOL) "lift_definition"} are not registred as abstract code equations.
-
- \item @{command (HOL) "lift_definition"} @{text "f :: \<tau> is t"}
- Defines a new function @{text f} with an abstract type @{text \<tau>} in
- terms of a corresponding operation @{text t} on a representation type.
- The term @{text t} doesn't have to be necessarily a constant but it can
- be any term.
+ \item @{command (HOL) "setup_lifting"} Sets up the Lifting package
+ to work with a user-defined type. The user must provide either a
+ quotient theorem @{text "Quotient R Abs Rep T"} or a
+ type_definition theorem @{text "type_definition Rep Abs A"}. The
+ package configures transfer rules for equality and quantifiers on
+ the type, and sets up the @{command_def (HOL) "lift_definition"}
+ command to work with the type. In the case of a quotient theorem,
+ an optional theorem @{text "reflp R"} can be provided as a second
+ argument. This allows the package to generate stronger transfer
+ rules.
+
+ @{command (HOL) "setup_lifting"} is called automatically if a
+ quotient type is defined by the command @{command (HOL)
+ "quotient_type"} from the Quotient package.
+
+ If @{command (HOL) "setup_lifting"} is called with a
+ type_definition theorem, the abstract type implicitly defined by
+ the theorem is declared as an abstract type in the code
+ generator. This allows @{command (HOL) "lift_definition"} to
+ register (generated) code certificate theorems as abstract code
+ equations in the code generator. The option @{text "no_abs_code"}
+ of the command @{command (HOL) "setup_lifting"} can turn off that
+ behavior and causes that code certificate theorems generated by
+ @{command (HOL) "lift_definition"} are not registred as abstract
+ code equations.
+
+ \item @{command (HOL) "lift_definition"} @{text "f :: \<tau> is t"}
+ Defines a new function @{text f} with an abstract type @{text \<tau>}
+ in terms of a corresponding operation @{text t} on a
+ representation type. The term @{text t} doesn't have to be
+ necessarily a constant but it can be any term.
Users must discharge a respectfulness proof obligation when each
- constant is defined. For a type copy, i.e. a typedef with @{text UNIV},
- the proof is discharged automatically. The obligation is
+ constant is defined. For a type copy, i.e. a typedef with @{text
+ UNIV}, the proof is discharged automatically. The obligation is
presented in a user-friendly, readable form. A respectfulness
- theorem in the standard format @{text f.rsp} and a transfer rule @{text f.tranfer}
- for the Transfer package are generated by the package.
+ theorem in the standard format @{text f.rsp} and a transfer rule
+ @{text f.tranfer} for the Transfer package are generated by the
+ package.
Integration with code_abstype: For typedefs (e.g. subtypes
- corresponding to a datatype invariant, such as dlist),
- @{command (HOL) "lift_definition"}
- generates a code certificate theorem @{text f.rep_eq} and sets up
- code generation for each constant.
+ corresponding to a datatype invariant, such as dlist), @{command
+ (HOL) "lift_definition"} generates a code certificate theorem
+ @{text f.rep_eq} and sets up code generation for each constant.
\item @{command (HOL) "print_quotmaps"} prints stored quotient map
- theorems.
-
- \item @{command (HOL) "print_quotients"} prints stored quotient theorems.
-
- \item @{attribute (HOL) quot_map} registers a quotient map theorem. For examples see
- @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy files.
-
- \item @{attribute (HOL) invariant_commute} registers a theorem which shows a relationship
- between the constant @{text Lifting.invariant} (used for internal encoding of proper subtypes)
- and a relator.
- Such theorems allows the package to hide @{text Lifting.invariant} from a user
- in a user-readable form of a respectfulness theorem. For examples see
- @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy files.
-
+ theorems.
+
+ \item @{command (HOL) "print_quotients"} prints stored quotient
+ theorems.
+
+ \item @{attribute (HOL) quot_map} registers a quotient map
+ theorem. For examples see @{file
+ "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
+ files.
+
+ \item @{attribute (HOL) invariant_commute} registers a theorem which
+ shows a relationship between the constant @{text
+ Lifting.invariant} (used for internal encoding of proper subtypes)
+ and a relator. Such theorems allows the package to hide @{text
+ Lifting.invariant} from a user in a user-readable form of a
+ respectfulness theorem. For examples see @{file
+ "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
+ files.
\end{description}
-
*}
+
section {* Quotient types *}
text {*
@@ -1434,7 +1444,7 @@
spec: @{syntax typespec} @{syntax mixfix}? '=' \\
@{syntax type} '/' ('partial' ':')? @{syntax term} \\
- (@'morphisms' @{syntax name} @{syntax name})?;
+ (@'morphisms' @{syntax name} @{syntax name})?;
"}
@{rail "
@@ -1875,7 +1885,7 @@
to search for a further genuine counterexample.
For this option to be effective, the @{text genuine_only} option
must be set to false.
-
+
\item[@{text eval}] takes a term or a list of terms and evaluates
these terms under the variable assignment found by quickcheck.
@@ -1889,10 +1899,10 @@
a locale context, i.e., they can be interpreted or expanded.
The option is a whitespace-separated list of the two words
@{text interpret} and @{text expand}. The list determines the
- order they are employed. The default setting is to first use
+ order they are employed. The default setting is to first use
interpretations and then test the expanded conjecture.
The option is only provided as attribute declaration, but not
- as parameter to the command.
+ as parameter to the command.
\item[@{text timeout}] sets the time limit in seconds.
@@ -1908,7 +1918,7 @@
\item[@{text quiet}] if set quickcheck does not output anything
while testing.
-
+
\item[@{text verbose}] if set quickcheck informs about the current
size and cardinality while testing.
@@ -2169,11 +2179,11 @@
syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
;
-
+
modedecl: (modes | ((const ':' modes) \\
(@'and' ((const ':' modes @'and') +))?))
;
-
+
modes: mode @'as' const
"}
@@ -2287,16 +2297,16 @@
argument compiles code into the system runtime environment and
modifies the code generator setup that future invocations of system
runtime code generation referring to one of the ``@{text
- "datatypes"}'' or ``@{text "functions"}'' entities use these precompiled
- entities. With a ``@{text "file"}'' argument, the corresponding code
- is generated into that specified file without modifying the code
- generator setup.
-
- \item @{command (HOL) "code_pred"} creates code equations for a predicate
- given a set of introduction rules. Optional mode annotations determine
- which arguments are supposed to be input or output. If alternative
- introduction rules are declared, one must prove a corresponding elimination
- rule.
+ "datatypes"}'' or ``@{text "functions"}'' entities use these
+ precompiled entities. With a ``@{text "file"}'' argument, the
+ corresponding code is generated into that specified file without
+ modifying the code generator setup.
+
+ \item @{command (HOL) "code_pred"} creates code equations for a
+ predicate given a set of introduction rules. Optional mode
+ annotations determine which arguments are supposed to be input or
+ output. If alternative introduction rules are declared, one must
+ prove a corresponding elimination rule.
\end{description}
*}