file for package tool type_mapper carries the same name as its Isar command
authorhaftmann
Wed Dec 01 11:33:17 2010 +0100 (2010-12-01)
changeset 40855149dcaa26728
parent 40835 fc750e794458
child 40856 3ad8a5925ba4
file for package tool type_mapper carries the same name as its Isar command
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Tools/functorial_mappers.ML
src/HOL/Tools/type_mapper.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Nov 30 20:02:01 2010 -0800
     1.2 +++ b/src/HOL/HOL.thy	Wed Dec 01 11:33:17 2010 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4    "Tools/async_manager.ML"
     1.5    "Tools/try.ML"
     1.6    ("Tools/cnf_funcs.ML")
     1.7 -  ("Tools/functorial_mappers.ML")
     1.8 +  ("Tools/type_mapper.ML")
     1.9  begin
    1.10  
    1.11  setup {* Intuitionistic.method_setup @{binding iprover} *}
    1.12 @@ -712,7 +712,7 @@
    1.13    and [Pure.elim?] = iffD1 iffD2 impE
    1.14  
    1.15  use "Tools/hologic.ML"
    1.16 -use "Tools/functorial_mappers.ML"
    1.17 +use "Tools/type_mapper.ML"
    1.18  
    1.19  
    1.20  subsubsection {* Atomizing meta-level connectives *}
     2.1 --- a/src/HOL/IsaMakefile	Tue Nov 30 20:02:01 2010 -0800
     2.2 +++ b/src/HOL/IsaMakefile	Wed Dec 01 11:33:17 2010 +0100
     2.3 @@ -147,7 +147,7 @@
     2.4    $(SRC)/Tools/solve_direct.ML \
     2.5    $(SRC)/Tools/value.ML \
     2.6    HOL.thy \
     2.7 -  Tools/functorial_mappers.ML \
     2.8 +  Tools/type_mapper.ML \
     2.9    Tools/hologic.ML \
    2.10    Tools/recfun_codegen.ML \
    2.11    Tools/simpdata.ML
     3.1 --- a/src/HOL/Tools/functorial_mappers.ML	Tue Nov 30 20:02:01 2010 -0800
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,215 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/functorial_mappers.ML
     3.5 -    Author:     Florian Haftmann, TU Muenchen
     3.6 -
     3.7 -Functorial mappers on types.
     3.8 -*)
     3.9 -
    3.10 -signature FUNCTORIAL_MAPPERS =
    3.11 -sig
    3.12 -  val find_atomic: theory -> typ -> (typ * (bool * bool)) list
    3.13 -  val construct_mapper: theory -> (string * bool -> term)
    3.14 -    -> bool -> typ -> typ -> term
    3.15 -  val type_mapper: term -> theory -> Proof.state
    3.16 -  type entry
    3.17 -  val entries: theory -> entry Symtab.table
    3.18 -end;
    3.19 -
    3.20 -structure Functorial_Mappers : FUNCTORIAL_MAPPERS =
    3.21 -struct
    3.22 -
    3.23 -val compositionalityN = "compositionality";
    3.24 -val identityN = "identity";
    3.25 -
    3.26 -(** functorial mappers and their properties **)
    3.27 -
    3.28 -(* bookkeeping *)
    3.29 -
    3.30 -type entry = { mapper: string, variances: (sort * (bool * bool)) list,
    3.31 -  compositionality: thm, identity: thm };
    3.32 -
    3.33 -structure Data = Theory_Data(
    3.34 -  type T = entry Symtab.table
    3.35 -  val empty = Symtab.empty
    3.36 -  fun merge (xy : T * T) = Symtab.merge (K true) xy
    3.37 -  val extend = I
    3.38 -);
    3.39 -
    3.40 -val entries = Data.get;
    3.41 -
    3.42 -
    3.43 -(* type analysis *)
    3.44 -
    3.45 -fun find_atomic thy T =
    3.46 -  let
    3.47 -    val variances_of = Option.map #variances o Symtab.lookup (Data.get thy);
    3.48 -    fun add_variance is_contra T =
    3.49 -      AList.map_default (op =) (T, (false, false))
    3.50 -        ((if is_contra then apsnd else apfst) (K true));
    3.51 -    fun analyze' is_contra (_, (co, contra)) T =
    3.52 -      (if co then analyze is_contra T else I)
    3.53 -      #> (if contra then analyze (not is_contra) T else I)
    3.54 -    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
    3.55 -          of NONE => add_variance is_contra T
    3.56 -           | SOME variances => fold2 (analyze' is_contra) variances Ts)
    3.57 -      | analyze is_contra T = add_variance is_contra T;
    3.58 -  in analyze false T [] end;
    3.59 -
    3.60 -fun construct_mapper thy atomic =
    3.61 -  let
    3.62 -    val lookup = the o Symtab.lookup (Data.get thy);
    3.63 -    fun constructs is_contra (_, (co, contra)) T T' =
    3.64 -      (if co then [construct is_contra T T'] else [])
    3.65 -      @ (if contra then [construct (not is_contra) T T'] else [])
    3.66 -    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
    3.67 -          let
    3.68 -            val { mapper, variances, ... } = lookup tyco;
    3.69 -            val args = maps (fn (arg_pattern, (T, T')) =>
    3.70 -              constructs is_contra arg_pattern T T')
    3.71 -                (variances ~~ (Ts ~~ Ts'));
    3.72 -            val (U, U') = if is_contra then (T', T) else (T, T');
    3.73 -          in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end
    3.74 -      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
    3.75 -  in construct end;
    3.76 -
    3.77 -
    3.78 -(* mapper properties *)
    3.79 -
    3.80 -fun make_compositionality_prop variances (tyco, mapper) =
    3.81 -  let
    3.82 -    fun invents n k nctxt =
    3.83 -      let
    3.84 -        val names = Name.invents nctxt n k;
    3.85 -      in (names, fold Name.declare names nctxt) end;
    3.86 -    val (((vs1, vs2), vs3), _) = Name.context
    3.87 -      |> invents Name.aT (length variances)
    3.88 -      ||>> invents Name.aT (length variances)
    3.89 -      ||>> invents Name.aT (length variances);
    3.90 -    fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
    3.91 -      vs variances;
    3.92 -    val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3);
    3.93 -    fun mk_argT ((T, T'), (_, (co, contra))) =
    3.94 -      (if co then [(T --> T')] else [])
    3.95 -      @ (if contra then [(T' --> T)] else []);
    3.96 -    val contras = maps (fn (_, (co, contra)) =>
    3.97 -      (if co then [false] else []) @ (if contra then [true] else [])) variances;
    3.98 -    val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
    3.99 -    val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
   3.100 -    val ((names21, names32), nctxt) = Name.context
   3.101 -      |> invents "f" (length Ts21)
   3.102 -      ||>> invents "f" (length Ts32);
   3.103 -    val T1 = Type (tyco, Ts1);
   3.104 -    val T2 = Type (tyco, Ts2);
   3.105 -    val T3 = Type (tyco, Ts3);
   3.106 -    val x = Free (the_single (Name.invents nctxt "a" 1), T3);
   3.107 -    val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
   3.108 -    val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
   3.109 -      if not is_contra then
   3.110 -        Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0))
   3.111 -      else
   3.112 -        Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
   3.113 -      ) contras (args21 ~~ args32)
   3.114 -    fun mk_mapper T T' args = list_comb (Const (mapper,
   3.115 -      map fastype_of args ---> T --> T'), args);
   3.116 -    val lhs = mk_mapper T2 T1 (map Free args21) $
   3.117 -      (mk_mapper T3 T2 (map Free args32) $ x);
   3.118 -    val rhs = mk_mapper T3 T1 args31 $ x;
   3.119 -  in (map Free (args21 @ args32) @ [x], (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
   3.120 -
   3.121 -fun make_identity_prop variances (tyco, mapper) =
   3.122 -  let
   3.123 -    val vs = Name.invents Name.context Name.aT (length variances);
   3.124 -    val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances;
   3.125 -    fun bool_num b = if b then 1 else 0;
   3.126 -    fun mk_argT (T, (_, (co, contra))) =
   3.127 -      replicate (bool_num co + bool_num contra) (T --> T)
   3.128 -    val Ts' = maps mk_argT (Ts ~~ variances)
   3.129 -    val T = Type (tyco, Ts);
   3.130 -    val x = Free ("a", T);
   3.131 -    val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
   3.132 -      map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
   3.133 -  in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;
   3.134 -
   3.135 -
   3.136 -(* analyzing and registering mappers *)
   3.137 -
   3.138 -fun consume eq x [] = (false, [])
   3.139 -  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
   3.140 -
   3.141 -fun split_mapper_typ "fun" T =
   3.142 -      let
   3.143 -        val (Ts', T') = strip_type T;
   3.144 -        val (Ts'', T'') = split_last Ts';
   3.145 -        val (Ts''', T''') = split_last Ts'';
   3.146 -      in (Ts''', T''', T'' --> T') end
   3.147 -  | split_mapper_typ tyco T =
   3.148 -      let
   3.149 -        val (Ts', T') = strip_type T;
   3.150 -        val (Ts'', T'') = split_last Ts';
   3.151 -      in (Ts'', T'', T') end;
   3.152 -
   3.153 -fun analyze_variances thy tyco T =
   3.154 -  let
   3.155 -    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T);
   3.156 -    val (Ts, T1, T2) = split_mapper_typ tyco T
   3.157 -      handle List.Empty => bad_typ ();
   3.158 -    val _ = pairself
   3.159 -      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
   3.160 -    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
   3.161 -      handle TYPE _ => bad_typ ();
   3.162 -    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
   3.163 -      then bad_typ () else ();
   3.164 -    fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) =
   3.165 -      let
   3.166 -        val coT = TFree var1 --> TFree var2;
   3.167 -        val contraT = TFree var2 --> TFree var1;
   3.168 -        val sort = Sign.inter_sort thy (sort1, sort2);
   3.169 -      in
   3.170 -        consume (op =) coT
   3.171 -        ##>> consume (op =) contraT
   3.172 -        #>> pair sort
   3.173 -      end;
   3.174 -    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
   3.175 -    val _ = if null left_variances then () else bad_typ ();
   3.176 -  in variances end;
   3.177 -
   3.178 -fun gen_type_mapper prep_term raw_t thy =
   3.179 -  let
   3.180 -    val (mapper, T) = case prep_term thy raw_t
   3.181 -     of Const cT => cT
   3.182 -      | t => error ("No constant: " ^ Syntax.string_of_term_global thy t);
   3.183 -    val _ = Type.no_tvars T;
   3.184 -    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
   3.185 -      | add_tycos _ = I;
   3.186 -    val tycos = add_tycos T [];
   3.187 -    val tyco = if tycos = ["fun"] then "fun"
   3.188 -      else case remove (op =) "fun" tycos
   3.189 -       of [tyco] => tyco
   3.190 -        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
   3.191 -    val variances = analyze_variances thy tyco T;
   3.192 -    val compositionality_prop = uncurry (fold_rev Logic.all)
   3.193 -      (make_compositionality_prop variances (tyco, mapper));
   3.194 -    val identity_prop = uncurry Logic.all
   3.195 -      (make_identity_prop variances (tyco, mapper));
   3.196 -    val qualify = Binding.qualify true (Long_Name.base_name mapper) o Binding.name;
   3.197 -    fun after_qed [single_compositionality, single_identity] lthy =
   3.198 -      lthy
   3.199 -      |> Local_Theory.note ((qualify compositionalityN, []), single_compositionality)
   3.200 -      ||>> Local_Theory.note ((qualify identityN, []), single_identity)
   3.201 -      |-> (fn ((_, [compositionality]), (_, [identity])) =>
   3.202 -          (Local_Theory.background_theory o Data.map)
   3.203 -            (Symtab.update (tyco, { mapper = mapper, variances = variances,
   3.204 -              compositionality = compositionality, identity = identity })));
   3.205 -  in
   3.206 -    thy
   3.207 -    |> Named_Target.theory_init
   3.208 -    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
   3.209 -  end
   3.210 -
   3.211 -val type_mapper = gen_type_mapper Sign.cert_term;
   3.212 -val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
   3.213 -
   3.214 -val _ =
   3.215 -  Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
   3.216 -    (Parse.term >> (fn t => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd t))));
   3.217 -
   3.218 -end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/type_mapper.ML	Wed Dec 01 11:33:17 2010 +0100
     4.3 @@ -0,0 +1,215 @@
     4.4 +(*  Title:      HOL/Tools/type_mapper.ML
     4.5 +    Author:     Florian Haftmann, TU Muenchen
     4.6 +
     4.7 +Functorial mappers on types.
     4.8 +*)
     4.9 +
    4.10 +signature TYPE_MAPPER =
    4.11 +sig
    4.12 +  val find_atomic: theory -> typ -> (typ * (bool * bool)) list
    4.13 +  val construct_mapper: theory -> (string * bool -> term)
    4.14 +    -> bool -> typ -> typ -> term
    4.15 +  val type_mapper: term -> theory -> Proof.state
    4.16 +  type entry
    4.17 +  val entries: theory -> entry Symtab.table
    4.18 +end;
    4.19 +
    4.20 +structure Type_Mapper : TYPE_MAPPER =
    4.21 +struct
    4.22 +
    4.23 +val compositionalityN = "compositionality";
    4.24 +val identityN = "identity";
    4.25 +
    4.26 +(** functorial mappers and their properties **)
    4.27 +
    4.28 +(* bookkeeping *)
    4.29 +
    4.30 +type entry = { mapper: string, variances: (sort * (bool * bool)) list,
    4.31 +  compositionality: thm, identity: thm };
    4.32 +
    4.33 +structure Data = Theory_Data(
    4.34 +  type T = entry Symtab.table
    4.35 +  val empty = Symtab.empty
    4.36 +  fun merge (xy : T * T) = Symtab.merge (K true) xy
    4.37 +  val extend = I
    4.38 +);
    4.39 +
    4.40 +val entries = Data.get;
    4.41 +
    4.42 +
    4.43 +(* type analysis *)
    4.44 +
    4.45 +fun find_atomic thy T =
    4.46 +  let
    4.47 +    val variances_of = Option.map #variances o Symtab.lookup (Data.get thy);
    4.48 +    fun add_variance is_contra T =
    4.49 +      AList.map_default (op =) (T, (false, false))
    4.50 +        ((if is_contra then apsnd else apfst) (K true));
    4.51 +    fun analyze' is_contra (_, (co, contra)) T =
    4.52 +      (if co then analyze is_contra T else I)
    4.53 +      #> (if contra then analyze (not is_contra) T else I)
    4.54 +    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
    4.55 +          of NONE => add_variance is_contra T
    4.56 +           | SOME variances => fold2 (analyze' is_contra) variances Ts)
    4.57 +      | analyze is_contra T = add_variance is_contra T;
    4.58 +  in analyze false T [] end;
    4.59 +
    4.60 +fun construct_mapper thy atomic =
    4.61 +  let
    4.62 +    val lookup = the o Symtab.lookup (Data.get thy);
    4.63 +    fun constructs is_contra (_, (co, contra)) T T' =
    4.64 +      (if co then [construct is_contra T T'] else [])
    4.65 +      @ (if contra then [construct (not is_contra) T T'] else [])
    4.66 +    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
    4.67 +          let
    4.68 +            val { mapper, variances, ... } = lookup tyco;
    4.69 +            val args = maps (fn (arg_pattern, (T, T')) =>
    4.70 +              constructs is_contra arg_pattern T T')
    4.71 +                (variances ~~ (Ts ~~ Ts'));
    4.72 +            val (U, U') = if is_contra then (T', T) else (T, T');
    4.73 +          in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end
    4.74 +      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
    4.75 +  in construct end;
    4.76 +
    4.77 +
    4.78 +(* mapper properties *)
    4.79 +
    4.80 +fun make_compositionality_prop variances (tyco, mapper) =
    4.81 +  let
    4.82 +    fun invents n k nctxt =
    4.83 +      let
    4.84 +        val names = Name.invents nctxt n k;
    4.85 +      in (names, fold Name.declare names nctxt) end;
    4.86 +    val (((vs1, vs2), vs3), _) = Name.context
    4.87 +      |> invents Name.aT (length variances)
    4.88 +      ||>> invents Name.aT (length variances)
    4.89 +      ||>> invents Name.aT (length variances);
    4.90 +    fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
    4.91 +      vs variances;
    4.92 +    val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3);
    4.93 +    fun mk_argT ((T, T'), (_, (co, contra))) =
    4.94 +      (if co then [(T --> T')] else [])
    4.95 +      @ (if contra then [(T' --> T)] else []);
    4.96 +    val contras = maps (fn (_, (co, contra)) =>
    4.97 +      (if co then [false] else []) @ (if contra then [true] else [])) variances;
    4.98 +    val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
    4.99 +    val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
   4.100 +    val ((names21, names32), nctxt) = Name.context
   4.101 +      |> invents "f" (length Ts21)
   4.102 +      ||>> invents "f" (length Ts32);
   4.103 +    val T1 = Type (tyco, Ts1);
   4.104 +    val T2 = Type (tyco, Ts2);
   4.105 +    val T3 = Type (tyco, Ts3);
   4.106 +    val x = Free (the_single (Name.invents nctxt "a" 1), T3);
   4.107 +    val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
   4.108 +    val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
   4.109 +      if not is_contra then
   4.110 +        Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0))
   4.111 +      else
   4.112 +        Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
   4.113 +      ) contras (args21 ~~ args32)
   4.114 +    fun mk_mapper T T' args = list_comb (Const (mapper,
   4.115 +      map fastype_of args ---> T --> T'), args);
   4.116 +    val lhs = mk_mapper T2 T1 (map Free args21) $
   4.117 +      (mk_mapper T3 T2 (map Free args32) $ x);
   4.118 +    val rhs = mk_mapper T3 T1 args31 $ x;
   4.119 +  in (map Free (args21 @ args32) @ [x], (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
   4.120 +
   4.121 +fun make_identity_prop variances (tyco, mapper) =
   4.122 +  let
   4.123 +    val vs = Name.invents Name.context Name.aT (length variances);
   4.124 +    val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances;
   4.125 +    fun bool_num b = if b then 1 else 0;
   4.126 +    fun mk_argT (T, (_, (co, contra))) =
   4.127 +      replicate (bool_num co + bool_num contra) (T --> T)
   4.128 +    val Ts' = maps mk_argT (Ts ~~ variances)
   4.129 +    val T = Type (tyco, Ts);
   4.130 +    val x = Free ("a", T);
   4.131 +    val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
   4.132 +      map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
   4.133 +  in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;
   4.134 +
   4.135 +
   4.136 +(* analyzing and registering mappers *)
   4.137 +
   4.138 +fun consume eq x [] = (false, [])
   4.139 +  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
   4.140 +
   4.141 +fun split_mapper_typ "fun" T =
   4.142 +      let
   4.143 +        val (Ts', T') = strip_type T;
   4.144 +        val (Ts'', T'') = split_last Ts';
   4.145 +        val (Ts''', T''') = split_last Ts'';
   4.146 +      in (Ts''', T''', T'' --> T') end
   4.147 +  | split_mapper_typ tyco T =
   4.148 +      let
   4.149 +        val (Ts', T') = strip_type T;
   4.150 +        val (Ts'', T'') = split_last Ts';
   4.151 +      in (Ts'', T'', T') end;
   4.152 +
   4.153 +fun analyze_variances thy tyco T =
   4.154 +  let
   4.155 +    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T);
   4.156 +    val (Ts, T1, T2) = split_mapper_typ tyco T
   4.157 +      handle List.Empty => bad_typ ();
   4.158 +    val _ = pairself
   4.159 +      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
   4.160 +    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
   4.161 +      handle TYPE _ => bad_typ ();
   4.162 +    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
   4.163 +      then bad_typ () else ();
   4.164 +    fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) =
   4.165 +      let
   4.166 +        val coT = TFree var1 --> TFree var2;
   4.167 +        val contraT = TFree var2 --> TFree var1;
   4.168 +        val sort = Sign.inter_sort thy (sort1, sort2);
   4.169 +      in
   4.170 +        consume (op =) coT
   4.171 +        ##>> consume (op =) contraT
   4.172 +        #>> pair sort
   4.173 +      end;
   4.174 +    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
   4.175 +    val _ = if null left_variances then () else bad_typ ();
   4.176 +  in variances end;
   4.177 +
   4.178 +fun gen_type_mapper prep_term raw_t thy =
   4.179 +  let
   4.180 +    val (mapper, T) = case prep_term thy raw_t
   4.181 +     of Const cT => cT
   4.182 +      | t => error ("No constant: " ^ Syntax.string_of_term_global thy t);
   4.183 +    val _ = Type.no_tvars T;
   4.184 +    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
   4.185 +      | add_tycos _ = I;
   4.186 +    val tycos = add_tycos T [];
   4.187 +    val tyco = if tycos = ["fun"] then "fun"
   4.188 +      else case remove (op =) "fun" tycos
   4.189 +       of [tyco] => tyco
   4.190 +        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
   4.191 +    val variances = analyze_variances thy tyco T;
   4.192 +    val compositionality_prop = uncurry (fold_rev Logic.all)
   4.193 +      (make_compositionality_prop variances (tyco, mapper));
   4.194 +    val identity_prop = uncurry Logic.all
   4.195 +      (make_identity_prop variances (tyco, mapper));
   4.196 +    val qualify = Binding.qualify true (Long_Name.base_name mapper) o Binding.name;
   4.197 +    fun after_qed [single_compositionality, single_identity] lthy =
   4.198 +      lthy
   4.199 +      |> Local_Theory.note ((qualify compositionalityN, []), single_compositionality)
   4.200 +      ||>> Local_Theory.note ((qualify identityN, []), single_identity)
   4.201 +      |-> (fn ((_, [compositionality]), (_, [identity])) =>
   4.202 +          (Local_Theory.background_theory o Data.map)
   4.203 +            (Symtab.update (tyco, { mapper = mapper, variances = variances,
   4.204 +              compositionality = compositionality, identity = identity })));
   4.205 +  in
   4.206 +    thy
   4.207 +    |> Named_Target.theory_init
   4.208 +    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
   4.209 +  end
   4.210 +
   4.211 +val type_mapper = gen_type_mapper Sign.cert_term;
   4.212 +val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
   4.213 +
   4.214 +val _ =
   4.215 +  Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
   4.216 +    (Parse.term >> (fn t => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd t))));
   4.217 +
   4.218 +end;