improved defcnf conversion
authorwebertj
Thu Jun 17 21:58:51 2004 +0200 (2004-06-17)
changeset 149642c1456d705e9
parent 14963 d584e32f7d46
child 14965 7155b319eafa
improved defcnf conversion
src/HOL/Tools/prop_logic.ML
     1.1 --- a/src/HOL/Tools/prop_logic.ML	Thu Jun 17 17:18:30 2004 +0200
     1.2 +++ b/src/HOL/Tools/prop_logic.ML	Thu Jun 17 21:58:51 2004 +0200
     1.3 @@ -206,23 +206,57 @@
     1.4  				val (fm2', new'') = defcnf_from_nnf (fm2, new')
     1.5  				(* prop_formula * prop_formula -> int -> prop_formula * int *)
     1.6  				fun defcnf_or (And (fm11, fm12), fm2) new =
     1.7 -					let
     1.8 -						val aux            = BoolVar new
     1.9 -						val (fm_a, new')   = defcnf_or (fm11, aux)     (new+1)
    1.10 -						val (fm_b, new'')  = defcnf_or (fm12, aux)     new'
    1.11 -						val (fm_c, new''') = defcnf_or (fm2,  Not aux) new''
    1.12 -					in
    1.13 -						(And (And (fm_a, fm_b), fm_c), new''')
    1.14 -					end
    1.15 +					(case fm2 of
    1.16 +					(* do not introduce an auxiliary variable for literals *)
    1.17 +					  BoolVar _ =>
    1.18 +						let
    1.19 +							val (fm_a, new')  = defcnf_or (fm11, fm2) new
    1.20 +							val (fm_b, new'') = defcnf_or (fm12, fm2) new'
    1.21 +						in
    1.22 +							(And (fm_a, fm_b), new'')
    1.23 +						end
    1.24 +					| Not _ =>
    1.25 +						let
    1.26 +							val (fm_a, new')  = defcnf_or (fm11, fm2) new
    1.27 +							val (fm_b, new'') = defcnf_or (fm12, fm2) new'
    1.28 +						in
    1.29 +							(And (fm_a, fm_b), new'')
    1.30 +						end
    1.31 +					| _ =>
    1.32 +						let
    1.33 +							val aux            = BoolVar new
    1.34 +							val (fm_a, new')   = defcnf_or (fm11, aux)     (new+1)
    1.35 +							val (fm_b, new'')  = defcnf_or (fm12, aux)     new'
    1.36 +							val (fm_c, new''') = defcnf_or (fm2,  Not aux) new''
    1.37 +						in
    1.38 +							(And (And (fm_a, fm_b), fm_c), new''')
    1.39 +						end)
    1.40  				  | defcnf_or (fm1, And (fm21, fm22)) new =
    1.41 -					let
    1.42 -						val aux            = BoolVar new
    1.43 -						val (fm_a, new')   = defcnf_or (fm1,  Not aux) (new+1)
    1.44 -						val (fm_b, new'')  = defcnf_or (fm21, aux)     new'
    1.45 -						val (fm_c, new''') = defcnf_or (fm22, aux)     new''
    1.46 -					in
    1.47 -						(And (fm_a, And (fm_b, fm_c)), new''')
    1.48 -					end
    1.49 +					(case fm1 of
    1.50 +					(* do not introduce an auxiliary variable for literals *)
    1.51 +					  BoolVar _ =>
    1.52 +						let
    1.53 +							val (fm_a, new')  = defcnf_or (fm1, fm21) new
    1.54 +							val (fm_b, new'') = defcnf_or (fm1, fm22) new'
    1.55 +						in
    1.56 +							(And (fm_a, fm_b), new'')
    1.57 +						end
    1.58 +					| Not _ =>
    1.59 +						let
    1.60 +							val (fm_a, new')  = defcnf_or (fm1, fm21) new
    1.61 +							val (fm_b, new'') = defcnf_or (fm1, fm22) new'
    1.62 +						in
    1.63 +							(And (fm_a, fm_b), new'')
    1.64 +						end
    1.65 +					| _ =>
    1.66 +						let
    1.67 +							val aux            = BoolVar new
    1.68 +							val (fm_a, new')   = defcnf_or (fm1,  Not aux) (new+1)
    1.69 +							val (fm_b, new'')  = defcnf_or (fm21, aux)     new'
    1.70 +							val (fm_c, new''') = defcnf_or (fm22, aux)     new''
    1.71 +						in
    1.72 +							(And (fm_a, And (fm_b, fm_c)), new''')
    1.73 +						end)
    1.74  				(* neither subformula contains 'and' *)
    1.75  				  | defcnf_or (fm1, fm2) new =
    1.76  					(Or (fm1, fm2), new)
    1.77 @@ -237,7 +271,7 @@
    1.78  			in
    1.79  				(And (fm1', fm2'), new'')
    1.80  			end
    1.81 -		val fm'    = nnf fm
    1.82 +		val fm' = nnf fm
    1.83  	in
    1.84  		(fst o defcnf_from_nnf) (fm', (maxidx fm')+1)
    1.85  	end;