merged
authorhaftmann
Fri Nov 19 10:04:08 2010 +0100 (2010-11-19)
changeset 4061323626b388e07
parent 40601 021278fdd0a8
parent 40612 7ae5b89d8913
child 40614 d6eeffa0d9a0
merged
     1.1 --- a/src/HOL/Bali/State.thy	Thu Nov 18 22:34:32 2010 +0100
     1.2 +++ b/src/HOL/Bali/State.thy	Fri Nov 19 10:04:08 2010 +0100
     1.3 @@ -631,11 +631,11 @@
     1.4  
     1.5  definition
     1.6    abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
     1.7 -  where "abupd f = prod_fun f id"
     1.8 +  where "abupd f = map_pair f id"
     1.9  
    1.10  definition
    1.11    supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
    1.12 -  where "supd = prod_fun id"
    1.13 +  where "supd = map_pair id"
    1.14    
    1.15  lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
    1.16  by (simp add: abupd_def)
     2.1 --- a/src/HOL/Fun.thy	Thu Nov 18 22:34:32 2010 +0100
     2.2 +++ b/src/HOL/Fun.thy	Fri Nov 19 10:04:08 2010 +0100
     2.3 @@ -117,6 +117,19 @@
     2.4  no_notation fcomp (infixl "\<circ>>" 60)
     2.5  
     2.6  
     2.7 +subsection {* Mapping functions *}
     2.8 +
     2.9 +definition map_fun :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" where
    2.10 +  "map_fun f g h = g \<circ> h \<circ> f"
    2.11 +
    2.12 +lemma map_fun_apply [simp]:
    2.13 +  "map_fun f g h x = g (h (f x))"
    2.14 +  by (simp add: map_fun_def)
    2.15 +
    2.16 +type_mapper map_fun
    2.17 +  by (simp_all add: fun_eq_iff)
    2.18 +
    2.19 +
    2.20  subsection {* Injectivity, Surjectivity and Bijectivity *}
    2.21  
    2.22  definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
     3.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Nov 18 22:34:32 2010 +0100
     3.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Nov 19 10:04:08 2010 +0100
     3.3 @@ -131,7 +131,7 @@
     3.4      SND       > snd
     3.5      CURRY     > curry
     3.6      UNCURRY   > split
     3.7 -    "##"      > prod_fun
     3.8 +    "##"      > map_pair
     3.9      pair_case > split;
    3.10  
    3.11  ignore_thms
     4.1 --- a/src/HOL/Import/HOL/pair.imp	Thu Nov 18 22:34:32 2010 +0100
     4.2 +++ b/src/HOL/Import/HOL/pair.imp	Fri Nov 19 10:04:08 2010 +0100
     4.3 @@ -18,7 +18,7 @@
     4.4    "LEX" > "HOL4Base.pair.LEX"
     4.5    "CURRY" > "Product_Type.curry"
     4.6    "," > "Product_Type.Pair"
     4.7 -  "##" > "prod_fun"
     4.8 +  "##" > "map_pair"
     4.9  
    4.10  thm_maps
    4.11    "pair_induction" > "Datatype.prod.induct_correctness"
    4.12 @@ -39,7 +39,7 @@
    4.13    "RPROD_DEF" > "HOL4Base.pair.RPROD_DEF"
    4.14    "PFORALL_THM" > "HOL4Base.pair.PFORALL_THM"
    4.15    "PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM"
    4.16 -  "PAIR_MAP_THM" > "Product_Type.prod_fun"
    4.17 +  "PAIR_MAP_THM" > "Product_Type.map_pair"
    4.18    "PAIR_MAP" > "HOL4Compat.PAIR_MAP"
    4.19    "PAIR_EQ" > "Datatype.prod.simps_1"
    4.20    "PAIR" > "HOL4Compat.PAIR"
     5.1 --- a/src/HOL/Import/HOL4Compat.thy	Thu Nov 18 22:34:32 2010 +0100
     5.2 +++ b/src/HOL/Import/HOL4Compat.thy	Fri Nov 19 10:04:08 2010 +0100
     5.3 @@ -95,8 +95,8 @@
     5.4  lemma PAIR: "(fst x,snd x) = x"
     5.5    by simp
     5.6  
     5.7 -lemma PAIR_MAP: "prod_fun f g p = (f (fst p),g (snd p))"
     5.8 -  by (simp add: prod_fun_def split_def)
     5.9 +lemma PAIR_MAP: "map_pair f g p = (f (fst p),g (snd p))"
    5.10 +  by (simp add: map_pair_def split_def)
    5.11  
    5.12  lemma pair_case_def: "split = split"
    5.13    ..;
     6.1 --- a/src/HOL/Library/Dlist.thy	Thu Nov 18 22:34:32 2010 +0100
     6.2 +++ b/src/HOL/Library/Dlist.thy	Fri Nov 19 10:04:08 2010 +0100
     6.3 @@ -173,6 +173,12 @@
     6.4  qed
     6.5  
     6.6  
     6.7 +section {* Functorial structure *}
     6.8 +
     6.9 +type_mapper map
    6.10 +  by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
    6.11 +
    6.12 +
    6.13  section {* Implementation of sets by distinct lists -- canonical! *}
    6.14  
    6.15  definition Set :: "'a dlist \<Rightarrow> 'a fset" where
     7.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Nov 18 22:34:32 2010 +0100
     7.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Nov 19 10:04:08 2010 +0100
     7.3 @@ -51,8 +51,8 @@
     7.4    unfolding of_nat_mult [symmetric] by simp
     7.5  
     7.6  lemma divmod_nat_code [code]:
     7.7 -  "divmod_nat n m = prod_fun nat nat (pdivmod (of_nat n) (of_nat m))"
     7.8 -  by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
     7.9 +  "divmod_nat n m = map_pair nat nat (pdivmod (of_nat n) (of_nat m))"
    7.10 +  by (simp add: map_pair_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
    7.11  
    7.12  lemma eq_nat_code [code]:
    7.13    "HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"
     8.1 --- a/src/HOL/Library/Fset.thy	Thu Nov 18 22:34:32 2010 +0100
     8.2 +++ b/src/HOL/Library/Fset.thy	Fri Nov 19 10:04:08 2010 +0100
     8.3 @@ -178,6 +178,9 @@
     8.4    "map f (Set xs) = Set (remdups (List.map f xs))"
     8.5    by (simp add: Set_def)
     8.6  
     8.7 +type_mapper map
     8.8 +  by (simp_all add: image_image)
     8.9 +
    8.10  definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    8.11    [simp]: "filter P A = Fset (More_Set.project P (member A))"
    8.12  
     9.1 --- a/src/HOL/Library/Mapping.thy	Thu Nov 18 22:34:32 2010 +0100
     9.2 +++ b/src/HOL/Library/Mapping.thy	Fri Nov 19 10:04:08 2010 +0100
     9.3 @@ -41,6 +41,19 @@
     9.4    "delete k m = Mapping ((lookup m)(k := None))"
     9.5  
     9.6  
     9.7 +subsection {* Functorial structure *}
     9.8 +
     9.9 +definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" where
    9.10 +  "map f g m = Mapping (Option.map g \<circ> lookup m \<circ> f)"
    9.11 +
    9.12 +lemma lookup_map [simp]:
    9.13 +  "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
    9.14 +  by (simp add: map_def)
    9.15 +
    9.16 +type_mapper map
    9.17 +  by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity)
    9.18 +
    9.19 +
    9.20  subsection {* Derived operations *}
    9.21  
    9.22  definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where
    9.23 @@ -69,7 +82,7 @@
    9.24    "map_default k v f m = map_entry k f (default k v m)" 
    9.25  
    9.26  definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where
    9.27 -  "tabulate ks f = Mapping (map_of (map (\<lambda>k. (k, f k)) ks))"
    9.28 +  "tabulate ks f = Mapping (map_of (List.map (\<lambda>k. (k, f k)) ks))"
    9.29  
    9.30  definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" where
    9.31    "bulkload xs = Mapping (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
    9.32 @@ -294,6 +307,6 @@
    9.33  
    9.34  
    9.35  hide_const (open) empty is_empty lookup update delete ordered_keys keys size
    9.36 -  replace default map_entry map_default tabulate bulkload
    9.37 +  replace default map_entry map_default tabulate bulkload map
    9.38  
    9.39  end
    9.40 \ No newline at end of file
    10.1 --- a/src/HOL/Library/Multiset.thy	Thu Nov 18 22:34:32 2010 +0100
    10.2 +++ b/src/HOL/Library/Multiset.thy	Fri Nov 19 10:04:08 2010 +0100
    10.3 @@ -1627,6 +1627,14 @@
    10.4    @{term "{#x+x|x:#M. x<c#}"}.
    10.5  *}
    10.6  
    10.7 +type_mapper image_mset proof -
    10.8 +  fix f g A show "image_mset f (image_mset g A) = image_mset (\<lambda>x. f (g x)) A"
    10.9 +    by (induct A) simp_all
   10.10 +next
   10.11 +  fix A show "image_mset (\<lambda>x. x) A = A"
   10.12 +    by (induct A) simp_all
   10.13 +qed
   10.14 +
   10.15  
   10.16  subsection {* Termination proofs with multiset orders *}
   10.17  
    11.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu Nov 18 22:34:32 2010 +0100
    11.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Nov 19 10:04:08 2010 +0100
    11.3 @@ -13,7 +13,7 @@
    11.4  where
    11.5    "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    11.6  
    11.7 -declare [[map prod = (prod_fun, prod_rel)]]
    11.8 +declare [[map prod = (map_pair, prod_rel)]]
    11.9  
   11.10  lemma prod_rel_apply [simp]:
   11.11    "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
   11.12 @@ -34,7 +34,7 @@
   11.13  lemma prod_quotient[quot_thm]:
   11.14    assumes q1: "Quotient R1 Abs1 Rep1"
   11.15    assumes q2: "Quotient R2 Abs2 Rep2"
   11.16 -  shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
   11.17 +  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
   11.18    unfolding Quotient_def
   11.19    apply(simp add: split_paired_all)
   11.20    apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
   11.21 @@ -53,7 +53,7 @@
   11.22  lemma Pair_prs[quot_preserve]:
   11.23    assumes q1: "Quotient R1 Abs1 Rep1"
   11.24    assumes q2: "Quotient R2 Abs2 Rep2"
   11.25 -  shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
   11.26 +  shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
   11.27    apply(simp add: fun_eq_iff)
   11.28    apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   11.29    done
   11.30 @@ -67,7 +67,7 @@
   11.31  lemma fst_prs[quot_preserve]:
   11.32    assumes q1: "Quotient R1 Abs1 Rep1"
   11.33    assumes q2: "Quotient R2 Abs2 Rep2"
   11.34 -  shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
   11.35 +  shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
   11.36    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
   11.37  
   11.38  lemma snd_rsp[quot_respect]:
   11.39 @@ -79,7 +79,7 @@
   11.40  lemma snd_prs[quot_preserve]:
   11.41    assumes q1: "Quotient R1 Abs1 Rep1"
   11.42    assumes q2: "Quotient R2 Abs2 Rep2"
   11.43 -  shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
   11.44 +  shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
   11.45    by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
   11.46  
   11.47  lemma split_rsp[quot_respect]:
   11.48 @@ -89,7 +89,7 @@
   11.49  lemma split_prs[quot_preserve]:
   11.50    assumes q1: "Quotient R1 Abs1 Rep1"
   11.51    and     q2: "Quotient R2 Abs2 Rep2"
   11.52 -  shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
   11.53 +  shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
   11.54    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   11.55  
   11.56  lemma [quot_respect]:
   11.57 @@ -101,7 +101,7 @@
   11.58    assumes q1: "Quotient R1 abs1 rep1"
   11.59    and     q2: "Quotient R2 abs2 rep2"
   11.60    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
   11.61 -  prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel"
   11.62 +  map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
   11.63    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   11.64  
   11.65  lemma [quot_preserve]:
   11.66 @@ -111,8 +111,8 @@
   11.67  
   11.68  declare Pair_eq[quot_preserve]
   11.69  
   11.70 -lemma prod_fun_id[id_simps]:
   11.71 -  shows "prod_fun id id = id"
   11.72 +lemma map_pair_id[id_simps]:
   11.73 +  shows "map_pair id id = id"
   11.74    by (simp add: fun_eq_iff)
   11.75  
   11.76  lemma prod_rel_eq[id_simps]:
    12.1 --- a/src/HOL/Library/Quotient_Sum.thy	Thu Nov 18 22:34:32 2010 +0100
    12.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Nov 19 10:04:08 2010 +0100
    12.3 @@ -16,12 +16,6 @@
    12.4  | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    12.5  | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    12.6  
    12.7 -primrec
    12.8 -  sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
    12.9 -where
   12.10 -  "sum_map f1 f2 (Inl a) = Inl (f1 a)"
   12.11 -| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
   12.12 -
   12.13  declare [[map sum = (sum_map, sum_rel)]]
   12.14  
   12.15  
    13.1 --- a/src/HOL/Library/Quotient_Syntax.thy	Thu Nov 18 22:34:32 2010 +0100
    13.2 +++ b/src/HOL/Library/Quotient_Syntax.thy	Fri Nov 19 10:04:08 2010 +0100
    13.3 @@ -10,7 +10,7 @@
    13.4  
    13.5  notation
    13.6    rel_conj (infixr "OOO" 75) and
    13.7 -  fun_map (infixr "--->" 55) and
    13.8 +  map_fun (infixr "--->" 55) and
    13.9    fun_rel (infixr "===>" 55)
   13.10  
   13.11  end
    14.1 --- a/src/HOL/Library/RBT.thy	Thu Nov 18 22:34:32 2010 +0100
    14.2 +++ b/src/HOL/Library/RBT.thy	Fri Nov 19 10:04:08 2010 +0100
    14.3 @@ -144,7 +144,7 @@
    14.4  
    14.5  lemma lookup_map [simp]:
    14.6    "lookup (map f t) k = Option.map (f k) (lookup t k)"
    14.7 -  by (simp add: map_def lookup_RBT lookup_map lookup_impl_of)
    14.8 +  by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
    14.9  
   14.10  lemma fold_fold:
   14.11    "fold f t = More_List.fold (prod_case f) (entries t)"
    15.1 --- a/src/HOL/List.thy	Thu Nov 18 22:34:32 2010 +0100
    15.2 +++ b/src/HOL/List.thy	Fri Nov 19 10:04:08 2010 +0100
    15.3 @@ -881,6 +881,9 @@
    15.4    "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
    15.5  by (induct rule:list_induct2, simp_all)
    15.6  
    15.7 +type_mapper map
    15.8 +  by simp_all
    15.9 +
   15.10  
   15.11  subsubsection {* @{text rev} *}
   15.12  
   15.13 @@ -4300,7 +4303,7 @@
   15.14  primrec -- {*The lexicographic ordering for lists of the specified length*}
   15.15    lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
   15.16      "lexn r 0 = {}"
   15.17 -  | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
   15.18 +  | "lexn r (Suc n) = (map_pair (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
   15.19        {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
   15.20  
   15.21  definition
   15.22 @@ -4316,7 +4319,7 @@
   15.23  apply (induct n, simp, simp)
   15.24  apply(rule wf_subset)
   15.25   prefer 2 apply (rule Int_lower1)
   15.26 -apply(rule wf_prod_fun_image)
   15.27 +apply(rule wf_map_pair_image)
   15.28   prefer 2 apply (rule inj_onI, auto)
   15.29  done
   15.30  
    16.1 --- a/src/HOL/Option.thy	Thu Nov 18 22:34:32 2010 +0100
    16.2 +++ b/src/HOL/Option.thy	Fri Nov 19 10:04:08 2010 +0100
    16.3 @@ -81,6 +81,16 @@
    16.4      "map f o sum_case g h = sum_case (map f o g) (map f o h)"
    16.5    by (rule ext) (simp split: sum.split)
    16.6  
    16.7 +type_mapper Option.map proof -
    16.8 +  fix f g x
    16.9 +  show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x"
   16.10 +    by (cases x) simp_all
   16.11 +next
   16.12 +  fix x
   16.13 +  show "Option.map (\<lambda>x. x) x = x"
   16.14 +    by (cases x) simp_all
   16.15 +qed
   16.16 +
   16.17  primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
   16.18  bind_lzero: "bind None f = None" |
   16.19  bind_lunit: "bind (Some x) f = f x"
    17.1 --- a/src/HOL/Product_Type.thy	Thu Nov 18 22:34:32 2010 +0100
    17.2 +++ b/src/HOL/Product_Type.thy	Fri Nov 19 10:04:08 2010 +0100
    17.3 @@ -824,58 +824,63 @@
    17.4  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    17.5  
    17.6  text {*
    17.7 -  @{term prod_fun} --- action of the product functor upon
    17.8 +  @{term map_pair} --- action of the product functor upon
    17.9    functions.
   17.10  *}
   17.11  
   17.12 -definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
   17.13 -  "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
   17.14 +definition map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
   17.15 +  "map_pair f g = (\<lambda>(x, y). (f x, g y))"
   17.16  
   17.17 -lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
   17.18 -  by (simp add: prod_fun_def)
   17.19 +lemma map_pair_simp [simp, code]:
   17.20 +  "map_pair f g (a, b) = (f a, g b)"
   17.21 +  by (simp add: map_pair_def)
   17.22  
   17.23 -lemma fst_prod_fun[simp]: "fst (prod_fun f g x) = f (fst x)"
   17.24 -by (cases x, auto)
   17.25 +type_mapper map_pair
   17.26 +  by (simp_all add: split_paired_all)
   17.27  
   17.28 -lemma snd_prod_fun[simp]: "snd (prod_fun f g x) = g (snd x)"
   17.29 -by (cases x, auto)
   17.30 +lemma fst_map_pair [simp]:
   17.31 +  "fst (map_pair f g x) = f (fst x)"
   17.32 +  by (cases x) simp_all
   17.33  
   17.34 -lemma fst_comp_prod_fun[simp]: "fst \<circ> prod_fun f g = f \<circ> fst"
   17.35 -by (rule ext) auto
   17.36 +lemma snd_prod_fun [simp]:
   17.37 +  "snd (map_pair f g x) = g (snd x)"
   17.38 +  by (cases x) simp_all
   17.39  
   17.40 -lemma snd_comp_prod_fun[simp]: "snd \<circ> prod_fun f g = g \<circ> snd"
   17.41 -by (rule ext) auto
   17.42 -
   17.43 +lemma fst_comp_map_pair [simp]:
   17.44 +  "fst \<circ> map_pair f g = f \<circ> fst"
   17.45 +  by (rule ext) simp_all
   17.46  
   17.47 -lemma prod_fun_compose:
   17.48 -  "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
   17.49 -by (rule ext) auto
   17.50 +lemma snd_comp_map_pair [simp]:
   17.51 +  "snd \<circ> map_pair f g = g \<circ> snd"
   17.52 +  by (rule ext) simp_all
   17.53  
   17.54 -lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
   17.55 -  by (rule ext) auto
   17.56 +lemma map_pair_compose:
   17.57 +  "map_pair (f1 o f2) (g1 o g2) = (map_pair f1 g1 o map_pair f2 g2)"
   17.58 +  by (rule ext) (simp add: map_pair.compositionality comp_def)
   17.59  
   17.60 -lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r"
   17.61 -  apply (rule image_eqI)
   17.62 -  apply (rule prod_fun [symmetric], assumption)
   17.63 -  done
   17.64 +lemma map_pair_ident [simp]:
   17.65 +  "map_pair (%x. x) (%y. y) = (%z. z)"
   17.66 +  by (rule ext) (simp add: map_pair.identity)
   17.67 +
   17.68 +lemma map_pair_imageI [intro]:
   17.69 +  "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_pair f g ` R"
   17.70 +  by (rule image_eqI) simp_all
   17.71  
   17.72  lemma prod_fun_imageE [elim!]:
   17.73 -  assumes major: "c: (prod_fun f g)`r"
   17.74 -    and cases: "!!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P"
   17.75 +  assumes major: "c \<in> map_pair f g ` R"
   17.76 +    and cases: "\<And>x y. c = (f x, g y) \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> P"
   17.77    shows P
   17.78    apply (rule major [THEN imageE])
   17.79    apply (case_tac x)
   17.80    apply (rule cases)
   17.81 -   apply (blast intro: prod_fun)
   17.82 -  apply blast
   17.83 +  apply simp_all
   17.84    done
   17.85  
   17.86 -
   17.87  definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
   17.88 -  "apfst f = prod_fun f id"
   17.89 +  "apfst f = map_pair f id"
   17.90  
   17.91  definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" where
   17.92 -  "apsnd f = prod_fun id f"
   17.93 +  "apsnd f = map_pair id f"
   17.94  
   17.95  lemma apfst_conv [simp, code]:
   17.96    "apfst f (x, y) = (f x, y)" 
   17.97 @@ -941,7 +946,7 @@
   17.98    Disjoint union of a family of sets -- Sigma.
   17.99  *}
  17.100  
  17.101 -definition  Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
  17.102 +definition Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
  17.103    Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
  17.104  
  17.105  abbreviation
  17.106 @@ -1091,66 +1096,6 @@
  17.107  lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
  17.108    by (auto, case_tac "f x", auto)
  17.109  
  17.110 -text{* The following @{const prod_fun} lemmas are due to Joachim Breitner: *}
  17.111 -
  17.112 -lemma prod_fun_inj_on:
  17.113 -  assumes "inj_on f A" and "inj_on g B"
  17.114 -  shows "inj_on (prod_fun f g) (A \<times> B)"
  17.115 -proof (rule inj_onI)
  17.116 -  fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
  17.117 -  assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
  17.118 -  assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
  17.119 -  assume "prod_fun f g x = prod_fun f g y"
  17.120 -  hence "fst (prod_fun f g x) = fst (prod_fun f g y)" by (auto)
  17.121 -  hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
  17.122 -  with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
  17.123 -  have "fst x = fst y" by (auto dest:dest:inj_onD)
  17.124 -  moreover from `prod_fun f g x = prod_fun f g y`
  17.125 -  have "snd (prod_fun f g x) = snd (prod_fun f g y)" by (auto)
  17.126 -  hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
  17.127 -  with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
  17.128 -  have "snd x = snd y" by (auto dest:dest:inj_onD)
  17.129 -  ultimately show "x = y" by(rule prod_eqI)
  17.130 -qed
  17.131 -
  17.132 -lemma prod_fun_surj:
  17.133 -  assumes "surj f" and "surj g"
  17.134 -  shows "surj (prod_fun f g)"
  17.135 -unfolding surj_def
  17.136 -proof
  17.137 -  fix y :: "'b \<times> 'd"
  17.138 -  from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
  17.139 -  moreover
  17.140 -  from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
  17.141 -  ultimately have "(fst y, snd y) = prod_fun f g (a,b)" by auto
  17.142 -  thus "\<exists>x. y = prod_fun f g x" by auto
  17.143 -qed
  17.144 -
  17.145 -lemma prod_fun_surj_on:
  17.146 -  assumes "f ` A = A'" and "g ` B = B'"
  17.147 -  shows "prod_fun f g ` (A \<times> B) = A' \<times> B'"
  17.148 -unfolding image_def
  17.149 -proof(rule set_eqI,rule iffI)
  17.150 -  fix x :: "'a \<times> 'c"
  17.151 -  assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = prod_fun f g x}"
  17.152 -  then obtain y where "y \<in> A \<times> B" and "x = prod_fun f g y" by blast
  17.153 -  from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
  17.154 -  moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
  17.155 -  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
  17.156 -  with `x = prod_fun f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
  17.157 -next
  17.158 -  fix x :: "'a \<times> 'c"
  17.159 -  assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
  17.160 -  from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
  17.161 -  then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
  17.162 -  moreover from `image g B = B'` and `snd x \<in> B'`
  17.163 -  obtain b where "b \<in> B" and "snd x = g b" by auto
  17.164 -  ultimately have "(fst x, snd x) = prod_fun f g (a,b)" by auto
  17.165 -  moreover from `a \<in> A` and  `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
  17.166 -  ultimately have "\<exists>y \<in> A \<times> B. x = prod_fun f g y" by auto
  17.167 -  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = prod_fun f g y}" by auto
  17.168 -qed
  17.169 -
  17.170  lemma swap_inj_on:
  17.171    "inj_on (\<lambda>(i, j). (j, i)) A"
  17.172    by (auto intro!: inj_onI)
  17.173 @@ -1167,6 +1112,66 @@
  17.174      using * eq[symmetric] by auto
  17.175  qed simp_all
  17.176  
  17.177 +text {* The following @{const map_pair} lemmas are due to Joachim Breitner: *}
  17.178 +
  17.179 +lemma map_pair_inj_on:
  17.180 +  assumes "inj_on f A" and "inj_on g B"
  17.181 +  shows "inj_on (map_pair f g) (A \<times> B)"
  17.182 +proof (rule inj_onI)
  17.183 +  fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
  17.184 +  assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
  17.185 +  assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
  17.186 +  assume "map_pair f g x = map_pair f g y"
  17.187 +  hence "fst (map_pair f g x) = fst (map_pair f g y)" by (auto)
  17.188 +  hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
  17.189 +  with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
  17.190 +  have "fst x = fst y" by (auto dest:dest:inj_onD)
  17.191 +  moreover from `map_pair f g x = map_pair f g y`
  17.192 +  have "snd (map_pair f g x) = snd (map_pair f g y)" by (auto)
  17.193 +  hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
  17.194 +  with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
  17.195 +  have "snd x = snd y" by (auto dest:dest:inj_onD)
  17.196 +  ultimately show "x = y" by(rule prod_eqI)
  17.197 +qed
  17.198 +
  17.199 +lemma map_pair_surj:
  17.200 +  assumes "surj f" and "surj g"
  17.201 +  shows "surj (map_pair f g)"
  17.202 +unfolding surj_def
  17.203 +proof
  17.204 +  fix y :: "'b \<times> 'd"
  17.205 +  from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
  17.206 +  moreover
  17.207 +  from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
  17.208 +  ultimately have "(fst y, snd y) = map_pair f g (a,b)" by auto
  17.209 +  thus "\<exists>x. y = map_pair f g x" by auto
  17.210 +qed
  17.211 +
  17.212 +lemma map_pair_surj_on:
  17.213 +  assumes "f ` A = A'" and "g ` B = B'"
  17.214 +  shows "map_pair f g ` (A \<times> B) = A' \<times> B'"
  17.215 +unfolding image_def
  17.216 +proof(rule set_eqI,rule iffI)
  17.217 +  fix x :: "'a \<times> 'c"
  17.218 +  assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = map_pair f g x}"
  17.219 +  then obtain y where "y \<in> A \<times> B" and "x = map_pair f g y" by blast
  17.220 +  from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
  17.221 +  moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
  17.222 +  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
  17.223 +  with `x = map_pair f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
  17.224 +next
  17.225 +  fix x :: "'a \<times> 'c"
  17.226 +  assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
  17.227 +  from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
  17.228 +  then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
  17.229 +  moreover from `image g B = B'` and `snd x \<in> B'`
  17.230 +  obtain b where "b \<in> B" and "snd x = g b" by auto
  17.231 +  ultimately have "(fst x, snd x) = map_pair f g (a,b)" by auto
  17.232 +  moreover from `a \<in> A` and  `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
  17.233 +  ultimately have "\<exists>y \<in> A \<times> B. x = map_pair f g y" by auto
  17.234 +  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_pair f g y}" by auto
  17.235 +qed
  17.236 +
  17.237  
  17.238  subsection {* Inductively defined sets *}
  17.239  
    18.1 --- a/src/HOL/Quotient.thy	Thu Nov 18 22:34:32 2010 +0100
    18.2 +++ b/src/HOL/Quotient.thy	Fri Nov 19 10:04:08 2010 +0100
    18.3 @@ -160,18 +160,11 @@
    18.4  
    18.5  subsection {* Function map and function relation *}
    18.6  
    18.7 -definition
    18.8 -  fun_map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" (infixr "--->" 55)
    18.9 -where
   18.10 -  "fun_map f g = (\<lambda>h. g \<circ> h \<circ> f)"
   18.11 +notation map_fun (infixr "--->" 55)
   18.12  
   18.13 -lemma fun_map_apply [simp]:
   18.14 -  "(f ---> g) h x = g (h (f x))"
   18.15 -  by (simp add: fun_map_def)
   18.16 -
   18.17 -lemma fun_map_id:
   18.18 +lemma map_fun_id:
   18.19    "(id ---> id) = id"
   18.20 -  by (simp add: fun_eq_iff id_def)
   18.21 +  by (simp add: fun_eq_iff)
   18.22  
   18.23  definition
   18.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)
   18.25 @@ -520,13 +513,13 @@
   18.26  lemma all_prs:
   18.27    assumes a: "Quotient R absf repf"
   18.28    shows "Ball (Respects R) ((absf ---> id) f) = All f"
   18.29 -  using a unfolding Quotient_def Ball_def in_respects id_apply comp_def fun_map_def
   18.30 +  using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def
   18.31    by metis
   18.32  
   18.33  lemma ex_prs:
   18.34    assumes a: "Quotient R absf repf"
   18.35    shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
   18.36 -  using a unfolding Quotient_def Bex_def in_respects id_apply comp_def fun_map_def
   18.37 +  using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def
   18.38    by metis
   18.39  
   18.40  subsection {* @{text Bex1_rel} quantifier *}
   18.41 @@ -789,7 +782,7 @@
   18.42  
   18.43  use "Tools/Quotient/quotient_info.ML"
   18.44  
   18.45 -declare [[map "fun" = (fun_map, fun_rel)]]
   18.46 +declare [[map "fun" = (map_fun, fun_rel)]]
   18.47  
   18.48  lemmas [quot_thm] = fun_quotient
   18.49  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
   18.50 @@ -800,7 +793,7 @@
   18.51  text {* Lemmas about simplifying id's. *}
   18.52  lemmas [id_simps] =
   18.53    id_def[symmetric]
   18.54 -  fun_map_id
   18.55 +  map_fun_id
   18.56    id_apply
   18.57    id_o
   18.58    o_id
   18.59 @@ -880,7 +873,7 @@
   18.60  
   18.61  no_notation
   18.62    rel_conj (infixr "OOO" 75) and
   18.63 -  fun_map (infixr "--->" 55) and
   18.64 +  map_fun (infixr "--->" 55) and
   18.65    fun_rel (infixr "===>" 55)
   18.66  
   18.67  end
    19.1 --- a/src/HOL/Sum_Type.thy	Thu Nov 18 22:34:32 2010 +0100
    19.2 +++ b/src/HOL/Sum_Type.thy	Fri Nov 19 10:04:08 2010 +0100
    19.3 @@ -91,6 +91,20 @@
    19.4    then show "P s" by (auto intro: sumE [of s])
    19.5  qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
    19.6  
    19.7 +primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
    19.8 +  "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    19.9 +| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
   19.10 +
   19.11 +type_mapper sum_map proof -
   19.12 +  fix f g h i s
   19.13 +  show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s"
   19.14 +    by (cases s) simp_all
   19.15 +next
   19.16 +  fix s
   19.17 +  show "sum_map (\<lambda>x. x) (\<lambda>x. x) s = s"
   19.18 +    by (cases s) simp_all
   19.19 +qed
   19.20 +
   19.21  
   19.22  subsection {* Projections *}
   19.23  
    20.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Nov 18 22:34:32 2010 +0100
    20.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Nov 19 10:04:08 2010 +0100
    20.3 @@ -383,7 +383,7 @@
    20.4      => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
    20.5  
    20.6      (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
    20.7 -    (* observe fun_map *)
    20.8 +    (* observe map_fun *)
    20.9  | _ $ _ $ _
   20.10      => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
   20.11         ORELSE' rep_abs_rsp_tac ctxt
   20.12 @@ -428,23 +428,23 @@
   20.13  
   20.14  (*** Cleaning of the Theorem ***)
   20.15  
   20.16 -(* expands all fun_maps, except in front of the (bound) variables listed in xs *)
   20.17 -fun fun_map_simple_conv xs ctrm =
   20.18 +(* expands all map_funs, except in front of the (bound) variables listed in xs *)
   20.19 +fun map_fun_simple_conv xs ctrm =
   20.20    case (term_of ctrm) of
   20.21 -    ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
   20.22 +    ((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) =>
   20.23          if member (op=) xs h
   20.24          then Conv.all_conv ctrm
   20.25 -        else Conv.rewr_conv @{thm fun_map_apply [THEN eq_reflection]} ctrm
   20.26 +        else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
   20.27    | _ => Conv.all_conv ctrm
   20.28  
   20.29 -fun fun_map_conv xs ctxt ctrm =
   20.30 +fun map_fun_conv xs ctxt ctrm =
   20.31    case (term_of ctrm) of
   20.32 -      _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
   20.33 -                fun_map_simple_conv xs) ctrm
   20.34 -    | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
   20.35 +      _ $ _ => (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
   20.36 +                map_fun_simple_conv xs) ctrm
   20.37 +    | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
   20.38      | _ => Conv.all_conv ctrm
   20.39  
   20.40 -fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
   20.41 +fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt)
   20.42  
   20.43  (* custom matching functions *)
   20.44  fun mk_abs u i t =
   20.45 @@ -480,7 +480,7 @@
   20.46  *)
   20.47  fun lambda_prs_simple_conv ctxt ctrm =
   20.48    case (term_of ctrm) of
   20.49 -    (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
   20.50 +    (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
   20.51        let
   20.52          val thy = ProofContext.theory_of ctxt
   20.53          val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
   20.54 @@ -534,7 +534,7 @@
   20.55  
   20.56    val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   20.57  in
   20.58 -  EVERY' [fun_map_tac lthy,
   20.59 +  EVERY' [map_fun_tac lthy,
   20.60            lambda_prs_tac lthy,
   20.61            simp_tac ss,
   20.62            TRY o rtac refl]
    21.1 --- a/src/HOL/Tools/functorial_mappers.ML	Thu Nov 18 22:34:32 2010 +0100
    21.2 +++ b/src/HOL/Tools/functorial_mappers.ML	Fri Nov 19 10:04:08 2010 +0100
    21.3 @@ -17,7 +17,7 @@
    21.4  structure Functorial_Mappers : FUNCTORIAL_MAPPERS =
    21.5  struct
    21.6  
    21.7 -val concatenateN = "concatenate";
    21.8 +val compositionalityN = "compositionality";
    21.9  val identityN = "identity";
   21.10  
   21.11  (** functorial mappers and their properties **)
   21.12 @@ -25,7 +25,7 @@
   21.13  (* bookkeeping *)
   21.14  
   21.15  type entry = { mapper: string, variances: (sort * (bool * bool)) list,
   21.16 -  concatenate: thm, identity: thm };
   21.17 +  compositionality: thm, identity: thm };
   21.18  
   21.19  structure Data = Theory_Data(
   21.20    type T = entry Symtab.table
   21.21 @@ -74,7 +74,7 @@
   21.22  
   21.23  (* mapper properties *)
   21.24  
   21.25 -fun make_concatenate_prop variances (tyco, mapper) =
   21.26 +fun make_compositionality_prop variances (tyco, mapper) =
   21.27    let
   21.28      fun invents n k nctxt =
   21.29        let
   21.30 @@ -186,23 +186,23 @@
   21.31         of [tyco] => tyco
   21.32          | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
   21.33      val variances = analyze_variances thy tyco T;
   21.34 -    val concatenate_prop = uncurry (fold_rev Logic.all)
   21.35 -      (make_concatenate_prop variances (tyco, mapper));
   21.36 +    val compositionality_prop = uncurry (fold_rev Logic.all)
   21.37 +      (make_compositionality_prop variances (tyco, mapper));
   21.38      val identity_prop = uncurry Logic.all
   21.39        (make_identity_prop variances (tyco, mapper));
   21.40      val qualify = Binding.qualify true (Long_Name.base_name mapper) o Binding.name;
   21.41 -    fun after_qed [single_concatenate, single_identity] lthy =
   21.42 +    fun after_qed [single_compositionality, single_identity] lthy =
   21.43        lthy
   21.44 -      |> Local_Theory.note ((qualify concatenateN, []), single_concatenate)
   21.45 +      |> Local_Theory.note ((qualify compositionalityN, []), single_compositionality)
   21.46        ||>> Local_Theory.note ((qualify identityN, []), single_identity)
   21.47 -      |-> (fn ((_, [concatenate]), (_, [identity])) =>
   21.48 +      |-> (fn ((_, [compositionality]), (_, [identity])) =>
   21.49            (Local_Theory.background_theory o Data.map)
   21.50              (Symtab.update (tyco, { mapper = mapper, variances = variances,
   21.51 -              concatenate = concatenate, identity = identity })));
   21.52 +              compositionality = compositionality, identity = identity })));
   21.53    in
   21.54      thy
   21.55      |> Named_Target.theory_init
   21.56 -    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [concatenate_prop, identity_prop])
   21.57 +    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
   21.58    end
   21.59  
   21.60  val type_mapper = gen_type_mapper Sign.cert_term;
    22.1 --- a/src/HOL/Wellfounded.thy	Thu Nov 18 22:34:32 2010 +0100
    22.2 +++ b/src/HOL/Wellfounded.thy	Fri Nov 19 10:04:08 2010 +0100
    22.3 @@ -240,7 +240,7 @@
    22.4  
    22.5  text{*Well-foundedness of image*}
    22.6  
    22.7 -lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
    22.8 +lemma wf_map_pair_image: "[| wf r; inj f |] ==> wf(map_pair f f ` r)"
    22.9  apply (simp only: wf_eq_minimal, clarify)
   22.10  apply (case_tac "EX p. f p : Q")
   22.11  apply (erule_tac x = "{p. f p : Q}" in allE)