32 (* pretty *) |
32 (* pretty *) |
33 |
33 |
34 fun pretty loc ctxt = |
34 fun pretty loc ctxt = |
35 let |
35 let |
36 val thy = ProofContext.theory_of ctxt; |
36 val thy = ProofContext.theory_of ctxt; |
|
37 val loc_kind = if is_some (Class.class_of_locale thy loc) then "class" else "locale"; |
|
38 val loc_name = Locale.extern thy loc; |
|
39 |
37 val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt)); |
40 val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt)); |
38 val assumes = map (fn A => (("", []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt)); |
41 val assumes = map (fn A => (("", []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt)); |
39 val elems = |
42 val elems = |
40 (if null fixes then [] else [Element.Fixes fixes]) @ |
43 (if null fixes then [] else [Element.Fixes fixes]) @ |
41 (if null assumes then [] else [Element.Assumes assumes]); |
44 (if null assumes then [] else [Element.Assumes assumes]); |
42 in |
45 in |
43 if loc = "" then |
46 Pretty.block [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy)] :: |
44 [Pretty.block |
47 (if loc = "" then [] |
45 [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy), |
48 else if null elems then [Pretty.str (loc_kind ^ " " ^ loc_name)] |
46 Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]] |
49 else [Pretty.big_list (loc_kind ^ " " ^ loc_name ^ " =") |
47 else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)] |
50 (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]) |
48 else |
|
49 [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =") |
|
50 (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] |
|
51 end; |
51 end; |
52 |
52 |
53 |
53 |
54 (* target declarations *) |
54 (* target declarations *) |
55 |
55 |
75 (if loc = "" then Sign.naming_of (ProofContext.theory_of lthy) |
75 (if loc = "" then Sign.naming_of (ProofContext.theory_of lthy) |
76 else ProofContext.naming_of (LocalTheory.target_of lthy)) |
76 else ProofContext.naming_of (LocalTheory.target_of lthy)) |
77 |> NameSpace.qualified_names; |
77 |> NameSpace.qualified_names; |
78 |
78 |
79 |
79 |
|
80 |
|
81 (* notes *) |
|
82 |
|
83 fun import_export_proof ctxt (name, raw_th) = |
|
84 let |
|
85 val thy = ProofContext.theory_of ctxt; |
|
86 val thy_ctxt = ProofContext.init thy; |
|
87 val certT = Thm.ctyp_of thy; |
|
88 val cert = Thm.cterm_of thy; |
|
89 |
|
90 (*export assumes/defines*) |
|
91 val th = Goal.norm_result raw_th; |
|
92 val (defs, th') = LocalDefs.export ctxt thy_ctxt th; |
|
93 val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th); |
|
94 val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt); |
|
95 val nprems = Thm.nprems_of th' - Thm.nprems_of th; |
|
96 |
|
97 (*export fixes*) |
|
98 val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); |
|
99 val frees = map Free (Thm.fold_terms Term.add_frees th' []); |
|
100 val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees)) |
|
101 |> Variable.export ctxt thy_ctxt |
|
102 |> Drule.zero_var_indexes_list; |
|
103 |
|
104 (*thm definition*) |
|
105 val result = th'' |
|
106 |> PureThy.name_thm true true "" |
|
107 |> Goal.close_result |
|
108 |> fold PureThy.tag_rule (ContextPosition.properties_of ctxt) |
|
109 |> PureThy.name_thm true true name; |
|
110 |
|
111 (*import fixes*) |
|
112 val (tvars, vars) = |
|
113 chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) |
|
114 |>> map Logic.dest_type; |
|
115 |
|
116 val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); |
|
117 val inst = filter (is_Var o fst) (vars ~~ frees); |
|
118 val cinstT = map (pairself certT o apfst TVar) instT; |
|
119 val cinst = map (pairself (cert o Term.map_types (TermSubst.instantiateT instT))) inst; |
|
120 val result' = Thm.instantiate (cinstT, cinst) result; |
|
121 |
|
122 (*import assumes/defines*) |
|
123 val assm_tac = FIRST' (map (fn assm => Tactic.compose_tac (false, assm, 0)) assms); |
|
124 val result'' = |
|
125 (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of |
|
126 NONE => raise THM ("Failed to re-import result", 0, [result']) |
|
127 | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv]) |
|
128 |> Goal.norm_result |
|
129 |> PureThy.name_thm false false name; |
|
130 |
|
131 in (result'', result) end; |
|
132 |
|
133 fun local_notes loc kind facts lthy = |
|
134 let |
|
135 val is_loc = loc <> ""; |
|
136 val thy = ProofContext.theory_of lthy; |
|
137 val full = LocalTheory.full_name lthy; |
|
138 |
|
139 val facts' = facts |
|
140 |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi (full (fst a))) bs)) |
|
141 |> PureThy.map_facts (import_export_proof lthy); |
|
142 val local_facts = PureThy.map_facts #1 facts' |
|
143 |> Attrib.map_facts (Attrib.attribute_i thy); |
|
144 val target_facts = PureThy.map_facts #1 facts' |
|
145 |> is_loc ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy)); |
|
146 val global_facts = PureThy.map_facts #2 facts' |
|
147 |> Attrib.map_facts (if is_loc then K I else Attrib.attribute_i thy); |
|
148 in |
|
149 lthy |> LocalTheory.theory |
|
150 (Sign.qualified_names |
|
151 #> PureThy.note_thmss_i kind global_facts #> snd |
|
152 #> Sign.restore_naming thy) |
|
153 |
|
154 |> is_loc ? LocalTheory.target (Locale.add_thmss loc kind target_facts) |
|
155 |
|
156 |> ProofContext.qualified_names |
|
157 |> ProofContext.note_thmss_i kind local_facts |
|
158 ||> ProofContext.restore_naming lthy |
|
159 end; |
|
160 |
|
161 |
80 (* consts *) |
162 (* consts *) |
81 |
163 |
82 fun target_abbrev prmode ((c, mx), rhs) phi = |
164 fun target_abbrev prmode ((c, mx), rhs) phi = |
83 let |
165 let |
84 val c' = Morphism.name phi c; |
166 val c' = Morphism.name phi c; |
94 #-> (fn (lhs, _) => |
176 #-> (fn (lhs, _) => |
95 Term.equiv_types (rhs, rhs') ? |
177 Term.equiv_types (rhs, rhs') ? |
96 Morphism.form (ProofContext.target_notation prmode [(lhs, mx)]))) |
178 Morphism.form (ProofContext.target_notation prmode [(lhs, mx)]))) |
97 end; |
179 end; |
98 |
180 |
99 fun internal_abbrev prmode ((c, mx), t) lthy = lthy |
181 fun internal_abbrev loc prmode ((c, mx), t) lthy = lthy |
100 (* FIXME really permissive *) |
182 (* FIXME really permissive *) |
101 |> LocalTheory.term_syntax (perhaps o try o target_abbrev prmode ((c, mx), t)) |
183 |> term_syntax loc (perhaps o try o target_abbrev prmode ((c, mx), t)) |
102 |> ProofContext.add_abbrev Syntax.internalM (ContextPosition.properties_of lthy) (c, t) |
184 |> ProofContext.add_abbrev Syntax.internalM (ContextPosition.properties_of lthy) (c, t) |
103 |> snd; |
185 |> snd; |
104 |
186 |
105 fun consts is_loc some_class depends decls lthy = |
187 fun declare_consts loc depends decls lthy = |
106 let |
188 let |
|
189 val thy = ProofContext.theory_of lthy; |
|
190 val is_loc = loc <> ""; |
|
191 val some_class = Class.class_of_locale thy loc; |
|
192 |
107 val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy))); |
193 val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy))); |
108 |
194 |
109 fun const ((c, T), mx) thy = |
195 fun const ((c, T), mx) thy = |
110 let |
196 let |
111 val U = map #2 xs ---> T; |
197 val U = map #2 xs ---> T; |
113 val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx; |
199 val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx; |
114 val mx3 = if is_loc then NoSyn else mx1; |
200 val mx3 = if is_loc then NoSyn else mx1; |
115 val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy; |
201 val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy; |
116 in (((c, mx2), t), thy') end; |
202 in (((c, mx2), t), thy') end; |
117 fun const_class (SOME class) ((c, _), mx) (_, t) = |
203 fun const_class (SOME class) ((c, _), mx) (_, t) = |
118 LocalTheory.raw_theory_result |
204 LocalTheory.raw_theory_result (Class.add_const_in_class class ((c, t), mx)) |
119 (Class.add_const_in_class class ((c, t), mx)) |
205 #-> Class.remove_constraint [class] |
120 #-> (fn c => Class.remove_constraint [class] c) |
|
121 | const_class NONE _ _ = I; |
206 | const_class NONE _ _ = I; |
122 fun hide_abbrev (SOME class) abbrs thy = |
207 fun hide_abbrev (SOME class) abbrs thy = |
123 let |
208 let |
124 val raw_cs = map (fst o fst) abbrs; |
209 val raw_cs = map (fst o fst) abbrs; |
125 val prfx = (Logic.const_of_class o NameSpace.base) class; |
210 val prfx = (Logic.const_of_class o NameSpace.base) class; |
166 Variable.declare_term rhs #> |
251 Variable.declare_term rhs #> |
167 Assumption.add_assms (K (K (I, Envir.expand_term_frees [((x', T), rhs)]))) [] #> snd #> |
252 Assumption.add_assms (K (K (I, Envir.expand_term_frees [((x', T), rhs)]))) [] #> snd #> |
168 pair (lhs, rhs) |
253 pair (lhs, rhs) |
169 end); |
254 end); |
170 |
255 |
171 fun abbrev is_loc some_class prmode ((raw_c, mx), raw_t) lthy = |
256 fun abbrev loc prmode ((raw_c, mx), raw_t) lthy = |
172 let |
257 let |
173 val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy); |
258 val thy = ProofContext.theory_of lthy; |
|
259 val is_loc = loc <> ""; |
|
260 val some_class = Class.class_of_locale thy loc; |
|
261 |
|
262 val thy_ctxt = ProofContext.init thy; |
174 val target = LocalTheory.target_of lthy; |
263 val target = LocalTheory.target_of lthy; |
175 val target_morphism = LocalTheory.target_morphism lthy; |
264 val target_morphism = LocalTheory.target_morphism lthy; |
176 |
265 |
177 val c = Morphism.name target_morphism raw_c; |
266 val c = Morphism.name target_morphism raw_c; |
178 val t = Morphism.term target_morphism raw_t; |
267 val t = Morphism.term target_morphism raw_t; |
189 in |
278 in |
190 lthy |
279 lthy |
191 |> LocalTheory.theory_result |
280 |> LocalTheory.theory_result |
192 (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u')) |
281 (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u')) |
193 |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)]) |
282 |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)]) |
194 #> is_loc ? internal_abbrev prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs)) |
283 #> is_loc ? internal_abbrev loc prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs)) |
195 #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1) |
284 #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1) |
196 #> local_abbrev (c, rhs)) |
285 #> local_abbrev (c, rhs)) |
197 end; |
286 end; |
198 |
287 |
199 |
288 |
222 val def = Thm.instantiate (recover_sorts, []) axm'; |
311 val def = Thm.instantiate (recover_sorts, []) axm'; |
223 in (Drule.unvarify def, thy') end; |
312 in (Drule.unvarify def, thy') end; |
224 |
313 |
225 in |
314 in |
226 |
315 |
227 fun local_def kind ((c, mx), ((name, atts), rhs)) lthy1 = |
316 fun local_def loc kind ((c, mx), ((name, atts), rhs)) lthy1 = |
228 let |
317 let |
229 val (rhs', rhs_conv) = expand_term lthy1 rhs; |
318 val (rhs', rhs_conv) = expand_term lthy1 rhs; |
230 val xs = Variable.add_fixed (LocalTheory.target_of lthy1) rhs' []; |
319 val xs = Variable.add_fixed (LocalTheory.target_of lthy1) rhs' []; |
231 val T = Term.fastype_of rhs; |
320 val T = Term.fastype_of rhs; |
232 |
321 |
233 (*consts*) |
322 (*consts*) |
234 val ([(lhs, lhs_def)], lthy2) = lthy1 |
323 val ([(lhs, lhs_def)], lthy2) = lthy1 |
235 |> LocalTheory.consts (member (op =) xs) [((c, T), mx)]; |
324 |> declare_consts loc (member (op =) xs) [((c, T), mx)]; |
236 val (_, lhs') = Logic.dest_equals (Thm.prop_of lhs_def); |
325 val (_, lhs') = Logic.dest_equals (Thm.prop_of lhs_def); |
237 |
326 |
238 (*def*) |
327 (*def*) |
239 val name' = Thm.def_name_optional c name; |
328 val name' = Thm.def_name_optional c name; |
240 val (def, lthy3) = lthy2 |
329 val (def, lthy3) = lthy2 |
265 val prems = map (Thm.assume o Thm.cterm_of thy') hyps; |
354 val prems = map (Thm.assume o Thm.cterm_of thy') hyps; |
266 in (Drule.implies_elim_list axm prems, thy') end; |
355 in (Drule.implies_elim_list axm prems, thy') end; |
267 |
356 |
268 in |
357 in |
269 |
358 |
270 fun axioms kind specs lthy = |
359 fun axioms loc kind specs lthy = |
271 let |
360 let |
272 val hyps = map Thm.term_of (Assumption.assms_of lthy); |
361 val hyps = map Thm.term_of (Assumption.assms_of lthy); |
273 fun axiom ((name, atts), props) thy = thy |
362 fun axiom ((name, atts), props) thy = thy |
274 |> fold_map (add_axiom hyps) (PureThy.name_multi name props) |
363 |> fold_map (add_axiom hyps) (PureThy.name_multi name props) |
275 |-> (fn ths => pair ((name, atts), [(ths, [])])); |
364 |-> (fn ths => pair ((name, atts), [(ths, [])])); |
276 in |
365 in |
277 lthy |
366 lthy |
278 |> fold (fold Variable.declare_term o snd) specs |
367 |> fold (fold Variable.declare_term o snd) specs |
279 |> LocalTheory.theory_result (fold_map axiom specs) |
368 |> LocalTheory.theory_result (fold_map axiom specs) |
280 |-> LocalTheory.notes kind |
369 |-> local_notes loc kind |
281 end; |
370 end; |
282 |
371 |
283 end; |
372 end; |
284 |
|
285 |
|
286 (* notes *) |
|
287 |
|
288 fun import_export_proof ctxt (name, raw_th) = |
|
289 let |
|
290 val thy = ProofContext.theory_of ctxt; |
|
291 val thy_ctxt = ProofContext.init thy; |
|
292 val certT = Thm.ctyp_of thy; |
|
293 val cert = Thm.cterm_of thy; |
|
294 |
|
295 (*export assumes/defines*) |
|
296 val th = Goal.norm_result raw_th; |
|
297 val (defs, th') = LocalDefs.export ctxt thy_ctxt th; |
|
298 val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th); |
|
299 val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt); |
|
300 val nprems = Thm.nprems_of th' - Thm.nprems_of th; |
|
301 |
|
302 (*export fixes*) |
|
303 val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); |
|
304 val frees = map Free (Thm.fold_terms Term.add_frees th' []); |
|
305 val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees)) |
|
306 |> Variable.export ctxt thy_ctxt |
|
307 |> Drule.zero_var_indexes_list; |
|
308 |
|
309 (*thm definition*) |
|
310 val result = th'' |
|
311 |> PureThy.name_thm true true "" |
|
312 |> Goal.close_result |
|
313 |> fold PureThy.tag_rule (ContextPosition.properties_of ctxt) |
|
314 |> PureThy.name_thm true true name; |
|
315 |
|
316 (*import fixes*) |
|
317 val (tvars, vars) = |
|
318 chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) |
|
319 |>> map Logic.dest_type; |
|
320 |
|
321 val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); |
|
322 val inst = filter (is_Var o fst) (vars ~~ frees); |
|
323 val cinstT = map (pairself certT o apfst TVar) instT; |
|
324 val cinst = map (pairself (cert o Term.map_types (TermSubst.instantiateT instT))) inst; |
|
325 val result' = Thm.instantiate (cinstT, cinst) result; |
|
326 |
|
327 (*import assumes/defines*) |
|
328 val assm_tac = FIRST' (map (fn assm => Tactic.compose_tac (false, assm, 0)) assms); |
|
329 val result'' = |
|
330 (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of |
|
331 NONE => raise THM ("Failed to re-import result", 0, [result']) |
|
332 | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv]) |
|
333 |> Goal.norm_result |
|
334 |> PureThy.name_thm false false name; |
|
335 |
|
336 in (result'', result) end; |
|
337 |
|
338 fun notes loc kind facts lthy = |
|
339 let |
|
340 val is_loc = loc <> ""; |
|
341 val thy = ProofContext.theory_of lthy; |
|
342 val full = LocalTheory.full_name lthy; |
|
343 |
|
344 val facts' = facts |
|
345 |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi (full (fst a))) bs)) |
|
346 |> PureThy.map_facts (import_export_proof lthy); |
|
347 val local_facts = PureThy.map_facts #1 facts' |
|
348 |> Attrib.map_facts (Attrib.attribute_i thy); |
|
349 val target_facts = PureThy.map_facts #1 facts' |
|
350 |> is_loc ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy)); |
|
351 val global_facts = PureThy.map_facts #2 facts' |
|
352 |> Attrib.map_facts (if is_loc then K I else Attrib.attribute_i thy); |
|
353 in |
|
354 lthy |> LocalTheory.theory |
|
355 (Sign.qualified_names |
|
356 #> PureThy.note_thmss_i kind global_facts #> snd |
|
357 #> Sign.restore_naming thy) |
|
358 |
|
359 |> is_loc ? LocalTheory.target (Locale.add_thmss loc kind target_facts) |
|
360 |
|
361 |> ProofContext.qualified_names |
|
362 |> ProofContext.note_thmss_i kind local_facts |
|
363 ||> ProofContext.restore_naming lthy |
|
364 end; |
|
365 |
373 |
366 |
374 |
367 (* init and exit *) |
375 (* init and exit *) |
368 |
376 |
369 fun begin loc ctxt = |
377 fun begin loc ctxt = |
370 let |
378 let |
371 val thy = ProofContext.theory_of ctxt; |
379 val thy = ProofContext.theory_of ctxt; |
372 val is_loc = loc <> ""; |
380 val is_loc = loc <> ""; |
373 val some_class = Class.class_of_locale thy loc; |
|
374 in |
381 in |
375 ctxt |
382 ctxt |
376 |> Data.put (if is_loc then SOME loc else NONE) |
383 |> Data.put (if is_loc then SOME loc else NONE) |
377 |> fold Class.init (the_list some_class) |
384 |> fold Class.init (the_list (Class.class_of_locale thy loc)) |
378 |> LocalTheory.init (NameSpace.base loc) |
385 |> LocalTheory.init (NameSpace.base loc) |
379 {pretty = pretty loc, |
386 {pretty = pretty loc, |
380 consts = consts is_loc some_class, |
387 consts = declare_consts loc, |
381 axioms = axioms, |
388 axioms = axioms loc, |
382 abbrev = abbrev is_loc some_class, |
389 abbrev = abbrev loc, |
383 def = local_def, |
390 def = local_def loc, |
384 notes = notes loc, |
391 notes = local_notes loc, |
385 type_syntax = type_syntax loc, |
392 type_syntax = type_syntax loc, |
386 term_syntax = term_syntax loc, |
393 term_syntax = term_syntax loc, |
387 declaration = declaration loc, |
394 declaration = declaration loc, |
388 target_naming = target_naming loc, |
395 target_naming = target_naming loc, |
389 reinit = fn _ => |
396 reinit = fn _ => |