739      (* For functional identity quotients, (op = ---> op =) *)

   739      (* For functional identity quotients, (op = ---> op =) *)

   740      (* TODO: think about the other way around, if we need to shorten the relation *)

   740      (* TODO: think about the other way around, if we need to shorten the relation *)

   741      CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])

   741      CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])

   742 *}

   742 *}

   743 

   743 

   744 lemma FUN_REL_I:

   745 lemma FUN_REL_I:

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

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

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

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

   747 using a by simp

   748 using a by simp

   748 

   749