[isabelle] Parametricity as a poor man's dependent typing

Dear Isabelle list,

when doing Group Theory in Isabelle, for example in the Free Groups
submission to AFP, I keep proving facts that are “obvious” to the
mathematician and where I would expect a type system to do the work for
me, but I was told that this cannot be done in Isabelle because it does
not support dependent types. This leads to code as in
(unfortunately, the lines have no anchors, but search for “The following
lemmas establish all” and see how I defined mems).

Note how almost all these lemmas would be trivial if we had “X = UNIV”
and “carrier G = UNIV”, or put differently, if these were types of their
own. But they are not, these are sets, although I do _not_ use any
property of their elements and I do _not_ anywhere require elements of
the set’s carrier type that are not in the set.

I was wondering if a parametricity argument as follows is sound, and if
it is, if it can somehow be used in Isabelle to simplify the proofs
(Syntax somewhat liberal, I hope I get the idea across):

        If for a free type variable 'a, “P(UNIV :: 'a)” holds,
        and given “S ≠ Ø”,
        we know “P S” holds.

Assume this ideas was provided as a lemma attribute. Then I could much
more easily prove, for example,

        [[ group G;  f ∈ gens -> carrier G; carrier G = UNIV :: 'a ]]
        	==> G.lift g ∈ hom (free_group X) G

and obtain the result that I want,

        [[ group G ; f ∈ gens -> carrier G ]]
        	==> G.lift g ∈ hom (free_group X) G
by something like
        lift_is_hom = lift_is_hom'[parametricity 'a "carrier G", simp].


PS: I posed a related question in December 2010 and Alexander Krauss
dangled a possible solution:

> This is a notorious problem, and there is no satisfactory solution.
> From 2011 on I'll be working on an infrastructure to deal with this
> (basically recovering what type systems do on the level of reasoning),
> but I am not expecting to have something usable for quite some time.


did anything come out of this already?

Joachim "nomeata" Breitner
  mail at joachim-breitner.de  |  nomeata at debian.org  |  GPG: 0x4743206C
  xmpp: nomeata at joachim-breitner.de | http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part

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