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



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.