[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
brianh at cs.pdx.edu
Fri Aug 26 19:08:46 CEST 2011
On Fri, Aug 26, 2011 at 9:36 AM, Andreas Schropp <schropp at in.tum.de> wrote:
> On 08/26/2011 06:50 PM, Tobias Nipkow wrote:
>> I agree. Since predicates are primitive, starting from them is
> Did I get this right:
> the idea is to implement our advanced typedef via a HOL4-style predicate
> That doesn't work because HOL4-style typedefs don't feature our extensions
> to typedef and they are only conservative via a global theory
What exactly are our extensions to typedef?
As far as I understand, the typedef package merely issues global
axioms of the form "type_definition Rep Abs S", as long as it is
provided with a proof of "EX x. x : S".
My understanding of the localized typedef is that it works by
declaring a global typedef behind the scenes (much like a local
definition of a polymorphic constant works by declaring a global
polymorphic definition behind the scenes).
What am I missing here?
More information about the isabelle-dev