support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps
authorwebertj
Wed Mar 10 22:33:48 2004 +0100 (2004-03-10)
changeset 14456cca28ec5f9a6
parent 14455 5c4a1e96efd6
child 14457 6d5d6e78d851
support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Mar 10 20:36:11 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed Mar 10 22:33:48 2004 +0100
     1.3 @@ -3,526 +3,77 @@
     1.4      Author:     Tjark Weber
     1.5      Copyright   2003-2004
     1.6  
     1.7 -Finite model generation for HOL formulae, using an external SAT solver.
     1.8 +Finite model generation for HOL formulae, using a SAT solver.
     1.9  *)
    1.10  
    1.11  (* ------------------------------------------------------------------------- *)
    1.12 -(* Declares the 'REFUTE' signature as well as a structure 'Refute'.  See     *)
    1.13 -(* 'find_model' below for a description of the implemented algorithm, and    *)
    1.14 -(* the Isabelle/Isar theories 'HOL/Refute.thy' and 'HOL/Main.thy' on how to  *)
    1.15 -(* set things up.                                                            *)
    1.16 +(* TODO: Change parameter handling so that only supported parameters can be  *)
    1.17 +(*       set, and specify defaults here, rather than in HOL/Main.thy.        *)
    1.18 +(* ------------------------------------------------------------------------- *)
    1.19 +
    1.20 +(* ------------------------------------------------------------------------- *)
    1.21 +(* Declares the 'REFUTE' signature as well as a structure 'Refute'.          *)
    1.22 +(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'.  *)
    1.23  (* ------------------------------------------------------------------------- *)
    1.24  
    1.25  signature REFUTE =
    1.26  sig
    1.27  
    1.28 +	exception REFUTE of string * string
    1.29 +
    1.30 +(* ------------------------------------------------------------------------- *)
    1.31 +(* Model/interpretation related code (translation HOL -> boolean formula)    *)
    1.32 +(* ------------------------------------------------------------------------- *)
    1.33 +
    1.34 +	exception CANNOT_INTERPRET
    1.35 +
    1.36 +	type interpretation
    1.37 +	type model
    1.38 +	type arguments
    1.39 +
    1.40 +	val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory
    1.41 +	val add_printer     : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory
    1.42 +
    1.43 +	val interpret           : theory -> model -> arguments -> Term.term -> interpretation * model * arguments  (* exception CANNOT_INTERPRET *)
    1.44 +	val is_satisfying_model : model -> interpretation -> bool -> PropLogic.prop_formula
    1.45 +
    1.46 +	val print       : theory -> model -> Term.term -> interpretation -> (int -> bool) -> string
    1.47 +	val print_model : theory -> model -> (int -> bool) -> string
    1.48 +
    1.49 +(* ------------------------------------------------------------------------- *)
    1.50 +(* Interface                                                                 *)
    1.51 +(* ------------------------------------------------------------------------- *)
    1.52 +
    1.53 +	val set_default_param  : (string * string) -> theory -> theory
    1.54 +	val get_default_param  : theory -> string -> string option
    1.55 +	val get_default_params : theory -> (string * string) list
    1.56 +	val actual_params      : theory -> (string * string) list -> (int * int * int * string)
    1.57 +
    1.58 +	val find_model : theory -> (int * int * int * string) -> Term.term -> bool -> unit
    1.59 +
    1.60 +	val satisfy_term   : theory -> (string * string) list -> Term.term -> unit  (* tries to find a model for a formula *)
    1.61 +	val refute_term    : theory -> (string * string) list -> Term.term -> unit  (* tries to find a model that refutes a formula *)
    1.62 +	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
    1.63 +
    1.64 +	val setup : (theory -> theory) list
    1.65 +end;
    1.66 +
    1.67 +structure Refute : REFUTE =
    1.68 +struct
    1.69 +
    1.70 +	open PropLogic;
    1.71 +
    1.72  	(* We use 'REFUTE' only for internal error conditions that should    *)
    1.73  	(* never occur in the first place (i.e. errors caused by bugs in our *)
    1.74  	(* code).  Otherwise (e.g. to indicate invalid input data) we use    *)
    1.75  	(* 'error'.                                                          *)
    1.76 -
    1.77 -	exception REFUTE of string * string;	(* ("in function", "cause") *)
    1.78 -
    1.79 -	val setup : (theory -> theory) list
    1.80 -
    1.81 -	val set_default_param : (string * string) -> theory -> theory
    1.82 -	val get_default_param : theory -> string -> string option
    1.83 -	val get_default_params : theory -> (string * string) list
    1.84 -
    1.85 -	val find_model : theory -> (string * string) list -> Term.term -> unit
    1.86 -
    1.87 -	val refute_term : theory -> (string * string) list -> Term.term -> unit
    1.88 -	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
    1.89 -end;
    1.90 -
    1.91 -
    1.92 -structure Refute : REFUTE =
    1.93 -struct
    1.94 -	exception REFUTE of string * string;
    1.95 -
    1.96 -	exception EMPTY_DATATYPE;
    1.97 -
    1.98 -	structure RefuteDataArgs =
    1.99 -	struct
   1.100 -		val name = "Refute/refute";
   1.101 -		type T = string Symtab.table;
   1.102 -		val empty = Symtab.empty;
   1.103 -		val copy = I;
   1.104 -		val prep_ext = I;
   1.105 -		val merge =
   1.106 -			fn (symTable1, symTable2) =>
   1.107 -				(Symtab.merge (op=) (symTable1, symTable2));
   1.108 -		fun print sg symTable =
   1.109 -			writeln
   1.110 -				("'refute', default parameters:\n" ^
   1.111 -				(space_implode "\n" (map (fn (name,value) => name ^ " = " ^ value) (Symtab.dest symTable))))
   1.112 -	end;
   1.113 -
   1.114 -	structure RefuteData = TheoryDataFun(RefuteDataArgs);
   1.115 -
   1.116 -
   1.117 -(* ------------------------------------------------------------------------- *)
   1.118 -(* INTERFACE, PART 1: INITIALIZATION, PARAMETER MANAGEMENT                   *)
   1.119 -(* ------------------------------------------------------------------------- *)
   1.120 -
   1.121 -(* ------------------------------------------------------------------------- *)
   1.122 -(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
   1.123 -(* structure                                                                 *)
   1.124 -(* ------------------------------------------------------------------------- *)
   1.125 -
   1.126 -	val setup = [RefuteData.init];
   1.127 -
   1.128 -(* ------------------------------------------------------------------------- *)
   1.129 -(* set_default_param: stores the '(name, value)' pair in RefuteData's symbol *)
   1.130 -(*                    table                                                  *)
   1.131 -(* ------------------------------------------------------------------------- *)
   1.132 -
   1.133 -	fun set_default_param (name, value) thy =
   1.134 -	let
   1.135 -		val symTable = RefuteData.get thy
   1.136 -	in
   1.137 -		case Symtab.lookup (symTable, name) of
   1.138 -			None   => RefuteData.put (Symtab.extend (symTable, [(name, value)])) thy
   1.139 -		|	Some _ => RefuteData.put (Symtab.update ((name, value), symTable)) thy
   1.140 -	end;
   1.141 -
   1.142 -(* ------------------------------------------------------------------------- *)
   1.143 -(* get_default_param: retrieves the value associated with 'name' from        *)
   1.144 -(*                    RefuteData's symbol table                              *)
   1.145 -(* ------------------------------------------------------------------------- *)
   1.146 -
   1.147 -	fun get_default_param thy name = Symtab.lookup (RefuteData.get thy, name);
   1.148 -
   1.149 -(* ------------------------------------------------------------------------- *)
   1.150 -(* get_default_params: returns a list of all '(name, value)' pairs that are  *)
   1.151 -(*                     stored in RefuteData's symbol table                   *)
   1.152 -(* ------------------------------------------------------------------------- *)
   1.153 -
   1.154 -	fun get_default_params thy = Symtab.dest (RefuteData.get thy);
   1.155 -
   1.156 -
   1.157 -(* ------------------------------------------------------------------------- *)
   1.158 -(* PROPOSITIONAL FORMULAS                                                    *)
   1.159 -(* ------------------------------------------------------------------------- *)
   1.160 -
   1.161 -(* ------------------------------------------------------------------------- *)
   1.162 -(* prop_formula: formulas of propositional logic, built from boolean         *)
   1.163 -(*               variables (referred to by index) and True/False using       *)
   1.164 -(*               not/or/and                                                  *)
   1.165 -(* ------------------------------------------------------------------------- *)
   1.166 -
   1.167 -	datatype prop_formula =
   1.168 -		  True
   1.169 -		| False
   1.170 -		| BoolVar of int
   1.171 -		| Not of prop_formula
   1.172 -		| Or of prop_formula * prop_formula
   1.173 -		| And of prop_formula * prop_formula;
   1.174 -
   1.175 -	(* the following constructor functions make sure that True and False do *)
   1.176 -	(* not occur within any of the other connectives (i.e. Not, Or, And)    *)
   1.177 -
   1.178 -	(* prop_formula -> prop_formula *)
   1.179 -
   1.180 -	fun SNot True  = False
   1.181 -	  | SNot False = True
   1.182 -	  | SNot fm    = Not fm;
   1.183 -
   1.184 -	(* prop_formula * prop_formula -> prop_formula *)
   1.185 -
   1.186 -	fun SOr (True, _)   = True
   1.187 -	  | SOr (_, True)   = True
   1.188 -	  | SOr (False, fm) = fm
   1.189 -	  | SOr (fm, False) = fm
   1.190 -	  | SOr (fm1, fm2)  = Or (fm1, fm2);
   1.191 -
   1.192 -	(* prop_formula * prop_formula -> prop_formula *)
   1.193 -
   1.194 -	fun SAnd (True, fm) = fm
   1.195 -	  | SAnd (fm, True) = fm
   1.196 -	  | SAnd (False, _) = False
   1.197 -	  | SAnd (_, False) = False
   1.198 -	  | SAnd (fm1, fm2) = And (fm1, fm2);
   1.199 +	exception REFUTE of string * string;  (* ("in function", "cause") *)
   1.200  
   1.201  (* ------------------------------------------------------------------------- *)
   1.202 -(* list_disjunction: computes the disjunction of a list of propositional     *)
   1.203 -(*                   formulas                                                *)
   1.204 -(* ------------------------------------------------------------------------- *)
   1.205 -
   1.206 -	(* prop_formula list -> prop_formula *)
   1.207 -
   1.208 -	fun list_disjunction []      = False
   1.209 -	  | list_disjunction (x::xs) = SOr (x, list_disjunction xs);
   1.210 -
   1.211 -(* ------------------------------------------------------------------------- *)
   1.212 -(* list_conjunction: computes the conjunction of a list of propositional     *)
   1.213 -(*                   formulas                                                *)
   1.214 -(* ------------------------------------------------------------------------- *)
   1.215 -
   1.216 -	(* prop_formula list -> prop_formula *)
   1.217 -
   1.218 -	fun list_conjunction []      = True
   1.219 -	  | list_conjunction (x::xs) = SAnd (x, list_conjunction xs);
   1.220 -
   1.221 -(* ------------------------------------------------------------------------- *)
   1.222 -(* prop_formula_dot_product: [x1,...,xn] * [y1,...,yn] -> x1*y1+...+xn*yn    *)
   1.223 -(* ------------------------------------------------------------------------- *)
   1.224 -
   1.225 -	(* prop_formula list * prop_formula list -> prop_formula *)
   1.226 -
   1.227 -	fun prop_formula_dot_product ([],[])       = False
   1.228 -	  | prop_formula_dot_product (x::xs,y::ys) = SOr (SAnd (x,y), prop_formula_dot_product (xs,ys))
   1.229 -	  | prop_formula_dot_product (_,_)         = raise REFUTE ("prop_formula_dot_product", "lists are of different length");
   1.230 -
   1.231 -(* ------------------------------------------------------------------------- *)
   1.232 -(* prop_formula_to_nnf: computes the negation normal form of a formula 'fm'  *)
   1.233 -(*                      of propositional logic (i.e. only variables may be   *)
   1.234 -(*                      negated, but not subformulas)                        *)
   1.235 -(* ------------------------------------------------------------------------- *)
   1.236 -
   1.237 -	(* prop_formula -> prop_formula *)
   1.238 -
   1.239 -	fun prop_formula_to_nnf fm =
   1.240 -		case fm of
   1.241 -		(* constants *)
   1.242 -		  True                => True
   1.243 -		| False               => False
   1.244 -		(* literals *)
   1.245 -		| BoolVar i           => BoolVar i
   1.246 -		| Not (BoolVar i)     => Not (BoolVar i)
   1.247 -		(* double-negation elimination *)
   1.248 -		| Not (Not fm)        => prop_formula_to_nnf fm
   1.249 -		(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
   1.250 -		| Not (Or  (fm1,fm2)) => SAnd (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
   1.251 -		| Not (And (fm1,fm2)) => SOr  (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
   1.252 -		(* 'or' and 'and' as outermost connectives are left untouched *)
   1.253 -		| Or  (fm1,fm2)       => SOr  (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
   1.254 -		| And (fm1,fm2)       => SAnd (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
   1.255 -		(* 'not' + constant *)
   1.256 -		| Not _               => raise REFUTE ("prop_formula_to_nnf", "'True'/'False' not allowed inside of 'Not'");
   1.257 -
   1.258 -(* ------------------------------------------------------------------------- *)
   1.259 -(* prop_formula_nnf_to_cnf: computes the conjunctive normal form of a        *)
   1.260 -(*      formula 'fm' of propositional logic that is given in negation normal *)
   1.261 -(*      form.  Note that there may occur an exponential blowup of the        *)
   1.262 -(*      formula.                                                             *)
   1.263 -(* ------------------------------------------------------------------------- *)
   1.264 -
   1.265 -	(* prop_formula -> prop_formula *)
   1.266 -
   1.267 -	fun prop_formula_nnf_to_cnf fm =
   1.268 -		case fm of
   1.269 -		(* constants *)
   1.270 -		  True            => True
   1.271 -		| False           => False
   1.272 -		(* literals *)
   1.273 -		| BoolVar i       => BoolVar i
   1.274 -		| Not (BoolVar i) => Not (BoolVar i)
   1.275 -		(* pushing 'or' inside of 'and' using distributive laws *)
   1.276 -		| Or (fm1,fm2)    =>
   1.277 -			let
   1.278 -				val fm1' = prop_formula_nnf_to_cnf fm1
   1.279 -				val fm2' = prop_formula_nnf_to_cnf fm2
   1.280 -			in
   1.281 -				case fm1' of
   1.282 -				  And (fm11,fm12) => prop_formula_nnf_to_cnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
   1.283 -				| _               =>
   1.284 -					(case fm2' of
   1.285 -					  And (fm21,fm22) => prop_formula_nnf_to_cnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
   1.286 -					(* neither subformula contains 'and' *)
   1.287 -					| _               => fm)
   1.288 -			end
   1.289 -		(* 'and' as outermost connective is left untouched *)
   1.290 -		| And (fm1,fm2)   => SAnd (prop_formula_nnf_to_cnf fm1, prop_formula_nnf_to_cnf fm2)
   1.291 -		(* error *)
   1.292 -		| _               => raise REFUTE ("prop_formula_nnf_to_cnf", "formula is not in negation normal form");
   1.293 -
   1.294 -(* ------------------------------------------------------------------------- *)
   1.295 -(* max: computes the maximum of two integer values 'i' and 'j'               *)
   1.296 -(* ------------------------------------------------------------------------- *)
   1.297 -
   1.298 -	(* int * int -> int *)
   1.299 -
   1.300 -	fun max (i,j) =
   1.301 -		if (i>j) then i else j;
   1.302 -
   1.303 -(* ------------------------------------------------------------------------- *)
   1.304 -(* max_var_index: computes the maximal variable index occuring in 'fm',      *)
   1.305 -(*      where 'fm' is a formula of propositional logic                       *)
   1.306 -(* ------------------------------------------------------------------------- *)
   1.307 -
   1.308 -	(* prop_formula -> int *)
   1.309 -
   1.310 -	fun max_var_index fm =
   1.311 -		case fm of
   1.312 -		  True          => 0
   1.313 -		| False         => 0
   1.314 -		| BoolVar i     => i
   1.315 -		| Not fm1       => max_var_index fm1
   1.316 -		| And (fm1,fm2) => max (max_var_index fm1, max_var_index fm2)
   1.317 -		| Or (fm1,fm2)  => max (max_var_index fm1, max_var_index fm2);
   1.318 -
   1.319 -(* ------------------------------------------------------------------------- *)
   1.320 -(* prop_formula_nnf_to_def_cnf: computes the definitional conjunctive normal *)
   1.321 -(*      form of a formula 'fm' of propositional logic that is given in       *)
   1.322 -(*      negation normal form.  To avoid an exponential blowup of the         *)
   1.323 -(*      formula, auxiliary variables may be introduced.  The result formula  *)
   1.324 -(*      is SAT-equivalent to 'fm' (i.e. it is satisfiable if and only if     *)
   1.325 -(*      'fm' is satisfiable).                                                *)
   1.326 +(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
   1.327  (* ------------------------------------------------------------------------- *)
   1.328  
   1.329 -	(* prop_formula -> prop_formula *)
   1.330 -
   1.331 -	fun prop_formula_nnf_to_def_cnf fm =
   1.332 -	let
   1.333 -		(* prop_formula * int -> prop_formula * int *)
   1.334 -		fun prop_formula_nnf_to_def_cnf_new (fm,new) =
   1.335 -		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   1.336 -			case fm of
   1.337 -			(* constants *)
   1.338 -			  True            => (True, new)
   1.339 -			| False           => (False, new)
   1.340 -			(* literals *)
   1.341 -			| BoolVar i       => (BoolVar i, new)
   1.342 -			| Not (BoolVar i) => (Not (BoolVar i), new)
   1.343 -			(* pushing 'or' inside of 'and' using distributive laws *)
   1.344 -			| Or (fm1,fm2)    =>
   1.345 -				let
   1.346 -					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
   1.347 -					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
   1.348 -				in
   1.349 -					case fst fm1' of
   1.350 -					  And (fm11,fm12) =>
   1.351 -						let
   1.352 -							val aux = BoolVar (snd fm2')
   1.353 -						in
   1.354 -							(* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
   1.355 -							prop_formula_nnf_to_def_cnf_new (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fst fm2', Not aux)), (snd fm2')+1)
   1.356 -						end
   1.357 -					| _               =>
   1.358 -						(case fst fm2' of
   1.359 -						  And (fm21,fm22) =>
   1.360 -							let
   1.361 -								val aux = BoolVar (snd fm2')
   1.362 -							in
   1.363 -								(* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
   1.364 -								prop_formula_nnf_to_def_cnf_new (SAnd (SOr (fst fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), (snd fm2')+1)
   1.365 -							end
   1.366 -						(* neither subformula contains 'and' *)
   1.367 -						| _               => (fm, new))
   1.368 -				end
   1.369 -			(* 'and' as outermost connective is left untouched *)
   1.370 -			| And (fm1,fm2)   =>
   1.371 -				let
   1.372 -					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
   1.373 -					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
   1.374 -				in
   1.375 -					(SAnd (fst fm1', fst fm2'), snd fm2')
   1.376 -				end
   1.377 -			(* error *)
   1.378 -			| _               => raise REFUTE ("prop_formula_nnf_to_def_cnf", "formula is not in negation normal form")
   1.379 -	in
   1.380 -		fst (prop_formula_nnf_to_def_cnf_new (fm, (max_var_index fm)+1))
   1.381 -	end;
   1.382 -
   1.383 -(* ------------------------------------------------------------------------- *)
   1.384 -(* prop_formula_to_cnf: computes the conjunctive normal form of a formula    *)
   1.385 -(*                      'fm' of propositional logic                          *)
   1.386 -(* ------------------------------------------------------------------------- *)
   1.387 -
   1.388 -	(* prop_formula -> prop_formula *)
   1.389 -
   1.390 -	fun prop_formula_to_cnf fm =
   1.391 -		prop_formula_nnf_to_cnf (prop_formula_to_nnf fm);
   1.392 -
   1.393 -(* ------------------------------------------------------------------------- *)
   1.394 -(* prop_formula_to_def_cnf: computes the definitional conjunctive normal     *)
   1.395 -(*      form of a formula 'fm' of propositional logic, introducing auxiliary *)
   1.396 -(*      variables if necessary to avoid an exponential blowup of the formula *)
   1.397 -(* ------------------------------------------------------------------------- *)
   1.398 -
   1.399 -	(* prop_formula -> prop_formula *)
   1.400 -
   1.401 -	fun prop_formula_to_def_cnf fm =
   1.402 -		prop_formula_nnf_to_def_cnf (prop_formula_to_nnf fm);
   1.403 -
   1.404 -(* ------------------------------------------------------------------------- *)
   1.405 -(* prop_formula_to_dimacs_cnf_format: serializes a formula of propositional  *)
   1.406 -(*      logic to a file in DIMACS CNF format (see "Satisfiability Suggested  *)
   1.407 -(*      Format", May 8 1993, Section 2.1)                                    *)
   1.408 -(* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
   1.409 -(*       index less than 1.                                                  *)
   1.410 -(* def : If true, translate 'fm' into definitional CNF.  Otherwise translate *)
   1.411 -(*       'fm' into CNF.                                                      *)
   1.412 -(* path: path of the file to be created                                      *)
   1.413 -(* ------------------------------------------------------------------------- *)
   1.414 -
   1.415 -	(* prop_formula -> bool -> Path.T -> unit *)
   1.416 -
   1.417 -	fun prop_formula_to_dimacs_cnf_format fm def path =
   1.418 -	let
   1.419 -		(* prop_formula *)
   1.420 -		val cnf =
   1.421 -			if def then
   1.422 -				prop_formula_to_def_cnf fm
   1.423 -			else
   1.424 -				prop_formula_to_cnf fm
   1.425 -		val fm' =
   1.426 -			case cnf of
   1.427 -			  True  => Or (BoolVar 1, Not (BoolVar 1))
   1.428 -			| False => And (BoolVar 1, Not (BoolVar 1))
   1.429 -			| _     => cnf (* either 'cnf'=True/False, or 'cnf' does not contain True/False at all *)
   1.430 -		(* prop_formula -> int *)
   1.431 -		fun cnf_number_of_clauses (And (fm1,fm2)) =
   1.432 -			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
   1.433 -		  | cnf_number_of_clauses _ =
   1.434 -			1
   1.435 -		(* prop_formula -> string *)
   1.436 -		fun cnf_prop_formula_to_string (BoolVar i) =
   1.437 -			if (i<1) then
   1.438 -				raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains a variable index less than 1")
   1.439 -			else
   1.440 -				(string_of_int i)
   1.441 -		  | cnf_prop_formula_to_string (Not fm1) =
   1.442 -			"-" ^ (cnf_prop_formula_to_string fm1)
   1.443 -		  | cnf_prop_formula_to_string (Or (fm1,fm2)) =
   1.444 -			(cnf_prop_formula_to_string fm1) ^ " " ^ (cnf_prop_formula_to_string fm2)
   1.445 -		  | cnf_prop_formula_to_string (And (fm1,fm2)) =
   1.446 -			(cnf_prop_formula_to_string fm1) ^ " 0\n" ^ (cnf_prop_formula_to_string fm2)
   1.447 -		  | cnf_prop_formula_to_string _ =
   1.448 -			raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains True/False")
   1.449 -	in
   1.450 -		File.write path ("c This file was generated by prop_formula_to_dimacs_cnf_format\n"
   1.451 -			^ "c (c) Tjark Weber\n"
   1.452 -			^ "p cnf " ^ (string_of_int (max_var_index fm')) ^ " " ^ (string_of_int (cnf_number_of_clauses fm')) ^ "\n"
   1.453 -			^ (cnf_prop_formula_to_string fm') ^ "\n")
   1.454 -	end;
   1.455 -
   1.456 -(* ------------------------------------------------------------------------- *)
   1.457 -(* prop_formula_to_dimacs_sat_format: serializes a formula of propositional  *)
   1.458 -(*      logic to a file in DIMACS SAT format (see "Satisfiability Suggested  *)
   1.459 -(*      Format", May 8 1993, Section 2.2)                                    *)
   1.460 -(* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
   1.461 -(*       index less than 1.                                                  *)
   1.462 -(* path: path of the file to be created                                      *)
   1.463 -(* ------------------------------------------------------------------------- *)
   1.464 -
   1.465 -	(* prop_formula -> Path.T -> unit *)
   1.466 -
   1.467 -	fun prop_formula_to_dimacs_sat_format fm path =
   1.468 -	let
   1.469 -		fun prop_formula_to_string True =
   1.470 -			"*()"
   1.471 -		  | prop_formula_to_string False =
   1.472 -			"+()"
   1.473 -		  | prop_formula_to_string (BoolVar i) =
   1.474 -			if (i<1) then
   1.475 -				raise REFUTE ("prop_formula_to_dimacs_sat_format", "formula contains a variable index less than 1")
   1.476 -			else
   1.477 -				(string_of_int i)
   1.478 -		  | prop_formula_to_string (Not fm1) =
   1.479 -			"-(" ^ (prop_formula_to_string fm1) ^ ")"
   1.480 -		  | prop_formula_to_string (Or (fm1,fm2)) =
   1.481 -			"+(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
   1.482 -		  | prop_formula_to_string (And (fm1,fm2)) =
   1.483 -			"*(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
   1.484 -	in
   1.485 -		File.write path ("c This file was generated by prop_formula_to_dimacs_sat_format\n"
   1.486 -			^ "c (c) Tjark Weber\n"
   1.487 -			^ "p sat " ^ (string_of_int (max (max_var_index fm, 1))) ^ "\n"
   1.488 -			^ "(" ^ (prop_formula_to_string fm) ^ ")\n")
   1.489 -	end;
   1.490 -
   1.491 -(* ------------------------------------------------------------------------- *)
   1.492 -(* prop_formula_sat_solver: try to find a satisfying assignment for the      *)
   1.493 -(*      boolean variables in a propositional formula, using an external SAT  *)
   1.494 -(*      solver.  If the SAT solver did not find an assignment, 'None' is     *)
   1.495 -(*      returned.  Otherwise 'Some (list of integers)' is returned, where    *)
   1.496 -(*      i>0 means that the boolean variable i is set to TRUE, and i<0 means  *)
   1.497 -(*      that the boolean variable i is set to FALSE.  Note that if           *)
   1.498 -(*      'satformat' is 'defcnf', then the assignment returned may contain    *)
   1.499 -(*      auxiliary variables that were not present in the original formula    *)
   1.500 -(*      'fm'.                                                                *)
   1.501 -(* fm        : formula that is passed to the SAT solver                      *) 
   1.502 -(* satpath   : path of the file used to store the propositional formula,     *)
   1.503 -(*             i.e. the input to the SAT solver                              *)
   1.504 -(* satformat : format of the SAT solver's input file.  Must be either "cnf", *)
   1.505 -(*             "defcnf", or "sat".                                           *)
   1.506 -(* resultpath: path of the file containing the SAT solver's output           *)
   1.507 -(* success   : part of the line in the SAT solver's output that is followed  *)
   1.508 -(*             by a line consisting of a list of integers representing the   *)
   1.509 -(*             satisfying assignment                                         *)
   1.510 -(* command   : system command used to execute the SAT solver                 *)
   1.511 -(* ------------------------------------------------------------------------- *)
   1.512 -
   1.513 -	(* prop_formula -> Path.T -> string -> Path.T -> string -> string -> int list option *)
   1.514 -
   1.515 -	fun prop_formula_sat_solver fm satpath satformat resultpath success command =
   1.516 -		if File.exists satpath then
   1.517 -			error ("file '" ^ (Path.pack satpath) ^ "' exists, please delete (will not overwrite)")
   1.518 -		else if File.exists resultpath then
   1.519 -			error ("file '" ^ (Path.pack resultpath) ^ "' exists, please delete (will not overwrite)")
   1.520 -		else
   1.521 -		(
   1.522 -			(* serialize the formula 'fm' to a file *)
   1.523 -			if satformat="cnf" then
   1.524 -				prop_formula_to_dimacs_cnf_format fm false satpath
   1.525 -			else if satformat="defcnf" then
   1.526 -				prop_formula_to_dimacs_cnf_format fm true satpath
   1.527 -			else if satformat="sat" then
   1.528 -				prop_formula_to_dimacs_sat_format fm satpath
   1.529 -			else
   1.530 -				error ("invalid argument: satformat='" ^ satformat ^ "' (must be either 'cnf', 'defcnf', or 'sat')");
   1.531 -			(* execute SAT solver *)
   1.532 -			if (system command)<>0 then
   1.533 -			(
   1.534 -				(* error executing SAT solver *)
   1.535 -				File.rm satpath;
   1.536 -				File.rm resultpath;
   1.537 -				error ("system command '" ^ command ^ "' failed (make sure a SAT solver is installed)")
   1.538 -			)
   1.539 -			else
   1.540 -			(
   1.541 -				(* read assignment from the result file *)
   1.542 -				File.rm satpath;
   1.543 -				let
   1.544 -					(* 'a option -> 'a Library.option *)
   1.545 -					fun option (SOME a) =
   1.546 -						Some a
   1.547 -					  | option NONE =
   1.548 -						None
   1.549 -					(* string -> int list *)
   1.550 -					fun string_to_int_list s =
   1.551 -						mapfilter (option o Int.fromString) (space_explode " " s)
   1.552 -					(* string -> string -> bool *)
   1.553 -					fun is_substring s1 s2 =
   1.554 -					let
   1.555 -						val length1 = String.size s1
   1.556 -						val length2 = String.size s2
   1.557 -					in
   1.558 -						if length2 < length1 then
   1.559 -							false
   1.560 -						else if s1 = String.substring (s2, 0, length1) then
   1.561 -							true
   1.562 -						else is_substring s1 (String.substring (s2, 1, length2-1))
   1.563 -					end
   1.564 -					(* string list -> int list option *)
   1.565 -					fun extract_solution [] =
   1.566 -						None
   1.567 -					  | extract_solution (line::lines) =
   1.568 -						if is_substring success line then
   1.569 -							(* the next line must be a list of integers *)
   1.570 -							Some (string_to_int_list (hd lines))
   1.571 -						else
   1.572 -							extract_solution lines
   1.573 -					val sat_result = File.read resultpath
   1.574 -				in
   1.575 -					File.rm resultpath;
   1.576 -					extract_solution (split_lines sat_result)
   1.577 -				end
   1.578 -			)
   1.579 -		);
   1.580 -
   1.581 +	exception CANNOT_INTERPRET;
   1.582  
   1.583  (* ------------------------------------------------------------------------- *)
   1.584  (* TREES                                                                     *)
   1.585 @@ -537,9 +88,6 @@
   1.586  		  Leaf of 'a
   1.587  		| Node of ('a tree) list;
   1.588  
   1.589 -	type prop_tree =
   1.590 -		prop_formula list tree;
   1.591 -
   1.592  	(* ('a -> 'b) -> 'a tree -> 'b tree *)
   1.593  
   1.594  	fun tree_map f tr =
   1.595 @@ -571,45 +119,95 @@
   1.596  				  Node ys => Node (map tree_pair (xs ~~ ys))
   1.597  				| Leaf _  => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
   1.598  
   1.599 +
   1.600  (* ------------------------------------------------------------------------- *)
   1.601 -(* prop_tree_to_true: returns a propositional formula that is true iff the   *)
   1.602 -(*      tree denotes the boolean value TRUE                                  *)
   1.603 +(* interpretation: a term's interpretation is given by a variable of type    *)
   1.604 +(*                 'interpretation'                                          *)
   1.605  (* ------------------------------------------------------------------------- *)
   1.606  
   1.607 -	(* prop_tree -> prop_formula *)
   1.608 -
   1.609 -	(* a term of type 'bool' is represented as a 2-element leaf, where *)
   1.610 -	(* the term is true iff the leaf's first element is true           *)
   1.611 -
   1.612 -	fun prop_tree_to_true (Leaf [fm,_]) =
   1.613 -		fm
   1.614 -	  | prop_tree_to_true _ =
   1.615 -		raise REFUTE ("prop_tree_to_true", "tree is not a 2-element leaf");
   1.616 +	type interpretation =
   1.617 +		prop_formula list tree;
   1.618  
   1.619  (* ------------------------------------------------------------------------- *)
   1.620 -(* prop_tree_to_false: returns a propositional formula that is true iff the  *)
   1.621 -(*      tree denotes the boolean value FALSE                                 *)
   1.622 +(* model: a model specifies the size of types and the interpretation of      *)
   1.623 +(*        terms                                                              *)
   1.624  (* ------------------------------------------------------------------------- *)
   1.625  
   1.626 -	(* prop_tree -> prop_formula *)
   1.627 +	type model =
   1.628 +		(Term.typ * int) list * (Term.term * interpretation) list;
   1.629  
   1.630 -	(* a term of type 'bool' is represented as a 2-element leaf, where *)
   1.631 -	(* the term is false iff the leaf's second element is true         *)
   1.632 +(* ------------------------------------------------------------------------- *)
   1.633 +(* arguments: additional arguments required during interpretation of terms   *)
   1.634 +(* ------------------------------------------------------------------------- *)
   1.635 +	
   1.636 +	type arguments =
   1.637 +		{next_idx: int, bounds: interpretation list, wellformed: prop_formula};
   1.638 +
   1.639  
   1.640 -	fun prop_tree_to_false (Leaf [_,fm]) =
   1.641 -		fm
   1.642 -	  | prop_tree_to_false _ =
   1.643 -		raise REFUTE ("prop_tree_to_false", "tree is not a 2-element leaf");
   1.644 +	structure RefuteDataArgs =
   1.645 +	struct
   1.646 +		val name = "HOL/refute";
   1.647 +		type T =
   1.648 +			{interpreters: (string * (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option)) list,
   1.649 +			 printers: (string * (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option)) list,
   1.650 +			 parameters: string Symtab.table};
   1.651 +		val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
   1.652 +		val copy = I;
   1.653 +		val prep_ext = I;
   1.654 +		fun merge
   1.655 +			({interpreters = in1, printers = pr1, parameters = pa1},
   1.656 +			 {interpreters = in2, printers = pr2, parameters = pa2}) =
   1.657 +			{interpreters = rev (merge_alists (rev in1) (rev in2)),
   1.658 +			 printers = rev (merge_alists (rev pr1) (rev pr2)),
   1.659 +			 parameters = Symtab.merge (op=) (pa1, pa2)};
   1.660 +		fun print sg {interpreters, printers, parameters} =
   1.661 +			Pretty.writeln (Pretty.chunks
   1.662 +				[Pretty.strs ("default parameters:" :: flat (map (fn (name,value) => [name, "=", value]) (Symtab.dest parameters))),
   1.663 +				 Pretty.strs ("interpreters:" :: map fst interpreters),
   1.664 +				 Pretty.strs ("printers:" :: map fst printers)]);
   1.665 +	end;
   1.666 +
   1.667 +	structure RefuteData = TheoryDataFun(RefuteDataArgs);
   1.668 +
   1.669  
   1.670  (* ------------------------------------------------------------------------- *)
   1.671 -(* restrict_to_single_element: returns a propositional formula which is true *)
   1.672 -(*      iff the tree 'tr' describes a single element of its corresponding    *)
   1.673 -(*      type, i.e. iff at each leaf, one and only one formula is true        *)
   1.674 +(* interpret: tries to interpret the term 't' using a suitable interpreter;  *)
   1.675 +(*            returns the interpretation and a (possibly extended) model     *)
   1.676 +(*            that keeps track of the interpretation of subterms             *)
   1.677 +(* Note: exception 'CANNOT_INTERPRETE' is raised if the term cannot be       *)
   1.678 +(*       interpreted by any interpreter                                      *)
   1.679  (* ------------------------------------------------------------------------- *)
   1.680  
   1.681 -	(* prop_tree -> prop_formula *)
   1.682 +	(* theory -> model -> arguments -> Term.term -> interpretation * model * arguments *)
   1.683 +
   1.684 +	fun interpret thy model args t =
   1.685 +		(case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of
   1.686 +		  None =>
   1.687 +			(std_output "\n"; warning ("Unable to interpret term:\n" ^ Sign.string_of_term (sign_of thy) t);
   1.688 +			raise CANNOT_INTERPRET)
   1.689 +		| Some x => x);
   1.690 +
   1.691 +(* ------------------------------------------------------------------------- *)
   1.692 +(* print: tries to print the constant denoted by the term 't' using a        *)
   1.693 +(*        suitable printer                                                   *)
   1.694 +(* ------------------------------------------------------------------------- *)
   1.695  
   1.696 -	fun restrict_to_single_element tr =
   1.697 +	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string *)
   1.698 +
   1.699 +	fun print thy model t intr assignment =
   1.700 +		(case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of
   1.701 +		  None => "<<no printer available>>"
   1.702 +		| Some s => s);
   1.703 +
   1.704 +(* ------------------------------------------------------------------------- *)
   1.705 +(* is_satisfying_model: returns a propositional formula that is true iff the *)
   1.706 +(*      given interpretation denotes 'satisfy', and the model meets certain  *)
   1.707 +(*      well-formedness properties                                           *)
   1.708 +(* ------------------------------------------------------------------------- *)
   1.709 +
   1.710 +	(* model -> interpretation -> bool -> PropLogic.prop_formula *)
   1.711 +
   1.712 +	fun is_satisfying_model model intr satisfy =
   1.713  	let
   1.714  		(* prop_formula list -> prop_formula *)
   1.715  		fun allfalse []      = True
   1.716 @@ -617,290 +215,1347 @@
   1.717  		(* prop_formula list -> prop_formula *)
   1.718  		fun exactly1true []      = False
   1.719  		  | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
   1.720 +	(* ------------------------------------------------------------------------- *)
   1.721 +	(* restrict_to_single_element: returns a propositional formula that is true  *)
   1.722 +	(*      iff the interpretation denotes a single element of its corresponding *)
   1.723 +	(*      type, i.e. iff at each leaf, one and only one formula is true        *)
   1.724 +	(* ------------------------------------------------------------------------- *)
   1.725 +		(* interpretation -> prop_formula *)
   1.726 +		fun restrict_to_single_element (Leaf [BoolVar i, Not (BoolVar j)]) =
   1.727 +			if (i=j) then
   1.728 +				True  (* optimization for boolean variables *)
   1.729 +			else
   1.730 +				raise REFUTE ("is_satisfying_model", "boolean variables in leaf have different indices")
   1.731 +		  | restrict_to_single_element (Leaf xs) =
   1.732 +			exactly1true xs
   1.733 +		  | restrict_to_single_element (Node trees) =
   1.734 +			PropLogic.all (map restrict_to_single_element trees)
   1.735  	in
   1.736 -		case tr of
   1.737 -		  Leaf [BoolVar _, Not (BoolVar _)] => True (* optimization for boolean variables *)
   1.738 -		| Leaf xs                           => exactly1true xs
   1.739 -		| Node trees                        => list_conjunction (map restrict_to_single_element trees)
   1.740 +		(* a term of type 'bool' is represented as a 2-element leaf, where  *)
   1.741 +		(* the term is true iff the leaf's first element is true, and false *)
   1.742 +		(* iff the leaf's second element is true                            *)
   1.743 +		case intr of
   1.744 +		  Leaf [fmT,fmF] =>
   1.745 +			(* well-formedness properties and formula 'fmT'/'fmF' *)
   1.746 +			SAnd (PropLogic.all (map (restrict_to_single_element o snd) (snd model)), if satisfy then fmT else fmF)
   1.747 +		| _ =>
   1.748 +			raise REFUTE ("is_satisfying_model", "interpretation does not denote a boolean value")
   1.749 +	end;
   1.750 +
   1.751 +(* ------------------------------------------------------------------------- *)
   1.752 +(* print_model: turns the model into a string, using a fixed interpretation  *)
   1.753 +(*              (given by an assignment for boolean variables) and suitable  *)
   1.754 +(*              printers                                                     *)
   1.755 +(* ------------------------------------------------------------------------- *)
   1.756 +
   1.757 +	fun print_model thy model assignment =
   1.758 +	let
   1.759 +		val (typs, terms) = model
   1.760 +	in
   1.761 +		(if null typs then
   1.762 +			"empty universe (no type variables in term)"
   1.763 +		else
   1.764 +			"Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs))
   1.765 +		^ "\n"
   1.766 +		^ (if null terms then
   1.767 +			"empty interpretation (no free variables in term)"
   1.768 +		  else
   1.769 +			space_implode "\n" (map
   1.770 +				(fn (t,intr) =>
   1.771 +					Sign.string_of_term (sign_of thy) t ^ ": " ^ print thy model t intr assignment)
   1.772 +				terms)
   1.773 +		  )
   1.774 +		^ "\n"
   1.775 +	end;
   1.776 +
   1.777 +
   1.778 +(* ------------------------------------------------------------------------- *)
   1.779 +(* PARAMETER MANAGEMENT                                                      *)
   1.780 +(* ------------------------------------------------------------------------- *)
   1.781 +
   1.782 +	(* string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory *)
   1.783 +
   1.784 +	fun add_interpreter name f thy =
   1.785 +	let
   1.786 +		val {interpreters, printers, parameters} = RefuteData.get thy
   1.787 +	in
   1.788 +		case assoc (interpreters, name) of
   1.789 +		  None   => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy
   1.790 +		| Some _ => error ("Interpreter " ^ name ^ " already declared")
   1.791 +	end;
   1.792 +
   1.793 +	(* string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory *)
   1.794 +
   1.795 +	fun add_printer name f thy =
   1.796 +	let
   1.797 +		val {interpreters, printers, parameters} = RefuteData.get thy
   1.798 +	in
   1.799 +		case assoc (printers, name) of
   1.800 +		  None   => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy
   1.801 +		| Some _ => error ("Printer " ^ name ^ " already declared")
   1.802 +	end;
   1.803 +
   1.804 +(* ------------------------------------------------------------------------- *)
   1.805 +(* set_default_param: stores the '(name, value)' pair in RefuteData's        *)
   1.806 +(*                    parameter table                                        *)
   1.807 +(* ------------------------------------------------------------------------- *)
   1.808 +
   1.809 +	(* (string * string) -> theory -> theory *)
   1.810 +
   1.811 +	fun set_default_param (name, value) thy =
   1.812 +	let
   1.813 +		val {interpreters, printers, parameters} = RefuteData.get thy
   1.814 +	in
   1.815 +		case Symtab.lookup (parameters, name) of
   1.816 +		  None   => RefuteData.put
   1.817 +			{interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy
   1.818 +		| Some _ => RefuteData.put
   1.819 +			{interpreters = interpreters, printers = printers, parameters = Symtab.update ((name, value), parameters)} thy
   1.820  	end;
   1.821  
   1.822  (* ------------------------------------------------------------------------- *)
   1.823 -(* HOL FORMULAS                                                              *)
   1.824 +(* get_default_param: retrieves the value associated with 'name' from        *)
   1.825 +(*                    RefuteData's parameter table                           *)
   1.826 +(* ------------------------------------------------------------------------- *)
   1.827 +
   1.828 +	(* theory -> string -> string option *)
   1.829 +
   1.830 +	fun get_default_param thy name = Symtab.lookup ((#parameters o RefuteData.get) thy, name);
   1.831 +
   1.832 +(* ------------------------------------------------------------------------- *)
   1.833 +(* get_default_params: returns a list of all '(name, value)' pairs that are  *)
   1.834 +(*                     stored in RefuteData's parameter table                *)
   1.835 +(* ------------------------------------------------------------------------- *)
   1.836 +
   1.837 +	(* theory -> (string * string) list *)
   1.838 +
   1.839 +	fun get_default_params thy = (Symtab.dest o #parameters o RefuteData.get) thy;
   1.840 +
   1.841 +(* ------------------------------------------------------------------------- *)
   1.842 +(* actual_params: takes a (possibly empty) list 'params' of parameters that  *)
   1.843 +(*      override the default parameters currently specified in 'thy', and    *)
   1.844 +(*      returns a tuple that can be passed to 'find_model'.                  *)
   1.845 +(*                                                                           *)
   1.846 +(* The following parameters are supported (and required!):                   *)
   1.847 +(*                                                                           *)
   1.848 +(* Name          Type    Description                                         *)
   1.849 +(*                                                                           *)
   1.850 +(* "minsize"     int     Only search for models with size at least           *)
   1.851 +(*                       'minsize'.                                          *)
   1.852 +(* "maxsize"     int     If >0, only search for models with size at most     *)
   1.853 +(*                       'maxsize'.                                          *)
   1.854 +(* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
   1.855 +(*                       when transforming the term into a propositional     *)
   1.856 +(*                       formula.                                            *)
   1.857 +(* "satsolver"   string  SAT solver to be used.                              *)
   1.858 +(* ------------------------------------------------------------------------- *)
   1.859 +
   1.860 +	(* theory -> (string * string) list -> (int * int * int * string) *)
   1.861 +
   1.862 +	fun actual_params thy params =
   1.863 +	let
   1.864 +		(* (string * string) list * string -> int *)
   1.865 +		fun read_int (parms, name) =
   1.866 +			case assoc_string (parms, name) of
   1.867 +			  Some s => (case Int.fromString s of
   1.868 +				  SOME i => i
   1.869 +				| NONE   => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value"))
   1.870 +			| None   => error ("parameter " ^ quote name ^ " must be assigned a value")
   1.871 +		(* (string * string) list * string -> string *)
   1.872 +		fun read_string (parms, name) =
   1.873 +			case assoc_string (parms, name) of
   1.874 +			  Some s => s
   1.875 +			| None   => error ("parameter " ^ quote name ^ " must be assigned a value")
   1.876 +		(* (string * string) list *)
   1.877 +		val allparams = params @ (get_default_params thy)  (* 'params' first, defaults last (to override) *)
   1.878 +		(* int *)
   1.879 +		val minsize   = read_int (allparams, "minsize")
   1.880 +		val maxsize   = read_int (allparams, "maxsize")
   1.881 +		val maxvars   = read_int (allparams, "maxvars")
   1.882 +		(* string *)
   1.883 +		val satsolver = read_string (allparams, "satsolver")
   1.884 +	in
   1.885 +		(minsize, maxsize, maxvars, satsolver)
   1.886 +	end;
   1.887 +
   1.888 +(* ------------------------------------------------------------------------- *)
   1.889 +(* find_model: repeatedly calls 'invoke_propgen' with appropriate            *)
   1.890 +(*             parameters, applies the SAT solver, and (in case a model is   *)
   1.891 +(*             found) displays the model to the user                         *)
   1.892 +(* thy      : the current theory                                             *)
   1.893 +(* minsize  : the minimal size of the model                                  *)
   1.894 +(* maxsize  : the maximal size of the model                                  *)
   1.895 +(* maxvars  : the maximal number of boolean variables to be used             *)
   1.896 +(* satsolver: the name of the SAT solver to be used                          *)
   1.897 +(* satisfy  : if 'True', search for a model that makes 't' true; otherwise   *)
   1.898 +(*            search for a model that makes 't' false                        *)
   1.899 +(* ------------------------------------------------------------------------- *)
   1.900 +
   1.901 +	(* theory ->  (int * int * int * string) -> Term.term -> bool -> unit *)
   1.902 +
   1.903 +	fun find_model thy (minsize, maxsize, maxvars, satsolver) t satisfy =
   1.904 +	let
   1.905 +		(* Term.typ list *)
   1.906 +		val tvars  = map (fn (i,s) => TVar(i,s)) (term_tvars t)
   1.907 +		val tfrees = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
   1.908 +		(* int -> unit *)
   1.909 +		fun find_model_loop size =
   1.910 +			(* 'maxsize=0' means "search for arbitrary large models" *)
   1.911 +			if size>maxsize andalso maxsize<>0 then
   1.912 +				writeln ("Search terminated: maxsize=" ^ string_of_int maxsize ^ " exceeded.")
   1.913 +			else
   1.914 +			let
   1.915 +				(* ------------------------------------------------------------------------- *)
   1.916 +				(* make_universes: given a list 'xs' of "types" and a universe size 'size',  *)
   1.917 +				(*      this function returns all possible partitions of the universe into   *)
   1.918 +				(*      the "types" in 'xs' such that no "type" is empty.  If 'size' is less *)
   1.919 +				(*      than 'length xs', the returned list of partitions is empty.          *)
   1.920 +				(*      Otherwise, if the list 'xs' is empty, then the returned list of      *)
   1.921 +				(*      partitions contains only the empty list, regardless of 'size'.       *)
   1.922 +				(* ------------------------------------------------------------------------- *)
   1.923 +				(* 'a list -> int -> ('a * int) list list *)
   1.924 +				fun make_universes xs size =
   1.925 +				let
   1.926 +					(* 'a list -> int -> int -> ('a * int) list list *)
   1.927 +					fun make_partitions_loop (x::xs) 0 total =
   1.928 +						map (fn us => ((x,0)::us)) (make_partitions xs total)
   1.929 +					  | make_partitions_loop (x::xs) first total =
   1.930 +						(map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
   1.931 +					  | make_partitions_loop _ _ _ =
   1.932 +						raise REFUTE ("find_model", "empty list (in make_partitions_loop)")
   1.933 +					and
   1.934 +					(* 'a list -> int -> ('a * int) list list *)
   1.935 +					make_partitions [x] size =
   1.936 +						(* we must use all remaining elements on the type 'x', so there is only one partition *)
   1.937 +						[[(x,size)]]
   1.938 +					  | make_partitions (x::xs) 0 =
   1.939 +						(* there are no elements left in the universe, so there is only one partition *)
   1.940 +						[map (fn t => (t,0)) (x::xs)]
   1.941 +					  | make_partitions (x::xs) size =
   1.942 +						(* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
   1.943 +						make_partitions_loop (x::xs) size size
   1.944 +					  | make_partitions _ _ =
   1.945 +						raise REFUTE ("find_model", "empty list (in make_partitions)")
   1.946 +					val len = length xs
   1.947 +				in
   1.948 +					if size<len then
   1.949 +						(* the universe isn't big enough to make every type non-empty *)
   1.950 +						[]
   1.951 +					else if xs=[] then
   1.952 +						(* no types: return one universe, regardless of the size *)
   1.953 +						[[]]
   1.954 +					else
   1.955 +						(* partition into possibly empty types, then add 1 element to each type *)
   1.956 +						map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
   1.957 +				end
   1.958 +				(* ('a * int) list -> bool *)
   1.959 +				fun find_interpretation xs =
   1.960 +				let
   1.961 +					val init_model          = (xs, [])
   1.962 +					val init_args           = {next_idx = 1, bounds = [], wellformed = True}
   1.963 +					val (intr, model, args) = interpret thy init_model init_args t
   1.964 +					val fm                  = SAnd (#wellformed args, is_satisfying_model model intr satisfy)
   1.965 +					val usedvars            = maxidx fm
   1.966 +				in
   1.967 +					(* 'maxvars=0' means "use as many variables as necessary" *)
   1.968 +					if usedvars>maxvars andalso maxvars<>0 then
   1.969 +						(writeln ("\nSearch terminated: " ^ string_of_int usedvars ^ " boolean variables used (only " ^ string_of_int maxvars ^ " allowed).");
   1.970 +						true)
   1.971 +					else
   1.972 +					(
   1.973 +						std_output " invoking SAT solver...";
   1.974 +						case SatSolver.invoke_solver satsolver fm of
   1.975 +						  None =>
   1.976 +							(std_output " no model found.\n";
   1.977 +							false)
   1.978 +						| Some assignment =>
   1.979 +							(writeln ("\nModel found:\n" ^ print_model thy model assignment);
   1.980 +							true)
   1.981 +					)
   1.982 +				end handle CANNOT_INTERPRET => true
   1.983 +					(* TODO: change this to false once the ability to interpret terms depends on the universe *)
   1.984 +			in
   1.985 +				case make_universes (tvars@tfrees) size of
   1.986 +				  [] =>
   1.987 +					(writeln ("Searching for a model of size " ^ string_of_int size ^ ": cannot make every type non-empty (model is too small).");
   1.988 +					find_model_loop (size+1))
   1.989 +				| [[]] =>
   1.990 +					(std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term...");
   1.991 +					if find_interpretation [] then
   1.992 +						()
   1.993 +					else
   1.994 +						writeln ("Search terminated: no type variables in term."))
   1.995 +				| us =>
   1.996 +					let
   1.997 +						fun loop []      =
   1.998 +							find_model_loop (size+1)
   1.999 +						  | loop (u::us) =
  1.1000 +							(std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term...");
  1.1001 +							if find_interpretation u then () else loop us)
  1.1002 +					in
  1.1003 +						loop us
  1.1004 +					end
  1.1005 +			end
  1.1006 +	in
  1.1007 +		writeln ("Trying to find a model that "
  1.1008 +			^ (if satisfy then "satisfies" else "refutes")
  1.1009 +			^ ": " ^ (Sign.string_of_term (sign_of thy) t));
  1.1010 +		if minsize<1 then
  1.1011 +			writeln "\"minsize\" is less than 1; starting search with size 1."
  1.1012 +		else ();
  1.1013 +		find_model_loop (Int.max (minsize,1))
  1.1014 +	end;
  1.1015 +
  1.1016 +
  1.1017 +(* ------------------------------------------------------------------------- *)
  1.1018 +(* INTERFACE, PART 2: FINDING A MODEL                                        *)
  1.1019  (* ------------------------------------------------------------------------- *)
  1.1020  
  1.1021  (* ------------------------------------------------------------------------- *)
  1.1022 -(* absvar: form an abstraction over a schematic variable                     *)
  1.1023 -(* ------------------------------------------------------------------------- *)
  1.1024 -
  1.1025 -	(* Term.indexname * Term.typ * Term.term -> Term.term *)
  1.1026 -
  1.1027 -	(* this function is similar to Term.absfree, but for schematic       *)
  1.1028 -	(* variables (rather than free variables)                            *)
  1.1029 -	fun absvar ((x,i),T,body) =
  1.1030 -		Abs(x, T, abstract_over (Var((x,i),T), body));
  1.1031 -
  1.1032 -(* ------------------------------------------------------------------------- *)
  1.1033 -(* list_all_var: quantification over a list of schematic variables           *)
  1.1034 +(* satisfy_term: calls 'find_model' to find a model that satisfies 't'       *)
  1.1035 +(* params      : list of '(name, value)' pairs used to override default      *)
  1.1036 +(*               parameters                                                  *)
  1.1037  (* ------------------------------------------------------------------------- *)
  1.1038  
  1.1039 -	(* (Term.indexname * Term.typ) list * Term.term -> Term.term *)
  1.1040 -
  1.1041 -	(* this function is similar to Term.list_all_free, but for schematic *)
  1.1042 -	(* variables (rather than free variables)                            *)
  1.1043 -	fun list_all_var ([], t) =
  1.1044 -		t
  1.1045 -	  | list_all_var ((idx,T)::vars, t) =
  1.1046 -		(all T) $ (absvar(idx, T, list_all_var(vars,t)));
  1.1047 +	(* theory -> (string * string) list -> Term.term -> unit *)
  1.1048  
  1.1049 -(* ------------------------------------------------------------------------- *)
  1.1050 -(* close_vars: close up a formula over all schematic variables by            *)
  1.1051 -(*             quantification (note that the result term may still contain   *)
  1.1052 -(*             (non-schematic) free variables)                               *)
  1.1053 -(* ------------------------------------------------------------------------- *)
  1.1054 -
  1.1055 -	(* Term.term -> Term.term *)
  1.1056 -
  1.1057 -	(* this function is similar to Logic.close_form, but for schematic   *)
  1.1058 -	(* variables (rather than free variables)                            *)
  1.1059 -	fun close_vars A =
  1.1060 -		list_all_var (sort_wrt (fst o fst) (map dest_Var (term_vars A)), A);
  1.1061 +	fun satisfy_term thy params t =
  1.1062 +		find_model thy (actual_params thy params) t true;
  1.1063  
  1.1064  (* ------------------------------------------------------------------------- *)
  1.1065 -(* make_universes: given a list 'xs' of "types" and a universe size 'size',  *)
  1.1066 -(*      this function returns all possible partitions of the universe into   *)
  1.1067 -(*      the "types" in 'xs' such that no "type" is empty.  If 'size' is less *)
  1.1068 -(*      than 'length xs', the returned list of partitions is empty.          *)
  1.1069 -(*      Otherwise, if the list 'xs' is empty, then the returned list of      *)
  1.1070 -(*      partitions contains only the empty list, regardless of 'size'.       *)
  1.1071 +(* refute_term: calls 'find_model' to find a model that refutes 't'          *)
  1.1072 +(* params     : list of '(name, value)' pairs used to override default       *)
  1.1073 +(*              parameters                                                   *)
  1.1074  (* ------------------------------------------------------------------------- *)
  1.1075  
  1.1076 -	(* 'a list -> int -> ('a * int) list list *)
  1.1077 +	(* theory -> (string * string) list -> Term.term -> unit *)
  1.1078  
  1.1079 -	fun make_universes xs size =
  1.1080 +	fun refute_term thy params t =
  1.1081  	let
  1.1082 -		(* 'a list -> int -> int -> ('a * int) list list *)
  1.1083 -		fun make_partitions_loop (x::xs) 0 total =
  1.1084 -			map (fn us => ((x,0)::us)) (make_partitions xs total)
  1.1085 -		  | make_partitions_loop (x::xs) first total =
  1.1086 -			(map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
  1.1087 -		  | make_partitions_loop _ _ _ =
  1.1088 -			raise REFUTE ("make_universes::make_partitions_loop", "empty list")
  1.1089 -		and
  1.1090 -		(* 'a list -> int -> ('a * int) list list *)
  1.1091 -		make_partitions [x] size =
  1.1092 -			(* we must use all remaining elements on the type 'x', so there is only one partition *)
  1.1093 -			[[(x,size)]]
  1.1094 -		  | make_partitions (x::xs) 0 =
  1.1095 -			(* there are no elements left in the universe, so there is only one partition *)
  1.1096 -			[map (fn t => (t,0)) (x::xs)]
  1.1097 -		  | make_partitions (x::xs) size =
  1.1098 -			(* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
  1.1099 -			make_partitions_loop (x::xs) size size
  1.1100 -		  | make_partitions _ _ =
  1.1101 -			raise REFUTE ("make_universes::make_partitions", "empty list")
  1.1102 -		val len = length xs
  1.1103 +		(* disallow schematic type variables, since we cannot properly negate terms containing them *)
  1.1104 +		val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables"
  1.1105 +		(* existential closure over schematic variables *)
  1.1106 +		(* (Term.indexname * Term.typ) list *)
  1.1107 +		val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
  1.1108 +		(* Term.term *)
  1.1109 +		val ex_closure = foldl
  1.1110 +			(fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
  1.1111 +			(t, vars)
  1.1112 +		(* If 't' is of type 'propT' (rather than 'boolT'), applying  *)
  1.1113 +		(* 'HOLogic.exists_const' is not type-correct.  However, this *)
  1.1114 +		(* isn't really a problem as long as 'find_model' still       *)
  1.1115 +		(* interprets the resulting term correctly, without checking  *)
  1.1116 +		(* its type.                                                  *)
  1.1117  	in
  1.1118 -		if size<len then
  1.1119 -			(* the universe isn't big enough to make every type non-empty *)
  1.1120 -			[]
  1.1121 -		else if xs=[] then
  1.1122 -			(* no types: return one universe, regardless of the size *)
  1.1123 -			[[]]
  1.1124 -		else
  1.1125 -			(* partition into possibly empty types, then add 1 element to each type *)
  1.1126 -			map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
  1.1127 +		find_model thy (actual_params thy params) ex_closure false
  1.1128  	end;
  1.1129  
  1.1130  (* ------------------------------------------------------------------------- *)
  1.1131 -(* sum: computes the sum of a list of integers; sum [] = 0                   *)
  1.1132 -(* ------------------------------------------------------------------------- *)
  1.1133 -
  1.1134 -	(* int list -> int *)
  1.1135 -
  1.1136 -	fun sum xs = foldl op+ (0, xs);
  1.1137 -
  1.1138 -(* ------------------------------------------------------------------------- *)
  1.1139 -(* product: computes the product of a list of integers; product [] = 1       *)
  1.1140 +(* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
  1.1141 +(* params        : list of '(name, value)' pairs used to override default    *)
  1.1142 +(*                 parameters                                                *)
  1.1143 +(* subgoal       : 0-based index specifying the subgoal number               *)
  1.1144  (* ------------------------------------------------------------------------- *)
  1.1145  
  1.1146 -	(* int list -> int *)
  1.1147 -
  1.1148 -	fun product xs = foldl op* (1, xs);
  1.1149 +	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
  1.1150  
  1.1151 -(* ------------------------------------------------------------------------- *)
  1.1152 -(* power: power(a,b) computes a^b, for a>=0, b>=0                            *)
  1.1153 -(* ------------------------------------------------------------------------- *)
  1.1154 +	fun refute_subgoal thy params thm subgoal =
  1.1155 +		refute_term thy params (nth_elem (subgoal, prems_of thm));
  1.1156  
  1.1157 -	(* int * int -> int *)
  1.1158 -
  1.1159 -	fun power (a,0) = 1
  1.1160 -	  | power (a,1) = a
  1.1161 -	  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end;
  1.1162  
  1.1163  (* ------------------------------------------------------------------------- *)
  1.1164 -(* size_of_type: returns the size of a type, where 'us' specifies the size   *)
  1.1165 -(*      of each basic type (i.e. each type variable), and 'cdepth' specifies *)
  1.1166 -(*      the maximal constructor depth for inductive datatypes                *)
  1.1167 +(* INTERPRETERS                                                              *)
  1.1168  (* ------------------------------------------------------------------------- *)
  1.1169  
  1.1170 -	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int *)
  1.1171 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1172  
  1.1173 -	fun size_of_type T us thy cdepth =
  1.1174 +	fun var_typevar_interpreter thy model args t =
  1.1175  	let
  1.1176 -		(* Term.typ -> (Term.typ * int) -> int *)
  1.1177 -		fun lookup_size T [] =
  1.1178 -			raise REFUTE ("size_of_type", "no size specified for type variable '" ^ (Sign.string_of_typ (sign_of thy) T) ^ "'")
  1.1179 -		  | lookup_size T ((typ,size)::pairs) =
  1.1180 -			if T=typ then size else lookup_size T pairs
  1.1181 +		fun is_var (Free _) = true
  1.1182 +		  | is_var (Var _)  = true
  1.1183 +		  | is_var _        = false
  1.1184 +		fun typeof (Free (_,T)) = T
  1.1185 +		  | typeof (Var (_,T))  = T
  1.1186 +		  | typeof _            = raise REFUTE ("var_typevar_interpreter", "term is not a variable")
  1.1187 +		fun is_typevar (TFree _) = true
  1.1188 +		  | is_typevar (TVar _)  = true
  1.1189 +		  | is_typevar _         = false
  1.1190 +		val (sizes, intrs) = model
  1.1191 +	in
  1.1192 +		if is_var t andalso is_typevar (typeof t) then
  1.1193 +			(case assoc (intrs, t) of
  1.1194 +			  Some intr => Some (intr, model, args)
  1.1195 +			| None      =>
  1.1196 +				let
  1.1197 +					val size = (the o assoc) (sizes, typeof t)  (* the model MUST specify a size for type variables *)
  1.1198 +					val idx  = #next_idx args
  1.1199 +					val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1))))
  1.1200 +					val next = (if size=2 then idx+1 else idx+size)
  1.1201 +				in
  1.1202 +					(* extend the model, increase 'next_idx' *)
  1.1203 +					Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args})
  1.1204 +				end)
  1.1205 +		else
  1.1206 +			None
  1.1207 +	end;
  1.1208 +
  1.1209 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1210 +
  1.1211 +	fun var_funtype_interpreter thy model args t =
  1.1212 +	let
  1.1213 +		fun is_var (Free _) = true
  1.1214 +		  | is_var (Var _)  = true
  1.1215 +		  | is_var _        = false
  1.1216 +		fun typeof (Free (_,T)) = T
  1.1217 +		  | typeof (Var (_,T))  = T
  1.1218 +		  | typeof _            = raise REFUTE ("var_funtype_interpreter", "term is not a variable")
  1.1219 +		fun stringof (Free (x,_))     = x
  1.1220 +		  | stringof (Var ((x,_), _)) = x
  1.1221 +		  | stringof _                = raise REFUTE ("var_funtype_interpreter", "term is not a variable")
  1.1222 +		fun is_funtype (Type ("fun", [_,_])) = true
  1.1223 +		  | is_funtype _                     = false
  1.1224 +		val (sizes, intrs) = model
  1.1225  	in
  1.1226 -		case T of
  1.1227 -		  Type ("prop", [])     => 2
  1.1228 -		| Type ("bool", [])     => 2
  1.1229 -		| Type ("Product_Type.unit", []) => 1
  1.1230 -		| Type ("+", [T1,T2])   => (size_of_type T1 us thy cdepth) + (size_of_type T2 us thy cdepth)
  1.1231 -		| Type ("*", [T1,T2])   => (size_of_type T1 us thy cdepth) * (size_of_type T2 us thy cdepth)
  1.1232 -		| Type ("fun", [T1,T2]) => power (size_of_type T2 us thy cdepth, size_of_type T1 us thy cdepth)
  1.1233 -		| Type ("set", [T1])    => size_of_type (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
  1.1234 -		| Type (s, Ts)          =>
  1.1235 -			(case DatatypePackage.datatype_info thy s of
  1.1236 -			  Some info => (* inductive datatype *)
  1.1237 -				if cdepth>0 then
  1.1238 +		if is_var t andalso is_funtype (typeof t) then
  1.1239 +			(case assoc (intrs, t) of
  1.1240 +			  Some intr => Some (intr, model, args)
  1.1241 +			| None      =>
  1.1242 +				let
  1.1243 +					val T1 = domain_type (typeof t)
  1.1244 +					val T2 = range_type (typeof t)
  1.1245 +					(* we create 'size_of_interpretation (interpret (... T1))' different copies *)
  1.1246 +					(* of the tree for 'T2', which are then combined into a single new tree     *)
  1.1247 +					val (i1, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (stringof t, T1))
  1.1248 +					(* power(a,b) computes a^b, for a>=0, b>=0 *)
  1.1249 +					(* int * int -> int *)
  1.1250 +					fun power (a,0) = 1
  1.1251 +					  | power (a,1) = a
  1.1252 +					  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
  1.1253 +					fun size_of_interpretation (Leaf xs) = length xs
  1.1254 +					  | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
  1.1255 +					val size = size_of_interpretation i1
  1.1256 +					(* make fresh copies, with different variable indices *)
  1.1257 +					(* int -> int -> (int * interpretation list *)
  1.1258 +					fun make_copies idx 0 =
  1.1259 +						(idx, [])
  1.1260 +					  | make_copies idx n =
  1.1261 +						let
  1.1262 +							val (copy, _, args) = interpret thy (sizes, []) {next_idx = idx, bounds = [], wellformed=True} (Free (stringof t, T2))
  1.1263 +							val (next, copies)  = make_copies (#next_idx args) (n-1)
  1.1264 +						in
  1.1265 +							(next, copy :: copies)
  1.1266 +						end
  1.1267 +					val (idx, copies) = make_copies (#next_idx args) (size_of_interpretation i1)
  1.1268 +					(* combine copies into a single tree *)
  1.1269 +					val intr = Node copies
  1.1270 +				in
  1.1271 +					(* extend the model, increase 'next_idx' *)
  1.1272 +					Some (intr, (sizes, (t, intr)::intrs), {next_idx = idx, bounds = #bounds args, wellformed = #wellformed args})
  1.1273 +				end)
  1.1274 +		else
  1.1275 +			None
  1.1276 +	end;
  1.1277 +
  1.1278 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1279 +
  1.1280 +	fun var_settype_interpreter thy model args t =
  1.1281 +		let
  1.1282 +			val (sizes, intrs) = model
  1.1283 +		in
  1.1284 +			case t of
  1.1285 +			  Free (x, Type ("set", [T])) =>
  1.1286 +				(case assoc (intrs, t) of
  1.1287 +				  Some intr => Some (intr, model, args)
  1.1288 +				| None      =>
  1.1289 +					let
  1.1290 +						val (intr, _, args') = interpret thy model args (Free (x, Type ("fun", [T, Type ("bool", [])])))
  1.1291 +					in
  1.1292 +						Some (intr, (sizes, (t, intr)::intrs), args')
  1.1293 +					end)
  1.1294 +			| Var ((x,i), Type ("set", [T])) =>
  1.1295 +				(case assoc (intrs, t) of
  1.1296 +				  Some intr => Some (intr, model, args)
  1.1297 +				| None      =>
  1.1298 +					let
  1.1299 +						val (intr, _, args') = interpret thy model args (Var ((x,i), Type ("fun", [T, Type ("bool", [])])))
  1.1300 +					in
  1.1301 +						Some (intr, (sizes, (t, intr)::intrs), args')
  1.1302 +					end)
  1.1303 +			| _ => None
  1.1304 +		end;
  1.1305 +
  1.1306 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1307 +
  1.1308 +	fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds args), model, args)
  1.1309 +	  | boundvar_interpreter thy model args _         = None;
  1.1310 +
  1.1311 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1312 +
  1.1313 +	fun abstraction_interpreter thy model args (Abs (x, T, t)) =
  1.1314 +		let
  1.1315 +			val (sizes, intrs) = model
  1.1316 +			(* create all constants of type T *)
  1.1317 +			val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (x, T))
  1.1318 +			(* returns a list with all unit vectors of length n *)
  1.1319 +			(* int -> interpretation list *)
  1.1320 +			fun unit_vectors n =
  1.1321 +			let
  1.1322 +				(* returns the k-th unit vector of length n *)
  1.1323 +				(* int * int -> interpretation *)
  1.1324 +				fun unit_vector (k,n) =
  1.1325 +					Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1.1326 +				(* int -> interpretation list -> interpretation list *)
  1.1327 +				fun unit_vectors_acc k vs =
  1.1328 +					if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1.1329 +			in
  1.1330 +				unit_vectors_acc 1 []
  1.1331 +			end
  1.1332 +			(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1.1333 +			(* 'a -> 'a list list -> 'a list list *)
  1.1334 +			fun cons_list x xss =
  1.1335 +				map (fn xs => x::xs) xss
  1.1336 +			(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1.1337 +			(* int -> 'a list -> 'a list list *)
  1.1338 +			fun pick_all 1 xs =
  1.1339 +				map (fn x => [x]) xs
  1.1340 +			  | pick_all n xs =
  1.1341 +				let val rec_pick = pick_all (n-1) xs in
  1.1342 +					foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1.1343 +				end
  1.1344 +			(* interpretation -> interpretation list *)
  1.1345 +			fun make_constants (Leaf xs) =
  1.1346 +				unit_vectors (length xs)
  1.1347 +			  | make_constants (Node xs) =
  1.1348 +				map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1.1349 +			(* interpret the body 't' separately for each constant *)
  1.1350 +			val ((model', args'), bodies) = foldl_map
  1.1351 +				(fn ((m,a), c) =>
  1.1352 +					let
  1.1353 +						(* add 'c' to 'bounds' *)
  1.1354 +						val (i',m',a') = interpret thy m {next_idx = #next_idx a, bounds = c::(#bounds a), wellformed = #wellformed a} t
  1.1355 +					in
  1.1356 +						(* keep the new model m' and 'next_idx', but use old 'bounds' *)
  1.1357 +						((m',{next_idx = #next_idx a', bounds = #bounds a, wellformed = #wellformed a'}), i')
  1.1358 +					end)
  1.1359 +				((model,args), make_constants i)
  1.1360 +		in
  1.1361 +			Some (Node bodies, model', args')
  1.1362 +		end
  1.1363 +	  | abstraction_interpreter thy model args _               = None;
  1.1364 +
  1.1365 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1366 +
  1.1367 +	fun apply_interpreter thy model args (t1 $ t2) =
  1.1368 +		let
  1.1369 +			(* auxiliary functions *)
  1.1370 +			(* interpretation * interpretation -> interpretation *)
  1.1371 +			fun interpretation_disjunction (tr1,tr2) =
  1.1372 +				tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
  1.1373 +			(* prop_formula * interpretation -> interpretation *)
  1.1374 +			fun prop_formula_times_interpretation (fm,tr) =
  1.1375 +				tree_map (map (fn x => SAnd (fm,x))) tr
  1.1376 +			(* prop_formula list * interpretation list -> interpretation *)
  1.1377 +			fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
  1.1378 +				prop_formula_times_interpretation (fm,tr)
  1.1379 +			  | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
  1.1380 +				interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees))
  1.1381 +			  | prop_formula_list_dot_product_interpretation_list (_,_) =
  1.1382 +				raise REFUTE ("apply_interpreter", "empty list (in dot product)")
  1.1383 +			(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1.1384 +			(* 'a -> 'a list list -> 'a list list *)
  1.1385 +			fun cons_list x xss =
  1.1386 +				map (fn xs => x::xs) xss
  1.1387 +			(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
  1.1388 +			(* 'a list list -> 'a list list *)
  1.1389 +			fun pick_all [xs] =
  1.1390 +				map (fn x => [x]) xs
  1.1391 +			  | pick_all (xs::xss) =
  1.1392 +				let val rec_pick = pick_all xss in
  1.1393 +					foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1.1394 +				end
  1.1395 +			  | pick_all _ =
  1.1396 +				raise REFUTE ("apply_interpreter", "empty list (in pick_all)")
  1.1397 +			(* interpretation -> prop_formula list *)
  1.1398 +			fun interpretation_to_prop_formula_list (Leaf xs) =
  1.1399 +				xs
  1.1400 +			  | interpretation_to_prop_formula_list (Node trees) =
  1.1401 +				map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees))
  1.1402 +			(* interpretation * interpretation -> interpretation *)
  1.1403 +			fun interpretation_apply (tr1,tr2) =
  1.1404 +				(case tr1 of
  1.1405 +				  Leaf _ =>
  1.1406 +					raise REFUTE ("apply_interpreter", "first interpretation is a leaf")
  1.1407 +				| Node xs =>
  1.1408 +					prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs))
  1.1409 +			(* interpret 't1' and 't2' *)
  1.1410 +			val (intr1, model1, args1) = interpret thy model args t1
  1.1411 +			val (intr2, model2, args2) = interpret thy model1 args1 t2
  1.1412 +		in
  1.1413 +			Some (interpretation_apply (intr1,intr2), model2, args2)
  1.1414 +		end
  1.1415 +	  | apply_interpreter thy model args _         = None;
  1.1416 +
  1.1417 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1418 +
  1.1419 +	fun const_unfold_interpreter thy model args t =
  1.1420 +		(* ------------------------------------------------------------------------- *)
  1.1421 +		(* We unfold constants for which a defining equation is given as an axiom.   *)
  1.1422 +		(* A polymorphic axiom's type variables are instantiated.  Eta-expansion is  *)
  1.1423 +		(* performed only if necessary; arguments in the axiom that are present as   *)
  1.1424 +		(* actual arguments in 't' are simply substituted.  If more actual than      *)
  1.1425 +		(* formal arguments are present, the constant is *not* unfolded, so that     *)
  1.1426 +		(* other interpreters (that may just not have looked into the term far       *)
  1.1427 +		(* enough yet) may be applied first (after 'apply_interpreter' gets rid of   *)
  1.1428 +		(* one argument).                                                            *)
  1.1429 +		(* ------------------------------------------------------------------------- *)
  1.1430 +		let
  1.1431 +			val (head, actuals) = strip_comb t
  1.1432 +			val actuals_count   = length actuals
  1.1433 +		in
  1.1434 +			case head of
  1.1435 +			  Const (s,T) =>
  1.1436 +				let
  1.1437 +					(* (string * Term.term) list *)
  1.1438 +					val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
  1.1439 +					(* Term.term * Term.term list * Term.term list -> Term.term *)
  1.1440 +					(* term, formal arguments, actual arguments *)
  1.1441 +					fun normalize (t, [],    [])    = t
  1.1442 +					  | normalize (t, [],    y::ys) = raise REFUTE ("const_unfold_interpreter", "more actual than formal parameters")
  1.1443 +					  | normalize (t, x::xs, [])    = normalize (lambda x t, xs, [])                (* eta-expansion *)
  1.1444 +					  | normalize (t, x::xs, y::ys) = normalize (betapply (lambda x t, y), xs, ys)  (* substitution *)
  1.1445 +					(* string -> Term.typ -> (string * Term.term) list -> Term.term option *)
  1.1446 +					fun get_defn s T [] =
  1.1447 +						None
  1.1448 +					  | get_defn s T ((_,ax)::axms) =
  1.1449 +						(let
  1.1450 +							val (lhs, rhs)   = Logic.dest_equals ax  (* equations only *)
  1.1451 +							val (c, formals) = strip_comb lhs
  1.1452 +							val (s', T')     = dest_Const c
  1.1453 +						in
  1.1454 +							if (s=s') andalso (actuals_count <= length formals) then
  1.1455 +								let
  1.1456 +									val varT'      = Type.varifyT T'  (* for polymorphic definitions *)
  1.1457 +									val typeSubs   = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (varT', T))
  1.1458 +									val varRhs     = map_term_types Type.varifyT rhs
  1.1459 +									val varFormals = map (map_term_types Type.varifyT) formals
  1.1460 +									val rhs'       = normalize (varRhs, varFormals, actuals)
  1.1461 +									val unvarRhs   = map_term_types
  1.1462 +										(map_type_tvar
  1.1463 +											(fn (v,_) =>
  1.1464 +												case Vartab.lookup (typeSubs, v) of
  1.1465 +												  None =>
  1.1466 +													raise REFUTE ("const_unfold_interpreter", "schematic type variable " ^ (fst v) ^ "not instantiated (in definition of " ^ quote s ^ ")")
  1.1467 +												| Some typ =>
  1.1468 +													typ))
  1.1469 +										rhs'
  1.1470 +								in
  1.1471 +									Some unvarRhs
  1.1472 +								end
  1.1473 +							else
  1.1474 +								get_defn s T axms
  1.1475 +						end
  1.1476 +						handle TERM _          => get_defn s T axms
  1.1477 +						     | Type.TYPE_MATCH => get_defn s T axms)
  1.1478 +				in
  1.1479 +					case get_defn s T axioms of
  1.1480 +					  Some t' => Some (interpret thy model args t')
  1.1481 +					| None    => None
  1.1482 +				end
  1.1483 +			| _ => None
  1.1484 +		end;
  1.1485 +
  1.1486 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1487 +
  1.1488 +	fun Pure_interpreter thy model args t =
  1.1489 +		let
  1.1490 +			fun toTrue (Leaf [fm,_]) = fm
  1.1491 +			  | toTrue _             = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value")
  1.1492 +			fun toFalse (Leaf [_,fm]) = fm
  1.1493 +			  | toFalse _             = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value")
  1.1494 +		in
  1.1495 +			case t of
  1.1496 +			  (*Const ("Goal", _) $ t1 =>
  1.1497 +				Some (interpret thy model args t1) |*)
  1.1498 +			  Const ("all", _) $ t1 =>
  1.1499 +				let
  1.1500 +					val (i,m,a) = (interpret thy model args t1)
  1.1501 +				in
  1.1502 +					case i of
  1.1503 +					  Node xs =>
  1.1504 +						let
  1.1505 +							val fmTrue  = PropLogic.all (map toTrue xs)
  1.1506 +							val fmFalse = PropLogic.exists (map toFalse xs)
  1.1507 +						in
  1.1508 +							Some (Leaf [fmTrue, fmFalse], m, a)
  1.1509 +						end
  1.1510 +					| _ =>
  1.1511 +						raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function")
  1.1512 +				end
  1.1513 +			| Const ("==", _) $ t1 $ t2 =>
  1.1514 +				let
  1.1515 +					val (i1,m1,a1) = interpret thy model args t1
  1.1516 +					val (i2,m2,a2) = interpret thy m1 a1 t2
  1.1517 +					(* interpretation * interpretation -> prop_formula *)
  1.1518 +					fun interpret_equal (tr1,tr2) =
  1.1519 +						(case tr1 of
  1.1520 +						  Leaf x =>
  1.1521 +							(case tr2 of
  1.1522 +							  Leaf y => PropLogic.dot_product (x,y)
  1.1523 +							| _      => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher"))
  1.1524 +						| Node xs =>
  1.1525 +							(case tr2 of
  1.1526 +							  Leaf _  => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher")
  1.1527 +							(* extensionality: two functions are equal iff they are equal for every element *)
  1.1528 +							| Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
  1.1529 +					(* interpretation * interpretation -> prop_formula *)
  1.1530 +					fun interpret_unequal (tr1,tr2) =
  1.1531 +						(case tr1 of
  1.1532 +						  Leaf x =>
  1.1533 +							(case tr2 of
  1.1534 +							  Leaf y =>
  1.1535 +								let
  1.1536 +									fun unequal [] ([],_) =
  1.1537 +										False
  1.1538 +									  | unequal (x::xs) (y::ys1, ys2) =
  1.1539 +										SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2))
  1.1540 +									  | unequal _ _ =
  1.1541 +										raise REFUTE ("Pure_interpreter", "\"==\": leafs have different width")
  1.1542 +								in
  1.1543 +									unequal x (y,[])
  1.1544 +								end
  1.1545 +							| _      => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher"))
  1.1546 +						| Node xs =>
  1.1547 +							(case tr2 of
  1.1548 +							  Leaf _  => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher")
  1.1549 +							(* extensionality: two functions are unequal iff there exist unequal elements *)
  1.1550 +							| Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys))))
  1.1551 +					val fmTrue  = interpret_equal (i1,i2)
  1.1552 +					val fmFalse = interpret_unequal (i1,i2)
  1.1553 +				in
  1.1554 +					Some (Leaf [fmTrue, fmFalse], m2, a2)
  1.1555 +				end
  1.1556 +			| Const ("==>", _) $ t1 $ t2 =>
  1.1557 +				let
  1.1558 +					val (i1,m1,a1) = interpret thy model args t1
  1.1559 +					val (i2,m2,a2) = interpret thy m1 a1 t2
  1.1560 +					val fmTrue     = SOr (toFalse i1, toTrue i2)
  1.1561 +					val fmFalse    = SAnd (toTrue i1, toFalse i2)
  1.1562 +				in
  1.1563 +					Some (Leaf [fmTrue, fmFalse], m2, a2)
  1.1564 +				end
  1.1565 +			| _ => None
  1.1566 +		end;
  1.1567 +
  1.1568 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1569 +
  1.1570 +	fun HOLogic_interpreter thy model args t =
  1.1571 +	(* ------------------------------------------------------------------------- *)
  1.1572 +	(* Providing interpretations directly is more efficient than unfolding the   *)
  1.1573 +	(* logical constants; however, we need versions for constants with arguments *)
  1.1574 +	(* (to avoid unfolding) as well as versions for constants without arguments  *)
  1.1575 +	(* (since in HOL, logical constants can themselves be arguments)             *)
  1.1576 +	(* ------------------------------------------------------------------------- *)
  1.1577 +	let
  1.1578 +		fun eta_expand t i =
  1.1579 +			let
  1.1580 +				val Ts = binder_types (fastype_of t)
  1.1581 +			in
  1.1582 +				foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
  1.1583 +					(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
  1.1584 +			end
  1.1585 +		val TT = Leaf [True, False]
  1.1586 +		val FF = Leaf [False, True]
  1.1587 +		fun toTrue (Leaf [fm,_]) = fm
  1.1588 +		  | toTrue _             = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value")
  1.1589 +		fun toFalse (Leaf [_,fm]) = fm
  1.1590 +		  | toFalse _             = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value")
  1.1591 +	in
  1.1592 +		case t of
  1.1593 +		  Const ("Trueprop", _) $ t1 =>
  1.1594 +			Some (interpret thy model args t1)
  1.1595 +		| Const ("Trueprop", _) =>
  1.1596 +			Some (Node [TT, FF], model, args)
  1.1597 +		| Const ("Not", _) $ t1 =>
  1.1598 +			apply_interpreter thy model args t
  1.1599 +		| Const ("Not", _) =>
  1.1600 +			Some (Node [FF, TT], model, args)
  1.1601 +		| Const ("True", _) =>
  1.1602 +			Some (TT, model, args)
  1.1603 +		| Const ("False", _) =>
  1.1604 +			Some (FF, model, args)
  1.1605 +		| Const ("arbitrary", T) =>
  1.1606 +			(* treat 'arbitrary' just like a free variable of the same type *)
  1.1607 +			(case assoc (snd model, t) of
  1.1608 +			  Some intr =>
  1.1609 +				Some (intr, model, args)
  1.1610 +			| None =>
  1.1611 +				let
  1.1612 +					val (sizes, intrs) = model
  1.1613 +					val (intr, _, a)   = interpret thy (sizes, []) args (Free ("<arbitrary>", T))
  1.1614 +				in
  1.1615 +					Some (intr, (sizes, (t,intr)::intrs), a)
  1.1616 +				end)
  1.1617 +		| Const ("The", _) $ t1 =>
  1.1618 +			apply_interpreter thy model args t
  1.1619 +		| Const ("The", T as Type ("fun", [_, T'])) =>
  1.1620 +			(* treat 'The' like a free variable, but with a fixed interpretation for boolean *)
  1.1621 +			(* functions that map exactly one constant of type T' to True                    *)
  1.1622 +			(case assoc (snd model, t) of
  1.1623 +				Some intr =>
  1.1624 +					Some (intr, model, args)
  1.1625 +			| None =>
  1.1626 +				let
  1.1627 +					val (sizes, intrs) = model
  1.1628 +					val (intr, _, a)   = interpret thy (sizes, []) args (Free ("<The>", T))
  1.1629 +					(* create all constants of type T' => bool, ... *)
  1.1630 +					val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<The>", Type ("fun", [T', Type ("bool",[])])))
  1.1631 +					(* ... and all constants of type T' *)
  1.1632 +					val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<The>", T'))
  1.1633 +					(* returns a list with all unit vectors of length n *)
  1.1634 +					(* int -> interpretation list *)
  1.1635 +					fun unit_vectors n =
  1.1636 +					let
  1.1637 +						(* returns the k-th unit vector of length n *)
  1.1638 +						(* int * int -> interpretation *)
  1.1639 +						fun unit_vector (k,n) =
  1.1640 +							Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1.1641 +						(* int -> interpretation list -> interpretation list *)
  1.1642 +						fun unit_vectors_acc k vs =
  1.1643 +							if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1.1644 +					in
  1.1645 +						unit_vectors_acc 1 []
  1.1646 +					end
  1.1647 +					(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1.1648 +					(* 'a -> 'a list list -> 'a list list *)
  1.1649 +					fun cons_list x xss =
  1.1650 +						map (fn xs => x::xs) xss
  1.1651 +					(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1.1652 +					(* int -> 'a list -> 'a list list *)
  1.1653 +					fun pick_all 1 xs =
  1.1654 +						map (fn x => [x]) xs
  1.1655 +					  | pick_all n xs =
  1.1656 +						let val rec_pick = pick_all (n-1) xs in
  1.1657 +							foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1.1658 +						end
  1.1659 +					(* interpretation -> interpretation list *)
  1.1660 +					fun make_constants (Leaf xs) =
  1.1661 +						unit_vectors (length xs)
  1.1662 +					  | make_constants (Node xs) =
  1.1663 +						map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1.1664 +					val constantsFun = make_constants intrFun
  1.1665 +					val constantsT'  = make_constants intrT'
  1.1666 +					(* interpretation -> interpretation list -> interpretation option *)
  1.1667 +					fun the_val (Node xs) cs =
  1.1668 +						let
  1.1669 +							val TrueCount = foldl (fn (n,x) => if toTrue x = True then n+1 else n) (0,xs)
  1.1670 +							fun findThe (x::xs) (c::cs) =
  1.1671 +								if toTrue x = True then
  1.1672 +									c
  1.1673 +								else
  1.1674 +									findThe xs cs
  1.1675 +							  | findThe _ _ =
  1.1676 +								raise REFUTE ("HOLogic_interpreter", "\"The\": not found")
  1.1677 +						in
  1.1678 +							if TrueCount=1 then
  1.1679 +								Some (findThe xs cs)
  1.1680 +							else
  1.1681 +								None
  1.1682 +						end
  1.1683 +					  | the_val _ _ =
  1.1684 +						raise REFUTE ("HOLogic_interpreter", "\"The\": function interpreted as a leaf")
  1.1685 +				in
  1.1686 +					case intr of
  1.1687 +					  Node xs =>
  1.1688 +						let
  1.1689 +							(* replace interpretation 'x' by the interpretation determined by 'f' *)
  1.1690 +							val intrThe = Node (map (fn (x,f) => if_none (the_val f constantsT') x) (xs ~~ constantsFun))
  1.1691 +						in
  1.1692 +							Some (intrThe, (sizes, (t,intrThe)::intrs), a)
  1.1693 +						end
  1.1694 +					| _ =>
  1.1695 +						raise REFUTE ("HOLogic_interpreter", "\"The\": interpretation is a leaf")
  1.1696 +				end)
  1.1697 +		| Const ("Hilbert_Choice.Eps", _) $ t1 =>
  1.1698 +			apply_interpreter thy model args t
  1.1699 +		| Const ("Hilbert_Choice.Eps", T as Type ("fun", [_, T'])) =>
  1.1700 +			(* treat 'The' like a free variable, but with a fixed interpretation for boolean *)
  1.1701 +			(* functions that map exactly one constant of type T' to True                    *)
  1.1702 +			(case assoc (snd model, t) of
  1.1703 +				Some intr =>
  1.1704 +					Some (intr, model, args)
  1.1705 +			| None =>
  1.1706 +				let
  1.1707 +					val (sizes, intrs) = model
  1.1708 +					val (intr, _, a)   = interpret thy (sizes, []) args (Free ("<Eps>", T))
  1.1709 +					(* create all constants of type T' => bool, ... *)
  1.1710 +					val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<Eps>", Type ("fun", [T', Type ("bool",[])])))
  1.1711 +					(* ... and all constants of type T' *)
  1.1712 +					val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<Eps>", T'))
  1.1713 +					(* returns a list with all unit vectors of length n *)
  1.1714 +					(* int -> interpretation list *)
  1.1715 +					fun unit_vectors n =
  1.1716 +					let
  1.1717 +						(* returns the k-th unit vector of length n *)
  1.1718 +						(* int * int -> interpretation *)
  1.1719 +						fun unit_vector (k,n) =
  1.1720 +							Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1.1721 +						(* int -> interpretation list -> interpretation list *)
  1.1722 +						fun unit_vectors_acc k vs =
  1.1723 +							if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1.1724 +					in
  1.1725 +						unit_vectors_acc 1 []
  1.1726 +					end
  1.1727 +					(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1.1728 +					(* 'a -> 'a list list -> 'a list list *)
  1.1729 +					fun cons_list x xss =
  1.1730 +						map (fn xs => x::xs) xss
  1.1731 +					(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1.1732 +					(* int -> 'a list -> 'a list list *)
  1.1733 +					fun pick_all 1 xs =
  1.1734 +						map (fn x => [x]) xs
  1.1735 +					  | pick_all n xs =
  1.1736 +						let val rec_pick = pick_all (n-1) xs in
  1.1737 +							foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1.1738 +						end
  1.1739 +					(* interpretation -> interpretation list *)
  1.1740 +					fun make_constants (Leaf xs) =
  1.1741 +						unit_vectors (length xs)
  1.1742 +					  | make_constants (Node xs) =
  1.1743 +						map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1.1744 +					val constantsFun = make_constants intrFun
  1.1745 +					val constantsT'  = make_constants intrT'
  1.1746 +					(* interpretation -> interpretation list -> interpretation list *)
  1.1747 +					fun true_values (Node xs) cs =
  1.1748 +						mapfilter (fn (x,c) => if toTrue x = True then Some c else None) (xs~~cs)
  1.1749 +					  | true_values _ _ =
  1.1750 +						raise REFUTE ("HOLogic_interpreter", "\"Eps\": function interpreted as a leaf")
  1.1751 +				in
  1.1752 +					case intr of
  1.1753 +					  Node xs =>
  1.1754 +						let
  1.1755 +							val (wf, intrsEps) = foldl_map (fn (w,(x,f)) =>
  1.1756 +								case true_values f constantsT' of
  1.1757 +								  []  => (w, x)  (* no value mapped to true -> no restriction *)
  1.1758 +								| [c] => (w, c)  (* one value mapped to true -> that's the one *)
  1.1759 +								| cs  =>
  1.1760 +									let
  1.1761 +										(* interpretation * interpretation -> prop_formula *)
  1.1762 +										fun interpret_equal (tr1,tr2) =
  1.1763 +											(case tr1 of
  1.1764 +											  Leaf x =>
  1.1765 +												(case tr2 of
  1.1766 +												  Leaf y => PropLogic.dot_product (x,y)
  1.1767 +												| _      => raise REFUTE ("HOLogic_interpreter", "\"Eps\": second tree is higher"))
  1.1768 +												| Node xs =>
  1.1769 +												(case tr2 of
  1.1770 +												  Leaf _  => raise REFUTE ("HOLogic_interpreter", "\"Eps\": first tree is higher")
  1.1771 +												(* extensionality: two functions are equal iff they are equal for every element *)
  1.1772 +												| Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
  1.1773 +									in
  1.1774 +										(SAnd (w, PropLogic.exists (map (fn c => interpret_equal (x,c)) cs)), x)  (* impose restrictions on x *)
  1.1775 +									end
  1.1776 +								)
  1.1777 +								(#wellformed a, xs ~~ constantsFun)
  1.1778 +							val intrEps = Node intrsEps
  1.1779 +						in
  1.1780 +							Some (intrEps, (sizes, (t,intrEps)::intrs), {next_idx = #next_idx a, bounds = #bounds a, wellformed = wf})
  1.1781 +						end
  1.1782 +					| _ =>
  1.1783 +						raise REFUTE ("HOLogic_interpreter", "\"Eps\": interpretation is a leaf")
  1.1784 +				end)
  1.1785 +		| Const ("All", _) $ t1 =>
  1.1786 +			let
  1.1787 +				val (i,m,a) = interpret thy model args t1
  1.1788 +			in
  1.1789 +				case i of
  1.1790 +				  Node xs =>
  1.1791 +					let
  1.1792 +						val fmTrue  = PropLogic.all (map toTrue xs)
  1.1793 +						val fmFalse = PropLogic.exists (map toFalse xs)
  1.1794 +					in
  1.1795 +						Some (Leaf [fmTrue, fmFalse], m, a)
  1.1796 +					end
  1.1797 +				| _ =>
  1.1798 +					raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function")
  1.1799 +			end
  1.1800 +		| Const ("All", _) =>
  1.1801 +			Some (interpret thy model args (eta_expand t 1))
  1.1802 +		| Const ("Ex", _) $ t1 =>
  1.1803 +			let
  1.1804 +				val (i,m,a) = interpret thy model args t1
  1.1805 +			in
  1.1806 +				case i of
  1.1807 +				  Node xs =>
  1.1808 +					let
  1.1809 +						val fmTrue  = PropLogic.exists (map toTrue xs)
  1.1810 +						val fmFalse = PropLogic.all (map toFalse xs)
  1.1811 +					in
  1.1812 +						Some (Leaf [fmTrue, fmFalse], m, a)
  1.1813 +					end
  1.1814 +				| _ =>
  1.1815 +					raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function")
  1.1816 +			end
  1.1817 +		| Const ("Ex", _) =>
  1.1818 +			Some (interpret thy model args (eta_expand t 1))
  1.1819 +		| Const ("Ex1", _) $ t1 =>
  1.1820 +			let
  1.1821 +				val (i,m,a) = interpret thy model args t1
  1.1822 +			in
  1.1823 +				case i of
  1.1824 +				  Node xs =>
  1.1825 +					let
  1.1826 +						(* interpretation list -> prop_formula *)
  1.1827 +						fun allfalse []      = True
  1.1828 +						  | allfalse (x::xs) = SAnd (toFalse x, allfalse xs)
  1.1829 +						(* interpretation list -> prop_formula *)
  1.1830 +						fun exactly1true []      = False
  1.1831 +						  | exactly1true (x::xs) = SOr (SAnd (toTrue x, allfalse xs), SAnd (toFalse x, exactly1true xs))
  1.1832 +						(* interpretation list -> prop_formula *)
  1.1833 +						fun atleast2true []      = False
  1.1834 +						  | atleast2true (x::xs) = SOr (SAnd (toTrue x, PropLogic.exists (map toTrue xs)), atleast2true xs)
  1.1835 +						val fmTrue  = exactly1true xs
  1.1836 +						val fmFalse = SOr (allfalse xs, atleast2true xs)
  1.1837 +					in
  1.1838 +						Some (Leaf [fmTrue, fmFalse], m, a)
  1.1839 +					end
  1.1840 +				| _ =>
  1.1841 +					raise REFUTE ("HOLogic_interpreter", "\"Ex1\" is not followed by a function")
  1.1842 +			end
  1.1843 +		| Const ("Ex1", _) =>
  1.1844 +			Some (interpret thy model args (eta_expand t 1))
  1.1845 +		| Const ("op =", _) $ t1 $ t2 =>
  1.1846 +				let
  1.1847 +					val (i1,m1,a1) = interpret thy model args t1
  1.1848 +					val (i2,m2,a2) = interpret thy m1 a1 t2
  1.1849 +					(* interpretation * interpretation -> prop_formula *)
  1.1850 +					fun interpret_equal (tr1,tr2) =
  1.1851 +						(case tr1 of
  1.1852 +						  Leaf x =>
  1.1853 +							(case tr2 of
  1.1854 +							  Leaf y => PropLogic.dot_product (x,y)
  1.1855 +							| _      => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher"))
  1.1856 +						| Node xs =>
  1.1857 +							(case tr2 of
  1.1858 +							  Leaf _  => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher")
  1.1859 +							(* extensionality: two functions are equal iff they are equal for every element *)
  1.1860 +							| Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
  1.1861 +					(* interpretation * interpretation -> prop_formula *)
  1.1862 +					fun interpret_unequal (tr1,tr2) =
  1.1863 +						(case tr1 of
  1.1864 +						  Leaf x =>
  1.1865 +							(case tr2 of
  1.1866 +							  Leaf y =>
  1.1867 +								let
  1.1868 +									fun unequal [] ([],_) =
  1.1869 +										False
  1.1870 +									  | unequal (x::xs) (y::ys1, ys2) =
  1.1871 +										SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2))
  1.1872 +									  | unequal _ _ =
  1.1873 +										raise REFUTE ("HOLogic_interpreter", "\"==\": leafs have different width")
  1.1874 +								in
  1.1875 +									unequal x (y,[])
  1.1876 +								end
  1.1877 +							| _      => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher"))
  1.1878 +						| Node xs =>
  1.1879 +							(case tr2 of
  1.1880 +							  Leaf _  => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher")
  1.1881 +							(* extensionality: two functions are unequal iff there exist unequal elements *)
  1.1882 +							| Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys))))
  1.1883 +					val fmTrue  = interpret_equal (i1,i2)
  1.1884 +					val fmFalse = interpret_unequal (i1,i2)
  1.1885 +				in
  1.1886 +					Some (Leaf [fmTrue, fmFalse], m2, a2)
  1.1887 +				end
  1.1888 +		| Const ("op =", _) $ t1 =>
  1.1889 +			Some (interpret thy model args (eta_expand t 1))
  1.1890 +		| Const ("op =", _) =>
  1.1891 +			Some (interpret thy model args (eta_expand t 2))
  1.1892 +		| Const ("op &", _) $ t1 $ t2 =>
  1.1893 +			apply_interpreter thy model args t
  1.1894 +		| Const ("op &", _) $ t1 =>
  1.1895 +			apply_interpreter thy model args t
  1.1896 +		| Const ("op &", _) =>
  1.1897 +			Some (Node [Node [TT, FF], Node [FF, FF]], model, args)
  1.1898 +		| Const ("op |", _) $ t1 $ t2 =>
  1.1899 +			apply_interpreter thy model args t
  1.1900 +		| Const ("op |", _) $ t1 =>
  1.1901 +			apply_interpreter thy model args t
  1.1902 +		| Const ("op |", _) =>
  1.1903 +			Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
  1.1904 +		| Const ("op -->", _) $ t1 $ t2 =>
  1.1905 +			apply_interpreter thy model args t
  1.1906 +		| Const ("op -->", _) $ t1 =>
  1.1907 +			apply_interpreter thy model args t
  1.1908 +		| Const ("op -->", _) =>
  1.1909 +			Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
  1.1910 +		| Const ("Collect", _) $ t1 =>
  1.1911 +			(* Collect == identity *)
  1.1912 +			Some (interpret thy model args t1)
  1.1913 +		| Const ("Collect", _) =>
  1.1914 +			Some (interpret thy model args (eta_expand t 1))
  1.1915 +		| Const ("op :", _) $ t1 $ t2 =>
  1.1916 +			(* op: == application *)
  1.1917 +			Some (interpret thy model args (t2 $ t1))
  1.1918 +		| Const ("op :", _) $ t1 =>
  1.1919 +			Some (interpret thy model args (eta_expand t 1))
  1.1920 +		| Const ("op :", _) =>
  1.1921 +			Some (interpret thy model args (eta_expand t 2))
  1.1922 +		| _ => None
  1.1923 +	end;
  1.1924 +
  1.1925 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1926 +
  1.1927 +	fun IDT_interpreter thy model args t =
  1.1928 +	let
  1.1929 +		fun is_var (Free _) = true
  1.1930 +		  | is_var (Var _)  = true
  1.1931 +		  | is_var _        = false
  1.1932 +		fun typeof (Free (_,T)) = T
  1.1933 +		  | typeof (Var (_,T))  = T
  1.1934 +		  | typeof _            = raise REFUTE ("var_IDT_interpreter", "term is not a variable")
  1.1935 +		val (sizes, intrs) = model
  1.1936 +		(* power(a,b) computes a^b, for a>=0, b>=0 *)
  1.1937 +		(* int * int -> int *)
  1.1938 +		fun power (a,0) = 1
  1.1939 +		  | power (a,1) = a
  1.1940 +		  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
  1.1941 +		(* interpretation -> int *)
  1.1942 +		fun size_of_interpretation (Leaf xs) = length xs
  1.1943 +		  | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
  1.1944 +		(* Term.typ -> int *)
  1.1945 +		fun size_of_type T =
  1.1946 +			let
  1.1947 +				val (i,_,_) = interpret thy model args (Free ("<IDT>", T))
  1.1948 +			in
  1.1949 +				size_of_interpretation i
  1.1950 +			end
  1.1951 +		(* int list -> int *)
  1.1952 +		fun sum xs = foldl op+ (0, xs)
  1.1953 +		(* int list -> int *)
  1.1954 +		fun product xs = foldl op* (1, xs)
  1.1955 +		(* DatatypeAux.dtyp * Term.typ -> DatatypeAux.dtyp -> Term.typ *)
  1.1956 +		fun typ_of_dtyp typ_assoc (DatatypeAux.DtTFree a) =
  1.1957 +			the (assoc (typ_assoc, DatatypeAux.DtTFree a))
  1.1958 +		  | typ_of_dtyp typ_assoc (DatatypeAux.DtRec i) =
  1.1959 +			raise REFUTE ("var_IDT_interpreter", "recursive datatype")
  1.1960 +		  | typ_of_dtyp typ_assoc (DatatypeAux.DtType (s, ds)) =
  1.1961 +			Type (s, map (typ_of_dtyp typ_assoc) ds)
  1.1962 +	in
  1.1963 +		if is_var t then
  1.1964 +			(case typeof t of
  1.1965 +			  Type (s, Ts) =>
  1.1966 +				(case DatatypePackage.datatype_info thy s of
  1.1967 +				  Some info =>  (* inductive datatype *)
  1.1968  					let
  1.1969  						val index               = #index info
  1.1970  						val descr               = #descr info
  1.1971  						val (_, dtyps, constrs) = the (assoc (descr, index))
  1.1972 -						val Typs                = dtyps ~~ Ts
  1.1973 -						(* DatatypeAux.dtyp -> Term.typ *)
  1.1974 -						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
  1.1975 -							the (assoc (Typs, DatatypeAux.DtTFree a))
  1.1976 -						  | typ_of_dtyp (DatatypeAux.DtRec i) =
  1.1977 -							let
  1.1978 -								val (s, ds, _) = the (assoc (descr, i))
  1.1979 -							in
  1.1980 -								Type (s, map typ_of_dtyp ds)
  1.1981 -							end
  1.1982 -						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
  1.1983 -							Type (s, map typ_of_dtyp ds)
  1.1984  					in
  1.1985 -						sum (map (fn (_,ds) => product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)) constrs)
  1.1986 +						if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
  1.1987 +							raise REFUTE ("var_IDT_interpreter", "recursive datatype argument")
  1.1988 +						else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
  1.1989 +							None  (* recursive datatype (requires an infinite model) *)
  1.1990 +						else
  1.1991 +							case assoc (intrs, t) of
  1.1992 +							  Some intr => Some (intr, model, args)
  1.1993 +							| None      =>
  1.1994 +								let
  1.1995 +									val typ_assoc = dtyps ~~ Ts
  1.1996 +									val size = sum (map (fn (_,ds) =>
  1.1997 +										product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) constrs)
  1.1998 +									val idx  = #next_idx args
  1.1999 +									(* for us, an IDT has no "internal structure" -- its interpretation is just a leaf *)
  1.2000 +									val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1))))
  1.2001 +									val next = (if size=2 then idx+1 else idx+size)
  1.2002 +								in
  1.2003 +									(* extend the model, increase 'next_idx' *)
  1.2004 +									Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args})
  1.2005 +								end
  1.2006  					end
  1.2007 -				else 0
  1.2008 -			| None      => error ("size_of_type: type contains an unknown type constructor: '" ^ s ^ "'"))
  1.2009 -		| TFree _               => lookup_size T us
  1.2010 -		| TVar _                => lookup_size T us
  1.2011 +				| None => None)
  1.2012 +			| _ => None)
  1.2013 +		else
  1.2014 +		let
  1.2015 +			val (head, params) = strip_comb t  (* look into applications to avoid unfolding *)
  1.2016 +		in
  1.2017 +			(case head of
  1.2018 +			  Const (c, T) =>
  1.2019 +				(case body_type T of
  1.2020 +				  Type (s, Ts) =>
  1.2021 +					(case DatatypePackage.datatype_info thy s of
  1.2022 +					  Some info =>  (* inductive datatype *)
  1.2023 +						let
  1.2024 +							val index               = #index info
  1.2025 +							val descr               = #descr info
  1.2026 +							val (_, dtyps, constrs) = the (assoc (descr, index))
  1.2027 +						in
  1.2028 +							if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
  1.2029 +								raise REFUTE ("var_IDT_interpreter", "recursive datatype argument")
  1.2030 +							else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
  1.2031 +								None  (* recursive datatype (requires an infinite model) *)
  1.2032 +							else
  1.2033 +								(case take_prefix (fn (c',_) => c' <> c) constrs of
  1.2034 +								  (_, []) =>
  1.2035 +									None (* unknown constructor *)
  1.2036 +								| (prevs, _) =>
  1.2037 +									if null params then
  1.2038 +									let
  1.2039 +										val typ_assoc = dtyps ~~ Ts
  1.2040 +										val offset = sum (map (fn (_,ds) =>
  1.2041 +											product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) prevs)
  1.2042 +										val (i,_,_) = interpret thy model args (Free ("<IDT>", T))
  1.2043 +										(* int * interpretation  -> int * interpretation *)
  1.2044 +										fun replace (offset, Leaf xs) =
  1.2045 +											(* replace the offset-th element by True, all others by False, inc. offset by 1 *)
  1.2046 +											(offset+1, Leaf (snd (foldl_map (fn (n,_) => (n+1, if n=offset then True else False)) (0, xs))))
  1.2047 +										  | replace (offset, Node xs) =
  1.2048 +											let
  1.2049 +												val (offset', xs') = foldl_map replace (offset, xs)
  1.2050 +											in
  1.2051 +												(offset', Node xs')
  1.2052 +											end
  1.2053 +										val (_,intr) = replace (offset, i)
  1.2054 +									in
  1.2055 +										Some (intr, model, args)
  1.2056 +									end
  1.2057 +									else
  1.2058 +										apply_interpreter thy model args t)  (* avoid unfolding by calling 'apply_interpreter' directly *)
  1.2059 +						end
  1.2060 +					| None => None)
  1.2061 +				| _ => None)
  1.2062 +			| _ => None)
  1.2063 +		end
  1.2064  	end;
  1.2065  
  1.2066 +
  1.2067  (* ------------------------------------------------------------------------- *)
  1.2068 -(* type_to_prop_tree: creates a tree of boolean variables that denotes an    *)
  1.2069 -(*      element of the type 'T'.  The height and branching factor of the     *)
  1.2070 -(*      tree depend on the size and "structure" of 'T'.                      *)
  1.2071 -(* 'us' : a "universe" specifying the number of elements for each basic type *)
  1.2072 -(*        (i.e. each type variable) in 'T'                                   *)
  1.2073 -(* 'cdepth': maximum constructor depth to be used for inductive datatypes    *)
  1.2074 -(* 'idx': the next index to be used for a boolean variable                   *)
  1.2075 +(* PRINTERS                                                                  *)
  1.2076  (* ------------------------------------------------------------------------- *)
  1.2077  
  1.2078 -	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *)
  1.2079 +	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1.2080  
  1.2081 -	fun type_to_prop_tree T us thy cdepth idx =
  1.2082 +	fun var_typevar_printer thy model t intr assignment =
  1.2083  	let
  1.2084 -		(* int -> Term.typ -> int -> prop_tree list * int *)
  1.2085 -		fun type_to_prop_tree_list 1 T' idx' =
  1.2086 -			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
  1.2087 -				([tr], newidx)
  1.2088 -			end
  1.2089 -		  | type_to_prop_tree_list n T' idx' =
  1.2090 -			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
  1.2091 -				let val (trees, lastidx) = type_to_prop_tree_list (n-1) T' newidx in
  1.2092 -					(tr::trees, lastidx)
  1.2093 -				end
  1.2094 -			end
  1.2095 +		fun is_var (Free _) = true
  1.2096 +		  | is_var (Var _)  = true
  1.2097 +		  | is_var _        = false
  1.2098 +		fun typeof (Free (_,T)) = T
  1.2099 +		  | typeof (Var (_,T))  = T
  1.2100 +		  | typeof _            = raise REFUTE ("var_typevar_printer", "term is not a variable")
  1.2101 +		fun is_typevar (TFree _) = true
  1.2102 +		  | is_typevar (TVar _)  = true
  1.2103 +		  | is_typevar _         = false
  1.2104  	in
  1.2105 -		case T of
  1.2106 -		  Type ("prop", []) =>
  1.2107 -			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
  1.2108 -		| Type ("bool", []) =>
  1.2109 -			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
  1.2110 -		| Type ("Product_Type.unit", []) =>
  1.2111 -			(Leaf [True], idx)
  1.2112 -		| Type ("+", [T1,T2]) =>
  1.2113 +		if is_var t andalso is_typevar (typeof t) then
  1.2114  			let
  1.2115 -				val s1 = size_of_type T1 us thy cdepth
  1.2116 -				val s2 = size_of_type T2 us thy cdepth
  1.2117 -				val s  = s1 + s2
  1.2118 -			in
  1.2119 -				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
  1.2120 -					raise EMPTY_DATATYPE
  1.2121 -				else
  1.2122 -					error "sum types (+) not implemented yet (TODO)"
  1.2123 -			end
  1.2124 -		| Type ("*", [T1,T2]) =>
  1.2125 -			let
  1.2126 -				val s1 = size_of_type T1 us thy cdepth
  1.2127 -				val s2 = size_of_type T2 us thy cdepth
  1.2128 -				val s  = s1 * s2
  1.2129 +				(* interpretation -> int *)
  1.2130 +				fun index_from_interpretation (Leaf xs) =
  1.2131 +					let
  1.2132 +						val idx = find_index (PropLogic.eval assignment) xs
  1.2133 +					in
  1.2134 +						if idx<0 then
  1.2135 +							raise REFUTE ("var_typevar_printer", "illegal interpretation: no value assigned")
  1.2136 +						else
  1.2137 +							idx
  1.2138 +					end
  1.2139 +				  | index_from_interpretation _ =
  1.2140 +					raise REFUTE ("var_typevar_printer", "interpretation is not a leaf")
  1.2141 +				(* string -> string *)
  1.2142 +				fun strip_leading_quote s =
  1.2143 +					(implode o (fn (x::xs) => if x="'" then xs else (x::xs)) o explode) s
  1.2144 +				(* Term.typ -> string *)
  1.2145 +				fun string_of_typ (TFree (x,_))    = strip_leading_quote x
  1.2146 +				  | string_of_typ (TVar ((x,i),_)) = strip_leading_quote x ^ string_of_int i
  1.2147 +				  | string_of_typ _                = raise REFUTE ("var_typevar_printer", "type is not a type variable")
  1.2148  			in
  1.2149 -				if s1=0 orelse s2=0 then
  1.2150 -					raise EMPTY_DATATYPE
  1.2151 -				else
  1.2152 -					error "product types (*) not implemented yet (TODO)"
  1.2153 -			end
  1.2154 -		| Type ("fun", [T1,T2]) =>
  1.2155 -			(* we create 'size_of_type T1' different copies of the tree for 'T2', *)
  1.2156 -			(* which are then combined into a single new tree                     *)
  1.2157 -			let
  1.2158 -				val s = size_of_type T1 us thy cdepth
  1.2159 -			in
  1.2160 -				if s=0 then
  1.2161 -					raise EMPTY_DATATYPE
  1.2162 -				else
  1.2163 -					let val (trees, newidx) = type_to_prop_tree_list s T2 idx in
  1.2164 -						(Node trees, newidx)
  1.2165 -					end
  1.2166 +				Some (string_of_typ (typeof t) ^ string_of_int (index_from_interpretation intr))
  1.2167  			end
  1.2168 -		| Type ("set", [T1]) =>
  1.2169 -			type_to_prop_tree (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth idx
  1.2170 -		| Type (s, _) =>
  1.2171 -			(case DatatypePackage.constrs_of thy s of
  1.2172 -			   Some _ => (* inductive datatype *)
  1.2173 -					let
  1.2174 -						val s = size_of_type T us thy cdepth
  1.2175 -					in
  1.2176 -						if s=0 then
  1.2177 -							raise EMPTY_DATATYPE
  1.2178 -						else
  1.2179 -							(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
  1.2180 -					end
  1.2181 -			 | None   => error ("type_to_prop_tree: type contains an unknown type constructor: '" ^ s ^ "'"))
  1.2182 -		| TFree _ =>
  1.2183 -			let val s = size_of_type T us thy cdepth in
  1.2184 -				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
  1.2185 -			end
  1.2186 -		| TVar _  =>
  1.2187 -			let val s = size_of_type T us thy cdepth in
  1.2188 -				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
  1.2189 -			end
  1.2190 +		else
  1.2191 +			None
  1.2192  	end;
  1.2193  
  1.2194 -(* ------------------------------------------------------------------------- *)
  1.2195 -(* type_to_constants: creates a list of prop_trees with constants (True,     *)
  1.2196 -(*      False) rather than boolean variables, one for every element in the   *)
  1.2197 -(*      type 'T'; c.f. type_to_prop_tree                                     *)
  1.2198 -(* ------------------------------------------------------------------------- *)
  1.2199 +	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1.2200  
  1.2201 -	(* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *)
  1.2202 +	fun var_funtype_printer thy model t intr assignment =
  1.2203 +	let
  1.2204 +		fun is_var (Free _) = true
  1.2205 +		  | is_var (Var _)  = true
  1.2206 +		  | is_var _        = false
  1.2207 +		fun typeof (Free (_,T)) = T
  1.2208 +		  | typeof (Var (_,T))  = T
  1.2209 +		  | typeof _            = raise REFUTE ("var_funtype_printer", "term is not a variable")
  1.2210 +		fun is_funtype (Type ("fun", [_,_])) = true
  1.2211 +		  | is_funtype _                     = false
  1.2212 +	in
  1.2213 +		if is_var t andalso is_funtype (typeof t) then
  1.2214 +			let
  1.2215 +				val T1         = domain_type (typeof t)
  1.2216 +				val T2         = range_type (typeof t)
  1.2217 +				val (sizes, _) = model
  1.2218 +				(* create all constants of type T1 *)
  1.2219 +				val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_funtype_printer", T1))
  1.2220 +				(* returns a list with all unit vectors of length n *)
  1.2221 +				(* int -> interpretation list *)
  1.2222 +				fun unit_vectors n =
  1.2223 +				let
  1.2224 +					(* returns the k-th unit vector of length n *)
  1.2225 +					(* int * int -> interpretation *)
  1.2226 +					fun unit_vector (k,n) =
  1.2227 +						Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1.2228 +					(* int -> interpretation list -> interpretation list *)
  1.2229 +					fun unit_vectors_acc k vs =
  1.2230 +						if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1.2231 +				in
  1.2232 +					unit_vectors_acc 1 []
  1.2233 +				end
  1.2234 +				(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1.2235 +				(* 'a -> 'a list list -> 'a list list *)
  1.2236 +				fun cons_list x xss =
  1.2237 +					map (fn xs => x::xs) xss
  1.2238 +				(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1.2239 +				(* int -> 'a list -> 'a list list *)
  1.2240 +				fun pick_all 1 xs =
  1.2241 +					map (fn x => [x]) xs
  1.2242 +				  | pick_all n xs =
  1.2243 +					let val rec_pick = pick_all (n-1) xs in
  1.2244 +						foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1.2245 +					end
  1.2246 +				(* interpretation -> interpretation list *)
  1.2247 +				fun make_constants (Leaf xs) =
  1.2248 +					unit_vectors (length xs)
  1.2249 +				  | make_constants (Node xs) =
  1.2250 +					map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1.2251 +				(* interpretation list *)
  1.2252 +				val results = (case intr of
  1.2253 +					  Node xs => xs
  1.2254 +					| _       => raise REFUTE ("var_funtype_printer", "interpretation is a leaf"))
  1.2255 +				(* string list *)
  1.2256 +				val strings = map
  1.2257 +					(fn (argi,resulti) => print thy model (Free ("var_funtype_printer", T1)) argi assignment
  1.2258 +						^ "\\<mapsto>"
  1.2259 +						^ print thy model (Free ("var_funtype_printer", T2)) resulti assignment)
  1.2260 +					((make_constants i) ~~ results)
  1.2261 +			in
  1.2262 +				Some (enclose "(" ")" (commas strings))
  1.2263 +			end
  1.2264 +		else
  1.2265 +			None
  1.2266 +	end;
  1.2267  
  1.2268 -	fun type_to_constants T us thy cdepth =
  1.2269 +	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1.2270 +
  1.2271 +	fun var_settype_printer thy model t intr assignment =
  1.2272  	let
  1.2273 +		val (sizes, _) = model
  1.2274  		(* returns a list with all unit vectors of length n *)
  1.2275 -		(* int -> prop_tree list *)
  1.2276 +		(* int -> interpretation list *)
  1.2277  		fun unit_vectors n =
  1.2278  		let
  1.2279  			(* returns the k-th unit vector of length n *)
  1.2280 -			(* int * int -> prop_tree *)
  1.2281 +			(* int * int -> interpretation *)
  1.2282  			fun unit_vector (k,n) =
  1.2283  				Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1.2284 -			(* int -> prop_tree list -> prop_tree list *)
  1.2285 +			(* int -> interpretation list -> interpretation list *)
  1.2286  			fun unit_vectors_acc k vs =
  1.2287  				if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1.2288  		in
  1.2289 @@ -918,731 +1573,238 @@
  1.2290  			let val rec_pick = pick_all (n-1) xs in
  1.2291  				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1.2292  			end
  1.2293 +		(* interpretation -> interpretation list *)
  1.2294 +		fun make_constants (Leaf xs) =
  1.2295 +			unit_vectors (length xs)
  1.2296 +		  | make_constants (Node xs) =
  1.2297 +			map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1.2298  	in
  1.2299 -		case T of
  1.2300 -		  Type ("prop", [])     => unit_vectors 2
  1.2301 -		| Type ("bool", [])     => unit_vectors 2
  1.2302 -		| Type ("Product_Type.unit", []) => unit_vectors 1
  1.2303 -                | Type ("+", [T1,T2])   =>
  1.2304 +		case t of
  1.2305 +		  Free (x, Type ("set", [T])) =>
  1.2306  			let
  1.2307 -				val s1 = size_of_type T1 us thy cdepth
  1.2308 -				val s2 = size_of_type T2 us thy cdepth
  1.2309 +				(* interpretation list *)
  1.2310 +				val results = (case intr of
  1.2311 +				  Node xs => xs
  1.2312 +					| _       => raise REFUTE ("var_settype_printer", "interpretation is a leaf"))
  1.2313 +				(* create all constants of type T *)
  1.2314 +				val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T))
  1.2315 +				(* string list *)
  1.2316 +				val strings = mapfilter
  1.2317 +					(fn (argi,Leaf [fmTrue,fmFalse]) =>
  1.2318 +						if PropLogic.eval assignment fmTrue then
  1.2319 +							Some (print thy model (Free ("x", T)) argi assignment)
  1.2320 +						else if PropLogic.eval assignment fmFalse then
  1.2321 +							None
  1.2322 +						else
  1.2323 +							raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned"))
  1.2324 +					((make_constants i) ~~ results)
  1.2325  			in
  1.2326 -				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
  1.2327 -					raise EMPTY_DATATYPE
  1.2328 -				else
  1.2329 -					error "sum types (+) not implemented yet (TODO)"
  1.2330 -			end
  1.2331 -                | Type ("*", [T1,T2])   =>
  1.2332 -			let
  1.2333 -				val s1 = size_of_type T1 us thy cdepth
  1.2334 -				val s2 = size_of_type T2 us thy cdepth
  1.2335 -			in
  1.2336 -				if s1=0 orelse s2=0 then
  1.2337 -					raise EMPTY_DATATYPE
  1.2338 -				else
  1.2339 -					error "product types (*) not implemented yet (TODO)"
  1.2340 +				Some (enclose "{" "}" (commas strings))
  1.2341  			end
  1.2342 -		| Type ("fun", [T1,T2]) =>
  1.2343 +		| Var ((x,i), Type ("set", [T])) =>
  1.2344  			let
  1.2345 -				val s = size_of_type T1 us thy cdepth
  1.2346 +				(* interpretation list *)
  1.2347 +				val results = (case intr of
  1.2348 +				  Node xs => xs
  1.2349 +					| _       => raise REFUTE ("var_settype_printer", "interpretation is a leaf"))
  1.2350 +				(* create all constants of type T *)
  1.2351 +				val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T))
  1.2352 +				(* string list *)
  1.2353 +				val strings = mapfilter
  1.2354 +					(fn (argi,Leaf [fmTrue,fmFalse]) =>
  1.2355 +						if PropLogic.eval assignment fmTrue then
  1.2356 +							Some (print thy model (Free ("var_settype_printer", T)) argi assignment)
  1.2357 +						else if PropLogic.eval assignment fmTrue then
  1.2358 +							None
  1.2359 +						else
  1.2360 +							raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned"))
  1.2361 +					((make_constants i) ~~ results)
  1.2362  			in
  1.2363 -				if s=0 then
  1.2364 -					raise EMPTY_DATATYPE
  1.2365 -				else
  1.2366 -					map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth))
  1.2367 +				Some (enclose "{" "}" (commas strings))
  1.2368  			end
  1.2369 -		| Type ("set", [T1])    => type_to_constants (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
  1.2370 -		| Type (s, _)           =>
  1.2371 -			(case DatatypePackage.constrs_of thy s of
  1.2372 -			   Some _ => (* inductive datatype *)
  1.2373 -					let
  1.2374 -						val s = size_of_type T us thy cdepth
  1.2375 -					in
  1.2376 -						if s=0 then
  1.2377 -							raise EMPTY_DATATYPE
  1.2378 -						else
  1.2379 -							unit_vectors s
  1.2380 -					end
  1.2381 -			 | None   => error ("type_to_constants: type contains an unknown type constructor: '" ^ s ^ "'"))
  1.2382 -		| TFree _               => unit_vectors (size_of_type T us thy cdepth)
  1.2383 -		| TVar _                => unit_vectors (size_of_type T us thy cdepth)
  1.2384 +		| _ => None
  1.2385  	end;
  1.2386  
  1.2387 -(* ------------------------------------------------------------------------- *)
  1.2388 -(* prop_tree_equal: returns a propositional formula that is true iff 'tr1'   *)
  1.2389 -(*      and 'tr2' both denote the same element                               *)
  1.2390 -(* ------------------------------------------------------------------------- *)
  1.2391 -
  1.2392 -	(* prop_tree * prop_tree -> prop_formula *)
  1.2393 +	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1.2394  
  1.2395 -	fun prop_tree_equal (tr1,tr2) =
  1.2396 -		case tr1 of
  1.2397 -		  Leaf x =>
  1.2398 -			(case tr2 of
  1.2399 -			  Leaf y => prop_formula_dot_product (x,y)
  1.2400 -			| _      => raise REFUTE ("prop_tree_equal", "second tree is higher"))
  1.2401 -		| Node xs =>
  1.2402 -			(case tr2 of
  1.2403 -			  Leaf _  => raise REFUTE ("prop_tree_equal", "first tree is higher")
  1.2404 -			(* extensionality: two functions are equal iff they are equal for every element *)
  1.2405 -			| Node ys => list_conjunction (map prop_tree_equal (xs ~~ ys)));
  1.2406 +	fun HOLogic_printer thy model t intr assignment =
  1.2407 +		case t of
  1.2408 +		(* 'arbitrary', 'The', 'Hilbert_Choice.Eps' are printed like free variables of the same type *)
  1.2409 +		  Const ("arbitrary", T) =>
  1.2410 +			Some (print thy model (Free ("<arbitrary>", T)) intr assignment)
  1.2411 +		| Const ("The", T) =>
  1.2412 +			Some (print thy model (Free ("<The>", T)) intr assignment)
  1.2413 +		| Const ("Hilbert_Choice.Eps", T) =>
  1.2414 +			Some (print thy model (Free ("<Eps>", T)) intr assignment)
  1.2415 +		| _ =>
  1.2416 +			None;
  1.2417  
  1.2418 -(* ------------------------------------------------------------------------- *)
  1.2419 -(* prop_tree_apply: returns a tree that denotes the element obtained by      *)
  1.2420 -(*      applying the function which is denoted by the tree 't1' to the       *)
  1.2421 -(*      element which is denoted by the tree 't2'                            *)
  1.2422 -(* ------------------------------------------------------------------------- *)
  1.2423 +	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1.2424  
  1.2425 -	(* prop_tree * prop_tree -> prop_tree *)
  1.2426 -
  1.2427 -	fun prop_tree_apply (tr1,tr2) =
  1.2428 +	fun var_IDT_printer thy model t intr assignment =
  1.2429  	let
  1.2430 -		(* prop_tree * prop_tree -> prop_tree *)
  1.2431 -		fun prop_tree_disjunction (tr1,tr2) =
  1.2432 -			tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
  1.2433 -		(* prop_formula * prop_tree -> prop_tree *)
  1.2434 -		fun prop_formula_times_prop_tree (fm,tr) =
  1.2435 -			tree_map (map (fn x => SAnd (fm,x))) tr
  1.2436 -		(* prop_formula list * prop_tree list -> prop_tree *)
  1.2437 -		fun prop_formula_list_dot_product_prop_tree_list ([fm],[tr]) =
  1.2438 -			prop_formula_times_prop_tree (fm,tr)
  1.2439 -		  | prop_formula_list_dot_product_prop_tree_list (fm::fms,tr::trees) =
  1.2440 -			prop_tree_disjunction (prop_formula_times_prop_tree (fm,tr), prop_formula_list_dot_product_prop_tree_list (fms,trees))
  1.2441 -		  | prop_formula_list_dot_product_prop_tree_list (_,_) =
  1.2442 -			raise REFUTE ("prop_tree_apply::prop_formula_list_dot_product_prop_tree_list", "empty list")
  1.2443 -		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1.2444 -		(* 'a -> 'a list list -> 'a list list *)
  1.2445 -		fun cons_list x xss =
  1.2446 -			map (fn xs => x::xs) xss
  1.2447 -		(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
  1.2448 -		(* 'a list list -> 'a list list *)
  1.2449 -		fun pick_all [xs] =
  1.2450 -			map (fn x => [x]) xs
  1.2451 -		  | pick_all (xs::xss) =
  1.2452 -			let val rec_pick = pick_all xss in
  1.2453 -				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1.2454 -			end
  1.2455 -		  | pick_all _ =
  1.2456 -			raise REFUTE ("prop_tree_apply::pick_all", "empty list")
  1.2457 -		(* prop_tree -> prop_formula list *)
  1.2458 -		fun prop_tree_to_prop_formula_list (Leaf xs) =
  1.2459 -			xs
  1.2460 -		  | prop_tree_to_prop_formula_list (Node trees) =
  1.2461 -			map list_conjunction (pick_all (map prop_tree_to_prop_formula_list trees))
  1.2462 +		fun is_var (Free _) = true
  1.2463 +		  | is_var (Var _)  = true
  1.2464 +		  | is_var _        = false
  1.2465 +		fun typeof (Free (_,T)) = T
  1.2466 +		  | typeof (Var (_,T))  = T
  1.2467 +		  | typeof _            = raise REFUTE ("var_IDT_printer", "term is not a variable")
  1.2468  	in
  1.2469 -		case tr1 of
  1.2470 -		  Leaf _ =>
  1.2471 -			raise REFUTE ("prop_tree_apply", "first tree is a leaf")
  1.2472 -		| Node xs =>
  1.2473 -			prop_formula_list_dot_product_prop_tree_list (prop_tree_to_prop_formula_list tr2, xs)
  1.2474 -	end
  1.2475 -
  1.2476 -(* ------------------------------------------------------------------------- *)
  1.2477 -(* term_to_prop_tree: translates a HOL term 't' into a tree of propositional *)
  1.2478 -(*      formulas; 'us' specifies the number of elements for each type        *)
  1.2479 -(*      variable in 't'; 'cdepth' specifies the maximal constructor depth    *)
  1.2480 -(*      for inductive datatypes.  Also returns the lowest index that was not *)
  1.2481 -(*      used for a boolean variable, and a substitution of terms (free/      *)
  1.2482 -(*      schematic variables) by prop_trees.                                  *)
  1.2483 -(* ------------------------------------------------------------------------- *)
  1.2484 -
  1.2485 -	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_tree * (int * (Term.term * prop_tree) list) *)
  1.2486 -
  1.2487 -	fun term_to_prop_tree t us thy cdepth =
  1.2488 -	let
  1.2489 -		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree * (int * (Term.term * prop_tree) list) *)
  1.2490 -		fun variable_to_prop_tree_subst t' (idx,subs) =
  1.2491 -			case assoc (subs,t') of
  1.2492 -			  Some tr =>
  1.2493 -				(* return the previously associated tree; the substitution remains unchanged *)
  1.2494 -				(tr, (idx,subs))
  1.2495 -			| None =>
  1.2496 -				(* generate a new tree; update the index; extend the substitution *)
  1.2497 -				let
  1.2498 -					val T = case t' of
  1.2499 -						  Free (_,T) => T
  1.2500 -						| Var (_,T)  => T
  1.2501 -						| _          => raise REFUTE ("variable_to_prop_tree_subst", "term is not a (free or schematic) variable")
  1.2502 -					val (tr,newidx) = type_to_prop_tree T us thy cdepth idx
  1.2503 -				in
  1.2504 -					(tr, (newidx, (t',tr)::subs))
  1.2505 -				end
  1.2506 -		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree list -> prop_tree * (int * (Term.term * prop_tree) list) *)
  1.2507 -		fun term_to_prop_tree_subst t' (idx,subs) bsubs =
  1.2508 -			case t' of
  1.2509 -			(* meta-logical constants *)
  1.2510 -			  Const ("Goal", _) $ t1 =>
  1.2511 -				term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2512 -			| Const ("all", _) $ t1 =>
  1.2513 -				let
  1.2514 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2515 -				in
  1.2516 -					case tree1 of
  1.2517 -					  Node xs =>
  1.2518 +		if is_var t then
  1.2519 +			(case typeof t of
  1.2520 +			  Type (s, Ts) =>
  1.2521 +				(case DatatypePackage.datatype_info thy s of
  1.2522 +				  Some info =>  (* inductive datatype *)
  1.2523 +					let
  1.2524 +						val index               = #index info
  1.2525 +						val descr               = #descr info
  1.2526 +						val (_, dtyps, constrs) = the (assoc (descr, index))
  1.2527 +					in
  1.2528 +						if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
  1.2529 +							raise REFUTE ("var_IDT_printer", "recursive datatype argument")
  1.2530 +						else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
  1.2531 +							None  (* recursive datatype (requires an infinite model) *)
  1.2532 +						else
  1.2533  						let
  1.2534 -							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
  1.2535 -							val fmFalse = list_disjunction (map prop_tree_to_false xs)
  1.2536 +							val (sizes, _) = model
  1.2537 +							val typ_assoc  = dtyps ~~ Ts
  1.2538 +							(* interpretation -> int *)
  1.2539 +							fun index_from_interpretation (Leaf xs) =
  1.2540 +								let
  1.2541 +									val idx = find_index (PropLogic.eval assignment) xs
  1.2542 +								in
  1.2543 +									if idx<0 then
  1.2544 +										raise REFUTE ("var_IDT_printer", "illegal interpretation: no value assigned")
  1.2545 +									else
  1.2546 +										idx
  1.2547 +								end
  1.2548 +							  | index_from_interpretation _ =
  1.2549 +								raise REFUTE ("var_IDT_printer", "interpretation is not a leaf")
  1.2550 +							(* string -> string *)
  1.2551 +							fun unqualify s =
  1.2552 +								implode (snd (take_suffix (fn c => c <> ".") (explode s)))
  1.2553 +							(* DatatypeAux.dtyp -> Term.typ *)
  1.2554 +							fun typ_of_dtyp (DatatypeAux.DtTFree a) =
  1.2555 +								the (assoc (typ_assoc, DatatypeAux.DtTFree a))
  1.2556 +							  | typ_of_dtyp (DatatypeAux.DtRec i) =
  1.2557 +								raise REFUTE ("var_IDT_printer", "recursive datatype")
  1.2558 +							  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
  1.2559 +								Type (s, map typ_of_dtyp ds)
  1.2560 +							fun sum xs     = foldl op+ (0, xs)
  1.2561 +							fun product xs = foldl op* (1, xs)
  1.2562 +							(* power(a,b) computes a^b, for a>=0, b>=0 *)
  1.2563 +							(* int * int -> int *)
  1.2564 +							fun power (a,0) = 1
  1.2565 +							  | power (a,1) = a
  1.2566 +							  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
  1.2567 +							fun size_of_interpretation (Leaf xs) = length xs
  1.2568 +							  | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
  1.2569 +							fun size_of_type T =
  1.2570 +								let
  1.2571 +									val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<IDT>", T))
  1.2572 +								in
  1.2573 +									size_of_interpretation i
  1.2574 +								end
  1.2575 +							(* returns a list with all unit vectors of length n *)
  1.2576 +							(* int -> interpretation list *)
  1.2577 +							fun unit_vectors n =
  1.2578 +							let
  1.2579 +								(* returns the k-th unit vector of length n *)
  1.2580 +								(* int * int -> interpretation *)
  1.2581 +								fun unit_vector (k,n) =
  1.2582 +									Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1.2583 +								(* int -> interpretation list -> interpretation list *)
  1.2584 +								fun unit_vectors_acc k vs =
  1.2585 +									if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1.2586 +							in
  1.2587 +								unit_vectors_acc 1 []
  1.2588 +							end
  1.2589 +							(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1.2590 +							(* 'a -> 'a list list -> 'a list list *)
  1.2591 +							fun cons_list x xss =
  1.2592 +								map (fn xs => x::xs) xss
  1.2593 +							(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1.2594 +							(* int -> 'a list -> 'a list list *)
  1.2595 +							fun pick_all 1 xs =
  1.2596 +								map (fn x => [x]) xs
  1.2597 +							  | pick_all n xs =
  1.2598 +								let val rec_pick = pick_all (n-1) xs in
  1.2599 +									foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1.2600 +								end
  1.2601 +							(* interpretation -> interpretation list *)
  1.2602 +							fun make_constants (Leaf xs) =
  1.2603 +								unit_vectors (length xs)
  1.2604 +							  | make_constants (Node xs) =
  1.2605 +								map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1.2606 +							(* DatatypeAux.dtyp list -> int -> string *)
  1.2607 +							fun string_of_inductive_type_cargs [] n =
  1.2608 +								if n<>0 then
  1.2609 +									raise REFUTE ("var_IDT_printer", "internal error computing the element index for an inductive type")
  1.2610 +								else
  1.2611 +									""
  1.2612 +							  | string_of_inductive_type_cargs (d::ds) n =
  1.2613 +								let
  1.2614 +									val size_ds   = product (map (fn d => size_of_type (typ_of_dtyp d)) ds)
  1.2615 +									val T         = typ_of_dtyp d
  1.2616 +									val (i,_,_)   = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<IDT>", T))
  1.2617 +									val constants = make_constants i
  1.2618 +								in
  1.2619 +									" "
  1.2620 +									^ (print thy model (Free ("<IDT>", T)) (nth_elem (n div size_ds, constants)) assignment)
  1.2621 +									^ (string_of_inductive_type_cargs ds (n mod size_ds))
  1.2622 +								end
  1.2623 +							(* (string * DatatypeAux.dtyp list) list -> int -> string *)
  1.2624 +							fun string_of_inductive_type_constrs [] n =
  1.2625 +								raise REFUTE ("var_IDT_printer", "inductive type has fewer elements than needed")
  1.2626 +							  | string_of_inductive_type_constrs ((c,ds)::cs) n =
  1.2627 +								let
  1.2628 +									val size = product (map (fn d => size_of_type (typ_of_dtyp d)) ds)
  1.2629 +								in
  1.2630 +									if n < size then
  1.2631 +										(unqualify c) ^ (string_of_inductive_type_cargs ds n)
  1.2632 +									else
  1.2633 +										string_of_inductive_type_constrs cs (n - size)
  1.2634 +								end
  1.2635  						in
  1.2636 -							(Leaf [fmTrue, fmFalse], (i1,s1))
  1.2637 +							Some (string_of_inductive_type_constrs constrs (index_from_interpretation intr))
  1.2638  						end
  1.2639 -					| _ =>
  1.2640 -						raise REFUTE ("term_to_prop_tree_subst", "'all' is not followed by a function")
  1.2641 -				end
  1.2642 -			| Const ("==", _) $ t1 $ t2 =>
  1.2643 -				let
  1.2644 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2645 -					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.2646 -					val fmTrue          = prop_tree_equal (tree1,tree2)
  1.2647 -					val fmFalse         = SNot fmTrue
  1.2648 -				in
  1.2649 -					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.2650 -				end
  1.2651 -			| Const ("==>", _) $ t1 $ t2 =>
  1.2652 -				let
  1.2653 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2654 -					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.2655 -					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
  1.2656 -					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
  1.2657 -				in
  1.2658 -					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.2659 -				end
  1.2660 -			(* HOL constants *)
  1.2661 -			| Const ("Trueprop", _) $ t1 =>
  1.2662 -				term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2663 -			| Const ("Not", _) $ t1 =>
  1.2664 -				let
  1.2665 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2666 -					val fmTrue          = prop_tree_to_false tree1
  1.2667 -					val fmFalse         = prop_tree_to_true tree1
  1.2668 -				in
  1.2669 -					(Leaf [fmTrue, fmFalse], (i1,s1))
  1.2670 -				end
  1.2671 -			| Const ("True", _) =>
  1.2672 -				(Leaf [True, False], (idx,subs))
  1.2673 -			| Const ("False", _) =>
  1.2674 -				(Leaf [False, True], (idx,subs))
  1.2675 -			| Const ("All", _) $ t1 =>
  1.2676 -				let
  1.2677 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2678 -				in
  1.2679 -					case tree1 of
  1.2680 -					  Node xs =>
  1.2681 -						let
  1.2682 -							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
  1.2683 -							val fmFalse = list_disjunction (map prop_tree_to_false xs)
  1.2684 -						in
  1.2685 -							(Leaf [fmTrue, fmFalse], (i1,s1))
  1.2686 -						end
  1.2687 -					| _ =>
  1.2688 -						raise REFUTE ("term_to_prop_tree_subst", "'All' is not followed by a function")
  1.2689 -				end
  1.2690 -			| Const ("Ex", _) $ t1 =>
  1.2691 -				let
  1.2692 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2693 -				in
  1.2694 -					case tree1 of
  1.2695 -					  Node xs =>
  1.2696 -						let
  1.2697 -							val fmTrue  = list_disjunction (map prop_tree_to_true xs)
  1.2698 -							val fmFalse = list_conjunction (map prop_tree_to_false xs)
  1.2699 -						in
  1.2700 -							(Leaf [fmTrue, fmFalse], (i1,s1))
  1.2701 -						end
  1.2702 -					| _ =>
  1.2703 -						raise REFUTE ("term_to_prop_tree_subst", "'Ex' is not followed by a function")
  1.2704 -				end
  1.2705 -			| Const ("Ex1", Type ("fun", [Type ("fun", [T, Type ("bool",[])]), Type ("bool",[])])) $ t1 =>
  1.2706 -				(* 'Ex1 t1' is equivalent to 'Ex Abs(x,T,t1' x & All Abs(y,T,t1'' y --> x=y))' *)
  1.2707 -				let
  1.2708 -					val t1'      = Term.incr_bv (1, 0, t1)
  1.2709 -					val t1''     = Term.incr_bv (2, 0, t1)
  1.2710 -					val t_equal  = (HOLogic.eq_const T) $ (Bound 1) $ (Bound 0)
  1.2711 -					val t_unique = (HOLogic.all_const T) $ Abs("y",T,HOLogic.mk_imp (t1'' $ (Bound 0),t_equal))
  1.2712 -					val t_ex1    = (HOLogic.exists_const T) $ Abs("x",T,HOLogic.mk_conj (t1' $ (Bound 0),t_unique))
  1.2713 -				in
  1.2714 -					term_to_prop_tree_subst t_ex1 (idx,subs) bsubs
  1.2715 -				end
  1.2716 -			| Const ("op =", _) $ t1 $ t2 =>
  1.2717 -				let
  1.2718 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2719 -					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.2720 -					val fmTrue          = prop_tree_equal (tree1,tree2)
  1.2721 -					val fmFalse         = SNot fmTrue
  1.2722 -				in
  1.2723 -					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.2724 -				end
  1.2725 -			| Const ("op &", _) $ t1 $ t2 =>
  1.2726 -				let
  1.2727 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2728 -					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.2729 -					val fmTrue          = SAnd (prop_tree_to_true tree1, prop_tree_to_true tree2)
  1.2730 -					val fmFalse         = SOr (prop_tree_to_false tree1, prop_tree_to_false tree2)
  1.2731 -				in
  1.2732 -					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.2733 -				end
  1.2734 -			| Const ("op |", _) $ t1 $ t2 =>
  1.2735 -				let
  1.2736 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2737 -					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.2738 -					val fmTrue          = SOr (prop_tree_to_true tree1, prop_tree_to_true tree2)
  1.2739 -					val fmFalse         = SAnd (prop_tree_to_false tree1, prop_tree_to_false tree2)
  1.2740 -				in
  1.2741 -					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.2742 -				end
  1.2743 -			| Const ("op -->", _) $ t1 $ t2 =>
  1.2744 -				let
  1.2745 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2746 -					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.2747 -					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
  1.2748 -					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
  1.2749 -				in
  1.2750 -					(Leaf [fmTrue, fmFalse], (i2,s2))
  1.2751 -				end
  1.2752 -			(* set constants *)
  1.2753 -			| Const ("Collect", _) $ t1 =>
  1.2754 -				term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2755 -			| Const ("op :", _) $ t1 $ t2 =>
  1.2756 -				term_to_prop_tree_subst (t2 $ t1) (idx,subs) bsubs
  1.2757 -			(* datatype constants *)
  1.2758 -			| Const ("Product_Type.Unity", _) =>
  1.2759 -				(Leaf [True], (idx,subs))
  1.2760 -			(* unknown constants *)
  1.2761 -			| Const (c, _) =>
  1.2762 -				error ("term contains an unknown constant: '" ^ c ^ "'")
  1.2763 -			(* abstractions *)
  1.2764 -			| Abs (_,T,body) =>
  1.2765 -				let
  1.2766 -					val constants       = type_to_constants T us thy cdepth
  1.2767 -					val (trees, substs) = split_list (map (fn c => term_to_prop_tree_subst body (idx,subs) (c::bsubs)) constants)
  1.2768 -				in
  1.2769 -					(* the substitutions in 'substs' are all identical *)
  1.2770 -					(Node trees, hd substs)
  1.2771 -				end
  1.2772 -			(* (free/schematic) variables *)
  1.2773 -			| Free _ =>
  1.2774 -				variable_to_prop_tree_subst t' (idx,subs)
  1.2775 -			| Var _ =>
  1.2776 -				variable_to_prop_tree_subst t' (idx,subs)
  1.2777 -			(* bound variables *)
  1.2778 -			| Bound i =>
  1.2779 -				if (length bsubs) <= i then
  1.2780 -					raise REFUTE ("term_to_prop_tree_subst", "term contains a loose bound variable (with index " ^ (string_of_int i) ^ ")")
  1.2781 -				else
  1.2782 -					(nth_elem (i,bsubs), (idx,subs))
  1.2783 -			(* application *)
  1.2784 -			| t1 $ t2 =>
  1.2785 -				let
  1.2786 -					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1.2787 -					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1.2788 -				in
  1.2789 -					(prop_tree_apply (tree1,tree2), (i2,s2))
  1.2790 -				end
  1.2791 -	in
  1.2792 -		term_to_prop_tree_subst t (1,[]) []
  1.2793 -	end;
  1.2794 -
  1.2795 -(* ------------------------------------------------------------------------- *)
  1.2796 -(* term_to_prop_formula: translates a HOL formula 't' into a propositional   *)
  1.2797 -(*      formula that is satisfiable if and only if 't' has a model of "size" *)
  1.2798 -(*      'us' (where 'us' specifies the number of elements for each free type *)
  1.2799 -(*      variable in 't') and maximal constructor depth 'cdepth'.             *)
  1.2800 -(* ------------------------------------------------------------------------- *)
  1.2801 -
  1.2802 -	(* TODO: shouldn't 'us' also specify the number of elements for schematic type variables? (if so, modify the comment above) *)
  1.2803 -
  1.2804 -	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_formula * (int * (Term.term * prop_tree) list) *)
  1.2805 -
  1.2806 -	fun term_to_prop_formula t us thy cdepth =
  1.2807 -	let
  1.2808 -		val (tr, (idx,subs)) = term_to_prop_tree t us thy cdepth
  1.2809 -		val fm               = prop_tree_to_true tr
  1.2810 -	in
  1.2811 -		if subs=[] then
  1.2812 -			(fm, (idx,subs))
  1.2813 +					end
  1.2814 +				| None => None)
  1.2815 +			| _ => None)
  1.2816  		else
  1.2817 -			(* make sure every tree that is substituted for a term describes a single element *)
  1.2818 -			(SAnd (list_conjunction (map (fn (_,tr) => restrict_to_single_element tr) subs), fm), (idx,subs))
  1.2819 +			None
  1.2820  	end;
  1.2821  
  1.2822  
  1.2823  (* ------------------------------------------------------------------------- *)
  1.2824 -(* INTERFACE, PART 2: FINDING A MODEL                                        *)
  1.2825 +(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
  1.2826 +(* structure                                                                 *)
  1.2827  (* ------------------------------------------------------------------------- *)
  1.2828  
  1.2829  (* ------------------------------------------------------------------------- *)
  1.2830 -(* string_of_universe: prints a universe, i.e. an assignment of sizes for    *)
  1.2831 -(*                     types                                                 *)
  1.2832 -(* thy: the current theory                                                   *)
  1.2833 -(* us : a list containing types together with their size                     *)
  1.2834 -(* ------------------------------------------------------------------------- *)
  1.2835 -
  1.2836 -	(* theory -> (Term.typ * int) list -> string *)
  1.2837 -
  1.2838 -	fun string_of_universe thy [] =
  1.2839 -		"empty universe (no type variables in term)"
  1.2840 -	  | string_of_universe thy us =
  1.2841 -		space_implode ", " (map (fn (T,i) => (Sign.string_of_typ (sign_of thy) T) ^ ": " ^ (string_of_int i)) us);
  1.2842 -
  1.2843 -(* ------------------------------------------------------------------------- *)
  1.2844 -(* string_of_model: prints a model, given by a substitution 'subs' of trees  *)
  1.2845 -(*      of propositional variables and an assignment 'ass' of truth values   *)
  1.2846 -(*      for these variables.                                                 *)
  1.2847 -(* thy   : the current theory                                                *)
  1.2848 -(* us    : universe, specifies the "size" of each type (i.e. type variable)  *)
  1.2849 -(* cdepth: maximal constructor depth for inductive datatypes                 *)
  1.2850 -(* subs  : substitution of trees of propositional formulas (for variables)   *)
  1.2851 -(* ass   : assignment of truth values for boolean variables; see function    *)
  1.2852 -(*         'truth_value' below for its meaning                               *)
  1.2853 +(* Note: the interpreters and printers are used in reverse order; however,   *)
  1.2854 +(*       an interpreter that can handle non-atomic terms ends up being       *)
  1.2855 +(*       applied before other interpreters are applied to subterms!          *)
  1.2856  (* ------------------------------------------------------------------------- *)
  1.2857  
  1.2858 -	(* theory -> (Term.typ * int) list -> int -> (Term.term * prop_formula tree) list -> int list -> string *)
  1.2859 -
  1.2860 -	fun string_of_model thy us cdepth [] ass =
  1.2861 -		"empty interpretation (no free variables in term)"
  1.2862 -	  | string_of_model thy us cdepth subs ass =
  1.2863 -		let
  1.2864 -			(* Sign.sg *)
  1.2865 -			val sg = sign_of thy
  1.2866 -			(* int -> bool *)
  1.2867 -			fun truth_value i =
  1.2868 -				if i mem ass then true
  1.2869 -				else if ~i mem ass then false
  1.2870 -				else error ("SAT solver assignment does not specify a value for variable " ^ (string_of_int i))
  1.2871 -			(* string -> string *)
  1.2872 -			fun strip_leading_quote str =
  1.2873 -				if nth_elem_string(0,str)="'" then
  1.2874 -					String.substring (str, 1, size str - 1)
  1.2875 -				else
  1.2876 -					str;
  1.2877 -			(* prop_formula list -> int *)
  1.2878 -			fun true_index xs =
  1.2879 -				(* returns the (0-based) index of the first true formula in xs *)
  1.2880 -				let fun true_index_acc [] _ =
  1.2881 -					raise REFUTE ("string_of_model::true_index", "no variable was set to true")
  1.2882 -				      | true_index_acc (x::xs) n =
  1.2883 -					case x of
  1.2884 -					  BoolVar i =>
  1.2885 -						if truth_value i then n else true_index_acc xs (n+1)
  1.2886 -					| True =>
  1.2887 -						n
  1.2888 -					| False =>
  1.2889 -						true_index_acc xs (n+1)
  1.2890 -					| _ =>
  1.2891 -						raise REFUTE ("string_of_model::true_index", "formula is not a boolean variable/true/false")
  1.2892 -				in
  1.2893 -					true_index_acc xs 0
  1.2894 -				end
  1.2895 -			(* Term.typ -> int -> prop_tree -> string *)
  1.2896 -			(* prop *)
  1.2897 -			fun string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
  1.2898 -				if truth_value i then "true" else "false"
  1.2899 -			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [True, False]) =
  1.2900 -				"true"
  1.2901 -			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [False, True]) =
  1.2902 -				"false"
  1.2903 -			(* bool *)
  1.2904 -			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
  1.2905 -				if truth_value i then "true" else "false"
  1.2906 -			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [True, False]) =
  1.2907 -				"true"
  1.2908 -			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [False, True]) =
  1.2909 -				"false"
  1.2910 -			(* unit *)
  1.2911 -			  | string_of_prop_tree (Type ("Product_Type.unit",[])) cdepth (Leaf [True]) =
  1.2912 -				"()"
  1.2913 -			  | string_of_prop_tree (Type (s,Ts)) cdepth (Leaf xs) =
  1.2914 -				(case DatatypePackage.datatype_info thy s of
  1.2915 -				   Some info => (* inductive datatype *)
  1.2916 -					let
  1.2917 -						val index               = #index info
  1.2918 -						val descr               = #descr info
  1.2919 -						val (_, dtyps, constrs) = the (assoc (descr, index))
  1.2920 -						val Typs                = dtyps ~~ Ts
  1.2921 -						(* string -> string *)
  1.2922 -						fun unqualify s =
  1.2923 -							implode (snd (take_suffix (fn c => c <> ".") (explode s)))
  1.2924 -						(* DatatypeAux.dtyp -> Term.typ *)
  1.2925 -						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
  1.2926 -							the (assoc (Typs, DatatypeAux.DtTFree a))
  1.2927 -						  | typ_of_dtyp (DatatypeAux.DtRec i) =
  1.2928 -							let
  1.2929 -								val (s, ds, _) = the (assoc (descr, i))
  1.2930 -							in
  1.2931 -								Type (s, map typ_of_dtyp ds)
  1.2932 -							end
  1.2933 -						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
  1.2934 -							Type (s, map typ_of_dtyp ds)
  1.2935 -						(* DatatypeAux.dtyp list -> int -> string *)
  1.2936 -						fun string_of_inductive_type_cargs [] n =
  1.2937 -							if n<>0 then
  1.2938 -								raise REFUTE ("string_of_model", "internal error computing the element index for an inductive type")
  1.2939 -							else
  1.2940 -								""
  1.2941 -						  | string_of_inductive_type_cargs (d::ds) n =
  1.2942 -							let
  1.2943 -								val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
  1.2944 -							in
  1.2945 -								" " ^ (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.2946 -							end
  1.2947 -						(* (string * DatatypeAux.dtyp list) list -> int -> string *)
  1.2948 -						fun string_of_inductive_type_constrs [] n =
  1.2949 -							raise REFUTE ("string_of_model", "inductive type has fewer elements than needed")
  1.2950 -						  | string_of_inductive_type_constrs ((s,ds)::cs) n =
  1.2951 -							let
  1.2952 -								val size = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
  1.2953 -							in
  1.2954 -								if n < size then
  1.2955 -									(unqualify s) ^ (string_of_inductive_type_cargs ds n)
  1.2956 -								else
  1.2957 -									string_of_inductive_type_constrs cs (n - size)
  1.2958 -							end
  1.2959 -					in
  1.2960 -						string_of_inductive_type_constrs constrs (true_index xs)
  1.2961 -					end
  1.2962 -				 | None =>
  1.2963 -					raise REFUTE ("string_of_model", "type contains an unknown type constructor: '" ^ s ^ "'"))
  1.2964 -			(* type variable *)
  1.2965 -			  | string_of_prop_tree (TFree (s,_)) cdepth (Leaf xs) =
  1.2966 -					(strip_leading_quote s) ^ (string_of_int (true_index xs))
  1.2967 -			  | string_of_prop_tree (TVar ((s,_),_)) cdepth (Leaf xs) =
  1.2968 -					(strip_leading_quote s) ^ (string_of_int (true_index xs))
  1.2969 -			(* function or set type *)
  1.2970 -			  | string_of_prop_tree T cdepth (Node xs) =
  1.2971 -				case T of
  1.2972 -				  Type ("fun", [T1,T2]) =>
  1.2973 -					let
  1.2974 -						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.2975 -					in
  1.2976 -						"(" ^ (space_implode ", " strings) ^ ")"
  1.2977 -					end
  1.2978 -				| Type ("set", [T1]) =>
  1.2979 -					let
  1.2980 -						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.2981 -					in
  1.2982 -						"{" ^ (space_implode ", " strings) ^ "}"
  1.2983 -					end
  1.2984 -				| _ => raise REFUTE ("string_of_model::string_of_prop_tree", "not a function/set type")
  1.2985 -			(* Term.term * prop_formula tree -> string *)
  1.2986 -			fun string_of_term_assignment (t,tr) =
  1.2987 -			let
  1.2988 -				val T = case t of
  1.2989 -					  Free (_,T) => T
  1.2990 -					| Var (_,T)  => T
  1.2991 -					| _          => raise REFUTE ("string_of_model::string_of_term_assignment", "term is not a (free or schematic) variable")
  1.2992 -			in
  1.2993 -				(Sign.string_of_term sg t) ^ " = " ^ (string_of_prop_tree T cdepth tr)
  1.2994 -			end
  1.2995 -		in
  1.2996 -			space_implode "\n" (map string_of_term_assignment subs)
  1.2997 -		end;
  1.2998 +	(* (theory -> theory) list *)
  1.2999  
  1.3000 -(* ------------------------------------------------------------------------- *)
  1.3001 -(* find_model: repeatedly calls 'prop_formula_sat_solver' with appropriate   *)
  1.3002 -(*             parameters, and displays the results to the user              *)
  1.3003 -(* params    : list of '(name, value)' pairs used to override default        *)
  1.3004 -(*             parameters                                                    *)
  1.3005 -(*                                                                           *)
  1.3006 -(* This is a brief description of the algorithm implemented:                 *)
  1.3007 -(*                                                                           *)
  1.3008 -(* 1. Let k = max ('minsize',1).                                             *)
  1.3009 -(* 2. Let the universe have k elements.  Find all possible partitions of     *)
  1.3010 -(*    these elements into the basic types occuring in 't' such that no basic *)
  1.3011 -(*    type is empty.                                                         *)
  1.3012 -(* 3. Translate 't' into a propositional formula p s.t. 't' has a model wrt. *)
  1.3013 -(*    the partition chosen in step (2.) if (actually, if and only if) p is   *)
  1.3014 -(*    satisfiable.  To do this, replace quantification by conjunction/       *)
  1.3015 -(*    disjunction over all elements of the type being quantified over.  (If  *)
  1.3016 -(*    p contains more than 'maxvars' boolean variables, terminate.)          *)
  1.3017 -(* 4. Serialize p to a file, and try to find a satisfying assignment for p   *)
  1.3018 -(*    by invoking an external SAT solver.                                    *)
  1.3019 -(* 5. If the SAT solver finds a satisfying assignment for p, translate this  *)
  1.3020 -(*    assignment back into a model for 't'.  Present this model to the user, *)
  1.3021 -(*    then terminate.                                                        *)
  1.3022 -(* 6. As long as there is another partition left, pick it and go back to     *)
  1.3023 -(*    step (3.).                                                             *)
  1.3024 -(* 7. Increase k by 1.  As long as k does not exceed 'maxsize', go back to   *)
  1.3025 -(*    step (2.).                                                             *)
  1.3026 -(*                                                                           *)
  1.3027 -(* The following parameters are currently supported (and required!):         *)
  1.3028 -(*                                                                           *)
  1.3029 -(* Name          Type    Description                                         *)
  1.3030 -(*                                                                           *)
  1.3031 -(* "minsize"     int     Only search for models with size at least           *)
  1.3032 -(*                       'minsize'.                                          *)
  1.3033 -(* "maxsize"     int     If >0, only search for models with size at most     *)
  1.3034 -(*                       'maxsize'.                                          *)
  1.3035 -(* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
  1.3036 -(*                       when transforming the term into a propositional     *)
  1.3037 -(*                       formula.                                            *)
  1.3038 -(* "satfile"     string  Name of the file used to store the propositional    *)
  1.3039 -(*                       formula, i.e. the input to the SAT solver.          *)
  1.3040 -(* "satformat"   string  Format of the SAT solver's input file.  Must be     *)
  1.3041 -(*                       either "cnf", "defcnf", or "sat".  Since "sat" is   *)
  1.3042 -(*                       not supported by most SAT solvers, and "cnf" can    *)
  1.3043 -(*                       cause exponential blowup of the formula, "defcnf"   *)
  1.3044 -(*                       is recommended.                                     *)
  1.3045 -(* "resultfile"  string  Name of the file containing the SAT solver's        *)
  1.3046 -(*                       output.                                             *)
  1.3047 -(* "success"     string  Part of the line in the SAT solver's output that    *)
  1.3048 -(*                       precedes a list of integers representing the        *)
  1.3049 -(*                       satisfying assignment.                              *)
  1.3050 -(* "command"     string  System command used to execute the SAT solver.      *)
  1.3051 -(*                       Note that you if you change 'satfile' or            *)
  1.3052 -(*                       'resultfile', you will also need to change          *)
  1.3053 -(*                       'command'.                                          *)
  1.3054 -(*                                                                           *)
  1.3055 -(* See the Isabelle/Isar theory 'Refute.thy' for reasonable default values.  *)
  1.3056 -(* ------------------------------------------------------------------------- *)
  1.3057 -
  1.3058 -	(* theory -> (string * string) list -> Term.term -> unit *)
  1.3059 -
  1.3060 -	fun find_model thy params t =
  1.3061 -	let
  1.3062 -		(* (string * string) list * (string * string) list -> (string * string) list *)
  1.3063 -		fun add_params (parms, []) =
  1.3064 -			parms
  1.3065 -		  | add_params (parms, defparm::defparms) =
  1.3066 -			add_params (gen_ins (fn (a, b) => (fst a) = (fst b)) (defparm, parms), defparms)
  1.3067 -		(* (string * string) list * string -> int *)
  1.3068 -		fun read_int (parms, name) =
  1.3069 -			case assoc_string (parms, name) of
  1.3070 -			  Some s => (case Int.fromString s of
  1.3071 -				  SOME i => i
  1.3072 -				| NONE   => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
  1.3073 -			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
  1.3074 -		(* (string * string) list * string -> string *)
  1.3075 -		fun read_string (parms, name) =
  1.3076 -			case assoc_string (parms, name) of
  1.3077 -			  Some s => s
  1.3078 -			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
  1.3079 -		(* (string * string) list *)
  1.3080 -		val allparams  = add_params (params, get_default_params thy)
  1.3081 -		(* int *)
  1.3082 -		val minsize    = read_int (allparams, "minsize")
  1.3083 -		val maxsize    = read_int (allparams, "maxsize")
  1.3084 -		val maxvars    = read_int (allparams, "maxvars")
  1.3085 -		(* string *)
  1.3086 -		val satfile    = read_string (allparams, "satfile")
  1.3087 -		val satformat  = read_string (allparams, "satformat")
  1.3088 -		val resultfile = read_string (allparams, "resultfile")
  1.3089 -		val success    = read_string (allparams, "success")
  1.3090 -		val command    = read_string (allparams, "command")
  1.3091 -		(* misc *)
  1.3092 -		val satpath    = Path.unpack satfile
  1.3093 -		val resultpath = Path.unpack resultfile
  1.3094 -		val sg         = sign_of thy
  1.3095 -		(* Term.typ list *)
  1.3096 -		val tvars      = map (fn (i,s) => TVar(i,s)) (term_tvars t)
  1.3097 -		val tfrees     = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
  1.3098 -		(* universe -> int -> bool *)
  1.3099 -		fun find_model_universe u cdepth =
  1.3100 -			let
  1.3101 -				(* given the universe 'u' and constructor depth 'cdepth', translate *)
  1.3102 -        	                (* the term 't' into a propositional formula 'fm'                   *)
  1.3103 -				val (fm,(idx,subs)) = term_to_prop_formula t u thy cdepth
  1.3104 -				val usedvars        = idx-1
  1.3105 -			in
  1.3106 -				(* 'maxvars=0' means "use as many variables as necessary" *)
  1.3107 -				if usedvars>maxvars andalso maxvars<>0 then
  1.3108 -					(
  1.3109 -						(* too many variables used: terminate *)
  1.3110 -						writeln ("\nSearch terminated: " ^ (string_of_int usedvars) ^ " boolean variables used (only " ^ (string_of_int maxvars) ^ " allowed).");
  1.3111 -						true
  1.3112 -					)
  1.3113 -				else
  1.3114 -					(* pass the formula 'fm' to an external SAT solver *)
  1.3115 -					case prop_formula_sat_solver fm satpath satformat resultpath success command of
  1.3116 -					  None =>
  1.3117 -						(* no model found *)
  1.3118 -						false
  1.3119 -					| Some assignment =>
  1.3120 -						(* model found: terminate *)
  1.3121 -						(
  1.3122 -							writeln ("\nModel found:\n" ^ (string_of_universe thy u) ^ "\n" ^ (string_of_model thy u cdepth subs assignment));
  1.3123 -							true
  1.3124 -						)
  1.3125 -			end
  1.3126 -		(* universe list -> int -> bool *)
  1.3127 -		fun find_model_universes [] cdepth =
  1.3128 -			(
  1.3129 -				std_output "\n";
  1.3130 -				false
  1.3131 -			)
  1.3132 -		  | find_model_universes (u::us) cdepth =
  1.3133 -			(
  1.3134 -				std_output ".";
  1.3135 -				((if find_model_universe u cdepth then
  1.3136 -					(* terminate *)
  1.3137 -					true
  1.3138 -				else
  1.3139 -					(* continue search with the next universe *)
  1.3140 -					find_model_universes us cdepth)
  1.3141 -				handle EMPTY_DATATYPE => (std_output "[empty inductive type (constructor depth too small)]\n"; false))
  1.3142 -			)
  1.3143 -		(* int * int -> unit *)
  1.3144 -		fun find_model_from_to (min,max) =
  1.3145 -			(* 'max=0' means "search for arbitrary large models" *)
  1.3146 -			if min>max andalso max<>0 then
  1.3147 -				writeln ("Search terminated: no model found.")
  1.3148 -			else
  1.3149 -			(
  1.3150 -				std_output ("Searching for a model of size " ^ (string_of_int min));
  1.3151 -				if find_model_universes (make_universes tfrees min) min then
  1.3152 -					(* terminate *)
  1.3153 -					()
  1.3154 -				else
  1.3155 -					(* continue search with increased size *)
  1.3156 -					find_model_from_to (min+1, max)
  1.3157 -			)
  1.3158 -	in
  1.3159 -		writeln ("Trying to find a model of: " ^ (Sign.string_of_term sg t));
  1.3160 -		if tvars<>[] then
  1.3161 -			(* TODO: deal with schematic type variables in a better way, if possible *)
  1.3162 -			error "term contains schematic type variables"
  1.3163 -		else
  1.3164 -		(
  1.3165 -			if minsize<1 then
  1.3166 -				writeln ("'minsize' is less than 1; starting search with size 1.")
  1.3167 -			else
  1.3168 -				();
  1.3169 -			if maxsize<max (minsize,1) andalso maxsize<>0 then
  1.3170 -				writeln ("'maxsize' is less than 'minsize': no model found.")
  1.3171 -			else
  1.3172 -				find_model_from_to (max (minsize,1), maxsize)
  1.3173 -		)
  1.3174 -	end;
  1.3175 -
  1.3176 -(* ------------------------------------------------------------------------- *)
  1.3177 -(* refute_term: calls 'find_model' on the negation of a term                 *)
  1.3178 -(* params     : list of '(name, value)' pairs used to override default       *)
  1.3179 -(*              parameters                                                   *)
  1.3180 -(* ------------------------------------------------------------------------- *)
  1.3181 -
  1.3182 -	(* theory -> (string * string) list -> Term.term -> unit *)
  1.3183 -
  1.3184 -	fun refute_term thy params t =
  1.3185 -	let
  1.3186 -		(* TODO: schematic type variables? *)
  1.3187 -		val negation = close_vars (HOLogic.Not $ t)
  1.3188 -		(* If 't' is of type 'propT' (rather than 'boolT'), applying *)
  1.3189 -		(* 'HOLogic.Not' is not type-correct.  However, this isn't   *)
  1.3190 -		(* really a problem as long as 'find_model' still interprets *)
  1.3191 -		(* the resulting term correctly, without checking its type.  *)
  1.3192 -	in
  1.3193 -		find_model thy params negation
  1.3194 -	end;
  1.3195 -
  1.3196 -(* ------------------------------------------------------------------------- *)
  1.3197 -(* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
  1.3198 -(* params        : list of '(name, value)' pairs used to override default    *)
  1.3199 -(*                 parameters                                                *)
  1.3200 -(* subgoal       : 0-based index specifying the subgoal number               *)
  1.3201 -(* ------------------------------------------------------------------------- *)
  1.3202 -
  1.3203 -	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
  1.3204 -
  1.3205 -	fun refute_subgoal thy params thm subgoal =
  1.3206 -		refute_term thy params (nth_elem (subgoal, prems_of thm));
  1.3207 +	val setup =
  1.3208 +		[RefuteData.init,
  1.3209 +		 add_interpreter "var_typevar"   var_typevar_interpreter,
  1.3210 +		 add_interpreter "var_funtype"   var_funtype_interpreter,
  1.3211 +		 add_interpreter "var_settype"   var_settype_interpreter,
  1.3212 +		 add_interpreter "boundvar"      boundvar_interpreter,
  1.3213 +		 add_interpreter "abstraction"   abstraction_interpreter,
  1.3214 +		 add_interpreter "apply"         apply_interpreter,
  1.3215 +		 add_interpreter "const_unfold"  const_unfold_interpreter,
  1.3216 +		 add_interpreter "Pure"          Pure_interpreter,
  1.3217 +		 add_interpreter "HOLogic"       HOLogic_interpreter,
  1.3218 +		 add_interpreter "IDT"           IDT_interpreter,
  1.3219 +		 add_printer "var_typevar"   var_typevar_printer,
  1.3220 +		 add_printer "var_funtype"   var_funtype_printer,
  1.3221 +		 add_printer "var_settype"   var_settype_printer,
  1.3222 +		 add_printer "HOLogic"       HOLogic_printer,
  1.3223 +		 add_printer "var_IDT"       var_IDT_printer];
  1.3224  
  1.3225  end