Re: [Axiom-developer] Call for help

[daly]

>This goes back to pop! ; it would seem that push/pop is an abstract
>logical idea and shouldn't be specialized with different versions for
>each domain/catagory.  I might like to temporarily push/pop one of the
>elements of the above, infinite, Euclidean domains during calculations
>for GCD and not have to rewrite push/pop with all the hazards that
>carries.  In addition I would have to rely on some abstract
>delineation to prove that my new code was "correct".  So the abstract
>idea and proof has to be abstract and domain free to be coherent.

You're correct that a full proof should be abstract and domain free. But
while proving the general case might be possible, a proof might only be
available for a specific function in a specific domain.

The generalization suggested last time was to add an "assuming"
clause, of the form,

)abbrev category FOO Foo
Foo: Category == Bar with
    sig1
    sig2
  == add
    sig1 == ...
  assuming
    AssociativeAxiom:
    CommuativeAxiom:
    Proviso1:
    Definition1:

However, within a domain a single function might be easily proven.
It might make sense to extend the syntax of == definitions to admit
a proof clause, e.g.

  fn(a:Integer,b:Integer) == 
        someop(a,b)
     proof:
         ...

Tim