[Isarmathlib-devel] Submission: Theory of generalization

[Victor Porton]

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