Merged
authoreberlm <eberlm@in.tum.de>
Fri Jul 22 15:39:32 2016 +0200 (2016-07-22)
changeset 635368cecf0100996
parent 63535 6887fda4541a
parent 63533 42b6186fc0e4
child 63537 831816778409
Merged
     1.1 --- a/NEWS	Fri Jul 22 15:39:27 2016 +0200
     1.2 +++ b/NEWS	Fri Jul 22 15:39:32 2016 +0200
     1.3 @@ -52,6 +52,11 @@
     1.4  * Proof method "blast" is more robust wrt. corner cases of Pure
     1.5  statements without object-logic judgment.
     1.6  
     1.7 +* Pure provides basic versions of proof methods "simp" and "simp_all"
     1.8 +that only know about meta-equality (==). Potential INCOMPATIBILITY in
     1.9 +theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
    1.10 +is relevant to avoid confusion of Pure.simp vs. HOL.simp.
    1.11 +
    1.12  
    1.13  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.14  
    1.15 @@ -103,6 +108,9 @@
    1.16  * Command 'proof' provides information about proof outline with cases,
    1.17  e.g. for proof methods "cases", "induct", "goal_cases".
    1.18  
    1.19 +* Completion templates for commands involving "begin ... end" blocks,
    1.20 +e.g. 'context', 'notepad'.
    1.21 +
    1.22  
    1.23  *** Isar ***
    1.24  
    1.25 @@ -145,8 +153,8 @@
    1.26  "method_facts". This is particularly useful for Eisbach method
    1.27  definitions.
    1.28  
    1.29 -* Eisbach provides method "use" to modify the main facts of a given
    1.30 -method expression, e.g.
    1.31 +* Proof method "use" allows to modify the main facts of a given method
    1.32 +expression, e.g.
    1.33  
    1.34    (use facts in simp)
    1.35    (use facts in \<open>simp add: ...\<close>)
     2.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Jul 22 15:39:27 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Jul 22 15:39:32 2016 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  (*:maxLineLen=78:*)
     2.5  
     2.6  theory Document_Preparation
     2.7 -imports Base Main
     2.8 +  imports Main Base
     2.9  begin
    2.10  
    2.11  chapter \<open>Document preparation \label{ch:document-prep}\<close>
     3.1 --- a/src/Doc/Isar_Ref/Framework.thy	Fri Jul 22 15:39:27 2016 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Framework.thy	Fri Jul 22 15:39:32 2016 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  (*:maxLineLen=78:*)
     3.5  
     3.6  theory Framework
     3.7 -imports Base Main
     3.8 +  imports Main Base
     3.9  begin
    3.10  
    3.11  chapter \<open>The Isabelle/Isar Framework \label{ch:isar-framework}\<close>
     4.1 --- a/src/Doc/Isar_Ref/Generic.thy	Fri Jul 22 15:39:27 2016 +0200
     4.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Fri Jul 22 15:39:32 2016 +0200
     4.3 @@ -1,23 +1,22 @@
     4.4  (*:maxLineLen=78:*)
     4.5  
     4.6  theory Generic
     4.7 -imports Base Main
     4.8 +imports Main Base
     4.9  begin
    4.10  
    4.11  chapter \<open>Generic tools and packages \label{ch:gen-tools}\<close>
    4.12  
    4.13  section \<open>Configuration options \label{sec:config}\<close>
    4.14  
    4.15 -text \<open>Isabelle/Pure maintains a record of named configuration
    4.16 -  options within the theory or proof context, with values of type
    4.17 -  @{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type
    4.18 -  string}.  Tools may declare options in ML, and then refer to these
    4.19 -  values (relative to the context).  Thus global reference variables
    4.20 -  are easily avoided.  The user may change the value of a
    4.21 -  configuration option by means of an associated attribute of the same
    4.22 -  name.  This form of context declaration works particularly well with
    4.23 -  commands such as @{command "declare"} or @{command "using"} like
    4.24 -  this:
    4.25 +text \<open>
    4.26 +  Isabelle/Pure maintains a record of named configuration options within the
    4.27 +  theory or proof context, with values of type @{ML_type bool}, @{ML_type
    4.28 +  int}, @{ML_type real}, or @{ML_type string}. Tools may declare options in
    4.29 +  ML, and then refer to these values (relative to the context). Thus global
    4.30 +  reference variables are easily avoided. The user may change the value of a
    4.31 +  configuration option by means of an associated attribute of the same name.
    4.32 +  This form of context declaration works particularly well with commands such
    4.33 +  as @{command "declare"} or @{command "using"} like this:
    4.34  \<close>
    4.35  
    4.36  (*<*)experiment begin(*>*)
    4.37 @@ -40,14 +39,14 @@
    4.38      @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
    4.39    \<close>}
    4.40  
    4.41 -  \<^descr> @{command "print_options"} prints the available configuration
    4.42 -  options, with names, types, and current values; the ``\<open>!\<close>'' option
    4.43 -  indicates extra verbosity.
    4.44 +  \<^descr> @{command "print_options"} prints the available configuration options,
    4.45 +  with names, types, and current values; the ``\<open>!\<close>'' option indicates extra
    4.46 +  verbosity.
    4.47    
    4.48 -  \<^descr> \<open>name = value\<close> as an attribute expression modifies the
    4.49 -  named option, with the syntax of the value depending on the option's
    4.50 -  type.  For @{ML_type bool} the default value is \<open>true\<close>.  Any
    4.51 -  attempt to change a global option in a local context is ignored.
    4.52 +  \<^descr> \<open>name = value\<close> as an attribute expression modifies the named option, with
    4.53 +  the syntax of the value depending on the option's type. For @{ML_type bool}
    4.54 +  the default value is \<open>true\<close>. Any attempt to change a global option in a
    4.55 +  local context is ignored.
    4.56  \<close>
    4.57  
    4.58  
    4.59 @@ -81,46 +80,41 @@
    4.60      @@{method sleep} @{syntax real}
    4.61    \<close>}
    4.62  
    4.63 -  \<^descr> @{method unfold}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> and @{method fold}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> expand (or fold back) the given definitions throughout
    4.64 -  all goals; any chained facts provided are inserted into the goal and
    4.65 -  subject to rewriting as well.
    4.66 -
    4.67 -  \<^descr> @{method insert}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> inserts theorems as facts
    4.68 -  into all goals of the proof state.  Note that current facts
    4.69 -  indicated for forward chaining are ignored.
    4.70 +  \<^descr> @{method unfold}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> and @{method fold}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> expand (or
    4.71 +  fold back) the given definitions throughout all goals; any chained facts
    4.72 +  provided are inserted into the goal and subject to rewriting as well.
    4.73  
    4.74 -  \<^descr> @{method erule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>, @{method
    4.75 -  drule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>, and @{method frule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> are similar to the basic @{method rule}
    4.76 -  method (see \secref{sec:pure-meth-att}), but apply rules by
    4.77 -  elim-resolution, destruct-resolution, and forward-resolution,
    4.78 -  respectively @{cite "isabelle-implementation"}.  The optional natural
    4.79 -  number argument (default 0) specifies additional assumption steps to
    4.80 -  be performed here.
    4.81 +  \<^descr> @{method insert}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> inserts theorems as facts into all goals of
    4.82 +  the proof state. Note that current facts indicated for forward chaining are
    4.83 +  ignored.
    4.84 +
    4.85 +  \<^descr> @{method erule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>, @{method drule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>, and @{method
    4.86 +  frule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> are similar to the basic @{method rule} method (see
    4.87 +  \secref{sec:pure-meth-att}), but apply rules by elim-resolution,
    4.88 +  destruct-resolution, and forward-resolution, respectively @{cite
    4.89 +  "isabelle-implementation"}. The optional natural number argument (default 0)
    4.90 +  specifies additional assumption steps to be performed here.
    4.91  
    4.92    Note that these methods are improper ones, mainly serving for
    4.93 -  experimentation and tactic script emulation.  Different modes of
    4.94 -  basic rule application are usually expressed in Isar at the proof
    4.95 -  language level, rather than via implicit proof state manipulations.
    4.96 -  For example, a proper single-step elimination would be done using
    4.97 -  the plain @{method rule} method, with forward chaining of current
    4.98 -  facts.
    4.99 +  experimentation and tactic script emulation. Different modes of basic rule
   4.100 +  application are usually expressed in Isar at the proof language level,
   4.101 +  rather than via implicit proof state manipulations. For example, a proper
   4.102 +  single-step elimination would be done using the plain @{method rule} method,
   4.103 +  with forward chaining of current facts.
   4.104  
   4.105 -  \<^descr> @{method intro} and @{method elim} repeatedly refine some goal
   4.106 -  by intro- or elim-resolution, after having inserted any chained
   4.107 -  facts.  Exactly the rules given as arguments are taken into account;
   4.108 -  this allows fine-tuned decomposition of a proof problem, in contrast
   4.109 -  to common automated tools.
   4.110 +  \<^descr> @{method intro} and @{method elim} repeatedly refine some goal by intro-
   4.111 +  or elim-resolution, after having inserted any chained facts. Exactly the
   4.112 +  rules given as arguments are taken into account; this allows fine-tuned
   4.113 +  decomposition of a proof problem, in contrast to common automated tools.
   4.114  
   4.115 -  \<^descr> @{method fail} yields an empty result sequence; it is the
   4.116 -  identity of the ``\<open>|\<close>'' method combinator (cf.\
   4.117 -  \secref{sec:proof-meth}).
   4.118 +  \<^descr> @{method fail} yields an empty result sequence; it is the identity of the
   4.119 +  ``\<open>|\<close>'' method combinator (cf.\ \secref{sec:proof-meth}).
   4.120  
   4.121 -  \<^descr> @{method succeed} yields a single (unchanged) result; it is
   4.122 -  the identity of the ``\<open>,\<close>'' method combinator (cf.\
   4.123 -  \secref{sec:proof-meth}).
   4.124 +  \<^descr> @{method succeed} yields a single (unchanged) result; it is the identity
   4.125 +  of the ``\<open>,\<close>'' method combinator (cf.\ \secref{sec:proof-meth}).
   4.126  
   4.127 -  \<^descr> @{method sleep}~\<open>s\<close> succeeds after a real-time delay of \<open>s\<close> seconds. This is occasionally useful for demonstration and testing
   4.128 -  purposes.
   4.129 +  \<^descr> @{method sleep}~\<open>s\<close> succeeds after a real-time delay of \<open>s\<close> seconds. This
   4.130 +  is occasionally useful for demonstration and testing purposes.
   4.131  
   4.132  
   4.133    \begin{matharray}{rcl}
   4.134 @@ -147,38 +141,35 @@
   4.135      @@{attribute rotated} @{syntax int}?
   4.136    \<close>}
   4.137  
   4.138 -  \<^descr> @{attribute tagged}~\<open>name value\<close> and @{attribute
   4.139 -  untagged}~\<open>name\<close> add and remove \<^emph>\<open>tags\<close> of some theorem.
   4.140 -  Tags may be any list of string pairs that serve as formal comment.
   4.141 -  The first string is considered the tag name, the second its value.
   4.142 -  Note that @{attribute untagged} removes any tags of the same name.
   4.143 +  \<^descr> @{attribute tagged}~\<open>name value\<close> and @{attribute untagged}~\<open>name\<close> add and
   4.144 +  remove \<^emph>\<open>tags\<close> of some theorem. Tags may be any list of string pairs that
   4.145 +  serve as formal comment. The first string is considered the tag name, the
   4.146 +  second its value. Note that @{attribute untagged} removes any tags of the
   4.147 +  same name.
   4.148  
   4.149 -  \<^descr> @{attribute THEN}~\<open>a\<close> composes rules by resolution; it
   4.150 -  resolves with the first premise of \<open>a\<close> (an alternative
   4.151 -  position may be also specified).  See also @{ML_op "RS"} in
   4.152 -  @{cite "isabelle-implementation"}.
   4.153 +  \<^descr> @{attribute THEN}~\<open>a\<close> composes rules by resolution; it resolves with the
   4.154 +  first premise of \<open>a\<close> (an alternative position may be also specified). See
   4.155 +  also @{ML_op "RS"} in @{cite "isabelle-implementation"}.
   4.156    
   4.157 -  \<^descr> @{attribute unfolded}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> and @{attribute
   4.158 -  folded}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> expand and fold back again the given
   4.159 -  definitions throughout a rule.
   4.160 +  \<^descr> @{attribute unfolded}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> and @{attribute folded}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>
   4.161 +  expand and fold back again the given definitions throughout a rule.
   4.162  
   4.163 -  \<^descr> @{attribute abs_def} turns an equation of the form @{prop "f x
   4.164 -  y \<equiv> t"} into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method
   4.165 -  simp} or @{method unfold} steps always expand it.  This also works
   4.166 -  for object-logic equality.
   4.167 +  \<^descr> @{attribute abs_def} turns an equation of the form @{prop "f x y \<equiv> t"}
   4.168 +  into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method simp} or @{method
   4.169 +  unfold} steps always expand it. This also works for object-logic equality.
   4.170  
   4.171 -  \<^descr> @{attribute rotated}~\<open>n\<close> rotate the premises of a
   4.172 -  theorem by \<open>n\<close> (default 1).
   4.173 +  \<^descr> @{attribute rotated}~\<open>n\<close> rotate the premises of a theorem by \<open>n\<close> (default
   4.174 +  1).
   4.175  
   4.176 -  \<^descr> @{attribute (Pure) elim_format} turns a destruction rule into
   4.177 -  elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
   4.178 -  (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
   4.179 +  \<^descr> @{attribute (Pure) elim_format} turns a destruction rule into elimination
   4.180 +  rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow> (PROP A \<Longrightarrow> PROP B) \<Longrightarrow>
   4.181 +  PROP B"}.
   4.182    
   4.183 -  Note that the Classical Reasoner (\secref{sec:classical}) provides
   4.184 -  its own version of this operation.
   4.185 +  Note that the Classical Reasoner (\secref{sec:classical}) provides its own
   4.186 +  version of this operation.
   4.187  
   4.188 -  \<^descr> @{attribute no_vars} replaces schematic variables by free
   4.189 -  ones; this is mainly for tuning output of pretty printed theorems.
   4.190 +  \<^descr> @{attribute no_vars} replaces schematic variables by free ones; this is
   4.191 +  mainly for tuning output of pretty printed theorems.
   4.192  \<close>
   4.193  
   4.194  
   4.195 @@ -197,51 +188,45 @@
   4.196      @@{method split} @{syntax thms}
   4.197    \<close>}
   4.198  
   4.199 -  These methods provide low-level facilities for equational reasoning
   4.200 -  that are intended for specialized applications only.  Normally,
   4.201 -  single step calculations would be performed in a structured text
   4.202 -  (see also \secref{sec:calculation}), while the Simplifier methods
   4.203 -  provide the canonical way for automated normalization (see
   4.204 -  \secref{sec:simplifier}).
   4.205 +  These methods provide low-level facilities for equational reasoning that are
   4.206 +  intended for specialized applications only. Normally, single step
   4.207 +  calculations would be performed in a structured text (see also
   4.208 +  \secref{sec:calculation}), while the Simplifier methods provide the
   4.209 +  canonical way for automated normalization (see \secref{sec:simplifier}).
   4.210 +
   4.211 +  \<^descr> @{method subst}~\<open>eq\<close> performs a single substitution step using rule \<open>eq\<close>,
   4.212 +  which may be either a meta or object equality.
   4.213  
   4.214 -  \<^descr> @{method subst}~\<open>eq\<close> performs a single substitution step
   4.215 -  using rule \<open>eq\<close>, which may be either a meta or object
   4.216 -  equality.
   4.217 -
   4.218 -  \<^descr> @{method subst}~\<open>(asm) eq\<close> substitutes in an
   4.219 -  assumption.
   4.220 +  \<^descr> @{method subst}~\<open>(asm) eq\<close> substitutes in an assumption.
   4.221  
   4.222 -  \<^descr> @{method subst}~\<open>(i \<dots> j) eq\<close> performs several
   4.223 -  substitutions in the conclusion. The numbers \<open>i\<close> to \<open>j\<close>
   4.224 -  indicate the positions to substitute at.  Positions are ordered from
   4.225 -  the top of the term tree moving down from left to right. For
   4.226 -  example, in \<open>(a + b) + (c + d)\<close> there are three positions
   4.227 -  where commutativity of \<open>+\<close> is applicable: 1 refers to \<open>a + b\<close>, 2 to the whole term, and 3 to \<open>c + d\<close>.
   4.228 +  \<^descr> @{method subst}~\<open>(i \<dots> j) eq\<close> performs several substitutions in the
   4.229 +  conclusion. The numbers \<open>i\<close> to \<open>j\<close> indicate the positions to substitute at.
   4.230 +  Positions are ordered from the top of the term tree moving down from left to
   4.231 +  right. For example, in \<open>(a + b) + (c + d)\<close> there are three positions where
   4.232 +  commutativity of \<open>+\<close> is applicable: 1 refers to \<open>a + b\<close>, 2 to the whole
   4.233 +  term, and 3 to \<open>c + d\<close>.
   4.234  
   4.235 -  If the positions in the list \<open>(i \<dots> j)\<close> are non-overlapping
   4.236 -  (e.g.\ \<open>(2 3)\<close> in \<open>(a + b) + (c + d)\<close>) you may
   4.237 -  assume all substitutions are performed simultaneously.  Otherwise
   4.238 -  the behaviour of \<open>subst\<close> is not specified.
   4.239 +  If the positions in the list \<open>(i \<dots> j)\<close> are non-overlapping (e.g.\ \<open>(2 3)\<close> in
   4.240 +  \<open>(a + b) + (c + d)\<close>) you may assume all substitutions are performed
   4.241 +  simultaneously. Otherwise the behaviour of \<open>subst\<close> is not specified.
   4.242  
   4.243 -  \<^descr> @{method subst}~\<open>(asm) (i \<dots> j) eq\<close> performs the
   4.244 -  substitutions in the assumptions. The positions refer to the
   4.245 -  assumptions in order from left to right.  For example, given in a
   4.246 -  goal of the form \<open>P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>\<close>, position 1 of
   4.247 -  commutativity of \<open>+\<close> is the subterm \<open>a + b\<close> and
   4.248 -  position 2 is the subterm \<open>c + d\<close>.
   4.249 +  \<^descr> @{method subst}~\<open>(asm) (i \<dots> j) eq\<close> performs the substitutions in the
   4.250 +  assumptions. The positions refer to the assumptions in order from left to
   4.251 +  right. For example, given in a goal of the form \<open>P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>\<close>,
   4.252 +  position 1 of commutativity of \<open>+\<close> is the subterm \<open>a + b\<close> and position 2 is
   4.253 +  the subterm \<open>c + d\<close>.
   4.254  
   4.255 -  \<^descr> @{method hypsubst} performs substitution using some
   4.256 -  assumption; this only works for equations of the form \<open>x =
   4.257 -  t\<close> where \<open>x\<close> is a free or bound variable.
   4.258 +  \<^descr> @{method hypsubst} performs substitution using some assumption; this only
   4.259 +  works for equations of the form \<open>x = t\<close> where \<open>x\<close> is a free or bound
   4.260 +  variable.
   4.261  
   4.262 -  \<^descr> @{method split}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> performs single-step case
   4.263 -  splitting using the given rules.  Splitting is performed in the
   4.264 -  conclusion or some assumption of the subgoal, depending of the
   4.265 -  structure of the rule.
   4.266 +  \<^descr> @{method split}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> performs single-step case splitting using the
   4.267 +  given rules. Splitting is performed in the conclusion or some assumption of
   4.268 +  the subgoal, depending of the structure of the rule.
   4.269    
   4.270 -  Note that the @{method simp} method already involves repeated
   4.271 -  application of split rules as declared in the current context, using
   4.272 -  @{attribute split}, for example.
   4.273 +  Note that the @{method simp} method already involves repeated application of
   4.274 +  split rules as declared in the current context, using @{attribute split},
   4.275 +  for example.
   4.276  \<close>
   4.277  
   4.278  
   4.279 @@ -273,6 +258,8 @@
   4.280    \begin{tabular}{rcll}
   4.281      @{method_def simp} & : & \<open>method\<close> \\
   4.282      @{method_def simp_all} & : & \<open>method\<close> \\
   4.283 +    \<open>Pure.\<close>@{method_def (Pure) simp} & : & \<open>method\<close> \\
   4.284 +    \<open>Pure.\<close>@{method_def (Pure) simp_all} & : & \<open>method\<close> \\
   4.285      @{attribute_def simp_depth_limit} & : & \<open>attribute\<close> & default \<open>100\<close> \\
   4.286    \end{tabular}
   4.287    \<^medskip>
   4.288 @@ -369,6 +356,12 @@
   4.289  
   4.290    \end{tabular}
   4.291    \end{center}
   4.292 +
   4.293 +  \<^medskip>
   4.294 +  In Isabelle/Pure, proof methods @{method (Pure) simp} and @{method (Pure)
   4.295 +  simp_all} only know about meta-equality \<open>\<equiv>\<close>. Any new object-logic needs to
   4.296 +  re-define these methods via @{ML Simplifier.method_setup} in ML:
   4.297 +  Isabelle/FOL or Isabelle/HOL may serve as blue-prints.
   4.298  \<close>
   4.299  
   4.300  
     5.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Jul 22 15:39:27 2016 +0200
     5.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Jul 22 15:39:32 2016 +0200
     5.3 @@ -1,68 +1,65 @@
     5.4  (*:maxLineLen=78:*)
     5.5  
     5.6  theory HOL_Specific
     5.7 -imports
     5.8 -  Base
     5.9 -  "~~/src/HOL/Library/Old_Datatype"
    5.10 -  "~~/src/HOL/Library/Old_Recdef"
    5.11 -  "~~/src/Tools/Adhoc_Overloading"
    5.12 -  "~~/src/HOL/Library/Dlist"
    5.13 -  "~~/src/HOL/Library/FSet"
    5.14 +  imports
    5.15 +    Main
    5.16 +    "~~/src/HOL/Library/Old_Datatype"
    5.17 +    "~~/src/HOL/Library/Old_Recdef"
    5.18 +    "~~/src/Tools/Adhoc_Overloading"
    5.19 +    "~~/src/HOL/Library/Dlist"
    5.20 +    "~~/src/HOL/Library/FSet"
    5.21 +    Base
    5.22  begin
    5.23  
    5.24  
    5.25  chapter \<open>Higher-Order Logic\<close>
    5.26  
    5.27 -text \<open>Isabelle/HOL is based on Higher-Order Logic, a polymorphic
    5.28 -  version of Church's Simple Theory of Types.  HOL can be best
    5.29 -  understood as a simply-typed version of classical set theory.  The
    5.30 -  logic was first implemented in Gordon's HOL system
    5.31 -  @{cite "mgordon-hol"}.  It extends Church's original logic
    5.32 -  @{cite "church40"} by explicit type variables (naive polymorphism) and
    5.33 -  a sound axiomatization scheme for new types based on subsets of
    5.34 -  existing types.
    5.35 -
    5.36 -  Andrews's book @{cite andrews86} is a full description of the
    5.37 -  original Church-style higher-order logic, with proofs of correctness
    5.38 -  and completeness wrt.\ certain set-theoretic interpretations.  The
    5.39 -  particular extensions of Gordon-style HOL are explained semantically
    5.40 -  in two chapters of the 1993 HOL book @{cite pitts93}.
    5.41 -
    5.42 -  Experience with HOL over decades has demonstrated that higher-order
    5.43 -  logic is widely applicable in many areas of mathematics and computer
    5.44 -  science.  In a sense, Higher-Order Logic is simpler than First-Order
    5.45 -  Logic, because there are fewer restrictions and special cases.  Note
    5.46 -  that HOL is \<^emph>\<open>weaker\<close> than FOL with axioms for ZF set theory,
    5.47 -  which is traditionally considered the standard foundation of regular
    5.48 -  mathematics, but for most applications this does not matter.  If you
    5.49 -  prefer ML to Lisp, you will probably prefer HOL to ZF.
    5.50 -
    5.51 -  \<^medskip>
    5.52 -  The syntax of HOL follows \<open>\<lambda>\<close>-calculus and
    5.53 -  functional programming.  Function application is curried.  To apply
    5.54 -  the function \<open>f\<close> of type \<open>\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3\<close> to the
    5.55 -  arguments \<open>a\<close> and \<open>b\<close> in HOL, you simply write \<open>f
    5.56 -  a b\<close> (as in ML or Haskell).  There is no ``apply'' operator; the
    5.57 -  existing application of the Pure \<open>\<lambda>\<close>-calculus is re-used.
    5.58 -  Note that in HOL \<open>f (a, b)\<close> means ``\<open>f\<close> applied to
    5.59 -  the pair \<open>(a, b)\<close> (which is notation for \<open>Pair a
    5.60 -  b\<close>).  The latter typically introduces extra formal efforts that can
    5.61 -  be avoided by currying functions by default.  Explicit tuples are as
    5.62 -  infrequent in HOL formalizations as in good ML or Haskell programs.
    5.63 -
    5.64 -  \<^medskip>
    5.65 -  Isabelle/HOL has a distinct feel, compared to other
    5.66 -  object-logics like Isabelle/ZF.  It identifies object-level types
    5.67 -  with meta-level types, taking advantage of the default
    5.68 -  type-inference mechanism of Isabelle/Pure.  HOL fully identifies
    5.69 -  object-level functions with meta-level functions, with native
    5.70 -  abstraction and application.
    5.71 -
    5.72 -  These identifications allow Isabelle to support HOL particularly
    5.73 -  nicely, but they also mean that HOL requires some sophistication
    5.74 -  from the user.  In particular, an understanding of Hindley-Milner
    5.75 -  type-inference with type-classes, which are both used extensively in
    5.76 -  the standard libraries and applications.\<close>
    5.77 +text \<open>
    5.78 +  Isabelle/HOL is based on Higher-Order Logic, a polymorphic version of
    5.79 +  Church's Simple Theory of Types. HOL can be best understood as a
    5.80 +  simply-typed version of classical set theory. The logic was first
    5.81 +  implemented in Gordon's HOL system @{cite "mgordon-hol"}. It extends
    5.82 +  Church's original logic @{cite "church40"} by explicit type variables (naive
    5.83 +  polymorphism) and a sound axiomatization scheme for new types based on
    5.84 +  subsets of existing types.
    5.85 +
    5.86 +  Andrews's book @{cite andrews86} is a full description of the original
    5.87 +  Church-style higher-order logic, with proofs of correctness and completeness
    5.88 +  wrt.\ certain set-theoretic interpretations. The particular extensions of
    5.89 +  Gordon-style HOL are explained semantically in two chapters of the 1993 HOL
    5.90 +  book @{cite pitts93}.
    5.91 +
    5.92 +  Experience with HOL over decades has demonstrated that higher-order logic is
    5.93 +  widely applicable in many areas of mathematics and computer science. In a
    5.94 +  sense, Higher-Order Logic is simpler than First-Order Logic, because there
    5.95 +  are fewer restrictions and special cases. Note that HOL is \<^emph>\<open>weaker\<close> than
    5.96 +  FOL with axioms for ZF set theory, which is traditionally considered the
    5.97 +  standard foundation of regular mathematics, but for most applications this
    5.98 +  does not matter. If you prefer ML to Lisp, you will probably prefer HOL to
    5.99 +  ZF.
   5.100 +
   5.101 +  \<^medskip> The syntax of HOL follows \<open>\<lambda>\<close>-calculus and functional programming.
   5.102 +  Function application is curried. To apply the function \<open>f\<close> of type \<open>\<tau>\<^sub>1 \<Rightarrow>
   5.103 +  \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3\<close> to the arguments \<open>a\<close> and \<open>b\<close> in HOL, you simply write \<open>f a b\<close> (as
   5.104 +  in ML or Haskell). There is no ``apply'' operator; the existing application
   5.105 +  of the Pure \<open>\<lambda>\<close>-calculus is re-used. Note that in HOL \<open>f (a, b)\<close> means ``\<open>f\<close>
   5.106 +  applied to the pair \<open>(a, b)\<close> (which is notation for \<open>Pair a b\<close>). The latter
   5.107 +  typically introduces extra formal efforts that can be avoided by currying
   5.108 +  functions by default. Explicit tuples are as infrequent in HOL
   5.109 +  formalizations as in good ML or Haskell programs.
   5.110 +
   5.111 +  \<^medskip> Isabelle/HOL has a distinct feel, compared to other object-logics like
   5.112 +  Isabelle/ZF. It identifies object-level types with meta-level types, taking
   5.113 +  advantage of the default type-inference mechanism of Isabelle/Pure. HOL
   5.114 +  fully identifies object-level functions with meta-level functions, with
   5.115 +  native abstraction and application.
   5.116 +
   5.117 +  These identifications allow Isabelle to support HOL particularly nicely, but
   5.118 +  they also mean that HOL requires some sophistication from the user. In
   5.119 +  particular, an understanding of Hindley-Milner type-inference with
   5.120 +  type-classes, which are both used extensively in the standard libraries and
   5.121 +  applications.
   5.122 +\<close>
   5.123  
   5.124  
   5.125  chapter \<open>Derived specification elements\<close>
   5.126 @@ -79,31 +76,27 @@
   5.127      @{attribute_def (HOL) mono} & : & \<open>attribute\<close> \\
   5.128    \end{matharray}
   5.129  
   5.130 -  An \<^emph>\<open>inductive definition\<close> specifies the least predicate or set
   5.131 -  \<open>R\<close> closed under given rules: applying a rule to elements of
   5.132 -  \<open>R\<close> yields a result within \<open>R\<close>.  For example, a
   5.133 -  structural operational semantics is an inductive definition of an
   5.134 -  evaluation relation.
   5.135 -
   5.136 -  Dually, a \<^emph>\<open>coinductive definition\<close> specifies the greatest
   5.137 -  predicate or set \<open>R\<close> that is consistent with given rules:
   5.138 -  every element of \<open>R\<close> can be seen as arising by applying a rule
   5.139 -  to elements of \<open>R\<close>.  An important example is using
   5.140 -  bisimulation relations to formalise equivalence of processes and
   5.141 -  infinite data structures.
   5.142 -
   5.143 -  Both inductive and coinductive definitions are based on the
   5.144 -  Knaster-Tarski fixed-point theorem for complete lattices.  The
   5.145 -  collection of introduction rules given by the user determines a
   5.146 -  functor on subsets of set-theoretic relations.  The required
   5.147 -  monotonicity of the recursion scheme is proven as a prerequisite to
   5.148 -  the fixed-point definition and the resulting consequences.  This
   5.149 -  works by pushing inclusion through logical connectives and any other
   5.150 -  operator that might be wrapped around recursive occurrences of the
   5.151 -  defined relation: there must be a monotonicity theorem of the form
   5.152 -  \<open>A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B\<close>, for each premise \<open>\<M> R t\<close> in an
   5.153 -  introduction rule.  The default rule declarations of Isabelle/HOL
   5.154 -  already take care of most common situations.
   5.155 +  An \<^emph>\<open>inductive definition\<close> specifies the least predicate or set \<open>R\<close> closed
   5.156 +  under given rules: applying a rule to elements of \<open>R\<close> yields a result within
   5.157 +  \<open>R\<close>. For example, a structural operational semantics is an inductive
   5.158 +  definition of an evaluation relation.
   5.159 +
   5.160 +  Dually, a \<^emph>\<open>coinductive definition\<close> specifies the greatest predicate or set
   5.161 +  \<open>R\<close> that is consistent with given rules: every element of \<open>R\<close> can be seen as
   5.162 +  arising by applying a rule to elements of \<open>R\<close>. An important example is using
   5.163 +  bisimulation relations to formalise equivalence of processes and infinite
   5.164 +  data structures.
   5.165 +
   5.166 +  Both inductive and coinductive definitions are based on the Knaster-Tarski
   5.167 +  fixed-point theorem for complete lattices. The collection of introduction
   5.168 +  rules given by the user determines a functor on subsets of set-theoretic
   5.169 +  relations. The required monotonicity of the recursion scheme is proven as a
   5.170 +  prerequisite to the fixed-point definition and the resulting consequences.
   5.171 +  This works by pushing inclusion through logical connectives and any other
   5.172 +  operator that might be wrapped around recursive occurrences of the defined
   5.173 +  relation: there must be a monotonicity theorem of the form \<open>A \<le> B \<Longrightarrow> \<M> A \<le> \<M>
   5.174 +  B\<close>, for each premise \<open>\<M> R t\<close> in an introduction rule. The default rule
   5.175 +  declarations of Isabelle/HOL already take care of most common situations.
   5.176  
   5.177    @{rail \<open>
   5.178      (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
   5.179 @@ -116,101 +109,98 @@
   5.180      @@{attribute (HOL) mono} (() | 'add' | 'del')
   5.181    \<close>}
   5.182  
   5.183 -  \<^descr> @{command (HOL) "inductive"} and @{command (HOL)
   5.184 -  "coinductive"} define (co)inductive predicates from the introduction
   5.185 -  rules.
   5.186 -
   5.187 -  The propositions given as \<open>clauses\<close> in the @{keyword
   5.188 -  "where"} part are either rules of the usual \<open>\<And>/\<Longrightarrow>\<close> format
   5.189 -  (with arbitrary nesting), or equalities using \<open>\<equiv>\<close>.  The
   5.190 -  latter specifies extra-logical abbreviations in the sense of
   5.191 -  @{command_ref abbreviation}.  Introducing abstract syntax
   5.192 -  simultaneously with the actual introduction rules is occasionally
   5.193 -  useful for complex specifications.
   5.194 -
   5.195 -  The optional @{keyword "for"} part contains a list of parameters of
   5.196 -  the (co)inductive predicates that remain fixed throughout the
   5.197 -  definition, in contrast to arguments of the relation that may vary
   5.198 -  in each occurrence within the given \<open>clauses\<close>.
   5.199 +  \<^descr> @{command (HOL) "inductive"} and @{command (HOL) "coinductive"} define
   5.200 +  (co)inductive predicates from the introduction rules.
   5.201 +
   5.202 +  The propositions given as \<open>clauses\<close> in the @{keyword "where"} part are
   5.203 +  either rules of the usual \<open>\<And>/\<Longrightarrow>\<close> format (with arbitrary nesting), or
   5.204 +  equalities using \<open>\<equiv>\<close>. The latter specifies extra-logical abbreviations in
   5.205 +  the sense of @{command_ref abbreviation}. Introducing abstract syntax
   5.206 +  simultaneously with the actual introduction rules is occasionally useful for
   5.207 +  complex specifications.
   5.208 +
   5.209 +  The optional @{keyword "for"} part contains a list of parameters of the
   5.210 +  (co)inductive predicates that remain fixed throughout the definition, in
   5.211 +  contrast to arguments of the relation that may vary in each occurrence
   5.212 +  within the given \<open>clauses\<close>.
   5.213  
   5.214    The optional @{keyword "monos"} declaration contains additional
   5.215 -  \<^emph>\<open>monotonicity theorems\<close>, which are required for each operator
   5.216 -  applied to a recursive set in the introduction rules.
   5.217 -
   5.218 -  \<^descr> @{command (HOL) "inductive_set"} and @{command (HOL)
   5.219 -  "coinductive_set"} are wrappers for to the previous commands for
   5.220 -  native HOL predicates.  This allows to define (co)inductive sets,
   5.221 -  where multiple arguments are simulated via tuples.
   5.222 +  \<^emph>\<open>monotonicity theorems\<close>, which are required for each operator applied to a
   5.223 +  recursive set in the introduction rules.
   5.224 +
   5.225 +  \<^descr> @{command (HOL) "inductive_set"} and @{command (HOL) "coinductive_set"}
   5.226 +  are wrappers for to the previous commands for native HOL predicates. This
   5.227 +  allows to define (co)inductive sets, where multiple arguments are simulated
   5.228 +  via tuples.
   5.229  
   5.230    \<^descr> @{command "print_inductives"} prints (co)inductive definitions and
   5.231    monotonicity rules; the ``\<open>!\<close>'' option indicates extra verbosity.
   5.232  
   5.233 -  \<^descr> @{attribute (HOL) mono} declares monotonicity rules in the
   5.234 -  context.  These rule are involved in the automated monotonicity
   5.235 -  proof of the above inductive and coinductive definitions.
   5.236 +  \<^descr> @{attribute (HOL) mono} declares monotonicity rules in the context. These
   5.237 +  rule are involved in the automated monotonicity proof of the above inductive
   5.238 +  and coinductive definitions.
   5.239  \<close>
   5.240  
   5.241  
   5.242  subsection \<open>Derived rules\<close>
   5.243  
   5.244 -text \<open>A (co)inductive definition of \<open>R\<close> provides the following
   5.245 -  main theorems:
   5.246 -
   5.247 -  \<^descr> \<open>R.intros\<close> is the list of introduction rules as proven
   5.248 -  theorems, for the recursive predicates (or sets).  The rules are
   5.249 -  also available individually, using the names given them in the
   5.250 -  theory file;
   5.251 +text \<open>
   5.252 +  A (co)inductive definition of \<open>R\<close> provides the following main theorems:
   5.253 +
   5.254 +  \<^descr> \<open>R.intros\<close> is the list of introduction rules as proven theorems, for the
   5.255 +  recursive predicates (or sets). The rules are also available individually,
   5.256 +  using the names given them in the theory file;
   5.257  
   5.258    \<^descr> \<open>R.cases\<close> is the case analysis (or elimination) rule;
   5.259  
   5.260 -  \<^descr> \<open>R.induct\<close> or \<open>R.coinduct\<close> is the (co)induction
   5.261 -  rule;
   5.262 -
   5.263 -  \<^descr> \<open>R.simps\<close> is the equation unrolling the fixpoint of the
   5.264 -  predicate one step.
   5.265 -
   5.266 -
   5.267 -  When several predicates \<open>R\<^sub>1, \<dots>, R\<^sub>n\<close> are defined simultaneously,
   5.268 -  the list of introduction rules is called \<open>R\<^sub>1_\<dots>_R\<^sub>n.intros\<close>, the
   5.269 -  case analysis rules are called \<open>R\<^sub>1.cases, \<dots>, R\<^sub>n.cases\<close>, and the
   5.270 -  list of mutual induction rules is called \<open>R\<^sub>1_\<dots>_R\<^sub>n.inducts\<close>.
   5.271 +  \<^descr> \<open>R.induct\<close> or \<open>R.coinduct\<close> is the (co)induction rule;
   5.272 +
   5.273 +  \<^descr> \<open>R.simps\<close> is the equation unrolling the fixpoint of the predicate one
   5.274 +  step.
   5.275 +
   5.276 +
   5.277 +  When several predicates \<open>R\<^sub>1, \<dots>, R\<^sub>n\<close> are defined simultaneously, the list
   5.278 +  of introduction rules is called \<open>R\<^sub>1_\<dots>_R\<^sub>n.intros\<close>, the case analysis rules
   5.279 +  are called \<open>R\<^sub>1.cases, \<dots>, R\<^sub>n.cases\<close>, and the list of mutual induction rules
   5.280 +  is called \<open>R\<^sub>1_\<dots>_R\<^sub>n.inducts\<close>.
   5.281  \<close>
   5.282  
   5.283  
   5.284  subsection \<open>Monotonicity theorems\<close>
   5.285  
   5.286 -text \<open>The context maintains a default set of theorems that are used
   5.287 -  in monotonicity proofs.  New rules can be declared via the
   5.288 -  @{attribute (HOL) mono} attribute.  See the main Isabelle/HOL
   5.289 -  sources for some examples.  The general format of such monotonicity
   5.290 -  theorems is as follows:
   5.291 -
   5.292 -  \<^item> Theorems of the form \<open>A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B\<close>, for proving
   5.293 -  monotonicity of inductive definitions whose introduction rules have
   5.294 -  premises involving terms such as \<open>\<M> R t\<close>.
   5.295 -
   5.296 -  \<^item> Monotonicity theorems for logical operators, which are of the
   5.297 -  general form \<open>(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>\<close>.  For example, in
   5.298 -  the case of the operator \<open>\<or>\<close>, the corresponding theorem is
   5.299 +text \<open>
   5.300 +  The context maintains a default set of theorems that are used in
   5.301 +  monotonicity proofs. New rules can be declared via the @{attribute (HOL)
   5.302 +  mono} attribute. See the main Isabelle/HOL sources for some examples. The
   5.303 +  general format of such monotonicity theorems is as follows:
   5.304 +
   5.305 +  \<^item> Theorems of the form \<open>A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B\<close>, for proving monotonicity of
   5.306 +  inductive definitions whose introduction rules have premises involving terms
   5.307 +  such as \<open>\<M> R t\<close>.
   5.308 +
   5.309 +  \<^item> Monotonicity theorems for logical operators, which are of the general form
   5.310 +  \<open>(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>\<close>. For example, in the case of the operator \<open>\<or>\<close>,
   5.311 +  the corresponding theorem is
   5.312    \[
   5.313    \infer{\<open>P\<^sub>1 \<or> P\<^sub>2 \<longrightarrow> Q\<^sub>1 \<or> Q\<^sub>2\<close>}{\<open>P\<^sub>1 \<longrightarrow> Q\<^sub>1\<close> & \<open>P\<^sub>2 \<longrightarrow> Q\<^sub>2\<close>}
   5.314    \]
   5.315  
   5.316 -  \<^item> De Morgan style equations for reasoning about the ``polarity''
   5.317 -  of expressions, e.g.
   5.318 +  \<^item> De Morgan style equations for reasoning about the ``polarity'' of
   5.319 +  expressions, e.g.
   5.320    \[
   5.321    @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad
   5.322    @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}
   5.323    \]
   5.324  
   5.325 -  \<^item> Equations for reducing complex operators to more primitive
   5.326 -  ones whose monotonicity can easily be proved, e.g.
   5.327 +  \<^item> Equations for reducing complex operators to more primitive ones whose
   5.328 +  monotonicity can easily be proved, e.g.
   5.329    \[
   5.330    @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad
   5.331    @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}
   5.332    \]
   5.333  \<close>
   5.334  
   5.335 +
   5.336  subsubsection \<open>Examples\<close>
   5.337  
   5.338  text \<open>The finite powerset operator can be defined inductively like this:\<close>
   5.339 @@ -228,9 +218,10 @@
   5.340  where acc: "(\<And>y. y \<prec> x \<Longrightarrow> acc r y) \<Longrightarrow> acc r x"
   5.341  (*<*)end(*>*)
   5.342  
   5.343 -text \<open>Common logical connectives can be easily characterized as
   5.344 -  non-recursive inductive definitions with parameters, but without
   5.345 -  arguments.\<close>
   5.346 +text \<open>
   5.347 +  Common logical connectives can be easily characterized as non-recursive
   5.348 +  inductive definitions with parameters, but without arguments.
   5.349 +\<close>
   5.350  
   5.351  (*<*)experiment begin(*>*)
   5.352  inductive AND for A B :: bool
   5.353 @@ -244,12 +235,13 @@
   5.354  where "B a \<Longrightarrow> EXISTS B"
   5.355  (*<*)end(*>*)
   5.356  
   5.357 -text \<open>Here the \<open>cases\<close> or \<open>induct\<close> rules produced by the
   5.358 -  @{command inductive} package coincide with the expected elimination rules
   5.359 -  for Natural Deduction. Already in the original article by Gerhard Gentzen
   5.360 -  @{cite "Gentzen:1935"} there is a hint that each connective can be
   5.361 -  characterized by its introductions, and the elimination can be constructed
   5.362 -  systematically.\<close>
   5.363 +text \<open>
   5.364 +  Here the \<open>cases\<close> or \<open>induct\<close> rules produced by the @{command inductive}
   5.365 +  package coincide with the expected elimination rules for Natural Deduction.
   5.366 +  Already in the original article by Gerhard Gentzen @{cite "Gentzen:1935"}
   5.367 +  there is a hint that each connective can be characterized by its
   5.368 +  introductions, and the elimination can be constructed systematically.
   5.369 +\<close>
   5.370  
   5.371  
   5.372  section \<open>Recursive functions \label{sec:recursion}\<close>
   5.373 @@ -275,22 +267,21 @@
   5.374      @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
   5.375    \<close>}
   5.376  
   5.377 -  \<^descr> @{command (HOL) "primrec"} defines primitive recursive functions
   5.378 -  over datatypes (see also @{command_ref (HOL) datatype}). The given \<open>equations\<close> specify reduction rules that are produced by instantiating the
   5.379 -  generic combinator for primitive recursion that is available for each
   5.380 -  datatype.
   5.381 +  \<^descr> @{command (HOL) "primrec"} defines primitive recursive functions over
   5.382 +  datatypes (see also @{command_ref (HOL) datatype}). The given \<open>equations\<close>
   5.383 +  specify reduction rules that are produced by instantiating the generic
   5.384 +  combinator for primitive recursion that is available for each datatype.
   5.385  
   5.386    Each equation needs to be of the form:
   5.387  
   5.388    @{text [display] "f x\<^sub>1 \<dots> x\<^sub>m (C y\<^sub>1 \<dots> y\<^sub>k) z\<^sub>1 \<dots> z\<^sub>n = rhs"}
   5.389  
   5.390 -  such that \<open>C\<close> is a datatype constructor, \<open>rhs\<close> contains only
   5.391 -  the free variables on the left-hand side (or from the context), and all
   5.392 -  recursive occurrences of \<open>f\<close> in \<open>rhs\<close> are of the form
   5.393 -  \<open>f \<dots> y\<^sub>i \<dots>\<close> for some \<open>i\<close>. At most one reduction rule for
   5.394 -  each constructor can be given. The order does not matter. For missing
   5.395 -  constructors, the function is defined to return a default value, but this
   5.396 -  equation is made difficult to access for users.
   5.397 +  such that \<open>C\<close> is a datatype constructor, \<open>rhs\<close> contains only the free
   5.398 +  variables on the left-hand side (or from the context), and all recursive
   5.399 +  occurrences of \<open>f\<close> in \<open>rhs\<close> are of the form \<open>f \<dots> y\<^sub>i \<dots>\<close> for some \<open>i\<close>. At
   5.400 +  most one reduction rule for each constructor can be given. The order does
   5.401 +  not matter. For missing constructors, the function is defined to return a
   5.402 +  default value, but this equation is made difficult to access for users.
   5.403  
   5.404    The reduction rules are declared as @{attribute simp} by default, which
   5.405    enables standard proof methods like @{method simp} and @{method auto} to
   5.406 @@ -304,62 +295,62 @@
   5.407    command generates proof obligations for the completeness and the
   5.408    compatibility of patterns.
   5.409  
   5.410 -  The defined function is considered partial, and the resulting
   5.411 -  simplification rules (named \<open>f.psimps\<close>) and induction rule (named
   5.412 -  \<open>f.pinduct\<close>) are guarded by a generated domain predicate \<open>f_dom\<close>. The @{command (HOL) "termination"} command can then be used to
   5.413 -  establish that the function is total.
   5.414 +  The defined function is considered partial, and the resulting simplification
   5.415 +  rules (named \<open>f.psimps\<close>) and induction rule (named \<open>f.pinduct\<close>) are guarded
   5.416 +  by a generated domain predicate \<open>f_dom\<close>. The @{command (HOL) "termination"}
   5.417 +  command can then be used to establish that the function is total.
   5.418  
   5.419    \<^descr> @{command (HOL) "fun"} is a shorthand notation for ``@{command (HOL)
   5.420 -  "function"}~\<open>(sequential)\<close>'', followed by automated proof attempts
   5.421 -  regarding pattern matching and termination. See @{cite
   5.422 -  "isabelle-function"} for further details.
   5.423 -
   5.424 -  \<^descr> @{command (HOL) "termination"}~\<open>f\<close> commences a termination
   5.425 -  proof for the previously defined function \<open>f\<close>. If this is omitted,
   5.426 -  the command refers to the most recent function definition. After the proof
   5.427 -  is closed, the recursive equations and the induction principle is
   5.428 -  established.
   5.429 -
   5.430 -  \<^descr> @{command (HOL) "fun_cases"} generates specialized elimination rules
   5.431 -  for function equations. It expects one or more function equations and
   5.432 -  produces rules that eliminate the given equalities, following the cases
   5.433 -  given in the function definition.
   5.434 -
   5.435 -
   5.436 -  Recursive definitions introduced by the @{command (HOL) "function"}
   5.437 -  command accommodate reasoning by induction (cf.\ @{method induct}): rule
   5.438 -  \<open>f.induct\<close> refers to a specific induction rule, with parameters
   5.439 -  named according to the user-specified equations. Cases are numbered
   5.440 -  starting from 1. For @{command (HOL) "primrec"}, the induction principle
   5.441 -  coincides with structural recursion on the datatype where the recursion is
   5.442 -  carried out.
   5.443 +  "function"}~\<open>(sequential)\<close>'', followed by automated proof attempts regarding
   5.444 +  pattern matching and termination. See @{cite "isabelle-function"} for
   5.445 +  further details.
   5.446 +
   5.447 +  \<^descr> @{command (HOL) "termination"}~\<open>f\<close> commences a termination proof for the
   5.448 +  previously defined function \<open>f\<close>. If this is omitted, the command refers to
   5.449 +  the most recent function definition. After the proof is closed, the
   5.450 +  recursive equations and the induction principle is established.
   5.451 +
   5.452 +  \<^descr> @{command (HOL) "fun_cases"} generates specialized elimination rules for
   5.453 +  function equations. It expects one or more function equations and produces
   5.454 +  rules that eliminate the given equalities, following the cases given in the
   5.455 +  function definition.
   5.456 +
   5.457 +
   5.458 +  Recursive definitions introduced by the @{command (HOL) "function"} command
   5.459 +  accommodate reasoning by induction (cf.\ @{method induct}): rule \<open>f.induct\<close>
   5.460 +  refers to a specific induction rule, with parameters named according to the
   5.461 +  user-specified equations. Cases are numbered starting from 1. For @{command
   5.462 +  (HOL) "primrec"}, the induction principle coincides with structural
   5.463 +  recursion on the datatype where the recursion is carried out.
   5.464  
   5.465    The equations provided by these packages may be referred later as theorem
   5.466 -  list \<open>f.simps\<close>, where \<open>f\<close> is the (collective) name of the
   5.467 -  functions defined. Individual equations may be named explicitly as well.
   5.468 +  list \<open>f.simps\<close>, where \<open>f\<close> is the (collective) name of the functions defined.
   5.469 +  Individual equations may be named explicitly as well.
   5.470  
   5.471    The @{command (HOL) "function"} command accepts the following options.
   5.472  
   5.473 -  \<^descr> \<open>sequential\<close> enables a preprocessor which disambiguates
   5.474 -  overlapping patterns by making them mutually disjoint. Earlier equations
   5.475 -  take precedence over later ones. This allows to give the specification in
   5.476 -  a format very similar to functional programming. Note that the resulting
   5.477 -  simplification and induction rules correspond to the transformed
   5.478 -  specification, not the one given originally. This usually means that each
   5.479 -  equation given by the user may result in several theorems. Also note that
   5.480 -  this automatic transformation only works for ML-style datatype patterns.
   5.481 -
   5.482 -  \<^descr> \<open>domintros\<close> enables the automated generation of introduction
   5.483 -  rules for the domain predicate. While mostly not needed, they can be
   5.484 -  helpful in some proofs about partial functions.
   5.485 +  \<^descr> \<open>sequential\<close> enables a preprocessor which disambiguates overlapping
   5.486 +  patterns by making them mutually disjoint. Earlier equations take precedence
   5.487 +  over later ones. This allows to give the specification in a format very
   5.488 +  similar to functional programming. Note that the resulting simplification
   5.489 +  and induction rules correspond to the transformed specification, not the one
   5.490 +  given originally. This usually means that each equation given by the user
   5.491 +  may result in several theorems. Also note that this automatic transformation
   5.492 +  only works for ML-style datatype patterns.
   5.493 +
   5.494 +  \<^descr> \<open>domintros\<close> enables the automated generation of introduction rules for the
   5.495 +  domain predicate. While mostly not needed, they can be helpful in some
   5.496 +  proofs about partial functions.
   5.497  \<close>
   5.498  
   5.499  
   5.500  subsubsection \<open>Example: evaluation of expressions\<close>
   5.501  
   5.502 -text \<open>Subsequently, we define mutual datatypes for arithmetic and boolean
   5.503 -  expressions, and use @{command primrec} for evaluation functions that
   5.504 -  follow the same recursive structure.\<close>
   5.505 +text \<open>
   5.506 +  Subsequently, we define mutual datatypes for arithmetic and boolean
   5.507 +  expressions, and use @{command primrec} for evaluation functions that follow
   5.508 +  the same recursive structure.
   5.509 +\<close>
   5.510  
   5.511  (*<*)experiment begin(*>*)
   5.512  datatype 'a aexp =
   5.513 @@ -387,16 +378,15 @@
   5.514  | "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
   5.515  | "evalb env (Neg b) = (\<not> evalb env b)"
   5.516  
   5.517 -text \<open>Since the value of an expression depends on the value of its
   5.518 -  variables, the functions @{const evala} and @{const evalb} take an
   5.519 -  additional parameter, an \<^emph>\<open>environment\<close> that maps variables to their
   5.520 -  values.
   5.521 +text \<open>
   5.522 +  Since the value of an expression depends on the value of its variables, the
   5.523 +  functions @{const evala} and @{const evalb} take an additional parameter, an
   5.524 +  \<^emph>\<open>environment\<close> that maps variables to their values.
   5.525  
   5.526    \<^medskip>
   5.527 -  Substitution on expressions can be defined similarly. The mapping
   5.528 -  \<open>f\<close> of type @{typ "'a \<Rightarrow> 'a aexp"} given as a parameter is lifted
   5.529 -  canonically on the types @{typ "'a aexp"} and @{typ "'a bexp"},
   5.530 -  respectively.
   5.531 +  Substitution on expressions can be defined similarly. The mapping \<open>f\<close> of
   5.532 +  type @{typ "'a \<Rightarrow> 'a aexp"} given as a parameter is lifted canonically on the
   5.533 +  types @{typ "'a aexp"} and @{typ "'a bexp"}, respectively.
   5.534  \<close>
   5.535  
   5.536  primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
   5.537 @@ -411,10 +401,11 @@
   5.538  | "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
   5.539  | "substb f (Neg b) = Neg (substb f b)"
   5.540  
   5.541 -text \<open>In textbooks about semantics one often finds substitution theorems,
   5.542 -  which express the relationship between substitution and evaluation. For
   5.543 -  @{typ "'a aexp"} and @{typ "'a bexp"}, we can prove such a theorem by
   5.544 -  mutual induction, followed by simplification.
   5.545 +text \<open>
   5.546 +  In textbooks about semantics one often finds substitution theorems, which
   5.547 +  express the relationship between substitution and evaluation. For @{typ "'a
   5.548 +  aexp"} and @{typ "'a bexp"}, we can prove such a theorem by mutual
   5.549 +  induction, followed by simplification.
   5.550  \<close>
   5.551  
   5.552  lemma subst_one:
   5.553 @@ -437,9 +428,10 @@
   5.554  (*<*)experiment begin(*>*)
   5.555  datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
   5.556  
   5.557 -text \<open>A substitution function on type @{typ "('a, 'b) term"} can be
   5.558 -  defined as follows, by working simultaneously on @{typ "('a, 'b)
   5.559 -  term list"}:\<close>
   5.560 +text \<open>
   5.561 +  A substitution function on type @{typ "('a, 'b) term"} can be defined as
   5.562 +  follows, by working simultaneously on @{typ "('a, 'b) term list"}:
   5.563 +\<close>
   5.564  
   5.565  primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term" and
   5.566    subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
   5.567 @@ -449,9 +441,10 @@
   5.568  | "subst_term_list f [] = []"
   5.569  | "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
   5.570  
   5.571 -text \<open>The recursion scheme follows the structure of the unfolded
   5.572 -  definition of type @{typ "('a, 'b) term"}.  To prove properties of this
   5.573 -  substitution function, mutual induction is needed:
   5.574 +text \<open>
   5.575 +  The recursion scheme follows the structure of the unfolded definition of
   5.576 +  type @{typ "('a, 'b) term"}. To prove properties of this substitution
   5.577 +  function, mutual induction is needed:
   5.578  \<close>
   5.579  
   5.580  lemma "subst_term (subst_term f1 \<circ> f2) t =
   5.581 @@ -475,9 +468,9 @@
   5.582    "map_tree f (Atom a) = Atom (f a)"
   5.583  | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
   5.584  
   5.585 -text \<open>Note that all occurrences of functions such as \<open>ts\<close> above must
   5.586 -  be applied to an argument. In particular, @{term "map_tree f \<circ> ts"} is not
   5.587 -  allowed here.
   5.588 +text \<open>
   5.589 +  Note that all occurrences of functions such as \<open>ts\<close> above must be applied to
   5.590 +  an argument. In particular, @{term "map_tree f \<circ> ts"} is not allowed here.
   5.591  
   5.592    \<^medskip>
   5.593    Here is a simple composition lemma for @{term map_tree}:
   5.594 @@ -511,45 +504,42 @@
   5.595      orders: ( 'max' | 'min' | 'ms' ) *
   5.596    \<close>}
   5.597  
   5.598 -  \<^descr> @{method (HOL) pat_completeness} is a specialized method to
   5.599 -  solve goals regarding the completeness of pattern matching, as
   5.600 -  required by the @{command (HOL) "function"} package (cf.\
   5.601 -  @{cite "isabelle-function"}).
   5.602 -
   5.603 -  \<^descr> @{method (HOL) relation}~\<open>R\<close> introduces a termination
   5.604 -  proof using the relation \<open>R\<close>.  The resulting proof state will
   5.605 -  contain goals expressing that \<open>R\<close> is wellfounded, and that the
   5.606 -  arguments of recursive calls decrease with respect to \<open>R\<close>.
   5.607 -  Usually, this method is used as the initial proof step of manual
   5.608 -  termination proofs.
   5.609 -
   5.610 -  \<^descr> @{method (HOL) "lexicographic_order"} attempts a fully
   5.611 -  automated termination proof by searching for a lexicographic
   5.612 -  combination of size measures on the arguments of the function. The
   5.613 -  method accepts the same arguments as the @{method auto} method,
   5.614 -  which it uses internally to prove local descents.  The @{syntax
   5.615 -  clasimpmod} modifiers are accepted (as for @{method auto}).
   5.616 -
   5.617 -  In case of failure, extensive information is printed, which can help
   5.618 -  to analyse the situation (cf.\ @{cite "isabelle-function"}).
   5.619 -
   5.620 -  \<^descr> @{method (HOL) "size_change"} also works on termination goals,
   5.621 -  using a variation of the size-change principle, together with a
   5.622 -  graph decomposition technique (see @{cite krauss_phd} for details).
   5.623 -  Three kinds of orders are used internally: \<open>max\<close>, \<open>min\<close>,
   5.624 -  and \<open>ms\<close> (multiset), which is only available when the theory
   5.625 -  \<open>Multiset\<close> is loaded. When no order kinds are given, they are
   5.626 -  tried in order. The search for a termination proof uses SAT solving
   5.627 +  \<^descr> @{method (HOL) pat_completeness} is a specialized method to solve goals
   5.628 +  regarding the completeness of pattern matching, as required by the @{command
   5.629 +  (HOL) "function"} package (cf.\ @{cite "isabelle-function"}).
   5.630 +
   5.631 +  \<^descr> @{method (HOL) relation}~\<open>R\<close> introduces a termination proof using the
   5.632 +  relation \<open>R\<close>. The resulting proof state will contain goals expressing that
   5.633 +  \<open>R\<close> is wellfounded, and that the arguments of recursive calls decrease with
   5.634 +  respect to \<open>R\<close>. Usually, this method is used as the initial proof step of
   5.635 +  manual termination proofs.
   5.636 +
   5.637 +  \<^descr> @{method (HOL) "lexicographic_order"} attempts a fully automated
   5.638 +  termination proof by searching for a lexicographic combination of size
   5.639 +  measures on the arguments of the function. The method accepts the same
   5.640 +  arguments as the @{method auto} method, which it uses internally to prove
   5.641 +  local descents. The @{syntax clasimpmod} modifiers are accepted (as for
   5.642 +  @{method auto}).
   5.643 +
   5.644 +  In case of failure, extensive information is printed, which can help to
   5.645 +  analyse the situation (cf.\ @{cite "isabelle-function"}).
   5.646 +
   5.647 +  \<^descr> @{method (HOL) "size_change"} also works on termination goals, using a
   5.648 +  variation of the size-change principle, together with a graph decomposition
   5.649 +  technique (see @{cite krauss_phd} for details). Three kinds of orders are
   5.650 +  used internally: \<open>max\<close>, \<open>min\<close>, and \<open>ms\<close> (multiset), which is only available
   5.651 +  when the theory \<open>Multiset\<close> is loaded. When no order kinds are given, they
   5.652 +  are tried in order. The search for a termination proof uses SAT solving
   5.653    internally.
   5.654  
   5.655 -  For local descent proofs, the @{syntax clasimpmod} modifiers are
   5.656 -  accepted (as for @{method auto}).
   5.657 -
   5.658 -  \<^descr> @{method (HOL) induction_schema} derives user-specified
   5.659 -  induction rules from well-founded induction and completeness of
   5.660 -  patterns. This factors out some operations that are done internally
   5.661 -  by the function package and makes them available separately. See
   5.662 -  @{file "~~/src/HOL/ex/Induction_Schema.thy"} for examples.
   5.663 +  For local descent proofs, the @{syntax clasimpmod} modifiers are accepted
   5.664 +  (as for @{method auto}).
   5.665 +
   5.666 +  \<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
   5.667 +  from well-founded induction and completeness of patterns. This factors out
   5.668 +  some operations that are done internally by the function package and makes
   5.669 +  them available separately. See @{file "~~/src/HOL/ex/Induction_Schema.thy"}
   5.670 +  for examples.
   5.671  \<close>
   5.672  
   5.673  
   5.674 @@ -566,51 +556,45 @@
   5.675        @{syntax specification}
   5.676    \<close>}
   5.677  
   5.678 -  \<^descr> @{command (HOL) "partial_function"}~\<open>(mode)\<close> defines
   5.679 -  recursive functions based on fixpoints in complete partial
   5.680 -  orders. No termination proof is required from the user or
   5.681 -  constructed internally. Instead, the possibility of non-termination
   5.682 -  is modelled explicitly in the result type, which contains an
   5.683 -  explicit bottom element.
   5.684 -
   5.685 -  Pattern matching and mutual recursion are currently not supported.
   5.686 -  Thus, the specification consists of a single function described by a
   5.687 -  single recursive equation.
   5.688 -
   5.689 -  There are no fixed syntactic restrictions on the body of the
   5.690 -  function, but the induced functional must be provably monotonic
   5.691 -  wrt.\ the underlying order.  The monotonicity proof is performed
   5.692 -  internally, and the definition is rejected when it fails. The proof
   5.693 -  can be influenced by declaring hints using the
   5.694 -  @{attribute (HOL) partial_function_mono} attribute.
   5.695 -
   5.696 -  The mandatory \<open>mode\<close> argument specifies the mode of operation
   5.697 -  of the command, which directly corresponds to a complete partial
   5.698 -  order on the result type. By default, the following modes are
   5.699 -  defined:
   5.700 -
   5.701 -    \<^descr> \<open>option\<close> defines functions that map into the @{type
   5.702 -    option} type. Here, the value @{term None} is used to model a
   5.703 -    non-terminating computation. Monotonicity requires that if @{term
   5.704 -    None} is returned by a recursive call, then the overall result must
   5.705 -    also be @{term None}. This is best achieved through the use of the
   5.706 -    monadic operator @{const "Option.bind"}.
   5.707 -
   5.708 -    \<^descr> \<open>tailrec\<close> defines functions with an arbitrary result
   5.709 -    type and uses the slightly degenerated partial order where @{term
   5.710 -    "undefined"} is the bottom element.  Now, monotonicity requires that
   5.711 -    if @{term undefined} is returned by a recursive call, then the
   5.712 -    overall result must also be @{term undefined}. In practice, this is
   5.713 -    only satisfied when each recursive call is a tail call, whose result
   5.714 -    is directly returned. Thus, this mode of operation allows the
   5.715 -    definition of arbitrary tail-recursive functions.
   5.716 -
   5.717 -  Experienced users may define new modes by instantiating the locale
   5.718 -  @{const "partial_function_definitions"} appropriately.
   5.719 -
   5.720 -  \<^descr> @{attribute (HOL) partial_function_mono} declares rules for
   5.721 -  use in the internal monotonicity proofs of partial function
   5.722 -  definitions.
   5.723 +  \<^descr> @{command (HOL) "partial_function"}~\<open>(mode)\<close> defines recursive functions
   5.724 +  based on fixpoints in complete partial orders. No termination proof is
   5.725 +  required from the user or constructed internally. Instead, the possibility
   5.726 +  of non-termination is modelled explicitly in the result type, which contains
   5.727 +  an explicit bottom element.
   5.728 +
   5.729 +  Pattern matching and mutual recursion are currently not supported. Thus, the
   5.730 +  specification consists of a single function described by a single recursive
   5.731 +  equation.
   5.732 +
   5.733 +  There are no fixed syntactic restrictions on the body of the function, but
   5.734 +  the induced functional must be provably monotonic wrt.\ the underlying
   5.735 +  order. The monotonicity proof is performed internally, and the definition is
   5.736 +  rejected when it fails. The proof can be influenced by declaring hints using
   5.737 +  the @{attribute (HOL) partial_function_mono} attribute.
   5.738 +
   5.739 +  The mandatory \<open>mode\<close> argument specifies the mode of operation of the
   5.740 +  command, which directly corresponds to a complete partial order on the
   5.741 +  result type. By default, the following modes are defined:
   5.742 +
   5.743 +    \<^descr> \<open>option\<close> defines functions that map into the @{type option} type. Here,
   5.744 +    the value @{term None} is used to model a non-terminating computation.
   5.745 +    Monotonicity requires that if @{term None} is returned by a recursive
   5.746 +    call, then the overall result must also be @{term None}. This is best
   5.747 +    achieved through the use of the monadic operator @{const "Option.bind"}.
   5.748 +
   5.749 +    \<^descr> \<open>tailrec\<close> defines functions with an arbitrary result type and uses the
   5.750 +    slightly degenerated partial order where @{term "undefined"} is the bottom
   5.751 +    element. Now, monotonicity requires that if @{term undefined} is returned
   5.752 +    by a recursive call, then the overall result must also be @{term
   5.753 +    undefined}. In practice, this is only satisfied when each recursive call
   5.754 +    is a tail call, whose result is directly returned. Thus, this mode of
   5.755 +    operation allows the definition of arbitrary tail-recursive functions.
   5.756 +
   5.757 +  Experienced users may define new modes by instantiating the locale @{const
   5.758 +  "partial_function_definitions"} appropriately.
   5.759 +
   5.760 +  \<^descr> @{attribute (HOL) partial_function_mono} declares rules for use in the
   5.761 +  internal monotonicity proofs of partial function definitions.
   5.762  \<close>
   5.763  
   5.764  
   5.765 @@ -635,21 +619,19 @@
   5.766        (() | 'add' | 'del') ':' @{syntax thms}) | @{syntax clasimpmod}
   5.767    \<close>}
   5.768  
   5.769 -  \<^descr> @{command (HOL) "recdef"} defines general well-founded
   5.770 -  recursive functions (using the TFL package).  The
   5.771 -  ``\<open>(permissive)\<close>'' option tells TFL to recover from
   5.772 -  failed proof attempts, returning unfinished results.  The
   5.773 -  \<open>recdef_simp\<close>, \<open>recdef_cong\<close>, and
   5.774 -  \<open>recdef_wf\<close> hints refer to auxiliary rules to be used
   5.775 -  in the internal automated proof process of TFL.  Additional
   5.776 -  @{syntax clasimpmod} declarations may be given to tune the context
   5.777 -  of the Simplifier (cf.\ \secref{sec:simplifier}) and Classical
   5.778 -  reasoner (cf.\ \secref{sec:classical}).
   5.779 +  \<^descr> @{command (HOL) "recdef"} defines general well-founded recursive functions
   5.780 +  (using the TFL package). The ``\<open>(permissive)\<close>'' option tells TFL to recover
   5.781 +  from failed proof attempts, returning unfinished results. The \<open>recdef_simp\<close>,
   5.782 +  \<open>recdef_cong\<close>, and \<open>recdef_wf\<close> hints refer to auxiliary rules to be used in
   5.783 +  the internal automated proof process of TFL. Additional @{syntax clasimpmod}
   5.784 +  declarations may be given to tune the context of the Simplifier (cf.\
   5.785 +  \secref{sec:simplifier}) and Classical reasoner (cf.\
   5.786 +  \secref{sec:classical}).
   5.787  
   5.788  
   5.789    \<^medskip>
   5.790 -  Hints for @{command (HOL) "recdef"} may be also declared
   5.791 -  globally, using the following attributes.
   5.792 +  Hints for @{command (HOL) "recdef"} may be also declared globally, using the
   5.793 +  following attributes.
   5.794  
   5.795    \begin{matharray}{rcl}
   5.796      @{attribute_def (HOL) recdef_simp} & : & \<open>attribute\<close> \\
   5.797 @@ -674,11 +656,10 @@
   5.798    \end{tabular}
   5.799  
   5.800    \<^medskip>
   5.801 -  Adhoc overloading allows to overload a constant depending on
   5.802 -  its type. Typically this involves the introduction of an
   5.803 -  uninterpreted constant (used for input and output) and the addition
   5.804 -  of some variants (used internally). For examples see
   5.805 -  @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and
   5.806 +  Adhoc overloading allows to overload a constant depending on its type.
   5.807 +  Typically this involves the introduction of an uninterpreted constant (used
   5.808 +  for input and output) and the addition of some variants (used internally).
   5.809 +  For examples see @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and
   5.810    @{file "~~/src/HOL/Library/Monad_Syntax.thy"}.
   5.811  
   5.812    @{rail \<open>
   5.813 @@ -686,18 +667,17 @@
   5.814        (@{syntax name} (@{syntax term} + ) + @'and')
   5.815    \<close>}
   5.816  
   5.817 -  \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close>
   5.818 -  associates variants with an existing constant.
   5.819 -
   5.820 -  \<^descr> @{command "no_adhoc_overloading"} is similar to
   5.821 -  @{command "adhoc_overloading"}, but removes the specified variants
   5.822 -  from the present context.
   5.823 -
   5.824 -  \<^descr> @{attribute "show_variants"} controls printing of variants
   5.825 -  of overloaded constants. If enabled, the internally used variants
   5.826 -  are printed instead of their respective overloaded constants. This
   5.827 -  is occasionally useful to check whether the system agrees with a
   5.828 -  user's expectations about derived variants.
   5.829 +  \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close> associates variants with an
   5.830 +  existing constant.
   5.831 +
   5.832 +  \<^descr> @{command "no_adhoc_overloading"} is similar to @{command
   5.833 +  "adhoc_overloading"}, but removes the specified variants from the present
   5.834 +  context.
   5.835 +
   5.836 +  \<^descr> @{attribute "show_variants"} controls printing of variants of overloaded
   5.837 +  constants. If enabled, the internally used variants are printed instead of
   5.838 +  their respective overloaded constants. This is occasionally useful to check
   5.839 +  whether the system agrees with a user's expectations about derived variants.
   5.840  \<close>
   5.841  
   5.842  
   5.843 @@ -715,17 +695,16 @@
   5.844      decl: (@{syntax name} ':')? @{syntax term} ('(' @'overloaded' ')')?
   5.845    \<close>}
   5.846  
   5.847 -  \<^descr> @{command (HOL) "specification"}~\<open>decls \<phi>\<close> sets up a
   5.848 -  goal stating the existence of terms with the properties specified to
   5.849 -  hold for the constants given in \<open>decls\<close>.  After finishing the
   5.850 -  proof, the theory will be augmented with definitions for the given
   5.851 -  constants, as well as with theorems stating the properties for these
   5.852 -  constants.
   5.853 -
   5.854 -  \<open>decl\<close> declares a constant to be defined by the
   5.855 -  specification given.  The definition for the constant \<open>c\<close> is
   5.856 -  bound to the name \<open>c_def\<close> unless a theorem name is given in
   5.857 -  the declaration.  Overloaded constants should be declared as such.
   5.858 +  \<^descr> @{command (HOL) "specification"}~\<open>decls \<phi>\<close> sets up a goal stating the
   5.859 +  existence of terms with the properties specified to hold for the constants
   5.860 +  given in \<open>decls\<close>. After finishing the proof, the theory will be augmented
   5.861 +  with definitions for the given constants, as well as with theorems stating
   5.862 +  the properties for these constants.
   5.863 +
   5.864 +  \<open>decl\<close> declares a constant to be defined by the specification given. The
   5.865 +  definition for the constant \<open>c\<close> is bound to the name \<open>c_def\<close> unless a
   5.866 +  theorem name is given in the declaration. Overloaded constants should be
   5.867 +  declared as such.
   5.868  \<close>
   5.869  
   5.870  
   5.871 @@ -755,22 +734,24 @@
   5.872    old-style datatypes.
   5.873  
   5.874  
   5.875 -  These commands are mostly obsolete; @{command (HOL) "datatype"}
   5.876 -  should be used instead.
   5.877 -
   5.878 -  See @{cite "isabelle-datatypes"} for more details on datatypes.  Apart from proper
   5.879 -  proof methods for case analysis and induction, there are also
   5.880 +  These commands are mostly obsolete; @{command (HOL) "datatype"} should be
   5.881 +  used instead.
   5.882 +
   5.883 +  See @{cite "isabelle-datatypes"} for more details on datatypes. Apart from
   5.884 +  proper proof methods for case analysis and induction, there are also
   5.885    emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
   5.886 -  induct_tac} available, see \secref{sec:hol-induct-tac}; these admit
   5.887 -  to refer directly to the internal structure of subgoals (including
   5.888 -  internally bound parameters).
   5.889 +  induct_tac} available, see \secref{sec:hol-induct-tac}; these admit to refer
   5.890 +  directly to the internal structure of subgoals (including internally bound
   5.891 +  parameters).
   5.892  \<close>
   5.893  
   5.894  
   5.895  subsubsection \<open>Examples\<close>
   5.896  
   5.897 -text \<open>We define a type of finite sequences, with slightly different names
   5.898 -  than the existing @{typ "'a list"} that is already in @{theory Main}:\<close>
   5.899 +text \<open>
   5.900 +  We define a type of finite sequences, with slightly different names than the
   5.901 +  existing @{typ "'a list"} that is already in @{theory Main}:
   5.902 +\<close>
   5.903  
   5.904  (*<*)experiment begin(*>*)
   5.905  datatype 'a seq = Empty | Seq 'a "'a seq"
   5.906 @@ -803,21 +784,21 @@
   5.907  
   5.908  text \<open>
   5.909    In principle, records merely generalize the concept of tuples, where
   5.910 -  components may be addressed by labels instead of just position.  The
   5.911 -  logical infrastructure of records in Isabelle/HOL is slightly more
   5.912 -  advanced, though, supporting truly extensible record schemes.  This
   5.913 -  admits operations that are polymorphic with respect to record
   5.914 -  extension, yielding ``object-oriented'' effects like (single)
   5.915 -  inheritance.  See also @{cite "NaraschewskiW-TPHOLs98"} for more
   5.916 -  details on object-oriented verification and record subtyping in HOL.
   5.917 +  components may be addressed by labels instead of just position. The logical
   5.918 +  infrastructure of records in Isabelle/HOL is slightly more advanced, though,
   5.919 +  supporting truly extensible record schemes. This admits operations that are
   5.920 +  polymorphic with respect to record extension, yielding ``object-oriented''
   5.921 +  effects like (single) inheritance. See also @{cite "NaraschewskiW-TPHOLs98"}
   5.922 +  for more details on object-oriented verification and record subtyping in
   5.923 +  HOL.
   5.924  \<close>
   5.925  
   5.926  
   5.927  subsection \<open>Basic concepts\<close>
   5.928  
   5.929  text \<open>
   5.930 -  Isabelle/HOL supports both \<^emph>\<open>fixed\<close> and \<^emph>\<open>schematic\<close> records
   5.931 -  at the level of terms and types.  The notation is as follows:
   5.932 +  Isabelle/HOL supports both \<^emph>\<open>fixed\<close> and \<^emph>\<open>schematic\<close> records at the level of
   5.933 +  terms and types. The notation is as follows:
   5.934  
   5.935    \begin{center}
   5.936    \begin{tabular}{l|l|l}
   5.937 @@ -830,47 +811,41 @@
   5.938  
   5.939    The ASCII representation of \<open>\<lparr>x = a\<rparr>\<close> is \<open>(| x = a |)\<close>.
   5.940  
   5.941 -  A fixed record \<open>\<lparr>x = a, y = b\<rparr>\<close> has field \<open>x\<close> of value
   5.942 -  \<open>a\<close> and field \<open>y\<close> of value \<open>b\<close>.  The corresponding
   5.943 -  type is \<open>\<lparr>x :: A, y :: B\<rparr>\<close>, assuming that \<open>a :: A\<close>
   5.944 -  and \<open>b :: B\<close>.
   5.945 -
   5.946 -  A record scheme like \<open>\<lparr>x = a, y = b, \<dots> = m\<rparr>\<close> contains fields
   5.947 -  \<open>x\<close> and \<open>y\<close> as before, but also possibly further fields
   5.948 -  as indicated by the ``\<open>\<dots>\<close>'' notation (which is actually part
   5.949 -  of the syntax).  The improper field ``\<open>\<dots>\<close>'' of a record
   5.950 -  scheme is called the \<^emph>\<open>more part\<close>.  Logically it is just a free
   5.951 -  variable, which is occasionally referred to as ``row variable'' in
   5.952 -  the literature.  The more part of a record scheme may be
   5.953 -  instantiated by zero or more further components.  For example, the
   5.954 -  previous scheme may get instantiated to \<open>\<lparr>x = a, y = b, z =
   5.955 -  c, \<dots> = m'\<rparr>\<close>, where \<open>m'\<close> refers to a different more part.
   5.956 -  Fixed records are special instances of record schemes, where
   5.957 -  ``\<open>\<dots>\<close>'' is properly terminated by the \<open>() :: unit\<close>
   5.958 -  element.  In fact, \<open>\<lparr>x = a, y = b\<rparr>\<close> is just an abbreviation
   5.959 -  for \<open>\<lparr>x = a, y = b, \<dots> = ()\<rparr>\<close>.
   5.960 +  A fixed record \<open>\<lparr>x = a, y = b\<rparr>\<close> has field \<open>x\<close> of value \<open>a\<close> and field \<open>y\<close> of
   5.961 +  value \<open>b\<close>. The corresponding type is \<open>\<lparr>x :: A, y :: B\<rparr>\<close>, assuming that \<open>a ::
   5.962 +  A\<close> and \<open>b :: B\<close>.
   5.963 +
   5.964 +  A record scheme like \<open>\<lparr>x = a, y = b, \<dots> = m\<rparr>\<close> contains fields \<open>x\<close> and \<open>y\<close> as
   5.965 +  before, but also possibly further fields as indicated by the ``\<open>\<dots>\<close>''
   5.966 +  notation (which is actually part of the syntax). The improper field ``\<open>\<dots>\<close>''
   5.967 +  of a record scheme is called the \<^emph>\<open>more part\<close>. Logically it is just a free
   5.968 +  variable, which is occasionally referred to as ``row variable'' in the
   5.969 +  literature. The more part of a record scheme may be instantiated by zero or
   5.970 +  more further components. For example, the previous scheme may get
   5.971 +  instantiated to \<open>\<lparr>x = a, y = b, z = c, \<dots> = m'\<rparr>\<close>, where \<open>m'\<close> refers to a
   5.972 +  different more part. Fixed records are special instances of record schemes,
   5.973 +  where ``\<open>\<dots>\<close>'' is properly terminated by the \<open>() :: unit\<close> element. In fact,
   5.974 +  \<open>\<lparr>x = a, y = b\<rparr>\<close> is just an abbreviation for \<open>\<lparr>x = a, y = b, \<dots> = ()\<rparr>\<close>.
   5.975  
   5.976    \<^medskip>
   5.977 -  Two key observations make extensible records in a simply
   5.978 -  typed language like HOL work out:
   5.979 -
   5.980 -  \<^enum> the more part is internalized, as a free term or type
   5.981 -  variable,
   5.982 -
   5.983 -  \<^enum> field names are externalized, they cannot be accessed within
   5.984 -  the logic as first-class values.
   5.985 +  Two key observations make extensible records in a simply typed language like
   5.986 +  HOL work out:
   5.987 +
   5.988 +  \<^enum> the more part is internalized, as a free term or type variable,
   5.989 +
   5.990 +  \<^enum> field names are externalized, they cannot be accessed within the logic as
   5.991 +  first-class values.
   5.992  
   5.993  
   5.994    \<^medskip>
   5.995 -  In Isabelle/HOL record types have to be defined explicitly,
   5.996 -  fixing their field names and types, and their (optional) parent
   5.997 -  record.  Afterwards, records may be formed using above syntax, while
   5.998 -  obeying the canonical order of fields as given by their declaration.
   5.999 -  The record package provides several standard operations like
  5.1000 -  selectors and updates.  The common setup for various generic proof
  5.1001 -  tools enable succinct reasoning patterns.  See also the Isabelle/HOL
  5.1002 -  tutorial @{cite "isabelle-hol-book"} for further instructions on using
  5.1003 -  records in practice.
  5.1004 +  In Isabelle/HOL record types have to be defined explicitly, fixing their
  5.1005 +  field names and types, and their (optional) parent record. Afterwards,
  5.1006 +  records may be formed using above syntax, while obeying the canonical order
  5.1007 +  of fields as given by their declaration. The record package provides several
  5.1008 +  standard operations like selectors and updates. The common setup for various
  5.1009 +  generic proof tools enable succinct reasoning patterns. See also the
  5.1010 +  Isabelle/HOL tutorial @{cite "isabelle-hol-book"} for further instructions
  5.1011 +  on using records in practice.
  5.1012  \<close>
  5.1013  
  5.1014  
  5.1015 @@ -893,45 +868,40 @@
  5.1016      modes: '(' (@{syntax name} +) ')'
  5.1017    \<close>}
  5.1018  
  5.1019 -  \<^descr> @{command (HOL) "record"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1
  5.1020 -  \<dots> c\<^sub>n :: \<sigma>\<^sub>n\<close> defines extensible record type \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close>,
  5.1021 -  derived from the optional parent record \<open>\<tau>\<close> by adding new
  5.1022 -  field components \<open>c\<^sub>i :: \<sigma>\<^sub>i\<close> etc.
  5.1023 -
  5.1024 -  The type variables of \<open>\<tau>\<close> and \<open>\<sigma>\<^sub>i\<close> need to be
  5.1025 -  covered by the (distinct) parameters \<open>\<alpha>\<^sub>1, \<dots>,
  5.1026 -  \<alpha>\<^sub>m\<close>.  Type constructor \<open>t\<close> has to be new, while \<open>\<tau>\<close> needs to specify an instance of an existing record type.  At
  5.1027 -  least one new field \<open>c\<^sub>i\<close> has to be specified.
  5.1028 -  Basically, field names need to belong to a unique record.  This is
  5.1029 -  not a real restriction in practice, since fields are qualified by
  5.1030 -  the record name internally.
  5.1031 -
  5.1032 -  The parent record specification \<open>\<tau>\<close> is optional; if omitted
  5.1033 -  \<open>t\<close> becomes a root record.  The hierarchy of all records
  5.1034 -  declared within a theory context forms a forest structure, i.e.\ a
  5.1035 -  set of trees starting with a root record each.  There is no way to
  5.1036 -  merge multiple parent records!
  5.1037 -
  5.1038 -  For convenience, \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> is made a
  5.1039 -  type abbreviation for the fixed record type \<open>\<lparr>c\<^sub>1 ::
  5.1040 -  \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>\<close>, likewise is \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme\<close> made an abbreviation for
  5.1041 -  \<open>\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::
  5.1042 -  \<zeta>\<rparr>\<close>.
  5.1043 -
  5.1044 - \<^descr> @{command (HOL) "print_record"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> prints the definition
  5.1045 - of record \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close>. Optionally \<open>modes\<close> can be specified, which are
  5.1046 - appended to the current print mode; see \secref{sec:print-modes}.
  5.1047 +  \<^descr> @{command (HOL) "record"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1 \<dots> c\<^sub>n :: \<sigma>\<^sub>n\<close>
  5.1048 +  defines extensible record type \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close>, derived from the optional
  5.1049 +  parent record \<open>\<tau>\<close> by adding new field components \<open>c\<^sub>i :: \<sigma>\<^sub>i\<close> etc.
  5.1050 +
  5.1051 +  The type variables of \<open>\<tau>\<close> and \<open>\<sigma>\<^sub>i\<close> need to be covered by the (distinct)
  5.1052 +  parameters \<open>\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m\<close>. Type constructor \<open>t\<close> has to be new, while \<open>\<tau>\<close>
  5.1053 +  needs to specify an instance of an existing record type. At least one new
  5.1054 +  field \<open>c\<^sub>i\<close> has to be specified. Basically, field names need to belong to a
  5.1055 +  unique record. This is not a real restriction in practice, since fields are
  5.1056 +  qualified by the record name internally.
  5.1057 +
  5.1058 +  The parent record specification \<open>\<tau>\<close> is optional; if omitted \<open>t\<close> becomes a
  5.1059 +  root record. The hierarchy of all records declared within a theory context
  5.1060 +  forms a forest structure, i.e.\ a set of trees starting with a root record
  5.1061 +  each. There is no way to merge multiple parent records!
  5.1062 +
  5.1063 +  For convenience, \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> is made a type abbreviation for the fixed
  5.1064 +  record type \<open>\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>\<close>, likewise is \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>)
  5.1065 +  t_scheme\<close> made an abbreviation for \<open>\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>\<close>.
  5.1066 +
  5.1067 +  \<^descr> @{command (HOL) "print_record"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> prints the definition of
  5.1068 +  record \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close>. Optionally \<open>modes\<close> can be specified, which are
  5.1069 +  appended to the current print mode; see \secref{sec:print-modes}.
  5.1070  \<close>
  5.1071  
  5.1072  
  5.1073  subsection \<open>Record operations\<close>
  5.1074  
  5.1075 -text \<open>Any record definition of the form presented above produces certain
  5.1076 -  standard operations. Selectors and updates are provided for any field,
  5.1077 -  including the improper one ``\<open>more\<close>''. There are also cumulative
  5.1078 -  record constructor functions. To simplify the presentation below, we
  5.1079 -  assume for now that \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> is a root record with fields
  5.1080 -  \<open>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<close>.
  5.1081 +text \<open>
  5.1082 +  Any record definition of the form presented above produces certain standard
  5.1083 +  operations. Selectors and updates are provided for any field, including the
  5.1084 +  improper one ``\<open>more\<close>''. There are also cumulative record constructor
  5.1085 +  functions. To simplify the presentation below, we assume for now that \<open>(\<alpha>\<^sub>1,
  5.1086 +  \<dots>, \<alpha>\<^sub>m) t\<close> is a root record with fields \<open>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<close>.
  5.1087  
  5.1088    \<^medskip>
  5.1089    \<^bold>\<open>Selectors\<close> and \<^bold>\<open>updates\<close> are available for any
  5.1090 @@ -942,33 +912,32 @@
  5.1091      \<open>c\<^sub>i_update\<close> & \<open>::\<close> & \<open>\<sigma>\<^sub>i \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>\<close> \\
  5.1092    \end{matharray}
  5.1093  
  5.1094 -  There is special syntax for application of updates: \<open>r\<lparr>x := a\<rparr>\<close>
  5.1095 -  abbreviates term \<open>x_update a r\<close>. Further notation for repeated
  5.1096 -  updates is also available: \<open>r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z := c\<rparr>\<close> may be
  5.1097 -  written \<open>r\<lparr>x := a, y := b, z := c\<rparr>\<close>. Note that because of postfix
  5.1098 -  notation the order of fields shown here is reverse than in the actual
  5.1099 -  term. Since repeated updates are just function applications, fields may be
  5.1100 -  freely permuted in \<open>\<lparr>x := a, y := b, z := c\<rparr>\<close>, as far as logical
  5.1101 -  equality is concerned. Thus commutativity of independent updates can be
  5.1102 -  proven within the logic for any two fields, but not as a general theorem.
  5.1103 +  There is special syntax for application of updates: \<open>r\<lparr>x := a\<rparr>\<close> abbreviates
  5.1104 +  term \<open>x_update a r\<close>. Further notation for repeated updates is also
  5.1105 +  available: \<open>r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z := c\<rparr>\<close> may be written \<open>r\<lparr>x := a, y := b, z
  5.1106 +  := c\<rparr>\<close>. Note that because of postfix notation the order of fields shown here
  5.1107 +  is reverse than in the actual term. Since repeated updates are just function
  5.1108 +  applications, fields may be freely permuted in \<open>\<lparr>x := a, y := b, z := c\<rparr>\<close>,
  5.1109 +  as far as logical equality is concerned. Thus commutativity of independent
  5.1110 +  updates can be proven within the logic for any two fields, but not as a
  5.1111 +  general theorem.
  5.1112  
  5.1113    \<^medskip>
  5.1114 -  The \<^bold>\<open>make\<close> operation provides a cumulative record
  5.1115 -  constructor function:
  5.1116 +  The \<^bold>\<open>make\<close> operation provides a cumulative record constructor function:
  5.1117  
  5.1118    \begin{matharray}{lll}
  5.1119      \<open>t.make\<close> & \<open>::\<close> & \<open>\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>\<close> \\
  5.1120    \end{matharray}
  5.1121  
  5.1122    \<^medskip>
  5.1123 -  We now reconsider the case of non-root records, which are derived
  5.1124 -  of some parent. In general, the latter may depend on another parent as
  5.1125 -  well, resulting in a list of \<^emph>\<open>ancestor records\<close>. Appending the lists
  5.1126 -  of fields of all ancestors results in a certain field prefix. The record
  5.1127 -  package automatically takes care of this by lifting operations over this
  5.1128 -  context of ancestor fields. Assuming that \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> has
  5.1129 -  ancestor fields \<open>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k\<close>, the above record
  5.1130 -  operations will get the following types:
  5.1131 +  We now reconsider the case of non-root records, which are derived of some
  5.1132 +  parent. In general, the latter may depend on another parent as well,
  5.1133 +  resulting in a list of \<^emph>\<open>ancestor records\<close>. Appending the lists of fields of
  5.1134 +  all ancestors results in a certain field prefix. The record package
  5.1135 +  automatically takes care of this by lifting operations over this context of
  5.1136 +  ancestor fields. Assuming that \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> has ancestor fields \<open>b\<^sub>1 ::
  5.1137 +  \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k\<close>, the above record operations will get the following
  5.1138 +  types:
  5.1139  
  5.1140    \<^medskip>
  5.1141    \begin{tabular}{lll}
  5.1142 @@ -981,12 +950,11 @@
  5.1143    \end{tabular}
  5.1144    \<^medskip>
  5.1145  
  5.1146 -  Some further operations address the extension aspect of a
  5.1147 -  derived record scheme specifically: \<open>t.fields\<close> produces a record
  5.1148 -  fragment consisting of exactly the new fields introduced here (the result
  5.1149 -  may serve as a more part elsewhere); \<open>t.extend\<close> takes a fixed
  5.1150 -  record and adds a given more part; \<open>t.truncate\<close> restricts a record
  5.1151 -  scheme to a fixed record.
  5.1152 +  Some further operations address the extension aspect of a derived record
  5.1153 +  scheme specifically: \<open>t.fields\<close> produces a record fragment consisting of
  5.1154 +  exactly the new fields introduced here (the result may serve as a more part
  5.1155 +  elsewhere); \<open>t.extend\<close> takes a fixed record and adds a given more part;
  5.1156 +  \<open>t.truncate\<close> restricts a record scheme to a fixed record.
  5.1157  
  5.1158    \<^medskip>
  5.1159    \begin{tabular}{lll}
  5.1160 @@ -997,52 +965,49 @@
  5.1161    \end{tabular}
  5.1162    \<^medskip>
  5.1163  
  5.1164 -  Note that \<open>t.make\<close> and \<open>t.fields\<close> coincide for
  5.1165 -  root records.
  5.1166 +  Note that \<open>t.make\<close> and \<open>t.fields\<close> coincide for root records.
  5.1167  \<close>
  5.1168  
  5.1169  
  5.1170  subsection \<open>Derived rules and proof tools\<close>
  5.1171  
  5.1172  text \<open>
  5.1173 -  The record package proves several results internally, declaring
  5.1174 -  these facts to appropriate proof tools.  This enables users to
  5.1175 -  reason about record structures quite conveniently.  Assume that
  5.1176 -  \<open>t\<close> is a record type as specified above.
  5.1177 +  The record package proves several results internally, declaring these facts
  5.1178 +  to appropriate proof tools. This enables users to reason about record
  5.1179 +  structures quite conveniently. Assume that \<open>t\<close> is a record type as specified
  5.1180 +  above.
  5.1181  
  5.1182    \<^enum> Standard conversions for selectors or updates applied to record
  5.1183    constructor terms are made part of the default Simplifier context; thus
  5.1184    proofs by reduction of basic operations merely require the @{method simp}
  5.1185 -  method without further arguments. These rules are available as \<open>t.simps\<close>, too.
  5.1186 +  method without further arguments. These rules are available as \<open>t.simps\<close>,
  5.1187 +  too.
  5.1188  
  5.1189    \<^enum> Selectors applied to updated records are automatically reduced by an
  5.1190    internal simplification procedure, which is also part of the standard
  5.1191    Simplifier setup.
  5.1192  
  5.1193 -  \<^enum> Inject equations of a form analogous to @{prop "(x, y) = (x', y') \<equiv>
  5.1194 -  x = x' \<and> y = y'"} are declared to the Simplifier and Classical Reasoner as
  5.1195 +  \<^enum> Inject equations of a form analogous to @{prop "(x, y) = (x', y') \<equiv> x = x'
  5.1196 +  \<and> y = y'"} are declared to the Simplifier and Classical Reasoner as
  5.1197    @{attribute iff} rules. These rules are available as \<open>t.iffs\<close>.
  5.1198  
  5.1199 -  \<^enum> The introduction rule for record equality analogous to \<open>x r =
  5.1200 -  x r' \<Longrightarrow> y r = y r' \<dots> \<Longrightarrow> r = r'\<close> is declared to the Simplifier, and as the
  5.1201 -  basic rule context as ``@{attribute intro}\<open>?\<close>''. The rule is
  5.1202 -  called \<open>t.equality\<close>.
  5.1203 -
  5.1204 -  \<^enum> Representations of arbitrary record expressions as canonical
  5.1205 -  constructor terms are provided both in @{method cases} and @{method
  5.1206 -  induct} format (cf.\ the generic proof methods of the same name,
  5.1207 -  \secref{sec:cases-induct}). Several variations are available, for fixed
  5.1208 -  records, record schemes, more parts etc.
  5.1209 +  \<^enum> The introduction rule for record equality analogous to \<open>x r = x r' \<Longrightarrow> y r =
  5.1210 +  y r' \<dots> \<Longrightarrow> r = r'\<close> is declared to the Simplifier, and as the basic rule
  5.1211 +  context as ``@{attribute intro}\<open>?\<close>''. The rule is called \<open>t.equality\<close>.
  5.1212 +
  5.1213 +  \<^enum> Representations of arbitrary record expressions as canonical constructor
  5.1214 +  terms are provided both in @{method cases} and @{method induct} format (cf.\
  5.1215 +  the generic proof methods of the same name, \secref{sec:cases-induct}).
  5.1216 +  Several variations are available, for fixed records, record schemes, more
  5.1217 +  parts etc.
  5.1218  
  5.1219    The generic proof methods are sufficiently smart to pick the most sensible
  5.1220    rule according to the type of the indicated record expression: users just
  5.1221 -  need to apply something like ``\<open>(cases r)\<close>'' to a certain proof
  5.1222 -  problem.
  5.1223 -
  5.1224 -  \<^enum> The derived record operations \<open>t.make\<close>, \<open>t.fields\<close>,
  5.1225 -  \<open>t.extend\<close>, \<open>t.truncate\<close> are \<^emph>\<open>not\<close> treated
  5.1226 -  automatically, but usually need to be expanded by hand, using the
  5.1227 -  collective fact \<open>t.defs\<close>.
  5.1228 +  need to apply something like ``\<open>(cases r)\<close>'' to a certain proof problem.
  5.1229 +
  5.1230 +  \<^enum> The derived record operations \<open>t.make\<close>, \<open>t.fields\<close>, \<open>t.extend\<close>,
  5.1231 +  \<open>t.truncate\<close> are \<^emph>\<open>not\<close> treated automatically, but usually need to be
  5.1232 +  expanded by hand, using the collective fact \<open>t.defs\<close>.
  5.1233  \<close>
  5.1234  
  5.1235  
  5.1236 @@ -1060,13 +1025,12 @@
  5.1237  
  5.1238    A type definition identifies a new type with a non-empty subset of an
  5.1239    existing type. More precisely, the new type is defined by exhibiting an
  5.1240 -  existing type \<open>\<tau>\<close>, a set \<open>A :: \<tau> set\<close>, and proving @{prop
  5.1241 -  "\<exists>x. x \<in> A"}. Thus \<open>A\<close> is a non-empty subset of \<open>\<tau>\<close>, and the
  5.1242 -  new type denotes this subset. New functions are postulated that establish
  5.1243 -  an isomorphism between the new type and the subset. In general, the type
  5.1244 -  \<open>\<tau>\<close> may involve type variables \<open>\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n\<close> which means
  5.1245 -  that the type definition produces a type constructor \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n)
  5.1246 -  t\<close> depending on those type arguments.
  5.1247 +  existing type \<open>\<tau>\<close>, a set \<open>A :: \<tau> set\<close>, and proving @{prop "\<exists>x. x \<in> A"}. Thus
  5.1248 +  \<open>A\<close> is a non-empty subset of \<open>\<tau>\<close>, and the new type denotes this subset. New
  5.1249 +  functions are postulated that establish an isomorphism between the new type
  5.1250 +  and the subset. In general, the type \<open>\<tau>\<close> may involve type variables \<open>\<alpha>\<^sub>1, \<dots>,
  5.1251 +  \<alpha>\<^sub>n\<close> which means that the type definition produces a type constructor \<open>(\<alpha>\<^sub>1,
  5.1252 +  \<dots>, \<alpha>\<^sub>n) t\<close> depending on those type arguments.
  5.1253  
  5.1254    @{rail \<open>
  5.1255      @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set
  5.1256 @@ -1078,98 +1042,94 @@
  5.1257      rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
  5.1258    \<close>}
  5.1259  
  5.1260 -  To understand the concept of type definition better, we need to recount
  5.1261 -  its somewhat complex history. The HOL logic goes back to the ``Simple
  5.1262 -  Theory of Types'' (STT) of A. Church @{cite "church40"}, which is further
  5.1263 -  explained in the book by P. Andrews @{cite "andrews86"}. The overview
  5.1264 -  article by W. Farmer @{cite "Farmer:2008"} points out the ``seven
  5.1265 -  virtues'' of this relatively simple family of logics. STT has only ground
  5.1266 -  types, without polymorphism and without type definitions.
  5.1267 +  To understand the concept of type definition better, we need to recount its
  5.1268 +  somewhat complex history. The HOL logic goes back to the ``Simple Theory of
  5.1269 +  Types'' (STT) of A. Church @{cite "church40"}, which is further explained in
  5.1270 +  the book by P. Andrews @{cite "andrews86"}. The overview article by W.
  5.1271 +  Farmer @{cite "Farmer:2008"} points out the ``seven virtues'' of this
  5.1272 +  relatively simple family of logics. STT has only ground types, without
  5.1273 +  polymorphism and without type definitions.
  5.1274  
  5.1275    \<^medskip>
  5.1276 -  M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by
  5.1277 -  adding schematic polymorphism (type variables and type constructors) and a
  5.1278 -  facility to introduce new types as semantic subtypes from existing types.
  5.1279 -  This genuine extension of the logic was explained semantically by A. Pitts
  5.1280 -  in the book of the original Cambridge HOL88 system @{cite "pitts93"}. Type
  5.1281 -  definitions work in this setting, because the general model-theory of STT
  5.1282 -  is restricted to models that ensure that the universe of type
  5.1283 -  interpretations is closed by forming subsets (via predicates taken from
  5.1284 -  the logic).
  5.1285 +  M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by adding
  5.1286 +  schematic polymorphism (type variables and type constructors) and a facility
  5.1287 +  to introduce new types as semantic subtypes from existing types. This
  5.1288 +  genuine extension of the logic was explained semantically by A. Pitts in the
  5.1289 +  book of the original Cambridge HOL88 system @{cite "pitts93"}. Type
  5.1290 +  definitions work in this setting, because the general model-theory of STT is
  5.1291 +  restricted to models that ensure that the universe of type interpretations
  5.1292 +  is closed by forming subsets (via predicates taken from the logic).
  5.1293  
  5.1294    \<^medskip>
  5.1295 -  Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded
  5.1296 -  constant definitions @{cite "Wenzel:1997:TPHOL" and
  5.1297 -  "Haftmann-Wenzel:2006:classes"}, which are actually a concept of
  5.1298 -  Isabelle/Pure and do not depend on particular set-theoretic semantics of
  5.1299 -  HOL. Over many years, there was no formal checking of semantic type
  5.1300 -  definitions in Isabelle/HOL versus syntactic constant definitions in
  5.1301 -  Isabelle/Pure. So the @{command typedef} command was described as
  5.1302 -  ``axiomatic'' in the sense of \secref{sec:axiomatizations}, only with some
  5.1303 -  local checks of the given type and its representing set.
  5.1304 +  Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded constant
  5.1305 +  definitions @{cite "Wenzel:1997:TPHOL" and "Haftmann-Wenzel:2006:classes"},
  5.1306 +  which are actually a concept of Isabelle/Pure and do not depend on
  5.1307 +  particular set-theoretic semantics of HOL. Over many years, there was no
  5.1308 +  formal checking of semantic type definitions in Isabelle/HOL versus
  5.1309 +  syntactic constant definitions in Isabelle/Pure. So the @{command typedef}
  5.1310 +  command was described as ``axiomatic'' in the sense of
  5.1311 +  \secref{sec:axiomatizations}, only with some local checks of the given type
  5.1312 +  and its representing set.
  5.1313  
  5.1314    Recent clarification of overloading in the HOL logic proper @{cite
  5.1315    "Kuncar-Popescu:2015"} demonstrates how the dissimilar concepts of constant
  5.1316    definitions versus type definitions may be understood uniformly. This
  5.1317    requires an interpretation of Isabelle/HOL that substantially reforms the
  5.1318    set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic
  5.1319 -  view on polymorphism and interpreting only ground types in the
  5.1320 -  set-theoretic sense of HOL88. Moreover, type-constructors may be
  5.1321 -  explicitly overloaded, e.g.\ by making the subset depend on type-class
  5.1322 -  parameters (cf.\ \secref{sec:class}). This is semantically like a
  5.1323 -  dependent type: the meaning relies on the operations provided by different
  5.1324 -  type-class instances.
  5.1325 -
  5.1326 -  \<^descr> @{command (HOL) "typedef"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A\<close> defines a
  5.1327 -  new type \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> from the set \<open>A\<close> over an existing
  5.1328 -  type. The set \<open>A\<close> may contain type variables \<open>\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n\<close>
  5.1329 -  as specified on the LHS, but no term variables. Non-emptiness of \<open>A\<close>
  5.1330 -  needs to be proven on the spot, in order to turn the internal conditional
  5.1331 -  characterization into usable theorems.
  5.1332 -
  5.1333 -  The ``\<open>(overloaded)\<close>'' option allows the @{command
  5.1334 -  "typedef"} specification to depend on constants that are not (yet)
  5.1335 -  specified and thus left open as parameters, e.g.\ type-class parameters.
  5.1336 +  view on polymorphism and interpreting only ground types in the set-theoretic
  5.1337 +  sense of HOL88. Moreover, type-constructors may be explicitly overloaded,
  5.1338 +  e.g.\ by making the subset depend on type-class parameters (cf.\
  5.1339 +  \secref{sec:class}). This is semantically like a dependent type: the meaning
  5.1340 +  relies on the operations provided by different type-class instances.
  5.1341 +
  5.1342 +  \<^descr> @{command (HOL) "typedef"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A\<close> defines a new type \<open>(\<alpha>\<^sub>1,
  5.1343 +  \<dots>, \<alpha>\<^sub>n) t\<close> from the set \<open>A\<close> over an existing type. The set \<open>A\<close> may contain
  5.1344 +  type variables \<open>\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n\<close> as specified on the LHS, but no term variables.
  5.1345 +  Non-emptiness of \<open>A\<close> needs to be proven on the spot, in order to turn the
  5.1346 +  internal conditional characterization into usable theorems.
  5.1347 +
  5.1348 +  The ``\<open>(overloaded)\<close>'' option allows the @{command "typedef"} specification
  5.1349 +  to depend on constants that are not (yet) specified and thus left open as
  5.1350 +  parameters, e.g.\ type-class parameters.
  5.1351  
  5.1352    Within a local theory specification, the newly introduced type constructor
  5.1353    cannot depend on parameters or assumptions of the context: this is
  5.1354 -  syntactically impossible in HOL. The non-emptiness proof may formally
  5.1355 -  depend on local assumptions, but this has little practical relevance.
  5.1356 -
  5.1357 -  For @{command (HOL) "typedef"}~\<open>t = A\<close> the newly introduced
  5.1358 -  type \<open>t\<close> is accompanied by a pair of morphisms to relate it to
  5.1359 -  the representing set over the old type.  By default, the injection
  5.1360 -  from type to set is called \<open>Rep_t\<close> and its inverse \<open>Abs_t\<close>: An explicit @{keyword (HOL) "morphisms"} specification
  5.1361 -  allows to provide alternative names.
  5.1362 +  syntactically impossible in HOL. The non-emptiness proof may formally depend
  5.1363 +  on local assumptions, but this has little practical relevance.
  5.1364 +
  5.1365 +  For @{command (HOL) "typedef"}~\<open>t = A\<close> the newly introduced type \<open>t\<close> is
  5.1366 +  accompanied by a pair of morphisms to relate it to the representing set over
  5.1367 +  the old type. By default, the injection from type to set is called \<open>Rep_t\<close>
  5.1368 +  and its inverse \<open>Abs_t\<close>: An explicit @{keyword (HOL) "morphisms"}
  5.1369 +  specification allows to provide alternative names.
  5.1370  
  5.1371    The logical characterization of @{command typedef} uses the predicate of
  5.1372    locale @{const type_definition} that is defined in Isabelle/HOL. Various
  5.1373 -  basic consequences of that are instantiated accordingly, re-using the
  5.1374 -  locale facts with names derived from the new type constructor. Thus the
  5.1375 -  generic theorem @{thm type_definition.Rep} is turned into the specific
  5.1376 -  \<open>Rep_t\<close>, for example.
  5.1377 -
  5.1378 -  Theorems @{thm type_definition.Rep}, @{thm
  5.1379 -  type_definition.Rep_inverse}, and @{thm type_definition.Abs_inverse}
  5.1380 -  provide the most basic characterization as a corresponding
  5.1381 -  injection/surjection pair (in both directions).  The derived rules
  5.1382 -  @{thm type_definition.Rep_inject} and @{thm
  5.1383 +  basic consequences of that are instantiated accordingly, re-using the locale
  5.1384 +  facts with names derived from the new type constructor. Thus the generic
  5.1385 +  theorem @{thm type_definition.Rep} is turned into the specific \<open>Rep_t\<close>, for
  5.1386 +  example.
  5.1387 +
  5.1388 +  Theorems @{thm type_definition.Rep}, @{thm type_definition.Rep_inverse}, and
  5.1389 +  @{thm type_definition.Abs_inverse} provide the most basic characterization
  5.1390 +  as a corresponding injection/surjection pair (in both directions). The
  5.1391 +  derived rules @{thm type_definition.Rep_inject} and @{thm
  5.1392    type_definition.Abs_inject} provide a more convenient version of
  5.1393 -  injectivity, suitable for automated proof tools (e.g.\ in
  5.1394 -  declarations involving @{attribute simp} or @{attribute iff}).
  5.1395 -  Furthermore, the rules @{thm type_definition.Rep_cases}~/ @{thm
  5.1396 -  type_definition.Rep_induct}, and @{thm type_definition.Abs_cases}~/
  5.1397 -  @{thm type_definition.Abs_induct} provide alternative views on
  5.1398 -  surjectivity.  These rules are already declared as set or type rules
  5.1399 -  for the generic @{method cases} and @{method induct} methods,
  5.1400 +  injectivity, suitable for automated proof tools (e.g.\ in declarations
  5.1401 +  involving @{attribute simp} or @{attribute iff}). Furthermore, the rules
  5.1402 +  @{thm type_definition.Rep_cases}~/ @{thm type_definition.Rep_induct}, and
  5.1403 +  @{thm type_definition.Abs_cases}~/ @{thm type_definition.Abs_induct} provide
  5.1404 +  alternative views on surjectivity. These rules are already declared as set
  5.1405 +  or type rules for the generic @{method cases} and @{method induct} methods,
  5.1406    respectively.
  5.1407  \<close>
  5.1408  
  5.1409  
  5.1410  subsubsection \<open>Examples\<close>
  5.1411  
  5.1412 -text \<open>The following trivial example pulls a three-element type into
  5.1413 -existence within the formal logical environment of Isabelle/HOL.\<close>
  5.1414 +text \<open>
  5.1415 +  The following trivial example pulls a three-element type into existence
  5.1416 +  within the formal logical environment of Isabelle/HOL.\<close>
  5.1417  
  5.1418  (*<*)experiment begin(*>*)
  5.1419  typedef three = "{(True, True), (True, False), (False, True)}"
  5.1420 @@ -1210,37 +1170,38 @@
  5.1421      @@{command (HOL) functor} (@{syntax name} ':')? @{syntax term}
  5.1422    \<close>}
  5.1423  
  5.1424 -  \<^descr> @{command (HOL) "functor"}~\<open>prefix: m\<close> allows to prove and
  5.1425 -  register properties about the functorial structure of type constructors.
  5.1426 -  These properties then can be used by other packages to deal with those
  5.1427 -  type constructors in certain type constructions. Characteristic theorems
  5.1428 -  are noted in the current local theory. By default, they are prefixed with
  5.1429 -  the base name of the type constructor, an explicit prefix can be given
  5.1430 +  \<^descr> @{command (HOL) "functor"}~\<open>prefix: m\<close> allows to prove and register
  5.1431 +  properties about the functorial structure of type constructors. These
  5.1432 +  properties then can be used by other packages to deal with those type
  5.1433 +  constructors in certain type constructions. Characteristic theorems are
  5.1434 +  noted in the current local theory. By default, they are prefixed with the
  5.1435 +  base name of the type constructor, an explicit prefix can be given
  5.1436    alternatively.
  5.1437  
  5.1438 -  The given term \<open>m\<close> is considered as \<^emph>\<open>mapper\<close> for the
  5.1439 -  corresponding type constructor and must conform to the following type
  5.1440 -  pattern:
  5.1441 +  The given term \<open>m\<close> is considered as \<^emph>\<open>mapper\<close> for the corresponding type
  5.1442 +  constructor and must conform to the following type pattern:
  5.1443  
  5.1444    \begin{matharray}{lll}
  5.1445      \<open>m\<close> & \<open>::\<close> &
  5.1446        \<open>\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>k \<Rightarrow> (\<^vec>\<alpha>\<^sub>n) t \<Rightarrow> (\<^vec>\<beta>\<^sub>n) t\<close> \\
  5.1447    \end{matharray}
  5.1448  
  5.1449 -  where \<open>t\<close> is the type constructor, \<open>\<^vec>\<alpha>\<^sub>n\<close>
  5.1450 -  and \<open>\<^vec>\<beta>\<^sub>n\<close> are distinct type variables free in the local
  5.1451 -  theory and \<open>\<sigma>\<^sub>1\<close>, \ldots, \<open>\<sigma>\<^sub>k\<close> is a subsequence of \<open>\<alpha>\<^sub>1 \<Rightarrow> \<beta>\<^sub>1\<close>, \<open>\<beta>\<^sub>1 \<Rightarrow> \<alpha>\<^sub>1\<close>, \ldots, \<open>\<alpha>\<^sub>n \<Rightarrow> \<beta>\<^sub>n\<close>, \<open>\<beta>\<^sub>n \<Rightarrow> \<alpha>\<^sub>n\<close>.
  5.1452 +  where \<open>t\<close> is the type constructor, \<open>\<^vec>\<alpha>\<^sub>n\<close> and \<open>\<^vec>\<beta>\<^sub>n\<close> are
  5.1453 +  distinct type variables free in the local theory and \<open>\<sigma>\<^sub>1\<close>, \ldots, \<open>\<sigma>\<^sub>k\<close> is
  5.1454 +  a subsequence of \<open>\<alpha>\<^sub>1 \<Rightarrow> \<beta>\<^sub>1\<close>, \<open>\<beta>\<^sub>1 \<Rightarrow> \<alpha>\<^sub>1\<close>, \ldots, \<open>\<alpha>\<^sub>n \<Rightarrow> \<beta>\<^sub>n\<close>, \<open>\<beta>\<^sub>n \<Rightarrow> \<alpha>\<^sub>n\<close>.
  5.1455  \<close>
  5.1456  
  5.1457  
  5.1458  section \<open>Quotient types with lifting and transfer\<close>
  5.1459  
  5.1460 -text \<open>The quotient package defines a new quotient type given a raw type and
  5.1461 -  a partial equivalence relation (\secref{sec:quotient-type}). The package
  5.1462 -  also historically includes automation for transporting definitions and
  5.1463 -  theorems (\secref{sec:old-quotient}), but most of this automation was
  5.1464 -  superseded by the Lifting (\secref{sec:lifting}) and Transfer
  5.1465 -  (\secref{sec:transfer}) packages.\<close>
  5.1466 +text \<open>
  5.1467 +  The quotient package defines a new quotient type given a raw type and a
  5.1468 +  partial equivalence relation (\secref{sec:quotient-type}). The package also
  5.1469 +  historically includes automation for transporting definitions and theorems
  5.1470 +  (\secref{sec:old-quotient}), but most of this automation was superseded by
  5.1471 +  the Lifting (\secref{sec:lifting}) and Transfer (\secref{sec:transfer})
  5.1472 +  packages.
  5.1473 +\<close>
  5.1474  
  5.1475  
  5.1476  subsection \<open>Quotient type definition \label{sec:quotient-type}\<close>
  5.1477 @@ -1262,21 +1223,23 @@
  5.1478      quot_parametric: @'parametric' @{syntax thm}
  5.1479    \<close>}
  5.1480  
  5.1481 -  \<^descr> @{command (HOL) "quotient_type"} defines a new quotient type \<open>\<tau>\<close>. The injection from a quotient type to a raw type is called \<open>rep_\<tau>\<close>, its inverse \<open>abs_\<tau>\<close> unless explicit @{keyword (HOL)
  5.1482 -  "morphisms"} specification provides alternative names. @{command (HOL)
  5.1483 -  "quotient_type"} requires the user to prove that the relation is an
  5.1484 -  equivalence relation (predicate \<open>equivp\<close>), unless the user specifies
  5.1485 -  explicitly \<open>partial\<close> in which case the obligation is \<open>part_equivp\<close>. A quotient defined with \<open>partial\<close> is weaker in the
  5.1486 -  sense that less things can be proved automatically.
  5.1487 +  \<^descr> @{command (HOL) "quotient_type"} defines a new quotient type \<open>\<tau>\<close>. The
  5.1488 +  injection from a quotient type to a raw type is called \<open>rep_\<tau>\<close>, its inverse
  5.1489 +  \<open>abs_\<tau>\<close> unless explicit @{keyword (HOL) "morphisms"} specification provides
  5.1490 +  alternative names. @{command (HOL) "quotient_type"} requires the user to
  5.1491 +  prove that the relation is an equivalence relation (predicate \<open>equivp\<close>),
  5.1492 +  unless the user specifies explicitly \<open>partial\<close> in which case the obligation
  5.1493 +  is \<open>part_equivp\<close>. A quotient defined with \<open>partial\<close> is weaker in the sense
  5.1494 +  that less things can be proved automatically.
  5.1495  
  5.1496    The command internally proves a Quotient theorem and sets up the Lifting
  5.1497 -  package by the command @{command (HOL) setup_lifting}. Thus the Lifting
  5.1498 -  and Transfer packages can be used also with quotient types defined by
  5.1499 -  @{command (HOL) "quotient_type"} without any extra set-up. The
  5.1500 -  parametricity theorem for the equivalence relation R can be provided as an
  5.1501 -  extra argument of the command and is passed to the corresponding internal
  5.1502 -  call of @{command (HOL) setup_lifting}. This theorem allows the Lifting
  5.1503 -  package to generate a stronger transfer rule for equality.
  5.1504 +  package by the command @{command (HOL) setup_lifting}. Thus the Lifting and
  5.1505 +  Transfer packages can be used also with quotient types defined by @{command
  5.1506 +  (HOL) "quotient_type"} without any extra set-up. The parametricity theorem
  5.1507 +  for the equivalence relation R can be provided as an extra argument of the
  5.1508 +  command and is passed to the corresponding internal call of @{command (HOL)
  5.1509 +  setup_lifting}. This theorem allows the Lifting package to generate a
  5.1510 +  stronger transfer rule for equality.
  5.1511  \<close>
  5.1512  
  5.1513  
  5.1514 @@ -1286,9 +1249,9 @@
  5.1515    The Lifting package allows users to lift terms of the raw type to the
  5.1516    abstract type, which is a necessary step in building a library for an
  5.1517    abstract type. Lifting defines a new constant by combining coercion
  5.1518 -  functions (@{term Abs} and @{term Rep}) with the raw term. It also proves
  5.1519 -  an appropriate transfer rule for the Transfer (\secref{sec:transfer})
  5.1520 -  package and, if possible, an equation for the code generator.
  5.1521 +  functions (@{term Abs} and @{term Rep}) with the raw term. It also proves an
  5.1522 +  appropriate transfer rule for the Transfer (\secref{sec:transfer}) package
  5.1523 +  and, if possible, an equation for the code generator.
  5.1524  
  5.1525    The Lifting package provides two main commands: @{command (HOL)
  5.1526    "setup_lifting"} for initializing the package to work with a new type, and
  5.1527 @@ -1330,12 +1293,12 @@
  5.1528        @{syntax thm} (@{syntax thm} @{syntax thm})?
  5.1529    \<close>}
  5.1530  
  5.1531 -  \<^descr> @{command (HOL) "setup_lifting"} Sets up the Lifting package to work
  5.1532 -  with a user-defined type. The command supports two modes.
  5.1533 -
  5.1534 -    \<^enum> The first one is a low-level mode when the user must provide as a
  5.1535 -    first argument of @{command (HOL) "setup_lifting"} a quotient theorem
  5.1536 -    @{term "Quotient R Abs Rep T"}. The package configures a transfer rule for
  5.1537 +  \<^descr> @{command (HOL) "setup_lifting"} Sets up the Lifting package to work with
  5.1538 +  a user-defined type. The command supports two modes.
  5.1539 +
  5.1540 +    \<^enum> The first one is a low-level mode when the user must provide as a first
  5.1541 +    argument of @{command (HOL) "setup_lifting"} a quotient theorem @{term
  5.1542 +    "Quotient R Abs Rep T"}. The package configures a transfer rule for
  5.1543      equality, a domain transfer rules and sets up the @{command_def (HOL)
  5.1544      "lift_definition"} command to work with the abstract type. An optional
  5.1545      theorem @{term "reflp R"}, which certifies that the equivalence relation R
  5.1546 @@ -1344,8 +1307,8 @@
  5.1547      for @{term R} can be provided as a third argument. This allows the package
  5.1548      to generate a stronger transfer rule for equality.
  5.1549  
  5.1550 -    Users generally will not prove the \<open>Quotient\<close> theorem manually for
  5.1551 -    new types, as special commands exist to automate the process.
  5.1552 +    Users generally will not prove the \<open>Quotient\<close> theorem manually for new
  5.1553 +    types, as special commands exist to automate the process.
  5.1554  
  5.1555      \<^enum> When a new subtype is defined by @{command (HOL) typedef}, @{command
  5.1556      (HOL) "lift_definition"} can be used in its second mode, where only the
  5.1557 @@ -1355,166 +1318,162 @@
  5.1558      (HOL) setup_lifting} using its first mode.
  5.1559  
  5.1560    For quotients, the command @{command (HOL) quotient_type} can be used. The
  5.1561 -  command defines a new quotient type and similarly to the previous case,
  5.1562 -  the corresponding Quotient theorem is proved and registered by @{command
  5.1563 -  (HOL) setup_lifting}.
  5.1564 +  command defines a new quotient type and similarly to the previous case, the
  5.1565 +  corresponding Quotient theorem is proved and registered by @{command (HOL)
  5.1566 +  setup_lifting}.
  5.1567  
  5.1568    \<^medskip>
  5.1569 -  The command @{command (HOL) "setup_lifting"} also sets up the
  5.1570 -  code generator for the new type. Later on, when a new constant is defined
  5.1571 -  by @{command (HOL) "lift_definition"}, the Lifting package proves and
  5.1572 -  registers a code equation (if there is one) for the new constant.
  5.1573 -
  5.1574 -  \<^descr> @{command (HOL) "lift_definition"} \<open>f :: \<tau>\<close> @{keyword (HOL)
  5.1575 -  "is"} \<open>t\<close> Defines a new function \<open>f\<close> with an abstract type
  5.1576 -  \<open>\<tau>\<close> in terms of a corresponding operation \<open>t\<close> on a
  5.1577 -  representation type. More formally, if \<open>t :: \<sigma>\<close>, then the command
  5.1578 -  builds a term \<open>F\<close> as a corresponding combination of abstraction
  5.1579 -  and representation functions such that \<open>F :: \<sigma> \<Rightarrow> \<tau>\<close> and defines
  5.1580 -  \<open>f \<equiv> F t\<close>. The term \<open>t\<close> does not have to be necessarily a
  5.1581 -  constant but it can be any term.
  5.1582 -
  5.1583 -  The command opens a proof and the user must discharge a respectfulness
  5.1584 -  proof obligation. For a type copy, i.e.\ a typedef with \<open>UNIV\<close>, the
  5.1585 -  obligation is discharged automatically. The proof goal is presented in a
  5.1586 -  user-friendly, readable form. A respectfulness theorem in the standard
  5.1587 -  format \<open>f.rsp\<close> and a transfer rule \<open>f.transfer\<close> for the
  5.1588 -  Transfer package are generated by the package.
  5.1589 -
  5.1590 -  The user can specify a parametricity theorems for \<open>t\<close> after the
  5.1591 -  keyword @{keyword "parametric"}, which allows the command to generate
  5.1592 -  parametric transfer rules for \<open>f\<close>.
  5.1593 +  The command @{command (HOL) "setup_lifting"} also sets up the code generator
  5.1594 +  for the new type. Later on, when a new constant is defined by @{command
  5.1595 +  (HOL) "lift_definition"}, the Lifting package proves and registers a code
  5.1596 +  equation (if there is one) for the new constant.
  5.1597 +
  5.1598 +  \<^descr> @{command (HOL) "lift_definition"} \<open>f :: \<tau>\<close> @{keyword (HOL) "is"} \<open>t\<close>
  5.1599 +  Defines a new function \<open>f\<close> with an abstract type \<open>\<tau>\<close> in terms of a
  5.1600 +  corresponding operation \<open>t\<close> on a representation type. More formally, if \<open>t
  5.1601 +  :: \<sigma>\<close>, then the command builds a term \<open>F\<close> as a corresponding combination of
  5.1602 +  abstraction and representation functions such that \<open>F :: \<sigma> \<Rightarrow> \<tau>\<close> and defines
  5.1603 +  \<open>f \<equiv> F t\<close>. The term \<open>t\<close> does not have to be necessarily a constant but it
  5.1604 +  can be any term.
  5.1605 +
  5.1606 +  The command opens a proof and the user must discharge a respectfulness proof
  5.1607 +  obligation. For a type copy, i.e.\ a typedef with \<open>UNIV\<close>, the obligation is
  5.1608 +  discharged automatically. The proof goal is presented in a user-friendly,
  5.1609 +  readable form. A respectfulness theorem in the standard format \<open>f.rsp\<close> and a
  5.1610 +  transfer rule \<open>f.transfer\<close> for the Transfer package are generated by the
  5.1611 +  package.
  5.1612 +
  5.1613 +  The user can specify a parametricity theorems for \<open>t\<close> after the keyword
  5.1614 +  @{keyword "parametric"}, which allows the command to generate parametric
  5.1615 +  transfer rules for \<open>f\<close>.
  5.1616  
  5.1617    For each constant defined through trivial quotients (type copies or
  5.1618 -  subtypes) \<open>f.rep_eq\<close> is generated. The equation is a code
  5.1619 -  certificate that defines \<open>f\<close> using the representation function.
  5.1620 -
  5.1621 -  For each constant \<open>f.abs_eq\<close> is generated. The equation is
  5.1622 -  unconditional for total quotients. The equation defines \<open>f\<close> using
  5.1623 -  the abstraction function.
  5.1624 +  subtypes) \<open>f.rep_eq\<close> is generated. The equation is a code certificate that
  5.1625 +  defines \<open>f\<close> using the representation function.
  5.1626 +
  5.1627 +  For each constant \<open>f.abs_eq\<close> is generated. The equation is unconditional for
  5.1628 +  total quotients. The equation defines \<open>f\<close> using the abstraction function.
  5.1629  
  5.1630    \<^medskip>
  5.1631 -  Integration with [@{attribute code} abstract]: For subtypes
  5.1632 -  (e.g.\ corresponding to a datatype invariant, such as @{typ "'a dlist"}),
  5.1633 -  @{command (HOL) "lift_definition"} uses a code certificate theorem \<open>f.rep_eq\<close> as a code equation. Because of the limitation of the code
  5.1634 -  generator, \<open>f.rep_eq\<close> cannot be used as a code equation if the
  5.1635 -  subtype occurs inside the result type rather than at the top level (e.g.\
  5.1636 -  function returning @{typ "'a dlist option"} vs. @{typ "'a dlist"}).
  5.1637 +  Integration with [@{attribute code} abstract]: For subtypes (e.g.\
  5.1638 +  corresponding to a datatype invariant, such as @{typ "'a dlist"}), @{command
  5.1639 +  (HOL) "lift_definition"} uses a code certificate theorem \<open>f.rep_eq\<close> as a
  5.1640 +  code equation. Because of the limitation of the code generator, \<open>f.rep_eq\<close>
  5.1641 +  cannot be used as a code equation if the subtype occurs inside the result
  5.1642 +  type rather than at the top level (e.g.\ function returning @{typ "'a dlist
  5.1643 +  option"} vs. @{typ "'a dlist"}).
  5.1644  
  5.1645    In this case, an extension of @{command (HOL) "lift_definition"} can be
  5.1646 -  invoked by specifying the flag \<open>code_dt\<close>. This extension enables
  5.1647 -  code execution through series of internal type and lifting definitions if
  5.1648 -  the return type \<open>\<tau>\<close> meets the following inductive conditions:
  5.1649 +  invoked by specifying the flag \<open>code_dt\<close>. This extension enables code
  5.1650 +  execution through series of internal type and lifting definitions if the
  5.1651 +  return type \<open>\<tau>\<close> meets the following inductive conditions:
  5.1652  
  5.1653      \<^descr> \<open>\<tau>\<close> is a type variable
  5.1654  
  5.1655 -    \<^descr> \<open>\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>\<close>,
  5.1656 -    where \<open>\<kappa>\<close> is an abstract type constructor and \<open>\<tau>\<^sub>1 \<dots> \<tau>\<^sub>n\<close>
  5.1657 -    do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed whereas
  5.1658 -    @{typ "int dlist dlist"} not)
  5.1659 -
  5.1660 -    \<^descr> \<open>\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>\<close>, \<open>\<kappa>\<close> is a type constructor that
  5.1661 -    was defined as a (co)datatype whose constructor argument types do not
  5.1662 -    contain either non-free datatypes or the function type.
  5.1663 +    \<^descr> \<open>\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>\<close>, where \<open>\<kappa>\<close> is an abstract type constructor and \<open>\<tau>\<^sub>1 \<dots>
  5.1664 +    \<tau>\<^sub>n\<close> do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed
  5.1665 +    whereas @{typ "int dlist dlist"} not)
  5.1666 +
  5.1667 +    \<^descr> \<open>\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>\<close>, \<open>\<kappa>\<close> is a type constructor that was defined as a
  5.1668 +    (co)datatype whose constructor argument types do not contain either
  5.1669 +    non-free datatypes or the function type.
  5.1670  
  5.1671    Integration with [@{attribute code} equation]: For total quotients,
  5.1672 -  @{command (HOL) "lift_definition"} uses \<open>f.abs_eq\<close> as a code
  5.1673 -  equation.
  5.1674 -
  5.1675 -  \<^descr> @{command (HOL) lifting_forget} and @{command (HOL) lifting_update}
  5.1676 -  These two commands serve for storing and deleting the set-up of the
  5.1677 -  Lifting package and corresponding transfer rules defined by this package.
  5.1678 -  This is useful for hiding of type construction details of an abstract type
  5.1679 -  when the construction is finished but it still allows additions to this
  5.1680 -  construction when this is later necessary.
  5.1681 -
  5.1682 -  Whenever the Lifting package is set up with a new abstract type \<open>\<tau>\<close> by @{command_def (HOL) "lift_definition"}, the package defines a new
  5.1683 -  bundle that is called \<open>\<tau>.lifting\<close>. This bundle already includes
  5.1684 -  set-up for the Lifting package. The new transfer rules introduced by
  5.1685 -  @{command (HOL) "lift_definition"} can be stored in the bundle by the
  5.1686 -  command @{command (HOL) "lifting_update"} \<open>\<tau>.lifting\<close>.
  5.1687 -
  5.1688 -  The command @{command (HOL) "lifting_forget"} \<open>\<tau>.lifting\<close> deletes
  5.1689 -  set-up of the Lifting package for \<open>\<tau>\<close> and deletes all the transfer
  5.1690 -  rules that were introduced by @{command (HOL) "lift_definition"} using
  5.1691 -  \<open>\<tau>\<close> as an abstract type.
  5.1692 +  @{command (HOL) "lift_definition"} uses \<open>f.abs_eq\<close> as a code equation.
  5.1693 +
  5.1694 +  \<^descr> @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} These
  5.1695 +  two commands serve for storing and deleting the set-up of the Lifting
  5.1696 +  package and corresponding transfer rules defined by this package. This is
  5.1697 +  useful for hiding of type construction details of an abstract type when the
  5.1698 +  construction is finished but it still allows additions to this construction
  5.1699 +  when this is later necessary.
  5.1700 +
  5.1701 +  Whenever the Lifting package is set up with a new abstract type \<open>\<tau>\<close> by
  5.1702 +  @{command_def (HOL) "lift_definition"}, the package defines a new bundle
  5.1703 +  that is called \<open>\<tau>.lifting\<close>. This bundle already includes set-up for the
  5.1704 +  Lifting package. The new transfer rules introduced by @{command (HOL)
  5.1705 +  "lift_definition"} can be stored in the bundle by the command @{command
  5.1706 +  (HOL) "lifting_update"} \<open>\<tau>.lifting\<close>.
  5.1707 +
  5.1708 +  The command @{command (HOL) "lifting_forget"} \<open>\<tau>.lifting\<close> deletes set-up of
  5.1709 +  the Lifting package for \<open>\<tau>\<close> and deletes all the transfer rules that were
  5.1710 +  introduced by @{command (HOL) "lift_definition"} using \<open>\<tau>\<close> as an abstract
  5.1711 +  type.
  5.1712  
  5.1713    The stored set-up in a bundle can be reintroduced by the Isar commands for
  5.1714    including a bundle (@{command "include"}, @{keyword "includes"} and
  5.1715    @{command "including"}).
  5.1716  
  5.1717 -  \<^descr> @{command (HOL) "print_quot_maps"} prints stored quotient map
  5.1718 -  theorems.
  5.1719 +  \<^descr> @{command (HOL) "print_quot_maps"} prints stored quotient map theorems.
  5.1720  
  5.1721    \<^descr> @{command (HOL) "print_quotients"} prints stored quotient theorems.
  5.1722  
  5.1723 -  \<^descr> @{attribute (HOL) quot_map} registers a quotient map theorem, a
  5.1724 -  theorem showing how to ``lift'' quotients over type constructors. E.g.\
  5.1725 -  @{term "Quotient R Abs Rep T \<Longrightarrow> Quotient (rel_set R) (image Abs) (image
  5.1726 -  Rep) (rel_set T)"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"}
  5.1727 -  or @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically
  5.1728 -  if the involved type is BNF without dead variables.
  5.1729 -
  5.1730 -  \<^descr> @{attribute (HOL) relator_eq_onp} registers a theorem that shows
  5.1731 -  that a relator applied to an equality restricted by a predicate @{term P}
  5.1732 -  (i.e.\ @{term "eq_onp P"}) is equal to a predicator applied to the @{term
  5.1733 -  P}. The combinator @{const eq_onp} is used for internal encoding of proper
  5.1734 -  subtypes. Such theorems allows the package to hide \<open>eq_onp\<close> from a
  5.1735 -  user in a user-readable form of a respectfulness theorem. For examples see
  5.1736 -  @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
  5.1737 -  This property is proved automatically if the involved type is BNF without
  5.1738 -  dead variables.
  5.1739 +  \<^descr> @{attribute (HOL) quot_map} registers a quotient map theorem, a theorem
  5.1740 +  showing how to ``lift'' quotients over type constructors. E.g.\ @{term
  5.1741 +  "Quotient R Abs Rep T \<Longrightarrow> Quotient (rel_set R) (image Abs) (image Rep)
  5.1742 +  (rel_set T)"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} or
  5.1743 +  @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically if
  5.1744 +  the involved type is BNF without dead variables.
  5.1745 +
  5.1746 +  \<^descr> @{attribute (HOL) relator_eq_onp} registers a theorem that shows that a
  5.1747 +  relator applied to an equality restricted by a predicate @{term P} (i.e.\
  5.1748 +  @{term "eq_onp P"}) is equal to a predicator applied to the @{term P}. The
  5.1749 +  combinator @{const eq_onp} is used for internal encoding of proper subtypes.
  5.1750 +  Such theorems allows the package to hide \<open>eq_onp\<close> from a user in a
  5.1751 +  user-readable form of a respectfulness theorem. For examples see @{file
  5.1752 +  "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
  5.1753 +  property is proved automatically if the involved type is BNF without dead
  5.1754 +  variables.
  5.1755  
  5.1756    \<^descr> @{attribute (HOL) "relator_mono"} registers a property describing a
  5.1757    monotonicity of a relator. E.g.\ @{prop "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}.
  5.1758    This property is needed for proving a stronger transfer rule in
  5.1759 -  @{command_def (HOL) "lift_definition"} when a parametricity theorem for
  5.1760 -  the raw term is specified and also for the reflexivity prover. For
  5.1761 -  examples see @{file "~~/src/HOL/Lifting_Set.thy"} or @{file
  5.1762 -  "~~/src/HOL/Lifting.thy"}. This property is proved automatically if the
  5.1763 -  involved type is BNF without dead variables.
  5.1764 +  @{command_def (HOL) "lift_definition"} when a parametricity theorem for the
  5.1765 +  raw term is specified and also for the reflexivity prover. For examples see
  5.1766 +  @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
  5.1767 +  This property is proved automatically if the involved type is BNF without
  5.1768 +  dead variables.
  5.1769  
  5.1770    \<^descr> @{attribute (HOL) "relator_distr"} registers a property describing a
  5.1771 -  distributivity of the relation composition and a relator. E.g.\ \<open>rel_set R \<circ>\<circ> rel_set S = rel_set (R \<circ>\<circ> S)\<close>. This property is needed for
  5.1772 -  proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
  5.1773 -  when a parametricity theorem for the raw term is specified. When this
  5.1774 -  equality does not hold unconditionally (e.g.\ for the function type), the
  5.1775 -  user can specified each direction separately and also register multiple
  5.1776 -  theorems with different set of assumptions. This attribute can be used
  5.1777 -  only after the monotonicity property was already registered by @{attribute
  5.1778 -  (HOL) "relator_mono"}. For examples see @{file
  5.1779 -  "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
  5.1780 -  property is proved automatically if the involved type is BNF without dead
  5.1781 -  variables.
  5.1782 -
  5.1783 -  \<^descr> @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
  5.1784 -  from the Lifting infrastructure and thus de-register the corresponding
  5.1785 -  quotient. This effectively causes that @{command (HOL) lift_definition}
  5.1786 -  will not do any lifting for the corresponding type. This attribute is
  5.1787 -  rather used for low-level manipulation with set-up of the Lifting package
  5.1788 -  because @{command (HOL) lifting_forget} is preferred for normal usage.
  5.1789 -
  5.1790 -  \<^descr> @{attribute (HOL) lifting_restore} \<open>Quotient_thm pcr_def
  5.1791 -  pcr_cr_eq_thm\<close> registers the Quotient theorem \<open>Quotient_thm\<close> in the
  5.1792 -  Lifting infrastructure and thus sets up lifting for an abstract type
  5.1793 -  \<open>\<tau>\<close> (that is defined by \<open>Quotient_thm\<close>). Optional theorems
  5.1794 -  \<open>pcr_def\<close> and \<open>pcr_cr_eq_thm\<close> can be specified to register the
  5.1795 -  parametrized correspondence relation for \<open>\<tau>\<close>. E.g.\ for @{typ "'a
  5.1796 -  dlist"}, \<open>pcr_def\<close> is \<open>pcr_dlist A \<equiv> list_all2 A \<circ>\<circ>
  5.1797 -  cr_dlist\<close> and \<open>pcr_cr_eq_thm\<close> is \<open>pcr_dlist (op =) = (op
  5.1798 -  =)\<close>. This attribute is rather used for low-level manipulation with set-up
  5.1799 -  of the Lifting package because using of the bundle \<open>\<tau>.lifting\<close>
  5.1800 -  together with the commands @{command (HOL) lifting_forget} and @{command
  5.1801 -  (HOL) lifting_update} is preferred for normal usage.
  5.1802 -
  5.1803 -  \<^descr> Integration with the BNF package @{cite "isabelle-datatypes"}: As
  5.1804 -  already mentioned, the theorems that are registered by the following
  5.1805 -  attributes are proved and registered automatically if the involved type is
  5.1806 -  BNF without dead variables: @{attribute (HOL) quot_map}, @{attribute (HOL)
  5.1807 -  relator_eq_onp}, @{attribute (HOL) "relator_mono"}, @{attribute (HOL)
  5.1808 -  "relator_distr"}. Also the definition of a relator and predicator is
  5.1809 -  provided automatically. Moreover, if the BNF represents a datatype,
  5.1810 -  simplification rules for a predicator are again proved automatically.
  5.1811 +  distributivity of the relation composition and a relator. E.g.\ \<open>rel_set R
  5.1812 +  \<circ>\<circ> rel_set S = rel_set (R \<circ>\<circ> S)\<close>. This property is needed for proving a
  5.1813 +  stronger transfer rule in @{command_def (HOL) "lift_definition"} when a
  5.1814 +  parametricity theorem for the raw term is specified. When this equality does
  5.1815 +  not hold unconditionally (e.g.\ for the function type), the user can
  5.1816 +  specified each direction separately and also register multiple theorems with
  5.1817 +  different set of assumptions. This attribute can be used only after the
  5.1818 +  monotonicity property was already registered by @{attribute (HOL)
  5.1819 +  "relator_mono"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} or
  5.1820 +  @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically if
  5.1821 +  the involved type is BNF without dead variables.
  5.1822 +
  5.1823 +  \<^descr> @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem from
  5.1824 +  the Lifting infrastructure and thus de-register the corresponding quotient.
  5.1825 +  This effectively causes that @{command (HOL) lift_definition} will not do
  5.1826 +  any lifting for the corresponding type. This attribute is rather used for
  5.1827 +  low-level manipulation with set-up of the Lifting package because @{command
  5.1828 +  (HOL) lifting_forget} is preferred for normal usage.
  5.1829 +
  5.1830 +  \<^descr> @{attribute (HOL) lifting_restore} \<open>Quotient_thm pcr_def pcr_cr_eq_thm\<close>
  5.1831 +  registers the Quotient theorem \<open>Quotient_thm\<close> in the Lifting infrastructure
  5.1832 +  and thus sets up lifting for an abstract type \<open>\<tau>\<close> (that is defined by
  5.1833 +  \<open>Quotient_thm\<close>). Optional theorems \<open>pcr_def\<close> and \<open>pcr_cr_eq_thm\<close> can be
  5.1834 +  specified to register the parametrized correspondence relation for \<open>\<tau>\<close>.
  5.1835 +  E.g.\ for @{typ "'a dlist"}, \<open>pcr_def\<close> is \<open>pcr_dlist A \<equiv> list_all2 A \<circ>\<circ>
  5.1836 +  cr_dlist\<close> and \<open>pcr_cr_eq_thm\<close> is \<open>pcr_dlist (op =) = (op =)\<close>. This attribute
  5.1837 +  is rather used for low-level manipulation with set-up of the Lifting package
  5.1838 +  because using of the bundle \<open>\<tau>.lifting\<close> together with the commands @{command
  5.1839 +  (HOL) lifting_forget} and @{command (HOL) lifting_update} is preferred for
  5.1840 +  normal usage.
  5.1841 +
  5.1842 +  \<^descr> Integration with the BNF package @{cite "isabelle-datatypes"}: As already
  5.1843 +  mentioned, the theorems that are registered by the following attributes are
  5.1844 +  proved and registered automatically if the involved type is BNF without dead
  5.1845 +  variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp},
  5.1846 +  @{attribute (HOL) "relator_mono"}, @{attribute (HOL) "relator_distr"}. Also
  5.1847 +  the definition of a relator and predicator is provided automatically.
  5.1848 +  Moreover, if the BNF represents a datatype, simplification rules for a
  5.1849 +  predicator are again proved automatically.
  5.1850  \<close>
  5.1851  
  5.1852  
  5.1853 @@ -1538,47 +1497,46 @@
  5.1854      @{attribute_def (HOL) "relator_domain"} & : & \<open>attribute\<close> \\
  5.1855    \end{matharray}
  5.1856  
  5.1857 -  \<^descr> @{method (HOL) "transfer"} method replaces the current subgoal with
  5.1858 -  a logically equivalent one that uses different types and constants. The
  5.1859 +  \<^descr> @{method (HOL) "transfer"} method replaces the current subgoal with a
  5.1860 +  logically equivalent one that uses different types and constants. The
  5.1861    replacement of types and constants is guided by the database of transfer
  5.1862    rules. Goals are generalized over all free variables by default; this is
  5.1863    necessary for variables whose types change, but can be overridden for
  5.1864    specific variables with e.g. \<open>transfer fixing: x y z\<close>.
  5.1865  
  5.1866 -  \<^descr> @{method (HOL) "transfer'"} is a variant of @{method (HOL) transfer}
  5.1867 -  that allows replacing a subgoal with one that is logically stronger
  5.1868 -  (rather than equivalent). For example, a subgoal involving equality on a
  5.1869 -  quotient type could be replaced with a subgoal involving equality (instead
  5.1870 -  of the corresponding equivalence relation) on the underlying raw type.
  5.1871 -
  5.1872 -  \<^descr> @{method (HOL) "transfer_prover"} method assists with proving a
  5.1873 -  transfer rule for a new constant, provided the constant is defined in
  5.1874 -  terms of other constants that already have transfer rules. It should be
  5.1875 -  applied after unfolding the constant definitions.
  5.1876 +  \<^descr> @{method (HOL) "transfer'"} is a variant of @{method (HOL) transfer} that
  5.1877 +  allows replacing a subgoal with one that is logically stronger (rather than
  5.1878 +  equivalent). For example, a subgoal involving equality on a quotient type
  5.1879 +  could be replaced with a subgoal involving equality (instead of the
  5.1880 +  corresponding equivalence relation) on the underlying raw type.
  5.1881 +
  5.1882 +  \<^descr> @{method (HOL) "transfer_prover"} method assists with proving a transfer
  5.1883 +  rule for a new constant, provided the constant is defined in terms of other
  5.1884 +  constants that already have transfer rules. It should be applied after
  5.1885 +  unfolding the constant definitions.
  5.1886  
  5.1887    \<^descr> @{method (HOL) "transfer_start"}, @{method (HOL) "transfer_step"},
  5.1888 -  @{method (HOL) "transfer_end"}, @{method (HOL) "transfer_prover_start"}
  5.1889 -  and @{method (HOL) "transfer_prover_end"} methods are meant to be used
  5.1890 -  for debugging of @{method (HOL) "transfer"} and @{method (HOL) "transfer_prover"},
  5.1891 -  which we can decompose as follows:
  5.1892 -  @{method (HOL) "transfer"} = (@{method (HOL) "transfer_start"}, 
  5.1893 -  @{method (HOL) "transfer_step"}+, @{method (HOL) "transfer_end"}) and
  5.1894 -  @{method (HOL) "transfer_prover"} = (@{method (HOL) "transfer_prover_start"}, 
  5.1895 -  @{method (HOL) "transfer_step"}+, @{method (HOL) "transfer_prover_end"}).
  5.1896 -  For usage examples see @{file "~~/src/HOL/ex/Transfer_Debug.thy"} 
  5.1897 -
  5.1898 -  \<^descr> @{attribute (HOL) "untransferred"} proves the same equivalent
  5.1899 -  theorem as @{method (HOL) "transfer"} internally does.
  5.1900 -
  5.1901 -  \<^descr> @{attribute (HOL) Transfer.transferred} works in the opposite
  5.1902 -  direction than @{method (HOL) "transfer'"}. E.g.\ given the transfer
  5.1903 -  relation \<open>ZN x n \<equiv> (x = int n)\<close>, corresponding transfer rules and
  5.1904 -  the theorem \<open>\<forall>x::int \<in> {0..}. x < x + 1\<close>, the attribute would
  5.1905 -  prove \<open>\<forall>n::nat. n < n + 1\<close>. The attribute is still in experimental
  5.1906 -  phase of development.
  5.1907 -
  5.1908 -  \<^descr> @{attribute (HOL) "transfer_rule"} attribute maintains a collection
  5.1909 -  of transfer rules, which relate constants at two different types. Typical
  5.1910 +  @{method (HOL) "transfer_end"}, @{method (HOL) "transfer_prover_start"} and
  5.1911 +  @{method (HOL) "transfer_prover_end"} methods are meant to be used for
  5.1912 +  debugging of @{method (HOL) "transfer"} and @{method (HOL)
  5.1913 +  "transfer_prover"}, which we can decompose as follows: @{method (HOL)
  5.1914 +  "transfer"} = (@{method (HOL) "transfer_start"}, @{method (HOL)
  5.1915 +  "transfer_step"}+, @{method (HOL) "transfer_end"}) and @{method (HOL)
  5.1916 +  "transfer_prover"} = (@{method (HOL) "transfer_prover_start"}, @{method
  5.1917 +  (HOL) "transfer_step"}+, @{method (HOL) "transfer_prover_end"}). For usage
  5.1918 +  examples see @{file "~~/src/HOL/ex/Transfer_Debug.thy"}
  5.1919 +
  5.1920 +  \<^descr> @{attribute (HOL) "untransferred"} proves the same equivalent theorem as
  5.1921 +  @{method (HOL) "transfer"} internally does.
  5.1922 +
  5.1923 +  \<^descr> @{attribute (HOL) Transfer.transferred} works in the opposite direction
  5.1924 +  than @{method (HOL) "transfer'"}. E.g.\ given the transfer relation \<open>ZN x n
  5.1925 +  \<equiv> (x = int n)\<close>, corresponding transfer rules and the theorem \<open>\<forall>x::int \<in>
  5.1926 +  {0..}. x < x + 1\<close>, the attribute would prove \<open>\<forall>n::nat. n < n + 1\<close>. The
  5.1927 +  attribute is still in experimental phase of development.
  5.1928 +
  5.1929 +  \<^descr> @{attribute (HOL) "transfer_rule"} attribute maintains a collection of
  5.1930 +  transfer rules, which relate constants at two different types. Typical
  5.1931    transfer rules may relate different type instances of the same polymorphic
  5.1932    constant, or they may relate an operation on a raw type to a corresponding
  5.1933    operation on an abstract type (quotient or subtype). For example:
  5.1934 @@ -1592,17 +1550,17 @@
  5.1935      \<open>bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct\<close> \\
  5.1936      \<open>\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)\<close>
  5.1937  
  5.1938 -  Preservation of predicates on relations (\<open>bi_unique, bi_total,
  5.1939 -  right_unique, right_total, left_unique, left_total\<close>) with the respect to
  5.1940 -  a relator is proved automatically if the involved type is BNF @{cite
  5.1941 +  Preservation of predicates on relations (\<open>bi_unique, bi_total, right_unique,
  5.1942 +  right_total, left_unique, left_total\<close>) with the respect to a relator is
  5.1943 +  proved automatically if the involved type is BNF @{cite
  5.1944    "isabelle-datatypes"} without dead variables.
  5.1945  
  5.1946 -  \<^descr> @{attribute (HOL) "transfer_domain_rule"} attribute maintains a
  5.1947 -  collection of rules, which specify a domain of a transfer relation by a
  5.1948 -  predicate. E.g.\ given the transfer relation \<open>ZN x n \<equiv> (x = int
  5.1949 -  n)\<close>, one can register the following transfer domain rule: \<open>Domainp
  5.1950 -  ZN = (\<lambda>x. x \<ge> 0)\<close>. The rules allow the package to produce more readable
  5.1951 -  transferred goals, e.g.\ when quantifiers are transferred.
  5.1952 +  \<^descr> @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
  5.1953 +  of rules, which specify a domain of a transfer relation by a predicate.
  5.1954 +  E.g.\ given the transfer relation \<open>ZN x n \<equiv> (x = int n)\<close>, one can register
  5.1955 +  the following transfer domain rule: \<open>Domainp ZN = (\<lambda>x. x \<ge> 0)\<close>. The rules
  5.1956 +  allow the package to produce more readable transferred goals, e.g.\ when
  5.1957 +  quantifiers are transferred.
  5.1958  
  5.1959    \<^descr> @{attribute (HOL) relator_eq} attribute collects identity laws for
  5.1960    relators of various type constructors, e.g. @{term "rel_set (op =) = (op
  5.1961 @@ -1660,8 +1618,8 @@
  5.1962      @@{method (HOL) lifting_setup} @{syntax thms}?
  5.1963    \<close>}
  5.1964  
  5.1965 -  \<^descr> @{command (HOL) "quotient_definition"} defines a constant on the
  5.1966 -  quotient type.
  5.1967 +  \<^descr> @{command (HOL) "quotient_definition"} defines a constant on the quotient
  5.1968 +  type.
  5.1969  
  5.1970    \<^descr> @{command (HOL) "print_quotmapsQ3"} prints quotient map functions.
  5.1971  
  5.1972 @@ -1669,42 +1627,42 @@
  5.1973  
  5.1974    \<^descr> @{command (HOL) "print_quotconsts"} prints quotient constants.
  5.1975  
  5.1976 -  \<^descr> @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"}
  5.1977 -  methods match the current goal with the given raw theorem to be lifted
  5.1978 -  producing three new subgoals: regularization, injection and cleaning
  5.1979 -  subgoals. @{method (HOL) "lifting"} tries to apply the heuristics for
  5.1980 -  automatically solving these three subgoals and leaves only the subgoals
  5.1981 -  unsolved by the heuristics to the user as opposed to @{method (HOL)
  5.1982 -  "lifting_setup"} which leaves the three subgoals unsolved.
  5.1983 -
  5.1984 -  \<^descr> @{method (HOL) "descending"} and @{method (HOL) "descending_setup"}
  5.1985 -  try to guess a raw statement that would lift to the current subgoal. Such
  5.1986 -  statement is assumed as a new subgoal and @{method (HOL) "descending"}
  5.1987 -  continues in the same way as @{method (HOL) "lifting"} does. @{method
  5.1988 -  (HOL) "descending"} tries to solve the arising regularization, injection
  5.1989 -  and cleaning subgoals with the analogous method @{method (HOL)
  5.1990 -  "descending_setup"} which leaves the four unsolved subgoals.
  5.1991 -
  5.1992 -  \<^descr> @{method (HOL) "partiality_descending"} finds the regularized
  5.1993 -  theorem that would lift to the current subgoal, lifts it and leaves as a
  5.1994 -  subgoal. This method can be used with partial equivalence quotients where
  5.1995 -  the non regularized statements would not be true. @{method (HOL)
  5.1996 +  \<^descr> @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"} methods
  5.1997 +  match the current goal with the given raw theorem to be lifted producing
  5.1998 +  three new subgoals: regularization, injection and cleaning subgoals.
  5.1999 +  @{method (HOL) "lifting"} tries to apply the heuristics for automatically
  5.2000 +  solving these three subgoals and leaves only the subgoals unsolved by the
  5.2001 +  heuristics to the user as opposed to @{method (HOL) "lifting_setup"} which
  5.2002 +  leaves the three subgoals unsolved.
  5.2003 +
  5.2004 +  \<^descr> @{method (HOL) "descending"} and @{method (HOL) "descending_setup"} try to
  5.2005 +  guess a raw statement that would lift to the current subgoal. Such statement
  5.2006 +  is assumed as a new subgoal and @{method (HOL) "descending"} continues in
  5.2007 +  the same way as @{method (HOL) "lifting"} does. @{method (HOL) "descending"}
  5.2008 +  tries to solve the arising regularization, injection and cleaning subgoals
  5.2009 +  with the analogous method @{method (HOL) "descending_setup"} which leaves
  5.2010 +  the four unsolved subgoals.
  5.2011 +
  5.2012 +  \<^descr> @{method (HOL) "partiality_descending"} finds the regularized theorem that
  5.2013 +  would lift to the current subgoal, lifts it and leaves as a subgoal. This
  5.2014 +  method can be used with partial equivalence quotients where the non
  5.2015 +  regularized statements would not be true. @{method (HOL)
  5.2016    "partiality_descending_setup"} leaves the injection and cleaning subgoals
  5.2017    unchanged.
  5.2018  
  5.2019 -  \<^descr> @{method (HOL) "regularize"} applies the regularization heuristics
  5.2020 -  to the current subgoal.
  5.2021 +  \<^descr> @{method (HOL) "regularize"} applies the regularization heuristics to the
  5.2022 +  current subgoal.
  5.2023  
  5.2024    \<^descr> @{method (HOL) "injection"} applies the injection heuristics to the
  5.2025    current goal using the stored quotient respectfulness theorems.
  5.2026  
  5.2027 -  \<^descr> @{method (HOL) "cleaning"} applies the injection cleaning heuristics
  5.2028 -  to the current subgoal using the stored quotient preservation theorems.
  5.2029 -
  5.2030 -  \<^descr> @{attribute (HOL) quot_lifted} attribute tries to automatically
  5.2031 -  transport the theorem to the quotient type. The attribute uses all the
  5.2032 -  defined quotients types and quotient constants often producing undesired
  5.2033 -  results or theorems that cannot be lifted.
  5.2034 +  \<^descr> @{method (HOL) "cleaning"} applies the injection cleaning heuristics to
  5.2035 +  the current subgoal using the stored quotient preservation theorems.
  5.2036 +
  5.2037 +  \<^descr> @{attribute (HOL) quot_lifted} attribute tries to automatically transport
  5.2038 +  the theorem to the quotient type. The attribute uses all the defined
  5.2039 +  quotients types and quotient constants often producing undesired results or
  5.2040 +  theorems that cannot be lifted.
  5.2041  
  5.2042    \<^descr> @{attribute (HOL) quot_respect} and @{attribute (HOL) quot_preserve}
  5.2043    attributes declare a theorem as a respectfulness and preservation theorem
  5.2044 @@ -1712,14 +1670,14 @@
  5.2045    @{method (HOL) "injection"} and @{method (HOL) "cleaning"} methods
  5.2046    respectively.
  5.2047  
  5.2048 -  \<^descr> @{attribute (HOL) quot_thm} declares that a certain theorem is a
  5.2049 -  quotient extension theorem. Quotient extension theorems allow for
  5.2050 -  quotienting inside container types. Given a polymorphic type that serves
  5.2051 -  as a container, a map function defined for this container using @{command
  5.2052 -  (HOL) "functor"} and a relation map defined for for the container type,
  5.2053 -  the quotient extension theorem should be @{term "Quotient3 R Abs Rep \<Longrightarrow>
  5.2054 -  Quotient3 (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
  5.2055 -  are stored in a database and are used all the steps of lifting theorems.
  5.2056 +  \<^descr> @{attribute (HOL) quot_thm} declares that a certain theorem is a quotient
  5.2057 +  extension theorem. Quotient extension theorems allow for quotienting inside
  5.2058 +  container types. Given a polymorphic type that serves as a container, a map
  5.2059 +  function defined for this container using @{command (HOL) "functor"} and a
  5.2060 +  relation map defined for for the container type, the quotient extension
  5.2061 +  theorem should be @{term "Quotient3 R Abs Rep \<Longrightarrow> Quotient3 (rel_map R) (map
  5.2062 +  Abs) (map Rep)"}. Quotient extension theorems are stored in a database and
  5.2063 +  are used all the steps of lifting theorems.
  5.2064  \<close>
  5.2065  
  5.2066  
  5.2067 @@ -1728,9 +1686,9 @@
  5.2068  section \<open>Proving propositions\<close>
  5.2069  
  5.2070  text \<open>
  5.2071 -  In addition to the standard proof methods, a number of diagnosis
  5.2072 -  tools search for proofs and provide an Isar proof snippet on success.
  5.2073 -  These tools are available via the following commands.
  5.2074 +  In addition to the standard proof methods, a number of diagnosis tools
  5.2075 +  search for proofs and provide an Isar proof snippet on success. These tools
  5.2076 +  are available via the following commands.
  5.2077  
  5.2078    \begin{matharray}{rcl}
  5.2079      @{command_def (HOL) "solve_direct"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
  5.2080 @@ -1758,25 +1716,23 @@
  5.2081      facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thms} ) + ) ? ')'
  5.2082    \<close>} % FIXME check args "value"
  5.2083  
  5.2084 -  \<^descr> @{command (HOL) "solve_direct"} checks whether the current
  5.2085 -  subgoals can be solved directly by an existing theorem. Duplicate
  5.2086 -  lemmas can be detected in this way.
  5.2087 -
  5.2088 -  \<^descr> @{command (HOL) "try0"} attempts to prove a subgoal
  5.2089 -  using a combination of standard proof methods (@{method auto},
  5.2090 -  @{method simp}, @{method blast}, etc.).  Additional facts supplied
  5.2091 -  via \<open>simp:\<close>, \<open>intro:\<close>, \<open>elim:\<close>, and \<open>dest:\<close> are passed to the appropriate proof methods.
  5.2092 -
  5.2093 -  \<^descr> @{command (HOL) "try"} attempts to prove or disprove a subgoal
  5.2094 -  using a combination of provers and disprovers (@{command (HOL)
  5.2095 -  "solve_direct"}, @{command (HOL) "quickcheck"}, @{command (HOL)
  5.2096 -  "try0"}, @{command (HOL) "sledgehammer"}, @{command (HOL)
  5.2097 -  "nitpick"}).
  5.2098 -
  5.2099 -  \<^descr> @{command (HOL) "sledgehammer"} attempts to prove a subgoal
  5.2100 -  using external automatic provers (resolution provers and SMT
  5.2101 -  solvers). See the Sledgehammer manual @{cite "isabelle-sledgehammer"}
  5.2102 -  for details.
  5.2103 +  \<^descr> @{command (HOL) "solve_direct"} checks whether the current subgoals can be
  5.2104 +  solved directly by an existing theorem. Duplicate lemmas can be detected in
  5.2105 +  this way.
  5.2106 +
  5.2107 +  \<^descr> @{command (HOL) "try0"} attempts to prove a subgoal using a combination of
  5.2108 +  standard proof methods (@{method auto}, @{method simp}, @{method blast},
  5.2109 +  etc.). Additional facts supplied via \<open>simp:\<close>, \<open>intro:\<close>, \<open>elim:\<close>, and \<open>dest:\<close>
  5.2110 +  are passed to the appropriate proof methods.
  5.2111 +
  5.2112 +  \<^descr> @{command (HOL) "try"} attempts to prove or disprove a subgoal using a
  5.2113 +  combination of provers and disprovers (@{command (HOL) "solve_direct"},
  5.2114 +  @{command (HOL) "quickcheck"}, @{command (HOL) "try0"}, @{command (HOL)
  5.2115 +  "sledgehammer"}, @{command (HOL) "nitpick"}).
  5.2116 +
  5.2117 +  \<^descr> @{command (HOL) "sledgehammer"} attempts to prove a subgoal using external
  5.2118 +  automatic provers (resolution provers and SMT solvers). See the Sledgehammer
  5.2119 +  manual @{cite "isabelle-sledgehammer"} for details.
  5.2120  
  5.2121    \<^descr> @{command (HOL) "sledgehammer_params"} changes @{command (HOL)
  5.2122    "sledgehammer"} configuration options persistently.
  5.2123 @@ -1786,9 +1742,9 @@
  5.2124  section \<open>Checking and refuting propositions\<close>
  5.2125  
  5.2126  text \<open>
  5.2127 -  Identifying incorrect propositions usually involves evaluation of
  5.2128 -  particular assignments and systematic counterexample search.  This
  5.2129 -  is supported by the following commands.
  5.2130 +  Identifying incorrect propositions usually involves evaluation of particular
  5.2131 +  assignments and systematic counterexample search. This is supported by the
  5.2132 +  following commands.
  5.2133  
  5.2134    \begin{matharray}{rcl}
  5.2135      @{command_def (HOL) "value"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  5.2136 @@ -1827,130 +1783,121 @@
  5.2137      args: ( @{syntax name} '=' value + ',' )
  5.2138    \<close>} % FIXME check "value"
  5.2139  
  5.2140 -  \<^descr> @{command (HOL) "value"}~\<open>t\<close> evaluates and prints a
  5.2141 -  term; optionally \<open>modes\<close> can be specified, which are appended
  5.2142 -  to the current print mode; see \secref{sec:print-modes}.
  5.2143 -  Evaluation is tried first using ML, falling
  5.2144 -  back to normalization by evaluation if this fails.
  5.2145 -  Alternatively a specific evaluator can be selected using square
  5.2146 -  brackets; typical evaluators use the current set of code equations
  5.2147 -  to normalize and include \<open>simp\<close> for fully symbolic evaluation
  5.2148 -  using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
  5.2149 +  \<^descr> @{command (HOL) "value"}~\<open>t\<close> evaluates and prints a term; optionally
  5.2150 +  \<open>modes\<close> can be specified, which are appended to the current print mode; see
  5.2151 +  \secref{sec:print-modes}. Evaluation is tried first using ML, falling back
  5.2152 +  to normalization by evaluation if this fails. Alternatively a specific
  5.2153 +  evaluator can be selected using square brackets; typical evaluators use the
  5.2154 +  current set of code equations to normalize and include \<open>simp\<close> for fully
  5.2155 +  symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
  5.2156    evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
  5.2157  
  5.2158 -  \<^descr> @{command (HOL) "values"}~\<open>t\<close> enumerates a set
  5.2159 -  comprehension by evaluation and prints its values up to the given
  5.2160 -  number of solutions; optionally \<open>modes\<close> can be specified,
  5.2161 -  which are appended to the current print mode; see
  5.2162 +  \<^descr> @{command (HOL) "values"}~\<open>t\<close> enumerates a set comprehension by evaluation
  5.2163 +  and prints its values up to the given number of solutions; optionally
  5.2164 +  \<open>modes\<close> can be specified, which are appended to the current print mode; see
  5.2165    \secref{sec:print-modes}.
  5.2166  
  5.2167 -  \<^descr> @{command (HOL) "quickcheck"} tests the current goal for
  5.2168 -  counterexamples using a series of assignments for its free
  5.2169 -  variables; by default the first subgoal is tested, an other can be
  5.2170 -  selected explicitly using an optional goal index.  Assignments can
  5.2171 -  be chosen exhausting the search space up to a given size, or using a
  5.2172 -  fixed number of random assignments in the search space, or exploring
  5.2173 -  the search space symbolically using narrowing.  By default,
  5.2174 -  quickcheck uses exhaustive testing.  A number of configuration
  5.2175 +  \<^descr> @{command (HOL) "quickcheck"} tests the current goal for counterexamples
  5.2176 +  using a series of assignments for its free variables; by default the first
  5.2177 +  subgoal is tested, an other can be selected explicitly using an optional
  5.2178 +  goal index. Assignments can be chosen exhausting the search space up to a
  5.2179 +  given size, or using a fixed number of random assignments in the search
  5.2180 +  space, or exploring the search space symbolically using narrowing. By
  5.2181 +  default, quickcheck uses exhaustive testing. A number of configuration
  5.2182    options are supported for @{command (HOL) "quickcheck"}, notably:
  5.2183  
  5.2184 -    \<^descr>[\<open>tester\<close>] specifies which testing approach to apply.
  5.2185 -    There are three testers, \<open>exhaustive\<close>, \<open>random\<close>, and
  5.2186 -    \<open>narrowing\<close>.  An unknown configuration option is treated as
  5.2187 -    an argument to tester, making \<open>tester =\<close> optional.  When
  5.2188 -    multiple testers are given, these are applied in parallel.  If no
  5.2189 -    tester is specified, quickcheck uses the testers that are set
  5.2190 -    active, i.e.\ configurations @{attribute
  5.2191 -    quickcheck_exhaustive_active}, @{attribute
  5.2192 -    quickcheck_random_active}, @{attribute
  5.2193 +    \<^descr>[\<open>tester\<close>] specifies which testing approach to apply. There are three
  5.2194 +    testers, \<open>exhaustive\<close>, \<open>random\<close>, and \<open>narrowing\<close>. An unknown configuration
  5.2195 +    option is treated as an argument to tester, making \<open>tester =\<close> optional.
  5.2196 +    When multiple testers are given, these are applied in parallel. If no
  5.2197 +    tester is specified, quickcheck uses the testers that are set active,
  5.2198 +    i.e.\ configurations @{attribute quickcheck_exhaustive_active},
  5.2199 +    @{attribute quickcheck_random_active}, @{attribute
  5.2200      quickcheck_narrowing_active} are set to true.
  5.2201  
  5.2202 -    \<^descr>[\<open>size\<close>] specifies the maximum size of the search space
  5.2203 -    for assignment values.
  5.2204 -
  5.2205 -    \<^descr>[\<open>genuine_only\<close>] sets quickcheck only to return genuine
  5.2206 -    counterexample, but not potentially spurious counterexamples due
  5.2207 -    to underspecified functions.
  5.2208 -
  5.2209 -    \<^descr>[\<open>abort_potential\<close>] sets quickcheck to abort once it
  5.2210 -    found a potentially spurious counterexample and to not continue
  5.2211 -    to search for a further genuine counterexample.
  5.2212 -    For this option to be effective, the \<open>genuine_only\<close> option
  5.2213 -    must be set to false.
  5.2214 -
  5.2215 -    \<^descr>[\<open>eval\<close>] takes a term or a list of terms and evaluates
  5.2216 -    these terms under the variable assignment found by quickcheck.
  5.2217 -    This option is currently only supported by the default
  5.2218 -    (exhaustive) tester.
  5.2219 -
  5.2220 -    \<^descr>[\<open>iterations\<close>] sets how many sets of assignments are
  5.2221 -    generated for each particular size.
  5.2222 -
  5.2223 -    \<^descr>[\<open>no_assms\<close>] specifies whether assumptions in
  5.2224 -    structured proofs should be ignored.
  5.2225 -
  5.2226 -    \<^descr>[\<open>locale\<close>] specifies how to process conjectures in
  5.2227 -    a locale context, i.e.\ they can be interpreted or expanded.
  5.2228 -    The option is a whitespace-separated list of the two words
  5.2229 -    \<open>interpret\<close> and \<open>expand\<close>. The list determines the
  5.2230 -    order they are employed. The default setting is to first use
  5.2231 -    interpretations and then test the expanded conjecture.
  5.2232 -    The option is only provided as attribute declaration, but not
  5.2233 -    as parameter to the command.
  5.2234 +    \<^descr>[\<open>size\<close>] specifies the maximum size of the search space for assignment
  5.2235 +    values.
  5.2236 +
  5.2237 +    \<^descr>[\<open>genuine_only\<close>] sets quickcheck only to return genuine counterexample,
  5.2238 +    but not potentially spurious counterexamples due to underspecified
  5.2239 +    functions.
  5.2240 +
  5.2241 +    \<^descr>[\<open>abort_potential\<close>] sets quickcheck to abort once it found a potentially
  5.2242 +    spurious counterexample and to not continue to search for a further
  5.2243 +    genuine counterexample. For this option to be effective, the
  5.2244 +    \<open>genuine_only\<close> option must be set to false.
  5.2245 +
  5.2246 +    \<^descr>[\<open>eval\<close>] takes a term or a list of terms and evaluates these terms under
  5.2247 +    the variable assignment found by quickcheck. This option is currently only
  5.2248 +    supported by the default (exhaustive) tester.
  5.2249 +
  5.2250 +    \<^descr>[\<open>iterations\<close>] sets how many sets of assignments are generated for each
  5.2251 +    particular size.
  5.2252 +
  5.2253 +    \<^descr>[\<open>no_assms\<close>] specifies whether assumptions in structured proofs should be
  5.2254 +    ignored.
  5.2255 +
  5.2256 +    \<^descr>[\<open>locale\<close>] specifies how to process conjectures in a locale context,
  5.2257 +    i.e.\ they can be interpreted or expanded. The option is a
  5.2258 +    whitespace-separated list of the two words \<open>interpret\<close> and \<open>expand\<close>. The
  5.2259 +    list determines the order they are employed. The default setting is to
  5.2260 +    first use interpretations and then test the expanded conjecture. The
  5.2261 +    option is only provided as attribute declaration, but not as parameter to
  5.2262 +    the command.
  5.2263  
  5.2264      \<^descr>[\<open>timeout\<close>] sets the time limit in seconds.
  5.2265  
  5.2266 -    \<^descr>[\<open>default_type\<close>] sets the type(s) generally used to
  5.2267 -    instantiate type variables.
  5.2268 -
  5.2269 -    \<^descr>[\<open>report\<close>] if set quickcheck reports how many tests
  5.2270 -    fulfilled the preconditions.
  5.2271 -
  5.2272 -    \<^descr>[\<open>use_subtype\<close>] if set quickcheck automatically lifts
  5.2273 -    conjectures to registered subtypes if possible, and tests the
  5.2274 -    lifted conjecture.
  5.2275 -
  5.2276 -    \<^descr>[\<open>quiet\<close>] if set quickcheck does not output anything
  5.2277 -    while testing.
  5.2278 -
  5.2279 -    \<^descr>[\<open>verbose\<close>] if set quickcheck informs about the current
  5.2280 -    size and cardinality while testing.
  5.2281 -
  5.2282 -    \<^descr>[\<open>expect\<close>] can be used to check if the user's
  5.2283 -    expectation was met (\<open>no_expectation\<close>, \<open>no_counterexample\<close>, or \<open>counterexample\<close>).
  5.2284 +    \<^descr>[\<open>default_type\<close>] sets the type(s) generally used to instantiate type
  5.2285 +    variables.
  5.2286 +
  5.2287 +    \<^descr>[\<open>report\<close>] if set quickcheck reports how many tests fulfilled the
  5.2288 +    preconditions.
  5.2289 +
  5.2290 +    \<^descr>[\<open>use_subtype\<close>] if set quickcheck automatically lifts conjectures to
  5.2291 +    registered subtypes if possible, and tests the lifted conjecture.
  5.2292 +
  5.2293 +    \<^descr>[\<open>quiet\<close>] if set quickcheck does not output anything while testing.
  5.2294 +
  5.2295 +    \<^descr>[\<open>verbose\<close>] if set quickcheck informs about the current size and
  5.2296 +    cardinality while testing.
  5.2297 +
  5.2298 +    \<^descr>[\<open>expect\<close>] can be used to check if the user's expectation was met
  5.2299 +    (\<open>no_expectation\<close>, \<open>no_counterexample\<close>, or \<open>counterexample\<close>).
  5.2300  
  5.2301    These option can be given within square brackets.
  5.2302  
  5.2303    Using the following type classes, the testers generate values and convert
  5.2304    them back into Isabelle terms for displaying counterexamples.
  5.2305  
  5.2306 -    \<^descr>[\<open>exhaustive\<close>] The parameters of the type classes @{class exhaustive}
  5.2307 -    and @{class full_exhaustive} implement the testing. They take a
  5.2308 -    testing function as a parameter, which takes a value of type @{typ "'a"}
  5.2309 -    and optionally produces a counterexample, and a size parameter for the test values.
  5.2310 -    In @{class full_exhaustive}, the testing function parameter additionally
  5.2311 -    expects a lazy term reconstruction in the type @{typ Code_Evaluation.term}
  5.2312 -    of the tested value.
  5.2313 +    \<^descr>[\<open>exhaustive\<close>] The parameters of the type classes @{class exhaustive} and
  5.2314 +    @{class full_exhaustive} implement the testing. They take a testing
  5.2315 +    function as a parameter, which takes a value of type @{typ "'a"} and
  5.2316 +    optionally produces a counterexample, and a size parameter for the test
  5.2317 +    values. In @{class full_exhaustive}, the testing function parameter
  5.2318 +    additionally expects a lazy term reconstruction in the type @{typ
  5.2319 +    Code_Evaluation.term} of the tested value.
  5.2320  
  5.2321      The canonical implementation for \<open>exhaustive\<close> testers calls the given
  5.2322 -    testing function on all values up to the given size and stops as soon
  5.2323 -    as a counterexample is found.
  5.2324 -
  5.2325 -    \<^descr>[\<open>random\<close>] The operation @{const Quickcheck_Random.random}
  5.2326 -    of the type class @{class random} generates a pseudo-random
  5.2327 -    value of the given size and a lazy term reconstruction of the value
  5.2328 -    in the type @{typ Code_Evaluation.term}. A pseudo-randomness generator
  5.2329 -    is defined in theory @{theory Random}.
  5.2330 -
  5.2331 -    \<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck @{cite "runciman-naylor-lindblad"}
  5.2332 -    using the type classes @{class narrowing} and @{class partial_term_of}.
  5.2333 -    Variables in the current goal are initially represented as symbolic variables.
  5.2334 -    If the execution of the goal tries to evaluate one of them, the test engine
  5.2335 -    replaces it with refinements provided by @{const narrowing}.
  5.2336 -    Narrowing views every value as a sum-of-products which is expressed using the operations
  5.2337 -    @{const Quickcheck_Narrowing.cons} (embedding a value),
  5.2338 -    @{const Quickcheck_Narrowing.apply} (product) and @{const Quickcheck_Narrowing.sum} (sum).
  5.2339 -    The refinement should enable further evaluation of the goal.
  5.2340 +    testing function on all values up to the given size and stops as soon as a
  5.2341 +    counterexample is found.
  5.2342 +
  5.2343 +    \<^descr>[\<open>random\<close>] The operation @{const Quickcheck_Random.random} of the type
  5.2344 +    class @{class random} generates a pseudo-random value of the given size
  5.2345 +    and a lazy term reconstruction of the value in the type @{typ
  5.2346 +    Code_Evaluation.term}. A pseudo-randomness generator is defined in theory
  5.2347 +    @{theory Random}.
  5.2348 +
  5.2349 +    \<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck @{cite
  5.2350 +    "runciman-naylor-lindblad"} using the type classes @{class narrowing} and
  5.2351 +    @{class partial_term_of}. Variables in the current goal are initially
  5.2352 +    represented as symbolic variables. If the execution of the goal tries to
  5.2353 +    evaluate one of them, the test engine replaces it with refinements
  5.2354 +    provided by @{const narrowing}. Narrowing views every value as a
  5.2355 +    sum-of-products which is expressed using the operations @{const
  5.2356 +    Quickcheck_Narrowing.cons} (embedding a value), @{const
  5.2357 +    Quickcheck_Narrowing.apply} (product) and @{const
  5.2358 +    Quickcheck_Narrowing.sum} (sum). The refinement should enable further
  5.2359 +    evaluation of the goal.
  5.2360  
  5.2361      For example, @{const narrowing} for the list type @{typ "'a :: narrowing list"}
  5.2362      can be recursively defined as
  5.2363 @@ -1960,45 +1907,44 @@
  5.2364                    (Quickcheck_Narrowing.cons (op #))
  5.2365                    narrowing)
  5.2366                  narrowing)"}.
  5.2367 -    If a symbolic variable of type @{typ "_ list"} is evaluated, it is replaced by (i)~the empty
  5.2368 -    list @{term "[]"} and (ii)~by a non-empty list whose head and tail can then be recursively
  5.2369 -    refined if needed.
  5.2370 -
  5.2371 -    To reconstruct counterexamples, the operation @{const partial_term_of} transforms
  5.2372 -    \<open>narrowing\<close>'s deep representation of terms to the type @{typ Code_Evaluation.term}.
  5.2373 -    The deep representation models symbolic variables as
  5.2374 -    @{const Quickcheck_Narrowing.Narrowing_variable}, which are normally converted to
  5.2375 -    @{const Code_Evaluation.Free}, and refined values as
  5.2376 -    @{term "Quickcheck_Narrowing.Narrowing_constructor i args"}, where @{term "i :: integer"}
  5.2377 -    denotes the index in the sum of refinements. In the above example for lists,
  5.2378 -    @{term "0"} corresponds to @{term "[]"} and @{term "1"}
  5.2379 +    If a symbolic variable of type @{typ "_ list"} is evaluated, it is
  5.2380 +    replaced by (i)~the empty list @{term "[]"} and (ii)~by a non-empty list
  5.2381 +    whose head and tail can then be recursively refined if needed.
  5.2382 +
  5.2383 +    To reconstruct counterexamples, the operation @{const partial_term_of}
  5.2384 +    transforms \<open>narrowing\<close>'s deep representation of terms to the type @{typ
  5.2385 +    Code_Evaluation.term}. The deep representation models symbolic variables
  5.2386 +    as @{const Quickcheck_Narrowing.Narrowing_variable}, which are normally
  5.2387 +    converted to @{const Code_Evaluation.Free}, and refined values as @{term
  5.2388 +    "Quickcheck_Narrowing.Narrowing_constructor i args"}, where @{term "i ::
  5.2389 +    integer"} denotes the index in the sum of refinements. In the above
  5.2390 +    example for lists, @{term "0"} corresponds to @{term "[]"} and @{term "1"}
  5.2391      to @{term "op #"}.
  5.2392  
  5.2393 -    The command @{command (HOL) "code_datatype"} sets up @{const partial_term_of}
  5.2394 -    such that the @{term "i"}-th refinement is interpreted as the @{term "i"}-th constructor,
  5.2395 -    but it does not ensures consistency with @{const narrowing}.
  5.2396 -
  5.2397 -  \<^descr> @{command (HOL) "quickcheck_params"} changes @{command (HOL)
  5.2398 -  "quickcheck"} configuration options persistently.
  5.2399 -
  5.2400 -  \<^descr> @{command (HOL) "quickcheck_generator"} creates random and
  5.2401 -  exhaustive value generators for a given type and operations.  It
  5.2402 -  generates values by using the operations as if they were
  5.2403 -  constructors of that type.
  5.2404 -
  5.2405 -  \<^descr> @{command (HOL) "nitpick"} tests the current goal for
  5.2406 -  counterexamples using a reduction to first-order relational
  5.2407 -  logic. See the Nitpick manual @{cite "isabelle-nitpick"} for details.
  5.2408 -
  5.2409 -  \<^descr> @{command (HOL) "nitpick_params"} changes @{command (HOL)
  5.2410 -  "nitpick"} configuration options persistently.
  5.2411 +    The command @{command (HOL) "code_datatype"} sets up @{const
  5.2412 +    partial_term_of} such that the @{term "i"}-th refinement is interpreted as
  5.2413 +    the @{term "i"}-th constructor, but it does not ensures consistency with
  5.2414 +    @{const narrowing}.
  5.2415 +
  5.2416 +  \<^descr> @{command (HOL) "quickcheck_params"} changes @{command (HOL) "quickcheck"}
  5.2417 +  configuration options persistently.
  5.2418 +
  5.2419 +  \<^descr> @{command (HOL) "quickcheck_generator"} creates random and exhaustive
  5.2420 +  value generators for a given type and operations. It generates values by
  5.2421 +  using the operations as if they were constructors of that type.
  5.2422 +
  5.2423 +  \<^descr> @{command (HOL) "nitpick"} tests the current goal for counterexamples
  5.2424 +  using a reduction to first-order relational logic. See the Nitpick manual
  5.2425 +  @{cite "isabelle-nitpick"} for details.
  5.2426 +
  5.2427 +  \<^descr> @{command (HOL) "nitpick_params"} changes @{command (HOL) "nitpick"}
  5.2428 +  configuration options persistently.
  5.2429  
  5.2430    \<^descr> @{command (HOL) "find_unused_assms"} finds potentially superfluous
  5.2431 -  assumptions in theorems using quickcheck.
  5.2432 -  It takes the theory name to be checked for superfluous assumptions as
  5.2433 -  optional argument. If not provided, it checks the current theory.
  5.2434 -  Options to the internal quickcheck invocations can be changed with
  5.2435 -  common configuration declarations.
  5.2436 +  assumptions in theorems using quickcheck. It takes the theory name to be
  5.2437 +  checked for superfluous assumptions as optional argument. If not provided,
  5.2438 +  it checks the current theory. Options to the internal quickcheck invocations
  5.2439 +  can be changed with common configuration declarations.
  5.2440  \<close>
  5.2441  
  5.2442  
  5.2443 @@ -2013,10 +1959,9 @@
  5.2444      @{attribute_def (HOL) coercion_args} & : & \<open>attribute\<close> \\
  5.2445    \end{matharray}
  5.2446  
  5.2447 -  Coercive subtyping allows the user to omit explicit type
  5.2448 -  conversions, also called \<^emph>\<open>coercions\<close>.  Type inference will add
  5.2449 -  them as necessary when parsing a term. See
  5.2450 -  @{cite "traytel-berghofer-nipkow-2011"} for details.
  5.2451 +  Coercive subtyping allows the user to omit explicit type conversions, also
  5.2452 +  called \<^emph>\<open>coercions\<close>. Type inference will add them as necessary when parsing
  5.2453 +  a term. See @{cite "traytel-berghofer-nipkow-2011"} for details.
  5.2454  
  5.2455    @{rail \<open>
  5.2456      @@{attribute (HOL) coercion} (@{syntax term})
  5.2457 @@ -2028,48 +1973,44 @@
  5.2458      @@{attribute (HOL) coercion_args} (@{syntax const}) (('+' | '0' | '-')+)
  5.2459    \<close>}
  5.2460  
  5.2461 -  \<^descr> @{attribute (HOL) "coercion"}~\<open>f\<close> registers a new
  5.2462 -  coercion function \<open>f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2\<close> where \<open>\<sigma>\<^sub>1\<close> and
  5.2463 -  \<open>\<sigma>\<^sub>2\<close> are type constructors without arguments.  Coercions are
  5.2464 -  composed by the inference algorithm if needed.  Note that the type
  5.2465 -  inference algorithm is complete only if the registered coercions
  5.2466 -  form a lattice.
  5.2467 -
  5.2468 -  \<^descr> @{attribute (HOL) "coercion_delete"}~\<open>f\<close> deletes a
  5.2469 -  preceding declaration (using @{attribute (HOL) "coercion"}) of the
  5.2470 -  function \<open>f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2\<close> as a coercion.
  5.2471 -
  5.2472 -  \<^descr> @{attribute (HOL) "coercion_map"}~\<open>map\<close> registers a
  5.2473 -  new map function to lift coercions through type constructors. The
  5.2474 -  function \<open>map\<close> must conform to the following type pattern
  5.2475 +  \<^descr> @{attribute (HOL) "coercion"}~\<open>f\<close> registers a new coercion function \<open>f ::
  5.2476 +  \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2\<close> where \<open>\<sigma>\<^sub>1\<close> and \<open>\<sigma>\<^sub>2\<close> are type constructors without arguments.
  5.2477 +  Coercions are composed by the inference algorithm if needed. Note that the
  5.2478 +  type inference algorithm is complete only if the registered coercions form a
  5.2479 +  lattice.
  5.2480 +
  5.2481 +  \<^descr> @{attribute (HOL) "coercion_delete"}~\<open>f\<close> deletes a preceding declaration
  5.2482 +  (using @{attribute (HOL) "coercion"}) of the function \<open>f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2\<close> as a
  5.2483 +  coercion.
  5.2484 +
  5.2485 +  \<^descr> @{attribute (HOL) "coercion_map"}~\<open>map\<close> registers a new map function to
  5.2486 +  lift coercions through type constructors. The function \<open>map\<close> must conform to
  5.2487 +  the following type pattern
  5.2488  
  5.2489    \begin{matharray}{lll}
  5.2490      \<open>map\<close> & \<open>::\<close> &
  5.2491        \<open>f\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> f\<^sub>n \<Rightarrow> (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Rightarrow> (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t\<close> \\
  5.2492    \end{matharray}
  5.2493  
  5.2494 -  where \<open>t\<close> is a type constructor and \<open>f\<^sub>i\<close> is of type
  5.2495 -  \<open>\<alpha>\<^sub>i \<Rightarrow> \<beta>\<^sub>i\<close> or \<open>\<beta>\<^sub>i \<Rightarrow> \<alpha>\<^sub>i\<close>.  Registering a map function
  5.2496 -  overwrites any existing map function for this particular type
  5.2497 -  constructor.
  5.2498 -
  5.2499 -  \<^descr> @{attribute (HOL) "coercion_args"} can be used to disallow
  5.2500 -  coercions to be inserted in certain positions in a term. For example,
  5.2501 -  given the constant \<open>c :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2 \<Rightarrow> \<sigma>\<^sub>3 \<Rightarrow> \<sigma>\<^sub>4\<close> and the list
  5.2502 -  of policies \<open>- + 0\<close> as arguments, coercions will not be
  5.2503 -  inserted in the first argument of \<open>c\<close> (policy \<open>-\<close>);
  5.2504 -  they may be inserted in the second argument (policy \<open>+\<close>)
  5.2505 -  even if the constant \<open>c\<close> itself is in a position where
  5.2506 -  coercions are disallowed; the third argument inherits the allowance
  5.2507 -  of coercsion insertion from the position of the constant \<open>c\<close>
  5.2508 -  (policy \<open>0\<close>). The standard usage of policies is the definition
  5.2509 -  of syntatic constructs (usually extralogical, i.e., processed and
  5.2510 -  stripped during type inference), that should not be destroyed by the
  5.2511 -  insertion of coercions (see, for example, the setup for the case syntax
  5.2512 -  in @{theory Ctr_Sugar}). 
  5.2513 -
  5.2514 -  \<^descr> @{attribute (HOL) "coercion_enabled"} enables the coercion
  5.2515 -  inference algorithm.
  5.2516 +  where \<open>t\<close> is a type constructor and \<open>f\<^sub>i\<close> is of type \<open>\<alpha>\<^sub>i \<Rightarrow> \<beta>\<^sub>i\<close> or \<open>\<beta>\<^sub>i \<Rightarrow>
  5.2517 +  \<alpha>\<^sub>i\<close>. Registering a map function overwrites any existing map function for
  5.2518 +  this particular type constructor.
  5.2519 +
  5.2520 +  \<^descr> @{attribute (HOL) "coercion_args"} can be used to disallow coercions to be
  5.2521 +  inserted in certain positions in a term. For example, given the constant \<open>c
  5.2522 +  :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2 \<Rightarrow> \<sigma>\<^sub>3 \<Rightarrow> \<sigma>\<^sub>4\<close> and the list of policies \<open>- + 0\<close> as arguments,
  5.2523 +  coercions will not be inserted in the first argument of \<open>c\<close> (policy \<open>-\<close>);
  5.2524 +  they may be inserted in the second argument (policy \<open>+\<close>) even if the
  5.2525 +  constant \<open>c\<close> itself is in a position where coercions are disallowed; the
  5.2526 +  third argument inherits the allowance of coercsion insertion from the
  5.2527 +  position of the constant \<open>c\<close> (policy \<open>0\<close>). The standard usage of policies is
  5.2528 +  the definition of syntatic constructs (usually extralogical, i.e., processed
  5.2529 +  and stripped during type inference), that should not be destroyed by the
  5.2530 +  insertion of coercions (see, for example, the setup for the case syntax in
  5.2531 +  @{theory Ctr_Sugar}).
  5.2532 +
  5.2533 +  \<^descr> @{attribute (HOL) "coercion_enabled"} enables the coercion inference
  5.2534 +  algorithm.
  5.2535  \<close>
  5.2536  
  5.2537  
  5.2538 @@ -2082,19 +2023,19 @@
  5.2539      @{attribute_def (HOL) arith_split} & : & \<open>attribute\<close> \\
  5.2540    \end{matharray}
  5.2541  
  5.2542 -  \<^descr> @{method (HOL) arith} decides linear arithmetic problems (on
  5.2543 -  types \<open>nat\<close>, \<open>int\<close>, \<open>real\<close>).  Any current facts
  5.2544 -  are inserted into the goal before running the procedure.
  5.2545 -
  5.2546 -  \<^descr> @{attribute (HOL) arith} declares facts that are supplied to
  5.2547 -  the arithmetic provers implicitly.
  5.2548 -
  5.2549 -  \<^descr> @{attribute (HOL) arith_split} attribute declares case split
  5.2550 -  rules to be expanded before @{method (HOL) arith} is invoked.
  5.2551 -
  5.2552 -
  5.2553 -  Note that a simpler (but faster) arithmetic prover is already
  5.2554 -  invoked by the Simplifier.
  5.2555 +  \<^descr> @{method (HOL) arith} decides linear arithmetic problems (on types \<open>nat\<close>,
  5.2556 +  \<open>int\<close>, \<open>real\<close>). Any current facts are inserted into the goal before running
  5.2557 +  the procedure.
  5.2558 +
  5.2559 +  \<^descr> @{attribute (HOL) arith} declares facts that are supplied to the
  5.2560 +  arithmetic provers implicitly.
  5.2561 +
  5.2562 +  \<^descr> @{attribute (HOL) arith_split} attribute declares case split rules to be
  5.2563 +  expanded before @{method (HOL) arith} is invoked.
  5.2564 +
  5.2565 +
  5.2566 +  Note that a simpler (but faster) arithmetic prover is already invoked by the
  5.2567 +  Simplifier.
  5.2568  \<close>
  5.2569  
  5.2570  
  5.2571 @@ -2109,19 +2050,18 @@
  5.2572      @@{method (HOL) iprover} (@{syntax rulemod} *)
  5.2573    \<close>}
  5.2574  
  5.2575 -  \<^descr> @{method (HOL) iprover} performs intuitionistic proof search,
  5.2576 -  depending on specifically declared rules from the context, or given
  5.2577 -  as explicit arguments.  Chained facts are inserted into the goal
  5.2578 -  before commencing proof search.
  5.2579 -
  5.2580 -  Rules need to be classified as @{attribute (Pure) intro},
  5.2581 -  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
  5.2582 -  ``\<open>!\<close>'' indicator refers to ``safe'' rules, which may be
  5.2583 -  applied aggressively (without considering back-tracking later).
  5.2584 -  Rules declared with ``\<open>?\<close>'' are ignored in proof search (the
  5.2585 -  single-step @{method (Pure) rule} method still observes these).  An
  5.2586 -  explicit weight annotation may be given as well; otherwise the
  5.2587 -  number of rule premises will be taken into account here.
  5.2588 +  \<^descr> @{method (HOL) iprover} performs intuitionistic proof search, depending on
  5.2589 +  specifically declared rules from the context, or given as explicit
  5.2590 +  arguments. Chained facts are inserted into the goal before commencing proof
  5.2591 +  search.
  5.2592 +
  5.2593 +  Rules need to be classified as @{attribute (Pure) intro}, @{attribute (Pure)
  5.2594 +  elim}, or @{attribute (Pure) dest}; here the ``\<open>!\<close>'' indicator refers to
  5.2595 +  ``safe'' rules, which may be applied aggressively (without considering
  5.2596 +  back-tracking later). Rules declared with ``\<open>?\<close>'' are ignored in proof
  5.2597 +  search (the single-step @{method (Pure) rule} method still observes these).
  5.2598 +  An explicit weight annotation may be given as well; otherwise the number of
  5.2599 +  rule premises will be taken into account here.
  5.2600  \<close>
  5.2601  
  5.2602  
  5.2603 @@ -2141,16 +2081,16 @@
  5.2604        @{syntax thms}?
  5.2605    \<close>}
  5.2606  
  5.2607 -  \<^descr> @{method (HOL) meson} implements Loveland's model elimination
  5.2608 -  procedure @{cite "loveland-78"}.  See @{file
  5.2609 -  "~~/src/HOL/ex/Meson_Test.thy"} for examples.
  5.2610 +  \<^descr> @{method (HOL) meson} implements Loveland's model elimination procedure
  5.2611 +  @{cite "loveland-78"}. See @{file "~~/src/HOL/ex/Meson_Test.thy"} for
  5.2612 +  examples.
  5.2613  
  5.2614    \<^descr> @{method (HOL) metis} combines ordered resolution and ordered
  5.2615 -  paramodulation to find first-order (or mildly higher-order) proofs.
  5.2616 -  The first optional argument specifies a type encoding; see the
  5.2617 -  Sledgehammer manual @{cite "isabelle-sledgehammer"} for details.  The
  5.2618 -  directory @{file "~~/src/HOL/Metis_Examples"} contains several small
  5.2619 -  theories developed to a large extent using @{method (HOL) metis}.
  5.2620 +  paramodulation to find first-order (or mildly higher-order) proofs. The
  5.2621 +  first optional argument specifies a type encoding; see the Sledgehammer
  5.2622 +  manual @{cite "isabelle-sledgehammer"} for details. The directory @{file
  5.2623 +  "~~/src/HOL/Metis_Examples"} contains several small theories developed to a
  5.2624 +  large extent using @{method (HOL) metis}.
  5.2625  \<close>
  5.2626  
  5.2627  
  5.2628 @@ -2170,23 +2110,21 @@
  5.2629      @@{attribute (HOL) algebra} (() | 'add' | 'del')
  5.2630    \<close>}
  5.2631  
  5.2632 -  \<^descr> @{method (HOL) algebra} performs algebraic reasoning via
  5.2633 -  Gr\"obner bases, see also @{cite "Chaieb-Wenzel:2007"} and
  5.2634 -  @{cite \<open>\S3.2\<close> "Chaieb-thesis"}. The method handles deals with two main
  5.2635 -  classes of problems:
  5.2636 +  \<^descr> @{method (HOL) algebra} performs algebraic reasoning via Gr\"obner bases,
  5.2637 +  see also @{cite "Chaieb-Wenzel:2007"} and @{cite \<open>\S3.2\<close> "Chaieb-thesis"}.
  5.2638 +  The method handles deals with two main classes of problems:
  5.2639  
  5.2640      \<^enum> Universal problems over multivariate polynomials in a
  5.2641      (semi)-ring/field/idom; the capabilities of the method are augmented
  5.2642 -    according to properties of these structures. For this problem class
  5.2643 -    the method is only complete for algebraically closed fields, since
  5.2644 -    the underlying method is based on Hilbert's Nullstellensatz, where
  5.2645 -    the equivalence only holds for algebraically closed fields.
  5.2646 -
  5.2647 -    The problems can contain equations \<open>p = 0\<close> or inequations
  5.2648 -    \<open>q \<noteq> 0\<close> anywhere within a universal problem statement.
  5.2649 -
  5.2650 -    \<^enum> All-exists problems of the following restricted (but useful)
  5.2651 -    form:
  5.2652 +    according to properties of these structures. For this problem class the
  5.2653 +    method is only complete for algebraically closed fields, since the
  5.2654 +    underlying method is based on Hilbert's Nullstellensatz, where the
  5.2655 +    equivalence only holds for algebraically closed fields.
  5.2656 +
  5.2657 +    The problems can contain equations \<open>p = 0\<close> or inequations \<open>q \<noteq> 0\<close> anywhere
  5.2658 +    within a universal problem statement.
  5.2659 +
  5.2660 +    \<^enum> All-exists problems of the following restricted (but useful) form:
  5.2661  
  5.2662      @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.
  5.2663        e\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<and> \<dots> \<and> e\<^sub>m(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<longrightarrow>
  5.2664 @@ -2195,23 +2133,25 @@
  5.2665          \<dots> \<and>
  5.2666          p\<^sub>t\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>t\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0)"}
  5.2667  
  5.2668 -    Here \<open>e\<^sub>1, \<dots>, e\<^sub>n\<close> and the \<open>p\<^sub>i\<^sub>j\<close> are multivariate
  5.2669 -    polynomials only in the variables mentioned as arguments.
  5.2670 -
  5.2671 -  The proof method is preceded by a simplification step, which may be
  5.2672 -  modified by using the form \<open>(algebra add: ths\<^sub>1 del: ths\<^sub>2)\<close>.
  5.2673 -  This acts like declarations for the Simplifier
  5.2674 -  (\secref{sec:simplifier}) on a private simpset for this tool.
  5.2675 -
  5.2676 -  \<^descr> @{attribute algebra} (as attribute) manages the default
  5.2677 -  collection of pre-simplification rules of the above proof method.
  5.2678 +    Here \<open>e\<^sub>1, \<dots>, e\<^sub>n\<close> and the \<open>p\<^sub>i\<^sub>j\<close> are multivariate polynomials only in
  5.2679 +    the variables mentioned as arguments.
  5.2680 +
  5.2681 +  The proof method is preceded by a simplification step, which may be modified
  5.2682 +  by using the form \<open>(algebra add: ths\<^sub>1 del: ths\<^sub>2)\<close>. This acts like
  5.2683 +  declarations for the Simplifier (\secref{sec:simplifier}) on a private
  5.2684 +  simpset for this tool.
  5.2685 +
  5.2686 +  \<^descr> @{attribute algebra} (as attribute) manages the default collection of
  5.2687 +  pre-simplification rules of the above proof method.
  5.2688  \<close>
  5.2689  
  5.2690  
  5.2691  subsubsection \<open>Example\<close>
  5.2692  
  5.2693 -text \<open>The subsequent example is from geometry: collinearity is
  5.2694 -  invariant by rotation.\<close>
  5.2695 +text \<open>
  5.2696 +  The subsequent example is from geometry: collinearity is invariant by
  5.2697 +  rotation.
  5.2698 +\<close>
  5.2699  
  5.2700  (*<*)experiment begin(*>*)
  5.2701  type_synonym point = "int \<times> int"
  5.2702 @@ -2243,19 +2183,19 @@
  5.2703      @@{method (HOL) coherent} @{syntax thms}?
  5.2704    \<close>}
  5.2705  
  5.2706 -  \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent
  5.2707 -  Logic\<close> @{cite "Bezem-Coquand:2005"}, which covers applications in
  5.2708 -  confluence theory, lattice theory and projective geometry.  See
  5.2709 -  @{file "~~/src/HOL/ex/Coherent.thy"} for some examples.
  5.2710 +  \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> @{cite
  5.2711 +  "Bezem-Coquand:2005"}, which covers applications in confluence theory,
  5.2712 +  lattice theory and projective geometry. See @{file
  5.2713 +  "~~/src/HOL/ex/Coherent.thy"} for some examples.
  5.2714  \<close>
  5.2715  
  5.2716  
  5.2717  section \<open>Unstructured case analysis and induction \label{sec:hol-induct-tac}\<close>
  5.2718  
  5.2719  text \<open>
  5.2720 -  The following tools of Isabelle/HOL support cases analysis and
  5.2721 -  induction in unstructured tactic scripts; see also
  5.2722 -  \secref{sec:cases-induct} for proper Isar versions of similar ideas.
  5.2723 +  The following tools of Isabelle/HOL support cases analysis and induction in
  5.2724 +  unstructured tactic scripts; see also \secref{sec:cases-induct} for proper
  5.2725 +  Isar versions of similar ideas.
  5.2726  
  5.2727    \begin{matharray}{rcl}
  5.2728      @{method_def (HOL) case_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
  5.2729 @@ -2276,31 +2216,29 @@
  5.2730      rule: 'rule' ':' @{syntax thm}
  5.2731    \<close>}
  5.2732  
  5.2733 -  \<^descr> @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit
  5.2734 -  to reason about inductive types.  Rules are selected according to
  5.2735 -  the declarations by the @{attribute cases} and @{attribute induct}
  5.2736 -  attributes, cf.\ \secref{sec:cases-induct}.  The @{command (HOL)
  5.2737 -  datatype} package already takes care of this.
  5.2738 +  \<^descr> @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit to reason
  5.2739 +  about inductive types. Rules are selected according to the declarations by
  5.2740 +  the @{attribute cases} and @{attribute induct} attributes, cf.\
  5.2741 +  \secref{sec:cases-induct}. The @{command (HOL) datatype} package already
  5.2742 +  takes care of this.
  5.2743  
  5.2744    These unstructured tactics feature both goal addressing and dynamic
  5.2745 -  instantiation.  Note that named rule cases are \<^emph>\<open>not\<close> provided
  5.2746 -  as would be by the proper @{method cases} and @{method induct} proof
  5.2747 -  methods (see \secref{sec:cases-induct}).  Unlike the @{method
  5.2748 -  induct} method, @{method induct_tac} does not handle structured rule
  5.2749 -  statements, only the compact object-logic conclusion of the subgoal
  5.2750 -  being addressed.
  5.2751 -
  5.2752 -  \<^descr> @{method (HOL) ind_cases} and @{command (HOL)
  5.2753 -  "inductive_cases"} provide an interface to the internal @{ML_text
  5.2754 -  mk_cases} operation.  Rules are simplified in an unrestricted
  5.2755 -  forward manner.
  5.2756 -
  5.2757 -  While @{method (HOL) ind_cases} is a proof method to apply the
  5.2758 -  result immediately as elimination rules, @{command (HOL)
  5.2759 -  "inductive_cases"} provides case split theorems at the theory level
  5.2760 -  for later use.  The @{keyword "for"} argument of the @{method (HOL)
  5.2761 -  ind_cases} method allows to specify a list of variables that should
  5.2762 -  be generalized before applying the resulting rule.
  5.2763 +  instantiation. Note that named rule cases are \<^emph>\<open>not\<close> provided as would be by
  5.2764 +  the proper @{method cases} and @{method induct} proof methods (see
  5.2765 +  \secref{sec:cases-induct}). Unlike the @{method induct} method, @{method
  5.2766 +  induct_tac} does not handle structured rule statements, only the compact
  5.2767 +  object-logic conclusion of the subgoal being addressed.
  5.2768 +
  5.2769 +  \<^descr> @{method (HOL) ind_cases} and @{command (HOL) "inductive_cases"} provide
  5.2770 +  an interface to the internal @{ML_text mk_cases} operation. Rules are
  5.2771 +  simplified in an unrestricted forward manner.
  5.2772 +
  5.2773 +  While @{method (HOL) ind_cases} is a proof method to apply the result
  5.2774 +  immediately as elimination rules, @{command (HOL) "inductive_cases"}
  5.2775 +  provides case split theorems at the theory level for later use. The
  5.2776 +  @{keyword "for"} argument of the @{method (HOL) ind_cases} method allows to
  5.2777 +  specify a list of variables that should be generalized before applying the
  5.2778 +  resulting rule.
  5.2779  \<close>
  5.2780  
  5.2781  
  5.2782 @@ -2315,9 +2253,9 @@
  5.2783      @@{attribute (HOL) split_format} ('(' 'complete' ')')?
  5.2784    \<close>}
  5.2785  
  5.2786 -  \<^descr> @{attribute (HOL) split_format}\ \<open>(complete)\<close> causes
  5.2787 -  arguments in function applications to be represented canonically
  5.2788 -  according to their tuple type structure.
  5.2789 +  \<^descr> @{attribute (HOL) split_format}\ \<open>(complete)\<close> causes arguments in function
  5.2790 +  applications to be represented canonically according to their tuple type
  5.2791 +  structure.
  5.2792  
  5.2793    Note that this operation tends to invent funny names for new local
  5.2794    parameters introduced.
  5.2795 @@ -2326,24 +2264,25 @@
  5.2796  
  5.2797  chapter \<open>Executable code\<close>
  5.2798  
  5.2799 -text \<open>For validation purposes, it is often useful to \<^emph>\<open>execute\<close>
  5.2800 -  specifications. In principle, execution could be simulated by Isabelle's
  5.2801 -  inference kernel, i.e. by a combination of resolution and simplification.
  5.2802 -  Unfortunately, this approach is rather inefficient. A more efficient way
  5.2803 -  of executing specifications is to translate them into a functional
  5.2804 -  programming language such as ML.
  5.2805 +text \<open>
  5.2806 +  For validation purposes, it is often useful to \<^emph>\<open>execute\<close> specifications. In
  5.2807 +  principle, execution could be simulated by Isabelle's inference kernel, i.e.
  5.2808 +  by a combination of resolution and simplification. Unfortunately, this
  5.2809 +  approach is rather inefficient. A more efficient way of executing
  5.2810 +  specifications is to translate them into a functional programming language
  5.2811 +  such as ML.
  5.2812  
  5.2813    Isabelle provides a generic framework to support code generation from
  5.2814    executable specifications. Isabelle/HOL instantiates these mechanisms in a
  5.2815    way that is amenable to end-user applications. Code can be generated for
  5.2816 -  functional programs (including overloading using type classes) targeting
  5.2817 -  SML @{cite SML}, OCaml @{cite OCaml}, Haskell @{cite
  5.2818 -  "haskell-revised-report"} and Scala @{cite "scala-overview-tech-report"}.
  5.2819 -  Conceptually, code generation is split up in three steps: \<^emph>\<open>selection\<close>
  5.2820 -  of code theorems, \<^emph>\<open>translation\<close> into an abstract executable view and
  5.2821 -  \<^emph>\<open>serialization\<close> to a specific \<^emph>\<open>target language\<close>. Inductive
  5.2822 -  specifications can be executed using the predicate compiler which operates
  5.2823 -  within HOL. See @{cite "isabelle-codegen"} for an introduction.
  5.2824 +  functional programs (including overloading using type classes) targeting SML
  5.2825 +  @{cite SML}, OCaml @{cite OCaml}, Haskell @{cite "haskell-revised-report"}
  5.2826 +  and Scala @{cite "scala-overview-tech-report"}. Conceptually, code
  5.2827 +  generation is split up in three steps: \<^emph>\<open>selection\<close> of code theorems,
  5.2828 +  \<^emph>\<open>translation\<close> into an abstract executable view and \<^emph>\<open>serialization\<close> to a
  5.2829 +  specific \<^emph>\<open>target language\<close>. Inductive specifications can be executed using
  5.2830 +  the predicate compiler which operates within HOL. See @{cite
  5.2831 +  "isabelle-codegen"} for an introduction.
  5.2832  
  5.2833    \begin{matharray}{rcl}
  5.2834      @{command_def (HOL) "export_code"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  5.2835 @@ -2456,22 +2395,20 @@
  5.2836    instruction is given, only abstract code is generated internally.
  5.2837  
  5.2838    Constants may be specified by giving them literally, referring to all
  5.2839 -  executable constants within a certain theory by giving \<open>name._\<close>,
  5.2840 -  or referring to \<^emph>\<open>all\<close> executable constants currently available by
  5.2841 -  giving \<open>_\<close>.
  5.2842 +  executable constants within a certain theory by giving \<open>name._\<close>, or
  5.2843 +  referring to \<^emph>\<open>all\<close> executable constants currently available by giving \<open>_\<close>.
  5.2844  
  5.2845    By default, exported identifiers are minimized per module. This can be
  5.2846    suppressed by prepending @{keyword "open"} before the list of constants.
  5.2847  
  5.2848 -  By default, for each involved theory one corresponding name space module
  5.2849 -  is generated. Alternatively, a module name may be specified after the
  5.2850 -  @{keyword "module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this
  5.2851 -  module.
  5.2852 -
  5.2853 -  For \<^emph>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification
  5.2854 -  refers to a single file; for \<^emph>\<open>Haskell\<close>, it refers to a whole
  5.2855 -  directory, where code is generated in multiple files reflecting the module
  5.2856 -  hierarchy. Omitting the file specification denotes standard output.
  5.2857 +  By default, for each involved theory one corresponding name space module is
  5.2858 +  generated. Alternatively, a module name may be specified after the @{keyword
  5.2859 +  "module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module.
  5.2860 +
  5.2861 +  For \<^emph>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification refers to a single
  5.2862 +  file; for \<^emph>\<open>Haskell\<close>, it refers to a whole directory, where code is
  5.2863 +  generated in multiple files reflecting the module hierarchy. Omitting the
  5.2864 +  file specification denotes standard output.
  5.2865  
  5.2866    Serializers take an optional list of arguments in parentheses. For
  5.2867    \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' argument;
  5.2868 @@ -2479,82 +2416,80 @@
  5.2869    appropriate datatype declaration.
  5.2870  
  5.2871    \<^descr> @{attribute (HOL) code} declare code equations for code generation.
  5.2872 -  Variant \<open>code equation\<close> declares a conventional equation as code
  5.2873 -  equation. Variants \<open>code abstype\<close> and \<open>code abstract\<close>
  5.2874 -  declare abstract datatype certificates or code equations on abstract
  5.2875 -  datatype representations respectively. Vanilla \<open>code\<close> falls back
  5.2876 -  to \<open>code equation\<close> or \<open>code abstype\<close> depending on the
  5.2877 -  syntactic shape of the underlying equation. Variant \<open>code del\<close>
  5.2878 -  deselects a code equation for code generation.
  5.2879 -
  5.2880 -  Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of
  5.2881 -  constant as arguments and drop all code equations declared for them. In
  5.2882 -  the case of {text abort}, these constants then are are not required to
  5.2883 -  have a definition by means of code equations; if needed these are
  5.2884 -  implemented by program abort (exception) instead.
  5.2885 +  Variant \<open>code equation\<close> declares a conventional equation as code equation.
  5.2886 +  Variants \<open>code abstype\<close> and \<open>code abstract\<close> declare abstract datatype
  5.2887 +  certificates or code equations on abstract datatype representations
  5.2888 +  respectively. Vanilla \<open>code\<close> falls back to \<open>code equation\<close> or \<open>code abstype\<close>
  5.2889 +  depending on the syntactic shape of the underlying equation. Variant \<open>code
  5.2890 +  del\<close> deselects a code equation for code generation.
  5.2891 +
  5.2892 +  Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constant as arguments
  5.2893 +  and drop all code equations declared for them. In the case of {text abort},
  5.2894 +  these constants then are are not required to have a definition by means of
  5.2895 +  code equations; if needed these are implemented by program abort (exception)
  5.2896 +  instead.
  5.2897  
  5.2898    Usually packages introducing code equations provide a reasonable default
  5.2899    setup for selection.
  5.2900  
  5.2901 -  \<^descr> @{command (HOL) "code_datatype"} specifies a constructor set for a
  5.2902 -  logical type.
  5.2903 -
  5.2904 -  \<^descr> @{command (HOL) "print_codesetup"} gives an overview on selected
  5.2905 -  code equations and code generator datatypes.
  5.2906 -
  5.2907 -  \<^descr> @{attribute (HOL) code_unfold} declares (or with option ``\<open>del\<close>'' removes) theorems which during preprocessing are applied as
  5.2908 -  rewrite rules to any code equation or evaluation input.
  5.2909 -
  5.2910 -  \<^descr> @{attribute (HOL) code_post} declares (or with option ``\<open>del\<close>'' removes) theorems which are applied as rewrite rules to any
  5.2911 -  result of an evaluation.
  5.2912 -
  5.2913 -  \<^descr> @{attribute (HOL) code_abbrev} declares (or with option ``\<open>del\<close>'' removes) equations which are applied as rewrite rules to any
  5.2914 -  result of an evaluation and symmetrically during preprocessing to any code
  5.2915 +  \<^descr> @{command (HOL) "code_datatype"} specifies a constructor set for a logical
  5.2916 +  type.
  5.2917 +
  5.2918 +  \<^descr> @{command (HOL) "print_codesetup"} gives an overview on selected code
  5.2919 +  equations and code generator datatypes.
  5.2920 +
  5.2921 +  \<^descr> @{attribute (HOL) code_unfold} declares (or with option ``\<open>del\<close>'' removes)
  5.2922 +  theorems which during preprocessing are applied as rewrite rules to any code
  5.2923    equation or evaluation input.
  5.2924  
  5.2925 -  \<^descr> @{command (HOL) "print_codeproc"} prints the setup of the code
  5.2926 -  generator preprocessor.
  5.2927 -
  5.2928 -  \<^descr> @{command (HOL) "code_thms"} prints a list of theorems representing
  5.2929 -  the corresponding program containing all given constants after
  5.2930 -  preprocessing.
  5.2931 +  \<^descr> @{attribute (HOL) code_post} declares (or with option ``\<open>del\<close>'' removes)
  5.2932 +  theorems which are applied as rewrite rules to any result of an evaluation.
  5.2933 +
  5.2934 +  \<^descr> @{attribute (HOL) code_abbrev} declares (or with option ``\<open>del\<close>'' removes)
  5.2935 +  equations which are applied as rewrite rules to any result of an evaluation
  5.2936 +  and symmetrically during preprocessing to any code equation or evaluation
  5.2937 +  input.
  5.2938 +
  5.2939 +  \<^descr> @{command (HOL) "print_codeproc"} prints the setup of the code generator
  5.2940 +  preprocessor.
  5.2941 +
  5.2942 +  \<^descr> @{command (HOL) "code_thms"} prints a list of theorems representing the
  5.2943 +  corresponding program containing all given constants after preprocessing.
  5.2944  
  5.2945    \<^descr> @{command (HOL) "code_deps"} visualizes dependencies of theorems
  5.2946 -  representing the corresponding program containing all given constants
  5.2947 -  after preprocessing.
  5.2948 -
  5.2949 -  \<^descr> @{command (HOL) "code_reserved"} declares a list of names as
  5.2950 -  reserved for a given target, preventing it to be shadowed by any generated
  5.2951 -  code.
  5.2952 +  representing the corresponding program containing all given constants after
  5.2953 +  preprocessing.
  5.2954 +
  5.2955 +  \<^descr> @{command (HOL) "code_reserved"} declares a list of names as reserved for
  5.2956 +  a given target, preventing it to be shadowed by any generated code.
  5.2957  
  5.2958    \<^descr> @{command (HOL) "code_printing"} associates a series of symbols
  5.2959    (constants, type constructors, classes, class relations, instances, module
  5.2960 -  names) with target-specific serializations; omitting a serialization
  5.2961 -  deletes an existing serialization.
  5.2962 -
  5.2963 -  \<^descr> @{command (HOL) "code_monad"} provides an auxiliary mechanism to
  5.2964 -  generate monadic code for Haskell.
  5.2965 +  names) with target-specific serializations; omitting a serialization deletes
  5.2966 +  an existing serialization.
  5.2967 +
  5.2968 +  \<^descr> @{command (HOL) "code_monad"} provides an auxiliary mechanism to generate
  5.2969 +  monadic code for Haskell.
  5.2970  
  5.2971    \<^descr> @{command (HOL) "code_identifier"} associates a a series of symbols
  5.2972    (constants, type constructors, classes, class relations, instances, module
  5.2973    names) with target-specific hints how these symbols shall be named. These
  5.2974    hints gain precedence over names for symbols with no hints at all.
  5.2975 -  Conflicting hints are subject to name disambiguation. \<^emph>\<open>Warning:\<close> It
  5.2976 -  is at the discretion of the user to ensure that name prefixes of
  5.2977 -  identifiers in compound statements like type classes or datatypes are
  5.2978 -  still the same.
  5.2979 -
  5.2980 -  \<^descr> @{command (HOL) "code_reflect"} without a ``\<open>file\<close>''
  5.2981 -  argument compiles code into the system runtime environment and modifies
  5.2982 -  the code generator setup that future invocations of system runtime code
  5.2983 -  generation referring to one of the ``\<open>datatypes\<close>'' or ``\<open>functions\<close>'' entities use these precompiled entities. With a ``\<open>file\<close>'' argument, the corresponding code is generated into that
  5.2984 -  specified file without modifying the code generator setup.
  5.2985 -
  5.2986 -  \<^descr> @{command (HOL) "code_pred"} creates code equations for a predicate
  5.2987 -  given a set of introduction rules. Optional mode annotations determine
  5.2988 -  which arguments are supposed to be input or output. If alternative
  5.2989 -  introduction rules are declared, one must prove a corresponding
  5.2990 -  elimination rule.
  5.2991 +  Conflicting hints are subject to name disambiguation. \<^emph>\<open>Warning:\<close> It is at
  5.2992 +  the discretion of the user to ensure that name prefixes of identifiers in
  5.2993 +  compound statements like type classes or datatypes are still the same.
  5.2994 +
  5.2995 +  \<^descr> @{command (HOL) "code_reflect"} without a ``\<open>file\<close>'' argument compiles
  5.2996 +  code into the system runtime environment and modifies the code generator
  5.2997 +  setup that future invocations of system runtime code generation referring to
  5.2998 +  one of the ``\<open>datatypes\<close>'' or ``\<open>functions\<close>'' entities use these precompiled
  5.2999 +  entities. With a ``\<open>file\<close>'' argument, the corresponding code is generated
  5.3000 +  into that specified file without modifying the code generator setup.
  5.3001 +
  5.3002 +  \<^descr> @{command (HOL) "code_pred"} creates code equations for a predicate given
  5.3003 +  a set of introduction rules. Optional mode annotations determine which
  5.3004 +  arguments are supposed to be input or output. If alternative introduction
  5.3005 +  rules are declared, one must prove a corresponding elimination rule.
  5.3006  \<close>
  5.3007  
  5.3008  end
     6.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jul 22 15:39:27 2016 +0200
     6.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jul 22 15:39:32 2016 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  (*:maxLineLen=78:*)
     6.5  
     6.6  theory Inner_Syntax
     6.7 -imports Base Main
     6.8 +  imports Main Base
     6.9  begin
    6.10  
    6.11  chapter \<open>Inner syntax --- the term language \label{ch:inner-syntax}\<close>
     7.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Jul 22 15:39:27 2016 +0200
     7.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Jul 22 15:39:32 2016 +0200
     7.3 @@ -1,7 +1,7 @@
     7.4  (*:maxLineLen=78:*)
     7.5  
     7.6  theory Outer_Syntax
     7.7 -imports Base Main
     7.8 +  imports Main Base
     7.9  begin
    7.10  
    7.11  chapter \<open>Outer syntax --- the theory language \label{ch:outer-syntax}\<close>
     8.1 --- a/src/Doc/Isar_Ref/Preface.thy	Fri Jul 22 15:39:27 2016 +0200
     8.2 +++ b/src/Doc/Isar_Ref/Preface.thy	Fri Jul 22 15:39:32 2016 +0200
     8.3 @@ -1,7 +1,7 @@
     8.4  (*:maxLineLen=78:*)
     8.5  
     8.6  theory Preface
     8.7 -imports Base Main
     8.8 +  imports Main Base
     8.9  begin
    8.10  
    8.11  text \<open>
     9.1 --- a/src/Doc/Isar_Ref/Proof.thy	Fri Jul 22 15:39:27 2016 +0200
     9.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Fri Jul 22 15:39:32 2016 +0200
     9.3 @@ -1,7 +1,7 @@
     9.4  (*:maxLineLen=78:*)
     9.5  
     9.6  theory Proof
     9.7 -imports Base Main
     9.8 +  imports Main Base
     9.9  begin
    9.10  
    9.11  chapter \<open>Proofs \label{ch:proofs}\<close>
    9.12 @@ -189,8 +189,8 @@
    9.13    "and"}; the resulting list of current facts consists of all of these
    9.14    concatenated.
    9.15  
    9.16 -  A structured assumption like \<^theory_text>\<open>assume "B x" and "A x" for x\<close> is equivalent
    9.17 -  to \<^theory_text>\<open>assume "\<And>x. A x \<Longrightarrow> B x"\<close>, but vacuous quantification is avoided: a
    9.18 +  A structured assumption like \<^theory_text>\<open>assume "B x" if "A x" for x\<close> is equivalent to
    9.19 +  \<^theory_text>\<open>assume "\<And>x. A x \<Longrightarrow> B x"\<close>, but vacuous quantification is avoided: a
    9.20    for-context only effects propositions according to actual use of variables.
    9.21  
    9.22    \<^descr> \<^theory_text>\<open>define x where "x = t"\<close> introduces a local (non-polymorphic) definition.
    9.23 @@ -283,6 +283,8 @@
    9.24      @{command_def "with"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
    9.25      @{command_def "using"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
    9.26      @{command_def "unfolding"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
    9.27 +    @{method_def "use"} & : & \<open>method\<close> \\
    9.28 +    @{fact_def "method_facts"} & : & \<open>fact\<close> \\
    9.29    \end{matharray}
    9.30  
    9.31    New facts are established either by assumption or proof of local statements.
    9.32 @@ -300,6 +302,8 @@
    9.33      ;
    9.34      (@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})
    9.35        (@{syntax thms} + @'and')
    9.36 +    ;
    9.37 +    @{method use} @{syntax thms} @'in' @{syntax method}
    9.38    \<close>}
    9.39  
    9.40    \<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>,
    9.41 @@ -323,14 +327,22 @@
    9.42    \<AND> this\<close>''; thus the forward chaining is from earlier facts together
    9.43    with the current ones.
    9.44  
    9.45 -  \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts being currently
    9.46 -  indicated for use by a subsequent refinement step (such as @{command_ref
    9.47 -  "apply"} or @{command_ref "proof"}).
    9.48 +  \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts to be used by a
    9.49 +  subsequent refinement step (such as @{command_ref "apply"} or @{command_ref
    9.50 +  "proof"}).
    9.51  
    9.52    \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally similar to @{command
    9.53 -  "using"}, but unfolds definitional equations \<open>b\<^sub>1, \<dots> b\<^sub>n\<close> throughout the
    9.54 +  "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the
    9.55    goal state and facts.
    9.56  
    9.57 +  \<^descr> \<^theory_text>\<open>(use b\<^sub>1 \<dots> b\<^sub>n in method)\<close> uses the facts in the given method
    9.58 +  expression. The facts provided by the proof state (via @{command "using"}
    9.59 +  etc.) are ignored, but it is possible to refer to @{fact method_facts}
    9.60 +  explicitly.
    9.61 +
    9.62 +  \<^descr> @{fact method_facts} is a dynamic fact that refers to the currently used
    9.63 +  facts of the goal state.
    9.64 +
    9.65  
    9.66    Forward chaining with an empty list of theorems is the same as not chaining
    9.67    at all. Thus ``@{command "from"}~\<open>nothing\<close>'' has no effect apart from
    10.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy	Fri Jul 22 15:39:27 2016 +0200
    10.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Fri Jul 22 15:39:32 2016 +0200
    10.3 @@ -1,7 +1,7 @@
    10.4  (*:maxLineLen=78:*)
    10.5  
    10.6  theory Proof_Script
    10.7 -imports Base Main
    10.8 +  imports Main Base
    10.9  begin
   10.10  
   10.11  chapter \<open>Proof scripts\<close>
    11.1 --- a/src/Doc/Isar_Ref/Quick_Reference.thy	Fri Jul 22 15:39:27 2016 +0200
    11.2 +++ b/src/Doc/Isar_Ref/Quick_Reference.thy	Fri Jul 22 15:39:32 2016 +0200
    11.3 @@ -1,7 +1,7 @@
    11.4  (*:maxLineLen=78:*)
    11.5  
    11.6  theory Quick_Reference
    11.7 -imports Base Main
    11.8 +  imports Main Base
    11.9  begin
   11.10  
   11.11  chapter \<open>Isabelle/Isar quick reference \label{ap:refcard}\<close>
    12.1 --- a/src/Doc/Isar_Ref/Spec.thy	Fri Jul 22 15:39:27 2016 +0200
    12.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Fri Jul 22 15:39:32 2016 +0200
    12.3 @@ -1,7 +1,7 @@
    12.4  (*:maxLineLen=78:*)
    12.5  
    12.6  theory Spec
    12.7 -imports Base Main
    12.8 +  imports Main Base
    12.9  begin
   12.10  
   12.11  chapter \<open>Specifications\<close>
    13.1 --- a/src/Doc/Isar_Ref/Symbols.thy	Fri Jul 22 15:39:27 2016 +0200
    13.2 +++ b/src/Doc/Isar_Ref/Symbols.thy	Fri Jul 22 15:39:32 2016 +0200
    13.3 @@ -1,7 +1,7 @@
    13.4  (*:maxLineLen=78:*)
    13.5  
    13.6  theory Symbols
    13.7 -imports Base Main
    13.8 +  imports Main Base
    13.9  begin
   13.10  
   13.11  chapter \<open>Predefined Isabelle symbols \label{app:symbols}\<close>
    14.1 --- a/src/Doc/Isar_Ref/Synopsis.thy	Fri Jul 22 15:39:27 2016 +0200
    14.2 +++ b/src/Doc/Isar_Ref/Synopsis.thy	Fri Jul 22 15:39:32 2016 +0200
    14.3 @@ -1,7 +1,7 @@
    14.4  (*:maxLineLen=78:*)
    14.5  
    14.6  theory Synopsis
    14.7 -imports Base Main
    14.8 +  imports Main Base
    14.9  begin
   14.10  
   14.11  chapter \<open>Synopsis\<close>
    15.1 --- a/src/HOL/Binomial.thy	Fri Jul 22 15:39:27 2016 +0200
    15.2 +++ b/src/HOL/Binomial.thy	Fri Jul 22 15:39:32 2016 +0200
    15.3 @@ -1424,18 +1424,6 @@
    15.4  lemma choose_one: "n choose 1 = n" for n :: nat
    15.5    by simp
    15.6  
    15.7 -(*FIXME: messy and apparently unused*)
    15.8 -lemma binomial_induct [rule_format]: "(\<forall>n::nat. P n n) \<longrightarrow>
    15.9 -    (\<forall>n. P (Suc n) 0) \<longrightarrow> (\<forall>n. (\<forall>k < n. P n k \<longrightarrow> P n (Suc k) \<longrightarrow>
   15.10 -    P (Suc n) (Suc k))) \<longrightarrow> (\<forall>k \<le> n. P n k)"
   15.11 -  apply (induct n)
   15.12 -  apply auto
   15.13 -  apply (case_tac "k = 0")
   15.14 -  apply auto
   15.15 -  apply (case_tac "k = Suc n")
   15.16 -  apply (auto simp add: le_Suc_eq elim: lessE)
   15.17 -  done
   15.18 -
   15.19  lemma card_UNION:
   15.20    assumes "finite A"
   15.21      and "\<forall>k \<in> A. finite k"
    16.1 --- a/src/HOL/Eisbach/Eisbach.thy	Fri Jul 22 15:39:27 2016 +0200
    16.2 +++ b/src/HOL/Eisbach/Eisbach.thy	Fri Jul 22 15:39:32 2016 +0200
    16.3 @@ -22,9 +22,4 @@
    16.4  
    16.5  method solves methods m = (m; fail)
    16.6  
    16.7 -method_setup use = \<open>
    16.8 -  Attrib.thms -- (Scan.lift @{keyword "in"} |-- Method_Closure.method_text) >>
    16.9 -    (fn (thms, text) => fn ctxt => fn _ => Method_Closure.method_evaluate text ctxt thms)
   16.10 -\<close> \<open>indicate method facts and context for method expression\<close>
   16.11 -
   16.12  end
    17.1 --- a/src/HOL/Eisbach/Eisbach_Tools.thy	Fri Jul 22 15:39:27 2016 +0200
    17.2 +++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Fri Jul 22 15:39:32 2016 +0200
    17.3 @@ -55,11 +55,11 @@
    17.4  \<close>
    17.5  
    17.6  method_setup catch = \<open>
    17.7 -  Method_Closure.method_text -- Method_Closure.method_text >>
    17.8 +  Method.text_closure -- Method.text_closure >>
    17.9      (fn (text, text') => fn ctxt => fn using => fn st =>
   17.10        let
   17.11 -        val method = Method_Closure.method_evaluate text ctxt using;
   17.12 -        val backup_results = Method_Closure.method_evaluate text' ctxt using st;
   17.13 +        val method = Method.evaluate_runtime text ctxt using;
   17.14 +        val backup_results = Method.evaluate_runtime text' ctxt using st;
   17.15        in
   17.16          (case try method st of
   17.17            SOME seq => try_map backup_results seq
    18.1 --- a/src/HOL/Eisbach/match_method.ML	Fri Jul 22 15:39:27 2016 +0200
    18.2 +++ b/src/HOL/Eisbach/match_method.ML	Fri Jul 22 15:39:32 2016 +0200
    18.3 @@ -100,7 +100,7 @@
    18.4      (case Token.get_value body of
    18.5        SOME (Token.Source src) =>
    18.6          let
    18.7 -          val text = Method_Closure.read ctxt src;
    18.8 +          val text = Method.read ctxt src;
    18.9            val ts' =
   18.10              map
   18.11                (fn (b, (Parse_Tools.Real_Val v, match_args)) =>
   18.12 @@ -201,7 +201,7 @@
   18.13              |> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev)
   18.14              ||> Proof_Context.restore_mode ctxt;
   18.15  
   18.16 -          val (text, src) = Method_Closure.read_closure_input ctxt6 (Token.input_of body);
   18.17 +          val (text, src) = Method.read_closure_input ctxt6 (Token.input_of body);
   18.18  
   18.19            val morphism =
   18.20              Variable.export_morphism ctxt6
   18.21 @@ -645,12 +645,12 @@
   18.22        Match_Fact net =>
   18.23          make_fact_matches goal_ctxt (Item_Net.retrieve net)
   18.24          |> Seq.map (fn (text, ctxt') =>
   18.25 -          Method_Closure.method_evaluate text ctxt' using (ctxt', st)
   18.26 +          Method.evaluate_runtime text ctxt' using (ctxt', st)
   18.27            |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm)))
   18.28      | Match_Term net =>
   18.29          make_term_matches goal_ctxt (Item_Net.retrieve net)
   18.30          |> Seq.map (fn (text, ctxt') =>
   18.31 -          Method_Closure.method_evaluate text ctxt' using (ctxt', st)
   18.32 +          Method.evaluate_runtime text ctxt' using (ctxt', st)
   18.33            |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm)))
   18.34      | match_kind =>
   18.35          if Thm.no_prems st then Seq.empty
   18.36 @@ -721,7 +721,7 @@
   18.37                end;
   18.38  
   18.39              fun apply_text (text, ctxt') =
   18.40 -                Method_Closure.method_evaluate text ctxt' using (ctxt', focused_goal)
   18.41 +                Method.evaluate_runtime text ctxt' using (ctxt', focused_goal)
   18.42                |> Seq.filter_results
   18.43                |> Seq.maps (Seq.DETERM do_retrofit)             
   18.44  
    19.1 --- a/src/HOL/Eisbach/method_closure.ML	Fri Jul 22 15:39:27 2016 +0200
    19.2 +++ b/src/HOL/Eisbach/method_closure.ML	Fri Jul 22 15:39:32 2016 +0200
    19.3 @@ -10,11 +10,6 @@
    19.4  
    19.5  signature METHOD_CLOSURE =
    19.6  sig
    19.7 -  val read: Proof.context -> Token.src -> Method.text
    19.8 -  val read_closure: Proof.context -> Token.src -> Method.text * Token.src
    19.9 -  val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src
   19.10 -  val method_text: Method.text context_parser
   19.11 -  val method_evaluate: Method.text -> Proof.context -> Method.method
   19.12    val apply_method: Proof.context -> string -> term list -> thm list list ->
   19.13      (Proof.context -> Method.method) list -> Proof.context -> thm list -> context_tactic
   19.14    val method: binding -> (binding * typ option * mixfix) list -> binding list ->
   19.15 @@ -82,51 +77,7 @@
   19.16    end;
   19.17  
   19.18  
   19.19 -(* read method text *)
   19.20 -
   19.21 -fun read ctxt src =
   19.22 -  (case Scan.read Token.stopper (Parse.!!! (Method.parser 0 --| Scan.ahead Parse.eof)) src of
   19.23 -    SOME (text, range) =>
   19.24 -      if Method.checked_text text then text
   19.25 -      else (Method.report (text, range); Method.check_text ctxt text)
   19.26 -  | NONE => error ("Failed to parse method" ^ Position.here (#1 (Token.range_of src))));
   19.27 -
   19.28 -fun read_closure ctxt src0 =
   19.29 -  let
   19.30 -    val src1 = map Token.init_assignable src0;
   19.31 -    val text = read ctxt src1 |> Method.map_source (Method.method_closure ctxt);
   19.32 -    val src2 = map Token.closure src1;
   19.33 -  in (text, src2) end;
   19.34 -
   19.35 -fun read_closure_input ctxt =
   19.36 -  Input.source_explode #>
   19.37 -  Token.read_no_commands (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof) #>
   19.38 -  read_closure ctxt;
   19.39 -
   19.40 -val method_text =
   19.41 -  Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
   19.42 -    (case Token.get_value tok of
   19.43 -      SOME (Token.Source src) => read ctxt src
   19.44 -    | _ =>
   19.45 -        let
   19.46 -          val (text, src) = read_closure_input ctxt (Token.input_of tok);
   19.47 -          val _ = Token.assign (SOME (Token.Source src)) tok;
   19.48 -        in text end));
   19.49 -
   19.50 -
   19.51 -(* evaluate method text *)
   19.52 -
   19.53 -fun method_evaluate text ctxt =
   19.54 -  let
   19.55 -    val text' =
   19.56 -      text |> (Method.map_source o map o Token.map_facts)
   19.57 -        (fn SOME name =>
   19.58 -              (case Proof_Context.lookup_fact ctxt name of
   19.59 -                SOME {dynamic = true, thms} => K thms
   19.60 -              | _ => I)
   19.61 -          | NONE => I);
   19.62 -    val ctxt' = Config.put Method.closure false ctxt;
   19.63 -  in fn facts => Method.RUNTIME (fn st => Method.evaluate text' ctxt' facts st) end;
   19.64 +(* instantiate and evaluate method text *)
   19.65  
   19.66  fun method_instantiate vars body ts ctxt =
   19.67    let
   19.68 @@ -134,7 +85,7 @@
   19.69      val subst = fold (Pattern.match thy) (vars ~~ ts) (Vartab.empty, Vartab.empty);
   19.70      val morphism = Morphism.term_morphism "method_instantiate" (Envir.subst_term subst);
   19.71      val body' = (Method.map_source o map) (Token.transform morphism) body;
   19.72 -  in method_evaluate body' ctxt end;
   19.73 +  in Method.evaluate_runtime body' ctxt end;
   19.74  
   19.75  
   19.76  
   19.77 @@ -215,12 +166,12 @@
   19.78    let
   19.79      fun bind_method (name, text) ctxt =
   19.80        let
   19.81 -        val method = method_evaluate text;
   19.82 +        val method = Method.evaluate_runtime text;
   19.83          val inner_update = method o update_dynamic_method (name, K (method ctxt));
   19.84        in update_dynamic_method (name, inner_update) ctxt end;
   19.85  
   19.86      fun rep [] x = Scan.succeed [] x
   19.87 -      | rep (m :: ms) x = ((method_text >> pair m) ::: rep ms) x;
   19.88 +      | rep (m :: ms) x = ((Method.text_closure >> pair m) ::: rep ms) x;
   19.89    in rep method_args >> fold bind_method end;
   19.90  
   19.91  fun gen_method add_fixes name vars uses declares methods source lthy =
   19.92 @@ -256,7 +207,7 @@
   19.93        |> put_recursive_method (full_name, fn _ => fn _ => Method.fail);
   19.94  
   19.95      val (text, src) =
   19.96 -      read_closure (Config.put Proof_Context.dynamic_facts_dummy true lthy3) source;
   19.97 +      Method.read_closure (Config.put Proof_Context.dynamic_facts_dummy true lthy3) source;
   19.98  
   19.99      val morphism =
  19.100        Variable.export_morphism lthy3
  19.101 @@ -273,7 +224,7 @@
  19.102      |> Proof_Context.restore_naming lthy
  19.103      |> put_closure name
  19.104          {vars = term_args', named_thms = named_thms, methods = method_args, body = text'}
  19.105 -    |> Method.local_setup name 
  19.106 +    |> Method.local_setup name
  19.107          (Args.context :|-- (fn ctxt =>
  19.108            let val {body, vars, ...} = get_closure ctxt full_name in
  19.109              parser vars (recursive_method full_name vars body) end)) ""
    20.1 --- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Fri Jul 22 15:39:27 2016 +0200
    20.2 +++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Fri Jul 22 15:39:32 2016 +0200
    20.3 @@ -82,7 +82,7 @@
    20.4    assumes "\<bottom>"
    20.5    shows A
    20.6  proof -
    20.7 -  from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def .
    20.8 +  from \<open>\<bottom>\<close> have "\<forall>A. A" by (simp only: false_def)
    20.9    then show A ..
   20.10  qed
   20.11  
   20.12 @@ -108,7 +108,7 @@
   20.13    assumes "\<not> A" and A
   20.14    shows B
   20.15  proof -
   20.16 -  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
   20.17 +  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" by (simp only: not_def)
   20.18    from this and \<open>A\<close> have "\<bottom>" ..
   20.19    then show B ..
   20.20  qed
    21.1 --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Jul 22 15:39:27 2016 +0200
    21.2 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Jul 22 15:39:32 2016 +0200
    21.3 @@ -7,8 +7,8 @@
    21.4  theory Adhoc_Overloading_Examples
    21.5  imports
    21.6    Main
    21.7 +  "~~/src/HOL/Library/Infinite_Set"
    21.8    "~~/src/Tools/Adhoc_Overloading"
    21.9 -  "~~/src/HOL/Library/Infinite_Set"
   21.10  begin
   21.11  
   21.12  text \<open>Adhoc overloading allows to overload a constant depending on
    22.1 --- a/src/Pure/General/symbol.scala	Fri Jul 22 15:39:27 2016 +0200
    22.2 +++ b/src/Pure/General/symbol.scala	Fri Jul 22 15:39:32 2016 +0200
    22.3 @@ -458,8 +458,9 @@
    22.4      val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
    22.5  
    22.6  
    22.7 -    /* comment */
    22.8 +    /* misc symbols */
    22.9  
   22.10 +    val newline_decoded = decode(newline)
   22.11      val comment_decoded = decode(comment)
   22.12  
   22.13  
   22.14 @@ -526,7 +527,15 @@
   22.15    def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
   22.16  
   22.17  
   22.18 -  /* comment */
   22.19 +  /* misc symbols */
   22.20 +
   22.21 +  val newline: Symbol = "\\<newline>"
   22.22 +  def newline_decoded: Symbol = symbols.newline_decoded
   22.23 +
   22.24 +  def print_newlines(str: String): String =
   22.25 +    if (str.contains('\n'))
   22.26 +      (for (s <- iterator(str)) yield { if (s == "\n") newline_decoded else s }).mkString
   22.27 +    else str
   22.28  
   22.29    val comment: Symbol = "\\<comment>"
   22.30    def comment_decoded: Symbol = symbols.comment_decoded
    23.1 --- a/src/Pure/Isar/method.ML	Fri Jul 22 15:39:27 2016 +0200
    23.2 +++ b/src/Pure/Isar/method.ML	Fri Jul 22 15:39:32 2016 +0200
    23.3 @@ -92,6 +92,7 @@
    23.4    val RUNTIME: context_tactic -> context_tactic
    23.5    val sleep: Time.time -> context_tactic
    23.6    val evaluate: text -> Proof.context -> method
    23.7 +  val evaluate_runtime: text -> Proof.context -> method
    23.8    type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
    23.9    val modifier: attribute -> Position.T -> modifier
   23.10    val old_section_parser: bool Config.T
   23.11 @@ -103,6 +104,10 @@
   23.12    val report: text_range -> unit
   23.13    val parser: int -> text_range parser
   23.14    val parse: text_range parser
   23.15 +  val read: Proof.context -> Token.src -> text
   23.16 +  val read_closure: Proof.context -> Token.src -> text * Token.src
   23.17 +  val read_closure_input: Proof.context -> Input.source -> text * Token.src
   23.18 +  val text_closure: text context_parser
   23.19  end;
   23.20  
   23.21  structure Method: METHOD =
   23.22 @@ -576,6 +581,18 @@
   23.23  
   23.24  end;
   23.25  
   23.26 +fun evaluate_runtime text ctxt =
   23.27 +  let
   23.28 +    val text' =
   23.29 +      text |> (map_source o map o Token.map_facts)
   23.30 +        (fn SOME name =>
   23.31 +              (case Proof_Context.lookup_fact ctxt name of
   23.32 +                SOME {dynamic = true, thms} => K thms
   23.33 +              | _ => I)
   23.34 +          | NONE => I);
   23.35 +    val ctxt' = Config.put closure false ctxt;
   23.36 +  in fn facts => RUNTIME (fn st => evaluate text' ctxt' facts st) end;
   23.37 +
   23.38  
   23.39  
   23.40  (** concrete syntax **)
   23.41 @@ -743,6 +760,38 @@
   23.42  end;
   23.43  
   23.44  
   23.45 +(* read method text *)
   23.46 +
   23.47 +fun read ctxt src =
   23.48 +  (case Scan.read Token.stopper (Parse.!!! (parser 0 --| Scan.ahead Parse.eof)) src of
   23.49 +    SOME (text, range) =>
   23.50 +      if checked_text text then text
   23.51 +      else (report (text, range); check_text ctxt text)
   23.52 +  | NONE => error ("Failed to parse method" ^ Position.here (#1 (Token.range_of src))));
   23.53 +
   23.54 +fun read_closure ctxt src0 =
   23.55 +  let
   23.56 +    val src1 = map Token.init_assignable src0;
   23.57 +    val text = read ctxt src1 |> map_source (method_closure ctxt);
   23.58 +    val src2 = map Token.closure src1;
   23.59 +  in (text, src2) end;
   23.60 +
   23.61 +fun read_closure_input ctxt =
   23.62 +  Input.source_explode #>
   23.63 +  Token.read_no_commands (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof) #>
   23.64 +  read_closure ctxt;
   23.65 +
   23.66 +val text_closure =
   23.67 +  Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
   23.68 +    (case Token.get_value tok of
   23.69 +      SOME (Token.Source src) => read ctxt src
   23.70 +    | _ =>
   23.71 +        let
   23.72 +          val (text, src) = read_closure_input ctxt (Token.input_of tok);
   23.73 +          val _ = Token.assign (SOME (Token.Source src)) tok;
   23.74 +        in text end));
   23.75 +
   23.76 +
   23.77  (* theory setup *)
   23.78  
   23.79  val _ = Theory.setup
   23.80 @@ -792,7 +841,11 @@
   23.81    setup @{binding tactic} (parse_tactic >> (K o METHOD))
   23.82      "ML tactic as proof method" #>
   23.83    setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac))
   23.84 -    "ML tactic as raw proof method");
   23.85 +    "ML tactic as raw proof method" #>
   23.86 +  setup @{binding use}
   23.87 +    (Attrib.thms -- (Scan.lift (Parse.$$$ "in") |-- text_closure) >>
   23.88 +      (fn (thms, text) => fn ctxt => fn _ => evaluate_runtime text ctxt thms))
   23.89 +    "indicate method facts and context for method expression");
   23.90  
   23.91  
   23.92  (*final declarations of this structure!*)
    24.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Jul 22 15:39:27 2016 +0200
    24.2 +++ b/src/Pure/Isar/outer_syntax.scala	Fri Jul 22 15:39:32 2016 +0200
    24.3 @@ -91,6 +91,8 @@
    24.4      val keywords1 = keywords + (name, kind, tags)
    24.5      val completion1 =
    24.6        if (replace == Some("")) completion
    24.7 +      else if (replace.isEmpty && Keyword.theory_block.contains(kind))
    24.8 +        completion + (name, name + "\nbegin\n\u0007\nend") + (name, name)
    24.9        else completion + (name, replace getOrElse name)
   24.10      new Outer_Syntax(keywords1, completion1, language_context, true)
   24.11    }
    25.1 --- a/src/Pure/simplifier.ML	Fri Jul 22 15:39:27 2016 +0200
    25.2 +++ b/src/Pure/simplifier.ML	Fri Jul 22 15:39:32 2016 +0200
    25.3 @@ -69,7 +69,10 @@
    25.4    val simp_modifiers': Method.modifier parser list
    25.5    val simp_modifiers: Method.modifier parser list
    25.6    val method_setup: Method.modifier parser list -> theory -> theory
    25.7 -  val easy_setup: thm -> thm list -> theory -> theory
    25.8 +  val unsafe_solver_tac: Proof.context -> int -> tactic
    25.9 +  val unsafe_solver: solver
   25.10 +  val safe_solver_tac: Proof.context -> int -> tactic
   25.11 +  val safe_solver: solver
   25.12  end;
   25.13  
   25.14  structure Simplifier: SIMPLIFIER =
   25.15 @@ -376,31 +379,22 @@
   25.16          (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))
   25.17      "simplification (all goals)";
   25.18  
   25.19 -fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn ctxt0 =>
   25.20 -  let
   25.21 -    val trivialities = Drule.reflexive_thm :: trivs;
   25.22 -
   25.23 -    fun unsafe_solver_tac ctxt =
   25.24 -      FIRST' [resolve_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
   25.25 -    val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
   25.26 -
   25.27 -    (*no premature instantiation of variables during simplification*)
   25.28 -    fun safe_solver_tac ctxt =
   25.29 -      FIRST' [match_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
   25.30 -    val safe_solver = mk_solver "easy safe" safe_solver_tac;
   25.31 +fun unsafe_solver_tac ctxt =
   25.32 +  FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
   25.33 +val unsafe_solver = mk_solver "Pure unsafe" unsafe_solver_tac;
   25.34  
   25.35 -    fun mk_eq thm =
   25.36 -      if can Logic.dest_equals (Thm.concl_of thm) then [thm]
   25.37 -      else [thm RS reflect] handle THM _ => [];
   25.38 +(*no premature instantiation of variables during simplification*)
   25.39 +fun safe_solver_tac ctxt =
   25.40 +  FIRST' [match_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), eq_assume_tac];
   25.41 +val safe_solver = mk_solver "Pure safe" safe_solver_tac;
   25.42  
   25.43 -    fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
   25.44 -  in
   25.45 -    empty_simpset ctxt0
   25.46 -    setSSolver safe_solver
   25.47 -    setSolver unsafe_solver
   25.48 -    |> set_subgoaler asm_simp_tac
   25.49 -    |> set_mksimps (K mksimps)
   25.50 -  end));
   25.51 +val _ =
   25.52 +  Theory.setup
   25.53 +    (method_setup [] #> Context.theory_map (map_ss (fn ctxt =>
   25.54 +      empty_simpset ctxt
   25.55 +      setSSolver safe_solver
   25.56 +      setSolver unsafe_solver
   25.57 +      |> set_subgoaler asm_simp_tac)));
   25.58  
   25.59  end;
   25.60  
    26.1 --- a/src/Sequents/LK.thy	Fri Jul 22 15:39:27 2016 +0200
    26.2 +++ b/src/Sequents/LK.thy	Fri Jul 22 15:39:32 2016 +0200
    26.3 @@ -205,7 +205,7 @@
    26.4  setup \<open>Simplifier.method_setup []\<close>
    26.5  
    26.6  
    26.7 -text \<open>To create substition rules\<close>
    26.8 +text \<open>To create substitution rules\<close>
    26.9  
   26.10  lemma eq_imp_subst: "\<turnstile> a = b \<Longrightarrow> $H, A(a), $G \<turnstile> $E, A(b), $F"
   26.11    by simp
    27.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Jul 22 15:39:27 2016 +0200
    27.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Jul 22 15:39:32 2016 +0200
    27.3 @@ -35,8 +35,8 @@
    27.4      private val html =
    27.5        item.description match {
    27.6          case a :: bs =>
    27.7 -          "<html><b>" + HTML.output(a) + "</b>" +
    27.8 -            HTML.output(bs.map(" " + _).mkString) + "</html>"
    27.9 +          "<html><b>" + HTML.output(Symbol.print_newlines(a)) + "</b>" +
   27.10 +            HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "</html>"
   27.11          case Nil => ""
   27.12        }
   27.13      override def toString: String = html