# HG changeset patch # User wenzelm # Date 1328197095 -3600 # Node ID 9be4d8c8d84270424b64f527bace2e1bb72f5fae # Parent ddf7f79abdacca7c72219e00442c6fb5635e9ee9 misc tuning and reformatting; diff -r ddf7f79abdac -r 9be4d8c8d842 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 \ local_theory"} \\ + @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def (HOL) "coinductive"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \ 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 \ local_theory"} \\ - @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def (HOL) "coinductive"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \ 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 \ theory)"} \\ @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \ 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 \ 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 \}, a set @{text "A :: \ set"}, and a theorem that proves @{prop "\x. x \ 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 \ 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 \ proof(prove)"}\\ @{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \ proof(prove)"}\\ @@ -1265,6 +1261,12 @@ @{command_def (HOL) "print_quotconsts"} & : & @{text "context \"}\\ \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 :: \\<^isub>1 \ - \\<^isub>2"} where @{text "\\<^isub>1"} and @{text - "\\<^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 :: \\<^isub>1 \ \\<^isub>2"} where @{text "\\<^isub>1"} and + @{text "\\<^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 \ \ \ f\<^isub>n \ (\\<^isub>1, \, \\<^isub>n) t \ (\\<^isub>1, \, \\<^isub>n) t"} \\ \end{matharray} - where @{text "t"} is a type constructor and @{text "f\<^isub>i"} is of - type @{text "\\<^isub>i \ \\<^isub>i"} or - @{text "\\<^isub>i \ \\<^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 "\\<^isub>i \ \\<^isub>i"} or @{text "\\<^isub>i \ \\<^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} *} diff -r ddf7f79abdac -r 9be4d8c8d842 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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% %