Email Gateway (Aug 18 2022 at 13:13): Email Gateway (Aug 18 2022 at 13:13):From: Victor Porton <porton@narod.ru>
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.
Last updated: Nov 21 2024 at 12:39 UTC