[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.
"(â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 (metis rtranclp.intros)
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.
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