added forward composition
authorhaftmann
Thu Mar 20 12:04:53 2008 +0100 (2008-03-20)
changeset 2635719b153ebda0b
parent 26356 2312df2efa12
child 26358 d6a508c16908
added forward composition
src/HOL/Fun.thy
     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.47    (Haskell "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