[isabelle] Simple subgoal involving sets & lists



I have a theorem which I have reduced to the following subgoal (ignore
the first assumption, it's left over from another part of the proof) :

\<And>a thelist.
       \<lbrakk>(\<forall>x. x \<in> set thelist \<Longrightarrow> x
\<in> G) \<Longrightarrow> prod_group thelist \<in> G;
        \<forall>x. x \<in> set (a # thelist) \<Longrightarrow> x \<in>
G\<rbrakk>
       \<Longrightarrow> a \<in> G

This looks quite provable to me.
If I apply( simp ), it reduces to:

\<And>a thelist.
       \<lbrakk>(\<forall>x. x \<in> set thelist \<Longrightarrow> x
\<in> G) \<Longrightarrow> prod_group thelist \<in> G;
        \<forall>x. x \<in> set (a # thelist) \<Longrightarrow> x \<in>
G\<rbrakk>
       \<Longrightarrow> a \<in> G

which looks even more provable.  However, I'm stuck.  Anyone know what's
going on?  Is this indeed unprovable because of a mistake I've made?

Thanks,
Matthew






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