[isabelle-dev] Quotient.invariant

[Ondřej Kunčar]

On 03/23/2012 05:34 PM, Makarius wrote:
> Just a note on the following changeset:
>
> changeset: 47095:3ea48c19673e
> user: kuncar
> date: Fri Mar 23 14:25:31 2012 +0100
> files: src/HOL/Quotient.thy src/HOL/Tools/Quotient/quotient_def.ML
> src/HOL/Tools/Quotient/quotient_term.ML
> src/HOL/Tools/Quotient/quotient_type.ML
> description:
> generation of a code certificate from a respectfulness theorem for
> constants lifted by the quotient_definition command & setup_lifting
> command: setups Quotient infrastructure from a typedef theorem
>
>
> It introduces a constant called "invariant" in main HOL. It might be a
> candidate for "hide_const (open)". Some experts on the Isabelle/HOL
> library can probably say more.

At this point it's not clear if this constant will be used only for 
internal purposes. The original idea was to allow users to write 
definitions like this one:

quotient_type 'a foo = 'a bar / invariant P

If it turns out that we need this constant only internally, it will be 
hidden.

Ondrej