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



Thanks all, hopefully that sorts the issue out for the future.

Cheers,
    Thomas.

On 08/07/15 02:03, Johannes HÃlzl wrote:
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.






________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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