# HG changeset patch
# User haftmann
# Date 1292950343 -3600
# Node ID 551eb49a6e9166c89b98d8c7c2b4c8f030ad7c4b
# Parent  35d2241c169cbc10b06dd5d489d796accd761d45
tuned type_lifting declarations

diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Datatype.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -15,7 +15,7 @@
 
 subsection {* Prelude: lifting over function space *}
 
-type_lifting map_fun
+type_lifting map_fun: map_fun
   by (simp_all add: fun_eq_iff)
 
 
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Library/Cset.thy
--- a/src/HOL/Library/Cset.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Library/Cset.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -188,8 +188,8 @@
   "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
   by (simp add: set_def)
 
-type_lifting map
-  by (simp_all add: image_image)
+type_lifting map: map
+  by (simp_all add: fun_eq_iff image_compose)
 
 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   [simp]: "filter P A = Set (More_Set.project P (member A))"
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Library/Dlist.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -175,8 +175,8 @@
 
 section {* Functorial structure *}
 
-type_lifting map
-  by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
+type_lifting map: map
+  by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
 
 
 section {* Implementation of sets by distinct lists -- canonical! *}
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Library/Mapping.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -50,8 +50,8 @@
   "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
   by (simp add: map_def)
 
-type_lifting map
-  by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity)
+type_lifting map: map
+  by (simp_all add: mapping_eq_iff fun_eq_iff Option.map.compositionality Option.map.id)
 
 
 subsection {* Derived operations *}
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -1643,12 +1643,21 @@
   @{term "{#x+x|x:#M. x<c#}"}.
 *}
 
-type_lifting 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
+type_lifting image_mset: image_mset proof -
+  fix f g 
+  show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
+  proof
+    fix A
+    show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
+      by (induct A) simp_all
+  qed
 next
-  fix A show "image_mset (\<lambda>x. x) A = A"
-    by (induct A) simp_all
+  show "image_mset id = id"
+  proof
+    fix A
+    show "image_mset id A = id A"
+      by (induct A) simp_all
+  qed
 qed
 
 
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -60,7 +60,7 @@
   assumes "Quotient R Abs Rep"
   shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
   apply (rule QuotientI)
-  apply (simp_all add: Option.map.compositionality Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
+  apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
   using Quotient_rel [OF assms]
   apply (simp add: option_rel_unfold split: option.split)
   done
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Library/Quotient_Product.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -38,7 +38,7 @@
   assumes "Quotient R2 Abs2 Rep2"
   shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
   apply (rule QuotientI)
-  apply (simp add: map_pair.compositionality map_pair.identity
+  apply (simp add: map_pair.compositionality comp_def map_pair.identity
      Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
   apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
   using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -61,10 +61,10 @@
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
   apply (rule QuotientI)
-  apply (simp_all add: sum_map.compositionality sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
+  apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
     Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
   using Quotient_rel [OF q1] Quotient_rel [OF q2]
-  apply (simp add: sum_rel_unfold split: sum.split)
+  apply (simp add: sum_rel_unfold comp_def split: sum.split)
   done
 
 lemma sum_Inl_rsp [quot_respect]:
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/List.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -881,8 +881,8 @@
   "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
 by (induct rule:list_induct2, simp_all)
 
-type_lifting map
-  by simp_all
+type_lifting map: map
+  by (simp_all add: fun_eq_iff id_def)
 
 
 subsubsection {* @{text rev} *}
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Option.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -81,14 +81,21 @@
     "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_lifting 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
+type_lifting map: Option.map proof -
+  fix f g
+  show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
+  proof
+    fix x
+    show "(Option.map f \<circ> Option.map g) x= Option.map (f \<circ> g) x"
+      by (cases x) simp_all
+  qed
 next
-  fix x
-  show "Option.map (\<lambda>x. x) x = x"
-    by (cases x) simp_all
+  show "Option.map id = id"
+  proof
+    fix x
+    show "Option.map id x = id x"
+      by (cases x) simp_all
+  qed
 qed
 
 primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Predicate.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -795,8 +795,8 @@
   "eval (map f P) = image f (eval P)"
   by (auto simp add: map_def)
 
-type_lifting map
-  by (auto intro!: pred_eqI simp add: image_image)
+type_lifting map: map
+  by (auto intro!: pred_eqI simp add: fun_eq_iff image_compose)
 
 
 subsubsection {* Implementation *}
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Product_Type.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -834,8 +834,8 @@
   "map_pair f g (a, b) = (f a, g b)"
   by (simp add: map_pair_def)
 
-type_lifting map_pair
-  by (simp_all add: split_paired_all)
+type_lifting map_pair: map_pair
+  by (auto simp add: split_paired_all intro: ext)
 
 lemma fst_map_pair [simp]:
   "fst (map_pair f g x) = f (fst x)"
diff -r 35d2241c169c -r 551eb49a6e91 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Sum_Type.thy	Tue Dec 21 17:52:23 2010 +0100
@@ -95,14 +95,22 @@
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
 
-type_lifting 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
+type_lifting sum_map: sum_map proof -
+  fix f g h i
+  show "sum_map f g \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)"
+  proof
+    fix s
+    show "(sum_map f g \<circ> sum_map h i) s = sum_map (f \<circ> h) (g \<circ> i) s"
+      by (cases s) simp_all
+  qed
 next
   fix s
-  show "sum_map (\<lambda>x. x) (\<lambda>x. x) s = s"
-    by (cases s) simp_all
+  show "sum_map id id = id"
+  proof
+    fix s
+    show "sum_map id id s = id s" 
+      by (cases s) simp_all
+  qed
 qed