40 (string * (string list * string list)) list list -> context -> |
40 (string * (string list * string list)) list list -> context -> |
41 string option * context * context * (term * (term list * term list)) list list |
41 string option * context * context * (term * (term list * term list)) list list |
42 val cert_context_statement: string option -> context attribute element_i list -> |
42 val cert_context_statement: string option -> context attribute element_i list -> |
43 (term * (term list * term list)) list list -> context -> |
43 (term * (term list * term list)) list list -> context -> |
44 string option * context * context * (term * (term list * term list)) list list |
44 string option * context * context * (term * (term list * term list)) list list |
|
45 |
45 val add_locale: bstring -> expr -> context attribute element list -> theory -> theory |
46 val add_locale: bstring -> expr -> context attribute element list -> theory -> theory |
46 val add_locale_i: bstring -> expr -> context attribute element_i list -> theory -> theory |
47 val add_locale_i: bstring -> expr -> context attribute element_i list -> theory -> theory |
47 val print_locales: theory -> unit |
48 val print_locales: theory -> unit |
48 val print_locale: theory -> expr -> unit |
49 val print_locale: theory -> expr -> unit |
49 val add_thmss: string -> ((string * thm list) * context attribute list) list -> theory -> theory |
|
50 val add_thmss_hybrid: string -> |
50 val add_thmss_hybrid: string -> |
51 ((bstring * theory attribute list) * (thm list * theory attribute list) list) list -> |
51 ((bstring * theory attribute list) * (thm list * theory attribute list) list) list -> |
52 (string * context attribute list list) option -> thm list list -> |
52 (string * context attribute list list) option -> thm list list -> |
53 theory -> theory * (string * thm list) list |
53 theory -> theory * (string * thm list) list |
54 val setup: (theory -> theory) list |
54 val setup: (theory -> theory) list |
|
55 val have_thmss: string -> string -> |
|
56 ((string * context attribute list) * (string * context attribute list) list) list -> |
|
57 theory -> theory * (string * thm list) list |
|
58 val have_thmss_i: string -> string -> |
|
59 ((string * context attribute list) * (thm list * context attribute list) list) list -> |
|
60 theory -> theory * (string * thm list) list |
55 end; |
61 end; |
56 |
62 |
57 structure Locale: LOCALE = |
63 structure Locale: LOCALE = |
58 struct |
64 struct |
59 |
65 |
697 |
703 |
698 |
704 |
699 |
705 |
700 (** store results **) |
706 (** store results **) |
701 |
707 |
|
708 local |
|
709 |
|
710 fun put_facts loc args thy = |
|
711 let |
|
712 val {import, params, elems, text} = the_locale thy loc; |
|
713 val note = Notes (map (fn ((a, more_atts), th_atts) => |
|
714 ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args); |
|
715 in thy |> put_locale loc (make_locale import (elems @ [(note, stamp ())]) params text) end; |
|
716 |
702 fun add_thmss loc args thy = |
717 fun add_thmss loc args thy = |
703 let |
718 let val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args in |
704 val {import, params, elems, text} = the_locale thy loc; |
719 thy |> ProofContext.init |> |
705 val note = Notes (map (fn ((a, ths), atts) => |
720 cert_context_statement (Some loc) [Elem (Notes args')] []; (*test attributes now!*) |
706 ((a, atts), [(map (curry Thm.name_thm a) ths, [])])) args); |
721 thy |> put_facts loc args' |
707 in |
|
708 thy |> ProofContext.init |
|
709 |> cert_context_statement (Some loc) [Elem note] []; (*test attributes!*) |
|
710 thy |> put_locale loc (make_locale import (elems @ [(note, stamp ())]) params text) |
|
711 end; |
722 end; |
712 |
723 |
713 fun hide_bound_names names thy = |
724 fun hide_bound_names names thy = |
714 thy |> PureThy.hide_thms false |
725 thy |> PureThy.hide_thms false |
715 (map (Sign.full_name (Theory.sign_of thy)) (filter_out (equal "") names)); |
726 (map (Sign.full_name (Theory.sign_of thy)) (filter_out (equal "") names)); |
716 |
727 |
|
728 fun have_thmss_qualified kind loc args thy = |
|
729 thy |
|
730 |> Theory.add_path (Sign.base_name loc) |
|
731 |> PureThy.have_thmss [Drule.kind kind] args |
|
732 |>> hide_bound_names (map (#1 o #1) args) |
|
733 |>> Theory.parent_path; |
|
734 |
|
735 fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy = |
|
736 let |
|
737 val thy_ctxt = ProofContext.init thy; |
|
738 val loc = prep_locale (Theory.sign_of thy) raw_loc; |
|
739 val loc_ctxt = #1 (#1 (cert_context (Locale loc) [] thy_ctxt)); |
|
740 val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args; |
|
741 val export = Drule.local_standard o ProofContext.export_single loc_ctxt thy_ctxt; |
|
742 val results = map (map export o #2) (#2 (ProofContext.have_thmss args loc_ctxt)); |
|
743 val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results; |
|
744 in |
|
745 thy |
|
746 |> put_facts loc args |
|
747 |> have_thmss_qualified kind loc args' |
|
748 end; |
|
749 |
|
750 in |
|
751 |
717 fun add_thmss_hybrid kind args None _ thy = PureThy.have_thmss [Drule.kind kind] args thy |
752 fun add_thmss_hybrid kind args None _ thy = PureThy.have_thmss [Drule.kind kind] args thy |
718 | add_thmss_hybrid kind args (Some (loc, loc_atts)) loc_ths thy = |
753 | add_thmss_hybrid kind args (Some (loc, loc_atts)) loc_ths thy = |
719 let val names = map (#1 o #1) args in |
754 if length args = length loc_atts then |
720 conditional (length names <> length loc_atts) (fn () => |
755 thy |
721 raise THEORY ("Bad number of locale attributes", [thy])); |
756 |> add_thmss loc ((map (#1 o #1) args ~~ loc_ths) ~~ loc_atts) |
722 thy |
757 |> have_thmss_qualified kind loc args |
723 |> add_thmss loc ((names ~~ loc_ths) ~~ loc_atts) |
758 else raise THEORY ("Bad number of locale attributes", [thy]); |
724 |> Theory.add_path (Sign.base_name loc) |
759 |
725 |> PureThy.have_thmss [Drule.kind kind] args |
760 val have_thmss = gen_have_thmss intern ProofContext.get_thms; |
726 |>> hide_bound_names names |
761 val have_thmss_i = gen_have_thmss (K I) (K I); |
727 |>> Theory.parent_path |
762 |
728 end; |
763 end; |
729 |
|
730 |
764 |
731 |
765 |
732 (** locale theory setup **) |
766 (** locale theory setup **) |
733 |
767 |
734 val setup = |
768 val setup = |