*To*: Matthew <superuser at mattweidner.com>*Subject*: Re: [isabelle] Lists, foldl, and group theory*From*: Johannes Hoelzl <hoelzl at in.tum.de>*Date*: Mon, 19 Sep 2011 17:00:03 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1316392993.4126.0.camel@matthew-desktop>*References*: <1316392993.4126.0.camel@matthew-desktop>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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"

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

Sledgehammer may in the current release of Isabelle find some false

- Johannes On Sun, 18 Sep 2011, Matthew wrote:

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

**References**:**[isabelle] Lists, foldl, and group theory***From:*Matthew

- Previous by Date: [isabelle] Lists, foldl, and group theory
- Next by Date: [isabelle] A simple theorem
- Previous by Thread: [isabelle] Lists, foldl, and group theory
- Next by Thread: [isabelle] A simple theorem
- Cl-isabelle-users September 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list