[isabelle] SMT and bound variables.



Hi,

I'm getting annoyed by the tediousness required to discharge seemingly trivial problems on words and thought I would try the "smt" method on them.

(BTW: Is proof reconstruction available for Bitvectors?)

I found a strange behaviour (in 2012, 2013 and ffc3f1659a25): Consider the two goals stated below. They are equivalent, the only difference is between free and bound variables. Yet "smt" can only solve the second goal and suggests a possibly spurious counter-example for the first one.

--------------------------------------------------------------------------
theory Scratch imports "~~/src/HOL/Word/Word" begin

lemma "⋀degree k. (degree :: 32 word) ≤ 3 ⟹ k ≤ degree ⟹ k + 1 ≠ 0"
  using [[smt_oracle=true]]
  apply smt (* Fails, talks about possibly spurious counter-example *)
  oops

lemma "(degree :: 32 word) ≤ 3 ⟹ k ≤ degree ⟹ k + 1 ≠ 0"
  using [[smt_oracle=true]]
  apply smt (* Succeeds *)
  done
--------------------------------------------------------------------------

Is this some known limitation or a bug in the preprocessing?

Best regards,
  Lars




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