>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
_______________________________________________
Axiom-developer mailing list
[email protected]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
