[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Isarmathlib-devel] Submission: Theory of generalization
From: |
Victor Porton |
Subject: |
[Isarmathlib-devel] Submission: Theory of generalization |
Date: |
Fri, 24 Dec 2010 02:20:06 +0300 |
I submit the following code to be included into IsarMathLib:
http://www.mathematics21.org/binaries/gen/isabelle-ZF.zip
It is accompanied with informal article (which I today submitted to a math
journal):
http://www.mathematics21.org/binaries/gen/generalization.pdf
http://www.mathematics21.org/generalization.html
The code is experimental but it is checked that it works (with an example).
In this my submission there are two little violations of IsarMathLib policy:
1. Some lemmas in ZF_Addons.thy are proved using apply-style proofs not ISAR.
That is because these lemmas were proved by Larry Paulson not by myself. I do
not know a good way to transform these proofs into ISAR.
2. Not every lemma is commented. I think this would be superfluous because my
code refers to an informal article where the theory is explained in details.
I ask to forgive me these two violations and include my code into IsarMathLib.
Afterward we may work on redefining the theory of integers using my definitions.
Looking forward for your reply,
--
Victor Porton - http://portonvictor.org
- [Isarmathlib-devel] Submission: Theory of generalization,
Victor Porton <=