[isabelle-dev] new lemmas for Transitive_Closure + renaming
nipkow at in.tum.de
Sat Dec 22 14:04:23 CET 2012
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):
> 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).
> 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?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev