Re: [isabelle] Monotonicity of rtrancl for inductive/inductive_set
Thanks all, hopefully that sorts the issue out for the future.
On 08/07/15 02:03, Johannes HÃlzl wrote:
Okay, added now as mono_rtranclp.
Am Dienstag, den 07.07.2015, 17:36 +0200 schrieb Andreas Lochbihler:
The monotonicity prover of the inductive package expects the conclusion and assumptions of
monotonicity rules to be HOL implications. To me, Thomas' rule has the right format and
should be added.
On 07/07/15 17:33, Johannes HÃlzl wrote:
So, you are proposing that this rule should be added to the Isabelle
repository as default rule? Sure I can add this rule!
But I wonder where the HOL implication â comes from? Is it introduced by
the inductive package?
Am Dienstag, den 07.07.2015, 13:57 +1000 schrieb Thomas Sewell:
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