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