[isabelle-dev] classes

[Alexander Krauss]

Hi Amine,

> class acf = field + assumes
>    algebraically_closed: "~ constant (poly p) ==> EX x. poly p x = 0"
> 
> instance complex :: acf
> using fundamental_theorem_of_algebra by (intro_classes, blast)

Hehe... Sometimes theorem proving can look really simple :-)

> This would have not been possible without merging some classes.

Which?

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...?

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

> There is a quantifier elimination procedure implemented for complex 
> numbers, which relies on fact easily portable to acf.

Cool.

> There is great future in merging classes, so why not roar ahead?

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.

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

After Isabelle2007 (which is soon, I think :-) ), we can "embrace 
change" again, and have this feature, and others.

Alex