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