408 val _ = if null arities then error "at least one arity must be given" else (); |
408 val _ = if null arities then error "at least one arity must be given" else (); |
409 val _ = case (duplicates (op =) o map #1) arities |
409 val _ = case (duplicates (op =) o map #1) arities |
410 of [] => () |
410 of [] => () |
411 | dupl_tycos => error ("type constructors occur more than once in arities: " |
411 | dupl_tycos => error ("type constructors occur more than once in arities: " |
412 ^ (commas o map quote) dupl_tycos); |
412 ^ (commas o map quote) dupl_tycos); |
413 val name = case raw_name |
413 val (bind_always, name) = case raw_name |
414 of "" => Thm.def_name ((space_implode "_" o map NameSpace.base) |
414 of "" => (false, Thm.def_name ((space_implode "_" o map NameSpace.base) |
415 (maps (fn (tyco, _, sort) => sort @ [tyco]) |
415 (maps (fn (tyco, _, sort) => sort @ [tyco]) |
416 (sort (fn ((tyco1, _, _), (tyco2, _, _)) => string_ord (tyco1, tyco2)) arities))) |
416 (sort (fn ((tyco1, _, _), (tyco2, _, _)) => string_ord (tyco1, tyco2)) arities)))) |
417 | _ => raw_name; |
417 | _ => (true, raw_name); |
418 val atts = map (prep_att theory) raw_atts; |
418 val atts = map (prep_att theory) raw_atts; |
419 fun already_defined (c, ty_inst) = |
419 fun already_defined (c, ty_inst) = |
420 is_some (find_first (fn (_, { lhs = [ty_inst'], ...}) => |
420 is_some (find_first (fn (_, { lhs = [ty_inst'], ...}) => |
421 Sign.typ_instance theory (ty_inst', ty_inst) orelse Sign.typ_instance theory (ty_inst, ty_inst')) |
421 Sign.typ_instance theory (ty_inst', ty_inst) orelse Sign.typ_instance theory (ty_inst, ty_inst')) |
422 (Defs.specifications_of (Theory.defs_of theory) c)); |
422 (Defs.specifications_of (Theory.defs_of theory) c)); |
471 |> PureThy.add_defs_i true (map snd defs) |
471 |> PureThy.add_defs_i true (map snd defs) |
472 |-> (fn thms => pair (map fst defs ~~ thms)); |
472 |-> (fn thms => pair (map fst defs ~~ thms)); |
473 fun note_all thy = |
473 fun note_all thy = |
474 (*FIXME: should avoid binding duplicated names*) |
474 (*FIXME: should avoid binding duplicated names*) |
475 let |
475 let |
|
476 val bind = bind_always orelse not (can (PureThy.get_thms thy) (Name name)); |
476 val thms = maps (fn (tyco, _, sort) => maps (fn class => |
477 val thms = maps (fn (tyco, _, sort) => maps (fn class => |
477 Symtab.lookup_list |
478 Symtab.lookup_list |
478 ((snd o the_class_data thy) class) tyco) (the_ancestry thy sort)) arities; |
479 ((snd o the_class_data thy) class) tyco) (the_ancestry thy sort)) arities; |
479 in |
480 in if bind then |
480 thy |
481 thy |
481 |> PureThy.note_thmss_i PureThy.internalK [((name, atts), [(thms, [])])] |
482 |> PureThy.note_thmss_i PureThy.internalK [((name, atts), [(thms, [])])] |
482 |> snd |
483 |> snd |
|
484 else |
|
485 thy |
483 end; |
486 end; |
484 fun after_qed cs thy = |
487 fun after_qed cs thy = |
485 thy |
488 thy |
486 |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs); |
489 |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs); |
487 in |
490 in |
565 |
568 |
566 (* extracting dictionary obligations from types *) |
569 (* extracting dictionary obligations from types *) |
567 |
570 |
568 type sortcontext = (string * sort) list; |
571 type sortcontext = (string * sort) list; |
569 |
572 |
570 fun sortcontext_of_typ thy ty = fold_atyps |
573 fun sortcontext_of_typ thy ty = (rev ooo fold_atyps) |
571 (fn TFree (v, S) => |
574 (fn TFree (v, S) => |
572 (case operational_sort_of thy S of |
575 (case operational_sort_of thy S of |
573 [] => I |
576 [] => I |
574 | S' => insert (op =) (v, S'))) (Type.no_tvars ty) []; |
577 | S' => insert (op =) (v, S'))) (Type.no_tvars ty) []; |
575 |
578 |