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

You need to quantify over all x, the meta-quantifier is "!!":

 (!!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

On Sun, 18 Sep 2011, Matthew wrote:


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
2. \<And>a list. \<lbrakk>x \<in> set (a # list) \<longrightarrow> x
\<in> G; foldl op ** 1 list \<in> G\<rbrakk> \<Longrightarrow> a \<in>
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?


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