# HG changeset patch
# User webertj
# Date 1122299490 -7200
# Node ID 2187e3f947614071d4211dbadf35bbf5009dd7d6
# Parent  74eddde1de2ff2eac83c7c65a4a43360bc5a25d9
defcnf modified to internally use a reference

diff -r 74eddde1de2f -r 2187e3f94761 src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Fri Jul 22 17:43:49 2005 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Mon Jul 25 15:51:30 2005 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/prop_logic.ML
     ID:         $Id$
     Author:     Tjark Weber
-    Copyright   2004
+    Copyright   2004-2005
 
 Formulas of propositional logic.
 *)
@@ -176,96 +176,73 @@
 (*      'fm' of propositional logic, introducing auxiliary variables if      *)
 (*      necessary to avoid an exponential blowup of the formula.  The result *)
 (*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
+(*      Auxiliary variables are introduced as switches for OR-nodes, based   *)
+(*      on the observation that "fm1 OR (fm21 AND fm22)" is equisatisfiable  *)
+(*      with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR aux)".            *)
 (* ------------------------------------------------------------------------- *)
 
 	(* prop_formula -> prop_formula *)
 
 	fun defcnf fm =
 	let
-		(* prop_formula * int -> prop_formula * int *)
+		(* convert formula to NNF first *)
+		val fm' = nnf fm
 		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
+		(* int ref *)
+		val new = ref (maxidx fm' + 1)
+		(* unit -> int *)
+		fun new_idx () = let val idx = !new in new := idx+1; idx end
+		(* prop_formula -> prop_formula *)
 		fun
 		(* constants *)
-		    defcnf_from_nnf (True, new)            = (True, new)
-		  | defcnf_from_nnf (False, new)           = (False, new)
+		    defcnf_from_nnf True  = True
+		  | defcnf_from_nnf False = False
 		(* literals *)
-		  | defcnf_from_nnf (BoolVar i, new)       = (BoolVar i, new)
-		  | defcnf_from_nnf (Not fm1, new)         = (Not fm1, new)  (* 'fm1' must be a variable since the formula is in NNF *)
+		  | defcnf_from_nnf (BoolVar i) = BoolVar i
+		  | defcnf_from_nnf (Not fm1)   = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
 		(* pushing 'or' inside of 'and' using auxiliary variables *)
-		  | defcnf_from_nnf (Or (fm1, fm2), new)   =
+		  | defcnf_from_nnf (Or (fm1, fm2)) =
 			let
-				val (fm1', new')  = defcnf_from_nnf (fm1, new)
-				val (fm2', new'') = defcnf_from_nnf (fm2, new')
-				(* prop_formula * prop_formula -> int -> prop_formula * int *)
-				fun defcnf_or (And (fm11, fm12), fm2) new =
+				val fm1' = defcnf_from_nnf fm1
+				val fm2' = defcnf_from_nnf fm2
+				(* prop_formula * prop_formula -> prop_formula *)
+				fun defcnf_or (And (fm11, fm12), fm2) =
 					(case fm2 of
 					(* do not introduce an auxiliary variable for literals *)
 					  BoolVar _ =>
-						let
-							val (fm_a, new')  = defcnf_or (fm11, fm2) new
-							val (fm_b, new'') = defcnf_or (fm12, fm2) new'
-						in
-							(And (fm_a, fm_b), new'')
-						end
+							And (defcnf_or (fm11, fm2), defcnf_or (fm12, fm2))
 					| Not _ =>
-						let
-							val (fm_a, new')  = defcnf_or (fm11, fm2) new
-							val (fm_b, new'') = defcnf_or (fm12, fm2) new'
-						in
-							(And (fm_a, fm_b), new'')
-						end
+							And (defcnf_or (fm11, fm2), defcnf_or (fm12, fm2))
 					| _ =>
 						let
-							val aux            = BoolVar new
-							val (fm_a, new')   = defcnf_or (fm11, aux)     (new+1)
-							val (fm_b, new'')  = defcnf_or (fm12, aux)     new'
-							val (fm_c, new''') = defcnf_or (fm2,  Not aux) new''
+							val aux = BoolVar (new_idx ())
 						in
-							(And (And (fm_a, fm_b), fm_c), new''')
+							And (And (defcnf_or (fm11, aux), defcnf_or (fm12, aux)), defcnf_or (fm2, Not aux))
 						end)
-				  | defcnf_or (fm1, And (fm21, fm22)) new =
+				  | defcnf_or (fm1, And (fm21, fm22)) =
 					(case fm1 of
 					(* do not introduce an auxiliary variable for literals *)
 					  BoolVar _ =>
-						let
-							val (fm_a, new')  = defcnf_or (fm1, fm21) new
-							val (fm_b, new'') = defcnf_or (fm1, fm22) new'
-						in
-							(And (fm_a, fm_b), new'')
-						end
+							And (defcnf_or (fm1, fm21), defcnf_or (fm1, fm22))
 					| Not _ =>
-						let
-							val (fm_a, new')  = defcnf_or (fm1, fm21) new
-							val (fm_b, new'') = defcnf_or (fm1, fm22) new'
-						in
-							(And (fm_a, fm_b), new'')
-						end
+							And (defcnf_or (fm1, fm21), defcnf_or (fm1, fm22))
 					| _ =>
 						let
-							val aux            = BoolVar new
-							val (fm_a, new')   = defcnf_or (fm1,  Not aux) (new+1)
-							val (fm_b, new'')  = defcnf_or (fm21, aux)     new'
-							val (fm_c, new''') = defcnf_or (fm22, aux)     new''
+							val aux = BoolVar (new_idx ())
 						in
-							(And (fm_a, And (fm_b, fm_c)), new''')
+							And (defcnf_or (fm1, Not aux), And (defcnf_or (fm21, aux), defcnf_or (fm22, aux)))
 						end)
 				(* neither subformula contains 'and' *)
-				  | defcnf_or (fm1, fm2) new =
-					(Or (fm1, fm2), new)
+				  | defcnf_or (fm1, fm2) =
+					Or (fm1, fm2)
 			in
-				defcnf_or (fm1', fm2') new''
+				defcnf_or (fm1', fm2')
 			end
 		(* 'and' as outermost connective is left untouched *)
-		  | defcnf_from_nnf (And (fm1, fm2), new)   =
-			let
-				val (fm1', new')  = defcnf_from_nnf (fm1, new)
-				val (fm2', new'') = defcnf_from_nnf (fm2, new')
-			in
-				(And (fm1', fm2'), new'')
-			end
-		val fm' = nnf fm
+		  | defcnf_from_nnf (And (fm1, fm2)) =
+				And (defcnf_from_nnf fm1, defcnf_from_nnf fm2)
 	in
-		(fst o defcnf_from_nnf) (fm', (maxidx fm')+1)
+		defcnf_from_nnf fm'
 	end;
 
 (* ------------------------------------------------------------------------- *)