Email Gateway (Aug 18 2022 at 15:14): Email Gateway (Aug 18 2022 at 15:14):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
I’m quite new to Isabelle and trying to get an overview of the
mathematics already formalized. I found some basic group theory in the
HOL/Algebra directory, but it seems to be relatively basic. It contains
abstract definitions, but I’m missing some more concrete groups,
especially the Free Group over a finite set of generators, matrix groups
such as GL_r(ℤ) and permutation groups.
Am I not looking in the right places? And if such theories really do not
exist, is there some principal problem in implementing them, or is it
something that just has not been done yet, but should not be
particularly hard?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 15:15):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Joachim,
Indeed, the Isabelle libraries contain a lot of more concrete
mathematical constructions, but they are spread over several different
places, and generally nobody has connected them up with HOL/Algebra to
show that they are instances of the more abstract notions.
Often these kind of constructions are formalized as type constructors.
For example, HOL/Matrix defines a type "'a matrix" of matrices with
elements of type 'a (it includes matrices of any finite size). You
could define GL_r(Z) as a subset of this type like this:
definition GL :: "nat => int matrix set"
where "GL n = {A::int matrix. nrows A = n & ncols A = n & (EX B.
inverse_matrix A B)}"
Then it would be straightforward to show that this set, together with
"op *" on type "int matrix", forms a group according to the
definitions defined in HOL/Algebra.
Some other constructions implemented as type constructors:
Library/Polynomial.thy defines the ring of univariate polynomials with
coefficients from type 'a as the type "'a poly". On the AFP
(afp.sourceforge.net) you will find a formalization of the Free
Boolean Algebra with generators from type 'a as the type "'a formula".
There is also a function "formulas :: 'a set => 'a formula set" which
can be used to reason about sub-algebras.
Also, the Isabelle library contains a very nice formalization of the
Free Monoid with generators from type 'a -- it can be found in
List.thy :) It also contains a function "lists :: 'a set => 'a list
set" that gives the lists generated by some subset of generators.
Similarly, a construction of the Free Commutative Monoid can be found
in Library/Multiset.thy, as type "'a multiset".
As far as I know, nobody has formalized Free Groups. I wouldn't expect
it to be difficult, but probably nobody has really needed them for
anything yet. You could define a type constructor for the free group
with generators over type 'a as a subset of type "(bool * 'a) list",
where you would have a function "normalize :: (bool * 'a) list =>
(bool * 'a) list" that removes adjacent copies of the same element
with opposite signs.
typedef 'a free_group = "{x :: (bool * 'a) list. normalize x = x}"
Then you could define a function analogous to "lists" with type "'a
set => 'a free_group set" that would pick out the values generated by
some smaller set. This would probably make a nice AFP entry, if you
wanted to formalize it.
As for permutations: There is a library Permutations.thy that
formalizes the set of permutations over a given set. (Currently it is
located in HOL/Multivariate_Analysis, since it is used by other
theories there; but in the next release of Isabelle it will be located
in HOL/Library.)
There are probably other examples that I can't think of right now.
Have fun exploring the Isabelle libraries!
Email Gateway (Aug 18 2022 at 15:15):From: Joachim Breitner <mail@joachim-breitner.de>
Hi Brian,
thanks for your reply.
I’m tempted to do so, once I’m more familiar with Isar syntax. After
doing more research, I also found http://isarmathlib.org/
This poses a new question: What foundation should I use? As a
mathematician, I’d first say that set theory is the correct base to
formalize pure math on – but does it really matter? Will I have problems
convincing other mathematician to trust a formalized proof on Higher
Logic?
Are the provable theorems within, say, pure algebra the same in either
systems, just with different proofs? If so, is this fact proven? Or is
it indeed necessary to prove results in either system?
Does the AFP also accept Isabelle/ZF submissions?
As a side note: One of my hopes when getting interested in theorem
provers and proof checkers was that I’d get a tool that can also
investigate proof. For example, tell me whether a certain proof uses the
axiom of choice or not. It seems that the Metamath system allows for
that, but is otherwise very laborious to use. To pick up the recent
discussion about proof certificates and stability: Has there been done
work or thought in the direction of exporting Isabelle proof objects
into Metamath proofs? It seems to me that this would provide for
inspectable and stable proofs, while exploiting the power of Isabelle
and ease of Isar.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 15:15):From: Brian Huffman <brianh@cs.pdx.edu>
On Mon, May 10, 2010 at 2:34 AM, Joachim Breitner
<mail@joachim-breitner.de> wrote:
This poses a new question: What foundation should I use? As a
mathematician, I’d first say that set theory is the correct base to
formalize pure math on – but does it really matter? Will I have problems
convincing other mathematician to trust a formalized proof on Higher
Logic?Are the provable theorems within, say, pure algebra the same in either
systems, just with different proofs? If so, is this fact proven? Or is
it indeed necessary to prove results in either system?
There should be no problem for mathematicians to trust Higher Order
Logic, since there is a straightforward model of HOL in set theory. In
fact, Alexander Krauss and Andreas Schropp have an upcoming paper
where they describe an automatic translation from Isabelle/HOL to
Isabelle/ZF:
http://www4.in.tum.de/~krauss/holzf/
On the other hand, there is no model of ZF in HOL (unless you add a
bunch of new axioms to HOL) so there is no translation the other way.
In particular, many constructions in set theory using the axiom of
replacement are impossible to represent in HOL (the cardinalities just
get too big).
In practice, using HOL is usually nicer than using ZF, since the
automation is better (automatic type checking/type inference, for
example). And in Isabelle, the libraries and tools are much more well
developed in Isabelle/HOL compared to Isabelle/ZF.
Does the AFP also accept Isabelle/ZF submissions?
There aren't any Isabelle/ZF submissions yet, but I'm sure they would
be welcome.
Email Gateway (Aug 18 2022 at 15:15):From: Tobias Nipkow <nipkow@in.tum.de>
Does the AFP also accept Isabelle/ZF submissions?
Yes, it does.
Tobias
Email Gateway (Aug 18 2022 at 15:16):From: Timothy McKenzie <tjm1983@gmail.com>
I have a related question. Looking at src/HOL/Algebra/Group.thy,
I see that (for example) the definition of the monoid locale has
"fixes G (structure)". Looking in the documentation,
"(structure)" is mentioned only twice in doc/isar-ref.pdf (as far
as I can see), and I haven't found it in the other documentation I
looked in. What does it mean? How would I go about instantiating
such a locale?
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 15:18):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Timothy,
(structure) is an (outdated) syntax feature. As far as I understand it
has no relevance for locale interpretation.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:18):From: Timothy McKenzie <tjm1983@gmail.com>
Hi,
Thanks for your reply. It took me a while to figure out that I
needed to use \<^bsub>...\<^esub> in a group interpretation. For
example, an interpretation of the integers under addition as a
group might begin:
interpretation group "(|carrier = UNIV, mult = op +, one =
0::int|)"
proof
let ?Z = "(|carrier = UNIV, mult = op +, one = 0::int|)"
fix x y
show "x ⊗\<^bsub>?Z\<^esub> y ∈ carrier ?Z" by simp
Timothy
<><
signature.asc
Last updated: Apr 26 2024 at 20:16 UTC