src/HOL/Tools/refute.ML
changeset 14350 41b32020d0b3
child 14351 cd3ef10d02be
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/refute.ML	Sat Jan 10 13:35:10 2004 +0100
     1.3 @@ -0,0 +1,1648 @@
     1.4 +(*  Title:      HOL/Tools/refute.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tjark Weber
     1.7 +    Copyright   2003-2004
     1.8 +
     1.9 +Finite model generation for HOL formulae, using an external SAT solver.
    1.10 +*)
    1.11 +
    1.12 +(* ------------------------------------------------------------------------- *)
    1.13 +(* Declares the 'REFUTE' signature as well as a structure 'Refute'.  See     *)
    1.14 +(* 'find_model' below for a description of the implemented algorithm, and    *)
    1.15 +(* the Isabelle/Isar theories 'HOL/Refute.thy' and 'HOL/Main.thy' on how to  *)
    1.16 +(* set things up.                                                            *)
    1.17 +(* ------------------------------------------------------------------------- *)
    1.18 +
    1.19 +signature REFUTE =
    1.20 +sig
    1.21 +
    1.22 +	(* We use 'REFUTE' only for internal error conditions that should    *)
    1.23 +	(* never occur in the first place (i.e. errors caused by bugs in our *)
    1.24 +	(* code).  Otherwise (e.g. to indicate invalid input data) we use    *)
    1.25 +	(* 'error'.                                                          *)
    1.26 +
    1.27 +	exception REFUTE of string * string;	(* ("in function", "cause") *)
    1.28 +
    1.29 +	val setup : (theory -> theory) list
    1.30 +
    1.31 +	val set_default_param : (string * string) -> theory -> theory
    1.32 +	val get_default_param : theory -> string -> string option
    1.33 +	val get_default_params : theory -> (string * string) list
    1.34 +
    1.35 +	val find_model : theory -> (string * string) list -> Term.term -> unit
    1.36 +
    1.37 +	val refute_term : theory -> (string * string) list -> Term.term -> unit
    1.38 +	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
    1.39 +end;
    1.40 +
    1.41 +
    1.42 +structure Refute : REFUTE =
    1.43 +struct
    1.44 +	exception REFUTE of string * string;
    1.45 +
    1.46 +	exception EMPTY_DATATYPE;
    1.47 +
    1.48 +	structure RefuteDataArgs =
    1.49 +	struct
    1.50 +		val name = "Refute/refute";
    1.51 +		type T = string Symtab.table;
    1.52 +		val empty = Symtab.empty;
    1.53 +		val copy = I;
    1.54 +		val prep_ext = I;
    1.55 +		val merge =
    1.56 +			fn (symTable1, symTable2) =>
    1.57 +				(Symtab.merge (op =) (symTable1, symTable2));
    1.58 +		fun print sg symTable =
    1.59 +			writeln
    1.60 +				("'refute', default parameters:\n" ^
    1.61 +				(space_implode "\n" (map (fn (name,value) => name ^ " = " ^ value) (Symtab.dest symTable))))
    1.62 +	end;
    1.63 +
    1.64 +	structure RefuteData = TheoryDataFun(RefuteDataArgs);
    1.65 +
    1.66 +
    1.67 +(* ------------------------------------------------------------------------- *)
    1.68 +(* INTERFACE, PART 1: INITIALIZATION, PARAMETER MANAGEMENT                   *)
    1.69 +(* ------------------------------------------------------------------------- *)
    1.70 +
    1.71 +(* ------------------------------------------------------------------------- *)
    1.72 +(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
    1.73 +(* structure                                                                 *)
    1.74 +(* ------------------------------------------------------------------------- *)
    1.75 +
    1.76 +	val setup = [RefuteData.init];
    1.77 +
    1.78 +(* ------------------------------------------------------------------------- *)
    1.79 +(* set_default_param: stores the '(name, value)' pair in RefuteData's symbol *)
    1.80 +(*                    table                                                  *)
    1.81 +(* ------------------------------------------------------------------------- *)
    1.82 +
    1.83 +	fun set_default_param (name, value) thy =
    1.84 +	let
    1.85 +		val symTable = RefuteData.get thy
    1.86 +	in
    1.87 +		case Symtab.lookup (symTable, name) of
    1.88 +			None   => RefuteData.put (Symtab.extend (symTable, [(name, value)])) thy
    1.89 +		|	Some _ => RefuteData.put (Symtab.update ((name, value), symTable)) thy
    1.90 +	end;
    1.91 +
    1.92 +(* ------------------------------------------------------------------------- *)
    1.93 +(* get_default_param: retrieves the value associated with 'name' from        *)
    1.94 +(*                    RefuteData's symbol table                              *)
    1.95 +(* ------------------------------------------------------------------------- *)
    1.96 +
    1.97 +	fun get_default_param thy name = Symtab.lookup (RefuteData.get thy, name);
    1.98 +
    1.99 +(* ------------------------------------------------------------------------- *)
   1.100 +(* get_default_params: returns a list of all '(name, value)' pairs that are  *)
   1.101 +(*                     stored in RefuteData's symbol table                   *)
   1.102 +(* ------------------------------------------------------------------------- *)
   1.103 +
   1.104 +	fun get_default_params thy = Symtab.dest (RefuteData.get thy);
   1.105 +
   1.106 +
   1.107 +(* ------------------------------------------------------------------------- *)
   1.108 +(* PROPOSITIONAL FORMULAS                                                    *)
   1.109 +(* ------------------------------------------------------------------------- *)
   1.110 +
   1.111 +(* ------------------------------------------------------------------------- *)
   1.112 +(* prop_formula: formulas of propositional logic, built from boolean         *)
   1.113 +(*               variables (referred to by index) and True/False using       *)
   1.114 +(*               not/or/and                                                  *)
   1.115 +(* ------------------------------------------------------------------------- *)
   1.116 +
   1.117 +	datatype prop_formula =
   1.118 +		  True
   1.119 +		| False
   1.120 +		| BoolVar of int
   1.121 +		| Not of prop_formula
   1.122 +		| Or of prop_formula * prop_formula
   1.123 +		| And of prop_formula * prop_formula;
   1.124 +
   1.125 +	(* the following constructor functions make sure that True and False do *)
   1.126 +	(* not occur within any of the other connectives (i.e. Not, Or, And)    *)
   1.127 +
   1.128 +	(* prop_formula -> prop_formula *)
   1.129 +
   1.130 +	fun SNot True  = False
   1.131 +	  | SNot False = True
   1.132 +	  | SNot fm    = Not fm;
   1.133 +
   1.134 +	(* prop_formula * prop_formula -> prop_formula *)
   1.135 +
   1.136 +	fun SOr (True, _)   = True
   1.137 +	  | SOr (_, True)   = True
   1.138 +	  | SOr (False, fm) = fm
   1.139 +	  | SOr (fm, False) = fm
   1.140 +	  | SOr (fm1, fm2)  = Or (fm1, fm2);
   1.141 +
   1.142 +	(* prop_formula * prop_formula -> prop_formula *)
   1.143 +
   1.144 +	fun SAnd (True, fm) = fm
   1.145 +	  | SAnd (fm, True) = fm
   1.146 +	  | SAnd (False, _) = False
   1.147 +	  | SAnd (_, False) = False
   1.148 +	  | SAnd (fm1, fm2) = And (fm1, fm2);
   1.149 +
   1.150 +(* ------------------------------------------------------------------------- *)
   1.151 +(* list_disjunction: computes the disjunction of a list of propositional     *)
   1.152 +(*                   formulas                                                *)
   1.153 +(* ------------------------------------------------------------------------- *)
   1.154 +
   1.155 +	(* prop_formula list -> prop_formula *)
   1.156 +
   1.157 +	fun list_disjunction []      = False
   1.158 +	  | list_disjunction (x::xs) = SOr (x, list_disjunction xs);
   1.159 +
   1.160 +(* ------------------------------------------------------------------------- *)
   1.161 +(* list_conjunction: computes the conjunction of a list of propositional     *)
   1.162 +(*                   formulas                                                *)
   1.163 +(* ------------------------------------------------------------------------- *)
   1.164 +
   1.165 +	(* prop_formula list -> prop_formula *)
   1.166 +
   1.167 +	fun list_conjunction []      = True
   1.168 +	  | list_conjunction (x::xs) = SAnd (x, list_conjunction xs);
   1.169 +
   1.170 +(* ------------------------------------------------------------------------- *)
   1.171 +(* prop_formula_dot_product: [x1,...,xn] * [y1,...,yn] -> x1*y1+...+xn*yn    *)
   1.172 +(* ------------------------------------------------------------------------- *)
   1.173 +
   1.174 +	(* prop_formula list * prop_formula list -> prop_formula *)
   1.175 +
   1.176 +	fun prop_formula_dot_product ([],[])       = False
   1.177 +	  | prop_formula_dot_product (x::xs,y::ys) = SOr (SAnd (x,y), prop_formula_dot_product (xs,ys))
   1.178 +	  | prop_formula_dot_product (_,_)         = raise REFUTE ("prop_formula_dot_product", "lists are of different length");
   1.179 +
   1.180 +(* ------------------------------------------------------------------------- *)
   1.181 +(* prop_formula_to_nnf: computes the negation normal form of a formula 'fm'  *)
   1.182 +(*                      of propositional logic (i.e. only variables may be   *)
   1.183 +(*                      negated, but not subformulas)                        *)
   1.184 +(* ------------------------------------------------------------------------- *)
   1.185 +
   1.186 +	(* prop_formula -> prop_formula *)
   1.187 +
   1.188 +	fun prop_formula_to_nnf fm =
   1.189 +		case fm of
   1.190 +		(* constants *)
   1.191 +		  True                => True
   1.192 +		| False               => False
   1.193 +		(* literals *)
   1.194 +		| BoolVar i           => BoolVar i
   1.195 +		| Not (BoolVar i)     => Not (BoolVar i)
   1.196 +		(* double-negation elimination *)
   1.197 +		| Not (Not fm)        => prop_formula_to_nnf fm
   1.198 +		(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
   1.199 +		| Not (Or  (fm1,fm2)) => SAnd (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
   1.200 +		| Not (And (fm1,fm2)) => SOr  (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
   1.201 +		(* 'or' and 'and' as outermost connectives are left untouched *)
   1.202 +		| Or  (fm1,fm2)       => SOr  (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
   1.203 +		| And (fm1,fm2)       => SAnd (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
   1.204 +		(* 'not' + constant *)
   1.205 +		| Not _               => raise REFUTE ("prop_formula_to_nnf", "'True'/'False' not allowed inside of 'Not'");
   1.206 +
   1.207 +(* ------------------------------------------------------------------------- *)
   1.208 +(* prop_formula_nnf_to_cnf: computes the conjunctive normal form of a        *)
   1.209 +(*      formula 'fm' of propositional logic that is given in negation normal *)
   1.210 +(*      form.  Note that there may occur an exponential blowup of the        *)
   1.211 +(*      formula.                                                             *)
   1.212 +(* ------------------------------------------------------------------------- *)
   1.213 +
   1.214 +	(* prop_formula -> prop_formula *)
   1.215 +
   1.216 +	fun prop_formula_nnf_to_cnf fm =
   1.217 +		case fm of
   1.218 +		(* constants *)
   1.219 +		  True            => True
   1.220 +		| False           => False
   1.221 +		(* literals *)
   1.222 +		| BoolVar i       => BoolVar i
   1.223 +		| Not (BoolVar i) => Not (BoolVar i)
   1.224 +		(* pushing 'or' inside of 'and' using distributive laws *)
   1.225 +		| Or (fm1,fm2)    =>
   1.226 +			let
   1.227 +				val fm1' = prop_formula_nnf_to_cnf fm1
   1.228 +				val fm2' = prop_formula_nnf_to_cnf fm2
   1.229 +			in
   1.230 +				case fm1' of
   1.231 +				  And (fm11,fm12) => prop_formula_nnf_to_cnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
   1.232 +				| _               =>
   1.233 +					(case fm2' of
   1.234 +					  And (fm21,fm22) => prop_formula_nnf_to_cnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
   1.235 +					(* neither subformula contains 'and' *)
   1.236 +					| _               => fm)
   1.237 +			end
   1.238 +		(* 'and' as outermost connective is left untouched *)
   1.239 +		| And (fm1,fm2)   => SAnd (prop_formula_nnf_to_cnf fm1, prop_formula_nnf_to_cnf fm2)
   1.240 +		(* error *)
   1.241 +		| _               => raise REFUTE ("prop_formula_nnf_to_cnf", "formula is not in negation normal form");
   1.242 +
   1.243 +(* ------------------------------------------------------------------------- *)
   1.244 +(* max: computes the maximum of two integer values 'i' and 'j'               *)
   1.245 +(* ------------------------------------------------------------------------- *)
   1.246 +
   1.247 +	(* int * int -> int *)
   1.248 +
   1.249 +	fun max (i,j) =
   1.250 +		if (i>j) then i else j;
   1.251 +
   1.252 +(* ------------------------------------------------------------------------- *)
   1.253 +(* max_var_index: computes the maximal variable index occuring in 'fm',      *)
   1.254 +(*      where 'fm' is a formula of propositional logic                       *)
   1.255 +(* ------------------------------------------------------------------------- *)
   1.256 +
   1.257 +	(* prop_formula -> int *)
   1.258 +
   1.259 +	fun max_var_index fm =
   1.260 +		case fm of
   1.261 +		  True          => 0
   1.262 +		| False         => 0
   1.263 +		| BoolVar i     => i
   1.264 +		| Not fm1       => max_var_index fm1
   1.265 +		| And (fm1,fm2) => max (max_var_index fm1, max_var_index fm2)
   1.266 +		| Or (fm1,fm2)  => max (max_var_index fm1, max_var_index fm2);
   1.267 +
   1.268 +(* ------------------------------------------------------------------------- *)
   1.269 +(* prop_formula_nnf_to_def_cnf: computes the definitional conjunctive normal *)
   1.270 +(*      form of a formula 'fm' of propositional logic that is given in       *)
   1.271 +(*      negation normal form.  To avoid an exponential blowup of the         *)
   1.272 +(*      formula, auxiliary variables may be introduced.  The result formula  *)
   1.273 +(*      is SAT-equivalent to 'fm' (i.e. it is satisfiable if and only if     *)
   1.274 +(*      'fm' is satisfiable).                                                *)
   1.275 +(* ------------------------------------------------------------------------- *)
   1.276 +
   1.277 +	(* prop_formula -> prop_formula *)
   1.278 +
   1.279 +	fun prop_formula_nnf_to_def_cnf fm =
   1.280 +	let
   1.281 +		(* prop_formula * int -> prop_formula * int *)
   1.282 +		fun prop_formula_nnf_to_def_cnf_new (fm,new) =
   1.283 +		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   1.284 +			case fm of
   1.285 +			(* constants *)
   1.286 +			  True            => (True, new)
   1.287 +			| False           => (False, new)
   1.288 +			(* literals *)
   1.289 +			| BoolVar i       => (BoolVar i, new)
   1.290 +			| Not (BoolVar i) => (Not (BoolVar i), new)
   1.291 +			(* pushing 'or' inside of 'and' using distributive laws *)
   1.292 +			| Or (fm1,fm2)    =>
   1.293 +				let
   1.294 +					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
   1.295 +					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
   1.296 +				in
   1.297 +					case fst fm1' of
   1.298 +					  And (fm11,fm12) =>
   1.299 +						let
   1.300 +							val aux = BoolVar (snd fm2')
   1.301 +						in
   1.302 +							(* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
   1.303 +							prop_formula_nnf_to_def_cnf_new (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fst fm2', Not aux)), (snd fm2')+1)
   1.304 +						end
   1.305 +					| _               =>
   1.306 +						(case fst fm2' of
   1.307 +						  And (fm21,fm22) =>
   1.308 +							let
   1.309 +								val aux = BoolVar (snd fm2')
   1.310 +							in
   1.311 +								(* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
   1.312 +								prop_formula_nnf_to_def_cnf_new (SAnd (SOr (fst fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), (snd fm2')+1)
   1.313 +							end
   1.314 +						(* neither subformula contains 'and' *)
   1.315 +						| _               => (fm, new))
   1.316 +				end
   1.317 +			(* 'and' as outermost connective is left untouched *)
   1.318 +			| And (fm1,fm2)   =>
   1.319 +				let
   1.320 +					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
   1.321 +					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
   1.322 +				in
   1.323 +					(SAnd (fst fm1', fst fm2'), snd fm2')
   1.324 +				end
   1.325 +			(* error *)
   1.326 +			| _               => raise REFUTE ("prop_formula_nnf_to_def_cnf", "formula is not in negation normal form")
   1.327 +	in
   1.328 +		fst (prop_formula_nnf_to_def_cnf_new (fm, (max_var_index fm)+1))
   1.329 +	end;
   1.330 +
   1.331 +(* ------------------------------------------------------------------------- *)
   1.332 +(* prop_formula_to_cnf: computes the conjunctive normal form of a formula    *)
   1.333 +(*                      'fm' of propositional logic                          *)
   1.334 +(* ------------------------------------------------------------------------- *)
   1.335 +
   1.336 +	(* prop_formula -> prop_formula *)
   1.337 +
   1.338 +	fun prop_formula_to_cnf fm =
   1.339 +		prop_formula_nnf_to_cnf (prop_formula_to_nnf fm);
   1.340 +
   1.341 +(* ------------------------------------------------------------------------- *)
   1.342 +(* prop_formula_to_def_cnf: computes the definitional conjunctive normal     *)
   1.343 +(*      form of a formula 'fm' of propositional logic, introducing auxiliary *)
   1.344 +(*      variables if necessary to avoid an exponential blowup of the formula *)
   1.345 +(* ------------------------------------------------------------------------- *)
   1.346 +
   1.347 +	(* prop_formula -> prop_formula *)
   1.348 +
   1.349 +	fun prop_formula_to_def_cnf fm =
   1.350 +		prop_formula_nnf_to_def_cnf (prop_formula_to_nnf fm);
   1.351 +
   1.352 +(* ------------------------------------------------------------------------- *)
   1.353 +(* prop_formula_to_dimacs_cnf_format: serializes a formula of propositional  *)
   1.354 +(*      logic to a file in DIMACS CNF format (see "Satisfiability Suggested  *)
   1.355 +(*      Format", May 8 1993, Section 2.1)                                    *)
   1.356 +(* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
   1.357 +(*       index less than 1.                                                  *)
   1.358 +(* def : If true, translate 'fm' into definitional CNF.  Otherwise translate *)
   1.359 +(*       'fm' into CNF.                                                      *)
   1.360 +(* path: path of the file to be created                                      *)
   1.361 +(* ------------------------------------------------------------------------- *)
   1.362 +
   1.363 +	(* prop_formula -> bool -> Path.T -> unit *)
   1.364 +
   1.365 +	fun prop_formula_to_dimacs_cnf_format fm def path =
   1.366 +	let
   1.367 +		(* prop_formula *)
   1.368 +		val cnf =
   1.369 +			if def then
   1.370 +				prop_formula_to_def_cnf fm
   1.371 +			else
   1.372 +				prop_formula_to_cnf fm
   1.373 +		val fm' =
   1.374 +			case cnf of
   1.375 +			  True  => Or (BoolVar 1, Not (BoolVar 1))
   1.376 +			| False => And (BoolVar 1, Not (BoolVar 1))
   1.377 +			| _     => cnf (* either 'cnf'=True/False, or 'cnf' does not contain True/False at all *)
   1.378 +		(* prop_formula -> int *)
   1.379 +		fun cnf_number_of_clauses (And (fm1,fm2)) =
   1.380 +			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
   1.381 +		  | cnf_number_of_clauses _ =
   1.382 +			1
   1.383 +		(* prop_formula -> string *)
   1.384 +		fun cnf_prop_formula_to_string (BoolVar i) =
   1.385 +			if (i<1) then
   1.386 +				raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains a variable index less than 1")
   1.387 +			else
   1.388 +				(string_of_int i)
   1.389 +		  | cnf_prop_formula_to_string (Not fm1) =
   1.390 +			"-" ^ (cnf_prop_formula_to_string fm1)
   1.391 +		  | cnf_prop_formula_to_string (Or (fm1,fm2)) =
   1.392 +			(cnf_prop_formula_to_string fm1) ^ " " ^ (cnf_prop_formula_to_string fm2)
   1.393 +		  | cnf_prop_formula_to_string (And (fm1,fm2)) =
   1.394 +			(cnf_prop_formula_to_string fm1) ^ " 0\n" ^ (cnf_prop_formula_to_string fm2)
   1.395 +		  | cnf_prop_formula_to_string _ =
   1.396 +			raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains True/False")
   1.397 +	in
   1.398 +		File.write path ("c This file was generated by prop_formula_to_dimacs_cnf_format\n"
   1.399 +			^ "c (c) Tjark Weber\n"
   1.400 +			^ "p cnf " ^ (string_of_int (max_var_index fm')) ^ " " ^ (string_of_int (cnf_number_of_clauses fm')) ^ "\n"
   1.401 +			^ (cnf_prop_formula_to_string fm') ^ "\n")
   1.402 +	end;
   1.403 +
   1.404 +(* ------------------------------------------------------------------------- *)
   1.405 +(* prop_formula_to_dimacs_sat_format: serializes a formula of propositional  *)
   1.406 +(*      logic to a file in DIMACS SAT format (see "Satisfiability Suggested  *)
   1.407 +(*      Format", May 8 1993, Section 2.2)                                    *)
   1.408 +(* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
   1.409 +(*       index less than 1.                                                  *)
   1.410 +(* path: path of the file to be created                                      *)
   1.411 +(* ------------------------------------------------------------------------- *)
   1.412 +
   1.413 +	(* prop_formula -> Path.T -> unit *)
   1.414 +
   1.415 +	fun prop_formula_to_dimacs_sat_format fm path =
   1.416 +	let
   1.417 +		fun prop_formula_to_string True =
   1.418 +			"*()"
   1.419 +		  | prop_formula_to_string False =
   1.420 +			"+()"
   1.421 +		  | prop_formula_to_string (BoolVar i) =
   1.422 +			if (i<1) then
   1.423 +				raise REFUTE ("prop_formula_to_dimacs_sat_format", "formula contains a variable index less than 1")
   1.424 +			else
   1.425 +				(string_of_int i)
   1.426 +		  | prop_formula_to_string (Not fm1) =
   1.427 +			"-(" ^ (prop_formula_to_string fm1) ^ ")"
   1.428 +		  | prop_formula_to_string (Or (fm1,fm2)) =
   1.429 +			"+(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
   1.430 +		  | prop_formula_to_string (And (fm1,fm2)) =
   1.431 +			"*(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
   1.432 +	in
   1.433 +		File.write path ("c This file was generated by prop_formula_to_dimacs_sat_format\n"
   1.434 +			^ "c (c) Tjark Weber\n"
   1.435 +			^ "p sat " ^ (string_of_int (max (max_var_index fm, 1))) ^ "\n"
   1.436 +			^ "(" ^ (prop_formula_to_string fm) ^ ")\n")
   1.437 +	end;
   1.438 +
   1.439 +(* ------------------------------------------------------------------------- *)
   1.440 +(* prop_formula_sat_solver: try to find a satisfying assignment for the      *)
   1.441 +(*      boolean variables in a propositional formula, using an external SAT  *)
   1.442 +(*      solver.  If the SAT solver did not find an assignment, 'None' is     *)
   1.443 +(*      returned.  Otherwise 'Some (list of integers)' is returned, where    *)
   1.444 +(*      i>0 means that the boolean variable i is set to TRUE, and i<0 means  *)
   1.445 +(*      that the boolean variable i is set to FALSE.  Note that if           *)
   1.446 +(*      'satformat' is 'defcnf', then the assignment returned may contain    *)
   1.447 +(*      auxiliary variables that were not present in the original formula    *)
   1.448 +(*      'fm'.                                                                *)
   1.449 +(* fm        : formula that is passed to the SAT solver                      *) 
   1.450 +(* satpath   : path of the file used to store the propositional formula,     *)
   1.451 +(*             i.e. the input to the SAT solver                              *)
   1.452 +(* satformat : format of the SAT solver's input file.  Must be either "cnf", *)
   1.453 +(*             "defcnf", or "sat".                                           *)
   1.454 +(* resultpath: path of the file containing the SAT solver's output           *)
   1.455 +(* success   : part of the line in the SAT solver's output that is followed  *)
   1.456 +(*             by a line consisting of a list of integers representing the   *)
   1.457 +(*             satisfying assignment                                         *)
   1.458 +(* command   : system command used to execute the SAT solver                 *)
   1.459 +(* ------------------------------------------------------------------------- *)
   1.460 +
   1.461 +	(* prop_formula -> Path.T -> string -> Path.T -> string -> string -> int list option *)
   1.462 +
   1.463 +	fun prop_formula_sat_solver fm satpath satformat resultpath success command =
   1.464 +		if File.exists satpath then
   1.465 +			error ("file '" ^ (Path.pack satpath) ^ "' exists, please delete (will not overwrite)")
   1.466 +		else if File.exists resultpath then
   1.467 +			error ("file '" ^ (Path.pack resultpath) ^ "' exists, please delete (will not overwrite)")
   1.468 +		else
   1.469 +		(
   1.470 +			(* serialize the formula 'fm' to a file *)
   1.471 +			if satformat="cnf" then
   1.472 +				prop_formula_to_dimacs_cnf_format fm false satpath
   1.473 +			else if satformat="defcnf" then
   1.474 +				prop_formula_to_dimacs_cnf_format fm true satpath
   1.475 +			else if satformat="sat" then
   1.476 +				prop_formula_to_dimacs_sat_format fm satpath
   1.477 +			else
   1.478 +				error ("invalid argument: satformat='" ^ satformat ^ "' (must be either 'cnf', 'defcnf', or 'sat')");
   1.479 +			(* execute SAT solver *)
   1.480 +			if (system command)<>0 then
   1.481 +			(
   1.482 +				(* error executing SAT solver *)
   1.483 +				File.rm satpath;
   1.484 +				File.rm resultpath;
   1.485 +				error ("system command '" ^ command ^ "' failed (make sure a SAT solver is installed)")
   1.486 +			)
   1.487 +			else
   1.488 +			(
   1.489 +				(* read assignment from the result file *)
   1.490 +				File.rm satpath;
   1.491 +				let
   1.492 +					(* 'a option -> 'a Library.option *)
   1.493 +					fun option (SOME a) =
   1.494 +						Some a
   1.495 +					  | option NONE =
   1.496 +						None
   1.497 +					(* string -> int list *)
   1.498 +					fun string_to_int_list s =
   1.499 +						mapfilter (option o LargeInt.fromString) (space_explode " " s)
   1.500 +					(* string -> string -> bool *)
   1.501 +					fun is_substring s1 s2 =
   1.502 +					let
   1.503 +						val length1 = String.size s1
   1.504 +						val length2 = String.size s2
   1.505 +					in
   1.506 +						if length2 < length1 then
   1.507 +							false
   1.508 +						else if s1 = String.substring (s2, 0, length1) then
   1.509 +							true
   1.510 +						else is_substring s1 (String.substring (s2, 1, length2-1))
   1.511 +					end
   1.512 +					(* string list -> int list option *)
   1.513 +					fun extract_solution [] =
   1.514 +						None
   1.515 +					  | extract_solution (line::lines) =
   1.516 +						if is_substring success line then
   1.517 +							(* the next line must be a list of integers *)
   1.518 +							Some (string_to_int_list (hd lines))
   1.519 +						else
   1.520 +							extract_solution lines
   1.521 +					val sat_result = File.read resultpath
   1.522 +				in
   1.523 +					File.rm resultpath;
   1.524 +					extract_solution (split_lines sat_result)
   1.525 +				end
   1.526 +			)
   1.527 +		);
   1.528 +
   1.529 +
   1.530 +(* ------------------------------------------------------------------------- *)
   1.531 +(* TREES                                                                     *)
   1.532 +(* ------------------------------------------------------------------------- *)
   1.533 +
   1.534 +(* ------------------------------------------------------------------------- *)
   1.535 +(* tree: implements an arbitrarily (but finitely) branching tree as a list   *)
   1.536 +(*       of (lists of ...) elements                                          *)
   1.537 +(* ------------------------------------------------------------------------- *)
   1.538 +
   1.539 +	datatype 'a tree =
   1.540 +		  Leaf of 'a
   1.541 +		| Node of ('a tree) list;
   1.542 +
   1.543 +	type prop_tree =
   1.544 +		prop_formula list tree;
   1.545 +
   1.546 +	(* ('a -> 'b) -> 'a tree -> 'b tree *)
   1.547 +
   1.548 +	fun tree_map f tr =
   1.549 +		case tr of
   1.550 +		  Leaf x  => Leaf (f x)
   1.551 +		| Node xs => Node (map (tree_map f) xs);
   1.552 +
   1.553 +	(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
   1.554 +
   1.555 +	fun tree_foldl f =
   1.556 +	let
   1.557 +		fun itl (e, Leaf x)  = f(e,x)
   1.558 +		  | itl (e, Node xs) = foldl (tree_foldl f) (e,xs)
   1.559 +	in
   1.560 +		itl
   1.561 +	end;
   1.562 +
   1.563 +	(* 'a tree * 'b tree -> ('a * 'b) tree *)
   1.564 +
   1.565 +	fun tree_pair (t1,t2) =
   1.566 +		case t1 of
   1.567 +		  Leaf x =>
   1.568 +			(case t2 of
   1.569 +				  Leaf y => Leaf (x,y)
   1.570 +				| Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)"))
   1.571 +		| Node xs =>
   1.572 +			(case t2 of
   1.573 +				  (* '~~' will raise an exception if the number of branches in both trees is different at the current node *)
   1.574 +				  Node ys => Node (map tree_pair (xs ~~ ys))
   1.575 +				| Leaf _  => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
   1.576 +
   1.577 +(* ------------------------------------------------------------------------- *)
   1.578 +(* prop_tree_to_true: returns a propositional formula that is true iff the   *)
   1.579 +(*      tree denotes the boolean value TRUE                                  *)
   1.580 +(* ------------------------------------------------------------------------- *)
   1.581 +
   1.582 +	(* prop_tree -> prop_formula *)
   1.583 +
   1.584 +	(* a term of type 'bool' is represented as a 2-element leaf, where *)
   1.585 +	(* the term is true iff the leaf's first element is true           *)
   1.586 +
   1.587 +	fun prop_tree_to_true (Leaf [fm,_]) =
   1.588 +		fm
   1.589 +	  | prop_tree_to_true _ =
   1.590 +		raise REFUTE ("prop_tree_to_true", "tree is not a 2-element leaf");
   1.591 +
   1.592 +(* ------------------------------------------------------------------------- *)
   1.593 +(* prop_tree_to_false: returns a propositional formula that is true iff the  *)
   1.594 +(*      tree denotes the boolean value FALSE                                 *)
   1.595 +(* ------------------------------------------------------------------------- *)
   1.596 +
   1.597 +	(* prop_tree -> prop_formula *)
   1.598 +
   1.599 +	(* a term of type 'bool' is represented as a 2-element leaf, where *)
   1.600 +	(* the term is false iff the leaf's second element is true         *)
   1.601 +
   1.602 +	fun prop_tree_to_false (Leaf [_,fm]) =
   1.603 +		fm
   1.604 +	  | prop_tree_to_false _ =
   1.605 +		raise REFUTE ("prop_tree_to_false", "tree is not a 2-element leaf");
   1.606 +
   1.607 +(* ------------------------------------------------------------------------- *)
   1.608 +(* restrict_to_single_element: returns a propositional formula which is true *)
   1.609 +(*      iff the tree 'tr' describes a single element of its corresponding    *)
   1.610 +(*      type, i.e. iff at each leaf, one and only one formula is true        *)
   1.611 +(* ------------------------------------------------------------------------- *)
   1.612 +
   1.613 +	(* prop_tree -> prop_formula *)
   1.614 +
   1.615 +	fun restrict_to_single_element tr =
   1.616 +	let
   1.617 +		(* prop_formula list -> prop_formula *)
   1.618 +		fun allfalse []      = True
   1.619 +		  | allfalse (x::xs) = SAnd (SNot x, allfalse xs)
   1.620 +		(* prop_formula list -> prop_formula *)
   1.621 +		fun exactly1true []      = False
   1.622 +		  | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
   1.623 +	in
   1.624 +		case tr of
   1.625 +		  Leaf [BoolVar _, Not (BoolVar _)] => True (* optimization for boolean variables *)
   1.626 +		| Leaf xs                           => exactly1true xs
   1.627 +		| Node trees                        => list_conjunction (map restrict_to_single_element trees)
   1.628 +	end;
   1.629 +
   1.630 +(* ------------------------------------------------------------------------- *)
   1.631 +(* HOL FORMULAS                                                              *)
   1.632 +(* ------------------------------------------------------------------------- *)
   1.633 +
   1.634 +(* ------------------------------------------------------------------------- *)
   1.635 +(* absvar: form an abstraction over a schematic variable                     *)
   1.636 +(* ------------------------------------------------------------------------- *)
   1.637 +
   1.638 +	(* Term.indexname * Term.typ * Term.term -> Term.term *)
   1.639 +
   1.640 +	(* this function is similar to Term.absfree, but for schematic       *)
   1.641 +	(* variables (rather than free variables)                            *)
   1.642 +	fun absvar ((x,i),T,body) =
   1.643 +		Abs(x, T, abstract_over (Var((x,i),T), body));
   1.644 +
   1.645 +(* ------------------------------------------------------------------------- *)
   1.646 +(* list_all_var: quantification over a list of schematic variables           *)
   1.647 +(* ------------------------------------------------------------------------- *)
   1.648 +
   1.649 +	(* (Term.indexname * Term.typ) list * Term.term -> Term.term *)
   1.650 +
   1.651 +	(* this function is similar to Term.list_all_free, but for schematic *)
   1.652 +	(* variables (rather than free variables)                            *)
   1.653 +	fun list_all_var ([], t) =
   1.654 +		t
   1.655 +	  | list_all_var ((idx,T)::vars, t) =
   1.656 +		(all T) $ (absvar(idx, T, list_all_var(vars,t)));
   1.657 +
   1.658 +(* ------------------------------------------------------------------------- *)
   1.659 +(* close_vars: close up a formula over all schematic variables by            *)
   1.660 +(*             quantification (note that the result term may still contain   *)
   1.661 +(*             (non-schematic) free variables)                               *)
   1.662 +(* ------------------------------------------------------------------------- *)
   1.663 +
   1.664 +	(* Term.term -> Term.term *)
   1.665 +
   1.666 +	(* this function is similar to Logic.close_form, but for schematic   *)
   1.667 +	(* variables (rather than free variables)                            *)
   1.668 +	fun close_vars A =
   1.669 +		list_all_var (sort_wrt (fst o fst) (map dest_Var (term_vars A)), A);
   1.670 +
   1.671 +(* ------------------------------------------------------------------------- *)
   1.672 +(* make_universes: given a list 'xs' of "types" and a universe size 'size',  *)
   1.673 +(*      this function returns all possible partitions of the universe into   *)
   1.674 +(*      the "types" in 'xs' such that no "type" is empty.  If 'size' is less *)
   1.675 +(*      than 'length xs', the returned list of partitions is empty.          *)
   1.676 +(*      Otherwise, if the list 'xs' is empty, then the returned list of      *)
   1.677 +(*      partitions contains only the empty list, regardless of 'size'.       *)
   1.678 +(* ------------------------------------------------------------------------- *)
   1.679 +
   1.680 +	(* 'a list -> int -> ('a * int) list list *)
   1.681 +
   1.682 +	fun make_universes xs size =
   1.683 +	let
   1.684 +		(* 'a list -> int -> int -> ('a * int) list list *)
   1.685 +		fun make_partitions_loop (x::xs) 0 total =
   1.686 +			map (fn us => ((x,0)::us)) (make_partitions xs total)
   1.687 +		  | make_partitions_loop (x::xs) first total =
   1.688 +			(map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
   1.689 +		  | make_partitions_loop _ _ _ =
   1.690 +			raise REFUTE ("make_universes::make_partitions_loop", "empty list")
   1.691 +		and
   1.692 +		(* 'a list -> int -> ('a * int) list list *)
   1.693 +		make_partitions [x] size =
   1.694 +			(* we must use all remaining elements on the type 'x', so there is only one partition *)
   1.695 +			[[(x,size)]]
   1.696 +		  | make_partitions (x::xs) 0 =
   1.697 +			(* there are no elements left in the universe, so there is only one partition *)
   1.698 +			[map (fn t => (t,0)) (x::xs)]
   1.699 +		  | make_partitions (x::xs) size =
   1.700 +			(* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
   1.701 +			make_partitions_loop (x::xs) size size
   1.702 +		  | make_partitions _ _ =
   1.703 +			raise REFUTE ("make_universes::make_partitions", "empty list")
   1.704 +		val len = length xs
   1.705 +	in
   1.706 +		if size<len then
   1.707 +			(* the universe isn't big enough to make every type non-empty *)
   1.708 +			[]
   1.709 +		else if xs=[] then
   1.710 +			(* no types: return one universe, regardless of the size *)
   1.711 +			[[]]
   1.712 +		else
   1.713 +			(* partition into possibly empty types, then add 1 element to each type *)
   1.714 +			map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
   1.715 +	end;
   1.716 +
   1.717 +(* ------------------------------------------------------------------------- *)
   1.718 +(* sum: computes the sum of a list of integers; sum [] = 0                   *)
   1.719 +(* ------------------------------------------------------------------------- *)
   1.720 +
   1.721 +	(* int list -> int *)
   1.722 +
   1.723 +	fun sum xs = foldl (op +) (0, xs);
   1.724 +
   1.725 +(* ------------------------------------------------------------------------- *)
   1.726 +(* product: computes the product of a list of integers; product [] = 1       *)
   1.727 +(* ------------------------------------------------------------------------- *)
   1.728 +
   1.729 +	(* int list -> int *)
   1.730 +
   1.731 +	fun product xs = foldl (op *) (1, xs);
   1.732 +
   1.733 +(* ------------------------------------------------------------------------- *)
   1.734 +(* power: power(a,b) computes a^b, for a>=0, b>=0                            *)
   1.735 +(* ------------------------------------------------------------------------- *)
   1.736 +
   1.737 +	(* int * int -> int *)
   1.738 +
   1.739 +	fun power (a,0) = 1
   1.740 +	  | power (a,1) = a
   1.741 +	  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end;
   1.742 +
   1.743 +(* ------------------------------------------------------------------------- *)
   1.744 +(* size_of_type: returns the size of a type, where 'us' specifies the size   *)
   1.745 +(*      of each basic type (i.e. each type variable), and 'cdepth' specifies *)
   1.746 +(*      the maximal constructor depth for inductive datatypes                *)
   1.747 +(* ------------------------------------------------------------------------- *)
   1.748 +
   1.749 +	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int *)
   1.750 +
   1.751 +	fun size_of_type T us thy cdepth =
   1.752 +	let
   1.753 +		(* Term.typ -> (Term.typ * int) -> int *)
   1.754 +		fun lookup_size T [] =
   1.755 +			raise REFUTE ("size_of_type", "no size specified for type variable '" ^ (Sign.string_of_typ (sign_of thy) T) ^ "'")
   1.756 +		  | lookup_size T ((typ,size)::pairs) =
   1.757 +			if T=typ then size else lookup_size T pairs
   1.758 +	in
   1.759 +		case T of
   1.760 +		  Type ("prop", [])     => 2
   1.761 +		| Type ("bool", [])     => 2
   1.762 +		| Type ("Product_Type.unit", []) => 1
   1.763 +		| Type ("+", [T1,T2])   => (size_of_type T1 us thy cdepth) + (size_of_type T2 us thy cdepth)
   1.764 +		| Type ("*", [T1,T2])   => (size_of_type T1 us thy cdepth) * (size_of_type T2 us thy cdepth)
   1.765 +		| Type ("fun", [T1,T2]) => power (size_of_type T2 us thy cdepth, size_of_type T1 us thy cdepth)
   1.766 +		| Type ("set", [T1])    => size_of_type (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
   1.767 +		| Type (s, Ts)          =>
   1.768 +			(case DatatypePackage.datatype_info thy s of
   1.769 +			  Some info => (* inductive datatype *)
   1.770 +				if cdepth>0 then
   1.771 +					let
   1.772 +						val index               = #index info
   1.773 +						val descr               = #descr info
   1.774 +						val (_, dtyps, constrs) = the (assoc (descr, index))
   1.775 +						val Typs                = dtyps ~~ Ts
   1.776 +						(* DatatypeAux.dtyp -> Term.typ *)
   1.777 +						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
   1.778 +							the (assoc (Typs, DatatypeAux.DtTFree a))
   1.779 +						  | typ_of_dtyp (DatatypeAux.DtRec i) =
   1.780 +							let
   1.781 +								val (s, ds, _) = the (assoc (descr, i))
   1.782 +							in
   1.783 +								Type (s, map typ_of_dtyp ds)
   1.784 +							end
   1.785 +						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
   1.786 +							Type (s, map typ_of_dtyp ds)
   1.787 +					in
   1.788 +						sum (map (fn (_,ds) => product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)) constrs)
   1.789 +					end
   1.790 +				else 0
   1.791 +			| None      => error ("size_of_type: type contains an unknown type constructor: '" ^ s ^ "'"))
   1.792 +		| TFree _               => lookup_size T us
   1.793 +		| TVar _                => lookup_size T us
   1.794 +	end;
   1.795 +
   1.796 +(* ------------------------------------------------------------------------- *)
   1.797 +(* type_to_prop_tree: creates a tree of boolean variables that denotes an    *)
   1.798 +(*      element of the type 'T'.  The height and branching factor of the     *)
   1.799 +(*      tree depend on the size and "structure" of 'T'.                      *)
   1.800 +(* 'us' : a "universe" specifying the number of elements for each basic type *)
   1.801 +(*        (i.e. each type variable) in 'T'                                   *)
   1.802 +(* 'cdepth': maximum constructor depth to be used for inductive datatypes    *)
   1.803 +(* 'idx': the next index to be used for a boolean variable                   *)
   1.804 +(* ------------------------------------------------------------------------- *)
   1.805 +
   1.806 +	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *)
   1.807 +
   1.808 +	fun type_to_prop_tree T us thy cdepth idx =
   1.809 +	let
   1.810 +		(* int -> Term.typ -> int -> prop_tree list * int *)
   1.811 +		fun type_to_prop_tree_list 1 T' idx' =
   1.812 +			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
   1.813 +				([tr], newidx)
   1.814 +			end
   1.815 +		  | type_to_prop_tree_list n T' idx' =
   1.816 +			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
   1.817 +				let val (trees, lastidx) = type_to_prop_tree_list (n-1) T' newidx in
   1.818 +					(tr::trees, lastidx)
   1.819 +				end
   1.820 +			end
   1.821 +	in
   1.822 +		case T of
   1.823 +		  Type ("prop", []) =>
   1.824 +			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
   1.825 +		| Type ("bool", []) =>
   1.826 +			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
   1.827 +		| Type ("Product_Type.unit", []) =>
   1.828 +			(Leaf [True], idx)
   1.829 +		| Type ("+", [T1,T2]) =>
   1.830 +			let
   1.831 +				val s1 = size_of_type T1 us thy cdepth
   1.832 +				val s2 = size_of_type T2 us thy cdepth
   1.833 +				val s  = s1 + s2
   1.834 +			in
   1.835 +				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
   1.836 +					raise EMPTY_DATATYPE
   1.837 +				else
   1.838 +					error "sum types (+) not implemented yet (TODO)"
   1.839 +			end
   1.840 +		| Type ("*", [T1,T2]) =>
   1.841 +			let
   1.842 +				val s1 = size_of_type T1 us thy cdepth
   1.843 +				val s2 = size_of_type T2 us thy cdepth
   1.844 +				val s  = s1 * s2
   1.845 +			in
   1.846 +				if s1=0 orelse s2=0 then
   1.847 +					raise EMPTY_DATATYPE
   1.848 +				else
   1.849 +					error "product types (*) not implemented yet (TODO)"
   1.850 +			end
   1.851 +		| Type ("fun", [T1,T2]) =>
   1.852 +			(* we create 'size_of_type T1' different copies of the tree for 'T2', *)
   1.853 +			(* which are then combined into a single new tree                     *)
   1.854 +			let
   1.855 +				val s = size_of_type T1 us thy cdepth
   1.856 +			in
   1.857 +				if s=0 then
   1.858 +					raise EMPTY_DATATYPE
   1.859 +				else
   1.860 +					let val (trees, newidx) = type_to_prop_tree_list s T2 idx in
   1.861 +						(Node trees, newidx)
   1.862 +					end
   1.863 +			end
   1.864 +		| Type ("set", [T1]) =>
   1.865 +			type_to_prop_tree (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth idx
   1.866 +		| Type (s, _) =>
   1.867 +			(case DatatypePackage.constrs_of thy s of
   1.868 +			   Some _ => (* inductive datatype *)
   1.869 +					let
   1.870 +						val s = size_of_type T us thy cdepth
   1.871 +					in
   1.872 +						if s=0 then
   1.873 +							raise EMPTY_DATATYPE
   1.874 +						else
   1.875 +							(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
   1.876 +					end
   1.877 +			 | None   => error ("type_to_prop_tree: type contains an unknown type constructor: '" ^ s ^ "'"))
   1.878 +		| TFree _ =>
   1.879 +			let val s = size_of_type T us thy cdepth in
   1.880 +				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
   1.881 +			end
   1.882 +		| TVar _  =>
   1.883 +			let val s = size_of_type T us thy cdepth in
   1.884 +				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
   1.885 +			end
   1.886 +	end;
   1.887 +
   1.888 +(* ------------------------------------------------------------------------- *)
   1.889 +(* type_to_constants: creates a list of prop_trees with constants (True,     *)
   1.890 +(*      False) rather than boolean variables, one for every element in the   *)
   1.891 +(*      type 'T'; c.f. type_to_prop_tree                                     *)
   1.892 +(* ------------------------------------------------------------------------- *)
   1.893 +
   1.894 +	(* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *)
   1.895 +
   1.896 +	fun type_to_constants T us thy cdepth =
   1.897 +	let
   1.898 +		(* returns a list with all unit vectors of length n *)
   1.899 +		(* int -> prop_tree list *)
   1.900 +		fun unit_vectors n =
   1.901 +		let
   1.902 +			(* returns the k-th unit vector of length n *)
   1.903 +			(* int * int -> prop_tree *)
   1.904 +			fun unit_vector (k,n) =
   1.905 +				Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
   1.906 +			(* int -> prop_tree list -> prop_tree list *)
   1.907 +			fun unit_vectors_acc k vs =
   1.908 +				if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
   1.909 +		in
   1.910 +			unit_vectors_acc 1 []
   1.911 +		end
   1.912 +		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
   1.913 +		(* 'a -> 'a list list -> 'a list list *)
   1.914 +		fun cons_list x xss =
   1.915 +			map (fn xs => x::xs) xss
   1.916 +		(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
   1.917 +		(* int -> 'a list -> 'a list list *)
   1.918 +		fun pick_all 1 xs =
   1.919 +			map (fn x => [x]) xs
   1.920 +		  | pick_all n xs =
   1.921 +			let val rec_pick = pick_all (n-1) xs in
   1.922 +				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   1.923 +			end
   1.924 +	in
   1.925 +		case T of
   1.926 +		  Type ("prop", [])     => unit_vectors 2
   1.927 +		| Type ("bool", [])     => unit_vectors 2
   1.928 +		| Type ("Product_Type.unit", []) => unit_vectors 1
   1.929 +                | Type ("+", [T1,T2])   =>
   1.930 +			let
   1.931 +				val s1 = size_of_type T1 us thy cdepth
   1.932 +				val s2 = size_of_type T2 us thy cdepth
   1.933 +			in
   1.934 +				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
   1.935 +					raise EMPTY_DATATYPE
   1.936 +				else
   1.937 +					error "sum types (+) not implemented yet (TODO)"
   1.938 +			end
   1.939 +                | Type ("*", [T1,T2])   =>
   1.940 +			let
   1.941 +				val s1 = size_of_type T1 us thy cdepth
   1.942 +				val s2 = size_of_type T2 us thy cdepth
   1.943 +			in
   1.944 +				if s1=0 orelse s2=0 then
   1.945 +					raise EMPTY_DATATYPE
   1.946 +				else
   1.947 +					error "product types (*) not implemented yet (TODO)"
   1.948 +			end
   1.949 +		| Type ("fun", [T1,T2]) =>
   1.950 +			let
   1.951 +				val s = size_of_type T1 us thy cdepth
   1.952 +			in
   1.953 +				if s=0 then
   1.954 +					raise EMPTY_DATATYPE
   1.955 +				else
   1.956 +					map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth))
   1.957 +			end
   1.958 +		| Type ("set", [T1])    => type_to_constants (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
   1.959 +		| Type (s, _)           =>
   1.960 +			(case DatatypePackage.constrs_of thy s of
   1.961 +			   Some _ => (* inductive datatype *)
   1.962 +					let
   1.963 +						val s = size_of_type T us thy cdepth
   1.964 +					in
   1.965 +						if s=0 then
   1.966 +							raise EMPTY_DATATYPE
   1.967 +						else
   1.968 +							unit_vectors s
   1.969 +					end
   1.970 +			 | None   => error ("type_to_constants: type contains an unknown type constructor: '" ^ s ^ "'"))
   1.971 +		| TFree _               => unit_vectors (size_of_type T us thy cdepth)
   1.972 +		| TVar _                => unit_vectors (size_of_type T us thy cdepth)
   1.973 +	end;
   1.974 +
   1.975 +(* ------------------------------------------------------------------------- *)
   1.976 +(* prop_tree_equal: returns a propositional formula that is true iff 'tr1'   *)
   1.977 +(*      and 'tr2' both denote the same element                               *)
   1.978 +(* ------------------------------------------------------------------------- *)
   1.979 +
   1.980 +	(* prop_tree * prop_tree -> prop_formula *)
   1.981 +
   1.982 +	fun prop_tree_equal (tr1,tr2) =
   1.983 +		case tr1 of
   1.984 +		  Leaf x =>
   1.985 +			(case tr2 of
   1.986 +			  Leaf y => prop_formula_dot_product (x,y)
   1.987 +			| _      => raise REFUTE ("prop_tree_equal", "second tree is higher"))
   1.988 +		| Node xs =>
   1.989 +			(case tr2 of
   1.990 +			  Leaf _  => raise REFUTE ("prop_tree_equal", "first tree is higher")
   1.991 +			(* extensionality: two functions are equal iff they are equal for every element *)
   1.992 +			| Node ys => list_conjunction (map prop_tree_equal (xs ~~ ys)));
   1.993 +
   1.994 +(* ------------------------------------------------------------------------- *)
   1.995 +(* prop_tree_apply: returns a tree that denotes the element obtained by      *)
   1.996 +(*      applying the function which is denoted by the tree 't1' to the       *)
   1.997 +(*      element which is denoted by the tree 't2'                            *)
   1.998 +(* ------------------------------------------------------------------------- *)
   1.999 +
  1.1000 +	(* prop_tree * prop_tree -> prop_tree *)
  1.1001 +
  1.1002 +	fun prop_tree_apply (tr1,tr2) =
  1.1003 +	let
  1.1004 +		(* prop_tree * prop_tree -> prop_tree *)
  1.1005 +		fun prop_tree_disjunction (tr1,tr2) =
  1.1006 +			tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
  1.1007 +		(* prop_formula * prop_tree -> prop_tree *)
  1.1008 +		fun prop_formula_times_prop_tree (fm,tr) =
  1.1009 +			tree_map (map (fn x => SAnd (fm,x))) tr
  1.1010 +		(* prop_formula list * prop_tree list -> prop_tree *)
  1.1011 +		fun prop_formula_list_dot_product_prop_tree_list ([fm],[tr]) =
  1.1012 +			prop_formula_times_prop_tree (fm,tr)
  1.1013 +		  | prop_formula_list_dot_product_prop_tree_list (fm::fms,tr::trees) =
  1.1014 +			prop_tree_disjunction (prop_formula_times_prop_tree (fm,tr), prop_formula_list_dot_product_prop_tree_list (fms,trees))
  1.1015 +		  | prop_formula_list_dot_product_prop_tree_list (_,_) =
  1.1016 +			raise REFUTE ("prop_tree_apply::prop_formula_list_dot_product_prop_tree_list", "empty list")
  1.1017 +		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1.1018 +		(* 'a -> 'a list list -> 'a list list *)
  1.1019 +		fun cons_list x xss =
  1.1020 +			map (fn xs => x::xs) xss
  1.1021 +		(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
  1.1022 +		(* 'a list list -> 'a list list *)
  1.1023 +		fun pick_all [xs] =
  1.1024 +			map (fn x => [x]) xs
  1.1025 +		  | pick_all (xs::xss) =
  1.1026 +			let val rec_pick = pick_all xss in
  1.1027 +				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1.1028 +			end
  1.1029 +		  | pick_all _ =
  1.1030 +			raise REFUTE ("prop_tree_apply::pick_all", "empty list")
  1.1031 +		(* prop_tree -> prop_formula list *)
  1.1032 +		fun prop_tree_to_prop_formula_list (Leaf xs) =
  1.1033 +			xs
  1.1034 +		  | prop_tree_to_prop_formula_list (Node trees) =
  1.1035 +			map list_conjunction (pick_all (map prop_tree_to_prop_formula_list trees))
  1.1036 +	in
  1.1037 +		case tr1 of
  1.1038 +		  Leaf _ =>
  1.1039 +			raise REFUTE ("prop_tree_apply", "first tree is a leaf")
  1.1040 +		| Node xs =>
  1.1041 +			prop_formula_list_dot_product_prop_tree_list (prop_tree_to_prop_formula_list tr2, xs)
  1.1042 +	end
  1.1043 +
  1.1044 +(* ------------------------------------------------------------------------- *)
  1.1045 +(* term_to_prop_tree: translates a HOL term 't' into a tree of propositional *)
  1.1046 +(*      formulas; 'us' specifies the number of elements for each type        *)
  1.1047 +(*      variable in 't'; 'cdepth' specifies the maximal constructor depth    *)
  1.1048 +(*      for inductive datatypes.  Also returns the lowest index that was not *)
  1.1049 +(*      used for a boolean variable, and a substitution of terms (free/      *)
  1.1050 +(*      schematic variables) by prop_trees.                                  *)
  1.1051 +(* ------------------------------------------------------------------------- *)
  1.1052 +
  1.1053 +	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_tree * (int * (Term.term * prop_tree) list) *)
  1.1054 +
  1.1055 +	fun term_to_prop_tree t us thy cdepth =
  1.1056 +	let
  1.1057 +		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree * (int * (Term.term * prop_tree) list) *)
  1.1058 +		fun variable_to_prop_tree_subst t' (idx,subs) =
  1.1059 +			case assoc (subs,t') of
  1.1060 +			  Some tr =>
  1.1061 +				(* return the previously associated tree; the substitution remains unchanged *)
  1.1062 +				(tr, (idx,subs))
  1.1063 +			| None =>
  1.1064 +				(* generate a new tree; update the index; extend the substitution *)
  1.1065 +				let
  1.1066 +					val T = case t' of
  1.1067 +						  Free (_,T) => T
  1.1068 +						| Var (_,T)  => T
  1.1069 +						| _          => raise REFUTE ("variable_to_prop_tree_subst", "term is not a (free or schematic) variable")
  1.1070 +					val (tr,newidx) = type_to_prop_tree T us thy cdepth idx
  1.1071 +				in
  1.1072 +					(tr, (newidx, (t',tr)::subs))
  1.1073 +				end
  1.1074 +		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree list -> prop_tree * (int * (Term.term * prop_tree) list) *)
  1.1075 +		fun term_to_prop_tree_subst t' (idx,subs) bsubs =
  1.1076 +			case t' of
  1.1077 +			(* meta-logical constants *)
  1.1078 +			  Const ("Goal", _) $ t1 =>
  1.1079 +				term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1080 +			| Const ("all", _) $ t1 =>
  1.1081 +				let
  1.1082 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1083 +				in
  1.1084 +					case tree1 of
  1.1085 +					  Node xs =>
  1.1086 +						let
  1.1087 +							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
  1.1088 +							val fmFalse = list_disjunction (map prop_tree_to_false xs)
  1.1089 +						in
  1.1090 +							(Leaf [fmTrue, fmFalse], (i1,s1))
  1.1091 +						end
  1.1092 +					| _ =>
  1.1093 +						raise REFUTE ("term_to_prop_tree_subst", "'all' is not followed by a function")
  1.1094 +				end
  1.1095 +			| Const ("==", _) $ t1 $ t2 =>
  1.1096 +				let
  1.1097 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1098 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.1099 +					val fmTrue          = prop_tree_equal (tree1,tree2)
  1.1100 +					val fmFalse         = SNot fmTrue
  1.1101 +				in
  1.1102 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.1103 +				end
  1.1104 +			| Const ("==>", _) $ t1 $ t2 =>
  1.1105 +				let
  1.1106 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1107 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.1108 +					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
  1.1109 +					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
  1.1110 +				in
  1.1111 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.1112 +				end
  1.1113 +			(* HOL constants *)
  1.1114 +			| Const ("Trueprop", _) $ t1 =>
  1.1115 +				term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1116 +			| Const ("Not", _) $ t1 =>
  1.1117 +				let
  1.1118 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1119 +					val fmTrue          = prop_tree_to_false tree1
  1.1120 +					val fmFalse         = prop_tree_to_true tree1
  1.1121 +				in
  1.1122 +					(Leaf [fmTrue, fmFalse], (i1,s1))
  1.1123 +				end
  1.1124 +			| Const ("True", _) =>
  1.1125 +				(Leaf [True, False], (idx,subs))
  1.1126 +			| Const ("False", _) =>
  1.1127 +				(Leaf [False, True], (idx,subs))
  1.1128 +			| Const ("All", _) $ t1 =>
  1.1129 +				let
  1.1130 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1131 +				in
  1.1132 +					case tree1 of
  1.1133 +					  Node xs =>
  1.1134 +						let
  1.1135 +							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
  1.1136 +							val fmFalse = list_disjunction (map prop_tree_to_false xs)
  1.1137 +						in
  1.1138 +							(Leaf [fmTrue, fmFalse], (i1,s1))
  1.1139 +						end
  1.1140 +					| _ =>
  1.1141 +						raise REFUTE ("term_to_prop_tree_subst", "'All' is not followed by a function")
  1.1142 +				end
  1.1143 +			| Const ("Ex", _) $ t1 =>
  1.1144 +				let
  1.1145 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1146 +				in
  1.1147 +					case tree1 of
  1.1148 +					  Node xs =>
  1.1149 +						let
  1.1150 +							val fmTrue  = list_disjunction (map prop_tree_to_true xs)
  1.1151 +							val fmFalse = list_conjunction (map prop_tree_to_false xs)
  1.1152 +						in
  1.1153 +							(Leaf [fmTrue, fmFalse], (i1,s1))
  1.1154 +						end
  1.1155 +					| _ =>
  1.1156 +						raise REFUTE ("term_to_prop_tree_subst", "'Ex' is not followed by a function")
  1.1157 +				end
  1.1158 +			| Const ("Ex1", Type ("fun", [Type ("fun", [T, Type ("bool",[])]), Type ("bool",[])])) $ t1 =>
  1.1159 +				(* 'Ex1 t1' is equivalent to 'Ex Abs(x,T,t1' x & All Abs(y,T,t1'' y --> x=y))' *)
  1.1160 +				let
  1.1161 +					val t1'      = Term.incr_bv (1, 0, t1)
  1.1162 +					val t1''     = Term.incr_bv (2, 0, t1)
  1.1163 +					val t_equal  = (HOLogic.eq_const T) $ (Bound 1) $ (Bound 0)
  1.1164 +					val t_unique = (HOLogic.all_const T) $ Abs("y",T,HOLogic.mk_imp (t1'' $ (Bound 0),t_equal))
  1.1165 +					val t_ex1    = (HOLogic.exists_const T) $ Abs("x",T,HOLogic.mk_conj (t1' $ (Bound 0),t_unique))
  1.1166 +				in
  1.1167 +					term_to_prop_tree_subst t_ex1 (idx,subs) bsubs
  1.1168 +				end
  1.1169 +			| Const ("op =", _) $ t1 $ t2 =>
  1.1170 +				let
  1.1171 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1172 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.1173 +					val fmTrue          = prop_tree_equal (tree1,tree2)
  1.1174 +					val fmFalse         = SNot fmTrue
  1.1175 +				in
  1.1176 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.1177 +				end
  1.1178 +			| Const ("op &", _) $ t1 $ t2 =>
  1.1179 +				let
  1.1180 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1181 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.1182 +					val fmTrue          = SAnd (prop_tree_to_true tree1, prop_tree_to_true tree2)
  1.1183 +					val fmFalse         = SOr (prop_tree_to_false tree1, prop_tree_to_false tree2)
  1.1184 +				in
  1.1185 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.1186 +				end
  1.1187 +			| Const ("op |", _) $ t1 $ t2 =>
  1.1188 +				let
  1.1189 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1190 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.1191 +					val fmTrue          = SOr (prop_tree_to_true tree1, prop_tree_to_true tree2)
  1.1192 +					val fmFalse         = SAnd (prop_tree_to_false tree1, prop_tree_to_false tree2)
  1.1193 +				in
  1.1194 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.1195 +				end
  1.1196 +			| Const ("op -->", _) $ t1 $ t2 =>
  1.1197 +				let
  1.1198 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1199 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.1200 +					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
  1.1201 +					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
  1.1202 +				in
  1.1203 +					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.1204 +				end
  1.1205 +			(* set constants *)
  1.1206 +			| Const ("Collect", _) $ t1 =>
  1.1207 +				term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1208 +			| Const ("op :", _) $ t1 $ t2 =>
  1.1209 +				term_to_prop_tree_subst (t2 $ t1) (idx,subs) bsubs
  1.1210 +			(* datatype constants *)
  1.1211 +			| Const ("Product_Type.Unity", _) =>
  1.1212 +				(Leaf [True], (idx,subs))
  1.1213 +			(* unknown constants *)
  1.1214 +			| Const (c, _) =>
  1.1215 +				error ("term contains an unknown constant: '" ^ c ^ "'")
  1.1216 +			(* abstractions *)
  1.1217 +			| Abs (_,T,body) =>
  1.1218 +				let
  1.1219 +					val constants       = type_to_constants T us thy cdepth
  1.1220 +					val (trees, substs) = split_list (map (fn c => term_to_prop_tree_subst body (idx,subs) (c::bsubs)) constants)
  1.1221 +				in
  1.1222 +					(* the substitutions in 'substs' are all identical *)
  1.1223 +					(Node trees, hd substs)
  1.1224 +				end
  1.1225 +			(* (free/schematic) variables *)
  1.1226 +			| Free _ =>
  1.1227 +				variable_to_prop_tree_subst t' (idx,subs)
  1.1228 +			| Var _ =>
  1.1229 +				variable_to_prop_tree_subst t' (idx,subs)
  1.1230 +			(* bound variables *)
  1.1231 +			| Bound i =>
  1.1232 +				if (length bsubs) <= i then
  1.1233 +					raise REFUTE ("term_to_prop_tree_subst", "term contains a loose bound variable (with index " ^ (string_of_int i) ^ ")")
  1.1234 +				else
  1.1235 +					(nth_elem (i,bsubs), (idx,subs))
  1.1236 +			(* application *)
  1.1237 +			| t1 $ t2 =>
  1.1238 +				let
  1.1239 +					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.1240 +					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.1241 +				in
  1.1242 +					(prop_tree_apply (tree1,tree2), (i2,s2))
  1.1243 +				end
  1.1244 +	in
  1.1245 +		term_to_prop_tree_subst t (1,[]) []
  1.1246 +	end;
  1.1247 +
  1.1248 +(* ------------------------------------------------------------------------- *)
  1.1249 +(* term_to_prop_formula: translates a HOL formula 't' into a propositional   *)
  1.1250 +(*      formula that is satisfiable if and only if 't' has a model of "size" *)
  1.1251 +(*      'us' (where 'us' specifies the number of elements for each free type *)
  1.1252 +(*      variable in 't') and maximal constructor depth 'cdepth'.             *)
  1.1253 +(* ------------------------------------------------------------------------- *)
  1.1254 +
  1.1255 +	(* TODO: shouldn't 'us' also specify the number of elements for schematic type variables? (if so, modify the comment above) *)
  1.1256 +
  1.1257 +	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_formula * (int * (Term.term * prop_tree) list) *)
  1.1258 +
  1.1259 +	fun term_to_prop_formula t us thy cdepth =
  1.1260 +	let
  1.1261 +		val (tr, (idx,subs)) = term_to_prop_tree t us thy cdepth
  1.1262 +		val fm               = prop_tree_to_true tr
  1.1263 +	in
  1.1264 +		if subs=[] then
  1.1265 +			(fm, (idx,subs))
  1.1266 +		else
  1.1267 +			(* make sure every tree that is substituted for a term describes a single element *)
  1.1268 +			(SAnd (list_conjunction (map (fn (_,tr) => restrict_to_single_element tr) subs), fm), (idx,subs))
  1.1269 +	end;
  1.1270 +
  1.1271 +
  1.1272 +(* ------------------------------------------------------------------------- *)
  1.1273 +(* INTERFACE, PART 2: FINDING A MODEL                                        *)
  1.1274 +(* ------------------------------------------------------------------------- *)
  1.1275 +
  1.1276 +(* ------------------------------------------------------------------------- *)
  1.1277 +(* string_of_universe: prints a universe, i.e. an assignment of sizes for    *)
  1.1278 +(*                     types                                                 *)
  1.1279 +(* thy: the current theory                                                   *)
  1.1280 +(* us : a list containing types together with their size                     *)
  1.1281 +(* ------------------------------------------------------------------------- *)
  1.1282 +
  1.1283 +	(* theory -> (Term.typ * int) list -> string *)
  1.1284 +
  1.1285 +	fun string_of_universe thy [] =
  1.1286 +		"empty universe (no type variables in term)"
  1.1287 +	  | string_of_universe thy us =
  1.1288 +		space_implode ", " (map (fn (T,i) => (Sign.string_of_typ (sign_of thy) T) ^ ": " ^ (string_of_int i)) us);
  1.1289 +
  1.1290 +(* ------------------------------------------------------------------------- *)
  1.1291 +(* string_of_model: prints a model, given by a substitution 'subs' of trees  *)
  1.1292 +(*      of propositional variables and an assignment 'ass' of truth values   *)
  1.1293 +(*      for these variables.                                                 *)
  1.1294 +(* thy   : the current theory                                                *)
  1.1295 +(* us    : universe, specifies the "size" of each type (i.e. type variable)  *)
  1.1296 +(* cdepth: maximal constructor depth for inductive datatypes                 *)
  1.1297 +(* subs  : substitution of trees of propositional formulas (for variables)   *)
  1.1298 +(* ass   : assignment of truth values for boolean variables; see function    *)
  1.1299 +(*         'truth_value' below for its meaning                               *)
  1.1300 +(* ------------------------------------------------------------------------- *)
  1.1301 +
  1.1302 +	(* theory -> (Term.typ * int) list -> int -> (Term.term * prop_formula tree) list -> int list -> string *)
  1.1303 +
  1.1304 +	fun string_of_model thy us cdepth [] ass =
  1.1305 +		"empty interpretation (no free variables in term)"
  1.1306 +	  | string_of_model thy us cdepth subs ass =
  1.1307 +		let
  1.1308 +			(* Sign.sg *)
  1.1309 +			val sg = sign_of thy
  1.1310 +			(* int -> bool *)
  1.1311 +			fun truth_value i =
  1.1312 +				if i mem ass then true
  1.1313 +				else if ~i mem ass then false
  1.1314 +				else error ("SAT solver assignment does not specify a value for variable " ^ (string_of_int i))
  1.1315 +			(* string -> string *)
  1.1316 +			fun strip_leading_quote str =
  1.1317 +				if nth_elem_string(0,str)="'" then
  1.1318 +					String.substring (str, 1, size str - 1)
  1.1319 +				else
  1.1320 +					str;
  1.1321 +			(* prop_formula list -> int *)
  1.1322 +			fun true_index xs =
  1.1323 +				(* returns the (0-based) index of the first true formula in xs *)
  1.1324 +				let fun true_index_acc [] _ =
  1.1325 +					raise REFUTE ("string_of_model::true_index", "no variable was set to true")
  1.1326 +				      | true_index_acc (x::xs) n =
  1.1327 +					case x of
  1.1328 +					  BoolVar i =>
  1.1329 +						if truth_value i then n else true_index_acc xs (n+1)
  1.1330 +					| True =>
  1.1331 +						n
  1.1332 +					| False =>
  1.1333 +						true_index_acc xs (n+1)
  1.1334 +					| _ =>
  1.1335 +						raise REFUTE ("string_of_model::true_index", "formula is not a boolean variable/true/false")
  1.1336 +				in
  1.1337 +					true_index_acc xs 0
  1.1338 +				end
  1.1339 +			(* Term.typ -> int -> prop_tree -> string *)
  1.1340 +			(* prop *)
  1.1341 +			fun string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
  1.1342 +				if truth_value i then "true" else "false"
  1.1343 +			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [True, False]) =
  1.1344 +				"true"
  1.1345 +			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [False, True]) =
  1.1346 +				"false"
  1.1347 +			(* bool *)
  1.1348 +			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
  1.1349 +				if truth_value i then "true" else "false"
  1.1350 +			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [True, False]) =
  1.1351 +				"true"
  1.1352 +			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [False, True]) =
  1.1353 +				"false"
  1.1354 +			(* unit *)
  1.1355 +			  | string_of_prop_tree (Type ("Product_Type.unit",[])) cdepth (Leaf [True]) =
  1.1356 +				"()"
  1.1357 +			  | string_of_prop_tree (Type (s,Ts)) cdepth (Leaf xs) =
  1.1358 +				(case DatatypePackage.datatype_info thy s of
  1.1359 +				   Some info => (* inductive datatype *)
  1.1360 +					let
  1.1361 +						val index               = #index info
  1.1362 +						val descr               = #descr info
  1.1363 +						val (_, dtyps, constrs) = the (assoc (descr, index))
  1.1364 +						val Typs                = dtyps ~~ Ts
  1.1365 +						(* string -> string *)
  1.1366 +						fun unqualify s =
  1.1367 +							implode (snd (take_suffix (fn c => c <> ".") (explode s)))
  1.1368 +						(* DatatypeAux.dtyp -> Term.typ *)
  1.1369 +						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
  1.1370 +							the (assoc (Typs, DatatypeAux.DtTFree a))
  1.1371 +						  | typ_of_dtyp (DatatypeAux.DtRec i) =
  1.1372 +							let
  1.1373 +								val (s, ds, _) = the (assoc (descr, i))
  1.1374 +							in
  1.1375 +								Type (s, map typ_of_dtyp ds)
  1.1376 +							end
  1.1377 +						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
  1.1378 +							Type (s, map typ_of_dtyp ds)
  1.1379 +						(* DatatypeAux.dtyp list -> int -> string *)
  1.1380 +						fun string_of_inductive_type_cargs [] n =
  1.1381 +							if n<>0 then
  1.1382 +								raise REFUTE ("string_of_model", "internal error computing the element index for an inductive type")
  1.1383 +							else
  1.1384 +								""
  1.1385 +						  | string_of_inductive_type_cargs (d::ds) n =
  1.1386 +							let
  1.1387 +								val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
  1.1388 +							in
  1.1389 +								" " ^ (string_of_prop_tree (typ_of_dtyp d) (cdepth-1) (nth_elem (n div size_ds, type_to_constants (typ_of_dtyp d) us thy (cdepth-1)))) ^ (string_of_inductive_type_cargs ds (n mod size_ds))
  1.1390 +							end
  1.1391 +						(* (string * DatatypeAux.dtyp list) list -> int -> string *)
  1.1392 +						fun string_of_inductive_type_constrs [] n =
  1.1393 +							raise REFUTE ("string_of_model", "inductive type has fewer elements than needed")
  1.1394 +						  | string_of_inductive_type_constrs ((s,ds)::cs) n =
  1.1395 +							let
  1.1396 +								val size = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
  1.1397 +							in
  1.1398 +								if n < size then
  1.1399 +									(unqualify s) ^ (string_of_inductive_type_cargs ds n)
  1.1400 +								else
  1.1401 +									string_of_inductive_type_constrs cs (n - size)
  1.1402 +							end
  1.1403 +					in
  1.1404 +						string_of_inductive_type_constrs constrs (true_index xs)
  1.1405 +					end
  1.1406 +				 | None =>
  1.1407 +					raise REFUTE ("string_of_model", "type contains an unknown type constructor: '" ^ s ^ "'"))
  1.1408 +			(* type variable *)
  1.1409 +			  | string_of_prop_tree (TFree (s,_)) cdepth (Leaf xs) =
  1.1410 +					(strip_leading_quote s) ^ (string_of_int (true_index xs))
  1.1411 +			  | string_of_prop_tree (TVar ((s,_),_)) cdepth (Leaf xs) =
  1.1412 +					(strip_leading_quote s) ^ (string_of_int (true_index xs))
  1.1413 +			(* function or set type *)
  1.1414 +			  | string_of_prop_tree T cdepth (Node xs) =
  1.1415 +				case T of
  1.1416 +				  Type ("fun", [T1,T2]) =>
  1.1417 +					let
  1.1418 +						val strings = foldl (fn (ss,(c,x)) => ss @ [(string_of_prop_tree T1 cdepth c) ^ "\\<mapsto>" ^ (string_of_prop_tree T2 cdepth x)]) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
  1.1419 +					in
  1.1420 +						"(" ^ (space_implode ", " strings) ^ ")"
  1.1421 +					end
  1.1422 +				| Type ("set", [T1]) =>
  1.1423 +					let
  1.1424 +						val strings = foldl (fn (ss,(c,x)) => if (string_of_prop_tree (Type ("bool",[])) cdepth x)="true" then ss @ [string_of_prop_tree T1 cdepth c] else ss) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
  1.1425 +					in
  1.1426 +						"{" ^ (space_implode ", " strings) ^ "}"
  1.1427 +					end
  1.1428 +				| _ => raise REFUTE ("string_of_model::string_of_prop_tree", "not a function/set type")
  1.1429 +			(* Term.term * prop_formula tree -> string *)
  1.1430 +			fun string_of_term_assignment (t,tr) =
  1.1431 +			let
  1.1432 +				val T = case t of
  1.1433 +					  Free (_,T) => T
  1.1434 +					| Var (_,T)  => T
  1.1435 +					| _          => raise REFUTE ("string_of_model::string_of_term_assignment", "term is not a (free or schematic) variable")
  1.1436 +			in
  1.1437 +				(Sign.string_of_term sg t) ^ " = " ^ (string_of_prop_tree T cdepth tr)
  1.1438 +			end
  1.1439 +		in
  1.1440 +			space_implode "\n" (map string_of_term_assignment subs)
  1.1441 +		end;
  1.1442 +
  1.1443 +(* ------------------------------------------------------------------------- *)
  1.1444 +(* find_model: repeatedly calls 'prop_formula_sat_solver' with appropriate   *)
  1.1445 +(*             parameters, and displays the results to the user              *)
  1.1446 +(* params    : list of '(name, value)' pairs used to override default        *)
  1.1447 +(*             parameters                                                    *)
  1.1448 +(*                                                                           *)
  1.1449 +(* This is a brief description of the algorithm implemented:                 *)
  1.1450 +(*                                                                           *)
  1.1451 +(* 1. Let k = max ('minsize',1).                                             *)
  1.1452 +(* 2. Let the universe have k elements.  Find all possible partitions of     *)
  1.1453 +(*    these elements into the basic types occuring in 't' such that no basic *)
  1.1454 +(*    type is empty.                                                         *)
  1.1455 +(* 3. Translate 't' into a propositional formula p s.t. 't' has a model wrt. *)
  1.1456 +(*    the partition chosen in step (2.) if (actually, if and only if) p is   *)
  1.1457 +(*    satisfiable.  To do this, replace quantification by conjunction/       *)
  1.1458 +(*    disjunction over all elements of the type being quantified over.  (If  *)
  1.1459 +(*    p contains more than 'maxvars' boolean variables, terminate.)          *)
  1.1460 +(* 4. Serialize p to a file, and try to find a satisfying assignment for p   *)
  1.1461 +(*    by invoking an external SAT solver.                                    *)
  1.1462 +(* 5. If the SAT solver finds a satisfying assignment for p, translate this  *)
  1.1463 +(*    assignment back into a model for 't'.  Present this model to the user, *)
  1.1464 +(*    then terminate.                                                        *)
  1.1465 +(* 6. As long as there is another partition left, pick it and go back to     *)
  1.1466 +(*    step (3.).                                                             *)
  1.1467 +(* 7. Increase k by 1.  As long as k does not exceed 'maxsize', go back to   *)
  1.1468 +(*    step (2.).                                                             *)
  1.1469 +(*                                                                           *)
  1.1470 +(* The following parameters are currently supported (and required!):         *)
  1.1471 +(*                                                                           *)
  1.1472 +(* Name          Type    Description                                         *)
  1.1473 +(*                                                                           *)
  1.1474 +(* "minsize"     int     Only search for models with size at least           *)
  1.1475 +(*                       'minsize'.                                          *)
  1.1476 +(* "maxsize"     int     If >0, only search for models with size at most     *)
  1.1477 +(*                       'maxsize'.                                          *)
  1.1478 +(* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
  1.1479 +(*                       when transforming the term into a propositional     *)
  1.1480 +(*                       formula.                                            *)
  1.1481 +(* "satfile"     string  Name of the file used to store the propositional    *)
  1.1482 +(*                       formula, i.e. the input to the SAT solver.          *)
  1.1483 +(* "satformat"   string  Format of the SAT solver's input file.  Must be     *)
  1.1484 +(*                       either "cnf", "defcnf", or "sat".  Since "sat" is   *)
  1.1485 +(*                       not supported by most SAT solvers, and "cnf" can    *)
  1.1486 +(*                       cause exponential blowup of the formula, "defcnf"   *)
  1.1487 +(*                       is recommended.                                     *)
  1.1488 +(* "resultfile"  string  Name of the file containing the SAT solver's        *)
  1.1489 +(*                       output.                                             *)
  1.1490 +(* "success"     string  Part of the line in the SAT solver's output that    *)
  1.1491 +(*                       precedes a list of integers representing the        *)
  1.1492 +(*                       satisfying assignment.                              *)
  1.1493 +(* "command"     string  System command used to execute the SAT solver.      *)
  1.1494 +(*                       Note that you if you change 'satfile' or            *)
  1.1495 +(*                       'resultfile', you will also need to change          *)
  1.1496 +(*                       'command'.                                          *)
  1.1497 +(*                                                                           *)
  1.1498 +(* See the Isabelle/Isar theory 'Refute.thy' for reasonable default values.  *)
  1.1499 +(* ------------------------------------------------------------------------- *)
  1.1500 +
  1.1501 +	(* theory -> (string * string) list -> Term.term -> unit *)
  1.1502 +
  1.1503 +	fun find_model thy params t =
  1.1504 +	let
  1.1505 +		(* (string * string) list * (string * string) list -> (string * string) list *)
  1.1506 +		fun add_params (parms, []) =
  1.1507 +			parms
  1.1508 +		  | add_params (parms, defparm::defparms) =
  1.1509 +			add_params (gen_ins (fn (a, b) => (fst a) = (fst b)) (defparm, parms), defparms)
  1.1510 +		(* (string * string) list * string -> int *)
  1.1511 +		fun read_int (parms, name) =
  1.1512 +			case assoc_string (parms, name) of
  1.1513 +			  Some s => (case LargeInt.fromString s of
  1.1514 +				  SOME i => i
  1.1515 +				| NONE   => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
  1.1516 +			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
  1.1517 +		(* (string * string) list * string -> string *)
  1.1518 +		fun read_string (parms, name) =
  1.1519 +			case assoc_string (parms, name) of
  1.1520 +			  Some s => s
  1.1521 +			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
  1.1522 +		(* (string * string) list *)
  1.1523 +		val allparams  = add_params (params, get_default_params thy)
  1.1524 +		(* int *)
  1.1525 +		val minsize    = read_int (allparams, "minsize")
  1.1526 +		val maxsize    = read_int (allparams, "maxsize")
  1.1527 +		val maxvars    = read_int (allparams, "maxvars")
  1.1528 +		(* string *)
  1.1529 +		val satfile    = read_string (allparams, "satfile")
  1.1530 +		val satformat  = read_string (allparams, "satformat")
  1.1531 +		val resultfile = read_string (allparams, "resultfile")
  1.1532 +		val success    = read_string (allparams, "success")
  1.1533 +		val command    = read_string (allparams, "command")
  1.1534 +		(* misc *)
  1.1535 +		val satpath    = Path.unpack satfile
  1.1536 +		val resultpath = Path.unpack resultfile
  1.1537 +		val sg         = sign_of thy
  1.1538 +		(* Term.typ list *)
  1.1539 +		val tvars      = map (fn (i,s) => TVar(i,s)) (term_tvars t)
  1.1540 +		val tfrees     = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
  1.1541 +		(* universe -> int -> bool *)
  1.1542 +		fun find_model_universe u cdepth =
  1.1543 +			let
  1.1544 +				(* given the universe 'u' and constructor depth 'cdepth', translate *)
  1.1545 +        	                (* the term 't' into a propositional formula 'fm'                   *)
  1.1546 +				val (fm,(idx,subs)) = term_to_prop_formula t u thy cdepth
  1.1547 +				val usedvars        = idx-1
  1.1548 +			in
  1.1549 +				(* 'maxvars=0' means "use as many variables as necessary" *)
  1.1550 +				if usedvars>maxvars andalso maxvars<>0 then
  1.1551 +					(
  1.1552 +						(* too many variables used: terminate *)
  1.1553 +						writeln ("\nSearch terminated: " ^ (string_of_int usedvars) ^ " boolean variables used (only " ^ (string_of_int maxvars) ^ " allowed).");
  1.1554 +						true
  1.1555 +					)
  1.1556 +				else
  1.1557 +					(* pass the formula 'fm' to an external SAT solver *)
  1.1558 +					case prop_formula_sat_solver fm satpath satformat resultpath success command of
  1.1559 +					  None =>
  1.1560 +						(* no model found *)
  1.1561 +						false
  1.1562 +					| Some assignment =>
  1.1563 +						(* model found: terminate *)
  1.1564 +						(
  1.1565 +							writeln ("\nModel found:\n" ^ (string_of_universe thy u) ^ "\n" ^ (string_of_model thy u cdepth subs assignment));
  1.1566 +							true
  1.1567 +						)
  1.1568 +			end
  1.1569 +		(* universe list -> int -> bool *)
  1.1570 +		fun find_model_universes [] cdepth =
  1.1571 +			(
  1.1572 +				std_output "\n";
  1.1573 +				false
  1.1574 +			)
  1.1575 +		  | find_model_universes (u::us) cdepth =
  1.1576 +			(
  1.1577 +				std_output ".";
  1.1578 +				((if find_model_universe u cdepth then
  1.1579 +					(* terminate *)
  1.1580 +					true
  1.1581 +				else
  1.1582 +					(* continue search with the next universe *)
  1.1583 +					find_model_universes us cdepth)
  1.1584 +				handle EMPTY_DATATYPE => (std_output "[empty inductive type (constructor depth too small)]\n"; false))
  1.1585 +			)
  1.1586 +		(* int * int -> unit *)
  1.1587 +		fun find_model_from_to (min,max) =
  1.1588 +			(* 'max=0' means "search for arbitrary large models" *)
  1.1589 +			if min>max andalso max<>0 then
  1.1590 +				writeln ("Search terminated: no model found.")
  1.1591 +			else
  1.1592 +			(
  1.1593 +				std_output ("Searching for a model of size " ^ (string_of_int min));
  1.1594 +				if find_model_universes (make_universes tfrees min) min then
  1.1595 +					(* terminate *)
  1.1596 +					()
  1.1597 +				else
  1.1598 +					(* continue search with increased size *)
  1.1599 +					find_model_from_to (min+1, max)
  1.1600 +			)
  1.1601 +	in
  1.1602 +		writeln ("Trying to find a model of: " ^ (Sign.string_of_term sg t));
  1.1603 +		if tvars<>[] then
  1.1604 +			(* TODO: deal with schematic type variables in a better way, if possible *)
  1.1605 +			error "term contains schematic type variables"
  1.1606 +		else
  1.1607 +		(
  1.1608 +			if minsize<1 then
  1.1609 +				writeln ("'minsize' is less than 1; starting search with size 1.")
  1.1610 +			else
  1.1611 +				();
  1.1612 +			if maxsize<max (minsize,1) andalso maxsize<>0 then
  1.1613 +				writeln ("'maxsize' is less than 'minsize': no model found.")
  1.1614 +			else
  1.1615 +				find_model_from_to (max (minsize,1), maxsize)
  1.1616 +		)
  1.1617 +	end;
  1.1618 +
  1.1619 +(* ------------------------------------------------------------------------- *)
  1.1620 +(* refute_term: calls 'find_model' on the negation of a term                 *)
  1.1621 +(* params     : list of '(name, value)' pairs used to override default       *)
  1.1622 +(*              parameters                                                   *)
  1.1623 +(* ------------------------------------------------------------------------- *)
  1.1624 +
  1.1625 +	(* theory -> (string * string) list -> Term.term -> unit *)
  1.1626 +
  1.1627 +	fun refute_term thy params t =
  1.1628 +	let
  1.1629 +		(* TODO: schematic type variables? *)
  1.1630 +		val negation = close_vars (HOLogic.Not $ t)
  1.1631 +		(* If 't' is of type 'propT' (rather than 'boolT'), applying *)
  1.1632 +		(* 'HOLogic.Not' is not type-correct.  However, this isn't   *)
  1.1633 +		(* really a problem as long as 'find_model' still interprets *)
  1.1634 +		(* the resulting term correctly, without checking its type.  *)
  1.1635 +	in
  1.1636 +		find_model thy params negation
  1.1637 +	end;
  1.1638 +
  1.1639 +(* ------------------------------------------------------------------------- *)
  1.1640 +(* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
  1.1641 +(* params        : list of '(name, value)' pairs used to override default    *)
  1.1642 +(*                 parameters                                                *)
  1.1643 +(* subgoal       : 0-based index specifying the subgoal number               *)
  1.1644 +(* ------------------------------------------------------------------------- *)
  1.1645 +
  1.1646 +	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
  1.1647 +
  1.1648 +	fun refute_subgoal thy params thm subgoal =
  1.1649 +		refute_term thy params (nth_elem (subgoal, prems_of thm));
  1.1650 +
  1.1651 +end