| changeset 53561 | 92bcac4f9ac9 |
| parent 53560 | 4b5f42cfa244 |
| child 54421 | 632be352a5a3 |
--- a/src/HOL/BNF/BNF_Def.thy Thu Sep 12 11:23:49 2013 +0200 +++ b/src/HOL/BNF/BNF_Def.thy Thu Sep 12 11:23:49 2013 +0200 @@ -89,6 +89,9 @@ lemma eq_OOI: "R = op = \<Longrightarrow> R = R OO R" by auto +lemma OO_Grp_alt: "(Grp A f)^--1 OO Grp A g = (\<lambda>x y. \<exists>z. z \<in> A \<and> f z = x \<and> g z = y)" + unfolding Grp_def by auto + lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f" unfolding Grp_def by auto