Re: [isabelle] mono attribute



The [mono] attribute is used by the "inductive" package to keep track
of monotonicity of predicates w.r.t implication (-->) on type bool. In
older versions of Isabelle it used monotonicity w.r.t the subset
ordering on type 'a set. I don't think the package can do anything
with rules about monotonicity w.r.t (<=) on type nat.

Isabelle2012 doesn't have a command for listing all the registered
mono theorems (although it appears Makarius added a 'print_inductives'
command to the dev repo recently, 9149a07a6c67) but you can access
them via ML:

ML_val {* Inductive.get_monos @{context} *}

This should give you a general idea of what kinds of rules are accepted.

- Brian

On Mon, Dec 17, 2012 at 2:46 PM, John Wickerson <jpw48 at cam.ac.uk> wrote:
> 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.