Re: [isabelle] mono attribute



Thanks Brian. I was just using "==>" when I should have used "-->".

john

On 18 Dec 2012, at 00:25, Brian Huffman wrote:

> 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.