Re: [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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.