# HG changeset patch # User wenzelm # Date 1294416420 -3600 # Node ID 537b290bbe387fa3bbfae225a6a65f790a596ad3 # Parent 92facb55382352e93738bd088321f646f96e0a52 tuned whitespace, indentation, comments; diff -r 92facb553823 -r 537b290bbe38 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Fri Jan 07 16:11:02 2011 +0100 +++ b/src/HOL/Tools/cnf_funcs.ML Fri Jan 07 17:07:00 2011 +0100 @@ -34,20 +34,20 @@ signature CNF = sig - val is_atom: term -> bool - val is_literal: term -> bool - val is_clause: term -> bool - val clause_is_trivial: term -> bool + val is_atom: term -> bool + val is_literal: term -> bool + val is_clause: term -> bool + val clause_is_trivial: term -> bool - val clause2raw_thm: thm -> thm + val clause2raw_thm: thm -> thm - val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *) + 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 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 *) + val make_cnf_thm: theory -> term -> thm + val make_cnfx_thm: theory -> 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 *) end; structure cnf : CNF = @@ -93,39 +93,35 @@ val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto}; -fun is_atom (Const (@{const_name False}, _)) = false - | is_atom (Const (@{const_name True}, _)) = false - | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false - | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false - | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false - | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false - | is_atom (Const (@{const_name Not}, _) $ _) = false - | is_atom _ = true; +fun is_atom (Const (@{const_name False}, _)) = false + | is_atom (Const (@{const_name True}, _)) = false + | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false + | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false + | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false + | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false + | is_atom (Const (@{const_name Not}, _) $ _) = false + | is_atom _ = true; fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x - | is_literal x = is_atom x; + | is_literal x = is_atom x; fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y - | is_clause x = is_literal x; + | is_clause x = is_literal x; (* ------------------------------------------------------------------------- *) (* clause_is_trivial: a clause is trivially true if it contains both an atom *) (* and the atom's negation *) (* ------------------------------------------------------------------------- *) -(* Term.term -> bool *) - fun clause_is_trivial c = - let - (* Term.term -> Term.term *) - fun dual (Const (@{const_name Not}, _) $ x) = x - | dual x = HOLogic.Not $ x - (* Term.term list -> bool *) - fun has_duals [] = false - | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs - in - has_duals (HOLogic.disjuncts c) - end; + let + fun dual (Const (@{const_name Not}, _) $ x) = x + | dual x = HOLogic.Not $ x + fun has_duals [] = false + | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs + in + has_duals (HOLogic.disjuncts c) + end; (* ------------------------------------------------------------------------- *) (* clause2raw_thm: translates a clause into a raw clause, i.e. *) @@ -135,41 +131,39 @@ (* where each xi' is the negation normal form of ~xi *) (* ------------------------------------------------------------------------- *) -(* Thm.thm -> Thm.thm *) - fun clause2raw_thm clause = -let - (* eliminates negated disjunctions from the i-th premise, possibly *) - (* adding new premises, then continues with the (i+1)-th premise *) - (* int -> Thm.thm -> Thm.thm *) - fun not_disj_to_prem i thm = - if i > nprems_of thm then - thm - else - not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) - (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *) - (* becomes "[..., A1, ..., An] |- B" *) - (* Thm.thm -> Thm.thm *) - fun prems_to_hyps thm = - fold (fn cprem => fn thm' => - Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm -in - (* [...] |- ~(x1 | ... | xn) ==> False *) - (clause2raw_notE OF [clause]) - (* [...] |- ~x1 ==> ... ==> ~xn ==> False *) - |> not_disj_to_prem 1 - (* [...] |- x1' ==> ... ==> xn' ==> False *) - |> Seq.hd o TRYALL (rtac clause2raw_not_not) - (* [..., x1', ..., xn'] |- False *) - |> prems_to_hyps -end; + let + (* eliminates negated disjunctions from the i-th premise, possibly *) + (* adding new premises, then continues with the (i+1)-th premise *) + (* int -> Thm.thm -> Thm.thm *) + fun not_disj_to_prem i thm = + if i > nprems_of thm then + thm + else + not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) + (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *) + (* becomes "[..., A1, ..., An] |- B" *) + (* Thm.thm -> Thm.thm *) + fun prems_to_hyps thm = + fold (fn cprem => fn thm' => + Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm + in + (* [...] |- ~(x1 | ... | xn) ==> False *) + (clause2raw_notE OF [clause]) + (* [...] |- ~x1 ==> ... ==> ~xn ==> False *) + |> not_disj_to_prem 1 + (* [...] |- x1' ==> ... ==> xn' ==> False *) + |> Seq.hd o TRYALL (rtac clause2raw_not_not) + (* [..., x1', ..., xn'] |- False *) + |> prems_to_hyps + end; (* ------------------------------------------------------------------------- *) (* inst_thm: instantiates a theorem with a list of terms *) (* ------------------------------------------------------------------------- *) fun inst_thm thy ts thm = - instantiate' [] (map (SOME o cterm_of thy) ts) thm; + instantiate' [] (map (SOME o cterm_of thy) ts) thm; (* ------------------------------------------------------------------------- *) (* Naive CNF transformation *) @@ -182,80 +176,81 @@ (* eliminated (possibly causing an exponential blowup) *) (* ------------------------------------------------------------------------- *) -(* Theory.theory -> Term.term -> Thm.thm *) - fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) = - let - val thm1 = make_nnf_thm thy x - val thm2 = make_nnf_thm thy y - in - conj_cong OF [thm1, thm2] - end + let + val thm1 = make_nnf_thm thy x + val thm2 = make_nnf_thm thy y + in + conj_cong OF [thm1, thm2] + end | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) = - let - val thm1 = make_nnf_thm thy x - val thm2 = make_nnf_thm thy y - in - disj_cong OF [thm1, thm2] - end + let + val thm1 = make_nnf_thm thy x + val thm2 = make_nnf_thm thy y + in + disj_cong OF [thm1, thm2] + end | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) = - let - val thm1 = make_nnf_thm thy (HOLogic.Not $ x) - val thm2 = make_nnf_thm thy y - in - make_nnf_imp OF [thm1, thm2] - end + let + val thm1 = make_nnf_thm thy (HOLogic.Not $ x) + val thm2 = make_nnf_thm thy y + in + make_nnf_imp OF [thm1, thm2] + end | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) = - let - val thm1 = make_nnf_thm thy x - val thm2 = make_nnf_thm thy (HOLogic.Not $ x) - val thm3 = make_nnf_thm thy y - val thm4 = make_nnf_thm thy (HOLogic.Not $ y) - in - make_nnf_iff OF [thm1, thm2, thm3, thm4] - end + let + val thm1 = make_nnf_thm thy x + val thm2 = make_nnf_thm thy (HOLogic.Not $ x) + val thm3 = make_nnf_thm thy y + val thm4 = make_nnf_thm thy (HOLogic.Not $ y) + in + make_nnf_iff OF [thm1, thm2, thm3, thm4] + end | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) = - make_nnf_not_false + make_nnf_not_false | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) = - make_nnf_not_true + make_nnf_not_true | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) = - let - val thm1 = make_nnf_thm thy (HOLogic.Not $ x) - val thm2 = make_nnf_thm thy (HOLogic.Not $ y) - in - make_nnf_not_conj OF [thm1, thm2] - end + let + val thm1 = make_nnf_thm thy (HOLogic.Not $ x) + val thm2 = make_nnf_thm thy (HOLogic.Not $ y) + in + make_nnf_not_conj OF [thm1, thm2] + end | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) = - let - val thm1 = make_nnf_thm thy (HOLogic.Not $ x) - val thm2 = make_nnf_thm thy (HOLogic.Not $ y) - in - make_nnf_not_disj OF [thm1, thm2] - end - | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.implies}, _) $ x $ y)) = - let - val thm1 = make_nnf_thm thy x - val thm2 = make_nnf_thm thy (HOLogic.Not $ y) - in - make_nnf_not_imp OF [thm1, thm2] - end - | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) = - let - val thm1 = make_nnf_thm thy x - val thm2 = make_nnf_thm thy (HOLogic.Not $ x) - val thm3 = make_nnf_thm thy y - val thm4 = make_nnf_thm thy (HOLogic.Not $ y) - in - make_nnf_not_iff OF [thm1, thm2, thm3, thm4] - end + let + val thm1 = make_nnf_thm thy (HOLogic.Not $ x) + val thm2 = make_nnf_thm thy (HOLogic.Not $ y) + in + make_nnf_not_disj OF [thm1, thm2] + end + | make_nnf_thm thy + (Const (@{const_name Not}, _) $ + (Const (@{const_name HOL.implies}, _) $ x $ y)) = + let + val thm1 = make_nnf_thm thy x + val thm2 = make_nnf_thm thy (HOLogic.Not $ y) + in + make_nnf_not_imp OF [thm1, thm2] + end + | make_nnf_thm thy + (Const (@{const_name Not}, _) $ + (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) = + let + val thm1 = make_nnf_thm thy x + val thm2 = make_nnf_thm thy (HOLogic.Not $ x) + val thm3 = make_nnf_thm thy y + val thm4 = make_nnf_thm thy (HOLogic.Not $ y) + in + make_nnf_not_iff OF [thm1, thm2, thm3, thm4] + end | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) = - let - val thm1 = make_nnf_thm thy x - in - make_nnf_not_not OF [thm1] - end - | make_nnf_thm thy t = - inst_thm thy [t] iff_refl; + let + val thm1 = make_nnf_thm thy x + in + make_nnf_not_not OF [thm1] + end + | make_nnf_thm thy t = inst_thm thy [t] iff_refl; (* ------------------------------------------------------------------------- *) (* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *) @@ -277,51 +272,50 @@ (* Theory.theory -> Term.term -> Thm.thm *) fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) = - let - val thm1 = simp_True_False_thm thy x - val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 - in - if x' = HOLogic.false_const then - simp_TF_conj_False_l OF [thm1] (* (x & y) = False *) - else - let - val thm2 = simp_True_False_thm thy y - val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 - in - if x' = HOLogic.true_const then - simp_TF_conj_True_l OF [thm1, thm2] (* (x & y) = y' *) - else if y' = HOLogic.false_const then - simp_TF_conj_False_r OF [thm2] (* (x & y) = False *) - else if y' = HOLogic.true_const then - simp_TF_conj_True_r OF [thm1, thm2] (* (x & y) = x' *) - else - conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *) - end - end + let + val thm1 = simp_True_False_thm thy x + val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 + in + if x' = HOLogic.false_const then + simp_TF_conj_False_l OF [thm1] (* (x & y) = False *) + else + let + val thm2 = simp_True_False_thm thy y + val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 + in + if x' = HOLogic.true_const then + simp_TF_conj_True_l OF [thm1, thm2] (* (x & y) = y' *) + else if y' = HOLogic.false_const then + simp_TF_conj_False_r OF [thm2] (* (x & y) = False *) + else if y' = HOLogic.true_const then + simp_TF_conj_True_r OF [thm1, thm2] (* (x & y) = x' *) + else + conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *) + end + end | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) = - let - val thm1 = simp_True_False_thm thy x - val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 - in - if x' = HOLogic.true_const then - simp_TF_disj_True_l OF [thm1] (* (x | y) = True *) - else - let - val thm2 = simp_True_False_thm thy y - val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 - in - if x' = HOLogic.false_const then - simp_TF_disj_False_l OF [thm1, thm2] (* (x | y) = y' *) - else if y' = HOLogic.true_const then - simp_TF_disj_True_r OF [thm2] (* (x | y) = True *) - else if y' = HOLogic.false_const then - simp_TF_disj_False_r OF [thm1, thm2] (* (x | y) = x' *) - else - disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) - end - end - | simp_True_False_thm thy t = - inst_thm thy [t] iff_refl; (* t = t *) + let + val thm1 = simp_True_False_thm thy x + val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 + in + if x' = HOLogic.true_const then + simp_TF_disj_True_l OF [thm1] (* (x | y) = True *) + else + let + val thm2 = simp_True_False_thm thy y + val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 + in + if x' = HOLogic.false_const then + simp_TF_disj_False_l OF [thm1, thm2] (* (x | y) = y' *) + else if y' = HOLogic.true_const then + simp_TF_disj_True_r OF [thm2] (* (x | y) = True *) + else if y' = HOLogic.false_const then + simp_TF_disj_False_r OF [thm1, thm2] (* (x | y) = x' *) + else + disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) + end + end + | simp_True_False_thm thy t = inst_thm thy [t] iff_refl; (* t = t *) (* ------------------------------------------------------------------------- *) (* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *) @@ -329,58 +323,54 @@ (* in the length of the term. *) (* ------------------------------------------------------------------------- *) -(* Theory.theory -> Term.term -> Thm.thm *) - fun make_cnf_thm thy t = -let - (* Term.term -> Thm.thm *) - fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) = - let - val thm1 = make_cnf_thm_from_nnf x - val thm2 = make_cnf_thm_from_nnf y - in - conj_cong OF [thm1, thm2] - end - | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) = - let - (* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *) - fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' = - let - val thm1 = make_cnf_disj_thm x1 y' - val thm2 = make_cnf_disj_thm x2 y' - in - make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *) - end - | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) = - let - val thm1 = make_cnf_disj_thm x' y1 - val thm2 = make_cnf_disj_thm x' y2 - in - make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) - end - | make_cnf_disj_thm x' y' = - inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *) - val thm1 = make_cnf_thm_from_nnf x - val thm2 = make_cnf_thm_from_nnf y - val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 - val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 - val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) - in - iff_trans OF [disj_thm, make_cnf_disj_thm x' y'] - end - | make_cnf_thm_from_nnf t = - inst_thm thy [t] iff_refl - (* convert 't' to NNF first *) - 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_cnf_thm_from_nnf simp -in - iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm] -end; + let + fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) = + let + val thm1 = make_cnf_thm_from_nnf x + val thm2 = make_cnf_thm_from_nnf y + in + conj_cong OF [thm1, thm2] + end + | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) = + let + (* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *) + fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' = + let + val thm1 = make_cnf_disj_thm x1 y' + val thm2 = make_cnf_disj_thm x2 y' + in + make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *) + end + | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) = + let + val thm1 = make_cnf_disj_thm x' y1 + val thm2 = make_cnf_disj_thm x' y2 + in + make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) + end + | make_cnf_disj_thm x' y' = + inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *) + val thm1 = make_cnf_thm_from_nnf x + val thm2 = make_cnf_thm_from_nnf y + val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 + val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 + val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) + in + iff_trans OF [disj_thm, make_cnf_disj_thm x' y'] + end + | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl + (* convert 't' to NNF first *) + 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_cnf_thm_from_nnf simp + in + iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm] + end; (* ------------------------------------------------------------------------- *) (* CNF transformation by introducing new literals *) @@ -396,106 +386,107 @@ (* in the case of nested equivalences. *) (* ------------------------------------------------------------------------- *) -(* Theory.theory -> Term.term -> Thm.thm *) - fun make_cnfx_thm thy t = -let - val var_id = Unsynchronized.ref 0 (* properly initialized below *) - fun new_free () = - Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT) - fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm = - let - val thm1 = make_cnfx_thm_from_nnf x - val thm2 = make_cnfx_thm_from_nnf y - in - conj_cong OF [thm1, thm2] - end - | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) = - if is_clause x andalso is_clause y then - inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl - else if is_literal y orelse is_literal x then let - (* produces a theorem "(x' | y') = t'", where x', y', and t' are *) - (* almost in CNF, and x' or y' is a literal *) - fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' = - let - val thm1 = make_cnfx_disj_thm x1 y' - val thm2 = make_cnfx_disj_thm x2 y' - in - make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *) - end - | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) = - let - val thm1 = make_cnfx_disj_thm x' y1 - val thm2 = make_cnfx_disj_thm x' y2 - in - make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) - end - | 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 () - val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *) - val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) - in - iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *) - end - | 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 () - val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *) - val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) - in - iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *) - end - | make_cnfx_disj_thm x' y' = - inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *) - val thm1 = make_cnfx_thm_from_nnf x - val thm2 = make_cnfx_thm_from_nnf y - val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 - val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 - val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) - in - iff_trans OF [disj_thm, make_cnfx_disj_thm x' y'] - end else let (* neither 'x' nor 'y' is a literal: introduce a fresh variable *) - val thm1 = inst_thm thy [x, y] make_cnfx_newlit (* (x | y) = EX v. (x | v) & (y | ~v) *) - val var = new_free () - val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var)) - val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *) - val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *) - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *) - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *) - in - iff_trans OF [thm1, thm5] - end - | make_cnfx_thm_from_nnf t = - inst_thm thy [t] iff_refl - (* convert 't' to NNF first *) - 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 - (* initialize var_id, in case the term already contains variables of the form "cnfx_" *) - val _ = (var_id := fold (fn free => fn max => - let - val (name, _) = dest_Free free - val idx = if String.isPrefix "cnfx_" name then - (Int.fromString o String.extract) (name, String.size "cnfx_", NONE) - else - NONE - in - 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_cnfx_thm_from_nnf simp -in - iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm] -end; + let + val var_id = Unsynchronized.ref 0 (* properly initialized below *) + fun new_free () = + Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT) + fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm = + let + val thm1 = make_cnfx_thm_from_nnf x + val thm2 = make_cnfx_thm_from_nnf y + in + conj_cong OF [thm1, thm2] + end + | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) = + if is_clause x andalso is_clause y then + inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl + else if is_literal y orelse is_literal x then + let + (* produces a theorem "(x' | y') = t'", where x', y', and t' are *) + (* almost in CNF, and x' or y' is a literal *) + fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' = + let + val thm1 = make_cnfx_disj_thm x1 y' + val thm2 = make_cnfx_disj_thm x2 y' + in + make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *) + end + | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) = + let + val thm1 = make_cnfx_disj_thm x' y1 + val thm2 = make_cnfx_disj_thm x' y2 + in + make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) + end + | 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 () + val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *) + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) + val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) + in + iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *) + end + | 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 () + val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *) + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) + val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) + in + iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *) + end + | make_cnfx_disj_thm x' y' = + inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *) + val thm1 = make_cnfx_thm_from_nnf x + val thm2 = make_cnfx_thm_from_nnf y + val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 + val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 + val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) + in + iff_trans OF [disj_thm, make_cnfx_disj_thm x' y'] + end + else + let (* neither 'x' nor 'y' is a literal: introduce a fresh variable *) + val thm1 = inst_thm thy [x, y] make_cnfx_newlit (* (x | y) = EX v. (x | v) & (y | ~v) *) + val var = new_free () + val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var)) + val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *) + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *) + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *) + val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *) + in + iff_trans OF [thm1, thm5] + end + | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl + (* convert 't' to NNF first *) + 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 + (* initialize var_id, in case the term already contains variables of the form "cnfx_" *) + val _ = (var_id := fold (fn free => fn max => + let + val (name, _) = dest_Free free + val idx = + if String.isPrefix "cnfx_" name then + (Int.fromString o String.extract) (name, String.size "cnfx_", NONE) + else + NONE + in + 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_cnfx_thm_from_nnf simp + in + iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm] + end; (* ------------------------------------------------------------------------- *) (* Tactics *) @@ -506,7 +497,7 @@ (* ------------------------------------------------------------------------- *) fun weakening_tac i = - dtac weakening_thm i THEN atac (i+1); + dtac weakening_thm i THEN atac (i+1); (* ------------------------------------------------------------------------- *) (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *) @@ -515,22 +506,22 @@ (* ------------------------------------------------------------------------- *) fun cnf_rewrite_tac ctxt i = - (* 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 cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems) - in - cut_facts_tac cut_thms 1 - end) ctxt i - (* remove the original premises *) - THEN SELECT_GOAL (fn thm => - let - val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) - in - PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm - end) i; + (* 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 cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems) + in + cut_facts_tac cut_thms 1 + end) ctxt i + (* remove the original premises *) + THEN SELECT_GOAL (fn thm => + let + val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) + in + PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm + end) i; (* ------------------------------------------------------------------------- *) (* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *) @@ -538,21 +529,21 @@ (* ------------------------------------------------------------------------- *) fun cnfx_rewrite_tac ctxt i = - (* 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 cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems) - in - cut_facts_tac cut_thms 1 - end) ctxt i - (* remove the original premises *) - THEN SELECT_GOAL (fn thm => - let - val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) - in - PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm - end) i; + (* 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 cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems) + in + cut_facts_tac cut_thms 1 + end) ctxt i + (* remove the original premises *) + THEN SELECT_GOAL (fn thm => + let + val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) + in + PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm + end) i; -end; (* of structure *) +end; diff -r 92facb553823 -r 537b290bbe38 src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Fri Jan 07 16:11:02 2011 +0100 +++ b/src/HOL/Tools/prop_logic.ML Fri Jan 07 17:07:00 2011 +0100 @@ -7,39 +7,39 @@ signature PROP_LOGIC = sig - datatype prop_formula = - True - | False - | BoolVar of int (* NOTE: only use indices >= 1 *) - | Not of prop_formula - | Or of prop_formula * prop_formula - | And of prop_formula * prop_formula + datatype prop_formula = + True + | False + | BoolVar of int (* NOTE: only use indices >= 1 *) + | Not of prop_formula + | Or of prop_formula * prop_formula + | And of prop_formula * prop_formula - val SNot : prop_formula -> prop_formula - val SOr : prop_formula * prop_formula -> prop_formula - val SAnd : prop_formula * prop_formula -> prop_formula - val simplify : prop_formula -> prop_formula (* eliminates True/False and double-negation *) + val SNot: prop_formula -> prop_formula + val SOr: prop_formula * prop_formula -> prop_formula + val SAnd: prop_formula * prop_formula -> prop_formula + val simplify: prop_formula -> prop_formula (* eliminates True/False and double-negation *) - val indices : prop_formula -> int list (* set of all variable indices *) - val maxidx : prop_formula -> int (* maximal variable index *) + val indices: prop_formula -> int list (* set of all variable indices *) + val maxidx: prop_formula -> int (* maximal variable index *) - val exists : prop_formula list -> prop_formula (* finite disjunction *) - val all : prop_formula list -> prop_formula (* finite conjunction *) - val dot_product : prop_formula list * prop_formula list -> prop_formula + val exists: prop_formula list -> prop_formula (* finite disjunction *) + val all: prop_formula list -> prop_formula (* finite conjunction *) + val dot_product: prop_formula list * prop_formula list -> prop_formula - val is_nnf : prop_formula -> bool (* returns true iff the formula is in negation normal form *) - val is_cnf : prop_formula -> bool (* returns true iff the formula is in conjunctive normal form *) + val is_nnf: prop_formula -> bool (* returns true iff the formula is in negation normal form *) + val is_cnf: prop_formula -> bool (* returns true iff the formula is in conjunctive normal form *) - val nnf : prop_formula -> prop_formula (* negation normal form *) - val cnf : prop_formula -> prop_formula (* conjunctive normal form *) - val defcnf : prop_formula -> prop_formula (* definitional cnf *) + val nnf: prop_formula -> prop_formula (* negation normal form *) + val cnf: prop_formula -> prop_formula (* conjunctive normal form *) + val defcnf: prop_formula -> prop_formula (* definitional cnf *) - val eval : (int -> bool) -> prop_formula -> bool (* semantics *) + val eval: (int -> bool) -> prop_formula -> bool (* semantics *) - (* propositional representation of HOL terms *) - val prop_formula_of_term : term -> int Termtab.table -> prop_formula * int Termtab.table - (* HOL term representation of propositional formulae *) - val term_of_prop_formula : prop_formula -> term + (* propositional representation of HOL terms *) + val prop_formula_of_term: term -> int Termtab.table -> prop_formula * int Termtab.table + (* HOL term representation of propositional formulae *) + val term_of_prop_formula: prop_formula -> term end; structure PropLogic : PROP_LOGIC = @@ -51,13 +51,13 @@ (* not/or/and *) (* ------------------------------------------------------------------------- *) - datatype prop_formula = - True - | False - | BoolVar of int (* NOTE: only use indices >= 1 *) - | Not of prop_formula - | Or of prop_formula * prop_formula - | And of prop_formula * prop_formula; +datatype prop_formula = + True + | False + | BoolVar of int (* NOTE: only use indices >= 1 *) + | Not of prop_formula + | Or of prop_formula * prop_formula + | And of prop_formula * prop_formula; (* ------------------------------------------------------------------------- *) (* The following constructor functions make sure that True and False do not *) @@ -65,114 +65,93 @@ (* perform double-negation elimination. *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> prop_formula *) - - fun SNot True = False - | SNot False = True - | SNot (Not fm) = fm - | SNot fm = Not fm; - - (* prop_formula * prop_formula -> prop_formula *) +fun SNot True = False + | SNot False = True + | SNot (Not fm) = fm + | SNot fm = Not fm; - fun SOr (True, _) = True - | SOr (_, True) = True - | SOr (False, fm) = fm - | SOr (fm, False) = fm - | SOr (fm1, fm2) = Or (fm1, fm2); +fun SOr (True, _) = True + | SOr (_, True) = True + | SOr (False, fm) = fm + | SOr (fm, False) = fm + | SOr (fm1, fm2) = Or (fm1, fm2); - (* prop_formula * prop_formula -> prop_formula *) - - fun SAnd (True, fm) = fm - | SAnd (fm, True) = fm - | SAnd (False, _) = False - | SAnd (_, False) = False - | SAnd (fm1, fm2) = And (fm1, fm2); +fun SAnd (True, fm) = fm + | SAnd (fm, True) = fm + | SAnd (False, _) = False + | SAnd (_, False) = False + | SAnd (fm1, fm2) = And (fm1, fm2); (* ------------------------------------------------------------------------- *) (* simplify: eliminates True/False below other connectives, and double- *) (* negation *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> prop_formula *) - - fun simplify (Not fm) = SNot (simplify fm) - | simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2) - | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2) - | simplify fm = fm; +fun simplify (Not fm) = SNot (simplify fm) + | simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2) + | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2) + | simplify fm = fm; (* ------------------------------------------------------------------------- *) (* indices: collects all indices of Boolean variables that occur in a *) (* propositional formula 'fm'; no duplicates *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> int list *) - - fun indices True = [] - | indices False = [] - | indices (BoolVar i) = [i] - | indices (Not fm) = indices fm - | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2) - | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2); +fun indices True = [] + | indices False = [] + | indices (BoolVar i) = [i] + | indices (Not fm) = indices fm + | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2) + | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2); (* ------------------------------------------------------------------------- *) (* maxidx: computes the maximal variable index occuring in a formula of *) (* propositional logic 'fm'; 0 if 'fm' contains no variable *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> int *) - - fun maxidx True = 0 - | maxidx False = 0 - | maxidx (BoolVar i) = i - | maxidx (Not fm) = maxidx fm - | maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2) - | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2); +fun maxidx True = 0 + | maxidx False = 0 + | maxidx (BoolVar i) = i + | maxidx (Not fm) = maxidx fm + | maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2) + | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2); (* ------------------------------------------------------------------------- *) (* exists: computes the disjunction over a list 'xs' of propositional *) (* formulas *) (* ------------------------------------------------------------------------- *) - (* prop_formula list -> prop_formula *) - - fun exists xs = Library.foldl SOr (False, xs); +fun exists xs = Library.foldl SOr (False, xs); (* ------------------------------------------------------------------------- *) (* all: computes the conjunction over a list 'xs' of propositional formulas *) (* ------------------------------------------------------------------------- *) - (* prop_formula list -> prop_formula *) - - fun all xs = Library.foldl SAnd (True, xs); +fun all xs = Library.foldl SAnd (True, xs); (* ------------------------------------------------------------------------- *) (* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn *) (* ------------------------------------------------------------------------- *) - (* prop_formula list * prop_formula list -> prop_formula *) - - fun dot_product (xs,ys) = exists (map SAnd (xs~~ys)); +fun dot_product (xs, ys) = exists (map SAnd (xs ~~ ys)); (* ------------------------------------------------------------------------- *) (* is_nnf: returns 'true' iff the formula is in negation normal form (i.e., *) (* only variables may be negated, but not subformulas). *) (* ------------------------------------------------------------------------- *) - local - fun is_literal (BoolVar _) = true - | is_literal (Not (BoolVar _)) = true - | is_literal _ = false - fun is_conj_disj (Or (fm1, fm2)) = - is_conj_disj fm1 andalso is_conj_disj fm2 - | is_conj_disj (And (fm1, fm2)) = - is_conj_disj fm1 andalso is_conj_disj fm2 - | is_conj_disj fm = - is_literal fm - in - fun is_nnf True = true - | is_nnf False = true - | is_nnf fm = is_conj_disj fm - end; +local + fun is_literal (BoolVar _) = true + | is_literal (Not (BoolVar _)) = true + | is_literal _ = false + fun is_conj_disj (Or (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2 + | is_conj_disj (And (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2 + | is_conj_disj fm = is_literal fm +in + fun is_nnf True = true + | is_nnf False = true + | is_nnf fm = is_conj_disj fm +end; (* ------------------------------------------------------------------------- *) (* is_cnf: returns 'true' iff the formula is in conjunctive normal form *) @@ -180,19 +159,19 @@ (* implies 'is_nnf'. *) (* ------------------------------------------------------------------------- *) - local - fun is_literal (BoolVar _) = true - | is_literal (Not (BoolVar _)) = true - | is_literal _ = false - fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2 - | is_disj fm = is_literal fm - fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2 - | is_conj fm = is_disj fm - in - fun is_cnf True = true - | is_cnf False = true - | is_cnf fm = is_conj fm - end; +local + fun is_literal (BoolVar _) = true + | is_literal (Not (BoolVar _)) = true + | is_literal _ = false + fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2 + | is_disj fm = is_literal fm + fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2 + | is_conj fm = is_disj fm +in + fun is_cnf True = true + | is_cnf False = true + | is_cnf fm = is_conj fm +end; (* ------------------------------------------------------------------------- *) (* nnf: computes the negation normal form of a formula 'fm' of propositional *) @@ -202,35 +181,31 @@ (* 'fm' if (and only if) 'is_nnf fm' returns 'true'. *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> prop_formula *) - - fun nnf fm = - let - fun - (* constants *) - nnf_aux True = True - | nnf_aux False = False - (* variables *) - | nnf_aux (BoolVar i) = (BoolVar i) - (* 'or' and 'and' as outermost connectives are left untouched *) - | nnf_aux (Or (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2) - | nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2) - (* 'not' + constant *) - | nnf_aux (Not True) = False - | nnf_aux (Not False) = True - (* 'not' + variable *) - | nnf_aux (Not (BoolVar i)) = Not (BoolVar i) - (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *) - | nnf_aux (Not (Or (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) - | nnf_aux (Not (And (fm1, fm2))) = SOr (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) - (* double-negation elimination *) - | nnf_aux (Not (Not fm)) = nnf_aux fm - in - if is_nnf fm then - fm - else - nnf_aux fm - end; +fun nnf fm = + let + fun + (* constants *) + nnf_aux True = True + | nnf_aux False = False + (* variables *) + | nnf_aux (BoolVar i) = (BoolVar i) + (* 'or' and 'and' as outermost connectives are left untouched *) + | nnf_aux (Or (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2) + | nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2) + (* 'not' + constant *) + | nnf_aux (Not True) = False + | nnf_aux (Not False) = True + (* 'not' + variable *) + | nnf_aux (Not (BoolVar i)) = Not (BoolVar i) + (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *) + | nnf_aux (Not (Or (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) + | nnf_aux (Not (And (fm1, fm2))) = SOr (nnf_aux (SNot fm1), nnf_aux (SNot fm2)) + (* double-negation elimination *) + | nnf_aux (Not (Not fm)) = nnf_aux fm + in + if is_nnf fm then fm + else nnf_aux fm + end; (* ------------------------------------------------------------------------- *) (* cnf: computes the conjunctive normal form (i.e., a conjunction of *) @@ -241,35 +216,30 @@ (* 'fm' if (and only if) 'is_cnf fm' returns 'true'. *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> prop_formula *) - - fun cnf fm = - let - (* function to push an 'Or' below 'And's, using distributive laws *) - fun cnf_or (And (fm11, fm12), fm2) = - And (cnf_or (fm11, fm2), cnf_or (fm12, fm2)) - | cnf_or (fm1, And (fm21, fm22)) = - And (cnf_or (fm1, fm21), cnf_or (fm1, fm22)) - (* neither subformula contains 'And' *) - | cnf_or (fm1, fm2) = - Or (fm1, fm2) - fun cnf_from_nnf True = True - | cnf_from_nnf False = False - | cnf_from_nnf (BoolVar i) = BoolVar i - (* 'fm' must be a variable since the formula is in NNF *) - | cnf_from_nnf (Not fm) = Not fm - (* 'Or' may need to be pushed below 'And' *) - | cnf_from_nnf (Or (fm1, fm2)) = - cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) - (* 'And' as outermost connective is left untouched *) - | cnf_from_nnf (And (fm1, fm2)) = - And (cnf_from_nnf fm1, cnf_from_nnf fm2) - in - if is_cnf fm then - fm - else - (cnf_from_nnf o nnf) fm - end; +fun cnf fm = + let + (* function to push an 'Or' below 'And's, using distributive laws *) + fun cnf_or (And (fm11, fm12), fm2) = + And (cnf_or (fm11, fm2), cnf_or (fm12, fm2)) + | cnf_or (fm1, And (fm21, fm22)) = + And (cnf_or (fm1, fm21), cnf_or (fm1, fm22)) + (* neither subformula contains 'And' *) + | cnf_or (fm1, fm2) = Or (fm1, fm2) + fun cnf_from_nnf True = True + | cnf_from_nnf False = False + | cnf_from_nnf (BoolVar i) = BoolVar i + (* 'fm' must be a variable since the formula is in NNF *) + | cnf_from_nnf (Not fm) = Not fm + (* 'Or' may need to be pushed below 'And' *) + | cnf_from_nnf (Or (fm1, fm2)) = + cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2) + (* 'And' as outermost connective is left untouched *) + | cnf_from_nnf (And (fm1, fm2)) = + And (cnf_from_nnf fm1, cnf_from_nnf fm2) + in + if is_cnf fm then fm + else (cnf_from_nnf o nnf) fm + end; (* ------------------------------------------------------------------------- *) (* defcnf: computes a definitional conjunctive normal form of a formula 'fm' *) @@ -282,86 +252,80 @@ (* 'is_cnf fm' returns 'true'. *) (* ------------------------------------------------------------------------- *) - (* prop_formula -> prop_formula *) - - fun defcnf fm = - if is_cnf fm then - fm - else - let - val fm' = nnf fm - (* 'new' specifies the next index that is available to introduce an auxiliary variable *) - (* int ref *) - val new = Unsynchronized.ref (maxidx fm' + 1) - (* unit -> int *) - fun new_idx () = let val idx = !new in new := idx+1; idx end - (* replaces 'And' by an auxiliary variable (and its definition) *) - (* prop_formula -> prop_formula * prop_formula list *) - fun defcnf_or (And x) = - let - val i = new_idx () - in - (* Note that definitions are in NNF, but not CNF. *) - (BoolVar i, [Or (Not (BoolVar i), And x)]) - end - | defcnf_or (Or (fm1, fm2)) = - let - val (fm1', defs1) = defcnf_or fm1 - val (fm2', defs2) = defcnf_or fm2 - in - (Or (fm1', fm2'), defs1 @ defs2) - end - | defcnf_or fm = - (fm, []) - (* prop_formula -> prop_formula *) - fun defcnf_from_nnf True = True - | defcnf_from_nnf False = False - | defcnf_from_nnf (BoolVar i) = BoolVar i - (* 'fm' must be a variable since the formula is in NNF *) - | defcnf_from_nnf (Not fm) = Not fm - (* 'Or' may need to be pushed below 'And' *) - (* 'Or' of literal and 'And': use distributivity *) - | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) = - And (defcnf_from_nnf (Or (BoolVar i, fm1)), - defcnf_from_nnf (Or (BoolVar i, fm2))) - | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) = - And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)), - defcnf_from_nnf (Or (Not (BoolVar i), fm2))) - | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) = - And (defcnf_from_nnf (Or (fm1, BoolVar i)), - defcnf_from_nnf (Or (fm2, BoolVar i))) - | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) = - And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))), - defcnf_from_nnf (Or (fm2, Not (BoolVar i)))) - (* all other cases: turn the formula into a disjunction of literals, *) - (* adding definitions as necessary *) - | defcnf_from_nnf (Or x) = - let - val (fm, defs) = defcnf_or (Or x) - val cnf_defs = map defcnf_from_nnf defs - in - all (fm :: cnf_defs) - end - (* 'And' as outermost connective is left untouched *) - | defcnf_from_nnf (And (fm1, fm2)) = - And (defcnf_from_nnf fm1, defcnf_from_nnf fm2) - in - defcnf_from_nnf fm' - end; +fun defcnf fm = + if is_cnf fm then fm + else + let + val fm' = nnf fm + (* 'new' specifies the next index that is available to introduce an auxiliary variable *) + (* int ref *) + val new = Unsynchronized.ref (maxidx fm' + 1) + (* unit -> int *) + fun new_idx () = let val idx = !new in new := idx+1; idx end + (* replaces 'And' by an auxiliary variable (and its definition) *) + (* prop_formula -> prop_formula * prop_formula list *) + fun defcnf_or (And x) = + let + val i = new_idx () + in + (* Note that definitions are in NNF, but not CNF. *) + (BoolVar i, [Or (Not (BoolVar i), And x)]) + end + | defcnf_or (Or (fm1, fm2)) = + let + val (fm1', defs1) = defcnf_or fm1 + val (fm2', defs2) = defcnf_or fm2 + in + (Or (fm1', fm2'), defs1 @ defs2) + end + | defcnf_or fm = (fm, []) + (* prop_formula -> prop_formula *) + fun defcnf_from_nnf True = True + | defcnf_from_nnf False = False + | defcnf_from_nnf (BoolVar i) = BoolVar i + (* 'fm' must be a variable since the formula is in NNF *) + | defcnf_from_nnf (Not fm) = Not fm + (* 'Or' may need to be pushed below 'And' *) + (* 'Or' of literal and 'And': use distributivity *) + | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) = + And (defcnf_from_nnf (Or (BoolVar i, fm1)), + defcnf_from_nnf (Or (BoolVar i, fm2))) + | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) = + And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)), + defcnf_from_nnf (Or (Not (BoolVar i), fm2))) + | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) = + And (defcnf_from_nnf (Or (fm1, BoolVar i)), + defcnf_from_nnf (Or (fm2, BoolVar i))) + | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) = + And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))), + defcnf_from_nnf (Or (fm2, Not (BoolVar i)))) + (* all other cases: turn the formula into a disjunction of literals, *) + (* adding definitions as necessary *) + | defcnf_from_nnf (Or x) = + let + val (fm, defs) = defcnf_or (Or x) + val cnf_defs = map defcnf_from_nnf defs + in + all (fm :: cnf_defs) + end + (* 'And' as outermost connective is left untouched *) + | defcnf_from_nnf (And (fm1, fm2)) = + And (defcnf_from_nnf fm1, defcnf_from_nnf fm2) + in + defcnf_from_nnf fm' + end; (* ------------------------------------------------------------------------- *) (* eval: given an assignment 'a' of Boolean values to variable indices, the *) (* truth value of a propositional formula 'fm' is computed *) (* ------------------------------------------------------------------------- *) - (* (int -> bool) -> prop_formula -> bool *) - - fun eval a True = true - | eval a False = false - | eval a (BoolVar i) = (a i) - | eval a (Not fm) = not (eval a fm) - | eval a (Or (fm1,fm2)) = (eval a fm1) orelse (eval a fm2) - | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2); +fun eval a True = true + | eval a False = false + | eval a (BoolVar i) = (a i) + | eval a (Not fm) = not (eval a fm) + | eval a (Or (fm1, fm2)) = (eval a fm1) orelse (eval a fm2) + | eval a (And (fm1, fm2)) = (eval a fm1) andalso (eval a fm2); (* ------------------------------------------------------------------------- *) (* prop_formula_of_term: returns the propositional structure of a HOL term, *) @@ -378,52 +342,47 @@ (* so that it does not have to be recomputed (by folding over the *) (* table) for each invocation. *) - (* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *) - fun prop_formula_of_term t table = - let - val next_idx_is_valid = Unsynchronized.ref false - val next_idx = Unsynchronized.ref 0 - fun get_next_idx () = - if !next_idx_is_valid then - Unsynchronized.inc next_idx - else ( - next_idx := Termtab.fold (Integer.max o snd) table 0; - next_idx_is_valid := true; - Unsynchronized.inc next_idx - ) - fun aux (Const (@{const_name True}, _)) table = - (True, table) - | aux (Const (@{const_name False}, _)) table = - (False, table) - | aux (Const (@{const_name Not}, _) $ x) table = - apfst Not (aux x table) - | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table = - let - val (fm1, table1) = aux x table - val (fm2, table2) = aux y table1 - in - (Or (fm1, fm2), table2) - end - | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table = - let - val (fm1, table1) = aux x table - val (fm2, table2) = aux y table1 - in - (And (fm1, fm2), table2) - end - | aux x table = - (case Termtab.lookup table x of - SOME i => - (BoolVar i, table) - | NONE => - let - val i = get_next_idx () - in - (BoolVar i, Termtab.update (x, i) table) - end) - in - aux t table - end; +fun prop_formula_of_term t table = + let + val next_idx_is_valid = Unsynchronized.ref false + val next_idx = Unsynchronized.ref 0 + fun get_next_idx () = + if !next_idx_is_valid then + Unsynchronized.inc next_idx + else ( + next_idx := Termtab.fold (Integer.max o snd) table 0; + next_idx_is_valid := true; + Unsynchronized.inc next_idx + ) + fun aux (Const (@{const_name True}, _)) table = (True, table) + | aux (Const (@{const_name False}, _)) table = (False, table) + | aux (Const (@{const_name Not}, _) $ x) table = apfst Not (aux x table) + | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table = + let + val (fm1, table1) = aux x table + val (fm2, table2) = aux y table1 + in + (Or (fm1, fm2), table2) + end + | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table = + let + val (fm1, table1) = aux x table + val (fm2, table2) = aux y table1 + in + (And (fm1, fm2), table2) + end + | aux x table = + (case Termtab.lookup table x of + SOME i => (BoolVar i, table) + | NONE => + let + val i = get_next_idx () + in + (BoolVar i, Termtab.update (x, i) table) + end) + in + aux t table + end; (* ------------------------------------------------------------------------- *) (* term_of_prop_formula: returns a HOL term that corresponds to a *) @@ -435,18 +394,13 @@ (* Boolean variables in the formula, similar to 'prop_formula_of_term' *) (* (but the other way round). *) - (* prop_formula -> Term.term *) - fun term_of_prop_formula True = - HOLogic.true_const - | term_of_prop_formula False = - HOLogic.false_const - | term_of_prop_formula (BoolVar i) = - Free ("v" ^ Int.toString i, HOLogic.boolT) - | term_of_prop_formula (Not fm) = - HOLogic.mk_not (term_of_prop_formula fm) - | term_of_prop_formula (Or (fm1, fm2)) = - HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2) - | term_of_prop_formula (And (fm1, fm2)) = - HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2); +fun term_of_prop_formula True = HOLogic.true_const + | term_of_prop_formula False = HOLogic.false_const + | term_of_prop_formula (BoolVar i) = Free ("v" ^ Int.toString i, HOLogic.boolT) + | term_of_prop_formula (Not fm) = HOLogic.mk_not (term_of_prop_formula fm) + | term_of_prop_formula (Or (fm1, fm2)) = + HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2) + | term_of_prop_formula (And (fm1, fm2)) = + HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2); end; diff -r 92facb553823 -r 537b290bbe38 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Fri Jan 07 16:11:02 2011 +0100 +++ b/src/HOL/Tools/sat_funcs.ML Fri Jan 07 17:07:00 2011 +0100 @@ -48,13 +48,13 @@ signature SAT = sig - val trace_sat: bool Unsynchronized.ref (* input: print trace messages *) - val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *) - val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *) - val rawsat_thm: Proof.context -> cterm list -> thm - val rawsat_tac: Proof.context -> int -> tactic - val sat_tac: Proof.context -> int -> tactic - val satx_tac: Proof.context -> int -> tactic + val trace_sat: bool Unsynchronized.ref (* input: print trace messages *) + val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *) + val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *) + val rawsat_thm: Proof.context -> cterm list -> thm + val rawsat_tac: Proof.context -> int -> tactic + val sat_tac: Proof.context -> int -> tactic + val satx_tac: Proof.context -> int -> tactic end functor SATFunc(cnf : CNF) : SAT = @@ -78,8 +78,7 @@ (* or negatively) as equal *) (* ------------------------------------------------------------------------- *) -fun lit_ord (i, j) = - int_ord (abs i, abs j); +fun lit_ord (i, j) = int_ord (abs i, abs j); (* ------------------------------------------------------------------------- *) (* CLAUSE: during proof reconstruction, three kinds of clauses are *) @@ -91,9 +90,10 @@ (* reconstruction *) (* ------------------------------------------------------------------------- *) -datatype CLAUSE = NO_CLAUSE - | ORIG_CLAUSE of thm - | RAW_CLAUSE of thm * (int * cterm) list; +datatype CLAUSE = + NO_CLAUSE + | ORIG_CLAUSE of thm + | RAW_CLAUSE of thm * (int * cterm) list; (* ------------------------------------------------------------------------- *) (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *) @@ -117,88 +117,87 @@ (* cterms. *) (* ------------------------------------------------------------------------- *) -(* (Thm.thm * (int * Thm.cterm) list) list -> Thm.thm * (int * Thm.cterm) list *) - fun resolve_raw_clauses [] = raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, []) | resolve_raw_clauses (c::cs) = - let - (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *) - fun merge xs [] = xs - | merge [] ys = ys - | merge (x::xs) (y::ys) = - (case (lit_ord o pairself fst) (x, y) of - LESS => x :: merge xs (y::ys) - | EQUAL => x :: merge xs ys - | GREATER => y :: merge (x::xs) ys) + let + (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *) + fun merge xs [] = xs + | merge [] ys = ys + | merge (x :: xs) (y :: ys) = + (case (lit_ord o pairself fst) (x, y) of + LESS => x :: merge xs (y :: ys) + | EQUAL => x :: merge xs ys + | GREATER => y :: merge (x :: xs) ys) - (* find out which two hyps are used in the resolution *) - (* (int * Thm.cterm) list * (int * Thm.cterm) list -> (int * Thm.cterm) list -> bool * Thm.cterm * Thm.cterm * (int * Thm.cterm) list *) - fun find_res_hyps ([], _) _ = - raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) - | find_res_hyps (_, []) _ = - raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) - | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc = - (case (lit_ord o pairself fst) (h1, h2) of - LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc) - | EQUAL => let - val (i1, chyp1) = h1 - val (i2, chyp2) = h2 - in - if i1 = ~ i2 then - (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2) - else (* i1 = i2 *) - find_res_hyps (hyps1, hyps2) (h1 :: acc) - end - | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc)) + (* find out which two hyps are used in the resolution *) + fun find_res_hyps ([], _) _ = + raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) + | find_res_hyps (_, []) _ = + raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) + | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc = + (case (lit_ord o pairself fst) (h1, h2) of + LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc) + | EQUAL => + let + val (i1, chyp1) = h1 + val (i2, chyp2) = h2 + in + if i1 = ~ i2 then + (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2) + else (* i1 = i2 *) + find_res_hyps (hyps1, hyps2) (h1 :: acc) + end + | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc)) - (* Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list *) - fun resolution (c1, hyps1) (c2, hyps2) = - let - val _ = - if ! trace_sat then - tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^ - " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1)) - ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^ - " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")") - else () + fun resolution (c1, hyps1) (c2, hyps2) = + let + val _ = + if ! trace_sat then + tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^ + " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1)) + ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^ + " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")") + else () - (* the two literals used for resolution *) - val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) [] + (* the two literals used for resolution *) + val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) [] - val c1' = Thm.implies_intr hyp1 c1 (* Gamma1 |- hyp1 ==> False *) - val c2' = Thm.implies_intr hyp2 c2 (* Gamma2 |- hyp2 ==> False *) + val c1' = Thm.implies_intr hyp1 c1 (* Gamma1 |- hyp1 ==> False *) + val c2' = Thm.implies_intr hyp2 c2 (* Gamma2 |- hyp2 ==> False *) - val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *) - let - val cLit = snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) - in - Thm.instantiate ([], [(cP, cLit)]) resolution_thm - end + val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *) + let + val cLit = + snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) + in + Thm.instantiate ([], [(cP, cLit)]) resolution_thm + end - val _ = - if !trace_sat then - tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm) - else () + val _ = + if !trace_sat then + tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm) + else () - (* Gamma1, Gamma2 |- False *) - val c_new = Thm.implies_elim - (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1')) - (if hyp1_is_neg then c1' else c2') + (* Gamma1, Gamma2 |- False *) + val c_new = + Thm.implies_elim + (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1')) + (if hyp1_is_neg then c1' else c2') - val _ = - if !trace_sat then - tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^ - " (hyps: " ^ ML_Syntax.print_list - (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")") - else () - val _ = Unsynchronized.inc counter - in - (c_new, new_hyps) - end - in - fold resolution cs c - end; + val _ = + if !trace_sat then + tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^ + " (hyps: " ^ ML_Syntax.print_list + (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")") + else () + val _ = Unsynchronized.inc counter + in + (c_new, new_hyps) + end + in + fold resolution cs c + end; (* ------------------------------------------------------------------------- *) (* replay_proof: replays the resolution proof returned by the SAT solver; *) @@ -210,68 +209,71 @@ (* occur (as part of a literal) in 'clauses' to positive integers. *) (* ------------------------------------------------------------------------- *) -(* int Termtab.table -> CLAUSE Array.array -> SatSolver.proof -> Thm.thm *) - fun replay_proof atom_table clauses (clause_table, empty_id) = -let - (* Thm.cterm -> int option *) - fun index_of_literal chyp = ( - case (HOLogic.dest_Trueprop o Thm.term_of) chyp of - (Const (@{const_name Not}, _) $ atom) => - SOME (~ (the (Termtab.lookup atom_table atom))) - | atom => - SOME (the (Termtab.lookup atom_table atom)) - ) handle TERM _ => NONE; (* 'chyp' is not a literal *) + let + fun index_of_literal chyp = + (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of + (Const (@{const_name Not}, _) $ atom) => + SOME (~ (the (Termtab.lookup atom_table atom))) + | atom => SOME (the (Termtab.lookup atom_table atom))) + handle TERM _ => NONE; (* 'chyp' is not a literal *) - (* int -> Thm.thm * (int * Thm.cterm) list *) - fun prove_clause id = - case Array.sub (clauses, id) of - RAW_CLAUSE clause => - clause - | ORIG_CLAUSE thm => - (* convert the original clause *) - let - val _ = if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else () - val raw = cnf.clause2raw_thm thm - val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp => - Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw))) - val clause = (raw, hyps) - val _ = Array.update (clauses, id, RAW_CLAUSE clause) - in - clause - end - | NO_CLAUSE => - (* prove the clause, using information from 'clause_table' *) - let - val _ = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else () - val ids = the (Inttab.lookup clause_table id) - val clause = resolve_raw_clauses (map prove_clause ids) - val _ = Array.update (clauses, id, RAW_CLAUSE clause) - val _ = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else () - in - clause - end + fun prove_clause id = + (case Array.sub (clauses, id) of + RAW_CLAUSE clause => clause + | ORIG_CLAUSE thm => + (* convert the original clause *) + let + val _ = + if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else () + val raw = cnf.clause2raw_thm thm + val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp => + Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw))) + val clause = (raw, hyps) + val _ = Array.update (clauses, id, RAW_CLAUSE clause) + in + clause + end + | NO_CLAUSE => + (* prove the clause, using information from 'clause_table' *) + let + val _ = + if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else () + val ids = the (Inttab.lookup clause_table id) + val clause = resolve_raw_clauses (map prove_clause ids) + val _ = Array.update (clauses, id, RAW_CLAUSE clause) + val _ = + if !trace_sat then + tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) + else () + in + clause + end) - val _ = counter := 0 - val empty_clause = fst (prove_clause empty_id) - val _ = if !trace_sat then tracing ("Proof reconstruction successful; " ^ string_of_int (!counter) ^ " resolution step(s) total.") else () -in - empty_clause -end; + val _ = counter := 0 + val empty_clause = fst (prove_clause empty_id) + val _ = + if !trace_sat then + tracing ("Proof reconstruction successful; " ^ + string_of_int (!counter) ^ " resolution step(s) total.") + else () + in + empty_clause + end; (* ------------------------------------------------------------------------- *) (* string_of_prop_formula: return a human-readable string representation of *) (* a 'prop_formula' (just for tracing) *) (* ------------------------------------------------------------------------- *) -(* PropLogic.prop_formula -> string *) - -fun string_of_prop_formula PropLogic.True = "True" - | string_of_prop_formula PropLogic.False = "False" - | string_of_prop_formula (PropLogic.BoolVar i) = "x" ^ string_of_int i - | string_of_prop_formula (PropLogic.Not fm) = "~" ^ string_of_prop_formula fm - | string_of_prop_formula (PropLogic.Or (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")" - | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; +fun string_of_prop_formula PropLogic.True = "True" + | string_of_prop_formula PropLogic.False = "False" + | string_of_prop_formula (PropLogic.BoolVar i) = "x" ^ string_of_int i + | string_of_prop_formula (PropLogic.Not fm) = "~" ^ string_of_prop_formula fm + | string_of_prop_formula (PropLogic.Or (fm1, fm2)) = + "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")" + | string_of_prop_formula (PropLogic.And (fm1, fm2)) = + "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")"; (* ------------------------------------------------------------------------- *) (* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *) @@ -281,112 +283,120 @@ (* ------------------------------------------------------------------------- *) fun rawsat_thm ctxt clauses = -let - (* remove premises that equal "True" *) - val clauses' = filter (fn clause => - (not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause - handle TERM ("dest_Trueprop", _) => true) clauses - (* remove non-clausal premises -- of course this shouldn't actually *) - (* remove anything as long as 'rawsat_tac' is only called after the *) - (* premises have been converted to clauses *) - val clauses'' = filter (fn clause => - ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause - handle TERM ("dest_Trueprop", _) => false) - orelse ( - warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause)); - false)) clauses' - (* remove trivial clauses -- this is necessary because zChaff removes *) - (* trivial clauses during preprocessing, and otherwise our clause *) - (* numbering would be off *) - val nontrivial_clauses = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses'' - (* sort clauses according to the term order -- an optimization, *) - (* useful because forming the union of hypotheses, as done by *) - (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *) - (* terms sorted in descending order, while only linear for terms *) - (* sorted in ascending order *) - val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses - val _ = if !trace_sat then - tracing ("Sorted non-trivial clauses:\n" ^ - cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) - else () - (* translate clauses from HOL terms to PropLogic.prop_formula *) - val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty - val _ = if !trace_sat then - tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) - else () - val fm = PropLogic.all fms - (* unit -> Thm.thm *) - fun make_quick_and_dirty_thm () = - let - val _ = if !trace_sat then - tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." - else () - val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const) - in - (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *) - (* Thm.weaken sorted_clauses' would be quadratic, since we sorted *) - (* clauses in ascending order (which is linear for *) - (* 'Conjunction.intr_balanced', used below) *) - fold Thm.weaken (rev sorted_clauses) False_thm - end -in - case - let val the_solver = ! solver - in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end - of - SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => ( - if !trace_sat then - tracing ("Proof trace from SAT solver:\n" ^ - "clauses: " ^ ML_Syntax.print_list - (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) - (Inttab.dest clause_table) ^ "\n" ^ - "empty clause: " ^ Int.toString empty_id) - else (); - if !quick_and_dirty then - make_quick_and_dirty_thm () - else - let - (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i"; *) - (* this avoids accumulation of hypotheses during resolution *) - (* [c_1, ..., c_n] |- c_1 && ... && c_n *) - val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses) - (* [c_1 && ... && c_n] |- c_1 && ... && c_n *) - val cnf_cterm = cprop_of clauses_thm - val cnf_thm = Thm.assume cnf_cterm - (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *) - val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm - (* initialize the clause array with the given clauses *) - val max_idx = the (Inttab.max_key clause_table) - val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) - val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) cnf_clauses 0 - (* replay the proof to derive the empty clause *) - (* [c_1 && ... && c_n] |- False *) - val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id) - in - (* [c_1, ..., c_n] |- False *) - Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm - end) - | SatSolver.UNSATISFIABLE NONE => - if !quick_and_dirty then ( - warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"; - make_quick_and_dirty_thm () - ) else - raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, []) - | SatSolver.SATISFIABLE assignment => - let - val msg = "SAT solver found a countermodel:\n" - ^ (commas - o map (fn (term, idx) => - Syntax.string_of_term_global @{theory} term ^ ": " ^ - (case assignment idx of NONE => "arbitrary" - | SOME true => "true" | SOME false => "false"))) - (Termtab.dest atom_table) - in - raise THM (msg, 0, []) - end - | SatSolver.UNKNOWN => - raise THM ("SAT solver failed to decide the formula", 0, []) -end; + let + (* remove premises that equal "True" *) + val clauses' = filter (fn clause => + (not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause + handle TERM ("dest_Trueprop", _) => true) clauses + (* remove non-clausal premises -- of course this shouldn't actually *) + (* remove anything as long as 'rawsat_tac' is only called after the *) + (* premises have been converted to clauses *) + val clauses'' = filter (fn clause => + ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause + handle TERM ("dest_Trueprop", _) => false) + orelse ( + warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause)); + false)) clauses' + (* remove trivial clauses -- this is necessary because zChaff removes *) + (* trivial clauses during preprocessing, and otherwise our clause *) + (* numbering would be off *) + val nontrivial_clauses = + filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses'' + (* sort clauses according to the term order -- an optimization, *) + (* useful because forming the union of hypotheses, as done by *) + (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *) + (* terms sorted in descending order, while only linear for terms *) + (* sorted in ascending order *) + val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses + val _ = + if !trace_sat then + tracing ("Sorted non-trivial clauses:\n" ^ + cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) + else () + (* translate clauses from HOL terms to PropLogic.prop_formula *) + val (fms, atom_table) = + fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) + sorted_clauses Termtab.empty + val _ = + if !trace_sat then + tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) + else () + val fm = PropLogic.all fms + (* unit -> Thm.thm *) + fun make_quick_and_dirty_thm () = + let + val _ = + if !trace_sat then + tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead." + else () + val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const) + in + (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *) + (* Thm.weaken sorted_clauses' would be quadratic, since we sorted *) + (* clauses in ascending order (which is linear for *) + (* 'Conjunction.intr_balanced', used below) *) + fold Thm.weaken (rev sorted_clauses) False_thm + end + in + case + let val the_solver = ! solver + in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end + of + SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => + (if !trace_sat then + tracing ("Proof trace from SAT solver:\n" ^ + "clauses: " ^ ML_Syntax.print_list + (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) + (Inttab.dest clause_table) ^ "\n" ^ + "empty clause: " ^ Int.toString empty_id) + else (); + if !quick_and_dirty then + make_quick_and_dirty_thm () + else + let + (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i"; *) + (* this avoids accumulation of hypotheses during resolution *) + (* [c_1, ..., c_n] |- c_1 && ... && c_n *) + val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses) + (* [c_1 && ... && c_n] |- c_1 && ... && c_n *) + val cnf_cterm = cprop_of clauses_thm + val cnf_thm = Thm.assume cnf_cterm + (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *) + val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm + (* initialize the clause array with the given clauses *) + val max_idx = the (Inttab.max_key clause_table) + val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) + val _ = + fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) + cnf_clauses 0 + (* replay the proof to derive the empty clause *) + (* [c_1 && ... && c_n] |- False *) + val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id) + in + (* [c_1, ..., c_n] |- False *) + Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm + end) + | SatSolver.UNSATISFIABLE NONE => + if !quick_and_dirty then + (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"; + make_quick_and_dirty_thm ()) + else + raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, []) + | SatSolver.SATISFIABLE assignment => + let + val msg = + "SAT solver found a countermodel:\n" ^ + (commas o map (fn (term, idx) => + Syntax.string_of_term_global @{theory} term ^ ": " ^ + (case assignment idx of NONE => "arbitrary" + | SOME true => "true" | SOME false => "false"))) + (Termtab.dest atom_table) + in + raise THM (msg, 0, []) + end + | SatSolver.UNKNOWN => + raise THM ("SAT solver failed to decide the formula", 0, []) + end; (* ------------------------------------------------------------------------- *) (* Tactics *) @@ -417,9 +427,9 @@ (* ------------------------------------------------------------------------- *) val pre_cnf_tac = - rtac ccontr THEN' - Object_Logic.atomize_prems_tac THEN' - CONVERSION Drule.beta_eta_conversion; + rtac ccontr THEN' + Object_Logic.atomize_prems_tac THEN' + CONVERSION Drule.beta_eta_conversion; (* ------------------------------------------------------------------------- *) (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *) @@ -429,7 +439,7 @@ (* ------------------------------------------------------------------------- *) fun cnfsat_tac ctxt i = - (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i); + (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i); (* ------------------------------------------------------------------------- *) (* cnfxsat_tac: checks if the empty clause "False" occurs among the *) @@ -439,8 +449,8 @@ (* ------------------------------------------------------------------------- *) fun cnfxsat_tac ctxt i = - (etac FalseE i) ORELSE - (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i); + (etac FalseE i) ORELSE + (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i); (* ------------------------------------------------------------------------- *) (* sat_tac: tactic for calling an external SAT solver, taking as input an *) @@ -449,7 +459,7 @@ (* ------------------------------------------------------------------------- *) fun sat_tac ctxt i = - pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i; + pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i; (* ------------------------------------------------------------------------- *) (* satx_tac: tactic for calling an external SAT solver, taking as input an *) @@ -458,6 +468,6 @@ (* ------------------------------------------------------------------------- *) fun satx_tac ctxt i = - pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i; + pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i; end;