tuned type_lifting declarations
authorhaftmann
Tue Dec 21 17:52:23 2010 +0100 (2010-12-21)
changeset 41372551eb49a6e91
parent 41371 35d2241c169c
child 41373 48503e4e96b6
tuned type_lifting declarations
src/HOL/Datatype.thy
src/HOL/Library/Cset.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/List.thy
src/HOL/Option.thy
src/HOL/Predicate.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
     1.1 --- a/src/HOL/Datatype.thy	Tue Dec 21 16:14:46 2010 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Tue Dec 21 17:52:23 2010 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  subsection {* Prelude: lifting over function space *}
     1.6  
     1.7 -type_lifting map_fun
     1.8 +type_lifting map_fun: map_fun
     1.9    by (simp_all add: fun_eq_iff)
    1.10  
    1.11  
     2.1 --- a/src/HOL/Library/Cset.thy	Tue Dec 21 16:14:46 2010 +0100
     2.2 +++ b/src/HOL/Library/Cset.thy	Tue Dec 21 17:52:23 2010 +0100
     2.3 @@ -188,8 +188,8 @@
     2.4    "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
     2.5    by (simp add: set_def)
     2.6  
     2.7 -type_lifting map
     2.8 -  by (simp_all add: image_image)
     2.9 +type_lifting map: map
    2.10 +  by (simp_all add: fun_eq_iff image_compose)
    2.11  
    2.12  definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    2.13    [simp]: "filter P A = Set (More_Set.project P (member A))"
     3.1 --- a/src/HOL/Library/Dlist.thy	Tue Dec 21 16:14:46 2010 +0100
     3.2 +++ b/src/HOL/Library/Dlist.thy	Tue Dec 21 17:52:23 2010 +0100
     3.3 @@ -175,8 +175,8 @@
     3.4  
     3.5  section {* Functorial structure *}
     3.6  
     3.7 -type_lifting map
     3.8 -  by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
     3.9 +type_lifting map: map
    3.10 +  by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
    3.11  
    3.12  
    3.13  section {* Implementation of sets by distinct lists -- canonical! *}
     4.1 --- a/src/HOL/Library/Mapping.thy	Tue Dec 21 16:14:46 2010 +0100
     4.2 +++ b/src/HOL/Library/Mapping.thy	Tue Dec 21 17:52:23 2010 +0100
     4.3 @@ -50,8 +50,8 @@
     4.4    "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
     4.5    by (simp add: map_def)
     4.6  
     4.7 -type_lifting map
     4.8 -  by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity)
     4.9 +type_lifting map: map
    4.10 +  by (simp_all add: mapping_eq_iff fun_eq_iff Option.map.compositionality Option.map.id)
    4.11  
    4.12  
    4.13  subsection {* Derived operations *}
     5.1 --- a/src/HOL/Library/Multiset.thy	Tue Dec 21 16:14:46 2010 +0100
     5.2 +++ b/src/HOL/Library/Multiset.thy	Tue Dec 21 17:52:23 2010 +0100
     5.3 @@ -1643,12 +1643,21 @@
     5.4    @{term "{#x+x|x:#M. x<c#}"}.
     5.5  *}
     5.6  
     5.7 -type_lifting image_mset proof -
     5.8 -  fix f g A show "image_mset f (image_mset g A) = image_mset (\<lambda>x. f (g x)) A"
     5.9 -    by (induct A) simp_all
    5.10 +type_lifting image_mset: image_mset proof -
    5.11 +  fix f g 
    5.12 +  show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
    5.13 +  proof
    5.14 +    fix A
    5.15 +    show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
    5.16 +      by (induct A) simp_all
    5.17 +  qed
    5.18  next
    5.19 -  fix A show "image_mset (\<lambda>x. x) A = A"
    5.20 -    by (induct A) simp_all
    5.21 +  show "image_mset id = id"
    5.22 +  proof
    5.23 +    fix A
    5.24 +    show "image_mset id A = id A"
    5.25 +      by (induct A) simp_all
    5.26 +  qed
    5.27  qed
    5.28  
    5.29  
     6.1 --- a/src/HOL/Library/Quotient_Option.thy	Tue Dec 21 16:14:46 2010 +0100
     6.2 +++ b/src/HOL/Library/Quotient_Option.thy	Tue Dec 21 17:52:23 2010 +0100
     6.3 @@ -60,7 +60,7 @@
     6.4    assumes "Quotient R Abs Rep"
     6.5    shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
     6.6    apply (rule QuotientI)
     6.7 -  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])
     6.8 +  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])
     6.9    using Quotient_rel [OF assms]
    6.10    apply (simp add: option_rel_unfold split: option.split)
    6.11    done
     7.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Dec 21 16:14:46 2010 +0100
     7.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Dec 21 17:52:23 2010 +0100
     7.3 @@ -38,7 +38,7 @@
     7.4    assumes "Quotient R2 Abs2 Rep2"
     7.5    shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
     7.6    apply (rule QuotientI)
     7.7 -  apply (simp add: map_pair.compositionality map_pair.identity
     7.8 +  apply (simp add: map_pair.compositionality comp_def map_pair.identity
     7.9       Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
    7.10    apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
    7.11    using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
     8.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Dec 21 16:14:46 2010 +0100
     8.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Dec 21 17:52:23 2010 +0100
     8.3 @@ -61,10 +61,10 @@
     8.4    assumes q2: "Quotient R2 Abs2 Rep2"
     8.5    shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
     8.6    apply (rule QuotientI)
     8.7 -  apply (simp_all add: sum_map.compositionality sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
     8.8 +  apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
     8.9      Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
    8.10    using Quotient_rel [OF q1] Quotient_rel [OF q2]
    8.11 -  apply (simp add: sum_rel_unfold split: sum.split)
    8.12 +  apply (simp add: sum_rel_unfold comp_def split: sum.split)
    8.13    done
    8.14  
    8.15  lemma sum_Inl_rsp [quot_respect]:
     9.1 --- a/src/HOL/List.thy	Tue Dec 21 16:14:46 2010 +0100
     9.2 +++ b/src/HOL/List.thy	Tue Dec 21 17:52:23 2010 +0100
     9.3 @@ -881,8 +881,8 @@
     9.4    "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
     9.5  by (induct rule:list_induct2, simp_all)
     9.6  
     9.7 -type_lifting map
     9.8 -  by simp_all
     9.9 +type_lifting map: map
    9.10 +  by (simp_all add: fun_eq_iff id_def)
    9.11  
    9.12  
    9.13  subsubsection {* @{text rev} *}
    10.1 --- a/src/HOL/Option.thy	Tue Dec 21 16:14:46 2010 +0100
    10.2 +++ b/src/HOL/Option.thy	Tue Dec 21 17:52:23 2010 +0100
    10.3 @@ -81,14 +81,21 @@
    10.4      "map f o sum_case g h = sum_case (map f o g) (map f o h)"
    10.5    by (rule ext) (simp split: sum.split)
    10.6  
    10.7 -type_lifting Option.map proof -
    10.8 -  fix f g x
    10.9 -  show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x"
   10.10 -    by (cases x) simp_all
   10.11 +type_lifting map: Option.map proof -
   10.12 +  fix f g
   10.13 +  show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
   10.14 +  proof
   10.15 +    fix x
   10.16 +    show "(Option.map f \<circ> Option.map g) x= Option.map (f \<circ> g) x"
   10.17 +      by (cases x) simp_all
   10.18 +  qed
   10.19  next
   10.20 -  fix x
   10.21 -  show "Option.map (\<lambda>x. x) x = x"
   10.22 -    by (cases x) simp_all
   10.23 +  show "Option.map id = id"
   10.24 +  proof
   10.25 +    fix x
   10.26 +    show "Option.map id x = id x"
   10.27 +      by (cases x) simp_all
   10.28 +  qed
   10.29  qed
   10.30  
   10.31  primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
    11.1 --- a/src/HOL/Predicate.thy	Tue Dec 21 16:14:46 2010 +0100
    11.2 +++ b/src/HOL/Predicate.thy	Tue Dec 21 17:52:23 2010 +0100
    11.3 @@ -795,8 +795,8 @@
    11.4    "eval (map f P) = image f (eval P)"
    11.5    by (auto simp add: map_def)
    11.6  
    11.7 -type_lifting map
    11.8 -  by (auto intro!: pred_eqI simp add: image_image)
    11.9 +type_lifting map: map
   11.10 +  by (auto intro!: pred_eqI simp add: fun_eq_iff image_compose)
   11.11  
   11.12  
   11.13  subsubsection {* Implementation *}
    12.1 --- a/src/HOL/Product_Type.thy	Tue Dec 21 16:14:46 2010 +0100
    12.2 +++ b/src/HOL/Product_Type.thy	Tue Dec 21 17:52:23 2010 +0100
    12.3 @@ -834,8 +834,8 @@
    12.4    "map_pair f g (a, b) = (f a, g b)"
    12.5    by (simp add: map_pair_def)
    12.6  
    12.7 -type_lifting map_pair
    12.8 -  by (simp_all add: split_paired_all)
    12.9 +type_lifting map_pair: map_pair
   12.10 +  by (auto simp add: split_paired_all intro: ext)
   12.11  
   12.12  lemma fst_map_pair [simp]:
   12.13    "fst (map_pair f g x) = f (fst x)"
    13.1 --- a/src/HOL/Sum_Type.thy	Tue Dec 21 16:14:46 2010 +0100
    13.2 +++ b/src/HOL/Sum_Type.thy	Tue Dec 21 17:52:23 2010 +0100
    13.3 @@ -95,14 +95,22 @@
    13.4    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    13.5  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    13.6  
    13.7 -type_lifting sum_map proof -
    13.8 -  fix f g h i s
    13.9 -  show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s"
   13.10 -    by (cases s) simp_all
   13.11 +type_lifting sum_map: sum_map proof -
   13.12 +  fix f g h i
   13.13 +  show "sum_map f g \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)"
   13.14 +  proof
   13.15 +    fix s
   13.16 +    show "(sum_map f g \<circ> sum_map h i) s = sum_map (f \<circ> h) (g \<circ> i) s"
   13.17 +      by (cases s) simp_all
   13.18 +  qed
   13.19  next
   13.20    fix s
   13.21 -  show "sum_map (\<lambda>x. x) (\<lambda>x. x) s = s"
   13.22 -    by (cases s) simp_all
   13.23 +  show "sum_map id id = id"
   13.24 +  proof
   13.25 +    fix s
   13.26 +    show "sum_map id id s = id s" 
   13.27 +      by (cases s) simp_all
   13.28 +  qed
   13.29  qed
   13.30  
   13.31