renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
authorblanchet
Fri Feb 14 07:53:46 2014 +0100 (2014-02-14)
changeset 55467a5c9002bc54d
parent 55466 786edc984c98
child 55468 98b25c51e9e5
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
src/Doc/IsarRef/HOL_Specific.thy
src/HOL/Fun.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/Predicate.thy
src/HOL/Product_Type.thy
src/HOL/Quotient_Examples/Lift_Fun.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/enriched_type.ML
src/HOL/Tools/functor.ML
     1.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -1194,16 +1194,16 @@
     1.4  
     1.5  text {*
     1.6    \begin{matharray}{rcl}
     1.7 -    @{command_def (HOL) "enriched_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
     1.8 +    @{command_def (HOL) "functor"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
     1.9    \end{matharray}
    1.10  
    1.11    @{rail \<open>
    1.12 -    @@{command (HOL) enriched_type} (@{syntax name} ':')? @{syntax term}
    1.13 +    @@{command (HOL) functor} (@{syntax name} ':')? @{syntax term}
    1.14    \<close>}
    1.15  
    1.16    \begin{description}
    1.17  
    1.18 -  \item @{command (HOL) "enriched_type"}~@{text "prefix: m"} allows to
    1.19 +  \item @{command (HOL) "functor"}~@{text "prefix: m"} allows to
    1.20    prove and register properties about the functorial structure of type
    1.21    constructors.  These properties then can be used by other packages
    1.22    to deal with those type constructors in certain type constructions.
    1.23 @@ -1375,7 +1375,7 @@
    1.24      is a quotient extension theorem. Quotient extension theorems
    1.25      allow for quotienting inside container types. Given a polymorphic
    1.26      type that serves as a container, a map function defined for this
    1.27 -    container using @{command (HOL) "enriched_type"} and a relation
    1.28 +    container using @{command (HOL) "functor"} and a relation
    1.29      map defined for for the container type, the quotient extension
    1.30      theorem should be @{term "Quotient3 R Abs Rep \<Longrightarrow> Quotient3
    1.31      (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
     2.1 --- a/src/HOL/Fun.thy	Fri Feb 14 07:53:46 2014 +0100
     2.2 +++ b/src/HOL/Fun.thy	Fri Feb 14 07:53:46 2014 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  
     2.5  theory Fun
     2.6  imports Complete_Lattices
     2.7 -keywords "enriched_type" :: thy_goal
     2.8 +keywords "functor" :: thy_goal
     2.9  begin
    2.10  
    2.11  lemma apply_inverse:
    2.12 @@ -904,12 +904,12 @@
    2.13  
    2.14  subsubsection {* Functorial structure of types *}
    2.15  
    2.16 -ML_file "Tools/enriched_type.ML"
    2.17 +ML_file "Tools/functor.ML"
    2.18  
    2.19 -enriched_type map_fun: map_fun
    2.20 +functor map_fun: map_fun
    2.21    by (simp_all add: fun_eq_iff)
    2.22  
    2.23 -enriched_type vimage
    2.24 +functor vimage
    2.25    by (simp_all add: fun_eq_iff vimage_comp)
    2.26  
    2.27  text {* Legacy theorem names *}
     3.1 --- a/src/HOL/Library/Dlist.thy	Fri Feb 14 07:53:46 2014 +0100
     3.2 +++ b/src/HOL/Library/Dlist.thy	Fri Feb 14 07:53:46 2014 +0100
     3.3 @@ -177,7 +177,7 @@
     3.4  
     3.5  subsection {* Functorial structure *}
     3.6  
     3.7 -enriched_type map: map
     3.8 +functor map: map
     3.9    by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
    3.10  
    3.11  
     4.1 --- a/src/HOL/Library/Mapping.thy	Fri Feb 14 07:53:46 2014 +0100
     4.2 +++ b/src/HOL/Library/Mapping.thy	Fri Feb 14 07:53:46 2014 +0100
     4.3 @@ -110,7 +110,7 @@
     4.4  
     4.5  subsection {* Functorial structure *}
     4.6  
     4.7 -enriched_type map: map
     4.8 +functor map: map
     4.9    by (transfer, auto simp add: fun_eq_iff option.map_comp option.map_id)+
    4.10  
    4.11  
     5.1 --- a/src/HOL/Library/Multiset.thy	Fri Feb 14 07:53:46 2014 +0100
     5.2 +++ b/src/HOL/Library/Multiset.thy	Fri Feb 14 07:53:46 2014 +0100
     5.3 @@ -880,7 +880,7 @@
     5.4    @{term "{#x+x|x:#M. x<c#}"}.
     5.5  *}
     5.6  
     5.7 -enriched_type image_mset: image_mset
     5.8 +functor image_mset: image_mset
     5.9  proof -
    5.10    fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
    5.11    proof
     6.1 --- a/src/HOL/List.thy	Fri Feb 14 07:53:46 2014 +0100
     6.2 +++ b/src/HOL/List.thy	Fri Feb 14 07:53:46 2014 +0100
     6.3 @@ -1160,7 +1160,7 @@
     6.4    "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
     6.5  by (induct rule:list_induct2, simp_all)
     6.6  
     6.7 -enriched_type map: map
     6.8 +functor map: map
     6.9  by (simp_all add: id_def)
    6.10  
    6.11  declare map.id [simp]
     7.1 --- a/src/HOL/Option.thy	Fri Feb 14 07:53:46 2014 +0100
     7.2 +++ b/src/HOL/Option.thy	Fri Feb 14 07:53:46 2014 +0100
     7.3 @@ -98,7 +98,7 @@
     7.4  lemma map_option_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map_option f x = map_option g y"
     7.5  by (cases x) auto
     7.6  
     7.7 -enriched_type map_option: map_option proof -
     7.8 +functor map_option: map_option proof -
     7.9    fix f g
    7.10    show "map_option f \<circ> map_option g = map_option (f \<circ> g)"
    7.11    proof
     8.1 --- a/src/HOL/Predicate.thy	Fri Feb 14 07:53:46 2014 +0100
     8.2 +++ b/src/HOL/Predicate.thy	Fri Feb 14 07:53:46 2014 +0100
     8.3 @@ -396,7 +396,7 @@
     8.4    "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
     8.5    by (auto simp add: map_def comp_def)
     8.6  
     8.7 -enriched_type map: map
     8.8 +functor map: map
     8.9    by (rule ext, rule pred_eqI, auto)+
    8.10  
    8.11  
     9.1 --- a/src/HOL/Product_Type.thy	Fri Feb 14 07:53:46 2014 +0100
     9.2 +++ b/src/HOL/Product_Type.thy	Fri Feb 14 07:53:46 2014 +0100
     9.3 @@ -834,7 +834,7 @@
     9.4    "map_pair f g (a, b) = (f a, g b)"
     9.5    by (simp add: map_pair_def)
     9.6  
     9.7 -enriched_type map_pair: map_pair
     9.8 +functor map_pair: map_pair
     9.9    by (auto simp add: split_paired_all)
    9.10  
    9.11  lemma fst_map_pair [simp]:
    10.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Feb 14 07:53:46 2014 +0100
    10.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Feb 14 07:53:46 2014 +0100
    10.3 @@ -51,7 +51,7 @@
    10.4  
    10.5  text {* Registration of the map function for 'a endofun. *}
    10.6  
    10.7 -enriched_type map_endofun : map_endofun
    10.8 +functor map_endofun : map_endofun
    10.9  proof -
   10.10    have "\<forall> x. abs_endofun (rep_endofun x) = x" using Quotient3_endofun by (auto simp: Quotient3_def)
   10.11    then show "map_endofun id id = id" 
    11.1 --- a/src/HOL/Sum_Type.thy	Fri Feb 14 07:53:46 2014 +0100
    11.2 +++ b/src/HOL/Sum_Type.thy	Fri Feb 14 07:53:46 2014 +0100
    11.3 @@ -122,7 +122,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 -enriched_type sum_map: sum_map proof -
    11.8 +functor sum_map: sum_map proof -
    11.9    fix f g h i
   11.10    show "sum_map f g \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)"
   11.11    proof
    12.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Feb 14 07:53:46 2014 +0100
    12.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Feb 14 07:53:46 2014 +0100
    12.3 @@ -66,15 +66,14 @@
    12.4    | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
    12.5  
    12.6  fun get_mapfun_data ctxt s =
    12.7 -  (case Symtab.lookup (Enriched_Type.entries ctxt) s of
    12.8 +  (case Symtab.lookup (Functor.entries ctxt) s of
    12.9      SOME [map_data] => (case try dest_Const (#mapper map_data) of
   12.10        SOME (c, _) => (Const (c, dummyT), #variances map_data)
   12.11      | NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant."))
   12.12    | SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.")
   12.13    | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) 
   12.14  
   12.15 -fun defined_mapfun_data ctxt s =
   12.16 -  Symtab.defined (Enriched_Type.entries ctxt) s
   12.17 +fun defined_mapfun_data ctxt = Symtab.defined (Functor.entries ctxt)
   12.18  
   12.19  (* looks up the (varified) rty and qty for
   12.20     a quotient definition
    13.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Feb 14 07:53:46 2014 +0100
    13.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Feb 14 07:53:46 2014 +0100
    13.3 @@ -262,7 +262,7 @@
    13.4        (case rty of
    13.5          Type (_, []) => warns
    13.6        | Type (s, _) =>
    13.7 -          if Symtab.defined (Enriched_Type.entries ctxt) s then warns else s :: warns
    13.8 +          if Symtab.defined (Functor.entries ctxt) s then warns else s :: warns
    13.9        | _ => warns)
   13.10  
   13.11      val warns = map_check_aux rty []
    14.1 --- a/src/HOL/Tools/enriched_type.ML	Fri Feb 14 07:53:46 2014 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,278 +0,0 @@
    14.4 -(*  Title:      HOL/Tools/enriched_type.ML
    14.5 -    Author:     Florian Haftmann, TU Muenchen
    14.6 -
    14.7 -Functorial structure of types.
    14.8 -*)
    14.9 -
   14.10 -signature ENRICHED_TYPE =
   14.11 -sig
   14.12 -  val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list
   14.13 -  val construct_mapper: Proof.context -> (string * bool -> term)
   14.14 -    -> bool -> typ -> typ -> term
   14.15 -  val enriched_type: string option -> term -> local_theory -> Proof.state
   14.16 -  type entry
   14.17 -  val entries: Proof.context -> entry list Symtab.table
   14.18 -end;
   14.19 -
   14.20 -structure Enriched_Type : ENRICHED_TYPE =
   14.21 -struct
   14.22 -
   14.23 -(* bookkeeping *)
   14.24 -
   14.25 -val compN = "comp";
   14.26 -val idN = "id";
   14.27 -val compositionalityN = "compositionality";
   14.28 -val identityN = "identity";
   14.29 -
   14.30 -type entry = { mapper: term, variances: (sort * (bool * bool)) list,
   14.31 -  comp: thm, id: thm };
   14.32 -
   14.33 -structure Data = Generic_Data
   14.34 -(
   14.35 -  type T = entry list Symtab.table
   14.36 -  val empty = Symtab.empty
   14.37 -  val extend = I
   14.38 -  fun merge data = Symtab.merge (K true) data
   14.39 -);
   14.40 -
   14.41 -val entries = Data.get o Context.Proof;
   14.42 -
   14.43 -
   14.44 -(* type analysis *)
   14.45 -
   14.46 -fun term_with_typ ctxt T t = Envir.subst_term_types
   14.47 -  (Type.typ_match (Proof_Context.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t;
   14.48 -
   14.49 -fun find_atomic ctxt T =
   14.50 -  let
   14.51 -    val variances_of = Option.map #variances o try hd o Symtab.lookup_list (entries ctxt);
   14.52 -    fun add_variance is_contra T =
   14.53 -      AList.map_default (op =) (T, (false, false))
   14.54 -        ((if is_contra then apsnd else apfst) (K true));
   14.55 -    fun analyze' is_contra (_, (co, contra)) T =
   14.56 -      (if co then analyze is_contra T else I)
   14.57 -      #> (if contra then analyze (not is_contra) T else I)
   14.58 -    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
   14.59 -          of NONE => add_variance is_contra T
   14.60 -           | SOME variances => fold2 (analyze' is_contra) variances Ts)
   14.61 -      | analyze is_contra T = add_variance is_contra T;
   14.62 -  in analyze false T [] end;
   14.63 -
   14.64 -fun construct_mapper ctxt atomic =
   14.65 -  let
   14.66 -    val lookup = hd o Symtab.lookup_list (entries ctxt);
   14.67 -    fun constructs is_contra (_, (co, contra)) T T' =
   14.68 -      (if co then [construct is_contra T T'] else [])
   14.69 -      @ (if contra then [construct (not is_contra) T T'] else [])
   14.70 -    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
   14.71 -          let
   14.72 -            val { mapper = raw_mapper, variances, ... } = lookup tyco;
   14.73 -            val args = maps (fn (arg_pattern, (T, T')) =>
   14.74 -              constructs is_contra arg_pattern T T')
   14.75 -                (variances ~~ (Ts ~~ Ts'));
   14.76 -            val (U, U') = if is_contra then (T', T) else (T, T');
   14.77 -            val mapper = term_with_typ ctxt (map fastype_of args ---> U --> U') raw_mapper;
   14.78 -          in list_comb (mapper, args) end
   14.79 -      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
   14.80 -  in construct end;
   14.81 -
   14.82 -
   14.83 -(* mapper properties *)
   14.84 -
   14.85 -val compositionality_ss =
   14.86 -  simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm comp_def}]);
   14.87 -
   14.88 -fun make_comp_prop ctxt variances (tyco, mapper) =
   14.89 -  let
   14.90 -    val sorts = map fst variances
   14.91 -    val (((vs3, vs2), vs1), _) = ctxt
   14.92 -      |> Variable.invent_types sorts
   14.93 -      ||>> Variable.invent_types sorts
   14.94 -      ||>> Variable.invent_types sorts
   14.95 -    val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3);
   14.96 -    fun mk_argT ((T, T'), (_, (co, contra))) =
   14.97 -      (if co then [(T --> T')] else [])
   14.98 -      @ (if contra then [(T' --> T)] else []);
   14.99 -    val contras = maps (fn (_, (co, contra)) =>
  14.100 -      (if co then [false] else []) @ (if contra then [true] else [])) variances;
  14.101 -    val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
  14.102 -    val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
  14.103 -    fun invents n k nctxt =
  14.104 -      let
  14.105 -        val names = Name.invent nctxt n k;
  14.106 -      in (names, fold Name.declare names nctxt) end;
  14.107 -    val ((names21, names32), nctxt) = Variable.names_of ctxt
  14.108 -      |> invents "f" (length Ts21)
  14.109 -      ||>> invents "f" (length Ts32);
  14.110 -    val T1 = Type (tyco, Ts1);
  14.111 -    val T2 = Type (tyco, Ts2);
  14.112 -    val T3 = Type (tyco, Ts3);
  14.113 -    val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
  14.114 -    val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
  14.115 -      if not is_contra then
  14.116 -        HOLogic.mk_comp (Free (f21, T21), Free (f32, T32))
  14.117 -      else
  14.118 -        HOLogic.mk_comp (Free (f32, T32), Free (f21, T21))
  14.119 -      ) contras (args21 ~~ args32)
  14.120 -    fun mk_mapper T T' args = list_comb
  14.121 -      (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args);
  14.122 -    val mapper21 = mk_mapper T2 T1 (map Free args21);
  14.123 -    val mapper32 = mk_mapper T3 T2 (map Free args32);
  14.124 -    val mapper31 = mk_mapper T3 T1 args31;
  14.125 -    val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
  14.126 -      (HOLogic.mk_comp (mapper21, mapper32), mapper31);
  14.127 -    val x = Free (the_single (Name.invent nctxt (Long_Name.base_name tyco) 1), T3)
  14.128 -    val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
  14.129 -      (mapper21 $ (mapper32 $ x), mapper31 $ x);
  14.130 -    val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
  14.131 -    val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
  14.132 -    fun prove_compositionality ctxt comp_thm = Goal.prove_sorry ctxt [] [] compositionality_prop
  14.133 -      (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
  14.134 -        THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
  14.135 -        THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
  14.136 -  in (comp_prop, prove_compositionality) end;
  14.137 -
  14.138 -val identity_ss =
  14.139 -  simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm id_def}]);
  14.140 -
  14.141 -fun make_id_prop ctxt variances (tyco, mapper) =
  14.142 -  let
  14.143 -    val (vs, _) = Variable.invent_types (map fst variances) ctxt;
  14.144 -    val Ts = map TFree vs;
  14.145 -    fun bool_num b = if b then 1 else 0;
  14.146 -    fun mk_argT (T, (_, (co, contra))) =
  14.147 -      replicate (bool_num co + bool_num contra) T
  14.148 -    val arg_Ts = maps mk_argT (Ts ~~ variances)
  14.149 -    val T = Type (tyco, Ts);
  14.150 -    val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper;
  14.151 -    val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts);
  14.152 -    val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts);
  14.153 -    val rhs = HOLogic.id_const T;
  14.154 -    val (id_prop, identity_prop) = pairself
  14.155 -      (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
  14.156 -    fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop
  14.157 -      (K (ALLGOALS (Method.insert_tac [id_thm] THEN'
  14.158 -        Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
  14.159 -  in (id_prop, prove_identity) end;
  14.160 -
  14.161 -
  14.162 -(* analyzing and registering mappers *)
  14.163 -
  14.164 -fun consume eq x [] = (false, [])
  14.165 -  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
  14.166 -
  14.167 -fun split_mapper_typ "fun" T =
  14.168 -      let
  14.169 -        val (Ts', T') = strip_type T;
  14.170 -        val (Ts'', T'') = split_last Ts';
  14.171 -        val (Ts''', T''') = split_last Ts'';
  14.172 -      in (Ts''', T''', T'' --> T') end
  14.173 -  | split_mapper_typ _ T =
  14.174 -      let
  14.175 -        val (Ts', T') = strip_type T;
  14.176 -        val (Ts'', T'') = split_last Ts';
  14.177 -      in (Ts'', T'', T') end;
  14.178 -
  14.179 -fun analyze_mapper ctxt input_mapper =
  14.180 -  let
  14.181 -    val T = fastype_of input_mapper;
  14.182 -    val _ = Type.no_tvars T;
  14.183 -    val _ =
  14.184 -      if null (subtract (op =) (Term.add_tfreesT T []) (Term.add_tfrees input_mapper []))
  14.185 -      then ()
  14.186 -      else error ("Illegal additional type variable(s) in term: " ^ Syntax.string_of_term ctxt input_mapper);
  14.187 -    val _ =
  14.188 -      if null (Term.add_vars (singleton
  14.189 -        (Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) [])
  14.190 -      then ()
  14.191 -      else error ("Illegal locally free variable(s) in term: "
  14.192 -        ^ Syntax.string_of_term ctxt input_mapper);;
  14.193 -    val mapper = singleton (Variable.polymorphic ctxt) input_mapper;
  14.194 -    val _ =
  14.195 -      if null (Term.add_tfreesT (fastype_of mapper) []) then ()
  14.196 -      else error ("Illegal locally fixed type variable(s) in type: " ^ Syntax.string_of_typ ctxt T);
  14.197 -    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
  14.198 -      | add_tycos _ = I;
  14.199 -    val tycos = add_tycos T [];
  14.200 -    val tyco = if tycos = ["fun"] then "fun"
  14.201 -      else case remove (op =) "fun" tycos
  14.202 -       of [tyco] => tyco
  14.203 -        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ ctxt T);
  14.204 -  in (mapper, T, tyco) end;
  14.205 -
  14.206 -fun analyze_variances ctxt tyco T =
  14.207 -  let
  14.208 -    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T);
  14.209 -    val (Ts, T1, T2) = split_mapper_typ tyco T
  14.210 -      handle List.Empty => bad_typ ();
  14.211 -    val _ = pairself
  14.212 -      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
  14.213 -      handle TYPE _ => bad_typ ();
  14.214 -    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
  14.215 -      handle TYPE _ => bad_typ ();
  14.216 -    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
  14.217 -      then bad_typ () else ();
  14.218 -    fun check_variance_pair (var1 as (_, sort1), var2 as (_, sort2)) =
  14.219 -      let
  14.220 -        val coT = TFree var1 --> TFree var2;
  14.221 -        val contraT = TFree var2 --> TFree var1;
  14.222 -        val sort = Sign.inter_sort (Proof_Context.theory_of ctxt) (sort1, sort2);
  14.223 -      in
  14.224 -        consume (op =) coT
  14.225 -        ##>> consume (op =) contraT
  14.226 -        #>> pair sort
  14.227 -      end;
  14.228 -    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
  14.229 -    val _ = if null left_variances then () else bad_typ ();
  14.230 -  in variances end;
  14.231 -
  14.232 -fun gen_enriched_type prep_term some_prfx raw_mapper lthy =
  14.233 -  let
  14.234 -    val (mapper, T, tyco) = analyze_mapper lthy (prep_term lthy raw_mapper);
  14.235 -    val prfx = the_default (Long_Name.base_name tyco) some_prfx;
  14.236 -    val variances = analyze_variances lthy tyco T;
  14.237 -    val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper);
  14.238 -    val (id_prop, prove_identity) = make_id_prop lthy variances (tyco, mapper);
  14.239 -    val qualify = Binding.qualify true prfx o Binding.name;
  14.240 -    fun mapper_declaration comp_thm id_thm phi context =
  14.241 -      let
  14.242 -        val typ_instance = Sign.typ_instance (Context.theory_of context);
  14.243 -        val mapper' = Morphism.term phi mapper;
  14.244 -        val T_T' = pairself fastype_of (mapper, mapper');
  14.245 -        val vars = Term.add_vars mapper' [];
  14.246 -      in
  14.247 -        if null vars andalso typ_instance T_T' andalso typ_instance (swap T_T')
  14.248 -        then (Data.map o Symtab.cons_list) (tyco,
  14.249 -          { mapper = mapper', variances = variances,
  14.250 -            comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
  14.251 -        else context
  14.252 -      end;
  14.253 -    fun after_qed [single_comp_thm, single_id_thm] lthy =
  14.254 -      lthy
  14.255 -      |> Local_Theory.note ((qualify compN, []), single_comp_thm)
  14.256 -      ||>> Local_Theory.note ((qualify idN, []), single_id_thm)
  14.257 -      |-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy =>
  14.258 -        lthy
  14.259 -        |> Local_Theory.note ((qualify compositionalityN, []),
  14.260 -            [prove_compositionality lthy comp_thm])
  14.261 -        |> snd
  14.262 -        |> Local_Theory.note ((qualify identityN, []),
  14.263 -            [prove_identity lthy id_thm])
  14.264 -        |> snd
  14.265 -        |> Local_Theory.declaration {syntax = false, pervasive = false}
  14.266 -          (mapper_declaration comp_thm id_thm))
  14.267 -  in
  14.268 -    lthy
  14.269 -    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
  14.270 -  end
  14.271 -
  14.272 -val enriched_type = gen_enriched_type Syntax.check_term;
  14.273 -val enriched_type_cmd = gen_enriched_type Syntax.read_term;
  14.274 -
  14.275 -val _ =
  14.276 -  Outer_Syntax.local_theory_to_proof @{command_spec "enriched_type"}
  14.277 -    "register operations managing the functorial structure of a type"
  14.278 -    (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
  14.279 -      >> (fn (prfx, t) => enriched_type_cmd prfx t));
  14.280 -
  14.281 -end;
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Tools/functor.ML	Fri Feb 14 07:53:46 2014 +0100
    15.3 @@ -0,0 +1,279 @@
    15.4 +(*  Title:      HOL/Tools/functor.ML
    15.5 +    Author:     Florian Haftmann, TU Muenchen
    15.6 +
    15.7 +Functorial structure of types.
    15.8 +*)
    15.9 +
   15.10 +signature FUNCTOR =
   15.11 +sig
   15.12 +  val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list
   15.13 +  val construct_mapper: Proof.context -> (string * bool -> term)
   15.14 +    -> bool -> typ -> typ -> term
   15.15 +  val functorx: string option -> term -> local_theory -> Proof.state
   15.16 +  val functor_cmd: string option -> string -> Proof.context -> Proof.state
   15.17 +  type entry
   15.18 +  val entries: Proof.context -> entry list Symtab.table
   15.19 +end;
   15.20 +
   15.21 +structure Functor : FUNCTOR =
   15.22 +struct
   15.23 +
   15.24 +(* bookkeeping *)
   15.25 +
   15.26 +val compN = "comp";
   15.27 +val idN = "id";
   15.28 +val compositionalityN = "compositionality";
   15.29 +val identityN = "identity";
   15.30 +
   15.31 +type entry = { mapper: term, variances: (sort * (bool * bool)) list,
   15.32 +  comp: thm, id: thm };
   15.33 +
   15.34 +structure Data = Generic_Data
   15.35 +(
   15.36 +  type T = entry list Symtab.table
   15.37 +  val empty = Symtab.empty
   15.38 +  val extend = I
   15.39 +  fun merge data = Symtab.merge (K true) data
   15.40 +);
   15.41 +
   15.42 +val entries = Data.get o Context.Proof;
   15.43 +
   15.44 +
   15.45 +(* type analysis *)
   15.46 +
   15.47 +fun term_with_typ ctxt T t = Envir.subst_term_types
   15.48 +  (Type.typ_match (Proof_Context.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t;
   15.49 +
   15.50 +fun find_atomic ctxt T =
   15.51 +  let
   15.52 +    val variances_of = Option.map #variances o try hd o Symtab.lookup_list (entries ctxt);
   15.53 +    fun add_variance is_contra T =
   15.54 +      AList.map_default (op =) (T, (false, false))
   15.55 +        ((if is_contra then apsnd else apfst) (K true));
   15.56 +    fun analyze' is_contra (_, (co, contra)) T =
   15.57 +      (if co then analyze is_contra T else I)
   15.58 +      #> (if contra then analyze (not is_contra) T else I)
   15.59 +    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
   15.60 +          of NONE => add_variance is_contra T
   15.61 +           | SOME variances => fold2 (analyze' is_contra) variances Ts)
   15.62 +      | analyze is_contra T = add_variance is_contra T;
   15.63 +  in analyze false T [] end;
   15.64 +
   15.65 +fun construct_mapper ctxt atomic =
   15.66 +  let
   15.67 +    val lookup = hd o Symtab.lookup_list (entries ctxt);
   15.68 +    fun constructs is_contra (_, (co, contra)) T T' =
   15.69 +      (if co then [construct is_contra T T'] else [])
   15.70 +      @ (if contra then [construct (not is_contra) T T'] else [])
   15.71 +    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
   15.72 +          let
   15.73 +            val { mapper = raw_mapper, variances, ... } = lookup tyco;
   15.74 +            val args = maps (fn (arg_pattern, (T, T')) =>
   15.75 +              constructs is_contra arg_pattern T T')
   15.76 +                (variances ~~ (Ts ~~ Ts'));
   15.77 +            val (U, U') = if is_contra then (T', T) else (T, T');
   15.78 +            val mapper = term_with_typ ctxt (map fastype_of args ---> U --> U') raw_mapper;
   15.79 +          in list_comb (mapper, args) end
   15.80 +      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
   15.81 +  in construct end;
   15.82 +
   15.83 +
   15.84 +(* mapper properties *)
   15.85 +
   15.86 +val compositionality_ss =
   15.87 +  simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm comp_def}]);
   15.88 +
   15.89 +fun make_comp_prop ctxt variances (tyco, mapper) =
   15.90 +  let
   15.91 +    val sorts = map fst variances
   15.92 +    val (((vs3, vs2), vs1), _) = ctxt
   15.93 +      |> Variable.invent_types sorts
   15.94 +      ||>> Variable.invent_types sorts
   15.95 +      ||>> Variable.invent_types sorts
   15.96 +    val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3);
   15.97 +    fun mk_argT ((T, T'), (_, (co, contra))) =
   15.98 +      (if co then [(T --> T')] else [])
   15.99 +      @ (if contra then [(T' --> T)] else []);
  15.100 +    val contras = maps (fn (_, (co, contra)) =>
  15.101 +      (if co then [false] else []) @ (if contra then [true] else [])) variances;
  15.102 +    val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
  15.103 +    val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
  15.104 +    fun invents n k nctxt =
  15.105 +      let
  15.106 +        val names = Name.invent nctxt n k;
  15.107 +      in (names, fold Name.declare names nctxt) end;
  15.108 +    val ((names21, names32), nctxt) = Variable.names_of ctxt
  15.109 +      |> invents "f" (length Ts21)
  15.110 +      ||>> invents "f" (length Ts32);
  15.111 +    val T1 = Type (tyco, Ts1);
  15.112 +    val T2 = Type (tyco, Ts2);
  15.113 +    val T3 = Type (tyco, Ts3);
  15.114 +    val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
  15.115 +    val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
  15.116 +      if not is_contra then
  15.117 +        HOLogic.mk_comp (Free (f21, T21), Free (f32, T32))
  15.118 +      else
  15.119 +        HOLogic.mk_comp (Free (f32, T32), Free (f21, T21))
  15.120 +      ) contras (args21 ~~ args32)
  15.121 +    fun mk_mapper T T' args = list_comb
  15.122 +      (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args);
  15.123 +    val mapper21 = mk_mapper T2 T1 (map Free args21);
  15.124 +    val mapper32 = mk_mapper T3 T2 (map Free args32);
  15.125 +    val mapper31 = mk_mapper T3 T1 args31;
  15.126 +    val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
  15.127 +      (HOLogic.mk_comp (mapper21, mapper32), mapper31);
  15.128 +    val x = Free (the_single (Name.invent nctxt (Long_Name.base_name tyco) 1), T3)
  15.129 +    val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
  15.130 +      (mapper21 $ (mapper32 $ x), mapper31 $ x);
  15.131 +    val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
  15.132 +    val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
  15.133 +    fun prove_compositionality ctxt comp_thm = Goal.prove_sorry ctxt [] [] compositionality_prop
  15.134 +      (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
  15.135 +        THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
  15.136 +        THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
  15.137 +  in (comp_prop, prove_compositionality) end;
  15.138 +
  15.139 +val identity_ss =
  15.140 +  simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm id_def}]);
  15.141 +
  15.142 +fun make_id_prop ctxt variances (tyco, mapper) =
  15.143 +  let
  15.144 +    val (vs, _) = Variable.invent_types (map fst variances) ctxt;
  15.145 +    val Ts = map TFree vs;
  15.146 +    fun bool_num b = if b then 1 else 0;
  15.147 +    fun mk_argT (T, (_, (co, contra))) =
  15.148 +      replicate (bool_num co + bool_num contra) T
  15.149 +    val arg_Ts = maps mk_argT (Ts ~~ variances)
  15.150 +    val T = Type (tyco, Ts);
  15.151 +    val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper;
  15.152 +    val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts);
  15.153 +    val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts);
  15.154 +    val rhs = HOLogic.id_const T;
  15.155 +    val (id_prop, identity_prop) = pairself
  15.156 +      (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
  15.157 +    fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop
  15.158 +      (K (ALLGOALS (Method.insert_tac [id_thm] THEN'
  15.159 +        Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
  15.160 +  in (id_prop, prove_identity) end;
  15.161 +
  15.162 +
  15.163 +(* analyzing and registering mappers *)
  15.164 +
  15.165 +fun consume _ _ [] = (false, [])
  15.166 +  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
  15.167 +
  15.168 +fun split_mapper_typ "fun" T =
  15.169 +      let
  15.170 +        val (Ts', T') = strip_type T;
  15.171 +        val (Ts'', T'') = split_last Ts';
  15.172 +        val (Ts''', T''') = split_last Ts'';
  15.173 +      in (Ts''', T''', T'' --> T') end
  15.174 +  | split_mapper_typ _ T =
  15.175 +      let
  15.176 +        val (Ts', T') = strip_type T;
  15.177 +        val (Ts'', T'') = split_last Ts';
  15.178 +      in (Ts'', T'', T') end;
  15.179 +
  15.180 +fun analyze_mapper ctxt input_mapper =
  15.181 +  let
  15.182 +    val T = fastype_of input_mapper;
  15.183 +    val _ = Type.no_tvars T;
  15.184 +    val _ =
  15.185 +      if null (subtract (op =) (Term.add_tfreesT T []) (Term.add_tfrees input_mapper []))
  15.186 +      then ()
  15.187 +      else error ("Illegal additional type variable(s) in term: " ^ Syntax.string_of_term ctxt input_mapper);
  15.188 +    val _ =
  15.189 +      if null (Term.add_vars (singleton
  15.190 +        (Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) [])
  15.191 +      then ()
  15.192 +      else error ("Illegal locally free variable(s) in term: "
  15.193 +        ^ Syntax.string_of_term ctxt input_mapper);;
  15.194 +    val mapper = singleton (Variable.polymorphic ctxt) input_mapper;
  15.195 +    val _ =
  15.196 +      if null (Term.add_tfreesT (fastype_of mapper) []) then ()
  15.197 +      else error ("Illegal locally fixed type variable(s) in type: " ^ Syntax.string_of_typ ctxt T);
  15.198 +    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
  15.199 +      | add_tycos _ = I;
  15.200 +    val tycos = add_tycos T [];
  15.201 +    val tyco = if tycos = ["fun"] then "fun"
  15.202 +      else case remove (op =) "fun" tycos
  15.203 +       of [tyco] => tyco
  15.204 +        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ ctxt T);
  15.205 +  in (mapper, T, tyco) end;
  15.206 +
  15.207 +fun analyze_variances ctxt tyco T =
  15.208 +  let
  15.209 +    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T);
  15.210 +    val (Ts, T1, T2) = split_mapper_typ tyco T
  15.211 +      handle List.Empty => bad_typ ();
  15.212 +    val _ = pairself
  15.213 +      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
  15.214 +      handle TYPE _ => bad_typ ();
  15.215 +    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
  15.216 +      handle TYPE _ => bad_typ ();
  15.217 +    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
  15.218 +      then bad_typ () else ();
  15.219 +    fun check_variance_pair (var1 as (_, sort1), var2 as (_, sort2)) =
  15.220 +      let
  15.221 +        val coT = TFree var1 --> TFree var2;
  15.222 +        val contraT = TFree var2 --> TFree var1;
  15.223 +        val sort = Sign.inter_sort (Proof_Context.theory_of ctxt) (sort1, sort2);
  15.224 +      in
  15.225 +        consume (op =) coT
  15.226 +        ##>> consume (op =) contraT
  15.227 +        #>> pair sort
  15.228 +      end;
  15.229 +    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
  15.230 +    val _ = if null left_variances then () else bad_typ ();
  15.231 +  in variances end;
  15.232 +
  15.233 +fun gen_functor prep_term some_prfx raw_mapper lthy =
  15.234 +  let
  15.235 +    val (mapper, T, tyco) = analyze_mapper lthy (prep_term lthy raw_mapper);
  15.236 +    val prfx = the_default (Long_Name.base_name tyco) some_prfx;
  15.237 +    val variances = analyze_variances lthy tyco T;
  15.238 +    val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper);
  15.239 +    val (id_prop, prove_identity) = make_id_prop lthy variances (tyco, mapper);
  15.240 +    val qualify = Binding.qualify true prfx o Binding.name;
  15.241 +    fun mapper_declaration comp_thm id_thm phi context =
  15.242 +      let
  15.243 +        val typ_instance = Sign.typ_instance (Context.theory_of context);
  15.244 +        val mapper' = Morphism.term phi mapper;
  15.245 +        val T_T' = pairself fastype_of (mapper, mapper');
  15.246 +        val vars = Term.add_vars mapper' [];
  15.247 +      in
  15.248 +        if null vars andalso typ_instance T_T' andalso typ_instance (swap T_T')
  15.249 +        then (Data.map o Symtab.cons_list) (tyco,
  15.250 +          { mapper = mapper', variances = variances,
  15.251 +            comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
  15.252 +        else context
  15.253 +      end;
  15.254 +    fun after_qed [single_comp_thm, single_id_thm] lthy =
  15.255 +      lthy
  15.256 +      |> Local_Theory.note ((qualify compN, []), single_comp_thm)
  15.257 +      ||>> Local_Theory.note ((qualify idN, []), single_id_thm)
  15.258 +      |-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy =>
  15.259 +        lthy
  15.260 +        |> Local_Theory.note ((qualify compositionalityN, []),
  15.261 +            [prove_compositionality lthy comp_thm])
  15.262 +        |> snd
  15.263 +        |> Local_Theory.note ((qualify identityN, []),
  15.264 +            [prove_identity lthy id_thm])
  15.265 +        |> snd
  15.266 +        |> Local_Theory.declaration {syntax = false, pervasive = false}
  15.267 +          (mapper_declaration comp_thm id_thm))
  15.268 +  in
  15.269 +    lthy
  15.270 +    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
  15.271 +  end
  15.272 +
  15.273 +val functorx = gen_functor Syntax.check_term;
  15.274 +val functor_cmd = gen_functor Syntax.read_term;
  15.275 +
  15.276 +val _ =
  15.277 +  Outer_Syntax.local_theory_to_proof @{command_spec "functor"}
  15.278 +    "register operations managing the functorial structure of a type"
  15.279 +    (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
  15.280 +      >> (fn (prfx, t) => functor_cmd prfx t));
  15.281 +
  15.282 +end;