--- 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)
--- 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))"
--- 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! *}
--- 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 *}
--- 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
--- 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
--- 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)]
--- 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]:
--- 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} *}
--- 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
--- 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 *}
--- 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)"
--- 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