[isabelle] mono attribute



Hi Isabelle,

I'm a bit confused about the [mono] attribute. The Isar tutorial says that I can declare new monotonicity rules using the mono attribute, but when I type the simplest monotonicity lemma I can think of:

lemma blah [mono]:
  "x ≤ y ⟹ Suc x ≤ Suc y"
by auto

I get the following error:

Bad monotonicity theorem:
?x ≤ ?y ⟹ Suc ?x ≤ Suc ?y 

Could somebody kindly explain what's happening here? Thanks very much.

john




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