summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 28 Aug 2012 18:57:32 +0200 | |

changeset 48985 | 5386df44a037 |

parent 48984 | f51d4a302962 |

child 48986 | 037d32448e29 |

renamed doc-src to src/Doc;
renamed TutorialI to Tutorial;

--- 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 extended with the new types, the -constructors, and the theorems listed in the previous section. - -Most of the theorems about datatypes become part of the default simpset and -you never need to see them again because the simplifier applies them -automatically. Only induction or case distinction are usually invoked by hand. -\begin{ttdescription} -\item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] - applies structural induction on variable $x$ to subgoal $i$, provided the - type of $x$ is a datatype. -\item[\texttt{induct_tac} - {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous - structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This - is the canonical way to prove properties of mutually recursive datatypes - such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as - \texttt{term}. -\end{ttdescription} -In some cases, induction is overkill and a case distinction over all -constructors of the datatype suffices. -\begin{ttdescription} -\item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$]