1(* Title: Pure/variable.ML 2 Author: Makarius 3 4Fixed type/term variables and polymorphic term abbreviations. 5*) 6 7signature VARIABLE = 8sig 9 val names_of: Proof.context -> Name.context 10 val binds_of: Proof.context -> (typ * term) Vartab.table 11 val maxidx_of: Proof.context -> int 12 val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table 13 val is_declared: Proof.context -> string -> bool 14 val check_name: binding -> string 15 val default_type: Proof.context -> string -> typ option 16 val def_type: Proof.context -> bool -> indexname -> typ option 17 val def_sort: Proof.context -> indexname -> sort option 18 val declare_maxidx: int -> Proof.context -> Proof.context 19 val declare_names: term -> Proof.context -> Proof.context 20 val declare_constraints: term -> Proof.context -> Proof.context 21 val declare_internal: term -> Proof.context -> Proof.context 22 val declare_term: term -> Proof.context -> Proof.context 23 val declare_typ: typ -> Proof.context -> Proof.context 24 val declare_prf: Proofterm.proof -> Proof.context -> Proof.context 25 val declare_thm: thm -> Proof.context -> Proof.context 26 val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list 27 val bind_term: indexname * term -> Proof.context -> Proof.context 28 val unbind_term: indexname -> Proof.context -> Proof.context 29 val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context 30 val expand_binds: Proof.context -> term -> term 31 val lookup_const: Proof.context -> string -> string option 32 val is_const: Proof.context -> string -> bool 33 val declare_const: string * string -> Proof.context -> Proof.context 34 val next_bound: string * typ -> Proof.context -> term * Proof.context 35 val revert_bounds: Proof.context -> term -> term 36 val is_body: Proof.context -> bool 37 val set_body: bool -> Proof.context -> Proof.context 38 val restore_body: Proof.context -> Proof.context -> Proof.context 39 val improper_fixes: Proof.context -> Proof.context 40 val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context 41 val is_improper: Proof.context -> string -> bool 42 val is_fixed: Proof.context -> string -> bool 43 val is_newly_fixed: Proof.context -> Proof.context -> string -> bool 44 val fixed_ord: Proof.context -> string ord 45 val intern_fixed: Proof.context -> string -> string 46 val lookup_fixed: Proof.context -> string -> string option 47 val revert_fixed: Proof.context -> string -> string 48 val markup_fixed: Proof.context -> string -> Markup.T 49 val markup: Proof.context -> string -> Markup.T 50 val markup_entity_def: Proof.context -> string -> Markup.T 51 val dest_fixes: Proof.context -> (string * string) list 52 val add_fixed_names: Proof.context -> term -> string list -> string list 53 val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list 54 val add_newly_fixed: Proof.context -> Proof.context -> 55 term -> (string * typ) list -> (string * typ) list 56 val add_free_names: Proof.context -> term -> string list -> string list 57 val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list 58 val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context 59 val add_fixes: string list -> Proof.context -> string list * Proof.context 60 val add_fixes_direct: string list -> Proof.context -> Proof.context 61 val add_fixes_implicit: term -> Proof.context -> Proof.context 62 val fix_dummy_patterns: term -> Proof.context -> term * Proof.context 63 val variant_fixes: string list -> Proof.context -> string list * Proof.context 64 val gen_all: Proof.context -> thm -> thm 65 val export_terms: Proof.context -> Proof.context -> term list -> term list 66 val exportT_terms: Proof.context -> Proof.context -> term list -> term list 67 val exportT: Proof.context -> Proof.context -> thm list -> thm list 68 val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof 69 val export: Proof.context -> Proof.context -> thm list -> thm list 70 val export_morphism: Proof.context -> Proof.context -> morphism 71 val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context 72 val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context 73 val import_inst: bool -> term list -> Proof.context -> 74 (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context 75 val importT_terms: term list -> Proof.context -> term list * Proof.context 76 val import_terms: bool -> term list -> Proof.context -> term list * Proof.context 77 val importT: thm list -> Proof.context -> 78 (((indexname * sort) * ctyp) list * thm list) * Proof.context 79 val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context 80 val import: bool -> thm list -> Proof.context -> 81 ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context 82 val import_vars: Proof.context -> thm -> thm 83 val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list 84 val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list 85 val is_bound_focus: Proof.context -> bool 86 val set_bound_focus: bool -> Proof.context -> Proof.context 87 val restore_bound_focus: Proof.context -> Proof.context -> Proof.context 88 val focus_params: binding list option -> term -> Proof.context -> 89 (string list * (string * typ) list) * Proof.context 90 val focus: binding list option -> term -> Proof.context -> 91 ((string * (string * typ)) list * term) * Proof.context 92 val focus_cterm: binding list option -> cterm -> Proof.context -> 93 ((string * cterm) list * cterm) * Proof.context 94 val focus_subgoal: binding list option -> int -> thm -> Proof.context -> 95 ((string * cterm) list * cterm) * Proof.context 96 val warn_extra_tfrees: Proof.context -> Proof.context -> unit 97 val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list 98 val polymorphic: Proof.context -> term list -> term list 99end; 100 101structure Variable: VARIABLE = 102struct 103 104(** local context data **) 105 106type fixes = (string * bool) Name_Space.table; 107val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN; 108 109datatype data = Data of 110 {names: Name.context, (*type/term variable names*) 111 consts: string Symtab.table, (*consts within the local scope*) 112 bounds: int * ((string * typ) * string) list, (*next index, internal name, type, external name*) 113 fixes: fixes, (*term fixes -- global name space, intern ~> extern*) 114 binds: (typ * term) Vartab.table, (*term bindings*) 115 type_occs: string list Symtab.table, (*type variables -- possibly within term variables*) 116 maxidx: int, (*maximum var index*) 117 constraints: 118 typ Vartab.table * (*type constraints*) 119 sort Vartab.table}; (*default sorts*) 120 121fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) = 122 Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds, 123 type_occs = type_occs, maxidx = maxidx, constraints = constraints}; 124 125val empty_data = 126 make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, 127 Symtab.empty, ~1, (Vartab.empty, Vartab.empty)); 128 129structure Data = Proof_Data 130( 131 type T = data; 132 fun init _ = empty_data; 133); 134 135fun map_data f = 136 Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, constraints} => 137 make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints))); 138 139fun map_names f = 140 map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 141 (f names, consts, bounds, fixes, binds, type_occs, maxidx, constraints)); 142 143fun map_consts f = 144 map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 145 (names, f consts, bounds, fixes, binds, type_occs, maxidx, constraints)); 146 147fun map_bounds f = 148 map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 149 (names, consts, f bounds, fixes, binds, type_occs, maxidx, constraints)); 150 151fun map_fixes f = 152 map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 153 (names, consts, bounds, f fixes, binds, type_occs, maxidx, constraints)); 154 155fun map_binds f = 156 map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 157 (names, consts, bounds, fixes, f binds, type_occs, maxidx, constraints)); 158 159fun map_type_occs f = 160 map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 161 (names, consts, bounds, fixes, binds, f type_occs, maxidx, constraints)); 162 163fun map_maxidx f = 164 map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 165 (names, consts, bounds, fixes, binds, type_occs, f maxidx, constraints)); 166 167fun map_constraints f = 168 map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => 169 (names, consts, bounds, fixes, binds, type_occs, maxidx, f constraints)); 170 171fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); 172 173val names_of = #names o rep_data; 174val fixes_of = #fixes o rep_data; 175val fixes_space = Name_Space.space_of_table o fixes_of; 176val binds_of = #binds o rep_data; 177val type_occs_of = #type_occs o rep_data; 178val maxidx_of = #maxidx o rep_data; 179val constraints_of = #constraints o rep_data; 180 181val is_declared = Name.is_declared o names_of; 182 183val check_name = Name_Space.base_name o tap Binding.check; 184 185 186 187(** declarations **) 188 189(* default sorts and types *) 190 191fun default_type ctxt x = Vartab.lookup (#1 (constraints_of ctxt)) (x, ~1); 192 193fun def_type ctxt pattern xi = 194 let val {binds, constraints = (types, _), ...} = rep_data ctxt in 195 (case Vartab.lookup types xi of 196 NONE => 197 if pattern then NONE 198 else Vartab.lookup binds xi |> Option.map (Type.mark_polymorphic o #1) 199 | some => some) 200 end; 201 202val def_sort = Vartab.lookup o #2 o constraints_of; 203 204 205(* maxidx *) 206 207val declare_maxidx = map_maxidx o Integer.max; 208 209 210(* names *) 211 212fun declare_type_names t = 213 map_names (fold_types (fold_atyps Term.declare_typ_names) t) #> 214 map_maxidx (fold_types Term.maxidx_typ t); 215 216fun declare_names t = 217 declare_type_names t #> 218 map_names (fold_aterms Term.declare_term_frees t) #> 219 map_maxidx (Term.maxidx_term t); 220 221 222(* type occurrences *) 223 224fun decl_type_occsT T = fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I) T; 225 226val decl_type_occs = fold_term_types 227 (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I) 228 | _ => decl_type_occsT); 229 230val declare_type_occsT = map_type_occs o fold_types decl_type_occsT; 231val declare_type_occs = map_type_occs o decl_type_occs; 232 233 234(* constraints *) 235 236fun constrain_tvar (xi, raw_S) = 237 let val S = #2 (Term_Position.decode_positionS raw_S) 238 in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end; 239 240fun declare_constraints t = map_constraints (fn (types, sorts) => 241 let 242 val types' = fold_aterms 243 (fn Free (x, T) => Vartab.update ((x, ~1), T) 244 | Var v => Vartab.update v 245 | _ => I) t types; 246 val sorts' = (fold_types o fold_atyps) 247 (fn TFree (x, S) => constrain_tvar ((x, ~1), S) 248 | TVar v => constrain_tvar v 249 | _ => I) t sorts; 250 in (types', sorts') end) 251 #> declare_type_occsT t 252 #> declare_type_names t; 253 254 255(* common declarations *) 256 257fun declare_internal t = 258 declare_names t #> 259 declare_type_occs t #> 260 Thm.declare_term_sorts t; 261 262fun declare_term t = 263 declare_internal t #> 264 declare_constraints t; 265 266val declare_typ = declare_term o Logic.mk_type; 267 268val declare_prf = 269 Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type); 270 271val declare_thm = Thm.fold_terms declare_internal; 272 273 274(* renaming term/type frees *) 275 276fun variant_frees ctxt ts frees = 277 let 278 val names = names_of (fold declare_names ts ctxt); 279 val xs = fst (fold_map Name.variant (map #1 frees) names); 280 in xs ~~ map snd frees end; 281 282 283 284(** term bindings **) 285 286fun bind_term ((x, i), t) = 287 let 288 val u = Term.close_schematic_term t; 289 val U = Term.fastype_of u; 290 in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end; 291 292val unbind_term = map_binds o Vartab.delete_safe; 293 294fun maybe_bind_term (xi, SOME t) = bind_term (xi, t) 295 | maybe_bind_term (xi, NONE) = unbind_term xi; 296 297fun expand_binds ctxt = 298 let 299 val binds = binds_of ctxt; 300 val get = fn Var (xi, _) => Vartab.lookup binds xi | _ => NONE; 301 in Envir.beta_norm o Envir.expand_term get end; 302 303 304 305(** consts **) 306 307val lookup_const = Symtab.lookup o #consts o rep_data; 308val is_const = is_some oo lookup_const; 309 310val declare_fixed = map_consts o Symtab.delete_safe; 311val declare_const = map_consts o Symtab.update; 312 313 314 315(** bounds **) 316 317fun next_bound (a, T) ctxt = 318 let 319 val b = Name.bound (#1 (#bounds (rep_data ctxt))); 320 val ctxt' = ctxt |> map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds)); 321 in (Free (b, T), ctxt') end; 322 323fun revert_bounds ctxt t = 324 (case #2 (#bounds (rep_data ctxt)) of 325 [] => t 326 | bounds => 327 let 328 val names = Term.declare_term_names t (names_of ctxt); 329 val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names)); 330 fun subst ((b, T), _) x' = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T)); 331 in Term.subst_atomic (map2 subst bounds xs) t end); 332 333 334 335(** fixes **) 336 337(* inner body mode *) 338 339val inner_body = Config.declare_bool ("inner_body", \<^here>) (K false); 340val is_body = Config.apply inner_body; 341val set_body = Config.put inner_body; 342val restore_body = set_body o is_body; 343 344 345(* proper mode *) 346 347val proper_fixes = Config.declare_bool ("proper_fixes", \<^here>) (K true); 348val improper_fixes = Config.put proper_fixes false; 349val restore_proper_fixes = Config.put proper_fixes o Config.apply proper_fixes; 350 351fun is_improper ctxt x = 352 (case Name_Space.lookup (fixes_of ctxt) x of 353 SOME (_, proper) => not proper 354 | NONE => false); 355 356 357(* specialized name space *) 358 359val is_fixed = Name_Space.defined o fixes_of; 360fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer); 361 362val fixed_ord = Name_Space.entry_ord o fixes_space; 363val intern_fixed = Name_Space.intern o fixes_space; 364 365fun lookup_fixed ctxt x = 366 let val x' = intern_fixed ctxt x 367 in if is_fixed ctxt x' then SOME x' else NONE end; 368 369fun revert_fixed ctxt x = 370 (case Name_Space.lookup (fixes_of ctxt) x of 371 SOME (x', _) => if intern_fixed ctxt x' = x then x' else x 372 | NONE => x); 373 374fun markup_fixed ctxt x = 375 Name_Space.markup (fixes_space ctxt) x 376 |> Markup.name (revert_fixed ctxt x); 377 378fun markup ctxt x = 379 if is_improper ctxt x then Markup.improper 380 else if Name.is_skolem x then Markup.skolem 381 else Markup.free; 382 383val markup_entity_def = Name_Space.markup_def o fixes_space; 384 385fun dest_fixes ctxt = 386 Name_Space.fold_table (fn (x, (y, _)) => cons (y, x)) (fixes_of ctxt) [] 387 |> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2); 388 389 390(* collect variables *) 391 392fun add_free_names ctxt = 393 fold_aterms (fn Free (x, _) => not (is_fixed ctxt x) ? insert (op =) x | _ => I); 394 395fun add_frees ctxt = 396 fold_aterms (fn Free (x, T) => not (is_fixed ctxt x) ? insert (op =) (x, T) | _ => I); 397 398fun add_fixed_names ctxt = 399 fold_aterms (fn Free (x, _) => is_fixed ctxt x ? insert (op =) x | _ => I); 400 401fun add_fixed ctxt = 402 fold_aterms (fn Free (x, T) => is_fixed ctxt x ? insert (op =) (x, T) | _ => I); 403 404fun add_newly_fixed ctxt' ctxt = 405 fold_aterms (fn Free (x, T) => is_newly_fixed ctxt' ctxt x ? insert (op =) (x, T) | _ => I); 406 407 408(* declarations *) 409 410local 411 412fun err_dups dups = 413 error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups)); 414 415fun new_fixed ((x, x'), pos) ctxt = 416 if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)] 417 else 418 let 419 val proper = Config.get ctxt proper_fixes; 420 val context = Context.Proof ctxt 421 |> Name_Space.map_naming (K Name_Space.global_naming) 422 |> Context_Position.set_visible_generic false; 423 in 424 ctxt 425 |> map_fixes 426 (Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #> 427 Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x') 428 |> declare_fixed x 429 |> declare_constraints (Syntax.free x') 430 end; 431 432fun new_fixes names' args = 433 map_names (K names') #> 434 fold new_fixed args #> 435 pair (map (#2 o #1) args); 436 437in 438 439fun add_fixes_binding bs ctxt = 440 let 441 val _ = 442 (case filter (Name.is_skolem o Binding.name_of) bs of 443 [] => () 444 | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads))); 445 val _ = 446 (case duplicates (op = o apply2 Binding.name_of) bs of 447 [] => () 448 | dups => err_dups dups); 449 450 val xs = map check_name bs; 451 val names = names_of ctxt; 452 val (xs', names') = 453 if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem 454 else (xs, fold Name.declare xs names); 455 in ctxt |> new_fixes names' ((xs ~~ xs') ~~ map Binding.pos_of bs) end; 456 457fun variant_names ctxt raw_xs = 458 let 459 val names = names_of ctxt; 460 val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs; 461 val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem); 462 in (names', xs ~~ xs') end; 463 464fun variant_fixes xs ctxt = 465 let val (names', vs) = variant_names ctxt xs; 466 in ctxt |> new_fixes names' (map (rpair Position.none) vs) end; 467 468fun bound_fixes xs ctxt = 469 let 470 val (names', vs) = variant_names ctxt (map #1 xs); 471 val (ys, ctxt') = fold_map next_bound (map2 (fn (x', _) => fn (_, T) => (x', T)) vs xs) ctxt; 472 val fixes = map2 (fn (x, _) => fn Free (y, _) => ((x, y), Position.none)) vs ys; 473 in ctxt' |> new_fixes names' fixes end; 474 475end; 476 477val add_fixes = add_fixes_binding o map Binding.name; 478 479fun add_fixes_direct xs ctxt = ctxt 480 |> set_body false 481 |> (snd o add_fixes xs) 482 |> restore_body ctxt; 483 484fun add_fixes_implicit t ctxt = ctxt 485 |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t [])); 486 487 488(* dummy patterns *) 489 490fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt = 491 let val ([x], ctxt') = ctxt |> set_body true |> add_fixes [Name.uu_] ||> restore_body ctxt 492 in (Free (x, T), ctxt') end 493 | fix_dummy_patterns (Abs (x, T, b)) ctxt = 494 let val (b', ctxt') = fix_dummy_patterns b ctxt 495 in (Abs (x, T, b'), ctxt') end 496 | fix_dummy_patterns (t $ u) ctxt = 497 let 498 val (t', ctxt') = fix_dummy_patterns t ctxt; 499 val (u', ctxt'') = fix_dummy_patterns u ctxt'; 500 in (t' $ u', ctxt'') end 501 | fix_dummy_patterns a ctxt = (a, ctxt); 502 503 504 505(** export -- generalize type/term variables (beware of closure sizes) **) 506 507fun gen_all ctxt th = 508 let 509 val i = Thm.maxidx_thm th (maxidx_of ctxt) + 1; 510 fun gen (x, T) = Thm.forall_elim (Thm.cterm_of ctxt (Var ((x, i), T))); 511 in fold gen (Drule.outer_params (Thm.prop_of th)) th end; 512 513fun export_inst inner outer = 514 let 515 val declared_outer = is_declared outer; 516 val still_fixed = not o is_newly_fixed inner outer; 517 518 val gen_fixes = 519 Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y) 520 (fixes_of inner) []; 521 522 val type_occs_inner = type_occs_of inner; 523 fun gen_fixesT ts = 524 Symtab.fold (fn (a, xs) => 525 if declared_outer a orelse exists still_fixed xs 526 then I else cons a) (fold decl_type_occs ts type_occs_inner) []; 527 in (gen_fixesT, gen_fixes) end; 528 529fun exportT_inst inner outer = #1 (export_inst inner outer); 530 531fun exportT_terms inner outer = 532 let 533 val mk_tfrees = exportT_inst inner outer; 534 val maxidx = maxidx_of outer; 535 in 536 fn ts => ts |> map 537 (Term_Subst.generalize (mk_tfrees ts, []) 538 (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1)) 539 end; 540 541fun export_terms inner outer = 542 let 543 val (mk_tfrees, tfrees) = export_inst inner outer; 544 val maxidx = maxidx_of outer; 545 in 546 fn ts => ts |> map 547 (Term_Subst.generalize (mk_tfrees ts, tfrees) 548 (fold Term.maxidx_term ts maxidx + 1)) 549 end; 550 551fun export_prf inner outer prf = 552 let 553 val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer; 554 val tfrees = mk_tfrees []; 555 val maxidx = maxidx_of outer; 556 val idx = Proofterm.maxidx_proof prf maxidx + 1; 557 val gen_term = Term_Subst.generalize_same (tfrees, frees) idx; 558 val gen_typ = Term_Subst.generalizeT_same tfrees idx; 559 in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end; 560 561 562fun gen_export (mk_tfrees, frees) maxidx ths = 563 let 564 val tfrees = mk_tfrees (map Thm.full_prop_of ths); 565 val idx = fold Thm.maxidx_thm ths maxidx + 1; 566 in map (Thm.generalize (tfrees, frees) idx) ths end; 567 568fun exportT inner outer = gen_export (exportT_inst inner outer, []) (maxidx_of outer); 569fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer); 570 571fun export_morphism inner outer = 572 let 573 val fact = export inner outer; 574 val term = singleton (export_terms inner outer); 575 val typ = Logic.type_map term; 576 in 577 Morphism.transfer_morphism' inner $> 578 Morphism.transfer_morphism' outer $> 579 Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]} 580 end; 581 582 583 584(** import -- fix schematic type/term variables **) 585 586fun invent_types Ss ctxt = 587 let 588 val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; 589 val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; 590 in (tfrees, ctxt') end; 591 592fun importT_inst ts ctxt = 593 let 594 val tvars = rev (fold Term.add_tvars ts []); 595 val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt; 596 in (tvars ~~ map TFree tfrees, ctxt') end; 597 598fun import_inst is_open ts ctxt = 599 let 600 val ren = Name.clean #> (if is_open then I else Name.internal); 601 val (instT, ctxt') = importT_inst ts ctxt; 602 val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts [])); 603 val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt'; 604 val inst = vars ~~ map Free (xs ~~ map #2 vars); 605 in ((instT, inst), ctxt'') end; 606 607fun importT_terms ts ctxt = 608 let val (instT, ctxt') = importT_inst ts ctxt 609 in (map (Term_Subst.instantiate (instT, [])) ts, ctxt') end; 610 611fun import_terms is_open ts ctxt = 612 let val (inst, ctxt') = import_inst is_open ts ctxt 613 in (map (Term_Subst.instantiate inst) ts, ctxt') end; 614 615fun importT ths ctxt = 616 let 617 val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; 618 val instT' = map (apsnd (Thm.ctyp_of ctxt')) instT; 619 val ths' = map (Thm.instantiate (instT', [])) ths; 620 in ((instT', ths'), ctxt') end; 621 622fun import_prf is_open prf ctxt = 623 let 624 val ts = rev (Proofterm.fold_proof_terms_types cons (cons o Logic.mk_type) prf []); 625 val (insts, ctxt') = import_inst is_open ts ctxt; 626 in (Proofterm.instantiate insts prf, ctxt') end; 627 628fun import is_open ths ctxt = 629 let 630 val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; 631 val insts' = 632 (map (apsnd (Thm.ctyp_of ctxt')) instT, 633 map (apsnd (Thm.cterm_of ctxt')) inst); 634 val ths' = map (Thm.instantiate insts') ths; 635 in ((insts', ths'), ctxt') end; 636 637fun import_vars ctxt th = 638 let val ((_, [th']), _) = ctxt |> set_body false |> import true [th]; 639 in th' end; 640 641 642(* import/export *) 643 644fun gen_trade imp exp f ctxt ths = 645 let val ((_, ths'), ctxt') = imp ths ctxt 646 in exp ctxt' ctxt (f ctxt' ths') end; 647 648val tradeT = gen_trade importT exportT; 649val trade = gen_trade (import true) export; 650 651 652(* focus on outermost parameters: \<And>x y z. B *) 653 654val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false); 655val is_bound_focus = Config.apply bound_focus; 656val set_bound_focus = Config.put bound_focus; 657val restore_bound_focus = set_bound_focus o is_bound_focus; 658 659fun focus_params bindings t ctxt = 660 let 661 val ps = Term.variant_frees t (Term.strip_all_vars t); (*as they are printed :-*) 662 val (xs, Ts) = split_list ps; 663 val (xs', ctxt') = 664 (case bindings of 665 SOME bs => ctxt |> set_body true |> add_fixes_binding bs ||> restore_body ctxt 666 | NONE => if is_bound_focus ctxt then bound_fixes ps ctxt else variant_fixes xs ctxt); 667 val ps' = xs' ~~ Ts; 668 val ctxt'' = ctxt' |> fold (declare_constraints o Free) ps'; 669 in ((xs, ps'), ctxt'') end; 670 671fun focus bindings t ctxt = 672 let 673 val ((xs, ps), ctxt') = focus_params bindings t ctxt; 674 val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t); 675 in (((xs ~~ ps), t'), ctxt') end; 676 677fun forall_elim_prop t prop = 678 Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t) 679 |> Thm.cprop_of |> Thm.dest_arg; 680 681fun focus_cterm bindings goal ctxt = 682 let 683 val ((xs, ps), ctxt') = focus_params bindings (Thm.term_of goal) ctxt; 684 val ps' = map (Thm.cterm_of ctxt' o Free) ps; 685 val goal' = fold forall_elim_prop ps' goal; 686 in ((xs ~~ ps', goal'), ctxt') end; 687 688fun focus_subgoal bindings i st = 689 let 690 val all_vars = Thm.fold_terms Term.add_vars st []; 691 in 692 fold (unbind_term o #1) all_vars #> 693 fold (declare_constraints o Var) all_vars #> 694 focus_cterm bindings (Thm.cprem_of st i) 695 end; 696 697 698 699(** implicit polymorphism **) 700 701(* warn_extra_tfrees *) 702 703fun warn_extra_tfrees ctxt1 ctxt2 = 704 let 705 fun occs_typ a = Term.exists_subtype (fn TFree (b, _) => a = b | _ => false); 706 fun occs_free a x = 707 (case def_type ctxt1 false (x, ~1) of 708 SOME T => if occs_typ a T then I else cons (a, x) 709 | NONE => cons (a, x)); 710 711 val occs1 = type_occs_of ctxt1; 712 val occs2 = type_occs_of ctxt2; 713 val extras = Symtab.fold (fn (a, xs) => 714 if Symtab.defined occs1 a then I else fold (occs_free a) xs) occs2 []; 715 val tfrees = map #1 extras |> sort_distinct string_ord; 716 val frees = map #2 extras |> sort_distinct string_ord; 717 in 718 if null extras orelse not (Context_Position.is_visible ctxt2) then () 719 else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^ 720 space_implode " or " (map quote frees)) 721 end; 722 723 724(* polymorphic terms *) 725 726fun polymorphic_types ctxt ts = 727 let 728 val ctxt' = fold declare_term ts ctxt; 729 val occs = type_occs_of ctxt; 730 val occs' = type_occs_of ctxt'; 731 val types = Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else cons a) occs' []; 732 val idx = maxidx_of ctxt' + 1; 733 val Ts' = (fold o fold_types o fold_atyps) 734 (fn T as TFree _ => 735 (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I) 736 | _ => I) ts []; 737 val ts' = map (Term_Subst.generalize (types, []) idx) ts; 738 in (rev Ts', ts') end; 739 740fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts); 741 742end; 743