src/HOL/Fun.thy
changeset 49739 13aa6d8268ec
parent 48891 c0eafbd55de3
child 49905 a81f95693c68
     1.1 --- a/src/HOL/Fun.thy	Mon Oct 08 11:37:03 2012 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Oct 08 12:03:49 2012 +0200
     1.3 @@ -41,34 +41,41 @@
     1.4  notation (HTML output)
     1.5    comp  (infixl "\<circ>" 55)
     1.6  
     1.7 -lemma o_apply [simp]: "(f o g) x = f (g x)"
     1.8 -by (simp add: comp_def)
     1.9 -
    1.10 -lemma o_assoc: "f o (g o h) = f o g o h"
    1.11 -by (simp add: comp_def)
    1.12 +lemma comp_apply [simp]: "(f o g) x = f (g x)"
    1.13 +  by (simp add: comp_def)
    1.14  
    1.15 -lemma id_o [simp]: "id o g = g"
    1.16 -by (simp add: comp_def)
    1.17 +lemma comp_assoc: "(f o g) o h = f o (g o h)"
    1.18 +  by (simp add: fun_eq_iff)
    1.19  
    1.20 -lemma o_id [simp]: "f o id = f"
    1.21 -by (simp add: comp_def)
    1.22 +lemma id_comp [simp]: "id o g = g"
    1.23 +  by (simp add: fun_eq_iff)
    1.24  
    1.25 -lemma o_eq_dest:
    1.26 +lemma comp_id [simp]: "f o id = f"
    1.27 +  by (simp add: fun_eq_iff)
    1.28 +
    1.29 +lemma comp_eq_dest:
    1.30    "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
    1.31 -  by (simp only: comp_def) (fact fun_cong)
    1.32 +  by (simp add: fun_eq_iff)
    1.33  
    1.34 -lemma o_eq_elim:
    1.35 +lemma comp_eq_elim:
    1.36    "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    1.37 -  by (erule meta_mp) (fact o_eq_dest) 
    1.38 +  by (simp add: fun_eq_iff) 
    1.39  
    1.40 -lemma image_compose: "(f o g) ` r = f`(g`r)"
    1.41 -by (simp add: comp_def, blast)
    1.42 -
    1.43 -lemma vimage_compose: "(g \<circ> f) -` x = f -` (g -` x)"
    1.44 +lemma image_comp:
    1.45 +  "(f o g) ` r = f ` (g ` r)"
    1.46    by auto
    1.47  
    1.48 -lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
    1.49 -by (unfold comp_def, blast)
    1.50 +lemma vimage_comp:
    1.51 +  "(g \<circ> f) -` x = f -` (g -` x)"
    1.52 +  by auto
    1.53 +
    1.54 +lemma INF_comp:
    1.55 +  "INFI A (g \<circ> f) = INFI (f ` A) g"
    1.56 +  by (simp add: INF_def image_comp)
    1.57 +
    1.58 +lemma SUP_comp:
    1.59 +  "SUPR A (g \<circ> f) = SUPR (f ` A) g"
    1.60 +  by (simp add: SUP_def image_comp)
    1.61  
    1.62  
    1.63  subsection {* The Forward Composition Operator @{text fcomp} *}
    1.64 @@ -735,10 +742,6 @@
    1.65    by (rule the_inv_into_f_f)
    1.66  
    1.67  
    1.68 -text{*compatibility*}
    1.69 -lemmas o_def = comp_def
    1.70 -
    1.71 -
    1.72  subsection {* Cantor's Paradox *}
    1.73  
    1.74  lemma Cantors_paradox [no_atp]:
    1.75 @@ -806,7 +809,19 @@
    1.76    by (simp_all add: fun_eq_iff)
    1.77  
    1.78  enriched_type vimage
    1.79 -  by (simp_all add: fun_eq_iff vimage_compose)
    1.80 +  by (simp_all add: fun_eq_iff vimage_comp)
    1.81 +
    1.82 +text {* Legacy theorem names *}
    1.83 +
    1.84 +lemmas o_def = comp_def
    1.85 +lemmas o_apply = comp_apply
    1.86 +lemmas o_assoc = comp_assoc [symmetric]
    1.87 +lemmas id_o = id_comp
    1.88 +lemmas o_id = comp_id
    1.89 +lemmas o_eq_dest = comp_eq_dest
    1.90 +lemmas o_eq_elim = comp_eq_elim
    1.91 +lemmas image_compose = image_comp
    1.92 +lemmas vimage_compose = vimage_comp
    1.93  
    1.94  end
    1.95