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