map_fun combinator in theory Fun
authorhaftmann
Thu Nov 18 17:01:15 2010 +0100 (2010-11-18)
changeset 4060291e583511113
parent 40598 16742772a9b3
child 40603 963ee2331d20
map_fun combinator in theory Fun
src/HOL/Fun.thy
src/HOL/Library/Quotient_Syntax.thy
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_tacs.ML
     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]