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>
> \<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?
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
"\<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"
"\<And>x. P x ==> Q x"
This archive was generated by a fusion of
Pipermail (Mailman edition) and