[isabelle-dev] classes

[Amine Chaieb]

>> This would have not been possible without merging some classes.
> 
> Which?
> 
Just these:

class recpower_semiring = semiring + recpower
class recpower_semiring_1 = semiring_1 + recpower
class recpower_semiring_0 = semiring_0 + recpower
class recpower_ring = ring + recpower
class recpower_ring_1 = ring_1 + recpower
subclass (in recpower_ring_1) recpower_ring by unfold_locales
subclass (in recpower_ring_1) recpower_ring by unfold_locales
class recpower_comm_semiring_1 = recpower + comm_semiring_1
class recpower_comm_ring_1 = recpower + comm_ring_1
subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 by 
unfold_locales
class recpower_idom = recpower + idom
subclass (in recpower_idom) recpower_comm_ring_1 by unfold_locales
class idom0 = idom + ring_char_0
class recpower_idom0 = recpower + idom0
subclass (in recpower_idom0) recpower_idom by unfold_locales
subclass (in idom0) comm_ring_1 by unfold_locales


> And what exactly does "merging" mean? Do you just add a new class which 
> "inherits" from both existing classes? Then it would be a conservative 
> extension...?

Yes, see above.

> 
> When you changed things locally, what effects did it have on other theories?
> 

I just added these at the beginning of my theory, so I have no idea what 
would happen if they were in HOL. I also did not try to do more than 
needed, just what I needed to make Polynomials local.

> I think I like this future, but I still agree with Makarius: Unless 
> there is something severely broken in the current state of affairs, we 
> should really be disciplined and wait for the release first.
> 

The release Idea (as far as I understood Makarius) is that the system 
should "freeze" for a couple of weeks while we are *using* it and report 
our experience. That's all I did, just report (while bemoaning, I must 
admit). I leave it to others to decide if this is important to change 
now of not. I myself think it quite manageable to fix in a reasonable 
time but I also fully understand that this release-preparation time is 
critical.

Regardless of release, there are several subtle issues with classes 
which need to be fixed.

> And in fact your proposal is more of the visionary kind than of the 
> "fixes a pressing problem" kind, isn't it?

It is not really a pressing problem. The other problem (parsing/type 
inference) I reported locally on the TUM list, is in my opinion pressing 
-- Thanks for Makarius who fixed it.

Amine.