# [isabelle] Associativity of conj not picked up by blast

```Hi,

```
In the attached example, blast fails when given an elim of the form "P /\ Q /\ R" but succeeds when given the same rule with parenthesis "(P /\ Q) /\ R". What is the explanation for that behaviour?
```
Thanks,
Kyndylan```

Attachment: BracketsAndBlast.pdf
Description: Adobe PDF document

```(*<*)
theory BracketsAndBlast

imports
Main
begin

(*>*)

text {* Some dummy definitions. *}

definition foo :: "bool" where
"foo = True"

definition bar :: "bool" where
"bar = foo"

definition baz :: "bool" where
"baz = bar"

text {* A conventional elim rule for bar. *}

lemma barE:
assumes "bar"
obtains "foo"
using assms
unfolding bar_def
by auto

text {* Version 1 of an elim rule for baz. *}

lemma bazE1:
assumes "baz"
obtains "bar \<and> True \<and> (\<forall>x. True)"
using assms
unfolding baz_def
by auto

text {* Blast is not able to use that version. *}

lemma
assumes "baz"
shows   "foo"
using assms
-- "apply (blast elim: bazE1 barE) fails"
oops

text {* Version 2. Note that the brackets are the only difference with version 1. *}

lemma bazE2:
assumes "baz"
obtains "(bar \<and> True) \<and> (\<forall>x. True)"
using assms
unfolding baz_def
by auto

text {* Now blast is able to prove the lemma. *}

lemma
assumes "baz"
shows   "foo"
using assms
by (blast elim: bazE2 barE)

text {* If the quantifier is removed, then the version without the brackets can be used by blast to
prove the lemma. *}

lemma bazE3:
assumes "baz"
obtains "bar \<and> True \<and> True"
using assms
unfolding baz_def
by auto

lemma
assumes "baz"
shows   "foo"
using assms
by (blast elim: bazE3 barE)

text {* Also, if there is only one layer of definitions (baz - bar), instead of two (baz - bar -
foo), then the version without the brackets works as well. *}

lemma bazE4:
assumes "baz"
obtains "bar \<and> True \<and> (\<forall>x. True)"
using assms
unfolding baz_def
by auto

lemma
assumes "baz"
shows   "bar"
using assms
by (blast elim: bazE4)

text {* Why is the combination of no brackets, the quantifier, and the extra layer of definitions
preventing blast from finding a proof? *}

(*<*)
end
(*>*)
```

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