468 |
468 |
469 |
469 |
470 (**** Freezing and thawing of variables in proof terms ****) |
470 (**** Freezing and thawing of variables in proof terms ****) |
471 |
471 |
472 fun frzT names = |
472 fun frzT names = |
473 map_type_tvar (fn (ixn, xs) => TFree (valOf (assoc (names, ixn)), xs)); |
473 map_type_tvar (fn (ixn, xs) => TFree (the (assoc (names, ixn)), xs)); |
474 |
474 |
475 fun thawT names = |
475 fun thawT names = |
476 map_type_tfree (fn (s, xs) => case assoc (names, s) of |
476 map_type_tfree (fn (s, xs) => case assoc (names, s) of |
477 NONE => TFree (s, xs) |
477 NONE => TFree (s, xs) |
478 | SOME ixn => TVar (ixn, xs)); |
478 | SOME ixn => TVar (ixn, xs)); |
482 | freeze names names' (Abs (s, T, t)) = |
482 | freeze names names' (Abs (s, T, t)) = |
483 Abs (s, frzT names' T, freeze names names' t) |
483 Abs (s, frzT names' T, freeze names names' t) |
484 | freeze names names' (Const (s, T)) = Const (s, frzT names' T) |
484 | freeze names names' (Const (s, T)) = Const (s, frzT names' T) |
485 | freeze names names' (Free (s, T)) = Free (s, frzT names' T) |
485 | freeze names names' (Free (s, T)) = Free (s, frzT names' T) |
486 | freeze names names' (Var (ixn, T)) = |
486 | freeze names names' (Var (ixn, T)) = |
487 Free (valOf (assoc (names, ixn)), frzT names' T) |
487 Free (the (assoc (names, ixn)), frzT names' T) |
488 | freeze names names' t = t; |
488 | freeze names names' t = t; |
489 |
489 |
490 fun thaw names names' (t $ u) = |
490 fun thaw names names' (t $ u) = |
491 thaw names names' t $ thaw names names' u |
491 thaw names names' t $ thaw names names' u |
492 | thaw names names' (Abs (s, T, t)) = |
492 | thaw names names' (Abs (s, T, t)) = |
551 let |
551 let |
552 val fs = add_term_tfrees (t, []) \\ fixed; |
552 val fs = add_term_tfrees (t, []) \\ fixed; |
553 val ixns = add_term_tvar_ixns (t, []); |
553 val ixns = add_term_tvar_ixns (t, []); |
554 val fmap = fs ~~ variantlist (map fst fs, map #1 ixns) |
554 val fmap = fs ~~ variantlist (map fst fs, map #1 ixns) |
555 fun thaw (f as (a, S)) = |
555 fun thaw (f as (a, S)) = |
556 (case gen_assoc (op =) (fmap, f) of |
556 (case AList.lookup (op =) fmap f of |
557 NONE => TFree f |
557 NONE => TFree f |
558 | SOME b => TVar ((b, 0), S)); |
558 | SOME b => TVar ((b, 0), S)); |
559 in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf |
559 in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf |
560 end; |
560 end; |
561 |
561 |
808 add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t) |
808 add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t) |
809 | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t) |
809 | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t) |
810 | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t) |
810 | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t) |
811 and add_npvars' Ts (vs, t) = (case strip_comb t of |
811 and add_npvars' Ts (vs, t) = (case strip_comb t of |
812 (Var (ixn, _), ts) => if test_args [] ts then vs |
812 (Var (ixn, _), ts) => if test_args [] ts then vs |
813 else Library.foldl (add_npvars' Ts) (overwrite (vs, |
813 else Library.foldl (add_npvars' Ts) |
814 (ixn, Library.foldl (add_funvars Ts) (getOpt (assoc (vs, ixn), []), ts))), ts) |
814 (AList.update (op =) (ixn, |
|
815 Library.foldl (add_funvars Ts) ((these ooo AList.lookup) (op =) vs ixn, ts)) vs, ts) |
815 | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts) |
816 | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts) |
816 | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts)); |
817 | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts)); |
817 |
818 |
818 fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q |
819 fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q |
819 | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t |
820 | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t |