src/HOL/Quotient.thy
changeset 40602 91e583511113
parent 40466 c6587375088e
child 40615 ab551d108feb
     1.1 --- a/src/HOL/Quotient.thy	Thu Nov 18 12:37:30 2010 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Thu Nov 18 17:01:15 2010 +0100
     1.3 @@ -160,18 +160,11 @@
     1.4  
     1.5  subsection {* Function map and function relation *}
     1.6  
     1.7 -definition
     1.8 -  fun_map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" (infixr "--->" 55)
     1.9 -where
    1.10 -  "fun_map f g = (\<lambda>h. g \<circ> h \<circ> f)"
    1.11 +notation map_fun (infixr "--->" 55)
    1.12  
    1.13 -lemma fun_map_apply [simp]:
    1.14 -  "(f ---> g) h x = g (h (f x))"
    1.15 -  by (simp add: fun_map_def)
    1.16 -
    1.17 -lemma fun_map_id:
    1.18 +lemma map_fun_id:
    1.19    "(id ---> id) = id"
    1.20 -  by (simp add: fun_eq_iff id_def)
    1.21 +  by (simp add: fun_eq_iff)
    1.22  
    1.23  definition
    1.24    fun_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" (infixr "===>" 55)
    1.25 @@ -520,13 +513,13 @@
    1.26  lemma all_prs:
    1.27    assumes a: "Quotient R absf repf"
    1.28    shows "Ball (Respects R) ((absf ---> id) f) = All f"
    1.29 -  using a unfolding Quotient_def Ball_def in_respects id_apply comp_def fun_map_def
    1.30 +  using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def
    1.31    by metis
    1.32  
    1.33  lemma ex_prs:
    1.34    assumes a: "Quotient R absf repf"
    1.35    shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
    1.36 -  using a unfolding Quotient_def Bex_def in_respects id_apply comp_def fun_map_def
    1.37 +  using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def
    1.38    by metis
    1.39  
    1.40  subsection {* @{text Bex1_rel} quantifier *}
    1.41 @@ -789,7 +782,7 @@
    1.42  
    1.43  use "Tools/Quotient/quotient_info.ML"
    1.44  
    1.45 -declare [[map "fun" = (fun_map, fun_rel)]]
    1.46 +declare [[map "fun" = (map_fun, fun_rel)]]
    1.47  
    1.48  lemmas [quot_thm] = fun_quotient
    1.49  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
    1.50 @@ -800,7 +793,7 @@
    1.51  text {* Lemmas about simplifying id's. *}
    1.52  lemmas [id_simps] =
    1.53    id_def[symmetric]
    1.54 -  fun_map_id
    1.55 +  map_fun_id
    1.56    id_apply
    1.57    id_o
    1.58    o_id
    1.59 @@ -880,7 +873,7 @@
    1.60  
    1.61  no_notation
    1.62    rel_conj (infixr "OOO" 75) and
    1.63 -  fun_map (infixr "--->" 55) and
    1.64 +  map_fun (infixr "--->" 55) and
    1.65    fun_rel (infixr "===>" 55)
    1.66  
    1.67  end