[isabelle-dev] Quotient.invariant

[Gerwin Klein]

If it turns out that the constant is not internal-only, it should get a more specific name. "invariant" really is a name that should be available to users without shadowing. 

Cheers,
Gerwin

On 24/03/2012, at 4:06, Ondřej Kunčar <kuncar at in.tum.de> wrote:

> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>