merged
authorblanchet
Mon, 06 Dec 2010 13:17:26 +0100
changeset 40984 ef119e33dc06
parent 40976 8df0a190df1e (diff)
parent 40983 07526f546680 (current diff)
child 40985 8b870370c26f
merged
--- a/etc/components	Mon Dec 06 11:41:24 2010 +0100
+++ b/etc/components	Mon Dec 06 13:17:26 2010 +0100
@@ -17,3 +17,4 @@
 src/HOL/Library/Sum_Of_Squares
 src/HOL/Tools/SMT
 src/HOL/Tools/Predicate_Compile
+src/HOL/Mutabelle
--- a/etc/isar-keywords.el	Mon Dec 06 11:41:24 2010 +0100
+++ b/etc/isar-keywords.el	Mon Dec 06 13:17:26 2010 +0100
@@ -248,7 +248,7 @@
     "txt"
     "txt_raw"
     "typ"
-    "type_mapper"
+    "type_lifting"
     "type_notation"
     "typed_print_translation"
     "typedecl"
@@ -551,7 +551,7 @@
     "sublocale"
     "termination"
     "theorem"
-    "type_mapper"
+    "type_lifting"
     "typedef"))
 
 (defconst isar-keywords-qed
--- a/src/HOL/Datatype.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Datatype.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -13,6 +13,12 @@
   ("Tools/Datatype/datatype_realizer.ML")
 begin
 
+subsection {* Prelude: lifting over function space *}
+
+type_lifting map_fun
+  by (simp_all add: fun_eq_iff)
+
+
 subsection {* The datatype universe *}
 
 typedef (Node)
--- a/src/HOL/Fun.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Fun.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -7,6 +7,7 @@
 
 theory Fun
 imports Complete_Lattice
+uses ("Tools/type_lifting.ML")
 begin
 
 text{*As a simplification rule, it replaces all function equalities by
@@ -126,9 +127,6 @@
   "map_fun f g h x = g (h (f x))"
   by (simp add: map_fun_def)
 
-type_mapper map_fun
-  by (simp_all add: fun_eq_iff)
-
 
 subsection {* Injectivity and Bijectivity *}
 
@@ -774,7 +772,9 @@
   thus False by best
 qed
 
-subsection {* Proof tool setup *} 
+subsection {* Setup *} 
+
+subsubsection {* Proof tools *}
 
 text {* simplifies terms of the form
   f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *}
@@ -809,7 +809,7 @@
 *}
 
 
-subsection {* Code generator setup *}
+subsubsection {* Code generator *}
 
 types_code
   "fun"  ("(_ ->/ _)")
@@ -840,4 +840,9 @@
 code_const "id"
   (Haskell "id")
 
+
+subsubsection {* Functorial structure of types *}
+
+use "Tools/type_lifting.ML"
+
 end
--- a/src/HOL/HOL.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/HOL.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -32,7 +32,6 @@
   "Tools/async_manager.ML"
   "Tools/try.ML"
   ("Tools/cnf_funcs.ML")
-  ("Tools/type_mapper.ML")
   "~~/src/Tools/subtyping.ML"
 begin
 
@@ -714,7 +713,6 @@
   and [Pure.elim?] = iffD1 iffD2 impE
 
 use "Tools/hologic.ML"
-use "Tools/type_mapper.ML"
 
 
 subsubsection {* Atomizing meta-level connectives *}
--- a/src/HOL/IsaMakefile	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/IsaMakefile	Mon Dec 06 13:17:26 2010 +0100
@@ -147,7 +147,6 @@
   $(SRC)/Tools/solve_direct.ML \
   $(SRC)/Tools/value.ML \
   HOL.thy \
-  Tools/type_mapper.ML \
   Tools/hologic.ML \
   Tools/recfun_codegen.ML \
   Tools/simpdata.ML
@@ -243,6 +242,7 @@
   Tools/split_rule.ML \
   Tools/try.ML \
   Tools/typedef.ML \
+  Tools/type_lifting.ML \
   Transitive_Closure.thy \
   Typedef.thy \
   Wellfounded.thy
--- a/src/HOL/Library/Cset.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Library/Cset.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -188,7 +188,7 @@
   "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
   by (simp add: set_def)
 
-type_mapper map
+type_lifting map
   by (simp_all add: image_image)
 
 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
--- a/src/HOL/Library/Dlist.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Library/Dlist.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -175,7 +175,7 @@
 
 section {* Functorial structure *}
 
-type_mapper map
+type_lifting map
   by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
 
 
--- a/src/HOL/Library/Mapping.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Library/Mapping.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -50,7 +50,7 @@
   "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
   by (simp add: map_def)
 
-type_mapper map
+type_lifting map
   by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity)
 
 
--- a/src/HOL/Library/Multiset.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -1631,7 +1631,7 @@
   @{term "{#x+x|x:#M. x<c#}"}.
 *}
 
-type_mapper image_mset proof -
+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
 next
--- a/src/HOL/List.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/List.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -881,7 +881,7 @@
   "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
 by (induct rule:list_induct2, simp_all)
 
-type_mapper map
+type_lifting map
   by simp_all
 
 
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Mon Dec 06 13:17:26 2010 +0100
@@ -22,7 +22,7 @@
   echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
   echo
   echo "  Options are:"
-  echo "    -L LOGIC     parent logic to use (default $ISABELLE_LOGIC)"
+  echo "    -L LOGIC     parent logic to use (default $MIRABELLE_LOGIC)"
   echo "    -T THEORY    parent theory to use (default $MIRABELLE_THEORY)"
   echo "    -O DIR       output directory for test data (default $out)"
   echo "    -t TIMEOUT   timeout for each action in seconds (default $timeout)"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mutabelle/etc/settings	Mon Dec 06 13:17:26 2010 +0100
@@ -0,0 +1,7 @@
+MUTABELLE_HOME="$COMPONENT"
+
+MUTABELLE_LOGIC=HOL
+MUTABELLE_IMPORT_THEORY=Complex_Main
+MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Mon Dec 06 13:17:26 2010 +0100
@@ -0,0 +1,107 @@
+#!/usr/bin/env bash
+#
+# Author: Lukas Bulwahn
+#
+# DESCRIPTION: mutant-testing tool for counterexample generators and automated proof tools
+
+
+PRG="$(basename "$0")"
+
+function usage() {
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] THEORY"
+  echo
+  echo "  Options are:"
+  echo "    -L LOGIC     parent logic to use (default $MUTABELLE_LOGIC)"
+  echo "    -T THEORY    parent theory to use (default $MUTABELLE_IMPORT_THEORY)"
+  echo "    -O DIR       output directory for test data (default $MUTABELLE_OUTPUT_PATH)"
+  echo
+  echo "  THEORY is the name of the theory of which all theorems should be mutated and tested"
+  exit 1
+}
+
+
+## process command line
+
+# options
+
+while getopts "L:T:O:t:q?" OPT
+do
+  case "$OPT" in
+    L)
+      MIRABELLE_LOGIC="$OPTARG"
+      ;;
+    T)
+      MIRABELLE_IMPORT_THEORY="$OPTARG"
+      ;;
+    O)
+      MIRABELLE_OUTPUT_PATH="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+[ "$#" -ne 1 ] && usage
+
+MUTABELLE_TEST_THEORY="$1"
+
+## main
+
+echo "Starting Mutabelle..."
+
+# setup
+
+mkdir -p "$MIRABELLE_OUTPUT_PATH"
+
+echo "theory Mutabelle_Test
+imports $MUTABELLE_IMPORT_THEORY
+uses     
+  \"$MUTABELLE_HOME/mutabelle.ML\"
+  \"$MUTABELLE_HOME/mutabelle_extra.ML\"
+begin
+
+ML {*
+val mtds = [
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\",
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\"
+]
+*}
+
+ML {*
+fun mutation_testing_of thy =
+  (MutabelleExtra.random_seed := 1.0;
+  MutabelleExtra.thms_of false thy
+  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
+         @{theory} mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
+*}
+
+ML {*
+  mutation_testing_of @{theory $MUTABELLE_TEST_THEORY}
+*}
+
+end" > $MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy
+
+# execution
+
+$ISABELLE_PROCESS -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q $MUTABELLE_LOGIC  > /dev/null 2>&1
+
+# make statistics
+
+GenuineCex_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: GenuineCex" | wc -l)
+NoCex_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: NoCex" | wc -l)
+Timeout_random=$(cat /$MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: Timeout" | wc -l)
+Errors_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: Error" | wc -l)
+
+GenuineCex_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: GenuineCex" | wc -l)
+NoCex_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: NoCex" | wc -l)
+Timeout_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: Timeout" | wc -l)
+Errors_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: Error" | wc -l)
+
+
+echo "random      :" C: $GenuineCex_random N: $NoCex_random T: $Timeout_random E: $Errors_random
+echo "exhaustive  :" C: $GenuineCex_exh N: $NoCex_exh T: $Timeout_exh E: $Errors_exh
+
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Dec 06 13:17:26 2010 +0100
@@ -25,6 +25,9 @@
 val solve_direct_mtd : mtd
 val try_mtd : mtd
 (*
+val sledgehammer_mtd : mtd
+*)
+(*
 val refute_mtd : mtd
 val nitpick_mtd : mtd
 *)
@@ -143,15 +146,26 @@
 
 fun invoke_try thy t =
   let
-    val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) 
+    val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
   in
-    case Try.invoke_try NONE state of
+    case Try.invoke_try (SOME (seconds 5.0)) state of
       true => (Solved, ([], NONE))
     | false => (Unsolved, ([], NONE))
   end
 
 val try_mtd = ("try", invoke_try)
 
+(** sledgehammer **)
+(*
+fun invoke_sledgehammer thy t =
+  if can (Goal.prove_global thy (Term.add_free_names t [])  [] t)
+      (fn {context, ...} => Sledgehammer_Tactics.sledgehammer_with_metis_tac context 1) then
+    (Solved, ([], NONE))
+  else
+    (Unsolved, ([], NONE))
+
+val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer)
+*)
 (*
 fun invoke_refute thy t =
   let
@@ -287,7 +301,14 @@
  @{const_name "Pure.term"},
  @{const_name "top_class.top"},
  (*@{const_name "HOL.equal"},*)
- @{const_name "Quotient.Quot_True"}
+ @{const_name "Quotient.Quot_True"},
+ @{const_name "equal_fun_inst.equal_fun"},
+ @{const_name "equal_bool_inst.equal_bool"},
+ @{const_name "ord_fun_inst.less_eq_fun"},
+ @{const_name "ord_fun_inst.less_fun"},
+ @{const_name Metis.fequal},
+ @{const_name Meson.skolem},
+ @{const_name transfer_morphism}
  (*@{const_name "==>"}, @{const_name "=="}*)]
 
 val forbidden_mutant_consts =
@@ -426,11 +447,12 @@
       else
         mutants
     val mutants = mutants
-          |> take_random max_mutants
           |> map Mutabelle.freeze |> map freezeT
 (*          |> filter (not o is_forbidden_mutant) *)
           |> List.mapPartial (try (Sign.cert_term thy))
-          |> List.filter (is_some o try (cterm_of thy))
+          |> List.filter (is_some o try (Thm.cterm_of thy))
+          |> List.filter (is_some o try (Syntax.check_term (ProofContext.init_global thy)))
+          |> take_random max_mutants
     val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
   in
     create_entry thy thm exec mutants mtds
--- a/src/HOL/Option.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Option.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -81,7 +81,7 @@
     "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_mapper Option.map proof -
+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
--- a/src/HOL/Product_Type.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Product_Type.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -835,7 +835,7 @@
   "map_pair f g (a, b) = (f a, g b)"
   by (simp add: map_pair_def)
 
-type_mapper map_pair
+type_lifting map_pair
   by (simp_all add: split_paired_all)
 
 lemma fst_map_pair [simp]:
--- a/src/HOL/Quickcheck.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Quickcheck.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -129,7 +129,6 @@
 use "Tools/quickcheck_generators.ML"
 setup Quickcheck_Generators.setup
 
-declare [[quickcheck_tester = random]]
 
 subsection {* Code setup *}
 
--- a/src/HOL/Sum_Type.thy	Mon Dec 06 11:41:24 2010 +0100
+++ b/src/HOL/Sum_Type.thy	Mon Dec 06 13:17:26 2010 +0100
@@ -95,7 +95,7 @@
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
 
-type_mapper sum_map proof -
+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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/type_lifting.ML	Mon Dec 06 13:17:26 2010 +0100
@@ -0,0 +1,217 @@
+(*  Title:      HOL/Tools/type_lifting.ML
+    Author:     Florian Haftmann, TU Muenchen
+
+Functorial structure of types.
+*)
+
+signature TYPE_LIFTING =
+sig
+  val find_atomic: theory -> typ -> (typ * (bool * bool)) list
+  val construct_mapper: theory -> (string * bool -> term)
+    -> bool -> typ -> typ -> term
+  val type_lifting: string option -> term -> theory -> Proof.state
+  type entry
+  val entries: theory -> entry Symtab.table
+end;
+
+structure Type_Lifting : TYPE_LIFTING =
+struct
+
+val compositionalityN = "compositionality";
+val identityN = "identity";
+
+(** functorial mappers and their properties **)
+
+(* bookkeeping *)
+
+type entry = { mapper: string, variances: (sort * (bool * bool)) list,
+  compositionality: thm, identity: thm };
+
+structure Data = Theory_Data(
+  type T = entry Symtab.table
+  val empty = Symtab.empty
+  fun merge (xy : T * T) = Symtab.merge (K true) xy
+  val extend = I
+);
+
+val entries = Data.get;
+
+
+(* type analysis *)
+
+fun find_atomic thy T =
+  let
+    val variances_of = Option.map #variances o Symtab.lookup (Data.get thy);
+    fun add_variance is_contra T =
+      AList.map_default (op =) (T, (false, false))
+        ((if is_contra then apsnd else apfst) (K true));
+    fun analyze' is_contra (_, (co, contra)) T =
+      (if co then analyze is_contra T else I)
+      #> (if contra then analyze (not is_contra) T else I)
+    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
+          of NONE => add_variance is_contra T
+           | SOME variances => fold2 (analyze' is_contra) variances Ts)
+      | analyze is_contra T = add_variance is_contra T;
+  in analyze false T [] end;
+
+fun construct_mapper thy atomic =
+  let
+    val lookup = the o Symtab.lookup (Data.get thy);
+    fun constructs is_contra (_, (co, contra)) T T' =
+      (if co then [construct is_contra T T'] else [])
+      @ (if contra then [construct (not is_contra) T T'] else [])
+    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
+          let
+            val { mapper, variances, ... } = lookup tyco;
+            val args = maps (fn (arg_pattern, (T, T')) =>
+              constructs is_contra arg_pattern T T')
+                (variances ~~ (Ts ~~ Ts'));
+            val (U, U') = if is_contra then (T', T) else (T, T');
+          in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end
+      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
+  in construct end;
+
+
+(* mapper properties *)
+
+fun make_compositionality_prop 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 (((vs1, vs2), vs3), _) = 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);
+    fun mk_argT ((T, T'), (_, (co, contra))) =
+      (if co then [(T --> T')] else [])
+      @ (if contra then [(T' --> T)] else []);
+    val contras = maps (fn (_, (co, contra)) =>
+      (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
+      |> 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))
+      else
+        Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
+      ) 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;
+
+fun make_identity_prop 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;
+    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;
+
+
+(* analyzing and registering mappers *)
+
+fun consume eq x [] = (false, [])
+  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
+
+fun split_mapper_typ "fun" T =
+      let
+        val (Ts', T') = strip_type T;
+        val (Ts'', T'') = split_last Ts';
+        val (Ts''', T''') = split_last Ts'';
+      in (Ts''', T''', T'' --> T') end
+  | split_mapper_typ tyco T =
+      let
+        val (Ts', T') = strip_type T;
+        val (Ts'', T'') = split_last Ts';
+      in (Ts'', T'', T') end;
+
+fun analyze_variances thy tyco T =
+  let
+    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T);
+    val (Ts, T1, T2) = split_mapper_typ tyco T
+      handle List.Empty => bad_typ ();
+    val _ = pairself
+      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
+    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
+      handle TYPE _ => bad_typ ();
+    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
+      then bad_typ () else ();
+    fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) =
+      let
+        val coT = TFree var1 --> TFree var2;
+        val contraT = TFree var2 --> TFree var1;
+        val sort = Sign.inter_sort thy (sort1, sort2);
+      in
+        consume (op =) coT
+        ##>> consume (op =) contraT
+        #>> pair sort
+      end;
+    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
+    val _ = if null left_variances then () else bad_typ ();
+  in variances end;
+
+fun gen_type_lifting prep_term some_prfx raw_t thy =
+  let
+    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;
+    val tycos = add_tycos T [];
+    val tyco = if tycos = ["fun"] then "fun"
+      else case remove (op =) "fun" tycos
+       of [tyco] => tyco
+        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
+    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 qualify = Binding.qualify true prfx o Binding.name;
+    fun after_qed [single_compositionality, single_identity] 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)
+            (Symtab.update (tyco, { mapper = mapper, variances = variances,
+              compositionality = compositionality, identity = identity })));
+  in
+    thy
+    |> Named_Target.theory_init
+    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
+  end
+
+val type_lifting = gen_type_lifting Sign.cert_term;
+val type_lifting_cmd = gen_type_lifting Syntax.read_term_global;
+
+val _ =
+  Outer_Syntax.command "type_lifting" "register operations managing the functorial structure of a type" Keyword.thy_goal
+    (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
+      >> (fn (prfx, t) => Toplevel.print o (Toplevel.theory_to_proof (type_lifting_cmd prfx t))));
+
+end;
--- a/src/HOL/Tools/type_mapper.ML	Mon Dec 06 11:41:24 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,217 +0,0 @@
-(*  Title:      HOL/Tools/type_mapper.ML
-    Author:     Florian Haftmann, TU Muenchen
-
-Functorial mappers on types.
-*)
-
-signature TYPE_MAPPER =
-sig
-  val find_atomic: theory -> typ -> (typ * (bool * bool)) list
-  val construct_mapper: theory -> (string * bool -> term)
-    -> bool -> typ -> typ -> term
-  val type_mapper: string option -> term -> theory -> Proof.state
-  type entry
-  val entries: theory -> entry Symtab.table
-end;
-
-structure Type_Mapper : TYPE_MAPPER =
-struct
-
-val compositionalityN = "compositionality";
-val identityN = "identity";
-
-(** functorial mappers and their properties **)
-
-(* bookkeeping *)
-
-type entry = { mapper: string, variances: (sort * (bool * bool)) list,
-  compositionality: thm, identity: thm };
-
-structure Data = Theory_Data(
-  type T = entry Symtab.table
-  val empty = Symtab.empty
-  fun merge (xy : T * T) = Symtab.merge (K true) xy
-  val extend = I
-);
-
-val entries = Data.get;
-
-
-(* type analysis *)
-
-fun find_atomic thy T =
-  let
-    val variances_of = Option.map #variances o Symtab.lookup (Data.get thy);
-    fun add_variance is_contra T =
-      AList.map_default (op =) (T, (false, false))
-        ((if is_contra then apsnd else apfst) (K true));
-    fun analyze' is_contra (_, (co, contra)) T =
-      (if co then analyze is_contra T else I)
-      #> (if contra then analyze (not is_contra) T else I)
-    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
-          of NONE => add_variance is_contra T
-           | SOME variances => fold2 (analyze' is_contra) variances Ts)
-      | analyze is_contra T = add_variance is_contra T;
-  in analyze false T [] end;
-
-fun construct_mapper thy atomic =
-  let
-    val lookup = the o Symtab.lookup (Data.get thy);
-    fun constructs is_contra (_, (co, contra)) T T' =
-      (if co then [construct is_contra T T'] else [])
-      @ (if contra then [construct (not is_contra) T T'] else [])
-    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
-          let
-            val { mapper, variances, ... } = lookup tyco;
-            val args = maps (fn (arg_pattern, (T, T')) =>
-              constructs is_contra arg_pattern T T')
-                (variances ~~ (Ts ~~ Ts'));
-            val (U, U') = if is_contra then (T', T) else (T, T');
-          in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end
-      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
-  in construct end;
-
-
-(* mapper properties *)
-
-fun make_compositionality_prop 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 (((vs1, vs2), vs3), _) = 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);
-    fun mk_argT ((T, T'), (_, (co, contra))) =
-      (if co then [(T --> T')] else [])
-      @ (if contra then [(T' --> T)] else []);
-    val contras = maps (fn (_, (co, contra)) =>
-      (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
-      |> 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))
-      else
-        Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
-      ) 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;
-
-fun make_identity_prop 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;
-    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;
-
-
-(* analyzing and registering mappers *)
-
-fun consume eq x [] = (false, [])
-  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
-
-fun split_mapper_typ "fun" T =
-      let
-        val (Ts', T') = strip_type T;
-        val (Ts'', T'') = split_last Ts';
-        val (Ts''', T''') = split_last Ts'';
-      in (Ts''', T''', T'' --> T') end
-  | split_mapper_typ tyco T =
-      let
-        val (Ts', T') = strip_type T;
-        val (Ts'', T'') = split_last Ts';
-      in (Ts'', T'', T') end;
-
-fun analyze_variances thy tyco T =
-  let
-    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T);
-    val (Ts, T1, T2) = split_mapper_typ tyco T
-      handle List.Empty => bad_typ ();
-    val _ = pairself
-      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
-    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
-      handle TYPE _ => bad_typ ();
-    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
-      then bad_typ () else ();
-    fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) =
-      let
-        val coT = TFree var1 --> TFree var2;
-        val contraT = TFree var2 --> TFree var1;
-        val sort = Sign.inter_sort thy (sort1, sort2);
-      in
-        consume (op =) coT
-        ##>> consume (op =) contraT
-        #>> pair sort
-      end;
-    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
-    val _ = if null left_variances then () else bad_typ ();
-  in variances end;
-
-fun gen_type_mapper prep_term some_prfx raw_t thy =
-  let
-    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;
-    val tycos = add_tycos T [];
-    val tyco = if tycos = ["fun"] then "fun"
-      else case remove (op =) "fun" tycos
-       of [tyco] => tyco
-        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
-    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 qualify = Binding.qualify true prfx o Binding.name;
-    fun after_qed [single_compositionality, single_identity] 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)
-            (Symtab.update (tyco, { mapper = mapper, variances = variances,
-              compositionality = compositionality, identity = identity })));
-  in
-    thy
-    |> Named_Target.theory_init
-    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
-  end
-
-val type_mapper = gen_type_mapper Sign.cert_term;
-val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
-
-val _ =
-  Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
-    (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
-      >> (fn (prfx, t) => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd prfx t))));
-
-end;