# HG changeset patch # User haftmann # Date 1290157448 -3600 # Node ID 23626b388e0715356a24cfb68ea2dc6c4b416358 # Parent 021278fdd0a8e98a557f177a292b4544021145d9# Parent 7ae5b89d89134307c9c1876c88f11e4a16a0b385 merged diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Bali/State.thy --- 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 \ abopt) \ state \ state" - where "abupd f = prod_fun f id" + where "abupd f = map_pair f id" definition supd :: "(st \ st) \ state \ 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) diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Fun.thy --- 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 "\>" 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 021278fdd0a8 -r 23626b388e07 src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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 diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Import/HOL/pair.imp --- 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" diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Import/HOL4Compat.thy --- 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" ..; diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Library/Dlist.thy --- 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 \ 'a fset" where diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Library/Efficient_Nat.thy --- 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 \ HOL.equal (of_nat n \ int) (of_nat m)" diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Library/Fset.thy --- 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 \ bool) \ 'a fset \ 'a fset" where [simp]: "filter P A = Fset (More_Set.project P (member A))" diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Library/Mapping.thy --- 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 \ 'a) \ ('b \ 'd) \ ('a, 'b) mapping \ ('c, 'd) mapping" where + "map f g m = Mapping (Option.map g \ lookup m \ f)" + +lemma lookup_map [simp]: + "lookup (map f g m) = Option.map g \ lookup m \ 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 \ '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 \ ('a \ 'b) \ ('a, 'b) mapping" where - "tabulate ks f = Mapping (map_of (map (\k. (k, f k)) ks))" + "tabulate ks f = Mapping (map_of (List.map (\k. (k, f k)) ks))" definition bulkload :: "'a list \ (nat, 'a) mapping" where "bulkload xs = Mapping (\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 diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Library/Multiset.thy --- 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. xx. f (g x)) A" + by (induct A) simp_all +next + fix A show "image_mset (\x. x) A = A" + by (induct A) simp_all +qed + subsection {* Termination proofs with multiset orders *} diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Library/Quotient_Product.thy --- 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 = (\(a, b) (c, d). R1 a c \ 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) \ R1 a c \ 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]: diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Library/Quotient_Sum.thy --- 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 \ 'c) \ ('b \ 'd) \ 'a + 'b \ '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)]] diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Library/Quotient_Syntax.thy --- 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 diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Library/RBT.thy --- 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)" diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/List.thy --- 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 \ 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 \ 'a) set \ nat \ ('a list \ '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 \ 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 diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Option.thy --- 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 (\x. f (g x)) x" + by (cases x) simp_all +next + fix x + show "Option.map (\x. x) x = x" + by (cases x) simp_all +qed + primrec bind :: "'a option \ ('a \ 'b option) \ 'b option" where bind_lzero: "bind None f = None" | bind_lunit: "bind (Some x) f = f x" diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Product_Type.thy --- 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 "\\" 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 \ 'c) \ ('b \ 'd) \ 'a \ 'b \ 'c \ 'd" where - "prod_fun f g = (\(x, y). (f x, g y))" +definition map_pair :: "('a \ 'c) \ ('b \ 'd) \ 'a \ 'b \ 'c \ 'd" where + "map_pair f g = (\(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 \ prod_fun f g = f \ 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 \ prod_fun f g = g \ snd" -by (rule ext) auto - +lemma fst_comp_map_pair [simp]: + "fst \ map_pair f g = f \ 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 \ map_pair f g = g \ 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) \ R \ (f a, g b) \ 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 \ map_pair f g ` R" + and cases: "\x y. c = (f x, g y) \ (x, y) \ R \ 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 \ 'c) \ 'a \ 'b \ 'c \ 'b" where - "apfst f = prod_fun f id" + "apfst f = map_pair f id" definition apsnd :: "('b \ 'c) \ 'a \ 'b \ 'a \ '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 \ 'b) set" where +definition Sigma :: "['a set, 'a => 'b set] => ('a \ '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 \ B) = ((fst \ f) -` A) \ ((snd \ 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 \ B)" -proof (rule inj_onI) - fix x :: "'a \ 'c" and y :: "'a \ 'c" - assume "x \ A \ B" hence "fst x \ A" and "snd x \ B" by auto - assume "y \ A \ B" hence "fst y \ A" and "snd y \ 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 \ A` and `fst y \ 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 \ B` and `snd y \ 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 \ '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 "\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 \ B) = A' \ B'" -unfolding image_def -proof(rule set_eqI,rule iffI) - fix x :: "'a \ 'c" - assume "x \ {y\'a \ 'c. \x\'b \ 'd\A \ B. y = prod_fun f g x}" - then obtain y where "y \ A \ B" and "x = prod_fun f g y" by blast - from `image f A = A'` and `y \ A \ B` have "f (fst y) \ A'" by auto - moreover from `image g B = B'` and `y \ A \ B` have "g (snd y) \ B'" by auto - ultimately have "(f (fst y), g (snd y)) \ (A' \ B')" by auto - with `x = prod_fun f g y` show "x \ A' \ B'" by (cases y, auto) -next - fix x :: "'a \ 'c" - assume "x \ A' \ B'" hence "fst x \ A'" and "snd x \ B'" by auto - from `image f A = A'` and `fst x \ A'` have "fst x \ image f A" by auto - then obtain a where "a \ A" and "fst x = f a" by (rule imageE) - moreover from `image g B = B'` and `snd x \ B'` - obtain b where "b \ 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 \ A` and `b \ B` have "(a , b) \ A \ B" by auto - ultimately have "\y \ A \ B. x = prod_fun f g y" by auto - thus "x \ {x. \y \ A \ B. x = prod_fun f g y}" by auto -qed - lemma swap_inj_on: "inj_on (\(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 \ B)" +proof (rule inj_onI) + fix x :: "'a \ 'c" and y :: "'a \ 'c" + assume "x \ A \ B" hence "fst x \ A" and "snd x \ B" by auto + assume "y \ A \ B" hence "fst y \ A" and "snd y \ 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 \ A` and `fst y \ 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 \ B` and `snd y \ 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 \ '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 "\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 \ B) = A' \ B'" +unfolding image_def +proof(rule set_eqI,rule iffI) + fix x :: "'a \ 'c" + assume "x \ {y\'a \ 'c. \x\'b \ 'd\A \ B. y = map_pair f g x}" + then obtain y where "y \ A \ B" and "x = map_pair f g y" by blast + from `image f A = A'` and `y \ A \ B` have "f (fst y) \ A'" by auto + moreover from `image g B = B'` and `y \ A \ B` have "g (snd y) \ B'" by auto + ultimately have "(f (fst y), g (snd y)) \ (A' \ B')" by auto + with `x = map_pair f g y` show "x \ A' \ B'" by (cases y, auto) +next + fix x :: "'a \ 'c" + assume "x \ A' \ B'" hence "fst x \ A'" and "snd x \ B'" by auto + from `image f A = A'` and `fst x \ A'` have "fst x \ image f A" by auto + then obtain a where "a \ A" and "fst x = f a" by (rule imageE) + moreover from `image g B = B'` and `snd x \ B'` + obtain b where "b \ 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 \ A` and `b \ B` have "(a , b) \ A \ B" by auto + ultimately have "\y \ A \ B. x = map_pair f g y" by auto + thus "x \ {x. \y \ A \ B. x = map_pair f g y}" by auto +qed + subsection {* Inductively defined sets *} diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Quotient.thy --- 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 \ '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 021278fdd0a8 -r 23626b388e07 src/HOL/Sum_Type.thy --- 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 \ 'c) \ ('b \ 'd) \ 'a + 'b \ '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 (\x. f (h x)) (\x. g (i x)) s" + by (cases s) simp_all +next + fix s + show "sum_map (\x. x) (\x. x) s = s" + by (cases s) simp_all +qed + subsection {* Projections *} diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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] diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Tools/functorial_mappers.ML --- 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; diff -r 021278fdd0a8 -r 23626b388e07 src/HOL/Wellfounded.thy --- 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)