Re: [isabelle] Monotonicity of rtrancl for inductive/inductive_set
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.
> 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)
> 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