# HG changeset patch # User paulson # Date 1233231840 0 # Node ID aba49b4fe95974900e6fb5294a4aeb5852a17c2d # Parent fa6f988f1c502c8fcfcf83d5f91d687b90993d95# Parent 40bf9f4e7a4ed81e6ce9a1f0320684c1f79bff4b Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle diff -r fa6f988f1c50 -r aba49b4fe959 src/HOL/MetisExamples/Abstraction.thy --- a/src/HOL/MetisExamples/Abstraction.thy Thu Jan 29 09:35:51 2009 +0000 +++ b/src/HOL/MetisExamples/Abstraction.thy Thu Jan 29 12:24:00 2009 +0000 @@ -62,9 +62,9 @@ ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect"*} lemma "(a,b) \ (SIGMA x: A. {y. x = f y}) ==> a \ A & a = f b" -(*???metis cannot prove this -by (metis CollectD SigmaD1 SigmaD2 UN_eq) -Also, UN_eq is unnecessary*) +(*???metis says this is satisfiable! +by (metis CollectD SigmaD1 SigmaD2) +*) by (meson CollectD SigmaD1 SigmaD2) diff -r fa6f988f1c50 -r aba49b4fe959 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Jan 29 09:35:51 2009 +0000 +++ b/src/HOL/Tools/meson.ML Thu Jan 29 12:24:00 2009 +0000 @@ -15,7 +15,6 @@ val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context val finish_cnf: thm list -> thm list val make_nnf: thm -> thm - val make_nnf1: thm -> thm val skolemize: thm -> thm val is_fol_term: theory -> term -> bool val make_clauses: thm list -> thm list @@ -296,7 +295,7 @@ (*Any need to extend this list with "HOL.type_class","HOL.eq_class","Pure.term"?*) val has_meta_conn = - exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1); + exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1); fun apply_skolem_ths (th, rls) = let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls) @@ -519,19 +518,21 @@ (*Pull existential quantifiers to front. This accomplishes Skolemization for clauses that arise from a subgoal.*) -fun skolemize th = +fun skolemize1 th = if not (has_conns ["Ex"] (prop_of th)) then th - else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2, + else (skolemize1 (tryres(th, [choice, conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2]))) handle THM ("tryres", _, _) => - skolemize (forward_res skolemize + skolemize1 (forward_res skolemize1 (tryres (th, [conj_forward, disj_forward, all_forward]))) handle THM ("tryres", _, _) => - forward_res skolemize (rename_bvs_RS th ex_forward); + forward_res skolemize1 (rename_bvs_RS th ex_forward); + +fun skolemize th = skolemize1 (make_nnf th); fun skolemize_nnf_list [] = [] | skolemize_nnf_list (th::ths) = - skolemize (make_nnf th) :: skolemize_nnf_list ths + skolemize th :: skolemize_nnf_list ths handle THM _ => (*RS can fail if Unify.search_bound is too small*) (warning ("Failed to Skolemize " ^ Display.string_of_thm th); skolemize_nnf_list ths); diff -r fa6f988f1c50 -r aba49b4fe959 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Thu Jan 29 09:35:51 2009 +0000 +++ b/src/HOL/Tools/res_clause.ML Thu Jan 29 12:24:00 2009 +0000 @@ -279,6 +279,14 @@ (*Given a list of sorted type variables, return a list of type literals.*) fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts); +(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear. + * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a + in a lemma has the same sort as 'a in the conjecture. + * Deleting such clauses will lead to problems with locales in other use of local results + where 'a is fixed. Probably we should delete clauses unless the sorts agree. + * Currently we include a class constraint in the clause, exactly as with TVars. +*) + (** make axiom and conjecture clauses. **) fun get_tvar_strs [] = []