*To*: Makarius <makarius at sketis.net>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Isabelle Foundation & Certification*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Sun, 27 Sep 2015 11:03:36 +0100*Accept-language*: en-US, en-GB*Acceptlanguage*: en-US, en-GB*Thread-index*: AdD5CI06W/3pRK9GSwKmNtwAvJwctA==*Thread-topic*: [isabelle] Isabelle Foundation & Certification

Hi Makarius, Many thanks for this great news! Declaring the Isabelle/HOL typedef to be definitional is well-justified and surely welcomed by the users. This definitional status, achieved on a tricky foundational terrain in the presence of constant overloading, benefits from the previous work on taming overloading by yourself, Steven Obua and Florian Haftmann (among others). I am looking forward to the relaxed discussion in front of us. :-) All the best, Andrei -----Original Message----- From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Makarius Sent: 26 September 2015 16:27 To: cl-isabelle-users at lists.cam.ac.uk Subject: Re: [isabelle] Isabelle Foundation & Certification (Back to this still open thread.) Last Monday I started to look at the actual sources and the patch that was mentioned in the paper, and learned a few more things that I will explain later, when writing up a full overview of my present understanding of it. Since reading ML sources and changesets is always a constructive process for me, I've produced various changesets over several days (being off-list), leading up to 64a5bce1f498 with the following NEWS entry: * 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. As well as the following updated section in the isar-ref manual (formerly "Typedef axiomatization"): section âSemantic subtype definitions \label{sec:hol-typedef}â text â \begin{matharray}{rcl} @{command_def (HOL) "typedef"} & : & @{text "local_theory â proof(prove)"} \\ \end{matharray} 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 "Îâ1, â, Îân"} which means that the type definition produces a type constructor @{text "(Îâ1, â, Îân) t"} depending on those type arguments. @{rail â @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set ; @{syntax_def "overloaded"}: ('(' @'overloaded' ')') ; abs_type: @{syntax typespec_sorts} @{syntax mixfix}? ; 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"}~ at {text "(Îâ1, â, Îân) t = A"} defines a new type @{text "(Îâ1, â, Îân) t"} from the set @{text A} over an existing type. The set @{text A} may contain type variables @{text "Îâ1, â,Îâ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 `` at {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"}~ at {text "t = A"} the newly introduced type @{text t} is accompanied by a pair of morphisms to relate it to the representing set over the old type. By default, the injection from type to set is called @{text Rep_t} and its inverse @{text Abs_t}: An explicit @{keyword (HOL) "morphisms"} specification allows to provide alternative names. 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 type_definition.Rep_inverse}, and @{thm type_definition.Abs_inverse} provide the most basic characterization as a corresponding injection/surjection pair (in both directions). The derived rules @{thm type_definition.Rep_inject} and @{thm type_definition.Abs_inject} provide a more convenient version of injectivity, suitable for automated proof tools (e.g.\ in declarations involving @{attribute simp} or @{attribute iff}). Furthermore, the rules @{thm type_definition.Rep_cases}~/ @{thm type_definition.Rep_induct}, and @{thm type_definition.Abs_cases}~/ @{thm type_definition.Abs_induct} provide alternative views on surjectivity. These rules are already declared as set or type rules for the generic @{method cases} and @{method induct} methods, respectively. \end{description} This may still require more polishing before the winter release of Isabelle2016, but there is time for that. My impression is that part of the discussion so far was encumbered by anxiety that this add-on feature won't make it into the next release. Now that there is no more pressure in this respect, we can sort out remaining low-level and high-level problems in a relaxed manner. In the next round I will comment more on the ITP paper and the notes on the original patch ... Makarius

**Follow-Ups**:**Re: [isabelle] Isabelle Foundation & Certification***From:*Makarius

- Previous by Date: Re: [isabelle] Isabelle Foundation & Certification
- Next by Date: [isabelle] tactic in Eisbach method
- Previous by Thread: Re: [isabelle] Isabelle Foundation & Certification
- Next by Thread: Re: [isabelle] Isabelle Foundation & Certification
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list