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