# HG changeset patch
# User webertj
# Date 1087502331 -7200
# Node ID 2c1456d705e9812d462eac5f10921a79f1afa1a1
# Parent  d584e32f7d460bc64ce48e93264c952ff7afa6a6
improved defcnf conversion

diff -r d584e32f7d46 -r 2c1456d705e9 src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Thu Jun 17 17:18:30 2004 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Thu Jun 17 21:58:51 2004 +0200
@@ -206,23 +206,57 @@
 				val (fm2', new'') = defcnf_from_nnf (fm2, new')
 				(* prop_formula * prop_formula -> int -> prop_formula * int *)
 				fun defcnf_or (And (fm11, fm12), fm2) new =
-					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''
-					in
-						(And (And (fm_a, fm_b), fm_c), new''')
-					end
+					(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
+					| 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
+					| _ =>
+						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''
+						in
+							(And (And (fm_a, fm_b), fm_c), new''')
+						end)
 				  | defcnf_or (fm1, And (fm21, fm22)) new =
-					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''
-					in
-						(And (fm_a, And (fm_b, fm_c)), new''')
-					end
+					(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
+					| 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
+					| _ =>
+						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''
+						in
+							(And (fm_a, And (fm_b, fm_c)), new''')
+						end)
 				(* neither subformula contains 'and' *)
 				  | defcnf_or (fm1, fm2) new =
 					(Or (fm1, fm2), new)
@@ -237,7 +271,7 @@
 			in
 				(And (fm1', fm2'), new'')
 			end
-		val fm'    = nnf fm
+		val fm' = nnf fm
 	in
 		(fst o defcnf_from_nnf) (fm', (maxidx fm')+1)
 	end;