Theory Tangle_Relation

theory Tangle_Relation
imports  Main
begin



lemma symmetry1: assumes "symp R" 
shows "x y. (x, y)  {(x, y). R x y}*  (y, x)  {(x, y). R x y}*" 
proof-
have  "R x y   R y x" by (metis assms sympD)
then have " (x, y)  {(x, y). R x y}  (y, x)  {(x, y). R x y}" by auto
then have 2:" x y. (x, y)  {(x, y). R x y}  (y, x)  {(x, y). R x y}"
 by (metis (full_types) assms mem_Collect_eq split_conv sympE)
then have "sym {(x, y). R x y}" unfolding sym_def by auto
then have 3: "sym (rtrancl {(x, y). R x y})" using sym_rtrancl by auto
then show ?thesis by (metis symE)
qed

lemma symmetry2: assumes "x y. (x, y)  {(x, y). R x y}*  (y, x)  {(x, y). R x y}* "
shows "symp R^**" 
unfolding symp_def Enum.rtranclp_rtrancl_eq assms by (metis assms)

lemma symmetry3: assumes "symp R" shows "symp R^**" using assms symmetry1 symmetry2 by metis

lemma symm_trans: assumes "symp R" shows "symp R^++" by (metis assms rtranclpD symmetry3 symp_def tranclp_into_rtranclp)

end