src/HOL/BNF/BNF_Def.thy
changeset 53561 92bcac4f9ac9
parent 53560 4b5f42cfa244
child 54421 632be352a5a3
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:23:49 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Thu Sep 12 11:23:49 2013 +0200
     1.3 @@ -89,6 +89,9 @@
     1.4  lemma eq_OOI: "R = op = \<Longrightarrow> R = R OO R"
     1.5    by auto
     1.6  
     1.7 +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)"
     1.8 +  unfolding Grp_def by auto
     1.9 +
    1.10  lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f"
    1.11  unfolding Grp_def by auto
    1.12