Looks like a special case of simulation: lemma rtrancl_sim: assumes "⋀x y a. ⟦(x, y) ∈ r; (x,a)∈S⟧ ⟹ ∃b. (y,b)∈S ∧ (a, b) ∈ s" and "(x, y) ∈ r⇧*" and "(x,a)∈S" shows "∃b. (y,b)∈S ∧ (a, b) ∈ s⇧*" using assms(2, 1,3) by (induct) (fastforce intro: rtrancl.rtrancl_into_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 rtrancl_sim[where S="{(x,f x) | x. True}"] assms by simp blast -- Peter On Mi, 2014-10-01 at 14:27 +0200, Christian Sternagel wrote: > 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 > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev