*To*: David Greenaway <david.greenaway at nicta.com.au>*Subject*: Re: [isabelle] simp_trace_new*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Mon, 08 Dec 2014 15:21:15 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5480E0B1.3030002@nicta.com.au>*References*: <5480888F.3030507@ist.tugraz.at> <5480E0B1.3030002@nicta.com.au>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

Hi David, thanks a lot for your reply to my questions in isabelle-users@ ...

lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)" using [[simp_trace_new mode=full]] using [[simp_break "_ ⟶ _"]] by autoWith focus on "auto" <Output> indeed showslemma (∃x. ∀y. ?P x y) ⟶ (∀y. ∃x. ?P x y) See <simplifier trace>but klicking "<simplifier trace>" opens two empty windows. Now I don't know whether * "auto" doesn't need the simplifier in the above proof * there is something I am doing wrong * "simp_trace_new mode=full" does not yet apply to Isabelle2014.If the simplifier trace doesn't help you, you might want to look at Daniel Matichuk's "apply_trace" command, which I have described at: http://stackoverflow.com/a/26827242/570879

... this looks great ...

(* attempt 5 to watch *) lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)" apply_trace auto done (*used theorems: allE: ∀x. ?P x ⟹ (?P ?x ⟹ ?R) ⟹ ?R allI: (⋀x. ?P x) ⟹ ∀x. ?P x ccontr: (¬ ?P ⟹ False) ⟹ ?P exE: ∃x. ?P x ⟹ (⋀x. ?P x ⟹ ?Q) ⟹ ?Q exI: ?P ?x ⟹ ∃x. ?P x impI: (?P ⟹ ?Q) ⟹ ?P ⟶ ?Q swap: ¬ ?P ⟹ (¬ ?R ⟹ ?P) ⟹ ?R *)

Walther

**Follow-Ups**:**Re: [isabelle] simp_trace_new***From:*Lawrence Paulson

**Re: [isabelle] simp_trace_new***From:*Makarius

**References**:**[isabelle] simp_trace_new***From:*Walther Neuper

- Previous by Date: Re: [isabelle] running bibtex through document preparation
- Next by Date: Re: [isabelle] simp_trace_new
- Previous by Thread: Re: [isabelle] simp_trace_new
- Next by Thread: Re: [isabelle] simp_trace_new
- Cl-isabelle-users December 2014 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