author haftmann Thu Nov 18 17:01:15 2010 +0100 (2010-11-18) changeset 40602 91e583511113 parent 40598 16742772a9b3 child 40603 963ee2331d20
map_fun combinator in theory Fun
 src/HOL/Fun.thy file | annotate | diff | revisions src/HOL/Library/Quotient_Syntax.thy file | annotate | diff | revisions src/HOL/Quotient.thy file | annotate | diff | revisions src/HOL/Tools/Quotient/quotient_tacs.ML file | annotate | diff | revisions
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.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.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.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.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.5  subsection {* Function map and function relation *}
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.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.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.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.40  subsection {* @{text Bex1_rel} quantifier *}
3.41 @@ -789,7 +782,7 @@
3.43  use "Tools/Quotient/quotient_info.ML"
3.45 -declare [[map "fun" = (fun_map, fun_rel)]]
3.46 +declare [[map "fun" = (map_fun, fun_rel)]]
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.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.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.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.14  (*** Cleaning of the Theorem ***)
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.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.40 -fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
4.41 +fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt)
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 @@