src/HOL/Tools/prop_logic.ML
changeset 16907 2187e3f94761
parent 15570 8d8c70b41bab
child 16909 acbc7a9c3864
     1.1 --- a/src/HOL/Tools/prop_logic.ML	Fri Jul 22 17:43:49 2005 +0200
     1.2 +++ b/src/HOL/Tools/prop_logic.ML	Mon Jul 25 15:51:30 2005 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Tools/prop_logic.ML
     1.5      ID:         $Id$
     1.6      Author:     Tjark Weber
     1.7 -    Copyright   2004
     1.8 +    Copyright   2004-2005
     1.9  
    1.10  Formulas of propositional logic.
    1.11  *)
    1.12 @@ -176,96 +176,73 @@
    1.13  (*      'fm' of propositional logic, introducing auxiliary variables if      *)
    1.14  (*      necessary to avoid an exponential blowup of the formula.  The result *)
    1.15  (*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
    1.16 +(*      Auxiliary variables are introduced as switches for OR-nodes, based   *)
    1.17 +(*      on the observation that "fm1 OR (fm21 AND fm22)" is equisatisfiable  *)
    1.18 +(*      with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR aux)".            *)
    1.19  (* ------------------------------------------------------------------------- *)
    1.20  
    1.21  	(* prop_formula -> prop_formula *)
    1.22  
    1.23  	fun defcnf fm =
    1.24  	let
    1.25 -		(* prop_formula * int -> prop_formula * int *)
    1.26 +		(* convert formula to NNF first *)
    1.27 +		val fm' = nnf fm
    1.28  		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
    1.29 +		(* int ref *)
    1.30 +		val new = ref (maxidx fm' + 1)
    1.31 +		(* unit -> int *)
    1.32 +		fun new_idx () = let val idx = !new in new := idx+1; idx end
    1.33 +		(* prop_formula -> prop_formula *)
    1.34  		fun
    1.35  		(* constants *)
    1.36 -		    defcnf_from_nnf (True, new)            = (True, new)
    1.37 -		  | defcnf_from_nnf (False, new)           = (False, new)
    1.38 +		    defcnf_from_nnf True  = True
    1.39 +		  | defcnf_from_nnf False = False
    1.40  		(* literals *)
    1.41 -		  | defcnf_from_nnf (BoolVar i, new)       = (BoolVar i, new)
    1.42 -		  | defcnf_from_nnf (Not fm1, new)         = (Not fm1, new)  (* 'fm1' must be a variable since the formula is in NNF *)
    1.43 +		  | defcnf_from_nnf (BoolVar i) = BoolVar i
    1.44 +		  | defcnf_from_nnf (Not fm1)   = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
    1.45  		(* pushing 'or' inside of 'and' using auxiliary variables *)
    1.46 -		  | defcnf_from_nnf (Or (fm1, fm2), new)   =
    1.47 +		  | defcnf_from_nnf (Or (fm1, fm2)) =
    1.48  			let
    1.49 -				val (fm1', new')  = defcnf_from_nnf (fm1, new)
    1.50 -				val (fm2', new'') = defcnf_from_nnf (fm2, new')
    1.51 -				(* prop_formula * prop_formula -> int -> prop_formula * int *)
    1.52 -				fun defcnf_or (And (fm11, fm12), fm2) new =
    1.53 +				val fm1' = defcnf_from_nnf fm1
    1.54 +				val fm2' = defcnf_from_nnf fm2
    1.55 +				(* prop_formula * prop_formula -> prop_formula *)
    1.56 +				fun defcnf_or (And (fm11, fm12), fm2) =
    1.57  					(case fm2 of
    1.58  					(* do not introduce an auxiliary variable for literals *)
    1.59  					  BoolVar _ =>
    1.60 -						let
    1.61 -							val (fm_a, new')  = defcnf_or (fm11, fm2) new
    1.62 -							val (fm_b, new'') = defcnf_or (fm12, fm2) new'
    1.63 -						in
    1.64 -							(And (fm_a, fm_b), new'')
    1.65 -						end
    1.66 +							And (defcnf_or (fm11, fm2), defcnf_or (fm12, fm2))
    1.67  					| Not _ =>
    1.68 -						let
    1.69 -							val (fm_a, new')  = defcnf_or (fm11, fm2) new
    1.70 -							val (fm_b, new'') = defcnf_or (fm12, fm2) new'
    1.71 -						in
    1.72 -							(And (fm_a, fm_b), new'')
    1.73 -						end
    1.74 +							And (defcnf_or (fm11, fm2), defcnf_or (fm12, fm2))
    1.75  					| _ =>
    1.76  						let
    1.77 -							val aux            = BoolVar new
    1.78 -							val (fm_a, new')   = defcnf_or (fm11, aux)     (new+1)
    1.79 -							val (fm_b, new'')  = defcnf_or (fm12, aux)     new'
    1.80 -							val (fm_c, new''') = defcnf_or (fm2,  Not aux) new''
    1.81 +							val aux = BoolVar (new_idx ())
    1.82  						in
    1.83 -							(And (And (fm_a, fm_b), fm_c), new''')
    1.84 +							And (And (defcnf_or (fm11, aux), defcnf_or (fm12, aux)), defcnf_or (fm2, Not aux))
    1.85  						end)
    1.86 -				  | defcnf_or (fm1, And (fm21, fm22)) new =
    1.87 +				  | defcnf_or (fm1, And (fm21, fm22)) =
    1.88  					(case fm1 of
    1.89  					(* do not introduce an auxiliary variable for literals *)
    1.90  					  BoolVar _ =>
    1.91 -						let
    1.92 -							val (fm_a, new')  = defcnf_or (fm1, fm21) new
    1.93 -							val (fm_b, new'') = defcnf_or (fm1, fm22) new'
    1.94 -						in
    1.95 -							(And (fm_a, fm_b), new'')
    1.96 -						end
    1.97 +							And (defcnf_or (fm1, fm21), defcnf_or (fm1, fm22))
    1.98  					| Not _ =>
    1.99 -						let
   1.100 -							val (fm_a, new')  = defcnf_or (fm1, fm21) new
   1.101 -							val (fm_b, new'') = defcnf_or (fm1, fm22) new'
   1.102 -						in
   1.103 -							(And (fm_a, fm_b), new'')
   1.104 -						end
   1.105 +							And (defcnf_or (fm1, fm21), defcnf_or (fm1, fm22))
   1.106  					| _ =>
   1.107  						let
   1.108 -							val aux            = BoolVar new
   1.109 -							val (fm_a, new')   = defcnf_or (fm1,  Not aux) (new+1)
   1.110 -							val (fm_b, new'')  = defcnf_or (fm21, aux)     new'
   1.111 -							val (fm_c, new''') = defcnf_or (fm22, aux)     new''
   1.112 +							val aux = BoolVar (new_idx ())
   1.113  						in
   1.114 -							(And (fm_a, And (fm_b, fm_c)), new''')
   1.115 +							And (defcnf_or (fm1, Not aux), And (defcnf_or (fm21, aux), defcnf_or (fm22, aux)))
   1.116  						end)
   1.117  				(* neither subformula contains 'and' *)
   1.118 -				  | defcnf_or (fm1, fm2) new =
   1.119 -					(Or (fm1, fm2), new)
   1.120 +				  | defcnf_or (fm1, fm2) =
   1.121 +					Or (fm1, fm2)
   1.122  			in
   1.123 -				defcnf_or (fm1', fm2') new''
   1.124 +				defcnf_or (fm1', fm2')
   1.125  			end
   1.126  		(* 'and' as outermost connective is left untouched *)
   1.127 -		  | defcnf_from_nnf (And (fm1, fm2), new)   =
   1.128 -			let
   1.129 -				val (fm1', new')  = defcnf_from_nnf (fm1, new)
   1.130 -				val (fm2', new'') = defcnf_from_nnf (fm2, new')
   1.131 -			in
   1.132 -				(And (fm1', fm2'), new'')
   1.133 -			end
   1.134 -		val fm' = nnf fm
   1.135 +		  | defcnf_from_nnf (And (fm1, fm2)) =
   1.136 +				And (defcnf_from_nnf fm1, defcnf_from_nnf fm2)
   1.137  	in
   1.138 -		(fst o defcnf_from_nnf) (fm', (maxidx fm')+1)
   1.139 +		defcnf_from_nnf fm'
   1.140  	end;
   1.141  
   1.142  (* ------------------------------------------------------------------------- *)