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}"
```