[isabelle-dev] rtrancl lemma proposal

[Peter Lammich]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev