Re: [isabelle] RC5: Syntactic class bit_operations is gone



Hi Peter,

> A theory that defines a bundle for its syntax, starting with
> no_notation ... to erase potential conflicting syntax, automatically
> depends on the theory declaring the conflicting syntax, even if they
> are logically independent. Otherwise, the user will be responsible to
> do such a declaration at the merge point of two theories declaring
> conflicting syntax.

I don't see that point.  The syntax woule be totally organized in
bundles and hence there are no conflicts at theory merges.

>> So, the bundle seems the way to go for now.  Since there is some
>> rationale to put the most important bit operations into HOL-Main, I
>> once
>> thought to organize all infix syntax on bits in bundles anyway, to
>> not
>> clutter the syntactic space of HOL-Main.  If this is once
>> accomplished
>> after the release, the infix syntax is completely free.
> 
> Also, the bundling approach prevents you from using the same syntax for
> the two related concepts, e.g., I can no longer write the statement: 
> 
> width a = width b ==> int_of (a AND b) = int_of a AND int_of b
> for a b :: ll_word
> 
> In my solution, I now went for introducing a similar looking syntax,
> i.e., a llAND b. But this approach will lead to cluttering the syntax
> space with many variations of the same syntax, just b/c you cannot
> share it where it would feel natural to share.
> 
> It seems like there is no fits-everything solution to this question
> yet.

Ok, now I understand that these operations are inherently partial and
hence there are no unguarded properties.

In the current state of affairs most lemmas

	"… AND … OR … XOR … = …"

are valid *without* any type annotation due to the algebraic foundation
of the underlying type class.  This should eliminate the felt need for
yet another infix syntax for word types only as seen in
Word_Lib/Word_Syntax.thy (which, by the way, is not found in typical
programming languages).  Hence I want to maintain that.

A compromise could be to have a syntactic class but by default a
stronger constraint.  I will investigate that in the future.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.