339 |
339 |
340 fun add_inst (a, S) insts = |
340 fun add_inst (a, S) insts = |
341 if AList.defined (op =) insts a then insts |
341 if AList.defined (op =) insts a then insts |
342 else (case AList.lookup (op =) subst a of NONE => insts | SOME T => (a, (S, T)) :: insts); |
342 else (case AList.lookup (op =) subst a of NONE => insts | SOME T => (a, (S, T)) :: insts); |
343 val insts = |
343 val insts = |
344 Term.fold_types (Term.fold_atyps (fn TFree v => add_inst v | _ => I)) |
344 (Term.fold_types o Term.fold_atyps) (fn TFree v => add_inst v | _ => I) |
345 (Thm.full_prop_of th) []; |
345 (Thm.full_prop_of th) []; |
346 in |
346 in |
347 th |
347 th |
348 |> Thm.generalize (map fst insts, []) idx |
348 |> Thm.generalize (map fst insts, []) idx |
349 |> Thm.instantiate (map cert_inst insts, []) |
349 |> Thm.instantiate (map cert_inst insts, []) |
363 end; |
363 end; |
364 |
364 |
365 |
365 |
366 (* instantiate types *) |
366 (* instantiate types *) |
367 |
367 |
368 fun instT_type env = |
368 fun instT_type_same env = |
369 if Symtab.is_empty env then I |
369 if Symtab.is_empty env then Same.same |
370 else Term.map_type_tfree (fn (x, S) => the_default (TFree (x, S)) (Symtab.lookup env x)); |
370 else |
371 |
371 Term_Subst.map_atypsT_same |
372 fun instT_term env = |
372 (fn TFree (a, _) => (case Symtab.lookup env a of SOME T => T | NONE => raise Same.SAME) |
373 if Symtab.is_empty env then I |
373 | _ => raise Same.SAME); |
374 else Term.map_types (instT_type env); |
374 |
375 |
375 fun instT_term_same env = |
376 fun instT_subst env th = (Thm.fold_terms o Term.fold_types o Term.fold_atyps) |
376 if Symtab.is_empty env then Same.same |
377 (fn T as TFree (a, _) => |
377 else Term_Subst.map_types_same (instT_type_same env); |
378 let val T' = the_default T (Symtab.lookup env a) |
378 |
379 in if T = T' then I else insert (op =) (a, T') end |
379 val instT_type = Same.commit o instT_type_same; |
380 | _ => I) th []; |
380 val instT_term = Same.commit o instT_term_same; |
|
381 |
|
382 fun instT_subst env th = |
|
383 (Thm.fold_terms o Term.fold_types o Term.fold_atyps) |
|
384 (fn T as TFree (a, _) => |
|
385 let val T' = the_default T (Symtab.lookup env a) |
|
386 in if T = T' then I else insert (op =) (a, T') end |
|
387 | _ => I) th []; |
381 |
388 |
382 fun instT_thm thy env th = |
389 fun instT_thm thy env th = |
383 if Symtab.is_empty env then th |
390 if Symtab.is_empty env then th |
384 else |
391 else |
385 let val subst = instT_subst env th |
392 let val subst = instT_subst env th |
398 (* instantiate types and terms *) |
405 (* instantiate types and terms *) |
399 |
406 |
400 fun inst_term (envT, env) = |
407 fun inst_term (envT, env) = |
401 if Symtab.is_empty env then instT_term envT |
408 if Symtab.is_empty env then instT_term envT |
402 else |
409 else |
403 let |
410 instT_term envT #> |
404 val instT = instT_type envT; |
411 Same.commit (Term_Subst.map_aterms_same |
405 fun inst (Const (x, T)) = Const (x, instT T) |
412 (fn Free (x, _) => (case Symtab.lookup env x of SOME t => t | NONE => raise Same.SAME) |
406 | inst (Free (x, T)) = |
413 | _ => raise Same.SAME)) #> |
407 (case Symtab.lookup env x of |
414 Envir.beta_norm; |
408 NONE => Free (x, instT T) |
|
409 | SOME t => t) |
|
410 | inst (Var (xi, T)) = Var (xi, instT T) |
|
411 | inst (b as Bound _) = b |
|
412 | inst (Abs (x, T, t)) = Abs (x, instT T, inst t) |
|
413 | inst (t $ u) = inst t $ inst u; |
|
414 in Envir.beta_norm o inst end; |
|
415 |
415 |
416 fun inst_thm thy (envT, env) th = |
416 fun inst_thm thy (envT, env) th = |
417 if Symtab.is_empty env then instT_thm thy envT th |
417 if Symtab.is_empty env then instT_thm thy envT th |
418 else |
418 else |
419 let |
419 let |
420 val substT = instT_subst envT th; |
420 val substT = instT_subst envT th; |
421 val subst = (Thm.fold_terms o Term.fold_aterms) |
421 val subst = |
422 (fn Free (x, T) => |
422 (Thm.fold_terms o Term.fold_aterms) |
423 let |
423 (fn Free (x, T) => |
424 val T' = instT_type envT T; |
424 let |
425 val t = Free (x, T'); |
425 val T' = instT_type envT T; |
426 val t' = the_default t (Symtab.lookup env x); |
426 val t = Free (x, T'); |
427 in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end |
427 val t' = the_default t (Symtab.lookup env x); |
428 | _ => I) th []; |
428 in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end |
|
429 | _ => I) th []; |
429 in |
430 in |
430 if null substT andalso null subst then th |
431 if null substT andalso null subst then th |
431 else th |> hyps_rule |
432 else th |> hyps_rule |
432 (instantiate_tfrees thy substT #> |
433 (instantiate_tfrees thy substT #> |
433 instantiate_frees thy subst #> |
434 instantiate_frees thy subst #> |
434 Conv.fconv_rule (Thm.beta_conversion true)) |
435 Conv.fconv_rule (Thm.beta_conversion true)) |
435 end; |
436 end; |
436 |
437 |
437 fun inst_morphism thy envs = |
438 fun inst_morphism thy (envT, env) = |
438 let val thy_ref = Theory.check_thy thy in |
439 let val thy_ref = Theory.check_thy thy in |
439 Morphism.morphism |
440 Morphism.morphism |
440 {binding = [], |
441 {binding = [], |
441 typ = [instT_type (#1 envs)], |
442 typ = [instT_type envT], |
442 term = [inst_term envs], |
443 term = [inst_term (envT, env)], |
443 fact = [map (fn th => inst_thm (Theory.deref thy_ref) envs th)]} |
444 fact = [map (fn th => inst_thm (Theory.deref thy_ref) (envT, env) th)]} |
444 end; |
445 end; |
445 |
446 |
446 |
447 |
447 (* satisfy hypotheses *) |
448 (* satisfy hypotheses *) |
448 |
449 |
449 fun satisfy_thm witns thm = thm |> fold (fn hyp => |
450 fun satisfy_thm witns thm = |
|
451 thm |> fold (fn hyp => |
450 (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of |
452 (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of |
451 NONE => I |
453 NONE => I |
452 | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm)); |
454 | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm)); |
453 |
455 |
454 val satisfy_morphism = Morphism.thm_morphism o satisfy_thm; |
456 val satisfy_morphism = Morphism.thm_morphism o satisfy_thm; |