--- a/Admin/Release/makedist Tue Aug 28 18:46:15 2012 +0200
+++ b/Admin/Release/makedist Tue Aug 28 18:57:32 2012 +0200
@@ -149,7 +149,7 @@
./Admin/build all || fail "Failed to build distribution"
-cp -a doc-src doc-src.orig
+cp -a src/Doc src/Doc.orig
./bin/isabelle build_doc -a || fail "Failed to build documentation"
if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
@@ -161,9 +161,9 @@
fi
rm -rf Admin
-rm -rf doc-src
+rm -rf src/Doc
-mv doc-src.orig doc-src
+mv src/Doc.orig src/Doc
mkdir -p contrib
cat >contrib/README <<EOF
--- a/ROOTS Tue Aug 28 18:46:15 2012 +0200
+++ b/ROOTS Tue Aug 28 18:57:32 2012 +0200
@@ -8,4 +8,4 @@
src/FOLP
src/LCF
src/Sequents
-doc-src
+src/Doc
--- a/doc-src/Classes/Classes.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,642 +0,0 @@
-theory Classes
-imports Main Setup
-begin
-
-section {* Introduction *}
-
-text {*
- Type classes were introduced by Wadler and Blott \cite{wadler89how}
- into the Haskell language to allow for a reasonable implementation
- of overloading\footnote{throughout this tutorial, we are referring
- to classical Haskell 1.0 type classes, not considering later
- additions in expressiveness}. As a canonical example, a polymorphic
- equality function @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on
- different types for @{text "\<alpha>"}, which is achieved by splitting
- introduction of the @{text eq} function from its overloaded
- definitions by means of @{text class} and @{text instance}
- declarations: \footnote{syntax here is a kind of isabellized
- Haskell}
-
- \begin{quote}
-
- \noindent@{text "class eq where"} \\
- \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
-
- \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
- \hspace*{2ex}@{text "eq 0 0 = True"} \\
- \hspace*{2ex}@{text "eq 0 _ = False"} \\
- \hspace*{2ex}@{text "eq _ 0 = False"} \\
- \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
-
- \medskip\noindent@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
- \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
-
- \medskip\noindent@{text "class ord extends eq where"} \\
- \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
- \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
-
- \end{quote}
-
- \noindent Type variables are annotated with (finitely many) classes;
- these annotations are assertions that a particular polymorphic type
- provides definitions for overloaded functions.
-
- Indeed, type classes not only allow for simple overloading but form
- a generic calculus, an instance of order-sorted algebra
- \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
-
- From a software engineering point of view, type classes roughly
- correspond to interfaces in object-oriented languages like Java; so,
- it is naturally desirable that type classes do not only provide
- functions (class parameters) but also state specifications
- implementations must obey. For example, the @{text "class eq"}
- above could be given the following specification, demanding that
- @{text "class eq"} is an equivalence relation obeying reflexivity,
- symmetry and transitivity:
-
- \begin{quote}
-
- \noindent@{text "class eq where"} \\
- \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
- @{text "satisfying"} \\
- \hspace*{2ex}@{text "refl: eq x x"} \\
- \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
- \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
-
- \end{quote}
-
- \noindent From a theoretical point of view, type classes are
- lightweight modules; Haskell type classes may be emulated by SML
- functors \cite{classes_modules}. Isabelle/Isar offers a discipline
- of type classes which brings all those aspects together:
-
- \begin{enumerate}
- \item specifying abstract parameters together with
- corresponding specifications,
- \item instantiating those abstract parameters by a particular
- type
- \item in connection with a ``less ad-hoc'' approach to overloading,
- \item with a direct link to the Isabelle module system:
- locales \cite{kammueller-locales}.
- \end{enumerate}
-
- \noindent Isar type classes also directly support code generation in
- a Haskell like fashion. Internally, they are mapped to more
- primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
-
- This tutorial demonstrates common elements of structured
- specifications and abstract reasoning with type classes by the
- algebraic hierarchy of semigroups, monoids and groups. Our
- background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
- which some familiarity is assumed.
-*}
-
-section {* A simple algebra example \label{sec:example} *}
-
-subsection {* Class definition *}
-
-text {*
- Depending on an arbitrary type @{text "\<alpha>"}, class @{text
- "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
- assumed to be associative:
-*}
-
-class %quote semigroup =
- fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70)
- assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
-
-text {*
- \noindent This @{command class} specification consists of two parts:
- the \qn{operational} part names the class parameter (@{element
- "fixes"}), the \qn{logical} part specifies properties on them
- (@{element "assumes"}). The local @{element "fixes"} and @{element
- "assumes"} are lifted to the theory toplevel, yielding the global
- parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
- global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z \<Colon>
- \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
-*}
-
-
-subsection {* Class instantiation \label{sec:class_inst} *}
-
-text {*
- The concrete type @{typ int} is made a @{class semigroup} instance
- by providing a suitable definition for the class parameter @{text
- "(\<otimes>)"} and a proof for the specification of @{fact assoc}. This is
- accomplished by the @{command instantiation} target:
-*}
-
-instantiation %quote int :: semigroup
-begin
-
-definition %quote
- mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
-
-instance %quote proof
- fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
- then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
- unfolding mult_int_def .
-qed
-
-end %quote
-
-text {*
- \noindent @{command instantiation} defines class parameters at a
- particular instance using common specification tools (here,
- @{command definition}). The concluding @{command instance} opens a
- proof that the given parameters actually conform to the class
- specification. Note that the first proof step is the @{method
- default} method, which for such instance proofs maps to the @{method
- intro_classes} method. This reduces an instance judgement to the
- relevant primitive proof goals; typically it is the first method
- applied in an instantiation proof.
-
- From now on, the type-checker will consider @{typ int} as a @{class
- semigroup} automatically, i.e.\ any general results are immediately
- available on concrete instances.
-
- \medskip Another instance of @{class semigroup} yields the natural
- numbers:
-*}
-
-instantiation %quote nat :: semigroup
-begin
-
-primrec %quote mult_nat where
- "(0\<Colon>nat) \<otimes> n = n"
- | "Suc m \<otimes> n = Suc (m \<otimes> n)"
-
-instance %quote proof
- fix m n q :: nat
- show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
- by (induct m) auto
-qed
-
-end %quote
-
-text {*
- \noindent Note the occurence of the name @{text mult_nat} in the
- primrec declaration; by default, the local name of a class operation
- @{text f} to be instantiated on type constructor @{text \<kappa>} is
- mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be
- inspected using the @{command "print_context"} command or the
- corresponding ProofGeneral button.
-*}
-
-subsection {* Lifting and parametric types *}
-
-text {*
- Overloaded definitions given at a class instantiation may include
- recursion over the syntactic structure of types. As a canonical
- example, we model product semigroups using our simple algebra:
-*}
-
-instantiation %quote prod :: (semigroup, semigroup) semigroup
-begin
-
-definition %quote
- mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
-
-instance %quote proof
- fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
- show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
- unfolding mult_prod_def by (simp add: assoc)
-qed
-
-end %quote
-
-text {*
- \noindent Associativity of product semigroups is established using
- the definition of @{text "(\<otimes>)"} on products and the hypothetical
- associativity of the type components; these hypotheses are
- legitimate due to the @{class semigroup} constraints imposed on the
- type components by the @{command instance} proposition. Indeed,
- this pattern often occurs with parametric types and type classes.
-*}
-
-
-subsection {* Subclassing *}
-
-text {*
- We define a subclass @{text monoidl} (a semigroup with a left-hand
- neutral) by extending @{class semigroup} with one additional
- parameter @{text neutral} together with its characteristic property:
-*}
-
-class %quote monoidl = semigroup +
- fixes neutral :: "\<alpha>" ("\<one>")
- assumes neutl: "\<one> \<otimes> x = x"
-
-text {*
- \noindent Again, we prove some instances, by providing suitable
- parameter definitions and proofs for the additional specifications.
- Observe that instantiations for types with the same arity may be
- simultaneous:
-*}
-
-instantiation %quote nat and int :: monoidl
-begin
-
-definition %quote
- neutral_nat_def: "\<one> = (0\<Colon>nat)"
-
-definition %quote
- neutral_int_def: "\<one> = (0\<Colon>int)"
-
-instance %quote proof
- fix n :: nat
- show "\<one> \<otimes> n = n"
- unfolding neutral_nat_def by simp
-next
- fix k :: int
- show "\<one> \<otimes> k = k"
- unfolding neutral_int_def mult_int_def by simp
-qed
-
-end %quote
-
-instantiation %quote prod :: (monoidl, monoidl) monoidl
-begin
-
-definition %quote
- neutral_prod_def: "\<one> = (\<one>, \<one>)"
-
-instance %quote proof
- fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
- show "\<one> \<otimes> p = p"
- unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
-qed
-
-end %quote
-
-text {*
- \noindent Fully-fledged monoids are modelled by another subclass,
- which does not add new parameters but tightens the specification:
-*}
-
-class %quote monoid = monoidl +
- assumes neutr: "x \<otimes> \<one> = x"
-
-instantiation %quote nat and int :: monoid
-begin
-
-instance %quote proof
- fix n :: nat
- show "n \<otimes> \<one> = n"
- unfolding neutral_nat_def by (induct n) simp_all
-next
- fix k :: int
- show "k \<otimes> \<one> = k"
- unfolding neutral_int_def mult_int_def by simp
-qed
-
-end %quote
-
-instantiation %quote prod :: (monoid, monoid) monoid
-begin
-
-instance %quote proof
- fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
- show "p \<otimes> \<one> = p"
- unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
-qed
-
-end %quote
-
-text {*
- \noindent To finish our small algebra example, we add a @{text
- group} class with a corresponding instance:
-*}
-
-class %quote group = monoidl +
- fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999)
- assumes invl: "x\<div> \<otimes> x = \<one>"
-
-instantiation %quote int :: group
-begin
-
-definition %quote
- inverse_int_def: "i\<div> = - (i\<Colon>int)"
-
-instance %quote proof
- fix i :: int
- have "-i + i = 0" by simp
- then show "i\<div> \<otimes> i = \<one>"
- unfolding mult_int_def neutral_int_def inverse_int_def .
-qed
-
-end %quote
-
-
-section {* Type classes as locales *}
-
-subsection {* A look behind the scenes *}
-
-text {*
- The example above gives an impression how Isar type classes work in
- practice. As stated in the introduction, classes also provide a
- link to Isar's locale system. Indeed, the logical core of a class
- is nothing other than a locale:
-*}
-
-class %quote idem =
- fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
- assumes idem: "f (f x) = f x"
-
-text {*
- \noindent essentially introduces the locale
-*} (*<*)setup %invisible {* Sign.add_path "foo" *}
-(*>*)
-locale %quote idem =
- fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
- assumes idem: "f (f x) = f x"
-
-text {* \noindent together with corresponding constant(s): *}
-
-consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
-
-text {*
- \noindent The connection to the type system is done by means
- of a primitive type class
-*} (*<*)setup %invisible {* Sign.add_path "foo" *}
-(*>*)
-classes %quote idem < type
-(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
-setup %invisible {* Sign.parent_path *}(*>*)
-
-text {* \noindent together with a corresponding interpretation: *}
-
-interpretation %quote idem_class:
- idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
-(*<*)proof qed (rule idem)(*>*)
-
-text {*
- \noindent This gives you the full power of the Isabelle module system;
- conclusions in locale @{text idem} are implicitly propagated
- to class @{text idem}.
-*} (*<*)setup %invisible {* Sign.parent_path *}
-(*>*)
-subsection {* Abstract reasoning *}
-
-text {*
- Isabelle locales enable reasoning at a general level, while results
- are implicitly transferred to all instances. For example, we can
- now establish the @{text "left_cancel"} lemma for groups, which
- states that the function @{text "(x \<otimes>)"} is injective:
-*}
-
-lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
-proof
- assume "x \<otimes> y = x \<otimes> z"
- then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
- then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
- then show "y = z" using neutl and invl by simp
-next
- assume "y = z"
- then show "x \<otimes> y = x \<otimes> z" by simp
-qed
-
-text {*
- \noindent Here the \qt{@{keyword "in"} @{class group}} target
- specification indicates that the result is recorded within that
- context for later use. This local theorem is also lifted to the
- global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon>
- \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been
- made an instance of @{text "group"} before, we may refer to that
- fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
- z"}.
-*}
-
-
-subsection {* Derived definitions *}
-
-text {*
- Isabelle locales are targets which support local definitions:
-*}
-
-primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
- "pow_nat 0 x = \<one>"
- | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
-
-text {*
- \noindent If the locale @{text group} is also a class, this local
- definition is propagated onto a global definition of @{term [source]
- "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} with corresponding theorems
-
- @{thm pow_nat.simps [no_vars]}.
-
- \noindent As you can see from this example, for local definitions
- you may use any specification tool which works together with
- locales, such as Krauss's recursive function package
- \cite{krauss2006}.
-*}
-
-
-subsection {* A functor analogy *}
-
-text {*
- We introduced Isar classes by analogy to type classes in functional
- programming; if we reconsider this in the context of what has been
- said about type classes and locales, we can drive this analogy
- further by stating that type classes essentially correspond to
- functors that have a canonical interpretation as type classes.
- There is also the possibility of other interpretations. For
- example, @{text list}s also form a monoid with @{text append} and
- @{term "[]"} as operations, but it seems inappropriate to apply to
- lists the same operations as for genuinely algebraic types. In such
- a case, we can simply make a particular interpretation of monoids
- for lists:
-*}
-
-interpretation %quote list_monoid: monoid append "[]"
- proof qed auto
-
-text {*
- \noindent This enables us to apply facts on monoids
- to lists, e.g. @{thm list_monoid.neutl [no_vars]}.
-
- When using this interpretation pattern, it may also
- be appropriate to map derived definitions accordingly:
-*}
-
-primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
- "replicate 0 _ = []"
- | "replicate (Suc n) xs = xs @ replicate n xs"
-
-interpretation %quote list_monoid: monoid append "[]" where
- "monoid.pow_nat append [] = replicate"
-proof -
- interpret monoid append "[]" ..
- show "monoid.pow_nat append [] = replicate"
- proof
- fix n
- show "monoid.pow_nat append [] n = replicate n"
- by (induct n) auto
- qed
-qed intro_locales
-
-text {*
- \noindent This pattern is also helpful to reuse abstract
- specifications on the \emph{same} type. For example, think of a
- class @{text preorder}; for type @{typ nat}, there are at least two
- possible instances: the natural order or the order induced by the
- divides relation. But only one of these instances can be used for
- @{command instantiation}; using the locale behind the class @{text
- preorder}, it is still possible to utilise the same abstract
- specification again using @{command interpretation}.
-*}
-
-subsection {* Additional subclass relations *}
-
-text {*
- Any @{text "group"} is also a @{text "monoid"}; this can be made
- explicit by claiming an additional subclass relation, together with
- a proof of the logical difference:
-*}
-
-subclass %quote (in group) monoid
-proof
- fix x
- from invl have "x\<div> \<otimes> x = \<one>" by simp
- with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
- with left_cancel show "x \<otimes> \<one> = x" by simp
-qed
-
-text {*
- The logical proof is carried out on the locale level. Afterwards it
- is propagated to the type system, making @{text group} an instance
- of @{text monoid} by adding an additional edge to the graph of
- subclass relations (\figref{fig:subclass}).
-
- \begin{figure}[htbp]
- \begin{center}
- \small
- \unitlength 0.6mm
- \begin{picture}(40,60)(0,0)
- \put(20,60){\makebox(0,0){@{text semigroup}}}
- \put(20,40){\makebox(0,0){@{text monoidl}}}
- \put(00,20){\makebox(0,0){@{text monoid}}}
- \put(40,00){\makebox(0,0){@{text group}}}
- \put(20,55){\vector(0,-1){10}}
- \put(15,35){\vector(-1,-1){10}}
- \put(25,35){\vector(1,-3){10}}
- \end{picture}
- \hspace{8em}
- \begin{picture}(40,60)(0,0)
- \put(20,60){\makebox(0,0){@{text semigroup}}}
- \put(20,40){\makebox(0,0){@{text monoidl}}}
- \put(00,20){\makebox(0,0){@{text monoid}}}
- \put(40,00){\makebox(0,0){@{text group}}}
- \put(20,55){\vector(0,-1){10}}
- \put(15,35){\vector(-1,-1){10}}
- \put(05,15){\vector(3,-1){30}}
- \end{picture}
- \caption{Subclass relationship of monoids and groups:
- before and after establishing the relationship
- @{text "group \<subseteq> monoid"}; transitive edges are left out.}
- \label{fig:subclass}
- \end{center}
- \end{figure}
-
- For illustration, a derived definition in @{text group} using @{text
- pow_nat}
-*}
-
-definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
- "pow_int k x = (if k >= 0
- then pow_nat (nat k) x
- else (pow_nat (nat (- k)) x)\<div>)"
-
-text {*
- \noindent yields the global definition of @{term [source] "pow_int \<Colon>
- int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm
- pow_int_def [no_vars]}.
-*}
-
-subsection {* A note on syntax *}
-
-text {*
- As a convenience, class context syntax allows references to local
- class operations and their global counterparts uniformly; type
- inference resolves ambiguities. For example:
-*}
-
-context %quote semigroup
-begin
-
-term %quote "x \<otimes> y" -- {* example 1 *}
-term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
-
-end %quote
-
-term %quote "x \<otimes> y" -- {* example 3 *}
-
-text {*
- \noindent Here in example 1, the term refers to the local class
- operation @{text "mult [\<alpha>]"}, whereas in example 2 the type
- constraint enforces the global class operation @{text "mult [nat]"}.
- In the global context in example 3, the reference is to the
- polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
-*}
-
-section {* Further issues *}
-
-subsection {* Type classes and code generation *}
-
-text {*
- Turning back to the first motivation for type classes, namely
- overloading, it is obvious that overloading stemming from @{command
- class} statements and @{command instantiation} targets naturally
- maps to Haskell type classes. The code generator framework
- \cite{isabelle-codegen} takes this into account. If the target
- language (e.g.~SML) lacks type classes, then they are implemented by
- an explicit dictionary construction. As example, let's go back to
- the power function:
-*}
-
-definition %quote example :: int where
- "example = pow_int 10 (-2)"
-
-text {*
- \noindent This maps to Haskell as follows:
-*}
-(*<*)code_include %invisible Haskell "Natural" -(*>*)
-text %quotetypewriter {*
- @{code_stmts example (Haskell)}
-*}
-
-text {*
- \noindent The code in SML has explicit dictionary passing:
-*}
-text %quotetypewriter {*
- @{code_stmts example (SML)}
-*}
-
-
-text {*
- \noindent In Scala, implicts are used as dictionaries:
-*}
-(*<*)code_include %invisible Scala "Natural" -(*>*)
-text %quotetypewriter {*
- @{code_stmts example (Scala)}
-*}
-
-
-subsection {* Inspecting the type class universe *}
-
-text {*
- To facilitate orientation in complex subclass structures, two
- diagnostics commands are provided:
-
- \begin{description}
-
- \item[@{command "print_classes"}] print a list of all classes
- together with associated operations etc.
-
- \item[@{command "class_deps"}] visualizes the subclass relation
- between all classes as a Hasse diagram.
-
- \end{description}
-*}
-
-end
--- a/doc-src/Classes/Setup.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-theory Setup
-imports Main "~~/src/HOL/Library/Code_Integer"
-begin
-
-ML_file "../antiquote_setup.ML"
-ML_file "../more_antiquote.ML"
-
-setup {*
- Antiquote_Setup.setup #>
- More_Antiquote.setup #>
- Code_Target.set_default_code_width 74
-*}
-
-syntax
- "_alpha" :: "type" ("\<alpha>")
- "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000)
- "_beta" :: "type" ("\<beta>")
- "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000)
-
-parse_ast_translation {*
- let
- fun alpha_ast_tr [] = Ast.Variable "'a"
- | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
- fun alpha_ofsort_ast_tr [ast] =
- Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'a", ast]
- | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
- fun beta_ast_tr [] = Ast.Variable "'b"
- | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
- fun beta_ofsort_ast_tr [ast] =
- Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
- | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
- in
- [(@{syntax_const "_alpha"}, alpha_ast_tr),
- (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
- (@{syntax_const "_beta"}, beta_ast_tr),
- (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
- end
-*}
-
-end
\ No newline at end of file
--- a/doc-src/Classes/document/build Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-#!/bin/bash
-
-set -e
-
-FORMAT="$1"
-VARIANT="$2"
-
-"$ISABELLE_TOOL" logo -o isabelle_isar.pdf Isar
-"$ISABELLE_TOOL" logo -o isabelle_isar.eps Isar
-
-cp "$ISABELLE_HOME/doc-src/iman.sty" .
-cp "$ISABELLE_HOME/doc-src/extra.sty" .
-cp "$ISABELLE_HOME/doc-src/isar.sty" .
-cp "$ISABELLE_HOME/doc-src/proof.sty" .
-cp "$ISABELLE_HOME/doc-src/manual.bib" .
-
-"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
-
--- a/doc-src/Classes/document/root.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-\documentclass[12pt,a4paper,fleqn]{article}
-\usepackage{latexsym,graphicx}
-\usepackage{iman,extra,isar,proof}
-\usepackage{isabelle,isabellesym}
-\usepackage{style}
-\usepackage{pdfsetup}
-
-
-\hyphenation{Isabelle}
-\hyphenation{Isar}
-\isadroptag{theory}
-
-\title{\includegraphics[scale=0.5]{isabelle_isar}
- \\[4ex] Haskell-style type classes with Isabelle/Isar}
-\author{\emph{Florian Haftmann}}
-
-\begin{document}
-
-\maketitle
-
-\begin{abstract}
- \noindent This tutorial introduces Isar type classes, which
- are a convenient mechanism for organizing specifications.
- Essentially, they combine an operational aspect (in the
- manner of Haskell) with a logical aspect, both managed uniformly.
-\end{abstract}
-
-\thispagestyle{empty}\clearpage
-
-\pagenumbering{roman}
-\clearfirst
-
-\input{Classes.tex}
-
-\begingroup
-\bibliographystyle{plain} \small\raggedright\frenchspacing
-\bibliography{manual}
-\endgroup
-
-\end{document}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
--- a/doc-src/Classes/document/style.sty Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-
-%% toc
-\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
-\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
-
-%% paragraphs
-\setlength{\parindent}{1em}
-
-%% references
-\newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\figref}[1]{figure~\ref{#1}}
-
-%% logical markup
-\newcommand{\strong}[1]{{\bfseries {#1}}}
-\newcommand{\qn}[1]{\emph{#1}}
-
-%% typographic conventions
-\newcommand{\qt}[1]{``{#1}''}
-\newcommand{\ditem}[1]{\item[\isastyletext #1]}
-
-%% quote environment
-\isakeeptag{quote}
-\renewenvironment{quote}
- {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
- {\endlist}
-\renewcommand{\isatagquote}{\begin{quote}}
-\renewcommand{\endisatagquote}{\end{quote}}
-\newcommand{\quotebreak}{\\[1.2ex]}
-
-%% typewriter text
-\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
-\renewcommand{\isadigit}[1]{{##1}}%
-\parindent0pt%
-\makeatletter\isa@parindent0pt\makeatother%
-\isabellestyle{tt}\isastyle%
-\fontsize{9pt}{9pt}\selectfont}{}
-
-\isakeeptag{quotetypewriter}
-\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
-\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
-
-%% presentation
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
-
-%% character detail
-\renewcommand{\isadigit}[1]{\isamath{#1}}
-\binperiod
-\underscoreoff
-
-%% format
-\pagestyle{headings}
-\isabellestyle{it}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "implementation"
-%%% End:
--- a/doc-src/Codegen/Adaptation.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,347 +0,0 @@
-theory Adaptation
-imports Setup
-begin
-
-setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I))
- #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", K I)) *}
-
-section {* Adaptation to target languages \label{sec:adaptation} *}
-
-subsection {* Adapting code generation *}
-
-text {*
- The aspects of code generation introduced so far have two aspects
- in common:
-
- \begin{itemize}
-
- \item They act uniformly, without reference to a specific target
- language.
-
- \item They are \emph{safe} in the sense that as long as you trust
- the code generator meta theory and implementation, you cannot
- produce programs that yield results which are not derivable in
- the logic.
-
- \end{itemize}
-
- \noindent In this section we will introduce means to \emph{adapt}
- the serialiser to a specific target language, i.e.~to print program
- fragments in a way which accommodates \qt{already existing}
- ingredients of a target language environment, for three reasons:
-
- \begin{itemize}
- \item improving readability and aesthetics of generated code
- \item gaining efficiency
- \item interface with language parts which have no direct counterpart
- in @{text "HOL"} (say, imperative data structures)
- \end{itemize}
-
- \noindent Generally, you should avoid using those features yourself
- \emph{at any cost}:
-
- \begin{itemize}
-
- \item The safe configuration methods act uniformly on every target
- language, whereas for adaptation you have to treat each target
- language separately.
-
- \item Application is extremely tedious since there is no
- abstraction which would allow for a static check, making it easy
- to produce garbage.
-
- \item Subtle errors can be introduced unconsciously.
-
- \end{itemize}
-
- \noindent However, even if you ought refrain from setting up
- adaptation yourself, already the @{text "HOL"} comes with some
- reasonable default adaptations (say, using target language list
- syntax). There also some common adaptation cases which you can
- setup by importing particular library theories. In order to
- understand these, we provide some clues here; these however are not
- supposed to replace a careful study of the sources.
-*}
-
-
-subsection {* The adaptation principle *}
-
-text {*
- Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is
- conceptually supposed to be:
-
- \begin{figure}[here]
- \includegraphics{adapt}
- \caption{The adaptation principle}
- \label{fig:adaptation}
- \end{figure}
-
- \noindent In the tame view, code generation acts as broker between
- @{text logic}, @{text "intermediate language"} and @{text "target
- language"} by means of @{text translation} and @{text
- serialisation}; for the latter, the serialiser has to observe the
- structure of the @{text language} itself plus some @{text reserved}
- keywords which have to be avoided for generated code. However, if
- you consider @{text adaptation} mechanisms, the code generated by
- the serializer is just the tip of the iceberg:
-
- \begin{itemize}
-
- \item @{text serialisation} can be \emph{parametrised} such that
- logical entities are mapped to target-specific ones
- (e.g. target-specific list syntax, see also
- \secref{sec:adaptation_mechanisms})
-
- \item Such parametrisations can involve references to a
- target-specific standard @{text library} (e.g. using the @{text
- Haskell} @{verbatim Maybe} type instead of the @{text HOL}
- @{type "option"} type); if such are used, the corresponding
- identifiers (in our example, @{verbatim Maybe}, @{verbatim
- Nothing} and @{verbatim Just}) also have to be considered @{text
- reserved}.
-
- \item Even more, the user can enrich the library of the
- target-language by providing code snippets (\qt{@{text
- "includes"}}) which are prepended to any generated code (see
- \secref{sec:include}); this typically also involves further
- @{text reserved} identifiers.
-
- \end{itemize}
-
- \noindent As figure \ref{fig:adaptation} illustrates, all these
- adaptation mechanisms have to act consistently; it is at the
- discretion of the user to take care for this.
-*}
-
-subsection {* Common adaptation patterns *}
-
-text {*
- The @{theory HOL} @{theory Main} theory already provides a code
- generator setup which should be suitable for most applications.
- Common extensions and modifications are available by certain
- theories of the @{text HOL} library; beside being useful in
- applications, they may serve as a tutorial for customising the code
- generator setup (see below \secref{sec:adaptation_mechanisms}).
-
- \begin{description}
-
- \item[@{text "Code_Integer"}] represents @{text HOL} integers by
- big integer literals in target languages.
-
- \item[@{text "Code_Char"}] represents @{text HOL} characters by
- character literals in target languages.
-
- \item[@{text "Code_Char_chr"}] like @{text "Code_Char"}, but
- also offers treatment of character codes; includes @{text
- "Code_Char"}.
-
- \item[@{text "Efficient_Nat"}] \label{eff_nat} implements
- natural numbers by integers, which in general will result in
- higher efficiency; pattern matching with @{term "0\<Colon>nat"} /
- @{const "Suc"} is eliminated; includes @{text "Code_Integer"}
- and @{text "Code_Numeral"}.
-
- \item[@{theory "Code_Numeral"}] provides an additional datatype
- @{typ index} which is mapped to target-language built-in
- integers. Useful for code setups which involve e.g.~indexing
- of target-language arrays. Part of @{text "HOL-Main"}.
-
- \item[@{theory "String"}] provides an additional datatype @{typ
- String.literal} which is isomorphic to strings; @{typ
- String.literal}s are mapped to target-language strings. Useful
- for code setups which involve e.g.~printing (error) messages.
- Part of @{text "HOL-Main"}.
-
- \end{description}
-
- \begin{warn}
- When importing any of those theories which are not part of
- @{text "HOL-Main"}, they should form the last
- items in an import list. Since these theories adapt the code
- generator setup in a non-conservative fashion, strange effects may
- occur otherwise.
- \end{warn}
-*}
-
-
-subsection {* Parametrising serialisation \label{sec:adaptation_mechanisms} *}
-
-text {*
- Consider the following function and its corresponding SML code:
-*}
-
-primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
- "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
-(*<*)
-code_type %invisible bool
- (SML)
-code_const %invisible True and False and "op \<and>" and Not
- (SML and and and)
-(*>*)
-text %quotetypewriter {*
- @{code_stmts in_interval (SML)}
-*}
-
-text {*
- \noindent Though this is correct code, it is a little bit
- unsatisfactory: boolean values and operators are materialised as
- distinguished entities with have nothing to do with the SML-built-in
- notion of \qt{bool}. This results in less readable code;
- additionally, eager evaluation may cause programs to loop or break
- which would perfectly terminate when the existing SML @{verbatim
- "bool"} would be used. To map the HOL @{typ bool} on SML @{verbatim
- "bool"}, we may use \qn{custom serialisations}:
-*}
-
-code_type %quotett bool
- (SML "bool")
-code_const %quotett True and False and "op \<and>"
- (SML "true" and "false" and "_ andalso _")
-
-text {*
- \noindent The @{command_def code_type} command takes a type constructor
- as arguments together with a list of custom serialisations. Each
- custom serialisation starts with a target language identifier
- followed by an expression, which during code serialisation is
- inserted whenever the type constructor would occur. For constants,
- @{command_def code_const} implements the corresponding mechanism. Each
- ``@{verbatim "_"}'' in a serialisation expression is treated as a
- placeholder for the type constructor's (the constant's) arguments.
-*}
-
-text %quotetypewriter {*
- @{code_stmts in_interval (SML)}
-*}
-
-text {*
- \noindent This still is not perfect: the parentheses around the
- \qt{andalso} expression are superfluous. Though the serialiser by
- no means attempts to imitate the rich Isabelle syntax framework, it
- provides some common idioms, notably associative infixes with
- precedences which may be used here:
-*}
-
-code_const %quotett "op \<and>"
- (SML infixl 1 "andalso")
-
-text %quotetypewriter {*
- @{code_stmts in_interval (SML)}
-*}
-
-text {*
- \noindent The attentive reader may ask how we assert that no
- generated code will accidentally overwrite. For this reason the
- serialiser has an internal table of identifiers which have to be
- avoided to be used for new declarations. Initially, this table
- typically contains the keywords of the target language. It can be
- extended manually, thus avoiding accidental overwrites, using the
- @{command_def "code_reserved"} command:
-*}
-
-code_reserved %quote "\<SMLdummy>" bool true false andalso
-
-text {*
- \noindent Next, we try to map HOL pairs to SML pairs, using the
- infix ``@{verbatim "*"}'' type constructor and parentheses:
-*}
-(*<*)
-code_type %invisible prod
- (SML)
-code_const %invisible Pair
- (SML)
-(*>*)
-code_type %quotett prod
- (SML infix 2 "*")
-code_const %quotett Pair
- (SML "!((_),/ (_))")
-
-text {*
- \noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
- never to put parentheses around the whole expression (they are
- already present), while the parentheses around argument place
- holders tell not to put parentheses around the arguments. The slash
- ``@{verbatim "/"}'' (followed by arbitrary white space) inserts a
- space which may be used as a break if necessary during pretty
- printing.
-
- These examples give a glimpse what mechanisms custom serialisations
- provide; however their usage requires careful thinking in order not
- to introduce inconsistencies -- or, in other words: custom
- serialisations are completely axiomatic.
-
- A further noteworthy detail is that any special character in a
- custom serialisation may be quoted using ``@{verbatim "'"}''; thus,
- in ``@{verbatim "fn '_ => _"}'' the first ``@{verbatim "_"}'' is a
- proper underscore while the second ``@{verbatim "_"}'' is a
- placeholder.
-*}
-
-
-subsection {* @{text Haskell} serialisation *}
-
-text {*
- For convenience, the default @{text HOL} setup for @{text Haskell}
- maps the @{class equal} class to its counterpart in @{text Haskell},
- giving custom serialisations for the class @{class equal} (by command
- @{command_def code_class}) and its operation @{const [source] HOL.equal}
-*}
-
-code_class %quotett equal
- (Haskell "Eq")
-
-code_const %quotett "HOL.equal"
- (Haskell infixl 4 "==")
-
-text {*
- \noindent A problem now occurs whenever a type which is an instance
- of @{class equal} in @{text HOL} is mapped on a @{text
- Haskell}-built-in type which is also an instance of @{text Haskell}
- @{text Eq}:
-*}
-
-typedecl %quote bar
-
-instantiation %quote bar :: equal
-begin
-
-definition %quote "HOL.equal (x\<Colon>bar) y \<longleftrightarrow> x = y"
-
-instance %quote by default (simp add: equal_bar_def)
-
-end %quote (*<*)
-
-(*>*) code_type %quotett bar
- (Haskell "Integer")
-
-text {*
- \noindent The code generator would produce an additional instance,
- which of course is rejected by the @{text Haskell} compiler. To
- suppress this additional instance, use @{command_def "code_instance"}:
-*}
-
-code_instance %quotett bar :: equal
- (Haskell -)
-
-
-subsection {* Enhancing the target language context \label{sec:include} *}
-
-text {*
- In rare cases it is necessary to \emph{enrich} the context of a
- target language; this is accomplished using the @{command_def
- "code_include"} command:
-*}
-
-code_include %quotett Haskell "Errno"
-{*errno i = error ("Error number: " ++ show i)*}
-
-code_reserved %quotett Haskell Errno
-
-text {*
- \noindent Such named @{text include}s are then prepended to every
- generated code. Inspect such code in order to find out how
- @{command "code_include"} behaves with respect to a particular
- target language.
-*}
-
-end
-
--- a/doc-src/Codegen/Evaluation.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,287 +0,0 @@
-theory Evaluation
-imports Setup
-begin
-
-section {* Evaluation \label{sec:evaluation} *}
-
-text {*
- Recalling \secref{sec:principle}, code generation turns a system of
- equations into a program with the \emph{same} equational semantics.
- As a consequence, this program can be used as a \emph{rewrite
- engine} for terms: rewriting a term @{term "t"} using a program to a
- term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}. This
- application of code generation in the following is referred to as
- \emph{evaluation}.
-*}
-
-
-subsection {* Evaluation techniques *}
-
-text {*
- The existing infrastructure provides a rich palette of evaluation
- techniques, each comprising different aspects:
-
- \begin{description}
-
- \item[Expressiveness.] Depending on how good symbolic computation
- is supported, the class of terms which can be evaluated may be
- bigger or smaller.
-
- \item[Efficiency.] The more machine-near the technique, the
- faster it is.
-
- \item[Trustability.] Techniques which a huge (and also probably
- more configurable infrastructure) are more fragile and less
- trustable.
-
- \end{description}
-*}
-
-
-subsubsection {* The simplifier (@{text simp}) *}
-
-text {*
- The simplest way for evaluation is just using the simplifier with
- the original code equations of the underlying program. This gives
- fully symbolic evaluation and highest trustablity, with the usual
- performance of the simplifier. Note that for operations on abstract
- datatypes (cf.~\secref{sec:invariant}), the original theorems as
- given by the users are used, not the modified ones.
-*}
-
-
-subsubsection {* Normalization by evaluation (@{text nbe}) *}
-
-text {*
- Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe}
- provides a comparably fast partially symbolic evaluation which
- permits also normalization of functions and uninterpreted symbols;
- the stack of code to be trusted is considerable.
-*}
-
-
-subsubsection {* Evaluation in ML (@{text code}) *}
-
-text {*
- Highest performance can be achieved by evaluation in ML, at the cost
- of being restricted to ground results and a layered stack of code to
- be trusted, including code generator configurations by the user.
-
- Evaluation is carried out in a target language \emph{Eval} which
- inherits from \emph{SML} but for convenience uses parts of the
- Isabelle runtime environment. The soundness of computation carried
- out there depends crucially on the correctness of the code
- generator setup; this is one of the reasons why you should not use
- adaptation (see \secref{sec:adaptation}) frivolously.
-*}
-
-
-subsection {* Aspects of evaluation *}
-
-text {*
- Each of the techniques can be combined with different aspects. The
- most important distinction is between dynamic and static evaluation.
- Dynamic evaluation takes the code generator configuration \qt{as it
- is} at the point where evaluation is issued. Best example is the
- @{command_def value} command which allows ad-hoc evaluation of
- terms:
-*}
-
-value %quote "42 / (12 :: rat)"
-
-text {*
- \noindent By default @{command value} tries all available evaluation
- techniques and prints the result of the first succeeding one. A particular
- technique may be specified in square brackets, e.g.
-*}
-
-value %quote [nbe] "42 / (12 :: rat)"
-
-text {*
- To employ dynamic evaluation in the document generation, there is also
- a @{text value} antiquotation. By default, it also tries all available evaluation
- techniques and prints the result of the first succeeding one, unless a particular
- technique is specified in square brackets.
-
- Static evaluation freezes the code generator configuration at a
- certain point and uses this context whenever evaluation is issued
- later on. This is particularly appropriate for proof procedures
- which use evaluation, since then the behaviour of evaluation is not
- changed or even compromised later on by actions of the user.
-
- As a technical complication, terms after evaluation in ML must be
- turned into Isabelle's internal term representation again. Since
- this is also configurable, it is never fully trusted. For this
- reason, evaluation in ML comes with further aspects:
-
- \begin{description}
-
- \item[Plain evaluation.] A term is normalized using the provided
- term reconstruction from ML to Isabelle; for applications which
- do not need to be fully trusted.
-
- \item[Property conversion.] Evaluates propositions; since these
- are monomorphic, the term reconstruction is fixed once and for all
- and therefore trustable.
-
- \item[Conversion.] Evaluates an arbitrary term @{term "t"} first
- by plain evaluation and certifies the result @{term "t'"} by
- checking the equation @{term "t \<equiv> t'"} using property
- conversion.
-
- \end{description}
-
- \noindent The picture is further complicated by the roles of
- exceptions. Here three cases have to be distinguished:
-
- \begin{itemize}
-
- \item Evaluation of @{term t} terminates with a result @{term
- "t'"}.
-
- \item Evaluation of @{term t} terminates which en exception
- indicating a pattern match failure or a non-implemented
- function. As sketched in \secref{sec:partiality}, this can be
- interpreted as partiality.
-
- \item Evaluation raises any other kind of exception.
-
- \end{itemize}
-
- \noindent For conversions, the first case yields the equation @{term
- "t = t'"}, the second defaults to reflexivity @{term "t = t"}.
- Exceptions of the third kind are propagated to the user.
-
- By default return values of plain evaluation are optional, yielding
- @{text "SOME t'"} in the first case, @{text "NONE"} in the
- second, and propagating the exception in the third case. A strict
- variant of plain evaluation either yields @{text "t'"} or propagates
- any exception, a liberal variant caputures any exception in a result
- of type @{text "Exn.result"}.
-
- For property conversion (which coincides with conversion except for
- evaluation in ML), methods are provided which solve a given goal by
- evaluation.
-*}
-
-
-subsection {* Schematic overview *}
-
-text {*
- \newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
- \fontsize{9pt}{12pt}\selectfont
- \begin{tabular}{ll||c|c|c}
- & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
- \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
- & interactive evaluation
- & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
- \tabularnewline
- & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
- & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
- & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
- & conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"}
- & \ttsize@{ML "Code_Evaluation.dynamic_conv"} \tabularnewline \hline \hline
- \multirow{3}{1ex}{\rotatebox{90}{static}}
- & plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5}
- & property conversion & &
- & \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5}
- & conversion & \ttsize@{ML "Code_Simp.static_conv"}
- & \ttsize@{ML "Nbe.static_conv"}
- & \ttsize@{ML "Code_Evaluation.static_conv"}
- \end{tabular}
-*}
-
-
-subsection {* Intimate connection between logic and system runtime *}
-
-text {*
- The toolbox of static evaluation conversions forms a reasonable base
- to interweave generated code and system tools. However in some
- situations more direct interaction is desirable.
-*}
-
-
-subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation *}
-
-text {*
- The @{text code} antiquotation allows to include constants from
- generated code directly into ML system code, as in the following toy
- example:
-*}
-
-datatype %quote form = T | F | And form form | Or form form (*<*)
-
-(*>*) ML %quotett {*
- fun eval_form @{code T} = true
- | eval_form @{code F} = false
- | eval_form (@{code And} (p, q)) =
- eval_form p andalso eval_form q
- | eval_form (@{code Or} (p, q)) =
- eval_form p orelse eval_form q;
-*}
-
-text {*
- \noindent @{text code} takes as argument the name of a constant;
- after the whole ML is read, the necessary code is generated
- transparently and the corresponding constant names are inserted.
- This technique also allows to use pattern matching on constructors
- stemming from compiled datatypes. Note that the @{text code}
- antiquotation may not refer to constants which carry adaptations;
- here you have to refer to the corresponding adapted code directly.
-
- For a less simplistic example, theory @{text Approximation} in
- the @{text Decision_Procs} session is a good reference.
-*}
-
-
-subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
-
-text {*
- The @{text code} antiquoation is lightweight, but the generated code
- is only accessible while the ML section is processed. Sometimes this
- is not appropriate, especially if the generated code contains datatype
- declarations which are shared with other parts of the system. In these
- cases, @{command_def code_reflect} can be used:
-*}
-
-code_reflect %quote Sum_Type
- datatypes sum = Inl | Inr
- functions "Sum_Type.Projl" "Sum_Type.Projr"
-
-text {*
- \noindent @{command_def code_reflect} takes a structure name and
- references to datatypes and functions; for these code is compiled
- into the named ML structure and the \emph{Eval} target is modified
- in a way that future code generation will reference these
- precompiled versions of the given datatypes and functions. This
- also allows to refer to the referenced datatypes and functions from
- arbitrary ML code as well.
-
- A typical example for @{command code_reflect} can be found in the
- @{theory Predicate} theory.
-*}
-
-
-subsubsection {* Separate compilation -- @{text code_reflect} *}
-
-text {*
- For technical reasons it is sometimes necessary to separate
- generation and compilation of code which is supposed to be used in
- the system runtime. For this @{command code_reflect} with an
- optional @{text "file"} argument can be used:
-*}
-
-code_reflect %quote Rat
- datatypes rat = Frct
- functions Fract
- "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
- "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
- file "examples/rat.ML"
-
-text {*
- \noindent This merely generates the referenced code to the given
- file which can be included into the system runtime later on.
-*}
-
-end
-
--- a/doc-src/Codegen/Foundations.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,347 +0,0 @@
-theory Foundations
-imports Introduction
-begin
-
-section {* Code generation foundations \label{sec:foundations} *}
-
-subsection {* Code generator architecture \label{sec:architecture} *}
-
-text {*
- The code generator is actually a framework consisting of different
- components which can be customised individually.
-
- Conceptually all components operate on Isabelle's logic framework
- @{theory Pure}. Practically, the object logic @{theory HOL}
- provides the necessary facilities to make use of the code generator,
- mainly since it is an extension of @{theory Pure}.
-
- The constellation of the different components is visualized in the
- following picture.
-
- \begin{figure}[h]
- \includegraphics{architecture}
- \caption{Code generator architecture}
- \label{fig:arch}
- \end{figure}
-
- \noindent Central to code generation is the notion of \emph{code
- equations}. A code equation as a first approximation is a theorem
- of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"} (an equation headed by a
- constant @{text f} with arguments @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right
- hand side @{text t}).
-
- \begin{itemize}
-
- \item Starting point of code generation is a collection of (raw)
- code equations in a theory. It is not relevant where they stem
- from, but typically they were either produced by specification
- tools or proved explicitly by the user.
-
- \item These raw code equations can be subjected to theorem
- transformations. This \qn{preprocessor} (see
- \secref{sec:preproc}) can apply the full expressiveness of
- ML-based theorem transformations to code generation. The result
- of preprocessing is a structured collection of code equations.
-
- \item These code equations are \qn{translated} to a program in an
- abstract intermediate language. Think of it as a kind of
- \qt{Mini-Haskell} with four \qn{statements}: @{text data} (for
- datatypes), @{text fun} (stemming from code equations), also
- @{text class} and @{text inst} (for type classes).
-
- \item Finally, the abstract program is \qn{serialised} into
- concrete source code of a target language. This step only
- produces concrete syntax but does not change the program in
- essence; all conceptual transformations occur in the translation
- step.
-
- \end{itemize}
-
- \noindent From these steps, only the last two are carried out
- outside the logic; by keeping this layer as thin as possible, the
- amount of code to trust is kept to a minimum.
-*}
-
-
-subsection {* The preprocessor \label{sec:preproc} *}
-
-text {*
- Before selected function theorems are turned into abstract code, a
- chain of definitional transformation steps is carried out:
- \emph{preprocessing}. The preprocessor consists of two
- components: a \emph{simpset} and \emph{function transformers}.
-
- The \emph{simpset} can apply the full generality of the Isabelle
- simplifier. Due to the interpretation of theorems as code
- equations, rewrites are applied to the right hand side and the
- arguments of the left hand side of an equation, but never to the
- constant heading the left hand side. An important special case are
- \emph{unfold theorems}, which may be declared and removed using the
- @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
- attribute, respectively.
-
- Some common applications:
-*}
-
-text_raw {*
- \begin{itemize}
-*}
-
-text {*
- \item replacing non-executable constructs by executable ones:
-*}
-
-lemma %quote [code_unfold]:
- "x \<in> set xs \<longleftrightarrow> List.member xs x" by (fact in_set_member)
-
-text {*
- \item replacing executable but inconvenient constructs:
-*}
-
-lemma %quote [code_unfold]:
- "xs = [] \<longleftrightarrow> List.null xs" by (fact eq_Nil_null)
-
-text {*
- \item eliminating disturbing expressions:
-*}
-
-lemma %quote [code_unfold]:
- "1 = Suc 0" by (fact One_nat_def)
-
-text_raw {*
- \end{itemize}
-*}
-
-text {*
- \noindent \emph{Function transformers} provide a very general
- interface, transforming a list of function theorems to another list
- of function theorems, provided that neither the heading constant nor
- its type change. The @{term "0\<Colon>nat"} / @{const Suc} pattern
- elimination implemented in theory @{text Efficient_Nat} (see
- \secref{eff_nat}) uses this interface.
-
- \noindent The current setup of the preprocessor may be inspected
- using the @{command_def print_codeproc} command. @{command_def
- code_thms} (see \secref{sec:equations}) provides a convenient
- mechanism to inspect the impact of a preprocessor setup on code
- equations.
-*}
-
-
-subsection {* Understanding code equations \label{sec:equations} *}
-
-text {*
- As told in \secref{sec:principle}, the notion of code equations is
- vital to code generation. Indeed most problems which occur in
- practice can be resolved by an inspection of the underlying code
- equations.
-
- It is possible to exchange the default code equations for constants
- by explicitly proving alternative ones:
-*}
-
-lemma %quote [code]:
- "dequeue (AQueue xs []) =
- (if xs = [] then (None, AQueue [] [])
- else dequeue (AQueue [] (rev xs)))"
- "dequeue (AQueue xs (y # ys)) =
- (Some y, AQueue xs ys)"
- by (cases xs, simp_all) (cases "rev xs", simp_all)
-
-text {*
- \noindent The annotation @{text "[code]"} is an @{text attribute}
- which states that the given theorems should be considered as code
- equations for a @{text fun} statement -- the corresponding constant
- is determined syntactically. The resulting code:
-*}
-
-text %quotetypewriter {*
- @{code_stmts dequeue (consts) dequeue (Haskell)}
-*}
-
-text {*
- \noindent You may note that the equality test @{term "xs = []"} has
- been replaced by the predicate @{term "List.null xs"}. This is due
- to the default setup of the \qn{preprocessor}.
-
- This possibility to select arbitrary code equations is the key
- technique for program and datatype refinement (see
- \secref{sec:refinement}).
-
- Due to the preprocessor, there is the distinction of raw code
- equations (before preprocessing) and code equations (after
- preprocessing).
-
- The first can be listed (among other data) using the @{command_def
- print_codesetup} command.
-
- The code equations after preprocessing are already are blueprint of
- the generated program and can be inspected using the @{command
- code_thms} command:
-*}
-
-code_thms %quote dequeue
-
-text {*
- \noindent This prints a table with the code equations for @{const
- dequeue}, including \emph{all} code equations those equations depend
- on recursively. These dependencies themselves can be visualized using
- the @{command_def code_deps} command.
-*}
-
-
-subsection {* Equality *}
-
-text {*
- Implementation of equality deserves some attention. Here an example
- function involving polymorphic equality:
-*}
-
-primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "collect_duplicates xs ys [] = xs"
-| "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
- then if z \<in> set ys
- then collect_duplicates xs ys zs
- else collect_duplicates xs (z#ys) zs
- else collect_duplicates (z#xs) (z#ys) zs)"
-
-text {*
- \noindent During preprocessing, the membership test is rewritten,
- resulting in @{const List.member}, which itself performs an explicit
- equality check, as can be seen in the corresponding @{text SML} code:
-*}
-
-text %quotetypewriter {*
- @{code_stmts collect_duplicates (SML)}
-*}
-
-text {*
- \noindent Obviously, polymorphic equality is implemented the Haskell
- way using a type class. How is this achieved? HOL introduces an
- explicit class @{class equal} with a corresponding operation @{const
- HOL.equal} such that @{thm equal [no_vars]}. The preprocessing
- framework does the rest by propagating the @{class equal} constraints
- through all dependent code equations. For datatypes, instances of
- @{class equal} are implicitly derived when possible. For other types,
- you may instantiate @{text equal} manually like any other type class.
-*}
-
-
-subsection {* Explicit partiality \label{sec:partiality} *}
-
-text {*
- Partiality usually enters the game by partial patterns, as
- in the following example, again for amortised queues:
-*}
-
-definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
- "strict_dequeue q = (case dequeue q
- of (Some x, q') \<Rightarrow> (x, q'))"
-
-lemma %quote strict_dequeue_AQueue [code]:
- "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
- "strict_dequeue (AQueue xs []) =
- (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
- by (simp_all add: strict_dequeue_def) (cases xs, simp_all split: list.split)
-
-text {*
- \noindent In the corresponding code, there is no equation
- for the pattern @{term "AQueue [] []"}:
-*}
-
-text %quotetypewriter {*
- @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
-*}
-
-text {*
- \noindent In some cases it is desirable to have this
- pseudo-\qt{partiality} more explicitly, e.g.~as follows:
-*}
-
-axiomatization %quote empty_queue :: 'a
-
-definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
- "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
-
-lemma %quote strict_dequeue'_AQueue [code]:
- "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
- else strict_dequeue' (AQueue [] (rev xs)))"
- "strict_dequeue' (AQueue xs (y # ys)) =
- (y, AQueue xs ys)"
- by (simp_all add: strict_dequeue'_def split: list.splits)
-
-text {*
- Observe that on the right hand side of the definition of @{const
- "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs.
-
- Normally, if constants without any code equations occur in a
- program, the code generator complains (since in most cases this is
- indeed an error). But such constants can also be thought
- of as function definitions which always fail,
- since there is never a successful pattern match on the left hand
- side. In order to categorise a constant into that category
- explicitly, use @{command_def "code_abort"}:
-*}
-
-code_abort %quote empty_queue
-
-text {*
- \noindent Then the code generator will just insert an error or
- exception at the appropriate position:
-*}
-
-text %quotetypewriter {*
- @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
-*}
-
-text {*
- \noindent This feature however is rarely needed in practice. Note
- also that the HOL default setup already declares @{const undefined}
- as @{command "code_abort"}, which is most likely to be used in such
- situations.
-*}
-
-
-subsection {* If something goes utterly wrong \label{sec:utterly_wrong} *}
-
-text {*
- Under certain circumstances, the code generator fails to produce
- code entirely. To debug these, the following hints may prove
- helpful:
-
- \begin{description}
-
- \ditem{\emph{Check with a different target language}.} Sometimes
- the situation gets more clear if you switch to another target
- language; the code generated there might give some hints what
- prevents the code generator to produce code for the desired
- language.
-
- \ditem{\emph{Inspect code equations}.} Code equations are the central
- carrier of code generation. Most problems occurring while generating
- code can be traced to single equations which are printed as part of
- the error message. A closer inspection of those may offer the key
- for solving issues (cf.~\secref{sec:equations}).
-
- \ditem{\emph{Inspect preprocessor setup}.} The preprocessor might
- transform code equations unexpectedly; to understand an
- inspection of its setup is necessary (cf.~\secref{sec:preproc}).
-
- \ditem{\emph{Generate exceptions}.} If the code generator
- complains about missing code equations, in can be helpful to
- implement the offending constants as exceptions
- (cf.~\secref{sec:partiality}); this allows at least for a formal
- generation of code, whose inspection may then give clues what is
- wrong.
-
- \ditem{\emph{Remove offending code equations}.} If code
- generation is prevented by just a single equation, this can be
- removed (cf.~\secref{sec:equations}) to allow formal code
- generation, whose result in turn can be used to trace the
- problem. The most prominent case here are mismatches in type
- class signatures (\qt{wellsortedness error}).
-
- \end{description}
-*}
-
-end
--- a/doc-src/Codegen/Further.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,351 +0,0 @@
-theory Further
-imports Setup
-begin
-
-section {* Further issues \label{sec:further} *}
-
-subsection {* Specialities of the @{text Scala} target language \label{sec:scala} *}
-
-text {*
- @{text Scala} deviates from languages of the ML family in a couple
- of aspects; those which affect code generation mainly have to do with
- @{text Scala}'s type system:
-
- \begin{itemize}
-
- \item @{text Scala} prefers tupled syntax over curried syntax.
-
- \item @{text Scala} sacrifices Hindely-Milner type inference for a
- much more rich type system with subtyping etc. For this reason
- type arguments sometimes have to be given explicitly in square
- brackets (mimicking System F syntax).
-
- \item In contrast to @{text Haskell} where most specialities of
- the type system are implemented using \emph{type classes},
- @{text Scala} provides a sophisticated system of \emph{implicit
- arguments}.
-
- \end{itemize}
-
- \noindent Concerning currying, the @{text Scala} serializer counts
- arguments in code equations to determine how many arguments
- shall be tupled; remaining arguments and abstractions in terms
- rather than function definitions are always curried.
-
- The second aspect affects user-defined adaptations with @{command
- code_const}. For regular terms, the @{text Scala} serializer prints
- all type arguments explicitly. For user-defined term adaptations
- this is only possible for adaptations which take no arguments: here
- the type arguments are just appended. Otherwise they are ignored;
- hence user-defined adaptations for polymorphic constants have to be
- designed very carefully to avoid ambiguity.
-
- Isabelle's type classes are mapped onto @{text Scala} implicits; in
- cases with diamonds in the subclass hierarchy this can lead to
- ambiguities in the generated code:
-*}
-
-class %quote class1 =
- fixes foo :: "'a \<Rightarrow> 'a"
-
-class %quote class2 = class1
-
-class %quote class3 = class1
-
-text {*
- \noindent Here both @{class class2} and @{class class3} inherit from @{class class1},
- forming the upper part of a diamond.
-*}
-
-definition %quote bar :: "'a :: {class2, class3} \<Rightarrow> 'a" where
- "bar = foo"
-
-text {*
- \noindent This yields the following code:
-*}
-
-text %quotetypewriter {*
- @{code_stmts bar (Scala)}
-*}
-
-text {*
- \noindent This code is rejected by the @{text Scala} compiler: in
- the definition of @{text bar}, it is not clear from where to derive
- the implicit argument for @{text foo}.
-
- The solution to the problem is to close the diamond by a further
- class with inherits from both @{class class2} and @{class class3}:
-*}
-
-class %quote class4 = class2 + class3
-
-text {*
- \noindent Then the offending code equation can be restricted to
- @{class class4}:
-*}
-
-lemma %quote [code]:
- "(bar :: 'a::class4 \<Rightarrow> 'a) = foo"
- by (simp only: bar_def)
-
-text {*
- \noindent with the following code:
-*}
-
-text %quotetypewriter {*
- @{code_stmts bar (Scala)}
-*}
-
-text {*
- \noindent which exposes no ambiguity.
-
- Since the preprocessor (cf.~\secref{sec:preproc}) propagates sort
- constraints through a system of code equations, it is usually not
- very difficult to identify the set of code equations which actually
- needs more restricted sort constraints.
-*}
-
-subsection {* Modules namespace *}
-
-text {*
- When invoking the @{command export_code} command it is possible to
- leave out the @{keyword "module_name"} part; then code is
- distributed over different modules, where the module name space
- roughly is induced by the Isabelle theory name space.
-
- Then sometimes the awkward situation occurs that dependencies
- between definitions introduce cyclic dependencies between modules,
- which in the @{text Haskell} world leaves you to the mercy of the
- @{text Haskell} implementation you are using, while for @{text
- SML}/@{text OCaml} code generation is not possible.
-
- A solution is to declare module names explicitly. Let use assume
- the three cyclically dependent modules are named \emph{A}, \emph{B}
- and \emph{C}. Then, by stating
-*}
-
-code_modulename %quote SML
- A ABC
- B ABC
- C ABC
-
-text {*
- \noindent we explicitly map all those modules on \emph{ABC},
- resulting in an ad-hoc merge of this three modules at serialisation
- time.
-*}
-
-subsection {* Locales and interpretation *}
-
-text {*
- A technical issue comes to surface when generating code from
- specifications stemming from locale interpretation.
-
- Let us assume a locale specifying a power operation on arbitrary
- types:
-*}
-
-locale %quote power =
- fixes power :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
- assumes power_commute: "power x \<circ> power y = power y \<circ> power x"
-begin
-
-text {*
- \noindent Inside that locale we can lift @{text power} to exponent
- lists by means of specification relative to that locale:
-*}
-
-primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
- "powers [] = id"
-| "powers (x # xs) = power x \<circ> powers xs"
-
-lemma %quote powers_append:
- "powers (xs @ ys) = powers xs \<circ> powers ys"
- by (induct xs) simp_all
-
-lemma %quote powers_power:
- "powers xs \<circ> power x = power x \<circ> powers xs"
- by (induct xs)
- (simp_all del: o_apply id_apply add: o_assoc [symmetric],
- simp del: o_apply add: o_assoc power_commute)
-
-lemma %quote powers_rev:
- "powers (rev xs) = powers xs"
- by (induct xs) (simp_all add: powers_append powers_power)
-
-end %quote
-
-text {*
- After an interpretation of this locale (say, @{command_def
- interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
- :: 'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
- "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
- can be generated. But this not the case: internally, the term
- @{text "fun_power.powers"} is an abbreviation for the foundational
- term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
- (see \cite{isabelle-locale} for the details behind).
-
- Fortunately, with minor effort the desired behaviour can be
- achieved. First, a dedicated definition of the constant on which
- the local @{text "powers"} after interpretation is supposed to be
- mapped on:
-*}
-
-definition %quote funpows :: "nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
- [code del]: "funpows = power.powers (\<lambda>n f. f ^^ n)"
-
-text {*
- \noindent In general, the pattern is @{text "c = t"} where @{text c}
- is the name of the future constant and @{text t} the foundational
- term corresponding to the local constant after interpretation.
-
- The interpretation itself is enriched with an equation @{text "t = c"}:
-*}
-
-interpretation %quote fun_power: power "\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n" where
- "power.powers (\<lambda>n f. f ^^ n) = funpows"
- by unfold_locales
- (simp_all add: fun_eq_iff funpow_mult mult_commute funpows_def)
-
-text {*
- \noindent This additional equation is trivially proved by the
- definition itself.
-
- After this setup procedure, code generation can continue as usual:
-*}
-
-text %quotetypewriter {*
- @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
-*}
-
-
-subsection {* Imperative data structures *}
-
-text {*
- If you consider imperative data structures as inevitable for a
- specific application, you should consider \emph{Imperative
- Functional Programming with Isabelle/HOL}
- \cite{bulwahn-et-al:2008:imperative}; the framework described there
- is available in session @{text Imperative_HOL}, together with a
- short primer document.
-*}
-
-
-subsection {* ML system interfaces \label{sec:ml} *}
-
-text {*
- Since the code generator framework not only aims to provide a nice
- Isar interface but also to form a base for code-generation-based
- applications, here a short description of the most fundamental ML
- interfaces.
-*}
-
-subsubsection {* Managing executable content *}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML Code.read_const: "theory -> string -> string"} \\
- @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
- @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
- @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
- @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
- @{index_ML Code_Preproc.add_functrans: "
- string * (theory -> (thm * bool) list -> (thm * bool) list option)
- -> theory -> theory"} \\
- @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
- @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
- @{index_ML Code.get_type: "theory -> string
- -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool"} \\
- @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML Code.read_const}~@{text thy}~@{text s}
- reads a constant as a concrete term expression @{text s}.
-
- \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
- theorem @{text "thm"} to executable content.
-
- \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
- theorem @{text "thm"} from executable content, if present.
-
- \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
- the preprocessor simpset.
-
- \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
- function transformer @{text f} (named @{text name}) to executable content;
- @{text f} is a transformer of the code equations belonging
- to a certain function definition, depending on the
- current theory context. Returning @{text NONE} indicates that no
- transformation took place; otherwise, the whole process will be iterated
- with the new code equations.
-
- \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
- function transformer named @{text name} from executable content.
-
- \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
- a datatype to executable content, with generation
- set @{text cs}.
-
- \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
- returns type constructor corresponding to
- constructor @{text const}; returns @{text NONE}
- if @{text const} is no constructor.
-
- \end{description}
-*}
-
-
-subsubsection {* Data depending on the theory's executable content *}
-
-text {*
- Implementing code generator applications on top of the framework set
- out so far usually not only involves using those primitive
- interfaces but also storing code-dependent data and various other
- things.
-
- Due to incrementality of code generation, changes in the theory's
- executable content have to be propagated in a certain fashion.
- Additionally, such changes may occur not only during theory
- extension but also during theory merge, which is a little bit nasty
- from an implementation point of view. The framework provides a
- solution to this technical challenge by providing a functorial data
- slot @{ML_functor Code_Data}; on instantiation of this functor, the
- following types and operations are required:
-
- \medskip
- \begin{tabular}{l}
- @{text "type T"} \\
- @{text "val empty: T"} \\
- \end{tabular}
-
- \begin{description}
-
- \item @{text T} the type of data to store.
-
- \item @{text empty} initial (empty) data.
-
- \end{description}
-
- \noindent An instance of @{ML_functor Code_Data} provides the
- following interface:
-
- \medskip
- \begin{tabular}{l}
- @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
- @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
- \end{tabular}
-
- \begin{description}
-
- \item @{text change} update of current data (cached!) by giving a
- continuation.
-
- \item @{text change_yield} update with side result.
-
- \end{description}
-*}
-
-end
-
--- a/doc-src/Codegen/Inductive_Predicate.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,275 +0,0 @@
-theory Inductive_Predicate
-imports Setup
-begin
-
-(*<*)
-hide_const %invisible append
-
-inductive %invisible append where
- "append [] ys ys"
-| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
-
-lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
- by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
-
-lemmas lexordp_def =
- lexordp_def [unfolded lexord_def mem_Collect_eq split]
-(*>*)
-
-section {* Inductive Predicates \label{sec:inductive} *}
-
-text {*
- The @{text "predicate compiler"} is an extension of the code generator
- which turns inductive specifications into equational ones, from
- which in turn executable code can be generated. The mechanisms of
- this compiler are described in detail in
- \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
-
- Consider the simple predicate @{const append} given by these two
- introduction rules:
-*}
-
-text %quote {*
- @{thm append.intros(1)[of ys]} \\
- @{thm append.intros(2)[of xs ys zs x]}
-*}
-
-text {*
- \noindent To invoke the compiler, simply use @{command_def "code_pred"}:
-*}
-
-code_pred %quote append .
-
-text {*
- \noindent The @{command "code_pred"} command takes the name of the
- inductive predicate and then you put a period to discharge a trivial
- correctness proof. The compiler infers possible modes for the
- predicate and produces the derived code equations. Modes annotate
- which (parts of the) arguments are to be taken as input, and which
- output. Modes are similar to types, but use the notation @{text "i"}
- for input and @{text "o"} for output.
-
- For @{term "append"}, the compiler can infer the following modes:
- \begin{itemize}
- \item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
- \item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
- \item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
- \end{itemize}
- You can compute sets of predicates using @{command_def "values"}:
-*}
-
-values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
-
-text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
-
-values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
-
-text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
-
-text {*
- \noindent If you are only interested in the first elements of the
- set comprehension (with respect to a depth-first search on the
- introduction rules), you can pass an argument to @{command "values"}
- to specify the number of elements you want:
-*}
-
-values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
-values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
-
-text {*
- \noindent The @{command "values"} command can only compute set
- comprehensions for which a mode has been inferred.
-
- The code equations for a predicate are made available as theorems with
- the suffix @{text "equation"}, and can be inspected with:
-*}
-
-thm %quote append.equation
-
-text {*
- \noindent More advanced options are described in the following subsections.
-*}
-
-subsection {* Alternative names for functions *}
-
-text {*
- By default, the functions generated from a predicate are named after
- the predicate with the mode mangled into the name (e.g., @{text
- "append_i_i_o"}). You can specify your own names as follows:
-*}
-
-code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat,
- o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split,
- i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append .
-
-subsection {* Alternative introduction rules *}
-
-text {*
- Sometimes the introduction rules of an predicate are not executable
- because they contain non-executable constants or specific modes
- could not be inferred. It is also possible that the introduction
- rules yield a function that loops forever due to the execution in a
- depth-first search manner. Therefore, you can declare alternative
- introduction rules for predicates with the attribute @{attribute
- "code_pred_intro"}. For example, the transitive closure is defined
- by:
-*}
-
-text %quote {*
- @{lemma [source] "r a b \<Longrightarrow> tranclp r a b" by (fact tranclp.intros(1))}\\
- @{lemma [source] "tranclp r a b \<Longrightarrow> r b c \<Longrightarrow> tranclp r a c" by (fact tranclp.intros(2))}
-*}
-
-text {*
- \noindent These rules do not suit well for executing the transitive
- closure with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as
- the second rule will cause an infinite loop in the recursive call.
- This can be avoided using the following alternative rules which are
- declared to the predicate compiler by the attribute @{attribute
- "code_pred_intro"}:
-*}
-
-lemma %quote [code_pred_intro]:
- "r a b \<Longrightarrow> tranclp r a b"
- "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
-by auto
-
-text {*
- \noindent After declaring all alternative rules for the transitive
- closure, you invoke @{command "code_pred"} as usual. As you have
- declared alternative rules for the predicate, you are urged to prove
- that these introduction rules are complete, i.e., that you can
- derive an elimination rule for the alternative rules:
-*}
-
-code_pred %quote tranclp
-proof -
- case tranclp
- from this converse_tranclpE [OF tranclp.prems] show thesis by metis
-qed
-
-text {*
- \noindent Alternative rules can also be used for constants that have
- not been defined inductively. For example, the lexicographic order
- which is defined as:
-*}
-
-text %quote {*
- @{thm [display] lexordp_def [of r]}
-*}
-
-text {*
- \noindent To make it executable, you can derive the following two
- rules and prove the elimination rule:
-*}
-
-lemma %quote [code_pred_intro]:
- "append xs (a # v) ys \<Longrightarrow> lexordp r xs ys"
-(*<*)unfolding lexordp_def by (auto simp add: append)(*>*)
-
-lemma %quote [code_pred_intro]:
- "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b
- \<Longrightarrow> lexordp r xs ys"
-(*<*)unfolding lexordp_def append apply simp
-apply (rule disjI2) by auto(*>*)
-
-code_pred %quote lexordp
-(*<*)proof -
- fix r xs ys
- assume lexord: "lexordp r xs ys"
- assume 1: "\<And>r' xs' ys' a v. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
- \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
- assume 2: "\<And>r' xs' ys' u a v b w. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
- \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> thesis"
- {
- assume "\<exists>a v. ys = xs @ a # v"
- from this 1 have thesis
- by (fastforce simp add: append)
- } moreover
- {
- assume "\<exists>u a b v w. r a b \<and> xs = u @ a # v \<and> ys = u @ b # w"
- from this 2 have thesis by (fastforce simp add: append)
- } moreover
- note lexord
- ultimately show thesis
- unfolding lexordp_def
- by fastforce
-qed(*>*)
-
-
-subsection {* Options for values *}
-
-text {*
- In the presence of higher-order predicates, multiple modes for some
- predicate could be inferred that are not disambiguated by the
- pattern of the set comprehension. To disambiguate the modes for the
- arguments of a predicate, you can state the modes explicitly in the
- @{command "values"} command. Consider the simple predicate @{term
- "succ"}:
-*}
-
-inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
- "succ 0 (Suc 0)"
-| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
-
-code_pred %quote succ .
-
-text {*
- \noindent For this, the predicate compiler can infer modes @{text "o
- \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"}, @{text "o \<Rightarrow> i \<Rightarrow> bool"} and
- @{text "i \<Rightarrow> i \<Rightarrow> bool"}. The invocation of @{command "values"}
- @{text "{n. tranclp succ 10 n}"} loops, as multiple modes for the
- predicate @{text "succ"} are possible and here the first mode @{text
- "o \<Rightarrow> o \<Rightarrow> bool"} is chosen. To choose another mode for the argument,
- you can declare the mode for the argument between the @{command
- "values"} and the number of elements.
-*}
-
-values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIMXE does not terminate for n\<ge>1*)
-values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}"
-
-
-subsection {* Embedding into functional code within Isabelle/HOL *}
-
-text {*
- To embed the computation of an inductive predicate into functions
- that are defined in Isabelle/HOL, you have a number of options:
-
- \begin{itemize}
-
- \item You want to use the first-order predicate with the mode
- where all arguments are input. Then you can use the predicate directly, e.g.
-
- \begin{quote}
- @{text "valid_suffix ys zs = "} \\
- @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
- \end{quote}
-
- \item If you know that the execution returns only one value (it is
- deterministic), then you can use the combinator @{term
- "Predicate.the"}, e.g., a functional concatenation of lists is
- defined with
-
- \begin{quote}
- @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
- \end{quote}
-
- Note that if the evaluation does not return a unique value, it
- raises a run-time error @{term "not_unique"}.
-
- \end{itemize}
-*}
-
-
-subsection {* Further Examples *}
-
-text {*
- Further examples for compiling inductive predicates can be found in
- the @{text "HOL/ex/Predicate_Compile_ex.thy"} theory file. There are
- also some examples in the Archive of Formal Proofs, notably in the
- @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
- sessions.
-*}
-
-end
-
--- a/doc-src/Codegen/Introduction.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,242 +0,0 @@
-theory Introduction
-imports Setup
-begin
-
-section {* Introduction *}
-
-text {*
- This tutorial introduces the code generator facilities of @{text
- "Isabelle/HOL"}. It allows to turn (a certain class of) HOL
- specifications into corresponding executable code in the programming
- languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml},
- @{text Haskell} \cite{haskell-revised-report} and @{text Scala}
- \cite{scala-overview-tech-report}.
-
- To profit from this tutorial, some familiarity and experience with
- @{theory HOL} \cite{isa-tutorial} and its basic theories is assumed.
-*}
-
-
-subsection {* Code generation principle: shallow embedding \label{sec:principle} *}
-
-text {*
- The key concept for understanding Isabelle's code generation is
- \emph{shallow embedding}: logical entities like constants, types and
- classes are identified with corresponding entities in the target
- language. In particular, the carrier of a generated program's
- semantics are \emph{equational theorems} from the logic. If we view
- a generated program as an implementation of a higher-order rewrite
- system, then every rewrite step performed by the program can be
- simulated in the logic, which guarantees partial correctness
- \cite{Haftmann-Nipkow:2010:code}.
-*}
-
-
-subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
-
-text {*
- In a HOL theory, the @{command_def datatype} and @{command_def
- definition}/@{command_def primrec}/@{command_def fun} declarations
- form the core of a functional programming language. By default
- equational theorems stemming from those are used for generated code,
- therefore \qt{naive} code generation can proceed without further
- ado.
-
- For example, here a simple \qt{implementation} of amortised queues:
-*}
-
-datatype %quote 'a queue = AQueue "'a list" "'a list"
-
-definition %quote empty :: "'a queue" where
- "empty = AQueue [] []"
-
-primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
- "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
-
-fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
- "dequeue (AQueue [] []) = (None, AQueue [] [])"
- | "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
- | "dequeue (AQueue xs []) =
- (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))" (*<*)
-
-lemma %invisible dequeue_nonempty_Nil [simp]:
- "xs \<noteq> [] \<Longrightarrow> dequeue (AQueue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))"
- by (cases xs) (simp_all split: list.splits) (*>*)
-
-text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
-
-export_code %quote empty dequeue enqueue in SML
- module_name Example file "examples/example.ML"
-
-text {* \noindent resulting in the following code: *}
-
-text %quotetypewriter {*
- @{code_stmts empty enqueue dequeue (SML)}
-*}
-
-text {*
- \noindent The @{command_def export_code} command takes a
- space-separated list of constants for which code shall be generated;
- anything else needed for those is added implicitly. Then follows a
- target language identifier and a freely chosen module name. A file
- name denotes the destination to store the generated code. Note that
- the semantics of the destination depends on the target language: for
- @{text SML}, @{text OCaml} and @{text Scala} it denotes a \emph{file},
- for @{text Haskell} it denotes a \emph{directory} where a file named as the
- module name (with extension @{text ".hs"}) is written:
-*}
-
-export_code %quote empty dequeue enqueue in Haskell
- module_name Example file "examples/"
-
-text {*
- \noindent This is the corresponding code:
-*}
-
-text %quotetypewriter {*
- @{code_stmts empty enqueue dequeue (Haskell)}
-*}
-
-text {*
- \noindent For more details about @{command export_code} see
- \secref{sec:further}.
-*}
-
-
-subsection {* Type classes *}
-
-text {*
- Code can also be generated from type classes in a Haskell-like
- manner. For illustration here an example from abstract algebra:
-*}
-
-class %quote semigroup =
- fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
- assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
-
-class %quote monoid = semigroup +
- fixes neutral :: 'a ("\<one>")
- assumes neutl: "\<one> \<otimes> x = x"
- and neutr: "x \<otimes> \<one> = x"
-
-instantiation %quote nat :: monoid
-begin
-
-primrec %quote mult_nat where
- "0 \<otimes> n = (0\<Colon>nat)"
- | "Suc m \<otimes> n = n + m \<otimes> n"
-
-definition %quote neutral_nat where
- "\<one> = Suc 0"
-
-lemma %quote add_mult_distrib:
- fixes n m q :: nat
- shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
- by (induct n) simp_all
-
-instance %quote proof
- fix m n q :: nat
- show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
- by (induct m) (simp_all add: add_mult_distrib)
- show "\<one> \<otimes> n = n"
- by (simp add: neutral_nat_def)
- show "m \<otimes> \<one> = m"
- by (induct m) (simp_all add: neutral_nat_def)
-qed
-
-end %quote
-
-text {*
- \noindent We define the natural operation of the natural numbers
- on monoids:
-*}
-
-primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
- "pow 0 a = \<one>"
- | "pow (Suc n) a = a \<otimes> pow n a"
-
-text {*
- \noindent This we use to define the discrete exponentiation
- function:
-*}
-
-definition %quote bexp :: "nat \<Rightarrow> nat" where
- "bexp n = pow n (Suc (Suc 0))"
-
-text {*
- \noindent The corresponding code in Haskell uses that language's
- native classes:
-*}
-
-text %quotetypewriter {*
- @{code_stmts bexp (Haskell)}
-*}
-
-text {*
- \noindent This is a convenient place to show how explicit dictionary
- construction manifests in generated code -- the same example in
- @{text SML}:
-*}
-
-text %quotetypewriter {*
- @{code_stmts bexp (SML)}
-*}
-
-text {*
- \noindent Note the parameters with trailing underscore (@{verbatim
- "A_"}), which are the dictionary parameters.
-*}
-
-
-subsection {* How to continue from here *}
-
-text {*
- What you have seen so far should be already enough in a lot of
- cases. If you are content with this, you can quit reading here.
-
- Anyway, to understand situations where problems occur or to increase
- the scope of code generation beyond default, it is necessary to gain
- some understanding how the code generator actually works:
-
- \begin{itemize}
-
- \item The foundations of the code generator are described in
- \secref{sec:foundations}.
-
- \item In particular \secref{sec:utterly_wrong} gives hints how to
- debug situations where code generation does not succeed as
- expected.
-
- \item The scope and quality of generated code can be increased
- dramatically by applying refinement techniques, which are
- introduced in \secref{sec:refinement}.
-
- \item Inductive predicates can be turned executable using an
- extension of the code generator \secref{sec:inductive}.
-
- \item If you want to utilize code generation to obtain fast
- evaluators e.g.~for decision procedures, have a look at
- \secref{sec:evaluation}.
-
- \item You may want to skim over the more technical sections
- \secref{sec:adaptation} and \secref{sec:further}.
-
- \item The target language Scala \cite{scala-overview-tech-report}
- comes with some specialities discussed in \secref{sec:scala}.
-
- \item For exhaustive syntax diagrams etc. you should visit the
- Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.
-
- \end{itemize}
-
- \bigskip
-
- \begin{center}\fbox{\fbox{\begin{minipage}{8cm}
-
- \begin{center}\textit{Happy proving, happy hacking!}\end{center}
-
- \end{minipage}}}\end{center}
-*}
-
-end
-
--- a/doc-src/Codegen/Refinement.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,274 +0,0 @@
-theory Refinement
-imports Setup
-begin
-
-section {* Program and datatype refinement \label{sec:refinement} *}
-
-text {*
- Code generation by shallow embedding (cf.~\secref{sec:principle})
- allows to choose code equations and datatype constructors freely,
- given that some very basic syntactic properties are met; this
- flexibility opens up mechanisms for refinement which allow to extend
- the scope and quality of generated code dramatically.
-*}
-
-
-subsection {* Program refinement *}
-
-text {*
- Program refinement works by choosing appropriate code equations
- explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci
- numbers:
-*}
-
-fun %quote fib :: "nat \<Rightarrow> nat" where
- "fib 0 = 0"
- | "fib (Suc 0) = Suc 0"
- | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
-
-text {*
- \noindent The runtime of the corresponding code grows exponential due
- to two recursive calls:
-*}
-
-text %quotetypewriter {*
- @{code_stmts fib (consts) fib (Haskell)}
-*}
-
-text {*
- \noindent A more efficient implementation would use dynamic
- programming, e.g.~sharing of common intermediate results between
- recursive calls. This idea is expressed by an auxiliary operation
- which computes a Fibonacci number and its successor simultaneously:
-*}
-
-definition %quote fib_step :: "nat \<Rightarrow> nat \<times> nat" where
- "fib_step n = (fib (Suc n), fib n)"
-
-text {*
- \noindent This operation can be implemented by recursion using
- dynamic programming:
-*}
-
-lemma %quote [code]:
- "fib_step 0 = (Suc 0, 0)"
- "fib_step (Suc n) = (let (m, q) = fib_step n in (m + q, m))"
- by (simp_all add: fib_step_def)
-
-text {*
- \noindent What remains is to implement @{const fib} by @{const
- fib_step} as follows:
-*}
-
-lemma %quote [code]:
- "fib 0 = 0"
- "fib (Suc n) = fst (fib_step n)"
- by (simp_all add: fib_step_def)
-
-text {*
- \noindent The resulting code shows only linear growth of runtime:
-*}
-
-text %quotetypewriter {*
- @{code_stmts fib (consts) fib fib_step (Haskell)}
-*}
-
-
-subsection {* Datatype refinement *}
-
-text {*
- Selecting specific code equations \emph{and} datatype constructors
- leads to datatype refinement. As an example, we will develop an
- alternative representation of the queue example given in
- \secref{sec:queue_example}. The amortised representation is
- convenient for generating code but exposes its \qt{implementation}
- details, which may be cumbersome when proving theorems about it.
- Therefore, here is a simple, straightforward representation of
- queues:
-*}
-
-datatype %quote 'a queue = Queue "'a list"
-
-definition %quote empty :: "'a queue" where
- "empty = Queue []"
-
-primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
- "enqueue x (Queue xs) = Queue (xs @ [x])"
-
-fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
- "dequeue (Queue []) = (None, Queue [])"
- | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
-
-text {*
- \noindent This we can use directly for proving; for executing,
- we provide an alternative characterisation:
-*}
-
-definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
- "AQueue xs ys = Queue (ys @ rev xs)"
-
-code_datatype %quote AQueue
-
-text {*
- \noindent Here we define a \qt{constructor} @{const "AQueue"} which
- is defined in terms of @{text "Queue"} and interprets its arguments
- according to what the \emph{content} of an amortised queue is supposed
- to be.
-
- The prerequisite for datatype constructors is only syntactical: a
- constructor must be of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
- "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
- @{text "\<tau>"}; then @{text "\<kappa>"} is its corresponding datatype. The
- HOL datatype package by default registers any new datatype with its
- constructors, but this may be changed using @{command_def
- code_datatype}; the currently chosen constructors can be inspected
- using the @{command print_codesetup} command.
-
- Equipped with this, we are able to prove the following equations
- for our primitive queue operations which \qt{implement} the simple
- queues in an amortised fashion:
-*}
-
-lemma %quote empty_AQueue [code]:
- "empty = AQueue [] []"
- by (simp add: AQueue_def empty_def)
-
-lemma %quote enqueue_AQueue [code]:
- "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
- by (simp add: AQueue_def)
-
-lemma %quote dequeue_AQueue [code]:
- "dequeue (AQueue xs []) =
- (if xs = [] then (None, AQueue [] [])
- else dequeue (AQueue [] (rev xs)))"
- "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
- by (simp_all add: AQueue_def)
-
-text {*
- \noindent It is good style, although no absolute requirement, to
- provide code equations for the original artefacts of the implemented
- type, if possible; in our case, these are the datatype constructor
- @{const Queue} and the case combinator @{const queue_case}:
-*}
-
-lemma %quote Queue_AQueue [code]:
- "Queue = AQueue []"
- by (simp add: AQueue_def fun_eq_iff)
-
-lemma %quote queue_case_AQueue [code]:
- "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
- by (simp add: AQueue_def)
-
-text {*
- \noindent The resulting code looks as expected:
-*}
-
-text %quotetypewriter {*
- @{code_stmts empty enqueue dequeue Queue queue_case (SML)}
-*}
-
-text {*
- The same techniques can also be applied to types which are not
- specified as datatypes, e.g.~type @{typ int} is originally specified
- as quotient type by means of @{command_def typedef}, but for code
- generation constants allowing construction of binary numeral values
- are used as constructors for @{typ int}.
-
- This approach however fails if the representation of a type demands
- invariants; this issue is discussed in the next section.
-*}
-
-
-subsection {* Datatype refinement involving invariants \label{sec:invariant} *}
-
-text {*
- Datatype representation involving invariants require a dedicated
- setup for the type and its primitive operations. As a running
- example, we implement a type @{text "'a dlist"} of list consisting
- of distinct elements.
-
- The first step is to decide on which representation the abstract
- type (in our example @{text "'a dlist"}) should be implemented.
- Here we choose @{text "'a list"}. Then a conversion from the concrete
- type to the abstract type must be specified, here:
-*}
-
-text %quote {*
- @{term_type Dlist}
-*}
-
-text {*
- \noindent Next follows the specification of a suitable \emph{projection},
- i.e.~a conversion from abstract to concrete type:
-*}
-
-text %quote {*
- @{term_type list_of_dlist}
-*}
-
-text {*
- \noindent This projection must be specified such that the following
- \emph{abstract datatype certificate} can be proven:
-*}
-
-lemma %quote [code abstype]:
- "Dlist (list_of_dlist dxs) = dxs"
- by (fact Dlist_list_of_dlist)
-
-text {*
- \noindent Note that so far the invariant on representations
- (@{term_type distinct}) has never been mentioned explicitly:
- the invariant is only referred to implicitly: all values in
- set @{term "{xs. list_of_dlist (Dlist xs) = xs}"} are invariant,
- and in our example this is exactly @{term "{xs. distinct xs}"}.
-
- The primitive operations on @{typ "'a dlist"} are specified
- indirectly using the projection @{const list_of_dlist}. For
- the empty @{text "dlist"}, @{const Dlist.empty}, we finally want
- the code equation
-*}
-
-text %quote {*
- @{term "Dlist.empty = Dlist []"}
-*}
-
-text {*
- \noindent This we have to prove indirectly as follows:
-*}
-
-lemma %quote [code abstract]:
- "list_of_dlist Dlist.empty = []"
- by (fact list_of_dlist_empty)
-
-text {*
- \noindent This equation logically encodes both the desired code
- equation and that the expression @{const Dlist} is applied to obeys
- the implicit invariant. Equations for insertion and removal are
- similar:
-*}
-
-lemma %quote [code abstract]:
- "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
- by (fact list_of_dlist_insert)
-
-lemma %quote [code abstract]:
- "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
- by (fact list_of_dlist_remove)
-
-text {*
- \noindent Then the corresponding code is as follows:
-*}
-
-text %quotetypewriter {*
- @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
-*} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *)
-
-text {*
- Typical data structures implemented by representations involving
- invariants are available in the library, theory @{theory Mapping}
- specifies key-value-mappings (type @{typ "('a, 'b) mapping"});
- these can be implemented by red-black-trees (theory @{theory RBT}).
-*}
-
-end
-
--- a/doc-src/Codegen/Setup.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-theory Setup
-imports
- Complex_Main
- "~~/src/HOL/Library/Dlist"
- "~~/src/HOL/Library/RBT"
- "~~/src/HOL/Library/Mapping"
-begin
-
-(* FIXME avoid writing into source directory *)
-ML {*
- Isabelle_System.mkdirs (Path.append (Thy_Load.master_directory @{theory}) (Path.basic "examples"))
-*}
-
-ML_file "../antiquote_setup.ML"
-ML_file "../more_antiquote.ML"
-
-setup {*
- Antiquote_Setup.setup #>
- More_Antiquote.setup #>
-let
- val typ = Simple_Syntax.read_typ;
-in
- Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
- [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
- Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
- [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
-end
-*}
-
-setup {* Code_Target.set_default_code_width 74 *}
-
-declare [[names_unique = false]]
-
-end
-
--- a/doc-src/Codegen/document/adapt.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-
-\documentclass[12pt]{article}
-\usepackage{tikz}
-
-\begin{document}
-
-\thispagestyle{empty}
-\setlength{\fboxrule}{0.01pt}
-\setlength{\fboxsep}{4pt}
-
-\fcolorbox{white}{white}{
-
-\begin{tikzpicture}[scale = 0.5]
- \tikzstyle water=[color = blue, thick]
- \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
- \tikzstyle process=[color = green, semithick, ->]
- \tikzstyle adaptation=[color = red, semithick, ->]
- \tikzstyle target=[color = black]
- \foreach \x in {0, ..., 24}
- \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
- + (0.25, -0.25) cos + (0.25, 0.25);
- \draw[style=ice] (1, 0) --
- (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
- \draw[style=ice] (9, 0) --
- (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
- \draw[style=ice] (15, -6) --
- (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
- \draw[style=process]
- (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
- \draw[style=process]
- (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
- \node (adaptation) at (11, -2) [style=adaptation] {adaptation};
- \node at (19, 3) [rotate=90] {generated};
- \node at (19.5, -5) {language};
- \node at (19.5, -3) {library};
- \node (includes) at (19.5, -1) {includes};
- \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
- \draw[style=process]
- (includes) -- (serialisation);
- \draw[style=process]
- (reserved) -- (serialisation);
- \draw[style=adaptation]
- (adaptation) -- (serialisation);
- \draw[style=adaptation]
- (adaptation) -- (includes);
- \draw[style=adaptation]
- (adaptation) -- (reserved);
-\end{tikzpicture}
-
-}
-
-\end{document}
--- a/doc-src/Codegen/document/architecture.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-
-\documentclass[12pt]{article}
-\usepackage{tikz}
-\usetikzlibrary{shapes}
-\usetikzlibrary{arrows}
-
-\begin{document}
-
-\thispagestyle{empty}
-\setlength{\fboxrule}{0.01pt}
-\setlength{\fboxsep}{4pt}
-
-\fcolorbox{white}{white}{
-
-\newcommand{\sys}[1]{\emph{#1}}
-
-\begin{tikzpicture}[x = 4cm, y = 1cm]
- \tikzstyle positive=[color = black, fill = white];
- \tikzstyle negative=[color = white, fill = black];
- \tikzstyle entity=[rounded corners, draw, thick];
- \tikzstyle process=[ellipse, draw, thick];
- \tikzstyle arrow=[-stealth, semithick];
- \node (spec) at (0, 3) [entity, positive] {specification tools};
- \node (user) at (1, 3) [entity, positive] {user proofs};
- \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
- \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
- \node (pre) at (1.5, 4) [process, positive] {preprocessing};
- \node (eqn) at (2.5, 4) [entity, positive] {code equations};
- \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
- \node (seri) at (1.5, 0) [process, positive] {serialisation};
- \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
- \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
- \node (Haskell) at (2.5, 1) [entity, positive] {\sys{Haskell}};
- \node (Scala) at (2.5, 0) [entity, positive] {\sys{Scala}};
- \draw [semithick] (spec) -- (spec_user_join);
- \draw [semithick] (user) -- (spec_user_join);
- \draw [-diamond, semithick] (spec_user_join) -- (raw);
- \draw [arrow] (raw) -- (pre);
- \draw [arrow] (pre) -- (eqn);
- \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
- \draw [arrow] (iml) -- (seri);
- \draw [arrow] (seri) -- (SML);
- \draw [arrow] (seri) -- (OCaml);
- \draw [arrow] (seri) -- (Haskell);
- \draw [arrow] (seri) -- (Scala);
-\end{tikzpicture}
-
-}
-
-\end{document}
--- a/doc-src/Codegen/document/build Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-#!/bin/bash
-
-set -e
-
-FORMAT="$1"
-VARIANT="$2"
-
-"$ISABELLE_TOOL" logo -o isabelle_isar.pdf "Isar"
-"$ISABELLE_TOOL" logo -o isabelle_isar.eps "Isar"
-
-cp "$ISABELLE_HOME/doc-src/iman.sty" .
-cp "$ISABELLE_HOME/doc-src/extra.sty" .
-cp "$ISABELLE_HOME/doc-src/isar.sty" .
-cp "$ISABELLE_HOME/doc-src/proof.sty" .
-cp "$ISABELLE_HOME/doc-src/manual.bib" .
-
-for NAME in architecture adapt
-do
- latex "$NAME"
- $ISABELLE_DVIPS -E -o "$NAME.eps" "$NAME.dvi"
- $ISABELLE_EPSTOPDF "$NAME.eps"
-done
-
-"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
-
--- a/doc-src/Codegen/document/root.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-
-\documentclass[12pt,a4paper,fleqn]{article}
-\usepackage{latexsym,graphicx}
-\usepackage{multirow}
-\usepackage{iman,extra,isar,proof}
-\usepackage{isabelle,isabellesym}
-\usepackage{style}
-\usepackage{pdfsetup}
-
-\hyphenation{Isabelle}
-\hyphenation{Isar}
-\isadroptag{theory}
-
-\title{\includegraphics[scale=0.5]{isabelle_isar}
- \\[4ex] Code generation from Isabelle/HOL theories}
-\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
-
-\begin{document}
-
-\maketitle
-
-\begin{abstract}
- \noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
- They empower the user to turn HOL specifications into corresponding executable
- programs in the languages SML, OCaml, Haskell and Scala.
-\end{abstract}
-
-\thispagestyle{empty}\clearpage
-
-\pagenumbering{roman}
-\clearfirst
-
-\input{Introduction.tex}
-\input{Foundations.tex}
-\input{Refinement.tex}
-\input{Inductive_Predicate.tex}
-\input{Adaptation.tex}
-\input{Evaluation.tex}
-\input{Further.tex}
-
-\begingroup
-\bibliographystyle{plain} \small\raggedright\frenchspacing
-\bibliography{manual}
-\endgroup
-
-\end{document}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
--- a/doc-src/Codegen/document/style.sty Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-
-%% toc
-\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
-\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
-
-%% paragraphs
-\setlength{\parindent}{1em}
-
-%% references
-\newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\figref}[1]{figure~\ref{#1}}
-
-%% logical markup
-\newcommand{\strong}[1]{{\bfseries {#1}}}
-\newcommand{\qn}[1]{\emph{#1}}
-
-%% typographic conventions
-\newcommand{\qt}[1]{``{#1}''}
-\newcommand{\ditem}[1]{\item[\isastyletext #1]}
-
-%% quote environment
-\isakeeptag{quote}
-\renewenvironment{quote}
- {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
- {\endlist}
-\renewcommand{\isatagquote}{\begin{quote}}
-\renewcommand{\endisatagquote}{\end{quote}}
-\newcommand{\quotebreak}{\\[1.2ex]}
-
-%% typewriter text
-\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
-\renewcommand{\isadigit}[1]{{##1}}%
-\parindent0pt%
-\makeatletter\isa@parindent0pt\makeatother%
-\isabellestyle{tt}\isastyle%
-\fontsize{9pt}{9pt}\selectfont}{}
-
-\isakeeptag{quotetypewriter}
-\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
-\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
-
-\isakeeptag{quotett}
-\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagquotett}{\end{quote}}
-
-%% a trick
-\newcommand{\isasymSML}{SML}
-\newcommand{\isasymSMLdummy}{SML}
-
-%% presentation
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
-
-%% character detail
-\renewcommand{\isadigit}[1]{\isamath{#1}}
-\binperiod
-\underscoreoff
-
-%% format
-\pagestyle{headings}
-\isabellestyle{it}
-
-%% ml reference
-\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
-
-\isakeeptag{mlref}
-\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
-\renewcommand{\endisatagmlref}{\endgroup}
-
-\isabellestyle{it}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "implementation"
-%%% End:
--- a/doc-src/Functions/Functions.thy Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1190 +0,0 @@
-(* Title: doc-src/IsarAdvanced/Functions/Thy/Fundefs.thy
- Author: Alexander Krauss, TU Muenchen
-
-Tutorial for function definitions with the new "function" package.
-*)
-
-theory Functions
-imports Main
-begin
-
-section {* Function Definitions for Dummies *}
-
-text {*
- In most cases, defining a recursive function is just as simple as other definitions:
-*}
-
-fun fib :: "nat \<Rightarrow> nat"
-where
- "fib 0 = 1"
-| "fib (Suc 0) = 1"
-| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
-
-text {*
- The syntax is rather self-explanatory: We introduce a function by
- giving its name, its type,
- and a set of defining recursive equations.
- If we leave out the type, the most general type will be
- inferred, which can sometimes lead to surprises: Since both @{term
- "1::nat"} and @{text "+"} are overloaded, we would end up
- with @{text "fib :: nat \<Rightarrow> 'a::{one,plus}"}.
-*}
-
-text {*
- The function always terminates, since its argument gets smaller in
- every recursive call.
- Since HOL is a logic of total functions, termination is a
- fundamental requirement to prevent inconsistencies\footnote{From the
- \qt{definition} @{text "f(n) = f(n) + 1"} we could prove
- @{text "0 = 1"} by subtracting @{text "f(n)"} on both sides.}.
- Isabelle tries to prove termination automatically when a definition
- is made. In \S\ref{termination}, we will look at cases where this
- fails and see what to do then.
-*}
-
-subsection {* Pattern matching *}
-
-text {* \label{patmatch}
- Like in functional programming, we can use pattern matching to
- define functions. At the moment we will only consider \emph{constructor
- patterns}, which only consist of datatype constructors and
- variables. Furthermore, patterns must be linear, i.e.\ all variables
- on the left hand side of an equation must be distinct. In
- \S\ref{genpats} we discuss more general pattern matching.
-
- If patterns overlap, the order of the equations is taken into
- account. The following function inserts a fixed element between any
- two elements of a list:
-*}
-
-fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
- "sep a (x#y#xs) = x # a # sep a (y # xs)"
-| "sep a xs = xs"
-
-text {*
- Overlapping patterns are interpreted as \qt{increments} to what is
- already there: The second equation is only meant for the cases where
- the first one does not match. Consequently, Isabelle replaces it
- internally by the remaining cases, making the patterns disjoint:
-*}
-
-thm sep.simps
-
-text {* @{thm [display] sep.simps[no_vars]} *}
-
-text {*
- \noindent The equations from function definitions are automatically used in
- simplification:
-*}
-
-lemma "sep 0 [1, 2, 3] = [1, 0, 2, 0, 3]"
-by simp
-
-subsection {* Induction *}
-
-text {*
-
- Isabelle provides customized induction rules for recursive
- functions. These rules follow the recursive structure of the
- definition. Here is the rule @{text sep.induct} arising from the
- above definition of @{const sep}:
-
- @{thm [display] sep.induct}
-
- We have a step case for list with at least two elements, and two
- base cases for the zero- and the one-element list. Here is a simple
- proof about @{const sep} and @{const map}
-*}
-
-lemma "map f (sep x ys) = sep (f x) (map f ys)"
-apply (induct x ys rule: sep.induct)
-
-txt {*
- We get three cases, like in the definition.
-
- @{subgoals [display]}
-*}
-
-apply auto
-done
-text {*
-
- With the \cmd{fun} command, you can define about 80\% of the
- functions that occur in practice. The rest of this tutorial explains
- the remaining 20\%.
-*}
-
-
-section {* fun vs.\ function *}
-
-text {*
- The \cmd{fun} command provides a
- convenient shorthand notation for simple function definitions. In
- this mode, Isabelle tries to solve all the necessary proof obligations
- automatically. If any proof fails, the definition is
- rejected. This can either mean that the definition is indeed faulty,
- or that the default proof procedures are just not smart enough (or
- rather: not designed) to handle the definition.
-
- By expanding the abbreviation to the more verbose \cmd{function} command, these proof obligations become visible and can be analyzed or
- solved manually. The expansion from \cmd{fun} to \cmd{function} is as follows:
-
-\end{isamarkuptext}
-
-
-\[\left[\;\begin{minipage}{0.25\textwidth}\vspace{6pt}
-\cmd{fun} @{text "f :: \<tau>"}\\%
-\cmd{where}\\%
-\hspace*{2ex}{\it equations}\\%
-\hspace*{2ex}\vdots\vspace*{6pt}
-\end{minipage}\right]
-\quad\equiv\quad
-\left[\;\begin{minipage}{0.48\textwidth}\vspace{6pt}
-\cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%
-\cmd{where}\\%
-\hspace*{2ex}{\it equations}\\%
-\hspace*{2ex}\vdots\\%
-\cmd{by} @{text "pat_completeness auto"}\\%
-\cmd{termination by} @{text "lexicographic_order"}\vspace{6pt}
-\end{minipage}
-\right]\]
-
-\begin{isamarkuptext}
- \vspace*{1em}
- \noindent Some details have now become explicit:
-
- \begin{enumerate}
- \item The \cmd{sequential} option enables the preprocessing of
- pattern overlaps which we already saw. Without this option, the equations
- must already be disjoint and complete. The automatic completion only
- works with constructor patterns.
-
- \item A function definition produces a proof obligation which
- expresses completeness and compatibility of patterns (we talk about
- this later). The combination of the methods @{text "pat_completeness"} and
- @{text "auto"} is used to solve this proof obligation.
-
- \item A termination proof follows the definition, started by the
- \cmd{termination} command. This will be explained in \S\ref{termination}.
- \end{enumerate}
- Whenever a \cmd{fun} command fails, it is usually a good idea to
- expand the syntax to the more verbose \cmd{function} form, to see
- what is actually going on.
- *}
-
-
-section {* Termination *}
-
-text {*\label{termination}
- The method @{text "lexicographic_order"} is the default method for
- termination proofs. It can prove termination of a
- certain class of functions by searching for a suitable lexicographic
- combination of size measures. Of course, not all functions have such
- a simple termination argument. For them, we can specify the termination
- relation manually.
-*}
-
-subsection {* The {\tt relation} method *}
-text{*
- Consider the following function, which sums up natural numbers up to
- @{text "N"}, using a counter @{text "i"}:
-*}
-
-function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
- "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
-by pat_completeness auto
-
-text {*
- \noindent The @{text "lexicographic_order"} method fails on this example, because none of the
- arguments decreases in the recursive call, with respect to the standard size ordering.
- To prove termination manually, we must provide a custom wellfounded relation.
-
- The termination argument for @{text "sum"} is based on the fact that
- the \emph{difference} between @{text "i"} and @{text "N"} gets
- smaller in every step, and that the recursion stops when @{text "i"}
- is greater than @{text "N"}. Phrased differently, the expression
- @{text "N + 1 - i"} always decreases.
-
- We can use this expression as a measure function suitable to prove termination.
-*}
-
-termination sum
-apply (relation "measure (\<lambda>(i,N). N + 1 - i)")
-
-txt {*
- The \cmd{termination} command sets up the termination goal for the
- specified function @{text "sum"}. If the function name is omitted, it
- implicitly refers to the last function definition.
-
- The @{text relation} method takes a relation of
- type @{typ "('a \<times> 'a) set"}, where @{typ "'a"} is the argument type of
- the function. If the function has multiple curried arguments, then
- these are packed together into a tuple, as it happened in the above
- example.
-
- The predefined function @{term[source] "measure :: ('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set"} constructs a
- wellfounded relation from a mapping into the natural numbers (a
- \emph{measure function}).
-
- After the invocation of @{text "relation"}, we must prove that (a)
- the relation we supplied is wellfounded, and (b) that the arguments
- of recursive calls indeed decrease with respect to the
- relation:
-
- @{subgoals[display,indent=0]}
-
- These goals are all solved by @{text "auto"}:
-*}
-
-apply auto
-done
-
-text {*
- Let us complicate the function a little, by adding some more
- recursive calls:
-*}
-
-function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
- "foo i N = (if i > N
- then (if N = 0 then 0 else foo 0 (N - 1))
- else i + foo (Suc i) N)"
-by pat_completeness auto
-
-text {*
- When @{text "i"} has reached @{text "N"}, it starts at zero again
- and @{text "N"} is decremented.
- This corresponds to a nested
- loop where one index counts up and the other down. Termination can
- be proved using a lexicographic combination of two measures, namely
- the value of @{text "N"} and the above difference. The @{const
- "measures"} combinator generalizes @{text "measure"} by taking a
- list of measure functions.
-*}
-
-termination
-by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
-
-subsection {* How @{text "lexicographic_order"} works *}
-
-(*fun fails :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
-where
- "fails a [] = a"
-| "fails a (x#xs) = fails (x + a) (x # xs)"
-*)
-
-text {*
- To see how the automatic termination proofs work, let's look at an
- example where it fails\footnote{For a detailed discussion of the
- termination prover, see \cite{bulwahnKN07}}:
-
-\end{isamarkuptext}
-\cmd{fun} @{text "fails :: \"nat \<Rightarrow> nat list \<Rightarrow> nat\""}\\%
-\cmd{where}\\%
-\hspace*{2ex}@{text "\"fails a [] = a\""}\\%
-|\hspace*{1.5ex}@{text "\"fails a (x#xs) = fails (x + a) (x#xs)\""}\\
-\begin{isamarkuptext}
-
-\noindent Isabelle responds with the following error:
-
-\begin{isabelle}
-*** Unfinished subgoals:\newline
-*** (a, 1, <):\newline
-*** \ 1.~@{text "\<And>x. x = 0"}\newline
-*** (a, 1, <=):\newline
-*** \ 1.~False\newline
-*** (a, 2, <):\newline
-*** \ 1.~False\newline
-*** Calls:\newline
-*** a) @{text "(a, x # xs) -->> (x + a, x # xs)"}\newline
-*** Measures:\newline
-*** 1) @{text "\<lambda>x. size (fst x)"}\newline
-*** 2) @{text "\<lambda>x. size (snd x)"}\newline
-*** Result matrix:\newline
-*** \ \ \ \ 1\ \ 2 \newline
-*** a: ? <= \newline
-*** Could not find lexicographic termination order.\newline
-*** At command "fun".\newline
-\end{isabelle}
-*}
-text {*
- The key to this error message is the matrix at the bottom. The rows
- of that matrix correspond to the different recursive calls (In our
- case, there is just one). The columns are the function's arguments
- (expressed through different measure functions, which map the
- argument tuple to a natural number).
-
- The contents of the matrix summarize what is known about argument
- descents: The second argument has a weak descent (@{text "<="}) at the
- recursive call, and for the first argument nothing could be proved,
- which is expressed by @{text "?"}. In general, there are the values
- @{text "<"}, @{text "<="} and @{text "?"}.
-
- For the failed proof attempts, the unfinished subgoals are also
- printed. Looking at these will often point to a missing lemma.
-*}
-
-subsection {* The @{text size_change} method *}
-
-text {*
- Some termination goals that are beyond the powers of
- @{text lexicographic_order} can be solved automatically by the
- more powerful @{text size_change} method, which uses a variant of
- the size-change principle, together with some other
- techniques. While the details are discussed
- elsewhere\cite{krauss_phd},
- here are a few typical situations where
- @{text lexicographic_order} has difficulties and @{text size_change}
- may be worth a try:
- \begin{itemize}
- \item Arguments are permuted in a recursive call.
- \item Several mutually recursive functions with multiple arguments.
- \item Unusual control flow (e.g., when some recursive calls cannot
- occur in sequence).
- \end{itemize}
-
- Loading the theory @{text Multiset} makes the @{text size_change}
- method a bit stronger: it can then use multiset orders internally.
-*}
-
-section {* Mutual Recursion *}
-
-text {*
- If two or more functions call one another mutually, they have to be defined
- in one step. Here are @{text "even"} and @{text "odd"}:
-*}
-
-function even :: "nat \<Rightarrow> bool"
- and odd :: "nat \<Rightarrow> bool"
-where
- "even 0 = True"
-| "odd 0 = False"
-| "even (Suc n) = odd n"
-| "odd (Suc n) = even n"
-by pat_completeness auto
-
-text {*
- To eliminate the mutual dependencies, Isabelle internally
- creates a single function operating on the sum
- type @{typ "nat + nat"}. Then, @{const even} and @{const odd} are
- defined as projections. Consequently, termination has to be proved
- simultaneously for both functions, by specifying a measure on the
- sum type:
-*}
-
-termination
-by (relation "measure (\<lambda>x. case x of Inl n \<Rightarrow> n | Inr n \<Rightarrow> n)") auto
-
-text {*
- We could also have used @{text lexicographic_order}, which
- supports mutual recursive termination proofs to a certain extent.
-*}
-
-subsection {* Induction for mutual recursion *}
-
-text {*
-
- When functions are mutually recursive, proving properties about them
- generally requires simultaneous induction. The induction rule @{text "even_odd.induct"}
- generated from the above definition reflects this.
-
- Let us prove something about @{const even} and @{const odd}:
-*}
-
-lemma even_odd_mod2:
- "even n = (n mod 2 = 0)"
- "odd n = (n mod 2 = 1)"
-
-txt {*
- We apply simultaneous induction, specifying the induction variable
- for both goals, separated by \cmd{and}: *}
-
-apply (induct n and n rule: even_odd.induct)
-
-txt {*
- We get four subgoals, which correspond to the clauses in the
- definition of @{const even} and @{const odd}:
- @{subgoals[display,indent=0]}
- Simplification solves the first two goals, leaving us with two
- statements about the @{text "mod"} operation to prove:
-*}
-
-apply simp_all
-
-txt {*
- @{subgoals[display,indent=0]}
-
- \noindent These can be handled by Isabelle's arithmetic decision procedures.
-
-*}
-
-apply arith
-apply arith
-done
-
-text {*
- In proofs like this, the simultaneous induction is really essential:
- Even if we are just interested in one of the results, the other
- one is necessary to strengthen the induction hypothesis. If we leave
- out the statement about @{const odd} and just write @{term True} instead,
- the same proof fails:
-*}
-
-lemma failed_attempt:
- "even n = (n mod 2 = 0)"
- "True"
-apply (induct n rule: even_odd.induct)
-
-txt {*
- \noindent Now the third subgoal is a dead end, since we have no
- useful induction hypothesis available:
-
- @{subgoals[display,indent=0]}
-*}
-
-oops
-
-section {* General pattern matching *}
-text{*\label{genpats} *}
-
-subsection {* Avoiding automatic pattern splitting *}
-
-text {*
-
- Up to now, we used pattern matching only on datatypes, and the
- patterns were always disjoint and complete, and if they weren't,
- they were made disjoint automatically like in the definition of
- @{const "sep"} in \S\ref{patmatch}.
-
- This automatic splitting can significantly increase the number of
- equations involved, and this is not always desirable. The following
- example shows the problem:
-
- Suppose we are modeling incomplete knowledge about the world by a
- three-valued datatype, which has values @{term "T"}, @{term "F"}
- and @{term "X"} for true, false and uncertain propositions, respectively.
-*}
-
-datatype P3 = T | F | X
-
-text {* \noindent Then the conjunction of such values can be defined as follows: *}
-
-fun And :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
-where
- "And T p = p"
-| "And p T = p"
-| "And p F = F"
-| "And F p = F"
-| "And X X = X"
-
-
-text {*
- This definition is useful, because the equations can directly be used
- as simplification rules. But the patterns overlap: For example,
- the expression @{term "And T T"} is matched by both the first and
- the second equation. By default, Isabelle makes the patterns disjoint by
- splitting them up, producing instances:
-*}
-
-thm And.simps
-
-text {*
- @{thm[indent=4] And.simps}
-
- \vspace*{1em}
- \noindent There are several problems with this:
-
- \begin{enumerate}
- \item If the datatype has many constructors, there can be an
- explosion of equations. For @{const "And"}, we get seven instead of
- five equations, which can be tolerated, but this is just a small
- example.
-
- \item Since splitting makes the equations \qt{less general}, they
- do not always match in rewriting. While the term @{term "And x F"}
- can be simplified to @{term "F"} with the original equations, a
- (manual) case split on @{term "x"} is now necessary.
-
- \item The splitting also concerns the induction rule @{text
- "And.induct"}. Instead of five premises it now has seven, which
- means that our induction proofs will have more cases.
-
- \item In general, it increases clarity if we get the same definition
- back which we put in.
- \end{enumerate}
-
- If we do not want the automatic splitting, we can switch it off by
- leaving out the \cmd{sequential} option. However, we will have to
- prove that our pattern matching is consistent\footnote{This prevents
- us from defining something like @{term "f x = True"} and @{term "f x
- = False"} simultaneously.}:
-*}
-
-function And2 :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
-where
- "And2 T p = p"
-| "And2 p T = p"
-| "And2 p F = F"
-| "And2 F p = F"
-| "And2 X X = X"
-
-txt {*
- \noindent Now let's look at the proof obligations generated by a
- function definition. In this case, they are:
-
- @{subgoals[display,indent=0]}\vspace{-1.2em}\hspace{3cm}\vdots\vspace{1.2em}
-
- The first subgoal expresses the completeness of the patterns. It has
- the form of an elimination rule and states that every @{term x} of
- the function's input type must match at least one of the patterns\footnote{Completeness could
- be equivalently stated as a disjunction of existential statements:
-@{term "(\<exists>p. x = (T, p)) \<or> (\<exists>p. x = (p, T)) \<or> (\<exists>p. x = (p, F)) \<or>
- (\<exists>p. x = (F, p)) \<or> (x = (X, X))"}, and you can use the method @{text atomize_elim} to get that form instead.}. If the patterns just involve
- datatypes, we can solve it with the @{text "pat_completeness"}
- method:
-*}
-
-apply pat_completeness
-
-txt {*
- The remaining subgoals express \emph{pattern compatibility}. We do
- allow that an input value matches multiple patterns, but in this
- case, the result (i.e.~the right hand sides of the equations) must
- also be equal. For each pair of two patterns, there is one such
- subgoal. Usually this needs injectivity of the constructors, which
- is used automatically by @{text "auto"}.
-*}
-
-by auto
-termination by (relation "{}") simp
-
-
-subsection {* Non-constructor patterns *}
-
-text {*
- Most of Isabelle's basic types take the form of inductive datatypes,
- and usually pattern matching works on the constructors of such types.
- However, this need not be always the case, and the \cmd{function}
- command handles other kind of patterns, too.
-
- One well-known instance of non-constructor patterns are
- so-called \emph{$n+k$-patterns}, which are a little controversial in
- the functional programming world. Here is the initial fibonacci
- example with $n+k$-patterns:
-*}
-
-function fib2 :: "nat \<Rightarrow> nat"
-where
- "fib2 0 = 1"
-| "fib2 1 = 1"
-| "fib2 (n + 2) = fib2 n + fib2 (Suc n)"
-
-txt {*
- This kind of matching is again justified by the proof of pattern
- completeness and compatibility.
- The proof obligation for pattern completeness states that every natural number is
- either @{term "0::nat"}, @{term "1::nat"} or @{term "n +
- (2::nat)"}:
-
- @{subgoals[display,indent=0,goals_limit=1]}
-
- This is an arithmetic triviality, but unfortunately the
- @{text arith} method cannot handle this specific form of an
- elimination rule. However, we can use the method @{text
- "atomize_elim"} to do an ad-hoc conversion to a disjunction of
- existentials, which can then be solved by the arithmetic decision procedure.
- Pattern compatibility and termination are automatic as usual.
-*}
-apply atomize_elim
-apply arith
-apply auto
-done
-termination by lexicographic_order
-text {*
- We can stretch the notion of pattern matching even more. The
- following function is not a sensible functional program, but a
- perfectly valid mathematical definition:
-*}
-
-function ev :: "nat \<Rightarrow> bool"
-where
- "ev (2 * n) = True"
-| "ev (2 * n + 1) = False"
-apply atomize_elim
-by arith+
-termination by (relation "{}") simp
-
-text {*
- This general notion of pattern matching gives you a certain freedom
- in writing down specifications. However, as always, such freedom should
- be used with care:
-
- If we leave the area of constructor
- patterns, we have effectively departed from the world of functional
- programming. This means that it is no longer possible to use the
- code generator, and expect it to generate ML code for our
- definitions. Also, such a specification might not work very well together with
- simplification. Your mileage may vary.
-*}
-
-
-subsection {* Conditional equations *}
-
-text {*
- The function package also supports conditional equations, which are
- similar to guards in a language like Haskell. Here is Euclid's
- algorithm written with conditional patterns\footnote{Note that the
- patterns are also overlapping in the base case}:
-*}
-
-function gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
- "gcd x 0 = x"
-| "gcd 0 y = y"
-| "x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y - x)"
-| "\<not> x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (x - y) (Suc y)"
-by (atomize_elim, auto, arith)
-termination by lexicographic_order
-
-text {*
- By now, you can probably guess what the proof obligations for the
- pattern completeness and compatibility look like.
-
- Again, functions with conditional patterns are not supported by the
- code generator.
-*}
-
-
-subsection {* Pattern matching on strings *}
-
-text {*
- As strings (as lists of characters) are normal datatypes, pattern
- matching on them is possible, but somewhat problematic. Consider the
- following definition:
-
-\end{isamarkuptext}
-\noindent\cmd{fun} @{text "check :: \"string \<Rightarrow> bool\""}\\%
-\cmd{where}\\%
-\hspace*{2ex}@{text "\"check (''good'') = True\""}\\%
-@{text "| \"check s = False\""}
-\begin{isamarkuptext}
-
- \noindent An invocation of the above \cmd{fun} command does not
- terminate. What is the problem? Strings are lists of characters, and
- characters are a datatype with a lot of constructors. Splitting the
- catch-all pattern thus leads to an explosion of cases, which cannot
- be handled by Isabelle.
-
- There are two things we can do here. Either we write an explicit
- @{text "if"} on the right hand side, or we can use conditional patterns:
-*}
-
-function check :: "string \<Rightarrow> bool"
-where
- "check (''good'') = True"
-| "s \<noteq> ''good'' \<Longrightarrow> check s = False"
-by auto
-termination by (relation "{}") simp
-
-
-section {* Partiality *}
-
-text {*
- In HOL, all functions are total. A function @{term "f"} applied to
- @{term "x"} always has the value @{term "f x"}, and there is no notion
- of undefinedness.
- This is why we have to do termination
- proofs when defining functions: The proof justifies that the
- function can be defined by wellfounded recursion.
-
- However, the \cmd{function} package does support partiality to a
- certain extent. Let's look at the following function which looks
- for a zero of a given function f.
-*}
-
-function (*<*)(domintros)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
-where
- "findzero f n = (if f n = 0 then n else findzero f (Suc n))"
-by pat_completeness auto
-
-text {*
- \noindent Clearly, any attempt of a termination proof must fail. And without
- that, we do not get the usual rules @{text "findzero.simps"} and
- @{text "findzero.induct"}. So what was the definition good for at all?
-*}
-
-subsection {* Domain predicates *}
-
-text {*
- The trick is that Isabelle has not only defined the function @{const findzero}, but also
- a predicate @{term "findzero_dom"} that characterizes the values where the function
- terminates: the \emph{domain} of the function. If we treat a
- partial function just as a total function with an additional domain
- predicate, we can derive simplification and
- induction rules as we do for total functions. They are guarded
- by domain conditions and are called @{text psimps} and @{text
- pinduct}:
-*}
-
-text {*
- \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage}
- \hfill(@{text "findzero.psimps"})
- \vspace{1em}
-
- \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage}
- \hfill(@{text "findzero.pinduct"})
-*}
-
-text {*
- Remember that all we
- are doing here is use some tricks to make a total function appear
- as if it was partial. We can still write the term @{term "findzero
- (\<lambda>x. 1) 0"} and like any other term of type @{typ nat} it is equal
- to some natural number, although we might not be able to find out
- which one. The function is \emph{underdefined}.
-
- But it is defined enough to prove something interesting about it. We
- can prove that if @{term "findzero f n"}
- terminates, it indeed returns a zero of @{term f}:
-*}
-
-lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"
-
-txt {* \noindent We apply induction as usual, but using the partial induction
- rule: *}
-
-apply (induct f n rule: findzero.pinduct)
-
-txt {* \noindent This gives the following subgoals:
-
- @{subgoals[display,indent=0]}
-
- \noindent The hypothesis in our lemma was used to satisfy the first premise in
- the induction rule. However, we also get @{term
- "findzero_dom (f, n)"} as a local assumption in the induction step. This
- allows unfolding @{term "findzero f n"} using the @{text psimps}
- rule, and the rest is trivial.
- *}
-apply (simp add: findzero.psimps)
-done
-
-text {*
- Proofs about partial functions are often not harder than for total
- functions. Fig.~\ref{findzero_isar} shows a slightly more
- complicated proof written in Isar. It is verbose enough to show how
- partiality comes into play: From the partial induction, we get an
- additional domain condition hypothesis. Observe how this condition
- is applied when calls to @{term findzero} are unfolded.
-*}
-
-text_raw {*
-\begin{figure}
-\hrule\vspace{6pt}
-\begin{minipage}{0.8\textwidth}
-\isabellestyle{it}
-\isastyle\isamarkuptrue
-*}
-lemma "\<lbrakk>findzero_dom (f, n); x \<in> {n ..< findzero f n}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"
-proof (induct rule: findzero.pinduct)
- fix f n assume dom: "findzero_dom (f, n)"
- and IH: "\<lbrakk>f n \<noteq> 0; x \<in> {Suc n ..< findzero f (Suc n)}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"
- and x_range: "x \<in> {n ..< findzero f n}"
- have "f n \<noteq> 0"
- proof
- assume "f n = 0"
- with dom have "findzero f n = n" by (simp add: findzero.psimps)
- with x_range show False by auto
- qed
-
- from x_range have "x = n \<or> x \<in> {Suc n ..< findzero f n}" by auto
- thus "f x \<noteq> 0"
- proof
- assume "x = n"
- with `f n \<noteq> 0` show ?thesis by simp
- next
- assume "x \<in> {Suc n ..< findzero f n}"
- with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by (simp add: findzero.psimps)
- with IH and `f n \<noteq> 0`
- show ?thesis by simp
- qed
-qed
-text_raw {*
-\isamarkupfalse\isabellestyle{tt}
-\end{minipage}\vspace{6pt}\hrule
-\caption{A proof about a partial function}\label{findzero_isar}
-\end{figure}
-*}
-
-subsection {* Partial termination proofs *}
-
-text {*
- Now that we have proved some interesting properties about our
- function, we should turn to the domain predicate and see if it is
- actually true for some values. Otherwise we would have just proved
- lemmas with @{term False} as a premise.
-
- Essentially, we need some introduction rules for @{text
- findzero_dom}. The function package can prove such domain
- introduction rules automatically. But since they are not used very
- often (they are almost never needed if the function is total), this
- functionality is disabled by default for efficiency reasons. So we have to go
- back and ask for them explicitly by passing the @{text
- "(domintros)"} option to the function package:
-
-\vspace{1ex}
-\noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
-\cmd{where}\isanewline%
-\ \ \ldots\\
-
- \noindent Now the package has proved an introduction rule for @{text findzero_dom}:
-*}
-
-thm findzero.domintros
-
-text {*
- @{thm[display] findzero.domintros}
-
- Domain introduction rules allow to show that a given value lies in the
- domain of a function, if the arguments of all recursive calls
- are in the domain as well. They allow to do a \qt{single step} in a
- termination proof. Usually, you want to combine them with a suitable
- induction principle.
-
- Since our function increases its argument at recursive calls, we
- need an induction principle which works \qt{backwards}. We will use
- @{text inc_induct}, which allows to do induction from a fixed number
- \qt{downwards}:
-
- \begin{center}@{thm inc_induct}\hfill(@{text "inc_induct"})\end{center}
-
- Figure \ref{findzero_term} gives a detailed Isar proof of the fact
- that @{text findzero} terminates if there is a zero which is greater
- or equal to @{term n}. First we derive two useful rules which will
- solve the base case and the step case of the induction. The
- induction is then straightforward, except for the unusual induction
- principle.
-
-*}
-
-text_raw {*
-\begin{figure}
-\hrule\vspace{6pt}
-\begin{minipage}{0.8\textwidth}
-\isabellestyle{it}
-\isastyle\isamarkuptrue
-*}
-lemma findzero_termination:
- assumes "x \<ge> n" and "f x = 0"
- shows "findzero_dom (f, n)"
-proof -
- have base: "findzero_dom (f, x)"
- by (rule findzero.domintros) (simp add:`f x = 0`)
-
- have step: "\<And>i. findzero_dom (f, Suc i)
- \<Longrightarrow> findzero_dom (f, i)"
- by (rule findzero.domintros) simp
-
- from `x \<ge> n` show ?thesis
- proof (induct rule:inc_induct)
- show "findzero_dom (f, x)" by (rule base)
- next
- fix i assume "findzero_dom (f, Suc i)"
- thus "findzero_dom (f, i)" by (rule step)
- qed
-qed
-text_raw {*
-\isamarkupfalse\isabellestyle{tt}
-\end{minipage}\vspace{6pt}\hrule
-\caption{Termination proof for @{text findzero}}\label{findzero_term}
-\end{figure}
-*}
-
-text {*
- Again, the proof given in Fig.~\ref{findzero_term} has a lot of
- detail in order to explain the principles. Using more automation, we
- can also have a short proof:
-*}
-
-lemma findzero_termination_short:
- assumes zero: "x >= n"
- assumes [simp]: "f x = 0"
- shows "findzero_dom (f, n)"
-using zero
-by (induct rule:inc_induct) (auto intro: findzero.domintros)
-
-text {*
- \noindent It is simple to combine the partial correctness result with the
- termination lemma:
-*}
-
-lemma findzero_total_correctness:
- "f x = 0 \<Longrightarrow> f (findzero f 0) = 0"
-by (blast intro: findzero_zero findzero_termination)
-
-subsection {* Definition of the domain predicate *}
-
-text {*
- Sometimes it is useful to know what the definition of the domain
- predicate looks like. Actually, @{text findzero_dom} is just an
- abbreviation:
-
- @{abbrev[display] findzero_dom}
-
- The domain predicate is the \emph{accessible part} of a relation @{const
- findzero_rel}, which was also created internally by the function
- package. @{const findzero_rel} is just a normal
- inductive predicate, so we can inspect its definition by
- looking at the introduction rules @{text findzero_rel.intros}.
- In our case there is just a single rule:
-
- @{thm[display] findzero_rel.intros}
-
- The predicate @{const findzero_rel}
- describes the \emph{recursion relation} of the function
- definition. The recursion relation is a binary relation on
- the arguments of the function that relates each argument to its
- recursive calls. In general, there is one introduction rule for each
- recursive call.
-
- The predicate @{term "accp findzero_rel"} is the accessible part of
- that relation. An argument belongs to the accessible part, if it can
- be reached in a finite number of steps (cf.~its definition in @{text
- "Wellfounded.thy"}).
-
- Since the domain predicate is just an abbreviation, you can use
- lemmas for @{const accp} and @{const findzero_rel} directly. Some
- lemmas which are occasionally useful are @{text accpI}, @{text
- accp_downward}, and of course the introduction and elimination rules
- for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.
-*}
-
-section {* Nested recursion *}
-
-text {*
- Recursive calls which are nested in one another frequently cause
- complications, since their termination proof can depend on a partial
- correctness property of the function itself.
-
- As a small example, we define the \qt{nested zero} function:
-*}
-
-function nz :: "nat \<Rightarrow> nat"
-where
- "nz 0 = 0"
-| "nz (Suc n) = nz (nz n)"
-by pat_completeness auto
-
-text {*
- If we attempt to prove termination using the identity measure on
- naturals, this fails:
-*}
-
-termination
- apply (relation "measure (\<lambda>n. n)")
- apply auto
-
-txt {*
- We get stuck with the subgoal
-
- @{subgoals[display]}
-
- Of course this statement is true, since we know that @{const nz} is
- the zero function. And in fact we have no problem proving this
- property by induction.
-*}
-(*<*)oops(*>*)
-lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
- by (induct rule:nz.pinduct) (auto simp: nz.psimps)
-
-text {*
- We formulate this as a partial correctness lemma with the condition
- @{term "nz_dom n"}. This allows us to prove it with the @{text
- pinduct} rule before we have proved termination. With this lemma,
- the termination proof works as expected:
-*}
-
-termination
- by (relation "measure (\<lambda>n. n)") (auto simp: nz_is_zero)
-
-text {*
- As a general strategy, one should prove the statements needed for
- termination as a partial property first. Then they can be used to do
- the termination proof. This also works for less trivial
- examples. Figure \ref{f91} defines the 91-function, a well-known
- challenge problem due to John McCarthy, and proves its termination.
-*}
-
-text_raw {*
-\begin{figure}
-\hrule\vspace{6pt}
-\begin{minipage}{0.8\textwidth}
-\isabellestyle{it}
-\isastyle\isamarkuptrue
-*}
-
-function f91 :: "nat \<Rightarrow> nat"
-where
- "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
-by pat_completeness auto
-
-lemma f91_estimate:
- assumes trm: "f91_dom n"
- shows "n < f91 n + 11"
-using trm by induct (auto simp: f91.psimps)
-
-termination
-proof
- let ?R = "measure (\<lambda>x. 101 - x)"
- show "wf ?R" ..
-
- fix n :: nat assume "\<not> 100 < n" -- "Assumptions for both calls"
-
- thus "(n + 11, n) \<in> ?R" by simp -- "Inner call"
-
- assume inner_trm: "f91_dom (n + 11)" -- "Outer call"
- with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
- with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp
-qed
-
-text_raw {*
-\isamarkupfalse\isabellestyle{tt}
-\end{minipage}
-\vspace{6pt}\hrule
-\caption{McCarthy's 91-function}\label{f91}
-\end{figure}
-*}
-
-
-section {* Higher-Order Recursion *}
-
-text {*
- Higher-order recursion occurs when recursive calls
- are passed as arguments to higher-order combinators such as @{const
- map}, @{term filter} etc.
- As an example, imagine a datatype of n-ary trees:
-*}
-
-datatype 'a tree =
- Leaf 'a
-| Branch "'a tree list"
-
-
-text {* \noindent We can define a function which swaps the left and right subtrees recursively, using the
- list functions @{const rev} and @{const map}: *}
-
-fun mirror :: "'a tree \<Rightarrow> 'a tree"
-where
- "mirror (Leaf n) = Leaf n"
-| "mirror (Branch l) = Branch (rev (map mirror l))"
-
-text {*
- Although the definition is accepted without problems, let us look at the termination proof:
-*}
-
-termination proof
- txt {*
-
- As usual, we have to give a wellfounded relation, such that the
- arguments of the recursive calls get smaller. But what exactly are
- the arguments of the recursive calls when mirror is given as an
- argument to @{const map}? Isabelle gives us the
- subgoals
-
- @{subgoals[display,indent=0]}
-
- So the system seems to know that @{const map} only
- applies the recursive call @{term "mirror"} to elements
- of @{term "l"}, which is essential for the termination proof.
-
- This knowledge about @{const map} is encoded in so-called congruence rules,
- which are special theorems known to the \cmd{function} command. The
- rule for @{const map} is
-
- @{thm[display] map_cong}
-
- You can read this in the following way: Two applications of @{const
- map} are equal, if the list arguments are equal and the functions
- coincide on the elements of the list. This means that for the value
- @{term "map f l"} we only have to know how @{term f} behaves on
- the elements of @{term l}.
-
- Usually, one such congruence rule is
- needed for each higher-order construct that is used when defining
- new functions. In fact, even basic functions like @{const
- If} and @{const Let} are handled by this mechanism. The congruence
- rule for @{const If} states that the @{text then} branch is only
- relevant if the condition is true, and the @{text else} branch only if it
- is false:
-
- @{thm[display] if_cong}
-
- Congruence rules can be added to the
- function package by giving them the @{term fundef_cong} attribute.
-
- The constructs that are predefined in Isabelle, usually
- come with the respective congruence rules.
- But if you define your own higher-order functions, you may have to
- state and prove the required congruence rules yourself, if you want to use your
- functions in recursive definitions.
-*}
-(*<*)oops(*>*)
-
-subsection {* Congruence Rules and Evaluation Order *}
-
-text {*
- Higher order logic differs from functional programming languages in
- that it has no built-in notion of evaluation order. A program is
- just a set of equations, and it is not specified how they must be
- evaluated.
-
- However for the purpose of function definition, we must talk about
- evaluation order implicitly, when we reason about termination.
- Congruence rules express that a certain evaluation order is
- consistent with the logical definition.
-
- Consider the following function.
-*}
-
-function f :: "nat \<Rightarrow> bool"
-where
- "f n = (n = 0 \<or> f (n - 1))"
-(*<*)by pat_completeness auto(*>*)
-
-text {*
- For this definition, the termination proof fails. The default configuration
- specifies no congruence rule for disjunction. We have to add a
- congruence rule that specifies left-to-right evaluation order:
-
- \vspace{1ex}
- \noindent @{thm disj_cong}\hfill(@{text "disj_cong"})
- \vspace{1ex}
-
- Now the definition works without problems. Note how the termination
- proof depends on the extra condition that we get from the congruence
- rule.
-
- However, as evaluation is not a hard-wired concept, we
- could just turn everything around by declaring a different
- congruence rule. Then we can make the reverse definition:
-*}
-
-lemma disj_cong2[fundef_cong]:
- "(\<not> Q' \<Longrightarrow> P = P') \<Longrightarrow> (Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
- by blast
-
-fun f' :: "nat \<Rightarrow> bool"
-where
- "f' n = (f' (n - 1) \<or> n = 0)"
-
-text {*
- \noindent These examples show that, in general, there is no \qt{best} set of
- congruence rules.
-
- However, such tweaking should rarely be necessary in
- practice, as most of the time, the default set of congruence rules
- works well.
-*}
-
-end
--- a/doc-src/Functions/document/build Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-#!/bin/bash
-
-set -e
-
-FORMAT="$1"
-VARIANT="$2"
-
-cp "$ISABELLE_HOME/doc-src/iman.sty" .
-cp "$ISABELLE_HOME/doc-src/extra.sty" .
-cp "$ISABELLE_HOME/doc-src/isar.sty" .
-cp "$ISABELLE_HOME/doc-src/manual.bib" .
-
-"$ISABELLE_HOME/doc-src/prepare_document" "$FORMAT"
-
--- a/doc-src/Functions/document/conclusion.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-\section{Conclusion}
-
-\fixme{}
-
-
-
-
--- a/doc-src/Functions/document/intro.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-\section{Introduction}
-
-Starting from Isabelle 2007, new facilities for recursive
-function definitions~\cite{krauss2006} are available. They provide
-better support for general recursive definitions than previous
-packages. But despite all tool support, function definitions can
-sometimes be a difficult thing.
-
-This tutorial is an example-guided introduction to the practical use
-of the package and related tools. It should help you get started with
-defining functions quickly. For the more difficult definitions we will
-discuss what problems can arise, and how they can be solved.
-
-We assume that you have mastered the fundamentals of Isabelle/HOL
-and are able to write basic specifications and proofs. To start out
-with Isabelle in general, consult the Isabelle/HOL tutorial
-\cite{isa-tutorial}.
-
-
-
-\paragraph{Structure of this tutorial.}
-Section 2 introduces the syntax and basic operation of the \cmd{fun}
-command, which provides full automation with reasonable default
-behavior. The impatient reader can stop after that
-section, and consult the remaining sections only when needed.
-Section 3 introduces the more verbose \cmd{function} command which
-gives fine-grained control. This form should be used
-whenever the short form fails.
-After that we discuss more specialized issues:
-termination, mutual, nested and higher-order recursion, partiality, pattern matching
-and others.
-
-
-\paragraph{Some background.}
-Following the LCF tradition, the package is realized as a definitional
-extension: Recursive definitions are internally transformed into a
-non-recursive form, such that the function can be defined using
-standard definition facilities. Then the recursive specification is
-derived from the primitive definition. This is a complex task, but it
-is fully automated and mostly transparent to the user. Definitional
-extensions are valuable because they are conservative by construction:
-The \qt{new} concept of general wellfounded recursion is completely reduced
-to existing principles.
-
-
-
-
-The new \cmd{function} command, and its short form \cmd{fun} have mostly
-replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
-a few of technical issues around \cmd{recdef}, and allow definitions
-which were not previously possible.
-
-
-
-
--- a/doc-src/Functions/document/mathpartir.sty Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,421 +0,0 @@
-% Mathpartir --- Math Paragraph for Typesetting Inference Rules
-%
-% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
-%
-% Author : Didier Remy
-% Version : 1.2.0
-% Bug Reports : to author
-% Web Site : http://pauillac.inria.fr/~remy/latex/
-%
-% Mathpartir is free software; you can redistribute it and/or modify
-% it under the terms of the GNU General Public License as published by
-% the Free Software Foundation; either version 2, or (at your option)
-% any later version.
-%
-% Mathpartir is distributed in the hope that it will be useful,
-% but WITHOUT ANY WARRANTY; without even the implied warranty of
-% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-% GNU General Public License for more details
-% (http://pauillac.inria.fr/~remy/license/GPL).
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% File mathpartir.sty (LaTeX macros)
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{mathpartir}
- [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
-
-%%
-
-%% Identification
-%% Preliminary declarations
-
-\RequirePackage {keyval}
-
-%% Options
-%% More declarations
-
-%% PART I: Typesetting maths in paragraphe mode
-
-\newdimen \mpr@tmpdim
-
-% To ensure hevea \hva compatibility, \hva should expands to nothing
-% in mathpar or in inferrule
-\let \mpr@hva \empty
-
-%% normal paragraph parametters, should rather be taken dynamically
-\def \mpr@savepar {%
- \edef \MathparNormalpar
- {\noexpand \lineskiplimit \the\lineskiplimit
- \noexpand \lineskip \the\lineskip}%
- }
-
-\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
-\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
-\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
-\let \MathparLineskip \mpr@lineskip
-\def \mpr@paroptions {\MathparLineskip}
-\let \mpr@prebindings \relax
-
-\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
-
-\def \mpr@goodbreakand
- {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
-\def \mpr@and {\hskip \mpr@andskip}
-\def \mpr@andcr {\penalty 50\mpr@and}
-\def \mpr@cr {\penalty -10000\mpr@and}
-\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
-
-\def \mpr@bindings {%
- \let \and \mpr@andcr
- \let \par \mpr@andcr
- \let \\\mpr@cr
- \let \eqno \mpr@eqno
- \let \hva \mpr@hva
- }
-\let \MathparBindings \mpr@bindings
-
-% \@ifundefined {ignorespacesafterend}
-% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
-
-\newenvironment{mathpar}[1][]
- {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
- \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
- \noindent $\displaystyle\fi
- \MathparBindings}
- {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
-
-% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
-% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
-
-%%% HOV BOXES
-
-\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
- \vbox \bgroup \tabskip 0em \let \\ \cr
- \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
- \egroup}
-
-\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
- \box0\else \mathvbox {#1}\fi}
-
-
-%% Part II -- operations on lists
-
-\newtoks \mpr@lista
-\newtoks \mpr@listb
-
-\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
-
-\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
-
-\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
-\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
-
-\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
-\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
-
-\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
-\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
-
-\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
- \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
- \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
- \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
- \mpr@flatten \mpr@all \mpr@to \mpr@one
- \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
- \mpr@all \mpr@stripend
- \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
- \ifx 1\mpr@isempty
- \repeat
-}
-
-\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
- \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
-
-%% Part III -- Type inference rules
-
-\newif \if@premisse
-\newbox \mpr@hlist
-\newbox \mpr@vlist
-\newif \ifmpr@center \mpr@centertrue
-\def \mpr@htovlist {%
- \setbox \mpr@hlist
- \hbox {\strut
- \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
- \unhbox \mpr@hlist}%
- \setbox \mpr@vlist
- \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
- \else \unvbox \mpr@vlist \box \mpr@hlist
- \fi}%
-}
-% OLD version
-% \def \mpr@htovlist {%
-% \setbox \mpr@hlist
-% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
-% \setbox \mpr@vlist
-% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
-% \else \unvbox \mpr@vlist \box \mpr@hlist
-% \fi}%
-% }
-
-\def \mpr@item #1{$\displaystyle #1$}
-\def \mpr@sep{2em}
-\def \mpr@blank { }
-\def \mpr@hovbox #1#2{\hbox
- \bgroup
- \ifx #1T\@premissetrue
- \else \ifx #1B\@premissefalse
- \else
- \PackageError{mathpartir}
- {Premisse orientation should either be T or B}
- {Fatal error in Package}%
- \fi \fi
- \def \@test {#2}\ifx \@test \mpr@blank\else
- \setbox \mpr@hlist \hbox {}%
- \setbox \mpr@vlist \vbox {}%
- \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
- \let \@hvlist \empty \let \@rev \empty
- \mpr@tmpdim 0em
- \expandafter \mpr@makelist #2\mpr@to \mpr@flat
- \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
- \def \\##1{%
- \def \@test {##1}\ifx \@test \empty
- \mpr@htovlist
- \mpr@tmpdim 0em %%% last bug fix not extensively checked
- \else
- \setbox0 \hbox{\mpr@item {##1}}\relax
- \advance \mpr@tmpdim by \wd0
- %\mpr@tmpdim 1.02\mpr@tmpdim
- \ifnum \mpr@tmpdim < \hsize
- \ifnum \wd\mpr@hlist > 0
- \if@premisse
- \setbox \mpr@hlist
- \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
- \else
- \setbox \mpr@hlist
- \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
- \fi
- \else
- \setbox \mpr@hlist \hbox {\unhbox0}%
- \fi
- \else
- \ifnum \wd \mpr@hlist > 0
- \mpr@htovlist
- \mpr@tmpdim \wd0
- \fi
- \setbox \mpr@hlist \hbox {\unhbox0}%
- \fi
- \advance \mpr@tmpdim by \mpr@sep
- \fi
- }%
- \@rev
- \mpr@htovlist
- \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
- \fi
- \egroup
-}
-
-%%% INFERENCE RULES
-
-\@ifundefined{@@over}{%
- \let\@@over\over % fallback if amsmath is not loaded
- \let\@@overwithdelims\overwithdelims
- \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
- \let\@@above\above \let\@@abovewithdelims\abovewithdelims
- }{}
-
-%% The default
-
-\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
- $\displaystyle {#1\mpr@over #2}$}}
-\let \mpr@fraction \mpr@@fraction
-
-%% A generic solution to arrow
-
-\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
- \def \mpr@tail{#1}%
- \def \mpr@body{#2}%
- \def \mpr@head{#3}%
- \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
- \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
- \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
- \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
- \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
- \setbox0=\hbox {$\box1 \@@atop \box2$}%
- \dimen0=\wd0\box0
- \box0 \hskip -\dimen0\relax
- \hbox to \dimen0 {$%
- \mathrel{\mpr@tail}\joinrel
- \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
- $}}}
-
-%% Old stuff should be removed in next version
-\def \mpr@@reduce #1#2{\hbox
- {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
-\def \mpr@@rewrite #1#2#3{\hbox
- {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
-\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
-
-\def \mpr@empty {}
-\def \mpr@inferrule
- {\bgroup
- \ifnum \linewidth<\hsize \hsize \linewidth\fi
- \mpr@rulelineskip
- \let \and \qquad
- \let \hva \mpr@hva
- \let \@rulename \mpr@empty
- \let \@rule@options \mpr@empty
- \let \mpr@over \@@over
- \mpr@inferrule@}
-\newcommand {\mpr@inferrule@}[3][]
- {\everymath={\displaystyle}%
- \def \@test {#2}\ifx \empty \@test
- \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
- \else
- \def \@test {#3}\ifx \empty \@test
- \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
- \else
- \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
- \fi \fi
- \def \@test {#1}\ifx \@test\empty \box0
- \else \vbox
-%%% Suggestion de Francois pour les etiquettes longues
-%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
- {\hbox {\RefTirName {#1}}\box0}\fi
- \egroup}
-
-\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
-
-% They are two forms
-% \inferrule [label]{[premisses}{conclusions}
-% or
-% \inferrule* [options]{[premisses}{conclusions}
-%
-% Premisses and conclusions are lists of elements separated by \\
-% Each \\ produces a break, attempting horizontal breaks if possible,
-% and vertical breaks if needed.
-%
-% An empty element obtained by \\\\ produces a vertical break in all cases.
-%
-% The former rule is aligned on the fraction bar.
-% The optional label appears on top of the rule
-% The second form to be used in a derivation tree is aligned on the last
-% line of its conclusion
-%
-% The second form can be parameterized, using the key=val interface. The
-% folloiwng keys are recognized:
-%
-% width set the width of the rule to val
-% narrower set the width of the rule to val\hsize
-% before execute val at the beginning/left
-% lab put a label [Val] on top of the rule
-% lskip add negative skip on the right
-% left put a left label [Val]
-% Left put a left label [Val], ignoring its width
-% right put a right label [Val]
-% Right put a right label [Val], ignoring its width
-% leftskip skip negative space on the left-hand side
-% rightskip skip negative space on the right-hand side
-% vdots lift the rule by val and fill vertical space with dots
-% after execute val at the end/right
-%
-% Note that most options must come in this order to avoid strange
-% typesetting (in particular leftskip must preceed left and Left and
-% rightskip must follow Right or right; vdots must come last
-% or be only followed by rightskip.
-%
-
-%% Keys that make sence in all kinds of rules
-\def \mprset #1{\setkeys{mprset}{#1}}
-\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
-\define@key {mprset}{center}[]{\mpr@centertrue}
-\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
-\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
-\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
-
-\newbox \mpr@right
-\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
-\define@key {mpr}{center}[]{\mpr@centertrue}
-\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
-\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
-\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
- \advance \hsize by -\wd0\box0}
-\define@key {mpr}{width}{\hsize #1}
-\define@key {mpr}{sep}{\def\mpr@sep{#1}}
-\define@key {mpr}{before}{#1}
-\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{narrower}{\hsize #1\hsize}
-\define@key {mpr}{leftskip}{\hskip -#1}
-\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
-\define@key {mpr}{rightskip}
- {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
-\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
- \advance \hsize by -\wd0\box0}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
- \advance \hsize by -\wd0\box0}
-\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
-\define@key {mpr}{right}
- {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
- \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{RIGHT}
- {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
- \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{Right}
- {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
-\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
-\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
-
-\newdimen \rule@dimen
-\newcommand \mpr@inferstar@ [3][]{\setbox0
- \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
- \setbox \mpr@right \hbox{}%
- $\setkeys{mpr}{#1}%
- \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
- \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
- \box \mpr@right \mpr@vdots$}
- \setbox1 \hbox {\strut}
- \rule@dimen \dp0 \advance \rule@dimen by -\dp1
- \raise \rule@dimen \box0}
-
-\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
-\newcommand \mpr@err@skipargs[3][]{}
-\def \mpr@inferstar*{\ifmmode
- \let \@do \mpr@inferstar@
- \else
- \let \@do \mpr@err@skipargs
- \PackageError {mathpartir}
- {\string\inferrule* can only be used in math mode}{}%
- \fi \@do}
-
-
-%%% Exports
-
-% Envirnonment mathpar
-
-\let \inferrule \mpr@infer
-
-% make a short name \infer is not already defined
-\@ifundefined {infer}{\let \infer \mpr@infer}{}
-
-\def \TirNameStyle #1{\small \textsc{#1}}
-\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
-\let \TirName \tir@name
-\let \DefTirName \TirName
-\let \RefTirName \TirName
-
-%%% Other Exports
-
-% \let \listcons \mpr@cons
-% \let \listsnoc \mpr@snoc
-% \let \listhead \mpr@head
-% \let \listmake \mpr@makelist
-
-
-
-
-\endinput
--- a/doc-src/Functions/document/root.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-
-\documentclass[a4paper,fleqn]{article}
-
-\usepackage{latexsym,graphicx}
-\usepackage[refpage]{nomencl}
-\usepackage{iman,extra,isar}
-\usepackage{isabelle,isabellesym}
-\usepackage{style}
-\usepackage{mathpartir}
-\usepackage{amsthm}
-\usepackage{pdfsetup}
-
-\newcommand{\cmd}[1]{\isacommand{#1}}
-
-\newcommand{\isasymINFIX}{\cmd{infix}}
-\newcommand{\isasymLOCALE}{\cmd{locale}}
-\newcommand{\isasymINCLUDES}{\cmd{includes}}
-\newcommand{\isasymDATATYPE}{\cmd{datatype}}
-\newcommand{\isasymDEFINES}{\cmd{defines}}
-\newcommand{\isasymNOTES}{\cmd{notes}}
-\newcommand{\isasymCLASS}{\cmd{class}}
-\newcommand{\isasymINSTANCE}{\cmd{instance}}
-\newcommand{\isasymLEMMA}{\cmd{lemma}}
-\newcommand{\isasymPROOF}{\cmd{proof}}
-\newcommand{\isasymQED}{\cmd{qed}}
-\newcommand{\isasymFIX}{\cmd{fix}}
-\newcommand{\isasymASSUME}{\cmd{assume}}
-\newcommand{\isasymSHOW}{\cmd{show}}
-\newcommand{\isasymNOTE}{\cmd{note}}
-\newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
-\newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}}
-\newcommand{\isasymFUN}{\cmd{fun}}
-\newcommand{\isasymFUNCTION}{\cmd{function}}
-\newcommand{\isasymPRIMREC}{\cmd{primrec}}
-\newcommand{\isasymRECDEF}{\cmd{recdef}}
-
-\newcommand{\qt}[1]{``#1''}
-\newcommand{\qtt}[1]{"{}{#1}"{}}
-\newcommand{\qn}[1]{\emph{#1}}
-\newcommand{\strong}[1]{{\bfseries #1}}
-\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
-
-\newtheorem{exercise}{Exercise}{\bf}{\itshape}
-%\newtheorem*{thmstar}{Theorem}{\bf}{\itshape}
-
-\hyphenation{Isabelle}
-\hyphenation{Isar}
-
-\isadroptag{theory}
-\title{Defining Recursive Functions in Isabelle/HOL}
-\author{Alexander Krauss}
-
-\isabellestyle{tt}
-\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
-
-\begin{document}
-
-\date{\ \\}
-\maketitle
-
-\begin{abstract}
- This tutorial describes the use of the new \emph{function} package,
- which provides general recursive function definitions for Isabelle/HOL.
- We start with very simple examples and then gradually move on to more
- advanced topics such as manual termination proofs, nested recursion,
- partiality, tail recursion and congruence rules.
-\end{abstract}
-
-%\thispagestyle{empty}\clearpage
-
-%\pagenumbering{roman}
-%\clearfirst
-
-\input{intro.tex}
-\input{Functions.tex}
-%\input{conclusion.tex}
-
-\begingroup
-%\tocentry{\bibname}
-\bibliographystyle{plain} \small\raggedright\frenchspacing
-\bibliography{manual}
-\endgroup
-
-\end{document}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
--- a/doc-src/Functions/document/style.sty Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-%% toc
-\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
-\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
-
-%% references
-\newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\chref}[1]{chapter~\ref{#1}}
-\newcommand{\figref}[1]{figure~\ref{#1}}
-
-%% math
-\newcommand{\text}[1]{\mbox{#1}}
-\newcommand{\isasymvartheta}{\isamath{\theta}}
-\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
-
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
-
-\pagestyle{headings}
-\sloppy
-\binperiod
-\underscoreon
-
-\renewcommand{\isadigit}[1]{\isamath{#1}}
-
-\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
-
-\isafoldtag{FIXME}
-\isakeeptag{mlref}
-\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
-\renewcommand{\endisatagmlref}{\endgroup}
-
-\newcommand{\isasymGUESS}{\isakeyword{guess}}
-\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
-\newcommand{\isasymTHEORY}{\isakeyword{theory}}
-\newcommand{\isasymUSES}{\isakeyword{uses}}
-\newcommand{\isasymEND}{\isakeyword{end}}
-\newcommand{\isasymCONSTS}{\isakeyword{consts}}
-\newcommand{\isasymDEFS}{\isakeyword{defs}}
-\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
-\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
-
-\isabellestyle{it}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "implementation"
-%%% End:
--- a/doc-src/HOL/document/HOL.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2089 +0,0 @@
-\chapter{Higher-Order Logic}
-\index{higher-order logic|(}
-\index{HOL system@{\sc hol} system}
-
-\begin{figure}
-\begin{constants}
- \it name &\it meta-type & \it description \\
- \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
- \cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\
- \cdx{True} & $bool$ & tautology ($\top$) \\
- \cdx{False} & $bool$ & absurdity ($\bot$) \\
- \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\
- \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
-\end{constants}
-\subcaption{Constants}
-
-\begin{constants}
-\index{"@@{\tt\at} symbol}
-\index{*"! symbol}\index{*"? symbol}
-\index{*"?"! symbol}\index{*"E"X"! symbol}
- \it symbol &\it name &\it meta-type & \it description \\
- \sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ &
- Hilbert description ($\varepsilon$) \\
- \sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ &
- universal quantifier ($\forall$) \\
- \sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ &
- existential quantifier ($\exists$) \\
- \texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ &
- unique existence ($\exists!$)\\
- \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ &
- least element
-\end{constants}
-\subcaption{Binders}
-
-\begin{constants}
-\index{*"= symbol}
-\index{&@{\tt\&} symbol}
-\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
-\index{*"-"-"> symbol}
- \it symbol & \it meta-type & \it priority & \it description \\
- \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
- Left 55 & composition ($\circ$) \\
- \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\
- \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
- \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
- less than or equals ($\leq$)\\
- \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
- \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
- \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
-\end{constants}
-\subcaption{Infixes}
-\caption{Syntax of \texttt{HOL}} \label{hol-constants}
-\end{figure}
-
-
-\begin{figure}
-\index{*let symbol}
-\index{*in symbol}
-\dquotes
-\[\begin{array}{rclcl}
- term & = & \hbox{expression of class~$term$} \\
- & | & "SOME~" id " . " formula
- & | & "\at~" id " . " formula \\
- & | &
- \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\
- & | &
- \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\
- & | & "LEAST"~ id " . " formula \\[2ex]
- formula & = & \hbox{expression of type~$bool$} \\
- & | & term " = " term \\
- & | & term " \ttilde= " term \\
- & | & term " < " term \\
- & | & term " <= " term \\
- & | & "\ttilde\ " formula \\
- & | & formula " \& " formula \\
- & | & formula " | " formula \\
- & | & formula " --> " formula \\
- & | & "ALL~" id~id^* " . " formula
- & | & "!~~~" id~id^* " . " formula \\
- & | & "EX~~" id~id^* " . " formula
- & | & "?~~~" id~id^* " . " formula \\
- & | & "EX!~" id~id^* " . " formula
- & | & "?!~~" id~id^* " . " formula \\
- \end{array}
-\]
-\caption{Full grammar for HOL} \label{hol-grammar}
-\end{figure}
-
-
-\section{Syntax}
-
-Figure~\ref{hol-constants} lists the constants (including infixes and
-binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
-higher-order logic. Note that $a$\verb|~=|$b$ is translated to
-$\lnot(a=b)$.
-
-\begin{warn}
- HOL has no if-and-only-if connective; logical equivalence is expressed using
- equality. But equality has a high priority, as befitting a relation, while
- if-and-only-if typically has the lowest priority. Thus, $\lnot\lnot P=P$
- abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$. When using $=$
- to mean logical equivalence, enclose both operands in parentheses.
-\end{warn}
-
-\subsection{Types and overloading}
-The universal type class of higher-order terms is called~\cldx{term}.
-By default, explicit type variables have class \cldx{term}. In
-particular the equality symbol and quantifiers are polymorphic over
-class \texttt{term}.
-
-The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
-formulae are terms. The built-in type~\tydx{fun}, which constructs
-function types, is overloaded with arity {\tt(term,\thinspace
- term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt
- term} if $\sigma$ and~$\tau$ do, allowing quantification over
-functions.
-
-HOL allows new types to be declared as subsets of existing types,
-either using the primitive \texttt{typedef} or the more convenient
-\texttt{datatype} (see~{\S}\ref{sec:HOL:datatype}).
-
-Several syntactic type classes --- \cldx{plus}, \cldx{minus},
-\cldx{times} and
-\cldx{power} --- permit overloading of the operators {\tt+},\index{*"+
- symbol} {\tt-}\index{*"- symbol}, {\tt*}.\index{*"* symbol}
-and \verb|^|.\index{^@\verb.^. symbol}
-%
-They are overloaded to denote the obvious arithmetic operations on types
-\tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the
-exponent always has type~\tdx{nat}.) Non-arithmetic overloadings are also
-done: the operator {\tt-} can denote set difference, while \verb|^| can
-denote exponentiation of relations (iterated composition). Unary minus is
-also written as~{\tt-} and is overloaded like its 2-place counterpart; it even
-can stand for set complement.
-
-The constant \cdx{0} is also overloaded. It serves as the zero element of
-several types, of which the most important is \tdx{nat} (the natural
-numbers). The type class \cldx{plus_ac0} comprises all types for which 0
-and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These
-types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also
-multisets. The summation operator \cdx{setsum} is available for all types in
-this class.
-
-Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
-signatures. The relations $<$ and $\leq$ are polymorphic over this
-class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
-the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
-\cldx{order} of \cldx{ord} which axiomatizes the types that are partially
-ordered with respect to~$\leq$. A further subclass \cldx{linorder} of
-\cldx{order} axiomatizes linear orderings.
-For details, see the file \texttt{Ord.thy}.
-
-If you state a goal containing overloaded functions, you may need to include
-type constraints. Type inference may otherwise make the goal more
-polymorphic than you intended, with confusing results. For example, the
-variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type
-$\alpha::\{ord,plus\}$, although you may have expected them to have some
-numeric type, e.g. $nat$. Instead you should have stated the goal as
-$(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have
-type $nat$.
-
-\begin{warn}
- If resolution fails for no obvious reason, try setting
- \ttindex{show_types} to \texttt{true}, causing Isabelle to display
- types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as
- well, causing Isabelle to display type classes and sorts.
-
- \index{unification!incompleteness of}
- Where function types are involved, Isabelle's unification code does not
- guarantee to find instantiations for type variables automatically. Be
- prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},
- possibly instantiating type variables. Setting
- \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report
- omitted search paths during unification.\index{tracing!of unification}
-\end{warn}
-
-
-\subsection{Binders}
-
-Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$
-satisfying~$P$, if such exists. Since all terms in HOL denote something, a
-description is always meaningful, but we do not know its value unless $P$
-defines it uniquely. We may write descriptions as \cdx{Eps}($\lambda x.
-P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}.
-
-Existential quantification is defined by
-\[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
-The unique existence quantifier, $\exists!x. P$, is defined in terms
-of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
-quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates
-$\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there
-exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.
-
-\medskip
-
-\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The
-basic Isabelle/HOL binders have two notations. Apart from the usual
-\texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also
-supports the original notation of Gordon's {\sc hol} system: \texttt{!}\
-and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be
-followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a
-quantification. Both notations are accepted for input. The print mode
-``\ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by
-passing option \texttt{-m HOL} to the \texttt{isabelle} executable),
-then~{\tt!}\ and~{\tt?}\ are displayed.
-
-\medskip
-
-If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
-variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
-to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see
-Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$
-choice operator, so \texttt{Least} is always meaningful, but may yield
-nothing useful in case there is not a unique least element satisfying
-$P$.\footnote{Class $ord$ does not require much of its instances, so
- $\leq$ need not be a well-ordering, not even an order at all!}
-
-\medskip All these binders have priority 10.
-
-\begin{warn}
-The low priority of binders means that they need to be enclosed in
-parenthesis when they occur in the context of other operations. For example,
-instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.
-\end{warn}
-
-
-\subsection{The let and case constructions}
-Local abbreviations can be introduced by a \texttt{let} construct whose
-syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
-the constant~\cdx{Let}. It can be expanded by rewriting with its
-definition, \tdx{Let_def}.
-
-HOL also defines the basic syntax
-\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
-as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case}
-and \sdx{of} are reserved words. Initially, this is mere syntax and has no
-logical meaning. By declaring translations, you can cause instances of the
-\texttt{case} construct to denote applications of particular case operators.
-This is what happens automatically for each \texttt{datatype} definition
-(see~{\S}\ref{sec:HOL:datatype}).
-
-\begin{warn}
-Both \texttt{if} and \texttt{case} constructs have as low a priority as
-quantifiers, which requires additional enclosing parentheses in the context
-of most other operations. For example, instead of $f~x = {\tt if\dots
-then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots
-else\dots})$.
-\end{warn}
-
-\section{Rules of inference}
-
-\begin{figure}
-\begin{ttbox}\makeatother
-\tdx{refl} t = (t::'a)
-\tdx{subst} [| s = t; P s |] ==> P (t::'a)
-\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x)
-\tdx{impI} (P ==> Q) ==> P-->Q
-\tdx{mp} [| P-->Q; P |] ==> Q
-\tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
-\tdx{someI} P(x::'a) ==> P(@x. P x)
-\tdx{True_or_False} (P=True) | (P=False)
-\end{ttbox}
-\caption{The \texttt{HOL} rules} \label{hol-rules}
-\end{figure}
-
-Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with
-their~{\ML} names. Some of the rules deserve additional comments:
-\begin{ttdescription}
-\item[\tdx{ext}] expresses extensionality of functions.
-\item[\tdx{iff}] asserts that logically equivalent formulae are
- equal.
-\item[\tdx{someI}] gives the defining property of the Hilbert
- $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule
- \tdx{some_equality} (see below) is often easier to use.
-\item[\tdx{True_or_False}] makes the logic classical.\footnote{In
- fact, the $\varepsilon$-operator already makes the logic classical, as
- shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
-\end{ttdescription}
-
-
-\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
-\begin{ttbox}\makeatother
-\tdx{True_def} True == ((\%x::bool. x)=(\%x. x))
-\tdx{All_def} All == (\%P. P = (\%x. True))
-\tdx{Ex_def} Ex == (\%P. P(@x. P x))
-\tdx{False_def} False == (!P. P)
-\tdx{not_def} not == (\%P. P-->False)
-\tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R)
-\tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
-\tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x))
-
-\tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x))
-\tdx{if_def} If P x y ==
- (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))
-\tdx{Let_def} Let s f == f s
-\tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
-\end{ttbox}
-\caption{The \texttt{HOL} definitions} \label{hol-defs}
-\end{figure}
-
-
-HOL follows standard practice in higher-order logic: only a few connectives
-are taken as primitive, with the remainder defined obscurely
-(Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
-corresponding definitions \cite[page~270]{mgordon-hol} using
-object-equality~({\tt=}), which is possible because equality in higher-order
-logic may equate formulae and even functions over formulae. But theory~HOL,
-like all other Isabelle theories, uses meta-equality~({\tt==}) for
-definitions.
-\begin{warn}
-The definitions above should never be expanded and are shown for completeness
-only. Instead users should reason in terms of the derived rules shown below
-or, better still, using high-level tactics.
-\end{warn}
-
-Some of the rules mention type variables; for example, \texttt{refl}
-mentions the type variable~{\tt'a}. This allows you to instantiate
-type variables explicitly by calling \texttt{res_inst_tac}.
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{sym} s=t ==> t=s
-\tdx{trans} [| r=s; s=t |] ==> r=t
-\tdx{ssubst} [| t=s; P s |] ==> P t
-\tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d
-\tdx{arg_cong} x = y ==> f x = f y
-\tdx{fun_cong} f = g ==> f x = g x
-\tdx{cong} [| f = g; x = y |] ==> f x = g y
-\tdx{not_sym} t ~= s ==> s ~= t
-\subcaption{Equality}
-
-\tdx{TrueI} True
-\tdx{FalseE} False ==> P
-
-\tdx{conjI} [| P; Q |] ==> P&Q
-\tdx{conjunct1} [| P&Q |] ==> P
-\tdx{conjunct2} [| P&Q |] ==> Q
-\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
-
-\tdx{disjI1} P ==> P|Q
-\tdx{disjI2} Q ==> P|Q
-\tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
-
-\tdx{notI} (P ==> False) ==> ~ P
-\tdx{notE} [| ~ P; P |] ==> R
-\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
-\subcaption{Propositional logic}
-
-\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
-\tdx{iffD1} [| P=Q; P |] ==> Q
-\tdx{iffD2} [| P=Q; Q |] ==> P
-\tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
-\subcaption{Logical equivalence}
-
-\end{ttbox}
-\caption{Derived rules for HOL} \label{hol-lemmas1}
-\end{figure}
-%
-%\tdx{eqTrueI} P ==> P=True
-%\tdx{eqTrueE} P=True ==> P
-
-
-\begin{figure}
-\begin{ttbox}\makeatother
-\tdx{allI} (!!x. P x) ==> !x. P x
-\tdx{spec} !x. P x ==> P x
-\tdx{allE} [| !x. P x; P x ==> R |] ==> R
-\tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R
-
-\tdx{exI} P x ==> ? x. P x
-\tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q
-
-\tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x
-\tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R
- |] ==> R
-
-\tdx{some_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a
-\subcaption{Quantifiers and descriptions}
-
-\tdx{ccontr} (~P ==> False) ==> P
-\tdx{classical} (~P ==> P) ==> P
-\tdx{excluded_middle} ~P | P
-
-\tdx{disjCI} (~Q ==> P) ==> P|Q
-\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x
-\tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
-\tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
-\tdx{notnotD} ~~P ==> P
-\tdx{swap} ~P ==> (~Q ==> P) ==> Q
-\subcaption{Classical logic}
-
-\tdx{if_P} P ==> (if P then x else y) = x
-\tdx{if_not_P} ~ P ==> (if P then x else y) = y
-\tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))
-\subcaption{Conditionals}
-\end{ttbox}
-\caption{More derived rules} \label{hol-lemmas2}
-\end{figure}
-
-Some derived rules are shown in Figures~\ref{hol-lemmas1}
-and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
-for the logical connectives, as well as sequent-style elimination rules for
-conjunctions, implications, and universal quantifiers.
-
-Note the equality rules: \tdx{ssubst} performs substitution in
-backward proofs, while \tdx{box_equals} supports reasoning by
-simplifying both sides of an equation.
-
-The following simple tactics are occasionally useful:
-\begin{ttdescription}
-\item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}
- repeatedly to remove all outermost universal quantifiers and implications
- from subgoal $i$.
-\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on
- $P$ for subgoal $i$: the latter is replaced by two identical subgoals with
- the added assumptions $P$ and $\lnot P$, respectively.
-\item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then
- \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining
- from an induction hypothesis. As a generalization of \texttt{mp_tac},
- if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and
- $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables)
- then it replaces the universally quantified implication by $Q \vec{a}$.
- It may instantiate unknowns. It fails if it can do nothing.
-\end{ttdescription}
-
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{rrr}
- \it name &\it meta-type & \it description \\
-\index{{}@\verb'{}' symbol}
- \verb|{}| & $\alpha\,set$ & the empty set \\
- \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
- & insertion of element \\
- \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
- & comprehension \\
- \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
- & intersection over a set\\
- \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
- & union over a set\\
- \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
- &set of sets intersection \\
- \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
- &set of sets union \\
- \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$
- & powerset \\[1ex]
- \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
- & range of a function \\[1ex]
- \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
- & bounded quantifiers
-\end{tabular}
-\end{center}
-\subcaption{Constants}
-
-\begin{center}
-\begin{tabular}{llrrr}
- \it symbol &\it name &\it meta-type & \it priority & \it description \\
- \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
- intersection\\
- \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
- union
-\end{tabular}
-\end{center}
-\subcaption{Binders}
-
-\begin{center}
-\index{*"`"` symbol}
-\index{*": symbol}
-\index{*"<"= symbol}
-\begin{tabular}{rrrr}
- \it symbol & \it meta-type & \it priority & \it description \\
- \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$
- & Left 90 & image \\
- \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
- & Left 70 & intersection ($\int$) \\
- \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
- & Left 65 & union ($\un$) \\
- \tt: & $[\alpha ,\alpha\,set]\To bool$
- & Left 50 & membership ($\in$) \\
- \tt <= & $[\alpha\,set,\alpha\,set]\To bool$
- & Left 50 & subset ($\subseteq$)
-\end{tabular}
-\end{center}
-\subcaption{Infixes}
-\caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}
-\end{figure}
-
-
-\begin{figure}
-\begin{center} \tt\frenchspacing
-\index{*"! symbol}
-\begin{tabular}{rrr}
- \it external & \it internal & \it description \\
- $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm not in\\
- {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\
- {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) &
- \rm comprehension \\
- \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ &
- \rm intersection \\
- \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ &
- \rm union \\
- \sdx{ALL} $x$:$A$.\ $P[x]$ or \texttt{!} $x$:$A$.\ $P[x]$ &
- Ball $A$ $\lambda x.\ P[x]$ &
- \rm bounded $\forall$ \\
- \sdx{EX}{\tt\ } $x$:$A$.\ $P[x]$ or \texttt{?} $x$:$A$.\ $P[x]$ &
- Bex $A$ $\lambda x.\ P[x]$ & \rm bounded $\exists$
-\end{tabular}
-\end{center}
-\subcaption{Translations}
-
-\dquotes
-\[\begin{array}{rclcl}
- term & = & \hbox{other terms\ldots} \\
- & | & "{\ttlbrace}{\ttrbrace}" \\
- & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
- & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\
- & | & term " `` " term \\
- & | & term " Int " term \\
- & | & term " Un " term \\
- & | & "INT~~" id ":" term " . " term \\
- & | & "UN~~~" id ":" term " . " term \\
- & | & "INT~~" id~id^* " . " term \\
- & | & "UN~~~" id~id^* " . " term \\[2ex]
- formula & = & \hbox{other formulae\ldots} \\
- & | & term " : " term \\
- & | & term " \ttilde: " term \\
- & | & term " <= " term \\
- & | & "ALL " id ":" term " . " formula
- & | & "!~" id ":" term " . " formula \\
- & | & "EX~~" id ":" term " . " formula
- & | & "?~" id ":" term " . " formula \\
- \end{array}
-\]
-\subcaption{Full Grammar}
-\caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}
-\end{figure}
-
-
-\section{A formulation of set theory}
-Historically, higher-order logic gives a foundation for Russell and
-Whitehead's theory of classes. Let us use modern terminology and call them
-{\bf sets}, but note that these sets are distinct from those of ZF set theory,
-and behave more like ZF classes.
-\begin{itemize}
-\item
-Sets are given by predicates over some type~$\sigma$. Types serve to
-define universes for sets, but type-checking is still significant.
-\item
-There is a universal set (for each type). Thus, sets have complements, and
-may be defined by absolute comprehension.
-\item
-Although sets may contain other sets as elements, the containing set must
-have a more complex type.
-\end{itemize}
-Finite unions and intersections have the same behaviour in HOL as they do
-in~ZF. In HOL the intersection of the empty set is well-defined, denoting the
-universal set for the given type.
-
-\subsection{Syntax of set theory}\index{*set type}
-HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially
-the same as $\alpha\To bool$. The new type is defined for clarity and to
-avoid complications involving function types in unification. The isomorphisms
-between the two types are declared explicitly. They are very natural:
-\texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}
-maps in the other direction (ignoring argument order).
-
-Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
-translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
-constructs. Infix operators include union and intersection ($A\un B$
-and $A\int B$), the subset and membership relations, and the image
-operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
-$\lnot(a\in b)$.
-
-The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
-the obvious manner using~\texttt{insert} and~$\{\}$:
-\begin{eqnarray*}
- \{a, b, c\} & \equiv &
- \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
-\end{eqnarray*}
-
-The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of
-suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain
-free occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda x.
-P[x])$. It defines sets by absolute comprehension, which is impossible in~ZF;
-the type of~$x$ implicitly restricts the comprehension.
-
-The set theory defines two {\bf bounded quantifiers}:
-\begin{eqnarray*}
- \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
- \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
-\end{eqnarray*}
-The constants~\cdx{Ball} and~\cdx{Bex} are defined
-accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may
-write\index{*"! symbol}\index{*"? symbol}
-\index{*ALL symbol}\index{*EX symbol}
-%
-\hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The
-original notation of Gordon's {\sc hol} system is supported as well:
-\texttt{!}\ and \texttt{?}.
-
-Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
-$\bigcap@{x\in A}B[x]$, are written
-\sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and
-\sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.
-
-Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
-B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and
-\sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous
-union and intersection operators when $A$ is the universal set.
-
-The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
-not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
-respectively.
-
-
-
-\begin{figure} \underscoreon
-\begin{ttbox}
-\tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a
-\tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A
-
-\tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace}
-\tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B
-\tdx{Ball_def} Ball A P == ! x. x:A --> P x
-\tdx{Bex_def} Bex A P == ? x. x:A & P x
-\tdx{subset_def} A <= B == ! x:A. x:B
-\tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace}
-\tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace}
-\tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace}
-\tdx{Compl_def} -A == {\ttlbrace}x. ~ x:A{\ttrbrace}
-\tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}
-\tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}
-\tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B
-\tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B
-\tdx{Inter_def} Inter S == (INT x:S. x)
-\tdx{Union_def} Union S == (UN x:S. x)
-\tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace}
-\tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}
-\tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace}
-\end{ttbox}
-\caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}
-\end{figure}
-
-
-\begin{figure} \underscoreon
-\begin{ttbox}
-\tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace}
-\tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a
-\tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W
-
-\tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x
-\tdx{bspec} [| ! x:A. P x; x:A |] ==> P x
-\tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q
-
-\tdx{bexI} [| P x; x:A |] ==> ? x:A. P x
-\tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x
-\tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q
-\subcaption{Comprehension and Bounded quantifiers}
-
-\tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B
-\tdx{subsetD} [| A <= B; c:A |] ==> c:B
-\tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
-
-\tdx{subset_refl} A <= A
-\tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C
-
-\tdx{equalityI} [| A <= B; B <= A |] ==> A = B
-\tdx{equalityD1} A = B ==> A<=B
-\tdx{equalityD2} A = B ==> B<=A
-\tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
-
-\tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
- [| ~ c:A; ~ c:B |] ==> P
- |] ==> P
-\subcaption{The subset and equality relations}
-\end{ttbox}
-\caption{Derived rules for set theory} \label{hol-set1}
-\end{figure}
-
-
-\begin{figure} \underscoreon
-\begin{ttbox}
-\tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P
-
-\tdx{insertI1} a : insert a B
-\tdx{insertI2} a : B ==> a : insert b B
-\tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P
-
-\tdx{ComplI} [| c:A ==> False |] ==> c : -A
-\tdx{ComplD} [| c : -A |] ==> ~ c:A
-
-\tdx{UnI1} c:A ==> c : A Un B
-\tdx{UnI2} c:B ==> c : A Un B
-\tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
-\tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
-
-\tdx{IntI} [| c:A; c:B |] ==> c : A Int B
-\tdx{IntD1} c : A Int B ==> c:A
-\tdx{IntD2} c : A Int B ==> c:B
-\tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
-
-\tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x)
-\tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R
-
-\tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)
-\tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a
-\tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R
-
-\tdx{UnionI} [| X:C; A:X |] ==> A : Union C
-\tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R
-
-\tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C
-\tdx{InterD} [| A : Inter C; X:C |] ==> A:X
-\tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R
-
-\tdx{PowI} A<=B ==> A: Pow B
-\tdx{PowD} A: Pow B ==> A<=B
-
-\tdx{imageI} [| x:A |] ==> f x : f``A
-\tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P
-
-\tdx{rangeI} f x : range f
-\tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P
-\end{ttbox}
-\caption{Further derived rules for set theory} \label{hol-set2}
-\end{figure}
-
-
-\subsection{Axioms and rules of set theory}
-Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
-axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
-that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of
-course, \hbox{\tt op :} also serves as the membership relation.
-
-All the other axioms are definitions. They include the empty set, bounded
-quantifiers, unions, intersections, complements and the subset relation.
-They also include straightforward constructions on functions: image~({\tt``})
-and \texttt{range}.
-
-%The predicate \cdx{inj_on} is used for simulating type definitions.
-%The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the
-%set~$A$, which specifies a subset of its domain type. In a type
-%definition, $f$ is the abstraction function and $A$ is the set of valid
-%representations; we should not expect $f$ to be injective outside of~$A$.
-
-%\begin{figure} \underscoreon
-%\begin{ttbox}
-%\tdx{Inv_f_f} inj f ==> Inv f (f x) = x
-%\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y
-%
-%\tdx{Inv_injective}
-% [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y
-%
-%
-%\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f
-%\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B
-%
-%\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f
-%\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f
-%\tdx{injD} [| inj f; f x = f y |] ==> x=y
-%
-%\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A
-%\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y
-%
-%\tdx{inj_on_inverseI}
-% (!!x. x:A ==> g(f x) = x) ==> inj_on f A
-%\tdx{inj_on_contraD}
-% [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y
-%\end{ttbox}
-%\caption{Derived rules involving functions} \label{hol-fun}
-%\end{figure}
-
-
-\begin{figure} \underscoreon
-\begin{ttbox}
-\tdx{Union_upper} B:A ==> B <= Union A
-\tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C
-
-\tdx{Inter_lower} B:A ==> Inter A <= B
-\tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A
-
-\tdx{Un_upper1} A <= A Un B
-\tdx{Un_upper2} B <= A Un B
-\tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
-
-\tdx{Int_lower1} A Int B <= A
-\tdx{Int_lower2} A Int B <= B
-\tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
-\end{ttbox}
-\caption{Derived rules involving subsets} \label{hol-subset}
-\end{figure}
-
-
-\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
-\begin{ttbox}
-\tdx{Int_absorb} A Int A = A
-\tdx{Int_commute} A Int B = B Int A
-\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
-\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
-
-\tdx{Un_absorb} A Un A = A
-\tdx{Un_commute} A Un B = B Un A
-\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
-\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
-
-\tdx{Compl_disjoint} A Int (-A) = {\ttlbrace}x. False{\ttrbrace}
-\tdx{Compl_partition} A Un (-A) = {\ttlbrace}x. True{\ttrbrace}
-\tdx{double_complement} -(-A) = A
-\tdx{Compl_Un} -(A Un B) = (-A) Int (-B)
-\tdx{Compl_Int} -(A Int B) = (-A) Un (-B)
-
-\tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B)
-\tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C)
-
-\tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B)
-\tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C)
-
-\end{ttbox}
-\caption{Set equalities} \label{hol-equalities}
-\end{figure}
-%\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
-%\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)
-
-Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
-obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such
-as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical
-reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
-not strictly necessary but yield more natural proofs. Similarly,
-\tdx{equalityCE} supports classical reasoning about extensionality, after the
-fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for proofs
-pertaining to set theory.
-
-Figure~\ref{hol-subset} presents lattice properties of the subset relation.
-Unions form least upper bounds; non-empty intersections form greatest lower
-bounds. Reasoning directly about subsets often yields clearer proofs than
-reasoning about the membership relation. See the file \texttt{HOL/subset.ML}.
-
-Figure~\ref{hol-equalities} presents many common set equalities. They
-include commutative, associative and distributive laws involving unions,
-intersections and complements. For a complete listing see the file {\tt
-HOL/equalities.ML}.
-
-\begin{warn}
-\texttt{Blast_tac} proves many set-theoretic theorems automatically.
-Hence you seldom need to refer to the theorems above.
-\end{warn}
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{rrr}
- \it name &\it meta-type & \it description \\
- \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
- & injective/surjective \\
- \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$
- & injective over subset\\
- \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
-\end{tabular}
-\end{center}
-
-\underscoreon
-\begin{ttbox}
-\tdx{inj_def} inj f == ! x y. f x=f y --> x=y
-\tdx{surj_def} surj f == ! y. ? x. y=f x
-\tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y
-\tdx{inv_def} inv f == (\%y. @x. f(x)=y)
-\end{ttbox}
-\caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}
-\end{figure}
-
-\subsection{Properties of functions}\nopagebreak
-Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.
-Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse
-of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived
-rules. Reasoning about function composition (the operator~\sdx{o}) and the
-predicate~\cdx{surj} is done simply by expanding the definitions.
-
-There is also a large collection of monotonicity theorems for constructions
-on sets in the file \texttt{HOL/mono.ML}.
-
-
-\section{Simplification and substitution}
-
-Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
-(\texttt{simpset()}), which works for most purposes. A quite minimal
-simplification set for higher-order logic is~\ttindexbold{HOL_ss};
-even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which
-also expresses logical equivalence, may be used for rewriting. See
-the file \texttt{HOL/simpdata.ML} for a complete listing of the basic
-simplification rules.
-
-See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
-{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
-and simplification.
-
-\begin{warn}\index{simplification!of conjunctions}%
- Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The
- left part of a conjunction helps in simplifying the right part. This effect
- is not available by default: it can be slow. It can be obtained by
- including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
-\end{warn}
-
-\begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}%
- By default only the condition of an \ttindex{if} is simplified but not the
- \texttt{then} and \texttt{else} parts. Of course the latter are simplified
- once the condition simplifies to \texttt{True} or \texttt{False}. To ensure
- full simplification of all parts of a conditional you must remove
- \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$.
-\end{warn}
-
-If the simplifier cannot use a certain rewrite rule --- either because
-of nontermination or because its left-hand side is too flexible ---
-then you might try \texttt{stac}:
-\begin{ttdescription}
-\item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
- replaces in subgoal $i$ instances of $lhs$ by corresponding instances of
- $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking
- may be necessary to select the desired ones.
-
-If $thm$ is a conditional equality, the instantiated condition becomes an
-additional (first) subgoal.
-\end{ttdescription}
-
-HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an
-equality throughout a subgoal and its hypotheses. This tactic uses HOL's
-general substitution rule.
-
-\subsection{Case splitting}
-\label{subsec:HOL:case:splitting}
-
-HOL also provides convenient means for case splitting during rewriting. Goals
-containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}
-often require a case distinction on $b$. This is expressed by the theorem
-\tdx{split_if}:
-$$
-\Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
-((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))
-\eqno{(*)}
-$$
-For example, a simple instance of $(*)$ is
-\[
-x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~
-((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))
-\]
-Because $(*)$ is too general as a rewrite rule for the simplifier (the
-left-hand side is not a higher-order pattern in the sense of
-\iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%
-{Chap.\ts\ref{chap:simplification}}), there is a special infix function
-\ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}
-(analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a
-simpset, as in
-\begin{ttbox}
-by(simp_tac (simpset() addsplits [split_if]) 1);
-\end{ttbox}
-The effect is that after each round of simplification, one occurrence of
-\texttt{if} is split acording to \texttt{split_if}, until all occurences of
-\texttt{if} have been eliminated.
-
-It turns out that using \texttt{split_if} is almost always the right thing to
-do. Hence \texttt{split_if} is already included in the default simpset. If
-you want to delete it from a simpset, use \ttindexbold{delsplits}, which is
-the inverse of \texttt{addsplits}:
-\begin{ttbox}
-by(simp_tac (simpset() delsplits [split_if]) 1);
-\end{ttbox}
-
-In general, \texttt{addsplits} accepts rules of the form
-\[
-\Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs
-\]
-where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
-right form because internally the left-hand side is
-$\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples
-are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list}
-and~{\S}\ref{subsec:datatype:basics}).
-
-Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also
-imperative versions of \texttt{addsplits} and \texttt{delsplits}
-\begin{ttbox}
-\ttindexbold{Addsplits}: thm list -> unit
-\ttindexbold{Delsplits}: thm list -> unit
-\end{ttbox}
-for adding splitting rules to, and deleting them from the current simpset.
-
-
-\section{Types}\label{sec:HOL:Types}
-This section describes HOL's basic predefined types ($\alpha \times \beta$,
-$\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new
-types in general. The most important type construction, the
-\texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}.
-
-
-\subsection{Product and sum types}\index{*"* type}\index{*"+ type}
-\label{subsec:prod-sum}
-
-\begin{figure}[htbp]
-\begin{constants}
- \it symbol & \it meta-type & & \it description \\
- \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
- & & ordered pairs $(a,b)$ \\
- \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
- \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
- \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
- & & generalized projection\\
- \cdx{Sigma} &
- $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
- & general sum of sets
-\end{constants}
-%\tdx{fst_def} fst p == @a. ? b. p = (a,b)
-%\tdx{snd_def} snd p == @b. ? a. p = (a,b)
-%\tdx{split_def} split c p == c (fst p) (snd p)
-\begin{ttbox}\makeatletter
-\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
-
-\tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b')
-\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R
-\tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q
-
-\tdx{fst_conv} fst (a,b) = a
-\tdx{snd_conv} snd (a,b) = b
-\tdx{surjective_pairing} p = (fst p,snd p)
-
-\tdx{split} split c (a,b) = c a b
-\tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
-
-\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
-
-\tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P
- |] ==> P
-\end{ttbox}
-\caption{Type $\alpha\times\beta$}\label{hol-prod}
-\end{figure}
-
-Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type
-$\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General
-tuples are simulated by pairs nested to the right:
-\begin{center}
-\begin{tabular}{c|c}
-external & internal \\
-\hline
-$\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\
-\hline
-$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
-\end{tabular}
-\end{center}
-In addition, it is possible to use tuples
-as patterns in abstractions:
-\begin{center}
-{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)}
-\end{center}
-Nested patterns are also supported. They are translated stepwise:
-\begin{eqnarray*}
-\hbox{\tt\%($x$,$y$,$z$).\ $t$}
- & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\
- & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\
- & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))}
-\end{eqnarray*}
-The reverse translation is performed upon printing.
-\begin{warn}
- The translation between patterns and \texttt{split} is performed automatically
- by the parser and printer. Thus the internal and external form of a term
- may differ, which can affects proofs. For example the term {\tt
- (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the
- default simpset) to rewrite to {\tt(b,a)}.
-\end{warn}
-In addition to explicit $\lambda$-abstractions, patterns can be used in any
-variable binding construct which is internally described by a
-$\lambda$-abstraction. Some important examples are
-\begin{description}
-\item[Let:] \texttt{let {\it pattern} = $t$ in $u$}
-\item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$}
-\item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$}
-\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}
-\item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}}
-\end{description}
-
-There is a simple tactic which supports reasoning about patterns:
-\begin{ttdescription}
-\item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all
- {\tt!!}-quantified variables of product type by individual variables for
- each component. A simple example:
-\begin{ttbox}
-{\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}
-by(split_all_tac 1);
-{\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}
-\end{ttbox}
-\end{ttdescription}
-
-Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}
-which contains only a single element named {\tt()} with the property
-\begin{ttbox}
-\tdx{unit_eq} u = ()
-\end{ttbox}
-\bigskip
-
-Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$
-which associates to the right and has a lower priority than $*$: $\tau@1 +
-\tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.
-
-The definition of products and sums in terms of existing types is not
-shown. The constructions are fairly standard and can be found in the
-respective theory files. Although the sum and product types are
-constructed manually for foundational reasons, they are represented as
-actual datatypes later.
-
-\begin{figure}
-\begin{constants}
- \it symbol & \it meta-type & & \it description \\
- \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
- \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
- \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
- & & conditional
-\end{constants}
-\begin{ttbox}\makeatletter
-\tdx{Inl_not_Inr} Inl a ~= Inr b
-
-\tdx{inj_Inl} inj Inl
-\tdx{inj_Inr} inj Inr
-
-\tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s
-
-\tdx{sum_case_Inl} sum_case f g (Inl x) = f x
-\tdx{sum_case_Inr} sum_case f g (Inr x) = g x
-
-\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
-\tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
- (! y. s = Inr(y) --> R(g(y))))
-\end{ttbox}
-\caption{Type $\alpha+\beta$}\label{hol-sum}
-\end{figure}
-
-\begin{figure}
-\index{*"< symbol}
-\index{*"* symbol}
-\index{*div symbol}
-\index{*mod symbol}
-\index{*dvd symbol}
-\index{*"+ symbol}
-\index{*"- symbol}
-\begin{constants}
- \it symbol & \it meta-type & \it priority & \it description \\
- \cdx{0} & $\alpha$ & & zero \\
- \cdx{Suc} & $nat \To nat$ & & successor function\\
- \tt * & $[\alpha,\alpha]\To \alpha$ & Left 70 & multiplication \\
- \tt div & $[\alpha,\alpha]\To \alpha$ & Left 70 & division\\
- \tt mod & $[\alpha,\alpha]\To \alpha$ & Left 70 & modulus\\
- \tt dvd & $[\alpha,\alpha]\To bool$ & Left 70 & ``divides'' relation\\
- \tt + & $[\alpha,\alpha]\To \alpha$ & Left 65 & addition\\
- \tt - & $[\alpha,\alpha]\To \alpha$ & Left 65 & subtraction
-\end{constants}
-\subcaption{Constants and infixes}
-
-\begin{ttbox}\makeatother
-\tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n
-
-\tdx{Suc_not_Zero} Suc m ~= 0
-\tdx{inj_Suc} inj Suc
-\tdx{n_not_Suc_n} n~=Suc n
-\subcaption{Basic properties}
-\end{ttbox}
-\caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}\makeatother
- 0+n = n
- (Suc m)+n = Suc(m+n)
-
- m-0 = m
- 0-n = n
- Suc(m)-Suc(n) = m-n
-
- 0*n = 0
- Suc(m)*n = n + m*n
-
-\tdx{mod_less} m<n ==> m mod n = m
-\tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n
-
-\tdx{div_less} m<n ==> m div n = 0
-\tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)
-\end{ttbox}
-\caption{Recursion equations for the arithmetic operators} \label{hol-nat2}
-\end{figure}
-
-\subsection{The type of natural numbers, \textit{nat}}
-\index{nat@{\textit{nat}} type|(}
-
-The theory \thydx{Nat} defines the natural numbers in a roundabout but
-traditional way. The axiom of infinity postulates a type~\tydx{ind} of
-individuals, which is non-empty and closed under an injective operation. The
-natural numbers are inductively generated by choosing an arbitrary individual
-for~0 and using the injective operation to take successors. This is a least
-fixedpoint construction.
-
-Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded
-functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min},
-\cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat}
-also shows that {\tt<=} is a linear order, so \tydx{nat} is
-also an instance of class \cldx{linorder}.
-
-Theory \thydx{NatArith} develops arithmetic on the natural numbers. It defines
-addition, multiplication and subtraction. Theory \thydx{Divides} defines
-division, remainder and the ``divides'' relation. The numerous theorems
-proved include commutative, associative, distributive, identity and
-cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The
-recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on
-\texttt{nat} are part of the default simpset.
-
-Functions on \tydx{nat} can be defined by primitive or well-founded recursion;
-see {\S}\ref{sec:HOL:recursive}. A simple example is addition.
-Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
-the standard convention.
-\begin{ttbox}
-\sdx{primrec}
- "0 + n = n"
- "Suc m + n = Suc (m + n)"
-\end{ttbox}
-There is also a \sdx{case}-construct
-of the form
-\begin{ttbox}
-case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)
-\end{ttbox}
-Note that Isabelle insists on precisely this format; you may not even change
-the order of the two cases.
-Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
-\cdx{nat_rec}, which is available because \textit{nat} is represented as
-a datatype.
-
-%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
-%Recursion along this relation resembles primitive recursion, but is
-%stronger because we are in higher-order logic; using primitive recursion to
-%define a higher-order function, we can easily Ackermann's function, which
-%is not primitive recursive \cite[page~104]{thompson91}.
-%The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
-%natural numbers are most easily expressed using recursion along~$<$.
-
-Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$
-in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived
-theorem \tdx{less_induct}:
-\begin{ttbox}
-[| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n
-\end{ttbox}
-
-
-\subsection{Numerical types and numerical reasoning}
-
-The integers (type \tdx{int}) are also available in HOL, and the reals (type
-\tdx{real}) are available in the logic image \texttt{HOL-Complex}. They support
-the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and
-multiplication (\texttt{*}), and much else. Type \tdx{int} provides the
-\texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real
-division and other operations. Both types belong to class \cldx{linorder}, so
-they inherit the relational operators and all the usual properties of linear
-orderings. For full details, please survey the theories in subdirectories
-\texttt{Integ}, \texttt{Real}, and \texttt{Complex}.
-
-All three numeric types admit numerals of the form \texttt{$sd\ldots d$},
-where $s$ is an optional minus sign and $d\ldots d$ is a string of digits.
-Numerals are represented internally by a datatype for binary notation, which
-allows numerical calculations to be performed by rewriting. For example, the
-integer division of \texttt{54342339} by \texttt{3452} takes about five
-seconds. By default, the simplifier cancels like terms on the opposite sites
-of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for
-instance. The simplifier also collects like terms, replacing \texttt{x+y+x*3}
-by \texttt{4*x+y}.
-
-Sometimes numerals are not wanted, because for example \texttt{n+3} does not
-match a pattern of the form \texttt{Suc $k$}. You can re-arrange the form of
-an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such as
-\texttt{n+3 = Suc (Suc (Suc n))}. As an alternative, you can disable the
-fancier simplifications by using a basic simpset such as \texttt{HOL_ss}
-rather than the default one, \texttt{simpset()}.
-
-Reasoning about arithmetic inequalities can be tedious. Fortunately, HOL
-provides a decision procedure for \emph{linear arithmetic}: formulae involving
-addition and subtraction. The simplifier invokes a weak version of this
-decision procedure automatically. If this is not sufficent, you can invoke the
-full procedure \ttindex{Lin_Arith.tac} explicitly. It copes with arbitrary
-formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
- min}, {\tt max} and numerical constants. Other subterms are treated as
-atomic, while subformulae not involving numerical types are ignored. Quantified
-subformulae are ignored unless they are positive universal or negative
-existential. The running time is exponential in the number of
-occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case
-distinctions.
-If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
-{\tt k dvd} are also supported. The former two are eliminated
-by case distinctions, again blowing up the running time.
-If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take
-super-exponential time and space.
-
-If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in
-the library. The theories \texttt{Nat} and \texttt{NatArith} contain
-theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
-Theory \texttt{Divides} contains theorems about \texttt{div} and
-\texttt{mod}. Use Proof General's \emph{find} button (or other search
-facilities) to locate them.
-
-\index{nat@{\textit{nat}} type|)}
-
-
-\begin{figure}
-\index{#@{\tt[]} symbol}
-\index{#@{\tt\#} symbol}
-\index{"@@{\tt\at} symbol}
-\index{*"! symbol}
-\begin{constants}
- \it symbol & \it meta-type & \it priority & \it description \\
- \tt[] & $\alpha\,list$ & & empty list\\
- \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &
- list constructor \\
- \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\
- \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\
- \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\
- \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\
- \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
- \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
- \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
- & & apply to all\\
- \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
- & & filter functional\\
- \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
- \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\
- \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
- & iteration \\
- \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\
- \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\
- \cdx{length} & $\alpha\,list \To nat$ & & length \\
- \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\
- \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&
- take/drop a prefix \\
- \cdx{takeWhile},\\
- \cdx{dropWhile} &
- $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&
- take/drop a prefix
-\end{constants}
-\subcaption{Constants and infixes}
-
-\begin{center} \tt\frenchspacing
-\begin{tabular}{rrr}
- \it external & \it internal & \it description \\{}
- [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
- \rm finite list \\{}
- [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ &
- \rm list comprehension
-\end{tabular}
-\end{center}
-\subcaption{Translations}
-\caption{The theory \thydx{List}} \label{hol-list}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}\makeatother
-null [] = True
-null (x#xs) = False
-
-hd (x#xs) = x
-
-tl (x#xs) = xs
-tl [] = []
-
-[] @ ys = ys
-(x#xs) @ ys = x # xs @ ys
-
-set [] = \ttlbrace\ttrbrace
-set (x#xs) = insert x (set xs)
-
-x mem [] = False
-x mem (y#ys) = (if y=x then True else x mem ys)
-
-concat([]) = []
-concat(x#xs) = x @ concat(xs)
-
-rev([]) = []
-rev(x#xs) = rev(xs) @ [x]
-
-length([]) = 0
-length(x#xs) = Suc(length(xs))
-
-xs!0 = hd xs
-xs!(Suc n) = (tl xs)!n
-\end{ttbox}
-\caption{Simple list processing functions}
-\label{fig:HOL:list-simps}
-\end{figure}
-
-\begin{figure}
-\begin{ttbox}\makeatother
-map f [] = []
-map f (x#xs) = f x # map f xs
-
-filter P [] = []
-filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
-
-foldl f a [] = a
-foldl f a (x#xs) = foldl f (f a x) xs
-
-take n [] = []
-take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)
-
-drop n [] = []
-drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)
-
-takeWhile P [] = []
-takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])
-
-dropWhile P [] = []
-dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)
-\end{ttbox}
-\caption{Further list processing functions}
-\label{fig:HOL:list-simps2}
-\end{figure}
-
-
-\subsection{The type constructor for lists, \textit{list}}
-\label{subsec:list}
-\index{list@{\textit{list}} type|(}
-
-Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
-operations with their types and syntax. Type $\alpha \; list$ is
-defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.
-As a result the generic structural induction and case analysis tactics
-\texttt{induct\_tac} and \texttt{cases\_tac} also become available for
-lists. A \sdx{case} construct of the form
-\begin{center}\tt
-case $e$ of [] => $a$ | \(x\)\#\(xs\) => b
-\end{center}
-is defined by translation. For details see~{\S}\ref{sec:HOL:datatype}. There
-is also a case splitting rule \tdx{split_list_case}
-\[
-\begin{array}{l}
-P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~
- x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\
-((e = \texttt{[]} \to P(a)) \land
- (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))
-\end{array}
-\]
-which can be fed to \ttindex{addsplits} just like
-\texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).
-
-\texttt{List} provides a basic library of list processing functions defined by
-primitive recursion. The recursion equations
-are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}.
-
-\index{list@{\textit{list}} type|)}
-
-
-\section{Datatype definitions}
-\label{sec:HOL:datatype}
-\index{*datatype|(}
-
-Inductive datatypes, similar to those of \ML, frequently appear in
-applications of Isabelle/HOL. In principle, such types could be defined by
-hand via \texttt{typedef}, but this would be far too
-tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\
-\cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an
-appropriate \texttt{typedef} based on a least fixed-point construction, and
-proves freeness theorems and induction rules, as well as theorems for
-recursion and case combinators. The user just has to give a simple
-specification of new inductive types using a notation similar to {\ML} or
-Haskell.
-
-The current datatype package can handle both mutual and indirect recursion.
-It also offers to represent existing types as datatypes giving the advantage
-of a more uniform view on standard theories.
-
-
-\subsection{Basics}
-\label{subsec:datatype:basics}
-
-A general \texttt{datatype} definition is of the following form:
-\[
-\begin{array}{llcl}
-\mathtt{datatype} & (\vec{\alpha})t@1 & = &
- C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~
- C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\
- & & \vdots \\
-\mathtt{and} & (\vec{\alpha})t@n & = &
- C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~
- C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}}
-\end{array}
-\]
-where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables,
-$C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em
- admissible} types containing at most the type variables $\alpha@1, \ldots,
-\alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em
- admissible} if and only if
-\begin{itemize}
-\item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the
-newly defined type constructors $t@1,\ldots,t@n$, or
-\item $\tau = (\vec{\alpha})t@{j'}$ where $1 \leq j' \leq n$, or
-\item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is
-the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$
-are admissible types.
-\item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible
-type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined
-types are {\em strictly positive})
-\end{itemize}
-If some $(\vec{\alpha})t@{j'}$ occurs in a type $\tau^j@{i,i'}$
-of the form
-\[
-(\ldots,\ldots ~ (\vec{\alpha})t@{j'} ~ \ldots,\ldots)t'
-\]
-this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple
-example of a datatype is the type \texttt{list}, which can be defined by
-\begin{ttbox}
-datatype 'a list = Nil
- | Cons 'a ('a list)
-\end{ttbox}
-Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled
-by the mutually recursive datatype definition
-\begin{ttbox}
-datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)
- | Sum ('a aexp) ('a aexp)
- | Diff ('a aexp) ('a aexp)
- | Var 'a
- | Num nat
-and 'a bexp = Less ('a aexp) ('a aexp)
- | And ('a bexp) ('a bexp)
- | Or ('a bexp) ('a bexp)
-\end{ttbox}
-The datatype \texttt{term}, which is defined by
-\begin{ttbox}
-datatype ('a, 'b) term = Var 'a
- | App 'b ((('a, 'b) term) list)
-\end{ttbox}
-is an example for a datatype with nested recursion. Using nested recursion
-involving function spaces, we may also define infinitely branching datatypes, e.g.
-\begin{ttbox}
-datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
-\end{ttbox}
-
-\medskip
-
-Types in HOL must be non-empty. Each of the new datatypes
-$(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a
-constructor $C^j@i$ with the following property: for all argument types
-$\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype
-$(\vec{\alpha})t@{j'}$ is non-empty.
-
-If there are no nested occurrences of the newly defined datatypes, obviously
-at least one of the newly defined datatypes $(\vec{\alpha})t@j$
-must have a constructor $C^j@i$ without recursive arguments, a \emph{base
- case}, to ensure that the new types are non-empty. If there are nested
-occurrences, a datatype can even be non-empty without having a base case
-itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t
- list)} is non-empty as well.
-
-
-\subsubsection{Freeness of the constructors}
-
-The datatype constructors are automatically defined as functions of their
-respective type:
-\[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \]
-These functions have certain {\em freeness} properties. They construct
-distinct values:
-\[
-C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad
-\mbox{for all}~ i \neq i'.
-\]
-The constructor functions are injective:
-\[
-(C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =
-(x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})
-\]
-Since the number of distinctness inequalities is quadratic in the number of
-constructors, the datatype package avoids proving them separately if there are
-too many constructors. Instead, specific inequalities are proved by a suitable
-simplification procedure on demand.\footnote{This procedure, which is already part
-of the default simpset, may be referred to by the ML identifier
-\texttt{DatatypePackage.distinct_simproc}.}
-
-\subsubsection{Structural induction}
-
-The datatype package also provides structural induction rules. For
-datatypes without nested recursion, this is of the following form:
-\[
-\infer{P@1~x@1 \land \dots \land P@n~x@n}
- {\begin{array}{lcl}
- \Forall x@1 \dots x@{m^1@1}.
- \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;
- P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp &
- P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\
- & \vdots \\
- \Forall x@1 \dots x@{m^1@{k@1}}.
- \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots;
- P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp &
- P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\
- & \vdots \\
- \Forall x@1 \dots x@{m^n@1}.
- \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots;
- P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp &
- P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\
- & \vdots \\
- \Forall x@1 \dots x@{m^n@{k@n}}.
- \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots
- P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp &
- P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right)
- \end{array}}
-\]
-where
-\[
-\begin{array}{rcl}
-Rec^j@i & := &
- \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
- \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]
-&& \left\{(i',i'')~\left|~
- 1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land
- \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}
-\end{array}
-\]
-i.e.\ the properties $P@j$ can be assumed for all recursive arguments.
-
-For datatypes with nested recursion, such as the \texttt{term} example from
-above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds
-a definition like
-\begin{ttbox}
-datatype ('a,'b) term = Var 'a
- | App 'b ((('a, 'b) term) list)
-\end{ttbox}
-to an equivalent definition without nesting:
-\begin{ttbox}
-datatype ('a,'b) term = Var
- | App 'b (('a, 'b) term_list)
-and ('a,'b) term_list = Nil'
- | Cons' (('a,'b) term) (('a,'b) term_list)
-\end{ttbox}
-Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt
- Nil'} and \texttt{Cons'} are not really introduced. One can directly work with
-the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing
-constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
-\texttt{term} gets the form
-\[
-\infer{P@1~x@1 \land P@2~x@2}
- {\begin{array}{l}
- \Forall x.~P@1~(\mathtt{Var}~x) \\
- \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\
- P@2~\mathtt{Nil} \\
- \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)
- \end{array}}
-\]
-Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}
-and one for the type \texttt{(('a, 'b) term) list}.
-
-For a datatype with function types such as \texttt{'a tree}, the induction rule
-is of the form
-\[
-\infer{P~t}
- {\Forall a.~P~(\mathtt{Atom}~a) &
- \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)}
-\]
-
-\medskip In principle, inductive types are already fully determined by
-freeness and structural induction. For convenience in applications,
-the following derived constructions are automatically provided for any
-datatype.
-
-\subsubsection{The \sdx{case} construct}
-
-The type comes with an \ML-like \texttt{case}-construct:
-\[
-\begin{array}{rrcl}
-\mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\
- \vdots \\
- \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j}
-\end{array}
-\]
-where the $x@{i,j}$ are either identifiers or nested tuple patterns as in
-{\S}\ref{subsec:prod-sum}.
-\begin{warn}
- All constructors must be present, their order is fixed, and nested patterns
- are not supported (with the exception of tuples). Violating this
- restriction results in strange error messages.
-\end{warn}
-
-To perform case distinction on a goal containing a \texttt{case}-construct,
-the theorem $t@j.$\texttt{split} is provided:
-\[
-\begin{array}{@{}rcl@{}}
-P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=&
-\!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to
- P(f@1~x@1\dots x@{m^j@1})) \\
-&&\!\!\! ~\land~ \dots ~\land \\
-&&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to
- P(f@{k@j}~x@1\dots x@{m^j@{k@j}})))
-\end{array}
-\]
-where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.
-This theorem can be added to a simpset via \ttindex{addsplits}
-(see~{\S}\ref{subsec:HOL:case:splitting}).
-
-Case splitting on assumption works as well, by using the rule
-$t@j.$\texttt{split_asm} in the same manner. Both rules are available under
-$t@j.$\texttt{splits} (this name is \emph{not} bound in ML, though).
-
-\begin{warn}\index{simplification!of \texttt{case}}%
- By default only the selector expression ($e$ above) in a
- \texttt{case}-construct is simplified, in analogy with \texttt{if} (see
- page~\pageref{if-simp}). Only if that reduces to a constructor is one of
- the arms of the \texttt{case}-construct exposed and simplified. To ensure
- full simplification of all parts of a \texttt{case}-construct for datatype
- $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for
- example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.
-\end{warn}
-
-\subsubsection{The function \cdx{size}}\label{sec:HOL:size}
-
-Theory \texttt{NatArith} declares a generic function \texttt{size} of type
-$\alpha\To nat$. Each datatype defines a particular instance of \texttt{size}
-by overloading according to the following scheme:
-%%% FIXME: This formula is too big and is completely unreadable
-\[
-size(C^j@i~x@1~\dots~x@{m^j@i}) = \!
-\left\{
-\begin{array}{ll}
-0 & \!\mbox{if $Rec^j@i = \emptyset$} \\
-1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} &
- \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
- \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$}
-\end{array}
-\right.
-\]
-where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the
-size of a leaf is 0 and the size of a node is the sum of the sizes of its
-subtrees ${}+1$.
-
-\subsection{Defining datatypes}
-
-The theory syntax for datatype definitions is given in the
-Isabelle/Isar reference manual. In order to be well-formed, a
-datatype definition has to obey the rules stated in the previous
-section. As a result the theory is exte
