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