author  wenzelm 
Wed, 15 Mar 2006 16:18:12 +0100  
changeset 19274  b85e16bd70d0 
parent 19270  d928b5468c43 
child 19310  9b2080d9ed28 
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 

7 
elements, polymorphic abbreviations, and extralogical data. 

5819  8 
*) 
9 

10 
signature PROOF_CONTEXT = 

11 
sig 

17756  12 
type context (*= Context.proof*) 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

13 
type export 
5819  14 
val theory_of: context > theory 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

15 
val init: theory > context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

16 
val set_body: bool > context > context 
18743  17 
val restore_body: context > context > context 
17451  18 
val assms_of: context > term list 
7557  19 
val prems_of: context > thm list 
16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

20 
val fact_index_of: context > FactIndex.T 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

21 
val is_fixed: context > string > bool 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

22 
val is_known: context > string > bool 
17072  23 
val transfer: theory > context > context 
19019  24 
val map_theory: (theory > theory) > context > context 
14828  25 
val pretty_term: context > term > Pretty.T 
26 
val pretty_typ: context > typ > Pretty.T 

27 
val pretty_sort: context > sort > Pretty.T 

28 
val pp: context > Pretty.pp 

29 
val pretty_thm: context > thm > Pretty.T 

30 
val pretty_thms: context > thm list > Pretty.T 

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

17072  32 
val pretty_proof: context > Proofterm.proof > Pretty.T 
33 
val pretty_proof_of: context > bool > thm > Pretty.T 

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

34 
val string_of_typ: context > typ > string 
14828  35 
val string_of_term: context > term > string 
17860
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

36 
val string_of_thm: context > thm > string 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

37 
val used_types: context > string list 
12414  38 
val default_type: context > string > typ option 
5819  39 
val read_typ: context > string > typ 
16348  40 
val read_typ_syntax: context > string > typ 
41 
val read_typ_abbrev: context > string > typ 

5819  42 
val cert_typ: context > typ > typ 
16348  43 
val cert_typ_syntax: context > typ > typ 
44 
val cert_typ_abbrev: context > typ > typ 

10583  45 
val get_skolem: context > string > string 
18255  46 
val revert_skolem: context > string > string 
9133  47 
val extern_skolem: context > term > term 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

48 
val read_termTs: context > (string > bool) > (indexname > typ option) 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

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

50 
> term list * (indexname * typ) list 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

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

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

53 
> term list * (indexname * typ) list 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

54 
val read_term_legacy: context > string > term 
5819  55 
val read_term: context > string > term 
56 
val read_prop: context > string > term 

11925  57 
val read_prop_schematic: context > string > term 
8096  58 
val read_term_pats: typ > context > string list > term list 
59 
val read_prop_pats: context > string list > term list 

5819  60 
val cert_term: context > term > term 
61 
val cert_prop: context > term > term 

8096  62 
val cert_term_pats: typ > context > term list > term list 
63 
val cert_prop_pats: context > term list > term list 

5819  64 
val declare_term: term > context > context 
18770  65 
val infer_type: context > string > typ 
66 
val inferred_param: string > context > (string * typ) * context 

67 
val inferred_fixes: context > (string * typ) list * context 

15703  68 
val read_tyname: context > string > typ 
69 
val read_const: context > string > term 

19019  70 
val rename_frees: context > term list > (string * 'a) list > (string * 'a) list 
7925  71 
val warn_extra_tfrees: context > context > context 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

72 
val generalize: context > context > term list > term list 
19270  73 
val monomorphic: context > term list > term list 
19001  74 
val polymorphic: context > term list > term list 
19270  75 
val hidden_polymorphism: term > typ > (indexname * sort) list 
18785
5ae1f1c1b764
renamed export to export_standard (again!), because it includes Drule.local_standard';
wenzelm
parents:
18770
diff
changeset

76 
val export_standard: context > context > thm > thm 
18042  77 
val exports: context > context > thm > thm Seq.seq 
78 
val goal_exports: context > context > thm > thm Seq.seq 

10810  79 
val drop_schematic: indexname * term option > indexname * term option 
80 
val add_binds: (indexname * string option) list > context > context 

81 
val add_binds_i: (indexname * term option) list > context > context 

12147  82 
val auto_bind_goal: term list > context > context 
83 
val auto_bind_facts: term list > context > context 

18310  84 
val match_bind: bool > (string list * string) list > context > term list * context 
85 
val match_bind_i: bool > (term list * term) list > context > term list * context 

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

86 
val read_propp: context * (string * (string list * string list)) list list 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

87 
> context * (term * (term list * term list)) list list 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

88 
val cert_propp: context * (term * (term list * term list)) list list 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

89 
> context * (term * (term list * term list)) list list 
10554  90 
val read_propp_schematic: context * (string * (string list * string list)) list list 
91 
> context * (term * (term list * term list)) list list 

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

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

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

94 
val bind_propp: context * (string * (string list * string list)) list list 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

95 
> context * (term list list * (context > context)) 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

96 
val bind_propp_i: context * (term * (term list * term list)) list list 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

97 
> context * (term list list * (context > context)) 
10554  98 
val bind_propp_schematic: context * (string * (string list * string list)) list list 
99 
> context * (term list list * (context > context)) 

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

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

18042  102 
val fact_tac: thm list > int > tactic 
103 
val some_fact_tac: context > int > tactic 

15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15452
diff
changeset

104 
val get_thm: context > thmref > thm 
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15452
diff
changeset

105 
val get_thm_closure: context > thmref > thm 
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15452
diff
changeset

106 
val get_thms: context > thmref > thm list 
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15452
diff
changeset

107 
val get_thms_closure: context > thmref > thm list 
16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

108 
val valid_thms: context > string * thm list > bool 
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

109 
val lthms_containing: context > FactIndex.spec > (string * thm list) list 
16348  110 
val extern_thm: context > string > xstring 
19019  111 
val no_base_names: context > context 
16147  112 
val qualified_names: context > context 
19062
0fd52e819c24
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19033
diff
changeset

113 
val sticky_prefix: string > context > context 
16147  114 
val restore_naming: context > context > context 
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13415
diff
changeset

115 
val hide_thms: bool > string list > context > context 
19079
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

116 
val put_thms: bool > string * thm list option > context > context 
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

117 
val put_thms_internal: string * thm list option > context > context 
14564  118 
val note_thmss: 
18728  119 
((bstring * attribute list) * (thmref * attribute list) list) list > 
17860
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

120 
context > (bstring * thm list) list * context 
14564  121 
val note_thmss_i: 
18728  122 
((bstring * attribute list) * (thm list * attribute list) list) list > 
17860
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

123 
context > (bstring * thm list) list * context 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

124 
val read_vars: (string * string option * mixfix) list > context > 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

125 
(string * typ option * mixfix) list * context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

126 
val cert_vars: (string * typ option * mixfix) list > context > 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

127 
(string * typ option * mixfix) list * context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

128 
val read_vars_legacy: (string * string option * mixfix) list > context > 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

129 
(string * typ option * mixfix) list * context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

130 
val cert_vars_legacy: (string * typ option * mixfix) list > context > 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

131 
(string * typ option * mixfix) list * context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

132 
val add_fixes: (string * string option * mixfix) list > context > string list * context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

133 
val add_fixes_i: (string * typ option * mixfix) list > context > string list * context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

134 
val add_fixes_legacy: (string * typ option * mixfix) list > context > string list * context 
18809  135 
val invent_fixes: string list > context > string list * context 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

136 
val fix_frees: term > context > context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

137 
val auto_fixes: context * (term list list * 'a) > context * (term list list * 'a) 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

138 
val bind_fixes: string list > context > (term > term) * context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

139 
val add_assms: export > 
18728  140 
((string * attribute list) * (string * (string list * string list)) list) list > 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

141 
context > (bstring * thm list) list * context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

142 
val add_assms_i: export > 
18728  143 
((string * attribute list) * (term * (term list * term list)) list) list > 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

144 
context > (bstring * thm list) list * context 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

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

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

147 
val add_view: context > cterm list > context > context 
18042  148 
val export_view: cterm list > context > context > thm > thm 
18609  149 
val add_cases: bool > (string * RuleCases.T option) list > context > context 
150 
val apply_case: RuleCases.T > context > (string * term list) list * context 

16147  151 
val get_case: context > string > string option list > RuleCases.T 
19001  152 
val add_abbrevs: bool > (bstring * string * mixfix) list > context > context 
153 
val add_abbrevs_i: bool > (bstring * term * mixfix) list > context > context 

10810  154 
val verbose: bool ref 
155 
val setmp_verbose: ('a > 'b) > 'a > 'b 

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

156 
val print_syntax: context > unit 
10810  157 
val print_binds: context > unit 
12057  158 
val print_lthms: context > unit 
10810  159 
val print_cases: context > unit 
160 
val prems_limit: int ref 

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

161 
val pretty_ctxt: context > Pretty.T list 
10810  162 
val pretty_context: context > Pretty.T list 
18809  163 
val debug: bool ref 
164 
val pprint_context: context > pprint_args > unit 

5819  165 
end; 
166 

16540  167 
structure ProofContext: PROOF_CONTEXT = 
5819  168 
struct 
169 

16540  170 
type context = Context.proof; 
5819  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 

5819  178 

16540  179 
(** Isar proof context information **) 
5819  180 

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

181 
type export = bool > cterm list > thm > thm Seq.seq; 
5819  182 

16540  183 
datatype ctxt = 
184 
Ctxt of 

19001  185 
{naming: NameSpace.naming, (*local naming conventions*) 
186 
syntax: LocalSyntax.T, (*local syntax*) 

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

187 
consts: Consts.T * Consts.T, (*global/local consts*) 
19001  188 
fixes: bool * (string * string) list, (*fixes: !!x. _ with proof body flag*) 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

189 
assms: 
19001  190 
((cterm list * export) list * (*assumes and views: A ==> _*) 
191 
(string * thm list) list), (*prems: A  A*) 

192 
binds: (typ * term) Vartab.table, (*term bindings*) 

193 
thms: thm list NameSpace.table * FactIndex.T, (*local thms*) 

194 
cases: (string * (RuleCases.T * bool)) list, (*local contexts*) 

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

195 
defaults: 
19001  196 
typ Vartab.table * (*type constraints*) 
197 
sort Vartab.table * (*default sorts*) 

198 
string list * (*used type variables*) 

199 
term list Symtab.table}; (*type variable occurrences*) 

5819  200 

19001  201 
fun make_ctxt (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) = 
202 
Ctxt {naming = naming, syntax = syntax, consts = consts, fixes = fixes, assms = assms, 

203 
binds = binds, thms = thms, cases = cases, defaults = defaults}; 

5819  204 

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

205 
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

206 

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

208 
( 
16540  209 
val name = "Isar/context"; 
210 
type T = ctxt; 

211 
fun init thy = 

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

212 
make_ctxt (local_naming, LocalSyntax.init thy, 
19033
24e251657e56
consts: maintain thy version for efficient transfer;
wenzelm
parents:
19019
diff
changeset

213 
(Sign.consts_of thy, Sign.consts_of thy), (false, []), ([], []), 
24e251657e56
consts: maintain thy version for efficient transfer;
wenzelm
parents:
19019
diff
changeset

214 
Vartab.empty, (NameSpace.empty_table, FactIndex.empty), [], 
16540  215 
(Vartab.empty, Vartab.empty, [], Symtab.empty)); 
216 
fun print _ _ = (); 

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

217 
); 
5819  218 

18708  219 
val _ = Context.add_setup ContextData.init; 
5819  220 

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

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

223 
fun map_context f = 
19001  224 
ContextData.map (fn Ctxt {naming, syntax, consts, fixes, assms, binds, thms, cases, defaults} => 
225 
make_ctxt (f (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults))); 

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

226 

19001  227 
fun map_naming f = 
228 
map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => 

229 
(f naming, syntax, consts, fixes, assms, binds, thms, cases, defaults)); 

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

230 

19001  231 
fun map_syntax f = 
232 
map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => 

233 
(naming, f syntax, consts, fixes, assms, binds, thms, cases, defaults)); 

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

234 

19001  235 
fun map_consts f = 
236 
map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => 

237 
(naming, syntax, f consts, fixes, assms, binds, thms, cases, defaults)); 

238 

239 
fun map_fixes f = 

240 
map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => 

241 
(naming, syntax, consts, f fixes, assms, binds, thms, cases, defaults)); 

18971  242 

19001  243 
fun map_assms f = 
244 
map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => 

245 
(naming, syntax, consts, fixes, f assms, binds, thms, cases, defaults)); 

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

246 

19001  247 
fun map_binds f = 
248 
map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => 

249 
(naming, syntax, consts, fixes, assms, f binds, thms, cases, defaults)); 

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

250 

19001  251 
fun map_thms f = 
252 
map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => 

253 
(naming, syntax, consts, fixes, assms, binds, f thms, cases, defaults)); 

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

254 

19001  255 
fun map_cases f = 
256 
map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => 

257 
(naming, syntax, consts, fixes, assms, binds, thms, f cases, defaults)); 

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

258 

19001  259 
fun map_defaults f = 
260 
map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => 

261 
(naming, syntax, consts, fixes, assms, binds, thms, cases, f defaults)); 

262 

263 
val naming_of = #naming o rep_context; 

5819  264 

16540  265 
val syntax_of = #syntax o rep_context; 
19001  266 
val syn_of = LocalSyntax.syn_of o syntax_of; 
267 

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

268 
val consts_of = #2 o #consts o rep_context; 
5819  269 

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

270 
val is_body = #1 o #fixes o rep_context; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

271 
fun set_body b = map_fixes (fn (_, fixes) => (b, fixes)); 
18743  272 
fun restore_body ctxt = set_body (is_body ctxt); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

273 

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

274 
val fixes_of = #2 o #fixes o rep_context; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

275 
val fixed_names_of = map #2 o fixes_of; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

276 

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

277 
val assumptions_of = #1 o #assms o rep_context; 
17451  278 
val assms_of = map Thm.term_of o List.concat o map #1 o assumptions_of; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

279 
val prems_of = List.concat o map #2 o #2 o #assms o rep_context; 
5819  280 

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

281 
val binds_of = #binds o rep_context; 
5819  282 

16540  283 
val thms_of = #thms o rep_context; 
19001  284 
val fact_index_of = #2 o thms_of; 
16540  285 

286 
val cases_of = #cases o rep_context; 

5819  287 

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

288 
val defaults_of = #defaults o rep_context; 
16540  289 
val type_occs_of = #4 o defaults_of; 
5819  290 

19019  291 
fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt); 
16894  292 
fun is_known ctxt x = Vartab.defined (#1 (defaults_of ctxt)) (x, ~1) orelse is_fixed ctxt x; 
5819  293 

294 

19001  295 
(* transfer *) 
12093  296 

19001  297 
fun transfer_syntax thy = 
298 
map_syntax (LocalSyntax.rebuild thy) #> 

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

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

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

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

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

303 
end); 
17072  304 

19001  305 
fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy; 
17072  306 

19019  307 
fun map_theory f ctxt = transfer (f (theory_of ctxt)) ctxt; 
308 

12093  309 

310 

14828  311 
(** pretty printing **) 
312 

19001  313 
fun pretty_term' abbrevs ctxt t = 
18971  314 
let 
19001  315 
val thy = theory_of ctxt; 
316 
val syntax = syntax_of ctxt; 

18971  317 
val consts = consts_of ctxt; 
19001  318 
val t' = t 
319 
> K abbrevs ? Pattern.rewrite_term thy (Consts.abbrevs_of consts) [] 

320 
> LocalSyntax.extern_term (NameSpace.extern (Consts.space_of consts)) thy syntax; 

321 
in Sign.pretty_term' (LocalSyntax.syn_of syntax) (Context.Proof ctxt) t' end; 

18971  322 

19001  323 
val pretty_term = pretty_term' true; 
16458  324 
fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T; 
325 
fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S; 

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

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

14828  328 

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

329 
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

330 
pretty_classrel ctxt, pretty_arity ctxt); 
14828  331 

17451  332 
fun pretty_thm ctxt th = 
333 
Display.pretty_thm_aux (pp ctxt) false true (assms_of ctxt) th; 

14828  334 

335 
fun pretty_thms ctxt [th] = pretty_thm ctxt th 

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

337 

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

339 
 pretty_fact ctxt (a, [th]) = 

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

341 
 pretty_fact ctxt (a, ths) = 

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

343 

17072  344 
fun pretty_proof ctxt prf = 
19001  345 
pretty_term' true (ctxt > transfer_syntax (ProofSyntax.proof_syntax prf (theory_of ctxt))) 
17072  346 
(ProofSyntax.term_of_proof prf); 
347 

348 
fun pretty_proof_of ctxt full th = 

349 
pretty_proof ctxt (ProofSyntax.proof_of full th); 

350 

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

351 
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

352 
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

353 
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

354 

14828  355 

356 

7663  357 
(** default sorts and types **) 
358 

17412  359 
val def_sort = Vartab.lookup o #2 o defaults_of; 
7663  360 

16540  361 
fun def_type ctxt pattern xi = 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

362 
let val {binds, defaults = (types, _, _, _), ...} = rep_context ctxt in 
17412  363 
(case Vartab.lookup types xi of 
16540  364 
NONE => 
365 
if pattern then NONE 

18953
93903be7ff66
norm_term: Sign.const_expansion, Envir.expand_atom;
wenzelm
parents:
18928
diff
changeset

366 
else Vartab.lookup binds xi > Option.map (TypeInfer.polymorphicT o #1) 
16540  367 
 some => some) 
368 
end; 

7663  369 

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

370 
val used_types = #3 o defaults_of; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

371 

17412  372 
fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt)) (x, ~1); 
12414  373 

7663  374 

5819  375 

376 
(** prepare types **) 

377 

9504  378 
local 
379 

380 
fun read_typ_aux read ctxt s = 

18857  381 
read (syn_of ctxt) (Context.Proof ctxt) (def_sort ctxt) s; 
5819  382 

10554  383 
fun cert_typ_aux cert ctxt raw_T = 
18678  384 
cert (theory_of ctxt) raw_T handle TYPE (msg, _, _) => error msg; 
9504  385 

386 
in 

387 

16348  388 
val read_typ = read_typ_aux Sign.read_typ'; 
389 
val read_typ_syntax = read_typ_aux Sign.read_typ_syntax'; 

390 
val read_typ_abbrev = read_typ_aux Sign.read_typ_abbrev'; 

391 
val cert_typ = cert_typ_aux Sign.certify_typ; 

392 
val cert_typ_syntax = cert_typ_aux Sign.certify_typ_syntax; 

393 
val cert_typ_abbrev = cert_typ_aux Sign.certify_typ_abbrev; 

9504  394 

395 
end; 

396 

5819  397 

7679  398 
(* internalize Skolem constants *) 
399 

17184  400 
val lookup_skolem = AList.lookup (op =) o fixes_of; 
18187  401 
fun get_skolem ctxt x = the_default x (lookup_skolem ctxt x); 
7679  402 

18678  403 
fun no_skolem internal x = 
9291
23705d14be8f
"_i" arguments now expected to have skolems already internalized;
wenzelm
parents:
9274
diff
changeset

404 
if can Syntax.dest_skolem x then 
18678  405 
error ("Illegal reference to internal Skolem constant: " ^ quote x) 
12504  406 
else if not internal andalso can Syntax.dest_internal x then 
18678  407 
error ("Illegal reference to internal variable: " ^ quote x) 
7679  408 
else x; 
409 

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

410 
fun intern_skolem ctxt internal = 
7679  411 
let 
412 
fun intern (t as Free (x, T)) = 

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

413 
if internal x then t 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

414 
else 
18678  415 
(case lookup_skolem ctxt (no_skolem false x) of 
15531  416 
SOME x' => Free (x', T) 
417 
 NONE => t) 

7679  418 
 intern (t $ u) = intern t $ intern u 
419 
 intern (Abs (x, T, t)) = Abs (x, T, intern t) 

420 
 intern a = a; 

421 
in intern end; 

422 

423 

18187  424 
(* externalize Skolem constants  approximation only! *) 
425 

18255  426 
fun rev_skolem ctxt = 
18187  427 
let val rev_fixes = map Library.swap (fixes_of ctxt) 
428 
in AList.lookup (op =) rev_fixes end; 

9133  429 

18255  430 
fun revert_skolem ctxt x = 
431 
(case rev_skolem ctxt x of 

432 
SOME x' => x' 

18375  433 
 NONE => perhaps (try Syntax.dest_skolem) x); 
18255  434 

9133  435 
fun extern_skolem ctxt = 
436 
let 

18255  437 
val revert = rev_skolem ctxt; 
9133  438 
fun extern (t as Free (x, T)) = 
18187  439 
(case revert x of 
440 
SOME x' => Free (if lookup_skolem ctxt x' = SOME x then x' else NameSpace.hidden x', T) 

441 
 NONE => t) 

9133  442 
 extern (t $ u) = extern t $ extern u 
443 
 extern (Abs (x, T, t)) = Abs (x, T, extern t) 

444 
 extern a = a; 

445 
in extern end 

446 

8096  447 

18187  448 

5819  449 
(** prepare terms and propositions **) 
450 

451 
(* 

16501  452 
(1) read / certify wrt. theory of context 
5819  453 
(2) intern Skolem constants 
454 
(3) expand term bindings 

455 
*) 

456 

457 

16501  458 
(* read wrt. theory *) (*exception ERROR*) 
5819  459 

18857  460 
fun read_def_termTs freeze pp syn ctxt (types, sorts, used) sTs = 
18971  461 
Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn (consts_of ctxt) 
18857  462 
(Context.Proof ctxt) (types, sorts) used freeze sTs; 
5874  463 

18857  464 
fun read_def_termT freeze pp syn ctxt defaults sT = 
465 
apfst hd (read_def_termTs freeze pp syn ctxt defaults [sT]); 

14828  466 

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

467 
fun read_term_thy freeze pp syn thy defaults s = 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

468 
#1 (read_def_termT freeze pp syn thy defaults (s, TypeInfer.logicT)); 
5874  469 

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

470 
fun read_prop_thy freeze pp syn thy defaults s = 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

471 
#1 (read_def_termT freeze pp syn thy defaults (s, propT)); 
12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

472 

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

473 
fun read_terms_thy freeze pp syn thy defaults = 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

474 
#1 o read_def_termTs freeze pp syn thy defaults o map (rpair TypeInfer.logicT); 
12072
4281198fb8cd
local syntax: add_syntax, proper read/pretty functions;
wenzelm
parents:
12066
diff
changeset

475 

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

476 
fun read_props_thy freeze pp syn thy defaults = 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

477 
#1 o read_def_termTs freeze pp syn thy defaults o map (rpair propT); 
5819  478 

479 

19001  480 
(* local abbreviations *) 
5819  481 

19001  482 
fun expand_consts ctxt = 
483 
Consts.certify (pp ctxt) (tsig_of ctxt) (consts_of ctxt); 

484 

485 
fun expand_binds ctxt schematic = 

5819  486 
let 
18971  487 
val binds = binds_of ctxt; 
5819  488 

19001  489 
fun expand_var (xi, T) = 
18971  490 
(case Vartab.lookup binds xi of 
19001  491 
SOME t => Envir.expand_atom (tsig_of ctxt) T t 
18971  492 
 NONE => 
493 
if schematic then Var (xi, T) 

494 
else error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi)); 

19001  495 
in Envir.beta_norm o Term.map_aterms (fn Var v => expand_var v  a => a) end; 
5819  496 

497 

6550  498 
(* dummy patterns *) 
499 

18310  500 
val prepare_dummies = 
501 
let val next = ref 1 in 

502 
fn t => 

503 
let val (i, u) = Term.replace_dummy_patterns (! next, t) 

504 
in next := i; u end 

505 
end; 

6762  506 

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

6550  509 

510 

5819  511 
(* read terms *) 
512 

10554  513 
local 
514 

15531  515 
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

516 

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

517 
fun gen_read' read app pattern schematic 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

518 
ctxt internal more_types more_sorts more_used s = 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13629
diff
changeset

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

520 
val types = append_env (def_type ctxt pattern) more_types; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

521 
val sorts = append_env (def_sort ctxt) more_sorts; 
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

522 
val used = used_types ctxt @ more_used; 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13629
diff
changeset

523 
in 
18857  524 
(read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) s 
18678  525 
handle TERM (msg, _) => error msg) 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

526 
> app (intern_skolem ctxt internal) 
19001  527 
> app (expand_consts ctxt) 
528 
> app (if pattern then I else expand_binds ctxt schematic) 

18678  529 
> app (if pattern then prepare_dummies else reject_dummies) 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

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

531 

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

532 
fun gen_read read app pattern schematic ctxt = 
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

533 
gen_read' read app pattern schematic ctxt (K false) (K NONE) (K NONE) []; 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

534 

10554  535 
in 
536 

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

537 
val read_termTs = gen_read' (read_def_termTs false) (apfst o map) false false; 
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

538 
val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false true; 
8096  539 

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

540 
fun read_term_pats T ctxt = 
16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

541 
#1 o gen_read (read_def_termTs false) (apfst o map) true false ctxt o map (rpair T); 
8096  542 
val read_prop_pats = read_term_pats propT; 
543 

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

544 
fun read_term_legacy ctxt = 
16458  545 
gen_read' (read_term_thy true) I false false ctxt (K true) (K NONE) (K NONE) []; 
14720
ceff6d4fb836
cleanup up read functions, include liberal versions;
wenzelm
parents:
14707
diff
changeset

546 

19143  547 
val read_term = gen_read (read_term_thy true) I false false; 
548 
val read_prop = gen_read (read_prop_thy true) I false false; 

549 
val read_prop_schematic = gen_read (read_prop_thy true) I false true; 

550 
val read_terms = gen_read (read_terms_thy true) map false false; 

551 
fun read_props schematic = gen_read (read_props_thy true) map false schematic; 

5819  552 

10554  553 
end; 
554 

5819  555 

556 
(* certify terms *) 

557 

10554  558 
local 
559 

18971  560 
fun gen_cert prop pattern schematic ctxt t = t 
19001  561 
> expand_consts ctxt 
562 
> (if pattern then I else expand_binds ctxt schematic) 

18971  563 
> (fn t' => #1 (Sign.certify false prop (pp ctxt) (theory_of ctxt) t') 
18678  564 
handle TYPE (msg, _, _) => error msg 
565 
 TERM (msg, _) => error msg); 

16501  566 

10554  567 
in 
8096  568 

18971  569 
val cert_term = gen_cert false false false; 
570 
val cert_prop = gen_cert true false false; 

571 
val cert_props = map oo gen_cert true false; 

10554  572 

18971  573 
fun cert_term_pats _ = map o gen_cert false true false; 
574 
val cert_prop_pats = map o gen_cert true true false; 

10554  575 

576 
end; 

5819  577 

578 

579 
(* declare terms *) 

580 

10381  581 
local 
582 

16861  583 
val ins_types = fold_aterms 
17412  584 
(fn Free (x, T) => Vartab.update ((x, ~1), T) 
585 
 Var v => Vartab.update v 

16861  586 
 _ => I); 
5819  587 

16861  588 
val ins_sorts = fold_types (fold_atyps 
19079
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

589 
(fn TFree (x, S) => Vartab.update ((x, ~1), S) 
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

590 
 TVar v => Vartab.update v 
16861  591 
 _ => I)); 
5819  592 

16861  593 
val ins_used = fold_term_types (fn t => 
594 
fold_atyps (fn TFree (x, _) => insert (op =) x  _ => I)); 

12291  595 

16861  596 
val ins_occs = fold_term_types (fn t => 
18953
93903be7ff66
norm_term: Sign.const_expansion, Envir.expand_atom;
wenzelm
parents:
18928
diff
changeset

597 
fold_atyps (fn TFree (x, _) => Symtab.update_list (x, t)  _ => I)); 
5819  598 

16861  599 
fun ins_skolem def_ty = fold_rev (fn (x, x') => 
600 
(case def_ty x' of 

17412  601 
SOME T => Vartab.update ((x, ~1), T) 
16861  602 
 NONE => I)); 
5994  603 

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

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

605 

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

606 
fun declare_syntax t = map_defaults (fn (types, sorts, used, occ) => 
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

607 
(ins_types t types, 
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

608 
ins_sorts t sorts, 
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

609 
ins_used t used, 
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

610 
occ)); 
10381  611 

19001  612 
fun declare_var (x, opt_T, mx) ctxt = 
613 
let val T = (case opt_T of SOME T => T  NONE => TypeInfer.mixfixT mx) 

614 
in ((x, T, mx), ctxt > declare_syntax (Free (x, T))) end; 

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

615 

16540  616 
fun declare_term t ctxt = 
16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

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

618 
> declare_syntax t 
12291  619 
> map_defaults (fn (types, sorts, used, occ) => 
19079
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

620 
(ins_skolem (fn x => Vartab.lookup types (x, ~1)) (fixes_of ctxt) types, 
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

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

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

623 
ins_occs t occ)); 
5819  624 

18770  625 
end; 
626 

627 

628 
(* inferred types of parameters *) 

629 

630 
fun infer_type ctxt x = 

631 
(case try (fn () => 

18971  632 
Sign.infer_types (pp ctxt) (theory_of ctxt) (consts_of ctxt) (def_type ctxt false) 
633 
(def_sort ctxt) (used_types ctxt) true ([Free (x, dummyT)], TypeInfer.logicT)) () of 

18770  634 
SOME (Free (_, T), _) => T 
635 
 _ => error ("Failed to infer type of fixed variable " ^ quote x)); 

636 

637 
fun inferred_param x ctxt = 

18619  638 
let val T = infer_type ctxt x 
19019  639 
in ((x, T), ctxt > declare_syntax (Free (x, T))) end; 
18619  640 

18770  641 
fun inferred_fixes ctxt = 
642 
fold_map inferred_param (rev (fixed_names_of ctxt)) ctxt; 

5819  643 

644 

15703  645 
(* type and constant names *) 
646 

647 
fun read_tyname ctxt c = 

18340  648 
if member (op =) (used_types ctxt) c then 
18187  649 
TFree (c, the_default (Sign.defaultS (theory_of ctxt)) (def_sort ctxt (c, ~1))) 
16458  650 
else Sign.read_tyname (theory_of ctxt) c; 
15703  651 

652 
fun read_const ctxt c = 

653 
(case lookup_skolem ctxt c of 

654 
SOME c' => Free (c', dummyT) 

18971  655 
 NONE => Consts.read_const (consts_of ctxt) c); 
15703  656 

657 

19019  658 
(* renaming term/type frees *) 
659 

660 
fun rename_frees ctxt ts frees = 

661 
let 

662 
val (types, sorts, _, _) = defaults_of (ctxt > fold declare_syntax ts); 

663 
fun rename (x, X) xs = 

664 
let 

19274  665 
fun used y = y = "" orelse y = "'" orelse member (op =) xs y orelse 
19019  666 
Vartab.defined types (y, ~1) orelse Vartab.defined sorts (y, ~1); 
667 
val x' = Term.variant_name used x; 

668 
in ((x', X), x' :: xs) end; 

669 
in #1 (fold_map rename frees []) end; 

670 

671 

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

672 

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

673 
(** HindleyMilner polymorphism **) 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

674 

7925  675 
(* warn_extra_tfrees *) 
676 

16540  677 
fun warn_extra_tfrees ctxt1 ctxt2 = 
12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

678 
let 
17451  679 
fun occs_typ a (Type (_, Ts)) = exists (occs_typ a) Ts 
680 
 occs_typ a (TFree (b, _)) = a = b 

681 
 occs_typ _ (TVar _) = false; 

682 
fun occs_free a (Free (x, _)) = 

683 
(case def_type ctxt1 false (x, ~1) of 

684 
SOME T => if occs_typ a T then I else cons (a, x) 

685 
 NONE => cons (a, x)) 

686 
 occs_free _ _ = I; 

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

687 

17451  688 
val occs1 = type_occs_of ctxt1 and occs2 = type_occs_of ctxt2; 
689 
val extras = Symtab.fold (fn (a, ts) => 

690 
if Symtab.defined occs1 a then I else fold (occs_free a) ts) occs2 []; 

18428  691 
val tfrees = map #1 extras > sort_distinct string_ord; 
692 
val frees = map #2 extras > sort_distinct string_ord; 

12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

693 
in 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

694 
if null extras then () 
17451  695 
else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^ 
17860
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

696 
space_implode " or " (map (string_of_term ctxt2 o Syntax.free) frees)); 
12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

697 
ctxt2 
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

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

699 

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

700 

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

701 
(* generalize type variables *) 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

702 

12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

703 
fun generalize_tfrees inner outer = 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

704 
let 
12057  705 
val extra_fixes = fixed_names_of inner \\ fixed_names_of outer; 
18340  706 
fun still_fixed (Free (x, _)) = not (member (op =) extra_fixes x) 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

707 
 still_fixed _ = false; 
16540  708 
val occs_inner = type_occs_of inner; 
709 
val occs_outer = type_occs_of outer; 

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

710 
fun add a gen = 
16894  711 
if Symtab.defined occs_outer a orelse 
18953
93903be7ff66
norm_term: Sign.const_expansion, Envir.expand_atom;
wenzelm
parents:
18928
diff
changeset

712 
exists still_fixed (Symtab.lookup_list occs_inner a) 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

713 
then gen else a :: gen; 
16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

714 
in fn tfrees => fold add tfrees [] end; 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

715 

12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

716 
fun generalize inner outer ts = 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

717 
let 
18187  718 
val tfrees = generalize_tfrees inner outer (map #1 (fold Term.add_tfrees ts [])); 
18340  719 
fun gen (x, S) = if member (op =) tfrees x then TVar ((x, 0), S) else TFree (x, S); 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

720 
in map (Term.map_term_types (Term.map_type_tfree gen)) ts end; 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

721 

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

722 

19001  723 
(* polymorphic terms *) 
724 

19270  725 
fun monomorphic ctxt ts = 
726 
let 

727 
val tvars = fold Term.add_tvars ts []; 

19274  728 
val tfrees = map TFree (rename_frees ctxt ts (map (pair "'" o #2) tvars)); 
19270  729 
val specialize = Term.instantiate ((tvars ~~ tfrees), []); 
730 
in map specialize ts end; 

731 

19001  732 
fun polymorphic ctxt ts = 
733 
generalize (ctxt > fold declare_term ts) ctxt ts; 

734 

19270  735 
fun hidden_polymorphism t T = 
736 
let 

737 
val tvarsT = Term.add_tvarsT T []; 

738 
val extra_tvars = Term.fold_types (Term.fold_atyps 

739 
(fn TVar v => if member (op =) tvarsT v then I else insert (op =) v  _ => I)) t []; 

740 
in extra_tvars end; 

19001  741 

742 

9553  743 

744 
(** export theorems **) 

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

745 

18042  746 
fun common_exports is_goal inner outer = 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

747 
let 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

748 
val gen = generalize_tfrees inner outer; 
12057  749 
val fixes = fixed_names_of inner \\ fixed_names_of outer; 
750 
val asms = Library.drop (length (assumptions_of outer), assumptions_of inner); 

11816  751 
val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms; 
16948  752 
in 
18255  753 
Goal.norm_hhf_protect 
16948  754 
#> Seq.EVERY (rev exp_asms) 
755 
#> Seq.map (fn rule => 

11816  756 
let 
16992  757 
val thy = Thm.theory_of_thm rule; 
758 
val prop = Thm.full_prop_of rule; 

18152  759 
val frees = map (Thm.cterm_of thy) (List.mapPartial (Term.find_free prop) fixes); 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

760 
val tfrees = gen (Term.add_term_tfree_names (prop, [])); 
11816  761 
in 
762 
rule 

763 
> Drule.forall_intr_list frees 

18255  764 
> Goal.norm_hhf_protect 
18138  765 
> Drule.tvars_intr_list tfrees > #2 
11816  766 
end) 
767 
end; 

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

768 

18785
5ae1f1c1b764
renamed export to export_standard (again!), because it includes Drule.local_standard';
wenzelm
parents:
18770
diff
changeset

769 
fun export_standard inner outer = 
18122  770 
let val exp = common_exports false inner outer in 
13378  771 
fn th => 
18122  772 
(case Seq.pull (exp th) of 
15531  773 
SOME (th', _) => th' > Drule.local_standard 
16850  774 
 NONE => sys_error "Failed to export theorem") 
13378  775 
end; 
12704  776 

18122  777 
val exports = common_exports false; 
778 
val goal_exports = common_exports true; 

7925  779 

5819  780 

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

781 

5819  782 
(** bindings **) 
783 

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

784 
(* delete_update_binds *) 
07e382399a96
binds/thms: do not store options, but delete from table;
wenzelm
parents:
15750
diff
changeset

785 

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

786 
local 
5819  787 

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

788 
val del_bind = map_binds o Vartab.delete_safe; 
7606  789 

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

790 
fun upd_bind ((x, i), t) = 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

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

792 
val T = Term.fastype_of t; 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

793 
val t' = 
19270  794 
if null (hidden_polymorphism t T) then t 
8637  795 
else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T); 
18953
93903be7ff66
norm_term: Sign.const_expansion, Envir.expand_atom;
wenzelm
parents:
18928
diff
changeset

796 
in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end; 
5819  797 

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

798 
fun del_upd_bind (xi, NONE) = del_bind xi 
07e382399a96
binds/thms: do not store options, but delete from table;
wenzelm
parents:
15750
diff
changeset

799 
 del_upd_bind (xi, SOME t) = upd_bind (xi, t); 
7606  800 

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

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

802 

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

803 
val delete_update_binds = fold del_upd_bind; 
07e382399a96
binds/thms: do not store options, but delete from table;
wenzelm
parents:
15750
diff
changeset

804 

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

805 
end; 
7606  806 

5819  807 

8096  808 
(* simult_matches *) 
809 

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

810 
fun simult_matches ctxt [] = [] 
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

811 
 simult_matches ctxt pairs = 
8096  812 
let 
18678  813 
fun fail () = error "Pattern match failed!"; 
10554  814 

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

815 
val maxidx = fold (fn (t1, t2) => fn i => 
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

816 
Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1; 
16458  817 
val envs = Unify.smash_unifiers (theory_of ctxt, Envir.empty maxidx, 
10554  818 
map swap pairs); (*prefer assignment of variables from patterns*) 
819 
val env = 

8096  820 
(case Seq.pull envs of 
15531  821 
NONE => fail () 
822 
 SOME (env, _) => env); (*ignore further results*) 

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

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

824 
filter_out Term.is_replaced_dummy_pattern (map #1 (Drule.vars_of_terms (map #1 pairs))); 
10554  825 
val _ = (*may not assign variables from text*) 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

826 
if null (map #1 (Envir.alist_of env) inter (map #1 (Drule.vars_of_terms (map #2 pairs)))) 
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

827 
then () else fail (); 
16948  828 
fun norm_bind (xi, (_, t)) = 
18310  829 
if member (op =) domain xi then SOME (xi, Envir.norm_term env t) else NONE; 
15570  830 
in List.mapPartial norm_bind (Envir.alist_of env) end; 
8096  831 

832 

833 
(* add_binds(_i) *) 

5819  834 

7925  835 
local 
836 

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

837 
fun gen_bind prep (xi as (x, _), raw_t) ctxt = 
15570  838 
ctxt > delete_update_binds [(xi, Option.map (prep ctxt) raw_t)]; 
5819  839 

10810  840 
in 
841 

15531  842 
fun drop_schematic (b as (xi, SOME t)) = if null (Term.term_vars t) then b else (xi, NONE) 
10554  843 
 drop_schematic b = b; 
844 

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

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

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

847 

16458  848 
fun auto_bind f ts ctxt = ctxt > add_binds_i (map drop_schematic (f (theory_of ctxt) ts)); 
12147  849 
val auto_bind_goal = auto_bind AutoBind.goal; 
850 
val auto_bind_facts = auto_bind AutoBind.facts; 

7925  851 

852 
end; 

5819  853 

854 

8096  855 
(* match_bind(_i) *) 
5819  856 

8096  857 
local 
858 

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

859 
fun prep_bind prep_pats (raw_pats, t) ctxt = 
5819  860 
let 
8096  861 
val ctxt' = declare_term t ctxt; 
862 
val pats = prep_pats (fastype_of t) ctxt' raw_pats; 

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

863 
val binds = simult_matches ctxt' (map (rpair t) pats); 
17860
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

864 
in (binds, ctxt') end; 
7670  865 

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

866 
fun gen_binds prep_terms prep_pats gen raw_binds ctxt = 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

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

868 
val ts = prep_terms ctxt (map snd raw_binds); 
17860
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

869 
val (binds, ctxt') = 
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

870 
apfst List.concat (fold_map (prep_bind prep_pats) (map fst raw_binds ~~ ts) ctxt); 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

871 
val binds' = 
12550
32843ad8160a
generalize type variables properly: start with occurrences in objects
wenzelm
parents:
12530
diff
changeset

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

873 
else binds; 
15531  874 
val binds'' = map (apsnd SOME) binds'; 
18310  875 
val ctxt'' = 
876 
warn_extra_tfrees ctxt 

877 
(if gen then 

878 
ctxt (*sic!*) > fold declare_term (map #2 binds') > add_binds_i binds'' 

879 
else ctxt' > add_binds_i binds''); 

880 
in (ts, ctxt'') end; 

8096  881 

882 
in 

5935  883 

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

884 
val match_bind = gen_binds read_terms read_term_pats; 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

885 
val match_bind_i = gen_binds (map o cert_term) cert_term_pats; 
8096  886 

887 
end; 

5935  888 

889 

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

890 
(* propositions with patterns *) 
5935  891 

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

892 
local 
8096  893 

10554  894 
fun prep_propp schematic prep_props prep_pats (context, args) = 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

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

896 
fun prep (_, (raw_pats1, raw_pats2)) (ctxt, prop :: props) = 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

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

898 
val ctxt' = declare_term prop ctxt; 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

899 
val pats = prep_pats ctxt' (raw_pats1 @ raw_pats2); (*simultaneous type inference!*) 
19019  900 
in ((prop, chop (length raw_pats1) pats), (ctxt', props)) end 
17860
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

901 
 prep _ _ = sys_error "prep_propp"; 
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

902 
val (propp, (context', _)) = (fold_map o fold_map) prep args 
b4cf247ea0d2
note_thmss, read/cert_vars etc.: natural argument order;
wenzelm
parents:
17756
diff
changeset

903 
(context, prep_props schematic context (List.concat (map (map fst) args))); 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

904 
in (context', propp) end; 
5935  905 

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

906 
fun matches ctxt (prop, (pats1, pats2)) = 
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

907 
simult_matches ctxt (map (rpair prop) pats1 @ map (rpair (Logic.strip_imp_concl prop)) pats2); 
8096  908 

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

909 
fun gen_bind_propp prepp (ctxt, raw_args) = 
8096  910 
let 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

911 
val (ctxt', args) = prepp (ctxt, raw_args); 
15570  912 
val binds = List.concat (List.concat (map (map (matches ctxt')) args)); 
10465
4aa6f8b5cdc4
added read_terms, read_props (simulataneous typeinference);
wenzelm
parents:
10381
diff
changeset

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

914 

10554  915 
(*generalize result: context evaluated now, binds added later*) 
8616
90d2fed59be1
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8462
diff
changeset

916 
val gen = generalize ctxt' ctxt; 
15531  917 
fun gen_binds c = c > add_binds_i (map #1 binds ~~ map SOME (gen (map #2 binds))); 
918 
in (ctxt' > add_binds_i (map (apsnd SOME) binds), (propss, gen_binds)) end; 

8096  919 

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

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

921 

11925  922 
val read_propp = prep_propp false read_props read_prop_pats; 
923 
val cert_propp = prep_propp false cert_props cert_prop_pats; 

10554  924 
val read_propp_schematic = prep_propp true read_props read_prop_pats; 
925 
val cert_propp_schematic = prep_propp true cert_props cert_prop_pats; 

926 

11925  927 
val bind_propp = gen_bind_propp read_propp; 
928 
val bind_propp_i = gen_bind_propp cert_propp; 

929 
val bind_propp_schematic = gen_bind_propp read_propp_schematic; 

10554  930 
val bind_propp_schematic_i = gen_bind_propp cert_propp_schematic; 
6789  931 

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

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

933 

6789  934 

5819  935 

936 
(** theorems **) 

937 

18042  938 
(* fact_tac *) 
939 

18122  940 
fun comp_incr_tac [] _ st = no_tac st 
941 
 comp_incr_tac (th :: ths) i st = 

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

18042  943 

18122  944 
fun fact_tac facts = Tactic.norm_hhf_tac THEN' comp_incr_tac facts; 
945 

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

18042  947 
let 
19001  948 
val index = fact_index_of ctxt; 
18042  949 
val facts = FactIndex.could_unify index (Term.strip_all_body goal); 
950 
in fact_tac facts i end); 

951 

952 

6091  953 
(* get_thm(s) *) 
5819  954 

18042  955 
fun retrieve_thms _ pick ctxt (Fact s) = 
16501  956 
let 
18042  957 
val thy = theory_of ctxt; 
958 
val th = Goal.prove thy [] [] (read_prop ctxt s) (K (ALLGOALS (some_fact_tac ctxt))) 

18678  959 
handle ERROR msg => cat_error msg "Failed to retrieve literal fact."; 
18042  960 
in pick "" [th] end 
961 
 retrieve_thms from_thy pick ctxt xthmref = 

962 
let 

963 
val thy = theory_of ctxt; 

19001  964 
val (space, tab) = #1 (thms_of ctxt); 
16501  965 
val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref; 
966 
val name = PureThy.name_of_thmref thmref; 

967 
in 

17412  968 
(case Symtab.lookup tab name of 
16540  969 
SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths) 
970 
 NONE => from_thy thy xthmref) > pick name 

18042  971 
end; 
5819  972 

9566  973 
val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm; 
974 
val get_thm_closure = retrieve_thms PureThy.get_thms_closure PureThy.single_thm; 

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

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

5819  977 

978 

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

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

980 

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

981 
fun valid_thms ctxt (name, ths) = 
18678  982 
(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

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

985 

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

986 

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

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

988 

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

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

990 
FactIndex.find (fact_index_of ctxt) spec 
18043  991 
> map ((not o valid_thms ctxt) ? apfst (fn name => 
18042  992 
NameSpace.hidden (if name = "" then "unnamed" else name))); 
16031
fbf3471214d6
moved everything related to thms_containing to find_theorems.ML;
wenzelm
parents:
15979
diff
changeset

993 

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

994 

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

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

996 

19001  997 
val extern_thm = NameSpace.extern o #1 o #1 o thms_of; 
12309
03e9287be350
name space for local thms (export cond_extern, qualified);
wenzelm
parents:
12291
diff
changeset

998 

19062
0fd52e819c24
replaced qualified_force_prefix to sticky_prefix;
wenzelm
parents:
19033
diff
changeset

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

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

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

1003 

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

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

1006 

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

1007 

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

1008 
(* put_thms *) 
5819  1009 

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

1010 
fun put_thms _ ("", NONE) ctxt = ctxt 
19143  1011 
 put_thms do_index ("", 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

1012 
let 
19143  1013 
val index' = FactIndex.add_local do_index (is_known ctxt) ("", ths) index; 
19001  1014 
in (facts, index') end) 
19079
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

1015 
 put_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

1016 
let 
19001  1017 
val name = NameSpace.full (naming_of ctxt) bname; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1018 
val tab' = Symtab.delete_safe name tab; 
19001  1019 
in ((space, tab'), index) end) 
19079
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

1020 
 put_thms do_index (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

1021 
let 
19001  1022 
val name = NameSpace.full (naming_of ctxt) bname; 
1023 
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

1024 
val tab' = Symtab.update (name, ths) tab; 
19143  1025 
val index' = FactIndex.add_local do_index (is_known ctxt) (name, ths) index; 
19001  1026 
in ((space', tab'), index') end); 
5819  1027 

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

1028 
fun put_thms_internal thms ctxt = 
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

1029 
ctxt > map_naming (K local_naming) > put_thms false thms > restore_naming ctxt; 
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

1030 

7606  1031 

14564  1032 
(* note_thmss *) 
5819  1033 

12711  1034 
local 
16147  1035 

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

1036 
fun gen_note_thmss get = fold_map (fn ((name, more_attrs), ths_attrs) => fn ctxt => 
5819  1037 
let 
17360
fa1f262dbc4e
added add_view, export_view (supercedes adhoc view arguments);
wenzelm
parents:
17221
diff
changeset

1038 
fun app (th, attrs) (ct, ths) = 
18728  1039 
let val (ct', th') = foldl_map (Thm.proof_attributes (attrs @ more_attrs)) (ct, get ctxt th) 
12711  1040 
in (ct', th' :: ths) end; 
17360
fa1f262dbc4e
added add_view, export_view (supercedes adhoc view arguments);
wenzelm
parents:
17221
diff
changeset

1041 
val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []); 
15570  1042 
val thms = List.concat (rev rev_thms); 
19079
9a7678a0736d
added put_thms_internal: local_naming, no fact index;
wenzelm
parents:
19062
diff
changeset

1043 
in ((name, thms), ctxt' > put_thms true (name, SOME thms)) end); 
12711  1044 

1045 
in 

1046 

16147  1047 
val note_thmss = gen_note_thmss get_thms; 
1048 
val note_thmss_i = gen_note_thmss (K I); 

15696  1049 

1050 
val note_thmss_accesses = gen_note_thmss get_thms; 

1051 
val note_thmss_accesses_i = gen_note_thmss (K I); 

12711  1052 

1053 
end; 

9196  1054 

5819  1055 

1056 

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

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

1058 

8096  1059 
(* variables *) 
1060 

10381  1061 
local 
1062 

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

1063 
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

1064 
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

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

1066 
val x = Syntax.const_name raw_x raw_mx; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1067 
val mx = Syntax.fix_mixfix raw_x raw_mx; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1068 
val _ = 
18678  1069 
if not legacy andalso not (Syntax.is_identifier (no_skolem internal x)) then 
1070 
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

1071 
else (); 
12504  1072 

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

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

1074 
if internal then T 
18678  1075 
else Type.no_tvars T handle TYPE (msg, _, _) => error msg; 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1076 
val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1077 
val var = (x, opt_T, mx); 
19001  1078 
in (var, ctxt > declare_var var > #2) end); 
8096  1079 

10381  1080 
in 
1081 

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

1082 
val read_vars = prep_vars read_typ false false; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1083 
val cert_vars = prep_vars cert_typ true false; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1084 
val read_vars_legacy = prep_vars read_typ true true; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1085 
val cert_vars_legacy = prep_vars cert_typ true true; 
8096  1086 

10381  1087 
end; 
1088 

8096  1089 

19001  1090 
(* abbreviations *) 
1091 

1092 
local 

1093 

1094 
fun gen_abbrevs prep_vars prep_term revert = fold (fn (raw_c, raw_t, raw_mx) => fn ctxt => 

1095 
let 

19019  1096 
val thy = theory_of ctxt and naming = naming_of ctxt; 
19001  1097 
val ([(c, _, mx)], _) = prep_vars [(raw_c, NONE, raw_mx)] ctxt; 
1098 
val [t] = polymorphic ctxt [prep_term ctxt raw_t]; 

19019  1099 
val T = Term.fastype_of t; 
19001  1100 
val _ = 
19270  1101 
if null (hidden_polymorphism t T) then () 
19001  1102 
else error ("Extra type variables on rhs of abbreviation: " ^ quote c); 
1103 
in 

1104 
ctxt 

1105 
> declare_term t 

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

1106 
> map_consts (apsnd (Consts.abbreviate (pp ctxt) (tsig_of ctxt) naming revert (c, t))) 
19019  1107 
> map_syntax (LocalSyntax.add_syntax thy [(false, (NameSpace.full naming c, T, mx))]) 
19001  1108 
end); 
1109 

1110 
in 

1111 

1112 
val add_abbrevs = gen_abbrevs read_vars read_term; 

1113 
val add_abbrevs_i = gen_abbrevs cert_vars cert_term; 

1114 

1115 
end; 

1116 

1117 

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

1118 
(* fixes *) 
5819  1119 

8096  1120 
local 
1121 

19001  1122 
fun prep_mixfix (x, T, mx) = 
19019  1123 
if mx <> NoSyn andalso mx <> Structure andalso 
1124 
(can Syntax.dest_internal x orelse can Syntax.dest_skolem x) then 

19001  1125 
error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x) 
1126 
else (true, (x, T, mx)); 

1127 

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

1128 
fun no_dups _ [] = () 
18900  1129 
 no_dups ctxt dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups); 
11925  1130 

18844  1131 
fun gen_fixes prep raw_vars ctxt = 
8096  1132 
let 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1133 
val (ys, zs) = split_list (fixes_of ctxt); 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1134 
val (vars, ctxt') = prep raw_vars ctxt; 
12130
30d9143aff7e
syntactic declaration of external *and* internal versions of fixes;
wenzelm
parents:
12123
diff
changeset

1135 
val xs = map #1 vars; 
18971  1136 
val _ = no_dups ctxt (duplicates (op =) xs); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

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

1138 
if is_body ctxt then Term.variantlist (map Syntax.skolem xs, zs) 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1139 
else (no_dups ctxt (xs inter_string ys); no_dups ctxt (xs inter_string zs); xs); 
8096  1140 
in 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

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

1142 
> map_fixes (fn (b, fixes) => (b, rev (xs ~~ xs') @ fixes)) 
19001  1143 
> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) 
19019  1144 
> (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

1145 
> pair xs' 
8096  1146 
end; 
5819  1147 

8096  1148 
in 
7679  1149 

18844  1150 
val add_fixes = gen_fixes read_vars; 
1151 
val add_fixes_i = gen_fixes cert_vars; 

1152 
val add_fixes_legacy = gen_fixes cert_vars_legacy; 

8096  1153 

1154 
end; 

5819  1155 

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

1156 

18844  1157 
(* invent fixes *) 
1158 

1159 
fun invent_fixes xs ctxt = 

1160 
ctxt 

1161 
> set_body true 

1162 
> add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs) 

1163 
> restore_body ctxt; 

1164 

1165 

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

1166 
(* fixes vs. frees *) 
12016  1167 

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

1168 
fun fix_frees t ctxt = 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

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

1170 
fun add (Free (x, T)) = if is_fixed ctxt x then I else insert (op =) (x, SOME T, NoSyn) 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

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

1172 
val fixes = rev (fold_aterms add t []); 
18809  1173 
in 
1174 
ctxt 

1175 
> declare_term t 

1176 
> set_body false 

1177 
> (snd o add_fixes_i fixes) 

1178 
> restore_body ctxt 

1179 
end; 

6895  1180 

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

1181 
fun auto_fixes (arg as (ctxt, (propss, x))) = 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1182 
if is_body ctxt then arg 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1183 
else ((fold o fold) fix_frees propss ctxt, (propss, x)); 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1184 

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

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

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

1187 
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

1188 
fun bind (t as Free (x, T)) = 
18340  1189 
if member (op =) xs x then 
15531  1190 
(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

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

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

1193 
 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

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

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

1196 

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

1197 

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

1198 

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

1199 
(** assumptions **) 
18187  1200 

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

1201 
(* generic assms *) 
18187  1202 

1203 
local 

1204 

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

1205 
fun gen_assm ((name, attrs), props) ctxt = 
18187  1206 
let 
1207 
val cprops = map (Thm.cterm_of (theory_of ctxt)) props; 

1208 
val asms = map (Goal.norm_hhf o Thm.assume) cprops; 

1209 

1210 
val ths = map (fn th => ([th], [])) asms; 

1211 
val ([(_, thms)], ctxt') = 

1212 
ctxt 

1213 
> auto_bind_facts props 

1214 
> note_thmss_i [((name, attrs), ths)]; 

1215 
in ((cprops, (name, asms), (name, thms)), ctxt') end; 

1216 

1217 
fun gen_assms prepp exp args ctxt = 

1218 
let 

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

1219 
val (propss, ctxt1) = swap (prepp (ctxt, map snd args)); 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1220 
val (results, ctxt2) = fold_map gen_assm (map fst args ~~ propss) ctxt1; 
18187  1221 

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

1222 
val new_asms = List.concat (map #1 results); 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1223 
val new_prems = map #2 results; 
18809  1224 
val ctxt3 = ctxt2 
1225 
> map_assms (fn (asms, prems) => (asms @ [(new_asms, exp)], prems @ new_prems)) 

1226 
val ctxt4 = ctxt3 

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

1227 
> put_thms_internal (AutoBind.premsN, SOME (prems_of ctxt3)); 
18672
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1228 
in (map #3 results, warn_extra_tfrees ctxt ctxt4) end; 
18187  1229 

1230 
in 

1231 

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

1232 
val add_assms = gen_assms (apsnd #1 o bind_propp); 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1233 
val add_assms_i = gen_assms (apsnd #1 o bind_propp_i); 
18187  1234 

1235 
end; 

1236 

1237 

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

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

1239 

18879  1240 
(* 
1241 
[A] 

18971  1242 
: 
18879  1243 
B 
1244 
 

1245 
#A ==> B 

1246 
*) 

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

1247 
fun assume_export true = Seq.single oo Drule.implies_intr_protected 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
changeset

1248 
 assume_export false = Seq.single oo Drule.implies_intr_list; 
ac1a048ca7dd
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
wenzelm
parents:
18619
diff
