# HG changeset patch
# User haftmann
# Date 1292950355 -3600
# Node ID a35af5180c0104ff62507e68735a2b5a929f147b
# Parent  17b09240893cb3046f6914c171500bd6ef6d135b# Parent  48503e4e96b67891d43c7644c924b6350a9367d6
merged

diff -r 17b09240893c -r a35af5180c01 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Datatype.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Library/Cset.thy
--- a/src/HOL/Library/Cset.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Cset.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Dlist.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Mapping.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Multiset.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Quotient_Option.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Quotient_Product.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Library/Quotient_Sum.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/List.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Option.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Predicate.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Product_Type.thy	Tue Dec 21 17:52:35 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 17b09240893c -r a35af5180c01 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Sum_Type.thy	Tue Dec 21 17:52:35 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
 
 
diff -r 17b09240893c -r a35af5180c01 src/HOL/Tools/type_lifting.ML
--- a/src/HOL/Tools/type_lifting.ML	Tue Dec 21 08:43:39 2010 -0800
+++ b/src/HOL/Tools/type_lifting.ML	Tue Dec 21 17:52:35 2010 +0100
@@ -17,6 +17,8 @@
 structure Type_Lifting : TYPE_LIFTING =
 struct
 
+val compN = "comp";
+val idN = "id";
 val compositionalityN = "compositionality";
 val identityN = "identity";
 
@@ -25,7 +27,7 @@
 (* bookkeeping *)
 
 type entry = { mapper: string, variances: (sort * (bool * bool)) list,
-  compositionality: thm, identity: thm };
+  comp: thm, id: thm };
 
 structure Data = Theory_Data(
   type T = entry Symtab.table
@@ -74,19 +76,14 @@
 
 (* mapper properties *)
 
-fun make_compositionality_prop variances (tyco, mapper) =
+fun make_comp_prop ctxt variances (tyco, mapper) =
   let
-    fun invents n k nctxt =
-      let
-        val names = Name.invents nctxt n k;
-      in (names, fold Name.declare names nctxt) end;
-    val (((vs3, vs2), vs1), _) = Name.context
-      |> invents Name.aT (length variances)
-      ||>> invents Name.aT (length variances)
-      ||>> invents Name.aT (length variances);
-    fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
-      vs variances;
-    val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3);
+    val sorts = map fst variances
+    val (((vs3, vs2), vs1), _) = ctxt
+      |> Variable.invent_types sorts
+      ||>> Variable.invent_types sorts
+      ||>> Variable.invent_types sorts
+    val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3);
     fun mk_argT ((T, T'), (_, (co, contra))) =
       (if co then [(T --> T')] else [])
       @ (if contra then [(T' --> T)] else []);
@@ -94,40 +91,66 @@
       (if co then [false] else []) @ (if contra then [true] else [])) variances;
     val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
     val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
-    val ((names21, names32), nctxt) = Name.context
+    fun invents n k nctxt =
+      let
+        val names = Name.invents nctxt n k;
+      in (names, fold Name.declare names nctxt) end;
+    val ((names21, names32), nctxt) = Variable.names_of ctxt
       |> invents "f" (length Ts21)
       ||>> invents "f" (length Ts32);
     val T1 = Type (tyco, Ts1);
     val T2 = Type (tyco, Ts2);
     val T3 = Type (tyco, Ts3);
-    val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3);
     val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
     val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
       if not is_contra then
-        Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0))
+        HOLogic.mk_comp (Free (f21, T21), Free (f32, T32))
       else
-        Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
+        HOLogic.mk_comp (Free (f32, T32), Free (f21, T21))
       ) contras (args21 ~~ args32)
     fun mk_mapper T T' args = list_comb (Const (mapper,
       map fastype_of args ---> T --> T'), args);
-    val lhs = mk_mapper T2 T1 (map Free args21) $
-      (mk_mapper T3 T2 (map Free args32) $ x);
-    val rhs = mk_mapper T3 T1 args31 $ x;
-  in (map Free (args21 @ args32) @ [x], (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
+    val lhs = HOLogic.mk_comp (mk_mapper T2 T1 (map Free args21), mk_mapper T3 T2 (map Free args32));
+    val rhs = mk_mapper T3 T1 args31;
+  in fold_rev Logic.all (map Free (args21 @ args32)) ((HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
 
-fun make_identity_prop variances (tyco, mapper) =
+fun make_id_prop ctxt variances (tyco, mapper) =
   let
-    val vs = Name.invents Name.context Name.aT (length variances);
-    val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances;
+    val (vs, ctxt') = Variable.invent_types (map fst variances) ctxt;
+    val Ts = map TFree vs;
     fun bool_num b = if b then 1 else 0;
     fun mk_argT (T, (_, (co, contra))) =
       replicate (bool_num co + bool_num contra) (T --> T)
     val Ts' = maps mk_argT (Ts ~~ variances)
     val T = Type (tyco, Ts);
-    val x = Free (Long_Name.base_name tyco, T);
     val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
-      map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
-  in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;
+      map (HOLogic.id_const o domain_type) Ts');
+  in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, HOLogic.id_const T) end;
+
+val comp_apply = Simpdata.mk_eq @{thm o_apply};
+val id_def = Simpdata.mk_eq @{thm id_def};
+
+fun make_compositionality ctxt thm =
+  let
+    val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt;
+    val thm'' = @{thm fun_cong} OF [thm'];
+    val thm''' =
+      (Conv.fconv_rule o Conv.arg_conv o Conv.arg1_conv o Conv.rewr_conv) comp_apply thm'';
+  in singleton (Variable.export ctxt' ctxt) thm''' end;
+
+fun args_conv k conv =
+  if k <= 0 then Conv.all_conv
+  else Conv.combination_conv (args_conv (k - 1) conv) conv;
+
+fun make_identity ctxt variances thm =
+  let
+    val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt;
+    fun bool_num b = if b then 1 else 0;
+    val num_args = Integer.sum
+      (map (fn (_, (co, contra)) => bool_num co + bool_num contra) variances);
+    val thm'' =
+      (Conv.fconv_rule o Conv.arg_conv o Conv.arg1_conv o args_conv num_args o Conv.rewr_conv) id_def thm';
+  in singleton (Variable.export ctxt' ctxt) thm'' end;
 
 
 (* analyzing and registering mappers *)
@@ -177,7 +200,6 @@
     val (mapper, T) = case prep_term thy raw_t
      of Const cT => cT
       | t => error ("No constant: " ^ Syntax.string_of_term_global thy t);
-    val prfx = the_default (Long_Name.base_name mapper) some_prfx;
     val _ = Type.no_tvars T;
     fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
       | add_tycos _ = I;
@@ -186,24 +208,29 @@
       else case remove (op =) "fun" tycos
        of [tyco] => tyco
         | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
+    val prfx = the_default (Long_Name.base_name tyco) some_prfx;
     val variances = analyze_variances thy tyco T;
-    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 ctxt = ProofContext.init_global thy;
+    val comp_prop = make_comp_prop ctxt variances (tyco, mapper);
+    val id_prop = make_id_prop ctxt variances (tyco, mapper);
     val qualify = Binding.qualify true prfx o Binding.name;
-    fun after_qed [single_compositionality, single_identity] lthy =
+    fun after_qed [single_comp, single_id] lthy =
       lthy
-      |> Local_Theory.note ((qualify compositionalityN, []), single_compositionality)
-      ||>> Local_Theory.note ((qualify identityN, []), single_identity)
-      |-> (fn ((_, [compositionality]), (_, [identity])) =>
-          (Local_Theory.background_theory o Data.map)
+      |> Local_Theory.note ((qualify compN, []), single_comp)
+      ||>> Local_Theory.note ((qualify idN, []), single_id)
+      |-> (fn ((_, [comp]), (_, [id])) => fn lthy =>
+        lthy
+        |> Local_Theory.note ((qualify compositionalityN, []), [make_compositionality lthy comp])
+        |> snd
+        |> Local_Theory.note ((qualify identityN, []), [make_identity lthy variances id])
+        |> snd
+        |> (Local_Theory.background_theory o Data.map)
             (Symtab.update (tyco, { mapper = mapper, variances = variances,
-              compositionality = compositionality, identity = identity })));
+              comp = comp, id = id })));
   in
     thy
     |> Named_Target.theory_init
-    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
+    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
   end
 
 val type_lifting = gen_type_lifting Sign.cert_term;