author  wenzelm 
Mon, 03 Jun 2019 21:47:54 +0200  
changeset 70311  e49bf4ebf330 
parent 70308  7f568724d67e 
child 70586  57df8a85317a 
permissions  rwrr 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/variable.ML 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

3 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

4 
Fixed type/term variables and polymorphic term abbreviations. 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

5 
*) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

6 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

7 
signature VARIABLE = 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

8 
sig 
20303  9 
val names_of: Proof.context > Name.context 
10 
val binds_of: Proof.context > (typ * term) Vartab.table 

24765  11 
val maxidx_of: Proof.context > int 
20303  12 
val constraints_of: Proof.context > typ Vartab.table * sort Vartab.table 
13 
val is_declared: Proof.context > string > bool 

42494  14 
val check_name: binding > string 
20303  15 
val default_type: Proof.context > string > typ option 
16 
val def_type: Proof.context > bool > indexname > typ option 

17 
val def_sort: Proof.context > indexname > sort option 

59646  18 
val declare_maxidx: int > Proof.context > Proof.context 
27280  19 
val declare_names: term > Proof.context > Proof.context 
20303  20 
val declare_constraints: term > Proof.context > Proof.context 
62012
12d3edd62932
more precise context  potentially relevant for Eisbach dummy thm;
wenzelm
parents:
61949
diff
changeset

21 
val declare_internal: term > Proof.context > Proof.context 
20303  22 
val declare_term: term > Proof.context > Proof.context 
27280  23 
val declare_typ: typ > Proof.context > Proof.context 
20303  24 
val declare_prf: Proofterm.proof > Proof.context > Proof.context 
25 
val declare_thm: thm > Proof.context > Proof.context 

26 
val variant_frees: Proof.context > term list > (string * 'a) list > (string * 'a) list 

60401  27 
val bind_term: indexname * term > Proof.context > Proof.context 
28 
val unbind_term: indexname > Proof.context > Proof.context 

29 
val maybe_bind_term: indexname * term option > Proof.context > Proof.context 

20303  30 
val expand_binds: Proof.context > term > term 
25325  31 
val lookup_const: Proof.context > string > string option 
25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

32 
val is_const: Proof.context > string > bool 
25325  33 
val declare_const: string * string > Proof.context > Proof.context 
55635  34 
val next_bound: string * typ > Proof.context > term * Proof.context 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

35 
val revert_bounds: Proof.context > term > term 
59798  36 
val is_body: Proof.context > bool 
37 
val set_body: bool > Proof.context > Proof.context 

38 
val restore_body: Proof.context > Proof.context > Proof.context 

59790  39 
val improper_fixes: Proof.context > Proof.context 
40 
val restore_proper_fixes: Proof.context > Proof.context > Proof.context 

41 
val is_improper: Proof.context > string > bool 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

42 
val is_fixed: Proof.context > string > bool 
59846  43 
val is_newly_fixed: Proof.context > Proof.context > string > bool 
42493
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset

44 
val fixed_ord: Proof.context > string * string > order 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

45 
val intern_fixed: Proof.context > string > string 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

46 
val lookup_fixed: Proof.context > string > string option 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

47 
val revert_fixed: Proof.context > string > string 
62987
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

48 
val markup_fixed: Proof.context > string > Markup.T 
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

49 
val markup: Proof.context > string > Markup.T 
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

50 
val markup_entity_def: Proof.context > string > Markup.T 
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

51 
val dest_fixes: Proof.context > (string * string) list 
42482  52 
val add_fixed_names: Proof.context > term > string list > string list 
53 
val add_fixed: Proof.context > term > (string * typ) list > (string * typ) list 

59846  54 
val add_newly_fixed: Proof.context > Proof.context > 
55 
term > (string * typ) list > (string * typ) list 

42482  56 
val add_free_names: Proof.context > term > string list > string list 
57 
val add_frees: Proof.context > term > (string * typ) list > (string * typ) list 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

58 
val add_fixes_binding: binding list > Proof.context > string list * Proof.context 
20303  59 
val add_fixes: string list > Proof.context > string list * Proof.context 
60 
val add_fixes_direct: string list > Proof.context > Proof.context 

59796  61 
val fix_dummy_patterns: term > Proof.context > term * Proof.context 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20579
diff
changeset

62 
val variant_fixes: string list > Proof.context > string list * Proof.context 
60822  63 
val gen_all: Proof.context > thm > thm 
20303  64 
val export_terms: Proof.context > Proof.context > term list > term list 
65 
val exportT_terms: Proof.context > Proof.context > term list > term list 

66 
val exportT: Proof.context > Proof.context > thm list > thm list 

67 
val export_prf: Proof.context > Proof.context > Proofterm.proof > Proofterm.proof 

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

21522  69 
val export_morphism: Proof.context > Proof.context > morphism 
59796  70 
val invent_types: sort list > Proof.context > (string * sort) list * Proof.context 
20303  71 
val importT_inst: term list > Proof.context > ((indexname * sort) * typ) list * Proof.context 
72 
val import_inst: bool > term list > Proof.context > 

73 
(((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context 

74 
val importT_terms: term list > Proof.context > term list * Proof.context 

75 
val import_terms: bool > term list > Proof.context > term list * Proof.context 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60401
diff
changeset

76 
val importT: thm list > Proof.context > 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60401
diff
changeset

77 
(((indexname * sort) * ctyp) list * thm list) * Proof.context 
20303  78 
val import_prf: bool > Proofterm.proof > Proof.context > Proofterm.proof * Proof.context 
31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30756
diff
changeset

79 
val import: bool > thm list > Proof.context > 
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60401
diff
changeset

80 
((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context 
70304  81 
val import_vars: Proof.context > thm > thm 
21287  82 
val tradeT: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 
83 
val trade: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 

60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

84 
val is_bound_focus: Proof.context > bool 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

85 
val set_bound_focus: bool > Proof.context > Proof.context 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

86 
val restore_bound_focus: Proof.context > Proof.context > Proof.context 
60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

87 
val focus_params: binding list option > term > Proof.context > 
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

88 
(string list * (string * typ) list) * Proof.context 
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

89 
val focus: binding list option > term > Proof.context > 
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

90 
((string * (string * typ)) list * term) * Proof.context 
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

91 
val focus_cterm: binding list option > cterm > Proof.context > 
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

92 
((string * cterm) list * cterm) * Proof.context 
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

93 
val focus_subgoal: binding list option > int > thm > Proof.context > 
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

94 
((string * cterm) list * cterm) * Proof.context 
20303  95 
val warn_extra_tfrees: Proof.context > Proof.context > unit 
24694  96 
val polymorphic_types: Proof.context > term list > (indexname * sort) list * term list 
20303  97 
val polymorphic: Proof.context > term list > term list 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

98 
end; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

99 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

100 
structure Variable: VARIABLE = 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

101 
struct 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

102 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

103 
(** local context data **) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

104 

59790  105 
type fixes = (string * bool) Name_Space.table; 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49688
diff
changeset

106 
val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN; 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

107 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

108 
datatype data = Data of 
59798  109 
{names: Name.context, (*type/term variable names*) 
25325  110 
consts: string Symtab.table, (*consts within the local scope*) 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

111 
bounds: int * ((string * typ) * string) list, (*next index, internal name, type, external name*) 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

112 
fixes: fixes, (*term fixes  global name space, intern ~> extern*) 
20102  113 
binds: (typ * term) Vartab.table, (*term bindings*) 
20162  114 
type_occs: string list Symtab.table, (*type variables  possibly within term variables*) 
24765  115 
maxidx: int, (*maximum var index*) 
20162  116 
constraints: 
20102  117 
typ Vartab.table * (*type constraints*) 
20162  118 
sort Vartab.table}; (*default sorts*) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

119 

61508  120 
fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) = 
59798  121 
Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds, 
61508  122 
type_occs = type_occs, maxidx = maxidx, constraints = constraints}; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

123 

59150  124 
val empty_data = 
59798  125 
make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, 
61508  126 
Symtab.empty, ~1, (Vartab.empty, Vartab.empty)); 
59150  127 

33519  128 
structure Data = Proof_Data 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

129 
( 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

130 
type T = data; 
59150  131 
fun init _ = empty_data; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

132 
); 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

133 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

134 
fun map_data f = 
61508  135 
Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, constraints} => 
136 
make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints))); 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

137 

17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

138 
fun map_names f = 
61508  139 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 
140 
(f names, consts, bounds, fixes, binds, type_occs, maxidx, constraints)); 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

141 

25325  142 
fun map_consts f = 
61508  143 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 
144 
(names, f consts, bounds, fixes, binds, type_occs, maxidx, constraints)); 

55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

145 

a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

146 
fun map_bounds f = 
61508  147 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 
148 
(names, consts, f bounds, fixes, binds, type_occs, maxidx, constraints)); 

20162  149 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

150 
fun map_fixes f = 
61508  151 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 
152 
(names, consts, bounds, f fixes, binds, type_occs, maxidx, constraints)); 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

153 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

154 
fun map_binds f = 
61508  155 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 
156 
(names, consts, bounds, fixes, f binds, type_occs, maxidx, constraints)); 

24765  157 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

158 
fun map_type_occs f = 
61508  159 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 
160 
(names, consts, bounds, fixes, binds, f type_occs, maxidx, constraints)); 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

161 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

162 
fun map_maxidx f = 
61508  163 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 
164 
(names, consts, bounds, fixes, binds, type_occs, f maxidx, constraints)); 

20102  165 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

166 
fun map_constraints f = 
61508  167 
map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 
168 
(names, consts, bounds, fixes, binds, type_occs, maxidx, f constraints)); 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

169 

45650  170 
fun rep_data ctxt = Data.get ctxt > (fn Data rep => rep); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

171 

20102  172 
val names_of = #names o rep_data; 
173 
val fixes_of = #fixes o rep_data; 

56025  174 
val fixes_space = Name_Space.space_of_table o fixes_of; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

175 
val binds_of = #binds o rep_data; 
20162  176 
val type_occs_of = #type_occs o rep_data; 
24765  177 
val maxidx_of = #maxidx o rep_data; 
20162  178 
val constraints_of = #constraints o rep_data; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

179 

20162  180 
val is_declared = Name.is_declared o names_of; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

181 

47021
f35f654f297d
clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
wenzelm
parents:
47005
diff
changeset

182 
val check_name = Name_Space.base_name o tap Binding.check; 
42357  183 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

184 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

185 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

186 
(** declarations **) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

187 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

188 
(* default sorts and types *) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

189 

20162  190 
fun default_type ctxt x = Vartab.lookup (#1 (constraints_of ctxt)) (x, ~1); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

191 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

192 
fun def_type ctxt pattern xi = 
20162  193 
let val {binds, constraints = (types, _), ...} = rep_data ctxt in 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

194 
(case Vartab.lookup types xi of 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

195 
NONE => 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

196 
if pattern then NONE 
39290
44e4d8dfd6bf
load type_infer.ML later  proper context for Type_Infer.infer_types;
wenzelm
parents:
38831
diff
changeset

197 
else Vartab.lookup binds xi > Option.map (Type.mark_polymorphic o #1) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

198 
 some => some) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

199 
end; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

200 

20162  201 
val def_sort = Vartab.lookup o #2 o constraints_of; 
202 

203 

59646  204 
(* maxidx *) 
205 

206 
val declare_maxidx = map_maxidx o Integer.max; 

207 

208 

20162  209 
(* names *) 
210 

24765  211 
fun declare_type_names t = 
29279  212 
map_names (fold_types (fold_atyps Term.declare_typ_names) t) #> 
24765  213 
map_maxidx (fold_types Term.maxidx_typ t); 
20162  214 

215 
fun declare_names t = 

216 
declare_type_names t #> 

29279  217 
map_names (fold_aterms Term.declare_term_frees t) #> 
24765  218 
map_maxidx (Term.maxidx_term t); 
20162  219 

220 

221 
(* type occurrences *) 

222 

24719
21d1cdab2d8c
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
wenzelm
parents:
24694
diff
changeset

223 
fun decl_type_occsT T = fold_atyps (fn TFree (a, _) => Symtab.default (a, [])  _ => I) T; 
21d1cdab2d8c
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
wenzelm
parents:
24694
diff
changeset

224 

22671  225 
val decl_type_occs = fold_term_types 
20162  226 
(fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x)  _ => I) 
24719
21d1cdab2d8c
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
wenzelm
parents:
24694
diff
changeset

227 
 _ => decl_type_occsT); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

228 

24719
21d1cdab2d8c
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
wenzelm
parents:
24694
diff
changeset

229 
val declare_type_occsT = map_type_occs o fold_types decl_type_occsT; 
22671  230 
val declare_type_occs = map_type_occs o decl_type_occs; 
231 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

232 

20162  233 
(* constraints *) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

234 

49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

235 
fun constrain_tvar (xi, raw_S) = 
49688  236 
let val S = #2 (Term_Position.decode_positionS raw_S) 
49685
4341e4d86872
allow position constraints to coexist with 0 or 1 sort constraints;
wenzelm
parents:
49674
diff
changeset

237 
in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end; 
21355  238 

20162  239 
fun declare_constraints t = map_constraints (fn (types, sorts) => 
240 
let 

241 
val types' = fold_aterms 

62955
2fd4378caca2
back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;
wenzelm
parents:
62771
diff
changeset

242 
(fn Free (x, T) => Vartab.update ((x, ~1), T) 
2fd4378caca2
back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;
wenzelm
parents:
62771
diff
changeset

243 
 Var v => Vartab.update v 
20162  244 
 _ => I) t types; 
45426  245 
val sorts' = (fold_types o fold_atyps) 
21355  246 
(fn TFree (x, S) => constrain_tvar ((x, ~1), S) 
247 
 TVar v => constrain_tvar v 

45426  248 
 _ => I) t sorts; 
20162  249 
in (types', sorts') end) 
24719
21d1cdab2d8c
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
wenzelm
parents:
24694
diff
changeset

250 
#> declare_type_occsT t 
22711  251 
#> declare_type_names t; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

252 

20162  253 

254 
(* common declarations *) 

255 

256 
fun declare_internal t = 

257 
declare_names t #> 

28625  258 
declare_type_occs t #> 
61508  259 
Thm.declare_term_sorts t; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

260 

20162  261 
fun declare_term t = 
262 
declare_internal t #> 

263 
declare_constraints t; 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

264 

27280  265 
val declare_typ = declare_term o Logic.mk_type; 
266 

20303  267 
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type); 
268 

22691  269 
val declare_thm = Thm.fold_terms declare_internal; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

270 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

271 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

272 
(* renaming term/type frees *) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

273 

20162  274 
fun variant_frees ctxt ts frees = 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

275 
let 
20162  276 
val names = names_of (fold declare_names ts ctxt); 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42495
diff
changeset

277 
val xs = fst (fold_map Name.variant (map #1 frees) names); 
20084  278 
in xs ~~ map snd frees end; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

279 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

280 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

281 

20303  282 
(** term bindings **) 
283 

60401  284 
fun bind_term ((x, i), t) = 
285 
let 

286 
val u = Term.close_schematic_term t; 

287 
val U = Term.fastype_of u; 

288 
in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end; 

289 

290 
val unbind_term = map_binds o Vartab.delete_safe; 

291 

292 
fun maybe_bind_term (xi, SOME t) = bind_term (xi, t) 

293 
 maybe_bind_term (xi, NONE) = unbind_term xi; 

20303  294 

295 
fun expand_binds ctxt = 

296 
let 

297 
val binds = binds_of ctxt; 

21799  298 
val get = fn Var (xi, _) => Vartab.lookup binds xi  _ => NONE; 
299 
in Envir.beta_norm o Envir.expand_term get end; 

20303  300 

301 

302 

25325  303 
(** consts **) 
25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

304 

25325  305 
val lookup_const = Symtab.lookup o #consts o rep_data; 
306 
val is_const = is_some oo lookup_const; 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

307 

25325  308 
val declare_fixed = map_consts o Symtab.delete_safe; 
309 
val declare_const = map_consts o Symtab.update; 

25316
17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

310 

17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

311 

17c183417f93
added is_const/declare_const for local scope of fixes/consts;
wenzelm
parents:
25051
diff
changeset

312 

55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

313 
(** bounds **) 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

314 

a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

315 
fun next_bound (a, T) ctxt = 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

316 
let 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

317 
val b = Name.bound (#1 (#bounds (rep_data ctxt))); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

318 
val ctxt' = ctxt > map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds)); 
55635  319 
in (Free (b, T), ctxt') end; 
55014
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

320 

a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

321 
fun revert_bounds ctxt t = 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

322 
(case #2 (#bounds (rep_data ctxt)) of 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

323 
[] => t 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

324 
 bounds => 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

325 
let 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

326 
val names = Term.declare_term_names t (names_of ctxt); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

327 
val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names)); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

328 
fun subst ((b, T), _) x' = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T)); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

329 
in Term.subst_atomic (map2 subst bounds xs) t end); 
a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

330 

a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

331 

a93f496f6c30
general notion of auxiliary bounds within context;
wenzelm
parents:
54740
diff
changeset

332 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

333 
(** fixes **) 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

334 

59798  335 
(* inner body mode *) 
336 

69575  337 
val inner_body = Config.declare_bool ("inner_body", \<^here>) (K false); 
69576  338 
val is_body = Config.apply inner_body; 
59798  339 
val set_body = Config.put inner_body; 
69576  340 
val restore_body = set_body o is_body; 
59798  341 

342 

59790  343 
(* proper mode *) 
344 

69575  345 
val proper_fixes = Config.declare_bool ("proper_fixes", \<^here>) (K true); 
59790  346 
val improper_fixes = Config.put proper_fixes false; 
69576  347 
val restore_proper_fixes = Config.put proper_fixes o Config.apply proper_fixes; 
59790  348 

349 
fun is_improper ctxt x = 

59884  350 
(case Name_Space.lookup (fixes_of ctxt) x of 
351 
SOME (_, proper) => not proper 

59790  352 
 NONE => false); 
353 

354 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

355 
(* specialized name space *) 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

356 

59883  357 
val is_fixed = Name_Space.defined o fixes_of; 
59846  358 
fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer); 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

359 

42493
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset

360 
val fixed_ord = Name_Space.entry_ord o fixes_space; 
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset

361 
val intern_fixed = Name_Space.intern o fixes_space; 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

362 

4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

363 
fun lookup_fixed ctxt x = 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

364 
let val x' = intern_fixed ctxt x 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

365 
in if is_fixed ctxt x' then SOME x' else NONE end; 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

366 

4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

367 
fun revert_fixed ctxt x = 
59884  368 
(case Name_Space.lookup (fixes_of ctxt) x of 
369 
SOME (x', _) => if intern_fixed ctxt x' = x then x' else x 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

370 
 NONE => x); 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

371 

45472  372 
fun markup_fixed ctxt x = 
373 
Name_Space.markup (fixes_space ctxt) x 

374 
> Markup.name (revert_fixed ctxt x); 

375 

62987
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

376 
fun markup ctxt x = 
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

377 
if is_improper ctxt x then Markup.improper 
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

378 
else if Name.is_skolem x then Markup.skolem 
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

379 
else Markup.free; 
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

380 

dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

381 
val markup_entity_def = Name_Space.markup_def o fixes_space; 
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62955
diff
changeset

382 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

383 
fun dest_fixes ctxt = 
59790  384 
Name_Space.fold_table (fn (x, (y, _)) => cons (y, x)) (fixes_of ctxt) [] 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58668
diff
changeset

385 
> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2); 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

386 

4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

387 

42482  388 
(* collect variables *) 
389 

390 
fun add_free_names ctxt = 

391 
fold_aterms (fn Free (x, _) => not (is_fixed ctxt x) ? insert (op =) x  _ => I); 

392 

393 
fun add_frees ctxt = 

394 
fold_aterms (fn Free (x, T) => not (is_fixed ctxt x) ? insert (op =) (x, T)  _ => I); 

395 

396 
fun add_fixed_names ctxt = 

397 
fold_aterms (fn Free (x, _) => is_fixed ctxt x ? insert (op =) x  _ => I); 

398 

399 
fun add_fixed ctxt = 

400 
fold_aterms (fn Free (x, T) => is_fixed ctxt x ? insert (op =) (x, T)  _ => I); 

401 

59846  402 
fun add_newly_fixed ctxt' ctxt = 
403 
fold_aterms (fn Free (x, T) => is_newly_fixed ctxt' ctxt x ? insert (op =) (x, T)  _ => I); 

404 

42482  405 

406 
(* declarations *) 

407 

20084  408 
local 
409 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

410 
fun err_dups dups = 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

411 
error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups)); 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

412 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

413 
fun new_fixed ((x, x'), pos) ctxt = 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

414 
if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)] 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

415 
else 
59790  416 
let 
417 
val proper = Config.get ctxt proper_fixes; 

61949  418 
val context = Context.Proof ctxt 
419 
> Name_Space.map_naming (K Name_Space.global_naming) 

420 
> Context_Position.set_visible_generic false; 

59790  421 
in 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

422 
ctxt 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

423 
> map_fixes 
59790  424 
(Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #> 
58668  425 
Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x') 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

426 
> declare_fixed x 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

427 
> declare_constraints (Syntax.free x') 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

428 
end; 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

429 

4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

430 
fun new_fixes names' xs xs' ps = 
20102  431 
map_names (K names') #> 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

432 
fold new_fixed ((xs ~~ xs') ~~ ps) #> 
20084  433 
pair xs'; 
434 

435 
in 

436 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

437 
fun add_fixes_binding bs ctxt = 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

438 
let 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

439 
val _ = 
55948  440 
(case filter (Name.is_skolem o Binding.name_of) bs of 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

441 
[] => () 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

442 
 bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads))); 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

443 
val _ = 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58668
diff
changeset

444 
(case duplicates (op = o apply2 Binding.name_of) bs of 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

445 
[] => () 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

446 
 dups => err_dups dups); 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

447 

42494  448 
val xs = map check_name bs; 
20102  449 
val names = names_of ctxt; 
20084  450 
val (xs', names') = 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42495
diff
changeset

451 
if is_body ctxt then fold_map Name.variant xs names >> map Name.skolem 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

452 
else (xs, fold Name.declare xs names); 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

453 
in ctxt > new_fixes names' xs xs' (map Binding.pos_of bs) end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

454 

60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

455 
fun bound_fixes xs ctxt = 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

456 
let 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

457 
val (xs', ctxt') = fold_map next_bound xs ctxt; 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

458 
val no_ps = replicate (length xs) Position.none; 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

459 
in ctxt' > new_fixes (names_of ctxt') (map #1 xs) (map (#1 o dest_Free) xs') no_ps end; 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

460 

20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20579
diff
changeset

461 
fun variant_fixes raw_xs ctxt = 
20084  462 
let 
20102  463 
val names = names_of ctxt; 
55948  464 
val xs = map (fn x => Name.clean x > Name.is_internal x ? Name.internal) raw_xs; 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42495
diff
changeset

465 
val (xs', names') = fold_map Name.variant xs names >> (is_body ctxt ? map Name.skolem); 
60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

466 
val no_ps = replicate (length xs) Position.none; 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

467 
in ctxt > new_fixes names' xs xs' no_ps end; 
20084  468 

469 
end; 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

470 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

471 
val add_fixes = add_fixes_binding o map Binding.name; 
20251  472 

473 
fun add_fixes_direct xs ctxt = ctxt 

474 
> set_body false 

475 
> (snd o add_fixes xs) 

476 
> restore_body ctxt; 

477 

59796  478 

479 
(* dummy patterns *) 

480 

481 
fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt = 

61923
a10cc7fb1841
clarified context policy to allow multiple dummies;
wenzelm
parents:
61508
diff
changeset

482 
let val ([x], ctxt') = ctxt > set_body true > add_fixes [Name.uu_] > restore_body ctxt 
59796  483 
in (Free (x, T), ctxt') end 
484 
 fix_dummy_patterns (Abs (x, T, b)) ctxt = 

485 
let val (b', ctxt') = fix_dummy_patterns b ctxt 

486 
in (Abs (x, T, b'), ctxt') end 

487 
 fix_dummy_patterns (t $ u) ctxt = 

488 
let 

489 
val (t', ctxt') = fix_dummy_patterns t ctxt; 

490 
val (u', ctxt'') = fix_dummy_patterns u ctxt'; 

491 
in (t' $ u', ctxt'') end 

492 
 fix_dummy_patterns a ctxt = (a, ctxt); 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

493 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

494 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

495 

22671  496 
(** export  generalize type/term variables (beware of closure sizes) **) 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

497 

60823  498 
fun gen_all ctxt th = 
499 
let 

500 
val i = Thm.maxidx_thm th (maxidx_of ctxt) + 1; 

501 
fun gen (x, T) = Thm.forall_elim (Thm.cterm_of ctxt (Var ((x, i), T))); 

502 
in fold gen (Drule.outer_params (Thm.prop_of th)) th end; 

60822  503 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

504 
fun export_inst inner outer = 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

505 
let 
20162  506 
val declared_outer = is_declared outer; 
59846  507 
val still_fixed = not o is_newly_fixed inner outer; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

508 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

509 
val gen_fixes = 
56025  510 
Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y) 
511 
(fixes_of inner) []; 

22671  512 

513 
val type_occs_inner = type_occs_of inner; 

514 
fun gen_fixesT ts = 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

515 
Symtab.fold (fn (a, xs) => 
20162  516 
if declared_outer a orelse exists still_fixed xs 
22671  517 
then I else cons a) (fold decl_type_occs ts type_occs_inner) []; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

518 
in (gen_fixesT, gen_fixes) end; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

519 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

520 
fun exportT_inst inner outer = #1 (export_inst inner outer); 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

521 

22671  522 
fun exportT_terms inner outer = 
59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

523 
let 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

524 
val mk_tfrees = exportT_inst inner outer; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

525 
val maxidx = maxidx_of outer; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

526 
in 
22671  527 
fn ts => ts > map 
31977  528 
(Term_Subst.generalize (mk_tfrees ts, []) 
59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

529 
(fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1)) 
22671  530 
end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

531 

22671  532 
fun export_terms inner outer = 
59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

533 
let 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

534 
val (mk_tfrees, tfrees) = export_inst inner outer; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

535 
val maxidx = maxidx_of outer; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

536 
in 
22671  537 
fn ts => ts > map 
31977  538 
(Term_Subst.generalize (mk_tfrees ts, tfrees) 
59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

539 
(fold Term.maxidx_term ts maxidx + 1)) 
22671  540 
end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

541 

20303  542 
fun export_prf inner outer prf = 
543 
let 

22671  544 
val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer; 
545 
val tfrees = mk_tfrees []; 

59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

546 
val maxidx = maxidx_of outer; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

547 
val idx = Proofterm.maxidx_proof prf maxidx + 1; 
36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36610
diff
changeset

548 
val gen_term = Term_Subst.generalize_same (tfrees, frees) idx; 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36610
diff
changeset

549 
val gen_typ = Term_Subst.generalizeT_same tfrees idx; 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36610
diff
changeset

550 
in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end; 
20303  551 

22671  552 

59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

553 
fun gen_export (mk_tfrees, frees) maxidx ths = 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

554 
let 
22671  555 
val tfrees = mk_tfrees (map Thm.full_prop_of ths); 
59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

556 
val idx = fold Thm.maxidx_thm ths maxidx + 1; 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

557 
in map (Thm.generalize (tfrees, frees) idx) ths end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

558 

59645
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

559 
fun exportT inner outer = gen_export (exportT_inst inner outer, []) (maxidx_of outer); 
f89464e9ffa0
clarified Variable.export: observe maxidx of target context;
wenzelm
parents:
59623
diff
changeset

560 
fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer); 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

561 

21522  562 
fun export_morphism inner outer = 
563 
let 

564 
val fact = export inner outer; 

565 
val term = singleton (export_terms inner outer); 

566 
val typ = Logic.type_map term; 

54740  567 
in 
70311  568 
Morphism.transfer_morphism' inner $> 
569 
Morphism.transfer_morphism' outer $> 

54740  570 
Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]} 
571 
end; 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

572 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

573 

24765  574 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

575 
(** import  fix schematic type/term variables **) 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

576 

59796  577 
fun invent_types Ss ctxt = 
578 
let 

579 
val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; 

580 
val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; 

581 
in (tfrees, ctxt') end; 

582 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

583 
fun importT_inst ts ctxt = 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

584 
let 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

585 
val tvars = rev (fold Term.add_tvars ts []); 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

586 
val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

587 
in (tvars ~~ map TFree tfrees, ctxt') end; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

588 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

589 
fun import_inst is_open ts ctxt = 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

590 
let 
26714
4773b832f1b1
variant_fixes: preserve internal state, mark skolem only for body mode;
wenzelm
parents:
25573
diff
changeset

591 
val ren = Name.clean #> (if is_open then I else Name.internal); 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

592 
val (instT, ctxt') = importT_inst ts ctxt; 
31977  593 
val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts [])); 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20579
diff
changeset

594 
val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt'; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

595 
val inst = vars ~~ map Free (xs ~~ map #2 vars); 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

596 
in ((instT, inst), ctxt'') end; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

597 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

598 
fun importT_terms ts ctxt = 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

599 
let val (instT, ctxt') = importT_inst ts ctxt 
31977  600 
in (map (Term_Subst.instantiate (instT, [])) ts, ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

601 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

602 
fun import_terms is_open ts ctxt = 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

603 
let val (inst, ctxt') = import_inst is_open ts ctxt 
31977  604 
in (map (Term_Subst.instantiate inst) ts, ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

605 

31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30756
diff
changeset

606 
fun importT ths ctxt = 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

607 
let 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

608 
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; 
60805  609 
val instT' = map (apsnd (Thm.ctyp_of ctxt')) instT; 
610 
val ths' = map (Thm.instantiate (instT', [])) ths; 

32280
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

611 
in ((instT', ths'), ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

612 

20303  613 
fun import_prf is_open prf ctxt = 
614 
let 

615 
val ts = rev (Proofterm.fold_proof_terms cons (cons o Logic.mk_type) prf []); 

616 
val (insts, ctxt') = import_inst is_open ts ctxt; 

617 
in (Proofterm.instantiate insts prf, ctxt') end; 

618 

31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30756
diff
changeset

619 
fun import is_open ths ctxt = 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

620 
let 
60805  621 
val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; 
622 
val insts' = 

623 
(map (apsnd (Thm.ctyp_of ctxt')) instT, 

624 
map (apsnd (Thm.cterm_of ctxt')) inst); 

32280
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

625 
val ths' = map (Thm.instantiate insts') ths; 
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

626 
in ((insts', ths'), ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

627 

70304  628 
fun import_vars ctxt th = 
629 
let val ((_, [th']), _) = ctxt > set_body false > import true [th]; 

630 
in th' end; 

631 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

632 

19926  633 
(* import/export *) 
634 

21287  635 
fun gen_trade imp exp f ctxt ths = 
20220  636 
let val ((_, ths'), ctxt') = imp ths ctxt 
21287  637 
in exp ctxt' ctxt (f ctxt' ths') end; 
19926  638 

31794
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30756
diff
changeset

639 
val tradeT = gen_trade importT exportT; 
71af1fd6a5e4
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef  Alice is no longer supported);
wenzelm
parents:
30756
diff
changeset

640 
val trade = gen_trade (import true) export; 
19926  641 

642 

67721  643 
(* focus on outermost parameters: \<And>x y z. B *) 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

644 

69575  645 
val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false); 
69576  646 
val is_bound_focus = Config.apply bound_focus; 
60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

647 
val set_bound_focus = Config.put bound_focus; 
69576  648 
val restore_bound_focus = set_bound_focus o is_bound_focus; 
60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

649 

60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

650 
fun focus_params bindings t ctxt = 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

651 
let 
60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

652 
val ps = Term.variant_frees t (Term.strip_all_vars t); (*as they are printed :*) 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

653 
val (xs, Ts) = split_list ps; 
60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

654 
val (xs', ctxt') = 
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

655 
(case bindings of 
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

656 
SOME bs => ctxt > set_body true > add_fixes_binding bs > restore_body ctxt 
60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

657 
 NONE => if is_bound_focus ctxt then bound_fixes ps ctxt else variant_fixes xs ctxt); 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

658 
val ps' = xs' ~~ Ts; 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

659 
val ctxt'' = ctxt' > fold (declare_constraints o Free) ps'; 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60695
diff
changeset

660 
in ((xs, ps'), ctxt'') end; 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

661 

60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

662 
fun focus bindings t ctxt = 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

663 
let 
60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

664 
val ((xs, ps), ctxt') = focus_params bindings t ctxt; 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

665 
val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t); 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

666 
in (((xs ~~ ps), t'), ctxt') end; 
20149  667 

668 
fun forall_elim_prop t prop = 

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45666
diff
changeset

669 
Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t) 
20579  670 
> Thm.cprop_of > Thm.dest_arg; 
20149  671 

60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

672 
fun focus_cterm bindings goal ctxt = 
20149  673 
let 
60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

674 
val ((xs, ps), ctxt') = focus_params bindings (Thm.term_of goal) ctxt; 
59623  675 
val ps' = map (Thm.cterm_of ctxt' o Free) ps; 
20220  676 
val goal' = fold forall_elim_prop ps' goal; 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

677 
in ((xs ~~ ps', goal'), ctxt') end; 
20149  678 

60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

679 
fun focus_subgoal bindings i st = 
20303  680 
let 
22691  681 
val all_vars = Thm.fold_terms Term.add_vars st []; 
20303  682 
in 
60401  683 
fold (unbind_term o #1) all_vars #> 
20303  684 
fold (declare_constraints o Var) all_vars #> 
60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
60642
diff
changeset

685 
focus_cterm bindings (Thm.cprem_of st i) 
20303  686 
end; 
687 

688 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

689 

300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

690 
(** implicit polymorphism **) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

691 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

692 
(* warn_extra_tfrees *) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

693 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

694 
fun warn_extra_tfrees ctxt1 ctxt2 = 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

695 
let 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

696 
fun occs_typ a = Term.exists_subtype (fn TFree (b, _) => a = b  _ => false); 
20162  697 
fun occs_free a x = 
698 
(case def_type ctxt1 false (x, ~1) of 

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

700 
 NONE => cons (a, x)); 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

701 

20162  702 
val occs1 = type_occs_of ctxt1; 
703 
val occs2 = type_occs_of ctxt2; 

19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

704 
val extras = Symtab.fold (fn (a, xs) => 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

705 
if Symtab.defined occs1 a then I else fold (occs_free a) xs) occs2 []; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

706 
val tfrees = map #1 extras > sort_distinct string_ord; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

707 
val frees = map #2 extras > sort_distinct string_ord; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

708 
in 
38831
4933a3dfd745
more careful treatment of context visibility flag wrt. spurious warnings;
wenzelm
parents:
37145
diff
changeset

709 
if null extras orelse not (Context_Position.is_visible ctxt2) then () 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

710 
else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^ 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

711 
space_implode " or " (map quote frees)) 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

712 
end; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

713 

b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

714 

20149  715 
(* polymorphic terms *) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

716 

24694  717 
fun polymorphic_types ctxt ts = 
20003  718 
let 
719 
val ctxt' = fold declare_term ts ctxt; 

20162  720 
val occs = type_occs_of ctxt; 
721 
val occs' = type_occs_of ctxt'; 

722 
val types = Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else cons a) occs' []; 

24765  723 
val idx = maxidx_of ctxt' + 1; 
24694  724 
val Ts' = (fold o fold_types o fold_atyps) 
725 
(fn T as TFree _ => 

31977  726 
(case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v  _ => I) 
24694  727 
 _ => I) ts []; 
31977  728 
val ts' = map (Term_Subst.generalize (types, []) idx) ts; 
24694  729 
in (rev Ts', ts') end; 
730 

731 
fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts); 

20003  732 

19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

733 
end; 