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