Email Gateway (Aug 22 2022 at 10:48): Email Gateway (Aug 22 2022 at 10:48):From: Thomas Sewell <thomas.sewell@nicta.com.au>
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.
Email Gateway (Aug 22 2022 at 10:49):From: Johannes Hölzl <hoelzl@in.tum.de>
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?
Email Gateway (Aug 22 2022 at 10:49):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Johannes,
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.
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:49):From: Johannes Hölzl <hoelzl@in.tum.de>
Okay, added now as mono_rtranclp.
Email Gateway (Aug 22 2022 at 10:50):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Thanks all, hopefully that sorts the issue out for the future.
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.
Last updated: Apr 20 2024 at 04:19 UTC