author  wenzelm 
Tue, 02 Oct 2007 16:06:41 +0200  
changeset 24812  8c2e8cf22fad 
parent 24778  3e7f71caae18 
child 24922  577ec55380d8 
permissions  rwrr 
5819  1 
(* Title: Pure/Isar/proof_context.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

19001  5 
The key concept of Isar proof contexts: elevates primitive local 
6 
reasoning Gamma  phi to a structured concept, with generic context 

20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

7 
elements. See also structure Variable and Assumption. 
5819  8 
*) 
9 

10 
signature PROOF_CONTEXT = 

11 
sig 

20310  12 
val theory_of: Proof.context > theory 
24812  13 
val tsig_of: Proof.context > Type.tsig 
20310  14 
val init: theory > Proof.context 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

15 
type mode 
24501  16 
val mode_default: mode 
17 
val mode_stmt: mode 

18 
val mode_pattern: mode 

19 
val mode_schematic: mode 

20 
val mode_abbrev: mode 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

21 
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

22 
val get_mode: Proof.context > mode 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

23 
val restore_mode: Proof.context > Proof.context > Proof.context 
21667
ce813b82c88b
add_notation: permissive about undeclared consts;
wenzelm
parents:
21648
diff
changeset

24 
val set_stmt: bool > Proof.context > Proof.context 
ce813b82c88b
add_notation: permissive about undeclared consts;
wenzelm
parents:
21648
diff
changeset

25 
val naming_of: Proof.context > NameSpace.naming 
20310  26 
val full_name: Proof.context > bstring > string 
27 
val consts_of: Proof.context > Consts.T 

21183  28 
val const_syntax_name: Proof.context > string > string 
24752  29 
val the_const_constraint: Proof.context > string > typ 
20784  30 
val set_syntax_mode: Syntax.mode > Proof.context > Proof.context 
20310  31 
val restore_syntax_mode: Proof.context > Proof.context > Proof.context 
22358  32 
val theorems_of: Proof.context > thm list NameSpace.table 
20310  33 
val fact_index_of: Proof.context > FactIndex.T 
34 
val transfer: theory > Proof.context > Proof.context 

20367  35 
val theory: (theory > theory) > Proof.context > Proof.context 
36 
val theory_result: (theory > 'a * theory) > Proof.context > 'a * Proof.context 

20310  37 
val pretty_term: Proof.context > term > Pretty.T 
21728  38 
val pretty_term_abbrev: Proof.context > term > Pretty.T 
20310  39 
val pretty_typ: Proof.context > typ > Pretty.T 
40 
val pretty_sort: Proof.context > sort > Pretty.T 

41 
val pretty_classrel: Proof.context > class list > Pretty.T 

42 
val pretty_arity: Proof.context > arity > Pretty.T 

43 
val pp: Proof.context > Pretty.pp 

22874  44 
val pretty_thm_legacy: thm > Pretty.T 
20310  45 
val pretty_thm: Proof.context > thm > Pretty.T 
46 
val pretty_thms: Proof.context > thm list > Pretty.T 

47 
val pretty_fact: Proof.context > string * thm list > Pretty.T 

48 
val pretty_proof: Proof.context > Proofterm.proof > Pretty.T 

49 
val pretty_proof_of: Proof.context > bool > thm > Pretty.T 

50 
val string_of_typ: Proof.context > typ > string 

51 
val string_of_term: Proof.context > term > string 

52 
val string_of_thm: Proof.context > thm > string 

53 
val read_typ: Proof.context > string > typ 

54 
val read_typ_syntax: Proof.context > string > typ 

55 
val read_typ_abbrev: Proof.context > string > typ 

56 
val cert_typ: Proof.context > typ > typ 

57 
val cert_typ_syntax: Proof.context > typ > typ 

58 
val cert_typ_abbrev: Proof.context > typ > typ 

59 
val get_skolem: Proof.context > string > string 

60 
val revert_skolem: Proof.context > string > string 

61 
val revert_skolems: Proof.context > term > term 

22763  62 
val decode_term: Proof.context > term > term 
24684  63 
val read_term_pattern: Proof.context > string > term 
64 
val read_term_schematic: Proof.context > string > term 

65 
val read_term_abbrev: Proof.context > string > term 

20310  66 
val read_termTs_schematic: Proof.context > (string > bool) > (indexname > typ option) 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

67 
> (indexname > sort option) > string list > (string * typ) list 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

68 
> term list * (indexname * typ) list 
22712  69 
val read_prop_legacy: Proof.context > string > term 
20310  70 
val cert_term: Proof.context > term > term 
71 
val cert_prop: Proof.context > term > term 

72 
val infer_type: Proof.context > string > typ 

73 
val inferred_param: string > Proof.context > (string * typ) * Proof.context 

74 
val inferred_fixes: Proof.context > (string * typ) list * Proof.context 

75 
val read_tyname: Proof.context > string > typ 

76 
val read_const: Proof.context > string > term 

77 
val goal_export: Proof.context > Proof.context > thm list > thm list 

78 
val export: Proof.context > Proof.context > thm list > thm list 

21531  79 
val export_morphism: Proof.context > Proof.context > morphism 
20310  80 
val add_binds: (indexname * string option) list > Proof.context > Proof.context 
81 
val add_binds_i: (indexname * term option) list > Proof.context > Proof.context 

82 
val auto_bind_goal: term list > Proof.context > Proof.context 

83 
val auto_bind_facts: term list > Proof.context > Proof.context 

84 
val match_bind: bool > (string list * string) list > Proof.context > term list * Proof.context 

85 
val match_bind_i: bool > (term list * term) list > Proof.context > term list * Proof.context 

86 
val read_propp: Proof.context * (string * string list) list list 

87 
> Proof.context * (term * term list) list list 

88 
val cert_propp: Proof.context * (term * term list) list list 

89 
> Proof.context * (term * term list) list list 

90 
val read_propp_schematic: Proof.context * (string * string list) list list 

91 
> Proof.context * (term * term list) list list 

92 
val cert_propp_schematic: Proof.context * (term * term list) list list 

93 
> Proof.context * (term * term list) list list 

94 
val bind_propp: Proof.context * (string * string list) list list 

95 
> Proof.context * (term list list * (Proof.context > Proof.context)) 

96 
val bind_propp_i: Proof.context * (term * term list) list list 

97 
> Proof.context * (term list list * (Proof.context > Proof.context)) 

98 
val bind_propp_schematic: Proof.context * (string * string list) list list 

99 
> Proof.context * (term list list * (Proof.context > Proof.context)) 

100 
val bind_propp_schematic_i: Proof.context * (term * term list) list list 

101 
> Proof.context * (term list list * (Proof.context > Proof.context)) 

18042  102 
val fact_tac: thm list > int > tactic 
20310  103 
val some_fact_tac: Proof.context > int > tactic 
104 
val get_thm: Proof.context > thmref > thm 

105 
val get_thm_closure: Proof.context > thmref > thm 

106 
val get_thms: Proof.context > thmref > thm list 

107 
val get_thms_closure: Proof.context > thmref > thm list 

108 
val valid_thms: Proof.context > string * thm list > bool 

109 
val lthms_containing: Proof.context > FactIndex.spec > (string * thm list) list 

22352  110 
val add_path: string > Proof.context > Proof.context 
20310  111 
val no_base_names: Proof.context > Proof.context 
112 
val qualified_names: Proof.context > Proof.context 

113 
val sticky_prefix: string > Proof.context > Proof.context 

114 
val restore_naming: Proof.context > Proof.context > Proof.context 

21728  115 
val reset_naming: Proof.context > Proof.context 
20310  116 
val hide_thms: bool > string list > Proof.context > Proof.context 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

117 
val put_thms: string * thm list option > Proof.context > Proof.context 
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

118 
val note_thmss: string > 
18728  119 
((bstring * attribute list) * (thmref * attribute list) list) list > 
20310  120 
Proof.context > (bstring * thm list) list * Proof.context 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

121 
val note_thmss_i: string > 
18728  122 
((bstring * attribute list) * (thm list * attribute list) list) list > 
20310  123 
Proof.context > (bstring * thm list) list * Proof.context 
124 
val read_vars: (string * string option * mixfix) list > Proof.context > 

125 
(string * typ option * mixfix) list * Proof.context 

126 
val cert_vars: (string * typ option * mixfix) list > Proof.context > 

127 
(string * typ option * mixfix) list * Proof.context 

128 
val read_vars_legacy: (string * string option * mixfix) list > Proof.context > 

129 
(string * typ option * mixfix) list * Proof.context 

130 
val cert_vars_legacy: (string * typ option * mixfix) list > Proof.context > 

131 
(string * typ option * mixfix) list * Proof.context 

132 
val add_fixes: (string * string option * mixfix) list > 

133 
Proof.context > string list * Proof.context 

134 
val add_fixes_i: (string * typ option * mixfix) list > 

135 
Proof.context > string list * Proof.context 

136 
val add_fixes_legacy: (string * typ option * mixfix) list > 

137 
Proof.context > string list * Proof.context 

138 
val auto_fixes: Proof.context * (term list list * 'a) > Proof.context * (term list list * 'a) 

139 
val bind_fixes: string list > Proof.context > (term > term) * Proof.context 

20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

140 
val add_assms: Assumption.export > 
19585  141 
((string * attribute list) * (string * string list) list) list > 
20310  142 
Proof.context > (bstring * thm list) list * Proof.context 
20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

143 
val add_assms_i: Assumption.export > 
19585  144 
((string * attribute list) * (term * term list) list) list > 
20310  145 
Proof.context > (bstring * thm list) list * Proof.context 
146 
val add_cases: bool > (string * RuleCases.T option) list > Proof.context > Proof.context 

147 
val apply_case: RuleCases.T > Proof.context > (string * term list) list * Proof.context 

148 
val get_case: Proof.context > string > string option list > RuleCases.T 

21208
62ccdaf9369a
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

149 
val add_notation: Syntax.mode > (term * mixfix) list > 
62ccdaf9369a
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

150 
Proof.context > Proof.context 
21744  151 
val target_notation: Syntax.mode > (term * mixfix) list > morphism > 
152 
Context.generic > Context.generic 

24767  153 
val add_const_constraint: string * typ option > Proof.context > Proof.context 
24778  154 
val add_abbrev: string > Markup.property list > 
155 
bstring * term > Proof.context > (term * term) * Proof.context 

10810  156 
val verbose: bool ref 
157 
val setmp_verbose: ('a > 'b) > 'a > 'b 

20310  158 
val print_syntax: Proof.context > unit 
21728  159 
val print_abbrevs: Proof.context > unit 
20310  160 
val print_binds: Proof.context > unit 
161 
val print_lthms: Proof.context > unit 

162 
val print_cases: Proof.context > unit 

163 
val debug: bool ref 

10810  164 
val prems_limit: int ref 
20310  165 
val pretty_ctxt: Proof.context > Pretty.T list 
166 
val pretty_context: Proof.context > Pretty.T list 

5819  167 
end; 
168 

16540  169 
structure ProofContext: PROOF_CONTEXT = 
5819  170 
struct 
171 

16540  172 
val theory_of = Context.theory_of_proof; 
19001  173 
val tsig_of = Sign.tsig_of o theory_of; 
174 

16540  175 
val init = Context.init_proof; 
12057  176 

7270  177 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

178 
(** inner syntax mode **) 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

179 

cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

180 
datatype mode = 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

181 
Mode of 
24486  182 
{stmt: bool, (*inner statement mode*) 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

183 
pattern: bool, (*pattern binding schematic variables*) 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

184 
schematic: bool, (*term referencing loose schematic variables*) 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

185 
abbrev: bool}; (*abbrev mode  no normalization*) 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

186 

24486  187 
fun make_mode (stmt, pattern, schematic, abbrev) = 
188 
Mode {stmt = stmt, pattern = pattern, schematic = schematic, abbrev = abbrev}; 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

189 

24486  190 
val mode_default = make_mode (false, false, false, false); 
191 
val mode_stmt = make_mode (true, false, false, false); 

192 
val mode_pattern = make_mode (false, true, false, false); 

193 
val mode_schematic = make_mode (false, false, true, false); 

194 
val mode_abbrev = make_mode (false, false, false, true); 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

195 

cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

196 

5819  197 

16540  198 
(** Isar proof context information **) 
5819  199 

16540  200 
datatype ctxt = 
201 
Ctxt of 

24675
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

202 
{mode: mode, (*inner syntax mode*) 
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

203 
naming: NameSpace.naming, (*local naming conventions*) 
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

204 
syntax: LocalSyntax.T, (*local syntax*) 
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

205 
consts: Consts.T * Consts.T, (*global/local consts*) 
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

206 
thms: thm list NameSpace.table * FactIndex.T, (*local thms*) 
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

207 
cases: (string * (RuleCases.T * bool)) list}; (*local contexts*) 
5819  208 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

209 
fun make_ctxt (mode, naming, syntax, consts, thms, cases) = 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

210 
Ctxt {mode = mode, naming = naming, syntax = syntax, 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

211 
consts = consts, thms = thms, cases = cases}; 
5819  212 

19079
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

213 
val local_naming = NameSpace.default_naming > NameSpace.add_path "local"; 
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

214 

16540  215 
structure ContextData = ProofDataFun 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

216 
( 
16540  217 
type T = ctxt; 
218 
fun init thy = 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

219 
make_ctxt (mode_default, local_naming, LocalSyntax.init thy, 
20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

220 
(Sign.consts_of thy, Sign.consts_of thy), 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

221 
(NameSpace.empty_table, FactIndex.empty), []); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

222 
); 
5819  223 

16540  224 
fun rep_context ctxt = ContextData.get ctxt > (fn Ctxt args => args); 
5819  225 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

226 
fun map_context f = 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

227 
ContextData.map (fn Ctxt {mode, naming, syntax, consts, thms, cases} => 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

228 
make_ctxt (f (mode, naming, syntax, consts, thms, cases))); 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

229 

cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

230 
fun set_mode mode = map_context (fn (_, naming, syntax, consts, thms, cases) => 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

231 
(mode, naming, syntax, consts, thms, cases)); 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

232 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

233 
fun map_mode f = 
24486  234 
map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, consts, thms, cases) => 
235 
(make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, consts, thms, cases)); 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

236 

19001  237 
fun map_naming f = 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

238 
map_context (fn (mode, naming, syntax, consts, thms, cases) => 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

239 
(mode, f naming, syntax, consts, thms, cases)); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

240 

19001  241 
fun map_syntax f = 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

242 
map_context (fn (mode, naming, syntax, consts, thms, cases) => 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

243 
(mode, naming, f syntax, consts, thms, cases)); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

244 

19001  245 
fun map_consts f = 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

246 
map_context (fn (mode, naming, syntax, consts, thms, cases) => 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

247 
(mode, naming, syntax, f consts, thms, cases)); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

248 

19001  249 
fun map_thms f = 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

250 
map_context (fn (mode, naming, syntax, consts, thms, cases) => 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

251 
(mode, naming, syntax, consts, f thms, cases)); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

252 

19001  253 
fun map_cases f = 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

254 
map_context (fn (mode, naming, syntax, consts, thms, cases) => 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

255 
(mode, naming, syntax, consts, thms, f cases)); 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

256 

cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

257 
val get_mode = #mode o rep_context; 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

258 
fun restore_mode ctxt = set_mode (get_mode ctxt); 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

259 

24486  260 
fun set_stmt stmt = 
261 
map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev)); 

19001  262 

263 
val naming_of = #naming o rep_context; 

19387  264 
val full_name = NameSpace.full o naming_of; 
5819  265 

16540  266 
val syntax_of = #syntax o rep_context; 
19001  267 
val syn_of = LocalSyntax.syn_of o syntax_of; 
19543  268 
val set_syntax_mode = map_syntax o LocalSyntax.set_mode; 
269 
val restore_syntax_mode = map_syntax o LocalSyntax.restore_mode o syntax_of; 

19001  270 

19033
24e251657e56
consts: maintain thy version for efficient transfer;
wenzelm
parents:
19019
diff
changeset

271 
val consts_of = #2 o #consts o rep_context; 
21183  272 
val const_syntax_name = Consts.syntax_name o consts_of; 
24752  273 
val the_const_constraint = Consts.the_constraint o consts_of; 
5819  274 

16540  275 
val thms_of = #thms o rep_context; 
22358  276 
val theorems_of = #1 o thms_of; 
19001  277 
val fact_index_of = #2 o thms_of; 
16540  278 

279 
val cases_of = #cases o rep_context; 

5819  280 

281 

20367  282 
(* theory transfer *) 
12093  283 

19001  284 
fun transfer_syntax thy = 
285 
map_syntax (LocalSyntax.rebuild thy) #> 

19033
24e251657e56
consts: maintain thy version for efficient transfer;
wenzelm
parents:
19019
diff
changeset

286 
map_consts (fn consts as (global_consts, local_consts) => 
24e251657e56
consts: maintain thy version for efficient transfer;
wenzelm
parents:
19019
diff
changeset

287 
let val thy_consts = Sign.consts_of thy in 
24e251657e56
consts: maintain thy version for efficient transfer;
wenzelm
parents:
19019
diff
changeset

288 
if Consts.eq_consts (thy_consts, global_consts) then consts 
24e251657e56
consts: maintain thy version for efficient transfer;
wenzelm
parents:
19019
diff
changeset

289 
else (thy_consts, Consts.merge (thy_consts, local_consts)) 
24e251657e56
consts: maintain thy version for efficient transfer;
wenzelm
parents:
19019
diff
changeset

290 
end); 
17072  291 

19001  292 
fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy; 
17072  293 

20367  294 
fun theory f ctxt = transfer (f (theory_of ctxt)) ctxt; 
295 

296 
fun theory_result f ctxt = 

297 
let val (res, thy') = f (theory_of ctxt) 

298 
in (res, ctxt > transfer thy') end; 

19019  299 

12093  300 

301 

14828  302 
(** pretty printing **) 
303 

19310  304 
local 
305 

24675
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

306 
fun rewrite_term thy rews t = 
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

307 
if can Term.type_of t then Pattern.rewrite_term thy rews [] t else t; 
19371  308 

19001  309 
fun pretty_term' abbrevs ctxt t = 
18971  310 
let 
19001  311 
val thy = theory_of ctxt; 
312 
val syntax = syntax_of ctxt; 

18971  313 
val consts = consts_of ctxt; 
22587  314 
val do_abbrevs = abbrevs andalso not (print_mode_active "no_abbrevs"); 
19001  315 
val t' = t 
24675
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

316 
> do_abbrevs ? rewrite_term thy (Consts.abbrevs_of consts (print_mode_value () @ [""])) 
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

317 
> do_abbrevs ? rewrite_term thy (Consts.abbrevs_of consts [Syntax.internalM]) 
19371  318 
> Sign.extern_term (Consts.extern_early consts) thy 
319 
> LocalSyntax.extern_term syntax; 

21772  320 
in Sign.pretty_term' ctxt (LocalSyntax.syn_of syntax) (Consts.extern consts) t' end; 
18971  321 

19310  322 
in 
323 

19001  324 
val pretty_term = pretty_term' true; 
21728  325 
val pretty_term_abbrev = pretty_term' false; 
19310  326 

327 
end; 

328 

16458  329 
fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T; 
330 
fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S; 

331 
fun pretty_classrel ctxt cs = Sign.pretty_classrel (theory_of ctxt) cs; 

332 
fun pretty_arity ctxt ar = Sign.pretty_arity (theory_of ctxt) ar; 

14828  333 

14974
b1ecb7859c99
avoid premature evaluation of syn_of (wastes time in conjunction with pp);
wenzelm
parents:
14901
diff
changeset

334 
fun pp ctxt = Pretty.pp (pretty_term ctxt, pretty_typ ctxt, pretty_sort ctxt, 
b1ecb7859c99
avoid premature evaluation of syn_of (wastes time in conjunction with pp);
wenzelm
parents:
14901
diff
changeset

335 
pretty_classrel ctxt, pretty_arity ctxt); 
14828  336 

22874  337 
fun pretty_thm_legacy th = 
338 
let val thy = Thm.theory_of_thm th 

339 
in Display.pretty_thm_aux (pp (init thy)) true false [] th end; 

20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

340 

17451  341 
fun pretty_thm ctxt th = 
22874  342 
let val asms = map Thm.term_of (Assumption.assms_of ctxt) 
343 
in Display.pretty_thm_aux (pp ctxt) false true asms th end; 

14828  344 

345 
fun pretty_thms ctxt [th] = pretty_thm ctxt th 

346 
 pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths)); 

347 

348 
fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths 

349 
 pretty_fact ctxt (a, [th]) = 

350 
Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th] 

351 
 pretty_fact ctxt (a, ths) = 

352 
Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths)); 

353 

17072  354 
fun pretty_proof ctxt prf = 
21728  355 
pretty_term_abbrev (ctxt > transfer_syntax (ProofSyntax.proof_syntax prf (theory_of ctxt))) 
17072  356 
(ProofSyntax.term_of_proof prf); 
357 

358 
fun pretty_proof_of ctxt full th = 

359 
pretty_proof ctxt (ProofSyntax.proof_of full th); 

360 

17860
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

361 
val string_of_typ = Pretty.string_of oo pretty_typ; 
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

362 
val string_of_term = Pretty.string_of oo pretty_term; 
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

363 
val string_of_thm = Pretty.string_of oo pretty_thm; 
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

364 

14828  365 

366 

5819  367 
(** prepare types **) 
368 

24277  369 
(* read_typ *) 
370 

371 
fun read_typ_mode mode ctxt s = 

24486  372 
Syntax.read_typ (Type.set_mode mode ctxt) s; 
24277  373 

374 
val read_typ = read_typ_mode Type.mode_default; 

375 
val read_typ_syntax = read_typ_mode Type.mode_syntax; 

376 
val read_typ_abbrev = read_typ_mode Type.mode_abbrev; 

377 

378 

379 
(* cert_typ *) 

380 

381 
fun cert_typ_mode mode ctxt T = 

382 
Sign.certify_typ_mode mode (theory_of ctxt) T 

383 
handle TYPE (msg, _, _) => error msg; 

384 

385 
val cert_typ = cert_typ_mode Type.mode_default; 

386 
val cert_typ_syntax = cert_typ_mode Type.mode_syntax; 

387 
val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev; 

388 

389 

24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

390 

cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

391 
(** prepare variables **) 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

392 

7679  393 
(* internalize Skolem constants *) 
394 

19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

395 
val lookup_skolem = AList.lookup (op =) o Variable.fixes_of; 
18187  396 
fun get_skolem ctxt x = the_default x (lookup_skolem ctxt x); 
7679  397 

18678  398 
fun no_skolem internal x = 
20086
94ca946fb689
adapted to more efficient Name/Variable implementation;
wenzelm
parents:
20049
diff
changeset

399 
if can Name.dest_skolem x then 
18678  400 
error ("Illegal reference to internal Skolem constant: " ^ quote x) 
20086
94ca946fb689
adapted to more efficient Name/Variable implementation;
wenzelm
parents:
20049
diff
changeset

401 
else if not internal andalso can Name.dest_internal x then 
18678  402 
error ("Illegal reference to internal variable: " ^ quote x) 
7679  403 
else x; 
404 

405 

20244
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

406 
(* revert Skolem constants  approximation only! *) 
18255  407 

20244
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

408 
fun revert_skolem ctxt = 
9133  409 
let 
20244
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

410 
val rev_fixes = map Library.swap (Variable.fixes_of ctxt); 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

411 
val revert = AList.lookup (op =) rev_fixes; 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

412 
in 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

413 
fn x => 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

414 
(case revert x of 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

415 
SOME x' => x' 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

416 
 NONE => perhaps (try Name.dest_skolem) x) 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

417 
end; 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

418 

89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

419 
fun revert_skolems ctxt = 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

420 
let 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

421 
val revert = revert_skolem ctxt; 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

422 
fun reverts (Free (x, T)) = Free (revert x, T) 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

423 
 reverts (t $ u) = reverts t $ reverts u 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

424 
 reverts (Abs (x, T, t)) = Abs (x, T, reverts t) 
89a407400874
replaced extern_skolem by slightly more simplistic revert_skolems;
wenzelm
parents:
20234
diff
changeset

425 
 reverts a = a; 
24495  426 
in reverts end; 
9133  427 

8096  428 

18187  429 

5819  430 
(** prepare terms and propositions **) 
431 

24684  432 
(* read_term *) 
433 

434 
fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt); 

435 

436 
val read_term_pattern = read_term_mode mode_pattern; 

437 
val read_term_schematic = read_term_mode mode_schematic; 

438 
val read_term_abbrev = read_term_mode mode_abbrev; 

439 

440 

19001  441 
(* local abbreviations *) 
5819  442 

24501  443 
local 
444 

19371  445 
fun certify_consts ctxt = 
24675
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

446 
let val Mode {abbrev, ...} = get_mode ctxt 
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

447 
in Consts.certify (pp ctxt) (tsig_of ctxt) (not abbrev) (consts_of ctxt) end; 
19001  448 

19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

449 
fun reject_schematic (Var (xi, _)) = 
22678  450 
error ("Unbound schematic variable: " ^ Term.string_of_vname xi) 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

451 
 reject_schematic (Abs (_, _, t)) = reject_schematic t 
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

452 
 reject_schematic (t $ u) = (reject_schematic t; reject_schematic u) 
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

453 
 reject_schematic _ = (); 
5819  454 

24495  455 
fun expand_binds ctxt = 
456 
let val Mode {pattern, schematic, ...} = get_mode ctxt in 

457 
if pattern then I 

458 
else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic) 

459 
end; 

5819  460 

24501  461 
in 
462 

463 
fun expand_abbrevs ctxt = certify_consts ctxt #> expand_binds ctxt; 

464 

465 
end; 

466 

5819  467 

24518  468 
(* patterns *) 
469 

470 
fun prepare_patternT ctxt = 

471 
let val Mode {pattern, schematic, ...} = get_mode ctxt in 

472 
if pattern orelse schematic then I 

473 
else Term.map_atyps 

474 
(fn T as TVar (xi, _) => 

475 
if not (TypeInfer.is_param xi) 

476 
then error ("Illegal schematic type variable: " ^ Term.string_of_vname xi) 

477 
else T 

478 
 T => T) 

479 
end; 

480 

22712  481 

24505  482 
local 
6550  483 

24767  484 
fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1); 
6762  485 

18678  486 
fun reject_dummies t = Term.no_dummy_patterns t 
487 
handle TERM _ => error "Illegal dummy pattern(s) in term"; 

6550  488 

24505  489 
in 
490 

24684  491 
fun prepare_patterns ctxt = 
24518  492 
let val Mode {pattern, ...} = get_mode ctxt in 
24767  493 
TypeInfer.fixate_params (Variable.names_of ctxt) #> 
494 
pattern ? Variable.polymorphic ctxt #> 

24684  495 
(map o Term.map_types) (prepare_patternT ctxt) #> 
24767  496 
(if pattern then prepare_dummies else map reject_dummies) 
24505  497 
end; 
498 

499 
end; 

500 

6550  501 

22763  502 
(* decoding raw terms (syntax trees) *) 
503 

504 
fun legacy_intern_skolem ctxt internal def_type x = (* FIXME cleanup this mess *) 

505 
let 

506 
val sko = lookup_skolem ctxt x; 

507 
val is_const = can (Consts.read_const (consts_of ctxt)) x; 

508 
val is_free = is_some sko orelse not is_const; 

509 
val is_internal = internal x; 

510 
val is_declared = is_some (def_type (x, ~1)); 

511 
val res = 

512 
if is_free andalso not is_internal then (no_skolem false x; sko) 

23361  513 
else ((no_skolem false x; ()) handle ERROR msg => 
514 
legacy_feature (msg ^ ContextPosition.str_of ctxt); 

22763  515 
if is_internal andalso is_declared then SOME x else NONE); 
516 
in if is_some res then res else if is_declared then SOME x else NONE end; 

517 

24371  518 
fun term_context ctxt = 
519 
let val thy = theory_of ctxt in 

520 
{get_sort = Sign.get_sort thy (Variable.def_sort ctxt), 

521 
map_const = try (#1 o Term.dest_Const o Consts.read_const (consts_of ctxt)), 

522 
map_free = legacy_intern_skolem ctxt (K false) (Variable.def_type ctxt false), 

523 
map_type = Sign.intern_tycons thy, 

524 
map_sort = Sign.intern_sort thy} 

525 
end; 

526 

22763  527 
fun decode_term ctxt = 
24371  528 
let val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt 
22763  529 
in Syntax.decode_term get_sort map_const map_free map_type map_sort end; 
530 

531 

24687  532 
(* read terms  legacy *) 
5819  533 

10554  534 
local 
535 

24687  536 
fun read_def_termTs freeze pp syn ctxt (types, sorts, used) fixed sTs = 
537 
Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn (consts_of ctxt) fixed 

538 
ctxt (types, sorts) used freeze sTs; 

539 

540 
fun read_def_termT freeze pp syn ctxt defaults fixed sT = 

541 
apfst hd (read_def_termTs freeze pp syn ctxt defaults fixed [sT]); 

542 

543 
fun read_prop_thy freeze pp syn thy defaults fixed s = 

544 
#1 (read_def_termT freeze pp syn thy defaults fixed (s, propT)); 

545 

15531  546 
fun append_env e1 e2 x = (case e2 x of NONE => e1 x  some => some); 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

547 

24687  548 
fun gen_read' read app schematic ctxt0 internal more_types more_sorts more_used s = 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13629
diff
changeset

549 
let 
24687  550 
val ctxt = if schematic then set_mode mode_schematic ctxt0 else ctxt0; 
551 
val types = append_env (Variable.def_type ctxt false) more_types; 

19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

552 
val sorts = append_env (Variable.def_sort ctxt) more_sorts; 
20163  553 
val used = fold Name.declare more_used (Variable.names_of ctxt); 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13629
diff
changeset

554 
in 
22763  555 
(read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) 
556 
(legacy_intern_skolem ctxt internal types) s 

18678  557 
handle TERM (msg, _) => error msg) 
24505  558 
> app (expand_abbrevs ctxt) 
24684  559 
> app (singleton (prepare_patterns ctxt)) 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

560 
end; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

561 

24687  562 
fun gen_read read app schematic ctxt = 
563 
gen_read' read app schematic ctxt (K false) (K NONE) (K NONE) []; 

14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

564 

10554  565 
in 
566 

24687  567 
val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) true; 
8096  568 

22712  569 
fun read_prop_legacy ctxt = 
24687  570 
gen_read' (read_prop_thy true) I false ctxt (K true) (K NONE) (K NONE) []; 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

571 

10554  572 
end; 
573 

5819  574 

575 
(* certify terms *) 

576 

10554  577 
local 
578 

24684  579 
fun gen_cert prop ctxt t = 
580 
t 

581 
> expand_abbrevs ctxt 

582 
> (fn t' => #1 (Sign.certify' prop (pp ctxt) false (consts_of ctxt) (theory_of ctxt) t') 

583 
handle TYPE (msg, _, _) => error msg 

584 
 TERM (msg, _) => error msg); 

16501  585 

10554  586 
in 
8096  587 

24684  588 
val cert_term = gen_cert false; 
589 
val cert_prop = gen_cert true; 

10554  590 

591 
end; 

5819  592 

593 

24495  594 
(* type checking/inference *) 
22701  595 

24495  596 
fun standard_infer_types ctxt ts = 
597 
let val Mode {pattern, ...} = get_mode ctxt in 

598 
TypeInfer.infer_types (pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt) 

599 
(try (Consts.the_constraint (consts_of ctxt))) (Variable.def_type ctxt pattern) 

24767  600 
(Variable.names_of ctxt) (Variable.maxidx_of ctxt) NONE (map (rpair dummyT) ts) 
24495  601 
> #1 > map #1 
602 
handle TYPE (msg, _, _) => error msg 

603 
end; 

24486  604 

24518  605 
local 
606 

607 
fun standard_typ_check ctxt = 

608 
map (cert_typ_mode (Type.get_mode ctxt) ctxt) #> 

609 
map (prepare_patternT ctxt); 

610 

24769
1372969969e0
standard_term_check: include expand_abbrevs (back again);
wenzelm
parents:
24767
diff
changeset

611 
fun standard_term_check ctxt = 
1372969969e0
standard_term_check: include expand_abbrevs (back again);
wenzelm
parents:
24767
diff
changeset

612 
standard_infer_types ctxt #> 
1372969969e0
standard_term_check: include expand_abbrevs (back again);
wenzelm
parents:
24767
diff
changeset

613 
map (expand_abbrevs ctxt); 
1372969969e0
standard_term_check: include expand_abbrevs (back again);
wenzelm
parents:
24767
diff
changeset

614 

24767  615 
fun add_check add f = Context.add_setup 
616 
(Context.theory_map (add (fn xs => fn ctxt => (f ctxt xs, ctxt)))); 

617 

24518  618 
in 
619 

24769
1372969969e0
standard_term_check: include expand_abbrevs (back again);
wenzelm
parents:
24767
diff
changeset

620 
val _ = add_check (Syntax.add_typ_check 0 "standard") standard_typ_check; 
1372969969e0
standard_term_check: include expand_abbrevs (back again);
wenzelm
parents:
24767
diff
changeset

621 
val _ = add_check (Syntax.add_term_check 0 "standard") standard_term_check; 
24767  622 
val _ = add_check (Syntax.add_term_check 100 "fixate") prepare_patterns; 
22701  623 

24518  624 
end; 
22701  625 

626 

18770  627 
(* inferred types of parameters *) 
628 

629 
fun infer_type ctxt x = 

24505  630 
Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) 
631 
(Free (x, dummyT))); 

18770  632 

633 
fun inferred_param x ctxt = 

18619  634 
let val T = infer_type ctxt x 
20163  635 
in ((x, T), ctxt > Variable.declare_term (Free (x, T))) end; 
18619  636 

18770  637 
fun inferred_fixes ctxt = 
20086
94ca946fb689
adapted to more efficient Name/Variable implementation;
wenzelm
parents:
20049
diff
changeset

638 
fold_map inferred_param (rev (map #2 (Variable.fixes_of ctxt))) ctxt; 
5819  639 

640 

15703  641 
(* type and constant names *) 
642 

643 
fun read_tyname ctxt c = 

20163  644 
if Syntax.is_tid c then 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

645 
TFree (c, the_default (Sign.defaultS (theory_of ctxt)) (Variable.def_sort ctxt (c, ~1))) 
16458  646 
else Sign.read_tyname (theory_of ctxt) c; 
15703  647 

648 
fun read_const ctxt c = 

649 
(case lookup_skolem ctxt c of 

21208
62ccdaf9369a
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

650 
SOME x => Free (x, infer_type ctxt x) 
18971  651 
 NONE => Consts.read_const (consts_of ctxt) c); 
15703  652 

653 

9553  654 

24767  655 
(** inner syntax operations **) 
24371  656 

657 
local 

658 

659 
fun parse_sort ctxt str = 

660 
Syntax.standard_parse_sort ctxt (syn_of ctxt) (Sign.intern_sort (theory_of ctxt)) str; 

661 

662 
fun parse_typ ctxt str = 

663 
let 

664 
val thy = ProofContext.theory_of ctxt; 

665 
val get_sort = Sign.get_sort thy (Variable.def_sort ctxt); 

666 
val T = Sign.intern_tycons thy 

667 
(Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) str); 

668 
in T end 

669 
handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str); 

670 

671 
fun parse_term T ctxt str = 

672 
let 

673 
val thy = theory_of ctxt; 

24684  674 
val infer = singleton (standard_infer_types (Type.set_mode Type.mode_default ctxt)) o 
675 
TypeInfer.constrain T; 

24371  676 
fun check t = Exn.Result (infer t) handle ERROR msg => Exn.Exn (ERROR msg); 
677 
val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt; 

24511
69d270cc7e4f
removed obsolete read/cert variations (cf. Syntax.read/check);
wenzelm
parents:
24505
diff
changeset

678 
val read = Syntax.standard_parse_term (pp ctxt) check get_sort map_const map_free map_type 
69d270cc7e4f
removed obsolete read/cert variations (cf. Syntax.read/check);
wenzelm
parents:
24505
diff
changeset

679 
map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) ((#1 (TypeInfer.paramify_dummies T 0))); 
24371  680 
in read str end; 
681 

682 
in 

683 

24767  684 
val _ = Syntax.install_operations 
685 
{parse_sort = parse_sort, 

686 
parse_typ = parse_typ, 

687 
parse_term = parse_term dummyT, 

688 
parse_prop = parse_term propT, 

689 
unparse_sort = undefined, 

690 
unparse_typ = undefined, 

691 
unparse_term = undefined}; 

24371  692 

693 
end; 

694 

695 

696 

21610  697 
(** export results **) 
21531  698 

20310  699 
fun common_export is_goal inner outer = 
700 
map (Assumption.export is_goal inner outer) #> 

701 
Variable.export inner outer; 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

702 

20310  703 
val goal_export = common_export true; 
704 
val export = common_export false; 

12704  705 

21531  706 
fun export_morphism inner outer = 
707 
Assumption.export_morphism inner outer $> 

708 
Variable.export_morphism inner outer; 

709 

710 

15758
07e382399a96
binds/thms: do not store options, but delete from table;
wenzelm
parents:
15750
diff
changeset

711 

5819  712 
(** bindings **) 
713 

8096  714 
(* simult_matches *) 
715 

19867  716 
fun simult_matches ctxt (t, pats) = 
717 
(case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of 

718 
NONE => error "Pattern match failed!" 

719 
 SOME (env, _) => map (apsnd snd) (Envir.alist_of env)); 

8096  720 

721 

722 
(* add_binds(_i) *) 

5819  723 

7925  724 
local 
725 

16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

726 
fun gen_bind prep (xi as (x, _), raw_t) ctxt = 
24511
69d270cc7e4f
removed obsolete read/cert variations (cf. Syntax.read/check);
wenzelm
parents:
24505
diff
changeset

727 
ctxt 
24675
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

728 
> Variable.add_binds [(xi, Option.map (prep (set_mode mode_default ctxt)) raw_t)]; 
5819  729 

10810  730 
in 
731 

20330  732 
fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b 
10554  733 
 drop_schematic b = b; 
734 

24511
69d270cc7e4f
removed obsolete read/cert variations (cf. Syntax.read/check);
wenzelm
parents:
24505
diff
changeset

735 
val add_binds = fold (gen_bind Syntax.read_term); 
16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

736 
val add_binds_i = fold (gen_bind cert_term); 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

737 

16458  738 
fun auto_bind f ts ctxt = ctxt > add_binds_i (map drop_schematic (f (theory_of ctxt) ts)); 
12147  739 
val auto_bind_goal = auto_bind AutoBind.goal; 
740 
val auto_bind_facts = auto_bind AutoBind.facts; 

7925  741 

742 
end; 

5819  743 

744 

8096  745 
(* match_bind(_i) *) 
5819  746 

8096  747 
local 
748 

24684  749 
fun gen_bind prep_terms gen raw_binds ctxt = 
5819  750 
let 
24684  751 
fun prep_bind (raw_pats, t) ctxt1 = 
752 
let 

753 
val T = Term.fastype_of t; 

754 
val ctxt2 = Variable.declare_term t ctxt1; 

755 
val pats = prep_terms (set_mode mode_pattern ctxt2) T raw_pats; 

756 
val binds = simult_matches ctxt2 (t, pats); 

757 
in (binds, ctxt2) end; 

7670  758 

24686  759 
val ts = prep_terms ctxt dummyT (map snd raw_binds); 
760 
val (binds, ctxt') = apfst flat (fold_map prep_bind (map fst raw_binds ~~ ts) ctxt); 

8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

761 
val binds' = 
19916
3bbb9cc5d4f1
export: simultaneous facts, refer to Variable.export;
wenzelm
parents:
19897
diff
changeset

762 
if gen then map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds) 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

763 
else binds; 
15531  764 
val binds'' = map (apsnd SOME) binds'; 
18310  765 
val ctxt'' = 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

766 
tap (Variable.warn_extra_tfrees ctxt) 
18310  767 
(if gen then 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

768 
ctxt (*sic!*) > fold Variable.declare_term (map #2 binds') > add_binds_i binds'' 
18310  769 
else ctxt' > add_binds_i binds''); 
770 
in (ts, ctxt'') end; 

8096  771 

772 
in 

5935  773 

24684  774 
fun read_terms ctxt T = 
775 
map (Syntax.parse_term ctxt #> TypeInfer.constrain T) #> Syntax.check_terms ctxt; 

776 

777 
val match_bind = gen_bind read_terms; 

778 
val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt)); 

8096  779 

780 
end; 

5935  781 

782 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

783 
(* propositions with patterns *) 
5935  784 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

785 
local 
8096  786 

24684  787 
fun prep_propp mode prep_props (context, args) = 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

788 
let 
19585  789 
fun prep (_, raw_pats) (ctxt, prop :: props) = 
24684  790 
let val ctxt' = Variable.declare_term prop ctxt 
791 
in ((prop, prep_props (set_mode mode_pattern ctxt') raw_pats), (ctxt', props)) end; 

792 

17860
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

793 
val (propp, (context', _)) = (fold_map o fold_map) prep args 
24684  794 
(context, prep_props (set_mode mode context) (maps (map fst) args)); 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

795 
in (context', propp) end; 
5935  796 

24684  797 
fun gen_bind_propp mode parse_prop (ctxt, raw_args) = 
8096  798 
let 
24684  799 
val (ctxt', args) = prep_propp mode parse_prop (ctxt, raw_args); 
19585  800 
val binds = flat (flat (map (map (simult_matches ctxt')) args)); 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

801 
val propss = map (map #1) args; 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

802 

10554  803 
(*generalize result: context evaluated now, binds added later*) 
19916
3bbb9cc5d4f1
export: simultaneous facts, refer to Variable.export;
wenzelm
parents:
19897
diff
changeset

804 
val gen = Variable.exportT_terms ctxt' ctxt; 
15531  805 
fun gen_binds c = c > add_binds_i (map #1 binds ~~ map SOME (gen (map #2 binds))); 
806 
in (ctxt' > add_binds_i (map (apsnd SOME) binds), (propss, gen_binds)) end; 

8096  807 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

808 
in 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

809 

24684  810 
val read_propp = prep_propp mode_default Syntax.read_props; 
811 
val cert_propp = prep_propp mode_default (map o cert_prop); 

812 
val read_propp_schematic = prep_propp mode_schematic Syntax.read_props; 

813 
val cert_propp_schematic = prep_propp mode_schematic (map o cert_prop); 

10554  814 

24684  815 
val bind_propp = gen_bind_propp mode_default Syntax.read_props; 
816 
val bind_propp_i = gen_bind_propp mode_default (map o cert_prop); 

817 
val bind_propp_schematic = gen_bind_propp mode_schematic Syntax.read_props; 

818 
val bind_propp_schematic_i = gen_bind_propp mode_schematic (map o cert_prop); 

6789  819 

10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

820 
end; 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

821 

6789  822 

5819  823 

824 
(** theorems **) 

825 

18042  826 
(* fact_tac *) 
827 

18122  828 
fun comp_incr_tac [] _ st = no_tac st 
829 
 comp_incr_tac (th :: ths) i st = 

830 
(Goal.compose_hhf_tac (Drule.incr_indexes st th) i APPEND comp_incr_tac ths i) st; 

18042  831 

21687  832 
fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts; 
18122  833 

834 
fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => 

18042  835 
let 
19001  836 
val index = fact_index_of ctxt; 
18042  837 
val facts = FactIndex.could_unify index (Term.strip_all_body goal); 
838 
in fact_tac facts i end); 

839 

840 

6091  841 
(* get_thm(s) *) 
5819  842 

18042  843 
fun retrieve_thms _ pick ctxt (Fact s) = 
16501  844 
let 
24511
69d270cc7e4f
removed obsolete read/cert variations (cf. Syntax.read/check);
wenzelm
parents:
24505
diff
changeset

845 
val prop = Syntax.read_prop (set_mode mode_default ctxt) s 
69d270cc7e4f
removed obsolete read/cert variations (cf. Syntax.read/check);
wenzelm
parents:
24505
diff
changeset

846 
> singleton (Variable.polymorphic ctxt); 
69d270cc7e4f
removed obsolete read/cert variations (cf. Syntax.read/check);
wenzelm
parents:
24505
diff
changeset

847 
val th = Goal.prove ctxt [] [] prop (K (ALLGOALS (some_fact_tac ctxt))) 
18678  848 
handle ERROR msg => cat_error msg "Failed to retrieve literal fact."; 
18042  849 
in pick "" [th] end 
850 
 retrieve_thms from_thy pick ctxt xthmref = 

851 
let 

852 
val thy = theory_of ctxt; 

19001  853 
val (space, tab) = #1 (thms_of ctxt); 
16501  854 
val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref; 
855 
val name = PureThy.name_of_thmref thmref; 

24012  856 
val thms = 
857 
if name = "" then [Thm.transfer thy Drule.dummy_thm] 

858 
else 

859 
(case Symtab.lookup tab name of 

860 
SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths) 

861 
 NONE => from_thy thy xthmref); 

862 
in pick name thms end; 

5819  863 

9566  864 
val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm; 
865 
val get_thm_closure = retrieve_thms PureThy.get_thms_closure PureThy.single_thm; 

866 
val get_thms = retrieve_thms PureThy.get_thms (K I); 

867 
val get_thms_closure = retrieve_thms PureThy.get_thms_closure (K I); 

5819  868 

869 

16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

870 
(* valid_thms *) 
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

871 

fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

872 
fun valid_thms ctxt (name, ths) = 
18678  873 
(case try (fn () => get_thms ctxt (Name name)) () of 
16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

874 
NONE => false 
16147  875 
 SOME ths' => Thm.eq_thms (ths, ths')); 
16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

876 

fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

877 

fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

878 
(* lthms_containing *) 
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

879 

fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

880 
fun lthms_containing ctxt spec = 
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

881 
FactIndex.find (fact_index_of ctxt) spec 
21569  882 
> map (fn (name, ths) => 
883 
if valid_thms ctxt (name, ths) then (name, ths) 

884 
else (NameSpace.hidden (if name = "" then "unnamed" else name), ths)); 

16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

885 

fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

886 

13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

887 
(* name space operations *) 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

888 

22352  889 
val add_path = map_naming o NameSpace.add_path; 
19062
0fd52e819c24
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19033
diff
changeset

890 
val no_base_names = map_naming NameSpace.no_base_names; 
16147  891 
val qualified_names = map_naming NameSpace.qualified_names; 
19062
0fd52e819c24
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19033
diff
changeset

892 
val sticky_prefix = map_naming o NameSpace.sticky_prefix; 
0fd52e819c24
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19033
diff
changeset

893 
val restore_naming = map_naming o K o naming_of; 
21728  894 
val reset_naming = map_naming (K local_naming); 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

895 

19001  896 
fun hide_thms fully names = map_thms (fn ((space, tab), index) => 
897 
((fold (NameSpace.hide fully) names space, tab), index)); 

13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

898 

12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

899 

17360
fa1f262dbc4e
added add_view, export_view (supercedes adhoc view arguments);
wenzelm
parents:
17221
diff
changeset

900 
(* put_thms *) 
5819  901 

21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

902 
fun update_thms _ ("", NONE) ctxt = ctxt 
21648  903 
 update_thms opts ("", SOME ths) ctxt = ctxt > map_thms (fn (facts, index) => 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

904 
let 
21648  905 
val index' = uncurry FactIndex.add_local opts ("", ths) index; 
19001  906 
in (facts, index') end) 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

907 
 update_thms _ (bname, NONE) ctxt = ctxt > map_thms (fn ((space, tab), index) => 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

908 
let 
19387  909 
val name = full_name ctxt bname; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

910 
val tab' = Symtab.delete_safe name tab; 
19001  911 
in ((space, tab'), index) end) 
21648  912 
 update_thms opts (bname, SOME ths) ctxt = ctxt > map_thms (fn ((space, tab), index) => 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

913 
let 
19387  914 
val name = full_name ctxt bname; 
19001  915 
val space' = NameSpace.declare (naming_of ctxt) name space; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

916 
val tab' = Symtab.update (name, ths) tab; 
21648  917 
val index' = uncurry FactIndex.add_local opts (name, ths) index; 
19001  918 
in ((space', tab'), index') end); 
5819  919 

21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

920 
fun put_thms thms ctxt = 
21648  921 
ctxt > map_naming (K local_naming) > update_thms (true, false) thms > restore_naming ctxt; 
19079
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

922 

7606  923 

14564  924 
(* note_thmss *) 
5819  925 

12711  926 
local 
16147  927 

21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

928 
fun gen_note_thmss get k = fold_map (fn ((bname, more_attrs), raw_facts) => fn ctxt => 
5819  929 
let 
21643
bdf3e74727df
note_thmss: added kind tag and nonofficial name;
wenzelm
parents:
21622
diff
changeset

930 
val name = full_name ctxt bname; 
bdf3e74727df
note_thmss: added kind tag and nonofficial name;
wenzelm
parents:
21622
diff
changeset

931 
val facts = PureThy.name_thmss false name (map (apfst (get ctxt)) raw_facts); 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

932 
fun app (th, attrs) x = 
21643
bdf3e74727df
note_thmss: added kind tag and nonofficial name;
wenzelm
parents:
21622
diff
changeset

933 
swap (foldl_map (Thm.proof_attributes (attrs @ more_attrs @ [PureThy.kind k])) (x, th)); 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

934 
val (res, ctxt') = fold_map app facts ctxt; 
21643
bdf3e74727df
note_thmss: added kind tag and nonofficial name;
wenzelm
parents:
21622
diff
changeset

935 
val thms = PureThy.name_thms false false name (flat res); 
24388
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

936 
val Mode {stmt, ...} = get_mode ctxt; 
cf24894b81ff
added inner syntax mode, includes former type_mode and is_stmt;
wenzelm
parents:
24371
diff
changeset

937 
in ((bname, thms), ctxt' > update_thms (stmt, true) (bname, SOME thms)) end); 
12711  938 

939 
in 

940 

21622  941 
fun note_thmss k = gen_note_thmss get_thms k; 
942 
fun note_thmss_i k = gen_note_thmss (K I) k; 

15696  943 

12711  944 
end; 
9196  945 

5819  946 

947 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

948 
(** parameters **) 
17360
fa1f262dbc4e
added add_view, export_view (supercedes adhoc view arguments);
wenzelm
parents:
17221
diff
changeset

949 

8096  950 
(* variables *) 
951 

19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

952 
fun declare_var (x, opt_T, mx) ctxt = 
22701  953 
let val T = (case opt_T of SOME T => T  NONE => Syntax.mixfixT mx) 
20163  954 
in ((x, T, mx), ctxt > Variable.declare_constraints (Free (x, T))) end; 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

955 

10381  956 
local 
957 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

958 
fun prep_vars prep_typ internal legacy = 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

959 
fold_map (fn (raw_x, raw_T, raw_mx) => fn ctxt => 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

960 
let 
19371  961 
val (x, mx) = Syntax.const_mixfix raw_x raw_mx; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

962 
val _ = 
18678  963 
if not legacy andalso not (Syntax.is_identifier (no_skolem internal x)) then 
964 
error ("Illegal variable name: " ^ quote x) 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

965 
else (); 
12504  966 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

967 
fun cond_tvars T = 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

968 
if internal then T 
18678  969 
else Type.no_tvars T handle TYPE (msg, _, _) => error msg; 
24277  970 
val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

971 
val var = (x, opt_T, mx); 
19001  972 
in (var, ctxt > declare_var var > #2) end); 
8096  973 

10381  974 
in 
975 

24277  976 
val read_vars = prep_vars Syntax.parse_typ false false; 
977 
val cert_vars = prep_vars (K I) true false; 

978 
val read_vars_legacy = prep_vars Syntax.parse_typ true true; 

979 
val cert_vars_legacy = prep_vars (K I) true true; 

8096  980 

10381  981 
end; 
982 

8096  983 

19681  984 
(* authentic constants *) 
19663  985 

21208
62ccdaf9369a
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

986 
fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx)) 
21667
ce813b82c88b
add_notation: permissive about undeclared consts;
wenzelm
parents:
21648
diff
changeset

987 
 const_syntax ctxt (Const (c, _), mx) = 
ce813b82c88b
add_notation: permissive about undeclared consts;
wenzelm
parents:
21648
diff
changeset

988 
Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx)) 
21208
62ccdaf9369a
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

989 
 const_syntax _ _ = NONE; 
62ccdaf9369a
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21183
diff
changeset

990 

21772  991 
fun context_const_ast_tr ctxt [Syntax.Variable c] = 
19681  992 
let 
21772  993 
val consts = consts_of ctxt; 
19681  994 
val c' = Consts.intern consts c; 
21728  995 
val _ = Consts.the_constraint consts c' handle TYPE (msg, _, _) => error msg; 
19681  996 
in Syntax.Constant (Syntax.constN ^ c') end 
997 
 context_const_ast_tr _ asts = raise Syntax.AST ("const_ast_tr", asts); 

998 

999 
val _ = Context.add_setup 

1000 
(Sign.add_syntax 

1001 
[("_context_const", "id => 'a", Delimfix "CONST _"), 

1002 
("_context_const", "longid => 'a", Delimfix "CONST _")] #> 

1003 
Sign.add_advanced_trfuns ([("_context_const", context_const_ast_tr)], [], [], [])); 

1004 

19663  1005 

21744  1006 
(* notation *) 
1007 

1008 
fun add_notation mode args ctxt = 

1009 
ctxt > map_syntax 

1010 
(LocalSyntax.add_modesyntax (theory_of ctxt) mode (map_filter (const_syntax ctxt) args)); 

1011 

21803  1012 
fun target_notation mode args phi = 
1013 
let val args' = filter (fn (t, _) => Term.equiv_types (t, Morphism.term phi t)) args; 

21744  1014 
in Context.mapping (Sign.add_notation mode args') (add_notation mode args') end; 
1015 

1016 

24767  1017 
(* local constants *) 
1018 

1019 
fun add_const_constraint (c, opt_T) ctxt = 

1020 
let 

1021 
fun prepT raw_T = 

1022 
let val T = cert_typ ctxt raw_T 

1023 
in cert_term ctxt (Const (c, T)); T end; 

1024 
in ctxt > map_consts (apsnd (Consts.constrain (c, Option.map prepT opt_T))) end; 

19001  1025 

24778  1026 
fun add_abbrev mode tags (c, raw_t) ctxt = 
19001  1027 
let 
24675
2be1253a20d3
removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
wenzelm
parents:
24612
diff
changeset

1028 
val t0 = cert_term (ctxt > set_mode mode_abbrev) raw_t 
21681  1029 
handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c); 
20008
8d9d770e1f06
add_abbrevs/polymorphic: Variable.exportT_terms avoids overgeneralization;
wenzelm
parents:
19916
diff
changeset

1030 
val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; 
21807
a59f083632a7
add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);
wenzelm
parents:
21803
diff
changeset

1031 
val ((lhs, rhs), consts') = consts_of ctxt 
24778  1032 
> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (c, t); 
19001  1033 
in 
1034 
ctxt 

21681  1035 
> map_consts (apsnd (K consts')) 
21803  1036 
> Variable.declare_term rhs 
1037 
> pair (lhs, rhs) 

21704  1038 
end; 
19001  1039 

1040 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1041 
(* fixes *) 
5819  1042 

8096  1043 
local 
1044 

19001  1045 
fun prep_mixfix (x, T, mx) = 
19019  1046 
if mx <> NoSyn andalso mx <> Structure andalso 
20086
94ca946fb689
adapted to more efficient Name/Variable implementation;
wenzelm
parents:
20049
diff
changeset

1047 
(can Name.dest_internal x orelse can Name.dest_skolem x) then 
19001  1048 
error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x) 
1049 
else (true, (x, T, mx)); 

1050 

18844  1051 
fun gen_fixes prep raw_vars ctxt = 
8096  1052 
let 
22712  1053 
val (vars, _) = prep raw_vars ctxt; 
1054 
val (xs', ctxt') = Variable.add_fixes (map #1 vars) ctxt; 

8096  1055 
in 
22712  1056 
ctxt' 
19001  1057 
> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

1058 
> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix) 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1059 
> pair xs' 
8096  1060 
end; 
5819  1061 

8096  1062 
in 
7679  1063 

18844  1064 
val add_fixes = gen_fixes read_vars; 
1065 
val add_fixes_i = gen_fixes cert_vars; 

1066 
val add_fixes_legacy = gen_fixes cert_vars_legacy; 

8096  1067 

1068 
end; 

5819  1069 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1070 

ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1071 
(* fixes vs. frees *) 
12016  1072 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1073 
fun auto_fixes (arg as (ctxt, (propss, x))) = 
21370
d9dd7b4e5e69
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents:
21269
diff
changeset

1074 
((fold o fold) Variable.auto_fixes propss ctxt, (propss, x)); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1075 

ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1076 
fun bind_fixes xs ctxt = 
9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1077 
let 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1078 
val (_, ctxt') = ctxt > add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs); 
9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1079 
fun bind (t as Free (x, T)) = 
18340  1080 
if member (op =) xs x then 
15531  1081 
(case lookup_skolem ctxt' x of SOME x' => Free (x', T)  NONE => t) 
9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1082 
else t 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1083 
 bind (t $ u) = bind t $ bind u 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1084 
 bind (Abs (x, T, t)) = Abs (x, T, bind t) 
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1085 
 bind a = a; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1086 
in (bind, ctxt') end; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1087 

9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1088 

23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

1089 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1090 
(** assumptions **) 
18187  1091 

20209  1092 
local 
1093 

1094 
fun gen_assms prepp exp args ctxt = 

1095 
let 

20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1096 
val cert = Thm.cterm_of (theory_of ctxt); 
20209  1097 
val (propss, ctxt1) = swap (prepp (ctxt, map snd args)); 
20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1098 
val _ = Variable.warn_extra_tfrees ctxt ctxt1; 
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1099 
val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1; 
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1100 
in 
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1101 
ctxt2 
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1102 
> auto_bind_facts (flat propss) 
21443
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

1103 
> put_thms (AutoBind.premsN, SOME (Assumption.prems_of ctxt2)) 
cc5095d57da4
added stmt mode, which affects naming/indexing of local facts;
wenzelm
parents:
21370
diff
changeset

1104 
> note_thmss_i Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss) 
20234
7e0693474bcd
added legacy_pretty_thm (with fallback on ProtoPure.thy);
wenzelm
parents:
20209
diff
changeset

1105 
end; 
20209  1106 

1107 
in 

1108 

1109 
val add_assms = gen_assms (apsnd #1 o bind_propp); 

1110 
val add_assms_i = gen_assms (apsnd #1 o bind_propp_i); 

1111 

1112 
end; 

1113 

1114 

5819  1115 

8373
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1116 
(** cases **) 
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1117 

16147  1118 
local 
1119 

16668  1120 
fun rem_case name = remove (fn (x: string, (y, _)) => x = y) name; 
16147  1121 

18476  1122 
fun add_case _ ("", _) cases = cases 
1123 
 add_case _ (name, NONE) cases = rem_case name cases 

1124 
 add_case is_proper (name, SOME c) cases = (name, (c, is_proper)) :: rem_case name cases; 

16147  1125 

18678  1126 
fun prep_case name fxs c = 
18609  1127 
let 
1128 
fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys 

1129 
 replace [] ys = ys 

18678  1130 
 replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name); 
18609  1131 
val RuleCases.Case {fixes, assumes, binds, cases} = c; 
1132 
val fixes' = replace fxs fixes; 

1133 
val binds' = map drop_schematic binds; 

1134 
in 

1135 
if null (fold (Term.add_tvarsT o snd) fixes []) andalso 

1136 
null (fold (fold Term.add_vars o snd) assumes []) then 

1137 
RuleCases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases} 

18678  1138 
else error ("Illegal schematic variable(s) in case " ^ quote name) 
18609  1139 
end; 
1140 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1141 
fun fix (x, T) ctxt = 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1142 
let 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1143 
val (bind, ctxt') = bind_fixes [x] ctxt; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1144 
val t = bind (Free (x, T)); 
20163  1145 
in (t, ctxt' > Variable.declare_constraints t) end; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1146 

16147  1147 
in 
1148 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1149 
fun add_cases is_proper = map_cases o fold (add_case is_proper); 
18609  1150 

1151 
fun case_result c ctxt = 

1152 
let 

1153 
val RuleCases.Case {fixes, ...} = c; 

18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1154 
val (ts, ctxt') = ctxt > fold_map fix fixes; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1155 
val RuleCases.Case {assumes, binds, cases, ...} = RuleCases.apply ts c; 
18609  1156 
in 
1157 
ctxt' 

18699
f3bfe81b6e58
case_result: drop_schematic, i.e. be permissive about illegal binds;
wenzelm
parents:
18678
diff
changeset

1158 
> add_binds_i (map drop_schematic binds) 
18609  1159 
> add_cases true (map (apsnd SOME) cases) 
1160 
> pair (assumes, (binds, cases)) 

1161 
end; 

1162 

1163 
val apply_case = apfst fst oo case_result; 

1164 

16540  1165 
fun get_case ctxt name xs = 
17184  1166 
(case AList.lookup (op =) (cases_of ctxt) name of 
18678  1167 
NONE => error ("Unknown case: " ^ quote name) 
1168 
 SOME (c, _) => prep_case name xs c); 

8373
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1169 

16147  1170 
end; 
8373
e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1171 

e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1172 

e7237c8fe29e
handling of local contexts: print_cases, get_case, add_cases;
wenzelm
parents:
8186
diff
changeset

1173 

10810  1174 
(** print context information **) 
1175 

20310  1176 
val debug = ref false; 
1177 

10810  1178 
val verbose = ref false; 
1179 
fun verb f x = if ! verbose then f (x ()) else []; 

1180 

1181 
fun setmp_verbose f x = Library.setmp verbose true f x; 

1182 

1183 

12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

1184 
(* local syntax *) 
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

1185 

12093  1186 
val print_syntax = Syntax.print_syntax o syn_of; 
12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

1187 

4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

1188 

21728  1189 
(* abbreviations *) 
18971  1190 

21728  1191 
fun pretty_abbrevs show_globals ctxt = 
18971  1192 
let 
19033
24e251657e56
consts: maintain thy version for efficient transfer;
wenzelm
parents:
19019
diff
changeset

1193 
val ((_, globals), (space, consts)) = 
24e251657e56
consts: maintain thy version for efficient transfer;
wenzelm
parents:
19019
diff
changeset

1194 
pairself (#constants o Consts.dest) (#consts (rep_context ctxt)); 
21803  1195 
fun add_abbr (_, (_, NONE)) = I 
1196 
 add_abbr (c, (T, SOME (t, _))) = 

21728  1197 
if not show_globals andalso Symtab.defined globals c then I 
1198 
else cons (c, Logic.mk_equals (Const (c, T), t)); 

21803  1199 
val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold add_abbr consts [])); 
18971  1200 
in 
1201 
if null abbrevs andalso not (! verbose) then [] 

21728  1202 
else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)] 
18971  1203 
end; 
1204 

21728  1205 
val print_abbrevs = Pretty.writeln o Pretty.chunks o pretty_abbrevs true; 
1206 

18971  1207 

10810  1208 
(* term bindings *) 
1209 

16540  1210 
fun pretty_binds ctxt = 
10810  1211 
let 
19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19882
diff
changeset

1212 
val binds = Variable.binds_of ctxt; 
21728  1213 
fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t)); 
10810  1214 
in 
15758
07e382399a96
binds/thms: do not store options, but delete from table;
wenzelm
parents:
15750
diff
changeset

1215 
if Vartab.is_empty binds andalso not (! verbose) then [] 
07e382399a96
binds/thms: do not store options, but delete from table;
wenzelm
parents:
15750
diff
changeset

1216 
else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))] 
10810  1217 
end; 
1218 

1219 
val print_binds = Pretty.writeln o Pretty.chunks o pretty_binds; 

1220 

1221 

1222 
(* local theorems *) 

1223 

16540  1224 
fun pretty_lthms ctxt = 
20012  1225 
let 
1226 
val props = FactIndex.props (fact_index_of ctxt); 

1227 
val facts = 

1228 
(if null props then I else cons ("unnamed", props)) 

1229 
(NameSpace.extern_table (#1 (thms_of ctxt))); 

1230 
in 

1231 
if null facts andalso not (! verbose) then [] 

1232 
else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)] 

1233 
end; 

10810  1234 

12057  1235 
val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms; 
10810  1236 

1237 

1238 
(* local contexts *) 

1239 

16540  1240 
fun pretty_cases ctxt = 
10810  1241 
let 
12057  1242 
val prt_term = pretty_term ctxt; 
1243 

10810  1244 
fun prt_let (xi, t) = Pretty.block 
10818  1245 
[Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1, 
10810  1246 
Pretty.quote (prt_term t)]; 
1247 

13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

1248 
fun prt_asm (a, ts) = Pretty.block (Pretty.breaks 
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

1249 
((if a = "" then [] else [Pretty.str (a ^ ":")]) @ map (Pretty.quote o prt_term) ts)); 
119ae829ad9b
support for split assumptio 