1.1 --- a/src/HOL/Tools/meson.ML Tue Jan 13 16:47:24 2009 +0000
1.2 +++ b/src/HOL/Tools/meson.ML Thu Jan 29 12:05:19 2009 +0000
1.3 @@ -15,7 +15,6 @@
1.4 val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
1.5 val finish_cnf: thm list -> thm list
1.6 val make_nnf: thm -> thm
1.7 - val make_nnf1: thm -> thm
1.8 val skolemize: thm -> thm
1.9 val is_fol_term: theory -> term -> bool
1.10 val make_clauses: thm list -> thm list
1.11 @@ -296,7 +295,7 @@
1.12 (*Any need to extend this list with
1.13 "HOL.type_class","HOL.eq_class","Pure.term"?*)
1.14 val has_meta_conn =
1.15 - exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
1.16 + exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
1.17
1.18 fun apply_skolem_ths (th, rls) =
1.19 let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
1.20 @@ -519,19 +518,21 @@
1.21
1.22 (*Pull existential quantifiers to front. This accomplishes Skolemization for
1.23 clauses that arise from a subgoal.*)
1.24 -fun skolemize th =
1.25 +fun skolemize1 th =
1.26 if not (has_conns ["Ex"] (prop_of th)) then th
1.27 - else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
1.28 + else (skolemize1 (tryres(th, [choice, conj_exD1, conj_exD2,
1.29 disj_exD, disj_exD1, disj_exD2])))
1.30 handle THM ("tryres", _, _) =>
1.31 - skolemize (forward_res skolemize
1.32 + skolemize1 (forward_res skolemize1
1.33 (tryres (th, [conj_forward, disj_forward, all_forward])))
1.34 handle THM ("tryres", _, _) =>
1.35 - forward_res skolemize (rename_bvs_RS th ex_forward);
1.36 + forward_res skolemize1 (rename_bvs_RS th ex_forward);
1.37 +
1.38 +fun skolemize th = skolemize1 (make_nnf th);
1.39
1.40 fun skolemize_nnf_list [] = []
1.41 | skolemize_nnf_list (th::ths) =
1.42 - skolemize (make_nnf th) :: skolemize_nnf_list ths
1.43 + skolemize th :: skolemize_nnf_list ths
1.44 handle THM _ => (*RS can fail if Unify.search_bound is too small*)
1.45 (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
1.46 skolemize_nnf_list ths);