*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 18 Dec 2013 16:21:16 -0600*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1312161721220.4442@lxbroy10.informatik.tu-muenchen.de>*References*: <52AB3E42.50501@gmx.com> <alpine.LNX.2.00.1312161721220.4442@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 12/16/2013 10:25 AM, Makarius wrote:

The particular problem above is "blast" failing repeatedly in a rathernoise way....

declare[[show_sorts=true]] lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False" apply(auto) oops

...You can try something like this: theorem "(!!P. P::bool) ==> PROP P" by blast e.g. with "isabelle tty" on the Terminal.

Regards, GB (****************************************************************************************) theory i131214a__isaU_Trueprop_False_meta_eq_auto_hangs_PIDE imports Complex_Main begin declare[[show_sorts=true]] declare[[show_brackets=true]] declare[[show_question_marks=true]] notation Trueprop ("_∷⇩T" [1000] 1000)

to run very long.*) lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))" apply(rule equal_intr_rule) (*apply(auto)*) oops

than about 5 seconds when I have "show_sorts=true".*) lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False" (*apply(auto)*) oops (*No problem with blast to prove ==, instead of auto.*) lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))" apply(rule equal_intr_rule) apply(blast) apply(blast) (*Failure messages here.*) done (*This direction with blast is okay, though there are failure messages.*) lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False" apply(blast) (*Failure messages here.*) done (*The other direction with auto is okay.*) lemma "False ==> (!!f. !!a. f = (%a. a | f a) ==> (f a = a))" apply(auto) done end

theory i131214a__isaU_Trueprop_False_meta_eq_auto_hangs_PIDE imports Complex_Main begin declare[[show_sorts=true]] declare[[show_brackets=true]] declare[[show_question_marks=true]] notation Trueprop ("_\<Colon>\<^sub>T" [1000] 1000) (*With "Auto Methods" off, auto goes off and doesn't come back, if it's allowed to run very long.*) lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))" apply(rule equal_intr_rule) (*apply(auto)*) oops (*This direction with auto is the problem. I need to terminate it within less than about 5 seconds when I have "show_sorts=true".*) lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False" (*apply(auto)*) oops (*No problem with blast to prove ==, instead of auto.*) lemma "Trueprop False == (!!f. !!a. f = (%a. a | f a) ==> (f a = a))" apply(rule equal_intr_rule) apply(blast) apply(blast) (*Failure messages here.*) done (*This direction with blast is okay, though there are failure messages.*) lemma "(!!f. !!a. f = (%a. a | f a) ==> (f a = a)) ==> False" apply(blast) (*Failure messages here.*) done (*The other direction with auto is okay.*) lemma "False ==> (!!f. !!a. f = (%a. a | f a) ==> (f a = a))" apply(auto) done end

**References**:**[isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE***From:*Gottfried Barrow

**Re: [isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE***From:*Makarius

- Previous by Date: [isabelle] isabelle build: number of threads
- Next by Date: Re: [isabelle] Infinitely recursive lambda expression or not?
- Previous by Thread: Re: [isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE
- Next by Thread: [isabelle] Infinitely recursive lambda expression or not?
- Cl-isabelle-users December 2013 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