1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 15 18:12:24 2008 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 15 18:12:43 2008 +0200
1.3 @@ -95,7 +95,7 @@
1.4 %
1.5 \begin{isamarkuptext}%
1.6 \begin{matharray}{rcl}
1.7 - \hyperlink{attribute.HOL.split_format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
1.8 + \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
1.9 \end{matharray}
1.10
1.11 \begin{rail}
1.12 @@ -105,7 +105,7 @@
1.13
1.14 \begin{descr}
1.15
1.16 - \item [\hyperlink{attribute.HOL.split_format}{\mbox{\isa{split{\isacharunderscore}format}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] puts expressions of
1.17 + \item [\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] puts expressions of
1.18 low-level tuple types into canonical form as specified by the
1.19 arguments given; the \isa{i}-th collection of arguments refers to
1.20 occurrences in premise \isa{i} of the rule. The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all} arguments in function
1.21 @@ -365,7 +365,7 @@
1.22 \begin{isamarkuptext}%
1.23 \begin{matharray}{rcl}
1.24 \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isartrans{theory}{theory} \\
1.25 - \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep_datatype}{\hyperlink{command.HOL.rep_datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\
1.26 + \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\
1.27 \end{matharray}
1.28
1.29 \begin{rail}
1.30 @@ -386,7 +386,7 @@
1.31 \item [\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}] defines inductive datatypes in
1.32 HOL.
1.33
1.34 - \item [\hyperlink{command.HOL.rep_datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}] represents existing types as
1.35 + \item [\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}] represents existing types as
1.36 inductive ones, generating the standard infrastructure of derived
1.37 concepts (primitive recursion etc.).
1.38
1.39 @@ -399,7 +399,7 @@
1.40 See \cite{isabelle-HOL} for more details on datatypes, but beware of
1.41 the old-style theory syntax being used there! Apart from proper
1.42 proof methods for case-analysis and induction, there are also
1.43 - emulations of ML tactics \hyperlink{method.HOL.case_tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct_tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} available, see \secref{sec:hol-induct-tac}; these admit
1.44 + emulations of ML tactics \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} available, see \secref{sec:hol-induct-tac}; these admit
1.45 to refer directly to the internal structure of subgoals (including
1.46 internally bound parameters).%
1.47 \end{isamarkuptext}%
1.48 @@ -518,9 +518,9 @@
1.49 %
1.50 \begin{isamarkuptext}%
1.51 \begin{matharray}{rcl}
1.52 - \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat_completeness}{\hyperlink{method.HOL.pat_completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isarmeth \\
1.53 + \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isarmeth \\
1.54 \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isarmeth \\
1.55 - \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic_order}{\hyperlink{method.HOL.lexicographic_order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isarmeth \\
1.56 + \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isarmeth \\
1.57 \end{matharray}
1.58
1.59 \begin{rail}
1.60 @@ -532,7 +532,7 @@
1.61
1.62 \begin{descr}
1.63
1.64 - \item [\hyperlink{method.HOL.pat_completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}] is a specialized method to
1.65 + \item [\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}] is a specialized method to
1.66 solve goals regarding the completeness of pattern matching, as
1.67 required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
1.68 \cite{isabelle-function}).
1.69 @@ -544,7 +544,7 @@
1.70 Usually, this method is used as the initial proof step of manual
1.71 termination proofs.
1.72
1.73 - \item [\hyperlink{method.HOL.lexicographic_order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}] attempts a fully
1.74 + \item [\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}] attempts a fully
1.75 automated termination proof by searching for a lexicographic
1.76 combination of size measures on the arguments of the function. The
1.77 method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
1.78 @@ -564,11 +564,11 @@
1.79 \isamarkuptrue%
1.80 %
1.81 \begin{isamarkuptext}%
1.82 -The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef_tc}{\mbox{\isa{\isacommand{recdef{\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.
1.83 +The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\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.
1.84
1.85 \begin{matharray}{rcl}
1.86 \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isartrans{theory}{theory} \\
1.87 - \indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef_tc}{\hyperlink{command.HOL.recdef_tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
1.88 + \indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
1.89 \end{matharray}
1.90
1.91 \begin{rail}
1.92 @@ -596,7 +596,7 @@
1.93 context of the Simplifier (cf.\ \secref{sec:simplifier}) and
1.94 Classical reasoner (cf.\ \secref{sec:classical}).
1.95
1.96 - \item [\hyperlink{command.HOL.recdef_tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the
1.97 + \item [\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the
1.98 proof for leftover termination condition number \isa{i} (default
1.99 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
1.100 constant \isa{c}.
1.101 @@ -610,9 +610,9 @@
1.102 globally, using the following attributes.
1.103
1.104 \begin{matharray}{rcl}
1.105 - \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef_simp}{\hyperlink{attribute.HOL.recdef_simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isaratt \\
1.106 - \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef_cong}{\hyperlink{attribute.HOL.recdef_cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isaratt \\
1.107 - \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef_wf}{\hyperlink{attribute.HOL.recdef_wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isaratt \\
1.108 + \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isaratt \\
1.109 + \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isaratt \\
1.110 + \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isaratt \\
1.111 \end{matharray}
1.112
1.113 \begin{rail}
1.114 @@ -629,7 +629,7 @@
1.115 \begin{isamarkuptext}%
1.116 \begin{matharray}{rcl}
1.117 \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
1.118 - \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax_specification}{\hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
1.119 + \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
1.120 \end{matharray}
1.121
1.122 \begin{rail}
1.123 @@ -647,7 +647,7 @@
1.124 constants, as well as with theorems stating the properties for these
1.125 constants.
1.126
1.127 - \item [\hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
1.128 + \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
1.129 up a goal stating the existence of terms with the properties
1.130 specified to hold for the constants given in \isa{decls}. After
1.131 finishing the proof, the theory will be augmented with axioms
1.132 @@ -660,13 +660,13 @@
1.133
1.134 \end{descr}
1.135
1.136 - Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style. \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by
1.137 - construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
1.138 + Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style. \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by
1.139 + construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
1.140 user has explicitly proven it to be safe. A practical issue must be
1.141 considered, though: After introducing two constants with the same
1.142 properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
1.143 that the two constants are, in fact, equal. If this might be a
1.144 - problem, one should use \hyperlink{command.HOL.ax_specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
1.145 + problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
1.146 \end{isamarkuptext}%
1.147 \isamarkuptrue%
1.148 %
1.149 @@ -699,9 +699,9 @@
1.150
1.151 \begin{matharray}{rcl}
1.152 \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.153 - \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive_set}{\hyperlink{command.HOL.inductive_set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.154 + \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.155 \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.156 - \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive_set}{\hyperlink{command.HOL.coinductive_set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.157 + \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}} & : & \isarkeep{local{\dsh}theory} \\
1.158 \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isaratt \\
1.159 \end{matharray}
1.160
1.161 @@ -727,7 +727,7 @@
1.162 \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}},
1.163 for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule!
1.164
1.165 - \item [\hyperlink{command.HOL.inductive_set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}} and \hyperlink{command.HOL.coinductive_set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}] are wrappers for to the previous commands,
1.166 + \item [\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}] are wrappers for to the previous commands,
1.167 allowing the definition of (co)inductive sets.
1.168
1.169 \item [\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}] declares monotonicity rules. These
1.170 @@ -818,14 +818,14 @@
1.171 \begin{isamarkuptext}%
1.172 \begin{matharray}{rcl}
1.173 \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isarmeth \\
1.174 - \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith_split}{\hyperlink{attribute.HOL.arith_split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isaratt \\
1.175 + \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isaratt \\
1.176 \end{matharray}
1.177
1.178 The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems
1.179 (on types \isa{nat}, \isa{int}, \isa{real}). Any current
1.180 facts are inserted into the goal before running the procedure.
1.181
1.182 - The \hyperlink{attribute.HOL.arith_split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
1.183 + The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
1.184 rules to be expanded before the arithmetic procedure is invoked.
1.185
1.186 Note that a simpler (but faster) version of arithmetic reasoning is
1.187 @@ -842,10 +842,10 @@
1.188 ported to Isar. These should be never used in proper proof texts!
1.189
1.190 \begin{matharray}{rcl}
1.191 - \indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.case_tac}{\hyperlink{method.HOL.case_tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.192 - \indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.induct_tac}{\hyperlink{method.HOL.induct_tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.193 - \indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.ind_cases}{\hyperlink{method.HOL.ind_cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.194 - \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive_cases}{\hyperlink{command.HOL.inductive_cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}} & : & \isartrans{theory}{theory} \\
1.195 + \indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.case-tac}{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.196 + \indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.induct-tac}{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.197 + \indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.ind-cases}{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
1.198 + \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}} & : & \isartrans{theory}{theory} \\
1.199 \end{matharray}
1.200
1.201 \begin{rail}
1.202 @@ -864,20 +864,20 @@
1.203
1.204 \begin{descr}
1.205
1.206 - \item [\hyperlink{method.HOL.case_tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct_tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}]
1.207 + \item [\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}]
1.208 admit to reason about inductive datatypes only (unless an
1.209 - alternative rule is given explicitly). Furthermore, \hyperlink{method.HOL.case_tac}{\mbox{\isa{case{\isacharunderscore}tac}}} does a classical case split on booleans; \hyperlink{method.HOL.induct_tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} allows only variables to be given as instantiation.
1.210 + alternative rule is given explicitly). Furthermore, \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} does a classical case split on booleans; \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} allows only variables to be given as instantiation.
1.211 These tactic emulations feature both goal addressing and dynamic
1.212 instantiation. Note that named rule cases are \emph{not} provided
1.213 as would be by the proper \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.cases}{\mbox{\isa{cases}}} proof
1.214 methods (see \secref{sec:cases-induct}).
1.215
1.216 - \item [\hyperlink{method.HOL.ind_cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} and \hyperlink{command.HOL.inductive_cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}] provide an interface to the internal \verb|mk_cases| operation. Rules are simplified in an unrestricted
1.217 + \item [\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}] provide an interface to the internal \verb|mk_cases| operation. Rules are simplified in an unrestricted
1.218 forward manner.
1.219
1.220 - While \hyperlink{method.HOL.ind_cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the
1.221 - result immediately as elimination rules, \hyperlink{command.HOL.inductive_cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level
1.222 - for later use. The \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} argument of the \hyperlink{method.HOL.ind_cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} method allows to specify a list of variables that should
1.223 + While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the
1.224 + result immediately as elimination rules, \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level
1.225 + for later use. The \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} argument of the \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} method allows to specify a list of variables that should
1.226 be generalized before applying the resulting rule.
1.227
1.228 \end{descr}%
1.229 @@ -900,10 +900,10 @@
1.230
1.231 \begin{matharray}{rcl}
1.232 \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.233 - \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code_module}{\hyperlink{command.HOL.code_module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isartrans{theory}{theory} \\
1.234 - \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code_library}{\hyperlink{command.HOL.code_library}{\mbox{\isa{\isacommand{code{\isacharunderscore}library}}}}} & : & \isartrans{theory}{theory} \\
1.235 - \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts_code}{\hyperlink{command.HOL.consts_code}{\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}}}} & : & \isartrans{theory}{theory} \\
1.236 - \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types_code}{\hyperlink{command.HOL.types_code}{\mbox{\isa{\isacommand{types{\isacharunderscore}code}}}}} & : & \isartrans{theory}{theory} \\
1.237 + \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isartrans{theory}{theory} \\
1.238 + \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isacharunderscore}library}}}}} & : & \isartrans{theory}{theory} \\
1.239 + \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}}}} & : & \isartrans{theory}{theory} \\
1.240 + \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isacharunderscore}code}}}}} & : & \isartrans{theory}{theory} \\
1.241 \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\
1.242 \end{matharray}
1.243
1.244 @@ -961,20 +961,20 @@
1.245 introduction on how to use it.
1.246
1.247 \begin{matharray}{rcl}
1.248 - \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export_code}{\hyperlink{command.HOL.export_code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.249 - \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code_thms}{\hyperlink{command.HOL.code_thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.250 - \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code_deps}{\hyperlink{command.HOL.code_deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.251 - \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code_datatype}{\hyperlink{command.HOL.code_datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\
1.252 - \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code_const}{\hyperlink{command.HOL.code_const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isartrans{theory}{theory} \\
1.253 - \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code_type}{\hyperlink{command.HOL.code_type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isartrans{theory}{theory} \\
1.254 - \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code_class}{\hyperlink{command.HOL.code_class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isartrans{theory}{theory} \\
1.255 - \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code_instance}{\hyperlink{command.HOL.code_instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isartrans{theory}{theory} \\
1.256 - \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code_monad}{\hyperlink{command.HOL.code_monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isartrans{theory}{theory} \\
1.257 - \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code_reserved}{\hyperlink{command.HOL.code_reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isartrans{theory}{theory} \\
1.258 - \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code_include}{\hyperlink{command.HOL.code_include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isartrans{theory}{theory} \\
1.259 - \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code_modulename}{\hyperlink{command.HOL.code_modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isartrans{theory}{theory} \\
1.260 - \indexdef{HOL}{command}{code\_exception}\hypertarget{command.HOL.code_exception}{\hyperlink{command.HOL.code_exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}} & : & \isartrans{theory}{theory} \\
1.261 - \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print_codesetup}{\hyperlink{command.HOL.print_codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.262 + \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.263 + \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.264 + \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.265 + \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\
1.266 + \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isartrans{theory}{theory} \\
1.267 + \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isartrans{theory}{theory} \\
1.268 + \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isartrans{theory}{theory} \\
1.269 + \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isartrans{theory}{theory} \\
1.270 + \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isartrans{theory}{theory} \\
1.271 + \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isartrans{theory}{theory} \\
1.272 + \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isartrans{theory}{theory} \\
1.273 + \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isartrans{theory}{theory} \\
1.274 + \indexdef{HOL}{command}{code\_exception}\hypertarget{command.HOL.code-exception}{\hyperlink{command.HOL.code-exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}} & : & \isartrans{theory}{theory} \\
1.275 + \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
1.276 \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\
1.277 \end{matharray}
1.278
1.279 @@ -1050,7 +1050,7 @@
1.280
1.281 \begin{descr}
1.282
1.283 - \item [\hyperlink{command.HOL.export_code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}] is the canonical interface
1.284 + \item [\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}] is the canonical interface
1.285 for generating and serializing code: for a given list of constants,
1.286 code is generated for the specified target languages. Abstract code
1.287 is cached incrementally. If no constant is given, the currently
1.288 @@ -1063,7 +1063,7 @@
1.289
1.290 By default, for each involved theory one corresponding name space
1.291 module is generated. Alternativly, a module name may be specified
1.292 - after the \hyperlink{keyword.module_name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
1.293 + after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
1.294 placed in this module.
1.295
1.296 For \emph{SML} and \emph{OCaml}, the file specification refers to a
1.297 @@ -1077,54 +1077,54 @@
1.298 \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
1.299 declaration.
1.300
1.301 - \item [\hyperlink{command.HOL.code_thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}] prints a list of theorems
1.302 + \item [\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}] prints a list of theorems
1.303 representing the corresponding program containing all given
1.304 constants; if no constants are given, the currently cached code
1.305 theorems are printed.
1.306
1.307 - \item [\hyperlink{command.HOL.code_deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}] visualizes dependencies of
1.308 + \item [\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}] visualizes dependencies of
1.309 theorems representing the corresponding program containing all given
1.310 constants; if no constants are given, the currently cached code
1.311 theorems are visualized.
1.312
1.313 - \item [\hyperlink{command.HOL.code_datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}] specifies a constructor set
1.314 + \item [\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}] specifies a constructor set
1.315 for a logical type.
1.316
1.317 - \item [\hyperlink{command.HOL.code_const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}] associates a list of constants
1.318 + \item [\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}] associates a list of constants
1.319 with target-specific serializations; omitting a serialization
1.320 deletes an existing serialization.
1.321
1.322 - \item [\hyperlink{command.HOL.code_type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}] associates a list of type
1.323 + \item [\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}] associates a list of type
1.324 constructors with target-specific serializations; omitting a
1.325 serialization deletes an existing serialization.
1.326
1.327 - \item [\hyperlink{command.HOL.code_class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
1.328 + \item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
1.329 with target-specific class names; in addition, constants associated
1.330 with this class may be given target-specific names used for instance
1.331 declarations; omitting a serialization deletes an existing
1.332 serialization. This applies only to \emph{Haskell}.
1.333
1.334 - \item [\hyperlink{command.HOL.code_instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
1.335 + \item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
1.336 constructor / class instance relations as ``already present'' for a
1.337 given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
1.338 ``already present'' declaration. This applies only to
1.339 \emph{Haskell}.
1.340
1.341 - \item [\hyperlink{command.HOL.code_monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary
1.342 + \item [\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary
1.343 mechanism to generate monadic code.
1.344
1.345 - \item [\hyperlink{command.HOL.code_reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as
1.346 + \item [\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as
1.347 reserved for a given target, preventing it to be shadowed by any
1.348 generated code.
1.349
1.350 - \item [\hyperlink{command.HOL.code_include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content
1.351 + \item [\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content
1.352 (``include'') to generated code. A as last argument ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}''
1.353 will remove an already added ``include''.
1.354
1.355 - \item [\hyperlink{command.HOL.code_modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from
1.356 + \item [\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from
1.357 one module name onto another.
1.358
1.359 - \item [\hyperlink{command.HOL.code_exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}] declares constants which
1.360 + \item [\hyperlink{command.HOL.code-exception}{\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}}] declares constants which
1.361 are not required to have a definition by a defining equations; these
1.362 are mapped on exceptions instead.
1.363
1.364 @@ -1138,7 +1138,7 @@
1.365 applied as rewrite rules to any defining equation during
1.366 preprocessing.
1.367
1.368 - \item [\hyperlink{command.HOL.print_codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on
1.369 + \item [\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on
1.370 selected defining equations, code generator datatypes and
1.371 preprocessor setup.
1.372