src/HOL/BNF_Greatest_Fixpoint.thy
changeset 67613 ce654b0e6d69
parent 67091 1393c2340eec
child 69605 a96320074298
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Tue Feb 13 14:24:50 2018 +0100
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Feb 15 12:11:00 2018 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4  lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
     1.5    by fast
     1.6  
     1.7 -lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
     1.8 +lemma converse_Times: "(A \<times> B)\<inverse> = B \<times> A"
     1.9    by fast
    1.10  
    1.11  lemma equiv_proj:
    1.12 @@ -56,7 +56,7 @@
    1.13  lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
    1.14    by auto
    1.15  
    1.16 -lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
    1.17 +lemma image2_Gr: "image2 A f g = (Gr A f)\<inverse> O (Gr A g)"
    1.18    unfolding image2_def Gr_def by auto
    1.19  
    1.20  lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
    1.21 @@ -99,10 +99,10 @@
    1.22    "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
    1.23  
    1.24  lemma relImage_Gr:
    1.25 -  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
    1.26 +  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)\<inverse> O R O Gr A f"
    1.27    unfolding relImage_def Gr_def relcomp_def by auto
    1.28  
    1.29 -lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
    1.30 +lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)\<inverse>"
    1.31    unfolding Gr_def relcomp_def image_def relInvImage_def by auto
    1.32  
    1.33  lemma relImage_mono: