[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
schropp at in.tum.de
Fri Aug 26 20:55:30 CEST 2011
On 08/26/2011 07:08 PM, Brian Huffman wrote:
> 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".
The global axiom is
EX x. x : A ==> type_definition Rep Abs A
allowing local typedefs whenever non-emptiness of A is
derivable, even using assumptions in the context.
This is not really a problem, but complicates my conservativity
argument. Before local typedefs the proof of (EX x. x : A) was
global. Actually Makarius' attitude on this was that those non-emptiness
proofs "should be global most of the time", but he didn't want to
introduce a check.
More information about the isabelle-dev