src/HOL/Tools/refute.ML
author webertj
Thu Mar 11 00:15:24 2004 +0100 (2004-03-11)
changeset 14460 04e787a4f17a
parent 14456 cca28ec5f9a6
child 14488 863258b0cdca
permissions -rw-r--r--
SML/NJ compatibility fixes
     1 (*  Title:      HOL/Tools/refute.ML
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2003-2004
     5 
     6 Finite model generation for HOL formulae, using a SAT solver.
     7 *)
     8 
     9 (* ------------------------------------------------------------------------- *)
    10 (* TODO: Change parameter handling so that only supported parameters can be  *)
    11 (*       set, and specify defaults here, rather than in HOL/Main.thy.        *)
    12 (* ------------------------------------------------------------------------- *)
    13 
    14 (* ------------------------------------------------------------------------- *)
    15 (* Declares the 'REFUTE' signature as well as a structure 'Refute'.          *)
    16 (* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'.  *)
    17 (* ------------------------------------------------------------------------- *)
    18 
    19 signature REFUTE =
    20 sig
    21 
    22 	exception REFUTE of string * string
    23 
    24 (* ------------------------------------------------------------------------- *)
    25 (* Model/interpretation related code (translation HOL -> boolean formula)    *)
    26 (* ------------------------------------------------------------------------- *)
    27 
    28 	exception CANNOT_INTERPRET
    29 
    30 	type interpretation
    31 	type model
    32 	type arguments
    33 
    34 	val add_interpreter : string -> (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option) -> theory -> theory
    35 	val add_printer     : string -> (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option) -> theory -> theory
    36 
    37 	val interpret           : theory -> model -> arguments -> Term.term -> interpretation * model * arguments  (* exception CANNOT_INTERPRET *)
    38 	val is_satisfying_model : model -> interpretation -> bool -> PropLogic.prop_formula
    39 
    40 	val print       : theory -> model -> Term.term -> interpretation -> (int -> bool) -> string
    41 	val print_model : theory -> model -> (int -> bool) -> string
    42 
    43 (* ------------------------------------------------------------------------- *)
    44 (* Interface                                                                 *)
    45 (* ------------------------------------------------------------------------- *)
    46 
    47 	val set_default_param  : (string * string) -> theory -> theory
    48 	val get_default_param  : theory -> string -> string option
    49 	val get_default_params : theory -> (string * string) list
    50 	val actual_params      : theory -> (string * string) list -> (int * int * int * string)
    51 
    52 	val find_model : theory -> (int * int * int * string) -> Term.term -> bool -> unit
    53 
    54 	val satisfy_term   : theory -> (string * string) list -> Term.term -> unit  (* tries to find a model for a formula *)
    55 	val refute_term    : theory -> (string * string) list -> Term.term -> unit  (* tries to find a model that refutes a formula *)
    56 	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
    57 
    58 	val setup : (theory -> theory) list
    59 end;
    60 
    61 structure Refute : REFUTE =
    62 struct
    63 
    64 	open PropLogic;
    65 
    66 	(* We use 'REFUTE' only for internal error conditions that should    *)
    67 	(* never occur in the first place (i.e. errors caused by bugs in our *)
    68 	(* code).  Otherwise (e.g. to indicate invalid input data) we use    *)
    69 	(* 'error'.                                                          *)
    70 	exception REFUTE of string * string;  (* ("in function", "cause") *)
    71 
    72 (* ------------------------------------------------------------------------- *)
    73 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
    74 (* ------------------------------------------------------------------------- *)
    75 
    76 	exception CANNOT_INTERPRET;
    77 
    78 (* ------------------------------------------------------------------------- *)
    79 (* TREES                                                                     *)
    80 (* ------------------------------------------------------------------------- *)
    81 
    82 (* ------------------------------------------------------------------------- *)
    83 (* tree: implements an arbitrarily (but finitely) branching tree as a list   *)
    84 (*       of (lists of ...) elements                                          *)
    85 (* ------------------------------------------------------------------------- *)
    86 
    87 	datatype 'a tree =
    88 		  Leaf of 'a
    89 		| Node of ('a tree) list;
    90 
    91 	(* ('a -> 'b) -> 'a tree -> 'b tree *)
    92 
    93 	fun tree_map f tr =
    94 		case tr of
    95 		  Leaf x  => Leaf (f x)
    96 		| Node xs => Node (map (tree_map f) xs);
    97 
    98 	(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
    99 
   100 	fun tree_foldl f =
   101 	let
   102 		fun itl (e, Leaf x)  = f(e,x)
   103 		  | itl (e, Node xs) = foldl (tree_foldl f) (e,xs)
   104 	in
   105 		itl
   106 	end;
   107 
   108 	(* 'a tree * 'b tree -> ('a * 'b) tree *)
   109 
   110 	fun tree_pair (t1,t2) =
   111 		case t1 of
   112 		  Leaf x =>
   113 			(case t2 of
   114 				  Leaf y => Leaf (x,y)
   115 				| Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)"))
   116 		| Node xs =>
   117 			(case t2 of
   118 				  (* '~~' will raise an exception if the number of branches in both trees is different at the current node *)
   119 				  Node ys => Node (map tree_pair (xs ~~ ys))
   120 				| Leaf _  => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
   121 
   122 
   123 (* ------------------------------------------------------------------------- *)
   124 (* interpretation: a term's interpretation is given by a variable of type    *)
   125 (*                 'interpretation'                                          *)
   126 (* ------------------------------------------------------------------------- *)
   127 
   128 	type interpretation =
   129 		prop_formula list tree;
   130 
   131 (* ------------------------------------------------------------------------- *)
   132 (* model: a model specifies the size of types and the interpretation of      *)
   133 (*        terms                                                              *)
   134 (* ------------------------------------------------------------------------- *)
   135 
   136 	type model =
   137 		(Term.typ * int) list * (Term.term * interpretation) list;
   138 
   139 (* ------------------------------------------------------------------------- *)
   140 (* arguments: additional arguments required during interpretation of terms   *)
   141 (* ------------------------------------------------------------------------- *)
   142 	
   143 	type arguments =
   144 		{next_idx: int, bounds: interpretation list, wellformed: prop_formula};
   145 
   146 
   147 	structure RefuteDataArgs =
   148 	struct
   149 		val name = "HOL/refute";
   150 		type T =
   151 			{interpreters: (string * (theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option)) list,
   152 			 printers: (string * (theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option)) list,
   153 			 parameters: string Symtab.table};
   154 		val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
   155 		val copy = I;
   156 		val prep_ext = I;
   157 		fun merge
   158 			({interpreters = in1, printers = pr1, parameters = pa1},
   159 			 {interpreters = in2, printers = pr2, parameters = pa2}) =
   160 			{interpreters = rev (merge_alists (rev in1) (rev in2)),
   161 			 printers = rev (merge_alists (rev pr1) (rev pr2)),
   162 			 parameters = Symtab.merge (op=) (pa1, pa2)};
   163 		fun print sg {interpreters, printers, parameters} =
   164 			Pretty.writeln (Pretty.chunks
   165 				[Pretty.strs ("default parameters:" :: flat (map (fn (name,value) => [name, "=", value]) (Symtab.dest parameters))),
   166 				 Pretty.strs ("interpreters:" :: map fst interpreters),
   167 				 Pretty.strs ("printers:" :: map fst printers)]);
   168 	end;
   169 
   170 	structure RefuteData = TheoryDataFun(RefuteDataArgs);
   171 
   172 
   173 (* ------------------------------------------------------------------------- *)
   174 (* interpret: tries to interpret the term 't' using a suitable interpreter;  *)
   175 (*            returns the interpretation and a (possibly extended) model     *)
   176 (*            that keeps track of the interpretation of subterms             *)
   177 (* Note: exception 'CANNOT_INTERPRETE' is raised if the term cannot be       *)
   178 (*       interpreted by any interpreter                                      *)
   179 (* ------------------------------------------------------------------------- *)
   180 
   181 	(* theory -> model -> arguments -> Term.term -> interpretation * model * arguments *)
   182 
   183 	fun interpret thy model args t =
   184 		(case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of
   185 		  None =>
   186 			(std_output "\n"; warning ("Unable to interpret term:\n" ^ Sign.string_of_term (sign_of thy) t);
   187 			raise CANNOT_INTERPRET)
   188 		| Some x => x);
   189 
   190 (* ------------------------------------------------------------------------- *)
   191 (* print: tries to print the constant denoted by the term 't' using a        *)
   192 (*        suitable printer                                                   *)
   193 (* ------------------------------------------------------------------------- *)
   194 
   195 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string *)
   196 
   197 	fun print thy model t intr assignment =
   198 		(case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of
   199 		  None => "<<no printer available>>"
   200 		| Some s => s);
   201 
   202 (* ------------------------------------------------------------------------- *)
   203 (* is_satisfying_model: returns a propositional formula that is true iff the *)
   204 (*      given interpretation denotes 'satisfy', and the model meets certain  *)
   205 (*      well-formedness properties                                           *)
   206 (* ------------------------------------------------------------------------- *)
   207 
   208 	(* model -> interpretation -> bool -> PropLogic.prop_formula *)
   209 
   210 	fun is_satisfying_model model intr satisfy =
   211 	let
   212 		(* prop_formula list -> prop_formula *)
   213 		fun allfalse []      = True
   214 		  | allfalse (x::xs) = SAnd (SNot x, allfalse xs)
   215 		(* prop_formula list -> prop_formula *)
   216 		fun exactly1true []      = False
   217 		  | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
   218 	(* ------------------------------------------------------------------------- *)
   219 	(* restrict_to_single_element: returns a propositional formula that is true  *)
   220 	(*      iff the interpretation denotes a single element of its corresponding *)
   221 	(*      type, i.e. iff at each leaf, one and only one formula is true        *)
   222 	(* ------------------------------------------------------------------------- *)
   223 		(* interpretation -> prop_formula *)
   224 		fun restrict_to_single_element (Leaf [BoolVar i, Not (BoolVar j)]) =
   225 			if (i=j) then
   226 				True  (* optimization for boolean variables *)
   227 			else
   228 				raise REFUTE ("is_satisfying_model", "boolean variables in leaf have different indices")
   229 		  | restrict_to_single_element (Leaf xs) =
   230 			exactly1true xs
   231 		  | restrict_to_single_element (Node trees) =
   232 			PropLogic.all (map restrict_to_single_element trees)
   233 	in
   234 		(* a term of type 'bool' is represented as a 2-element leaf, where  *)
   235 		(* the term is true iff the leaf's first element is true, and false *)
   236 		(* iff the leaf's second element is true                            *)
   237 		case intr of
   238 		  Leaf [fmT,fmF] =>
   239 			(* well-formedness properties and formula 'fmT'/'fmF' *)
   240 			SAnd (PropLogic.all (map (restrict_to_single_element o snd) (snd model)), if satisfy then fmT else fmF)
   241 		| _ =>
   242 			raise REFUTE ("is_satisfying_model", "interpretation does not denote a boolean value")
   243 	end;
   244 
   245 (* ------------------------------------------------------------------------- *)
   246 (* print_model: turns the model into a string, using a fixed interpretation  *)
   247 (*              (given by an assignment for boolean variables) and suitable  *)
   248 (*              printers                                                     *)
   249 (* ------------------------------------------------------------------------- *)
   250 
   251 	fun print_model thy model assignment =
   252 	let
   253 		val (typs, terms) = model
   254 	in
   255 		(if null typs then
   256 			"empty universe (no type variables in term)"
   257 		else
   258 			"Size of types: " ^ commas (map (fn (T,i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs))
   259 		^ "\n"
   260 		^ (if null terms then
   261 			"empty interpretation (no free variables in term)"
   262 		  else
   263 			space_implode "\n" (map
   264 				(fn (t,intr) =>
   265 					Sign.string_of_term (sign_of thy) t ^ ": " ^ print thy model t intr assignment)
   266 				terms)
   267 		  )
   268 		^ "\n"
   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) -> string 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 tuple that can be passed to 'find_model'.                  *)
   338 (*                                                                           *)
   339 (* The following parameters are supported (and required!):                   *)
   340 (*                                                                           *)
   341 (* Name          Type    Description                                         *)
   342 (*                                                                           *)
   343 (* "minsize"     int     Only search for models with size at least           *)
   344 (*                       'minsize'.                                          *)
   345 (* "maxsize"     int     If >0, only search for models with size at most     *)
   346 (*                       'maxsize'.                                          *)
   347 (* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
   348 (*                       when transforming the term into a propositional     *)
   349 (*                       formula.                                            *)
   350 (* "satsolver"   string  SAT solver to be used.                              *)
   351 (* ------------------------------------------------------------------------- *)
   352 
   353 	(* theory -> (string * string) list -> (int * int * int * string) *)
   354 
   355 	fun actual_params thy params =
   356 	let
   357 		(* (string * string) list * string -> int *)
   358 		fun read_int (parms, name) =
   359 			case assoc_string (parms, name) of
   360 			  Some s => (case Int.fromString s of
   361 				  SOME i => i
   362 				| NONE   => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value"))
   363 			| None   => error ("parameter " ^ quote name ^ " must be assigned a value")
   364 		(* (string * string) list * string -> string *)
   365 		fun read_string (parms, name) =
   366 			case assoc_string (parms, name) of
   367 			  Some s => s
   368 			| None   => error ("parameter " ^ quote name ^ " must be assigned a value")
   369 		(* (string * string) list *)
   370 		val allparams = params @ (get_default_params thy)  (* 'params' first, defaults last (to override) *)
   371 		(* int *)
   372 		val minsize   = read_int (allparams, "minsize")
   373 		val maxsize   = read_int (allparams, "maxsize")
   374 		val maxvars   = read_int (allparams, "maxvars")
   375 		(* string *)
   376 		val satsolver = read_string (allparams, "satsolver")
   377 	in
   378 		(minsize, maxsize, maxvars, satsolver)
   379 	end;
   380 
   381 (* ------------------------------------------------------------------------- *)
   382 (* find_model: repeatedly calls 'invoke_propgen' with appropriate            *)
   383 (*             parameters, applies the SAT solver, and (in case a model is   *)
   384 (*             found) displays the model to the user                         *)
   385 (* thy      : the current theory                                             *)
   386 (* minsize  : the minimal size of the model                                  *)
   387 (* maxsize  : the maximal size of the model                                  *)
   388 (* maxvars  : the maximal number of boolean variables to be used             *)
   389 (* satsolver: the name of the SAT solver to be used                          *)
   390 (* satisfy  : if 'True', search for a model that makes 't' true; otherwise   *)
   391 (*            search for a model that makes 't' false                        *)
   392 (* ------------------------------------------------------------------------- *)
   393 
   394 	(* theory ->  (int * int * int * string) -> Term.term -> bool -> unit *)
   395 
   396 	fun find_model thy (minsize, maxsize, maxvars, satsolver) t satisfy =
   397 	let
   398 		(* Term.typ list *)
   399 		val tvars  = map (fn (i,s) => TVar(i,s)) (term_tvars t)
   400 		val tfrees = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
   401 		(* int -> unit *)
   402 		fun find_model_loop size =
   403 			(* 'maxsize=0' means "search for arbitrary large models" *)
   404 			if size>maxsize andalso maxsize<>0 then
   405 				writeln ("Search terminated: maxsize=" ^ string_of_int maxsize ^ " exceeded.")
   406 			else
   407 			let
   408 				(* ------------------------------------------------------------------------- *)
   409 				(* make_universes: given a list 'xs' of "types" and a universe size 'size',  *)
   410 				(*      this function returns all possible partitions of the universe into   *)
   411 				(*      the "types" in 'xs' such that no "type" is empty.  If 'size' is less *)
   412 				(*      than 'length xs', the returned list of partitions is empty.          *)
   413 				(*      Otherwise, if the list 'xs' is empty, then the returned list of      *)
   414 				(*      partitions contains only the empty list, regardless of 'size'.       *)
   415 				(* ------------------------------------------------------------------------- *)
   416 				(* 'a list -> int -> ('a * int) list list *)
   417 				fun make_universes xs size =
   418 				let
   419 					(* 'a list -> int -> int -> ('a * int) list list *)
   420 					fun make_partitions_loop (x::xs) 0 total =
   421 						map (fn us => ((x,0)::us)) (make_partitions xs total)
   422 					  | make_partitions_loop (x::xs) first total =
   423 						(map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
   424 					  | make_partitions_loop _ _ _ =
   425 						raise REFUTE ("find_model", "empty list (in make_partitions_loop)")
   426 					and
   427 					(* 'a list -> int -> ('a * int) list list *)
   428 					make_partitions [x] size =
   429 						(* we must use all remaining elements on the type 'x', so there is only one partition *)
   430 						[[(x,size)]]
   431 					  | make_partitions (x::xs) 0 =
   432 						(* there are no elements left in the universe, so there is only one partition *)
   433 						[map (fn t => (t,0)) (x::xs)]
   434 					  | make_partitions (x::xs) size =
   435 						(* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
   436 						make_partitions_loop (x::xs) size size
   437 					  | make_partitions _ _ =
   438 						raise REFUTE ("find_model", "empty list (in make_partitions)")
   439 					val len = length xs
   440 				in
   441 					if size<len then
   442 						(* the universe isn't big enough to make every type non-empty *)
   443 						[]
   444 					else if xs=[] then
   445 						(* no types: return one universe, regardless of the size *)
   446 						[[]]
   447 					else
   448 						(* partition into possibly empty types, then add 1 element to each type *)
   449 						map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
   450 				end
   451 				(* ('a * int) list -> bool *)
   452 				fun find_interpretation xs =
   453 				let
   454 					val init_model          = (xs, [])
   455 					val init_args           = {next_idx = 1, bounds = [], wellformed = True}
   456 					val (intr, model, args) = interpret thy init_model init_args t
   457 					val fm                  = SAnd (#wellformed args, is_satisfying_model model intr satisfy)
   458 					val usedvars            = maxidx fm
   459 				in
   460 					(* 'maxvars=0' means "use as many variables as necessary" *)
   461 					if usedvars>maxvars andalso maxvars<>0 then
   462 						(writeln ("\nSearch terminated: " ^ string_of_int usedvars ^ " boolean variables used (only " ^ string_of_int maxvars ^ " allowed).");
   463 						true)
   464 					else
   465 					(
   466 						std_output " invoking SAT solver...";
   467 						case SatSolver.invoke_solver satsolver fm of
   468 						  None =>
   469 							(std_output " no model found.\n";
   470 							false)
   471 						| Some assignment =>
   472 							(writeln ("\nModel found:\n" ^ print_model thy model assignment);
   473 							true)
   474 					)
   475 				end handle CANNOT_INTERPRET => true
   476 					(* TODO: change this to false once the ability to interpret terms depends on the universe *)
   477 			in
   478 				case make_universes (tvars@tfrees) size of
   479 				  [] =>
   480 					(writeln ("Searching for a model of size " ^ string_of_int size ^ ": cannot make every type non-empty (model is too small).");
   481 					find_model_loop (size+1))
   482 				| [[]] =>
   483 					(std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term...");
   484 					if find_interpretation [] then
   485 						()
   486 					else
   487 						writeln ("Search terminated: no type variables in term."))
   488 				| us =>
   489 					let
   490 						fun loop []      =
   491 							find_model_loop (size+1)
   492 						  | loop (u::us) =
   493 							(std_output ("Searching for a model of size " ^ string_of_int size ^ ", translating term...");
   494 							if find_interpretation u then () else loop us)
   495 					in
   496 						loop us
   497 					end
   498 			end
   499 	in
   500 		writeln ("Trying to find a model that "
   501 			^ (if satisfy then "satisfies" else "refutes")
   502 			^ ": " ^ (Sign.string_of_term (sign_of thy) t));
   503 		if minsize<1 then
   504 			writeln "\"minsize\" is less than 1; starting search with size 1."
   505 		else ();
   506 		find_model_loop (Int.max (minsize,1))
   507 	end;
   508 
   509 
   510 (* ------------------------------------------------------------------------- *)
   511 (* INTERFACE, PART 2: FINDING A MODEL                                        *)
   512 (* ------------------------------------------------------------------------- *)
   513 
   514 (* ------------------------------------------------------------------------- *)
   515 (* satisfy_term: calls 'find_model' to find a model that satisfies 't'       *)
   516 (* params      : list of '(name, value)' pairs used to override default      *)
   517 (*               parameters                                                  *)
   518 (* ------------------------------------------------------------------------- *)
   519 
   520 	(* theory -> (string * string) list -> Term.term -> unit *)
   521 
   522 	fun satisfy_term thy params t =
   523 		find_model thy (actual_params thy params) t true;
   524 
   525 (* ------------------------------------------------------------------------- *)
   526 (* refute_term: calls 'find_model' to find a model that refutes 't'          *)
   527 (* params     : list of '(name, value)' pairs used to override default       *)
   528 (*              parameters                                                   *)
   529 (* ------------------------------------------------------------------------- *)
   530 
   531 	(* theory -> (string * string) list -> Term.term -> unit *)
   532 
   533 	fun refute_term thy params t =
   534 	let
   535 		(* disallow schematic type variables, since we cannot properly negate terms containing them *)
   536 		val _ = assert (null (term_tvars t)) "Term to be refuted contains schematic type variables"
   537 		(* existential closure over schematic variables *)
   538 		(* (Term.indexname * Term.typ) list *)
   539 		val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   540 		(* Term.term *)
   541 		val ex_closure = foldl
   542 			(fn (t', ((x,i),T)) => (HOLogic.exists_const T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
   543 			(t, vars)
   544 		(* If 't' is of type 'propT' (rather than 'boolT'), applying  *)
   545 		(* 'HOLogic.exists_const' is not type-correct.  However, this *)
   546 		(* isn't really a problem as long as 'find_model' still       *)
   547 		(* interprets the resulting term correctly, without checking  *)
   548 		(* its type.                                                  *)
   549 	in
   550 		find_model thy (actual_params thy params) ex_closure false
   551 	end;
   552 
   553 (* ------------------------------------------------------------------------- *)
   554 (* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
   555 (* params        : list of '(name, value)' pairs used to override default    *)
   556 (*                 parameters                                                *)
   557 (* subgoal       : 0-based index specifying the subgoal number               *)
   558 (* ------------------------------------------------------------------------- *)
   559 
   560 	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
   561 
   562 	fun refute_subgoal thy params thm subgoal =
   563 		refute_term thy params (nth_elem (subgoal, prems_of thm));
   564 
   565 
   566 (* ------------------------------------------------------------------------- *)
   567 (* INTERPRETERS                                                              *)
   568 (* ------------------------------------------------------------------------- *)
   569 
   570 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   571 
   572 	fun var_typevar_interpreter thy model args t =
   573 	let
   574 		fun is_var (Free _) = true
   575 		  | is_var (Var _)  = true
   576 		  | is_var _        = false
   577 		fun typeof (Free (_,T)) = T
   578 		  | typeof (Var (_,T))  = T
   579 		  | typeof _            = raise REFUTE ("var_typevar_interpreter", "term is not a variable")
   580 		fun is_typevar (TFree _) = true
   581 		  | is_typevar (TVar _)  = true
   582 		  | is_typevar _         = false
   583 		val (sizes, intrs) = model
   584 	in
   585 		if is_var t andalso is_typevar (typeof t) then
   586 			(case assoc (intrs, t) of
   587 			  Some intr => Some (intr, model, args)
   588 			| None      =>
   589 				let
   590 					val size = (the o assoc) (sizes, typeof t)  (* the model MUST specify a size for type variables *)
   591 					val idx  = #next_idx args
   592 					val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1))))
   593 					val next = (if size=2 then idx+1 else idx+size)
   594 				in
   595 					(* extend the model, increase 'next_idx' *)
   596 					Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args})
   597 				end)
   598 		else
   599 			None
   600 	end;
   601 
   602 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   603 
   604 	fun var_funtype_interpreter thy model args t =
   605 	let
   606 		fun is_var (Free _) = true
   607 		  | is_var (Var _)  = true
   608 		  | is_var _        = false
   609 		fun typeof (Free (_,T)) = T
   610 		  | typeof (Var (_,T))  = T
   611 		  | typeof _            = raise REFUTE ("var_funtype_interpreter", "term is not a variable")
   612 		fun stringof (Free (x,_))     = x
   613 		  | stringof (Var ((x,_), _)) = x
   614 		  | stringof _                = raise REFUTE ("var_funtype_interpreter", "term is not a variable")
   615 		fun is_funtype (Type ("fun", [_,_])) = true
   616 		  | is_funtype _                     = false
   617 		val (sizes, intrs) = model
   618 	in
   619 		if is_var t andalso is_funtype (typeof t) then
   620 			(case assoc (intrs, t) of
   621 			  Some intr => Some (intr, model, args)
   622 			| None      =>
   623 				let
   624 					val T1 = domain_type (typeof t)
   625 					val T2 = range_type (typeof t)
   626 					(* we create 'size_of_interpretation (interpret (... T1))' different copies *)
   627 					(* of the tree for 'T2', which are then combined into a single new tree     *)
   628 					val (i1, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (stringof t, T1))
   629 					(* power(a,b) computes a^b, for a>=0, b>=0 *)
   630 					(* int * int -> int *)
   631 					fun power (a,0) = 1
   632 					  | power (a,1) = a
   633 					  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
   634 					fun size_of_interpretation (Leaf xs) = length xs
   635 					  | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
   636 					val size = size_of_interpretation i1
   637 					(* make fresh copies, with different variable indices *)
   638 					(* int -> int -> (int * interpretation list *)
   639 					fun make_copies idx 0 =
   640 						(idx, [])
   641 					  | make_copies idx n =
   642 						let
   643 							val (copy, _, args) = interpret thy (sizes, []) {next_idx = idx, bounds = [], wellformed=True} (Free (stringof t, T2))
   644 							val (next, copies)  = make_copies (#next_idx args) (n-1)
   645 						in
   646 							(next, copy :: copies)
   647 						end
   648 					val (idx, copies) = make_copies (#next_idx args) (size_of_interpretation i1)
   649 					(* combine copies into a single tree *)
   650 					val intr = Node copies
   651 				in
   652 					(* extend the model, increase 'next_idx' *)
   653 					Some (intr, (sizes, (t, intr)::intrs), {next_idx = idx, bounds = #bounds args, wellformed = #wellformed args})
   654 				end)
   655 		else
   656 			None
   657 	end;
   658 
   659 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   660 
   661 	fun var_settype_interpreter thy model args t =
   662 		let
   663 			val (sizes, intrs) = model
   664 		in
   665 			case t of
   666 			  Free (x, Type ("set", [T])) =>
   667 				(case assoc (intrs, t) of
   668 				  Some intr => Some (intr, model, args)
   669 				| None      =>
   670 					let
   671 						val (intr, _, args') = interpret thy model args (Free (x, Type ("fun", [T, Type ("bool", [])])))
   672 					in
   673 						Some (intr, (sizes, (t, intr)::intrs), args')
   674 					end)
   675 			| Var ((x,i), Type ("set", [T])) =>
   676 				(case assoc (intrs, t) of
   677 				  Some intr => Some (intr, model, args)
   678 				| None      =>
   679 					let
   680 						val (intr, _, args') = interpret thy model args (Var ((x,i), Type ("fun", [T, Type ("bool", [])])))
   681 					in
   682 						Some (intr, (sizes, (t, intr)::intrs), args')
   683 					end)
   684 			| _ => None
   685 		end;
   686 
   687 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   688 
   689 	fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds (args:arguments)), model, args)
   690 	  | boundvar_interpreter thy model args _         = None;
   691 
   692 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   693 
   694 	fun abstraction_interpreter thy model args (Abs (x, T, t)) =
   695 		let
   696 			val (sizes, intrs) = model
   697 			(* create all constants of type T *)
   698 			val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free (x, T))
   699 			(* returns a list with all unit vectors of length n *)
   700 			(* int -> interpretation list *)
   701 			fun unit_vectors n =
   702 			let
   703 				(* returns the k-th unit vector of length n *)
   704 				(* int * int -> interpretation *)
   705 				fun unit_vector (k,n) =
   706 					Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
   707 				(* int -> interpretation list -> interpretation list *)
   708 				fun unit_vectors_acc k vs =
   709 					if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
   710 			in
   711 				unit_vectors_acc 1 []
   712 			end
   713 			(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
   714 			(* 'a -> 'a list list -> 'a list list *)
   715 			fun cons_list x xss =
   716 				map (fn xs => x::xs) xss
   717 			(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
   718 			(* int -> 'a list -> 'a list list *)
   719 			fun pick_all 1 xs =
   720 				map (fn x => [x]) xs
   721 			  | pick_all n xs =
   722 				let val rec_pick = pick_all (n-1) xs in
   723 					foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   724 				end
   725 			(* interpretation -> interpretation list *)
   726 			fun make_constants (Leaf xs) =
   727 				unit_vectors (length xs)
   728 			  | make_constants (Node xs) =
   729 				map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
   730 			(* interpret the body 't' separately for each constant *)
   731 			val ((model', args'), bodies) = foldl_map
   732 				(fn ((m,a), c) =>
   733 					let
   734 						(* add 'c' to 'bounds' *)
   735 						val (i',m',a') = interpret thy m {next_idx = #next_idx a, bounds = c::(#bounds a), wellformed = #wellformed a} t
   736 					in
   737 						(* keep the new model m' and 'next_idx', but use old 'bounds' *)
   738 						((m',{next_idx = #next_idx a', bounds = #bounds a, wellformed = #wellformed a'}), i')
   739 					end)
   740 				((model,args), make_constants i)
   741 		in
   742 			Some (Node bodies, model', args')
   743 		end
   744 	  | abstraction_interpreter thy model args _               = None;
   745 
   746 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   747 
   748 	fun apply_interpreter thy model args (t1 $ t2) =
   749 		let
   750 			(* auxiliary functions *)
   751 			(* interpretation * interpretation -> interpretation *)
   752 			fun interpretation_disjunction (tr1,tr2) =
   753 				tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
   754 			(* prop_formula * interpretation -> interpretation *)
   755 			fun prop_formula_times_interpretation (fm,tr) =
   756 				tree_map (map (fn x => SAnd (fm,x))) tr
   757 			(* prop_formula list * interpretation list -> interpretation *)
   758 			fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
   759 				prop_formula_times_interpretation (fm,tr)
   760 			  | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
   761 				interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees))
   762 			  | prop_formula_list_dot_product_interpretation_list (_,_) =
   763 				raise REFUTE ("apply_interpreter", "empty list (in dot product)")
   764 			(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
   765 			(* 'a -> 'a list list -> 'a list list *)
   766 			fun cons_list x xss =
   767 				map (fn xs => x::xs) xss
   768 			(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
   769 			(* 'a list list -> 'a list list *)
   770 			fun pick_all [xs] =
   771 				map (fn x => [x]) xs
   772 			  | pick_all (xs::xss) =
   773 				let val rec_pick = pick_all xss in
   774 					foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   775 				end
   776 			  | pick_all _ =
   777 				raise REFUTE ("apply_interpreter", "empty list (in pick_all)")
   778 			(* interpretation -> prop_formula list *)
   779 			fun interpretation_to_prop_formula_list (Leaf xs) =
   780 				xs
   781 			  | interpretation_to_prop_formula_list (Node trees) =
   782 				map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees))
   783 			(* interpretation * interpretation -> interpretation *)
   784 			fun interpretation_apply (tr1,tr2) =
   785 				(case tr1 of
   786 				  Leaf _ =>
   787 					raise REFUTE ("apply_interpreter", "first interpretation is a leaf")
   788 				| Node xs =>
   789 					prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs))
   790 			(* interpret 't1' and 't2' *)
   791 			val (intr1, model1, args1) = interpret thy model args t1
   792 			val (intr2, model2, args2) = interpret thy model1 args1 t2
   793 		in
   794 			Some (interpretation_apply (intr1,intr2), model2, args2)
   795 		end
   796 	  | apply_interpreter thy model args _         = None;
   797 
   798 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   799 
   800 	fun const_unfold_interpreter thy model args t =
   801 		(* ------------------------------------------------------------------------- *)
   802 		(* We unfold constants for which a defining equation is given as an axiom.   *)
   803 		(* A polymorphic axiom's type variables are instantiated.  Eta-expansion is  *)
   804 		(* performed only if necessary; arguments in the axiom that are present as   *)
   805 		(* actual arguments in 't' are simply substituted.  If more actual than      *)
   806 		(* formal arguments are present, the constant is *not* unfolded, so that     *)
   807 		(* other interpreters (that may just not have looked into the term far       *)
   808 		(* enough yet) may be applied first (after 'apply_interpreter' gets rid of   *)
   809 		(* one argument).                                                            *)
   810 		(* ------------------------------------------------------------------------- *)
   811 		let
   812 			val (head, actuals) = strip_comb t
   813 			val actuals_count   = length actuals
   814 		in
   815 			case head of
   816 			  Const (s,T) =>
   817 				let
   818 					(* (string * Term.term) list *)
   819 					val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
   820 					(* Term.term * Term.term list * Term.term list -> Term.term *)
   821 					(* term, formal arguments, actual arguments *)
   822 					fun normalize (t, [],    [])    = t
   823 					  | normalize (t, [],    y::ys) = raise REFUTE ("const_unfold_interpreter", "more actual than formal parameters")
   824 					  | normalize (t, x::xs, [])    = normalize (lambda x t, xs, [])                (* eta-expansion *)
   825 					  | normalize (t, x::xs, y::ys) = normalize (betapply (lambda x t, y), xs, ys)  (* substitution *)
   826 					(* string -> Term.typ -> (string * Term.term) list -> Term.term option *)
   827 					fun get_defn s T [] =
   828 						None
   829 					  | get_defn s T ((_,ax)::axms) =
   830 						(let
   831 							val (lhs, rhs)   = Logic.dest_equals ax  (* equations only *)
   832 							val (c, formals) = strip_comb lhs
   833 							val (s', T')     = dest_Const c
   834 						in
   835 							if (s=s') andalso (actuals_count <= length formals) then
   836 								let
   837 									val varT'      = Type.varifyT T'  (* for polymorphic definitions *)
   838 									val typeSubs   = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (varT', T))
   839 									val varRhs     = map_term_types Type.varifyT rhs
   840 									val varFormals = map (map_term_types Type.varifyT) formals
   841 									val rhs'       = normalize (varRhs, varFormals, actuals)
   842 									val unvarRhs   = map_term_types
   843 										(map_type_tvar
   844 											(fn (v,_) =>
   845 												case Vartab.lookup (typeSubs, v) of
   846 												  None =>
   847 													raise REFUTE ("const_unfold_interpreter", "schematic type variable " ^ (fst v) ^ "not instantiated (in definition of " ^ quote s ^ ")")
   848 												| Some typ =>
   849 													typ))
   850 										rhs'
   851 								in
   852 									Some unvarRhs
   853 								end
   854 							else
   855 								get_defn s T axms
   856 						end
   857 						handle TERM _          => get_defn s T axms
   858 						     | Type.TYPE_MATCH => get_defn s T axms)
   859 				in
   860 					case get_defn s T axioms of
   861 					  Some t' => Some (interpret thy model args t')
   862 					| None    => None
   863 				end
   864 			| _ => None
   865 		end;
   866 
   867 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   868 
   869 	fun Pure_interpreter thy model args t =
   870 		let
   871 			fun toTrue (Leaf [fm,_]) = fm
   872 			  | toTrue _             = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value")
   873 			fun toFalse (Leaf [_,fm]) = fm
   874 			  | toFalse _             = raise REFUTE ("Pure_interpreter", "interpretation does not denote a boolean value")
   875 		in
   876 			case t of
   877 			  (*Const ("Goal", _) $ t1 =>
   878 				Some (interpret thy model args t1) |*)
   879 			  Const ("all", _) $ t1 =>
   880 				let
   881 					val (i,m,a) = (interpret thy model args t1)
   882 				in
   883 					case i of
   884 					  Node xs =>
   885 						let
   886 							val fmTrue  = PropLogic.all (map toTrue xs)
   887 							val fmFalse = PropLogic.exists (map toFalse xs)
   888 						in
   889 							Some (Leaf [fmTrue, fmFalse], m, a)
   890 						end
   891 					| _ =>
   892 						raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function")
   893 				end
   894 			| Const ("==", _) $ t1 $ t2 =>
   895 				let
   896 					val (i1,m1,a1) = interpret thy model args t1
   897 					val (i2,m2,a2) = interpret thy m1 a1 t2
   898 					(* interpretation * interpretation -> prop_formula *)
   899 					fun interpret_equal (tr1,tr2) =
   900 						(case tr1 of
   901 						  Leaf x =>
   902 							(case tr2 of
   903 							  Leaf y => PropLogic.dot_product (x,y)
   904 							| _      => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher"))
   905 						| Node xs =>
   906 							(case tr2 of
   907 							  Leaf _  => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher")
   908 							(* extensionality: two functions are equal iff they are equal for every element *)
   909 							| Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
   910 					(* interpretation * interpretation -> prop_formula *)
   911 					fun interpret_unequal (tr1,tr2) =
   912 						(case tr1 of
   913 						  Leaf x =>
   914 							(case tr2 of
   915 							  Leaf y =>
   916 								let
   917 									fun unequal [] ([],_) =
   918 										False
   919 									  | unequal (x::xs) (y::ys1, ys2) =
   920 										SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2))
   921 									  | unequal _ _ =
   922 										raise REFUTE ("Pure_interpreter", "\"==\": leafs have different width")
   923 								in
   924 									unequal x (y,[])
   925 								end
   926 							| _      => raise REFUTE ("Pure_interpreter", "\"==\": second tree is higher"))
   927 						| Node xs =>
   928 							(case tr2 of
   929 							  Leaf _  => raise REFUTE ("Pure_interpreter", "\"==\": first tree is higher")
   930 							(* extensionality: two functions are unequal iff there exist unequal elements *)
   931 							| Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys))))
   932 					val fmTrue  = interpret_equal (i1,i2)
   933 					val fmFalse = interpret_unequal (i1,i2)
   934 				in
   935 					Some (Leaf [fmTrue, fmFalse], m2, a2)
   936 				end
   937 			| Const ("==>", _) $ t1 $ t2 =>
   938 				let
   939 					val (i1,m1,a1) = interpret thy model args t1
   940 					val (i2,m2,a2) = interpret thy m1 a1 t2
   941 					val fmTrue     = SOr (toFalse i1, toTrue i2)
   942 					val fmFalse    = SAnd (toTrue i1, toFalse i2)
   943 				in
   944 					Some (Leaf [fmTrue, fmFalse], m2, a2)
   945 				end
   946 			| _ => None
   947 		end;
   948 
   949 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   950 
   951 	fun HOLogic_interpreter thy model args t =
   952 	(* ------------------------------------------------------------------------- *)
   953 	(* Providing interpretations directly is more efficient than unfolding the   *)
   954 	(* logical constants; however, we need versions for constants with arguments *)
   955 	(* (to avoid unfolding) as well as versions for constants without arguments  *)
   956 	(* (since in HOL, logical constants can themselves be arguments)             *)
   957 	(* ------------------------------------------------------------------------- *)
   958 	let
   959 		fun eta_expand t i =
   960 			let
   961 				val Ts = binder_types (fastype_of t)
   962 			in
   963 				foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
   964 					(take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
   965 			end
   966 		val TT = Leaf [True, False]
   967 		val FF = Leaf [False, True]
   968 		fun toTrue (Leaf [fm,_]) = fm
   969 		  | toTrue _             = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value")
   970 		fun toFalse (Leaf [_,fm]) = fm
   971 		  | toFalse _             = raise REFUTE ("HOLogic_interpreter", "interpretation does not denote a boolean value")
   972 	in
   973 		case t of
   974 		  Const ("Trueprop", _) $ t1 =>
   975 			Some (interpret thy model args t1)
   976 		| Const ("Trueprop", _) =>
   977 			Some (Node [TT, FF], model, args)
   978 		| Const ("Not", _) $ t1 =>
   979 			apply_interpreter thy model args t
   980 		| Const ("Not", _) =>
   981 			Some (Node [FF, TT], model, args)
   982 		| Const ("True", _) =>
   983 			Some (TT, model, args)
   984 		| Const ("False", _) =>
   985 			Some (FF, model, args)
   986 		| Const ("arbitrary", T) =>
   987 			(* treat 'arbitrary' just like a free variable of the same type *)
   988 			(case assoc (snd model, t) of
   989 			  Some intr =>
   990 				Some (intr, model, args)
   991 			| None =>
   992 				let
   993 					val (sizes, intrs) = model
   994 					val (intr, _, a)   = interpret thy (sizes, []) args (Free ("<arbitrary>", T))
   995 				in
   996 					Some (intr, (sizes, (t,intr)::intrs), a)
   997 				end)
   998 		| Const ("The", _) $ t1 =>
   999 			apply_interpreter thy model args t
  1000 		| Const ("The", T as Type ("fun", [_, T'])) =>
  1001 			(* treat 'The' like a free variable, but with a fixed interpretation for boolean *)
  1002 			(* functions that map exactly one constant of type T' to True                    *)
  1003 			(case assoc (snd model, t) of
  1004 				Some intr =>
  1005 					Some (intr, model, args)
  1006 			| None =>
  1007 				let
  1008 					val (sizes, intrs) = model
  1009 					val (intr, _, a)   = interpret thy (sizes, []) args (Free ("<The>", T))
  1010 					(* create all constants of type T' => bool, ... *)
  1011 					val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<The>", Type ("fun", [T', Type ("bool",[])])))
  1012 					(* ... and all constants of type T' *)
  1013 					val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<The>", T'))
  1014 					(* returns a list with all unit vectors of length n *)
  1015 					(* int -> interpretation list *)
  1016 					fun unit_vectors n =
  1017 					let
  1018 						(* returns the k-th unit vector of length n *)
  1019 						(* int * int -> interpretation *)
  1020 						fun unit_vector (k,n) =
  1021 							Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1022 						(* int -> interpretation list -> interpretation list *)
  1023 						fun unit_vectors_acc k vs =
  1024 							if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1025 					in
  1026 						unit_vectors_acc 1 []
  1027 					end
  1028 					(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1029 					(* 'a -> 'a list list -> 'a list list *)
  1030 					fun cons_list x xss =
  1031 						map (fn xs => x::xs) xss
  1032 					(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1033 					(* int -> 'a list -> 'a list list *)
  1034 					fun pick_all 1 xs =
  1035 						map (fn x => [x]) xs
  1036 					  | pick_all n xs =
  1037 						let val rec_pick = pick_all (n-1) xs in
  1038 							foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1039 						end
  1040 					(* interpretation -> interpretation list *)
  1041 					fun make_constants (Leaf xs) =
  1042 						unit_vectors (length xs)
  1043 					  | make_constants (Node xs) =
  1044 						map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1045 					val constantsFun = make_constants intrFun
  1046 					val constantsT'  = make_constants intrT'
  1047 					(* interpretation -> interpretation list -> interpretation option *)
  1048 					fun the_val (Node xs) cs =
  1049 						let
  1050 							val TrueCount = foldl (fn (n,x) => if toTrue x = True then n+1 else n) (0,xs)
  1051 							fun findThe (x::xs) (c::cs) =
  1052 								if toTrue x = True then
  1053 									c
  1054 								else
  1055 									findThe xs cs
  1056 							  | findThe _ _ =
  1057 								raise REFUTE ("HOLogic_interpreter", "\"The\": not found")
  1058 						in
  1059 							if TrueCount=1 then
  1060 								Some (findThe xs cs)
  1061 							else
  1062 								None
  1063 						end
  1064 					  | the_val _ _ =
  1065 						raise REFUTE ("HOLogic_interpreter", "\"The\": function interpreted as a leaf")
  1066 				in
  1067 					case intr of
  1068 					  Node xs =>
  1069 						let
  1070 							(* replace interpretation 'x' by the interpretation determined by 'f' *)
  1071 							val intrThe = Node (map (fn (x,f) => if_none (the_val f constantsT') x) (xs ~~ constantsFun))
  1072 						in
  1073 							Some (intrThe, (sizes, (t,intrThe)::intrs), a)
  1074 						end
  1075 					| _ =>
  1076 						raise REFUTE ("HOLogic_interpreter", "\"The\": interpretation is a leaf")
  1077 				end)
  1078 		| Const ("Hilbert_Choice.Eps", _) $ t1 =>
  1079 			apply_interpreter thy model args t
  1080 		| Const ("Hilbert_Choice.Eps", T as Type ("fun", [_, T'])) =>
  1081 			(* treat 'The' like a free variable, but with a fixed interpretation for boolean *)
  1082 			(* functions that map exactly one constant of type T' to True                    *)
  1083 			(case assoc (snd model, t) of
  1084 				Some intr =>
  1085 					Some (intr, model, args)
  1086 			| None =>
  1087 				let
  1088 					val (sizes, intrs) = model
  1089 					val (intr, _, a)   = interpret thy (sizes, []) args (Free ("<Eps>", T))
  1090 					(* create all constants of type T' => bool, ... *)
  1091 					val (intrFun, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<Eps>", Type ("fun", [T', Type ("bool",[])])))
  1092 					(* ... and all constants of type T' *)
  1093 					val (intrT', _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<Eps>", T'))
  1094 					(* returns a list with all unit vectors of length n *)
  1095 					(* int -> interpretation list *)
  1096 					fun unit_vectors n =
  1097 					let
  1098 						(* returns the k-th unit vector of length n *)
  1099 						(* int * int -> interpretation *)
  1100 						fun unit_vector (k,n) =
  1101 							Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1102 						(* int -> interpretation list -> interpretation list *)
  1103 						fun unit_vectors_acc k vs =
  1104 							if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1105 					in
  1106 						unit_vectors_acc 1 []
  1107 					end
  1108 					(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1109 					(* 'a -> 'a list list -> 'a list list *)
  1110 					fun cons_list x xss =
  1111 						map (fn xs => x::xs) xss
  1112 					(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1113 					(* int -> 'a list -> 'a list list *)
  1114 					fun pick_all 1 xs =
  1115 						map (fn x => [x]) xs
  1116 					  | pick_all n xs =
  1117 						let val rec_pick = pick_all (n-1) xs in
  1118 							foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1119 						end
  1120 					(* interpretation -> interpretation list *)
  1121 					fun make_constants (Leaf xs) =
  1122 						unit_vectors (length xs)
  1123 					  | make_constants (Node xs) =
  1124 						map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1125 					val constantsFun = make_constants intrFun
  1126 					val constantsT'  = make_constants intrT'
  1127 					(* interpretation -> interpretation list -> interpretation list *)
  1128 					fun true_values (Node xs) cs =
  1129 						mapfilter (fn (x,c) => if toTrue x = True then Some c else None) (xs~~cs)
  1130 					  | true_values _ _ =
  1131 						raise REFUTE ("HOLogic_interpreter", "\"Eps\": function interpreted as a leaf")
  1132 				in
  1133 					case intr of
  1134 					  Node xs =>
  1135 						let
  1136 							val (wf, intrsEps) = foldl_map (fn (w,(x,f)) =>
  1137 								case true_values f constantsT' of
  1138 								  []  => (w, x)  (* no value mapped to true -> no restriction *)
  1139 								| [c] => (w, c)  (* one value mapped to true -> that's the one *)
  1140 								| cs  =>
  1141 									let
  1142 										(* interpretation * interpretation -> prop_formula *)
  1143 										fun interpret_equal (tr1,tr2) =
  1144 											(case tr1 of
  1145 											  Leaf x =>
  1146 												(case tr2 of
  1147 												  Leaf y => PropLogic.dot_product (x,y)
  1148 												| _      => raise REFUTE ("HOLogic_interpreter", "\"Eps\": second tree is higher"))
  1149 												| Node xs =>
  1150 												(case tr2 of
  1151 												  Leaf _  => raise REFUTE ("HOLogic_interpreter", "\"Eps\": first tree is higher")
  1152 												(* extensionality: two functions are equal iff they are equal for every element *)
  1153 												| Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
  1154 									in
  1155 										(SAnd (w, PropLogic.exists (map (fn c => interpret_equal (x,c)) cs)), x)  (* impose restrictions on x *)
  1156 									end
  1157 								)
  1158 								(#wellformed a, xs ~~ constantsFun)
  1159 							val intrEps = Node intrsEps
  1160 						in
  1161 							Some (intrEps, (sizes, (t,intrEps)::intrs), {next_idx = #next_idx a, bounds = #bounds a, wellformed = wf})
  1162 						end
  1163 					| _ =>
  1164 						raise REFUTE ("HOLogic_interpreter", "\"Eps\": interpretation is a leaf")
  1165 				end)
  1166 		| Const ("All", _) $ t1 =>
  1167 			let
  1168 				val (i,m,a) = interpret thy model args t1
  1169 			in
  1170 				case i of
  1171 				  Node xs =>
  1172 					let
  1173 						val fmTrue  = PropLogic.all (map toTrue xs)
  1174 						val fmFalse = PropLogic.exists (map toFalse xs)
  1175 					in
  1176 						Some (Leaf [fmTrue, fmFalse], m, a)
  1177 					end
  1178 				| _ =>
  1179 					raise REFUTE ("HOLogic_interpreter", "\"All\" is not followed by a function")
  1180 			end
  1181 		| Const ("All", _) =>
  1182 			Some (interpret thy model args (eta_expand t 1))
  1183 		| Const ("Ex", _) $ t1 =>
  1184 			let
  1185 				val (i,m,a) = interpret thy model args t1
  1186 			in
  1187 				case i of
  1188 				  Node xs =>
  1189 					let
  1190 						val fmTrue  = PropLogic.exists (map toTrue xs)
  1191 						val fmFalse = PropLogic.all (map toFalse xs)
  1192 					in
  1193 						Some (Leaf [fmTrue, fmFalse], m, a)
  1194 					end
  1195 				| _ =>
  1196 					raise REFUTE ("HOLogic_interpreter", "\"Ex\" is not followed by a function")
  1197 			end
  1198 		| Const ("Ex", _) =>
  1199 			Some (interpret thy model args (eta_expand t 1))
  1200 		| Const ("Ex1", _) $ t1 =>
  1201 			let
  1202 				val (i,m,a) = interpret thy model args t1
  1203 			in
  1204 				case i of
  1205 				  Node xs =>
  1206 					let
  1207 						(* interpretation list -> prop_formula *)
  1208 						fun allfalse []      = True
  1209 						  | allfalse (x::xs) = SAnd (toFalse x, allfalse xs)
  1210 						(* interpretation list -> prop_formula *)
  1211 						fun exactly1true []      = False
  1212 						  | exactly1true (x::xs) = SOr (SAnd (toTrue x, allfalse xs), SAnd (toFalse x, exactly1true xs))
  1213 						(* interpretation list -> prop_formula *)
  1214 						fun atleast2true []      = False
  1215 						  | atleast2true (x::xs) = SOr (SAnd (toTrue x, PropLogic.exists (map toTrue xs)), atleast2true xs)
  1216 						val fmTrue  = exactly1true xs
  1217 						val fmFalse = SOr (allfalse xs, atleast2true xs)
  1218 					in
  1219 						Some (Leaf [fmTrue, fmFalse], m, a)
  1220 					end
  1221 				| _ =>
  1222 					raise REFUTE ("HOLogic_interpreter", "\"Ex1\" is not followed by a function")
  1223 			end
  1224 		| Const ("Ex1", _) =>
  1225 			Some (interpret thy model args (eta_expand t 1))
  1226 		| Const ("op =", _) $ t1 $ t2 =>
  1227 				let
  1228 					val (i1,m1,a1) = interpret thy model args t1
  1229 					val (i2,m2,a2) = interpret thy m1 a1 t2
  1230 					(* interpretation * interpretation -> prop_formula *)
  1231 					fun interpret_equal (tr1,tr2) =
  1232 						(case tr1 of
  1233 						  Leaf x =>
  1234 							(case tr2 of
  1235 							  Leaf y => PropLogic.dot_product (x,y)
  1236 							| _      => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher"))
  1237 						| Node xs =>
  1238 							(case tr2 of
  1239 							  Leaf _  => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher")
  1240 							(* extensionality: two functions are equal iff they are equal for every element *)
  1241 							| Node ys => PropLogic.all (map interpret_equal (xs ~~ ys))))
  1242 					(* interpretation * interpretation -> prop_formula *)
  1243 					fun interpret_unequal (tr1,tr2) =
  1244 						(case tr1 of
  1245 						  Leaf x =>
  1246 							(case tr2 of
  1247 							  Leaf y =>
  1248 								let
  1249 									fun unequal [] ([],_) =
  1250 										False
  1251 									  | unequal (x::xs) (y::ys1, ys2) =
  1252 										SOr (SAnd (x, PropLogic.exists (ys1@ys2)), unequal xs (ys1, y::ys2))
  1253 									  | unequal _ _ =
  1254 										raise REFUTE ("HOLogic_interpreter", "\"==\": leafs have different width")
  1255 								in
  1256 									unequal x (y,[])
  1257 								end
  1258 							| _      => raise REFUTE ("HOLogic_interpreter", "\"==\": second tree is higher"))
  1259 						| Node xs =>
  1260 							(case tr2 of
  1261 							  Leaf _  => raise REFUTE ("HOLogic_interpreter", "\"==\": first tree is higher")
  1262 							(* extensionality: two functions are unequal iff there exist unequal elements *)
  1263 							| Node ys => PropLogic.exists (map interpret_unequal (xs ~~ ys))))
  1264 					val fmTrue  = interpret_equal (i1,i2)
  1265 					val fmFalse = interpret_unequal (i1,i2)
  1266 				in
  1267 					Some (Leaf [fmTrue, fmFalse], m2, a2)
  1268 				end
  1269 		| Const ("op =", _) $ t1 =>
  1270 			Some (interpret thy model args (eta_expand t 1))
  1271 		| Const ("op =", _) =>
  1272 			Some (interpret thy model args (eta_expand t 2))
  1273 		| Const ("op &", _) $ t1 $ t2 =>
  1274 			apply_interpreter thy model args t
  1275 		| Const ("op &", _) $ t1 =>
  1276 			apply_interpreter thy model args t
  1277 		| Const ("op &", _) =>
  1278 			Some (Node [Node [TT, FF], Node [FF, FF]], model, args)
  1279 		| Const ("op |", _) $ t1 $ t2 =>
  1280 			apply_interpreter thy model args t
  1281 		| Const ("op |", _) $ t1 =>
  1282 			apply_interpreter thy model args t
  1283 		| Const ("op |", _) =>
  1284 			Some (Node [Node [TT, TT], Node [TT, FF]], model, args)
  1285 		| Const ("op -->", _) $ t1 $ t2 =>
  1286 			apply_interpreter thy model args t
  1287 		| Const ("op -->", _) $ t1 =>
  1288 			apply_interpreter thy model args t
  1289 		| Const ("op -->", _) =>
  1290 			Some (Node [Node [TT, FF], Node [TT, TT]], model, args)
  1291 		| Const ("Collect", _) $ t1 =>
  1292 			(* Collect == identity *)
  1293 			Some (interpret thy model args t1)
  1294 		| Const ("Collect", _) =>
  1295 			Some (interpret thy model args (eta_expand t 1))
  1296 		| Const ("op :", _) $ t1 $ t2 =>
  1297 			(* op: == application *)
  1298 			Some (interpret thy model args (t2 $ t1))
  1299 		| Const ("op :", _) $ t1 =>
  1300 			Some (interpret thy model args (eta_expand t 1))
  1301 		| Const ("op :", _) =>
  1302 			Some (interpret thy model args (eta_expand t 2))
  1303 		| _ => None
  1304 	end;
  1305 
  1306 	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1307 
  1308 	fun IDT_interpreter thy model args t =
  1309 	let
  1310 		fun is_var (Free _) = true
  1311 		  | is_var (Var _)  = true
  1312 		  | is_var _        = false
  1313 		fun typeof (Free (_,T)) = T
  1314 		  | typeof (Var (_,T))  = T
  1315 		  | typeof _            = raise REFUTE ("var_IDT_interpreter", "term is not a variable")
  1316 		val (sizes, intrs) = model
  1317 		(* power(a,b) computes a^b, for a>=0, b>=0 *)
  1318 		(* int * int -> int *)
  1319 		fun power (a,0) = 1
  1320 		  | power (a,1) = a
  1321 		  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
  1322 		(* interpretation -> int *)
  1323 		fun size_of_interpretation (Leaf xs) = length xs
  1324 		  | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
  1325 		(* Term.typ -> int *)
  1326 		fun size_of_type T =
  1327 			let
  1328 				val (i,_,_) = interpret thy model args (Free ("<IDT>", T))
  1329 			in
  1330 				size_of_interpretation i
  1331 			end
  1332 		(* int list -> int *)
  1333 		fun sum xs = foldl op+ (0, xs)
  1334 		(* int list -> int *)
  1335 		fun product xs = foldl op* (1, xs)
  1336 		(* DatatypeAux.dtyp * Term.typ -> DatatypeAux.dtyp -> Term.typ *)
  1337 		fun typ_of_dtyp typ_assoc (DatatypeAux.DtTFree a) =
  1338 			the (assoc (typ_assoc, DatatypeAux.DtTFree a))
  1339 		  | typ_of_dtyp typ_assoc (DatatypeAux.DtRec i) =
  1340 			raise REFUTE ("var_IDT_interpreter", "recursive datatype")
  1341 		  | typ_of_dtyp typ_assoc (DatatypeAux.DtType (s, ds)) =
  1342 			Type (s, map (typ_of_dtyp typ_assoc) ds)
  1343 	in
  1344 		if is_var t then
  1345 			(case typeof t of
  1346 			  Type (s, Ts) =>
  1347 				(case DatatypePackage.datatype_info thy s of
  1348 				  Some info =>  (* inductive datatype *)
  1349 					let
  1350 						val index               = #index info
  1351 						val descr               = #descr info
  1352 						val (_, dtyps, constrs) = the (assoc (descr, index))
  1353 					in
  1354 						if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
  1355 							raise REFUTE ("var_IDT_interpreter", "recursive datatype argument")
  1356 						else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
  1357 							None  (* recursive datatype (requires an infinite model) *)
  1358 						else
  1359 							case assoc (intrs, t) of
  1360 							  Some intr => Some (intr, model, args)
  1361 							| None      =>
  1362 								let
  1363 									val typ_assoc = dtyps ~~ Ts
  1364 									val size = sum (map (fn (_,ds) =>
  1365 										product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) constrs)
  1366 									val idx  = #next_idx args
  1367 									(* for us, an IDT has no "internal structure" -- its interpretation is just a leaf *)
  1368 									val intr = (if size=2 then Leaf [BoolVar idx, Not (BoolVar idx)] else Leaf (map BoolVar (idx upto (idx+size-1))))
  1369 									val next = (if size=2 then idx+1 else idx+size)
  1370 								in
  1371 									(* extend the model, increase 'next_idx' *)
  1372 									Some (intr, (sizes, (t, intr)::intrs), {next_idx = next, bounds = #bounds args, wellformed = #wellformed args})
  1373 								end
  1374 					end
  1375 				| None => None)
  1376 			| _ => None)
  1377 		else
  1378 		let
  1379 			val (head, params) = strip_comb t  (* look into applications to avoid unfolding *)
  1380 		in
  1381 			(case head of
  1382 			  Const (c, T) =>
  1383 				(case body_type T of
  1384 				  Type (s, Ts) =>
  1385 					(case DatatypePackage.datatype_info thy s of
  1386 					  Some info =>  (* inductive datatype *)
  1387 						let
  1388 							val index               = #index info
  1389 							val descr               = #descr info
  1390 							val (_, dtyps, constrs) = the (assoc (descr, index))
  1391 						in
  1392 							if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
  1393 								raise REFUTE ("var_IDT_interpreter", "recursive datatype argument")
  1394 							else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
  1395 								None  (* recursive datatype (requires an infinite model) *)
  1396 							else
  1397 								(case take_prefix (fn (c',_) => c' <> c) constrs of
  1398 								  (_, []) =>
  1399 									None (* unknown constructor *)
  1400 								| (prevs, _) =>
  1401 									if null params then
  1402 									let
  1403 										val typ_assoc = dtyps ~~ Ts
  1404 										val offset = sum (map (fn (_,ds) =>
  1405 											product (map (fn d => size_of_type (typ_of_dtyp typ_assoc d)) ds)) prevs)
  1406 										val (i,_,_) = interpret thy model args (Free ("<IDT>", T))
  1407 										(* int * interpretation  -> int * interpretation *)
  1408 										fun replace (offset, Leaf xs) =
  1409 											(* replace the offset-th element by True, all others by False, inc. offset by 1 *)
  1410 											(offset+1, Leaf (snd (foldl_map (fn (n,_) => (n+1, if n=offset then True else False)) (0, xs))))
  1411 										  | replace (offset, Node xs) =
  1412 											let
  1413 												val (offset', xs') = foldl_map replace (offset, xs)
  1414 											in
  1415 												(offset', Node xs')
  1416 											end
  1417 										val (_,intr) = replace (offset, i)
  1418 									in
  1419 										Some (intr, model, args)
  1420 									end
  1421 									else
  1422 										apply_interpreter thy model args t)  (* avoid unfolding by calling 'apply_interpreter' directly *)
  1423 						end
  1424 					| None => None)
  1425 				| _ => None)
  1426 			| _ => None)
  1427 		end
  1428 	end;
  1429 
  1430 
  1431 (* ------------------------------------------------------------------------- *)
  1432 (* PRINTERS                                                                  *)
  1433 (* ------------------------------------------------------------------------- *)
  1434 
  1435 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1436 
  1437 	fun var_typevar_printer thy model t intr assignment =
  1438 	let
  1439 		fun is_var (Free _) = true
  1440 		  | is_var (Var _)  = true
  1441 		  | is_var _        = false
  1442 		fun typeof (Free (_,T)) = T
  1443 		  | typeof (Var (_,T))  = T
  1444 		  | typeof _            = raise REFUTE ("var_typevar_printer", "term is not a variable")
  1445 		fun is_typevar (TFree _) = true
  1446 		  | is_typevar (TVar _)  = true
  1447 		  | is_typevar _         = false
  1448 	in
  1449 		if is_var t andalso is_typevar (typeof t) then
  1450 			let
  1451 				(* interpretation -> int *)
  1452 				fun index_from_interpretation (Leaf xs) =
  1453 					let
  1454 						val idx = find_index (PropLogic.eval assignment) xs
  1455 					in
  1456 						if idx<0 then
  1457 							raise REFUTE ("var_typevar_printer", "illegal interpretation: no value assigned")
  1458 						else
  1459 							idx
  1460 					end
  1461 				  | index_from_interpretation _ =
  1462 					raise REFUTE ("var_typevar_printer", "interpretation is not a leaf")
  1463 				(* string -> string *)
  1464 				fun strip_leading_quote s =
  1465 					(implode o (fn (x::xs) => if x="'" then xs else (x::xs)) o explode) s
  1466 				(* Term.typ -> string *)
  1467 				fun string_of_typ (TFree (x,_))    = strip_leading_quote x
  1468 				  | string_of_typ (TVar ((x,i),_)) = strip_leading_quote x ^ string_of_int i
  1469 				  | string_of_typ _                = raise REFUTE ("var_typevar_printer", "type is not a type variable")
  1470 			in
  1471 				Some (string_of_typ (typeof t) ^ string_of_int (index_from_interpretation intr))
  1472 			end
  1473 		else
  1474 			None
  1475 	end;
  1476 
  1477 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1478 
  1479 	fun var_funtype_printer thy model t intr assignment =
  1480 	let
  1481 		fun is_var (Free _) = true
  1482 		  | is_var (Var _)  = true
  1483 		  | is_var _        = false
  1484 		fun typeof (Free (_,T)) = T
  1485 		  | typeof (Var (_,T))  = T
  1486 		  | typeof _            = raise REFUTE ("var_funtype_printer", "term is not a variable")
  1487 		fun is_funtype (Type ("fun", [_,_])) = true
  1488 		  | is_funtype _                     = false
  1489 	in
  1490 		if is_var t andalso is_funtype (typeof t) then
  1491 			let
  1492 				val T1         = domain_type (typeof t)
  1493 				val T2         = range_type (typeof t)
  1494 				val (sizes, _) = model
  1495 				(* create all constants of type T1 *)
  1496 				val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_funtype_printer", T1))
  1497 				(* returns a list with all unit vectors of length n *)
  1498 				(* int -> interpretation list *)
  1499 				fun unit_vectors n =
  1500 				let
  1501 					(* returns the k-th unit vector of length n *)
  1502 					(* int * int -> interpretation *)
  1503 					fun unit_vector (k,n) =
  1504 						Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1505 					(* int -> interpretation list -> interpretation list *)
  1506 					fun unit_vectors_acc k vs =
  1507 						if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1508 				in
  1509 					unit_vectors_acc 1 []
  1510 				end
  1511 				(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1512 				(* 'a -> 'a list list -> 'a list list *)
  1513 				fun cons_list x xss =
  1514 					map (fn xs => x::xs) xss
  1515 				(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1516 				(* int -> 'a list -> 'a list list *)
  1517 				fun pick_all 1 xs =
  1518 					map (fn x => [x]) xs
  1519 				  | pick_all n xs =
  1520 					let val rec_pick = pick_all (n-1) xs in
  1521 						foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1522 					end
  1523 				(* interpretation -> interpretation list *)
  1524 				fun make_constants (Leaf xs) =
  1525 					unit_vectors (length xs)
  1526 				  | make_constants (Node xs) =
  1527 					map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1528 				(* interpretation list *)
  1529 				val results = (case intr of
  1530 					  Node xs => xs
  1531 					| _       => raise REFUTE ("var_funtype_printer", "interpretation is a leaf"))
  1532 				(* string list *)
  1533 				val strings = map
  1534 					(fn (argi,resulti) => print thy model (Free ("var_funtype_printer", T1)) argi assignment
  1535 						^ "\\<mapsto>"
  1536 						^ print thy model (Free ("var_funtype_printer", T2)) resulti assignment)
  1537 					((make_constants i) ~~ results)
  1538 			in
  1539 				Some (enclose "(" ")" (commas strings))
  1540 			end
  1541 		else
  1542 			None
  1543 	end;
  1544 
  1545 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1546 
  1547 	fun var_settype_printer thy model t intr assignment =
  1548 	let
  1549 		val (sizes, _) = model
  1550 		(* returns a list with all unit vectors of length n *)
  1551 		(* int -> interpretation list *)
  1552 		fun unit_vectors n =
  1553 		let
  1554 			(* returns the k-th unit vector of length n *)
  1555 			(* int * int -> interpretation *)
  1556 			fun unit_vector (k,n) =
  1557 				Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1558 			(* int -> interpretation list -> interpretation list *)
  1559 			fun unit_vectors_acc k vs =
  1560 				if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1561 		in
  1562 			unit_vectors_acc 1 []
  1563 		end
  1564 		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1565 		(* 'a -> 'a list list -> 'a list list *)
  1566 		fun cons_list x xss =
  1567 			map (fn xs => x::xs) xss
  1568 		(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1569 		(* int -> 'a list -> 'a list list *)
  1570 		fun pick_all 1 xs =
  1571 			map (fn x => [x]) xs
  1572 		  | pick_all n xs =
  1573 			let val rec_pick = pick_all (n-1) xs in
  1574 				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1575 			end
  1576 		(* interpretation -> interpretation list *)
  1577 		fun make_constants (Leaf xs) =
  1578 			unit_vectors (length xs)
  1579 		  | make_constants (Node xs) =
  1580 			map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1581 	in
  1582 		case t of
  1583 		  Free (x, Type ("set", [T])) =>
  1584 			let
  1585 				(* interpretation list *)
  1586 				val results = (case intr of
  1587 				  Node xs => xs
  1588 					| _       => raise REFUTE ("var_settype_printer", "interpretation is a leaf"))
  1589 				(* create all constants of type T *)
  1590 				val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T))
  1591 				(* string list *)
  1592 				val strings = mapfilter
  1593 					(fn (argi,Leaf [fmTrue,fmFalse]) =>
  1594 						if PropLogic.eval assignment fmTrue then
  1595 							Some (print thy model (Free ("x", T)) argi assignment)
  1596 						else if PropLogic.eval assignment fmFalse then
  1597 							None
  1598 						else
  1599 							raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned"))
  1600 					((make_constants i) ~~ results)
  1601 			in
  1602 				Some (enclose "{" "}" (commas strings))
  1603 			end
  1604 		| Var ((x,i), Type ("set", [T])) =>
  1605 			let
  1606 				(* interpretation list *)
  1607 				val results = (case intr of
  1608 				  Node xs => xs
  1609 					| _       => raise REFUTE ("var_settype_printer", "interpretation is a leaf"))
  1610 				(* create all constants of type T *)
  1611 				val (i, _, _) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("var_settype_printer", T))
  1612 				(* string list *)
  1613 				val strings = mapfilter
  1614 					(fn (argi,Leaf [fmTrue,fmFalse]) =>
  1615 						if PropLogic.eval assignment fmTrue then
  1616 							Some (print thy model (Free ("var_settype_printer", T)) argi assignment)
  1617 						else if PropLogic.eval assignment fmTrue then
  1618 							None
  1619 						else
  1620 							raise REFUTE ("var_settype_printer", "illegal interpretation: no value assigned"))
  1621 					((make_constants i) ~~ results)
  1622 			in
  1623 				Some (enclose "{" "}" (commas strings))
  1624 			end
  1625 		| _ => None
  1626 	end;
  1627 
  1628 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1629 
  1630 	fun HOLogic_printer thy model t intr assignment =
  1631 		case t of
  1632 		(* 'arbitrary', 'The', 'Hilbert_Choice.Eps' are printed like free variables of the same type *)
  1633 		  Const ("arbitrary", T) =>
  1634 			Some (print thy model (Free ("<arbitrary>", T)) intr assignment)
  1635 		| Const ("The", T) =>
  1636 			Some (print thy model (Free ("<The>", T)) intr assignment)
  1637 		| Const ("Hilbert_Choice.Eps", T) =>
  1638 			Some (print thy model (Free ("<Eps>", T)) intr assignment)
  1639 		| _ =>
  1640 			None;
  1641 
  1642 	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> string option *)
  1643 
  1644 	fun var_IDT_printer thy model t intr assignment =
  1645 	let
  1646 		fun is_var (Free _) = true
  1647 		  | is_var (Var _)  = true
  1648 		  | is_var _        = false
  1649 		fun typeof (Free (_,T)) = T
  1650 		  | typeof (Var (_,T))  = T
  1651 		  | typeof _            = raise REFUTE ("var_IDT_printer", "term is not a variable")
  1652 	in
  1653 		if is_var t then
  1654 			(case typeof t of
  1655 			  Type (s, Ts) =>
  1656 				(case DatatypePackage.datatype_info thy s of
  1657 				  Some info =>  (* inductive datatype *)
  1658 					let
  1659 						val index               = #index info
  1660 						val descr               = #descr info
  1661 						val (_, dtyps, constrs) = the (assoc (descr, index))
  1662 					in
  1663 						if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then
  1664 							raise REFUTE ("var_IDT_printer", "recursive datatype argument")
  1665 						else if Library.exists (fn (_,ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
  1666 							None  (* recursive datatype (requires an infinite model) *)
  1667 						else
  1668 						let
  1669 							val (sizes, _) = model
  1670 							val typ_assoc  = dtyps ~~ Ts
  1671 							(* interpretation -> int *)
  1672 							fun index_from_interpretation (Leaf xs) =
  1673 								let
  1674 									val idx = find_index (PropLogic.eval assignment) xs
  1675 								in
  1676 									if idx<0 then
  1677 										raise REFUTE ("var_IDT_printer", "illegal interpretation: no value assigned")
  1678 									else
  1679 										idx
  1680 								end
  1681 							  | index_from_interpretation _ =
  1682 								raise REFUTE ("var_IDT_printer", "interpretation is not a leaf")
  1683 							(* string -> string *)
  1684 							fun unqualify s =
  1685 								implode (snd (take_suffix (fn c => c <> ".") (explode s)))
  1686 							(* DatatypeAux.dtyp -> Term.typ *)
  1687 							fun typ_of_dtyp (DatatypeAux.DtTFree a) =
  1688 								the (assoc (typ_assoc, DatatypeAux.DtTFree a))
  1689 							  | typ_of_dtyp (DatatypeAux.DtRec i) =
  1690 								raise REFUTE ("var_IDT_printer", "recursive datatype")
  1691 							  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
  1692 								Type (s, map typ_of_dtyp ds)
  1693 							fun sum xs     = foldl op+ (0, xs)
  1694 							fun product xs = foldl op* (1, xs)
  1695 							(* power(a,b) computes a^b, for a>=0, b>=0 *)
  1696 							(* int * int -> int *)
  1697 							fun power (a,0) = 1
  1698 							  | power (a,1) = a
  1699 							  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
  1700 							fun size_of_interpretation (Leaf xs) = length xs
  1701 							  | size_of_interpretation (Node xs) = power (size_of_interpretation (hd xs), length xs)
  1702 							fun size_of_type T =
  1703 								let
  1704 									val (i,_,_) = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<IDT>", T))
  1705 								in
  1706 									size_of_interpretation i
  1707 								end
  1708 							(* returns a list with all unit vectors of length n *)
  1709 							(* int -> interpretation list *)
  1710 							fun unit_vectors n =
  1711 							let
  1712 								(* returns the k-th unit vector of length n *)
  1713 								(* int * int -> interpretation *)
  1714 								fun unit_vector (k,n) =
  1715 									Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1716 								(* int -> interpretation list -> interpretation list *)
  1717 								fun unit_vectors_acc k vs =
  1718 									if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
  1719 							in
  1720 								unit_vectors_acc 1 []
  1721 							end
  1722 							(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1723 							(* 'a -> 'a list list -> 'a list list *)
  1724 							fun cons_list x xss =
  1725 								map (fn xs => x::xs) xss
  1726 							(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
  1727 							(* int -> 'a list -> 'a list list *)
  1728 							fun pick_all 1 xs =
  1729 								map (fn x => [x]) xs
  1730 							  | pick_all n xs =
  1731 								let val rec_pick = pick_all (n-1) xs in
  1732 									foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1733 								end
  1734 							(* interpretation -> interpretation list *)
  1735 							fun make_constants (Leaf xs) =
  1736 								unit_vectors (length xs)
  1737 							  | make_constants (Node xs) =
  1738 								map (fn xs' => Node xs') (pick_all (length xs) (make_constants (hd xs)))
  1739 							(* DatatypeAux.dtyp list -> int -> string *)
  1740 							fun string_of_inductive_type_cargs [] n =
  1741 								if n<>0 then
  1742 									raise REFUTE ("var_IDT_printer", "internal error computing the element index for an inductive type")
  1743 								else
  1744 									""
  1745 							  | string_of_inductive_type_cargs (d::ds) n =
  1746 								let
  1747 									val size_ds   = product (map (fn d => size_of_type (typ_of_dtyp d)) ds)
  1748 									val T         = typ_of_dtyp d
  1749 									val (i,_,_)   = interpret thy (sizes, []) {next_idx=1, bounds=[], wellformed=True} (Free ("<IDT>", T))
  1750 									val constants = make_constants i
  1751 								in
  1752 									" "
  1753 									^ (print thy model (Free ("<IDT>", T)) (nth_elem (n div size_ds, constants)) assignment)
  1754 									^ (string_of_inductive_type_cargs ds (n mod size_ds))
  1755 								end
  1756 							(* (string * DatatypeAux.dtyp list) list -> int -> string *)
  1757 							fun string_of_inductive_type_constrs [] n =
  1758 								raise REFUTE ("var_IDT_printer", "inductive type has fewer elements than needed")
  1759 							  | string_of_inductive_type_constrs ((c,ds)::cs) n =
  1760 								let
  1761 									val size = product (map (fn d => size_of_type (typ_of_dtyp d)) ds)
  1762 								in
  1763 									if n < size then
  1764 										(unqualify c) ^ (string_of_inductive_type_cargs ds n)
  1765 									else
  1766 										string_of_inductive_type_constrs cs (n - size)
  1767 								end
  1768 						in
  1769 							Some (string_of_inductive_type_constrs constrs (index_from_interpretation intr))
  1770 						end
  1771 					end
  1772 				| None => None)
  1773 			| _ => None)
  1774 		else
  1775 			None
  1776 	end;
  1777 
  1778 
  1779 (* ------------------------------------------------------------------------- *)
  1780 (* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
  1781 (* structure                                                                 *)
  1782 (* ------------------------------------------------------------------------- *)
  1783 
  1784 (* ------------------------------------------------------------------------- *)
  1785 (* Note: the interpreters and printers are used in reverse order; however,   *)
  1786 (*       an interpreter that can handle non-atomic terms ends up being       *)
  1787 (*       applied before other interpreters are applied to subterms!          *)
  1788 (* ------------------------------------------------------------------------- *)
  1789 
  1790 	(* (theory -> theory) list *)
  1791 
  1792 	val setup =
  1793 		[RefuteData.init,
  1794 		 add_interpreter "var_typevar"   var_typevar_interpreter,
  1795 		 add_interpreter "var_funtype"   var_funtype_interpreter,
  1796 		 add_interpreter "var_settype"   var_settype_interpreter,
  1797 		 add_interpreter "boundvar"      boundvar_interpreter,
  1798 		 add_interpreter "abstraction"   abstraction_interpreter,
  1799 		 add_interpreter "apply"         apply_interpreter,
  1800 		 add_interpreter "const_unfold"  const_unfold_interpreter,
  1801 		 add_interpreter "Pure"          Pure_interpreter,
  1802 		 add_interpreter "HOLogic"       HOLogic_interpreter,
  1803 		 add_interpreter "IDT"           IDT_interpreter,
  1804 		 add_printer "var_typevar"   var_typevar_printer,
  1805 		 add_printer "var_funtype"   var_funtype_printer,
  1806 		 add_printer "var_settype"   var_settype_printer,
  1807 		 add_printer "HOLogic"       HOLogic_printer,
  1808 		 add_printer "var_IDT"       var_IDT_printer];
  1809 
  1810 end