--- 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_<int>" *)
- 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_<int>" *)
+ 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;
--- 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;
--- 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;