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
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
