1.1 --- a/src/HOL/HOL.thy Wed Dec 01 06:50:54 2010 -0800
1.2 +++ b/src/HOL/HOL.thy Wed Dec 01 18:00:40 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 Wed Dec 01 06:50:54 2010 -0800
2.2 +++ b/src/HOL/IsaMakefile Wed Dec 01 18:00:40 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 Wed Dec 01 06:50:54 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 18:00:40 2010 +0100
4.3 @@ -0,0 +1,217 @@
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: string option -> 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 (Long_Name.base_name tyco) 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 (Long_Name.base_name tyco, 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 some_prfx 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 prfx = the_default (Long_Name.base_name mapper) some_prfx;
4.184 + val _ = Type.no_tvars T;
4.185 + fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
4.186 + | add_tycos _ = I;
4.187 + val tycos = add_tycos T [];
4.188 + val tyco = if tycos = ["fun"] then "fun"
4.189 + else case remove (op =) "fun" tycos
4.190 + of [tyco] => tyco
4.191 + | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
4.192 + val variances = analyze_variances thy tyco T;
4.193 + val compositionality_prop = uncurry (fold_rev Logic.all)
4.194 + (make_compositionality_prop variances (tyco, mapper));
4.195 + val identity_prop = uncurry Logic.all
4.196 + (make_identity_prop variances (tyco, mapper));
4.197 + val qualify = Binding.qualify true prfx o Binding.name;
4.198 + fun after_qed [single_compositionality, single_identity] lthy =
4.199 + lthy
4.200 + |> Local_Theory.note ((qualify compositionalityN, []), single_compositionality)
4.201 + ||>> Local_Theory.note ((qualify identityN, []), single_identity)
4.202 + |-> (fn ((_, [compositionality]), (_, [identity])) =>
4.203 + (Local_Theory.background_theory o Data.map)
4.204 + (Symtab.update (tyco, { mapper = mapper, variances = variances,
4.205 + compositionality = compositionality, identity = identity })));
4.206 + in
4.207 + thy
4.208 + |> Named_Target.theory_init
4.209 + |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
4.210 + end
4.211 +
4.212 +val type_mapper = gen_type_mapper Sign.cert_term;
4.213 +val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
4.214 +
4.215 +val _ =
4.216 + Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
4.217 + (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
4.218 + >> (fn (prfx, t) => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd prfx t))));
4.219 +
4.220 +end;