[isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer



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/





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.