# HG changeset patch
# User paulson
# Date 1116404651 -7200
# Node ID bc916036cf8482d5cc9991583e0e63d0210d1659
# Parent  c71031d7988ce92e513670ee4e942d69a2e15494
new cnf function taking Skolemization theorems as an extra argument

diff -r c71031d7988c -r bc916036cf84 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed May 18 10:23:47 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Wed May 18 10:24:11 2005 +0200
@@ -14,6 +14,7 @@
 signature BASIC_MESON =
 sig
   val size_of_subgoals	: thm -> int
+  val make_cnf		: thm list -> thm -> thm list
   val make_nnf		: thm -> thm
   val skolemize		: thm -> thm
   val make_clauses	: thm list -> thm list
@@ -122,32 +123,43 @@
 		     radixstring(26, "A", !name_ref))
   in  read_instantiate [("x", newname)] sth  end;
 
+(*Used with METAHYPS below. There is one assumption, which gets bound to prem
+  and then normalized via function nf. The normal form is given to resolve_tac,
+  presumably to instantiate a Boolean variable.*)
 fun resop nf [prem] = resolve_tac (nf prem) 1;
 
-(*Conjunctive normal form, detecting tautologies early.
-  Strips universal quantifiers and breaks up conjunctions. *)
-fun cnf_aux seen (th,ths) =
- if taut_lits (literals(prop_of th) @ seen)  
-  then ths     (*tautology ignored*)
-  else if not (has_consts ["All","op &"] (prop_of th))  
-  then th::ths (*no work to do, terminate*)
-  else (*conjunction?*)
-	cnf_aux seen (th RS conjunct1,
-		      cnf_aux seen (th RS conjunct2, ths))
-  handle THM _ => (*universal quant?*)
-	cnf_aux  seen (freeze_spec th,  ths)
-  handle THM _ => (*disjunction?*)
-    let val tac =
-	(METAHYPS (resop (cnf_nil seen)) 1) THEN
-	(fn st' => st' |>
+(*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
+  Detects tautologies early, with "seen" holding the other literals of a clause.
+  Strips universal quantifiers and breaks up conjunctions.
+  Eliminates existential quantifiers using skoths: Skolemization theorems.*)
+fun cnf skoths (th,ths) =
+  let fun cnf_aux seen (th,ths) =
+        if taut_lits (literals(prop_of th) @ seen)  
+	then ths     (*tautology ignored*)
+	else if not (has_consts ["All","Ex","op &"] (prop_of th))  
+	then th::ths (*no work to do, terminate*)
+	else (*conjunction?*)
+	      cnf_aux seen (th RS conjunct1,
+			    cnf_aux seen (th RS conjunct2, ths))
+	handle THM _ => (*universal quantifier?*)
+	      cnf_aux seen (freeze_spec th,  ths)
+	handle THM _ => (*existential quantifier? Insert Skolem functions.*)
+	      cnf_aux seen (tryres (th,skoths), ths)
+	handle THM _ => (*disjunction?*)
+	  let val tac =
+	      (METAHYPS (resop (cnf_nil seen)) 1) THEN
+	     (fn st' => st' |>  
 		METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
-    in  Seq.list_of (tac (th RS disj_forward)) @ ths  end 
-and cnf_nil seen th = (cnf_aux seen (th,[]))
+	  in  Seq.list_of (tac (th RS disj_forward)) @ ths  end 
+      and cnf_nil seen th = (cnf_aux seen (th,[]))
+  in 
+    name_ref := 19;  (*It's safe to reset this in a top-level call to cnf*)
+    (cnf skoths (th RS conjunct1, cnf skoths (th RS conjunct2, ths))
+     handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths))
+  end;
 
-(*Top-level call to cnf -- it's safe to reset name_ref*)
-fun cnf (th,ths) =
-   (name_ref := 19;  cnf (th RS conjunct1, cnf (th RS conjunct2, ths))
-    handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths));
+fun make_cnf skoths th = cnf skoths (th, []);
+
 
 (**** Removal of duplicate literals ****)
 
@@ -332,7 +344,7 @@
 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   The resulting clauses are HOL disjunctions.*)
 fun make_clauses ths =
-    (sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
+    (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
 
 
 (*Convert a list of clauses to (contrapositive) Horn clauses*)