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

author | wenzelm |

Wed, 24 May 2006 21:58:07 +0200 | |

changeset 19711 | 2401b1a3087f |

parent 19710 | ee9c7fa80d21 |

child 19712 | 3ae3cc4b1eac |

Pure: update on overloaded defs;

NEWS | file | annotate | diff | comparison | revisions | |

doc-src/IsarRef/pure.tex | file | annotate | diff | comparison | revisions |

--- a/NEWS Wed May 24 10:02:36 2006 +0200 +++ b/NEWS Wed May 24 21:58:07 2006 +0200 @@ -38,19 +38,22 @@ syntax. * Overloaded definitions are now actually checked for acyclic -dependencies. Overloading of some constant c :: 'a decl is restricted -to schematic instances c :: ('b)t decl, for any type constructor t. -The RHS may mention overloaded constants recursively at type instances -corresponding to the immediate argument types 'b. This scheme covers -the disciplined overloading of Haskell98, although Isabelle does not -demand an exact correspondence to type class and instance -declarations. There is an internal dependency graph of all overloaded -and non-overloaded definitions, which ensures that the collection of -interdependent constants in a theory can still be interpreted in terms -of the basic logic. - -INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more -exotic overloading schemes -- at the discretion of the user! +dependencies. The overloading scheme covers is slightly more general +that the disciplined overloading of Haskell98, although Isabelle does +not demand an exact correspondence to type class and instance +declarations. INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to +admit more exotic overloading schemes. + +Polymorphic constants are represented via type arguments, i.e. the +instantiation that matches an instance against the most general +declaration given in the signature. For example, with the declaration +c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented +as c(nat). Overloading is essentially simultaneous structural +recursion over such type arguments. Incomplete specification patterns +impose global constraints on all occurrences, e.g. defining c('a * 'a) +means that general c('a * 'b) will be disallowed. Command +'print_theory' outputs the normalized system of recursive equations, +see section "definitions". * Isar: improper proof element 'guess' is like 'obtain', but derives the obtained context from the course of reasoning! For example:

--- a/doc-src/IsarRef/pure.tex Wed May 24 10:02:36 2006 +0200 +++ b/doc-src/IsarRef/pure.tex Wed May 24 21:58:07 2006 +0200 @@ -264,15 +264,11 @@ decl$ may be defined separately on type instances $c :: (\vec\beta)\,t\,decl$ for each type constructor $t$. The RHS may mention overloaded constants recursively at type instances -corresponding to the immediate argument types $\vec\beta$. This -scheme covers the disciplined overloading of Haskell98, although -Isabelle does not demand an exact correspondence to type class and -instance declarations. - -There is an internal dependency graph of all overloaded and -non-overloaded definitions, which ensures that the collection of -interdependent constants in a theory can still be interpreted in terms -of the basic logic. +corresponding to the immediate argument types $\vec\beta$. Incomplete +specification patterns impose global constraints on all occurrences, +e.g. $d :: \alpha \times \alpha$ on the LHS means that all +corresponding occurrences on some RHS need to be an instance of this, +general $d :: \alpha \times \beta$ will be disallowed. \indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl} \begin{matharray}{rcl}