renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
--- a/src/Doc/IsarRef/HOL_Specific.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy Fri Feb 14 07:53:46 2014 +0100
@@ -1194,16 +1194,16 @@
text {*
\begin{matharray}{rcl}
- @{command_def (HOL) "enriched_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
+ @{command_def (HOL) "functor"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
\end{matharray}
@{rail \<open>
- @@{command (HOL) enriched_type} (@{syntax name} ':')? @{syntax term}
+ @@{command (HOL) functor} (@{syntax name} ':')? @{syntax term}
\<close>}
\begin{description}
- \item @{command (HOL) "enriched_type"}~@{text "prefix: m"} allows to
+ \item @{command (HOL) "functor"}~@{text "prefix: m"} allows to
prove and register properties about the functorial structure of type
constructors. These properties then can be used by other packages
to deal with those type constructors in certain type constructions.
@@ -1375,7 +1375,7 @@
is a quotient extension theorem. Quotient extension theorems
allow for quotienting inside container types. Given a polymorphic
type that serves as a container, a map function defined for this
- container using @{command (HOL) "enriched_type"} and a relation
+ container using @{command (HOL) "functor"} and a relation
map defined for for the container type, the quotient extension
theorem should be @{term "Quotient3 R Abs Rep \<Longrightarrow> Quotient3
(rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
--- a/src/HOL/Fun.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Fun.thy Fri Feb 14 07:53:46 2014 +0100
@@ -8,7 +8,7 @@
theory Fun
imports Complete_Lattices
-keywords "enriched_type" :: thy_goal
+keywords "functor" :: thy_goal
begin
lemma apply_inverse:
@@ -904,12 +904,12 @@
subsubsection {* Functorial structure of types *}
-ML_file "Tools/enriched_type.ML"
+ML_file "Tools/functor.ML"
-enriched_type map_fun: map_fun
+functor map_fun: map_fun
by (simp_all add: fun_eq_iff)
-enriched_type vimage
+functor vimage
by (simp_all add: fun_eq_iff vimage_comp)
text {* Legacy theorem names *}
--- a/src/HOL/Library/Dlist.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Library/Dlist.thy Fri Feb 14 07:53:46 2014 +0100
@@ -177,7 +177,7 @@
subsection {* Functorial structure *}
-enriched_type map: map
+functor map: map
by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
--- a/src/HOL/Library/Mapping.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Library/Mapping.thy Fri Feb 14 07:53:46 2014 +0100
@@ -110,7 +110,7 @@
subsection {* Functorial structure *}
-enriched_type map: map
+functor map: map
by (transfer, auto simp add: fun_eq_iff option.map_comp option.map_id)+
--- a/src/HOL/Library/Multiset.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Feb 14 07:53:46 2014 +0100
@@ -880,7 +880,7 @@
@{term "{#x+x|x:#M. x<c#}"}.
*}
-enriched_type image_mset: image_mset
+functor image_mset: image_mset
proof -
fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
proof
--- a/src/HOL/List.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/List.thy Fri Feb 14 07:53:46 2014 +0100
@@ -1160,7 +1160,7 @@
"length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
by (induct rule:list_induct2, simp_all)
-enriched_type map: map
+functor map: map
by (simp_all add: id_def)
declare map.id [simp]
--- a/src/HOL/Option.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Option.thy Fri Feb 14 07:53:46 2014 +0100
@@ -98,7 +98,7 @@
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"
by (cases x) auto
-enriched_type map_option: map_option proof -
+functor map_option: map_option proof -
fix f g
show "map_option f \<circ> map_option g = map_option (f \<circ> g)"
proof
--- a/src/HOL/Predicate.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Predicate.thy Fri Feb 14 07:53:46 2014 +0100
@@ -396,7 +396,7 @@
"eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
by (auto simp add: map_def comp_def)
-enriched_type map: map
+functor map: map
by (rule ext, rule pred_eqI, auto)+
--- a/src/HOL/Product_Type.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Product_Type.thy Fri Feb 14 07:53:46 2014 +0100
@@ -834,7 +834,7 @@
"map_pair f g (a, b) = (f a, g b)"
by (simp add: map_pair_def)
-enriched_type map_pair: map_pair
+functor map_pair: map_pair
by (auto simp add: split_paired_all)
lemma fst_map_pair [simp]:
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy Fri Feb 14 07:53:46 2014 +0100
@@ -51,7 +51,7 @@
text {* Registration of the map function for 'a endofun. *}
-enriched_type map_endofun : map_endofun
+functor map_endofun : map_endofun
proof -
have "\<forall> x. abs_endofun (rep_endofun x) = x" using Quotient3_endofun by (auto simp: Quotient3_def)
then show "map_endofun id id = id"
--- a/src/HOL/Sum_Type.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Sum_Type.thy Fri Feb 14 07:53:46 2014 +0100
@@ -122,7 +122,7 @@
"sum_map f1 f2 (Inl a) = Inl (f1 a)"
| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
-enriched_type sum_map: sum_map proof -
+functor sum_map: sum_map proof -
fix f g h i
show "sum_map f g \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)"
proof
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Feb 14 07:53:46 2014 +0100
@@ -66,15 +66,14 @@
| RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
fun get_mapfun_data ctxt s =
- (case Symtab.lookup (Enriched_Type.entries ctxt) s of
+ (case Symtab.lookup (Functor.entries ctxt) s of
SOME [map_data] => (case try dest_Const (#mapper map_data) of
SOME (c, _) => (Const (c, dummyT), #variances map_data)
| NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant."))
| SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.")
| NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found."))
-fun defined_mapfun_data ctxt s =
- Symtab.defined (Enriched_Type.entries ctxt) s
+fun defined_mapfun_data ctxt = Symtab.defined (Functor.entries ctxt)
(* looks up the (varified) rty and qty for
a quotient definition
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Feb 14 07:53:46 2014 +0100
@@ -262,7 +262,7 @@
(case rty of
Type (_, []) => warns
| Type (s, _) =>
- if Symtab.defined (Enriched_Type.entries ctxt) s then warns else s :: warns
+ if Symtab.defined (Functor.entries ctxt) s then warns else s :: warns
| _ => warns)
val warns = map_check_aux rty []
--- a/src/HOL/Tools/enriched_type.ML Fri Feb 14 07:53:46 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,278 +0,0 @@
-(* Title: HOL/Tools/enriched_type.ML
- Author: Florian Haftmann, TU Muenchen
-
-Functorial structure of types.
-*)
-
-signature ENRICHED_TYPE =
-sig
- val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list
- val construct_mapper: Proof.context -> (string * bool -> term)
- -> bool -> typ -> typ -> term
- val enriched_type: string option -> term -> local_theory -> Proof.state
- type entry
- val entries: Proof.context -> entry list Symtab.table
-end;
-
-structure Enriched_Type : ENRICHED_TYPE =
-struct
-
-(* bookkeeping *)
-
-val compN = "comp";
-val idN = "id";
-val compositionalityN = "compositionality";
-val identityN = "identity";
-
-type entry = { mapper: term, variances: (sort * (bool * bool)) list,
- comp: thm, id: thm };
-
-structure Data = Generic_Data
-(
- type T = entry list Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data = Symtab.merge (K true) data
-);
-
-val entries = Data.get o Context.Proof;
-
-
-(* type analysis *)
-
-fun term_with_typ ctxt T t = Envir.subst_term_types
- (Type.typ_match (Proof_Context.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t;
-
-fun find_atomic ctxt T =
- let
- val variances_of = Option.map #variances o try hd o Symtab.lookup_list (entries ctxt);
- fun add_variance is_contra T =
- AList.map_default (op =) (T, (false, false))
- ((if is_contra then apsnd else apfst) (K true));
- fun analyze' is_contra (_, (co, contra)) T =
- (if co then analyze is_contra T else I)
- #> (if contra then analyze (not is_contra) T else I)
- and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
- of NONE => add_variance is_contra T
- | SOME variances => fold2 (analyze' is_contra) variances Ts)
- | analyze is_contra T = add_variance is_contra T;
- in analyze false T [] end;
-
-fun construct_mapper ctxt atomic =
- let
- val lookup = hd o Symtab.lookup_list (entries ctxt);
- fun constructs is_contra (_, (co, contra)) T T' =
- (if co then [construct is_contra T T'] else [])
- @ (if contra then [construct (not is_contra) T T'] else [])
- and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
- let
- val { mapper = raw_mapper, variances, ... } = lookup tyco;
- val args = maps (fn (arg_pattern, (T, T')) =>
- constructs is_contra arg_pattern T T')
- (variances ~~ (Ts ~~ Ts'));
- val (U, U') = if is_contra then (T', T) else (T, T');
- val mapper = term_with_typ ctxt (map fastype_of args ---> U --> U') raw_mapper;
- in list_comb (mapper, args) end
- | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
- in construct end;
-
-
-(* mapper properties *)
-
-val compositionality_ss =
- simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm comp_def}]);
-
-fun make_comp_prop ctxt variances (tyco, mapper) =
- let
- val sorts = map fst variances
- val (((vs3, vs2), vs1), _) = ctxt
- |> Variable.invent_types sorts
- ||>> Variable.invent_types sorts
- ||>> Variable.invent_types sorts
- val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3);
- fun mk_argT ((T, T'), (_, (co, contra))) =
- (if co then [(T --> T')] else [])
- @ (if contra then [(T' --> T)] else []);
- val contras = maps (fn (_, (co, contra)) =>
- (if co then [false] else []) @ (if contra then [true] else [])) variances;
- val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
- val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
- fun invents n k nctxt =
- let
- val names = Name.invent nctxt n k;
- in (names, fold Name.declare names nctxt) end;
- val ((names21, names32), nctxt) = Variable.names_of ctxt
- |> invents "f" (length Ts21)
- ||>> invents "f" (length Ts32);
- val T1 = Type (tyco, Ts1);
- val T2 = Type (tyco, Ts2);
- val T3 = Type (tyco, Ts3);
- val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
- val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
- if not is_contra then
- HOLogic.mk_comp (Free (f21, T21), Free (f32, T32))
- else
- HOLogic.mk_comp (Free (f32, T32), Free (f21, T21))
- ) contras (args21 ~~ args32)
- fun mk_mapper T T' args = list_comb
- (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args);
- val mapper21 = mk_mapper T2 T1 (map Free args21);
- val mapper32 = mk_mapper T3 T2 (map Free args32);
- val mapper31 = mk_mapper T3 T1 args31;
- val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
- (HOLogic.mk_comp (mapper21, mapper32), mapper31);
- val x = Free (the_single (Name.invent nctxt (Long_Name.base_name tyco) 1), T3)
- val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
- (mapper21 $ (mapper32 $ x), mapper31 $ x);
- val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
- val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
- fun prove_compositionality ctxt comp_thm = Goal.prove_sorry ctxt [] [] compositionality_prop
- (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
- THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
- THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
- in (comp_prop, prove_compositionality) end;
-
-val identity_ss =
- simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm id_def}]);
-
-fun make_id_prop ctxt variances (tyco, mapper) =
- let
- val (vs, _) = Variable.invent_types (map fst variances) ctxt;
- val Ts = map TFree vs;
- fun bool_num b = if b then 1 else 0;
- fun mk_argT (T, (_, (co, contra))) =
- replicate (bool_num co + bool_num contra) T
- val arg_Ts = maps mk_argT (Ts ~~ variances)
- val T = Type (tyco, Ts);
- val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper;
- val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts);
- val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts);
- val rhs = HOLogic.id_const T;
- val (id_prop, identity_prop) = pairself
- (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
- fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop
- (K (ALLGOALS (Method.insert_tac [id_thm] THEN'
- Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
- in (id_prop, prove_identity) end;
-
-
-(* analyzing and registering mappers *)
-
-fun consume eq x [] = (false, [])
- | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
-
-fun split_mapper_typ "fun" T =
- let
- val (Ts', T') = strip_type T;
- val (Ts'', T'') = split_last Ts';
- val (Ts''', T''') = split_last Ts'';
- in (Ts''', T''', T'' --> T') end
- | split_mapper_typ _ T =
- let
- val (Ts', T') = strip_type T;
- val (Ts'', T'') = split_last Ts';
- in (Ts'', T'', T') end;
-
-fun analyze_mapper ctxt input_mapper =
- let
- val T = fastype_of input_mapper;
- val _ = Type.no_tvars T;
- val _ =
- if null (subtract (op =) (Term.add_tfreesT T []) (Term.add_tfrees input_mapper []))
- then ()
- else error ("Illegal additional type variable(s) in term: " ^ Syntax.string_of_term ctxt input_mapper);
- val _ =
- if null (Term.add_vars (singleton
- (Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) [])
- then ()
- else error ("Illegal locally free variable(s) in term: "
- ^ Syntax.string_of_term ctxt input_mapper);;
- val mapper = singleton (Variable.polymorphic ctxt) input_mapper;
- val _ =
- if null (Term.add_tfreesT (fastype_of mapper) []) then ()
- else error ("Illegal locally fixed type variable(s) in type: " ^ Syntax.string_of_typ ctxt T);
- fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
- | add_tycos _ = I;
- val tycos = add_tycos T [];
- val tyco = if tycos = ["fun"] then "fun"
- else case remove (op =) "fun" tycos
- of [tyco] => tyco
- | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ ctxt T);
- in (mapper, T, tyco) end;
-
-fun analyze_variances ctxt tyco T =
- let
- fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T);
- val (Ts, T1, T2) = split_mapper_typ tyco T
- handle List.Empty => bad_typ ();
- val _ = pairself
- ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
- handle TYPE _ => bad_typ ();
- val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
- handle TYPE _ => bad_typ ();
- val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
- then bad_typ () else ();
- fun check_variance_pair (var1 as (_, sort1), var2 as (_, sort2)) =
- let
- val coT = TFree var1 --> TFree var2;
- val contraT = TFree var2 --> TFree var1;
- val sort = Sign.inter_sort (Proof_Context.theory_of ctxt) (sort1, sort2);
- in
- consume (op =) coT
- ##>> consume (op =) contraT
- #>> pair sort
- end;
- val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
- val _ = if null left_variances then () else bad_typ ();
- in variances end;
-
-fun gen_enriched_type prep_term some_prfx raw_mapper lthy =
- let
- val (mapper, T, tyco) = analyze_mapper lthy (prep_term lthy raw_mapper);
- val prfx = the_default (Long_Name.base_name tyco) some_prfx;
- val variances = analyze_variances lthy tyco T;
- val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper);
- val (id_prop, prove_identity) = make_id_prop lthy variances (tyco, mapper);
- val qualify = Binding.qualify true prfx o Binding.name;
- fun mapper_declaration comp_thm id_thm phi context =
- let
- val typ_instance = Sign.typ_instance (Context.theory_of context);
- val mapper' = Morphism.term phi mapper;
- val T_T' = pairself fastype_of (mapper, mapper');
- val vars = Term.add_vars mapper' [];
- in
- if null vars andalso typ_instance T_T' andalso typ_instance (swap T_T')
- then (Data.map o Symtab.cons_list) (tyco,
- { mapper = mapper', variances = variances,
- comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
- else context
- end;
- fun after_qed [single_comp_thm, single_id_thm] lthy =
- lthy
- |> Local_Theory.note ((qualify compN, []), single_comp_thm)
- ||>> Local_Theory.note ((qualify idN, []), single_id_thm)
- |-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy =>
- lthy
- |> Local_Theory.note ((qualify compositionalityN, []),
- [prove_compositionality lthy comp_thm])
- |> snd
- |> Local_Theory.note ((qualify identityN, []),
- [prove_identity lthy id_thm])
- |> snd
- |> Local_Theory.declaration {syntax = false, pervasive = false}
- (mapper_declaration comp_thm id_thm))
- in
- lthy
- |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
- end
-
-val enriched_type = gen_enriched_type Syntax.check_term;
-val enriched_type_cmd = gen_enriched_type Syntax.read_term;
-
-val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "enriched_type"}
- "register operations managing the functorial structure of a type"
- (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
- >> (fn (prfx, t) => enriched_type_cmd prfx t));
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/functor.ML Fri Feb 14 07:53:46 2014 +0100
@@ -0,0 +1,279 @@
+(* Title: HOL/Tools/functor.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Functorial structure of types.
+*)
+
+signature FUNCTOR =
+sig
+ val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list
+ val construct_mapper: Proof.context -> (string * bool -> term)
+ -> bool -> typ -> typ -> term
+ val functorx: string option -> term -> local_theory -> Proof.state
+ val functor_cmd: string option -> string -> Proof.context -> Proof.state
+ type entry
+ val entries: Proof.context -> entry list Symtab.table
+end;
+
+structure Functor : FUNCTOR =
+struct
+
+(* bookkeeping *)
+
+val compN = "comp";
+val idN = "id";
+val compositionalityN = "compositionality";
+val identityN = "identity";
+
+type entry = { mapper: term, variances: (sort * (bool * bool)) list,
+ comp: thm, id: thm };
+
+structure Data = Generic_Data
+(
+ type T = entry list Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data = Symtab.merge (K true) data
+);
+
+val entries = Data.get o Context.Proof;
+
+
+(* type analysis *)
+
+fun term_with_typ ctxt T t = Envir.subst_term_types
+ (Type.typ_match (Proof_Context.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t;
+
+fun find_atomic ctxt T =
+ let
+ val variances_of = Option.map #variances o try hd o Symtab.lookup_list (entries ctxt);
+ fun add_variance is_contra T =
+ AList.map_default (op =) (T, (false, false))
+ ((if is_contra then apsnd else apfst) (K true));
+ fun analyze' is_contra (_, (co, contra)) T =
+ (if co then analyze is_contra T else I)
+ #> (if contra then analyze (not is_contra) T else I)
+ and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
+ of NONE => add_variance is_contra T
+ | SOME variances => fold2 (analyze' is_contra) variances Ts)
+ | analyze is_contra T = add_variance is_contra T;
+ in analyze false T [] end;
+
+fun construct_mapper ctxt atomic =
+ let
+ val lookup = hd o Symtab.lookup_list (entries ctxt);
+ fun constructs is_contra (_, (co, contra)) T T' =
+ (if co then [construct is_contra T T'] else [])
+ @ (if contra then [construct (not is_contra) T T'] else [])
+ and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
+ let
+ val { mapper = raw_mapper, variances, ... } = lookup tyco;
+ val args = maps (fn (arg_pattern, (T, T')) =>
+ constructs is_contra arg_pattern T T')
+ (variances ~~ (Ts ~~ Ts'));
+ val (U, U') = if is_contra then (T', T) else (T, T');
+ val mapper = term_with_typ ctxt (map fastype_of args ---> U --> U') raw_mapper;
+ in list_comb (mapper, args) end
+ | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
+ in construct end;
+
+
+(* mapper properties *)
+
+val compositionality_ss =
+ simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm comp_def}]);
+
+fun make_comp_prop ctxt variances (tyco, mapper) =
+ let
+ val sorts = map fst variances
+ val (((vs3, vs2), vs1), _) = ctxt
+ |> Variable.invent_types sorts
+ ||>> Variable.invent_types sorts
+ ||>> Variable.invent_types sorts
+ val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3);
+ fun mk_argT ((T, T'), (_, (co, contra))) =
+ (if co then [(T --> T')] else [])
+ @ (if contra then [(T' --> T)] else []);
+ val contras = maps (fn (_, (co, contra)) =>
+ (if co then [false] else []) @ (if contra then [true] else [])) variances;
+ val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
+ val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
+ fun invents n k nctxt =
+ let
+ val names = Name.invent nctxt n k;
+ in (names, fold Name.declare names nctxt) end;
+ val ((names21, names32), nctxt) = Variable.names_of ctxt
+ |> invents "f" (length Ts21)
+ ||>> invents "f" (length Ts32);
+ val T1 = Type (tyco, Ts1);
+ val T2 = Type (tyco, Ts2);
+ val T3 = Type (tyco, Ts3);
+ val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
+ val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
+ if not is_contra then
+ HOLogic.mk_comp (Free (f21, T21), Free (f32, T32))
+ else
+ HOLogic.mk_comp (Free (f32, T32), Free (f21, T21))
+ ) contras (args21 ~~ args32)
+ fun mk_mapper T T' args = list_comb
+ (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args);
+ val mapper21 = mk_mapper T2 T1 (map Free args21);
+ val mapper32 = mk_mapper T3 T2 (map Free args32);
+ val mapper31 = mk_mapper T3 T1 args31;
+ val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
+ (HOLogic.mk_comp (mapper21, mapper32), mapper31);
+ val x = Free (the_single (Name.invent nctxt (Long_Name.base_name tyco) 1), T3)
+ val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
+ (mapper21 $ (mapper32 $ x), mapper31 $ x);
+ val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
+ val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
+ fun prove_compositionality ctxt comp_thm = Goal.prove_sorry ctxt [] [] compositionality_prop
+ (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
+ THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
+ THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
+ in (comp_prop, prove_compositionality) end;
+
+val identity_ss =
+ simpset_of (put_simpset HOL_basic_ss @{context} addsimps [Simpdata.mk_eq @{thm id_def}]);
+
+fun make_id_prop ctxt variances (tyco, mapper) =
+ let
+ val (vs, _) = Variable.invent_types (map fst variances) ctxt;
+ val Ts = map TFree vs;
+ fun bool_num b = if b then 1 else 0;
+ fun mk_argT (T, (_, (co, contra))) =
+ replicate (bool_num co + bool_num contra) T
+ val arg_Ts = maps mk_argT (Ts ~~ variances)
+ val T = Type (tyco, Ts);
+ val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper;
+ val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts);
+ val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts);
+ val rhs = HOLogic.id_const T;
+ val (id_prop, identity_prop) = pairself
+ (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
+ fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop
+ (K (ALLGOALS (Method.insert_tac [id_thm] THEN'
+ Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
+ in (id_prop, prove_identity) end;
+
+
+(* analyzing and registering mappers *)
+
+fun consume _ _ [] = (false, [])
+ | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
+
+fun split_mapper_typ "fun" T =
+ let
+ val (Ts', T') = strip_type T;
+ val (Ts'', T'') = split_last Ts';
+ val (Ts''', T''') = split_last Ts'';
+ in (Ts''', T''', T'' --> T') end
+ | split_mapper_typ _ T =
+ let
+ val (Ts', T') = strip_type T;
+ val (Ts'', T'') = split_last Ts';
+ in (Ts'', T'', T') end;
+
+fun analyze_mapper ctxt input_mapper =
+ let
+ val T = fastype_of input_mapper;
+ val _ = Type.no_tvars T;
+ val _ =
+ if null (subtract (op =) (Term.add_tfreesT T []) (Term.add_tfrees input_mapper []))
+ then ()
+ else error ("Illegal additional type variable(s) in term: " ^ Syntax.string_of_term ctxt input_mapper);
+ val _ =
+ if null (Term.add_vars (singleton
+ (Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) [])
+ then ()
+ else error ("Illegal locally free variable(s) in term: "
+ ^ Syntax.string_of_term ctxt input_mapper);;
+ val mapper = singleton (Variable.polymorphic ctxt) input_mapper;
+ val _ =
+ if null (Term.add_tfreesT (fastype_of mapper) []) then ()
+ else error ("Illegal locally fixed type variable(s) in type: " ^ Syntax.string_of_typ ctxt T);
+ fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
+ | add_tycos _ = I;
+ val tycos = add_tycos T [];
+ val tyco = if tycos = ["fun"] then "fun"
+ else case remove (op =) "fun" tycos
+ of [tyco] => tyco
+ | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ ctxt T);
+ in (mapper, T, tyco) end;
+
+fun analyze_variances ctxt tyco T =
+ let
+ fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T);
+ val (Ts, T1, T2) = split_mapper_typ tyco T
+ handle List.Empty => bad_typ ();
+ val _ = pairself
+ ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
+ handle TYPE _ => bad_typ ();
+ val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
+ handle TYPE _ => bad_typ ();
+ val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
+ then bad_typ () else ();
+ fun check_variance_pair (var1 as (_, sort1), var2 as (_, sort2)) =
+ let
+ val coT = TFree var1 --> TFree var2;
+ val contraT = TFree var2 --> TFree var1;
+ val sort = Sign.inter_sort (Proof_Context.theory_of ctxt) (sort1, sort2);
+ in
+ consume (op =) coT
+ ##>> consume (op =) contraT
+ #>> pair sort
+ end;
+ val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
+ val _ = if null left_variances then () else bad_typ ();
+ in variances end;
+
+fun gen_functor prep_term some_prfx raw_mapper lthy =
+ let
+ val (mapper, T, tyco) = analyze_mapper lthy (prep_term lthy raw_mapper);
+ val prfx = the_default (Long_Name.base_name tyco) some_prfx;
+ val variances = analyze_variances lthy tyco T;
+ val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper);
+ val (id_prop, prove_identity) = make_id_prop lthy variances (tyco, mapper);
+ val qualify = Binding.qualify true prfx o Binding.name;
+ fun mapper_declaration comp_thm id_thm phi context =
+ let
+ val typ_instance = Sign.typ_instance (Context.theory_of context);
+ val mapper' = Morphism.term phi mapper;
+ val T_T' = pairself fastype_of (mapper, mapper');
+ val vars = Term.add_vars mapper' [];
+ in
+ if null vars andalso typ_instance T_T' andalso typ_instance (swap T_T')
+ then (Data.map o Symtab.cons_list) (tyco,
+ { mapper = mapper', variances = variances,
+ comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
+ else context
+ end;
+ fun after_qed [single_comp_thm, single_id_thm] lthy =
+ lthy
+ |> Local_Theory.note ((qualify compN, []), single_comp_thm)
+ ||>> Local_Theory.note ((qualify idN, []), single_id_thm)
+ |-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy =>
+ lthy
+ |> Local_Theory.note ((qualify compositionalityN, []),
+ [prove_compositionality lthy comp_thm])
+ |> snd
+ |> Local_Theory.note ((qualify identityN, []),
+ [prove_identity lthy id_thm])
+ |> snd
+ |> Local_Theory.declaration {syntax = false, pervasive = false}
+ (mapper_declaration comp_thm id_thm))
+ in
+ lthy
+ |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
+ end
+
+val functorx = gen_functor Syntax.check_term;
+val functor_cmd = gen_functor Syntax.read_term;
+
+val _ =
+ Outer_Syntax.local_theory_to_proof @{command_spec "functor"}
+ "register operations managing the functorial structure of a type"
+ (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
+ >> (fn (prfx, t) => functor_cmd prfx t));
+
+end;