author haftmann Thu Mar 20 12:04:53 2008 +0100 (2008-03-20) changeset 26357 19b153ebda0b parent 26356 2312df2efa12 child 26358 d6a508c16908
 src/HOL/Fun.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Fun.thy	Thu Mar 20 12:02:52 2008 +0100
1.2 +++ b/src/HOL/Fun.thy	Thu Mar 20 12:04:53 2008 +0100
1.3 @@ -20,7 +20,7 @@
1.4  done
1.5
1.6  lemma apply_inverse:
1.7 -  "f x =u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
1.8 +  "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
1.9    by auto
1.10
1.11
1.12 @@ -82,6 +82,32 @@
1.13  by (unfold comp_def, blast)
1.14
1.15
1.16 +subsection {* The Forward Composition Operator @{text "f \<circ>> g"} *}
1.17 +
1.18 +definition
1.19 +  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o>" 60)
1.20 +where
1.21 +  "f o> g = (\<lambda>x. g (f x))"
1.22 +
1.23 +notation (xsymbols)
1.24 +  fcomp  (infixl "\<circ>>" 60)
1.25 +
1.26 +notation (HTML output)
1.27 +  fcomp  (infixl "\<circ>>" 60)
1.28 +
1.29 +lemma fcomp_apply:  "(f o> g) x = g (f x)"
1.30 +  by (simp add: fcomp_def)
1.31 +
1.32 +lemma fcomp_assoc: "(f o> g) o> h = f o> (g o> h)"
1.33 +  by (simp add: fcomp_def)
1.34 +
1.35 +lemma id_fcomp [simp]: "id o> g = g"
1.36 +  by (simp add: fcomp_def)
1.37 +
1.38 +lemma fcomp_id [simp]: "f o> id = f"
1.39 +  by (simp add: fcomp_def)
1.40 +
1.41 +
1.42  subsection {* Injectivity and Surjectivity *}
1.43
1.44  constdefs
1.45 @@ -528,23 +554,4 @@
1.46  code_const "id"
1.48
1.49 -
1.50 -subsection {* ML legacy bindings *}
1.51 -
1.52 -ML {*
1.53 -val set_cs = @{claset} delrules [@{thm equalityI}]
1.54 -*}
1.55 -
1.56 -ML {*
1.57 -val id_apply = @{thm id_apply}
1.58 -val id_def = @{thm id_def}
1.59 -val o_apply = @{thm o_apply}
1.60 -val o_assoc = @{thm o_assoc}
1.61 -val o_def = @{thm o_def}
1.62 -val injD = @{thm injD}
1.63 -val datatype_injI = @{thm datatype_injI}
1.64 -val range_ex1_eq = @{thm range_ex1_eq}
1.65 -val expand_fun_eq = @{thm expand_fun_eq}
1.66 -*}
1.67 -
1.68  end
```