src/HOL/BNF_FP_Base.thy
changeset 55066 4e5ddf3162ac
parent 55062 6d3fad6f01c9
child 55079 ec08a67e993b
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  by auto
     1.5  
     1.6  lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
     1.7 -unfolding o_def fun_eq_iff by simp
     1.8 +unfolding comp_def fun_eq_iff by simp
     1.9  
    1.10  lemma o_bij:
    1.11    assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
    1.12 @@ -113,16 +113,16 @@
    1.13  by blast
    1.14  
    1.15  lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
    1.16 -  unfolding o_def fun_eq_iff by auto
    1.17 +  unfolding comp_def fun_eq_iff by auto
    1.18  
    1.19  lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2"
    1.20 -  unfolding o_def fun_eq_iff by auto
    1.21 +  unfolding comp_def fun_eq_iff by auto
    1.22  
    1.23  lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
    1.24 -  unfolding o_def fun_eq_iff by auto
    1.25 +  unfolding comp_def fun_eq_iff by auto
    1.26  
    1.27  lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r"
    1.28 -  unfolding o_def fun_eq_iff by auto
    1.29 +  unfolding comp_def fun_eq_iff by auto
    1.30  
    1.31  lemma convol_o: "<f, g> o h = <f o h, g o h>"
    1.32    unfolding convol_def by auto
    1.33 @@ -131,16 +131,16 @@
    1.34    unfolding convol_def by auto
    1.35  
    1.36  lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
    1.37 -  unfolding map_pair_o_convol id_o o_id ..
    1.38 +  unfolding map_pair_o_convol id_comp comp_id ..
    1.39  
    1.40  lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
    1.41 -  unfolding o_def by (auto split: sum.splits)
    1.42 +  unfolding comp_def by (auto split: sum.splits)
    1.43  
    1.44  lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
    1.45 -  unfolding o_def by (auto split: sum.splits)
    1.46 +  unfolding comp_def by (auto split: sum.splits)
    1.47  
    1.48  lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
    1.49 -  unfolding sum_case_o_sum_map id_o o_id ..
    1.50 +  unfolding sum_case_o_sum_map id_comp comp_id ..
    1.51  
    1.52  lemma fun_rel_def_butlast:
    1.53    "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"