Email Gateway (Aug 19 2022 at 09:32): Email Gateway (Aug 19 2022 at 09:32):From: John Wickerson <jpw48@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 09:32):From: Brian Huffman <huffman@in.tum.de>
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.
Email Gateway (Aug 19 2022 at 09:33):From: John Wickerson <jpw48@cam.ac.uk>
Thanks Brian. I was just using "==>" when I should have used "-->".
john
Last updated: Apr 19 2024 at 04:17 UTC