equal
deleted
inserted
replaced
80 |
80 |
81 lemma UN_o: "UNION A (g o f) = UNION (f`A) g" |
81 lemma UN_o: "UNION A (g o f) = UNION (f`A) g" |
82 by (unfold comp_def, blast) |
82 by (unfold comp_def, blast) |
83 |
83 |
84 |
84 |
85 subsection {* The Forward Composition Operator @{text "f \<circ>> g"} *} |
85 subsection {* The Forward Composition Operator @{text fcomp} *} |
86 |
86 |
87 definition |
87 definition |
88 fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o>" 60) |
88 fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o>" 60) |
89 where |
89 where |
90 "f o> g = (\<lambda>x. g (f x))" |
90 "f o> g = (\<lambda>x. g (f x))" |
91 |
91 |
92 notation (xsymbols) |
|
93 fcomp (infixl "\<circ>>" 60) |
|
94 |
|
95 notation (HTML output) |
|
96 fcomp (infixl "\<circ>>" 60) |
|
97 |
|
98 lemma fcomp_apply: "(f o> g) x = g (f x)" |
92 lemma fcomp_apply: "(f o> g) x = g (f x)" |
99 by (simp add: fcomp_def) |
93 by (simp add: fcomp_def) |
100 |
94 |
101 lemma fcomp_assoc: "(f o> g) o> h = f o> (g o> h)" |
95 lemma fcomp_assoc: "(f o> g) o> h = f o> (g o> h)" |
102 by (simp add: fcomp_def) |
96 by (simp add: fcomp_def) |
104 lemma id_fcomp [simp]: "id o> g = g" |
98 lemma id_fcomp [simp]: "id o> g = g" |
105 by (simp add: fcomp_def) |
99 by (simp add: fcomp_def) |
106 |
100 |
107 lemma fcomp_id [simp]: "f o> id = f" |
101 lemma fcomp_id [simp]: "f o> id = f" |
108 by (simp add: fcomp_def) |
102 by (simp add: fcomp_def) |
|
103 |
|
104 no_notation fcomp (infixl "o>" 60) |
109 |
105 |
110 |
106 |
111 subsection {* Injectivity and Surjectivity *} |
107 subsection {* Injectivity and Surjectivity *} |
112 |
108 |
113 constdefs |
109 constdefs |