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