[isabelle-dev] new lemmas for Transitive_Closure + renaming

[Tobias Nipkow]

Am 21/12/2012 05:18, schrieb Christian Sternagel:
> Dear all,
> 
> I suggest to add the following lemmas to Transitive_Closure and the simplifier
> (I just copied the unicode-tokens from Isabelle/jEdit... I hope what arrives
> after emailing is the same what I sent):
> 
> lemma
>   reflcl_idemp [simp]: "(R⇧=)⇧= = R⇧=" and
>   reflclp_idemp [simp]: "(P⇧=⇧=)⇧=⇧= = P⇧=⇧="
>   by blast+

I have added the first one, in more general form: since R^= abbreviates "R Un
Id", I added, in the most general type class, the simp rule "f (f A B) B = f A
B", wondering what this would do. The result surprised me: zero impact on the
distribution and exactly 1 proof became shorter in the AFP (where f = max).

Tobias

> Plus, for consistency, the following lemmas should be renamed:
> 
>   reflcl_tranclp ~> reflclp_tranclp
>   rtranclp_reflcl ~> rtranclp_reflclp
> 
> and maybe
> 
>   reflcl_set_eq ~> reflclp_reflcl_conv
> 
> What do you think?
> 
> cheers
> 
> chris
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev