1 (* Title: Pure/Isar/locale.ML |
1 (* Title: Pure/Isar/locale.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU München |
3 Author: Markus Wenzel, LMU München |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 Locales -- Isar proof contexts as meta-level predicates, with local |
6 Locales -- Isar proof contexts as meta-level predicates, with local |
7 syntax and implicit structures. |
7 syntax and implicit structures. |
8 |
8 |
51 end; |
51 end; |
52 |
52 |
53 structure Locale: LOCALE = |
53 structure Locale: LOCALE = |
54 struct |
54 struct |
55 |
55 |
56 |
|
57 (** locale elements and expressions **) |
56 (** locale elements and expressions **) |
58 |
57 |
59 type context = ProofContext.context; |
58 type context = ProofContext.context; |
60 |
59 |
61 datatype ('typ, 'term, 'fact, 'att) elem = |
60 datatype ('typ, 'term, 'fact, 'att) elem = |
212 |
211 |
213 fun inst_thm [] th = th |
212 fun inst_thm [] th = th |
214 | inst_thm env th = |
213 | inst_thm env th = |
215 let |
214 let |
216 val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th; |
215 val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th; |
217 val cert = Thm.cterm_of sign and certT = Thm.ctyp_of sign; |
216 val cert = Thm.cterm_of sign; |
218 val names = foldr Term.add_term_tfree_names (prop :: hyps, []); |
217 val certT = Thm.ctyp_of sign; |
219 val env' = filter (fn ((a, _), _) => a mem_string names) env; |
218 val occs = foldr Term.add_term_tfree_names (prop :: hyps, []); |
|
219 val env' = filter (fn ((a, _), _) => a mem_string occs) env; |
220 in |
220 in |
221 if null env' then th |
221 if null env' then th |
222 else |
222 else |
223 th |
223 th |
224 |> Drule.implies_intr_list (map cert hyps) |
224 |> Drule.implies_intr_list (map cert hyps) |
225 |> Drule.tvars_intr_list names |
225 |> Drule.tvars_intr_list (map (#1 o #1) env') |
226 |> (fn (th', al) => th' |> |
226 |> (fn (th', al) => th' |> |
227 Thm.instantiate ((map (fn ((a, _), T) => (the (assoc (al, a)), certT T)) env'), [])) |
227 Thm.instantiate ((map (fn ((a, _), T) => (the (assoc (al, a)), certT T)) env'), [])) |
228 |> (fn th'' => Drule.implies_elim_list th'' |
228 |> (fn th'' => Drule.implies_elim_list th'' |
229 (map (Thm.assume o cert o inst_term env') hyps)) |
229 (map (Thm.assume o cert o inst_term env') hyps)) |
230 end; |
230 end; |
322 val envs = unify_parms ctxt fixed_parms (map (#2 o #1) elemss); |
322 val envs = unify_parms ctxt fixed_parms (map (#2 o #1) elemss); |
323 fun inst (((name, ps), elems), env) = |
323 fun inst (((name, ps), elems), env) = |
324 ((name, map (apsnd (apsome (inst_type env))) ps), map (inst_elem env) elems); |
324 ((name, map (apsnd (apsome (inst_type env))) ps), map (inst_elem env) elems); |
325 in map inst (elemss ~~ envs) end; |
325 in map inst (elemss ~~ envs) end; |
326 |
326 |
327 fun flatten_expr ctxt expr = |
327 fun flatten_expr ctxt (prev_idents, expr) = |
328 let |
328 let |
329 val thy = ProofContext.theory_of ctxt; |
329 val thy = ProofContext.theory_of ctxt; |
330 |
330 |
331 fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys |
331 fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys |
332 | renaming (None :: xs) (y :: ys) = renaming xs ys |
332 | renaming (None :: xs) (y :: ys) = renaming xs ys |
368 else ((map (apfst (rename ren)) ps, map (rename ren) qs), |
368 else ((map (apfst (rename ren)) ps, map (rename ren) qs), |
369 map (rename_elem ren o #1) elems); |
369 map (rename_elem ren o #1) elems); |
370 val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems'; |
370 val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems'; |
371 in ((name, params'), elems'') end; |
371 in ((name, params'), elems'') end; |
372 |
372 |
373 val raw_elemss = unique_parms ctxt (map eval (#1 (identify (([], []), expr)))); |
373 val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents); |
|
374 val raw_elemss = unique_parms ctxt (map eval idents); |
374 val elemss = unify_elemss ctxt [] raw_elemss; |
375 val elemss = unify_elemss ctxt [] raw_elemss; |
375 in elemss end; |
376 in (prev_idents @ idents, elemss) end; |
376 |
377 |
377 end; |
378 end; |
378 |
379 |
379 |
380 |
380 (* activate elements *) |
381 (* activate elements *) |
381 |
382 |
382 fun declare_fixes fixes = |
|
383 ProofContext.add_syntax fixes o |
|
384 ProofContext.fix_direct (map (fn (x, T, _) => ([x], T)) fixes); |
|
385 |
|
386 local |
383 local |
387 |
384 |
388 fun activate_elem (Fixes fixes) = declare_fixes fixes |
385 fun activate_elem (Fixes fixes) = ProofContext.add_fixes fixes |
389 | activate_elem (Assumes asms) = |
386 | activate_elem (Assumes asms) = |
390 #1 o ProofContext.assume_i ProofContext.export_assume asms o |
387 #1 o ProofContext.assume_i ProofContext.export_assume asms o |
391 ProofContext.fix_frees (flat (map (map #1 o #2) asms)) |
388 ProofContext.fix_frees (flat (map (map #1 o #2) asms)) |
392 | activate_elem (Defines defs) = (fn ctxt => #1 (ProofContext.assume_i ProofContext.export_def |
389 | activate_elem (Defines defs) = (fn ctxt => #1 (ProofContext.assume_i ProofContext.export_def |
393 (map (fn ((name, atts), (t, ps)) => |
390 (map (fn ((name, atts), (t, ps)) => |
455 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b; |
452 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b; |
456 |
453 |
457 local |
454 local |
458 |
455 |
459 fun declare_int_elem i (ctxt, Fixes fixes) = |
456 fun declare_int_elem i (ctxt, Fixes fixes) = |
460 (ctxt |> declare_fixes (map (fn (x, T, mx) => |
457 (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) => |
461 (x, apsome (Term.map_type_tfree (Type.param i)) T, mx)) fixes), []) |
458 (x, apsome (Term.map_type_tfree (Type.param i)) T, mx)) fixes), []) |
462 | declare_int_elem _ (ctxt, _) = (ctxt, []); |
459 | declare_int_elem _ (ctxt, _) = (ctxt, []); |
463 |
460 |
464 fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) = |
461 fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) = |
465 (ctxt |> declare_fixes (prep_fixes ctxt fixes), []) |
462 (ctxt |> ProofContext.add_fixes (prep_fixes ctxt fixes), []) |
466 | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms) |
463 | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms) |
467 | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs) |
464 | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs) |
468 | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []); |
465 | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []); |
469 |
466 |
470 fun declare_elems prep_fixes ((ctxt, i), ((name, ps), elems)) = |
467 fun declare_elems prep_fixes ((ctxt, i), ((name, ps), elems)) = |
478 |
475 |
479 fun close_frees ctxt t = |
476 fun close_frees ctxt t = |
480 let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Term.add_frees ([], t))) |
477 let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Term.add_frees ([], t))) |
481 in Term.list_all_free (frees, t) end; |
478 in Term.list_all_free (frees, t) end; |
482 |
479 |
|
480 fun no_binds _ [] = [] |
|
481 | no_binds ctxt _ = raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt); |
|
482 |
483 fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) => |
483 fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) => |
484 (a, map (fn (t, _) => (close_frees ctxt t, ([], []))) propps))) |
484 (a, map (fn (t, (ps, qs)) => (close_frees ctxt t, |
485 | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, _)) => |
485 (no_binds ctxt ps, no_binds ctxt qs))) propps))) |
486 (a, (close_frees ctxt (#2 (ProofContext.cert_def ctxt t)), [])))) |
486 | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, ps)) => |
|
487 (a, (close_frees ctxt (#2 (ProofContext.cert_def ctxt t)), no_binds ctxt ps)))) |
487 | closeup ctxt elem = elem; |
488 | closeup ctxt elem = elem; |
488 |
489 |
489 fun finish_elem parms _ (Fixes fixes, _) = Ext (Fixes (map (fn (x, _, mx) => |
490 fun finish_elem parms _ (Fixes fixes, _) = Ext (Fixes (map (fn (x, _, mx) => |
490 (x, assoc_string (parms, x), mx)) fixes)) |
491 (x, assoc_string (parms, x), mx)) fixes)) |
491 | finish_elem _ close (Assumes asms, propp) = Ext (close (Assumes (map #1 asms ~~ propp))) |
492 | finish_elem _ close (Assumes asms, propp) = Ext (close (Assumes (map #1 asms ~~ propp))) |
569 |
570 |
570 fun prep_context_statement prep_expr prep_elemss prep_facts |
571 fun prep_context_statement prep_expr prep_elemss prep_facts |
571 close fixed_params import elements raw_concl context = |
572 close fixed_params import elements raw_concl context = |
572 let |
573 let |
573 val sign = ProofContext.sign_of context; |
574 val sign = ProofContext.sign_of context; |
574 fun flatten (Elem (Fixes fixes)) = [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))] |
575 fun flatten (ids, Elem (Fixes fixes)) = |
575 | flatten (Elem elem) = [(("", []), Ext elem)] |
576 (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))]) |
576 | flatten (Expr expr) = map (apsnd Int) (flatten_expr context (prep_expr sign expr)); |
577 | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)]) |
|
578 | flatten (ids, Expr expr) = |
|
579 let val (ids', elemss) = flatten_expr context (ids, prep_expr sign expr) |
|
580 in (ids', map (apsnd Int) elemss) end |
577 val activate = activate_facts prep_facts; |
581 val activate = activate_facts prep_facts; |
578 |
582 |
579 val raw_import_elemss = flatten (Expr import); |
583 val (import_ids, raw_import_elemss) = flatten ([], Expr import); |
580 val raw_elemss = flat (map flatten elements); |
584 val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements)))); |
581 val (parms, all_elemss, concl) = |
585 val (parms, all_elemss, concl) = |
582 prep_elemss close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; |
586 prep_elemss close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; |
583 |
587 |
584 val n = length raw_import_elemss; |
588 val n = length raw_import_elemss; |
585 val (import_ctxt, import_elemss) = foldl_map activate (context, take (n, all_elemss)); |
589 val (import_ctxt, import_elemss) = foldl_map activate (context, take (n, all_elemss)); |
623 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
627 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
624 val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt; |
628 val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt; |
625 |
629 |
626 fun prt_syn syn = |
630 fun prt_syn syn = |
627 let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx) |
631 let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx) |
628 in if s = "" then [] else [Pretty.brk 4, Pretty.str s] end; |
632 in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end; |
629 fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: |
633 fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: |
630 prt_typ T :: Pretty.brk 1 :: prt_syn syn) |
634 prt_typ T :: Pretty.brk 1 :: prt_syn syn) |
631 | prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn); |
635 | prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn); |
632 |
636 |
633 fun prt_name "" = [Pretty.brk 1] |
637 fun prt_name "" = [Pretty.brk 1] |