# HG changeset patch # User blanchet # Date 1302773044 -7200 # Node ID cb8aa792d138051397ea7376cdf415939d24fb19 # Parent 8e58cc1390c7ec6b5e86d946ae2665691db4a1dd experiment with definitional CNF diff -r 8e58cc1390c7 -r cb8aa792d138 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Thu Apr 14 11:24:04 2011 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Thu Apr 14 11:24:04 2011 +0200 @@ -14,6 +14,7 @@ val size_of_subgoals: thm -> int val has_too_many_clauses: Proof.context -> term -> bool val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context + val make_xxx_skolem: Proof.context -> thm list -> thm -> thm val finish_cnf: thm list -> thm list val presimplify: thm -> thm val make_nnf: Proof.context -> thm -> thm @@ -393,6 +394,48 @@ fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, []) +val disj_imp_cong = + @{lemma "[| P --> P'; Q --> Q'; P | Q |] ==> P' | Q'" by auto} + +val impI = @{thm impI} + +(* ### *) +(* Match untyped terms. *) +fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b) + | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b) + | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = true + | untyped_aconv (Free (a, _)) (Var ((b, _), _)) = true + | untyped_aconv (Var ((a, _), _)) (Free (b, _)) = true + | untyped_aconv (Bound i) (Bound j) = (i = j) + | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u + | untyped_aconv (t1 $ t2) (u1 $ u2) = + untyped_aconv t1 u1 andalso untyped_aconv t2 u2 + | untyped_aconv _ _ = false + +fun make_xxx_skolem ctxt skolem_ths th = + let + val thy = ProofContext.theory_of ctxt + fun do_connective fwd_thm t1 t2 = + do_formula t1 + COMP rotate_prems 1 (do_formula t2 COMP (rotate_prems 2 fwd_thm)) + and do_formula t = + case t of + @{const Trueprop} $ t' => do_formula t' + | @{const conj} $ t1 $ t2 => do_connective @{thm conj_forward} t1 t2 + | @{const disj} $ t1 $ t2 => do_connective @{thm disj_forward} t1 t2 + | Const (@{const_name Ex}, _) $ Abs _ => + let + val th = + find_first (fn sko_th => (untyped_aconv (Logic.nth_prem (1, prop_of sko_th)) (HOLogic.mk_Trueprop t))) + skolem_ths |> the + in + th + RS + do_formula (Logic.strip_imp_concl (prop_of th)) + end + | _ => Thm.trivial (cterm_of thy (HOLogic.mk_Trueprop t)) + in th COMP do_formula (HOLogic.dest_Trueprop (prop_of th)) end + (*Generalization, removal of redundant equalities, removal of tautologies.*) fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths); diff -r 8e58cc1390c7 -r cb8aa792d138 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Apr 14 11:24:04 2011 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Apr 14 11:24:04 2011 +0200 @@ -13,7 +13,7 @@ val extensionalize_theorem : thm -> thm val introduce_combinators_in_cterm : cterm -> thm val introduce_combinators_in_theorem : thm -> thm - val to_definitional_cnf_with_quantifiers : theory -> thm -> thm + val to_definitional_cnf_with_quantifiers : Proof.context -> thm -> thm val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool val cnf_axiom : Proof.context -> bool -> int -> thm -> (thm * term) option * thm list @@ -229,9 +229,9 @@ |> Thm.varifyT_global end -fun to_definitional_cnf_with_quantifiers thy th = +fun to_definitional_cnf_with_quantifiers ctxt th = let - val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th)) + val eqth = cnf.make_cnfx_thm ctxt (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 @@ -341,8 +341,8 @@ cterm_of thy) |> zap true val fixes = - Term.add_free_names (prop_of zapped_th) [] - |> filter is_zapped_var_name + [] |> Term.add_free_names (prop_of zapped_th) + |> filter is_zapped_var_name val ctxt' = ctxt |> Variable.add_fixes_direct fixes val fully_skolemized_t = zapped_th |> singleton (Variable.export ctxt' ctxt) @@ -366,6 +366,58 @@ (NONE, (th, ctxt)) end +val all_out_ss = + Simplifier.clear_ss HOL_basic_ss addsimps @{thms all_simps[symmetric]} + +val meta_allI = @{lemma "ALL x. P x ==> (!!x. P x)" by auto} + +fun repeat f x = + case try f x of + SOME y => repeat f y + | NONE => x + +fun close_thm thy th = + fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of th) []) th + +fun cnf_axiom_xxx ctxt0 new_skolemizer ax_no th = + let + val ctxt0 = Variable.global_thm_context th + val thy = ProofContext.theory_of ctxt0 + val choice_ths = choice_theorems thy + val (opt, (nnf_th, ctxt)) = + nnf_axiom choice_ths new_skolemizer ax_no th ctxt0 + val skolem_ths = map (old_skolem_theorem_from_def thy) o old_skolem_defs + fun make_cnf th = Meson.make_cnf (skolem_ths th) th + val (cnf_ths, ctxt) = + make_cnf nnf_th ctxt + |> (fn (cnf, _) => + let + val _ = tracing ("nondef CNF: " ^ string_of_int (length cnf) ^ " clause(s)") + val sko_th = + nnf_th |> Simplifier.simplify all_out_ss + |> repeat (fn th => th RS meta_allI) + |> Meson.make_xxx_skolem ctxt (skolem_ths nnf_th) + |> close_thm thy + |> Conv.fconv_rule Object_Logic.atomize + |> to_definitional_cnf_with_quantifiers ctxt + in make_cnf sko_th ctxt end + | p => p) + fun intr_imp ct th = + Thm.instantiate ([], map (pairself (cterm_of thy)) + [(Var (("i", 0), @{typ nat}), + HOLogic.mk_nat ax_no)]) + (zero_var_indexes @{thm skolem_COMBK_D}) + RS Thm.implies_intr ct th + in + (NONE (*###*), + cnf_ths |> map (introduce_combinators_in_theorem + #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I)) + |> Variable.export ctxt ctxt0 + |> finish_cnf + |> map Thm.close_derivation) + end + + (* Convert a theorem to CNF, with additional premises due to skolemization. *) fun cnf_axiom ctxt0 new_skolemizer ax_no th = let @@ -382,8 +434,23 @@ val (cnf_ths, ctxt) = clausify nnf_th |> (fn ([], _) => - (* FIXME: This probably doesn't work with the new Skolemizer *) - clausify (to_definitional_cnf_with_quantifiers thy nnf_th) + if new_skolemizer then + let +val _ = tracing ("**** NEW CLAUSIFIER, DEF-CNF: " ^ Display.string_of_thm ctxt (to_definitional_cnf_with_quantifiers ctxt nnf_th)) (*###*) +val _ = tracing (" *** th: " ^ Display.string_of_thm ctxt th) (*###*) + val (_, (th1, ctxt)) = nnf_axiom choice_ths true ax_no th ctxt0 +val _ = tracing (" *** th1: " ^ Display.string_of_thm ctxt th1) (*###*) + val th2 = to_definitional_cnf_with_quantifiers ctxt th1 +val _ = tracing (" *** th2: " ^ Display.string_of_thm ctxt th2) (*###*) + val (ths3, ctxt) = clausify th2 +val _ = tracing (" *** hd ths3: " ^ Display.string_of_thm ctxt (hd ths3)) (*###*) + in (ths3, ctxt) end + else +let +val _ = tracing ("**** OLD CLAUSIFIER, DEF-CNF: " ^ Display.string_of_thm ctxt (to_definitional_cnf_with_quantifiers ctxt nnf_th)) +(*###*) in + clausify (to_definitional_cnf_with_quantifiers ctxt nnf_th) +end | p => p) fun intr_imp ct th = Thm.instantiate ([], map (pairself (cterm_of thy)) diff -r 8e58cc1390c7 -r cb8aa792d138 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Thu Apr 14 11:24:04 2011 +0200 +++ b/src/HOL/Tools/cnf_funcs.ML Thu Apr 14 11:24:04 2011 +0200 @@ -40,11 +40,12 @@ val clause_is_trivial: term -> bool val clause2raw_thm: thm -> thm + val make_nnf_thm: theory -> term -> thm val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *) - val make_cnf_thm: theory -> term -> thm - val make_cnfx_thm: theory -> term -> thm + val make_cnf_thm: Proof.context -> term -> thm + val make_cnfx_thm: Proof.context -> term -> thm val cnf_rewrite_tac: Proof.context -> int -> tactic (* converts all prems of a subgoal to CNF *) val cnfx_rewrite_tac: Proof.context -> int -> tactic (* converts all prems of a subgoal to (almost) definitional CNF *) @@ -252,6 +253,24 @@ end | make_nnf_thm thy t = inst_thm thy [t] iff_refl; +val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} +val eq_reflection = @{thm eq_reflection} + +fun make_under_quantifiers ctxt make t = + let + val thy = ProofContext.theory_of ctxt + fun conv ctxt ct = + case term_of ct of + (t1 as Const _) $ (t2 as Abs _) => + Conv.comb_conv (conv ctxt) ct + | Abs _ => Conv.abs_conv (conv o snd) ctxt ct + | Const _ => Conv.all_conv ct + | t => make t RS eq_reflection + in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end + +fun make_nnf_thm_under_quantifiers ctxt = + make_under_quantifiers ctxt (make_nnf_thm (ProofContext.theory_of ctxt)) + (* ------------------------------------------------------------------------- *) (* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *) (* t, but simplified wrt. the following theorems: *) @@ -323,8 +342,9 @@ (* in the length of the term. *) (* ------------------------------------------------------------------------- *) -fun make_cnf_thm thy t = +fun make_cnf_thm ctxt t = let + val thy = ProofContext.theory_of ctxt fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) = let val thm1 = make_cnf_thm_from_nnf x @@ -361,13 +381,19 @@ end | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl (* convert 't' to NNF first *) + val nnf_thm = make_nnf_thm_under_quantifiers ctxt t +(*### val nnf_thm = make_nnf_thm thy t +*) val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm (* then simplify wrt. True/False (this should preserve NNF) *) val simp_thm = simp_True_False_thm thy nnf val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm (* finally, convert to CNF (this should preserve the simplification) *) + val cnf_thm = make_under_quantifiers ctxt make_cnf_thm_from_nnf simp +(* ### val cnf_thm = make_cnf_thm_from_nnf simp +*) in iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm] end; @@ -386,8 +412,9 @@ (* in the case of nested equivalences. *) (* ------------------------------------------------------------------------- *) -fun make_cnfx_thm thy t = +fun make_cnfx_thm ctxt t = let + val thy = ProofContext.theory_of ctxt val var_id = Unsynchronized.ref 0 (* properly initialized below *) fun new_free () = Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT) @@ -465,7 +492,10 @@ end | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl (* convert 't' to NNF first *) + val nnf_thm = make_nnf_thm_under_quantifiers ctxt t +(* ### val nnf_thm = make_nnf_thm thy t +*) val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm (* then simplify wrt. True/False (this should preserve NNF) *) val simp_thm = simp_True_False_thm thy nnf @@ -483,7 +513,10 @@ Int.max (max, the_default 0 idx) end) (OldTerm.term_frees simp) 0) (* finally, convert to definitional CNF (this should preserve the simplification) *) + val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp +(*### val cnfx_thm = make_cnfx_thm_from_nnf simp +*) in iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm] end; @@ -509,8 +542,7 @@ (* cut the CNF formulas as new premises *) Subgoal.FOCUS (fn {prems, ...} => let - val thy = ProofContext.theory_of ctxt - val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems + val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems) in cut_facts_tac cut_thms 1 @@ -532,8 +564,7 @@ (* cut the CNF formulas as new premises *) Subgoal.FOCUS (fn {prems, ...} => let - val thy = ProofContext.theory_of ctxt; - val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems + val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o prop_of) prems val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems) in cut_facts_tac cut_thms 1