Re: [isabelle] Monotonicity of rtrancl for inductive/inductive_set



Okay, added now as mono_rtranclp.

 - Johannes

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.
> 
> Best,
> Andreas
> 
> 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 MHonArc.