[isabelle] Sledgehammer proof reconstruction failed


I was trying to infer the following:

theory Scratch
  imports Complex_Main

notepad begin
  fix a n :: nat
  assume "a dvd n" "a < n powr (1/3)" "1 < n"
  then have "a < n" by (smt divide_le_eq_1_pos of_nat_1_eq_iff of_nat_less_iff powr_less_cancel powr_one_gt_zero_iff)

This smt call has been suggested by Sledgehammer, but with the words
"proof reconstruction failed". Here is the exact error it generates:

exception THM 1 raised (line 2237 of "thm.ML"):
 RSN: no unifiers
 1 < n
 ¬ real n + - 1 * real 1 ≤ 0 ⟹ 1 < n

Is this a bug? It certainly seems like one...

Jakub Kądziołka

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