*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Associativity of conj not picked up by blast*From*: "K. Nienhuis" <kn307 at cam.ac.uk>*Date*: Fri, 06 Mar 2015 10:11:56 +0000*User-agent*: Roundcube Webmail/1.0.2

Hi,

Thanks, Kyndylan

**Attachment:
BracketsAndBlast.pdf**

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

**Follow-Ups**:**Re: [isabelle] Associativity of conj not picked up by blast***From:*Larry Paulson

**Re: [isabelle] Associativity of conj not picked up by blast***From:*Makarius

- Previous by Date: Re: [isabelle] Tracing intro and elim in auto
- Next by Date: Re: [isabelle] Tracing intro and elim in auto
- Previous by Thread: Re: [isabelle] Tracing intro and elim in auto
- Next by Thread: Re: [isabelle] Associativity of conj not picked up by blast
- Cl-isabelle-users March 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list