63 fun old_skolem_defs th = |
63 fun old_skolem_defs th = |
64 let |
64 let |
65 fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss = |
65 fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss = |
66 (*Existential: declare a Skolem function, then insert into body and continue*) |
66 (*Existential: declare a Skolem function, then insert into body and continue*) |
67 let |
67 let |
68 val args = OldTerm.term_frees body |
68 val args = Misc_Legacy.term_frees body |
69 (* Forms a lambda-abstraction over the formal parameters *) |
69 (* Forms a lambda-abstraction over the formal parameters *) |
70 val rhs = |
70 val rhs = |
71 list_abs_free (map dest_Free args, |
71 list_abs_free (map dest_Free args, |
72 HOLogic.choice_const T $ beta_eta_in_abs_body body) |
72 HOLogic.choice_const T $ beta_eta_in_abs_body body) |
73 |> mk_old_skolem_term_wrapper |
73 |> mk_old_skolem_term_wrapper |
74 val comb = list_comb (rhs, args) |
74 val comb = list_comb (rhs, args) |
75 in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end |
75 in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end |
76 | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = |
76 | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = |
77 (*Universal quant: insert a free variable into body and continue*) |
77 (*Universal quant: insert a free variable into body and continue*) |
78 let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a |
78 let val fname = singleton (Name.variant_list (Misc_Legacy.add_term_names (p, []))) a |
79 in dec_sko (subst_bound (Free(fname,T), p)) rhss end |
79 in dec_sko (subst_bound (Free(fname,T), p)) rhss end |
80 | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
80 | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
81 | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
81 | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
82 | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss |
82 | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss |
83 | dec_sko _ rhss = rhss |
83 | dec_sko _ rhss = rhss |
90 | is_quasi_lambda_free (t1 $ t2) = |
90 | is_quasi_lambda_free (t1 $ t2) = |
91 is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 |
91 is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 |
92 | is_quasi_lambda_free (Abs _) = false |
92 | is_quasi_lambda_free (Abs _) = false |
93 | is_quasi_lambda_free _ = true |
93 | is_quasi_lambda_free _ = true |
94 |
94 |
95 val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); |
95 val [f_B,g_B] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_B})); |
96 val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); |
96 val [g_C,f_C] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_C})); |
97 val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); |
97 val [f_S,g_S] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_S})); |
98 |
98 |
99 (* FIXME: Requires more use of cterm constructors. *) |
99 (* FIXME: Requires more use of cterm constructors. *) |
100 fun abstract ct = |
100 fun abstract ct = |
101 let |
101 let |
102 val thy = theory_of_cterm ct |
102 val thy = theory_of_cterm ct |