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.