[isabelle-dev] [isabelle] (Re-)introducing set as a type constructor rather than as mere abbreviation[SEC=UNCLASSIFIED]
schropp at in.tum.de
Mon Sep 5 20:13:58 CEST 2011
On 08/24/2011 08:30 PM, Florian Haftmann wrote:
>> I don't think it's possible to have it both ways. We need to either say we are making this change (and then pushing it through) or not making this change.
> Having full compatible versions indeed is illusive.
From a naive POV sets and predicates are isomorphic and
results about them could be transferred at any time.
Not that I advocate this on a large scale, but where does
this break down? Tools?
Is this intrinsic or rather an artifact of Isabelle or HOL?
I am asking because I still believe that one day
(somewhat distant, even given my levels of optimism ^^)
theorem proving will be modulo isomorphisms.
I.e. Voevodsky et. al.'s vision should become true not only
in the fancyful calculi they are designing.
More information about the isabelle-dev