--- a/src/HOL/Fun.thy Thu Mar 20 12:02:52 2008 +0100
+++ b/src/HOL/Fun.thy Thu Mar 20 12:04:53 2008 +0100
@@ -20,7 +20,7 @@
done
lemma apply_inverse:
- "f x =u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
+ "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
by auto
@@ -82,6 +82,32 @@
by (unfold comp_def, blast)
+subsection {* The Forward Composition Operator @{text "f \<circ>> g"} *}
+
+definition
+ fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o>" 60)
+where
+ "f o> g = (\<lambda>x. g (f x))"
+
+notation (xsymbols)
+ fcomp (infixl "\<circ>>" 60)
+
+notation (HTML output)
+ fcomp (infixl "\<circ>>" 60)
+
+lemma fcomp_apply: "(f o> g) x = g (f x)"
+ by (simp add: fcomp_def)
+
+lemma fcomp_assoc: "(f o> g) o> h = f o> (g o> h)"
+ by (simp add: fcomp_def)
+
+lemma id_fcomp [simp]: "id o> g = g"
+ by (simp add: fcomp_def)
+
+lemma fcomp_id [simp]: "f o> id = f"
+ by (simp add: fcomp_def)
+
+
subsection {* Injectivity and Surjectivity *}
constdefs
@@ -528,23 +554,4 @@
code_const "id"
(Haskell "id")
-
-subsection {* ML legacy bindings *}
-
-ML {*
-val set_cs = @{claset} delrules [@{thm equalityI}]
-*}
-
-ML {*
-val id_apply = @{thm id_apply}
-val id_def = @{thm id_def}
-val o_apply = @{thm o_apply}
-val o_assoc = @{thm o_assoc}
-val o_def = @{thm o_def}
-val injD = @{thm injD}
-val datatype_injI = @{thm datatype_injI}
-val range_ex1_eq = @{thm range_ex1_eq}
-val expand_fun_eq = @{thm expand_fun_eq}
-*}
-
end