1.1 --- a/src/HOL/Fun.thy Thu Nov 18 12:37:30 2010 +0100
1.2 +++ b/src/HOL/Fun.thy Thu Nov 18 17:01:15 2010 +0100
1.3 @@ -117,6 +117,19 @@
1.4 no_notation fcomp (infixl "\<circ>>" 60)
1.5
1.6
1.7 +subsection {* Mapping functions *}
1.8 +
1.9 +definition map_fun :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" where
1.10 + "map_fun f g h = g \<circ> h \<circ> f"
1.11 +
1.12 +lemma map_fun_apply [simp]:
1.13 + "map_fun f g h x = g (h (f x))"
1.14 + by (simp add: map_fun_def)
1.15 +
1.16 +type_mapper map_fun
1.17 + by (simp_all add: fun_eq_iff)
1.18 +
1.19 +
1.20 subsection {* Injectivity, Surjectivity and Bijectivity *}
1.21
1.22 definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
2.1 --- a/src/HOL/Library/Quotient_Syntax.thy Thu Nov 18 12:37:30 2010 +0100
2.2 +++ b/src/HOL/Library/Quotient_Syntax.thy Thu Nov 18 17:01:15 2010 +0100
2.3 @@ -10,7 +10,7 @@
2.4
2.5 notation
2.6 rel_conj (infixr "OOO" 75) and
2.7 - fun_map (infixr "--->" 55) and
2.8 + map_fun (infixr "--->" 55) and
2.9 fun_rel (infixr "===>" 55)
2.10
2.11 end
3.1 --- a/src/HOL/Quotient.thy Thu Nov 18 12:37:30 2010 +0100
3.2 +++ b/src/HOL/Quotient.thy Thu Nov 18 17:01:15 2010 +0100
3.3 @@ -160,18 +160,11 @@
3.4
3.5 subsection {* Function map and function relation *}
3.6
3.7 -definition
3.8 - fun_map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" (infixr "--->" 55)
3.9 -where
3.10 - "fun_map f g = (\<lambda>h. g \<circ> h \<circ> f)"
3.11 +notation map_fun (infixr "--->" 55)
3.12
3.13 -lemma fun_map_apply [simp]:
3.14 - "(f ---> g) h x = g (h (f x))"
3.15 - by (simp add: fun_map_def)
3.16 -
3.17 -lemma fun_map_id:
3.18 +lemma map_fun_id:
3.19 "(id ---> id) = id"
3.20 - by (simp add: fun_eq_iff id_def)
3.21 + by (simp add: fun_eq_iff)
3.22
3.23 definition
3.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)
3.25 @@ -520,13 +513,13 @@
3.26 lemma all_prs:
3.27 assumes a: "Quotient R absf repf"
3.28 shows "Ball (Respects R) ((absf ---> id) f) = All f"
3.29 - using a unfolding Quotient_def Ball_def in_respects id_apply comp_def fun_map_def
3.30 + using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def
3.31 by metis
3.32
3.33 lemma ex_prs:
3.34 assumes a: "Quotient R absf repf"
3.35 shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
3.36 - using a unfolding Quotient_def Bex_def in_respects id_apply comp_def fun_map_def
3.37 + using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def
3.38 by metis
3.39
3.40 subsection {* @{text Bex1_rel} quantifier *}
3.41 @@ -789,7 +782,7 @@
3.42
3.43 use "Tools/Quotient/quotient_info.ML"
3.44
3.45 -declare [[map "fun" = (fun_map, fun_rel)]]
3.46 +declare [[map "fun" = (map_fun, fun_rel)]]
3.47
3.48 lemmas [quot_thm] = fun_quotient
3.49 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
3.50 @@ -800,7 +793,7 @@
3.51 text {* Lemmas about simplifying id's. *}
3.52 lemmas [id_simps] =
3.53 id_def[symmetric]
3.54 - fun_map_id
3.55 + map_fun_id
3.56 id_apply
3.57 id_o
3.58 o_id
3.59 @@ -880,7 +873,7 @@
3.60
3.61 no_notation
3.62 rel_conj (infixr "OOO" 75) and
3.63 - fun_map (infixr "--->" 55) and
3.64 + map_fun (infixr "--->" 55) and
3.65 fun_rel (infixr "===>" 55)
3.66
3.67 end
4.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Nov 18 12:37:30 2010 +0100
4.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Nov 18 17:01:15 2010 +0100
4.3 @@ -383,7 +383,7 @@
4.4 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
4.5
4.6 (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
4.7 - (* observe fun_map *)
4.8 + (* observe map_fun *)
4.9 | _ $ _ $ _
4.10 => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
4.11 ORELSE' rep_abs_rsp_tac ctxt
4.12 @@ -428,23 +428,23 @@
4.13
4.14 (*** Cleaning of the Theorem ***)
4.15
4.16 -(* expands all fun_maps, except in front of the (bound) variables listed in xs *)
4.17 -fun fun_map_simple_conv xs ctrm =
4.18 +(* expands all map_funs, except in front of the (bound) variables listed in xs *)
4.19 +fun map_fun_simple_conv xs ctrm =
4.20 case (term_of ctrm) of
4.21 - ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
4.22 + ((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) =>
4.23 if member (op=) xs h
4.24 then Conv.all_conv ctrm
4.25 - else Conv.rewr_conv @{thm fun_map_apply [THEN eq_reflection]} ctrm
4.26 + else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
4.27 | _ => Conv.all_conv ctrm
4.28
4.29 -fun fun_map_conv xs ctxt ctrm =
4.30 +fun map_fun_conv xs ctxt ctrm =
4.31 case (term_of ctrm) of
4.32 - _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
4.33 - fun_map_simple_conv xs) ctrm
4.34 - | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
4.35 + _ $ _ => (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
4.36 + map_fun_simple_conv xs) ctrm
4.37 + | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
4.38 | _ => Conv.all_conv ctrm
4.39
4.40 -fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
4.41 +fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt)
4.42
4.43 (* custom matching functions *)
4.44 fun mk_abs u i t =
4.45 @@ -480,7 +480,7 @@
4.46 *)
4.47 fun lambda_prs_simple_conv ctxt ctrm =
4.48 case (term_of ctrm) of
4.49 - (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
4.50 + (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
4.51 let
4.52 val thy = ProofContext.theory_of ctxt
4.53 val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
4.54 @@ -534,7 +534,7 @@
4.55
4.56 val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
4.57 in
4.58 - EVERY' [fun_map_tac lthy,
4.59 + EVERY' [map_fun_tac lthy,
4.60 lambda_prs_tac lthy,
4.61 simp_tac ss,
4.62 TRY o rtac refl]