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