Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Lists, foldl, and group theory

Email Gateway (Aug 18 2022 at 18:23):

From: Matthew <superuser@mattweidner.com>
Hello,

To get myself used to Isabelle/Isar, I am attempting to formalize some
basic results of group theory (I realize this has already been done in
theory Group-Ring-Module). I have already formalized the axioms and
basic results (e.g., ab = 1 ==> a = b^-1).
However, I have been having great difficulty with the theorem which can
be represented informally as:
a1 : G; a2 : G; ... an : G ==> a1 a2 ... ** an : G
where the a's with subscripts are members of G, G is the group's set, **
is the group operation, and : indicates set membership.
My approach so far has been to use a list of elements, where membership
in the list implies membership in G, and then to show that foldl( ** 1
thelist ) is in G (1 is the identity element), i.e.,
"\<lbrakk>x \<in> set( thelist::'a list ) \<longrightarrow> x \<in> G
\<rbrakk> \<longrightarrow> (foldl (prod) 1 thelist ) \<in> G"

Is this the correct approach?

Using induction, I have reduced the problem to several subgoals which
look provable:
" 1. \<And>a list.
\<lbrakk>x \<in> set (a # list) \<longrightarrow> x \<in> G;
foldl op ** 1 list \<in> G; a \<in> G\<rbrakk>
\<Longrightarrow> foldl op (1 a) list = a foldl op 1
list

2. \<And>a list. \<lbrakk>x \<in> set (a # list) \<longrightarrow> x
   \<in> G; foldl op ** 1 list \<in> G\<rbrakk> \<Longrightarrow> a \<in>
   G"
   where "a" and "list" are variables generated by the application of
   (induct_tac thelist).
   However, these subgoals have been extremely difficult to prove. The
   most frustrating thing is that sledgehammer will claim to find proofs,
   but metis is unable to reconstruct them.

Is my whole approach wrong, or am I missing some essential theorems?

Thanks,
Matthew

Email Gateway (Aug 18 2022 at 18:23):

From: Johannes Hoelzl <hoelzl@in.tum.de>
You need to quantify over all x, the meta-quantifier is "!!":

"\<lbrakk>
(!!x. x \<in> set( thelist::'a list ) \<longrightarrow> x \<in> G)
\<rbrakk> \<longrightarrow> (foldl (prod) 1 thelist ) \<in> G"

without quantifier you assume there is one x which if it is in thelist
then also in G. With the quantifer you assume that all elements in the
list are in G.

With this the lemma should be solveable
by (induct thelist) (auto simp add: ...)

Btw: Don't use induct_tac, use the induct method. Generally try to avoid
the _tac methods when working in Isabelle/Isar.

Sledgehammer may in the current release of Isabelle find some false
"proofs", which are then not proveable by metis. In the next version
Sledgehammer shouldn't return that it found a proof.

- Johannes

Last updated: Apr 19 2024 at 12:27 UTC