[isabelle-dev] rtrancl lemma proposal

[Christian Sternagel]

Dear developers,

the following lemma seems like a basic fact about rtrancl:

lemma rtrancl_map:
   assumes "⋀x y. (x, y) ∈ r ⟹ (f x, f y) ∈ s"
     and "(x, y) ∈ r⇧*"
   shows "(f x, f y) ∈ s⇧*"
   using assms(2, 1)
   by (induct) (auto intro: rtrancl.rtrancl_into_rtrancl)

I didn't find it in Main. Did anybody else ever use/need it? Is it 
already part of some theory I did overlook? How about adding it?

Caveat: It seems to be necessary to strongly instantiate it before usage.

cheers

chris