src/HOL/Tools/refute.ML
author webertj
Mon Aug 09 15:27:27 2004 +0200 (2004-08-09)
changeset 15125 5224130bc0d6
parent 14984 edbc81e60809
child 15280 e0e9bf44afad
permissions -rw-r--r--
warning for recursion over IDTs added
     1 (*  Title:      HOL/Tools/refute.ML
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2003-2004
     5 
     6 Finite model generation for HOL formulas, using a SAT solver.
     7 *)
     8 
     9 (* TODO: case, recursion, size for IDTs are not supported yet *)
    10 
    11 (* ------------------------------------------------------------------------- *)
    12 (* Declares the 'REFUTE' signature as well as a structure 'Refute'.          *)
    13 (* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'.  *)
    14 (* ------------------------------------------------------------------------- *)
    15 
    16 signature REFUTE =
    17 sig
    18 
    19 	exception REFUTE of string * string
    20 
    21 (* ------------------------------------------------------------------------- *)
    22 (* Model/interpretation related code (translation HOL -> propositional logic *)
    23 (* ------------------------------------------------------------------------- *)
    24 
    25 	type params
    26 	type interpretation
    27 	type model
    28 	type arguments
    29 
    30 	exception CANNOT_INTERPRET of Term.term
    31 	exception MAXVARS_EXCEEDED
    32 
    33 	val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory
    34 	val add_printer     : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option) -> theory -> theory
    35 
    36 	val interpret : theory -> model -> arguments -> Term.term -> (interpretation * model * arguments)  (* exception CANNOT_INTERPRET *)
    37 
    38 	val print       : theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term
    39 	val print_model : theory -> model -> (int -> bool) -> string
    40 
    41 (* ------------------------------------------------------------------------- *)
    42 (* Interface                                                                 *)
    43 (* ------------------------------------------------------------------------- *)
    44 
    45 	val set_default_param  : (string * string) -> theory -> theory
    46 	val get_default_param  : theory -> string -> string option
    47 	val get_default_params : theory -> (string * string) list
    48 	val actual_params      : theory -> (string * string) list -> params
    49 
    50 	val find_model : theory -> params -> Term.term -> bool -> unit
    51 
    52 	val satisfy_term   : theory -> (string * string) list -> Term.term -> unit  (* tries to find a model for a formula *)
    53 	val refute_term    : theory -> (string * string) list -> Term.term -> unit  (* tries to find a model that refutes a formula *)
    54 	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
    55 
    56 	val setup : (theory -> theory) list
    57 end;
    58 
    59 structure Refute : REFUTE =
    60 struct
    61 
    62 	open PropLogic;
    63 
    64 	(* We use 'REFUTE' only for internal error conditions that should    *)
    65 	(* never occur in the first place (i.e. errors caused by bugs in our *)
    66 	(* code).  Otherwise (e.g. to indicate invalid input data) we use    *)
    67 	(* 'error'.                                                          *)
    68 	exception REFUTE of string * string;  (* ("in function", "cause") *)
    69 
    70 	exception CANNOT_INTERPRET of Term.term;
    71 
    72 	(* should be raised by an interpreter when more variables would be *)
    73 	(* required than allowed by 'maxvars'                              *)
    74 	exception MAXVARS_EXCEEDED;
    75 
    76 (* ------------------------------------------------------------------------- *)
    77 (* TREES                                                                     *)
    78 (* ------------------------------------------------------------------------- *)
    79 
    80 (* ------------------------------------------------------------------------- *)
    81 (* tree: implements an arbitrarily (but finitely) branching tree as a list   *)
    82 (*       of (lists of ...) elements                                          *)
    83 (* ------------------------------------------------------------------------- *)
    84 
    85 	datatype 'a tree =
    86 		  Leaf of 'a
    87 		| Node of ('a tree) list;
    88 
    89 	(* ('a -> 'b) -> 'a tree -> 'b tree *)
    90 
    91 	fun tree_map f tr =
    92 		case tr of
    93 		  Leaf x  => Leaf (f x)
    94 		| Node xs => Node (map (tree_map f) xs);
    95 
    96 	(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
    97 
    98 	fun tree_foldl f =
    99 	let
   100 		fun itl (e, Leaf x)  = f(e,x)
   101 		  | itl (e, Node xs) = foldl (tree_foldl f) (e,xs)
   102 	in
   103 		itl
   104 	end;
   105 
   106 	(* 'a tree * 'b tree -> ('a * 'b) tree *)
   107 
   108 	fun tree_pair (t1,t2) =
   109 		case t1 of
   110 		  Leaf x =>
   111 			(case t2 of
   112 				  Leaf y => Leaf (x,y)
   113 				| Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)"))
   114 		| Node xs =>
   115 			(case t2 of
   116 				  (* '~~' will raise an exception if the number of branches in   *)
   117 				  (* both trees is different at the current node                 *)
   118 				  Node ys => Node (map tree_pair (xs ~~ ys))
   119 				| Leaf _  => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
   120 
   121 
   122 (* ------------------------------------------------------------------------- *)
   123 (* params: parameters that control the translation into a propositional      *)
   124 (*         formula/model generation                                          *)
   125 (*                                                                           *)
   126 (* The following parameters are supported (and required (!), except for      *)
   127 (* "sizes"):                                                                 *)
   128 (*                                                                           *)
   129 (* Name          Type    Description                                         *)
   130 (*                                                                           *)
   131 (* "sizes"       (string * int) list                                         *)
   132 (*                       Size of ground types (e.g. 'a=2), or depth of IDTs. *)
   133 (* "minsize"     int     If >0, minimal size of each ground type/IDT depth.  *)
   134 (* "maxsize"     int     If >0, maximal size of each ground type/IDT depth.  *)
   135 (* "maxvars"     int     If >0, use at most 'maxvars' Boolean variables      *)
   136 (*                       when transforming the term into a propositional     *)
   137 (*                       formula.                                            *)
   138 (* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
   139 (* "satsolver"   string  SAT solver to be used.                              *)
   140 (* ------------------------------------------------------------------------- *)
   141 
   142 	type params =
   143 		{
   144 			sizes    : (string * int) list,
   145 			minsize  : int,
   146 			maxsize  : int,
   147 			maxvars  : int,
   148 			maxtime  : int,
   149 			satsolver: string
   150 		};
   151 
   152 (* ------------------------------------------------------------------------- *)
   153 (* interpretation: a term's interpretation is given by a variable of type    *)
   154 (*                 'interpretation'                                          *)
   155 (* ------------------------------------------------------------------------- *)
   156 
   157 	type interpretation =
   158 		prop_formula list tree;
   159 
   160 (* ------------------------------------------------------------------------- *)
   161 (* model: a model specifies the size of types and the interpretation of      *)
   162 (*        terms                                                              *)
   163 (* ------------------------------------------------------------------------- *)
   164 
   165 	type model =
   166 		(Term.typ * int) list * (Term.term * interpretation) list;
   167 
   168 (* ------------------------------------------------------------------------- *)
   169 (* arguments: additional arguments required during interpretation of terms   *)
   170 (* ------------------------------------------------------------------------- *)
   171 
   172 	type arguments =
   173 		{
   174 			(* just passed unchanged from 'params' *)
   175 			maxvars   : int,
   176 			(* these may change during the translation *)
   177 			next_idx  : int,
   178 			bounds    : interpretation list,
   179 			wellformed: prop_formula
   180 		};
   181 
   182 
   183 	structure RefuteDataArgs =
   184 	struct
   185 		val name = "HOL/refute";
   186 		type T =
   187 			{interpreters: (string * (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option)) list,
   188 			 printers: (string * (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option)) list,
   189 			 parameters: string Symtab.table};
   190 		val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
   191 		val copy = I;
   192 		val prep_ext = I;
   193 		fun merge
   194 			({interpreters = in1, printers = pr1, parameters = pa1},
   195 			 {interpreters = in2, printers = pr2, parameters = pa2}) =
   196 			{interpreters = rev (merge_alists (rev in1) (rev in2)),
   197 			 printers = rev (merge_alists (rev pr1) (rev pr2)),
   198 			 parameters = Symtab.merge (op=) (pa1, pa2)};
   199 		fun print sg {interpreters, printers, parameters} =
   200 			Pretty.writeln (Pretty.chunks
   201 				[Pretty.strs ("default parameters:" :: flat (map (fn (name,value) => [name, "=", value]) (Symtab.dest parameters))),
   202 				 Pretty.strs ("interpreters:" :: map fst interpreters),
   203 				 Pretty.strs ("printers:" :: map fst printers)]);
   204 	end;
   205 
   206 	structure RefuteData = TheoryDataFun(RefuteDataArgs);
   207 
   208 
   209 (* ------------------------------------------------------------------------- *)
   210 (* interpret: tries to interpret the term 't' using a suitable interpreter;  *)
   211 (*            returns the interpretation and a (possibly extended) model     *)
   212 (*            that keeps track of the interpretation of subterms             *)
   213 (* Note: exception 'CANNOT_INTERPRET t' is raised if the term cannot be      *)
   214 (*       interpreted by any interpreter                                      *)
   215 (* ------------------------------------------------------------------------- *)
   216 
   217 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) *)
   218 
   219 	fun interpret thy model args t =
   220 		(case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of
   221 		  None   => raise (CANNOT_INTERPRET t)
   222 		| Some x => x);
   223 
   224 (* ------------------------------------------------------------------------- *)
   225 (* print: tries to convert the constant denoted by the term 't' into a term  *)
   226 (*        using a suitable printer                                           *)
   227 (* ------------------------------------------------------------------------- *)
   228 
   229 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term *)
   230 
   231 	fun print thy model t intr assignment =
   232 		(case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of
   233 		  None   => Const ("<<no printer available>>", fastype_of t)
   234 		| Some x => x);
   235 
   236 (* ------------------------------------------------------------------------- *)
   237 (* print_model: turns the model into a string, using a fixed interpretation  *)
   238 (*              (given by an assignment for Boolean variables) and suitable  *)
   239 (*              printers                                                     *)
   240 (* ------------------------------------------------------------------------- *)
   241 
   242 	(* theory -> model -> (int -> bool) -> string *)
   243 
   244 	fun print_model thy model assignment =
   245 	let
   246 		val (typs, terms) = model
   247 		val typs_msg =
   248 			if null typs then
   249 				"empty universe (no type variables in term)\n"
   250 			else
   251 				"Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n"
   252 		val show_consts_msg =
   253 			if not (!show_consts) andalso Library.exists (is_Const o fst) terms then
   254 				"set \"show_consts\" to show the interpretation of constants\n"
   255 			else
   256 				""
   257 		val terms_msg =
   258 			if null terms then
   259 				"empty interpretation (no free variables in term)\n"
   260 			else
   261 				space_implode "\n" (mapfilter (fn (t,intr) =>
   262 					(* print constants only if 'show_consts' is true *)
   263 					if (!show_consts) orelse not (is_Const t) then
   264 						Some (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment))
   265 					else
   266 						None) terms) ^ "\n"
   267 	in
   268 		typs_msg ^ show_consts_msg ^ terms_msg
   269 	end;
   270 
   271 
   272 (* ------------------------------------------------------------------------- *)
   273 (* PARAMETER MANAGEMENT                                                      *)
   274 (* ------------------------------------------------------------------------- *)
   275 
   276 	(* string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory *)
   277 
   278 	fun add_interpreter name f thy =
   279 	let
   280 		val {interpreters, printers, parameters} = RefuteData.get thy
   281 	in
   282 		case assoc (interpreters, name) of
   283 		  None   => RefuteData.put {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} thy
   284 		| Some _ => error ("Interpreter " ^ name ^ " already declared")
   285 	end;
   286 
   287 	(* string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option) -> theory -> theory *)
   288 
   289 	fun add_printer name f thy =
   290 	let
   291 		val {interpreters, printers, parameters} = RefuteData.get thy
   292 	in
   293 		case assoc (printers, name) of
   294 		  None   => RefuteData.put {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} thy
   295 		| Some _ => error ("Printer " ^ name ^ " already declared")
   296 	end;
   297 
   298 (* ------------------------------------------------------------------------- *)
   299 (* set_default_param: stores the '(name, value)' pair in RefuteData's        *)
   300 (*                    parameter table                                        *)
   301 (* ------------------------------------------------------------------------- *)
   302 
   303 	(* (string * string) -> theory -> theory *)
   304 
   305 	fun set_default_param (name, value) thy =
   306 	let
   307 		val {interpreters, printers, parameters} = RefuteData.get thy
   308 	in
   309 		case Symtab.lookup (parameters, name) of
   310 		  None   => RefuteData.put
   311 			{interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy
   312 		| Some _ => RefuteData.put
   313 			{interpreters = interpreters, printers = printers, parameters = Symtab.update ((name, value), parameters)} thy
   314 	end;
   315 
   316 (* ------------------------------------------------------------------------- *)
   317 (* get_default_param: retrieves the value associated with 'name' from        *)
   318 (*                    RefuteData's parameter table                           *)
   319 (* ------------------------------------------------------------------------- *)
   320 
   321 	(* theory -> string -> string option *)
   322 
   323 	fun get_default_param thy name = Symtab.lookup ((#parameters o RefuteData.get) thy, name);
   324 
   325 (* ------------------------------------------------------------------------- *)
   326 (* get_default_params: returns a list of all '(name, value)' pairs that are  *)
   327 (*                     stored in RefuteData's parameter table                *)
   328 (* ------------------------------------------------------------------------- *)
   329 
   330 	(* theory -> (string * string) list *)
   331 
   332 	fun get_default_params thy = (Symtab.dest o #parameters o RefuteData.get) thy;
   333 
   334 (* ------------------------------------------------------------------------- *)
   335 (* actual_params: takes a (possibly empty) list 'params' of parameters that  *)
   336 (*      override the default parameters currently specified in 'thy', and    *)
   337 (*      returns a record that can be passed to 'find_model'.                 *)
   338 (* ------------------------------------------------------------------------- *)
   339 
   340 	(* theory -> (string * string) list -> params *)
   341 
   342 	fun actual_params thy override =
   343 	let
   344 		(* (string * string) list * string -> int *)
   345 		fun read_int (parms, name) =
   346 			case assoc_string (parms, name) of
   347 			  Some s => (case Int.fromString s of
   348 				  SOME i => i
   349 				| NONE   => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value"))
   350 			| None   => error ("parameter " ^ quote name ^ " must be assigned a value")
   351 		(* (string * string) list * string -> string *)
   352 		fun read_string (parms, name) =
   353 			case assoc_string (parms, name) of
   354 			  Some s => s
   355 			| None   => error ("parameter " ^ quote name ^ " must be assigned a value")
   356 		(* (string * string) list *)
   357 		val allparams = override @ (get_default_params thy)  (* 'override' first, defaults last *)
   358 		(* int *)
   359 		val minsize   = read_int (allparams, "minsize")
   360 		val maxsize   = read_int (allparams, "maxsize")
   361 		val maxvars   = read_int (allparams, "maxvars")
   362       val maxtime   = read_int (allparams, "maxtime")
   363 		(* string *)
   364 		val satsolver = read_string (allparams, "satsolver")
   365 		(* all remaining parameters of the form "string=int" are collected in  *)
   366 		(* 'sizes'                                                             *)
   367 		(* TODO: it is currently not possible to specify a size for a type     *)
   368 		(*       whose name is one of the other parameters (e.g. 'maxvars')    *)
   369 		(* (string * int) list *)
   370 		val sizes     = mapfilter
   371 			(fn (name,value) => (case Int.fromString value of SOME i => Some (name, i) | NONE => None))
   372 			(filter (fn (name,_) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" andalso name<>"satsolver")
   373 				allparams)
   374 	in
   375 		{sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, maxtime=maxtime, satsolver=satsolver}
   376 	end;
   377 
   378 
   379 (* ------------------------------------------------------------------------- *)
   380 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
   381 (* ------------------------------------------------------------------------- *)
   382 
   383 (* ------------------------------------------------------------------------- *)
   384 (* collect_axioms: collects (monomorphic, universally quantified versions    *)
   385 (*                 of) all HOL axioms that are relevant w.r.t 't'            *)
   386 (* ------------------------------------------------------------------------- *)
   387 
   388 	(* TODO: to make the collection of axioms more easily extensible, this    *)
   389 	(*       function could be based on user-supplied "axiom collectors",     *)
   390 	(*       similar to 'interpret'/interpreters or 'print'/printers          *)
   391 
   392 	(* theory -> Term.term -> Term.term list *)
   393 
   394 	(* Which axioms are "relevant" for a particular term/type goes hand in    *)
   395 	(* hand with the interpretation of that term/type by its interpreter (see *)
   396 	(* way below): if the interpretation respects an axiom anyway, the axiom  *)
   397 	(* does not need to be added as a constraint here.                        *)
   398 
   399 	(* When an axiom is added as relevant, further axioms may need to be      *)
   400 	(* added as well (e.g. when a constant is defined in terms of other       *)
   401 	(* constants).  To avoid infinite recursion (which should not happen for  *)
   402 	(* constants anyway, but it could happen for "typedef"-related axioms,    *)
   403 	(* since they contain the type again), we use an accumulator 'axs' and    *)
   404 	(* add a relevant axiom only if it is not in 'axs' yet.                   *)
   405 
   406 	fun collect_axioms thy t =
   407 	let
   408 		val _ = immediate_output "Adding axioms..."
   409 		(* (string * Term.term) list *)
   410 		val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
   411 		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
   412 		(* 't' has a (possibly) more general type, the schematic type          *)
   413 		(* variables in 't' are instantiated to match the type 'T'             *)
   414 		(* (string * Term.typ) * Term.term -> Term.term *)
   415 		fun specialize_type ((s, T), t) =
   416 		let
   417 			fun find_typeSubs (Const (s', T')) =
   418 				(if s=s' then
   419 					Some (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T)))
   420 				else
   421 					None
   422 				handle Type.TYPE_MATCH => None)
   423 			  | find_typeSubs (Free _)           = None
   424 			  | find_typeSubs (Var _)            = None
   425 			  | find_typeSubs (Bound _)          = None
   426 			  | find_typeSubs (Abs (_, _, body)) = find_typeSubs body
   427 			  | find_typeSubs (t1 $ t2)          = (case find_typeSubs t1 of Some x => Some x | None => find_typeSubs t2)
   428 			val typeSubs = (case find_typeSubs t of
   429 				  Some x => x
   430 				| None   => raise REFUTE ("collect_axioms", "no type instantiation found for " ^ quote s ^ " in " ^ Sign.string_of_term (sign_of thy) t))
   431 		in
   432 			map_term_types
   433 				(map_type_tvar
   434 					(fn (v,_) =>
   435 						case Vartab.lookup (typeSubs, v) of
   436 						  None =>
   437 							(* schematic type variable not instantiated *)
   438 							raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")")
   439 						| Some typ =>
   440 							typ))
   441 					t
   442 		end
   443 		(* Term.term list * Term.typ -> Term.term list *)
   444 		fun collect_type_axioms (axs, T) =
   445 			case T of
   446 			(* simple types *)
   447 			  Type ("prop", [])      => axs
   448 			| Type ("fun", [T1, T2]) => collect_type_axioms (collect_type_axioms (axs, T1), T2)
   449 			| Type ("set", [T1])     => collect_type_axioms (axs, T1)
   450 			| Type (s, Ts)           =>
   451 				let
   452 					(* look up the definition of a type, as created by "typedef" *)
   453 					(* (string * Term.term) list -> (string * Term.term) option *)
   454 					fun get_typedefn [] =
   455 						None
   456 					  | get_typedefn ((axname,ax)::axms) =
   457 						(let
   458 							(* Term.term -> Term.typ option *)
   459 							fun type_of_type_definition (Const (s', T')) =
   460 								if s'="Typedef.type_definition" then
   461 									Some T'
   462 								else
   463 									None
   464 							  | type_of_type_definition (Free _)           = None
   465 							  | type_of_type_definition (Var _)            = None
   466 							  | type_of_type_definition (Bound _)          = None
   467 							  | type_of_type_definition (Abs (_, _, body)) = type_of_type_definition body
   468 							  | type_of_type_definition (t1 $ t2)          = (case type_of_type_definition t1 of Some x => Some x | None => type_of_type_definition t2)
   469 						in
   470 							case type_of_type_definition ax of
   471 							  Some T' =>
   472 								let
   473 									val T''      = (domain_type o domain_type) T'
   474 									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', T))
   475 									val unvar_ax = map_term_types
   476 										(map_type_tvar
   477 											(fn (v,_) =>
   478 												case Vartab.lookup (typeSubs, v) of
   479 												  None =>
   480 													(* schematic type variable not instantiated *)
   481 													raise ERROR
   482 												| Some typ =>
   483 													typ))
   484 										ax
   485 								in
   486 									Some (axname, unvar_ax)
   487 								end
   488 							| None =>
   489 								get_typedefn axms
   490 						end
   491 						handle ERROR           => get_typedefn axms
   492 						     | MATCH           => get_typedefn axms
   493 						     | Type.TYPE_MATCH => get_typedefn axms)
   494 				in
   495 					case DatatypePackage.datatype_info thy s of
   496 					  Some info =>  (* inductive datatype *)
   497 							(* only collect relevant type axioms for the argument types *)
   498 							foldl collect_type_axioms (axs, Ts)
   499 					| None =>
   500 						(case get_typedefn axioms of
   501 						  Some (axname, ax) => 
   502 							if mem_term (ax, axs) then
   503 								(* collect relevant type axioms for the argument types *)
   504 								foldl collect_type_axioms (axs, Ts)
   505 							else
   506 								(immediate_output (" " ^ axname);
   507 								collect_term_axioms (ax :: axs, ax))
   508 						| None =>
   509 							(* at least collect relevant type axioms for the argument types *)
   510 							foldl collect_type_axioms (axs, Ts))
   511 				end
   512 			(* TODO: include sort axioms *)
   513 			| TFree (_, sorts)       => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
   514 			| TVar  (_, sorts)       => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
   515 		(* Term.term list * Term.term -> Term.term list *)
   516 		and collect_term_axioms (axs, t) =
   517 			case t of
   518 			(* Pure *)
   519 			  Const ("all", _)                => axs
   520 			| Const ("==", _)                 => axs
   521 			| Const ("==>", _)                => axs
   522 			(* HOL *)
   523 			| Const ("Trueprop", _)           => axs
   524 			| Const ("Not", _)                => axs
   525 			| Const ("True", _)               => axs  (* redundant, since 'True' is also an IDT constructor *)
   526 			| Const ("False", _)              => axs  (* redundant, since 'False' is also an IDT constructor *)
   527 			| Const ("arbitrary", T)          => collect_type_axioms (axs, T)
   528 			| Const ("The", T)                =>
   529 				let
   530 					val ax = specialize_type (("The", T), (the o assoc) (axioms, "HOL.the_eq_trivial"))
   531 				in
   532 					if mem_term (ax, axs) then
   533 						collect_type_axioms (axs, T)
   534 					else
   535 						(immediate_output " HOL.the_eq_trivial";
   536 						collect_term_axioms (ax :: axs, ax))
   537 				end
   538 			| Const ("Hilbert_Choice.Eps", T) =>
   539 				let
   540 					val ax = specialize_type (("Hilbert_Choice.Eps", T), (the o assoc) (axioms, "Hilbert_Choice.someI"))
   541 				in
   542 					if mem_term (ax, axs) then
   543 						collect_type_axioms (axs, T)
   544 					else
   545 						(immediate_output " Hilbert_Choice.someI";
   546 						collect_term_axioms (ax :: axs, ax))
   547 				end
   548 			| Const ("All", _) $ t1           => collect_term_axioms (axs, t1)
   549 			| Const ("Ex", _) $ t1            => collect_term_axioms (axs, t1)
   550 			| Const ("op =", T)               => collect_type_axioms (axs, T)
   551 			| Const ("op &", _)               => axs
   552 			| Const ("op |", _)               => axs
   553 			| Const ("op -->", _)             => axs
   554 			(* sets *)
   555 			| Const ("Collect", T)            => collect_type_axioms (axs, T)
   556 			| Const ("op :", T)               => collect_type_axioms (axs, T)
   557 			(* other optimizations *)
   558 			| Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
   559 			(* simply-typed lambda calculus *)
   560 			| Const (s, T)                    =>
   561 				let
   562 					(* look up the definition of a constant, as created by "constdefs" *)
   563 					(* string -> Term.typ -> (string * Term.term) list -> (string * Term.term) option *)
   564 					fun get_defn [] =
   565 						None
   566 					  | get_defn ((axname,ax)::axms) =
   567 						(let
   568 							val (lhs, _) = Logic.dest_equals ax  (* equations only *)
   569 							val c        = head_of lhs
   570 							val (s', T') = dest_Const c
   571 						in
   572 							if s=s' then
   573 								let
   574 									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))
   575 									val unvar_ax = map_term_types
   576 										(map_type_tvar
   577 											(fn (v,_) =>
   578 												case Vartab.lookup (typeSubs, v) of
   579 												  None =>
   580 													(* schematic type variable not instantiated *)
   581 													raise ERROR
   582 												| Some typ =>
   583 													typ))
   584 										ax
   585 								in
   586 									Some (axname, unvar_ax)
   587 								end
   588 							else
   589 								get_defn axms
   590 						end
   591 						handle ERROR           => get_defn axms
   592 						     | TERM _          => get_defn axms
   593 						     | Type.TYPE_MATCH => get_defn axms)
   594 						(* unit -> bool *)
   595 						fun is_IDT_constructor () =
   596 							(case body_type T of
   597 							  Type (s', _) =>
   598 								(case DatatypePackage.constrs_of thy s' of
   599 								  Some constrs =>
   600 									Library.exists (fn c =>
   601 										(case c of
   602 										  Const (cname, ctype) =>
   603 											cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype)
   604 										| _ =>
   605 											raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
   606 										constrs
   607 								| None =>
   608 									false)
   609 							| _  =>
   610 								false)
   611 						(* unit -> bool *)
   612 						fun is_IDT_recursor () =
   613 							(* the type of a recursion operator: [T1,...,Tn,IDT]--->TResult (where *)
   614 							(* the T1,...,Tn depend on the types of the datatype's constructors)   *)
   615 							((case last_elem (binder_types T) of
   616 							  Type (s', _) =>
   617 								(case DatatypePackage.datatype_info thy s' of
   618 								  Some info =>
   619 									(* TODO: I'm not quite sure if comparing the names is sufficient, or if *)
   620 									(*       we should also check the type                                  *)
   621 									s mem (#rec_names info)
   622 								| None =>  (* not an inductive datatype *)
   623 									false)
   624 							| _ =>  (* a (free or schematic) type variable *)
   625 								false)
   626 							handle LIST "last_elem" => false)  (* not even a function type *)
   627 				in
   628 					if is_IDT_constructor () then
   629 						(* only collect relevant type axioms *)
   630 						collect_type_axioms (axs, T)
   631 					else if is_IDT_recursor () then (
   632 						(* TODO: we must add the definition of the recursion operator to the axioms, or *)
   633 						(*       (better yet, since simply unfolding the definition won't work for      *)
   634 						(*       initial fragments of recursive IDTs) write an interpreter that         *)
   635 						(*       respects it                                                            *)
   636 						warning "Term contains recursion over a datatype; countermodel(s) may be spurious!";
   637 						(* only collect relevant type axioms *)
   638 						collect_type_axioms (axs, T)
   639 					) else
   640 						(case get_defn axioms of
   641 						  Some (axname, ax) => 
   642 							if mem_term (ax, axs) then
   643 								(* collect relevant type axioms *)
   644 								collect_type_axioms (axs, T)
   645 							else
   646 								(immediate_output (" " ^ axname);
   647 								collect_term_axioms (ax :: axs, ax))
   648 						| None =>
   649 							(* collect relevant type axioms *)
   650 							collect_type_axioms (axs, T))
   651 				end
   652 			| Free (_, T)                     => collect_type_axioms (axs, T)
   653 			| Var (_, T)                      => collect_type_axioms (axs, T)
   654 			| Bound i                         => axs
   655 			| Abs (_, T, body)                => collect_term_axioms (collect_type_axioms (axs, T), body)
   656 			| t1 $ t2                         => collect_term_axioms (collect_term_axioms (axs, t1), t2)
   657 		(* universal closure over schematic variables *)
   658 		(* Term.term -> Term.term *)
   659 		fun close_form t =
   660 		let
   661 			(* (Term.indexname * Term.typ) list *)
   662 			val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   663 		in
   664 			foldl
   665 				(fn (t', ((x,i),T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
   666 				(t, vars)
   667 		end
   668 		(* Term.term list *)
   669 		val result = map close_form (collect_term_axioms ([], t))
   670 		val _ = writeln " ...done."
   671 	in
   672 		result
   673 	end;
   674 
   675 (* ------------------------------------------------------------------------- *)
   676 (* ground_types: collects all ground types in a term (including argument     *)
   677 (*               types of other types), suppressing duplicates.  Does not    *)
   678 (*               return function types, set types, non-recursive IDTs, or    *)
   679 (*               'propT'.  For IDTs, also the argument types of constructors *)
   680 (*               are considered.                                             *)
   681 (* ------------------------------------------------------------------------- *)
   682 
   683 	(* theory -> Term.term -> Term.typ list *)
   684 
   685 	fun ground_types thy t =
   686 	let
   687 		(* Term.typ * Term.typ list -> Term.typ list *)
   688 		fun collect_types (T, acc) =
   689 			if T mem acc then
   690 				acc  (* prevent infinite recursion (for IDTs) *)
   691 			else
   692 				(case T of
   693 				  Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc))
   694 				| Type ("prop", [])      => acc
   695 				| Type ("set", [T1])     => collect_types (T1, acc)
   696 				| Type (s, Ts)           =>
   697 					(case DatatypePackage.datatype_info thy s of
   698 					  Some info =>  (* inductive datatype *)
   699 						let
   700 							val index               = #index info
   701 							val descr               = #descr info
   702 							val (_, dtyps, constrs) = (the o assoc) (descr, index)
   703 							val typ_assoc           = dtyps ~~ Ts
   704 							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   705 							val _ = (if Library.exists (fn d =>
   706 									case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
   707 								then
   708 									raise REFUTE ("ground_types", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable")
   709 								else
   710 									())
   711 							(* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
   712 							fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
   713 								(* replace a 'DtTFree' variable by the associated type *)
   714 								(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
   715 							  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
   716 								let
   717 									val (s, ds, _) = (the o assoc) (descr, i)
   718 								in
   719 									Type (s, map (typ_of_dtyp descr typ_assoc) ds)
   720 								end
   721 							  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
   722 								Type (s, map (typ_of_dtyp descr typ_assoc) ds)
   723 							(* if the current type is a recursive IDT (i.e. a depth is required), add it to 'acc' *)
   724 							val acc' = (if Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
   725 									T ins acc
   726 								else
   727 									acc)
   728 							(* collect argument types *)
   729 							val acc_args = foldr collect_types (Ts, acc')
   730 							(* collect constructor types *)
   731 							val acc_constrs = foldr collect_types (flat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs), acc_args)
   732 						in
   733 							acc_constrs
   734 						end
   735 					| None =>  (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *)
   736 						T ins (foldr collect_types (Ts, acc)))
   737 				| TFree _                => T ins acc
   738 				| TVar _                 => T ins acc)
   739 	in
   740 		it_term_types collect_types (t, [])
   741 	end;
   742 
   743 (* ------------------------------------------------------------------------- *)
   744 (* string_of_typ: (rather naive) conversion from types to strings, used to   *)
   745 (*                look up the size of a type in 'sizes'.  Parameterized      *)
   746 (*                types with different parameters (e.g. "'a list" vs. "bool  *)
   747 (*                list") are identified.                                     *)
   748 (* ------------------------------------------------------------------------- *)
   749 
   750 	(* Term.typ -> string *)
   751 
   752 	fun string_of_typ (Type (s, _))     = s
   753 	  | string_of_typ (TFree (s, _))    = s
   754 	  | string_of_typ (TVar ((s,_), _)) = s;
   755 
   756 (* ------------------------------------------------------------------------- *)
   757 (* first_universe: returns the "first" (i.e. smallest) universe by assigning *)
   758 (*                 'minsize' to every type for which no size is specified in *)
   759 (*                 'sizes'                                                   *)
   760 (* ------------------------------------------------------------------------- *)
   761 
   762 	(* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *)
   763 
   764 	fun first_universe xs sizes minsize =
   765 	let
   766 		fun size_of_typ T =
   767 			case assoc (sizes, string_of_typ T) of
   768 			  Some n => n
   769 			| None   => minsize
   770 	in
   771 		map (fn T => (T, size_of_typ T)) xs
   772 	end;
   773 
   774 (* ------------------------------------------------------------------------- *)
   775 (* next_universe: enumerates all universes (i.e. assignments of sizes to     *)
   776 (*                types), where the minimal size of a type is given by       *)
   777 (*                'minsize', the maximal size is given by 'maxsize', and a   *)
   778 (*                type may have a fixed size given in 'sizes'                *)
   779 (* ------------------------------------------------------------------------- *)
   780 
   781 	(* (Term.typ * int) list -> (string * int) list -> int -> int -> (Term.typ * int) list option *)
   782 
   783 	fun next_universe xs sizes minsize maxsize =
   784 	let
   785 		(* int -> int list -> int list option *)
   786 		fun add1 _ [] =
   787 			None  (* overflow *)
   788 		  | add1 max (x::xs) =
   789 		 	if x<max orelse max<0 then
   790 				Some ((x+1)::xs)  (* add 1 to the head *)
   791 			else
   792 				apsome (fn xs' => 0 :: xs') (add1 max xs)  (* carry-over *)
   793 		(* int -> int list * int list -> int list option *)
   794 		fun shift _ (_, []) =
   795 			None
   796 		  | shift max (zeros, x::xs) =
   797 			if x=0 then
   798 				shift max (0::zeros, xs)
   799 			else
   800 				apsome (fn xs' => (x-1) :: (zeros @ xs')) (add1 max xs)
   801 		(* creates the "first" list of length 'len', where the sum of all list *)
   802 		(* elements is 'sum', and the length of the list is 'len'              *)
   803 		(* int -> int -> int -> int list option *)
   804 		fun make_first 0 sum _ =
   805 			if sum=0 then
   806 				Some []
   807 			else
   808 				None
   809 		  | make_first len sum max =
   810 			if sum<=max orelse max<0 then
   811 				apsome (fn xs' => sum :: xs') (make_first (len-1) 0 max)
   812 			else
   813 				apsome (fn xs' => max :: xs') (make_first (len-1) (sum-max) max)
   814 		(* enumerates all int lists with a fixed length, where 0<=x<='max' for *)
   815 		(* all list elements x (unless 'max'<0)                                *)
   816 		(* int -> int list -> int list option *)
   817 		fun next max xs =
   818 			(case shift max ([], xs) of
   819 			  Some xs' =>
   820 				Some xs'
   821 			| None =>
   822 				let
   823 					val (len, sum) = foldl (fn ((l, s), x) => (l+1, s+x)) ((0, 0), xs)
   824 				in
   825 					make_first len (sum+1) max  (* increment 'sum' by 1 *)
   826 				end)
   827 		(* only consider those types for which the size is not fixed *)
   828 		val mutables = filter (fn (T, _) => assoc (sizes, string_of_typ T) = None) xs
   829 		(* subtract 'minsize' from every size (will be added again at the end) *)
   830 		val diffs = map (fn (_, n) => n-minsize) mutables
   831 	in
   832 		case next (maxsize-minsize) diffs of
   833 		  Some diffs' =>
   834 			(* merge with those types for which the size is fixed *)
   835 			Some (snd (foldl_map (fn (ds, (T, _)) =>
   836 				case assoc (sizes, string_of_typ T) of
   837 				  Some n => (ds, (T, n))                      (* return the fixed size *)
   838 				| None   => (tl ds, (T, minsize + (hd ds))))  (* consume the head of 'ds', add 'minsize' *)
   839 				(diffs', xs)))
   840 		| None =>
   841 			None
   842 	end;
   843 
   844 (* ------------------------------------------------------------------------- *)
   845 (* toTrue: converts the interpretation of a Boolean value to a propositional *)
   846 (*         formula that is true iff the interpretation denotes "true"        *)
   847 (* ------------------------------------------------------------------------- *)
   848 
   849 	(* interpretation -> prop_formula *)
   850 
   851 	fun toTrue (Leaf [fm,_]) = fm
   852 	  | toTrue _             = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value");
   853 
   854 (* ------------------------------------------------------------------------- *)
   855 (* toFalse: converts the interpretation of a Boolean value to a              *)
   856 (*          propositional formula that is true iff the interpretation        *)
   857 (*          denotes "false"                                                  *)
   858 (* ------------------------------------------------------------------------- *)
   859 
   860 	(* interpretation -> prop_formula *)
   861 
   862 	fun toFalse (Leaf [_,fm]) = fm
   863 	  | toFalse _             = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");
   864 
   865 (* ------------------------------------------------------------------------- *)
   866 (* find_model: repeatedly calls 'interpret' with appropriate parameters,     *)
   867 (*             applies a SAT solver, and (in case a model is found) displays *)
   868 (*             the model to the user by calling 'print_model'                *)
   869 (* thy       : the current theory                                            *)
   870 (* {...}     : parameters that control the translation/model generation      *)
   871 (* t         : term to be translated into a propositional formula            *)
   872 (* negate    : if true, find a model that makes 't' false (rather than true) *)
   873 (* Note: exception 'TimeOut' is raised if the algorithm does not terminate   *)
   874 (*       within 'maxtime' seconds (if 'maxtime' >0)                          *)
   875 (* ------------------------------------------------------------------------- *)
   876 
   877 	(* theory -> params -> Term.term -> bool -> unit *)
   878 
   879 	fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver} t negate =
   880 	let
   881 		(* unit -> unit *)
   882 		fun wrapper () =
   883 		let
   884 			(* Term.term list *)
   885 			val axioms = collect_axioms thy t
   886 			(* Term.typ list *)
   887 			val types  = foldl (fn (acc, t') => acc union (ground_types thy t')) ([], t :: axioms)
   888 			val _      = writeln ("Ground types: "
   889 				^ (if null types then "none."
   890 				   else commas (map (Sign.string_of_typ (sign_of thy)) types)))
   891 			(* (Term.typ * int) list -> unit *)
   892 			fun find_model_loop universe =
   893 			(let
   894 				val init_model             = (universe, [])
   895 				val init_args              = {maxvars = maxvars, next_idx = 1, bounds = [], wellformed = True}
   896 				val _                      = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
   897 				(* translate 't' and all axioms *)
   898 				val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
   899 					let
   900 						val (i, m', a') = interpret thy m a t'
   901 					in
   902 						((m', a'), i)
   903 					end) ((init_model, init_args), t :: axioms)
   904 				(* make 't' either true or false, and make all axioms true, and *)
   905 				(* add the well-formedness side condition                       *)
   906 				val fm_t  = (if negate then toFalse else toTrue) (hd intrs)
   907 				val fm_ax = PropLogic.all (map toTrue (tl intrs))
   908 				val fm    = PropLogic.all [#wellformed args, fm_ax, fm_t]
   909 			in
   910 				immediate_output " invoking SAT solver...";
   911 				(case SatSolver.invoke_solver satsolver fm of
   912 				  SatSolver.SATISFIABLE assignment =>
   913 					writeln ("\n*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of Some b => b | None => true))
   914 				| _ =>  (* SatSolver.UNSATISFIABLE, SatSolver.UNKNOWN *)
   915 					(immediate_output " no model found.\n";
   916 					case next_universe universe sizes minsize maxsize of
   917 					  Some universe' => find_model_loop universe'
   918 					| None           => writeln "Search terminated, no larger universe within the given limits."))
   919 				handle SatSolver.NOT_CONFIGURED =>
   920 					error ("SAT solver " ^ quote satsolver ^ " is not configured.")
   921 			end handle MAXVARS_EXCEEDED =>
   922 				writeln ("\nSearch terminated, number of Boolean variables (" ^ string_of_int maxvars ^ " allowed) exceeded.")
   923 			| CANNOT_INTERPRET t' =>
   924 				error ("Unable to interpret term " ^ Sign.string_of_term (sign_of thy) t'))
   925 			in
   926 				find_model_loop (first_universe types sizes minsize)
   927 			end
   928 		in
   929 			(* some parameter sanity checks *)
   930 			assert (minsize>=1) ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1");
   931 			assert (maxsize>=1) ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1");
   932 			assert (maxsize>=minsize) ("\"maxsize\" (=" ^ string_of_int maxsize ^ ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ").");
   933 			assert (maxvars>=0) ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0");
   934 			assert (maxtime>=0) ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
   935 			(* enter loop with/without time limit *)
   936 			writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": "
   937 				^ Sign.string_of_term (sign_of thy) t);
   938 			if maxtime>0 then
   939 				(TimeLimit.timeLimit (Time.fromSeconds (Int.toLarge maxtime))
   940 					wrapper ()
   941 				handle TimeLimit.TimeOut =>
   942 					writeln ("\nSearch terminated, time limit ("
   943 						^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds")
   944 						^ ") exceeded."))
   945 			else
   946 				wrapper ()
   947 		end;
   948 
   949 
   950 (* ------------------------------------------------------------------------- *)
   951 (* INTERFACE, PART 2: FINDING A MODEL                                        *)
   952 (* ------------------------------------------------------------------------- *)
   953 
   954 (* ------------------------------------------------------------------------- *)
   955 (* satisfy_term: calls 'find_model' to find a model that satisfies 't'       *)
   956 (* params      : list of '(name, value)' pairs used to override default      *)
   957 (*               parameters                                                  *)
   958 (* ------------------------------------------------------------------------- *)
   959 
   960 	(* theory -> (string * string) list -> Term.term -> unit *)
   961 
   962 	fun satisfy_term thy params t =
   963 		find_model thy (actual_params thy params) t false;
   964 
   965 (* ------------------------------------------------------------------------- *)
   966 (* refute_term: calls 'find_model' to find a model that refutes 't'          *)
   967 (* params     : list of '(name, value)' pairs used to override default       *)
   968 (*              parameters                                                   *)
   969 (* ------------------------------------------------------------------------- *)
   970 
   971 	(* theory -> (string * string) list -> Term.term -> unit *)
   972 
   973 	fun refute_term thy params t =
   974 	let
   975 		(* disallow schematic type variables, since we cannot properly negate  *)
   976 		(* terms containing them (their logical meaning is that there EXISTS a *)
   977 		(* type s.t. ...; to refute such a formula, we would have to show that *)
   978 		(* for ALL types, not ...)                                             *)
   979 		val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables"
   980 		(* existential closure over schematic variables *)
   981 		(* (Term.indexname * Term.typ) list *)
   982 		val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   983 		(* Term.term *)
   984 		val ex_closure = foldl
   985 			(fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
   986 			(t, vars)
   987 		(* If 't' is of type 'propT' (rather than 'boolT'), applying  *)
   988 		(* 'HOLogic.exists_const' is not type-correct.  However, this *)
   989 		(* is not really a problem as long as 'find_model' still      *)
   990 		(* interprets the resulting term correctly, without checking  *)
   991 		(* its type.                                                  *)
   992 	in
   993 		find_model thy (actual_params thy params) ex_closure true
   994 	end;
   995 
   996 (* ------------------------------------------------------------------------- *)
   997 (* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
   998 (* params        : list of '(name, value)' pairs used to override default    *)
   999 (*                 parameters                                                *)
  1000 (* subgoal       : 0-based index specifying the subgoal number               *)
  1001 (* ------------------------------------------------------------------------- *)
  1002 
  1003 	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
  1004 
  1005 	fun refute_subgoal thy params thm subgoal =
  1006 		refute_term thy params (nth_elem (subgoal, prems_of thm));
  1007 
  1008 
  1009 (* ------------------------------------------------------------------------- *)
  1010 (* INTERPRETERS                                                              *)
  1011 (* ------------------------------------------------------------------------- *)
  1012 
  1013 (* ------------------------------------------------------------------------- *)
  1014 (* make_constants: returns all interpretations that have the same tree       *)
  1015 (*                 structure as 'intr', but consist of unit vectors with     *)
  1016 (*                 'True'/'False' only (no Boolean variables)                *)
  1017 (* ------------------------------------------------------------------------- *)
  1018 
  1019 	(* interpretation -> interpretation list *)
  1020 
  1021 	fun make_constants intr =
  1022 	let
  1023 		(* returns a list with all unit vectors of length n *)
  1024 		(* int -> interpretation list *)
  1025 		fun unit_vectors n =
  1026 		let
  1027 			(* returns the k-th unit vector of length n *)
  1028 			(* int * int -> interpretation *)
  1029 			fun unit_vector (k,n) =
  1030 				Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1031 			(* int -> interpretation list -> interpretation list *)
  1032 			fun unit_vectors_acc k vs =
  1033 				if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1034 		in
  1035 			unit_vectors_acc 1 []
  1036 		end
  1037 		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1038 		(* 'a -> 'a list list -> 'a list list *)
  1039 		fun cons_list x xss =
  1040 			map (fn xs => x::xs) xss
  1041 		(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1042 		(* int -> 'a list -> 'a list list *)
  1043 		fun pick_all 1 xs =
  1044 			map (fn x => [x]) xs
  1045 		  | pick_all n xs =
  1046 			let val rec_pick = pick_all (n-1) xs in
  1047 				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1048 			end
  1049 	in
  1050 		case intr of
  1051 		  Leaf xs => unit_vectors (length xs)
  1052 		| Node xs => map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1053 	end;
  1054 
  1055 (* ------------------------------------------------------------------------- *)
  1056 (* size_of_type: returns the number of constants in a type (i.e. 'length     *)
  1057 (*               (make_constants intr)', but implemented more efficiently)   *)
  1058 (* ------------------------------------------------------------------------- *)
  1059 
  1060 	(* interpretation -> int *)
  1061 
  1062 	fun size_of_type intr =
  1063 	let
  1064 		(* power(a,b) computes a^b, for a>=0, b>=0 *)
  1065 		(* int * int -> int *)
  1066 		fun power (a,0) = 1
  1067 		  | power (a,1) = a
  1068 		  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
  1069 	in
  1070 		case intr of
  1071 		  Leaf xs => length xs
  1072 		| Node xs => power (size_of_type (hd xs), length xs)
  1073 	end;
  1074 
  1075 (* ------------------------------------------------------------------------- *)
  1076 (* TT/FF: interpretations that denote "true" or "false", respectively        *)
  1077 (* ------------------------------------------------------------------------- *)
  1078 
  1079 	(* interpretation *)
  1080 
  1081 	val TT = Leaf [True, False];
  1082 
  1083 	val FF = Leaf [False, True];
  1084 
  1085 (* ------------------------------------------------------------------------- *)
  1086 (* make_equality: returns an interpretation that denotes (extensional)       *)
  1087 (*                equality of two interpretations                            *)
  1088 (* ------------------------------------------------------------------------- *)
  1089 
  1090 	(* We could in principle represent '=' on a type T by a particular        *)
  1091 	(* interpretation.  However, the size of that interpretation is quadratic *)
  1092 	(* in the size of T.  Therefore comparing the interpretations 'i1' and    *)
  1093 	(* 'i2' directly is more efficient than constructing the interpretation   *)
  1094 	(* for equality on T first, and "applying" this interpretation to 'i1'    *)
  1095 	(* and 'i2' in the usual way (cf. 'interpretation_apply') then.           *)
  1096 
  1097 	(* interpretation * interpretation -> interpretation *)
  1098 
  1099 	fun make_equality (i1, i2) =
  1100 	let
  1101 		(* interpretation * interpretation -> prop_formula *)
  1102 		fun equal (i1, i2) =
  1103 			(case i1 of
  1104 			  Leaf xs =>
  1105 				(case i2 of
  1106 				  Leaf ys => PropLogic.dot_product (xs, ys)
  1107 				| Node _  => raise REFUTE ("make_equality", "second interpretation is higher"))
  1108 			| Node xs =>
  1109 				(case i2 of
  1110 				  Leaf _  => raise REFUTE ("make_equality", "first interpretation is higher")
  1111 				| Node ys => PropLogic.all (map equal (xs ~~ ys))))
  1112 		(* interpretation * interpretation -> prop_formula *)
  1113 		fun not_equal (i1, i2) =
  1114 			(case i1 of
  1115 			  Leaf xs =>
  1116 				(case i2 of
  1117 				  Leaf ys => PropLogic.all ((PropLogic.exists xs) :: (PropLogic.exists ys) ::
  1118 					(map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys)))  (* defined and not equal *)
  1119 				| Node _  => raise REFUTE ("make_equality", "second interpretation is higher"))
  1120 			| Node xs =>
  1121 				(case i2 of
  1122 				  Leaf _  => raise REFUTE ("make_equality", "first interpretation is higher")
  1123 				| Node ys => PropLogic.exists (map not_equal (xs ~~ ys))))
  1124 	in
  1125 		(* a value may be undefined; therefore 'not_equal' is not just the     *)
  1126 		(* negation of 'equal':                                                *)
  1127 		(* - two interpretations are 'equal' iff they are both defined and     *)
  1128 		(*   denote the same value                                             *)
  1129 		(* - two interpretations are 'not_equal' iff they are both defined at  *)
  1130 		(*   least partially, and a defined part denotes different values      *)
  1131 		(* - an undefined interpretation is neither 'equal' nor 'not_equal' to *)
  1132 		(*   another value                                                     *)
  1133 		Leaf [equal (i1, i2), not_equal (i1, i2)]
  1134 	end;
  1135 
  1136 
  1137 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1138 
  1139 	(* simply typed lambda calculus: Isabelle's basic term syntax, with type  *)
  1140 	(* variables, function types, and propT                                   *)
  1141 
  1142 	fun stlc_interpreter thy model args t =
  1143 	let
  1144 		val (typs, terms)                           = model
  1145 		val {maxvars, next_idx, bounds, wellformed} = args
  1146 		(* Term.typ -> (interpretation * model * arguments) option *)
  1147 		fun interpret_groundterm T =
  1148 		let
  1149 			(* unit -> (interpretation * model * arguments) option *)
  1150 			fun interpret_groundtype () =
  1151 			let
  1152 				val size = (if T = Term.propT then 2 else (the o assoc) (typs, T))  (* the model MUST specify a size for ground types *)
  1153 				val next = (if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 2 *)
  1154 				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
  1155 				(* prop_formula list *)
  1156 				val fms  = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
  1157 					else (map BoolVar (next_idx upto (next_idx+size-1))))
  1158 				(* interpretation *)
  1159 				val intr = Leaf fms
  1160 				(* prop_formula list -> prop_formula *)
  1161 				fun one_of_two_false []      = True
  1162 				  | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs)
  1163 				(* prop_formula list -> prop_formula *)
  1164 				fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
  1165 				(* prop_formula *)
  1166 				val wf   = (if size=2 then True else exactly_one_true fms)
  1167 			in
  1168 				(* extend the model, increase 'next_idx', add well-formedness condition *)
  1169 				Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
  1170 			end
  1171 		in
  1172 			case T of
  1173 			  Type ("fun", [T1, T2]) =>
  1174 				let
  1175 					(* we create 'size_of_type (interpret (... T1))' different copies *)
  1176 					(* of the interpretation for 'T2', which are then combined into a *)
  1177 					(* single new interpretation                                      *)
  1178 					val (i1, _, _) =
  1179 						(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
  1180 						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1181 					(* make fresh copies, with different variable indices *)
  1182 					(* 'idx': next variable index                         *)
  1183 					(* 'n'  : number of copies                            *)
  1184 					(* int -> int -> (int * interpretation list * prop_formula *)
  1185 					fun make_copies idx 0 =
  1186 						(idx, [], True)
  1187 					  | make_copies idx n =
  1188 						let
  1189 							val (copy, _, new_args) =
  1190 								(interpret thy (typs, []) {maxvars = maxvars, next_idx = idx, bounds = [], wellformed = True} (Free ("dummy", T2))
  1191 								handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1192 							val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1)
  1193 						in
  1194 							(idx', copy :: copies, SAnd (#wellformed new_args, wf'))
  1195 						end
  1196 					val (next, copies, wf) = make_copies next_idx (size_of_type i1)
  1197 					(* combine copies into a single interpretation *)
  1198 					val intr = Node copies
  1199 				in
  1200 					(* extend the model, increase 'next_idx', add well-formedness condition *)
  1201 					Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
  1202 				end
  1203 			| Type _  => interpret_groundtype ()
  1204 			| TFree _ => interpret_groundtype ()
  1205 			| TVar  _ => interpret_groundtype ()
  1206 		end
  1207 	in
  1208 		case assoc (terms, t) of
  1209 		  Some intr =>
  1210 			(* return an existing interpretation *)
  1211 			Some (intr, model, args)
  1212 		| None =>
  1213 			(case t of
  1214 			  Const (_, T)     =>
  1215 				interpret_groundterm T
  1216 			| Free (_, T)      =>
  1217 				interpret_groundterm T
  1218 			| Var (_, T)       =>
  1219 				interpret_groundterm T
  1220 			| Bound i          =>
  1221 				Some (nth_elem (i, #bounds args), model, args)
  1222 			| Abs (x, T, body) =>
  1223 				let
  1224 					(* create all constants of type 'T' *)
  1225 					val (i, _, _) =
  1226 						(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1227 						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1228 					val constants = make_constants i
  1229 					(* interpret the 'body' separately for each constant *)
  1230 					val ((model', args'), bodies) = foldl_map
  1231 						(fn ((m,a), c) =>
  1232 							let
  1233 								(* add 'c' to 'bounds' *)
  1234 								val (i', m', a') = interpret thy m {maxvars = #maxvars a, next_idx = #next_idx a, bounds = (c :: #bounds a), wellformed = #wellformed a} body
  1235 							in
  1236 								(* keep the new model m' and 'next_idx' and 'wellformed', but use old 'bounds' *)
  1237 								((m', {maxvars = maxvars, next_idx = #next_idx a', bounds = bounds, wellformed = #wellformed a'}), i')
  1238 							end)
  1239 						((model, args), constants)
  1240 				in
  1241 					Some (Node bodies, model', args')
  1242 				end
  1243 			| t1 $ t2          =>
  1244 				let
  1245 					(* auxiliary functions *)
  1246 					(* interpretation * interpretation -> interpretation *)
  1247 					fun interpretation_disjunction (tr1,tr2) =
  1248 						tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
  1249 					(* prop_formula * interpretation -> interpretation *)
  1250 					fun prop_formula_times_interpretation (fm,tr) =
  1251 						tree_map (map (fn x => SAnd (fm,x))) tr
  1252 					(* prop_formula list * interpretation list -> interpretation *)
  1253 					fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
  1254 						prop_formula_times_interpretation (fm,tr)
  1255 					  | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
  1256 						interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees))
  1257 					  | prop_formula_list_dot_product_interpretation_list (_,_) =
  1258 						raise REFUTE ("stlc_interpreter", "empty list (in dot product)")
  1259 					(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1260 					(* 'a -> 'a list list -> 'a list list *)
  1261 					fun cons_list x xss =
  1262 						map (fn xs => x::xs) xss
  1263 					(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
  1264 					(* 'a list list -> 'a list list *)
  1265 					fun pick_all [xs] =
  1266 						map (fn x => [x]) xs
  1267 					  | pick_all (xs::xss) =
  1268 						let val rec_pick = pick_all xss in
  1269 							foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1270 						end
  1271 					  | pick_all _ =
  1272 						raise REFUTE ("stlc_interpreter", "empty list (in pick_all)")
  1273 					(* interpretation -> prop_formula list *)
  1274 					fun interpretation_to_prop_formula_list (Leaf xs) =
  1275 						xs
  1276 					  | interpretation_to_prop_formula_list (Node trees) =
  1277 						map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees))
  1278 					(* interpretation * interpretation -> interpretation *)
  1279 					fun interpretation_apply (tr1,tr2) =
  1280 						(case tr1 of
  1281 						  Leaf _ =>
  1282 							raise REFUTE ("stlc_interpreter", "first interpretation is a leaf")
  1283 						| Node xs =>
  1284 							prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs))
  1285 					(* interpret 't1' and 't2' separately *)
  1286 					val (intr1, model1, args1) = interpret thy model args t1
  1287 					val (intr2, model2, args2) = interpret thy model1 args1 t2
  1288 				in
  1289 					Some (interpretation_apply (intr1,intr2), model2, args2)
  1290 				end)
  1291 	end;
  1292 
  1293 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1294 
  1295 	fun Pure_interpreter thy model args t =
  1296 		case t of
  1297 		  Const ("all", _) $ t1 =>  (* in the meta-logic, 'all' MUST be followed by an argument term *)
  1298 			let
  1299 				val (i, m, a) = interpret thy model args t1
  1300 			in
  1301 				case i of
  1302 				  Node xs =>
  1303 					let
  1304 						val fmTrue  = PropLogic.all (map toTrue xs)
  1305 						val fmFalse = PropLogic.exists (map toFalse xs)
  1306 					in
  1307 						Some (Leaf [fmTrue, fmFalse], m, a)
  1308 					end
  1309 				| _ =>
  1310 					raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function")
  1311 			end
  1312 		| Const ("==", _) $ t1 $ t2 =>
  1313 			let
  1314 				val (i1, m1, a1) = interpret thy model args t1
  1315 				val (i2, m2, a2) = interpret thy m1 a1 t2
  1316 			in
  1317 				Some (make_equality (i1, i2), m2, a2)
  1318 			end
  1319 		| Const ("==>", _) =>  (* simpler than translating 'Const ("==>", _) $ t1 $ t2' *)
  1320 			Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
  1321 		| _ => None;
  1322 
  1323 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1324 
  1325 	fun HOLogic_interpreter thy model args t =
  1326 	let
  1327 		(* Term.term -> int -> Term.term *)
  1328 		fun eta_expand t i =
  1329 		let
  1330 			val Ts = binder_types (fastype_of t)
  1331 		in
  1332 			foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
  1333 				(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
  1334 		end
  1335 	in
  1336 	(* ------------------------------------------------------------------------- *)
  1337 	(* Providing interpretations directly is more efficient than unfolding the   *)
  1338 	(* logical constants.  IN HOL however, logical constants can themselves be   *)
  1339 	(* arguments.  "All" and "Ex" are then translated just like any other        *)
  1340 	(* constant, with the relevant axiom being added by 'collect_axioms'.        *)
  1341 	(* ------------------------------------------------------------------------- *)
  1342 		case t of
  1343 		  Const ("Trueprop", _) =>
  1344 			Some (Node [TT, FF], model, args)
  1345 		| Const ("Not", _) =>
  1346 			Some (Node [FF, TT], model, args)
  1347 		| Const ("True", _) =>  (* redundant, since 'True' is also an IDT constructor *)
  1348 			Some (TT, model, args)
  1349 		| Const ("False", _) =>  (* redundant, since 'False' is also an IDT constructor *)
  1350 			Some (FF, model, args)
  1351 		| Const ("All", _) $ t1 =>
  1352 			let
  1353 				val (i, m, a) = interpret thy model args t1
  1354 			in
  1355 				case i of
  1356 				  Node xs =>
  1357 					let
  1358 						val fmTrue  = PropLogic.all (map toTrue xs)
  1359 						val fmFalse = PropLogic.exists (map toFalse xs)
  1360 					in
  1361 						Some (Leaf [fmTrue, fmFalse], m, a)
  1362 					end
  1363 				| _ =>
  1364 					raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function")
  1365 			end
  1366 		| Const ("Ex", _) $ t1 =>
  1367 			let
  1368 				val (i, m, a) = interpret thy model args t1
  1369 			in
  1370 				case i of
  1371 				  Node xs =>
  1372 					let
  1373 						val fmTrue  = PropLogic.exists (map toTrue xs)
  1374 						val fmFalse = PropLogic.all (map toFalse xs)
  1375 					in
  1376 						Some (Leaf [fmTrue, fmFalse], m, a)
  1377 					end
  1378 				| _ =>
  1379 					raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function")
  1380 			end
  1381 		| Const ("op =", _) $ t1 $ t2 =>
  1382 			let
  1383 				val (i1, m1, a1) = interpret thy model args t1
  1384 				val (i2, m2, a2) = interpret thy m1 a1 t2
  1385 			in
  1386 				Some (make_equality (i1, i2), m2, a2)
  1387 			end
  1388 		| Const ("op =", _) $ t1 =>
  1389 			(Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1390 		| Const ("op =", _) =>
  1391 			(Some (interpret thy model args (eta_expand t 2)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1392 		| Const ("op &", _) =>
  1393 			Some (Node [Node [TT, FF], Node [FF, FF]], model, args)
  1394 		| Const ("op |", _) =>
  1395 			Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
  1396 		| Const ("op -->", _) =>
  1397 			Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
  1398 		| _ => None
  1399 	end;
  1400 
  1401 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1402 
  1403 	fun set_interpreter thy model args t =
  1404 	(* "T set" is isomorphic to "T --> bool" *)
  1405 	let
  1406 		val (typs, terms) = model
  1407 		(* Term.term -> int -> Term.term *)
  1408 		fun eta_expand t i =
  1409 		let
  1410 			val Ts = binder_types (fastype_of t)
  1411 		in
  1412 			foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
  1413 				(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
  1414 		end
  1415 	in
  1416 		case assoc (terms, t) of
  1417 		  Some intr =>
  1418 			(* return an existing interpretation *)
  1419 			Some (intr, model, args)
  1420 		| None =>
  1421 			(case t of
  1422 			  Free (x, Type ("set", [T])) =>
  1423 				(let
  1424 					val (intr, _, args') = interpret thy (typs, []) args (Free (x, T --> HOLogic.boolT))
  1425 				in
  1426 					Some (intr, (typs, (t, intr)::terms), args')
  1427 				end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1428 			| Var ((x,i), Type ("set", [T])) =>
  1429 				(let
  1430 					val (intr, _, args') = interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT))
  1431 				in
  1432 					Some (intr, (typs, (t, intr)::terms), args')
  1433 				end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1434 			| Const (s, Type ("set", [T])) =>
  1435 				(let
  1436 					val (intr, _, args') = interpret thy (typs, []) args (Const (s, T --> HOLogic.boolT))
  1437 				in
  1438 					Some (intr, (typs, (t, intr)::terms), args')
  1439 				end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1440 			(* 'Collect' == identity *)
  1441 			| Const ("Collect", _) $ t1 =>
  1442 				Some (interpret thy model args t1)
  1443 			| Const ("Collect", _) =>
  1444 				(Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1445 			(* 'op :' == application *)
  1446 			| Const ("op :", _) $ t1 $ t2 =>
  1447 				Some (interpret thy model args (t2 $ t1))
  1448 			| Const ("op :", _) $ t1 =>
  1449 				(Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1450 			| Const ("op :", _) =>
  1451 				(Some (interpret thy model args (eta_expand t 2)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1452 			| _ => None)
  1453 	end;
  1454 
  1455 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1456 
  1457 	fun IDT_interpreter thy model args t =
  1458 	let
  1459 		val (typs, terms) = model
  1460 		(* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
  1461 		fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
  1462 			(* replace a 'DtTFree' variable by the associated type *)
  1463 			(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
  1464 		  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
  1465 			let
  1466 				val (s, ds, _) = (the o assoc) (descr, i)
  1467 			in
  1468 				Type (s, map (typ_of_dtyp descr typ_assoc) ds)
  1469 			end
  1470 		  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
  1471 			Type (s, map (typ_of_dtyp descr typ_assoc) ds)
  1472 		(* int list -> int *)
  1473 		fun sum xs = foldl op+ (0, xs)
  1474 		(* int list -> int *)
  1475 		fun product xs = foldl op* (1, xs)
  1476 		(* the size of an IDT is the sum (over its constructors) of the        *)
  1477 		(* product (over their arguments) of the size of the argument type     *)
  1478 		(* (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *)
  1479 		fun size_of_dtyp typs descr typ_assoc constrs =
  1480 			sum (map (fn (_, ds) =>
  1481 				product (map (fn d =>
  1482 					let
  1483 						val T         = typ_of_dtyp descr typ_assoc d
  1484 						val (i, _, _) =
  1485 							(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1486 							handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1487 					in
  1488 						size_of_type i
  1489 					end) ds)) constrs)
  1490 		(* Term.typ -> (interpretation * model * arguments) option *)
  1491 		fun interpret_variable (Type (s, Ts)) =
  1492 			(case DatatypePackage.datatype_info thy s of
  1493 			  Some info =>  (* inductive datatype *)
  1494 				let
  1495 					val (typs, terms) = model
  1496 					(* int option -- only recursive IDTs have an associated depth *)
  1497 					val depth         = assoc (typs, Type (s, Ts))
  1498 				in
  1499 					if depth = (Some 0) then  (* termination condition to avoid infinite recursion *)
  1500 						(* return a leaf of size 0 *)
  1501 						Some (Leaf [], model, args)
  1502 					else
  1503 						let
  1504 							val index               = #index info
  1505 							val descr               = #descr info
  1506 							val (_, dtyps, constrs) = (the o assoc) (descr, index)
  1507 							val typ_assoc           = dtyps ~~ Ts
  1508 							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1509 							val _ = (if Library.exists (fn d =>
  1510 									case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
  1511 								then
  1512 									raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable")
  1513 								else
  1514 									())
  1515 							(* if the model specifies a depth for the current type, decrement it to avoid infinite recursion *)
  1516 							val typs'    = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1)))
  1517 							(* recursively compute the size of the datatype *)
  1518 							val size     = size_of_dtyp typs' descr typ_assoc constrs
  1519 							val next_idx = #next_idx args
  1520 							val next     = (if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 2 *)
  1521 							val _        = (if next-1>(#maxvars args) andalso (#maxvars args)>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
  1522 							(* prop_formula list *)
  1523 							val fms      = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
  1524 								else (map BoolVar (next_idx upto (next_idx+size-1))))
  1525 							(* interpretation *)
  1526 							val intr     = Leaf fms
  1527 							(* prop_formula list -> prop_formula *)
  1528 							fun one_of_two_false []      = True
  1529 							  | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs)
  1530 							(* prop_formula list -> prop_formula *)
  1531 							fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
  1532 							(* prop_formula *)
  1533 							val wf       = (if size=2 then True else exactly_one_true fms)
  1534 						in
  1535 							(* extend the model, increase 'next_idx', add well-formedness condition *)
  1536 							Some (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)})
  1537 						end
  1538 				end
  1539 			| None =>  (* not an inductive datatype *)
  1540 				None)
  1541 		  | interpret_variable _ =  (* a (free or schematic) type variable *)
  1542 			None
  1543 	in
  1544 		case assoc (terms, t) of
  1545 		  Some intr =>
  1546 			(* return an existing interpretation *)
  1547 			Some (intr, model, args)
  1548 		| None =>
  1549 			(case t of
  1550 			  Free (_, T)  => interpret_variable T
  1551 			| Var (_, T)   => interpret_variable T
  1552 			| Const (s, T) =>
  1553 				(* TODO: case, recursion, size *)
  1554 				let
  1555 					(* unit -> (interpretation * model * arguments) option *)
  1556 					fun interpret_constructor () =
  1557 						(case body_type T of
  1558 						  Type (s', Ts') =>
  1559 							(case DatatypePackage.datatype_info thy s' of
  1560 							  Some info =>  (* body type is an inductive datatype *)
  1561 								let
  1562 									val index               = #index info
  1563 									val descr               = #descr info
  1564 									val (_, dtyps, constrs) = (the o assoc) (descr, index)
  1565 									val typ_assoc           = dtyps ~~ Ts'
  1566 									(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1567 									val _ = (if Library.exists (fn d =>
  1568 											case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
  1569 										then
  1570 											raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s', Ts')) ^ ") is not a variable")
  1571 										else
  1572 											())
  1573 									(* split the constructors into those occuring before/after 'Const (s, T)' *)
  1574 									val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
  1575 										not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T,
  1576 											map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs
  1577 								in
  1578 									case constrs2 of
  1579 									  [] =>
  1580 										(* 'Const (s, T)' is not a constructor of this datatype *)
  1581 										None
  1582 									| c::cs =>
  1583 										let
  1584 											(* int option -- only recursive IDTs have an associated depth *)
  1585 											val depth = assoc (typs, Type (s', Ts'))
  1586 											val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s', Ts'), n-1)))
  1587 											(* constructors before 'Const (s, T)' generate elements of the datatype *)
  1588 											val offset  = size_of_dtyp typs' descr typ_assoc constrs1
  1589 											(* 'Const (s, T)' and constructors after it generate elements of the datatype *)
  1590 											val total   = offset + (size_of_dtyp typs' descr typ_assoc constrs2)
  1591 											(* create an interpretation that corresponds to the constructor 'Const (s, T)' *)
  1592 											(* by recursion over its argument types                                        *)
  1593 											(* DatatypeAux.dtyp list -> interpretation *)
  1594 											fun make_partial [] =
  1595 												(* all entries of the leaf are 'False' *)
  1596 												Leaf (replicate total False)
  1597 											  | make_partial (d::ds) =
  1598 												let
  1599 													(* compute the "new" size of the type 'd' *)
  1600 													val T         = typ_of_dtyp descr typ_assoc d
  1601 													val (i, _, _) =
  1602 														(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1603 														handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1604 												in
  1605 													(* all entries of the whole subtree are 'False' *)
  1606 													Node (replicate (size_of_type i) (make_partial ds))
  1607 												end
  1608 											(* int * DatatypeAux.dtyp list -> int * interpretation *)
  1609 											fun make_constr (offset, []) =
  1610 												if offset<total then
  1611 													(offset+1, Leaf ((replicate offset False) @ True :: (replicate (total-offset-1) False)))
  1612 												else
  1613 													raise REFUTE ("IDT_interpreter", "internal error: offset >= total")
  1614 											  | make_constr (offset, d::ds) =
  1615 												let
  1616 													(* compute the "new" and "old" size of the type 'd' *)
  1617 													val T         = typ_of_dtyp descr typ_assoc d
  1618 													val (i, _, _) =
  1619 														(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1620 														handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1621 													val (i', _, _) =
  1622 														(interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1623 														handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1624 													val size  = size_of_type i
  1625 													val size' = size_of_type i'
  1626 													val _ = if size<size' then
  1627 															raise REFUTE ("IDT_interpreter", "internal error: new size < old size")
  1628 														else
  1629 															()
  1630 													val (new_offset, intrs) = foldl_map make_constr (offset, replicate size' ds)
  1631 												in
  1632 													(* the first size' elements of the type actually yield a result *)
  1633 													(* element, while the remaining size-size' elements don't       *)
  1634 													(new_offset, Node (intrs @ (replicate (size-size') (make_partial ds))))
  1635 												end
  1636 										in
  1637 											Some ((snd o make_constr) (offset, snd c), model, args)
  1638 										end
  1639 								end
  1640 							| None =>  (* body type is not an inductive datatype *)
  1641 								None)
  1642 						| _ =>  (* body type is a (free or schematic) type variable *)
  1643 							None)
  1644 				in
  1645 					case interpret_constructor () of
  1646 					  Some x => Some x
  1647 					| None   => interpret_variable T
  1648 				end
  1649 			| _ => None)
  1650 	end;
  1651 
  1652 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1653 
  1654 	(* only an optimization: 'card' could in principle be interpreted with    *)
  1655 	(* interpreters available already (using its definition), but the code    *)
  1656 	(* below is much more efficient                                           *)
  1657 
  1658 	fun Finite_Set_card_interpreter thy model args t =
  1659 		case t of
  1660 		  Const ("Finite_Set.card", Type ("fun", [Type ("set", [T]), Type ("nat", [])])) =>
  1661 			let
  1662 				val (i_nat, _, _) =
  1663 					(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
  1664 						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1665 				val size_nat      = size_of_type i_nat
  1666 				val (i_set, _, _) =
  1667 					(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T])))
  1668 						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1669 				val constants     = make_constants i_set
  1670 				(* interpretation -> int *)
  1671 				fun number_of_elements (Node xs) =
  1672 					foldl (fn (n, x) =>
  1673 						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)
  1674 				  | number_of_elements (Leaf _) =
  1675 					raise REFUTE ("Finite_Set_card_interpreter", "interpretation for set type is a leaf")
  1676 				(* takes an interpretation for a set and returns an interpretation for a 'nat' *)
  1677 				(* interpretation -> interpretation *)
  1678 				fun card i =
  1679 					let
  1680 						val n = number_of_elements i
  1681 					in
  1682 						if n<size_nat then
  1683 							Leaf ((replicate n False) @ True :: (replicate (size_nat-n-1) False))
  1684 						else
  1685 							Leaf (replicate size_nat False)
  1686 					end
  1687 			in
  1688 				Some (Node (map card constants), model, args)
  1689 			end
  1690 		| _ =>
  1691 			None;
  1692 
  1693 
  1694 (* ------------------------------------------------------------------------- *)
  1695 (* PRINTERS                                                                  *)
  1696 (* ------------------------------------------------------------------------- *)
  1697 
  1698 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option *)
  1699 
  1700 	fun stlc_printer thy model t intr assignment =
  1701 	let
  1702 		(* Term.term -> Term.typ option *)
  1703 		fun typeof (Free (_, T))  = Some T
  1704 		  | typeof (Var (_, T))   = Some T
  1705 		  | typeof (Const (_, T)) = Some T
  1706 		  | typeof _              = None
  1707 		(* string -> string *)
  1708 		fun strip_leading_quote s =
  1709 			(implode o (fn ss => case ss of [] => [] | x::xs => if x="'" then xs else ss) o explode) s
  1710 		(* Term.typ -> string *)
  1711 		fun string_of_typ (Type (s, _))     = s
  1712 		  | string_of_typ (TFree (x, _))    = strip_leading_quote x
  1713 		  | string_of_typ (TVar ((x,i), _)) = strip_leading_quote x ^ string_of_int i
  1714 		(* interpretation -> int *)
  1715 		fun index_from_interpretation (Leaf xs) =
  1716 			let
  1717 				val idx = find_index (PropLogic.eval assignment) xs
  1718 			in
  1719 				if idx<0 then
  1720 					raise REFUTE ("stlc_printer", "illegal interpretation: no value assigned (SAT solver unsound?)")
  1721 				else
  1722 					idx
  1723 			end
  1724 		  | index_from_interpretation _ =
  1725 			raise REFUTE ("stlc_printer", "interpretation for ground type is not a leaf")
  1726 	in
  1727 		case typeof t of
  1728 		  Some T =>
  1729 			(case T of
  1730 			  Type ("fun", [T1, T2]) =>
  1731 				(let
  1732 					(* create all constants of type 'T1' *)
  1733 					val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
  1734 					val constants = make_constants i
  1735 					(* interpretation list *)
  1736 					val results = (case intr of
  1737 						  Node xs => xs
  1738 						| _       => raise REFUTE ("stlc_printer", "interpretation for function type is a leaf"))
  1739 					(* Term.term list *)
  1740 					val pairs = map (fn (arg, result) =>
  1741 						HOLogic.mk_prod
  1742 							(print thy model (Free ("dummy", T1)) arg assignment,
  1743 							 print thy model (Free ("dummy", T2)) result assignment))
  1744 						(constants ~~ results)
  1745 					(* Term.typ *)
  1746 					val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
  1747 					val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
  1748 					(* Term.term *)
  1749 					val HOLogic_empty_set = Const ("{}", HOLogic_setT)
  1750 					val HOLogic_insert    = Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
  1751 				in
  1752 					Some (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
  1753 				end handle CANNOT_INTERPRET _ => None)
  1754 			| Type ("prop", [])      =>
  1755 				(case index_from_interpretation intr of
  1756 				  0 => Some (HOLogic.mk_Trueprop HOLogic.true_const)
  1757 				| 1 => Some (HOLogic.mk_Trueprop HOLogic.false_const)
  1758 				| _ => raise REFUTE ("stlc_interpreter", "illegal interpretation for a propositional value"))
  1759 			| Type _  => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
  1760 			| TFree _ => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
  1761 			| TVar _  => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T)))
  1762 		| None =>
  1763 			None
  1764 	end;
  1765 
  1766 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1767 
  1768 	fun set_printer thy model t intr assignment =
  1769 	let
  1770 		(* Term.term -> Term.typ option *)
  1771 		fun typeof (Free (_, T))  = Some T
  1772 		  | typeof (Var (_, T))   = Some T
  1773 		  | typeof (Const (_, T)) = Some T
  1774 		  | typeof _              = None
  1775 	in
  1776 		case typeof t of
  1777 		  Some (Type ("set", [T])) =>
  1778 			(let
  1779 				(* create all constants of type 'T' *)
  1780 				val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1781 				val constants = make_constants i
  1782 				(* interpretation list *)
  1783 				val results = (case intr of
  1784 					  Node xs => xs
  1785 					| _       => raise REFUTE ("set_printer", "interpretation for set type is a leaf"))
  1786 				(* Term.term list *)
  1787 				val elements = mapfilter (fn (arg, result) =>
  1788 					case result of
  1789 					  Leaf [fmTrue, fmFalse] =>
  1790 						if PropLogic.eval assignment fmTrue then
  1791 							Some (print thy model (Free ("dummy", T)) arg assignment)
  1792 						else if PropLogic.eval assignment fmFalse then
  1793 							None
  1794 						else
  1795 							raise REFUTE ("set_printer", "illegal interpretation: no value assigned (SAT solver unsound?)")
  1796 					| _ =>
  1797 						raise REFUTE ("set_printer", "illegal interpretation for a Boolean value"))
  1798 					(constants ~~ results)
  1799 				(* Term.typ *)
  1800 				val HOLogic_setT  = HOLogic.mk_setT T
  1801 				(* Term.term *)
  1802 				val HOLogic_empty_set = Const ("{}", HOLogic_setT)
  1803 				val HOLogic_insert    = Const ("insert", T --> HOLogic_setT --> HOLogic_setT)
  1804 			in
  1805 				Some (foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) (HOLogic_empty_set, elements))
  1806 			end handle CANNOT_INTERPRET _ => None)
  1807 		| _ =>
  1808 			None
  1809 	end;
  1810 
  1811 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option *)
  1812 
  1813 	fun IDT_printer thy model t intr assignment =
  1814 	let
  1815 		(* Term.term -> Term.typ option *)
  1816 		fun typeof (Free (_, T))  = Some T
  1817 		  | typeof (Var (_, T))   = Some T
  1818 		  | typeof (Const (_, T)) = Some T
  1819 		  | typeof _              = None
  1820 	in
  1821 		case typeof t of
  1822 		  Some (Type (s, Ts)) =>
  1823 			(case DatatypePackage.datatype_info thy s of
  1824 			  Some info =>  (* inductive datatype *)
  1825 				let
  1826 					val (typs, _)           = model
  1827 					val index               = #index info
  1828 					val descr               = #descr info
  1829 					val (_, dtyps, constrs) = (the o assoc) (descr, index)
  1830 					val typ_assoc           = dtyps ~~ Ts
  1831 					(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1832 					val _ = (if Library.exists (fn d =>
  1833 							case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
  1834 						then
  1835 							raise REFUTE ("IDT_printer", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable")
  1836 						else
  1837 							())
  1838 					(* the index of the element in the datatype *)
  1839 					val element = (case intr of
  1840 						  Leaf xs => find_index (PropLogic.eval assignment) xs
  1841 						| Node _  => raise REFUTE ("IDT_printer", "interpretation is not a leaf"))
  1842 					val _ = (if element<0 then raise REFUTE ("IDT_printer", "invalid interpretation (no value assigned)") else ())
  1843 					(* int option -- only recursive IDTs have an associated depth *)
  1844 					val depth = assoc (typs, Type (s, Ts))
  1845 					val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1)))
  1846 					(* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
  1847 					fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
  1848 						(* replace a 'DtTFree' variable by the associated type *)
  1849 						(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
  1850 					  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
  1851 						let
  1852 							val (s, ds, _) = (the o assoc) (descr, i)
  1853 						in
  1854 							Type (s, map (typ_of_dtyp descr typ_assoc) ds)
  1855 						end
  1856 					  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
  1857 						Type (s, map (typ_of_dtyp descr typ_assoc) ds)
  1858 					(* int list -> int *)
  1859 					fun sum xs = foldl op+ (0, xs)
  1860 					(* int list -> int *)
  1861 					fun product xs = foldl op* (1, xs)
  1862 					(* the size of an IDT is the sum (over its constructors) of the        *)
  1863 					(* product (over their arguments) of the size of the argument type     *)
  1864 					(* (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *)
  1865 					fun size_of_dtyp typs descr typ_assoc xs =
  1866 						sum (map (fn (_, ds) =>
  1867 							product (map (fn d =>
  1868 								let
  1869 									val T         = typ_of_dtyp descr typ_assoc d
  1870 									val (i, _, _) =
  1871 										(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1872 										handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1873 					in
  1874 						size_of_type i
  1875 					end) ds)) xs)
  1876 					(* int -> DatatypeAux.dtyp list -> Term.term list *)
  1877 					fun make_args n [] =
  1878 						if n<>0 then
  1879 							raise REFUTE ("IDT_printer", "error computing the element: remainder is not 0")
  1880 						else
  1881 							[]
  1882 					  | make_args n (d::ds) =
  1883 						let
  1884 							val dT        = typ_of_dtyp descr typ_assoc d
  1885 							val (i, _, _) =
  1886 								(interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", dT))
  1887 								handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1888 							val size      = size_of_type i
  1889 							val consts    = make_constants i  (* we only need the (n mod size)-th element of *)
  1890 								(* this list, so there might be a more efficient implementation that does not *)
  1891 								(* generate all constants                                                     *)
  1892 						in
  1893 							(print thy (typs', []) (Free ("dummy", dT)) (nth_elem (n mod size, consts)) assignment)::(make_args (n div size) ds)
  1894 						end
  1895 					(* int -> (string * DatatypeAux.dtyp list) list -> Term.term *)
  1896 					fun make_term _ [] =
  1897 						raise REFUTE ("IDT_printer", "invalid interpretation (value too large - not enough constructors)")
  1898 					  | make_term n (c::cs) =
  1899 						let
  1900 							val c_size = size_of_dtyp typs' descr typ_assoc [c]
  1901 						in
  1902 							if n<c_size then
  1903 								let
  1904 									val (cname, cargs) = c
  1905 									val c_term = Const (cname, (map (typ_of_dtyp descr typ_assoc) cargs) ---> Type (s, Ts))
  1906 								in
  1907 									foldl op$ (c_term, rev (make_args n (rev cargs)))
  1908 								end
  1909 							else
  1910 								make_term (n-c_size) cs
  1911 						end
  1912 				in
  1913 					Some (make_term element constrs)
  1914 				end
  1915 			| None =>  (* not an inductive datatype *)
  1916 				None)
  1917 		| _ =>  (* a (free or schematic) type variable *)
  1918 			None
  1919 	end;
  1920 
  1921 
  1922 (* ------------------------------------------------------------------------- *)
  1923 (* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
  1924 (* structure                                                                 *)
  1925 (* ------------------------------------------------------------------------- *)
  1926 
  1927 (* ------------------------------------------------------------------------- *)
  1928 (* Note: the interpreters and printers are used in reverse order; however,   *)
  1929 (*       an interpreter that can handle non-atomic terms ends up being       *)
  1930 (*       applied before the 'stlc_interpreter' breaks the term apart into    *)
  1931 (*       subterms that are then passed to other interpreters!                *)
  1932 (* ------------------------------------------------------------------------- *)
  1933 
  1934 	(* (theory -> theory) list *)
  1935 
  1936 	val setup =
  1937 		[RefuteData.init,
  1938 		 add_interpreter "stlc"            stlc_interpreter,
  1939 		 add_interpreter "Pure"            Pure_interpreter,
  1940 		 add_interpreter "HOLogic"         HOLogic_interpreter,
  1941 		 add_interpreter "set"             set_interpreter,
  1942 		 add_interpreter "IDT"             IDT_interpreter,
  1943 		 add_interpreter "Finite_Set.card" Finite_Set_card_interpreter,
  1944 		 add_printer "stlc" stlc_printer,
  1945 		 add_printer "set"  set_printer,
  1946 		 add_printer "IDT"  IDT_printer];
  1947 
  1948 end