*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer*From*: Christoph LANGE <math.semantic.web at gmail.com>*Date*: Sun, 27 Oct 2013 16:06:16 +0100*Organization*: University of Birmingham*Sender*: Christoph Lange <allegristas at gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130919 Thunderbird/17.0.9

Dear Isabelle experts, my impression (which may have been wrong) from Isabelle2013 was that "try" tries "try0" before "sledgehammer". In Isabelle2013-1-RC3 this no longer seems to be the case. I find this quite annoying because I have made it a habit to enter "try" after almost every statement. In many cases I don't know whether try0 would be sufficient to prove something, or whether a more complex proof (such as those that sledgehammer finds) is required. Then, when sledgehammer finds a proof, looking at the lemmas used by this proof sometimes gives me the intuition that try0 might also suffice, e.g. when I know that all of these lemmas are simp rules. Here is a self-contained almost minimal example. I didn't try this with older versions but I'd be happy to do so. Please ignore the first step: maybe there is an easier proof for this, but for _this_ email only the second step is relevant. notepad begin fix R::"('a × 'b) set" and N::"'a set" and n::'a have "{ (x, y) . (x, y) ∈ R ∧ x ≠ n }¯ = { (y, x) . (y, x) ∈ R¯ ∧ x ≠ n }" by (smt Collect_cong converse_unfold curryE curry_split mem_Collect_eq splitD split_cong) then have "Domain { (x, y) . (x, y) ∈ R ∧ x ≠ n } = Range { (y, x) . (y, x) ∈ R¯ ∧ x ≠ n}" try end On my machine try0 finds that simp/auto/force each take 2 ms. However when I say "try", it resorts to running sledgehammer, which tells me: --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and "nitpick"... "z3": Sledgehammer ("z3") found a proof: by (metis Range_converse) (128 ms). To minimize: sledgehammer min (Range_converse `{(x, y). (x, y) ∈ R ∧ x ≠ n}¯ = {(y, x). (y, x) ∈ R¯ ∧ x ≠ n}`). "spass": Sledgehammer ("spass") found a proof: by (metis Range_converse) (108 ms). To minimize: sledgehammer min (Range_converse `{(x, y). (x, y) ∈ R ∧ x ≠ n}¯ = {(y, x). (y, x) ∈ R¯ ∧ x ≠ n}`). "remote_vampire": Sledgehammer ("remote_vampire") found a proof: by (metis Range_converse converse_unfold) (109 ms). To minimize: sledgehammer min (Range_converse converse_unfold `{(x, y). (x, y) ∈ R ∧ x ≠ n}¯ = {(y, x). (y, x) ∈ R¯ ∧ x ≠ n}`). "e": Sledgehammer ("e") found a proof: by (smt Collect_mem_eq Domain_Collect_split Domain_converse Domain_unfold converse_converse converse_unfold internal_split_def) (28 ms). To minimize: sledgehammer min [smt] (Collect_mem_eq Domain_Collect_split Domain_converse Domain_unfold converse_converse converse_unfold internal_split_def `{(x, y). (x, y) ∈ R ∧ x ≠ n}¯ = {(y, x). (y, x) ∈ R¯ ∧ x ≠ n}`). Structured proof (3 ms): proof - show "Domain {(x, y). (x, y) ∈ R ∧ x ≠ n} = Range {(y, x). (y, x) ∈ R¯ ∧ x ≠ n}" using Domain_unfold by auto qed --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- Here, it was clearly the last sledgehammer output that gave me the idea that try0 can do the job. In other cases (I'll be happy to dig out some more) it's not that easy. Any ideas? Cheers, and thanks in advance, Christoph -- Christoph Lange, School of Computer Science, University of Birmingham http://cs.bham.ac.uk/~langec/, Skype duke4701 → Mathematics in Computer Science Special Issue on “Enabling Domain Experts to use Formalised Reasoning”; submission until 31 October. http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/

**Follow-Ups**:

- Previous by Date: [isabelle] Relational & Algebraic Methods --- RAMiCS 2014 --- Final CFP, with Deadlines extended!
- Next by Date: Re: [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer
- Previous by Thread: [isabelle] Relational & Algebraic Methods --- RAMiCS 2014 --- Final CFP, with Deadlines extended!
- Next by Thread: Re: [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer
- Cl-isabelle-users October 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