author haftmann Thu, 18 Nov 2010 17:01:15 +0100 changeset 40602 91e583511113 parent 40598 16742772a9b3 child 40603 963ee2331d20
map_fun combinator in theory Fun
 src/HOL/Fun.thy file | annotate | diff | comparison | revisions src/HOL/Library/Quotient_Syntax.thy file | annotate | diff | comparison | revisions src/HOL/Quotient.thy file | annotate | diff | comparison | revisions src/HOL/Tools/Quotient/quotient_tacs.ML file | annotate | diff | comparison | revisions
```--- 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]```