| author | wenzelm |
| Mon, 13 Apr 2020 22:08:14 +0200 | |
| changeset 71751 | abf3e80bd815 |
| parent 70734 | 31364e70ff3e |
| child 71674 | 48ff625687f5 |
| permissions | -rw-r--r-- |
| 5819 | 1 |
(* Title: Pure/Isar/proof_context.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
| 19001 | 4 |
The key concept of Isar proof contexts: elevates primitive local |
5 |
reasoning Gamma |- phi to a structured concept, with generic context |
|
|
20234
7e0693474bcd
added legacy_pretty_thm (with fall-back on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset
|
6 |
elements. See also structure Variable and Assumption. |
| 5819 | 7 |
*) |
8 |
||
9 |
signature PROOF_CONTEXT = |
|
10 |
sig |
|
| 20310 | 11 |
val theory_of: Proof.context -> theory |
|
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36542
diff
changeset
|
12 |
val init_global: theory -> Proof.context |
| 51686 | 13 |
val get_global: theory -> string -> Proof.context |
|
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset
|
14 |
type mode |
| 24501 | 15 |
val mode_default: mode |
16 |
val mode_pattern: mode |
|
17 |
val mode_schematic: mode |
|
18 |
val mode_abbrev: mode |
|
|
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset
|
19 |
val set_mode: mode -> Proof.context -> Proof.context |
|
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset
|
20 |
val get_mode: Proof.context -> mode |
|
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset
|
21 |
val restore_mode: Proof.context -> Proof.context -> Proof.context |
| 27286 | 22 |
val abbrev_mode: Proof.context -> bool |
| 35111 | 23 |
val syn_of: Proof.context -> Syntax.syntax |
|
35669
a91c7ed801b8
added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
wenzelm
parents:
35616
diff
changeset
|
24 |
val tsig_of: Proof.context -> Type.tsig |
| 36451 | 25 |
val set_defsort: sort -> Proof.context -> Proof.context |
| 35680 | 26 |
val default_sort: Proof.context -> indexname -> sort |
| 59840 | 27 |
val arity_sorts: Proof.context -> string -> sort -> sort list |
| 20310 | 28 |
val consts_of: Proof.context -> Consts.T |
| 20784 | 29 |
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context |
| 20310 | 30 |
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context |
|
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset
|
31 |
val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context |
|
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset
|
32 |
val naming_of: Proof.context -> Name_Space.naming |
|
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset
|
33 |
val restore_naming: Proof.context -> Proof.context -> Proof.context |
|
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset
|
34 |
val full_name: Proof.context -> binding -> string |
| 59886 | 35 |
val get_scope: Proof.context -> Binding.scope option |
36 |
val new_scope: Proof.context -> Binding.scope * Proof.context |
|
|
59923
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59917
diff
changeset
|
37 |
val private_scope: Binding.scope -> Proof.context -> Proof.context |
|
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59917
diff
changeset
|
38 |
val private: Position.T -> Proof.context -> Proof.context |
|
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59970
diff
changeset
|
39 |
val qualified_scope: Binding.scope -> Proof.context -> Proof.context |
|
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59970
diff
changeset
|
40 |
val qualified: Position.T -> Proof.context -> Proof.context |
|
59880
30687c3f2b10
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
wenzelm
parents:
59859
diff
changeset
|
41 |
val concealed: Proof.context -> Proof.context |
| 42359 | 42 |
val class_space: Proof.context -> Name_Space.T |
43 |
val type_space: Proof.context -> Name_Space.T |
|
44 |
val const_space: Proof.context -> Name_Space.T |
|
|
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61168
diff
changeset
|
45 |
val defs_context: Proof.context -> Defs.context |
| 42359 | 46 |
val intern_class: Proof.context -> xstring -> string |
47 |
val intern_type: Proof.context -> xstring -> string |
|
48 |
val intern_const: Proof.context -> xstring -> string |
|
49 |
val extern_class: Proof.context -> string -> xstring |
|
| 55304 | 50 |
val markup_class: Proof.context -> string -> string |
51 |
val pretty_class: Proof.context -> string -> Pretty.T |
|
| 42359 | 52 |
val extern_type: Proof.context -> string -> xstring |
| 55304 | 53 |
val markup_type: Proof.context -> string -> string |
54 |
val pretty_type: Proof.context -> string -> Pretty.T |
|
| 42359 | 55 |
val extern_const: Proof.context -> string -> xstring |
| 55304 | 56 |
val markup_const: Proof.context -> string -> string |
57 |
val pretty_const: Proof.context -> string -> Pretty.T |
|
| 20310 | 58 |
val transfer: theory -> Proof.context -> Proof.context |
|
57928
f4ff42c5b05b
transfer result of Global_Theory.add_thms_dynamic to context stack;
wenzelm
parents:
57887
diff
changeset
|
59 |
val transfer_facts: theory -> Proof.context -> Proof.context |
|
38756
d07959fabde6
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38328
diff
changeset
|
60 |
val background_theory: (theory -> theory) -> Proof.context -> Proof.context |
|
d07959fabde6
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38328
diff
changeset
|
61 |
val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context |
|
56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset
|
62 |
val facts_of: Proof.context -> Facts.T |
|
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset
|
63 |
val facts_of_fact: Proof.context -> string -> Facts.T |
|
63080
8326aa594273
find dynamic facts as well, but static ones are preferred;
wenzelm
parents:
63057
diff
changeset
|
64 |
val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring |
| 70308 | 65 |
val augment: term -> Proof.context -> Proof.context |
|
64398
5076725247fa
more robust printing of names in the context of outer syntax;
wenzelm
parents:
63640
diff
changeset
|
66 |
val print_name: Proof.context -> string -> string |
|
5076725247fa
more robust printing of names in the context of outer syntax;
wenzelm
parents:
63640
diff
changeset
|
67 |
val pretty_name: Proof.context -> string -> Pretty.T |
| 21728 | 68 |
val pretty_term_abbrev: Proof.context -> term -> Pretty.T |
| 20310 | 69 |
val pretty_fact: Proof.context -> string * thm list -> Pretty.T |
|
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset
|
70 |
val check_class: Proof.context -> xstring * Position.T -> class * Position.report list |
|
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset
|
71 |
val read_class: Proof.context -> string -> class |
| 20310 | 72 |
val read_typ: Proof.context -> string -> typ |
73 |
val read_typ_syntax: Proof.context -> string -> typ |
|
74 |
val read_typ_abbrev: Proof.context -> string -> typ |
|
75 |
val cert_typ: Proof.context -> typ -> typ |
|
76 |
val cert_typ_syntax: Proof.context -> typ -> typ |
|
77 |
val cert_typ_abbrev: Proof.context -> typ -> typ |
|
|
36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36503
diff
changeset
|
78 |
val infer_type: Proof.context -> string * typ -> typ |
| 60407 | 79 |
val inferred_param: string -> Proof.context -> (string * typ) * Proof.context |
| 25328 | 80 |
val inferred_fixes: Proof.context -> (string * typ) list * Proof.context |
| 56002 | 81 |
val check_type_name: {proper: bool, strict: bool} -> Proof.context ->
|
|
55922
710bc66f432c
more markup for inner syntax class/type names (notably for completion);
wenzelm
parents:
55843
diff
changeset
|
82 |
xstring * Position.T -> typ * Position.report list |
| 56002 | 83 |
val read_type_name: {proper: bool, strict: bool} -> Proof.context -> string -> typ
|
|
55956
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55955
diff
changeset
|
84 |
val consts_completion_message: Proof.context -> xstring * Position.T list -> string |
| 56002 | 85 |
val check_const: {proper: bool, strict: bool} -> Proof.context ->
|
|
55959
c3b458435f4f
more decisive commitment to get_free vs. the_const;
wenzelm
parents:
55956
diff
changeset
|
86 |
xstring * Position.T list -> term * Position.report list |
| 56002 | 87 |
val read_const: {proper: bool, strict: bool} -> Proof.context -> string -> term
|
|
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset
|
88 |
val read_arity: Proof.context -> xstring * string list * string -> arity |
|
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
46849
diff
changeset
|
89 |
val cert_arity: Proof.context -> arity -> arity |
| 27259 | 90 |
val allow_dummies: Proof.context -> Proof.context |
|
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56294
diff
changeset
|
91 |
val prepare_sortsT: Proof.context -> typ list -> string list * typ list |
|
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56294
diff
changeset
|
92 |
val prepare_sorts: Proof.context -> term list -> string list * term list |
| 36152 | 93 |
val check_tfree: Proof.context -> string * sort -> string * sort |
| 24684 | 94 |
val read_term_pattern: Proof.context -> string -> term |
95 |
val read_term_schematic: Proof.context -> string -> term |
|
96 |
val read_term_abbrev: Proof.context -> string -> term |
|
|
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
39557
diff
changeset
|
97 |
val show_abbrevs: bool Config.T |
|
25345
dd5b851f8ef0
renamed ProofContext.read_const' to ProofContext.read_const_proper;
wenzelm
parents:
25332
diff
changeset
|
98 |
val expand_abbrevs: Proof.context -> term -> term |
| 20310 | 99 |
val cert_term: Proof.context -> term -> term |
100 |
val cert_prop: Proof.context -> term -> term |
|
|
35616
b342390d296f
provide ProofContext.def_type depending on "pattern" mode;
wenzelm
parents:
35429
diff
changeset
|
101 |
val def_type: Proof.context -> indexname -> typ option |
| 45429 | 102 |
val standard_typ_check: Proof.context -> typ list -> typ list |
103 |
val standard_term_check_finish: Proof.context -> term list -> term list |
|
104 |
val standard_term_uncheck: Proof.context -> term list -> term list |
|
| 20310 | 105 |
val goal_export: Proof.context -> Proof.context -> thm list -> thm list |
106 |
val export: Proof.context -> Proof.context -> thm list -> thm list |
|
| 21531 | 107 |
val export_morphism: Proof.context -> Proof.context -> morphism |
| 28396 | 108 |
val norm_export_morphism: Proof.context -> Proof.context -> morphism |
| 20310 | 109 |
val auto_bind_goal: term list -> Proof.context -> Proof.context |
110 |
val auto_bind_facts: term list -> Proof.context -> Proof.context |
|
| 70728 | 111 |
val simult_matches: Proof.context -> term * term list -> (indexname * term) list |
112 |
val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context |
|
113 |
val bind_term: indexname * term -> Proof.context -> Proof.context |
|
| 60388 | 114 |
val cert_propp: Proof.context -> (term * term list) list list -> |
115 |
(term list list * (indexname * term) list) |
|
116 |
val read_propp: Proof.context -> (string * string list) list list -> |
|
117 |
(term list list * (indexname * term) list) |
|
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54740
diff
changeset
|
118 |
val fact_tac: Proof.context -> thm list -> int -> tactic |
| 20310 | 119 |
val some_fact_tac: Proof.context -> int -> tactic |
| 63255 | 120 |
val lookup_fact: Proof.context -> string -> {dynamic: bool, thms: thm list} option
|
|
62078
76399b8fde4d
more systematic treatment of dynamic facts, when forming closure;
wenzelm
parents:
61902
diff
changeset
|
121 |
val dynamic_facts_dummy: bool Config.T |
|
57942
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57928
diff
changeset
|
122 |
val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list |
|
26346
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
123 |
val get_fact: Proof.context -> Facts.ref -> thm list |
|
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
124 |
val get_fact_single: Proof.context -> Facts.ref -> thm |
|
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
125 |
val get_thms: Proof.context -> xstring -> thm list |
|
17debd2fff8e
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
126 |
val get_thm: Proof.context -> xstring -> thm |
| 67679 | 127 |
val is_stmt: Proof.context -> bool |
| 63083 | 128 |
val set_stmt: bool -> Proof.context -> Proof.context |
129 |
val restore_stmt: Proof.context -> Proof.context -> Proof.context |
|
|
61811
1530a0f19539
added Proof_Context.add_thms_dynamic, which is potentially useful for Eisbach;
wenzelm
parents:
61268
diff
changeset
|
130 |
val add_thms_dynamic: binding * (Context.generic -> thm list) -> |
|
1530a0f19539
added Proof_Context.add_thms_dynamic, which is potentially useful for Eisbach;
wenzelm
parents:
61268
diff
changeset
|
131 |
Proof.context -> string * Proof.context |
|
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67670
diff
changeset
|
132 |
val add_thms_lazy: string -> (binding * thm list lazy) -> Proof.context -> Proof.context |
| 67713 | 133 |
val note_thms: string -> Thm.binding * (thm list * attribute list) list -> |
134 |
Proof.context -> (string * thm list) * Proof.context |
|
|
30761
ac7570d80c3d
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
wenzelm
parents:
30758
diff
changeset
|
135 |
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> |
| 30211 | 136 |
Proof.context -> (string * thm list) list * Proof.context |
|
28082
37350f301128
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28017
diff
changeset
|
137 |
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context |
| 66246 | 138 |
val alias_fact: binding -> string -> Proof.context -> Proof.context |
| 60379 | 139 |
val read_var: binding * string option * mixfix -> Proof.context -> |
140 |
(binding * typ option * mixfix) * Proof.context |
|
141 |
val cert_var: binding * typ option * mixfix -> Proof.context -> |
|
142 |
(binding * typ option * mixfix) * Proof.context |
|
|
30763
6976521b4263
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
wenzelm
parents:
30761
diff
changeset
|
143 |
val add_fixes: (binding * typ option * mixfix) list -> Proof.context -> |
|
6976521b4263
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version; |