# HG changeset patch # User wenzelm # Date 1443217148 -7200 # Node ID 64a5bce1f49859f67bf459a1f1c9183e226b87f1 # Parent abe08fb15a121b4267df9086daf3289c163141e9 documentation for "Semantic subtype definitions"; misc tuning and simplification; diff -r abe08fb15a12 -r 64a5bce1f498 NEWS --- a/NEWS Fri Sep 25 20:37:59 2015 +0200 +++ b/NEWS Fri Sep 25 23:39:08 2015 +0200 @@ -197,6 +197,13 @@ *** HOL *** +* The 'typedef' command has been upgraded from a partially checked +"axiomatization", to a full definitional specification that takes the +global collection of overloaded constant / type definitions into +account. Type definitions with open dependencies on overloaded +definitions need to be specified as "typedef (overloaded)". This +provides extra robustness in theory construction. Rare INCOMPATIBILITY. + * Qualification of various formal entities in the libraries is done more uniformly via "context begin qualified definition ... end" instead of old-style "hide_const (open) ...". Consequently, both the defined diff -r abe08fb15a12 -r 64a5bce1f498 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Sep 25 20:37:59 2015 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Sep 25 23:39:08 2015 +0200 @@ -1100,35 +1100,22 @@ text \See @{file "~~/src/HOL/ex/Records.thy"}, for example.\ -section \Typedef axiomatization \label{sec:hol-typedef}\ +section \Semantic subtype definitions \label{sec:hol-typedef}\ text \ \begin{matharray}{rcl} @{command_def (HOL) "typedef"} & : & @{text "local_theory \ proof(prove)"} \\ \end{matharray} - A Gordon/HOL-style type definition is a certain axiom scheme that - identifies a new type with a subset of an existing type. More - precisely, the new type is defined by exhibiting an existing type - @{text \}, a set @{text "A :: \ set"}, and a theorem that proves - @{prop "\x. x \ A"}. Thus @{text A} is a non-empty subset of @{text - \}, and the new type denotes this subset. New functions are - postulated that establish an isomorphism between the new type and - the subset. In general, the type @{text \} may involve type - variables @{text "\\<^sub>1, \, \\<^sub>n"} which means that the type definition - produces a type constructor @{text "(\\<^sub>1, \, \\<^sub>n) t"} depending on - those type arguments. - - The axiomatization can be considered a ``definition'' in the sense of the - particular set-theoretic interpretation of HOL @{cite pitts93}, where the - universe of types is required to be downwards-closed wrt.\ arbitrary - non-empty subsets. Thus genuinely new types introduced by @{command - "typedef"} stay within the range of HOL models by construction. - - In contrast, the command @{command_ref type_synonym} from Isabelle/Pure - merely introduces syntactic abbreviations, without any logical - significance. Thus it is more faithful to the idea of a genuine type - definition, but less powerful in practice. + A type definition identifies a new type with a non-empty subset of an + existing type. More precisely, the new type is defined by exhibiting an + existing type @{text \}, a set @{text "A :: \ set"}, and proving @{prop + "\x. x \ A"}. Thus @{text A} is a non-empty subset of @{text \}, and the + new type denotes this subset. New functions are postulated that establish + an isomorphism between the new type and the subset. In general, the type + @{text \} may involve type variables @{text "\\<^sub>1, \, \\<^sub>n"} which means + that the type definition produces a type constructor @{text "(\\<^sub>1, \, \\<^sub>n) + t"} depending on those type arguments. @{rail \ @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set @@ -1140,23 +1127,63 @@ rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})? \} + To understand the concept of type definition better, we need to recount + its somewhat complex history. The HOL logic goes back to the ``Simple + Theory of Types'' (STT) of A. Church @{cite "church40"}, which is further + explained in the book by P. Andrews @{cite "andrews86"}. The overview + article by W. Farmer @{cite "Farmer:2008"} points out the ``seven + virtues'' of this relatively simple family of logics. STT has only ground + types, without polymorphism and without type definitions. + + \medskip M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by + adding schematic polymorphism (type variables and type constructors) and a + facility to introduce new types as semantic subtypes from existing types. + This genuine extension of the logic was explained semantically by A. Pitts + in the book of the original Cambridge HOL88 system @{cite "pitts93"}. Type + definitions work in this setting, because the general model-theory of STT + is restricted to models that ensure that the universe of type + interpretations is closed by forming subsets (via predicates taken from + the logic). + + \medskip Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded + constant definitions @{cite "Wenzel:1997:TPHOL" and + "Haftmann-Wenzel:2006:classes"}, which are actually a concept of + Isabelle/Pure and do not depend on particular set-theoretic semantics of + HOL. Over many years, there was no formal checking of semantic type + definitions in Isabelle/HOL versus syntactic constant definitions in + Isabelle/Pure. So the @{command typedef} command was described as + ``axiomatic'' in the sense of \secref{sec:axiomatizations}, only with some + local checks of the given type and its representing set. + + Recent clarification of overloading in the HOL logic proper @{cite + "Kuncar-Popescu:2015"} demonstrate how the dissimilar concepts of constant + definitions versus type definitions may be understood uniformly. This + requires an interpretation of Isabelle/HOL that substantially reforms the + set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic + view on polymorphism and interpreting only ground types in the + set-theoretic sense of HOL88. Moreover, type-constructors may be + explicitly overloaded, e.g.\ by making the subset depend on type-class + parameters (cf.\ \secref{sec:class}). This is semantically like a + dependent type: the meaning relies on the operations provided by different + type-class instances. + \begin{description} - \item @{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = A"} produces an - axiomatization (\secref{sec:axiomatizations}) for a type definition in the - background theory of the current context, depending on a non-emptiness - result of the set @{text A} that needs to be proven here. The set @{text - A} may contain type variables @{text "\\<^sub>1, \, \\<^sub>n"} as specified on the - LHS, but no term variables. - - Even though a local theory specification, the newly introduced type - constructor cannot depend on parameters or assumptions of the - context: this is structurally impossible in HOL. In contrast, the - non-emptiness proof may use local assumptions in unusual situations, - which could result in different interpretations in target contexts: - the meaning of the bijection between the representing set @{text A} - and the new type @{text t} may then change in different application - contexts. + \item @{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = A"} defines a + new type @{text "(\\<^sub>1, \, \\<^sub>n) t"} from the set @{text A} over an existing + type. The set @{text A} may contain type variables @{text "\\<^sub>1, \, \\<^sub>n"} + as specified on the LHS, but no term variables. Non-emptiness of @{text A} + needs to be proven on the spot, in order to turn the internal conditional + characterization into usable theorems. + + The ``@{text "(overloaded)"}'' option allows the @{command + "typedef"} specification to depend on constants that are not (yet) + specified and thus left open as parameters, e.g.\ type-class parameters. + + Within a local theory specification, the newly introduced type constructor + cannot depend on parameters or assumptions of the context: this is + syntactically impossible in HOL. The non-emptiness proof may formally + depend on local assumptions, but this has little practical relevance. For @{command (HOL) "typedef"}~@{text "t = A"} the newly introduced type @{text t} is accompanied by a pair of morphisms to relate it to @@ -1165,11 +1192,11 @@ Abs_t}: An explicit @{keyword (HOL) "morphisms"} specification allows to provide alternative names. - The core axiomatization uses the locale predicate @{const - type_definition} as defined in Isabelle/HOL. Various basic - consequences of that are instantiated accordingly, re-using the - locale facts with names derived from the new type constructor. Thus - the generic @{thm type_definition.Rep} is turned into the specific + The logical characterization of @{command typedef} uses the predicate of + locale @{const type_definition} that is defined in Isabelle/HOL. Various + basic consequences of that are instantiated accordingly, re-using the + locale facts with names derived from the new type constructor. Thus the + generic theorem @{thm type_definition.Rep} is turned into the specific @{text "Rep_t"}, for example. Theorems @{thm type_definition.Rep}, @{thm @@ -1187,40 +1214,14 @@ for the generic @{method cases} and @{method induct} methods, respectively. - \medskip The ``@{text "(overloaded)"}'' option allows the @{command - "typedef"} specification to depend on constants that are not (yet) - specified and thus left open as parameters. In particular, a @{command - typedef} depending on type-class parameters (cf.\ \secref{sec:class}) is - semantically like a dependent type: its meaning is determined for - different type-class instances according to their respective operations. - \end{description} \ subsubsection \Examples\ -text \Type definitions permit the introduction of abstract data - types in a safe way, namely by providing models based on already - existing types. Given some abstract axiomatic description @{text P} - of a type, this involves two steps: - - \begin{enumerate} - - \item Find an appropriate type @{text \} and subset @{text A} which - has the desired properties @{text P}, and make a type definition - based on this representation. - - \item Prove that @{text P} holds for @{text \} by lifting @{text P} - from the representation. - - \end{enumerate} - - You can later forget about the representation and work solely in - terms of the abstract properties @{text P}. - - \medskip The following trivial example pulls a three-element type - into existence within the formal logical environment of HOL.\ +text \The following trivial example pulls a three-element type into +existence within the formal logical environment of Isabelle/HOL.\ (*<*)experiment begin(*>*) typedef three = "{(True, True), (True, False), (False, True)}" diff -r abe08fb15a12 -r 64a5bce1f498 src/Doc/manual.bib --- a/src/Doc/manual.bib Fri Sep 25 20:37:59 2015 +0200 +++ b/src/Doc/manual.bib Fri Sep 25 23:39:08 2015 +0200 @@ -601,6 +601,17 @@ year = 1993, pages = {213-248}} +@article{Farmer:2008, + author = {William M. Farmer}, + title = {The seven virtues of simple type theory}, + journal = {J. Applied Logic}, + volume = {6}, + number = {3}, + pages = {267--286}, + year = {2008}, + url = {http://dx.doi.org/10.1016/j.jal.2007.11.001}, +} + @InProceedings{felty91a, Author = {Amy Felty}, Title = {A Logic Program for Transforming Sequent Proofs to Natural @@ -679,6 +690,14 @@ publisher = CUP, note = {Translated by Yves Lafont and Paul Taylor}} +@TechReport{Gordon:1985:HOL, + author = {M. J. C. Gordon}, + title = {{HOL}: A machine oriented formulation of higher order logic}, + institution = {University of Cambridge Computer Laboratory}, + year = 1985, + number = 68 +} + @Book{mgordon-hol, editor = {M. J. C. Gordon and T. F. Melham}, title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}, @@ -978,6 +997,20 @@ note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}} } +@inproceedings{Kuncar-Popescu:2015, + author = {Ondrej Kuncar and Andrei Popescu}, + title = {A Consistent Foundation for {Isabelle/HOL}}, + editor = {Christian Urban and Xingyuan Zhang}, + booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP} + 2015, Nanjing, China, August 24-27, 2015, Proceedings}, + year = {2015}, + url = {http://dx.doi.org/10.1007/978-3-319-22102-1_16}, + series = {Lecture Notes in Computer Science}, + volume = {9236}, + publisher = {Springer}, + year = {2015}, +} + @Book{kunen80, author = {Kenneth Kunen}, title = {Set Theory: An Introduction to Independence Proofs},