[isabelle] Monotonicity of rtrancl for inductive/inductive_set



Hello Isabelle users.

It looks like the following inductive-compatible monotonicity rule for
rtranclp is useful for some inductive definitions.

lemma rtrancl_mono_proof[mono]:
  "(âa b. x a b â y a b) â rtranclp x a b â rtranclp y a b"
  apply (rule impI, rotate_tac, induct rule: rtranclp.induct)
   apply simp_all
  apply (metis rtranclp.intros)
  done

It looks like this is the kind of rule the system should supply by
default, especially as coercion between trancl/rtrancl can leave users
quite confused what the problem really is.

Cheers,
    Thomas.

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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