author  wenzelm 
Wed, 03 Oct 2012 16:43:41 +0200  
changeset 49688  c517d900805a 
parent 49685  4341e4d86872 
child 50201  c26369c9eda6 
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 is_body: Proof.context > bool 
10 
val set_body: bool > Proof.context > Proof.context 

11 
val restore_body: Proof.context > Proof.context > Proof.context 

12 
val names_of: Proof.context > Name.context 

13 
val binds_of: Proof.context > (typ * term) Vartab.table 

24765  14 
val maxidx_of: Proof.context > int 
28625  15 
val sorts_of: Proof.context > sort list 
20303  16 
val constraints_of: Proof.context > typ Vartab.table * sort Vartab.table 
17 
val is_declared: Proof.context > string > bool 

42494  18 
val check_name: binding > string 
20303  19 
val default_type: Proof.context > string > typ option 
20 
val def_type: Proof.context > bool > indexname > typ option 

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

27280  22 
val declare_names: term > Proof.context > Proof.context 
20303  23 
val declare_constraints: term > Proof.context > Proof.context 
24 
val declare_term: term > Proof.context > Proof.context 

27280  25 
val declare_typ: typ > Proof.context > Proof.context 
20303  26 
val declare_prf: Proofterm.proof > Proof.context > Proof.context 
27 
val declare_thm: thm > Proof.context > Proof.context 

36603
d5d6111761a6
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
wenzelm
parents:
33957
diff
changeset

28 
val global_thm_context: thm > Proof.context 
20303  29 
val variant_frees: Proof.context > term list > (string * 'a) list > (string * 'a) list 
30756  30 
val bind_term: indexname * term option > Proof.context > Proof.context 
20303  31 
val expand_binds: Proof.context > term > term 
25325  32 
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

33 
val is_const: Proof.context > string > bool 
25325  34 
val declare_const: string * string > Proof.context > Proof.context 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

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

36 
val 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

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

38 
val intern_fixed: Proof.context > string > string 
42493
01430341fc79
more informative markup for fixed variables (via name space entry);
wenzelm
parents:
42488
diff
changeset

39 
val markup_fixed: Proof.context > string > Markup.T 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

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

41 
val revert_fixed: Proof.context > string > string 
42482  42 
val add_fixed_names: Proof.context > term > string list > string list 
43 
val add_fixed: Proof.context > term > (string * typ) list > (string * typ) list 

44 
val add_free_names: Proof.context > term > string list > string list 

45 
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

46 
val add_fixes_binding: binding list > Proof.context > string list * Proof.context 
20303  47 
val add_fixes: string list > Proof.context > string list * Proof.context 
48 
val add_fixes_direct: string list > Proof.context > Proof.context 

21369  49 
val auto_fixes: term > Proof.context > Proof.context 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20579
diff
changeset

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

51 
val dest_fixes: Proof.context > (string * string) list 
20303  52 
val invent_types: sort list > Proof.context > (string * sort) list * Proof.context 
53 
val export_terms: Proof.context > Proof.context > term list > term list 

54 
val exportT_terms: Proof.context > Proof.context > term list > term list 

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

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

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

21522  58 
val export_morphism: Proof.context > Proof.context > morphism 
20303  59 
val importT_inst: term list > Proof.context > ((indexname * sort) * typ) list * Proof.context 
60 
val import_inst: bool > term list > Proof.context > 

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

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

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

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

64 
val importT: thm list > Proof.context > ((ctyp * ctyp) list * thm list) * Proof.context 
20303  65 
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

66 
val import: bool > thm list > Proof.context > 
32280
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

67 
(((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context 
21287  68 
val tradeT: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 
69 
val trade: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 

42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

70 
val focus: term > Proof.context > ((string * (string * typ)) list * term) * Proof.context 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

71 
val focus_cterm: cterm > Proof.context > ((string * cterm) list * cterm) * Proof.context 
32199  72 
val focus_subgoal: int > thm > Proof.context > ((string * cterm) list * cterm) * Proof.context 
20303  73 
val warn_extra_tfrees: Proof.context > Proof.context > unit 
24694  74 
val polymorphic_types: Proof.context > term list > (indexname * sort) list * term list 
20303  75 
val polymorphic: Proof.context > term list > term list 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

77 

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

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

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

80 

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

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

82 

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

83 
type fixes = string Name_Space.table; 
45666  84 
val empty_fixes: fixes = Name_Space.empty_table Isabelle_Markup.fixedN; 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

85 

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

86 
datatype data = Data of 
20102  87 
{is_body: bool, (*inner body mode*) 
20162  88 
names: Name.context, (*type/term variable names*) 
25325  89 
consts: string Symtab.table, (*consts within the local scope*) 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

90 
fixes: fixes, (*term fixes  global name space, intern ~> extern*) 
20102  91 
binds: (typ * term) Vartab.table, (*term bindings*) 
20162  92 
type_occs: string list Symtab.table, (*type variables  possibly within term variables*) 
24765  93 
maxidx: int, (*maximum var index*) 
40124  94 
sorts: sort Ord_List.T, (*declared sort occurrences*) 
20162  95 
constraints: 
20102  96 
typ Vartab.table * (*type constraints*) 
20162  97 
sort Vartab.table}; (*default sorts*) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

98 

28625  99 
fun make_data (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) = 
25325  100 
Data {is_body = is_body, names = names, consts = consts, fixes = fixes, binds = binds, 
28625  101 
type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

102 

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

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

105 
type T = data; 
32784  106 
fun init _ = 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

107 
make_data (false, Name.context, Symtab.empty, empty_fixes, Vartab.empty, 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

108 
Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

110 

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

111 
fun map_data f = 
28625  112 
Data.map (fn Data {is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints} => 
113 
make_data (f (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints))); 

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

114 

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

115 
fun map_names f = 
28625  116 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
117 
(is_body, f names, consts, fixes, binds, type_occs, maxidx, sorts, constraints)); 

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

118 

25325  119 
fun map_consts f = 
28625  120 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
121 
(is_body, names, f consts, fixes, binds, type_occs, maxidx, sorts, constraints)); 

20162  122 

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

123 
fun map_fixes f = 
28625  124 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
125 
(is_body, names, consts, f fixes, binds, type_occs, maxidx, sorts, constraints)); 

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

126 

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

127 
fun map_binds f = 
28625  128 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
129 
(is_body, names, consts, fixes, f binds, type_occs, maxidx, sorts, constraints)); 

24765  130 

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

131 
fun map_type_occs f = 
28625  132 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
133 
(is_body, names, consts, fixes, binds, f type_occs, maxidx, sorts, constraints)); 

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

134 

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

135 
fun map_maxidx f = 
28625  136 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
137 
(is_body, names, consts, fixes, binds, type_occs, f maxidx, sorts, constraints)); 

138 

139 
fun map_sorts f = 

140 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 

141 
(is_body, names, consts, fixes, binds, type_occs, maxidx, f sorts, constraints)); 

20102  142 

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

143 
fun map_constraints f = 
28625  144 
map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 
145 
(is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, f constraints)); 

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

146 

45650  147 
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

148 

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

149 
val is_body = #is_body o rep_data; 
24765  150 

28625  151 
fun set_body b = 
152 
map_data (fn (_, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) => 

153 
(b, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints)); 

24765  154 

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

155 
fun restore_body ctxt = set_body (is_body ctxt); 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

156 

20102  157 
val names_of = #names o rep_data; 
158 
val fixes_of = #fixes o rep_data; 

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

159 
val fixes_space = #1 o fixes_of; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

160 
val binds_of = #binds o rep_data; 
20162  161 
val type_occs_of = #type_occs o rep_data; 
24765  162 
val maxidx_of = #maxidx o rep_data; 
28625  163 
val sorts_of = #sorts o rep_data; 
20162  164 
val constraints_of = #constraints o rep_data; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

165 

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

167 

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

168 
val check_name = Name_Space.base_name o tap Binding.check; 
42357  169 

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

170 

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

171 

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

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

173 

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

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

175 

20162  176 
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

177 

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

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

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

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

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

183 
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

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

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

186 

20162  187 
val def_sort = Vartab.lookup o #2 o constraints_of; 
188 

189 

190 
(* names *) 

191 

24765  192 
fun declare_type_names t = 
29279  193 
map_names (fold_types (fold_atyps Term.declare_typ_names) t) #> 
24765  194 
map_maxidx (fold_types Term.maxidx_typ t); 
20162  195 

196 
fun declare_names t = 

197 
declare_type_names t #> 

29279  198 
map_names (fold_aterms Term.declare_term_frees t) #> 
24765  199 
map_maxidx (Term.maxidx_term t); 
20162  200 

201 

202 
(* type occurrences *) 

203 

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

204 
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

205 

22671  206 
val decl_type_occs = fold_term_types 
20162  207 
(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

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

209 

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

210 
val declare_type_occsT = map_type_occs o fold_types decl_type_occsT; 
22671  211 
val declare_type_occs = map_type_occs o decl_type_occs; 
212 

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

213 

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

215 

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

216 
fun constrain_tvar (xi, raw_S) = 
49688  217 
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

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

20162  220 
fun declare_constraints t = map_constraints (fn (types, sorts) => 
221 
let 

222 
val types' = fold_aterms 

223 
(fn Free (x, T) => Vartab.update ((x, ~1), T) 

224 
 Var v => Vartab.update v 

225 
 _ => I) t types; 

45426  226 
val sorts' = (fold_types o fold_atyps) 
21355  227 
(fn TFree (x, S) => constrain_tvar ((x, ~1), S) 
228 
 TVar v => constrain_tvar v 

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

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

233 

20162  234 

235 
(* common declarations *) 

236 

237 
fun declare_internal t = 

238 
declare_names t #> 

28625  239 
declare_type_occs t #> 
240 
map_sorts (Sorts.insert_term t); 

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

241 

20162  242 
fun declare_term t = 
243 
declare_internal t #> 

244 
declare_constraints t; 

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

245 

27280  246 
val declare_typ = declare_term o Logic.mk_type; 
247 

20303  248 
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type); 
249 

22691  250 
val declare_thm = Thm.fold_terms declare_internal; 
42360  251 
fun global_thm_context th = declare_thm th (Proof_Context.init_global (Thm.theory_of_thm th)); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

252 

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

253 

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

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

255 

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

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

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

261 

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

262 

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

263 

20303  264 
(** term bindings **) 
265 

30756  266 
fun bind_term (xi, NONE) = map_binds (Vartab.delete_safe xi) 
267 
 bind_term ((x, i), SOME t) = 

20303  268 
let 
25051  269 
val u = Term.close_schematic_term t; 
270 
val U = Term.fastype_of u; 

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

20303  272 

273 
fun expand_binds ctxt = 

274 
let 

275 
val binds = binds_of ctxt; 

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

20303  278 

279 

280 

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

282 

25325  283 
val lookup_const = Symtab.lookup o #consts o rep_data; 
284 
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

285 

25325  286 
val declare_fixed = map_consts o Symtab.delete_safe; 
287 
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

288 

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

289 

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

290 

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

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

292 

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

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

294 

46869  295 
val is_fixed = Name_Space.defined_entry o fixes_space; 
296 
fun 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

297 

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

298 
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

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

300 

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

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

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

303 
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

304 

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

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

306 
(case Symtab.lookup (#2 (fixes_of ctxt)) x of 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

307 
SOME x' => if intern_fixed ctxt x' = x then x' else x 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

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

309 

45472  310 
fun markup_fixed ctxt x = 
311 
Name_Space.markup (fixes_space ctxt) x 

312 
> Markup.name (revert_fixed ctxt x); 

313 

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

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

315 
let val (space, tab) = fixes_of ctxt 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

316 
in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end; 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

317 

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

318 

42482  319 
(* collect variables *) 
320 

321 
fun add_free_names ctxt = 

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

323 

324 
fun add_frees ctxt = 

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

326 

327 
fun add_fixed_names ctxt = 

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

329 

330 
fun add_fixed ctxt = 

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

332 

333 

334 
(* declarations *) 

335 

20084  336 
local 
337 

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

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

339 
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

340 

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

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

342 
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

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

344 
let val context = Context.Proof ctxt > Name_Space.map_naming (K Name_Space.default_naming) in 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

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

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

347 
(Name_Space.define context true (Binding.make (x', pos), x) #> snd #>> 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

348 
Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x') 
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46869
diff
changeset

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

350 
> 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

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

352 

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

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

355 
fold new_fixed ((xs ~~ xs') ~~ ps) #> 
20084  356 
pair xs'; 
357 

358 
in 

359 

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

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

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

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

363 
(case filter (can Name.dest_skolem o Binding.name_of) bs of 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

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

365 
 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

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

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

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

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

370 

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

374 
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

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

376 
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

377 

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

378 
fun variant_fixes raw_xs ctxt = 
20084  379 
let 
20102  380 
val names = names_of ctxt; 
26714
4773b832f1b1
variant_fixes: preserve internal state, mark skolem only for body mode;
wenzelm
parents:
25573
diff
changeset

381 
val xs = map (fn x => Name.clean x > can Name.dest_internal x ? Name.internal) raw_xs; 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42495
diff
changeset

382 
val (xs', names') = fold_map Name.variant xs names >> (is_body ctxt ? map Name.skolem); 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

383 
in ctxt > new_fixes names' xs xs' (replicate (length xs) Position.none) end; 
20084  384 

385 
end; 

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

386 

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

387 
val add_fixes = add_fixes_binding o map Binding.name; 
20251  388 

389 
fun add_fixes_direct xs ctxt = ctxt 

390 
> set_body false 

391 
> (snd o add_fixes xs) 

392 
> restore_body ctxt; 

393 

42482  394 
fun auto_fixes t ctxt = ctxt 
395 
> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t [])) 

20251  396 
> declare_term t; 
397 

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

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

399 
let 
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset

400 
val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; 
20162  401 
val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

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

403 

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

404 

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

405 

22671  406 
(** 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

407 

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

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

409 
let 
20162  410 
val declared_outer = is_declared outer; 
46869  411 
val still_fixed = not o newly_fixed inner outer; 
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 
val gen_fixes = 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

414 
Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y) 
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42482
diff
changeset

415 
(#2 (fixes_of inner)) []; 
22671  416 

417 
val type_occs_inner = type_occs_of inner; 

418 
fun gen_fixesT ts = 

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

419 
Symtab.fold (fn (a, xs) => 
20162  420 
if declared_outer a orelse exists still_fixed xs 
22671  421 
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

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

423 

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

424 
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

425 

22671  426 
fun exportT_terms inner outer = 
427 
let val mk_tfrees = exportT_inst inner outer in 

428 
fn ts => ts > map 

31977  429 
(Term_Subst.generalize (mk_tfrees ts, []) 
22671  430 
(fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) 
431 
end; 

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

432 

22671  433 
fun export_terms inner outer = 
434 
let val (mk_tfrees, tfrees) = export_inst inner outer in 

435 
fn ts => ts > map 

31977  436 
(Term_Subst.generalize (mk_tfrees ts, tfrees) 
22671  437 
(fold Term.maxidx_term ts ~1 + 1)) 
438 
end; 

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

439 

20303  440 
fun export_prf inner outer prf = 
441 
let 

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

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

445 
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

446 
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

447 
in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end; 
20303  448 

22671  449 

450 
fun gen_export (mk_tfrees, frees) ths = 

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

451 
let 
22671  452 
val tfrees = mk_tfrees (map Thm.full_prop_of ths); 
453 
val maxidx = fold Thm.maxidx_thm ths ~1; 

454 
in map (Thm.generalize (tfrees, frees) (maxidx + 1)) ths end; 

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

455 

22671  456 
fun exportT inner outer = gen_export (exportT_inst inner outer, []); 
457 
fun export inner outer = gen_export (export_inst inner outer); 

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

458 

21522  459 
fun export_morphism inner outer = 
460 
let 

461 
val fact = export inner outer; 

462 
val term = singleton (export_terms inner outer); 

463 
val typ = Logic.type_map term; 

45289
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
43790
diff
changeset

464 
in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [fact]} end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

465 

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

466 

24765  467 

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

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

469 

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

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

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

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

473 
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

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

475 

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

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

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

478 
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

479 
val (instT, ctxt') = importT_inst ts ctxt; 
31977  480 
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

481 
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

482 
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

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

484 

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

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

486 
let val (instT, ctxt') = importT_inst ts ctxt 
31977  487 
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

488 

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

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

490 
let val (inst, ctxt') = import_inst is_open ts ctxt 
31977  491 
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

492 

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

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

494 
let 
42360  495 
val thy = Proof_Context.theory_of ctxt; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

496 
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; 
32280
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

497 
val insts' as (instT', _) = Thm.certify_inst thy (instT, []); 
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

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

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

500 

20303  501 
fun import_prf is_open prf ctxt = 
502 
let 

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

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

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

506 

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

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

508 
let 
42360  509 
val thy = Proof_Context.theory_of ctxt; 
32280
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

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

511 
val insts' = Thm.certify_inst thy insts; 
4fb3f426052a
Variable.importT/import: return full instantiations, tuned;
wenzelm
parents:
32199
diff
changeset

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

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

514 

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

515 

19926  516 
(* import/export *) 
517 

21287  518 
fun gen_trade imp exp f ctxt ths = 
20220  519 
let val ((_, ths'), ctxt') = imp ths ctxt 
21287  520 
in exp ctxt' ctxt (f ctxt' ths') end; 
19926  521 

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

522 
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

523 
val trade = gen_trade (import true) export; 
19926  524 

525 

42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

526 
(* focus on outermost parameters: !!x y z. B *) 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

527 

1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

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

529 
let 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

530 
val (xs, Ts) = 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

531 
split_list (Term.variant_frees t (Term.strip_all_vars t)); (*as they are printed :*) 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

532 
val (xs', ctxt') = variant_fixes xs ctxt; 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

533 
val ps = xs' ~~ Ts; 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

534 
val ctxt'' = ctxt' > fold (declare_constraints o Free) ps; 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

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

536 

1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

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

538 
let 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

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

540 
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

541 
in (((xs ~~ ps), t'), ctxt') end; 
20149  542 

543 
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

544 
Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t) 
20579  545 
> Thm.cprop_of > Thm.dest_arg; 
20149  546 

42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

547 
fun focus_cterm goal ctxt = 
20149  548 
let 
549 
val cert = Thm.cterm_of (Thm.theory_of_cterm goal); 

42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

550 
val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt; 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

551 
val ps' = map (cert o Free) ps; 
20220  552 
val goal' = fold forall_elim_prop ps' goal; 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

553 
in ((xs ~~ ps', goal'), ctxt') end; 
20149  554 

20303  555 
fun focus_subgoal i st = 
556 
let 

22691  557 
val all_vars = Thm.fold_terms Term.add_vars st []; 
20303  558 
val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars; 
559 
in 

30756  560 
fold bind_term no_binds #> 
20303  561 
fold (declare_constraints o Var) all_vars #> 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

562 
focus_cterm (Thm.cprem_of st i) 
20303  563 
end; 
564 

565 

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

566 

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

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

568 

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

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

570 

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

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

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

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

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

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

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

578 

20162  579 
val occs1 = type_occs_of ctxt1; 
580 
val occs2 = type_occs_of ctxt2; 

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

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

582 
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

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

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

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

586 
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

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

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

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

590 

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

591 

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

593 

24694  594 
fun polymorphic_types ctxt ts = 
20003  595 
let 
596 
val ctxt' = fold declare_term ts ctxt; 

20162  597 
val occs = type_occs_of ctxt; 
598 
val occs' = type_occs_of ctxt'; 

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

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

31977  603 
(case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v  _ => I) 
24694  604 
 _ => I) ts []; 
31977  605 
val ts' = map (Term_Subst.generalize (types, []) idx) ts; 
24694  606 
in (rev Ts', ts') end; 
607 

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

20003  609 

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

610 
end; 