src/HOL/Tools/refute.ML
author webertj
Thu Nov 25 19:04:32 2004 +0100 (2004-11-25 ago)
changeset 15333 77b2bca7fcb5
parent 15292 09e218879265
child 15334 d5a92997dc1b
permissions -rw-r--r--
comments edited
     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 		(* applies a type substitution 'typeSubs' for all type variables in a  *)
   444 		(* term 't'                                                            *)
   445 		(* Term.typ Term.Vartab.table -> Term.term -> Term.term *)
   446 		fun monomorphic_term typeSubs t =
   447 			map_term_types (map_type_tvar
   448 				(fn (v,_) =>
   449 					case Vartab.lookup (typeSubs, v) of
   450 					  None =>
   451 						(* schematic type variable not instantiated *)
   452 						raise ERROR
   453 					| Some typ =>
   454 						typ)) t
   455 		(* Term.term list * Term.typ -> Term.term list *)
   456 		fun collect_type_axioms (axs, T) =
   457 			case T of
   458 			(* simple types *)
   459 			  Type ("prop", [])      => axs
   460 			| Type ("fun", [T1, T2]) => collect_type_axioms (collect_type_axioms (axs, T1), T2)
   461 			| Type ("set", [T1])     => collect_type_axioms (axs, T1)
   462 			| Type (s, Ts)           =>
   463 				let
   464 					(* look up the definition of a type, as created by "typedef" *)
   465 					(* (string * Term.term) list -> (string * Term.term) option *)
   466 					fun get_typedefn [] =
   467 						None
   468 					  | get_typedefn ((axname,ax)::axms) =
   469 						(let
   470 							(* Term.term -> Term.typ option *)
   471 							fun type_of_type_definition (Const (s', T')) =
   472 								if s'="Typedef.type_definition" then
   473 									Some T'
   474 								else
   475 									None
   476 							  | type_of_type_definition (Free _)           = None
   477 							  | type_of_type_definition (Var _)            = None
   478 							  | type_of_type_definition (Bound _)          = None
   479 							  | type_of_type_definition (Abs (_, _, body)) = type_of_type_definition body
   480 							  | type_of_type_definition (t1 $ t2)          = (case type_of_type_definition t1 of Some x => Some x | None => type_of_type_definition t2)
   481 						in
   482 							case type_of_type_definition ax of
   483 							  Some T' =>
   484 								let
   485 									val T''      = (domain_type o domain_type) T'
   486 									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', T))
   487 								in
   488 									Some (axname, monomorphic_term typeSubs ax)
   489 								end
   490 							| None =>
   491 								get_typedefn axms
   492 						end
   493 						handle ERROR           => get_typedefn axms
   494 						     | MATCH           => get_typedefn axms
   495 						     | Type.TYPE_MATCH => get_typedefn axms)
   496 				in
   497 					case DatatypePackage.datatype_info thy s of
   498 					  Some info =>  (* inductive datatype *)
   499 							(* only collect relevant type axioms for the argument types *)
   500 							foldl collect_type_axioms (axs, Ts)
   501 					| None =>
   502 						(case get_typedefn axioms of
   503 						  Some (axname, ax) => 
   504 							if mem_term (ax, axs) then
   505 								(* collect relevant type axioms for the argument types *)
   506 								foldl collect_type_axioms (axs, Ts)
   507 							else
   508 								(immediate_output (" " ^ axname);
   509 								collect_term_axioms (ax :: axs, ax))
   510 						| None =>
   511 							(* at least collect relevant type axioms for the argument types *)
   512 							foldl collect_type_axioms (axs, Ts))
   513 				end
   514 			(* TODO: include sort axioms *)
   515 			| TFree (_, sorts)       => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
   516 			| TVar  (_, sorts)       => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
   517 		(* Term.term list * Term.term -> Term.term list *)
   518 		and collect_term_axioms (axs, t) =
   519 			case t of
   520 			(* Pure *)
   521 			  Const ("all", _)                => axs
   522 			| Const ("==", _)                 => axs
   523 			| Const ("==>", _)                => axs
   524 			(* HOL *)
   525 			| Const ("Trueprop", _)           => axs
   526 			| Const ("Not", _)                => axs
   527 			| Const ("True", _)               => axs  (* redundant, since 'True' is also an IDT constructor *)
   528 			| Const ("False", _)              => axs  (* redundant, since 'False' is also an IDT constructor *)
   529 			| Const ("arbitrary", T)          => collect_type_axioms (axs, T)
   530 			| Const ("The", T)                =>
   531 				let
   532 					val ax = specialize_type (("The", T), (the o assoc) (axioms, "HOL.the_eq_trivial"))
   533 				in
   534 					if mem_term (ax, axs) then
   535 						collect_type_axioms (axs, T)
   536 					else
   537 						(immediate_output " HOL.the_eq_trivial";
   538 						collect_term_axioms (ax :: axs, ax))
   539 				end
   540 			| Const ("Hilbert_Choice.Eps", T) =>
   541 				let
   542 					val ax = specialize_type (("Hilbert_Choice.Eps", T), (the o assoc) (axioms, "Hilbert_Choice.someI"))
   543 				in
   544 					if mem_term (ax, axs) then
   545 						collect_type_axioms (axs, T)
   546 					else
   547 						(immediate_output " Hilbert_Choice.someI";
   548 						collect_term_axioms (ax :: axs, ax))
   549 				end
   550 			| Const ("All", _) $ t1           => collect_term_axioms (axs, t1)
   551 			| Const ("Ex", _) $ t1            => collect_term_axioms (axs, t1)
   552 			| Const ("op =", T)               => collect_type_axioms (axs, T)
   553 			| Const ("op &", _)               => axs
   554 			| Const ("op |", _)               => axs
   555 			| Const ("op -->", _)             => axs
   556 			(* sets *)
   557 			| Const ("Collect", T)            => collect_type_axioms (axs, T)
   558 			| Const ("op :", T)               => collect_type_axioms (axs, T)
   559 			(* other optimizations *)
   560 			| Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
   561 			(* simply-typed lambda calculus *)
   562 			| Const (s, T)                    =>
   563 				let
   564 					(* look up the definition of a constant, as created by "constdefs" *)
   565 					(* string -> Term.typ -> (string * Term.term) list -> (string * Term.term) option *)
   566 					fun get_defn [] =
   567 						None
   568 					  | get_defn ((axname,ax)::axms) =
   569 						(let
   570 							val (lhs, _) = Logic.dest_equals ax  (* equations only *)
   571 							val c        = head_of lhs
   572 							val (s', T') = dest_Const c
   573 						in
   574 							if s=s' then
   575 								let
   576 									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))
   577 								in
   578 									Some (axname, monomorphic_term typeSubs ax)
   579 								end
   580 							else
   581 								get_defn axms
   582 						end
   583 						handle ERROR           => get_defn axms
   584 						     | TERM _          => get_defn axms
   585 						     | Type.TYPE_MATCH => get_defn axms)
   586 						(* unit -> bool *)
   587 						fun is_IDT_constructor () =
   588 							(case body_type T of
   589 							  Type (s', _) =>
   590 								(case DatatypePackage.constrs_of thy s' of
   591 								  Some constrs =>
   592 									Library.exists (fn c =>
   593 										(case c of
   594 										  Const (cname, ctype) =>
   595 											cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype)
   596 										| _ =>
   597 											raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
   598 										constrs
   599 								| None =>
   600 									false)
   601 							| _  =>
   602 								false)
   603 						(* unit -> bool *)
   604 						fun is_IDT_recursor () =
   605 							(* the type of a recursion operator: [T1,...,Tn,IDT]--->TResult (where *)
   606 							(* the T1,...,Tn depend on the types of the datatype's constructors)   *)
   607 							((case last_elem (binder_types T) of
   608 							  Type (s', _) =>
   609 								(case DatatypePackage.datatype_info thy s' of
   610 								  Some info => s mem (#rec_names info)
   611 								| None      => false)  (* not an inductive datatype *)
   612 							| _ =>  (* a (free or schematic) type variable *)
   613 								false)
   614 							handle LIST "last_elem" => false)  (* not even a function type *)
   615 				in
   616 					if is_IDT_constructor () then
   617 						(* only collect relevant type axioms *)
   618 						collect_type_axioms (axs, T)
   619 					else if is_IDT_recursor () then (
   620 						(* TODO: we must add the definition of the recursion operator to the axioms, or *)
   621 						(*       (better yet, since simply unfolding the definition won't work for      *)
   622 						(*       initial fragments of recursive IDTs) write an interpreter that         *)
   623 						(*       respects it                                                            *)
   624 						warning "Term contains recursion over a datatype; countermodel(s) may be spurious!";
   625 						(* only collect relevant type axioms *)
   626 						collect_type_axioms (axs, T)
   627 					) else
   628 						(case get_defn axioms of
   629 						  Some (axname, ax) => 
   630 							if mem_term (ax, axs) then
   631 								(* collect relevant type axioms *)
   632 								collect_type_axioms (axs, T)
   633 							else
   634 								(immediate_output (" " ^ axname);
   635 								collect_term_axioms (ax :: axs, ax))
   636 						| None =>
   637 							(* collect relevant type axioms *)
   638 							collect_type_axioms (axs, T))
   639 				end
   640 			| Free (_, T)                     => collect_type_axioms (axs, T)
   641 			| Var (_, T)                      => collect_type_axioms (axs, T)
   642 			| Bound i                         => axs
   643 			| Abs (_, T, body)                => collect_term_axioms (collect_type_axioms (axs, T), body)
   644 			| t1 $ t2                         => collect_term_axioms (collect_term_axioms (axs, t1), t2)
   645 		(* universal closure over schematic variables *)
   646 		(* Term.term -> Term.term *)
   647 		fun close_form t =
   648 		let
   649 			(* (Term.indexname * Term.typ) list *)
   650 			val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   651 		in
   652 			foldl
   653 				(fn (t', ((x,i),T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
   654 				(t, vars)
   655 		end
   656 		(* Term.term list *)
   657 		val result = map close_form (collect_term_axioms ([], t))
   658 		val _ = writeln " ...done."
   659 	in
   660 		result
   661 	end;
   662 
   663 (* ------------------------------------------------------------------------- *)
   664 (* ground_types: collects all ground types in a term (including argument     *)
   665 (*               types of other types), suppressing duplicates.  Does not    *)
   666 (*               return function types, set types, non-recursive IDTs, or    *)
   667 (*               'propT'.  For IDTs, also the argument types of constructors *)
   668 (*               are considered.                                             *)
   669 (* ------------------------------------------------------------------------- *)
   670 
   671 	(* theory -> Term.term -> Term.typ list *)
   672 
   673 	fun ground_types thy t =
   674 	let
   675 		(* Term.typ * Term.typ list -> Term.typ list *)
   676 		fun collect_types (T, acc) =
   677 			if T mem acc then
   678 				acc  (* prevent infinite recursion (for IDTs) *)
   679 			else
   680 				(case T of
   681 				  Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc))
   682 				| Type ("prop", [])      => acc
   683 				| Type ("set", [T1])     => collect_types (T1, acc)
   684 				| Type (s, Ts)           =>
   685 					(case DatatypePackage.datatype_info thy s of
   686 					  Some info =>  (* inductive datatype *)
   687 						let
   688 							val index               = #index info
   689 							val descr               = #descr info
   690 							val (_, dtyps, constrs) = (the o assoc) (descr, index)
   691 							val typ_assoc           = dtyps ~~ Ts
   692 							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   693 							val _ = (if Library.exists (fn d =>
   694 									case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
   695 								then
   696 									raise REFUTE ("ground_types", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable")
   697 								else
   698 									())
   699 							(* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
   700 							fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
   701 								(* replace a 'DtTFree' variable by the associated type *)
   702 								(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
   703 							  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
   704 								let
   705 									val (s, ds, _) = (the o assoc) (descr, i)
   706 								in
   707 									Type (s, map (typ_of_dtyp descr typ_assoc) ds)
   708 								end
   709 							  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
   710 								Type (s, map (typ_of_dtyp descr typ_assoc) ds)
   711 							(* if the current type is a recursive IDT (i.e. a depth is required), add it to 'acc' *)
   712 							val acc' = (if Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
   713 									T ins acc
   714 								else
   715 									acc)
   716 							(* collect argument types *)
   717 							val acc_args = foldr collect_types (Ts, acc')
   718 							(* collect constructor types *)
   719 							val acc_constrs = foldr collect_types (flat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs), acc_args)
   720 						in
   721 							acc_constrs
   722 						end
   723 					| None =>  (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *)
   724 						T ins (foldr collect_types (Ts, acc)))
   725 				| TFree _                => T ins acc
   726 				| TVar _                 => T ins acc)
   727 	in
   728 		it_term_types collect_types (t, [])
   729 	end;
   730 
   731 (* ------------------------------------------------------------------------- *)
   732 (* string_of_typ: (rather naive) conversion from types to strings, used to   *)
   733 (*                look up the size of a type in 'sizes'.  Parameterized      *)
   734 (*                types with different parameters (e.g. "'a list" vs. "bool  *)
   735 (*                list") are identified.                                     *)
   736 (* ------------------------------------------------------------------------- *)
   737 
   738 	(* Term.typ -> string *)
   739 
   740 	fun string_of_typ (Type (s, _))     = s
   741 	  | string_of_typ (TFree (s, _))    = s
   742 	  | string_of_typ (TVar ((s,_), _)) = s;
   743 
   744 (* ------------------------------------------------------------------------- *)
   745 (* first_universe: returns the "first" (i.e. smallest) universe by assigning *)
   746 (*                 'minsize' to every type for which no size is specified in *)
   747 (*                 'sizes'                                                   *)
   748 (* ------------------------------------------------------------------------- *)
   749 
   750 	(* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *)
   751 
   752 	fun first_universe xs sizes minsize =
   753 	let
   754 		fun size_of_typ T =
   755 			case assoc (sizes, string_of_typ T) of
   756 			  Some n => n
   757 			| None   => minsize
   758 	in
   759 		map (fn T => (T, size_of_typ T)) xs
   760 	end;
   761 
   762 (* ------------------------------------------------------------------------- *)
   763 (* next_universe: enumerates all universes (i.e. assignments of sizes to     *)
   764 (*                types), where the minimal size of a type is given by       *)
   765 (*                'minsize', the maximal size is given by 'maxsize', and a   *)
   766 (*                type may have a fixed size given in 'sizes'                *)
   767 (* ------------------------------------------------------------------------- *)
   768 
   769 	(* (Term.typ * int) list -> (string * int) list -> int -> int -> (Term.typ * int) list option *)
   770 
   771 	fun next_universe xs sizes minsize maxsize =
   772 	let
   773 		(* int -> int list -> int list option *)
   774 		fun add1 _ [] =
   775 			None  (* overflow *)
   776 		  | add1 max (x::xs) =
   777 		 	if x<max orelse max<0 then
   778 				Some ((x+1)::xs)  (* add 1 to the head *)
   779 			else
   780 				apsome (fn xs' => 0 :: xs') (add1 max xs)  (* carry-over *)
   781 		(* int -> int list * int list -> int list option *)
   782 		fun shift _ (_, []) =
   783 			None
   784 		  | shift max (zeros, x::xs) =
   785 			if x=0 then
   786 				shift max (0::zeros, xs)
   787 			else
   788 				apsome (fn xs' => (x-1) :: (zeros @ xs')) (add1 max xs)
   789 		(* creates the "first" list of length 'len', where the sum of all list *)
   790 		(* elements is 'sum', and the length of the list is 'len'              *)
   791 		(* int -> int -> int -> int list option *)
   792 		fun make_first 0 sum _ =
   793 			if sum=0 then
   794 				Some []
   795 			else
   796 				None
   797 		  | make_first len sum max =
   798 			if sum<=max orelse max<0 then
   799 				apsome (fn xs' => sum :: xs') (make_first (len-1) 0 max)
   800 			else
   801 				apsome (fn xs' => max :: xs') (make_first (len-1) (sum-max) max)
   802 		(* enumerates all int lists with a fixed length, where 0<=x<='max' for *)
   803 		(* all list elements x (unless 'max'<0)                                *)
   804 		(* int -> int list -> int list option *)
   805 		fun next max xs =
   806 			(case shift max ([], xs) of
   807 			  Some xs' =>
   808 				Some xs'
   809 			| None =>
   810 				let
   811 					val (len, sum) = foldl (fn ((l, s), x) => (l+1, s+x)) ((0, 0), xs)
   812 				in
   813 					make_first len (sum+1) max  (* increment 'sum' by 1 *)
   814 				end)
   815 		(* only consider those types for which the size is not fixed *)
   816 		val mutables = filter (fn (T, _) => assoc (sizes, string_of_typ T) = None) xs
   817 		(* subtract 'minsize' from every size (will be added again at the end) *)
   818 		val diffs = map (fn (_, n) => n-minsize) mutables
   819 	in
   820 		case next (maxsize-minsize) diffs of
   821 		  Some diffs' =>
   822 			(* merge with those types for which the size is fixed *)
   823 			Some (snd (foldl_map (fn (ds, (T, _)) =>
   824 				case assoc (sizes, string_of_typ T) of
   825 				  Some n => (ds, (T, n))                      (* return the fixed size *)
   826 				| None   => (tl ds, (T, minsize + (hd ds))))  (* consume the head of 'ds', add 'minsize' *)
   827 				(diffs', xs)))
   828 		| None =>
   829 			None
   830 	end;
   831 
   832 (* ------------------------------------------------------------------------- *)
   833 (* toTrue: converts the interpretation of a Boolean value to a propositional *)
   834 (*         formula that is true iff the interpretation denotes "true"        *)
   835 (* ------------------------------------------------------------------------- *)
   836 
   837 	(* interpretation -> prop_formula *)
   838 
   839 	fun toTrue (Leaf [fm,_]) = fm
   840 	  | toTrue _             = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value");
   841 
   842 (* ------------------------------------------------------------------------- *)
   843 (* toFalse: converts the interpretation of a Boolean value to a              *)
   844 (*          propositional formula that is true iff the interpretation        *)
   845 (*          denotes "false"                                                  *)
   846 (* ------------------------------------------------------------------------- *)
   847 
   848 	(* interpretation -> prop_formula *)
   849 
   850 	fun toFalse (Leaf [_,fm]) = fm
   851 	  | toFalse _             = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");
   852 
   853 (* ------------------------------------------------------------------------- *)
   854 (* find_model: repeatedly calls 'interpret' with appropriate parameters,     *)
   855 (*             applies a SAT solver, and (in case a model is found) displays *)
   856 (*             the model to the user by calling 'print_model'                *)
   857 (* thy       : the current theory                                            *)
   858 (* {...}     : parameters that control the translation/model generation      *)
   859 (* t         : term to be translated into a propositional formula            *)
   860 (* negate    : if true, find a model that makes 't' false (rather than true) *)
   861 (* Note: exception 'TimeOut' is raised if the algorithm does not terminate   *)
   862 (*       within 'maxtime' seconds (if 'maxtime' >0)                          *)
   863 (* ------------------------------------------------------------------------- *)
   864 
   865 	(* theory -> params -> Term.term -> bool -> unit *)
   866 
   867 	fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver} t negate =
   868 	let
   869 		(* unit -> unit *)
   870 		fun wrapper () =
   871 		let
   872 			(* Term.term list *)
   873 			val axioms = collect_axioms thy t
   874 			(* Term.typ list *)
   875 			val types  = foldl (fn (acc, t') => acc union (ground_types thy t')) ([], t :: axioms)
   876 			val _      = writeln ("Ground types: "
   877 				^ (if null types then "none."
   878 				   else commas (map (Sign.string_of_typ (sign_of thy)) types)))
   879 			(* (Term.typ * int) list -> unit *)
   880 			fun find_model_loop universe =
   881 			(let
   882 				val init_model             = (universe, [])
   883 				val init_args              = {maxvars = maxvars, next_idx = 1, bounds = [], wellformed = True}
   884 				val _                      = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
   885 				(* translate 't' and all axioms *)
   886 				val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
   887 					let
   888 						val (i, m', a') = interpret thy m a t'
   889 					in
   890 						((m', a'), i)
   891 					end) ((init_model, init_args), t :: axioms)
   892 				(* make 't' either true or false, and make all axioms true, and *)
   893 				(* add the well-formedness side condition                       *)
   894 				val fm_t  = (if negate then toFalse else toTrue) (hd intrs)
   895 				val fm_ax = PropLogic.all (map toTrue (tl intrs))
   896 				val fm    = PropLogic.all [#wellformed args, fm_ax, fm_t]
   897 			in
   898 				immediate_output " invoking SAT solver...";
   899 				(case SatSolver.invoke_solver satsolver fm of
   900 				  SatSolver.SATISFIABLE assignment =>
   901 					writeln ("\n*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of Some b => b | None => true))
   902 				| _ =>  (* SatSolver.UNSATISFIABLE, SatSolver.UNKNOWN *)
   903 					(immediate_output " no model found.\n";
   904 					case next_universe universe sizes minsize maxsize of
   905 					  Some universe' => find_model_loop universe'
   906 					| None           => writeln "Search terminated, no larger universe within the given limits."))
   907 				handle SatSolver.NOT_CONFIGURED =>
   908 					error ("SAT solver " ^ quote satsolver ^ " is not configured.")
   909 			end handle MAXVARS_EXCEEDED =>
   910 				writeln ("\nSearch terminated, number of Boolean variables (" ^ string_of_int maxvars ^ " allowed) exceeded.")
   911 			| CANNOT_INTERPRET t' =>
   912 				error ("Unable to interpret term " ^ Sign.string_of_term (sign_of thy) t'))
   913 			in
   914 				find_model_loop (first_universe types sizes minsize)
   915 			end
   916 		in
   917 			(* some parameter sanity checks *)
   918 			assert (minsize>=1) ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1");
   919 			assert (maxsize>=1) ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1");
   920 			assert (maxsize>=minsize) ("\"maxsize\" (=" ^ string_of_int maxsize ^ ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ").");
   921 			assert (maxvars>=0) ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0");
   922 			assert (maxtime>=0) ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
   923 			(* enter loop with/without time limit *)
   924 			writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": "
   925 				^ Sign.string_of_term (sign_of thy) t);
   926 			if maxtime>0 then
   927 				(TimeLimit.timeLimit (Time.fromSeconds (Int.toLarge maxtime))
   928 					wrapper ()
   929 				handle TimeLimit.TimeOut =>
   930 					writeln ("\nSearch terminated, time limit ("
   931 						^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds")
   932 						^ ") exceeded."))
   933 			else
   934 				wrapper ()
   935 		end;
   936 
   937 
   938 (* ------------------------------------------------------------------------- *)
   939 (* INTERFACE, PART 2: FINDING A MODEL                                        *)
   940 (* ------------------------------------------------------------------------- *)
   941 
   942 (* ------------------------------------------------------------------------- *)
   943 (* satisfy_term: calls 'find_model' to find a model that satisfies 't'       *)
   944 (* params      : list of '(name, value)' pairs used to override default      *)
   945 (*               parameters                                                  *)
   946 (* ------------------------------------------------------------------------- *)
   947 
   948 	(* theory -> (string * string) list -> Term.term -> unit *)
   949 
   950 	fun satisfy_term thy params t =
   951 		find_model thy (actual_params thy params) t false;
   952 
   953 (* ------------------------------------------------------------------------- *)
   954 (* refute_term: calls 'find_model' to find a model that refutes 't'          *)
   955 (* params     : list of '(name, value)' pairs used to override default       *)
   956 (*              parameters                                                   *)
   957 (* ------------------------------------------------------------------------- *)
   958 
   959 	(* theory -> (string * string) list -> Term.term -> unit *)
   960 
   961 	fun refute_term thy params t =
   962 	let
   963 		(* disallow schematic type variables, since we cannot properly negate  *)
   964 		(* terms containing them (their logical meaning is that there EXISTS a *)
   965 		(* type s.t. ...; to refute such a formula, we would have to show that *)
   966 		(* for ALL types, not ...)                                             *)
   967 		val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables"
   968 		(* existential closure over schematic variables *)
   969 		(* (Term.indexname * Term.typ) list *)
   970 		val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   971 		(* Term.term *)
   972 		val ex_closure = foldl
   973 			(fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
   974 			(t, vars)
   975 		(* If 't' is of type 'propT' (rather than 'boolT'), applying  *)
   976 		(* 'HOLogic.exists_const' is not type-correct.  However, this *)
   977 		(* is not really a problem as long as 'find_model' still      *)
   978 		(* interprets the resulting term correctly, without checking  *)
   979 		(* its type.                                                  *)
   980 	in
   981 		find_model thy (actual_params thy params) ex_closure true
   982 	end;
   983 
   984 (* ------------------------------------------------------------------------- *)
   985 (* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
   986 (* params        : list of '(name, value)' pairs used to override default    *)
   987 (*                 parameters                                                *)
   988 (* subgoal       : 0-based index specifying the subgoal number               *)
   989 (* ------------------------------------------------------------------------- *)
   990 
   991 	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
   992 
   993 	fun refute_subgoal thy params thm subgoal =
   994 		refute_term thy params (nth_elem (subgoal, prems_of thm));
   995 
   996 
   997 (* ------------------------------------------------------------------------- *)
   998 (* INTERPRETERS: Auxiliary Functions                                         *)
   999 (* ------------------------------------------------------------------------- *)
  1000 
  1001 (* ------------------------------------------------------------------------- *)
  1002 (* make_constants: returns all interpretations that have the same tree       *)
  1003 (*                 structure as 'intr', but consist of unit vectors with     *)
  1004 (*                 'True'/'False' only (no Boolean variables)                *)
  1005 (* ------------------------------------------------------------------------- *)
  1006 
  1007 	(* interpretation -> interpretation list *)
  1008 
  1009 	fun make_constants intr =
  1010 	let
  1011 		(* returns a list with all unit vectors of length n *)
  1012 		(* int -> interpretation list *)
  1013 		fun unit_vectors n =
  1014 		let
  1015 			(* returns the k-th unit vector of length n *)
  1016 			(* int * int -> interpretation *)
  1017 			fun unit_vector (k,n) =
  1018 				Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1019 			(* int -> interpretation list -> interpretation list *)
  1020 			fun unit_vectors_acc k vs =
  1021 				if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1022 		in
  1023 			unit_vectors_acc 1 []
  1024 		end
  1025 		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1026 		(* 'a -> 'a list list -> 'a list list *)
  1027 		fun cons_list x xss =
  1028 			map (fn xs => x::xs) xss
  1029 		(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1030 		(* int -> 'a list -> 'a list list *)
  1031 		fun pick_all 1 xs =
  1032 			map (fn x => [x]) xs
  1033 		  | pick_all n xs =
  1034 			let val rec_pick = pick_all (n-1) xs in
  1035 				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1036 			end
  1037 	in
  1038 		case intr of
  1039 		  Leaf xs => unit_vectors (length xs)
  1040 		| Node xs => map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1041 	end;
  1042 
  1043 (* ------------------------------------------------------------------------- *)
  1044 (* size_of_type: returns the number of constants in a type (i.e. 'length     *)
  1045 (*               (make_constants intr)', but implemented more efficiently)   *)
  1046 (* ------------------------------------------------------------------------- *)
  1047 
  1048 	(* interpretation -> int *)
  1049 
  1050 	fun size_of_type intr =
  1051 	let
  1052 		(* power(a,b) computes a^b, for a>=0, b>=0 *)
  1053 		(* int * int -> int *)
  1054 		fun power (a,0) = 1
  1055 		  | power (a,1) = a
  1056 		  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
  1057 	in
  1058 		case intr of
  1059 		  Leaf xs => length xs
  1060 		| Node xs => power (size_of_type (hd xs), length xs)
  1061 	end;
  1062 
  1063 (* ------------------------------------------------------------------------- *)
  1064 (* TT/FF: interpretations that denote "true" or "false", respectively        *)
  1065 (* ------------------------------------------------------------------------- *)
  1066 
  1067 	(* interpretation *)
  1068 
  1069 	val TT = Leaf [True, False];
  1070 
  1071 	val FF = Leaf [False, True];
  1072 
  1073 (* ------------------------------------------------------------------------- *)
  1074 (* make_equality: returns an interpretation that denotes (extensional)       *)
  1075 (*                equality of two interpretations                            *)
  1076 (* ------------------------------------------------------------------------- *)
  1077 
  1078 	(* We could in principle represent '=' on a type T by a particular        *)
  1079 	(* interpretation.  However, the size of that interpretation is quadratic *)
  1080 	(* in the size of T.  Therefore comparing the interpretations 'i1' and    *)
  1081 	(* 'i2' directly is more efficient than constructing the interpretation   *)
  1082 	(* for equality on T first, and "applying" this interpretation to 'i1'    *)
  1083 	(* and 'i2' in the usual way (cf. 'interpretation_apply') then.           *)
  1084 
  1085 	(* interpretation * interpretation -> interpretation *)
  1086 
  1087 	fun make_equality (i1, i2) =
  1088 	let
  1089 		(* interpretation * interpretation -> prop_formula *)
  1090 		fun equal (i1, i2) =
  1091 			(case i1 of
  1092 			  Leaf xs =>
  1093 				(case i2 of
  1094 				  Leaf ys => PropLogic.dot_product (xs, ys)
  1095 				| Node _  => raise REFUTE ("make_equality", "second interpretation is higher"))
  1096 			| Node xs =>
  1097 				(case i2 of
  1098 				  Leaf _  => raise REFUTE ("make_equality", "first interpretation is higher")
  1099 				| Node ys => PropLogic.all (map equal (xs ~~ ys))))
  1100 		(* interpretation * interpretation -> prop_formula *)
  1101 		fun not_equal (i1, i2) =
  1102 			(case i1 of
  1103 			  Leaf xs =>
  1104 				(case i2 of
  1105 				  Leaf ys => PropLogic.all ((PropLogic.exists xs) :: (PropLogic.exists ys) ::
  1106 					(map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys)))  (* defined and not equal *)
  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.exists (map not_equal (xs ~~ ys))))
  1112 	in
  1113 		(* a value may be undefined; therefore 'not_equal' is not just the     *)
  1114 		(* negation of 'equal':                                                *)
  1115 		(* - two interpretations are 'equal' iff they are both defined and     *)
  1116 		(*   denote the same value                                             *)
  1117 		(* - two interpretations are 'not_equal' iff they are both defined at  *)
  1118 		(*   least partially, and a defined part denotes different values      *)
  1119 		(* - an undefined interpretation is neither 'equal' nor 'not_equal' to *)
  1120 		(*   another value                                                     *)
  1121 		Leaf [equal (i1, i2), not_equal (i1, i2)]
  1122 	end;
  1123 
  1124 (* ------------------------------------------------------------------------- *)
  1125 (* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions      *)
  1126 (* ------------------------------------------------------------------------- *)
  1127 
  1128 	(* Term.term -> int -> Term.term *)
  1129 
  1130 	fun eta_expand t i =
  1131 	let
  1132 		val Ts = binder_types (fastype_of t)
  1133 	in
  1134 		foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
  1135 			(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
  1136 	end;
  1137 
  1138 
  1139 (* ------------------------------------------------------------------------- *)
  1140 (* INTERPRETERS: Actual Interpreters                                         *)
  1141 (* ------------------------------------------------------------------------- *)
  1142 
  1143 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1144 
  1145 	(* simply typed lambda calculus: Isabelle's basic term syntax, with type  *)
  1146 	(* variables, function types, and propT                                   *)
  1147 
  1148 	fun stlc_interpreter thy model args t =
  1149 	let
  1150 		val (typs, terms)                           = model
  1151 		val {maxvars, next_idx, bounds, wellformed} = args
  1152 		(* Term.typ -> (interpretation * model * arguments) option *)
  1153 		fun interpret_groundterm T =
  1154 		let
  1155 			(* unit -> (interpretation * model * arguments) option *)
  1156 			fun interpret_groundtype () =
  1157 			let
  1158 				val size = (if T = Term.propT then 2 else (the o assoc) (typs, T))                      (* the model MUST specify a size for ground types *)
  1159 				val next = (if size=1 then next_idx else if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 1 or 2 *)
  1160 				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())    (* check if 'maxvars' is large enough *)
  1161 				(* prop_formula list *)
  1162 				val fms  = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
  1163 					else (map BoolVar (next_idx upto (next_idx+size-1))))
  1164 				(* interpretation *)
  1165 				val intr = Leaf fms
  1166 				(* prop_formula list -> prop_formula *)
  1167 				fun one_of_two_false []      = True
  1168 				  | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs)
  1169 				(* prop_formula list -> prop_formula *)
  1170 				fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
  1171 				(* prop_formula *)
  1172 				val wf   = (if size=1 then True else if size=2 then True else exactly_one_true fms)
  1173 			in
  1174 				(* extend the model, increase 'next_idx', add well-formedness condition *)
  1175 				Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
  1176 			end
  1177 		in
  1178 			case T of
  1179 			  Type ("fun", [T1, T2]) =>
  1180 				let
  1181 					(* we create 'size_of_type (interpret (... T1))' different copies *)
  1182 					(* of the interpretation for 'T2', which are then combined into a *)
  1183 					(* single new interpretation                                      *)
  1184 					val (i1, _, _) =
  1185 						(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
  1186 						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1187 					(* make fresh copies, with different variable indices *)
  1188 					(* 'idx': next variable index                         *)
  1189 					(* 'n'  : number of copies                            *)
  1190 					(* int -> int -> (int * interpretation list * prop_formula *)
  1191 					fun make_copies idx 0 =
  1192 						(idx, [], True)
  1193 					  | make_copies idx n =
  1194 						let
  1195 							val (copy, _, new_args) =
  1196 								(interpret thy (typs, []) {maxvars = maxvars, next_idx = idx, bounds = [], wellformed = True} (Free ("dummy", T2))
  1197 								handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1198 							val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1)
  1199 						in
  1200 							(idx', copy :: copies, SAnd (#wellformed new_args, wf'))
  1201 						end
  1202 					val (next, copies, wf) = make_copies next_idx (size_of_type i1)
  1203 					(* combine copies into a single interpretation *)
  1204 					val intr = Node copies
  1205 				in
  1206 					(* extend the model, increase 'next_idx', add well-formedness condition *)
  1207 					Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
  1208 				end
  1209 			| Type _  => interpret_groundtype ()
  1210 			| TFree _ => interpret_groundtype ()
  1211 			| TVar  _ => interpret_groundtype ()
  1212 		end
  1213 	in
  1214 		case assoc (terms, t) of
  1215 		  Some intr =>
  1216 			(* return an existing interpretation *)
  1217 			Some (intr, model, args)
  1218 		| None =>
  1219 			(case t of
  1220 			  Const (_, T)     =>
  1221 				interpret_groundterm T
  1222 			| Free (_, T)      =>
  1223 				interpret_groundterm T
  1224 			| Var (_, T)       =>
  1225 				interpret_groundterm T
  1226 			| Bound i          =>
  1227 				Some (nth_elem (i, #bounds args), model, args)
  1228 			| Abs (x, T, body) =>
  1229 				let
  1230 					(* create all constants of type 'T' *)
  1231 					val (i, _, _) =
  1232 						(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1233 						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1234 					val constants = make_constants i
  1235 					(* interpret the 'body' separately for each constant *)
  1236 					val ((model', args'), bodies) = foldl_map
  1237 						(fn ((m,a), c) =>
  1238 							let
  1239 								(* add 'c' to 'bounds' *)
  1240 								val (i', m', a') = interpret thy m {maxvars = #maxvars a, next_idx = #next_idx a, bounds = (c :: #bounds a), wellformed = #wellformed a} body
  1241 							in
  1242 								(* keep the new model m' and 'next_idx' and 'wellformed', but use old 'bounds' *)
  1243 								((m', {maxvars = maxvars, next_idx = #next_idx a', bounds = bounds, wellformed = #wellformed a'}), i')
  1244 							end)
  1245 						((model, args), constants)
  1246 				in
  1247 					Some (Node bodies, model', args')
  1248 				end
  1249 			| t1 $ t2          =>
  1250 				let
  1251 					(* auxiliary functions *)
  1252 					(* interpretation * interpretation -> interpretation *)
  1253 					fun interpretation_disjunction (tr1,tr2) =
  1254 						tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
  1255 					(* prop_formula * interpretation -> interpretation *)
  1256 					fun prop_formula_times_interpretation (fm,tr) =
  1257 						tree_map (map (fn x => SAnd (fm,x))) tr
  1258 					(* prop_formula list * interpretation list -> interpretation *)
  1259 					fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
  1260 						prop_formula_times_interpretation (fm,tr)
  1261 					  | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
  1262 						interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees))
  1263 					  | prop_formula_list_dot_product_interpretation_list (_,_) =
  1264 						raise REFUTE ("stlc_interpreter", "empty list (in dot product)")
  1265 					(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1266 					(* 'a -> 'a list list -> 'a list list *)
  1267 					fun cons_list x xss =
  1268 						map (fn xs => x::xs) xss
  1269 					(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
  1270 					(* 'a list list -> 'a list list *)
  1271 					fun pick_all [xs] =
  1272 						map (fn x => [x]) xs
  1273 					  | pick_all (xs::xss) =
  1274 						let val rec_pick = pick_all xss in
  1275 							foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1276 						end
  1277 					  | pick_all _ =
  1278 						raise REFUTE ("stlc_interpreter", "empty list (in pick_all)")
  1279 					(* interpretation -> prop_formula list *)
  1280 					fun interpretation_to_prop_formula_list (Leaf xs) =
  1281 						xs
  1282 					  | interpretation_to_prop_formula_list (Node trees) =
  1283 						map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees))
  1284 					(* interpretation * interpretation -> interpretation *)
  1285 					fun interpretation_apply (tr1,tr2) =
  1286 						(case tr1 of
  1287 						  Leaf _ =>
  1288 							raise REFUTE ("stlc_interpreter", "first interpretation is a leaf")
  1289 						| Node xs =>
  1290 							prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs))
  1291 					(* interpret 't1' and 't2' separately *)
  1292 					val (intr1, model1, args1) = interpret thy model args t1
  1293 					val (intr2, model2, args2) = interpret thy model1 args1 t2
  1294 				in
  1295 					Some (interpretation_apply (intr1,intr2), model2, args2)
  1296 				end)
  1297 	end;
  1298 
  1299 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1300 
  1301 	fun Pure_interpreter thy model args t =
  1302 		case t of
  1303 		  Const ("all", _) $ t1 =>  (* in the meta-logic, 'all' MUST be followed by an argument term *)
  1304 			let
  1305 				val (i, m, a) = interpret thy model args t1
  1306 			in
  1307 				case i of
  1308 				  Node xs =>
  1309 					let
  1310 						val fmTrue  = PropLogic.all (map toTrue xs)
  1311 						val fmFalse = PropLogic.exists (map toFalse xs)
  1312 					in
  1313 						Some (Leaf [fmTrue, fmFalse], m, a)
  1314 					end
  1315 				| _ =>
  1316 					raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function")
  1317 			end
  1318 		| Const ("==", _) $ t1 $ t2 =>
  1319 			let
  1320 				val (i1, m1, a1) = interpret thy model args t1
  1321 				val (i2, m2, a2) = interpret thy m1 a1 t2
  1322 			in
  1323 				Some (make_equality (i1, i2), m2, a2)
  1324 			end
  1325 		| Const ("==>", _) =>  (* simpler than translating 'Const ("==>", _) $ t1 $ t2' *)
  1326 			Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
  1327 		| _ => None;
  1328 
  1329 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1330 
  1331 	fun HOLogic_interpreter thy model args t =
  1332 	(* ------------------------------------------------------------------------- *)
  1333 	(* Providing interpretations directly is more efficient than unfolding the   *)
  1334 	(* logical constants.  In HOL however, logical constants can themselves be   *)
  1335 	(* arguments.  "All" and "Ex" are then translated just like any other        *)
  1336 	(* constant, with the relevant axiom being added by 'collect_axioms'.        *)
  1337 	(* ------------------------------------------------------------------------- *)
  1338 		case t of
  1339 		  Const ("Trueprop", _) =>
  1340 			Some (Node [TT, FF], model, args)
  1341 		| Const ("Not", _) =>
  1342 			Some (Node [FF, TT], model, args)
  1343 		| Const ("True", _) =>  (* redundant, since 'True' is also an IDT constructor *)
  1344 			Some (TT, model, args)
  1345 		| Const ("False", _) =>  (* redundant, since 'False' is also an IDT constructor *)
  1346 			Some (FF, model, args)
  1347 		| Const ("All", _) $ t1 =>
  1348 		(* if "All" occurs without an argument (i.e. as argument to a higher-order *)
  1349 		(* function or  predicate), it is handled by the 'stlc_interpreter' (i.e.  *)
  1350 		(* by unfolding its definition)                                            *)
  1351 			let
  1352 				val (i, m, a) = interpret thy model args t1
  1353 			in
  1354 				case i of
  1355 				  Node xs =>
  1356 					let
  1357 						val fmTrue  = PropLogic.all (map toTrue xs)
  1358 						val fmFalse = PropLogic.exists (map toFalse xs)
  1359 					in
  1360 						Some (Leaf [fmTrue, fmFalse], m, a)
  1361 					end
  1362 				| _ =>
  1363 					raise REFUTE ("HOLogic_interpreter", "\"All\" is followed by a non-function")
  1364 			end
  1365 		| Const ("Ex", _) $ t1 =>
  1366 		(* if "Ex" occurs without an argument (i.e. as argument to a higher-order  *)
  1367 		(* function or  predicate), it is handled by the 'stlc_interpreter' (i.e.  *)
  1368 		(* by unfolding its definition)                                            *)
  1369 			let
  1370 				val (i, m, a) = interpret thy model args t1
  1371 			in
  1372 				case i of
  1373 				  Node xs =>
  1374 					let
  1375 						val fmTrue  = PropLogic.exists (map toTrue xs)
  1376 						val fmFalse = PropLogic.all (map toFalse xs)
  1377 					in
  1378 						Some (Leaf [fmTrue, fmFalse], m, a)
  1379 					end
  1380 				| _ =>
  1381 					raise REFUTE ("HOLogic_interpreter", "\"Ex\" is followed by a non-function")
  1382 			end
  1383 		| Const ("op =", _) $ t1 $ t2 =>
  1384 			let
  1385 				val (i1, m1, a1) = interpret thy model args t1
  1386 				val (i2, m2, a2) = interpret thy m1 a1 t2
  1387 			in
  1388 				Some (make_equality (i1, i2), m2, a2)
  1389 			end
  1390 		| Const ("op =", _) $ t1 =>
  1391 			(Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1392 		| Const ("op =", _) =>
  1393 			(Some (interpret thy model args (eta_expand t 2)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1394 		| Const ("op &", _) =>
  1395 			Some (Node [Node [TT, FF], Node [FF, FF]], model, args)
  1396 		| Const ("op |", _) =>
  1397 			Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
  1398 		| Const ("op -->", _) =>
  1399 			Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
  1400 		| _ => None;
  1401 
  1402 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1403 
  1404 	fun set_interpreter thy model args t =
  1405 	(* "T set" is isomorphic to "T --> bool" *)
  1406 	let
  1407 		val (typs, terms) = model
  1408 	in
  1409 		case assoc (terms, t) of
  1410 		  Some intr =>
  1411 			(* return an existing interpretation *)
  1412 			Some (intr, model, args)
  1413 		| None =>
  1414 			(case t of
  1415 			  Free (x, Type ("set", [T])) =>
  1416 				(let
  1417 					val (intr, _, args') = interpret thy (typs, []) args (Free (x, T --> HOLogic.boolT))
  1418 				in
  1419 					Some (intr, (typs, (t, intr)::terms), args')
  1420 				end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1421 			| Var ((x,i), Type ("set", [T])) =>
  1422 				(let
  1423 					val (intr, _, args') = interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT))
  1424 				in
  1425 					Some (intr, (typs, (t, intr)::terms), args')
  1426 				end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1427 			| Const (s, Type ("set", [T])) =>
  1428 				(let
  1429 					val (intr, _, args') = interpret thy (typs, []) args (Const (s, T --> HOLogic.boolT))
  1430 				in
  1431 					Some (intr, (typs, (t, intr)::terms), args')
  1432 				end handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1433 			(* 'Collect' == identity *)
  1434 			| Const ("Collect", _) $ t1 =>
  1435 				Some (interpret thy model args t1)
  1436 			| Const ("Collect", _) =>
  1437 				(Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1438 			(* 'op :' == application *)
  1439 			| Const ("op :", _) $ t1 $ t2 =>
  1440 				Some (interpret thy model args (t2 $ t1))
  1441 			| Const ("op :", _) $ t1 =>
  1442 				(Some (interpret thy model args (eta_expand t 1)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1443 			| Const ("op :", _) =>
  1444 				(Some (interpret thy model args (eta_expand t 2)) handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1445 			| _ => None)
  1446 	end;
  1447 
  1448 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1449 
  1450 	fun IDT_interpreter thy model args t =
  1451 	let
  1452 		val (typs, terms) = model
  1453 		(* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
  1454 		fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
  1455 			(* replace a 'DtTFree' variable by the associated type *)
  1456 			(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
  1457 		  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
  1458 			let
  1459 				val (s, ds, _) = (the o assoc) (descr, i)
  1460 			in
  1461 				Type (s, map (typ_of_dtyp descr typ_assoc) ds)
  1462 			end
  1463 		  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
  1464 			Type (s, map (typ_of_dtyp descr typ_assoc) ds)
  1465 		(* int list -> int *)
  1466 		fun sum xs = foldl op+ (0, xs)
  1467 		(* int list -> int *)
  1468 		fun product xs = foldl op* (1, xs)
  1469 		(* the size of an IDT is the sum (over its constructors) of the        *)
  1470 		(* product (over their arguments) of the size of the argument type     *)
  1471 		(* (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *)
  1472 		fun size_of_dtyp typs descr typ_assoc constrs =
  1473 			sum (map (fn (_, ds) =>
  1474 				product (map (fn d =>
  1475 					let
  1476 						val T         = typ_of_dtyp descr typ_assoc d
  1477 						val (i, _, _) =
  1478 							(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1479 							handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1480 					in
  1481 						size_of_type i
  1482 					end) ds)) constrs)
  1483 		(* Term.typ -> (interpretation * model * arguments) option *)
  1484 		fun interpret_variable (Type (s, Ts)) =
  1485 			(case DatatypePackage.datatype_info thy s of
  1486 			  Some info =>  (* inductive datatype *)
  1487 				let
  1488 					val (typs, terms) = model
  1489 					(* int option -- only recursive IDTs have an associated depth *)
  1490 					val depth         = assoc (typs, Type (s, Ts))
  1491 				in
  1492 					if depth = (Some 0) then  (* termination condition to avoid infinite recursion *)
  1493 						(* return a leaf of size 0 *)
  1494 						Some (Leaf [], model, args)
  1495 					else
  1496 						let
  1497 							val index               = #index info
  1498 							val descr               = #descr info
  1499 							val (_, dtyps, constrs) = (the o assoc) (descr, index)
  1500 							val typ_assoc           = dtyps ~~ Ts
  1501 							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1502 							val _ = (if Library.exists (fn d =>
  1503 									case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
  1504 								then
  1505 									raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable")
  1506 								else
  1507 									())
  1508 							(* if the model specifies a depth for the current type, decrement it to avoid infinite recursion *)
  1509 							val typs'    = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1)))
  1510 							(* recursively compute the size of the datatype *)
  1511 							val size     = size_of_dtyp typs' descr typ_assoc constrs
  1512 							val next_idx = #next_idx args
  1513 							val next     = (if size=1 then next_idx else if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 1 or size 2 *)
  1514 							val _        = (if next-1>(#maxvars args) andalso (#maxvars args)>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
  1515 							(* prop_formula list *)
  1516 							val fms      = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
  1517 								else (map BoolVar (next_idx upto (next_idx+size-1))))
  1518 							(* interpretation *)
  1519 							val intr     = Leaf fms
  1520 							(* prop_formula list -> prop_formula *)
  1521 							fun one_of_two_false []      = True
  1522 							  | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs)
  1523 							(* prop_formula list -> prop_formula *)
  1524 							fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
  1525 							(* prop_formula *)
  1526 							val wf       = (if size=1 then True else if size=2 then True else exactly_one_true fms)
  1527 						in
  1528 							(* extend the model, increase 'next_idx', add well-formedness condition *)
  1529 							Some (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)})
  1530 						end
  1531 				end
  1532 			| None =>  (* not an inductive datatype *)
  1533 				None)
  1534 		  | interpret_variable _ =  (* a (free or schematic) type variable *)
  1535 			None
  1536 	in
  1537 		case assoc (terms, t) of
  1538 		  Some intr =>
  1539 			(* return an existing interpretation *)
  1540 			Some (intr, model, args)
  1541 		| None =>
  1542 			(case t of
  1543 			  Free (_, T)  => interpret_variable T
  1544 			| Var (_, T)   => interpret_variable T
  1545 			| Const (s, T) =>
  1546 				(* TODO: case, recursion, size *)
  1547 				let
  1548 					(* unit -> (interpretation * model * arguments) option *)
  1549 					fun interpret_constructor () =
  1550 						(case body_type T of
  1551 						  Type (s', Ts') =>
  1552 							(case DatatypePackage.datatype_info thy s' of
  1553 							  Some info =>  (* body type is an inductive datatype *)
  1554 								let
  1555 									val index               = #index info
  1556 									val descr               = #descr info
  1557 									val (_, dtyps, constrs) = (the o assoc) (descr, index)
  1558 									val typ_assoc           = dtyps ~~ Ts'
  1559 									(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1560 									val _ = (if Library.exists (fn d =>
  1561 											case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
  1562 										then
  1563 											raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s', Ts')) ^ ") is not a variable")
  1564 										else
  1565 											())
  1566 									(* split the constructors into those occuring before/after 'Const (s, T)' *)
  1567 									val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
  1568 										not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T,
  1569 											map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs
  1570 								in
  1571 									case constrs2 of
  1572 									  [] =>
  1573 										(* 'Const (s, T)' is not a constructor of this datatype *)
  1574 										None
  1575 									| c::cs =>
  1576 										let
  1577 											(* int option -- only recursive IDTs have an associated depth *)
  1578 											val depth = assoc (typs, Type (s', Ts'))
  1579 											val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s', Ts'), n-1)))
  1580 											(* constructors before 'Const (s, T)' generate elements of the datatype *)
  1581 											val offset  = size_of_dtyp typs' descr typ_assoc constrs1
  1582 											(* 'Const (s, T)' and constructors after it generate elements of the datatype *)
  1583 											val total   = offset + (size_of_dtyp typs' descr typ_assoc constrs2)
  1584 											(* create an interpretation that corresponds to the constructor 'Const (s, T)' *)
  1585 											(* by recursion over its argument types                                        *)
  1586 											(* DatatypeAux.dtyp list -> interpretation *)
  1587 											fun make_partial [] =
  1588 												(* all entries of the leaf are 'False' *)
  1589 												Leaf (replicate total False)
  1590 											  | make_partial (d::ds) =
  1591 												let
  1592 													(* compute the "new" size of the type 'd' *)
  1593 													val T         = typ_of_dtyp descr typ_assoc d
  1594 													val (i, _, _) =
  1595 														(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1596 														handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1597 												in
  1598 													(* all entries of the whole subtree are 'False' *)
  1599 													Node (replicate (size_of_type i) (make_partial ds))
  1600 												end
  1601 											(* int * DatatypeAux.dtyp list -> int * interpretation *)
  1602 											fun make_constr (offset, []) =
  1603 												if offset<total then
  1604 													(offset+1, Leaf ((replicate offset False) @ True :: (replicate (total-offset-1) False)))
  1605 												else
  1606 													raise REFUTE ("IDT_interpreter", "internal error: offset >= total")
  1607 											  | make_constr (offset, d::ds) =
  1608 												let
  1609 													(* compute the "new" and "old" size of the type 'd' *)
  1610 													val T         = typ_of_dtyp descr typ_assoc d
  1611 													val (i, _, _) =
  1612 														(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1613 														handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1614 													val (i', _, _) =
  1615 														(interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1616 														handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1617 													val size  = size_of_type i
  1618 													val size' = size_of_type i'
  1619 													val _ = if size<size' then
  1620 															raise REFUTE ("IDT_interpreter", "internal error: new size < old size")
  1621 														else
  1622 															()
  1623 													val (new_offset, intrs) = foldl_map make_constr (offset, replicate size' ds)
  1624 												in
  1625 													(* the first size' elements of the type actually yield a result *)
  1626 													(* element, while the remaining size-size' elements don't       *)
  1627 													(new_offset, Node (intrs @ (replicate (size-size') (make_partial ds))))
  1628 												end
  1629 										in
  1630 											Some ((snd o make_constr) (offset, snd c), model, args)
  1631 										end
  1632 								end
  1633 							| None =>  (* body type is not an inductive datatype *)
  1634 								None)
  1635 						| _ =>  (* body type is a (free or schematic) type variable *)
  1636 							None)
  1637 				in
  1638 					case interpret_constructor () of
  1639 					  Some x => Some x
  1640 					| None   => interpret_variable T
  1641 				end
  1642 			| _ => None)
  1643 	end;
  1644 
  1645 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1646 
  1647 	(* only an optimization: 'card' could in principle be interpreted with    *)
  1648 	(* interpreters available already (using its definition), but the code    *)
  1649 	(* below is much more efficient                                           *)
  1650 
  1651 	fun Finite_Set_card_interpreter thy model args t =
  1652 		case t of
  1653 		  Const ("Finite_Set.card", Type ("fun", [Type ("set", [T]), Type ("nat", [])])) =>
  1654 			let
  1655 				val (i_nat, _, _) =
  1656 					(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
  1657 						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1658 				val size_nat      = size_of_type i_nat
  1659 				val (i_set, _, _) =
  1660 					(interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T])))
  1661 						handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1662 				val constants     = make_constants i_set
  1663 				(* interpretation -> int *)
  1664 				fun number_of_elements (Node xs) =
  1665 					foldl (fn (n, x) =>
  1666 						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)
  1667 				  | number_of_elements (Leaf _) =
  1668 					raise REFUTE ("Finite_Set_card_interpreter", "interpretation for set type is a leaf")
  1669 				(* takes an interpretation for a set and returns an interpretation for a 'nat' *)
  1670 				(* interpretation -> interpretation *)
  1671 				fun card i =
  1672 					let
  1673 						val n = number_of_elements i
  1674 					in
  1675 						if n<size_nat then
  1676 							Leaf ((replicate n False) @ True :: (replicate (size_nat-n-1) False))
  1677 						else
  1678 							Leaf (replicate size_nat False)
  1679 					end
  1680 			in
  1681 				Some (Node (map card constants), model, args)
  1682 			end
  1683 		| _ =>
  1684 			None;
  1685 
  1686 
  1687 (* ------------------------------------------------------------------------- *)
  1688 (* PRINTERS                                                                  *)
  1689 (* ------------------------------------------------------------------------- *)
  1690 
  1691 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option *)
  1692 
  1693 	fun stlc_printer thy model t intr assignment =
  1694 	let
  1695 		(* Term.term -> Term.typ option *)
  1696 		fun typeof (Free (_, T))  = Some T
  1697 		  | typeof (Var (_, T))   = Some T
  1698 		  | typeof (Const (_, T)) = Some T
  1699 		  | typeof _              = None
  1700 		(* string -> string *)
  1701 		fun strip_leading_quote s =
  1702 			(implode o (fn ss => case ss of [] => [] | x::xs => if x="'" then xs else ss) o explode) s
  1703 		(* Term.typ -> string *)
  1704 		fun string_of_typ (Type (s, _))     = s
  1705 		  | string_of_typ (TFree (x, _))    = strip_leading_quote x
  1706 		  | string_of_typ (TVar ((x,i), _)) = strip_leading_quote x ^ string_of_int i
  1707 		(* interpretation -> int *)
  1708 		fun index_from_interpretation (Leaf xs) =
  1709 			let
  1710 				val idx = find_index (PropLogic.eval assignment) xs
  1711 			in
  1712 				if idx<0 then
  1713 					raise REFUTE ("stlc_printer", "illegal interpretation: no value assigned (SAT solver unsound?)")
  1714 				else
  1715 					idx
  1716 			end
  1717 		  | index_from_interpretation _ =
  1718 			raise REFUTE ("stlc_printer", "interpretation for ground type is not a leaf")
  1719 	in
  1720 		case typeof t of
  1721 		  Some T =>
  1722 			(case T of
  1723 			  Type ("fun", [T1, T2]) =>
  1724 				(let
  1725 					(* create all constants of type 'T1' *)
  1726 					val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
  1727 					val constants = make_constants i
  1728 					(* interpretation list *)
  1729 					val results = (case intr of
  1730 						  Node xs => xs
  1731 						| _       => raise REFUTE ("stlc_printer", "interpretation for function type is a leaf"))
  1732 					(* Term.term list *)
  1733 					val pairs = map (fn (arg, result) =>
  1734 						HOLogic.mk_prod
  1735 							(print thy model (Free ("dummy", T1)) arg assignment,
  1736 							 print thy model (Free ("dummy", T2)) result assignment))
  1737 						(constants ~~ results)
  1738 					(* Term.typ *)
  1739 					val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
  1740 					val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
  1741 					(* Term.term *)
  1742 					val HOLogic_empty_set = Const ("{}", HOLogic_setT)
  1743 					val HOLogic_insert    = Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
  1744 				in
  1745 					Some (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
  1746 				end handle CANNOT_INTERPRET _ => None)
  1747 			| Type ("prop", [])      =>
  1748 				(case index_from_interpretation intr of
  1749 				  0 => Some (HOLogic.mk_Trueprop HOLogic.true_const)
  1750 				| 1 => Some (HOLogic.mk_Trueprop HOLogic.false_const)
  1751 				| _ => raise REFUTE ("stlc_interpreter", "illegal interpretation for a propositional value"))
  1752 			| Type _  => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
  1753 			| TFree _ => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
  1754 			| TVar _  => Some (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T)))
  1755 		| None =>
  1756 			None
  1757 	end;
  1758 
  1759 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1760 
  1761 	fun set_printer thy model t intr assignment =
  1762 	let
  1763 		(* Term.term -> Term.typ option *)
  1764 		fun typeof (Free (_, T))  = Some T
  1765 		  | typeof (Var (_, T))   = Some T
  1766 		  | typeof (Const (_, T)) = Some T
  1767 		  | typeof _              = None
  1768 	in
  1769 		case typeof t of
  1770 		  Some (Type ("set", [T])) =>
  1771 			(let
  1772 				(* create all constants of type 'T' *)
  1773 				val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1774 				val constants = make_constants i
  1775 				(* interpretation list *)
  1776 				val results = (case intr of
  1777 					  Node xs => xs
  1778 					| _       => raise REFUTE ("set_printer", "interpretation for set type is a leaf"))
  1779 				(* Term.term list *)
  1780 				val elements = mapfilter (fn (arg, result) =>
  1781 					case result of
  1782 					  Leaf [fmTrue, fmFalse] =>
  1783 						if PropLogic.eval assignment fmTrue then
  1784 							Some (print thy model (Free ("dummy", T)) arg assignment)
  1785 						else if PropLogic.eval assignment fmFalse then
  1786 							None
  1787 						else
  1788 							raise REFUTE ("set_printer", "illegal interpretation: no value assigned (SAT solver unsound?)")
  1789 					| _ =>
  1790 						raise REFUTE ("set_printer", "illegal interpretation for a Boolean value"))
  1791 					(constants ~~ results)
  1792 				(* Term.typ *)
  1793 				val HOLogic_setT  = HOLogic.mk_setT T
  1794 				(* Term.term *)
  1795 				val HOLogic_empty_set = Const ("{}", HOLogic_setT)
  1796 				val HOLogic_insert    = Const ("insert", T --> HOLogic_setT --> HOLogic_setT)
  1797 			in
  1798 				Some (foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) (HOLogic_empty_set, elements))
  1799 			end handle CANNOT_INTERPRET _ => None)
  1800 		| _ =>
  1801 			None
  1802 	end;
  1803 
  1804 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term option *)
  1805 
  1806 	fun IDT_printer thy model t intr assignment =
  1807 	let
  1808 		(* Term.term -> Term.typ option *)
  1809 		fun typeof (Free (_, T))  = Some T
  1810 		  | typeof (Var (_, T))   = Some T
  1811 		  | typeof (Const (_, T)) = Some T
  1812 		  | typeof _              = None
  1813 	in
  1814 		case typeof t of
  1815 		  Some (Type (s, Ts)) =>
  1816 			(case DatatypePackage.datatype_info thy s of
  1817 			  Some info =>  (* inductive datatype *)
  1818 				let
  1819 					val (typs, _)           = model
  1820 					val index               = #index info
  1821 					val descr               = #descr info
  1822 					val (_, dtyps, constrs) = (the o assoc) (descr, index)
  1823 					val typ_assoc           = dtyps ~~ Ts
  1824 					(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1825 					val _ = (if Library.exists (fn d =>
  1826 							case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
  1827 						then
  1828 							raise REFUTE ("IDT_printer", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable")
  1829 						else
  1830 							())
  1831 					(* the index of the element in the datatype *)
  1832 					val element = (case intr of
  1833 						  Leaf xs => find_index (PropLogic.eval assignment) xs
  1834 						| Node _  => raise REFUTE ("IDT_printer", "interpretation is not a leaf"))
  1835 					val _ = (if element<0 then raise REFUTE ("IDT_printer", "invalid interpretation (no value assigned)") else ())
  1836 					(* int option -- only recursive IDTs have an associated depth *)
  1837 					val depth = assoc (typs, Type (s, Ts))
  1838 					val typs' = (case depth of None => typs | Some n => overwrite (typs, (Type (s, Ts), n-1)))
  1839 					(* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp -> Term.typ *)
  1840 					fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
  1841 						(* replace a 'DtTFree' variable by the associated type *)
  1842 						(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
  1843 					  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
  1844 						let
  1845 							val (s, ds, _) = (the o assoc) (descr, i)
  1846 						in
  1847 							Type (s, map (typ_of_dtyp descr typ_assoc) ds)
  1848 						end
  1849 					  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
  1850 						Type (s, map (typ_of_dtyp descr typ_assoc) ds)
  1851 					(* int list -> int *)
  1852 					fun sum xs = foldl op+ (0, xs)
  1853 					(* int list -> int *)
  1854 					fun product xs = foldl op* (1, xs)
  1855 					(* the size of an IDT is the sum (over its constructors) of the        *)
  1856 					(* product (over their arguments) of the size of the argument type     *)
  1857 					(* (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *)
  1858 					fun size_of_dtyp typs descr typ_assoc xs =
  1859 						sum (map (fn (_, ds) =>
  1860 							product (map (fn d =>
  1861 								let
  1862 									val T         = typ_of_dtyp descr typ_assoc d
  1863 									val (i, _, _) =
  1864 										(interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1865 										handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1866 					in
  1867 						size_of_type i
  1868 					end) ds)) xs)
  1869 					(* int -> DatatypeAux.dtyp list -> Term.term list *)
  1870 					fun make_args n [] =
  1871 						if n<>0 then
  1872 							raise REFUTE ("IDT_printer", "error computing the element: remainder is not 0")
  1873 						else
  1874 							[]
  1875 					  | make_args n (d::ds) =
  1876 						let
  1877 							val dT        = typ_of_dtyp descr typ_assoc d
  1878 							val (i, _, _) =
  1879 								(interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", dT))
  1880 								handle CANNOT_INTERPRET _ => raise CANNOT_INTERPRET t)
  1881 							val size      = size_of_type i
  1882 							val consts    = make_constants i  (* we only need the (n mod size)-th element of *)
  1883 								(* this list, so there might be a more efficient implementation that does not *)
  1884 								(* generate all constants                                                     *)
  1885 						in
  1886 							(print thy (typs', []) (Free ("dummy", dT)) (nth_elem (n mod size, consts)) assignment)::(make_args (n div size) ds)
  1887 						end
  1888 					(* int -> (string * DatatypeAux.dtyp list) list -> Term.term *)
  1889 					fun make_term _ [] =
  1890 						raise REFUTE ("IDT_printer", "invalid interpretation (value too large - not enough constructors)")
  1891 					  | make_term n (c::cs) =
  1892 						let
  1893 							val c_size = size_of_dtyp typs' descr typ_assoc [c]
  1894 						in
  1895 							if n<c_size then
  1896 								let
  1897 									val (cname, cargs) = c
  1898 									val c_term = Const (cname, (map (typ_of_dtyp descr typ_assoc) cargs) ---> Type (s, Ts))
  1899 								in
  1900 									foldl op$ (c_term, rev (make_args n (rev cargs)))
  1901 								end
  1902 							else
  1903 								make_term (n-c_size) cs
  1904 						end
  1905 				in
  1906 					Some (make_term element constrs)
  1907 				end
  1908 			| None =>  (* not an inductive datatype *)
  1909 				None)
  1910 		| _ =>  (* a (free or schematic) type variable *)
  1911 			None
  1912 	end;
  1913 
  1914 
  1915 (* ------------------------------------------------------------------------- *)
  1916 (* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
  1917 (* structure                                                                 *)
  1918 (* ------------------------------------------------------------------------- *)
  1919 
  1920 (* ------------------------------------------------------------------------- *)
  1921 (* Note: the interpreters and printers are used in reverse order; however,   *)
  1922 (*       an interpreter that can handle non-atomic terms ends up being       *)
  1923 (*       applied before the 'stlc_interpreter' breaks the term apart into    *)
  1924 (*       subterms that are then passed to other interpreters!                *)
  1925 (* ------------------------------------------------------------------------- *)
  1926 
  1927 	(* (theory -> theory) list *)
  1928 
  1929 	val setup =
  1930 		[RefuteData.init,
  1931 		 add_interpreter "stlc"            stlc_interpreter,
  1932 		 add_interpreter "Pure"            Pure_interpreter,
  1933 		 add_interpreter "HOLogic"         HOLogic_interpreter,
  1934 		 add_interpreter "set"             set_interpreter,
  1935 		 add_interpreter "IDT"             IDT_interpreter,
  1936 		 add_interpreter "Finite_Set.card" Finite_Set_card_interpreter,
  1937 		 add_printer "stlc" stlc_printer,
  1938 		 add_printer "set"  set_printer,
  1939 		 add_printer "IDT"  IDT_printer];
  1940 
  1941 end