--- a/src/HOL/Fun.thy Thu Nov 18 12:37:30 2010 +0100
+++ b/src/HOL/Fun.thy Thu Nov 18 17:01:15 2010 +0100
@@ -117,6 +117,19 @@
no_notation fcomp (infixl "\<circ>>" 60)
+subsection {* Mapping functions *}
+
+definition map_fun :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" where
+ "map_fun f g h = g \<circ> h \<circ> f"
+
+lemma map_fun_apply [simp]:
+ "map_fun f g h x = g (h (f x))"
+ by (simp add: map_fun_def)
+
+type_mapper map_fun
+ by (simp_all add: fun_eq_iff)
+
+
subsection {* Injectivity, Surjectivity and Bijectivity *}
definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
--- a/src/HOL/Library/Quotient_Syntax.thy Thu Nov 18 12:37:30 2010 +0100
+++ b/src/HOL/Library/Quotient_Syntax.thy Thu Nov 18 17:01:15 2010 +0100
@@ -10,7 +10,7 @@
notation
rel_conj (infixr "OOO" 75) and
- fun_map (infixr "--->" 55) and
+ map_fun (infixr "--->" 55) and
fun_rel (infixr "===>" 55)
end
--- a/src/HOL/Quotient.thy Thu Nov 18 12:37:30 2010 +0100
+++ b/src/HOL/Quotient.thy Thu Nov 18 17:01:15 2010 +0100
@@ -160,18 +160,11 @@
subsection {* Function map and function relation *}
-definition
- fun_map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" (infixr "--->" 55)
-where
- "fun_map f g = (\<lambda>h. g \<circ> h \<circ> f)"
+notation map_fun (infixr "--->" 55)
-lemma fun_map_apply [simp]:
- "(f ---> g) h x = g (h (f x))"
- by (simp add: fun_map_def)
-
-lemma fun_map_id:
+lemma map_fun_id:
"(id ---> id) = id"
- by (simp add: fun_eq_iff id_def)
+ by (simp add: fun_eq_iff)
definition
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)
@@ -520,13 +513,13 @@
lemma all_prs:
assumes a: "Quotient R absf repf"
shows "Ball (Respects R) ((absf ---> id) f) = All f"
- using a unfolding Quotient_def Ball_def in_respects id_apply comp_def fun_map_def
+ using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def
by metis
lemma ex_prs:
assumes a: "Quotient R absf repf"
shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
- using a unfolding Quotient_def Bex_def in_respects id_apply comp_def fun_map_def
+ using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def
by metis
subsection {* @{text Bex1_rel} quantifier *}
@@ -789,7 +782,7 @@
use "Tools/Quotient/quotient_info.ML"
-declare [[map "fun" = (fun_map, fun_rel)]]
+declare [[map "fun" = (map_fun, fun_rel)]]
lemmas [quot_thm] = fun_quotient
lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
@@ -800,7 +793,7 @@
text {* Lemmas about simplifying id's. *}
lemmas [id_simps] =
id_def[symmetric]
- fun_map_id
+ map_fun_id
id_apply
id_o
o_id
@@ -880,7 +873,7 @@
no_notation
rel_conj (infixr "OOO" 75) and
- fun_map (infixr "--->" 55) and
+ map_fun (infixr "--->" 55) and
fun_rel (infixr "===>" 55)
end
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Nov 18 12:37:30 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Nov 18 17:01:15 2010 +0100
@@ -383,7 +383,7 @@
=> resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
- (* observe fun_map *)
+ (* observe map_fun *)
| _ $ _ $ _
=> (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
ORELSE' rep_abs_rsp_tac ctxt
@@ -428,23 +428,23 @@
(*** Cleaning of the Theorem ***)
-(* expands all fun_maps, except in front of the (bound) variables listed in xs *)
-fun fun_map_simple_conv xs ctrm =
+(* expands all map_funs, except in front of the (bound) variables listed in xs *)
+fun map_fun_simple_conv xs ctrm =
case (term_of ctrm) of
- ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
+ ((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) =>
if member (op=) xs h
then Conv.all_conv ctrm
- else Conv.rewr_conv @{thm fun_map_apply [THEN eq_reflection]} ctrm
+ else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
| _ => Conv.all_conv ctrm
-fun fun_map_conv xs ctxt ctrm =
+fun map_fun_conv xs ctxt ctrm =
case (term_of ctrm) of
- _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
- fun_map_simple_conv xs) ctrm
- | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
+ _ $ _ => (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
+ map_fun_simple_conv xs) ctrm
+ | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
| _ => Conv.all_conv ctrm
-fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
+fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt)
(* custom matching functions *)
fun mk_abs u i t =
@@ -480,7 +480,7 @@
*)
fun lambda_prs_simple_conv ctxt ctrm =
case (term_of ctrm) of
- (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
+ (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
let
val thy = ProofContext.theory_of ctxt
val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
@@ -534,7 +534,7 @@
val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
in
- EVERY' [fun_map_tac lthy,
+ EVERY' [map_fun_tac lthy,
lambda_prs_tac lthy,
simp_tac ss,
TRY o rtac refl]