src/HOL/Library/BNF_Corec.thy
changeset 67091 1393c2340eec
parent 64379 71f42dcaa1df
child 67399 eab6ce8368fa
--- a/src/HOL/Library/BNF_Corec.thy	Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Library/BNF_Corec.thy	Sun Nov 26 21:08:32 2017 +0100
@@ -31,17 +31,17 @@
   unfolding BNF_Def.Grp_def by auto
 
 lemma sum_comp_cases:
-  assumes "f o Inl = g o Inl" and "f o Inr = g o Inr"
+  assumes "f \<circ> Inl = g \<circ> Inl" and "f \<circ> Inr = g \<circ> Inr"
   shows "f = g"
 proof (rule ext)
   fix a show "f a = g a"
     using assms unfolding comp_def fun_eq_iff by (cases a) auto
 qed
 
-lemma case_sum_Inl_Inr_L: "case_sum (f o Inl) (f o Inr) = f"
+lemma case_sum_Inl_Inr_L: "case_sum (f \<circ> Inl) (f \<circ> Inr) = f"
   by (metis case_sum_expand_Inr')
 
-lemma eq_o_InrI: "\<lbrakk>g o Inl = h; case_sum h f = g\<rbrakk> \<Longrightarrow> f = g o Inr"
+lemma eq_o_InrI: "\<lbrakk>g \<circ> Inl = h; case_sum h f = g\<rbrakk> \<Longrightarrow> f = g \<circ> Inr"
   by (auto simp: fun_eq_iff split: sum.splits)
 
 lemma id_bnf_o: "BNF_Composition.id_bnf \<circ> f = f"
@@ -63,7 +63,7 @@
 
 subsection \<open>Coinduction\<close>
 
-lemma eq_comp_compI: "a o b = f o x \<Longrightarrow> x o c = id \<Longrightarrow> f = a o (b o c)"
+lemma eq_comp_compI: "a \<circ> b = f \<circ> x \<Longrightarrow> x \<circ> c = id \<Longrightarrow> f = a \<circ> (b \<circ> c)"
   unfolding fun_eq_iff by simp
 
 lemma self_bounded_weaken_left: "(a :: 'a :: semilattice_inf) \<le> inf a b \<Longrightarrow> a \<le> b"
@@ -159,7 +159,7 @@
   by (simp add: antisym cong_gen_cong gen_cong_minimal leq_gen_cong)
 
 lemma gen_cong_rho:
-  "\<rho> = eval o f \<Longrightarrow> rel (gen_cong R) (f x) (f y) \<Longrightarrow> gen_cong R (\<rho> x) (\<rho> y)"
+  "\<rho> = eval \<circ> f \<Longrightarrow> rel (gen_cong R) (f x) (f y) \<Longrightarrow> gen_cong R (\<rho> x) (\<rho> y)"
   by (simp add: gen_cong_eval)
 lemma coinduction:
   assumes coind: "\<forall>R. R \<le> retr R \<longrightarrow> R \<le> op ="
@@ -181,7 +181,7 @@
   fixes rel eval rel' eval' retr emb
   assumes base: "cong rel eval retr"
   and step: "cong rel' eval' retr"
-  and emb: "eval' o emb = eval"
+  and emb: "eval' \<circ> emb = eval"
   and emb_transfer: "rel_fun (rel R) (rel' R) emb emb"
 begin