Email Gateway (Aug 18 2022 at 18:25): Email Gateway (Aug 18 2022 at 18:25):From: Matthew <superuser@mattweidner.com>
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
Email Gateway (Aug 18 2022 at 18:25):From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Le Dimanche 25 Septembre 2011 20:19:25 Matthew a écrit :
Hi Matthew,
The problem lies in the confusion between the operators of Isabelle/Pure and
Isabelle/HOL, and in this case between:
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
Last updated: Apr 26 2024 at 16:20 UTC