52 |
52 |
53 fun mk_old_skolem_term_wrapper t = |
53 fun mk_old_skolem_term_wrapper t = |
54 let val T = fastype_of t |
54 let val T = fastype_of t |
55 in \<^Const>\<open>Meson.skolem T for t\<close> end |
55 in \<^Const>\<open>Meson.skolem T for t\<close> end |
56 |
56 |
|
57 fun eta_expand_All_Ex_arg ((cst as (Const _)) $ Abs (s, T, t')) = |
|
58 cst $ Abs (s, T, eta_expand_All_Ex_arg t') |
|
59 | eta_expand_All_Ex_arg ((cst as (Const (cst_s, cst_T))) $ t') = |
|
60 if member (op =) [\<^const_name>\<open>All\<close>, \<^const_name>\<open>Ex\<close>] cst_s then |
|
61 cst $ Abs (Name.uu, domain_type (domain_type cst_T), |
|
62 incr_boundvars 1 (eta_expand_All_Ex_arg t') $ Bound 0) |
|
63 else |
|
64 cst $ eta_expand_All_Ex_arg t' |
|
65 | eta_expand_All_Ex_arg (Abs (s, T, t')) = Abs (s, T, eta_expand_All_Ex_arg t') |
|
66 | eta_expand_All_Ex_arg (t1 $ t2) = |
|
67 eta_expand_All_Ex_arg t1 $ eta_expand_All_Ex_arg t2 |
|
68 | eta_expand_All_Ex_arg t = t |
|
69 |
57 fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t') |
70 fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t') |
58 | beta_eta_in_abs_body t = Envir.beta_eta_contract t |
71 | beta_eta_in_abs_body t = eta_expand_All_Ex_arg (Envir.beta_eta_contract t) |
59 |
72 |
60 (*Traverse a theorem, accumulating Skolem function definitions.*) |
73 (*Traverse a theorem, accumulating Skolem function definitions.*) |
61 fun old_skolem_defs th = |
74 fun old_skolem_defs th = |
62 let |
75 let |
63 fun dec_sko \<^Const_>\<open>Ex _ for \<open>body as Abs (_, T, p)\<close>\<close> rhss = |
76 fun dec_sko \<^Const_>\<open>Ex _ for \<open>body as Abs (_, T, p)\<close>\<close> rhss = |