18 val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
18 val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
19 val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list |
19 val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list |
20 val burrow_facts: ('a list -> 'b list) -> |
20 val burrow_facts: ('a list -> 'b list) -> |
21 ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
21 ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
22 val name_multi: string -> 'a list -> (string * 'a) list |
22 val name_multi: string -> 'a list -> (string * 'a) list |
23 val name_thm: bool -> bool -> string -> thm -> thm |
23 val name_thm: bool -> bool -> Position.T -> string -> thm -> thm |
24 val name_thms: bool -> bool -> string -> thm list -> thm list |
24 val name_thms: bool -> bool -> Position.T -> string -> thm list -> thm list |
25 val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list |
25 val name_thmss: bool -> Position.T -> string -> (thm list * 'a) list -> (thm list * 'a) list |
26 val store_thms: bstring * thm list -> theory -> thm list * theory |
26 val store_thms: bstring * thm list -> theory -> thm list * theory |
27 val store_thm: bstring * thm -> theory -> thm * theory |
27 val store_thm: bstring * thm -> theory -> thm * theory |
28 val store_thm_open: bstring * thm -> theory -> thm * theory |
28 val store_thm_open: bstring * thm -> theory -> thm * theory |
29 val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory |
29 val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory |
30 val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory |
30 val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory |
31 val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory |
31 val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory |
32 val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory |
32 val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory |
33 val note_thmss: string -> ((bstring * attribute list) * |
33 val note_thmss: string -> ((Name.binding * attribute list) * |
34 (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory |
34 (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory |
35 val note_thmss_grouped: string -> string -> ((bstring * attribute list) * |
35 val note_thmss_grouped: string -> string -> ((Name.binding * attribute list) * |
36 (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory |
36 (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory |
37 val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory |
37 val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory |
38 val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory |
38 val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory |
39 val add_defs: bool -> ((bstring * term) * attribute list) list -> |
39 val add_defs: bool -> ((bstring * term) * attribute list) list -> |
40 theory -> thm list * theory |
40 theory -> thm list * theory |
41 val add_defs_unchecked: bool -> ((bstring * term) * attribute list) list -> |
41 val add_defs_unchecked: bool -> ((bstring * term) * attribute list) list -> |
113 |
113 |
114 fun name_multi name [x] = [(name, x)] |
114 fun name_multi name [x] = [(name, x)] |
115 | name_multi "" xs = map (pair "") xs |
115 | name_multi "" xs = map (pair "") xs |
116 | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; |
116 | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; |
117 |
117 |
118 fun name_thm pre official name thm = thm |
118 fun name_thm pre official pos name thm = thm |
119 |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) |
119 |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) |
120 |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name) |
120 |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name) |
|
121 |> Thm.default_position pos |
121 |> Thm.default_position (Position.thread_data ()); |
122 |> Thm.default_position (Position.thread_data ()); |
122 |
123 |
123 fun name_thms pre official name xs = |
124 fun name_thms pre official pos name xs = |
124 map (uncurry (name_thm pre official)) (name_multi name xs); |
125 map (uncurry (name_thm pre official pos)) (name_multi name xs); |
125 |
126 |
126 fun name_thmss official name fact = |
127 fun name_thmss official pos name fact = |
127 burrow_fact (name_thms true official name) fact; |
128 burrow_fact (name_thms true official pos name) fact; |
128 |
129 |
129 |
130 |
130 (* enter_thms *) |
131 (* enter_thms *) |
131 |
132 |
132 fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) |> swap |
133 fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) |> swap |
140 in (thms'', thy'') end; |
141 in (thms'', thy'') end; |
141 |
142 |
142 |
143 |
143 (* store_thm(s) *) |
144 (* store_thm(s) *) |
144 |
145 |
145 val store_thms = enter_thms (name_thms true true) (name_thms false true) I; |
146 val store_thms = |
|
147 enter_thms (name_thms true true Position.none) (name_thms false true Position.none) I; |
|
148 |
146 fun store_thm (name, th) = store_thms (name, [th]) #>> the_single; |
149 fun store_thm (name, th) = store_thms (name, [th]) #>> the_single; |
147 |
150 |
148 fun store_thm_open (name, th) = |
151 fun store_thm_open (name, th) = |
149 enter_thms (name_thms true false) (name_thms false false) I (name, [th]) #>> the_single; |
152 enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I |
|
153 (name, [th]) #>> the_single; |
150 |
154 |
151 |
155 |
152 (* add_thms(s) *) |
156 (* add_thms(s) *) |
153 |
157 |
154 fun add_thms_atts pre_name ((bname, thms), atts) = |
158 fun add_thms_atts pre_name ((bname, thms), atts) = |
155 enter_thms pre_name (name_thms false true) |
159 enter_thms pre_name (name_thms false true Position.none) |
156 (foldl_map (Thm.theory_attributes atts)) (bname, thms); |
160 (foldl_map (Thm.theory_attributes atts)) (bname, thms); |
157 |
161 |
158 fun gen_add_thmss pre_name = |
162 fun gen_add_thmss pre_name = |
159 fold_map (add_thms_atts pre_name); |
163 fold_map (add_thms_atts pre_name); |
160 |
164 |
161 fun gen_add_thms pre_name args = |
165 fun gen_add_thms pre_name args = |
162 apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args); |
166 apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args); |
163 |
167 |
164 val add_thmss = gen_add_thmss (name_thms true true); |
168 val add_thmss = gen_add_thmss (name_thms true true Position.none); |
165 val add_thms = gen_add_thms (name_thms true true); |
169 val add_thms = gen_add_thms (name_thms true true Position.none); |
166 val add_thm = yield_singleton add_thms; |
170 val add_thm = yield_singleton add_thms; |
167 |
171 |
168 |
172 |
169 (* add_thms_dynamic *) |
173 (* add_thms_dynamic *) |
170 |
174 |
175 |
179 |
176 (* note_thmss *) |
180 (* note_thmss *) |
177 |
181 |
178 local |
182 local |
179 |
183 |
180 fun gen_note_thmss tag = fold_map (fn ((bname, more_atts), ths_atts) => fn thy => |
184 fun gen_note_thmss tag = fold_map (fn ((binding, more_atts), ths_atts) => fn thy => |
181 let |
185 let |
|
186 val bname = Name.name_of binding; |
|
187 val pos = Name.pos_of binding; |
|
188 val name = Sign.full_name thy bname; |
|
189 val _ = Position.report (Markup.fact_decl name) pos; |
|
190 |
182 fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths); |
191 fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths); |
183 val (thms, thy') = thy |> enter_thms |
192 val (thms, thy') = thy |> enter_thms |
184 (name_thmss true) (name_thms false true) (apsnd flat o foldl_map app) |
193 (name_thmss true pos) (name_thms false true pos) (apsnd flat o foldl_map app) |
185 (bname, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts); |
194 (bname, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts); |
186 in ((bname, thms), thy') end); |
195 in ((name, thms), thy') end); |
187 |
196 |
188 in |
197 in |
189 |
198 |
190 fun note_thmss k = gen_note_thmss (Thm.kind k); |
199 fun note_thmss k = gen_note_thmss (Thm.kind k); |
191 fun note_thmss_grouped k g = gen_note_thmss (Thm.kind k #> Thm.group g); |
200 fun note_thmss_grouped k g = gen_note_thmss (Thm.kind k #> Thm.group g); |