# HG changeset patch # User blanchet # Date 1283427939 -7200 # Node ID bef9e5dd0fd07d729d19058d841df4d4d519db04 # Parent ebeb48fd653b54e2a751359972fe3935eb6265f1# Parent dfea12cc5f5a74dd6319bce11d5f34ab06570fed merged diff -r ebeb48fd653b -r bef9e5dd0fd0 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Sep 02 12:30:22 2010 +0200 +++ b/src/HOL/HOL.thy Thu Sep 02 13:45:39 2010 +0200 @@ -32,6 +32,7 @@ ("Tools/recfun_codegen.ML") "Tools/async_manager.ML" "Tools/try.ML" + ("Tools/cnf_funcs.ML") begin setup {* Intuitionistic.method_setup @{binding iprover} *} @@ -1645,7 +1646,6 @@ "(\ \(P)) = P" by blast+ - subsection {* Basic ML bindings *} ML {* @@ -1699,6 +1699,7 @@ val trans = @{thm trans} *} +use "Tools/cnf_funcs.ML" subsection {* Code generator setup *} diff -r ebeb48fd653b -r bef9e5dd0fd0 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Thu Sep 02 12:30:22 2010 +0200 +++ b/src/HOL/Hilbert_Choice.thy Thu Sep 02 13:45:39 2010 +0200 @@ -7,7 +7,8 @@ theory Hilbert_Choice imports Nat Wellfounded Plain -uses ("Tools/meson.ML") ("Tools/choice_specification.ML") +uses ("Tools/meson.ML") + ("Tools/choice_specification.ML") begin subsection {* Hilbert's epsilon *} diff -r ebeb48fd653b -r bef9e5dd0fd0 src/HOL/SAT.thy --- a/src/HOL/SAT.thy Thu Sep 02 12:30:22 2010 +0200 +++ b/src/HOL/SAT.thy Thu Sep 02 13:45:39 2010 +0200 @@ -10,7 +10,6 @@ theory SAT imports Refute uses - "Tools/cnf_funcs.ML" "Tools/sat_funcs.ML" begin diff -r ebeb48fd653b -r bef9e5dd0fd0 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Sep 02 12:30:22 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Thu Sep 02 13:45:39 2010 +0200 @@ -26,6 +26,9 @@ ("Tools/Sledgehammer/sledgehammer_isar.ML") begin +lemma TruepropI: "P \ Q \ Trueprop P \ Trueprop Q" +by simp + definition skolem_id :: "'a \ 'a" where [no_atp]: "skolem_id = (\x. x)" diff -r ebeb48fd653b -r bef9e5dd0fd0 src/HOL/Tools/Sledgehammer/clausifier.ML --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Sep 02 12:30:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Sep 02 13:45:39 2010 +0200 @@ -10,7 +10,8 @@ val extensionalize_theorem : thm -> thm val introduce_combinators_in_cterm : cterm -> thm val introduce_combinators_in_theorem : thm -> thm - val cnf_axiom: theory -> thm -> thm list + val to_definitional_cnf_with_quantifiers : theory -> thm -> thm + val cnf_axiom : theory -> thm -> thm list end; structure Clausifier : CLAUSIFIER = @@ -228,19 +229,26 @@ |> Meson.make_nnf ctxt in (th3, ctxt) end +fun to_definitional_cnf_with_quantifiers thy th = + let + val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th)) + val eqth = eqth RS @{thm eq_reflection} + val eqth = eqth RS @{thm TruepropI} + in Thm.equal_elim eqth th end + (* Convert a theorem to CNF, with Skolem functions as additional premises. *) fun cnf_axiom thy th = let val ctxt0 = Variable.global_thm_context th - val (nnfth, ctxt) = to_nnf th ctxt0 - val sko_ths = map (skolem_theorem_of_def thy) - (assume_skolem_funs nnfth) - val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt + val (nnf_th, ctxt) = to_nnf th ctxt0 + val def_th = to_definitional_cnf_with_quantifiers thy nnf_th + val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th) + val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt in - cnfs |> map introduce_combinators_in_theorem - |> Variable.export ctxt ctxt0 - |> Meson.finish_cnf - |> map Thm.close_derivation + cnf_ths |> map introduce_combinators_in_theorem + |> Variable.export ctxt ctxt0 + |> Meson.finish_cnf + |> map Thm.close_derivation end handle THM _ => [] diff -r ebeb48fd653b -r bef9e5dd0fd0 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 02 12:30:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 02 13:45:39 2010 +0200 @@ -795,13 +795,15 @@ fun generic_metis_tac mode ctxt ths i st0 = let + val thy = ProofContext.theory_of ctxt val _ = trace_msg (fn () => "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) in if exists_type type_has_top_sort (prop_of st0) then (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) else - Meson.MESON (maps neg_clausify) + Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *) + (maps neg_clausify) (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i st0 end diff -r ebeb48fd653b -r bef9e5dd0fd0 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Thu Sep 02 12:30:22 2010 +0200 +++ b/src/HOL/Tools/cnf_funcs.ML Thu Sep 02 13:45:39 2010 +0200 @@ -430,7 +430,7 @@ in make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) end - | make_cnfx_disj_thm (Const (@{const_name Ex}, _) $ x') y' = + | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' = let val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *) val var = new_free () @@ -441,7 +441,7 @@ in iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *) end - | make_cnfx_disj_thm x' (Const (@{const_name Ex}, _) $ y') = + | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') = let val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *) val var = new_free () diff -r ebeb48fd653b -r bef9e5dd0fd0 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Sep 02 12:30:22 2010 +0200 +++ b/src/HOL/Tools/meson.ML Thu Sep 02 13:45:39 2010 +0200 @@ -25,7 +25,9 @@ val depth_prolog_tac: thm list -> tactic val gocls: thm list -> thm list val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic - val MESON: (thm list -> thm list) -> (thm list -> tactic) -> Proof.context -> int -> tactic + val MESON: + (int -> tactic) -> (thm list -> thm list) -> (thm list -> tactic) + -> Proof.context -> int -> tactic val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic val safe_best_meson_tac: Proof.context -> int -> tactic val depth_meson_tac: Proof.context -> int -> tactic @@ -315,8 +317,8 @@ (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*) fun resop nf [prem] = resolve_tac (nf prem) 1; -(*Any need to extend this list with - "HOL.type_class","HOL.eq_class","Pure.term"?*) +(* Any need to extend this list with "HOL.type_class", "HOL.eq_class", + and "Pure.term"? *) val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1); fun apply_skolem_theorem (th, rls) = @@ -573,7 +575,8 @@ (*Make clauses from a list of theorems, previously Skolemized and put into nnf. The resulting clauses are HOL disjunctions.*) -fun make_clauses_unsorted ths = fold_rev add_clauses ths []; +fun make_clauses_unsorted ths = fold_rev add_clauses ths [] +handle exn => error (ML_Compiler.exn_message exn) (*###*) val make_clauses = sort_clauses o make_clauses_unsorted; (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*) @@ -598,20 +601,22 @@ (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. Function mkcl converts theorems to clauses.*) -fun MESON mkcl cltac ctxt i st = +fun MESON preskolem_tac mkcl cltac ctxt i st = SELECT_GOAL (EVERY [Object_Logic.atomize_prems_tac 1, rtac ccontr 1, Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} => - EVERY1 [skolemize_prems_tac ctxt negs, + EVERY1 [preskolem_tac, + skolemize_prems_tac ctxt negs, Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) + (** Best-first search versions **) (*ths is a list of additional clauses (HOL disjunctions) to use.*) fun best_meson_tac sizef = - MESON make_clauses + MESON (K all_tac) make_clauses (fn cls => THEN_BEST_FIRST (resolve_tac (gocls cls) 1) (has_fewer_prems 1, sizef) @@ -625,7 +630,7 @@ (** Depth-first search version **) val depth_meson_tac = - MESON make_clauses + MESON (K all_tac) make_clauses (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]); @@ -645,7 +650,7 @@ fun iter_deepen_prolog_tac horns = ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns); -fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses +fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON (K all_tac) make_clauses (fn cls => (case (gocls (cls @ ths)) of [] => no_tac (*no goal clauses*)