src/HOL/BNF_Def.thy
changeset 57641 dc59f147b27d
parent 57398 882091eb1e9a
child 57698 afef6616cbae
     1.1 --- a/src/HOL/BNF_Def.thy	Thu Jul 24 11:51:22 2014 +0200
     1.2 +++ b/src/HOL/BNF_Def.thy	Thu Jul 24 11:54:15 2014 +0200
     1.3 @@ -53,21 +53,21 @@
     1.4  lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
     1.5    by (rule ext) (auto simp only: comp_apply collect_def)
     1.6  
     1.7 -definition convol ("<_ , _>") where
     1.8 -"<f , g> \<equiv> %a. (f a, g a)"
     1.9 +definition convol ("\<langle>(_,/ _)\<rangle>") where
    1.10 +"\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
    1.11  
    1.12  lemma fst_convol:
    1.13 -"fst \<circ> <f , g> = f"
    1.14 +"fst \<circ> \<langle>f, g\<rangle> = f"
    1.15  apply(rule ext)
    1.16  unfolding convol_def by simp
    1.17  
    1.18  lemma snd_convol:
    1.19 -"snd \<circ> <f , g> = g"
    1.20 +"snd \<circ> \<langle>f, g\<rangle> = g"
    1.21  apply(rule ext)
    1.22  unfolding convol_def by simp
    1.23  
    1.24  lemma convol_mem_GrpI:
    1.25 -"x \<in> A \<Longrightarrow> <id , g> x \<in> (Collect (split (Grp A g)))"
    1.26 +"x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))"
    1.27  unfolding convol_def Grp_def by auto
    1.28  
    1.29  definition csquare where
    1.30 @@ -182,7 +182,7 @@
    1.31  lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
    1.32    unfolding rel_fun_def vimage2p_def by auto
    1.33  
    1.34 -lemma convol_image_vimage2p: "<f \<circ> fst, g \<circ> snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
    1.35 +lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
    1.36    unfolding vimage2p_def convol_def by auto
    1.37  
    1.38  lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"