author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24848  5dbbd33c3236 
child 25051  71cd45fdf332 
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 
ID: $Id$ 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

4 

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

5 
Fixed type/term variables and polymorphic term abbreviations. 
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 

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

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

9 
sig 
20303  10 
val is_body: Proof.context > bool 
11 
val set_body: bool > Proof.context > Proof.context 

12 
val restore_body: Proof.context > Proof.context > Proof.context 

13 
val names_of: Proof.context > Name.context 

14 
val fixes_of: Proof.context > (string * string) list 

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

24765  16 
val maxidx_of: Proof.context > int 
20303  17 
val constraints_of: Proof.context > typ Vartab.table * sort Vartab.table 
18 
val is_declared: Proof.context > string > bool 

19 
val is_fixed: Proof.context > string > bool 

20 
val newly_fixed: Proof.context > Proof.context > string > bool 

21571  21 
val add_fixed: Proof.context > term > (string * typ) list > (string * typ) list 
20303  22 
val default_type: Proof.context > string > typ option 
23 
val def_type: Proof.context > bool > indexname > typ option 

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

25 
val declare_constraints: term > Proof.context > Proof.context 

26 
val declare_internal: term > Proof.context > Proof.context 

27 
val declare_term: term > Proof.context > Proof.context 

28 
val declare_prf: Proofterm.proof > Proof.context > Proof.context 

29 
val declare_thm: thm > Proof.context > Proof.context 

30 
val thm_context: thm > Proof.context 

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

32 
val add_binds: (indexname * term option) list > Proof.context > Proof.context 

33 
val expand_binds: Proof.context > term > term 

34 
val add_fixes: string list > Proof.context > string list * Proof.context 

35 
val add_fixes_direct: string list > Proof.context > Proof.context 

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

37 
val variant_fixes: string list > Proof.context > string list * Proof.context 
20303  38 
val invent_types: sort list > Proof.context > (string * sort) list * Proof.context 
39 
val export_terms: Proof.context > Proof.context > term list > term list 

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

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

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

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

21522  44 
val export_morphism: Proof.context > Proof.context > morphism 
20303  45 
val importT_inst: term list > Proof.context > ((indexname * sort) * typ) list * Proof.context 
46 
val import_inst: bool > term list > Proof.context > 

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

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

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

22601  50 
val importT_thms: thm list > Proof.context > (ctyp list * thm list) * Proof.context 
20303  51 
val import_prf: bool > Proofterm.proof > Proof.context > Proofterm.proof * Proof.context 
22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
21799
diff
changeset

52 
val import_thms: bool > thm list > Proof.context > 
20303  53 
((ctyp list * cterm list) * thm list) * Proof.context 
21287  54 
val tradeT: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 
55 
val trade: (Proof.context > thm list > thm list) > Proof.context > thm list > thm list 

20303  56 
val focus: cterm > Proof.context > (cterm list * cterm) * Proof.context 
57 
val focus_subgoal: int > thm > Proof.context > (cterm list * cterm) * Proof.context 

58 
val warn_extra_tfrees: Proof.context > Proof.context > unit 

24694  59 
val polymorphic_types: Proof.context > term list > (indexname * sort) list * term list 
20303  60 
val polymorphic: Proof.context > term list > term list 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

62 

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

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

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

65 

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

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

67 

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

68 
datatype data = Data of 
20102  69 
{is_body: bool, (*inner body mode*) 
20162  70 
names: Name.context, (*type/term variable names*) 
71 
fixes: (string * string) list, (*term fixes  extern/intern*) 

20102  72 
binds: (typ * term) Vartab.table, (*term bindings*) 
20162  73 
type_occs: string list Symtab.table, (*type variables  possibly within term variables*) 
24765  74 
maxidx: int, (*maximum var index*) 
20162  75 
constraints: 
20102  76 
typ Vartab.table * (*type constraints*) 
20162  77 
sort Vartab.table}; (*default sorts*) 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

78 

24765  79 
fun make_data (is_body, names, fixes, binds, type_occs, maxidx, constraints) = 
20162  80 
Data {is_body = is_body, names = names, fixes = fixes, binds = binds, 
24765  81 
type_occs = type_occs, maxidx = maxidx, constraints = constraints}; 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

82 

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

83 
structure Data = ProofDataFun 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

85 
type T = data; 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

86 
fun init thy = 
24765  87 
make_data (false, Name.context, [], Vartab.empty, Symtab.empty, 
88 
~1, (Vartab.empty, Vartab.empty)); 

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

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

90 

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

91 
fun map_data f = 
24765  92 
Data.map (fn Data {is_body, names, fixes, binds, type_occs, maxidx, constraints} => 
93 
make_data (f (is_body, names, fixes, binds, type_occs, maxidx, constraints))); 

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

94 

24765  95 
fun map_names f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) => 
96 
(is_body, f names, fixes, binds, type_occs, maxidx, constraints)); 

20162  97 

24765  98 
fun map_fixes f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) => 
99 
(is_body, names, f fixes, binds, type_occs, maxidx, constraints)); 

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

100 

24765  101 
fun map_binds f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) => 
102 
(is_body, names, fixes, f binds, type_occs, maxidx, constraints)); 

103 

104 
fun map_type_occs f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) => 

105 
(is_body, names, fixes, binds, f type_occs, maxidx, constraints)); 

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

106 

24765  107 
fun map_maxidx f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) => 
108 
(is_body, names, fixes, binds, type_occs, f maxidx, constraints)); 

20102  109 

24765  110 
fun map_constraints f = map_data (fn (is_body, names, fixes, binds, type_occs, maxidx, constraints) => 
111 
(is_body, names, fixes, binds, type_occs, maxidx, f constraints)); 

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

112 

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

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

114 

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

115 
val is_body = #is_body o rep_data; 
24765  116 

117 
fun set_body b = map_data (fn (_, names, fixes, binds, type_occs, maxidx, constraints) => 

118 
(b, names, fixes, binds, type_occs, maxidx, constraints)); 

119 

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

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

121 

20102  122 
val names_of = #names o rep_data; 
123 
val fixes_of = #fixes o rep_data; 

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

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

128 

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

130 
fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt); 
20149  131 
fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

132 

21571  133 
fun add_fixed ctxt = Term.fold_aterms 
134 
(fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I  _ => I); 

135 

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

136 

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

137 

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

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

139 

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

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

141 

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

143 

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

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

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

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

148 
if pattern then NONE 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

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

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

152 

20162  153 
val def_sort = Vartab.lookup o #2 o constraints_of; 
154 

155 

156 
(* names *) 

157 

24765  158 
fun declare_type_names t = 
159 
map_names (fold_types (fold_atyps (fn TFree (a, _) => Name.declare a  _ => I)) t) #> 

160 
map_maxidx (fold_types Term.maxidx_typ t); 

20162  161 

162 
fun declare_names t = 

163 
declare_type_names t #> 

24765  164 
map_names (fold_aterms (fn Free (x, _) => Name.declare x  _ => I) t) #> 
165 
map_maxidx (Term.maxidx_term t); 

20162  166 

167 

168 
(* type occurrences *) 

169 

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

170 
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

171 

22671  172 
val decl_type_occs = fold_term_types 
20162  173 
(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

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

175 

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

176 
val declare_type_occsT = map_type_occs o fold_types decl_type_occsT; 
22671  177 
val declare_type_occs = map_type_occs o decl_type_occs; 
178 

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

179 

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

181 

21355  182 
fun constrain_tvar (xi, S) = 
183 
if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S); 

184 

20162  185 
fun declare_constraints t = map_constraints (fn (types, sorts) => 
186 
let 

187 
val types' = fold_aterms 

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

189 
 Var v => Vartab.update v 

190 
 _ => I) t types; 

191 
val sorts' = fold_types (fold_atyps 

21355  192 
(fn TFree (x, S) => constrain_tvar ((x, ~1), S) 
193 
 TVar v => constrain_tvar v 

20162  194 
 _ => I)) t sorts; 
195 
in (types', sorts') end) 

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

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

198 

20162  199 

200 
(* common declarations *) 

201 

202 
fun declare_internal t = 

203 
declare_names t #> 

204 
declare_type_occs t; 

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

205 

20162  206 
fun declare_term t = 
207 
declare_internal t #> 

208 
declare_constraints t; 

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

209 

20303  210 
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type); 
211 

22691  212 
val declare_thm = Thm.fold_terms declare_internal; 
21522  213 
fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th)); 
19899
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

214 

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

215 

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

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

217 

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

219 
let 
20162  220 
val names = names_of (fold declare_names ts ctxt); 
20084  221 
val xs = fst (Name.variants (map #1 frees) names); 
222 
in xs ~~ map snd frees end; 

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

223 

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

224 

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

225 

20303  226 
(** term bindings **) 
227 

228 
fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi) 

229 
 add_bind ((x, i), SOME t) = 

230 
let 

231 
val T = Term.fastype_of t; 

232 
val t' = 

21683  233 
if null (Term.hidden_polymorphism t T) then t 
20303  234 
else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T); 
235 
in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end; 

236 

237 
val add_binds = fold add_bind; 

238 

239 
fun expand_binds ctxt = 

240 
let 

241 
val binds = binds_of ctxt; 

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

20303  244 

245 

246 

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

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

248 

20084  249 
local 
250 

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

251 
fun no_dups [] = () 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

252 
 no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups); 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

253 

20102  254 
fun new_fixes names' xs xs' = 
255 
map_names (K names') #> 

256 
map_fixes (fn fixes => (rev (xs ~~ xs') @ fixes)) #> 

20162  257 
fold (declare_constraints o Syntax.free) xs' #> 
20084  258 
pair xs'; 
259 

260 
in 

261 

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

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

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

264 
val _ = 
20084  265 
(case filter (can Name.dest_skolem) xs of [] => () 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

266 
 bads => error ("Illegal internal Skolem constant(s): " ^ commas_quote bads)); 
20084  267 
val _ = no_dups (duplicates (op =) xs); 
268 
val (ys, zs) = split_list (fixes_of ctxt); 

20102  269 
val names = names_of ctxt; 
20084  270 
val (xs', names') = 
20149  271 
if is_body ctxt then Name.variants xs names >> map Name.skolem 
20084  272 
else (no_dups (xs inter_string ys); no_dups (xs inter_string zs); 
273 
(xs, fold Name.declare xs names)); 

20102  274 
in ctxt > new_fixes names' xs xs' end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

275 

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

276 
fun variant_fixes raw_xs ctxt = 
20084  277 
let 
20102  278 
val names = names_of ctxt; 
20149  279 
val xs = map Name.clean raw_xs; 
280 
val (xs', names') = Name.variants xs names >> map Name.skolem; 

20102  281 
in ctxt > new_fixes names' xs xs' end; 
20084  282 

283 
end; 

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

284 

20251  285 

286 
fun add_fixes_direct xs ctxt = ctxt 

287 
> set_body false 

288 
> (snd o add_fixes xs) 

289 
> restore_body ctxt; 

290 

291 
fun fix_frees t ctxt = ctxt 

292 
> add_fixes_direct 

293 
(rev (fold_aterms (fn Free (x, _) => 

21369  294 
if is_fixed ctxt x then I else insert (op =) x  _ => I) t [])); 
295 

296 
fun auto_fixes t ctxt = 

297 
(if is_body ctxt then ctxt else fix_frees t ctxt) 

20251  298 
> declare_term t; 
299 

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

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

301 
let 
24848  302 
val tfrees = Name.invents (names_of ctxt) Name.aT (length Ss) ~~ Ss; 
20162  303 
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

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

305 

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

306 

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

307 

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

309 

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

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

311 
let 
20162  312 
val declared_outer = is_declared outer; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

313 
val fixes_inner = fixes_of inner; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

314 
val fixes_outer = fixes_of outer; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

315 

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

316 
val gen_fixes = map #2 (Library.take (length fixes_inner  length fixes_outer, fixes_inner)); 
20162  317 
val still_fixed = not o member (op =) gen_fixes; 
22671  318 

319 
val type_occs_inner = type_occs_of inner; 

320 
fun gen_fixesT ts = 

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

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

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

325 

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

326 
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

327 

22671  328 
fun exportT_terms inner outer = 
329 
let val mk_tfrees = exportT_inst inner outer in 

330 
fn ts => ts > map 

331 
(TermSubst.generalize (mk_tfrees ts, []) 

332 
(fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) 

333 
end; 

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

334 

22671  335 
fun export_terms inner outer = 
336 
let val (mk_tfrees, tfrees) = export_inst inner outer in 

337 
fn ts => ts > map 

338 
(TermSubst.generalize (mk_tfrees ts, tfrees) 

339 
(fold Term.maxidx_term ts ~1 + 1)) 

340 
end; 

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

341 

20303  342 
fun export_prf inner outer prf = 
343 
let 

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

20303  346 
val idx = Proofterm.maxidx_proof prf ~1 + 1; 
22671  347 
val gen_term = TermSubst.generalize_option (tfrees, frees) idx; 
348 
val gen_typ = TermSubst.generalizeT_option tfrees idx; 

20303  349 
in Proofterm.map_proof_terms_option gen_term gen_typ prf end; 
350 

22671  351 

352 
fun gen_export (mk_tfrees, frees) ths = 

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

353 
let 
22671  354 
val tfrees = mk_tfrees (map Thm.full_prop_of ths); 
355 
val maxidx = fold Thm.maxidx_thm ths ~1; 

356 
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

357 

22671  358 
fun exportT inner outer = gen_export (exportT_inst inner outer, []); 
359 
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

360 

21522  361 
fun export_morphism inner outer = 
362 
let 

363 
val fact = export inner outer; 

364 
val term = singleton (export_terms inner outer); 

365 
val typ = Logic.type_map term; 

366 
in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = fact} end; 

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

367 

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

368 

24765  369 

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

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

371 

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

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

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

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

375 
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

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

377 

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

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

379 
let 
20198  380 
val ren = 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

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

383 
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

384 
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

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

386 

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

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

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

390 

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

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

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

394 

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

396 
let 
21522  397 
val thy = ProofContext.theory_of ctxt; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

398 
val certT = Thm.ctyp_of thy; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

399 
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

400 
val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

401 
val ths' = map (Thm.instantiate (instT', [])) ths; 
20220  402 
in ((map #2 instT', ths'), ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

403 

20303  404 
fun import_prf is_open prf ctxt = 
405 
let 

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

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

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

409 

22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
21799
diff
changeset

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

411 
let 
21522  412 
val thy = ProofContext.theory_of ctxt; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

413 
val cert = Thm.cterm_of thy; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

414 
val certT = Thm.ctyp_of thy; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

415 
val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

416 
val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

417 
val inst' = map (fn (v, t) => (cert (Var v), cert t)) inst; 
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

418 
val ths' = map (Thm.instantiate (instT', inst')) ths; 
20220  419 
in (((map #2 instT', map #2 inst'), ths'), ctxt') end; 
19911
300bc6ce970d
major reworking of export functionality  based on Term/Thm.generalize;
wenzelm
parents:
19899
diff
changeset

420 

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

421 

19926  422 
(* import/export *) 
423 

21287  424 
fun gen_trade imp exp f ctxt ths = 
20220  425 
let val ((_, ths'), ctxt') = imp ths ctxt 
21287  426 
in exp ctxt' ctxt (f ctxt' ths') end; 
19926  427 

22601  428 
val tradeT = gen_trade importT_thms exportT; 
22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
21799
diff
changeset

429 
val trade = gen_trade (import_thms true) export; 
19926  430 

431 

20162  432 
(* focus on outermost parameters *) 
20149  433 

434 
fun forall_elim_prop t prop = 

20579  435 
Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t) 
436 
> Thm.cprop_of > Thm.dest_arg; 

20149  437 

438 
fun focus goal ctxt = 

439 
let 

440 
val cert = Thm.cterm_of (Thm.theory_of_cterm goal); 

441 
val t = Thm.term_of goal; 

20162  442 
val ps = Term.variant_frees t (Term.strip_all_vars t); (*as they are printed :*) 
20149  443 
val (xs, Ts) = split_list ps; 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20579
diff
changeset

444 
val (xs', ctxt') = variant_fixes xs ctxt; 
20220  445 
val ps' = ListPair.map (cert o Free) (xs', Ts); 
446 
val goal' = fold forall_elim_prop ps' goal; 

20149  447 
in ((ps', goal'), ctxt') end; 
448 

20303  449 
fun focus_subgoal i st = 
450 
let 

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

454 
add_binds no_binds #> 

455 
fold (declare_constraints o Var) all_vars #> 

456 
focus (Thm.cprem_of st i) 

457 
end; 

458 

459 

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

460 

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

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

462 

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

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

464 

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

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

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

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

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

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

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

472 

20162  473 
val occs1 = type_occs_of ctxt1; 
474 
val occs2 = type_occs_of ctxt2; 

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

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

476 
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

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

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

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

480 
if null extras then () 
b7385ca02d79
Fixed type/term variables and polymorphic term abbreviations.
wenzelm
parents:
diff
changeset

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

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

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

484 

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

485 

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

487 

24694  488 
fun polymorphic_types ctxt ts = 
20003  489 
let 
490 
val ctxt' = fold declare_term ts ctxt; 

20162  491 
val occs = type_occs_of ctxt; 
492 
val occs' = type_occs_of ctxt'; 

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

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

497 
(case TermSubst.generalizeT types idx T of TVar v => insert (op =) v  _ => I) 

498 
 _ => I) ts []; 

499 
val ts' = map (TermSubst.generalize (types, []) idx) ts; 

500 
in (rev Ts', ts') end; 

501 

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

20003  503 

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

504 
end; 