--- a/src/HOL/Bali/State.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Bali/State.thy Fri Nov 19 10:04:08 2010 +0100
@@ -631,11 +631,11 @@
definition
abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
- where "abupd f = prod_fun f id"
+ where "abupd f = map_pair f id"
definition
supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
- where "supd = prod_fun id"
+ where "supd = map_pair id"
lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
by (simp add: abupd_def)
--- a/src/HOL/Fun.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Fun.thy Fri Nov 19 10:04:08 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/Import/Generate-HOL/GenHOL4Base.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Nov 19 10:04:08 2010 +0100
@@ -131,7 +131,7 @@
SND > snd
CURRY > curry
UNCURRY > split
- "##" > prod_fun
+ "##" > map_pair
pair_case > split;
ignore_thms
--- a/src/HOL/Import/HOL/pair.imp Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Import/HOL/pair.imp Fri Nov 19 10:04:08 2010 +0100
@@ -18,7 +18,7 @@
"LEX" > "HOL4Base.pair.LEX"
"CURRY" > "Product_Type.curry"
"," > "Product_Type.Pair"
- "##" > "prod_fun"
+ "##" > "map_pair"
thm_maps
"pair_induction" > "Datatype.prod.induct_correctness"
@@ -39,7 +39,7 @@
"RPROD_DEF" > "HOL4Base.pair.RPROD_DEF"
"PFORALL_THM" > "HOL4Base.pair.PFORALL_THM"
"PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM"
- "PAIR_MAP_THM" > "Product_Type.prod_fun"
+ "PAIR_MAP_THM" > "Product_Type.map_pair"
"PAIR_MAP" > "HOL4Compat.PAIR_MAP"
"PAIR_EQ" > "Datatype.prod.simps_1"
"PAIR" > "HOL4Compat.PAIR"
--- a/src/HOL/Import/HOL4Compat.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Import/HOL4Compat.thy Fri Nov 19 10:04:08 2010 +0100
@@ -95,8 +95,8 @@
lemma PAIR: "(fst x,snd x) = x"
by simp
-lemma PAIR_MAP: "prod_fun f g p = (f (fst p),g (snd p))"
- by (simp add: prod_fun_def split_def)
+lemma PAIR_MAP: "map_pair f g p = (f (fst p),g (snd p))"
+ by (simp add: map_pair_def split_def)
lemma pair_case_def: "split = split"
..;
--- a/src/HOL/Library/Dlist.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Library/Dlist.thy Fri Nov 19 10:04:08 2010 +0100
@@ -173,6 +173,12 @@
qed
+section {* Functorial structure *}
+
+type_mapper map
+ by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
+
+
section {* Implementation of sets by distinct lists -- canonical! *}
definition Set :: "'a dlist \<Rightarrow> 'a fset" where
--- a/src/HOL/Library/Efficient_Nat.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Fri Nov 19 10:04:08 2010 +0100
@@ -51,8 +51,8 @@
unfolding of_nat_mult [symmetric] by simp
lemma divmod_nat_code [code]:
- "divmod_nat n m = prod_fun nat nat (pdivmod (of_nat n) (of_nat m))"
- by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
+ "divmod_nat n m = map_pair nat nat (pdivmod (of_nat n) (of_nat m))"
+ by (simp add: map_pair_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
lemma eq_nat_code [code]:
"HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"
--- a/src/HOL/Library/Fset.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Library/Fset.thy Fri Nov 19 10:04:08 2010 +0100
@@ -178,6 +178,9 @@
"map f (Set xs) = Set (remdups (List.map f xs))"
by (simp add: Set_def)
+type_mapper map
+ by (simp_all add: image_image)
+
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
[simp]: "filter P A = Fset (More_Set.project P (member A))"
--- a/src/HOL/Library/Mapping.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Library/Mapping.thy Fri Nov 19 10:04:08 2010 +0100
@@ -41,6 +41,19 @@
"delete k m = Mapping ((lookup m)(k := None))"
+subsection {* Functorial structure *}
+
+definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" where
+ "map f g m = Mapping (Option.map g \<circ> lookup m \<circ> f)"
+
+lemma lookup_map [simp]:
+ "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
+ by (simp add: map_def)
+
+type_mapper map
+ by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity)
+
+
subsection {* Derived operations *}
definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where
@@ -69,7 +82,7 @@
"map_default k v f m = map_entry k f (default k v m)"
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where
- "tabulate ks f = Mapping (map_of (map (\<lambda>k. (k, f k)) ks))"
+ "tabulate ks f = Mapping (map_of (List.map (\<lambda>k. (k, f k)) ks))"
definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" where
"bulkload xs = Mapping (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
@@ -294,6 +307,6 @@
hide_const (open) empty is_empty lookup update delete ordered_keys keys size
- replace default map_entry map_default tabulate bulkload
+ replace default map_entry map_default tabulate bulkload map
end
\ No newline at end of file
--- a/src/HOL/Library/Multiset.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Nov 19 10:04:08 2010 +0100
@@ -1627,6 +1627,14 @@
@{term "{#x+x|x:#M. x<c#}"}.
*}
+type_mapper image_mset proof -
+ fix f g A show "image_mset f (image_mset g A) = image_mset (\<lambda>x. f (g x)) A"
+ by (induct A) simp_all
+next
+ fix A show "image_mset (\<lambda>x. x) A = A"
+ by (induct A) simp_all
+qed
+
subsection {* Termination proofs with multiset orders *}
--- a/src/HOL/Library/Quotient_Product.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Library/Quotient_Product.thy Fri Nov 19 10:04:08 2010 +0100
@@ -13,7 +13,7 @@
where
"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-declare [[map prod = (prod_fun, prod_rel)]]
+declare [[map prod = (map_pair, prod_rel)]]
lemma prod_rel_apply [simp]:
"prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
@@ -34,7 +34,7 @@
lemma prod_quotient[quot_thm]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
- shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
+ shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
unfolding Quotient_def
apply(simp add: split_paired_all)
apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
@@ -53,7 +53,7 @@
lemma Pair_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
+ shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
apply(simp add: fun_eq_iff)
apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
done
@@ -67,7 +67,7 @@
lemma fst_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
+ shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
lemma snd_rsp[quot_respect]:
@@ -79,7 +79,7 @@
lemma snd_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
+ shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
lemma split_rsp[quot_respect]:
@@ -89,7 +89,7 @@
lemma split_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"
- shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
+ shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
lemma [quot_respect]:
@@ -101,7 +101,7 @@
assumes q1: "Quotient R1 abs1 rep1"
and q2: "Quotient R2 abs2 rep2"
shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
- prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel"
+ map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
lemma [quot_preserve]:
@@ -111,8 +111,8 @@
declare Pair_eq[quot_preserve]
-lemma prod_fun_id[id_simps]:
- shows "prod_fun id id = id"
+lemma map_pair_id[id_simps]:
+ shows "map_pair id id = id"
by (simp add: fun_eq_iff)
lemma prod_rel_eq[id_simps]:
--- a/src/HOL/Library/Quotient_Sum.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy Fri Nov 19 10:04:08 2010 +0100
@@ -16,12 +16,6 @@
| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
-primrec
- sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
-where
- "sum_map f1 f2 (Inl a) = Inl (f1 a)"
-| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
-
declare [[map sum = (sum_map, sum_rel)]]
--- a/src/HOL/Library/Quotient_Syntax.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Library/Quotient_Syntax.thy Fri Nov 19 10:04:08 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/Library/RBT.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Library/RBT.thy Fri Nov 19 10:04:08 2010 +0100
@@ -144,7 +144,7 @@
lemma lookup_map [simp]:
"lookup (map f t) k = Option.map (f k) (lookup t k)"
- by (simp add: map_def lookup_RBT lookup_map lookup_impl_of)
+ by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
lemma fold_fold:
"fold f t = More_List.fold (prod_case f) (entries t)"
--- a/src/HOL/List.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/List.thy Fri Nov 19 10:04:08 2010 +0100
@@ -881,6 +881,9 @@
"length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
by (induct rule:list_induct2, simp_all)
+type_mapper map
+ by simp_all
+
subsubsection {* @{text rev} *}
@@ -4300,7 +4303,7 @@
primrec -- {*The lexicographic ordering for lists of the specified length*}
lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
"lexn r 0 = {}"
- | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
+ | "lexn r (Suc n) = (map_pair (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
{(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
definition
@@ -4316,7 +4319,7 @@
apply (induct n, simp, simp)
apply(rule wf_subset)
prefer 2 apply (rule Int_lower1)
-apply(rule wf_prod_fun_image)
+apply(rule wf_map_pair_image)
prefer 2 apply (rule inj_onI, auto)
done
--- a/src/HOL/Option.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Option.thy Fri Nov 19 10:04:08 2010 +0100
@@ -81,6 +81,16 @@
"map f o sum_case g h = sum_case (map f o g) (map f o h)"
by (rule ext) (simp split: sum.split)
+type_mapper Option.map proof -
+ fix f g x
+ show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x"
+ by (cases x) simp_all
+next
+ fix x
+ show "Option.map (\<lambda>x. x) x = x"
+ by (cases x) simp_all
+qed
+
primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
bind_lzero: "bind None f = None" |
bind_lunit: "bind (Some x) f = f x"
--- a/src/HOL/Product_Type.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Product_Type.thy Fri Nov 19 10:04:08 2010 +0100
@@ -824,58 +824,63 @@
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
text {*
- @{term prod_fun} --- action of the product functor upon
+ @{term map_pair} --- action of the product functor upon
functions.
*}
-definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
- "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
+definition map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
+ "map_pair f g = (\<lambda>(x, y). (f x, g y))"
-lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
- by (simp add: prod_fun_def)
+lemma map_pair_simp [simp, code]:
+ "map_pair f g (a, b) = (f a, g b)"
+ by (simp add: map_pair_def)
-lemma fst_prod_fun[simp]: "fst (prod_fun f g x) = f (fst x)"
-by (cases x, auto)
+type_mapper map_pair
+ by (simp_all add: split_paired_all)
-lemma snd_prod_fun[simp]: "snd (prod_fun f g x) = g (snd x)"
-by (cases x, auto)
+lemma fst_map_pair [simp]:
+ "fst (map_pair f g x) = f (fst x)"
+ by (cases x) simp_all
-lemma fst_comp_prod_fun[simp]: "fst \<circ> prod_fun f g = f \<circ> fst"
-by (rule ext) auto
+lemma snd_prod_fun [simp]:
+ "snd (map_pair f g x) = g (snd x)"
+ by (cases x) simp_all
-lemma snd_comp_prod_fun[simp]: "snd \<circ> prod_fun f g = g \<circ> snd"
-by (rule ext) auto
-
+lemma fst_comp_map_pair [simp]:
+ "fst \<circ> map_pair f g = f \<circ> fst"
+ by (rule ext) simp_all
-lemma prod_fun_compose:
- "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
-by (rule ext) auto
+lemma snd_comp_map_pair [simp]:
+ "snd \<circ> map_pair f g = g \<circ> snd"
+ by (rule ext) simp_all
-lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
- by (rule ext) auto
+lemma map_pair_compose:
+ "map_pair (f1 o f2) (g1 o g2) = (map_pair f1 g1 o map_pair f2 g2)"
+ by (rule ext) (simp add: map_pair.compositionality comp_def)
-lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r"
- apply (rule image_eqI)
- apply (rule prod_fun [symmetric], assumption)
- done
+lemma map_pair_ident [simp]:
+ "map_pair (%x. x) (%y. y) = (%z. z)"
+ by (rule ext) (simp add: map_pair.identity)
+
+lemma map_pair_imageI [intro]:
+ "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_pair f g ` R"
+ by (rule image_eqI) simp_all
lemma prod_fun_imageE [elim!]:
- assumes major: "c: (prod_fun f g)`r"
- and cases: "!!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P"
+ assumes major: "c \<in> map_pair f g ` R"
+ and cases: "\<And>x y. c = (f x, g y) \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> P"
shows P
apply (rule major [THEN imageE])
apply (case_tac x)
apply (rule cases)
- apply (blast intro: prod_fun)
- apply blast
+ apply simp_all
done
-
definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
- "apfst f = prod_fun f id"
+ "apfst f = map_pair f id"
definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" where
- "apsnd f = prod_fun id f"
+ "apsnd f = map_pair id f"
lemma apfst_conv [simp, code]:
"apfst f (x, y) = (f x, y)"
@@ -941,7 +946,7 @@
Disjoint union of a family of sets -- Sigma.
*}
-definition Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
+definition Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
abbreviation
@@ -1091,66 +1096,6 @@
lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
by (auto, case_tac "f x", auto)
-text{* The following @{const prod_fun} lemmas are due to Joachim Breitner: *}
-
-lemma prod_fun_inj_on:
- assumes "inj_on f A" and "inj_on g B"
- shows "inj_on (prod_fun f g) (A \<times> B)"
-proof (rule inj_onI)
- fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
- assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
- assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
- assume "prod_fun f g x = prod_fun f g y"
- hence "fst (prod_fun f g x) = fst (prod_fun f g y)" by (auto)
- hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
- with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
- have "fst x = fst y" by (auto dest:dest:inj_onD)
- moreover from `prod_fun f g x = prod_fun f g y`
- have "snd (prod_fun f g x) = snd (prod_fun f g y)" by (auto)
- hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
- with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
- have "snd x = snd y" by (auto dest:dest:inj_onD)
- ultimately show "x = y" by(rule prod_eqI)
-qed
-
-lemma prod_fun_surj:
- assumes "surj f" and "surj g"
- shows "surj (prod_fun f g)"
-unfolding surj_def
-proof
- fix y :: "'b \<times> 'd"
- from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
- moreover
- from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
- ultimately have "(fst y, snd y) = prod_fun f g (a,b)" by auto
- thus "\<exists>x. y = prod_fun f g x" by auto
-qed
-
-lemma prod_fun_surj_on:
- assumes "f ` A = A'" and "g ` B = B'"
- shows "prod_fun f g ` (A \<times> B) = A' \<times> B'"
-unfolding image_def
-proof(rule set_eqI,rule iffI)
- fix x :: "'a \<times> 'c"
- assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = prod_fun f g x}"
- then obtain y where "y \<in> A \<times> B" and "x = prod_fun f g y" by blast
- from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
- moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
- ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
- with `x = prod_fun f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
-next
- fix x :: "'a \<times> 'c"
- assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
- from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
- then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
- moreover from `image g B = B'` and `snd x \<in> B'`
- obtain b where "b \<in> B" and "snd x = g b" by auto
- ultimately have "(fst x, snd x) = prod_fun f g (a,b)" by auto
- moreover from `a \<in> A` and `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
- ultimately have "\<exists>y \<in> A \<times> B. x = prod_fun f g y" by auto
- thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = prod_fun f g y}" by auto
-qed
-
lemma swap_inj_on:
"inj_on (\<lambda>(i, j). (j, i)) A"
by (auto intro!: inj_onI)
@@ -1167,6 +1112,66 @@
using * eq[symmetric] by auto
qed simp_all
+text {* The following @{const map_pair} lemmas are due to Joachim Breitner: *}
+
+lemma map_pair_inj_on:
+ assumes "inj_on f A" and "inj_on g B"
+ shows "inj_on (map_pair f g) (A \<times> B)"
+proof (rule inj_onI)
+ fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
+ assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
+ assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
+ assume "map_pair f g x = map_pair f g y"
+ hence "fst (map_pair f g x) = fst (map_pair f g y)" by (auto)
+ hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
+ with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
+ have "fst x = fst y" by (auto dest:dest:inj_onD)
+ moreover from `map_pair f g x = map_pair f g y`
+ have "snd (map_pair f g x) = snd (map_pair f g y)" by (auto)
+ hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
+ with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
+ have "snd x = snd y" by (auto dest:dest:inj_onD)
+ ultimately show "x = y" by(rule prod_eqI)
+qed
+
+lemma map_pair_surj:
+ assumes "surj f" and "surj g"
+ shows "surj (map_pair f g)"
+unfolding surj_def
+proof
+ fix y :: "'b \<times> 'd"
+ from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
+ moreover
+ from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
+ ultimately have "(fst y, snd y) = map_pair f g (a,b)" by auto
+ thus "\<exists>x. y = map_pair f g x" by auto
+qed
+
+lemma map_pair_surj_on:
+ assumes "f ` A = A'" and "g ` B = B'"
+ shows "map_pair f g ` (A \<times> B) = A' \<times> B'"
+unfolding image_def
+proof(rule set_eqI,rule iffI)
+ fix x :: "'a \<times> 'c"
+ assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = map_pair f g x}"
+ then obtain y where "y \<in> A \<times> B" and "x = map_pair f g y" by blast
+ from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
+ moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
+ ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
+ with `x = map_pair f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
+next
+ fix x :: "'a \<times> 'c"
+ assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
+ from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
+ then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
+ moreover from `image g B = B'` and `snd x \<in> B'`
+ obtain b where "b \<in> B" and "snd x = g b" by auto
+ ultimately have "(fst x, snd x) = map_pair f g (a,b)" by auto
+ moreover from `a \<in> A` and `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
+ ultimately have "\<exists>y \<in> A \<times> B. x = map_pair f g y" by auto
+ thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_pair f g y}" by auto
+qed
+
subsection {* Inductively defined sets *}
--- a/src/HOL/Quotient.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Quotient.thy Fri Nov 19 10:04:08 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/Sum_Type.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Sum_Type.thy Fri Nov 19 10:04:08 2010 +0100
@@ -91,6 +91,20 @@
then show "P s" by (auto intro: sumE [of s])
qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
+primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
+ "sum_map f1 f2 (Inl a) = Inl (f1 a)"
+| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
+
+type_mapper sum_map proof -
+ fix f g h i s
+ show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s"
+ by (cases s) simp_all
+next
+ fix s
+ show "sum_map (\<lambda>x. x) (\<lambda>x. x) s = s"
+ by (cases s) simp_all
+qed
+
subsection {* Projections *}
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Nov 19 10:04:08 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]
--- a/src/HOL/Tools/functorial_mappers.ML Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Tools/functorial_mappers.ML Fri Nov 19 10:04:08 2010 +0100
@@ -17,7 +17,7 @@
structure Functorial_Mappers : FUNCTORIAL_MAPPERS =
struct
-val concatenateN = "concatenate";
+val compositionalityN = "compositionality";
val identityN = "identity";
(** functorial mappers and their properties **)
@@ -25,7 +25,7 @@
(* bookkeeping *)
type entry = { mapper: string, variances: (sort * (bool * bool)) list,
- concatenate: thm, identity: thm };
+ compositionality: thm, identity: thm };
structure Data = Theory_Data(
type T = entry Symtab.table
@@ -74,7 +74,7 @@
(* mapper properties *)
-fun make_concatenate_prop variances (tyco, mapper) =
+fun make_compositionality_prop variances (tyco, mapper) =
let
fun invents n k nctxt =
let
@@ -186,23 +186,23 @@
of [tyco] => tyco
| _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
val variances = analyze_variances thy tyco T;
- val concatenate_prop = uncurry (fold_rev Logic.all)
- (make_concatenate_prop variances (tyco, mapper));
+ val compositionality_prop = uncurry (fold_rev Logic.all)
+ (make_compositionality_prop variances (tyco, mapper));
val identity_prop = uncurry Logic.all
(make_identity_prop variances (tyco, mapper));
val qualify = Binding.qualify true (Long_Name.base_name mapper) o Binding.name;
- fun after_qed [single_concatenate, single_identity] lthy =
+ fun after_qed [single_compositionality, single_identity] lthy =
lthy
- |> Local_Theory.note ((qualify concatenateN, []), single_concatenate)
+ |> Local_Theory.note ((qualify compositionalityN, []), single_compositionality)
||>> Local_Theory.note ((qualify identityN, []), single_identity)
- |-> (fn ((_, [concatenate]), (_, [identity])) =>
+ |-> (fn ((_, [compositionality]), (_, [identity])) =>
(Local_Theory.background_theory o Data.map)
(Symtab.update (tyco, { mapper = mapper, variances = variances,
- concatenate = concatenate, identity = identity })));
+ compositionality = compositionality, identity = identity })));
in
thy
|> Named_Target.theory_init
- |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [concatenate_prop, identity_prop])
+ |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
end
val type_mapper = gen_type_mapper Sign.cert_term;
--- a/src/HOL/Wellfounded.thy Thu Nov 18 22:34:32 2010 +0100
+++ b/src/HOL/Wellfounded.thy Fri Nov 19 10:04:08 2010 +0100
@@ -240,7 +240,7 @@
text{*Well-foundedness of image*}
-lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
+lemma wf_map_pair_image: "[| wf r; inj f |] ==> wf(map_pair f f ` r)"
apply (simp only: wf_eq_minimal, clarify)
apply (case_tac "EX p. f p : Q")
apply (erule_tac x = "{p. f p : Q}" in allE)