Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set


Below Alex is referring to a transfer method that Amine and I developed while I was revising Isabelle's number theory library, designed to help transfer theorems about the natural numbers to equivalent statements about the nonnegative integers and vice-versa.

The idea is simple: whenever you have a bijection from a subset A of one type (possibly the universal set) to a subset B of another, and some functions and relations that respect the bijection, then any theorem about A is equivalent to a theorem about B. (Similarly things can be said about surjections rather than bijections, e.g. quotient maps.) The transfer method simply applies carefully chosen rewrite rules to translate theorems back and forth between such domains.

You can find the code for transfer in Transfer.ML, and the rules designed specifically for transfer between nats and ints in Nat_Transfer.thy of the developer version. They are put to use in files like GCD.thy, Primes.thy, and UniqueFactorization.thy (the latter two are in NumberTheory). It is pretty nifty: you give the method a nat theorem and it returns the corresponding int theorem, or vice-versa. It even works with higher-order constructs like summation, etc.

But the methods are still in a prototype stage. Amine and I still need to find time to polish them and put in rules for other higher-order constructs, and improve the interface and document it. I'm not sure if/ when that will happen...

Unfortunately, this won't solve Peter's problem. The issue is that, in general, one does not have bijections between parameterized structures and types. This is what makes simple type theory simple: types can't depend on parameters. (There is a trick due to John Harrison for encoding natural numbers as types, and using polymorphism over type variables, but it is limited.) Axiomatic type classes are simply stuck in type-land.

If you really want to use structures that depend on parameters, here are some options:

(1) (Re)do everything in locales, as Larry suggests.

(2) Give up on simple type theory and use a dependent type theory like Coq (see e.g. Gonthier's finite group theory project).

(3) Give up on simple type theory and go the other direction, to set theory. See, for example, Mizar's type system for an example of how infrastructure for keeping track of types can be added on top of set theory.

Tobias Nipkow, Brian Huffman, Amine Chaieb, and I once discussed ways that one could embed Isabelle's type theory in a larger set-theoretic framework, e.g. adding a type of sets and axioms that guarantee that "small" types correspond to sets. If done right, that could yield a consistent system (e.g. having the same logical strength as set theory) where one could go back and forth between typed and set- theoretic versions of theorems, and so, indirectly, from axiomatic- type class versions to set-based locale versions. I still think that's an idea worth exploring, if anyone is willing and able.

Best wishes,


On Oct 26, 2009, at 9:19 PM, Alexander Krauss wrote:

Hi Peter,

My concrete problem is, that I have many theorems for the implicit
carrier-set, but the algorithms I want to verify require parametric
carrier sets, e.g.
Any ideas? Is the only way to redo the proofs of all necessary theorems
for explicit carrier sets?

The developer version contains a transfer tool (written by Amine Chaieb) which may be helpful in situations like yours. Currently it is used for lifting theorems between int and nat etc. But there is not really much experience in using it, and it is not part of an official release, so expect the unexpected! (and maybe redoing the proofs is less painful in the end). Probably Amine or someone else can point you to an example of how it can be used...


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