1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Jan 10 22:03:24 2011 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jan 11 14:12:37 2011 +0100
     1.3 @@ -388,17 +388,17 @@
     1.4  
     1.5  text {*
     1.6    \begin{matharray}{rcl}
     1.7 -    @{command_def (HOL) "type_lifting"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
     1.8 +    @{command_def (HOL) "enriched_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
     1.9    \end{matharray}
    1.10  
    1.11    \begin{rail}
    1.12 -    'type_lifting' (prefix ':')? term
    1.13 +    'enriched_type' (prefix ':')? term
    1.14      ;
    1.15    \end{rail}
    1.16  
    1.17    \begin{description}
    1.18  
    1.19 -  \item @{command (HOL) "type_lifting"} allows to prove and register
    1.20 +  \item @{command (HOL) "enriched_type"} allows to prove and register
    1.21    properties about type constructors which refer to their functorial
    1.22    structure; these properties then can be used by other packages to
    1.23    deal with those type constructors in certain type constructions.

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jan 10 22:03:24 2011 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jan 11 14:12:37 2011 +0100
     2.3 @@ -403,7 +403,7 @@
     2.4    \end{matharray}
     2.5  
     2.6    \begin{rail}
     2.7 -    'type_lifting' (prefix ':')? term
     2.8 +    'enriched_type' (prefix ':')? term
     2.9      ;
    2.10    \end{rail}
    2.11  

     3.1 --- a/src/HOL/Datatype.thy	Mon Jan 10 22:03:24 2011 +0100
     3.2 +++ b/src/HOL/Datatype.thy	Tue Jan 11 14:12:37 2011 +0100
     3.3 @@ -15,7 +15,7 @@
     3.4  
     3.5  subsection {* Prelude: lifting over function space *}
     3.6  
     3.7 -type_lifting map_fun: map_fun
     3.8 +enriched_type map_fun: map_fun
     3.9    by (simp_all add: fun_eq_iff)
    3.10  
    3.11  

     4.1 --- a/src/HOL/Fun.thy	Mon Jan 10 22:03:24 2011 +0100
     4.2 +++ b/src/HOL/Fun.thy	Tue Jan 11 14:12:37 2011 +0100
     4.3 @@ -7,7 +7,7 @@
     4.4  
     4.5  theory Fun
     4.6  imports Complete_Lattice
     4.7 -uses ("Tools/type_lifting.ML")
     4.8 +uses ("Tools/enriched_type.ML")
     4.9  begin
    4.10  
    4.11  text{*As a simplification rule, it replaces all function equalities by
    4.12 @@ -843,6 +843,6 @@
    4.13  
    4.14  subsubsection {* Functorial structure of types *}
    4.15  
    4.16 -use "Tools/type_lifting.ML"
    4.17 +use "Tools/enriched_type.ML"
    4.18  
    4.19  end

     5.1 --- a/src/HOL/IsaMakefile	Mon Jan 10 22:03:24 2011 +0100
     5.2 +++ b/src/HOL/IsaMakefile	Tue Jan 11 14:12:37 2011 +0100
     5.3 @@ -241,7 +241,7 @@
     5.4    Tools/split_rule.ML \
     5.5    Tools/try.ML \
     5.6    Tools/typedef.ML \
     5.7 -  Tools/type_lifting.ML \
     5.8 +  Tools/enriched_type.ML \
     5.9    Transitive_Closure.thy \
    5.10    Typedef.thy \
    5.11    Wellfounded.thy

     6.1 --- a/src/HOL/Library/Cset.thy	Mon Jan 10 22:03:24 2011 +0100
     6.2 +++ b/src/HOL/Library/Cset.thy	Tue Jan 11 14:12:37 2011 +0100
     6.3 @@ -188,7 +188,7 @@
     6.4    "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
     6.5    by (simp add: set_def)
     6.6  
     6.7 -type_lifting map: map
     6.8 +enriched_type map: map
     6.9    by (simp_all add: fun_eq_iff image_compose)
    6.10  
    6.11  definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where

     7.1 --- a/src/HOL/Library/Dlist.thy	Mon Jan 10 22:03:24 2011 +0100
     7.2 +++ b/src/HOL/Library/Dlist.thy	Tue Jan 11 14:12:37 2011 +0100
     7.3 @@ -175,7 +175,7 @@
     7.4  
     7.5  section {* Functorial structure *}
     7.6  
     7.7 -type_lifting map: map
     7.8 +enriched_type map: map
     7.9    by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
    7.10  
    7.11  

     8.1 --- a/src/HOL/Library/Mapping.thy	Mon Jan 10 22:03:24 2011 +0100
     8.2 +++ b/src/HOL/Library/Mapping.thy	Tue Jan 11 14:12:37 2011 +0100
     8.3 @@ -50,7 +50,7 @@
     8.4    "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
     8.5    by (simp add: map_def)
     8.6  
     8.7 -type_lifting map: map
     8.8 +enriched_type map: map
     8.9    by (simp_all add: mapping_eq_iff fun_eq_iff Option.map.compositionality Option.map.id)
    8.10  
    8.11  

     9.1 --- a/src/HOL/Library/Multiset.thy	Mon Jan 10 22:03:24 2011 +0100
     9.2 +++ b/src/HOL/Library/Multiset.thy	Tue Jan 11 14:12:37 2011 +0100
     9.3 @@ -1643,7 +1643,7 @@
     9.4    @{term "{#x+x|x:#M. x<c#}"}.
     9.5  *}
     9.6  
     9.7 -type_lifting image_mset: image_mset proof -
     9.8 +enriched_type image_mset: image_mset proof -
     9.9    fix f g 
    9.10    show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
    9.11    proof

    10.1 --- a/src/HOL/List.thy	Mon Jan 10 22:03:24 2011 +0100
    10.2 +++ b/src/HOL/List.thy	Tue Jan 11 14:12:37 2011 +0100
    10.3 @@ -880,7 +880,7 @@
    10.4    "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
    10.5  by (induct rule:list_induct2, simp_all)
    10.6  
    10.7 -type_lifting map: map
    10.8 +enriched_type map: map
    10.9    by (simp_all add: fun_eq_iff id_def)
   10.10  
   10.11  

    11.1 --- a/src/HOL/Option.thy	Mon Jan 10 22:03:24 2011 +0100
    11.2 +++ b/src/HOL/Option.thy	Tue Jan 11 14:12:37 2011 +0100
    11.3 @@ -81,7 +81,7 @@
    11.4      "map f o sum_case g h = sum_case (map f o g) (map f o h)"
    11.5    by (rule ext) (simp split: sum.split)
    11.6  
    11.7 -type_lifting map: Option.map proof -
    11.8 +enriched_type map: Option.map proof -
    11.9    fix f g
   11.10    show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
   11.11    proof

    12.1 --- a/src/HOL/Predicate.thy	Mon Jan 10 22:03:24 2011 +0100
    12.2 +++ b/src/HOL/Predicate.thy	Tue Jan 11 14:12:37 2011 +0100
    12.3 @@ -795,7 +795,7 @@
    12.4    "eval (map f P) = image f (eval P)"
    12.5    by (auto simp add: map_def)
    12.6  
    12.7 -type_lifting map: map
    12.8 +enriched_type map: map
    12.9    by (auto intro!: pred_eqI simp add: fun_eq_iff image_compose)
   12.10  
   12.11  

    13.1 --- a/src/HOL/Product_Type.thy	Mon Jan 10 22:03:24 2011 +0100
    13.2 +++ b/src/HOL/Product_Type.thy	Tue Jan 11 14:12:37 2011 +0100
    13.3 @@ -834,7 +834,7 @@
    13.4    "map_pair f g (a, b) = (f a, g b)"
    13.5    by (simp add: map_pair_def)
    13.6  
    13.7 -type_lifting map_pair: map_pair
    13.8 +enriched_type map_pair: map_pair
    13.9    by (auto simp add: split_paired_all intro: ext)
   13.10  
   13.11  lemma fst_map_pair [simp]:

    14.1 --- a/src/HOL/Sum_Type.thy	Mon Jan 10 22:03:24 2011 +0100
    14.2 +++ b/src/HOL/Sum_Type.thy	Tue Jan 11 14:12:37 2011 +0100
    14.3 @@ -95,7 +95,7 @@
    14.4    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    14.5  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    14.6  
    14.7 -type_lifting sum_map: sum_map proof -
    14.8 +enriched_type sum_map: sum_map proof -
    14.9    fix f g h i
   14.10    show "sum_map f g \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)"
   14.11    proof

    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Tools/enriched_type.ML	Tue Jan 11 14:12:37 2011 +0100
    15.3 @@ -0,0 +1,256 @@
    15.4 +(*  Title:      HOL/Tools/enriched_type.ML
    15.5 +    Author:     Florian Haftmann, TU Muenchen
    15.6 +
    15.7 +Functorial structure of types.
    15.8 +*)
    15.9 +
   15.10 +signature ENRICHED_TYPE =
   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 enriched_type: string option -> term -> local_theory -> Proof.state
   15.16 +  type entry
   15.17 +  val entries: Proof.context -> entry list Symtab.table
   15.18 +end;
   15.19 +
   15.20 +structure Enriched_Type : ENRICHED_TYPE =
   15.21 +struct
   15.22 +
   15.23 +(* bookkeeping *)
   15.24 +
   15.25 +val compN = "comp";
   15.26 +val idN = "id";
   15.27 +val compositionalityN = "compositionality";
   15.28 +val identityN = "identity";
   15.29 +
   15.30 +type entry = { mapper: term, variances: (sort * (bool * bool)) list,
   15.31 +  comp: thm, id: thm };
   15.32 +
   15.33 +structure Data = Generic_Data
   15.34 +(
   15.35 +  type T = entry list Symtab.table
   15.36 +  val empty = Symtab.empty
   15.37 +  val extend = I
   15.38 +  fun merge data = Symtab.merge (K true) data
   15.39 +);
   15.40 +
   15.41 +val entries = Data.get o Context.Proof;
   15.42 +
   15.43 +
   15.44 +(* type analysis *)
   15.45 +
   15.46 +fun term_with_typ ctxt T t = Envir.subst_term_types
   15.47 +  (Type.typ_match (ProofContext.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t;
   15.48 +
   15.49 +fun find_atomic ctxt T =
   15.50 +  let
   15.51 +    val variances_of = Option.map #variances o try hd o Symtab.lookup_list (entries ctxt);
   15.52 +    fun add_variance is_contra T =
   15.53 +      AList.map_default (op =) (T, (false, false))
   15.54 +        ((if is_contra then apsnd else apfst) (K true));
   15.55 +    fun analyze' is_contra (_, (co, contra)) T =
   15.56 +      (if co then analyze is_contra T else I)
   15.57 +      #> (if contra then analyze (not is_contra) T else I)
   15.58 +    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
   15.59 +          of NONE => add_variance is_contra T
   15.60 +           | SOME variances => fold2 (analyze' is_contra) variances Ts)
   15.61 +      | analyze is_contra T = add_variance is_contra T;
   15.62 +  in analyze false T [] end;
   15.63 +
   15.64 +fun construct_mapper ctxt atomic =
   15.65 +  let
   15.66 +    val lookup = hd o Symtab.lookup_list (entries ctxt);
   15.67 +    fun constructs is_contra (_, (co, contra)) T T' =
   15.68 +      (if co then [construct is_contra T T'] else [])
   15.69 +      @ (if contra then [construct (not is_contra) T T'] else [])
   15.70 +    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
   15.71 +          let
   15.72 +            val { mapper = raw_mapper, variances, ... } = lookup tyco;
   15.73 +            val args = maps (fn (arg_pattern, (T, T')) =>
   15.74 +              constructs is_contra arg_pattern T T')
   15.75 +                (variances ~~ (Ts ~~ Ts'));
   15.76 +            val (U, U') = if is_contra then (T', T) else (T, T');
   15.77 +            val mapper = term_with_typ ctxt (map fastype_of args ---> U --> U') raw_mapper;
   15.78 +          in list_comb (mapper, args) end
   15.79 +      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
   15.80 +  in construct end;
   15.81 +
   15.82 +
   15.83 +(* mapper properties *)
   15.84 +
   15.85 +val compositionality_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm comp_def}) HOL_basic_ss;
   15.86 +
   15.87 +fun make_comp_prop ctxt variances (tyco, mapper) =
   15.88 +  let
   15.89 +    val sorts = map fst variances
   15.90 +    val (((vs3, vs2), vs1), _) = ctxt
   15.91 +      |> Variable.invent_types sorts
   15.92 +      ||>> Variable.invent_types sorts
   15.93 +      ||>> Variable.invent_types sorts
   15.94 +    val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3);
   15.95 +    fun mk_argT ((T, T'), (_, (co, contra))) =
   15.96 +      (if co then [(T --> T')] else [])
   15.97 +      @ (if contra then [(T' --> T)] else []);
   15.98 +    val contras = maps (fn (_, (co, contra)) =>
   15.99 +      (if co then [false] else []) @ (if contra then [true] else [])) variances;
  15.100 +    val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
  15.101 +    val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
  15.102 +    fun invents n k nctxt =
  15.103 +      let
  15.104 +        val names = Name.invents nctxt n k;
  15.105 +      in (names, fold Name.declare names nctxt) end;
  15.106 +    val ((names21, names32), nctxt) = Variable.names_of ctxt
  15.107 +      |> invents "f" (length Ts21)
  15.108 +      ||>> invents "f" (length Ts32);
  15.109 +    val T1 = Type (tyco, Ts1);
  15.110 +    val T2 = Type (tyco, Ts2);
  15.111 +    val T3 = Type (tyco, Ts3);
  15.112 +    val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
  15.113 +    val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
  15.114 +      if not is_contra then
  15.115 +        HOLogic.mk_comp (Free (f21, T21), Free (f32, T32))
  15.116 +      else
  15.117 +        HOLogic.mk_comp (Free (f32, T32), Free (f21, T21))
  15.118 +      ) contras (args21 ~~ args32)
  15.119 +    fun mk_mapper T T' args = list_comb
  15.120 +      (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args);
  15.121 +    val mapper21 = mk_mapper T2 T1 (map Free args21);
  15.122 +    val mapper32 = mk_mapper T3 T2 (map Free args32);
  15.123 +    val mapper31 = mk_mapper T3 T1 args31;
  15.124 +    val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
  15.125 +      (HOLogic.mk_comp (mapper21, mapper32), mapper31);
  15.126 +    val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3)
  15.127 +    val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
  15.128 +      (mapper21 $ (mapper32 $ x), mapper31 $ x);
  15.129 +    val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
  15.130 +    val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
  15.131 +    fun prove_compositionality ctxt comp_thm = Skip_Proof.prove ctxt [] [] compositionality_prop
  15.132 +      (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
  15.133 +        THEN' Simplifier.asm_lr_simp_tac compositionality_ss
  15.134 +        THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
  15.135 +  in (comp_prop, prove_compositionality) end;
  15.136 +
  15.137 +val identity_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm id_def}) HOL_basic_ss;
  15.138 +
  15.139 +fun make_id_prop ctxt variances (tyco, mapper) =
  15.140 +  let
  15.141 +    val (vs, ctxt') = Variable.invent_types (map fst variances) ctxt;
  15.142 +    val Ts = map TFree vs;
  15.143 +    fun bool_num b = if b then 1 else 0;
  15.144 +    fun mk_argT (T, (_, (co, contra))) =
  15.145 +      replicate (bool_num co + bool_num contra) T
  15.146 +    val arg_Ts = maps mk_argT (Ts ~~ variances)
  15.147 +    val T = Type (tyco, Ts);
  15.148 +    val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper;
  15.149 +    val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts);
  15.150 +    val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts);
  15.151 +    val rhs = HOLogic.id_const T;
  15.152 +    val (id_prop, identity_prop) = pairself
  15.153 +      (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
  15.154 +    fun prove_identity ctxt id_thm = Skip_Proof.prove ctxt [] [] identity_prop
  15.155 +      (K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss)));
  15.156 +  in (id_prop, prove_identity) end;
  15.157 +
  15.158 +
  15.159 +(* analyzing and registering mappers *)
  15.160 +
  15.161 +fun consume eq x [] = (false, [])
  15.162 +  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
  15.163 +
  15.164 +fun split_mapper_typ "fun" T =
  15.165 +      let
  15.166 +        val (Ts', T') = strip_type T;
  15.167 +        val (Ts'', T'') = split_last Ts';
  15.168 +        val (Ts''', T''') = split_last Ts'';
  15.169 +      in (Ts''', T''', T'' --> T') end
  15.170 +  | split_mapper_typ tyco T =
  15.171 +      let
  15.172 +        val (Ts', T') = strip_type T;
  15.173 +        val (Ts'', T'') = split_last Ts';
  15.174 +      in (Ts'', T'', T') end;
  15.175 +
  15.176 +fun analyze_variances ctxt tyco T =
  15.177 +  let
  15.178 +    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T);
  15.179 +    val (Ts, T1, T2) = split_mapper_typ tyco T
  15.180 +      handle List.Empty => bad_typ ();
  15.181 +    val _ = pairself
  15.182 +      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
  15.183 +      handle TYPE _ => bad_typ ();
  15.184 +    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
  15.185 +      handle TYPE _ => bad_typ ();
  15.186 +    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
  15.187 +      then bad_typ () else ();
  15.188 +    fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) =
  15.189 +      let
  15.190 +        val coT = TFree var1 --> TFree var2;
  15.191 +        val contraT = TFree var2 --> TFree var1;
  15.192 +        val sort = Sign.inter_sort (ProofContext.theory_of ctxt) (sort1, sort2);
  15.193 +      in
  15.194 +        consume (op =) coT
  15.195 +        ##>> consume (op =) contraT
  15.196 +        #>> pair sort
  15.197 +      end;
  15.198 +    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
  15.199 +    val _ = if null left_variances then () else bad_typ ();
  15.200 +  in variances end;
  15.201 +
  15.202 +fun gen_enriched_type prep_term some_prfx raw_mapper lthy =
  15.203 +  let
  15.204 +    val input_mapper = prep_term lthy raw_mapper;
  15.205 +    val T = fastype_of input_mapper;
  15.206 +    val _ = Type.no_tvars T;
  15.207 +    val mapper = singleton (Variable.polymorphic lthy) input_mapper;
  15.208 +    val _ = if null (Term.add_tfreesT (fastype_of mapper) []) then ()
  15.209 +      else error ("Illegal locally fixed variables in type: " ^ Syntax.string_of_typ lthy T);
  15.210 +    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
  15.211 +      | add_tycos _ = I;
  15.212 +    val tycos = add_tycos T [];
  15.213 +    val tyco = if tycos = ["fun"] then "fun"
  15.214 +      else case remove (op =) "fun" tycos
  15.215 +       of [tyco] => tyco
  15.216 +        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ lthy T);
  15.217 +    val prfx = the_default (Long_Name.base_name tyco) some_prfx;
  15.218 +    val variances = analyze_variances lthy tyco T;
  15.219 +    val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper);
  15.220 +    val (id_prop, prove_identity) = make_id_prop lthy variances (tyco, mapper);
  15.221 +    val qualify = Binding.qualify true prfx o Binding.name;
  15.222 +    fun mapper_declaration comp_thm id_thm phi context =
  15.223 +      let
  15.224 +        val typ_instance = Type.typ_instance (ProofContext.tsig_of (Context.proof_of context));
  15.225 +        val mapper' = Morphism.term phi mapper;
  15.226 +        val T_T' = pairself fastype_of (mapper, mapper');
  15.227 +      in if typ_instance T_T' andalso typ_instance (swap T_T')
  15.228 +        then (Data.map o Symtab.cons_list) (tyco,
  15.229 +          { mapper = mapper', variances = variances,
  15.230 +            comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
  15.231 +        else context
  15.232 +      end;
  15.233 +    fun after_qed [single_comp_thm, single_id_thm] lthy =
  15.234 +      lthy
  15.235 +      |> Local_Theory.note ((qualify compN, []), single_comp_thm)
  15.236 +      ||>> Local_Theory.note ((qualify idN, []), single_id_thm)
  15.237 +      |-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy =>
  15.238 +        lthy
  15.239 +        |> Local_Theory.note ((qualify compositionalityN, []),
  15.240 +            [prove_compositionality lthy comp_thm])
  15.241 +        |> snd
  15.242 +        |> Local_Theory.note ((qualify identityN, []),
  15.243 +            [prove_identity lthy id_thm])
  15.244 +        |> snd
  15.245 +        |> Local_Theory.declaration false (mapper_declaration comp_thm id_thm))
  15.246 +  in
  15.247 +    lthy
  15.248 +    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
  15.249 +  end
  15.250 +
  15.251 +val enriched_type = gen_enriched_type Syntax.check_term;
  15.252 +val enriched_type_cmd = gen_enriched_type Syntax.read_term;
  15.253 +
  15.254 +val _ = Outer_Syntax.local_theory_to_proof "enriched_type"
  15.255 +  "register operations managing the functorial structure of a type"
  15.256 +  Keyword.thy_goal (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
  15.257 +    >> (fn (prfx, t) => enriched_type_cmd prfx t));
  15.258 +
  15.259 +end;

    16.1 --- a/src/HOL/Tools/type_lifting.ML	Mon Jan 10 22:03:24 2011 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,256 +0,0 @@
    16.4 -(*  Title:      HOL/Tools/type_lifting.ML
    16.5 -    Author:     Florian Haftmann, TU Muenchen
    16.6 -
    16.7 -Functorial structure of types.
    16.8 -*)
    16.9 -
   16.10 -signature TYPE_LIFTING =
   16.11 -sig
   16.12 -  val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list
   16.13 -  val construct_mapper: Proof.context -> (string * bool -> term)
   16.14 -    -> bool -> typ -> typ -> term
   16.15 -  val type_lifting: string option -> term -> local_theory -> Proof.state
   16.16 -  type entry
   16.17 -  val entries: Proof.context -> entry list Symtab.table
   16.18 -end;
   16.19 -
   16.20 -structure Type_Lifting : TYPE_LIFTING =
   16.21 -struct
   16.22 -
   16.23 -(* bookkeeping *)
   16.24 -
   16.25 -val compN = "comp";
   16.26 -val idN = "id";
   16.27 -val compositionalityN = "compositionality";
   16.28 -val identityN = "identity";
   16.29 -
   16.30 -type entry = { mapper: term, variances: (sort * (bool * bool)) list,
   16.31 -  comp: thm, id: thm };
   16.32 -
   16.33 -structure Data = Generic_Data
   16.34 -(
   16.35 -  type T = entry list Symtab.table
   16.36 -  val empty = Symtab.empty
   16.37 -  val extend = I
   16.38 -  fun merge data = Symtab.merge (K true) data
   16.39 -);
   16.40 -
   16.41 -val entries = Data.get o Context.Proof;
   16.42 -
   16.43 -
   16.44 -(* type analysis *)
   16.45 -
   16.46 -fun term_with_typ ctxt T t = Envir.subst_term_types
   16.47 -  (Type.typ_match (ProofContext.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t;
   16.48 -
   16.49 -fun find_atomic ctxt T =
   16.50 -  let
   16.51 -    val variances_of = Option.map #variances o try hd o Symtab.lookup_list (entries ctxt);
   16.52 -    fun add_variance is_contra T =
   16.53 -      AList.map_default (op =) (T, (false, false))
   16.54 -        ((if is_contra then apsnd else apfst) (K true));
   16.55 -    fun analyze' is_contra (_, (co, contra)) T =
   16.56 -      (if co then analyze is_contra T else I)
   16.57 -      #> (if contra then analyze (not is_contra) T else I)
   16.58 -    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
   16.59 -          of NONE => add_variance is_contra T
   16.60 -           | SOME variances => fold2 (analyze' is_contra) variances Ts)
   16.61 -      | analyze is_contra T = add_variance is_contra T;
   16.62 -  in analyze false T [] end;
   16.63 -
   16.64 -fun construct_mapper ctxt atomic =
   16.65 -  let
   16.66 -    val lookup = hd o Symtab.lookup_list (entries ctxt);
   16.67 -    fun constructs is_contra (_, (co, contra)) T T' =
   16.68 -      (if co then [construct is_contra T T'] else [])
   16.69 -      @ (if contra then [construct (not is_contra) T T'] else [])
   16.70 -    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
   16.71 -          let
   16.72 -            val { mapper = raw_mapper, variances, ... } = lookup tyco;
   16.73 -            val args = maps (fn (arg_pattern, (T, T')) =>
   16.74 -              constructs is_contra arg_pattern T T')
   16.75 -                (variances ~~ (Ts ~~ Ts'));
   16.76 -            val (U, U') = if is_contra then (T', T) else (T, T');
   16.77 -            val mapper = term_with_typ ctxt (map fastype_of args ---> U --> U') raw_mapper;
   16.78 -          in list_comb (mapper, args) end
   16.79 -      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
   16.80 -  in construct end;
   16.81 -
   16.82 -
   16.83 -(* mapper properties *)
   16.84 -
   16.85 -val compositionality_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm comp_def}) HOL_basic_ss;
   16.86 -
   16.87 -fun make_comp_prop ctxt variances (tyco, mapper) =
   16.88 -  let
   16.89 -    val sorts = map fst variances
   16.90 -    val (((vs3, vs2), vs1), _) = ctxt
   16.91 -      |> Variable.invent_types sorts
   16.92 -      ||>> Variable.invent_types sorts
   16.93 -      ||>> Variable.invent_types sorts
   16.94 -    val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3);
   16.95 -    fun mk_argT ((T, T'), (_, (co, contra))) =
   16.96 -      (if co then [(T --> T')] else [])
   16.97 -      @ (if contra then [(T' --> T)] else []);
   16.98 -    val contras = maps (fn (_, (co, contra)) =>
   16.99 -      (if co then [false] else []) @ (if contra then [true] else [])) variances;
  16.100 -    val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
  16.101 -    val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
  16.102 -    fun invents n k nctxt =
  16.103 -      let
  16.104 -        val names = Name.invents nctxt n k;
  16.105 -      in (names, fold Name.declare names nctxt) end;
  16.106 -    val ((names21, names32), nctxt) = Variable.names_of ctxt
  16.107 -      |> invents "f" (length Ts21)
  16.108 -      ||>> invents "f" (length Ts32);
  16.109 -    val T1 = Type (tyco, Ts1);
  16.110 -    val T2 = Type (tyco, Ts2);
  16.111 -    val T3 = Type (tyco, Ts3);
  16.112 -    val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
  16.113 -    val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
  16.114 -      if not is_contra then
  16.115 -        HOLogic.mk_comp (Free (f21, T21), Free (f32, T32))
  16.116 -      else
  16.117 -        HOLogic.mk_comp (Free (f32, T32), Free (f21, T21))
  16.118 -      ) contras (args21 ~~ args32)
  16.119 -    fun mk_mapper T T' args = list_comb
  16.120 -      (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args);
  16.121 -    val mapper21 = mk_mapper T2 T1 (map Free args21);
  16.122 -    val mapper32 = mk_mapper T3 T2 (map Free args32);
  16.123 -    val mapper31 = mk_mapper T3 T1 args31;
  16.124 -    val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
  16.125 -      (HOLogic.mk_comp (mapper21, mapper32), mapper31);
  16.126 -    val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3)
  16.127 -    val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
  16.128 -      (mapper21 $ (mapper32 $ x), mapper31 $ x);
  16.129 -    val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
  16.130 -    val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
  16.131 -    fun prove_compositionality ctxt comp_thm = Skip_Proof.prove ctxt [] [] compositionality_prop
  16.132 -      (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
  16.133 -        THEN' Simplifier.asm_lr_simp_tac compositionality_ss
  16.134 -        THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
  16.135 -  in (comp_prop, prove_compositionality) end;
  16.136 -
  16.137 -val identity_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm id_def}) HOL_basic_ss;
  16.138 -
  16.139 -fun make_id_prop ctxt variances (tyco, mapper) =
  16.140 -  let
  16.141 -    val (vs, ctxt') = Variable.invent_types (map fst variances) ctxt;
  16.142 -    val Ts = map TFree vs;
  16.143 -    fun bool_num b = if b then 1 else 0;
  16.144 -    fun mk_argT (T, (_, (co, contra))) =
  16.145 -      replicate (bool_num co + bool_num contra) T
  16.146 -    val arg_Ts = maps mk_argT (Ts ~~ variances)
  16.147 -    val T = Type (tyco, Ts);
  16.148 -    val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper;
  16.149 -    val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts);
  16.150 -    val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts);
  16.151 -    val rhs = HOLogic.id_const T;
  16.152 -    val (id_prop, identity_prop) = pairself
  16.153 -      (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
  16.154 -    fun prove_identity ctxt id_thm = Skip_Proof.prove ctxt [] [] identity_prop
  16.155 -      (K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss)));
  16.156 -  in (id_prop, prove_identity) end;
  16.157 -
  16.158 -
  16.159 -(* analyzing and registering mappers *)
  16.160 -
  16.161 -fun consume eq x [] = (false, [])
  16.162 -  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
  16.163 -
  16.164 -fun split_mapper_typ "fun" T =
  16.165 -      let
  16.166 -        val (Ts', T') = strip_type T;
  16.167 -        val (Ts'', T'') = split_last Ts';
  16.168 -        val (Ts''', T''') = split_last Ts'';
  16.169 -      in (Ts''', T''', T'' --> T') end
  16.170 -  | split_mapper_typ tyco T =
  16.171 -      let
  16.172 -        val (Ts', T') = strip_type T;
  16.173 -        val (Ts'', T'') = split_last Ts';
  16.174 -      in (Ts'', T'', T') end;
  16.175 -
  16.176 -fun analyze_variances ctxt tyco T =
  16.177 -  let
  16.178 -    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T);
  16.179 -    val (Ts, T1, T2) = split_mapper_typ tyco T
  16.180 -      handle List.Empty => bad_typ ();
  16.181 -    val _ = pairself
  16.182 -      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
  16.183 -      handle TYPE _ => bad_typ ();
  16.184 -    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
  16.185 -      handle TYPE _ => bad_typ ();
  16.186 -    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
  16.187 -      then bad_typ () else ();
  16.188 -    fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) =
  16.189 -      let
  16.190 -        val coT = TFree var1 --> TFree var2;
  16.191 -        val contraT = TFree var2 --> TFree var1;
  16.192 -        val sort = Sign.inter_sort (ProofContext.theory_of ctxt) (sort1, sort2);
  16.193 -      in
  16.194 -        consume (op =) coT
  16.195 -        ##>> consume (op =) contraT
  16.196 -        #>> pair sort
  16.197 -      end;
  16.198 -    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
  16.199 -    val _ = if null left_variances then () else bad_typ ();
  16.200 -  in variances end;
  16.201 -
  16.202 -fun gen_type_lifting prep_term some_prfx raw_mapper lthy =
  16.203 -  let
  16.204 -    val input_mapper = prep_term lthy raw_mapper;
  16.205 -    val T = fastype_of input_mapper;
  16.206 -    val _ = Type.no_tvars T;
  16.207 -    val mapper = singleton (Variable.polymorphic lthy) input_mapper;
  16.208 -    val _ = if null (Term.add_tfreesT (fastype_of mapper) []) then ()
  16.209 -      else error ("Illegal locally fixed variables in type: " ^ Syntax.string_of_typ lthy T);
  16.210 -    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
  16.211 -      | add_tycos _ = I;
  16.212 -    val tycos = add_tycos T [];
  16.213 -    val tyco = if tycos = ["fun"] then "fun"
  16.214 -      else case remove (op =) "fun" tycos
  16.215 -       of [tyco] => tyco
  16.216 -        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ lthy T);
  16.217 -    val prfx = the_default (Long_Name.base_name tyco) some_prfx;
  16.218 -    val variances = analyze_variances lthy tyco T;
  16.219 -    val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper);
  16.220 -    val (id_prop, prove_identity) = make_id_prop lthy variances (tyco, mapper);
  16.221 -    val qualify = Binding.qualify true prfx o Binding.name;
  16.222 -    fun mapper_declaration comp_thm id_thm phi context =
  16.223 -      let
  16.224 -        val typ_instance = Type.typ_instance (ProofContext.tsig_of (Context.proof_of context));
  16.225 -        val mapper' = Morphism.term phi mapper;
  16.226 -        val T_T' = pairself fastype_of (mapper, mapper');
  16.227 -      in if typ_instance T_T' andalso typ_instance (swap T_T')
  16.228 -        then (Data.map o Symtab.cons_list) (tyco,
  16.229 -          { mapper = mapper', variances = variances,
  16.230 -            comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
  16.231 -        else context
  16.232 -      end;
  16.233 -    fun after_qed [single_comp_thm, single_id_thm] lthy =
  16.234 -      lthy
  16.235 -      |> Local_Theory.note ((qualify compN, []), single_comp_thm)
  16.236 -      ||>> Local_Theory.note ((qualify idN, []), single_id_thm)
  16.237 -      |-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy =>
  16.238 -        lthy
  16.239 -        |> Local_Theory.note ((qualify compositionalityN, []),
  16.240 -            [prove_compositionality lthy comp_thm])
  16.241 -        |> snd
  16.242 -        |> Local_Theory.note ((qualify identityN, []),
  16.243 -            [prove_identity lthy id_thm])
  16.244 -        |> snd
  16.245 -        |> Local_Theory.declaration false (mapper_declaration comp_thm id_thm))
  16.246 -  in
  16.247 -    lthy
  16.248 -    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
  16.249 -  end
  16.250 -
  16.251 -val type_lifting = gen_type_lifting Syntax.check_term;
  16.252 -val type_lifting_cmd = gen_type_lifting Syntax.read_term;
  16.253 -
  16.254 -val _ = Outer_Syntax.local_theory_to_proof "type_lifting"
  16.255 -  "register operations managing the functorial structure of a type"
  16.256 -  Keyword.thy_goal (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
  16.257 -    >> (fn (prfx, t) => type_lifting_cmd prfx t));
  16.258 -
  16.259 -end;