[isabelle] Lists, foldl, and group theory



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 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.