[isabelle-dev] new lemmas for Transitive_Closure + renaming

Christian Sternagel c-sterna at jaist.ac.jp
Fri Dec 21 05:18:35 CET 2012

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+

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?



More information about the isabelle-dev mailing list