src/Pure/Tools/class_package.ML
changeset 22302 bf5bdb7f7607
parent 22222 bb07dd6cb1b9
child 22321 e5cddafe2629
equal deleted inserted replaced
22301:1435d027e453 22302:bf5bdb7f7607
     5 Type classes derived from primitive axclasses and locales.
     5 Type classes derived from primitive axclasses and locales.
     6 *)
     6 *)
     7 
     7 
     8 signature CLASS_PACKAGE =
     8 signature CLASS_PACKAGE =
     9 sig
     9 sig
       
    10   val fork_mixfix: bool -> bool -> mixfix -> mixfix * mixfix
       
    11 
    10   val class: bstring -> class list -> Element.context_i Locale.element list -> theory ->
    12   val class: bstring -> class list -> Element.context_i Locale.element list -> theory ->
    11     string * Proof.context
    13     string * Proof.context
       
    14   val class_e: bstring -> string list -> Element.context Locale.element list -> theory ->
       
    15     string * Proof.context
    12   val instance_arity: ((bstring * sort list) * sort) list
    16   val instance_arity: ((bstring * sort list) * sort) list
    13     -> ((bstring * attribute list) * term) list
    17     -> ((bstring * Attrib.src list) * term) list
       
    18     -> theory -> Proof.state
       
    19   val instance_arity_e: ((bstring * string list) * string) list
       
    20     -> ((bstring * Attrib.src list) * string) list
    14     -> theory -> Proof.state
    21     -> theory -> Proof.state
    15   val prove_instance_arity: tactic -> ((string * sort list) * sort) list
    22   val prove_instance_arity: tactic -> ((string * sort list) * sort) list
    16     -> ((bstring * attribute list) * term) list
    23     -> ((bstring * Attrib.src list) * term) list
    17     -> theory -> theory
    24     -> theory -> theory
    18   val instance_sort: class * sort -> theory -> Proof.state
    25   val instance_sort: class * sort -> theory -> Proof.state
       
    26   val instance_sort_e: string * string -> theory -> Proof.state
    19   val prove_instance_sort: tactic -> class * sort -> theory -> theory
    27   val prove_instance_sort: tactic -> class * sort -> theory -> theory
    20 
    28 
    21   val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool
    29   val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool
    22   val assume_arities_thy: theory -> ((string * sort list) * sort) list -> (theory -> 'a) -> 'a
    30   val assume_arities_thy: theory -> ((string * sort list) * sort) list -> (theory -> 'a) -> 'a
    23     (*'a must not keep any reference to theory*)
    31     (*'a must not keep any reference to theory*)
    24 
    32 
    25   (* experimental class target *)
    33   (* experimental class target *)
    26   val add_def: class * thm -> theory -> theory
    34   val class_of_locale: theory -> string -> class option
    27   val export_typ: theory -> class -> typ -> typ
    35   val add_def_in_class: local_theory -> string
    28   val export_def: theory -> class -> term -> term
    36     -> (string * Syntax.mixfix) * ((string * Attrib.src list) * (term * thm)) -> theory -> theory
    29   val export_thm: theory -> class -> thm -> thm
       
    30 
    37 
    31   val print_classes: theory -> unit
    38   val print_classes: theory -> unit
    32   val intro_classes_tac: thm list -> tactic
    39   val intro_classes_tac: thm list -> tactic
    33   val default_intro_classes_tac: thm list -> tactic
    40   val default_intro_classes_tac: thm list -> tactic
    34 end;
    41 end;
    35 
    42 
    36 structure ClassPackage : CLASS_PACKAGE =
    43 structure ClassPackage : CLASS_PACKAGE =
    37 struct
    44 struct
    38 
    45 
    39 (** axclasses with implicit parameter handling **)
    46 (** auxiliary **)
    40 
    47 
    41 (* axclass instances *)
    48 fun fork_mixfix is_class is_loc mx =
       
    49   let
       
    50     val mx' = Syntax.unlocalize_mixfix mx;
       
    51     val mx1 = if is_class orelse (is_loc andalso mx = mx') then NoSyn else mx';
       
    52     val mx2 = if is_loc then mx else NoSyn;
       
    53   in (mx1, mx2) end;
       
    54 
       
    55 
       
    56 (** AxClasses with implicit parameter handling **)
       
    57 
       
    58 (* AxClass instances *)
    42 
    59 
    43 local
    60 local
    44 
    61 
    45 fun gen_instance mk_prop add_thm after_qed insts thy =
    62 fun gen_instance mk_prop add_thm after_qed insts thy =
    46   let
    63   let
    79       Sign.add_const_constraint_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
    96       Sign.add_const_constraint_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
    80   in
    97   in
    81     thy
    98     thy
    82     |> fold_map add_const consts
    99     |> fold_map add_const consts
    83     |-> (fn cs => mk_axioms cs
   100     |-> (fn cs => mk_axioms cs
    84     #-> (fn axioms => AxClass.define_class_i (name, superclasses) (map fst cs) axioms
   101     #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs) axioms_prop
    85     #-> (fn class => `(fn thy => AxClass.get_definition thy class)
   102     #-> (fn class => `(fn thy => AxClass.get_definition thy class)
    86     #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
   103     #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
    87     #> pair (class, ((intro, axioms), cs))))))
   104     #> pair (class, ((intro, (map snd axioms_prop, axioms)), cs))))))
    88   end;
   105   end;
    89 
   106 
    90 
   107 
    91 (* contexts with arity assumptions *)
   108 (* contexts with arity assumptions *)
    92 
   109 
   118     val name = case raw_name
   135     val name = case raw_name
   119      of "" => NONE
   136      of "" => NONE
   120       | _ => SOME raw_name;
   137       | _ => SOME raw_name;
   121   in (c, (insts, ((name, t), atts))) end;
   138   in (c, (insts, ((name, t), atts))) end;
   122 
   139 
   123 fun read_def_e thy = gen_read_def thy Attrib.attribute read_axm;
   140 fun read_def_e thy = gen_read_def thy Attrib.intern_src read_axm;
   124 fun read_def thy = gen_read_def thy (K I) (K I);
   141 fun read_def thy = gen_read_def thy (K I) (K I);
   125 
   142 
   126 fun gen_instance_arity prep_arity prep_att read_def do_proof raw_arities raw_defs theory =
   143 fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =
   127   let
   144   let
   128     fun prep_arity' ((tyco, asorts), sort) = prep_arity theory (tyco, asorts, sort);
   145     fun prep_arity' ((tyco, asorts), sort) = prep_arity theory (tyco, asorts, sort);
   129     val arities = map prep_arity' raw_arities;
   146     val arities = map prep_arity' raw_arities;
   130     val arities_pair = map (fn (tyco, asorts, sort) => ((tyco, asorts), sort)) arities;
   147     val arities_pair = map (fn (tyco, asorts, sort) => ((tyco, asorts), sort)) arities;
   131     val _ = if null arities then error "at least one arity must be given" else ();
   148     val _ = if null arities then error "at least one arity must be given" else ();
   177         |> Sign.add_const_constraint_i (c, NONE)
   194         |> Sign.add_const_constraint_i (c, NONE)
   178         |> pair (c, Logic.unvarifyT ty)
   195         |> pair (c, Logic.unvarifyT ty)
   179       end;
   196       end;
   180     fun add_defs defs thy =
   197     fun add_defs defs thy =
   181       thy
   198       thy
   182       |> PureThy.add_defs_i true (map snd defs)
   199       |> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs)
   183       |-> (fn thms => pair (map fst defs ~~ thms));
   200       |-> (fn thms => pair (map fst defs ~~ thms));
   184     fun after_qed cs thy =
   201     fun after_qed cs thy =
   185       thy
   202       thy
   186       |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs);
   203       |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs);
   187   in
   204   in
   189     |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
   206     |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
   190     ||>> add_defs defs
   207     ||>> add_defs defs
   191     |-> (fn (cs, _) => do_proof (after_qed cs) arities)
   208     |-> (fn (cs, _) => do_proof (after_qed cs) arities)
   192   end;
   209   end;
   193 
   210 
   194 fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute
   211 fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity read_def_e do_proof;
   195   read_def_e do_proof;
   212 fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof;
   196 fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity (K I)
       
   197   read_def do_proof;
       
   198 fun tactic_proof tac after_qed arities =
   213 fun tactic_proof tac after_qed arities =
   199   fold (fn arity => AxClass.prove_arity arity tac) arities
   214   fold (fn arity => AxClass.prove_arity arity tac) arities
   200   #> after_qed;
   215   #> after_qed;
   201 
   216 
   202 in
   217 in
   215 
   230 
   216 datatype class_data = ClassData of {
   231 datatype class_data = ClassData of {
   217   locale: string,
   232   locale: string,
   218   consts: (string * string) list
   233   consts: (string * string) list
   219     (*locale parameter ~> toplevel theory constant*),
   234     (*locale parameter ~> toplevel theory constant*),
       
   235   witness: Element.witness list,
   220   propnames: string list,
   236   propnames: string list,
   221     (*for ad-hoc instance in*)
   237     (*for ad-hoc instance_in*)
   222   defs: thm list
   238   primdefs: thm list
   223     (*for experimental class target*)
   239     (*for experimental class target*)
   224 };
   240 };
   225 
   241 
   226 fun rep_classdata (ClassData c) = c;
   242 fun rep_classdata (ClassData c) = c;
       
   243 
       
   244 fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
   227 
   245 
   228 structure ClassData = TheoryDataFun (
   246 structure ClassData = TheoryDataFun (
   229   struct
   247   struct
   230     val name = "Pure/classes";
   248     val name = "Pure/classes";
   231     type T = class_data Graph.T;
   249     type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
   232     val empty = Graph.empty;
   250     val empty = (Graph.empty, Symtab.empty);
   233     val copy = I;
   251     val copy = I;
   234     val extend = I;
   252     val extend = I;
   235     fun merge _ = Graph.merge (K true);
   253     fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
   236     fun print _ _ = ();
   254     fun print _ _ = ();
   237   end
   255   end
   238 );
   256 );
   239 
   257 
   240 val _ = Context.add_setup ClassData.init;
   258 val _ = Context.add_setup ClassData.init;
   241 
   259 
   242 
   260 
   243 (* queries *)
   261 (* queries *)
   244 
   262 
   245 val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o ClassData.get;
   263 val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o ClassData.get;
   246 val is_class = can o Graph.get_node o ClassData.get;
   264 fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy);
       
   265 
   247 fun the_class_data thy class =
   266 fun the_class_data thy class =
   248   case lookup_class_data thy class
   267   case lookup_class_data thy class
   249     of NONE => error ("undeclared class " ^ quote class)
   268     of NONE => error ("undeclared class " ^ quote class)
   250      | SOME data => data;
   269      | SOME data => data;
   251 
   270 
   252 fun the_ancestry thy = Graph.all_succs (ClassData.get thy);
   271 val ancestry = Graph.all_succs o fst o ClassData.get;
   253 
   272 
   254 fun the_parm_map thy class =
   273 fun param_map thy = 
   255   let
   274   let
   256     val const_typs = (#params o AxClass.get_definition thy) class;
   275     fun params thy class =
   257     val const_names = (#consts o the_class_data thy) class;
   276       let
   258   in
   277         val const_typs = (#params o AxClass.get_definition thy) class;
   259     map (apsnd (fn c => (c, (the o AList.lookup (op =) const_typs) c))) const_names
   278         val const_names = (#consts o the_class_data thy) class;
   260   end;
   279       in
   261 
   280         (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names
       
   281       end;
       
   282   in maps (params thy) o ancestry thy end;
       
   283 
       
   284 val the_witness = #witness oo the_class_data;
   262 val the_propnames = #propnames oo the_class_data;
   285 val the_propnames = #propnames oo the_class_data;
   263 
   286 
   264 fun print_classes thy =
   287 fun print_classes thy =
   265   let
   288   let
   266     val algebra = Sign.classes_of thy;
   289     val algebra = Sign.classes_of thy;
   294   end;
   317   end;
   295 
   318 
   296 
   319 
   297 (* updaters *)
   320 (* updaters *)
   298 
   321 
   299 fun add_class_data ((class, superclasses), (locale, consts, propnames)) =
   322 fun add_class_data ((class, superclasses), (locale, consts, witness, propnames)) =
   300   ClassData.map (
   323   ClassData.map (fn (gr, tab) => (
   301     Graph.new_node (class, ClassData {
   324     gr
       
   325     |> Graph.new_node (class, ClassData {
   302       locale = locale,
   326       locale = locale,
   303       consts = consts,
   327       consts = consts,
       
   328       witness = witness,
   304       propnames = propnames,
   329       propnames = propnames,
   305       defs = []})
   330       primdefs = []})
   306     #> fold (curry Graph.add_edge class) superclasses
   331     |> fold (curry Graph.add_edge class) superclasses,
   307   );
   332     tab
   308 
   333     |> Symtab.update (locale, class)
   309 fun add_def (class, thm) =
   334   ));
   310   (ClassData.map o Graph.map_node class)
   335 
   311     (fn ClassData { locale, consts, propnames, defs } => ClassData { locale = locale,
   336 fun add_primdef (class, thm) thy =
   312       consts = consts, propnames = propnames, defs = thm :: defs });
   337   (ClassData.map o apfst o Graph.map_node class)
       
   338     (fn ClassData { locale, consts, witness, propnames, primdefs } => ClassData { locale = locale,
       
   339       consts = consts, witness = witness, propnames = propnames, primdefs = thm :: primdefs });
       
   340 
       
   341 
       
   342 (* exporting terms and theorems to global toplevel *)
       
   343 (*FIXME should also be used when introducing classes*)
       
   344 
       
   345 fun globalize thy classes =
       
   346   let
       
   347     val consts = param_map thy classes;
       
   348     val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) classes;
       
   349     val subst_typ = Term.map_type_tfree (fn var as (v, sort) =>
       
   350       if v = AxClass.param_tyvarname then TFree (v, constrain_sort sort) else TFree var)
       
   351     fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v
       
   352          of SOME (c, _) => Const (c, ty)
       
   353           | NONE => t)
       
   354       | subst_aterm t = t;
       
   355   in (subst_typ, map_types subst_typ #> Term.map_aterms subst_aterm) end;
       
   356 
       
   357 val global_term = snd oo globalize
   313 
   358 
   314 
   359 
   315 (* tactics and methods *)
   360 (* tactics and methods *)
   316 
   361 
   317 fun intro_classes_tac facts st =
   362 fun intro_classes_tac facts st =
   372     val loc_name = (#locale o the_class_data theory) class;
   417     val loc_name = (#locale o the_class_data theory) class;
   373     val loc_expr =
   418     val loc_expr =
   374       (Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort;
   419       (Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort;
   375     val const_names = (map (NameSpace.base o snd)
   420     val const_names = (map (NameSpace.base o snd)
   376       o maps (#consts o the_class_data theory)
   421       o maps (#consts o the_class_data theory)
   377       o the_ancestry theory) [class];
   422       o ancestry theory) [class];
   378     fun get_thms thy =
   423     fun get_thms thy =
   379       the_ancestry thy sort
   424       ancestry thy sort
   380       |> AList.make (the_propnames thy)
   425       |> AList.make (the_propnames thy)
   381       |> map (apsnd (map (NameSpace.append (Logic.const_of_class loc_name))))
   426       |> map (apsnd (map (NameSpace.append (Logic.const_of_class loc_name))))
   382       |> map_filter (fn (superclass, thm_names) =>
   427       |> map_filter (fn (superclass, thm_names) =>
   383           case map_filter (try (PureThy.get_thm thy o Name)) thm_names
   428           case map_filter (try (PureThy.get_thm thy o Name)) thm_names
   384            of [] => NONE
   429            of [] => NONE
   416   certify_class thy o Sign.intern_class thy;
   461   certify_class thy o Sign.intern_class thy;
   417 
   462 
   418 fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
   463 fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
   419   let
   464   let
   420     val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) raw_elems [];
   465     val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) raw_elems [];
       
   466       (*FIXME add constrains here to elements as hint for locale*)
   421     val supclasses = map (prep_class thy) raw_supclasses;
   467     val supclasses = map (prep_class thy) raw_supclasses;
   422     val supsort =
   468     val supsort =
   423       supclasses
   469       supclasses
   424       |> Sign.certify_sort thy
   470       |> Sign.certify_sort thy
   425       |> (fn [] => Sign.defaultS thy | S => S);    (* FIXME Why syntax defaultS? *)
   471       |> (fn [] => Sign.defaultS thy | S => S);    (*FIXME Why syntax defaultS?*)
   426     val supexpr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses);
   472     val supexpr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses);
   427     val supconsts = AList.make
   473     val supconsts = AList.make
   428       (the o AList.lookup (op =) ((maps (the_parm_map thy) o the_ancestry thy) supclasses))
   474       (the o AList.lookup (op =) (param_map thy supclasses))
   429       ((map (fst o fst) o Locale.parameters_of_expr thy) supexpr);
   475       ((map (fst o fst) o Locale.parameters_of_expr thy) supexpr);
   430     fun check_locale thy name_locale =
   476     fun check_locale thy name_locale =
   431       let
   477       let
   432         val tfrees =
   478         val tfrees =
   433           []
   479           []
   442             (commas o map fst) tfrees)
   488             (commas o map fst) tfrees)
   443       end;
   489       end;
   444     fun extract_params thy name_locale =
   490     fun extract_params thy name_locale =
   445       Locale.parameters_of thy name_locale
   491       Locale.parameters_of thy name_locale
   446       |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, [])))
   492       |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, [])))
   447       |> (map o apsnd) (TheoryTarget.fork_mixfix false true #> fst)
   493       |> (map o apsnd) (fork_mixfix false true #> fst)
   448       |> chop (length supconsts)
   494       |> chop (length supconsts)
   449       |> snd;
   495       |> snd;
   450     fun extract_assumes name_locale params thy cs =
   496     fun extract_assumes name_locale params thy cs =
   451       let
   497       let
   452         val consts = supconsts @ (map (fst o fst) params ~~ cs);
   498         val consts = supconsts @ (map (fst o fst) params ~~ cs);
   473     |-> (fn name_locale => ProofContext.theory_result (
   519     |-> (fn name_locale => ProofContext.theory_result (
   474       tap (fn thy => check_locale thy name_locale)
   520       tap (fn thy => check_locale thy name_locale)
   475       #> `(fn thy => extract_params thy name_locale)
   521       #> `(fn thy => extract_params thy name_locale)
   476       #-> (fn params =>
   522       #-> (fn params =>
   477         axclass_params (bname, supsort) params (extract_assumes name_locale params)
   523         axclass_params (bname, supsort) params (extract_assumes name_locale params)
   478       #-> (fn (name_axclass, ((_, ax_axioms), consts)) =>
   524       #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
   479         `(fn thy => extract_axiom_names thy name_locale)
   525         `(fn thy => extract_axiom_names thy name_locale)
   480       #-> (fn axiom_names =>
   526       #-> (fn axiom_names =>
   481         add_class_data ((name_axclass, supclasses),
   527         add_class_data ((name_axclass, supclasses),
   482           (name_locale, map (fst o fst) params ~~ map fst consts, axiom_names))
   528           (name_locale, map (fst o fst) params ~~ map fst consts,
       
   529             map2 Element.make_witness (map Logic.mk_conjunction_list ax_terms) ax_axioms, axiom_names))
   483       #> prove_interpretation (Logic.const_of_class bname, [])
   530       #> prove_interpretation (Logic.const_of_class bname, [])
   484           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts))
   531           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts))
   485             ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   532             ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   486       #> pair name_axclass
   533       #> pair name_axclass
   487       )))))
   534       )))))
   498 
   545 
   499 fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory =
   546 fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory =
   500   let
   547   let
   501     val class = prep_class theory raw_class;
   548     val class = prep_class theory raw_class;
   502     val sort = prep_sort theory raw_sort;
   549     val sort = prep_sort theory raw_sort;
   503   in if is_class theory class andalso forall (is_class theory) sort then
   550     val is_class = is_some o lookup_class_data theory;
       
   551   in if is_class class andalso forall is_class sort then
   504     theory
   552     theory
   505     |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort)
   553     |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort)
   506   else case sort
   554   else case sort
   507    of [class'] =>
   555    of [class'] =>
   508         theory
   556         theory
   518 end; (* local *)
   566 end; (* local *)
   519 
   567 
   520 
   568 
   521 (** experimental class target **)
   569 (** experimental class target **)
   522 
   570 
   523 fun export_typ thy loc =
   571 fun add_def_in_class lthy loc ((c, syn), ((name, atts), (rhs, eq))) thy =
   524   let
   572   let
   525     val class = loc (*FIXME*);
   573     val SOME class = class_of_locale thy loc;
   526     val (v, _) = AxClass.params_of_class thy class;
   574     val rhs' = global_term thy [class] rhs;
   527   in
   575     val (syn', _) = fork_mixfix true true syn;
   528     Term.map_type_tfree (fn var as (w, sort) =>
   576     val ty = Term.fastype_of rhs';
   529       if w = v then TFree (w, Sorts.inter_sort (Sign.classes_of thy)
   577     fun add_const (c, ty, syn) =
   530         (sort, [class])) else TFree var)
   578       Sign.add_consts_authentic [(c, ty, syn)]
   531   end;
   579       #> pair (Sign.full_name thy c, ty);
   532 
   580     fun add_def ((name, atts), prop) thy =
   533 fun export_def thy loc =
   581       thy
   534   let
   582       |> PureThy.add_defs_i false [((name, prop), map (Attrib.attribute thy) atts)]
   535     val class = loc (*FIXME*);
   583       |>> the_single;
   536     val consts = the_parm_map thy class;
   584     (*val _ = Output.info "------ DEF ------";
   537     val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   585     val _ = Output.info c;
   538       if w = AxClass.param_tyvarname then TFree (w, Sorts.inter_sort (Sign.classes_of thy)
   586     val _ = Output.info name;
   539         (sort, [class])) else TFree var)
   587     val _ = (Output.info o Sign.string_of_term thy) rhs';
   540     fun subst (t as Free (v, _)) = (case AList.lookup (op =) consts v
   588     val eq' = Morphism.thm (LocalTheory.target_morphism lthy) eq;
   541          of SOME c_ty => Const c_ty
   589     val _ = (Output.info o string_of_thm) eq;
   542           | NONE => t)
   590     val _ = (Output.info o string_of_thm) eq';
   543       | subst t = t;
   591     val witness = the_witness thy class;
   544   in
   592     val _ = Output.info "------ WIT ------";
   545     Term.map_aterms subst #> map_types subst_typ
   593     fun print_wit (t, thm) = "(" ^ Sign.string_of_term thy t ^ ", " ^ Display.string_of_thm thm ^ ")"
   546   end;
   594     val _ = (Output.info o cat_lines o map (print_wit o Element.dest_witness)) witness;
   547 
   595     val _ = (Output.info o string_of_thm) eq';
   548 fun export_thm thy loc =
   596     val eq'' = Element.satisfy_thm witness eq';
   549   let
   597     val _ = (Output.info o string_of_thm) eq'';*)
   550     val class = loc (*FIXME*);
   598   in
   551     val thms = (#defs o the_class_data thy) class;
   599     thy
   552   in
   600     (*|> add_const (c, ty, syn')
   553     MetaSimplifier.rewrite_rule thms
   601     |-> (fn c => add_def ((name, atts), Logic.mk_equals (Const c, rhs')))
   554   end;
   602     |-> (fn global_def_thm => tap (fn _ => (Output.info o string_of_thm) global_def_thm))*)
   555 
   603   end;
   556 
       
   557 
       
   558 (** toplevel interface **)
       
   559 
       
   560 local
       
   561 
       
   562 structure P = OuterParse
       
   563 and K = OuterKeyword
       
   564 
       
   565 in
       
   566 
       
   567 val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
       
   568 
       
   569 val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
       
   570 val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
       
   571 
       
   572 val parse_arity =
       
   573   (P.xname --| P.$$$ "::" -- P.!!! P.arity)
       
   574     >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
       
   575 
       
   576 val classP =
       
   577   OuterSyntax.command classK "define type class" K.thy_decl (
       
   578     P.name --| P.$$$ "="
       
   579     -- (
       
   580       class_subP --| P.$$$ "+" -- class_bodyP
       
   581       || class_subP >> rpair []
       
   582       || class_bodyP >> pair [])
       
   583     -- P.opt_begin
       
   584     >> (fn ((bname, (supclasses, elems)), begin) =>
       
   585         Toplevel.begin_local_theory begin
       
   586           (class_e bname supclasses elems #-> TheoryTarget.begin true)));
       
   587 
       
   588 val instanceP =
       
   589   OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
       
   590       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
       
   591            >> instance_sort_e
       
   592       || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
       
   593            >> (fn (arities, defs) => instance_arity_e arities defs)
       
   594     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
       
   595 
       
   596 val print_classesP =
       
   597   OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag
       
   598     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
       
   599       o Toplevel.keep (print_classes o Toplevel.theory_of)));
       
   600 
       
   601 val _ = OuterSyntax.add_parsers [classP, instanceP, print_classesP];
       
   602 
       
   603 end; (*local*)
       
   604 
   604 
   605 end;
   605 end;