Email Gateway (Aug 22 2022 at 18:30): Email Gateway (Aug 22 2022 at 18:30):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Jose,
Andrei wrote:
The Top 100 Theorems in Isabelle - Computer Science and ...<http://www.cse.unsw.edu.au/~kleing/top100/<https://emea01.safelinks.protection.outlook.com/?url=http:%2F%2Fwww.cse.unsw.edu.au%2F~kleing%2Ftop100%2F&data=02%7C01%7CA.Popescu%40mdx.ac.uk%7Ce2bca454f78e470b0fbc08d618c74bfb%7C38e37b88a3a148cf9f056537427fed24%7C0%7C0%7C636723641585848072&sdata=owOIs8el33pBvKclkp7V6YCNx48yddRAEKs5ZCdVUbg%3D&reserved=0>>
www.cse.unsw.edu.au<https://emea01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.cse.unsw.edu.au&data=02%7C01%7CA.Popescu%40mdx.ac.uk%7Ce2bca454f78e470b0fbc08d618c74bfb%7C38e37b88a3a148cf9f056537427fed24%7C0%7C0%7C636723641585848072&sdata=pn8IYQXOZBSEjtm%2BQTyLPzfg7TnnuIRk1mQiecEfcrs%3D&reserved=0>
The following are the theorems from this list proved so far in the Isabelle proof assistant. If you have proved additional ones or know of any, please send me email so I can add them here. If the theorem is not part of the Isabelle distribution, the entry will usually contain a link to the ...
I did not write that. You are quoting from a website maintained by Gerwin Klein.
I formalized the classical nontrivial result that harmonic numbers are not integers, except for 1 (I think that this is new in Isabelle). Also, some theorems about Pythagorean triangles and perfect powers. Feel free to take a look if some of these theorems are interesting for the list (the statements of the theorems are at the begging of the thy file) https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory<https://emea01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fjosephcmac%2FFolklore-and-miscellaneous-results-in-number-theory&data=02%7C01%7CA.Popescu%40mdx.ac.uk%7Ce2bca454f78e470b0fbc08d618c74bfb%7C38e37b88a3a148cf9f056537427fed24%7C0%7C0%7C636723641585848072&sdata=aDB7XEpeOrscqfah2S%2B53r5AZFFeW%2BnqsPYjb%2FR%2F3jU%3D&reserved=0>
I am afraid I am not the best person to look at these.
Best wishes,
Andrei
Email Gateway (Aug 22 2022 at 18:30):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
I saw this message below your email. So, I have no idea who wrote the
message. Here I copy the message in context as I received:
Message: 5
Date: Wed, 12 Sep 2018 14:04:21 +0000
From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Subject: Re: [isabelle] Where I could find the Schroeder-Bernstein
Theorem?
To: "cl-isabelle-users@lists.cam.ac.uk"
<cl-isabelle-users@lists.cam.ac.uk>
Message-ID:
<
VI1PR01MB4240E9C82ACCDF4679307D5AB71B0@VI1PR01MB4240.eurprd01.prod.exchangelabs.com
>
Content-Type: text/plain; charset="utf-8"
... and a version for arbitrary sets:
theory Draft
imports "HOL-Library.Cardinal_Notations"
begin
lemma "inj_on f A ⟹ inj_on g B ⟹ f A ⊆ B ⟹ g B ⊆ A ⟹ |A| =o |B|"
by (meson Schroeder_Bernstein card_of_ordIso)
end
Best wishes,
Andrei
From: cl-isabelle-users-bounces@lists.cam.ac.uk <
cl-isabelle-users-bounces@lists.cam.ac.uk> on behalf of Tobias Nipkow <
nipkow@in.tum.de>
Sent: 12 September 2018 14:34:08
To: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Where I could find the Schroeder-Bernstein Theorem?
It is part of Main:
thm Schroeder_Bernstein
There are two proofs. You can find both versions by grepping for Schroeder.
Tobias
On 12/09/2018 13:19, José Manuel Rodriguez Caballero wrote:
Hello,
I was implementing a number-theoretic proof where I used the following
finite version of Schroeder-Bernstein Theorem:definition injfun:: ‹('a ⇒ 'b) ⇒ 'a set ⇒ bool› where
‹injfun ≡ λ f. λ A. (∀ x y::'a. x ∈ A ∧ y ∈ A ∧ f x = f y ⟶ x = y )›definition typefun:: ‹('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ bool› where
‹typefun ≡ λ f. λ A. λ B. (∀ x ::'a. (x ∈ A ⟶ f x ∈ B) )›lemma CantorBernsteinSchroeder:
fixes A :: ‹'a set› and B :: ‹'b set› and f :: ‹'a ⇒ 'b› and g :: ‹'b ⇒
'a›
assumes ‹typefun f A B› and ‹typefun g B A› and ‹injfun f A› and
‹injfun
g B›
and ‹finite A› and ‹finite B›
shows ‹card A = card B›Although I can prove this auxiliary result by myself, this was already
done
in Isabelle/HOL. Indeed in the Top 100 Theorems in Isabelle (
http://www.cse.unsw.edu.au/~kleing/top100/) a more general version of this
The Top 100 Theorems in Isabelle - Computer Science and ...<
http://www.cse.unsw.edu.au/~kleing/top100/>
www.cse.unsw.edu.au
The following are the theorems from this list proved so far in the Isabelle
proof assistant. If you have proved additional ones or know of any, please
send me email so I can add them here. If the theorem is not part of the
Isabelle distribution, the entry will usually contain a link to the ...
result is in position 25:
lemma schroeder_bernstein:
"[| f ∈ inj(X,Y); g ∈ inj(Y,X) |] ==> ∃h. h ∈ bij(X,Y)"So, my question is: Where I could find this theorem in order to obtain the
particular version that I need as a trivial consequence? Thank you in
advance.Kind Regards,
José M.https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory
End of Cl-isabelle-users Digest, Vol 159, Issue 13
El mié., 12 sept. 2018 a las 14:03, Andrei Popescu (<A.Popescu@mdx.ac.uk>)
escribió:
Hi Jose,
Andrei wrote:
The Top 100 Theorems in Isabelle - Computer Science and ...<
http://www.cse.unsw.edu.au/~kleing/top100/
<https://emea01.safelinks.protection.outlook.com/?url=http:%2F%2Fwww.cse.unsw.edu.au%2F~kleing%2Ftop100%2F&data=02%7C01%7CA.Popescu%40mdx.ac.uk%7Ce2bca454f78e470b0fbc08d618c74bfb%7C38e37b88a3a148cf9f056537427fed24%7C0%7C0%7C636723641585848072&sdata=owOIs8el33pBvKclkp7V6YCNx48yddRAEKs5ZCdVUbg%3D&reserved=0>www.cse.unsw.edu.au
<https://emea01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.cse.unsw.edu.au&data=02%7C01%7CA.Popescu%40mdx.ac.uk%7Ce2bca454f78e470b0fbc08d618c74bfb%7C38e37b88a3a148cf9f056537427fed24%7C0%7C0%7C636723641585848072&sdata=pn8IYQXOZBSEjtm%2BQTyLPzfg7TnnuIRk1mQiecEfcrs%3D&reserved=0>
The following are the theorems from this list proved so far in the
Isabelle proof assistant. If you have proved additional ones or know of
any, please send me email so I can add them here. If the theorem is not
part of the Isabelle distribution, the entry will usually contain a link to
the ...I did not write that. You are quoting from a website maintained by Gerwin
Klein.I formalized the classical nontrivial result that harmonic numbers are
not integers, except for 1 (I think that this is new in Isabelle). Also,
some theorems about Pythagorean triangles and perfect powers. Feel free to
take a look if some of these theorems are interesting for the list (the
statements of the theorems are at the begging of the thy file)
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory
<https://emea01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fjosephcmac%2FFolklore-and-miscellaneous-results-in-number-theory&data=02%7C01%7CA.Popescu%40mdx.ac.uk%7Ce2bca454f78e470b0fbc08d618c74bfb%7C38e37b88a3a148cf9f056537427fed24%7C0%7C0%7C636723641585848072&sdata=aDB7XEpeOrscqfah2S%2B53r5AZFFeW%2BnqsPYjb%2FR%2F3jU%3D&reserved=0>I am afraid I am not the best person to look at these.
Best wishes,
Andrei
Last updated: Apr 24 2024 at 04:17 UTC