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,
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
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
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.
On Oct 26, 2009, at 9:19 PM, Alexander Krauss wrote:
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
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