# HG changeset patch # User haftmann # Date 1290096075 -3600 # Node ID 91e58351111382a9af182c1bc06fb9f8406704f2 # Parent 16742772a9b37a00285acd1e24a161198ef31f04 map_fun combinator in theory Fun diff -r 16742772a9b3 -r 91e583511113 src/HOL/Fun.thy --- 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 "\>" 60) +subsection {* Mapping functions *} + +definition map_fun :: "('c \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd" where + "map_fun f g h = g \ h \ 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 \ 'b) \ 'a set \ bool" where -- "injective" diff -r 16742772a9b3 -r 91e583511113 src/HOL/Library/Quotient_Syntax.thy --- 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 diff -r 16742772a9b3 -r 91e583511113 src/HOL/Quotient.thy --- 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 \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd" (infixr "--->" 55) -where - "fun_map f g = (\h. g \ h \ 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 \ 'a \ bool) \ ('b \ 'b \ bool) \ ('a \ 'b) \ ('a \ 'b) \ 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 diff -r 16742772a9b3 -r 91e583511113 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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]