wenzelm@404: (* Title: Pure/axclass.ML wenzelm@404: ID: $Id$ wenzelm@404: Author: Markus Wenzel, TU Muenchen wenzelm@404: wenzelm@24964: Type classes defined as predicates, associated with a record of wenzelm@24964: parameters. wenzelm@404: *) wenzelm@404: wenzelm@404: signature AX_CLASS = wenzelm@3938: sig haftmann@24589: val define_class: bstring * class list -> string list -> haftmann@24589: ((bstring * attribute list) * term list) list -> theory -> class * theory haftmann@24589: val add_classrel: thm -> theory -> theory haftmann@24589: val add_arity: thm -> theory -> theory haftmann@24589: val prove_classrel: class * class -> tactic -> theory -> theory haftmann@24589: val prove_arity: string * sort list * sort -> tactic -> theory -> theory wenzelm@24964: val get_info: theory -> class -> wenzelm@24964: {def: thm, intro: thm, axioms: thm list, params: (string * typ) list} wenzelm@19243: val class_intros: theory -> thm list haftmann@20107: val class_of_param: theory -> string -> class option wenzelm@19405: val cert_classrel: theory -> class * class -> class * class wenzelm@19405: val read_classrel: theory -> xstring * xstring -> class * class wenzelm@24929: val axiomatize_class: bstring * class list -> theory -> theory wenzelm@24929: val axiomatize_class_cmd: bstring * xstring list -> theory -> theory wenzelm@24929: val axiomatize_classrel: (class * class) list -> theory -> theory wenzelm@24929: val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory wenzelm@24929: val axiomatize_arity: arity -> theory -> theory wenzelm@24929: val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory haftmann@25486: val instance_name: string * class -> string haftmann@25597: val declare_overloaded: string * typ -> theory -> term * theory haftmann@25597: val define_overloaded: string -> string * term -> theory -> thm * theory haftmann@25597: val inst_tyco_of: theory -> string * typ -> string option haftmann@25597: val unoverload: theory -> thm -> thm haftmann@25597: val overload: theory -> thm -> thm haftmann@25597: val unoverload_conv: theory -> conv haftmann@25597: val overload_conv: theory -> conv haftmann@25597: val unoverload_const: theory -> string * typ -> string haftmann@25597: val param_of_inst: theory -> string * string -> string haftmann@25597: val inst_of_param: theory -> string -> (string * string) option haftmann@27397: val these_arity_tags: theory -> class * string -> Markup.property list wenzelm@19574: type cache wenzelm@24929: val of_sort: theory -> typ * sort -> cache -> thm list * cache (*exception Sorts.CLASS_ERROR*) wenzelm@19574: val cache: cache haftmann@26246: val introN: string haftmann@25617: val axiomsN: string wenzelm@3938: end; wenzelm@404: wenzelm@15801: structure AxClass: AX_CLASS = wenzelm@404: struct wenzelm@404: wenzelm@19405: (** theory data **) wenzelm@423: wenzelm@19405: (* class parameters (canonical order) *) wenzelm@423: wenzelm@19405: type param = string * class; wenzelm@423: wenzelm@19405: fun add_param pp ((x, c): param) params = wenzelm@19405: (case AList.lookup (op =) params x of wenzelm@19405: NONE => (x, c) :: params wenzelm@19405: | SOME c' => error ("Duplicate class parameter " ^ quote x ^ wenzelm@19405: " for " ^ Pretty.string_of_sort pp [c] ^ wenzelm@19405: (if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c']))); wenzelm@423: wenzelm@19405: fun merge_params _ ([], qs) = qs wenzelm@19405: | merge_params pp (ps, qs) = wenzelm@19405: fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps; wenzelm@423: wenzelm@423: wenzelm@19511: (* axclasses *) wenzelm@6379: wenzelm@19243: val introN = "intro"; wenzelm@19511: val superN = "super"; wenzelm@19243: val axiomsN = "axioms"; wenzelm@19243: wenzelm@19392: datatype axclass = AxClass of wenzelm@19460: {def: thm, wenzelm@19392: intro: thm, haftmann@21463: axioms: thm list, haftmann@21925: params: (string * typ) list}; wenzelm@19392: wenzelm@19460: type axclasses = axclass Symtab.table * param list; wenzelm@19392: haftmann@27397: fun make_axclass ((def, intro, axioms), params) = AxClass haftmann@27397: {def = def, intro = intro, axioms = axioms, params = params}; wenzelm@19405: wenzelm@19405: fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses = wenzelm@19405: (Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2)); wenzelm@19405: wenzelm@19392: wenzelm@19392: (* instances *) wenzelm@19392: wenzelm@20628: val classrel_prefix = "classrel_"; wenzelm@20628: val arity_prefix = "arity_"; wenzelm@19511: wenzelm@19574: type instances = wenzelm@19574: ((class * class) * thm) list * wenzelm@19574: ((class * sort list) * thm) list Symtab.table; wenzelm@6379: wenzelm@19574: fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) = wenzelm@19574: (merge (eq_fst op =) (classrel1, classrel2), wenzelm@19574: Symtab.join (K (merge (eq_fst op =))) (arities1, arities2)); wenzelm@19392: wenzelm@19392: haftmann@25597: (* instance parameters *) haftmann@25597: haftmann@25597: type inst_params = haftmann@25597: (string * thm) Symtab.table Symtab.table haftmann@25597: (*constant name ~> type constructor ~> (constant name, equation)*) haftmann@25597: * (string * string) Symtab.table; (*constant name ~> (constant name, type constructor)*) haftmann@25597: haftmann@25597: fun merge_inst_params ((const_param1, param_const1), (const_param2, param_const2)) = haftmann@25597: (Symtab.join (K (Symtab.merge (K true))) (const_param1, const_param2), haftmann@25597: Symtab.merge (K true) (param_const1, param_const2)); haftmann@25597: haftmann@25597: wenzelm@19511: (* setup data *) wenzelm@19392: wenzelm@19392: structure AxClassData = TheoryDataFun wenzelm@22846: ( haftmann@25597: type T = axclasses * (instances * inst_params); haftmann@25597: val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty))); wenzelm@19574: val copy = I; wenzelm@19574: val extend = I; haftmann@25597: fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) = haftmann@25597: (merge_axclasses pp (axclasses1, axclasses2), haftmann@25597: (merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2))); wenzelm@22846: ); wenzelm@6379: wenzelm@6379: wenzelm@19574: (* maintain axclasses *) wenzelm@19392: wenzelm@19574: val get_axclasses = #1 o AxClassData.get; haftmann@25597: val map_axclasses = AxClassData.map o apfst; wenzelm@19574: wenzelm@19574: val lookup_def = Symtab.lookup o #1 o get_axclasses; wenzelm@6379: wenzelm@24929: fun get_info thy c = wenzelm@19511: (case lookup_def thy c of wenzelm@19392: SOME (AxClass info) => info wenzelm@21919: | NONE => error ("No such axclass: " ^ quote c)); wenzelm@6379: wenzelm@19123: fun class_intros thy = wenzelm@19392: let wenzelm@19392: fun add_intro c = wenzelm@19511: (case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I); wenzelm@21931: val classes = Sign.all_classes thy; wenzelm@19392: in map (Thm.class_triv thy) classes @ fold add_intro classes [] end; wenzelm@15876: wenzelm@15876: wenzelm@19460: fun get_params thy pred = wenzelm@19574: let val params = #2 (get_axclasses thy); wenzelm@19460: in fold (fn (x, c) => if pred c then cons x else I) params [] end; wenzelm@19460: wenzelm@19460: fun params_of thy c = get_params thy (fn c' => c' = c); wenzelm@19460: fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c])); wenzelm@19460: wenzelm@24964: fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy)); wenzelm@19460: wenzelm@21919: wenzelm@19511: (* maintain instances *) wenzelm@19503: haftmann@25486: fun instance_name (a, c) = NameSpace.base c ^ "_" ^ NameSpace.base a; haftmann@25486: haftmann@25597: val get_instances = #1 o #2 o AxClassData.get; haftmann@25597: val map_instances = AxClassData.map o apsnd o apfst; wenzelm@19528: wenzelm@19528: wenzelm@19574: fun the_classrel thy (c1, c2) = wenzelm@19574: (case AList.lookup (op =) (#1 (get_instances thy)) (c1, c2) of wenzelm@19574: SOME th => Thm.transfer thy th wenzelm@24920: | NONE => error ("Unproven class relation " ^ wenzelm@24920: Syntax.string_of_classrel (ProofContext.init thy) [c1, c2])); wenzelm@19574: wenzelm@19574: fun put_classrel arg = map_instances (fn (classrel, arities) => wenzelm@19574: (insert (eq_fst op =) arg classrel, arities)); wenzelm@19503: wenzelm@19503: wenzelm@19574: fun the_arity thy a (c, Ss) = wenzelm@24929: (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of wenzelm@19574: SOME th => Thm.transfer thy th wenzelm@24920: | NONE => error ("Unproven type arity " ^ wenzelm@24920: Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c]))); wenzelm@19503: haftmann@27397: fun these_arity_tags thy (c, a) = case find_first (fn ((c', _), _) => c = c') haftmann@27397: (these (Symtab.lookup (snd (get_instances thy)) a)) of haftmann@27397: SOME ((_, _), th) => Thm.get_tags th haftmann@27397: | NONE => []; haftmann@27397: wenzelm@19574: fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) => wenzelm@19574: (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th)))); wenzelm@19503: wenzelm@19503: haftmann@27397: haftmann@27397: haftmann@25597: (* maintain instance parameters *) haftmann@25597: haftmann@25597: val get_inst_params = #2 o #2 o AxClassData.get; haftmann@25597: val map_inst_params = AxClassData.map o apsnd o apsnd; haftmann@25597: haftmann@25597: fun get_inst_param thy (c, tyco) = haftmann@25597: (the o Symtab.lookup ((the o Symtab.lookup (fst (get_inst_params thy))) c)) tyco; haftmann@25597: haftmann@25597: fun add_inst_param (c, tyco) inst = (map_inst_params o apfst haftmann@25597: o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst)) haftmann@25597: #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco))); haftmann@25597: haftmann@25597: val inst_of_param = Symtab.lookup o snd o get_inst_params; haftmann@25597: val param_of_inst = fst oo get_inst_param; haftmann@25597: haftmann@25597: fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst) haftmann@25597: (get_inst_params thy) []; haftmann@25597: haftmann@25863: fun inst_tyco_of thy = try (fst o dest_Type o the_single o Sign.const_typargs thy); haftmann@25597: haftmann@25597: fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy); haftmann@25597: fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy)); haftmann@25597: haftmann@25597: fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy); haftmann@25597: fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy)); haftmann@25597: haftmann@25597: fun unoverload_const thy (c_ty as (c, _)) = haftmann@25597: case class_of_param thy c haftmann@25597: of SOME class => (case inst_tyco_of thy c_ty haftmann@25597: of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c haftmann@25597: | NONE => c) haftmann@25597: | NONE => c; haftmann@25597: wenzelm@404: wenzelm@19511: (** instances **) wenzelm@19418: wenzelm@19418: (* class relations *) wenzelm@19418: wenzelm@19405: fun cert_classrel thy raw_rel = wenzelm@15876: let wenzelm@26939: val string_of_sort = Syntax.string_of_sort_global thy; wenzelm@19405: val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; wenzelm@24271: val _ = Sign.primitive_classrel (c1, c2) (Theory.copy thy); wenzelm@19405: val _ = wenzelm@19460: (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of wenzelm@19405: [] => () wenzelm@26939: | xs => raise TYPE ("Class " ^ string_of_sort [c1] ^ " lacks parameter(s) " ^ wenzelm@26939: commas_quote xs ^ " of " ^ string_of_sort [c2], [], [])); wenzelm@19405: in (c1, c2) end; wenzelm@19405: wenzelm@19405: fun read_classrel thy raw_rel = wenzelm@19405: cert_classrel thy (pairself (Sign.read_class thy) raw_rel) wenzelm@19405: handle TYPE (msg, _, _) => error msg; wenzelm@19405: wenzelm@19405: wenzelm@19405: (* primitive rules *) wenzelm@19405: wenzelm@19405: fun add_classrel th thy = wenzelm@19405: let wenzelm@19405: fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); wenzelm@22691: val prop = Thm.plain_prop_of (Thm.transfer thy th); wenzelm@19405: val rel = Logic.dest_classrel prop handle TERM _ => err (); wenzelm@19405: val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); wenzelm@19574: in wenzelm@19574: thy wenzelm@19574: |> Sign.primitive_classrel (c1, c2) wenzelm@19574: |> put_classrel ((c1, c2), Drule.unconstrainTs th) wenzelm@19574: end; wenzelm@15876: wenzelm@19405: fun add_arity th thy = wenzelm@15876: let wenzelm@19528: fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); wenzelm@22691: val prop = Thm.plain_prop_of (Thm.transfer thy th); wenzelm@19528: val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); wenzelm@24731: val _ = map (Sign.certify_sort thy) Ss = Ss orelse err (); haftmann@26516: val _ = case filter_out (fn c => can (get_inst_param thy) (c, t)) (params_of thy c) haftmann@26516: of [] => () haftmann@26516: | cs => Output.legacy_feature haftmann@26516: ("Missing specifications for overloaded parameters " ^ commas_quote cs) haftmann@27397: val th' = th haftmann@27397: |> Drule.unconstrainTs haftmann@27397: |> (Thm.map_tags o AList.default (op =)) haftmann@27397: (Markup.theory_nameN, Context.theory_name thy) wenzelm@19574: in wenzelm@19574: thy wenzelm@19574: |> Sign.primitive_arity (t, Ss, [c]) haftmann@27397: |> put_arity ((t, Ss, c), th') wenzelm@19574: end; wenzelm@404: wenzelm@404: wenzelm@19243: (* tactical proofs *) wenzelm@15876: wenzelm@19405: fun prove_classrel raw_rel tac thy = wenzelm@15876: let wenzelm@24920: val ctxt = ProofContext.init thy; wenzelm@19405: val (c1, c2) = cert_classrel thy raw_rel; wenzelm@24920: val th = Goal.prove ctxt [] [] wenzelm@20049: (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg => wenzelm@19243: cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ wenzelm@24920: quote (Syntax.string_of_classrel ctxt [c1, c2])); wenzelm@19511: in wenzelm@19511: thy wenzelm@20628: |> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])] wenzelm@19511: |-> (fn [th'] => add_classrel th') wenzelm@19511: end; wenzelm@404: wenzelm@19243: fun prove_arity raw_arity tac thy = wenzelm@15876: let wenzelm@24920: val ctxt = ProofContext.init thy; wenzelm@19243: val arity = Sign.cert_arity thy raw_arity; wenzelm@20628: val names = map (prefix arity_prefix) (Logic.name_arities arity); wenzelm@19405: val props = Logic.mk_arities arity; wenzelm@24920: val ths = Goal.prove_multi ctxt [] [] props wenzelm@21687: (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => wenzelm@19243: cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ wenzelm@24920: quote (Syntax.string_of_arity ctxt arity)); wenzelm@19511: in wenzelm@19511: thy wenzelm@20628: |> PureThy.add_thms (map (rpair []) (names ~~ ths)) wenzelm@19511: |-> fold add_arity wenzelm@19511: end; wenzelm@19511: wenzelm@19511: haftmann@25597: (* instance parameters and overloaded definitions *) haftmann@25597: haftmann@25597: (* declaration and definition of instances of overloaded constants *) haftmann@25597: haftmann@25597: fun declare_overloaded (c, T) thy = haftmann@25597: let haftmann@25605: val class = case class_of_param thy c haftmann@25605: of SOME class => class haftmann@25605: | NONE => error ("Not a class parameter: " ^ quote c); haftmann@25605: val tyco = case inst_tyco_of thy (c, T) haftmann@25605: of SOME tyco => tyco haftmann@25605: | NONE => error ("Illegal type for instantiation of class parameter: " wenzelm@26939: ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T)); haftmann@25597: val name_inst = instance_name (tyco, class) ^ "_inst"; haftmann@25597: val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco; haftmann@25597: val T' = Type.strip_sorts T; haftmann@25597: in haftmann@25597: thy haftmann@25597: |> Sign.sticky_prefix name_inst haftmann@25597: |> Sign.no_base_names haftmann@25597: |> Sign.declare_const [] (c', T', NoSyn) haftmann@25597: |-> (fn const' as Const (c'', _) => Thm.add_def false true haftmann@25597: (Thm.def_name c', Logic.mk_equals (Const (c, T'), const')) haftmann@25597: #>> Thm.varifyT haftmann@25597: #-> (fn thm => add_inst_param (c, tyco) (c'', thm) haftmann@25597: #> PureThy.note Thm.internalK (c', thm) haftmann@25597: #> snd haftmann@25597: #> Sign.restore_naming thy haftmann@25597: #> pair (Const (c, T)))) haftmann@25597: end; haftmann@25597: haftmann@25597: fun define_overloaded name (c, t) thy = haftmann@25597: let haftmann@25597: val T = Term.fastype_of t; haftmann@25597: val SOME tyco = inst_tyco_of thy (c, T); haftmann@25597: val (c', eq) = get_inst_param thy (c, tyco); haftmann@25597: val prop = Logic.mk_equals (Const (c', T), t); haftmann@25597: val name' = Thm.def_name_optional haftmann@25597: (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name; haftmann@25597: in haftmann@25597: thy haftmann@25597: |> Thm.add_def false false (name', prop) haftmann@25597: |>> (fn thm => Drule.transitive_thm OF [eq, thm]) haftmann@25597: end; haftmann@25597: haftmann@25597: wenzelm@19511: wenzelm@19511: (** class definitions **) wenzelm@19511: wenzelm@23421: fun split_defined n eq = wenzelm@23421: let wenzelm@23421: val intro = wenzelm@23421: (eq RS Drule.equal_elim_rule2) wenzelm@23421: |> Conjunction.curry_balanced n wenzelm@23421: |> n = 0 ? Thm.eq_assumption 1; wenzelm@23421: val dests = wenzelm@23421: if n = 0 then [] wenzelm@23421: else wenzelm@23421: (eq RS Drule.equal_elim_rule1) wenzelm@23421: |> BalancedTree.dest (fn th => wenzelm@23421: (th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n; wenzelm@23421: in (intro, dests) end; wenzelm@23421: wenzelm@24964: fun define_class (bclass, raw_super) raw_params raw_specs thy = wenzelm@19511: let wenzelm@19511: val ctxt = ProofContext.init thy; wenzelm@24964: val pp = Syntax.pp ctxt; wenzelm@19511: wenzelm@19511: wenzelm@24964: (* class *) wenzelm@19511: wenzelm@19511: val bconst = Logic.const_of_class bclass; wenzelm@19511: val class = Sign.full_name thy bclass; wenzelm@24731: val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super); wenzelm@19511: wenzelm@24964: fun check_constraint (a, S) = wenzelm@24964: if Sign.subsort thy (super, S) then () wenzelm@24964: else error ("Sort constraint of type variable " ^ wenzelm@24964: setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^ wenzelm@24964: " needs to be weaker than " ^ Pretty.string_of_sort pp super); wenzelm@24964: wenzelm@24964: wenzelm@24964: (* params *) wenzelm@24964: wenzelm@24964: val params = raw_params |> map (fn p => wenzelm@24964: let wenzelm@24964: val T = Sign.the_const_type thy p; wenzelm@24964: val _ = wenzelm@24964: (case Term.add_tvarsT T [] of wenzelm@24964: [((a, _), S)] => check_constraint (a, S) wenzelm@24964: | _ => error ("Exactly one type variable expected in class parameter " ^ quote p)); wenzelm@24964: val T' = Term.map_type_tvar (fn _ => TFree (Name.aT, [class])) T; wenzelm@24964: in (p, T') end); wenzelm@24964: wenzelm@24964: wenzelm@24964: (* axioms *) wenzelm@24964: wenzelm@19511: fun prep_axiom t = wenzelm@19511: (case Term.add_tfrees t [] of wenzelm@24964: [(a, S)] => check_constraint (a, S) wenzelm@24964: | [] => () wenzelm@24964: | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t); wenzelm@24964: t wenzelm@24964: |> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U)) wenzelm@24964: |> Logic.close_form); wenzelm@19511: wenzelm@24681: val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs; haftmann@22745: val name_atts = map fst raw_specs; wenzelm@19511: wenzelm@19511: wenzelm@19511: (* definition *) wenzelm@19511: wenzelm@19511: val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss; wenzelm@19511: val class_eq = wenzelm@23421: Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_balanced conjs); wenzelm@19511: wenzelm@19511: val ([def], def_thy) = wenzelm@19511: thy wenzelm@19511: |> Sign.primitive_class (bclass, super) wenzelm@19511: |> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])]; wenzelm@19511: val (raw_intro, (raw_classrel, raw_axioms)) = wenzelm@23421: split_defined (length conjs) def ||> chop (length super); wenzelm@19392: wenzelm@19418: wenzelm@19511: (* facts *) wenzelm@19511: wenzelm@19511: val class_triv = Thm.class_triv def_thy class; wenzelm@19511: val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) = wenzelm@19511: def_thy wenzelm@19511: |> PureThy.note_thmss_qualified "" bconst wenzelm@19511: [((introN, []), [([Drule.standard raw_intro], [])]), wenzelm@19511: ((superN, []), [(map Drule.standard raw_classrel, [])]), wenzelm@19511: ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]; wenzelm@19511: wenzelm@24847: wenzelm@19511: (* result *) wenzelm@19511: wenzelm@24964: val axclass = make_axclass ((def, intro, axioms), params); wenzelm@19511: val result_thy = wenzelm@19511: facts_thy wenzelm@19574: |> fold put_classrel (map (pair class) super ~~ classrel) wenzelm@19511: |> Sign.add_path bconst wenzelm@19511: |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd wenzelm@19511: |> Sign.restore_naming facts_thy wenzelm@19574: |> map_axclasses (fn (axclasses, parameters) => wenzelm@21919: (Symtab.update (class, axclass) axclasses, wenzelm@24964: fold (fn (x, _) => add_param pp (x, class)) params parameters)); wenzelm@19511: wenzelm@19511: in (class, result_thy) end; wenzelm@19511: wenzelm@19511: wenzelm@19531: wenzelm@19511: (** axiomatizations **) wenzelm@19511: wenzelm@19511: local wenzelm@19511: wenzelm@20628: fun axiomatize prep mk name add raw_args thy = wenzelm@20628: let wenzelm@20628: val args = prep thy raw_args; wenzelm@20628: val specs = mk args; wenzelm@20628: val names = name args; wenzelm@20628: in thy |> PureThy.add_axioms_i (map (rpair []) (names ~~ specs)) |-> fold add end; wenzelm@19511: wenzelm@19511: fun ax_classrel prep = wenzelm@20628: axiomatize (map o prep) (map Logic.mk_classrel) wenzelm@20628: (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; wenzelm@19511: wenzelm@19511: fun ax_arity prep = wenzelm@20628: axiomatize prep Logic.mk_arities wenzelm@20628: (map (prefix arity_prefix) o Logic.name_arities) add_arity; wenzelm@19511: wenzelm@19706: fun class_const c = wenzelm@19706: (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT); wenzelm@19706: wenzelm@19511: fun ax_class prep_class prep_classrel (bclass, raw_super) thy = wenzelm@19511: let wenzelm@19511: val class = Sign.full_name thy bclass; wenzelm@24731: val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy; wenzelm@19511: in wenzelm@19511: thy wenzelm@19511: |> Sign.primitive_class (bclass, super) wenzelm@19511: |> ax_classrel prep_classrel (map (fn c => (class, c)) super) wenzelm@19706: |> Theory.add_deps "" (class_const class) (map class_const super) wenzelm@19511: end; wenzelm@19511: wenzelm@19511: in wenzelm@19511: wenzelm@24929: val axiomatize_class = ax_class Sign.certify_class cert_classrel; wenzelm@24929: val axiomatize_class_cmd = ax_class Sign.read_class read_classrel; wenzelm@24929: val axiomatize_classrel = ax_classrel cert_classrel; wenzelm@24929: val axiomatize_classrel_cmd = ax_classrel read_classrel; wenzelm@24929: val axiomatize_arity = ax_arity Sign.cert_arity; wenzelm@24929: val axiomatize_arity_cmd = ax_arity Sign.read_arity; wenzelm@19511: wenzelm@19511: end; wenzelm@19511: wenzelm@19511: wenzelm@19511: wenzelm@19511: (** explicit derivations -- cached **) wenzelm@19511: wenzelm@19574: datatype cache = Types of (class * thm) list Typtab.table; wenzelm@19574: wenzelm@19511: local wenzelm@19503: wenzelm@19574: fun lookup_type (Types cache) = AList.lookup (op =) o Typtab.lookup_list cache; wenzelm@19574: fun insert_type T der (Types cache) = Types (Typtab.insert_list (eq_fst op =) (T, der) cache); wenzelm@19503: wenzelm@19522: fun derive_type _ (_, []) = [] wenzelm@19522: | derive_type thy (typ, sort) = wenzelm@19522: let wenzelm@19528: val vars = Term.fold_atyps wenzelm@19522: (fn T as TFree (_, S) => insert (eq_fst op =) (T, S) wenzelm@19522: | T as TVar (_, S) => insert (eq_fst op =) (T, S) wenzelm@19528: | _ => I) typ []; wenzelm@19574: val hyps = vars wenzelm@19574: |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S)); wenzelm@26939: val ths = (typ, sort) wenzelm@26939: |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy) wenzelm@22570: {class_relation = wenzelm@19574: fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2), wenzelm@22570: type_constructor = wenzelm@19574: fn a => fn dom => fn c => wenzelm@19574: let val Ss = map (map snd) dom and ths = maps (map fst) dom wenzelm@19574: in ths MRS the_arity thy a (c, Ss) end, wenzelm@22570: type_variable = wenzelm@19574: the_default [] o AList.lookup (op =) hyps}; wenzelm@19574: in ths end; wenzelm@19503: wenzelm@19511: in wenzelm@19511: wenzelm@19574: fun of_sort thy (typ, sort) cache = wenzelm@19574: let wenzelm@19574: val sort' = filter (is_none o lookup_type cache typ) sort; wenzelm@19574: val ths' = derive_type thy (typ, sort') wenzelm@19574: handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^ wenzelm@26939: Syntax.string_of_typ_global thy typ ^ " :: " ^ Syntax.string_of_sort_global thy sort'); wenzelm@19574: val cache' = cache |> fold (insert_type typ) (sort' ~~ ths'); wenzelm@19574: val ths = wenzelm@19574: sort |> map (fn c => wenzelm@19574: Goal.finish (the (lookup_type cache' typ c) RS wenzelm@19574: Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c)))) wenzelm@20260: |> Thm.adjust_maxidx_thm ~1); wenzelm@19574: in (ths, cache') end; wenzelm@19503: wenzelm@19511: end; wenzelm@19418: wenzelm@24929: val cache = Types Typtab.empty; wenzelm@24929: wenzelm@15876: end;