Re: [isabelle] Monotonicity of rtrancl for inductive/inductive_set
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and