--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jan 11 14:12:37 2011 +0100
@@ -388,17 +388,17 @@
text {*
\begin{matharray}{rcl}
- @{command_def (HOL) "type_lifting"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
+ @{command_def (HOL) "enriched_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
\end{matharray}
\begin{rail}
- 'type_lifting' (prefix ':')? term
+ 'enriched_type' (prefix ':')? term
;
\end{rail}
\begin{description}
- \item @{command (HOL) "type_lifting"} allows to prove and register
+ \item @{command (HOL) "enriched_type"} allows to prove and register
properties about type constructors which refer to their functorial
structure; these properties then can be used by other packages to
deal with those type constructors in certain type constructions.
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jan 10 22:03:24 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Jan 11 14:12:37 2011 +0100
@@ -403,7 +403,7 @@
\end{matharray}
\begin{rail}
- 'type_lifting' (prefix ':')? term
+ 'enriched_type' (prefix ':')? term
;
\end{rail}
--- a/src/HOL/Datatype.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Datatype.thy Tue Jan 11 14:12:37 2011 +0100
@@ -15,7 +15,7 @@
subsection {* Prelude: lifting over function space *}
-type_lifting map_fun: map_fun
+enriched_type map_fun: map_fun
by (simp_all add: fun_eq_iff)
--- a/src/HOL/Fun.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Fun.thy Tue Jan 11 14:12:37 2011 +0100
@@ -7,7 +7,7 @@
theory Fun
imports Complete_Lattice
-uses ("Tools/type_lifting.ML")
+uses ("Tools/enriched_type.ML")
begin
text{*As a simplification rule, it replaces all function equalities by
@@ -843,6 +843,6 @@
subsubsection {* Functorial structure of types *}
-use "Tools/type_lifting.ML"
+use "Tools/enriched_type.ML"
end
--- a/src/HOL/IsaMakefile Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/IsaMakefile Tue Jan 11 14:12:37 2011 +0100
@@ -241,7 +241,7 @@
Tools/split_rule.ML \
Tools/try.ML \
Tools/typedef.ML \
- Tools/type_lifting.ML \
+ Tools/enriched_type.ML \
Transitive_Closure.thy \
Typedef.thy \
Wellfounded.thy
--- a/src/HOL/Library/Cset.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Library/Cset.thy Tue Jan 11 14:12:37 2011 +0100
@@ -188,7 +188,7 @@
"map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
by (simp add: set_def)
-type_lifting map: map
+enriched_type map: map
by (simp_all add: fun_eq_iff image_compose)
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
--- a/src/HOL/Library/Dlist.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Library/Dlist.thy Tue Jan 11 14:12:37 2011 +0100
@@ -175,7 +175,7 @@
section {* Functorial structure *}
-type_lifting map: map
+enriched_type map: map
by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
--- a/src/HOL/Library/Mapping.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Library/Mapping.thy Tue Jan 11 14:12:37 2011 +0100
@@ -50,7 +50,7 @@
"lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
by (simp add: map_def)
-type_lifting map: map
+enriched_type map: map
by (simp_all add: mapping_eq_iff fun_eq_iff Option.map.compositionality Option.map.id)
--- a/src/HOL/Library/Multiset.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Jan 11 14:12:37 2011 +0100
@@ -1643,7 +1643,7 @@
@{term "{#x+x|x:#M. x<c#}"}.
*}
-type_lifting image_mset: image_mset proof -
+enriched_type 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 Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/List.thy Tue Jan 11 14:12:37 2011 +0100
@@ -880,7 +880,7 @@
"length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
by (induct rule:list_induct2, simp_all)
-type_lifting map: map
+enriched_type map: map
by (simp_all add: fun_eq_iff id_def)
--- a/src/HOL/Option.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Option.thy Tue Jan 11 14:12:37 2011 +0100
@@ -81,7 +81,7 @@
"map f o sum_case g h = sum_case (map f o g) (map f o h)"
by (rule ext) (simp split: sum.split)
-type_lifting map: Option.map proof -
+enriched_type map: Option.map proof -
fix f g
show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
proof
--- a/src/HOL/Predicate.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Predicate.thy Tue Jan 11 14:12:37 2011 +0100
@@ -795,7 +795,7 @@
"eval (map f P) = image f (eval P)"
by (auto simp add: map_def)
-type_lifting map: map
+enriched_type map: map
by (auto intro!: pred_eqI simp add: fun_eq_iff image_compose)
--- a/src/HOL/Product_Type.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Product_Type.thy Tue Jan 11 14:12:37 2011 +0100
@@ -834,7 +834,7 @@
"map_pair f g (a, b) = (f a, g b)"
by (simp add: map_pair_def)
-type_lifting map_pair: map_pair
+enriched_type map_pair: map_pair
by (auto simp add: split_paired_all intro: ext)
lemma fst_map_pair [simp]:
--- a/src/HOL/Sum_Type.thy Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Sum_Type.thy Tue Jan 11 14:12:37 2011 +0100
@@ -95,7 +95,7 @@
"sum_map f1 f2 (Inl a) = Inl (f1 a)"
| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
-type_lifting sum_map: sum_map proof -
+enriched_type 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/enriched_type.ML Tue Jan 11 14:12:37 2011 +0100
@@ -0,0 +1,256 @@
+(* 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 (ProofContext.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 = Simplifier.add_simp (Simpdata.mk_eq @{thm comp_def}) HOL_basic_ss;
+
+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.invents 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.invents 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 = Skip_Proof.prove ctxt [] [] compositionality_prop
+ (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
+ THEN' Simplifier.asm_lr_simp_tac compositionality_ss
+ THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
+ in (comp_prop, prove_compositionality) end;
+
+val identity_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm id_def}) HOL_basic_ss;
+
+fun make_id_prop ctxt variances (tyco, mapper) =
+ let
+ val (vs, ctxt') = 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 = Skip_Proof.prove ctxt [] [] identity_prop
+ (K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss)));
+ 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 tyco T =
+ let
+ val (Ts', T') = strip_type T;
+ val (Ts'', T'') = split_last Ts';
+ in (Ts'', T'', T') 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 (v1, sort1), var2 as (v2, sort2)) =
+ let
+ val coT = TFree var1 --> TFree var2;
+ val contraT = TFree var2 --> TFree var1;
+ val sort = Sign.inter_sort (ProofContext.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 input_mapper = prep_term lthy raw_mapper;
+ val T = fastype_of input_mapper;
+ val _ = Type.no_tvars T;
+ val mapper = singleton (Variable.polymorphic lthy) input_mapper;
+ val _ = if null (Term.add_tfreesT (fastype_of mapper) []) then ()
+ else error ("Illegal locally fixed variables in type: " ^ Syntax.string_of_typ lthy 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 lthy T);
+ 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 = Type.typ_instance (ProofContext.tsig_of (Context.proof_of context));
+ val mapper' = Morphism.term phi mapper;
+ val T_T' = pairself fastype_of (mapper, mapper');
+ in if 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 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 "enriched_type"
+ "register operations managing the functorial structure of a type"
+ Keyword.thy_goal (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
+ >> (fn (prfx, t) => enriched_type_cmd prfx t));
+
+end;
--- a/src/HOL/Tools/type_lifting.ML Mon Jan 10 22:03:24 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-(* Title: HOL/Tools/type_lifting.ML
- Author: Florian Haftmann, TU Muenchen
-
-Functorial structure of types.
-*)
-
-signature TYPE_LIFTING =
-sig
- val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list
- val construct_mapper: Proof.context -> (string * bool -> term)
- -> bool -> typ -> typ -> term
- val type_lifting: string option -> term -> local_theory -> Proof.state
- type entry
- val entries: Proof.context -> entry list Symtab.table
-end;
-
-structure Type_Lifting : TYPE_LIFTING =
-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 (ProofContext.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 = Simplifier.add_simp (Simpdata.mk_eq @{thm comp_def}) HOL_basic_ss;
-
-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.invents 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.invents 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 = Skip_Proof.prove ctxt [] [] compositionality_prop
- (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
- THEN' Simplifier.asm_lr_simp_tac compositionality_ss
- THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
- in (comp_prop, prove_compositionality) end;
-
-val identity_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm id_def}) HOL_basic_ss;
-
-fun make_id_prop ctxt variances (tyco, mapper) =
- let
- val (vs, ctxt') = 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 = Skip_Proof.prove ctxt [] [] identity_prop
- (K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss)));
- 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 tyco T =
- let
- val (Ts', T') = strip_type T;
- val (Ts'', T'') = split_last Ts';
- in (Ts'', T'', T') 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 (v1, sort1), var2 as (v2, sort2)) =
- let
- val coT = TFree var1 --> TFree var2;
- val contraT = TFree var2 --> TFree var1;
- val sort = Sign.inter_sort (ProofContext.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_type_lifting prep_term some_prfx raw_mapper lthy =
- let
- val input_mapper = prep_term lthy raw_mapper;
- val T = fastype_of input_mapper;
- val _ = Type.no_tvars T;
- val mapper = singleton (Variable.polymorphic lthy) input_mapper;
- val _ = if null (Term.add_tfreesT (fastype_of mapper) []) then ()
- else error ("Illegal locally fixed variables in type: " ^ Syntax.string_of_typ lthy 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 lthy T);
- 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 = Type.typ_instance (ProofContext.tsig_of (Context.proof_of context));
- val mapper' = Morphism.term phi mapper;
- val T_T' = pairself fastype_of (mapper, mapper');
- in if 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 false (mapper_declaration comp_thm id_thm))
- in
- lthy
- |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
- end
-
-val type_lifting = gen_type_lifting Syntax.check_term;
-val type_lifting_cmd = gen_type_lifting Syntax.read_term;
-
-val _ = Outer_Syntax.local_theory_to_proof "type_lifting"
- "register operations managing the functorial structure of a type"
- Keyword.thy_goal (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term
- >> (fn (prfx, t) => type_lifting_cmd prfx t));
-
-end;