Re: [isabelle] Simple subgoal involving sets & lists



Le Dimanche 25 Septembre 2011 20:19:25 Matthew a écrit :
> 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.
> ...
> Anyone know what's
> going on?  Is this indeed unprovable because of a mistake I've made?

Hi Matthew,

The problem lies in the confusion between the operators of Isabelle/Pure and 
Isabelle/HOL, and in this case between:
 * "\<And>" and "\<forall>"
 * "\<Longrightarrow>" and "\<longrightarrow>"

As Isabelle/HOL operators have higher priority than Isabelle/Pure ones, here 
you have:
  "\<forall>x. P x \<Longrightarrow> Q x"
which is read as:
  "(\<forall>x. P x) \<Longrightarrow> Q x"

and where the "x" on the right is implicitly universally bound over the 
complete formula (you can see it is blue while the x on the left is green).

Then the assumption of this implication in your case is not generally true 
("thelist" would have to contain all the elements but "a").

The formulae you seemed to expect would be:
  "\<forall>x. P x \<longrightarrow> Q x"
or
  "\<And>x. P x ==> Q x"

Regards,

Mathieu




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