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?

 - Johannes

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)
>    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.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.