src/HOL/BNF_Greatest_Fixpoint.thy
changeset 67091 1393c2340eec
parent 66248 df85956228c2
child 67613 ce654b0e6d69
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4  
     1.5  lemma equiv_proj:
     1.6    assumes e: "equiv A R" and m: "z \<in> R"
     1.7 -  shows "(proj R o fst) z = (proj R o snd) z"
     1.8 +  shows "(proj R \<circ> fst) z = (proj R \<circ> snd) z"
     1.9  proof -
    1.10    from m have z: "(fst z, snd z) \<in> R" by auto
    1.11    with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R"
    1.12 @@ -139,10 +139,10 @@
    1.13  lemma fst_diag_id: "(fst \<circ> (\<lambda>x. (x, x))) z = id z" by simp
    1.14  lemma snd_diag_id: "(snd \<circ> (\<lambda>x. (x, x))) z = id z" by simp
    1.15  
    1.16 -lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
    1.17 -lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
    1.18 -lemma fst_diag_snd: "fst o ((\<lambda>x. (x, x)) o snd) = snd" by auto
    1.19 -lemma snd_diag_snd: "snd o ((\<lambda>x. (x, x)) o snd) = snd" by auto
    1.20 +lemma fst_diag_fst: "fst \<circ> ((\<lambda>x. (x, x)) \<circ> fst) = fst" by auto
    1.21 +lemma snd_diag_fst: "snd \<circ> ((\<lambda>x. (x, x)) \<circ> fst) = fst" by auto
    1.22 +lemma fst_diag_snd: "fst \<circ> ((\<lambda>x. (x, x)) \<circ> snd) = snd" by auto
    1.23 +lemma snd_diag_snd: "snd \<circ> ((\<lambda>x. (x, x)) \<circ> snd) = snd" by auto
    1.24  
    1.25  definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
    1.26  definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"