80 fun vars_of_thm th = |
80 fun vars_of_thm th = |
81 map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); |
81 map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); |
82 |
82 |
83 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]} |
83 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]} |
84 |
84 |
85 (* Removes the lambdas from an equation of the form t = (%x. u). *) |
85 (* ### FIXME: removes only one lambda? *) |
86 fun extensionalize th = |
86 (* Removes the lambdas from an equation of the form "t = (%x. u)" (cf. |
|
87 "extensionalize_term" in "ATP_Systems"). *) |
|
88 fun extensionalize_theorem th = |
87 case prop_of th of |
89 case prop_of th of |
88 _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _])) |
90 _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _])) |
89 $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all) |
91 $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all) |
90 | _ => th |
92 | _ => th |
91 |
93 |
92 fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true |
94 fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true |
93 | is_quasi_lambda_free (t1 $ t2) = |
95 | is_quasi_lambda_free (t1 $ t2) = |
94 is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 |
96 is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 |
224 into NNF. *) |
226 into NNF. *) |
225 fun to_nnf th ctxt0 = |
227 fun to_nnf th ctxt0 = |
226 let val th1 = th |> transform_elim |> zero_var_indexes |
228 let val th1 = th |> transform_elim |> zero_var_indexes |
227 val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 |
229 val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 |
228 val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize |
230 val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize |
229 |> extensionalize |
231 |> extensionalize_theorem |
230 |> Meson.make_nnf ctxt |
232 |> Meson.make_nnf ctxt |
231 in (th3, ctxt) end; |
233 in (th3, ctxt) end; |
232 |
234 |
233 (* Skolemize a named theorem, with Skolem functions as additional premises. *) |
235 (* Skolemize a named theorem, with Skolem functions as additional premises. *) |
234 fun skolemize_theorem thy cheat th = |
236 fun skolemize_theorem thy cheat th = |