Re: [isabelle] Monotonicity of rtrancl for inductive/inductive_set
Okay, added now as mono_rtranclp.
Am Dienstag, den 07.07.2015, 17:36 +0200 schrieb Andreas Lochbihler:
> 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.
> 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?
> > - 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