(*<*)
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
(*>*)