# HG changeset patch # User wenzelm # Date 1294761621 -3600 # Node ID f1e7e244dcf5bdeb25b5340845c5dc6f7edf1a15 # Parent 4c717333b0cc68033e9aada14f4dcbcf81111f3b# Parent f0f20a5b54df254b25706e590c83933d3bd3bb14 merged diff -r f0f20a5b54df -r f1e7e244dcf5 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jan 11 17:00:21 2011 +0100 @@ -388,22 +388,22 @@ text {* \begin{matharray}{rcl} - @{command_def (HOL) "type_lifting"} & : & @{text "local_theory \ proof(prove)"} + @{command_def (HOL) "enriched_type"} & : & @{text "local_theory \ 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 - properties about type constructors which refer to their functorial - structure; these properties then can be used by other packages to + \item @{command (HOL) "enriched_type"} 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. Characteristic theorems are noted in the current local theory; by - default, they are prefixed with base name of the type constructor, + default, they are prefixed with the base name of the type constructor, an explicit prefix can be given alternatively. The given term @{text "m"} is considered as \emph{mapper} for the diff -r f0f20a5b54df -r f1e7e244dcf5 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Jan 11 16:23:28 2011 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Jan 11 17:00:21 2011 +0100 @@ -399,22 +399,22 @@ % \begin{isamarkuptext}% \begin{matharray}{rcl} - \indexdef{HOL}{command}{type\_lifting}\hypertarget{command.HOL.type-lifting}{\hyperlink{command.HOL.type-lifting}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}lifting}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} + \indexdef{HOL}{command}{enriched\_type}\hypertarget{command.HOL.enriched-type}{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \end{matharray} \begin{rail} - 'type_lifting' (prefix ':')? term + 'enriched_type' (prefix ':')? term ; \end{rail} \begin{description} - \item \hyperlink{command.HOL.type-lifting}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}lifting}}}} 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 + \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} 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. Characteristic theorems are noted in the current local theory; by - default, they are prefixed with base name of the type constructor, + default, they are prefixed with the base name of the type constructor, an explicit prefix can be given alternatively. The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/Datatype.thy Tue Jan 11 17:00:21 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) diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/Fun.thy Tue Jan 11 17:00:21 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 diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/IsaMakefile Tue Jan 11 17:00:21 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 diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Library/Cset.thy --- a/src/HOL/Library/Cset.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/Library/Cset.thy Tue Jan 11 17:00:21 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 \ bool) \ 'a Cset.set \ 'a Cset.set" where diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Library/Dlist.thy --- a/src/HOL/Library/Dlist.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/Library/Dlist.thy Tue Jan 11 17:00:21 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) diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/Library/Mapping.thy Tue Jan 11 17:00:21 2011 +0100 @@ -50,7 +50,7 @@ "lookup (map f g m) = Option.map g \ lookup m \ 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) diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/Library/Multiset.thy Tue Jan 11 17:00:21 2011 +0100 @@ -1643,7 +1643,7 @@ @{term "{#x+x|x:#M. x image_mset g = image_mset (f \ g)" proof diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/List.thy --- a/src/HOL/List.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/List.thy Tue Jan 11 17:00:21 2011 +0100 @@ -880,7 +880,7 @@ "length xs = length ys \ 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) diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Option.thy --- a/src/HOL/Option.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/Option.thy Tue Jan 11 17:00:21 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 \ Option.map g = Option.map (f \ g)" proof diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/Predicate.thy Tue Jan 11 17:00:21 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) diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/Product_Type.thy Tue Jan 11 17:00:21 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]: diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Tue Jan 11 16:23:28 2011 +0100 +++ b/src/HOL/Sum_Type.thy Tue Jan 11 17:00:21 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 \ sum_map h i = sum_map (f \ h) (g \ i)" proof diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Tools/enriched_type.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/enriched_type.ML Tue Jan 11 17:00:21 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; diff -r f0f20a5b54df -r f1e7e244dcf5 src/HOL/Tools/type_lifting.ML --- a/src/HOL/Tools/type_lifting.ML Tue Jan 11 16:23:28 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;