3 Author: Makarius |
3 Author: Makarius |
4 |
4 |
5 Local theory operations, with optional target locale. |
5 Local theory operations, with optional target locale. |
6 *) |
6 *) |
7 |
7 |
|
8 type local_theory = Proof.context; |
|
9 |
8 signature LOCAL_THEORY = |
10 signature LOCAL_THEORY = |
9 sig |
11 sig |
10 val params_of: Proof.context -> (string * typ) list |
12 val params_of: local_theory -> (string * typ) list |
11 val hyps_of: Proof.context -> term list |
13 val hyps_of: local_theory -> term list |
12 val standard: Proof.context -> thm -> thm |
14 val standard: local_theory -> thm -> thm |
13 val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T |
15 val pretty_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> Pretty.T |
14 val print_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit |
16 val quiet_mode: bool ref |
15 val theory: (theory -> theory) -> Proof.context -> Proof.context |
17 val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit |
16 val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context |
18 val theory: (theory -> theory) -> local_theory -> local_theory |
17 val init: xstring option -> theory -> Proof.context |
19 val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory |
18 val init_i: string option -> theory -> Proof.context |
20 val init: xstring option -> theory -> local_theory |
19 val exit: Proof.context -> Proof.context * theory |
21 val init_i: string option -> theory -> local_theory |
20 val consts: ((bstring * typ) * mixfix) list -> Proof.context -> term list * Proof.context |
22 val exit: local_theory -> local_theory * theory |
|
23 val consts: ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory |
21 val consts_restricted: (string * typ -> bool) -> |
24 val consts_restricted: (string * typ -> bool) -> |
22 ((bstring * typ) * mixfix) list -> Proof.context -> term list * Proof.context |
25 ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory |
23 val axioms: ((bstring * Attrib.src list) * term list) list -> Proof.context -> |
26 val axioms: ((bstring * Attrib.src list) * term list) list -> local_theory -> |
24 (bstring * thm list) list * Proof.context |
27 (bstring * thm list) list * local_theory |
25 val axioms_finish: (Proof.context -> thm -> thm) -> |
28 val axioms_finish: (local_theory -> thm -> thm) -> |
26 ((bstring * Attrib.src list) * term list) list -> Proof.context -> |
29 ((bstring * Attrib.src list) * term list) list -> local_theory -> |
27 (bstring * thm list) list * Proof.context |
30 (bstring * thm list) list * local_theory |
28 val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
31 val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> |
29 Proof.context -> (bstring * thm list) list * Proof.context |
32 local_theory -> (bstring * thm list) list * local_theory |
30 val note: (bstring * Attrib.src list) * thm list -> Proof.context -> |
33 val note: (bstring * Attrib.src list) * thm list -> local_theory -> |
31 (bstring * thm list) * Proof.context |
34 (bstring * thm list) * local_theory |
32 val def: (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> |
35 val def: (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> |
33 Proof.context -> (term * (bstring * thm)) * Proof.context |
36 local_theory -> (term * (bstring * thm)) * local_theory |
34 val def_finish: (Proof.context -> term -> thm -> thm) -> |
37 val def_finish: (local_theory -> term -> thm -> thm) -> |
35 (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> |
38 (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> |
36 Proof.context -> (term * (bstring * thm)) * Proof.context |
39 local_theory -> (term * (bstring * thm)) * local_theory |
37 end; |
40 end; |
38 |
41 |
39 structure LocalTheory: LOCAL_THEORY = |
42 structure LocalTheory: LOCAL_THEORY = |
40 struct |
43 struct |
41 |
44 |
69 | SOME (_, (_, loc_ctxt)) => ProofContext.export_standard ctxt loc_ctxt); |
72 | SOME (_, (_, loc_ctxt)) => ProofContext.export_standard ctxt loc_ctxt); |
70 |
73 |
71 |
74 |
72 (* print consts *) |
75 (* print consts *) |
73 |
76 |
|
77 val quiet_mode = ref false; |
|
78 |
74 local |
79 local |
75 |
80 |
76 fun pretty_var ctxt (x, T) = |
81 fun pretty_var ctxt (x, T) = |
77 Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1, |
82 Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1, |
78 Pretty.quote (ProofContext.pretty_typ ctxt T)]; |
83 Pretty.quote (ProofContext.pretty_typ ctxt T)]; |
85 (case filter pred (params_of ctxt) of |
90 (case filter pred (params_of ctxt) of |
86 [] => pretty_vars ctxt "constants" cs |
91 [] => pretty_vars ctxt "constants" cs |
87 | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]); |
92 | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]); |
88 |
93 |
89 fun print_consts _ _ [] = () |
94 fun print_consts _ _ [] = () |
90 | print_consts ctxt pred cs = Pretty.writeln (pretty_consts ctxt pred cs); |
95 | print_consts ctxt pred cs = |
|
96 if ! quiet_mode then () else Pretty.writeln (pretty_consts ctxt pred cs); |
91 |
97 |
92 end; |
98 end; |
93 |
99 |
94 |
100 |
95 (* theory/locale substructures *) |
101 (* theory/locale substructures *) |