haftmann@24218: (* Title: Pure/Isar/class.ML haftmann@24218: ID: $Id$ haftmann@24218: Author: Florian Haftmann, TU Muenchen haftmann@24218: haftmann@24218: Type classes derived from primitive axclasses and locales. haftmann@24218: *) haftmann@24218: haftmann@24218: signature CLASS = haftmann@24218: sig haftmann@25462: (*classes*) haftmann@26247: val class: bstring -> class list -> Element.context_i list haftmann@26518: -> theory -> string * Proof.context haftmann@26247: val class_cmd: bstring -> xstring list -> Element.context list haftmann@26518: -> theory -> string * Proof.context haftmann@25485: haftmann@25311: val init: class -> theory -> Proof.context wenzelm@28017: val declare: class -> Properties.T haftmann@27690: -> (string * mixfix) * term -> theory -> theory wenzelm@28017: val abbrev: class -> Syntax.mode -> Properties.T wenzelm@25104: -> (string * mixfix) * term -> theory -> theory haftmann@27690: val note: class -> string wenzelm@28084: -> (Attrib.binding * (thm list * Attrib.src list) list) list haftmann@27690: -> theory -> (bstring * thm list) list * theory haftmann@27690: val declaration: class -> declaration -> theory -> theory haftmann@25083: val refresh_syntax: class -> Proof.context -> Proof.context haftmann@25485: haftmann@24589: val intro_classes_tac: thm list -> tactic haftmann@26470: val default_intro_tac: Proof.context -> thm list -> tactic haftmann@27684: val prove_subclass: class * class -> thm option -> theory -> theory haftmann@25485: haftmann@25485: val class_prefix: string -> string haftmann@25485: val is_class: theory -> class -> bool haftmann@26518: val these_params: theory -> sort -> (string * (class * (string * typ))) list haftmann@24589: val print_classes: theory -> unit haftmann@24423: haftmann@25462: (*instances*) haftmann@26247: val init_instantiation: string list * (string * sort) list * sort haftmann@26247: -> theory -> local_theory haftmann@26247: val instantiation_instance: (local_theory -> local_theory) haftmann@26247: -> local_theory -> Proof.state haftmann@26247: val prove_instantiation_instance: (Proof.context -> tactic) haftmann@26247: -> local_theory -> local_theory haftmann@25485: val conclude_instantiation: local_theory -> local_theory haftmann@25603: val instantiation_param: local_theory -> string -> string option haftmann@25485: val confirm_declaration: string -> local_theory -> local_theory haftmann@25603: val pretty_instantiation: local_theory -> Pretty.T haftmann@26259: val type_name: string -> string haftmann@25485: haftmann@25462: (*old axclass layer*) haftmann@25462: val axclass_cmd: bstring * xstring list wenzelm@28084: -> (Attrib.binding * string list) list haftmann@25462: -> theory -> class * theory haftmann@25462: val classrel_cmd: xstring * xstring -> theory -> Proof.state haftmann@25462: haftmann@25462: (*old instance layer*) haftmann@25536: val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state haftmann@25536: val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state haftmann@24218: end; haftmann@24218: haftmann@24218: structure Class : CLASS = haftmann@24218: struct haftmann@24218: haftmann@24218: (** auxiliary **) haftmann@24218: haftmann@25002: fun prove_interpretation tac prfx_atts expr inst = haftmann@25002: Locale.interpretation_i I prfx_atts expr inst haftmann@24589: #> Proof.global_terminal_proof ballarin@27761: (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE) haftmann@24589: #> ProofContext.theory_of; haftmann@24589: haftmann@25195: fun prove_interpretation_in tac after_qed (name, expr) = haftmann@25195: Locale.interpretation_in_locale haftmann@25195: (ProofContext.theory after_qed) (name, expr) haftmann@25195: #> Proof.global_terminal_proof haftmann@25195: (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) haftmann@25195: #> ProofContext.theory_of; haftmann@25195: haftmann@24589: haftmann@25485: (** primitive axclass and instance commands **) haftmann@24589: haftmann@24218: fun axclass_cmd (class, raw_superclasses) raw_specs thy = haftmann@24218: let haftmann@24218: val ctxt = ProofContext.init thy; haftmann@24218: val superclasses = map (Sign.read_class thy) raw_superclasses; haftmann@24589: val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) haftmann@24589: raw_specs; haftmann@24589: val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) haftmann@24589: raw_specs) haftmann@24218: |> snd haftmann@24218: |> (map o map) fst; haftmann@24589: in haftmann@24589: AxClass.define_class (class, superclasses) [] haftmann@24589: (name_atts ~~ axiomss) thy haftmann@24589: end; haftmann@24218: haftmann@24218: local haftmann@24218: haftmann@24218: fun gen_instance mk_prop add_thm after_qed insts thy = haftmann@24218: let haftmann@24218: fun after_qed' results = haftmann@24218: ProofContext.theory ((fold o fold) add_thm results #> after_qed); haftmann@24218: in haftmann@24218: thy haftmann@24218: |> ProofContext.init haftmann@24589: |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) haftmann@25536: o mk_prop thy) insts) haftmann@24218: end; haftmann@24218: haftmann@24218: in haftmann@24218: haftmann@24589: val instance_arity = haftmann@24218: gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; haftmann@25502: val instance_arity_cmd = haftmann@25502: gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I; haftmann@24589: val classrel = haftmann@25536: gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I; haftmann@24589: val classrel_cmd = haftmann@25536: gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I; haftmann@24218: haftmann@24218: end; (*local*) haftmann@24218: haftmann@24218: haftmann@24589: (** class data **) haftmann@24218: haftmann@24218: datatype class_data = ClassData of { haftmann@24218: consts: (string * string) list haftmann@24836: (*locale parameter ~> constant name*), haftmann@25062: base_sort: sort, haftmann@25083: inst: term option list haftmann@25083: (*canonical interpretation*), haftmann@25711: morphism: theory -> thm list -> morphism, haftmann@25062: (*partial morphism of canonical interpretation*) haftmann@25618: assm_intro: thm option, haftmann@25618: of_class: thm, haftmann@25618: axiom: thm option, haftmann@24657: defs: thm list, haftmann@25368: operations: (string * (class * (typ * term))) list haftmann@24657: }; haftmann@24218: haftmann@24657: fun rep_class_data (ClassData d) = d; haftmann@25618: fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom), haftmann@25368: (defs, operations)) = haftmann@25062: ClassData { consts = consts, base_sort = base_sort, inst = inst, wenzelm@26463: morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom, haftmann@25618: defs = defs, operations = operations }; haftmann@25618: fun map_class_data f (ClassData { consts, base_sort, inst, morphism, haftmann@25618: assm_intro, of_class, axiom, defs, operations }) = haftmann@25618: mk_class_data (f ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom), haftmann@25368: (defs, operations))); haftmann@25038: fun merge_class_data _ (ClassData { consts = consts, haftmann@25618: base_sort = base_sort, inst = inst, morphism = morphism, assm_intro = assm_intro, haftmann@25618: of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 }, haftmann@25618: ClassData { consts = _, base_sort = _, inst = _, morphism = _, assm_intro = _, haftmann@25618: of_class = _, axiom = _, defs = defs2, operations = operations2 }) = haftmann@25618: mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom), haftmann@24914: (Thm.merge_thms (defs1, defs2), haftmann@25368: AList.merge (op =) (K true) (operations1, operations2))); haftmann@24218: haftmann@24218: structure ClassData = TheoryDataFun haftmann@24218: ( haftmann@25038: type T = class_data Graph.T haftmann@25038: val empty = Graph.empty; haftmann@24218: val copy = I; haftmann@24218: val extend = I; haftmann@25038: fun merge _ = Graph.join merge_class_data; haftmann@24218: ); haftmann@24218: haftmann@24218: haftmann@24218: (* queries *) haftmann@24218: haftmann@25038: val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get; haftmann@24218: haftmann@24589: fun the_class_data thy class = case lookup_class_data thy class wenzelm@25020: of NONE => error ("Undeclared class " ^ quote class) haftmann@24589: | SOME data => data; haftmann@24218: haftmann@25038: val is_class = is_some oo lookup_class_data; haftmann@25038: haftmann@25038: val ancestry = Graph.all_succs o ClassData.get; haftmann@24218: haftmann@25002: fun these_params thy = haftmann@24218: let haftmann@24218: fun params class = haftmann@24218: let wenzelm@24930: val const_typs = (#params o AxClass.get_info thy) class; haftmann@24657: val const_names = (#consts o the_class_data thy) class; haftmann@24218: in haftmann@26518: (map o apsnd) haftmann@26518: (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names haftmann@24218: end; haftmann@24218: in maps params o ancestry thy end; haftmann@24218: haftmann@24657: fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy; haftmann@24218: haftmann@25711: fun morphism thy class = #morphism (the_class_data thy class) thy (these_defs thy [class]); haftmann@25062: haftmann@25618: fun these_assm_intros thy = haftmann@25618: Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm) haftmann@25618: ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) []; haftmann@24218: haftmann@24836: fun these_operations thy = haftmann@24836: maps (#operations o the_class_data thy) o ancestry thy; haftmann@24657: haftmann@24218: fun print_classes thy = haftmann@24218: let wenzelm@24920: val ctxt = ProofContext.init thy; haftmann@24218: val algebra = Sign.classes_of thy; haftmann@24218: val arities = haftmann@24218: Symtab.empty haftmann@24218: |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => haftmann@24218: Symtab.map_default (class, []) (insert (op =) tyco)) arities) haftmann@24218: ((#arities o Sorts.rep_algebra) algebra); haftmann@24218: val the_arities = these o Symtab.lookup arities; haftmann@24218: fun mk_arity class tyco = haftmann@24218: let haftmann@24218: val Ss = Sorts.mg_domain algebra tyco [class]; wenzelm@24920: in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; haftmann@24218: fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " wenzelm@24920: ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty); haftmann@24218: fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ haftmann@25062: (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), haftmann@24218: (SOME o Pretty.block) [Pretty.str "supersort: ", wenzelm@24920: (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class], haftmann@25062: if is_class thy class then (SOME o Pretty.str) haftmann@25062: ("locale: " ^ Locale.extern thy class) else NONE, haftmann@25062: ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) haftmann@25062: (Pretty.str "parameters:" :: ps)) o map mk_param wenzelm@24930: o these o Option.map #params o try (AxClass.get_info thy)) class, haftmann@24218: (SOME o Pretty.block o Pretty.breaks) [ haftmann@24218: Pretty.str "instances:", haftmann@24218: Pretty.list "" "" (map (mk_arity class) (the_arities class)) haftmann@24218: ] haftmann@24218: ] haftmann@24218: in haftmann@24589: (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") haftmann@24589: o map mk_entry o Sorts.all_classes) algebra haftmann@24218: end; haftmann@24218: haftmann@24218: haftmann@24218: (* updaters *) haftmann@24218: haftmann@25618: fun add_class_data ((class, superclasses), haftmann@25711: (params, base_sort, inst, phi, axiom, assm_intro, of_class)) thy = haftmann@25002: let haftmann@25368: val operations = map (fn (v_ty as (_, ty), (c, _)) => haftmann@25683: (c, (class, (ty, Free v_ty)))) params; haftmann@25038: val add_class = Graph.new_node (class, haftmann@25683: mk_class_data (((map o pairself) fst params, base_sort, haftmann@25618: map (SOME o Const) inst, phi, assm_intro, of_class, axiom), ([], operations))) haftmann@25002: #> fold (curry Graph.add_edge class) superclasses; haftmann@25618: in ClassData.map add_class thy end; haftmann@24218: haftmann@25368: fun register_operation class (c, (t, some_def)) thy = haftmann@25062: let haftmann@25368: val base_sort = (#base_sort o the_class_data thy) class; haftmann@26518: val prep_typ = map_type_tvar haftmann@26518: (fn (vi as (v, _), sort) => if Name.aT = v haftmann@25368: then TFree (v, base_sort) else TVar (vi, sort)); haftmann@25368: val t' = map_types prep_typ t; haftmann@25368: val ty' = Term.fastype_of t'; haftmann@25062: in haftmann@25062: thy haftmann@25062: |> (ClassData.map o Graph.map_node class o map_class_data o apsnd) haftmann@25368: (fn (defs, operations) => haftmann@25096: (fold cons (the_list some_def) defs, haftmann@25368: (c, (class, (ty', t'))) :: operations)) haftmann@25062: end; haftmann@24218: haftmann@24589: haftmann@24589: (** rule calculation, tactics and methods **) haftmann@24589: wenzelm@25024: val class_prefix = Logic.const_of_class o Sign.base_name; wenzelm@25024: haftmann@26247: fun calculate sups base_sort assm_axiom param_map class thy = haftmann@25062: let haftmann@25711: (*static parts of morphism*) haftmann@26518: val subst_typ = map_type_tfree (fn (v, sort) => haftmann@26518: if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort)); haftmann@25683: fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) param_map v haftmann@25062: of SOME (c, _) => Const (c, ty) haftmann@25062: | NONE => t) haftmann@25062: | subst_aterm t = t; haftmann@25711: fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0)) haftmann@25711: (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy) haftmann@25711: (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty), haftmann@25711: Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map); haftmann@27690: (*fun inst thy sort thm = (tracing (makestring thm); instantiate thy sort thm); haftmann@27690: val instantiate = inst;*) haftmann@25683: val (proto_assm_intro, locale_intro) = Locale.intros thy class haftmann@25683: |> pairself (try the_single); haftmann@25683: val axiom_premises = map_filter (#axiom o the_class_data thy) sups haftmann@25683: @ the_list assm_axiom; haftmann@25711: val axiom = locale_intro haftmann@27690: |> Option.map (Thm.close_derivation o Drule.standard' o (fn thm => thm OF axiom_premises) o instantiate thy [class]) haftmann@25711: |> (fn x as SOME _ => x | NONE => assm_axiom); haftmann@25711: val lift_axiom = case axiom haftmann@27690: of SOME axiom => (fn thm => ((*tracing "-(morphism)-"; haftmann@27690: tracing (makestring thm); haftmann@27690: tracing (makestring axiom);*) haftmann@27690: Thm.implies_elim thm axiom)) haftmann@25683: | NONE => I; haftmann@25062: haftmann@25711: (*dynamic parts of morphism*) haftmann@27708: fun avoid_a thy thm = haftmann@27708: let haftmann@27708: val tvars = Term.add_tvars (Thm.prop_of thm) []; haftmann@27708: val thm' = case AList.lookup (op =) tvars (Name.aT, 0) haftmann@27708: of SOME sort => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o rpair sort o rpair 0) haftmann@27708: (Name.aT, Name.variant (map (fst o fst) tvars) Name.aT)], []) thm haftmann@27708: | NONE => thm; haftmann@27708: in thm' end; haftmann@25711: fun rew_term thy defs = Pattern.rewrite_term thy haftmann@25711: (map (Logic.dest_equals o Thm.prop_of) defs) []; haftmann@25711: fun subst_term thy defs = map_aterms subst_aterm #> rew_term thy defs haftmann@25711: #> map_types subst_typ; haftmann@27708: fun subst_thm thy defs = Drule.zero_var_indexes #> avoid_a thy haftmann@27708: #> Drule.standard' #> instantiate thy [class] #> lift_axiom haftmann@25711: #> MetaSimplifier.rewrite_rule defs; wenzelm@26463: fun morphism thy defs = haftmann@25711: Morphism.typ_morphism subst_typ haftmann@25711: $> Morphism.term_morphism (subst_term thy defs) haftmann@27690: $> Morphism.thm_morphism (subst_thm thy defs); haftmann@25711: haftmann@25711: (*class rules*) haftmann@25711: val defs = these_defs thy sups; haftmann@25618: val assm_intro = proto_assm_intro haftmann@27690: |> Option.map (instantiate thy base_sort) haftmann@25711: |> Option.map (MetaSimplifier.rewrite_rule defs) wenzelm@26628: |> Option.map Thm.close_derivation; haftmann@26247: val class_intro = (#intro o AxClass.get_info thy) class; haftmann@25711: val fixate = Thm.instantiate haftmann@25711: (map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)), haftmann@25711: (TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], []) haftmann@25618: val of_class_sups = if null sups haftmann@25711: then map (fixate o Thm.class_triv thy) base_sort haftmann@25711: else map (fixate o #of_class o the_class_data thy) sups; haftmann@25683: val locale_dests = map Drule.standard' (Locale.dests thy class); haftmann@25711: val num_trivs = case length locale_dests haftmann@25711: of 0 => if is_none axiom then 0 else 1 haftmann@25711: | n => n; haftmann@25711: val pred_trivs = if num_trivs = 0 then [] haftmann@25711: else the axiom haftmann@25711: |> Thm.prop_of haftmann@25711: |> (map_types o map_atyps o K) (TFree (Name.aT, base_sort)) haftmann@25711: |> (Thm.assume o Thm.cterm_of thy) haftmann@25711: |> replicate num_trivs; haftmann@26247: val of_class = (fixate class_intro OF of_class_sups OF locale_dests OF pred_trivs) haftmann@25711: |> Drule.standard' wenzelm@26628: |> Thm.close_derivation; haftmann@26247: val this_intro = assm_intro |> the_default class_intro; haftmann@26247: in haftmann@26247: thy haftmann@26247: |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN) haftmann@27684: |> PureThy.store_thm (AxClass.introN, this_intro) haftmann@26247: |> snd haftmann@26247: |> Sign.restore_naming thy haftmann@26247: |> pair (morphism, axiom, assm_intro, of_class) haftmann@26247: end; haftmann@24589: haftmann@27690: fun class_interpretation class facts defs thy = thy; haftmann@27690: haftmann@24589: fun class_interpretation class facts defs thy = haftmann@24589: let haftmann@26518: val consts = map (apsnd fst o snd) (these_params thy [class]); haftmann@26518: val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT, haftmann@26518: [class]))) (Sign.the_const_type thy c)) consts; haftmann@26238: val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints; haftmann@26238: fun add_constraint c T = Sign.add_const_constraint (c, SOME T); haftmann@25083: val inst = (#inst o the_class_data thy) class; ballarin@27761: fun tac ctxt = ALLGOALS (ProofContext.fact_tac facts ballarin@27761: ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n)); haftmann@25038: val prfx = class_prefix class; haftmann@24589: in haftmann@25038: thy haftmann@26518: |> fold2 add_constraint (map snd consts) no_constraints haftmann@26238: |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) wenzelm@28084: (inst, map (fn def => (Attrib.no_binding, def)) defs) haftmann@26518: |> fold2 add_constraint (map snd consts) constraints haftmann@24589: end; haftmann@24218: haftmann@27684: fun prove_subclass (sub, sup) some_thm thy = haftmann@25618: let haftmann@25711: val of_class = (#of_class o the_class_data thy) sup; haftmann@27684: val intro = case some_thm haftmann@27684: of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm]) haftmann@27684: | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0)) haftmann@27684: ([], [sub])], []) of_class; haftmann@27684: val classrel = (intro OF (the_list o #axiom o the_class_data thy) sub) haftmann@27684: |> Thm.close_derivation; haftmann@25618: in haftmann@25618: thy haftmann@25618: |> AxClass.add_classrel classrel haftmann@27684: |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac (the_list some_thm))) haftmann@25618: I (sub, Locale.Locale sup) haftmann@25618: |> ClassData.map (Graph.add_edge (sub, sup)) haftmann@25618: end; haftmann@25618: haftmann@24218: fun intro_classes_tac facts st = haftmann@24218: let haftmann@24218: val thy = Thm.theory_of_thm st; haftmann@24218: val classes = Sign.all_classes thy; haftmann@24218: val class_trivs = map (Thm.class_triv thy) classes; haftmann@25618: val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; haftmann@25618: val assm_intros = these_assm_intros thy; haftmann@24218: in haftmann@25618: Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st haftmann@24218: end; haftmann@24218: haftmann@26470: fun default_intro_tac ctxt [] = haftmann@26470: intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] haftmann@26470: | default_intro_tac _ _ = no_tac; haftmann@24218: haftmann@24218: fun default_tac rules ctxt facts = haftmann@24218: HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE haftmann@26470: default_intro_tac ctxt facts; haftmann@24218: wenzelm@26463: val _ = Context.>> (Context.map_theory wenzelm@26463: (Method.add_methods wenzelm@26463: [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), wenzelm@26463: "back-chain introduction rules of classes"), wenzelm@26463: ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), wenzelm@26463: "apply some intro/elim rule")])); wenzelm@26463: haftmann@24218: haftmann@24589: (** classes and class target **) haftmann@24218: haftmann@25002: (* class context syntax *) haftmann@24748: haftmann@26238: fun synchronize_class_syntax sups base_sort ctxt = haftmann@24914: let wenzelm@25344: val thy = ProofContext.theory_of ctxt; haftmann@26596: val algebra = Sign.classes_of thy; haftmann@25083: val operations = these_operations thy sups; haftmann@26518: fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort))); haftmann@26518: val primary_constraints = haftmann@25368: (map o apsnd) (subst_class_typ base_sort o fst o snd) operations; haftmann@26518: val secondary_constraints = haftmann@25368: (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations; wenzelm@25318: fun declare_const (c, _) = wenzelm@25318: let val b = Sign.base_name c wenzelm@25344: in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; haftmann@26518: fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c haftmann@26238: of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty haftmann@26238: of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0) haftmann@26596: of SOME (_, ty' as TVar (tvar as (vi, sort))) => haftmann@26238: if TypeInfer.is_param vi haftmann@26596: andalso Sorts.sort_le algebra (base_sort, sort) haftmann@26596: then SOME (ty', TFree (Name.aT, base_sort)) haftmann@26596: else NONE haftmann@26238: | _ => NONE) haftmann@26238: | NONE => NONE) haftmann@26238: | NONE => NONE) haftmann@26238: fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c); haftmann@25368: val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations; haftmann@25083: in haftmann@25083: ctxt haftmann@26518: |> fold declare_const primary_constraints haftmann@26518: |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints), haftmann@26730: (((improve, subst), true), unchecks)), false)) haftmann@26518: |> Overloading.set_primary_constraints haftmann@25083: end; haftmann@25083: haftmann@25083: fun refresh_syntax class ctxt = haftmann@25002: let haftmann@25002: val thy = ProofContext.theory_of ctxt; haftmann@25062: val base_sort = (#base_sort o the_class_data thy) class; haftmann@26238: in synchronize_class_syntax [class] base_sort ctxt end; haftmann@25002: wenzelm@25344: fun init_ctxt sups base_sort ctxt = haftmann@25083: ctxt haftmann@25083: |> Variable.declare_term haftmann@25083: (Logic.mk_type (TFree (Name.aT, base_sort))) haftmann@26238: |> synchronize_class_syntax sups base_sort haftmann@26238: |> Overloading.add_improvable_syntax; haftmann@24901: haftmann@25311: fun init class thy = haftmann@25311: thy haftmann@25311: |> Locale.init class wenzelm@25344: |> init_ctxt [class] ((#base_sort o the_class_data thy) class); haftmann@24914: haftmann@24748: haftmann@27690: (* class target *) haftmann@27690: haftmann@27690: fun declare class pos ((c, mx), dict) thy = haftmann@27690: let haftmann@27690: val prfx = class_prefix class; haftmann@27690: val thy' = thy |> Sign.add_path prfx; haftmann@27690: val phi = morphism thy' class; haftmann@27690: haftmann@27690: val c' = Sign.full_name thy' c; haftmann@27690: val dict' = Morphism.term phi dict; haftmann@27690: val dict_def = map_types Logic.unvarifyT dict'; haftmann@27690: val ty' = Term.fastype_of dict_def; haftmann@27690: val ty'' = Type.strip_sorts ty'; haftmann@27690: val def_eq = Logic.mk_equals (Const (c', ty'), dict_def); haftmann@27690: fun get_axiom thy = ((Thm.varifyT o Thm.get_axiom_i thy) c', thy); haftmann@27690: in haftmann@27690: thy' haftmann@27690: |> Sign.declare_const pos (c, ty'', mx) |> snd haftmann@27690: |> Thm.add_def false false (c, def_eq) haftmann@27690: |>> Thm.symmetric haftmann@27690: ||>> get_axiom haftmann@27690: |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def] haftmann@27690: #> register_operation class (c', (dict', SOME (Thm.symmetric def'))) haftmann@27690: #> PureThy.store_thm (c ^ "_raw", def') haftmann@27690: #> snd) haftmann@27690: |> Sign.restore_naming thy haftmann@27690: |> Sign.add_const_constraint (c', SOME ty') haftmann@27690: end; haftmann@27690: haftmann@27690: fun abbrev class prmode pos ((c, mx), rhs) thy = haftmann@27690: let haftmann@27690: val prfx = class_prefix class; haftmann@27690: val thy' = thy |> Sign.add_path prfx; haftmann@27690: haftmann@27690: val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) haftmann@27690: (these_operations thy [class]); haftmann@27690: val c' = Sign.full_name thy' c; haftmann@27690: val rhs' = Pattern.rewrite_term thy unchecks [] rhs; haftmann@27690: val rhs'' = map_types Logic.varifyT rhs'; haftmann@27690: val ty' = Term.fastype_of rhs'; haftmann@27690: in haftmann@27690: thy' haftmann@27690: |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd haftmann@27690: |> Sign.add_const_constraint (c', SOME ty') haftmann@27690: |> Sign.notation true prmode [(Const (c', ty'), mx)] haftmann@27690: |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE)) haftmann@27690: |> Sign.restore_naming thy haftmann@27690: end; haftmann@27690: haftmann@27690: fun note class kind facts thy = haftmann@27690: let haftmann@27690: val phi = morphism thy class; haftmann@27690: val facts' = facts haftmann@27690: |> PureThy.map_facts (Morphism.thm phi) haftmann@27690: |> Attrib.map_facts (Attrib.attribute_i thy); haftmann@27690: in haftmann@27690: thy haftmann@27690: |> Sign.add_path (class_prefix class) haftmann@27690: |> PureThy.note_thmss kind facts' haftmann@27690: ||> Sign.restore_naming thy haftmann@27690: end; haftmann@27690: haftmann@27690: fun declaration class decl thy = haftmann@27690: Context.theory_map (decl (morphism thy class)) thy; haftmann@27690: haftmann@27690: haftmann@24589: (* class definition *) haftmann@24218: haftmann@24218: local haftmann@24218: haftmann@26247: fun gen_class_spec prep_class process_expr thy raw_supclasses raw_elems = haftmann@24218: let haftmann@24748: val supclasses = map (prep_class thy) raw_supclasses; haftmann@24748: val supsort = Sign.minimize_sort thy supclasses; haftmann@25618: val sups = filter (is_class thy) supsort; haftmann@26995: val supparam_names = map fst (these_params thy sups); haftmann@26995: val _ = if has_duplicates (op =) supparam_names haftmann@26995: then error ("Duplicate parameter(s) in superclasses: " haftmann@26995: ^ (commas o map quote o duplicates (op =)) supparam_names) haftmann@26995: else (); haftmann@25618: val base_sort = if null sups then supsort else haftmann@26167: foldr1 (Sorts.inter_sort (Sign.classes_of thy)) haftmann@26167: (map (#base_sort o the_class_data thy) sups); haftmann@25038: val suplocales = map Locale.Locale sups; haftmann@24748: val supexpr = Locale.Merge suplocales; haftmann@24748: val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; haftmann@26247: val mergeexpr = Locale.Merge (suplocales); haftmann@24748: val constrain = Element.Constrains ((map o apsnd o map_atyps) haftmann@26167: (K (TFree (Name.aT, base_sort))) supparams); haftmann@25683: fun fork_syn (Element.Fixes xs) = wenzelm@28083: fold_map (fn (c, ty, syn) => cons (Name.name_of c, syn) #> pair (c, ty, NoSyn)) xs haftmann@25683: #>> Element.Fixes haftmann@25683: | fork_syn x = pair x; haftmann@25683: fun fork_syntax elems = haftmann@25683: let haftmann@25683: val (elems', global_syntax) = fold_map fork_syn elems []; haftmann@26247: in (constrain :: elems', global_syntax) end; haftmann@25683: val (elems, global_syntax) = haftmann@25683: ProofContext.init thy haftmann@25683: |> Locale.cert_expr supexpr [constrain] haftmann@25683: |> snd haftmann@25683: |> init_ctxt sups base_sort haftmann@25683: |> process_expr Locale.empty raw_elems haftmann@25683: |> fst haftmann@25683: |> fork_syntax haftmann@25683: in (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) end; haftmann@24748: haftmann@26247: val read_class_spec = gen_class_spec Sign.intern_class Locale.read_expr; haftmann@26247: val check_class_spec = gen_class_spec (K I) Locale.cert_expr; haftmann@24748: haftmann@26518: fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy = wenzelm@24968: let haftmann@25683: val supconsts = map fst supparams haftmann@26518: |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups)) haftmann@25683: |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]); haftmann@25683: val all_params = map fst (Locale.parameters_of thy class); haftmann@25683: fun add_const (v, raw_ty) thy = haftmann@25683: let haftmann@25683: val c = Sign.full_name thy v; haftmann@25683: val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty; haftmann@25683: val ty0 = Type.strip_sorts ty; haftmann@25683: val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0; haftmann@25683: val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v; haftmann@25683: in haftmann@25683: thy haftmann@25683: |> Sign.declare_const [] (v, ty0, syn) haftmann@25683: |> snd haftmann@25683: |> pair ((v, ty), (c, ty')) haftmann@25683: end; haftmann@25683: fun add_consts raw_params thy = haftmann@25683: thy haftmann@25683: |> Sign.add_path (Logic.const_of_class bname) haftmann@25683: |> fold_map add_const raw_params haftmann@25683: ||> Sign.restore_naming thy haftmann@25683: |-> (fn params => pair (supconsts @ (map o apfst) fst params, params)); haftmann@25683: fun globalize param_map = map_aterms haftmann@25683: (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) haftmann@25683: | t => t); haftmann@25683: val raw_pred = Locale.intros thy class haftmann@25683: |> fst haftmann@25683: |> map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of); haftmann@25683: fun get_axiom thy = case (#axioms o AxClass.get_info thy) class haftmann@25683: of [] => NONE haftmann@25683: | [thm] => SOME thm; wenzelm@24968: in wenzelm@24968: thy haftmann@25683: |> add_consts ((snd o chop (length supparams)) all_params) haftmann@25683: |-> (fn (param_map, params) => AxClass.define_class (bname, supsort) haftmann@26518: (map (fst o snd) params) wenzelm@28083: [((Name.binding (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)] haftmann@25683: #> snd haftmann@25683: #> `get_axiom haftmann@25683: #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params haftmann@25683: #> pair (param_map, params, assm_axiom))) wenzelm@24968: end; wenzelm@24968: haftmann@26518: fun gen_class prep_spec bname raw_supclasses raw_elems thy = haftmann@24748: let haftmann@25038: val class = Sign.full_name thy bname; haftmann@25683: val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) = haftmann@26247: prep_spec thy raw_supclasses raw_elems; haftmann@24218: in haftmann@24218: thy haftmann@27684: |> Locale.add_locale_i "" bname mergeexpr elems haftmann@25038: |> snd haftmann@25311: |> ProofContext.theory_of haftmann@26518: |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax haftmann@25683: |-> (fn (param_map, params, assm_axiom) => haftmann@26247: calculate sups base_sort assm_axiom param_map class haftmann@25711: #-> (fn (morphism, axiom, assm_intro, of_class) => haftmann@25683: add_class_data ((class, sups), (params, base_sort, haftmann@25711: map snd param_map, morphism, axiom, assm_intro, of_class)) haftmann@27708: (*#> `(fn thy => Locale.facts_of thy class) haftmann@27708: #-> (fn facts => fold_map (note class Thm.assumptionK) facts haftmann@27690: #> snd*) haftmann@27708: #> class_interpretation class (the_list axiom) [])) haftmann@25268: |> init class haftmann@25038: |> pair class haftmann@24218: end; haftmann@24218: haftmann@24218: in haftmann@24218: haftmann@26518: val class_cmd = gen_class read_class_spec; haftmann@26518: val class = gen_class check_class_spec; haftmann@24218: haftmann@24218: end; (*local*) haftmann@24218: haftmann@24218: haftmann@25462: haftmann@25462: (** instantiation target **) haftmann@25462: haftmann@25462: (* bookkeeping *) haftmann@25462: haftmann@25462: datatype instantiation = Instantiation of { haftmann@25864: arities: string list * (string * sort) list * sort, haftmann@25462: params: ((string * string) * (string * typ)) list haftmann@25603: (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*) haftmann@25462: } haftmann@25462: haftmann@25462: structure Instantiation = ProofDataFun haftmann@25462: ( haftmann@25462: type T = instantiation haftmann@25536: fun init _ = Instantiation { arities = ([], [], []), params = [] }; haftmann@25462: ); haftmann@25462: haftmann@25485: fun mk_instantiation (arities, params) = haftmann@25485: Instantiation { arities = arities, params = params }; haftmann@25514: fun get_instantiation lthy = case Instantiation.get (LocalTheory.target_of lthy) haftmann@25485: of Instantiation data => data; haftmann@25514: fun map_instantiation f = (LocalTheory.target o Instantiation.map) haftmann@25514: (fn Instantiation { arities, params } => mk_instantiation (f (arities, params))); haftmann@25462: haftmann@25514: fun the_instantiation lthy = case get_instantiation lthy haftmann@25536: of { arities = ([], [], []), ... } => error "No instantiation target" haftmann@25485: | data => data; haftmann@25462: haftmann@25485: val instantiation_params = #params o get_instantiation; haftmann@25462: haftmann@25514: fun instantiation_param lthy v = instantiation_params lthy haftmann@25462: |> find_first (fn (_, (v', _)) => v = v') haftmann@25462: |> Option.map (fst o fst); haftmann@25462: haftmann@25462: haftmann@25462: (* syntax *) haftmann@25462: haftmann@26238: fun synchronize_inst_syntax ctxt = haftmann@25462: let haftmann@26259: val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt; haftmann@26238: val thy = ProofContext.theory_of ctxt; haftmann@26238: fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty) haftmann@26238: of SOME tyco => (case AList.lookup (op =) params (c, tyco) haftmann@26238: of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty) haftmann@26238: | NONE => NONE) haftmann@26238: | NONE => NONE; haftmann@26238: val unchecks = haftmann@26238: map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params; haftmann@26238: in haftmann@26238: ctxt haftmann@26259: |> Overloading.map_improvable_syntax haftmann@26730: (fn (((primary_constraints, _), (((improve, _), _), _)), _) => haftmann@26730: (((primary_constraints, []), (((improve, subst), false), unchecks)), false)) haftmann@26238: end; haftmann@25462: haftmann@25462: haftmann@25462: (* target *) haftmann@25462: haftmann@25485: val sanatize_name = (*FIXME*) haftmann@25485: let haftmann@25574: fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s haftmann@25574: orelse s = "'" orelse s = "_"; haftmann@25485: val is_junk = not o is_valid andf Symbol.is_regular; haftmann@25485: val junk = Scan.many is_junk; haftmann@25485: val scan_valids = Symbol.scanner "Malformed input" haftmann@25485: ((junk |-- haftmann@25485: (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) haftmann@25485: --| junk)) wenzelm@25999: ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); haftmann@25485: in haftmann@25485: explode #> scan_valids #> implode haftmann@25485: end; haftmann@25485: haftmann@26259: fun type_name "*" = "prod" haftmann@26259: | type_name "+" = "sum" haftmann@26259: | type_name s = sanatize_name (NameSpace.base s); (*FIXME*) haftmann@26259: haftmann@26518: fun resort_terms pp algebra consts constraints ts = haftmann@26518: let haftmann@26518: fun matchings (Const (c_ty as (c, _))) = (case constraints c haftmann@26518: of NONE => I haftmann@26518: | SOME sorts => fold2 (curry (Sorts.meet_sort algebra)) haftmann@26518: (Consts.typargs consts c_ty) sorts) haftmann@26518: | matchings _ = I haftmann@26518: val tvartab = (fold o fold_aterms) matchings ts Vartab.empty wenzelm@26642: handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e); haftmann@27089: val inst = map_type_tvar haftmann@27089: (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); haftmann@26518: in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; haftmann@26518: haftmann@25864: fun init_instantiation (tycos, vs, sort) thy = haftmann@25462: let haftmann@25536: val _ = if null tycos then error "At least one arity must be given" else (); haftmann@26518: val params = these_params thy sort; haftmann@26518: fun get_param tyco (param, (_, (c, ty))) = if can (AxClass.param_of_inst thy) (c, tyco) haftmann@25603: then NONE else SOME ((c, tyco), haftmann@25864: (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); haftmann@26518: val inst_params = map_product get_param tycos params |> map_filter I; haftmann@26518: val primary_constraints = map (apsnd haftmann@26518: (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params; wenzelm@26939: val pp = Syntax.pp_global thy; haftmann@26518: val algebra = Sign.classes_of thy haftmann@26518: |> fold (fn tyco => Sorts.add_arities pp haftmann@26518: (tyco, map (fn class => (class, map snd vs)) sort)) tycos; haftmann@26518: val consts = Sign.consts_of thy; haftmann@26518: val improve_constraints = AList.lookup (op =) haftmann@26518: (map (fn (_, (class, (c, _))) => (c, [[class]])) params); haftmann@26518: fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts haftmann@26518: of NONE => NONE haftmann@26518: | SOME ts' => SOME (ts', ctxt); haftmann@26518: fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty) haftmann@26329: of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco) haftmann@26518: of SOME (_, ty') => if Type.raw_instance (ty', ty) then SOME (ty, ty') else NONE haftmann@26259: | NONE => NONE) haftmann@26259: | NONE => NONE; haftmann@25485: in haftmann@25485: thy haftmann@25485: |> ProofContext.init haftmann@26329: |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params)) wenzelm@27281: |> fold (Variable.declare_typ o TFree) vs haftmann@26329: |> fold (Variable.declare_names o Free o snd) inst_params haftmann@26259: |> (Overloading.map_improvable_syntax o apfst) haftmann@26329: (fn ((_, _), ((_, subst), unchecks)) => haftmann@26730: ((primary_constraints, []), (((improve, K NONE), false), []))) haftmann@26259: |> Overloading.add_improvable_syntax haftmann@26518: |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check) haftmann@26238: |> synchronize_inst_syntax haftmann@25485: end; haftmann@25485: haftmann@26238: fun confirm_declaration c = (map_instantiation o apsnd) haftmann@26238: (filter_out (fn (_, (c', _)) => c' = c)) haftmann@26238: #> LocalTheory.target synchronize_inst_syntax haftmann@26238: haftmann@25485: fun gen_instantiation_instance do_proof after_qed lthy = haftmann@25485: let haftmann@25864: val (tycos, vs, sort) = (#arities o the_instantiation) lthy; haftmann@25864: val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; haftmann@25462: fun after_qed' results = haftmann@25462: LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results) haftmann@25462: #> after_qed; haftmann@25462: in haftmann@25462: lthy haftmann@25462: |> do_proof after_qed' arities_proof haftmann@25462: end; haftmann@25462: haftmann@25485: val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts => haftmann@25462: Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts)); haftmann@25462: haftmann@25485: fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed => haftmann@25502: fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t haftmann@25502: (fn {context, ...} => tac context)) ts) lthy) I; haftmann@25462: haftmann@25462: fun conclude_instantiation lthy = haftmann@25462: let haftmann@25485: val { arities, params } = the_instantiation lthy; haftmann@25864: val (tycos, vs, sort) = arities; haftmann@25462: val thy = ProofContext.theory_of lthy; haftmann@25597: val _ = map (fn tyco => if Sign.of_sort thy haftmann@25864: (Type (tyco, map TFree vs), sort) haftmann@25462: then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) haftmann@25597: tycos; haftmann@25597: in lthy end; haftmann@25462: haftmann@25603: fun pretty_instantiation lthy = haftmann@25603: let haftmann@25603: val { arities, params } = the_instantiation lthy; haftmann@25864: val (tycos, vs, sort) = arities; haftmann@25603: val thy = ProofContext.theory_of lthy; haftmann@25864: fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); haftmann@25603: fun pr_param ((c, _), (v, ty)) = haftmann@25864: (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", wenzelm@26939: (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty]; haftmann@25603: in haftmann@25603: (Pretty.block o Pretty.fbreaks) haftmann@25603: (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params) haftmann@25603: end; haftmann@25603: haftmann@24218: end; haftmann@25683: