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