[isabelle-dev] rtrancl lemma proposal
c.sternagel at gmail.com
Wed Oct 1 14:27:48 CEST 2014
the following lemma seems like a basic fact about rtrancl:
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.
More information about the isabelle-dev