replace `type_mapper` by the more adequate `type_lifting`
authorhaftmann
Mon Dec 06 09:19:10 2010 +0100 (2010-12-06)
changeset 40968a6fcd305f7dc
parent 40965 54b6c9e1c157
child 40969 fb2d3ccda5a7
replace `type_mapper` by the more adequate `type_lifting`
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Library/Cset.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Multiset.thy
src/HOL/List.thy
src/HOL/Option.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/type_lifting.ML
src/HOL/Tools/type_mapper.ML
     1.1 --- a/src/HOL/Fun.thy	Sun Dec 05 14:02:16 2010 +0100
     1.2 +++ b/src/HOL/Fun.thy	Mon Dec 06 09:19:10 2010 +0100
     1.3 @@ -126,7 +126,7 @@
     1.4    "map_fun f g h x = g (h (f x))"
     1.5    by (simp add: map_fun_def)
     1.6  
     1.7 -type_mapper map_fun
     1.8 +type_lifting map_fun
     1.9    by (simp_all add: fun_eq_iff)
    1.10  
    1.11  
     2.1 --- a/src/HOL/HOL.thy	Sun Dec 05 14:02:16 2010 +0100
     2.2 +++ b/src/HOL/HOL.thy	Mon Dec 06 09:19:10 2010 +0100
     2.3 @@ -32,7 +32,7 @@
     2.4    "Tools/async_manager.ML"
     2.5    "Tools/try.ML"
     2.6    ("Tools/cnf_funcs.ML")
     2.7 -  ("Tools/type_mapper.ML")
     2.8 +  ("Tools/type_lifting.ML")
     2.9    "~~/src/Tools/subtyping.ML"
    2.10  begin
    2.11  
    2.12 @@ -714,7 +714,7 @@
    2.13    and [Pure.elim?] = iffD1 iffD2 impE
    2.14  
    2.15  use "Tools/hologic.ML"
    2.16 -use "Tools/type_mapper.ML"
    2.17 +use "Tools/type_lifting.ML"
    2.18  
    2.19  
    2.20  subsubsection {* Atomizing meta-level connectives *}
     3.1 --- a/src/HOL/IsaMakefile	Sun Dec 05 14:02:16 2010 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Mon Dec 06 09:19:10 2010 +0100
     3.3 @@ -147,7 +147,7 @@
     3.4    $(SRC)/Tools/solve_direct.ML \
     3.5    $(SRC)/Tools/value.ML \
     3.6    HOL.thy \
     3.7 -  Tools/type_mapper.ML \
     3.8 +  Tools/type_lifting.ML \
     3.9    Tools/hologic.ML \
    3.10    Tools/recfun_codegen.ML \
    3.11    Tools/simpdata.ML
     4.1 --- a/src/HOL/Library/Cset.thy	Sun Dec 05 14:02:16 2010 +0100
     4.2 +++ b/src/HOL/Library/Cset.thy	Mon Dec 06 09:19:10 2010 +0100
     4.3 @@ -188,7 +188,7 @@
     4.4    "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
     4.5    by (simp add: set_def)
     4.6  
     4.7 -type_mapper map
     4.8 +type_lifting map
     4.9    by (simp_all add: image_image)
    4.10  
    4.11  definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
     5.1 --- a/src/HOL/Library/Dlist.thy	Sun Dec 05 14:02:16 2010 +0100
     5.2 +++ b/src/HOL/Library/Dlist.thy	Mon Dec 06 09:19:10 2010 +0100
     5.3 @@ -175,7 +175,7 @@
     5.4  
     5.5  section {* Functorial structure *}
     5.6  
     5.7 -type_mapper map
     5.8 +type_lifting map
     5.9    by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
    5.10  
    5.11  
     6.1 --- a/src/HOL/Library/Mapping.thy	Sun Dec 05 14:02:16 2010 +0100
     6.2 +++ b/src/HOL/Library/Mapping.thy	Mon Dec 06 09:19:10 2010 +0100
     6.3 @@ -50,7 +50,7 @@
     6.4    "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
     6.5    by (simp add: map_def)
     6.6  
     6.7 -type_mapper map
     6.8 +type_lifting map
     6.9    by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity)
    6.10  
    6.11  
     7.1 --- a/src/HOL/Library/Multiset.thy	Sun Dec 05 14:02:16 2010 +0100
     7.2 +++ b/src/HOL/Library/Multiset.thy	Mon Dec 06 09:19:10 2010 +0100
     7.3 @@ -1631,7 +1631,7 @@
     7.4    @{term "{#x+x|x:#M. x<c#}"}.
     7.5  *}
     7.6  
     7.7 -type_mapper image_mset proof -
     7.8 +type_lifting image_mset proof -
     7.9    fix f g A show "image_mset f (image_mset g A) = image_mset (\<lambda>x. f (g x)) A"
    7.10      by (induct A) simp_all
    7.11  next
     8.1 --- a/src/HOL/List.thy	Sun Dec 05 14:02:16 2010 +0100
     8.2 +++ b/src/HOL/List.thy	Mon Dec 06 09:19:10 2010 +0100
     8.3 @@ -881,7 +881,7 @@
     8.4    "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
     8.5  by (induct rule:list_induct2, simp_all)
     8.6  
     8.7 -type_mapper map
     8.8 +type_lifting map
     8.9    by simp_all
    8.10  
    8.11  
     9.1 --- a/src/HOL/Option.thy	Sun Dec 05 14:02:16 2010 +0100
     9.2 +++ b/src/HOL/Option.thy	Mon Dec 06 09:19:10 2010 +0100
     9.3 @@ -81,7 +81,7 @@
     9.4      "map f o sum_case g h = sum_case (map f o g) (map f o h)"
     9.5    by (rule ext) (simp split: sum.split)
     9.6  
     9.7 -type_mapper Option.map proof -
     9.8 +type_lifting Option.map proof -
     9.9    fix f g x
    9.10    show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x"
    9.11      by (cases x) simp_all
    10.1 --- a/src/HOL/Product_Type.thy	Sun Dec 05 14:02:16 2010 +0100
    10.2 +++ b/src/HOL/Product_Type.thy	Mon Dec 06 09:19:10 2010 +0100
    10.3 @@ -835,7 +835,7 @@
    10.4    "map_pair f g (a, b) = (f a, g b)"
    10.5    by (simp add: map_pair_def)
    10.6  
    10.7 -type_mapper map_pair
    10.8 +type_lifting map_pair
    10.9    by (simp_all add: split_paired_all)
   10.10  
   10.11  lemma fst_map_pair [simp]:
    11.1 --- a/src/HOL/Sum_Type.thy	Sun Dec 05 14:02:16 2010 +0100
    11.2 +++ b/src/HOL/Sum_Type.thy	Mon Dec 06 09:19:10 2010 +0100
    11.3 @@ -95,7 +95,7 @@
    11.4    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    11.5  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    11.6  
    11.7 -type_mapper sum_map proof -
    11.8 +type_lifting sum_map proof -
    11.9    fix f g h i s
   11.10    show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s"
   11.11      by (cases s) simp_all
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Tools/type_lifting.ML	Mon Dec 06 09:19:10 2010 +0100
    12.3 @@ -0,0 +1,217 @@
    12.4 +(*  Title:      HOL/Tools/type_lifting.ML
    12.5 +    Author:     Florian Haftmann, TU Muenchen
    12.6 +
    12.7 +Functorial structure of types.
    12.8 +*)
    12.9 +
   12.10 +signature TYPE_LIFTING =
   12.11 +sig
   12.12 +  val find_atomic: theory -> typ -> (typ * (bool * bool)) list
   12.13 +  val construct_mapper: theory -> (string * bool -> term)
   12.14 +    -> bool -> typ -> typ -> term
   12.15 +  val type_lifting: string option -> term -> theory -> Proof.state
   12.16 +  type entry
   12.17 +  val entries: theory -> entry Symtab.table
   12.18 +end;
   12.19 +
   12.20 +structure Type_Lifting : TYPE_LIFTING =
   12.21 +struct
   12.22 +
   12.23 +val compositionalityN = "compositionality";
   12.24 +val identityN = "identity";
   12.25 +
   12.26 +(** functorial mappers and their properties **)
   12.27 +
   12.28 +(* bookkeeping *)
   12.29 +
   12.30 +type entry = { mapper: string, variances: (sort * (bool * bool)) list,
   12.31 +  compositionality: thm, identity: thm };
   12.32 +
   12.33 +structure Data = Theory_Data(
   12.34 +  type T = entry Symtab.table
   12.35 +  val empty = Symtab.empty
   12.36 +  fun merge (xy : T * T) = Symtab.merge (K true) xy
   12.37 +  val extend = I
   12.38 +);
   12.39 +
   12.40 +val entries = Data.get;
   12.41 +
   12.42 +
   12.43 +(* type analysis *)
   12.44 +
   12.45 +fun find_atomic thy T =
   12.46 +  let
   12.47 +    val variances_of = Option.map #variances o Symtab.lookup (Data.get thy);
   12.48 +    fun add_variance is_contra T =
   12.49 +      AList.map_default (op =) (T, (false, false))
   12.50 +        ((if is_contra then apsnd else apfst) (K true));
   12.51 +    fun analyze' is_contra (_, (co, contra)) T =
   12.52 +      (if co then analyze is_contra T else I)
   12.53 +      #> (if contra then analyze (not is_contra) T else I)
   12.54 +    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
   12.55 +          of NONE => add_variance is_contra T
   12.56 +           | SOME variances => fold2 (analyze' is_contra) variances Ts)
   12.57 +      | analyze is_contra T = add_variance is_contra T;
   12.58 +  in analyze false T [] end;
   12.59 +
   12.60 +fun construct_mapper thy atomic =
   12.61 +  let
   12.62 +    val lookup = the o Symtab.lookup (Data.get thy);
   12.63 +    fun constructs is_contra (_, (co, contra)) T T' =
   12.64 +      (if co then [construct is_contra T T'] else [])
   12.65 +      @ (if contra then [construct (not is_contra) T T'] else [])
   12.66 +    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
   12.67 +          let
   12.68 +            val { mapper, variances, ... } = lookup tyco;
   12.69 +            val args = maps (fn (arg_pattern, (T, T')) =>
   12.70 +              constructs is_contra arg_pattern T T')
   12.71 +                (variances ~~ (Ts ~~ Ts'));
   12.72 +            val (U, U') = if is_contra then (T', T) else (T, T');
   12.73 +          in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end
   12.74 +      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
   12.75 +  in construct end;
   12.76 +
   12.77 +
   12.78 +(* mapper properties *)
   12.79 +
   12.80 +fun make_compositionality_prop variances (tyco, mapper) =
   12.81 +  let
   12.82 +    fun invents n k nctxt =
   12.83 +      let
   12.84 +        val names = Name.invents nctxt n k;
   12.85 +      in (names, fold Name.declare names nctxt) end;
   12.86 +    val (((vs1, vs2), vs3), _) = Name.context
   12.87 +      |> invents Name.aT (length variances)
   12.88 +      ||>> invents Name.aT (length variances)
   12.89 +      ||>> invents Name.aT (length variances);
   12.90 +    fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
   12.91 +      vs variances;
   12.92 +    val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3);
   12.93 +    fun mk_argT ((T, T'), (_, (co, contra))) =
   12.94 +      (if co then [(T --> T')] else [])
   12.95 +      @ (if contra then [(T' --> T)] else []);
   12.96 +    val contras = maps (fn (_, (co, contra)) =>
   12.97 +      (if co then [false] else []) @ (if contra then [true] else [])) variances;
   12.98 +    val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
   12.99 +    val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
  12.100 +    val ((names21, names32), nctxt) = Name.context
  12.101 +      |> invents "f" (length Ts21)
  12.102 +      ||>> invents "f" (length Ts32);
  12.103 +    val T1 = Type (tyco, Ts1);
  12.104 +    val T2 = Type (tyco, Ts2);
  12.105 +    val T3 = Type (tyco, Ts3);
  12.106 +    val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3);
  12.107 +    val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
  12.108 +    val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
  12.109 +      if not is_contra then
  12.110 +        Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0))
  12.111 +      else
  12.112 +        Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
  12.113 +      ) contras (args21 ~~ args32)
  12.114 +    fun mk_mapper T T' args = list_comb (Const (mapper,
  12.115 +      map fastype_of args ---> T --> T'), args);
  12.116 +    val lhs = mk_mapper T2 T1 (map Free args21) $
  12.117 +      (mk_mapper T3 T2 (map Free args32) $ x);
  12.118 +    val rhs = mk_mapper T3 T1 args31 $ x;
  12.119 +  in (map Free (args21 @ args32) @ [x], (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
  12.120 +
  12.121 +fun make_identity_prop variances (tyco, mapper) =
  12.122 +  let
  12.123 +    val vs = Name.invents Name.context Name.aT (length variances);
  12.124 +    val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances;
  12.125 +    fun bool_num b = if b then 1 else 0;
  12.126 +    fun mk_argT (T, (_, (co, contra))) =
  12.127 +      replicate (bool_num co + bool_num contra) (T --> T)
  12.128 +    val Ts' = maps mk_argT (Ts ~~ variances)
  12.129 +    val T = Type (tyco, Ts);
  12.130 +    val x = Free (Long_Name.base_name tyco, T);
  12.131 +    val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
  12.132 +      map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
  12.133 +  in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;
  12.134 +
  12.135 +
  12.136 +(* analyzing and registering mappers *)
  12.137 +
  12.138 +fun consume eq x [] = (false, [])
  12.139 +  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
  12.140 +
  12.141 +fun split_mapper_typ "fun" T =
  12.142 +      let
  12.143 +        val (Ts', T') = strip_type T;
  12.144 +        val (Ts'', T'') = split_last Ts';
  12.145 +        val (Ts''', T''') = split_last Ts'';
  12.146 +      in (Ts''', T''', T'' --> T') end
  12.147 +  | split_mapper_typ tyco T =
  12.148 +      let
  12.149 +        val (Ts', T') = strip_type T;
  12.150 +        val (Ts'', T'') = split_last Ts';
  12.151 +      in (Ts'', T'', T') end;
  12.152 +
  12.153 +fun analyze_variances thy tyco T =
  12.154 +  let
  12.155 +    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T);
  12.156 +    val (Ts, T1, T2) = split_mapper_typ tyco T
  12.157 +      handle List.Empty => bad_typ ();
  12.158 +    val _ = pairself
  12.159 +      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
  12.160 +    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
  12.161 +      handle TYPE _ => bad_typ ();
  12.162 +    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
  12.163 +      then bad_typ () else ();
  12.164 +    fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) =
  12.165 +      let
  12.166 +        val coT = TFree var1 --> TFree var2;
  12.167 +        val contraT = TFree var2 --> TFree var1;
  12.168 +        val sort = Sign.inter_sort thy (sort1, sort2);
  12.169 +      in
  12.170 +        consume (op =) coT
  12.171 +        ##>> consume (op =) contraT
  12.172 +        #>> pair sort
  12.173 +      end;
  12.174 +    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
  12.175 +    val _ = if null left_variances then () else bad_typ ();
  12.176 +  in variances end;
  12.177 +
  12.178 +fun gen_type_lifting prep_term some_prfx raw_t thy =
  12.179 +  let
  12.180 +    val (mapper, T) = case prep_term thy raw_t
  12.181 +     of Const cT => cT
  12.182 +      | t => error ("No constant: " ^ Syntax.string_of_term_global thy t);
  12.183 +    val prfx = the_default (Long_Name.base_name mapper) some_prfx;
  12.184 +    val _ = Type.no_tvars T;
  12.185 +    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
  12.186 +      | add_tycos _ = I;
  12.187 +    val tycos = add_tycos T [];
  12.188 +    val tyco = if tycos = ["fun"] then "fun"
  12.189 +      else case remove (op =) "fun" tycos
  12.190 +       of [tyco] => tyco
  12.191 +        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
  12.192 +    val variances = analyze_variances thy tyco T;
  12.193 +    val compositionality_prop = uncurry (fold_rev Logic.all)
  12.194 +      (make_compositionality_prop variances (tyco, mapper));
  12.195 +    val identity_prop = uncurry Logic.all
  12.196 +      (make_identity_prop variances (tyco, mapper));
  12.197 +    val qualify = Binding.qualify true prfx o Binding.name;
  12.198 +    fun after_qed [single_compositionality, single_identity] lthy =
  12.199 +      lthy
  12.200 +      |> Local_Theory.note ((qualify compositionalityN, []), single_compositionality)
  12.201 +      ||>> Local_Theory.note ((qualify identityN, []), single_identity)
  12.202 +      |-> (fn ((_, [compositionality]), (_, [identity])) =>
  12.203 +          (Local_Theory.background_theory o Data.map)
  12.204 +            (Symtab.update (tyco, { mapper = mapper, variances = variances,
  12.205 +              compositionality = compositionality, identity = identity })));
  12.206 +  in
  12.207 +    thy
  12.208 +    |> Named_Target.theory_init
  12.209 +    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
  12.210 +  end
  12.211 +
  12.212 +val type_lifting = gen_type_lifting Sign.cert_term;
  12.213 +val type_lifting_cmd = gen_type_lifting Syntax.read_term_global;
  12.214 +
  12.215 +val _ =
  12.216 +  Outer_Syntax.command "type_lifting" "register operations managing the functorial structure of a type" Keyword.thy_goal
  12.217 +    (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
  12.218 +      >> (fn (prfx, t) => Toplevel.print o (Toplevel.theory_to_proof (type_lifting_cmd prfx t))));
  12.219 +
  12.220 +end;
    13.1 --- a/src/HOL/Tools/type_mapper.ML	Sun Dec 05 14:02:16 2010 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,217 +0,0 @@
    13.4 -(*  Title:      HOL/Tools/type_mapper.ML
    13.5 -    Author:     Florian Haftmann, TU Muenchen
    13.6 -
    13.7 -Functorial mappers on types.
    13.8 -*)
    13.9 -
   13.10 -signature TYPE_MAPPER =
   13.11 -sig
   13.12 -  val find_atomic: theory -> typ -> (typ * (bool * bool)) list
   13.13 -  val construct_mapper: theory -> (string * bool -> term)
   13.14 -    -> bool -> typ -> typ -> term
   13.15 -  val type_mapper: string option -> term -> theory -> Proof.state
   13.16 -  type entry
   13.17 -  val entries: theory -> entry Symtab.table
   13.18 -end;
   13.19 -
   13.20 -structure Type_Mapper : TYPE_MAPPER =
   13.21 -struct
   13.22 -
   13.23 -val compositionalityN = "compositionality";
   13.24 -val identityN = "identity";
   13.25 -
   13.26 -(** functorial mappers and their properties **)
   13.27 -
   13.28 -(* bookkeeping *)
   13.29 -
   13.30 -type entry = { mapper: string, variances: (sort * (bool * bool)) list,
   13.31 -  compositionality: thm, identity: thm };
   13.32 -
   13.33 -structure Data = Theory_Data(
   13.34 -  type T = entry Symtab.table
   13.35 -  val empty = Symtab.empty
   13.36 -  fun merge (xy : T * T) = Symtab.merge (K true) xy
   13.37 -  val extend = I
   13.38 -);
   13.39 -
   13.40 -val entries = Data.get;
   13.41 -
   13.42 -
   13.43 -(* type analysis *)
   13.44 -
   13.45 -fun find_atomic thy T =
   13.46 -  let
   13.47 -    val variances_of = Option.map #variances o Symtab.lookup (Data.get thy);
   13.48 -    fun add_variance is_contra T =
   13.49 -      AList.map_default (op =) (T, (false, false))
   13.50 -        ((if is_contra then apsnd else apfst) (K true));
   13.51 -    fun analyze' is_contra (_, (co, contra)) T =
   13.52 -      (if co then analyze is_contra T else I)
   13.53 -      #> (if contra then analyze (not is_contra) T else I)
   13.54 -    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
   13.55 -          of NONE => add_variance is_contra T
   13.56 -           | SOME variances => fold2 (analyze' is_contra) variances Ts)
   13.57 -      | analyze is_contra T = add_variance is_contra T;
   13.58 -  in analyze false T [] end;
   13.59 -
   13.60 -fun construct_mapper thy atomic =
   13.61 -  let
   13.62 -    val lookup = the o Symtab.lookup (Data.get thy);
   13.63 -    fun constructs is_contra (_, (co, contra)) T T' =
   13.64 -      (if co then [construct is_contra T T'] else [])
   13.65 -      @ (if contra then [construct (not is_contra) T T'] else [])
   13.66 -    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
   13.67 -          let
   13.68 -            val { mapper, variances, ... } = lookup tyco;
   13.69 -            val args = maps (fn (arg_pattern, (T, T')) =>
   13.70 -              constructs is_contra arg_pattern T T')
   13.71 -                (variances ~~ (Ts ~~ Ts'));
   13.72 -            val (U, U') = if is_contra then (T', T) else (T, T');
   13.73 -          in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end
   13.74 -      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
   13.75 -  in construct end;
   13.76 -
   13.77 -
   13.78 -(* mapper properties *)
   13.79 -
   13.80 -fun make_compositionality_prop variances (tyco, mapper) =
   13.81 -  let
   13.82 -    fun invents n k nctxt =
   13.83 -      let
   13.84 -        val names = Name.invents nctxt n k;
   13.85 -      in (names, fold Name.declare names nctxt) end;
   13.86 -    val (((vs1, vs2), vs3), _) = Name.context
   13.87 -      |> invents Name.aT (length variances)
   13.88 -      ||>> invents Name.aT (length variances)
   13.89 -      ||>> invents Name.aT (length variances);
   13.90 -    fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
   13.91 -      vs variances;
   13.92 -    val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3);
   13.93 -    fun mk_argT ((T, T'), (_, (co, contra))) =
   13.94 -      (if co then [(T --> T')] else [])
   13.95 -      @ (if contra then [(T' --> T)] else []);
   13.96 -    val contras = maps (fn (_, (co, contra)) =>
   13.97 -      (if co then [false] else []) @ (if contra then [true] else [])) variances;
   13.98 -    val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
   13.99 -    val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
  13.100 -    val ((names21, names32), nctxt) = Name.context
  13.101 -      |> invents "f" (length Ts21)
  13.102 -      ||>> invents "f" (length Ts32);
  13.103 -    val T1 = Type (tyco, Ts1);
  13.104 -    val T2 = Type (tyco, Ts2);
  13.105 -    val T3 = Type (tyco, Ts3);
  13.106 -    val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3);
  13.107 -    val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
  13.108 -    val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
  13.109 -      if not is_contra then
  13.110 -        Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0))
  13.111 -      else
  13.112 -        Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
  13.113 -      ) contras (args21 ~~ args32)
  13.114 -    fun mk_mapper T T' args = list_comb (Const (mapper,
  13.115 -      map fastype_of args ---> T --> T'), args);
  13.116 -    val lhs = mk_mapper T2 T1 (map Free args21) $
  13.117 -      (mk_mapper T3 T2 (map Free args32) $ x);
  13.118 -    val rhs = mk_mapper T3 T1 args31 $ x;
  13.119 -  in (map Free (args21 @ args32) @ [x], (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
  13.120 -
  13.121 -fun make_identity_prop variances (tyco, mapper) =
  13.122 -  let
  13.123 -    val vs = Name.invents Name.context Name.aT (length variances);
  13.124 -    val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances;
  13.125 -    fun bool_num b = if b then 1 else 0;
  13.126 -    fun mk_argT (T, (_, (co, contra))) =
  13.127 -      replicate (bool_num co + bool_num contra) (T --> T)
  13.128 -    val Ts' = maps mk_argT (Ts ~~ variances)
  13.129 -    val T = Type (tyco, Ts);
  13.130 -    val x = Free (Long_Name.base_name tyco, T);
  13.131 -    val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
  13.132 -      map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
  13.133 -  in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;
  13.134 -
  13.135 -
  13.136 -(* analyzing and registering mappers *)
  13.137 -
  13.138 -fun consume eq x [] = (false, [])
  13.139 -  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
  13.140 -
  13.141 -fun split_mapper_typ "fun" T =
  13.142 -      let
  13.143 -        val (Ts', T') = strip_type T;
  13.144 -        val (Ts'', T'') = split_last Ts';
  13.145 -        val (Ts''', T''') = split_last Ts'';
  13.146 -      in (Ts''', T''', T'' --> T') end
  13.147 -  | split_mapper_typ tyco T =
  13.148 -      let
  13.149 -        val (Ts', T') = strip_type T;
  13.150 -        val (Ts'', T'') = split_last Ts';
  13.151 -      in (Ts'', T'', T') end;
  13.152 -
  13.153 -fun analyze_variances thy tyco T =
  13.154 -  let
  13.155 -    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T);
  13.156 -    val (Ts, T1, T2) = split_mapper_typ tyco T
  13.157 -      handle List.Empty => bad_typ ();
  13.158 -    val _ = pairself
  13.159 -      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
  13.160 -    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
  13.161 -      handle TYPE _ => bad_typ ();
  13.162 -    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
  13.163 -      then bad_typ () else ();
  13.164 -    fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) =
  13.165 -      let
  13.166 -        val coT = TFree var1 --> TFree var2;
  13.167 -        val contraT = TFree var2 --> TFree var1;
  13.168 -        val sort = Sign.inter_sort thy (sort1, sort2);
  13.169 -      in
  13.170 -        consume (op =) coT
  13.171 -        ##>> consume (op =) contraT
  13.172 -        #>> pair sort
  13.173 -      end;
  13.174 -    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
  13.175 -    val _ = if null left_variances then () else bad_typ ();
  13.176 -  in variances end;
  13.177 -
  13.178 -fun gen_type_mapper prep_term some_prfx raw_t thy =
  13.179 -  let
  13.180 -    val (mapper, T) = case prep_term thy raw_t
  13.181 -     of Const cT => cT
  13.182 -      | t => error ("No constant: " ^ Syntax.string_of_term_global thy t);
  13.183 -    val prfx = the_default (Long_Name.base_name mapper) some_prfx;
  13.184 -    val _ = Type.no_tvars T;
  13.185 -    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
  13.186 -      | add_tycos _ = I;
  13.187 -    val tycos = add_tycos T [];
  13.188 -    val tyco = if tycos = ["fun"] then "fun"
  13.189 -      else case remove (op =) "fun" tycos
  13.190 -       of [tyco] => tyco
  13.191 -        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
  13.192 -    val variances = analyze_variances thy tyco T;
  13.193 -    val compositionality_prop = uncurry (fold_rev Logic.all)
  13.194 -      (make_compositionality_prop variances (tyco, mapper));
  13.195 -    val identity_prop = uncurry Logic.all
  13.196 -      (make_identity_prop variances (tyco, mapper));
  13.197 -    val qualify = Binding.qualify true prfx o Binding.name;
  13.198 -    fun after_qed [single_compositionality, single_identity] lthy =
  13.199 -      lthy
  13.200 -      |> Local_Theory.note ((qualify compositionalityN, []), single_compositionality)
  13.201 -      ||>> Local_Theory.note ((qualify identityN, []), single_identity)
  13.202 -      |-> (fn ((_, [compositionality]), (_, [identity])) =>
  13.203 -          (Local_Theory.background_theory o Data.map)
  13.204 -            (Symtab.update (tyco, { mapper = mapper, variances = variances,
  13.205 -              compositionality = compositionality, identity = identity })));
  13.206 -  in
  13.207 -    thy
  13.208 -    |> Named_Target.theory_init
  13.209 -    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [compositionality_prop, identity_prop])
  13.210 -  end
  13.211 -
  13.212 -val type_mapper = gen_type_mapper Sign.cert_term;
  13.213 -val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
  13.214 -
  13.215 -val _ =
  13.216 -  Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
  13.217 -    (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
  13.218 -      >> (fn (prfx, t) => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd prfx t))));
  13.219 -
  13.220 -end;