# 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
;
;
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.

"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.