384 lemma fun_rel_id:

   384 lemma fun_rel_id:

   385   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"

   385   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"

   386   shows "(R1 ===> R2) f g"

   386   shows "(R1 ===> R2) f g"

   387 using a by simp

   387 using a by simp

   388 

   388 

   389 lemma quot_rel_rsp:

   394 lemma quot_rel_rsp:

   390   assumes a: "Quotient R Abs Rep"

   395   assumes a: "Quotient R Abs Rep"

   391   shows "(R ===> R ===> op =) R R"

   396   shows "(R ===> R ===> op =) R R"

   392   apply(rule fun_rel_id)+

   397   apply(rule fun_rel_id)+

   393   apply(rule equals_rsp[OF a])

   398   apply(rule equals_rsp[OF a])