[isabelle] About Generalization theory

In a previous message I sent a draft of Generalization.thy theory.

With that theory we can significantly change the way Isabelle/ZF works.

For example:

We can define new versions of Nat_ZF.thy and Int_ZF.thy (maybe we should
name these Nat_ZF_2.thy and Int_ZF_2.thy) with "+" used to sum two
numbers (not "$*" or "#*").

Using my Generalization theory we identify nat with a subset of int and
can prove that either "+" yields the same value whether its arguments
are considered nat or int.

Then a user could import only one of either Nat_ZF_2 or Int_ZF_2 and get
"+" which does what it could be expected (in the same way as we deal in
informal mathematics).

I hope somebody will help me to finish development of Generalization.thy
theory. For this purpose I am going to put my draft of
Generalization.thy at vdash.org when vdash.org will be up. But we can
work on this not waiting for vdash.org.

Victor Porton - http://www.mathematics21.org

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