381 |
381 |
382 fun instT_subst env th = |
382 fun instT_subst env th = |
383 (Thm.fold_terms o Term.fold_types o Term.fold_atyps) |
383 (Thm.fold_terms o Term.fold_types o Term.fold_atyps) |
384 (fn T as TFree (a, _) => |
384 (fn T as TFree (a, _) => |
385 let val T' = the_default T (Symtab.lookup env 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 |
386 in if T = T' then I else insert (eq_fst (op =)) (a, T') end |
387 | _ => I) th []; |
387 | _ => I) th []; |
388 |
388 |
389 fun instT_thm thy env th = |
389 fun instT_thm thy env th = |
390 if Symtab.is_empty env then th |
390 if Symtab.is_empty env then th |
391 else |
391 else |
411 Same.commit (Term_Subst.map_aterms_same |
411 Same.commit (Term_Subst.map_aterms_same |
412 (fn Free (x, _) => (case Symtab.lookup env x of SOME t => t | NONE => raise Same.SAME) |
412 (fn Free (x, _) => (case Symtab.lookup env x of SOME t => t | NONE => raise Same.SAME) |
413 | _ => raise Same.SAME)) #> |
413 | _ => raise Same.SAME)) #> |
414 Envir.beta_norm; |
414 Envir.beta_norm; |
415 |
415 |
|
416 fun inst_subst (envT, env) th = |
|
417 (Thm.fold_terms o Term.fold_aterms) |
|
418 (fn Free (x, T) => |
|
419 let |
|
420 val T' = instT_type envT T; |
|
421 val t = Free (x, T'); |
|
422 val t' = the_default t (Symtab.lookup env x); |
|
423 in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end |
|
424 | _ => I) th []; |
|
425 |
416 fun inst_thm thy (envT, env) th = |
426 fun inst_thm thy (envT, env) th = |
417 if Symtab.is_empty env then instT_thm thy envT th |
427 if Symtab.is_empty env then instT_thm thy envT th |
418 else |
428 else |
419 let |
429 let |
420 val substT = instT_subst envT th; |
430 val substT = instT_subst envT th; |
421 val subst = |
431 val subst = inst_subst (envT, env) th; |
422 (Thm.fold_terms o Term.fold_aterms) |
|
423 (fn Free (x, T) => |
|
424 let |
|
425 val T' = instT_type envT T; |
|
426 val t = Free (x, T'); |
|
427 val t' = the_default t (Symtab.lookup env x); |
|
428 in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end |
|
429 | _ => I) th []; |
|
430 in |
432 in |
431 if null substT andalso null subst then th |
433 if null substT andalso null subst then th |
432 else th |> hyps_rule |
434 else th |> hyps_rule |
433 (instantiate_tfrees thy substT #> |
435 (instantiate_tfrees thy substT #> |
434 instantiate_frees thy subst #> |
436 instantiate_frees thy subst #> |