src/HOL/Tools/refute.ML
changeset 15547 f08e2d83681e
parent 15531 08c8dad8e399
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Feb 23 10:23:22 2005 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed Feb 23 14:04:53 2005 +0100
     1.3 @@ -1,13 +1,11 @@
     1.4  (*  Title:      HOL/Tools/refute.ML
     1.5      ID:         $Id$
     1.6      Author:     Tjark Weber
     1.7 -    Copyright   2003-2004
     1.8 +    Copyright   2003-2005
     1.9  
    1.10  Finite model generation for HOL formulas, using a SAT solver.
    1.11  *)
    1.12  
    1.13 -(* TODO: case, recursion, size for IDTs are not supported yet *)
    1.14 -
    1.15  (* ------------------------------------------------------------------------- *)
    1.16  (* Declares the 'REFUTE' signature as well as a structure 'Refute'.          *)
    1.17  (* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'.  *)
    1.18 @@ -115,7 +113,6 @@
    1.19  				  Node ys => Node (map tree_pair (xs ~~ ys))
    1.20  				| Leaf _  => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
    1.21  
    1.22 -
    1.23  (* ------------------------------------------------------------------------- *)
    1.24  (* params: parameters that control the translation into a propositional      *)
    1.25  (*         formula/model generation                                          *)
    1.26 @@ -168,9 +165,9 @@
    1.27  
    1.28  	type arguments =
    1.29  		{
    1.30 -			(* just passed unchanged from 'params' *)
    1.31 -			maxvars   : int,
    1.32 -			(* these may change during the translation *)
    1.33 +			maxvars   : int,   (* just passed unchanged from 'params' *)
    1.34 +			def_eq    : bool,  (* whether to use 'make_equality' or 'make_def_equality' *)
    1.35 +			(* the following may change during the translation *)
    1.36  			next_idx  : int,
    1.37  			bounds    : interpretation list,
    1.38  			wellformed: prop_formula
    1.39 @@ -213,19 +210,19 @@
    1.40  
    1.41  	fun interpret thy model args t =
    1.42  		(case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of
    1.43 -		  NONE   => raise REFUTE ("interpret", "unable to interpret term " ^ quote (Sign.string_of_term (sign_of thy) t))
    1.44 +		  NONE   => raise REFUTE ("interpret", "no interpreter for term " ^ quote (Sign.string_of_term (sign_of thy) t))
    1.45  		| SOME x => x);
    1.46  
    1.47  (* ------------------------------------------------------------------------- *)
    1.48 -(* print: tries to convert the constant denoted by the term 't' into a term  *)
    1.49 -(*        using a suitable printer                                           *)
    1.50 +(* print: converts the constant denoted by the term 't' into a term using a  *)
    1.51 +(*        suitable printer                                                   *)
    1.52  (* ------------------------------------------------------------------------- *)
    1.53  
    1.54  	(* theory -> model -> Term.term -> interpretation -> (int -> bool) -> Term.term *)
    1.55  
    1.56  	fun print thy model t intr assignment =
    1.57  		(case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of
    1.58 -		  NONE   => Const ("<<no printer available>>", fastype_of t)
    1.59 +		  NONE   => raise REFUTE ("print", "no printer for term " ^ quote (Sign.string_of_term (sign_of thy) t))
    1.60  		| SOME x => x);
    1.61  
    1.62  (* ------------------------------------------------------------------------- *)
    1.63 @@ -386,21 +383,21 @@
    1.64  	fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
    1.65  		(* replace a 'DtTFree' variable by the associated type *)
    1.66  		(the o assoc) (typ_assoc, DatatypeAux.DtTFree a)
    1.67 +	  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
    1.68 +		Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.69  	  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
    1.70  		let
    1.71  			val (s, ds, _) = (the o assoc) (descr, i)
    1.72  		in
    1.73  			Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.74 -		end
    1.75 -	  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
    1.76 -		Type (s, map (typ_of_dtyp descr typ_assoc) ds);
    1.77 +		end;
    1.78  
    1.79  (* ------------------------------------------------------------------------- *)
    1.80  (* collect_axioms: collects (monomorphic, universally quantified versions    *)
    1.81  (*                 of) all HOL axioms that are relevant w.r.t 't'            *)
    1.82  (* ------------------------------------------------------------------------- *)
    1.83  
    1.84 -	(* TODO: to make the collection of axioms more easily extensible, this    *)
    1.85 +	(* Note: to make the collection of axioms more easily extensible, this    *)
    1.86  	(*       function could be based on user-supplied "axiom collectors",     *)
    1.87  	(*       similar to 'interpret'/interpreters or 'print'/printers          *)
    1.88  
    1.89 @@ -423,18 +420,23 @@
    1.90  		val _ = immediate_output "Adding axioms..."
    1.91  		(* (string * Term.term) list *)
    1.92  		val axioms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
    1.93 +		(* string list *)
    1.94 +		val rec_names = Symtab.foldl (fn (acc, (_, info)) =>
    1.95 +			#rec_names info @ acc) ([], DatatypePackage.get_datatypes thy)
    1.96 +		(* string list *)
    1.97 +		val const_of_class_names = map Sign.const_of_class (Sign.classes (sign_of thy))
    1.98  		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
    1.99  		(* 't' has a (possibly) more general type, the schematic type          *)
   1.100 -		(* variables in 't' are instantiated to match the type 'T'             *)
   1.101 +		(* variables in 't' are instantiated to match the type 'T' (may raise  *)
   1.102 +		(* Type.TYPE_MATCH)                                                    *)
   1.103  		(* (string * Term.typ) * Term.term -> Term.term *)
   1.104  		fun specialize_type ((s, T), t) =
   1.105  		let
   1.106  			fun find_typeSubs (Const (s', T')) =
   1.107  				(if s=s' then
   1.108 -					SOME (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T)))
   1.109 +					SOME (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))) handle Type.TYPE_MATCH => NONE
   1.110  				else
   1.111 -					NONE
   1.112 -				handle Type.TYPE_MATCH => NONE)
   1.113 +					NONE)
   1.114  			  | find_typeSubs (Free _)           = NONE
   1.115  			  | find_typeSubs (Var _)            = NONE
   1.116  			  | find_typeSubs (Bound _)          = NONE
   1.117 @@ -442,7 +444,7 @@
   1.118  			  | find_typeSubs (t1 $ t2)          = (case find_typeSubs t1 of SOME x => SOME x | NONE => find_typeSubs t2)
   1.119  			val typeSubs = (case find_typeSubs t of
   1.120  				  SOME x => x
   1.121 -				| NONE   => raise REFUTE ("collect_axioms", "no type instantiation found for " ^ quote s ^ " in " ^ Sign.string_of_term (sign_of thy) t))
   1.122 +				| NONE   => raise Type.TYPE_MATCH (* no match found - perhaps due to sort constraints *))
   1.123  		in
   1.124  			map_term_types
   1.125  				(map_type_tvar
   1.126 @@ -460,7 +462,7 @@
   1.127  		(* Term.typ Term.Vartab.table -> Term.term -> Term.term *)
   1.128  		fun monomorphic_term typeSubs t =
   1.129  			map_term_types (map_type_tvar
   1.130 -				(fn (v,_) =>
   1.131 +				(fn (v, _) =>
   1.132  					case Vartab.lookup (typeSubs, v) of
   1.133  					  NONE =>
   1.134  						(* schematic type variable not instantiated *)
   1.135 @@ -468,12 +470,55 @@
   1.136  					| SOME typ =>
   1.137  						typ)) t
   1.138  		(* Term.term list * Term.typ -> Term.term list *)
   1.139 -		fun collect_type_axioms (axs, T) =
   1.140 +		fun collect_sort_axioms (axs, T) =
   1.141 +			let
   1.142 +				(* collect the axioms for a single 'class' (but not for its superclasses) *)
   1.143 +				(* Term.term list * string -> Term.term list *)
   1.144 +				fun collect_class_axioms (axs, class) =
   1.145 +					let
   1.146 +						(* obtain the axioms generated by the "axclass" command *)
   1.147 +						(* (string * Term.term) list *)
   1.148 +						val class_axioms             = filter (fn (s, _) => String.isPrefix (class ^ ".axioms_") s) axioms
   1.149 +						(* replace the one schematic type variable in each axiom by the actual type 'T' *)
   1.150 +						(* (string * Term.term) list *)
   1.151 +						val monomorphic_class_axioms = map (fn (axname, ax) =>
   1.152 +							let
   1.153 +								val (idx, _) = (case term_tvars ax of
   1.154 +									  [is] => is
   1.155 +									| _    => raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ Sign.string_of_term (sign_of thy) ax ^ ") does not contain exactly one type variable"))
   1.156 +							in
   1.157 +								(axname, monomorphic_term (Vartab.make [(idx, T)]) ax)
   1.158 +							end) class_axioms
   1.159 +						(* Term.term list * (string * Term.term) list -> Term.term list *)
   1.160 +						fun collect_axiom (axs, (axname, ax)) =
   1.161 +							if mem_term (ax, axs) then
   1.162 +								axs
   1.163 +							else (
   1.164 +								immediate_output (" " ^ axname);
   1.165 +								collect_term_axioms (ax :: axs, ax)
   1.166 +							)
   1.167 +					in
   1.168 +						foldl collect_axiom (axs, monomorphic_class_axioms)
   1.169 +					end
   1.170 +				(* string list *)
   1.171 +				val sort = (case T of
   1.172 +					  TFree (_, sort) => sort
   1.173 +					| TVar (_, sort)  => sort
   1.174 +					| _               => raise REFUTE ("collect_axioms", "type " ^ Sign.string_of_typ (sign_of thy) T ^ " is not a variable"))
   1.175 +				(* obtain all superclasses of classes in 'sort' *)
   1.176 +				(* string list *)
   1.177 +				val superclasses = Graph.all_succs ((#classes o Type.rep_tsig o Sign.tsig_of o sign_of) thy) sort
   1.178 +			in
   1.179 +				foldl collect_class_axioms (axs, superclasses)
   1.180 +			end
   1.181 +		(* Term.term list * Term.typ -> Term.term list *)
   1.182 +		and collect_type_axioms (axs, T) =
   1.183  			case T of
   1.184  			(* simple types *)
   1.185  			  Type ("prop", [])      => axs
   1.186  			| Type ("fun", [T1, T2]) => collect_type_axioms (collect_type_axioms (axs, T1), T2)
   1.187  			| Type ("set", [T1])     => collect_type_axioms (axs, T1)
   1.188 +			| Type ("itself", [T1])  => collect_type_axioms (axs, T1)  (* axiomatic type classes *)
   1.189  			| Type (s, Ts)           =>
   1.190  				let
   1.191  					(* look up the definition of a type, as created by "typedef" *)
   1.192 @@ -517,18 +562,18 @@
   1.193  						(case get_typedefn axioms of
   1.194  						  SOME (axname, ax) => 
   1.195  							if mem_term (ax, axs) then
   1.196 -								(* collect relevant type axioms for the argument types *)
   1.197 +								(* only collect relevant type axioms for the argument types *)
   1.198  								foldl collect_type_axioms (axs, Ts)
   1.199  							else
   1.200  								(immediate_output (" " ^ axname);
   1.201  								collect_term_axioms (ax :: axs, ax))
   1.202  						| NONE =>
   1.203 +							(* unspecified type, perhaps introduced with 'typedecl' *)
   1.204  							(* at least collect relevant type axioms for the argument types *)
   1.205  							foldl collect_type_axioms (axs, Ts))
   1.206  				end
   1.207 -			(* TODO: include sort axioms *)
   1.208 -			| TFree (_, sorts)       => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
   1.209 -			| TVar  (_, sorts)       => ((*if not (null sorts) then immediate_output " *ignoring sorts*" else ();*) axs)
   1.210 +			| TFree _                => collect_sort_axioms (axs, T)  (* axiomatic type classes *)
   1.211 +			| TVar _                 => collect_sort_axioms (axs, T)  (* axiomatic type classes *)
   1.212  		(* Term.term list * Term.term -> Term.term list *)
   1.213  		and collect_term_axioms (axs, t) =
   1.214  			case t of
   1.215 @@ -536,6 +581,7 @@
   1.216  			  Const ("all", _)                => axs
   1.217  			| Const ("==", _)                 => axs
   1.218  			| Const ("==>", _)                => axs
   1.219 +			| Const ("TYPE", T)               => collect_type_axioms (axs, T)  (* axiomatic type classes *)
   1.220  			(* HOL *)
   1.221  			| Const ("Trueprop", _)           => axs
   1.222  			| Const ("Not", _)                => axs
   1.223 @@ -573,6 +619,10 @@
   1.224  			| Const ("op :", T)               => collect_type_axioms (axs, T)
   1.225  			(* other optimizations *)
   1.226  			| Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
   1.227 +			| Const ("op <", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T)
   1.228 +			| Const ("op +", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
   1.229 +			| Const ("op -", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
   1.230 +			| Const ("op *", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
   1.231  			(* simply-typed lambda calculus *)
   1.232  			| Const (s, T)                    =>
   1.233  				let
   1.234 @@ -580,7 +630,7 @@
   1.235  					(* string -> Term.typ -> (string * Term.term) list -> (string * Term.term) option *)
   1.236  					fun get_defn [] =
   1.237  						NONE
   1.238 -					  | get_defn ((axname,ax)::axms) =
   1.239 +					  | get_defn ((axname, ax)::axms) =
   1.240  						(let
   1.241  							val (lhs, _) = Logic.dest_equals ax  (* equations only *)
   1.242  							val c        = head_of lhs
   1.243 @@ -598,49 +648,68 @@
   1.244  						handle ERROR           => get_defn axms
   1.245  						     | TERM _          => get_defn axms
   1.246  						     | Type.TYPE_MATCH => get_defn axms)
   1.247 -						(* unit -> bool *)
   1.248 -						fun is_IDT_constructor () =
   1.249 -							(case body_type T of
   1.250 -							  Type (s', _) =>
   1.251 -								(case DatatypePackage.constrs_of thy s' of
   1.252 -								  SOME constrs =>
   1.253 -									Library.exists (fn c =>
   1.254 -										(case c of
   1.255 -										  Const (cname, ctype) =>
   1.256 -											cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype)
   1.257 -										| _ =>
   1.258 -											raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
   1.259 -										constrs
   1.260 -								| NONE =>
   1.261 -									false)
   1.262 -							| _  =>
   1.263 +					(* axiomatic type classes *)
   1.264 +					(* unit -> bool *)
   1.265 +					fun is_const_of_class () =
   1.266 +						(* I'm not quite sure if checking the name 's' is sufficient, *)
   1.267 +						(* or if we should also check the type 'T'                    *)
   1.268 +						s mem const_of_class_names
   1.269 +					(* inductive data types *)
   1.270 +					(* unit -> bool *)
   1.271 +					fun is_IDT_constructor () =
   1.272 +						(case body_type T of
   1.273 +						  Type (s', _) =>
   1.274 +							(case DatatypePackage.constrs_of thy s' of
   1.275 +							  SOME constrs =>
   1.276 +								Library.exists (fn c =>
   1.277 +									(case c of
   1.278 +									  Const (cname, ctype) =>
   1.279 +										cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype)
   1.280 +									| _ =>
   1.281 +										raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
   1.282 +									constrs
   1.283 +							| NONE =>
   1.284  								false)
   1.285 -						(* unit -> bool *)
   1.286 -						fun is_IDT_recursor () =
   1.287 -							(* the type of a recursion operator: [T1,...,Tn,IDT]--->TResult (where *)
   1.288 -							(* the T1,...,Tn depend on the types of the datatype's constructors)   *)
   1.289 -							((case last_elem (binder_types T) of
   1.290 -							  Type (s', _) =>
   1.291 -								(case DatatypePackage.datatype_info thy s' of
   1.292 -								  SOME info => s mem (#rec_names info)
   1.293 -								| NONE      => false)  (* not an inductive datatype *)
   1.294 -							| _ =>  (* a (free or schematic) type variable *)
   1.295 -								false)
   1.296 -							handle LIST "last_elem" => false)  (* not even a function type *)
   1.297 +						| _  =>
   1.298 +							false)
   1.299 +					(* unit -> bool *)
   1.300 +					fun is_IDT_recursor () =
   1.301 +						(* I'm not quite sure if checking the name 's' is sufficient, *)
   1.302 +						(* or if we should also check the type 'T'                    *)
   1.303 +						s mem rec_names
   1.304  				in
   1.305 -					if is_IDT_constructor () then
   1.306 +					if is_const_of_class () then
   1.307 +						(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" and *)
   1.308 +						(* the introduction rule "class.intro" as axioms              *)
   1.309 +						let
   1.310 +							val class   = Sign.class_of_const s
   1.311 +							val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
   1.312 +							(* Term.term option *)
   1.313 +							val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
   1.314 +							val intro_ax   = (apsome (fn t => specialize_type ((s, T), t)) (assoc (axioms, class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
   1.315 +							val axs'       = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
   1.316 +									(* collect relevant type axioms *)
   1.317 +									collect_type_axioms (axs, T)
   1.318 +								else
   1.319 +									(immediate_output (" " ^ Sign.string_of_term (sign_of thy) ax);
   1.320 +									collect_term_axioms (ax :: axs, ax)))
   1.321 +							val axs''      = (case intro_ax of NONE => axs' | SOME ax => if mem_term (ax, axs') then
   1.322 +									(* collect relevant type axioms *)
   1.323 +									collect_type_axioms (axs', T)
   1.324 +								else
   1.325 +									(immediate_output (" " ^ class ^ ".intro");
   1.326 +									collect_term_axioms (ax :: axs', ax)))
   1.327 +						in
   1.328 +							axs''
   1.329 +						end
   1.330 +					else if is_IDT_constructor () then
   1.331  						(* only collect relevant type axioms *)
   1.332  						collect_type_axioms (axs, T)
   1.333 -					else if is_IDT_recursor () then (
   1.334 -						(* TODO: we must add the definition of the recursion operator to the axioms, or *)
   1.335 -						(*       (better yet, since simply unfolding the definition won't work for      *)
   1.336 -						(*       initial fragments of recursive IDTs) write an interpreter that         *)
   1.337 -						(*       respects it                                                            *)
   1.338 -						warning "Term contains recursion over a datatype; countermodel(s) may be spurious!";
   1.339 +					else if is_IDT_recursor () then
   1.340  						(* only collect relevant type axioms *)
   1.341  						collect_type_axioms (axs, T)
   1.342 -					) else
   1.343 -						(case get_defn axioms of
   1.344 +					else (
   1.345 +						case get_defn axioms of
   1.346  						  SOME (axname, ax) => 
   1.347  							if mem_term (ax, axs) then
   1.348  								(* collect relevant type axioms *)
   1.349 @@ -650,7 +719,8 @@
   1.350  								collect_term_axioms (ax :: axs, ax))
   1.351  						| NONE =>
   1.352  							(* collect relevant type axioms *)
   1.353 -							collect_type_axioms (axs, T))
   1.354 +							collect_type_axioms (axs, T)
   1.355 +					)
   1.356  				end
   1.357  			| Free (_, T)                     => collect_type_axioms (axs, T)
   1.358  			| Var (_, T)                      => collect_type_axioms (axs, T)
   1.359 @@ -665,7 +735,7 @@
   1.360  			val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   1.361  		in
   1.362  			foldl
   1.363 -				(fn (t', ((x,i),T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x,i),T), t')))
   1.364 +				(fn (t', ((x, i), T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x, i), T), t')))
   1.365  				(t, vars)
   1.366  		end
   1.367  		(* Term.term list *)
   1.368 @@ -773,60 +843,46 @@
   1.369  
   1.370  	fun next_universe xs sizes minsize maxsize =
   1.371  	let
   1.372 -		(* int -> int list -> int list option *)
   1.373 -		fun add1 _ [] =
   1.374 -			NONE  (* overflow *)
   1.375 -		  | add1 max (x::xs) =
   1.376 -		 	if x<max orelse max<0 then
   1.377 -				SOME ((x+1)::xs)  (* add 1 to the head *)
   1.378 -			else
   1.379 -				apsome (fn xs' => 0 :: xs') (add1 max xs)  (* carry-over *)
   1.380 -		(* int -> int list * int list -> int list option *)
   1.381 -		fun shift _ (_, []) =
   1.382 -			NONE
   1.383 -		  | shift max (zeros, x::xs) =
   1.384 -			if x=0 then
   1.385 -				shift max (0::zeros, xs)
   1.386 -			else
   1.387 -				apsome (fn xs' => (x-1) :: (zeros @ xs')) (add1 max xs)
   1.388  		(* creates the "first" list of length 'len', where the sum of all list *)
   1.389  		(* elements is 'sum', and the length of the list is 'len'              *)
   1.390  		(* int -> int -> int -> int list option *)
   1.391 -		fun make_first 0 sum _ =
   1.392 +		fun make_first _ 0 sum =
   1.393  			if sum=0 then
   1.394  				SOME []
   1.395  			else
   1.396  				NONE
   1.397 -		  | make_first len sum max =
   1.398 +		  | make_first max len sum =
   1.399  			if sum<=max orelse max<0 then
   1.400 -				apsome (fn xs' => sum :: xs') (make_first (len-1) 0 max)
   1.401 +				apsome (fn xs' => sum :: xs') (make_first max (len-1) 0)
   1.402  			else
   1.403 -				apsome (fn xs' => max :: xs') (make_first (len-1) (sum-max) max)
   1.404 +				apsome (fn xs' => max :: xs') (make_first max (len-1) (sum-max))
   1.405  		(* enumerates all int lists with a fixed length, where 0<=x<='max' for *)
   1.406  		(* all list elements x (unless 'max'<0)                                *)
   1.407 -		(* int -> int list -> int list option *)
   1.408 -		fun next max xs =
   1.409 -			(case shift max ([], xs) of
   1.410 -			  SOME xs' =>
   1.411 -				SOME xs'
   1.412 -			| NONE =>
   1.413 -				let
   1.414 -					val (len, sum) = foldl (fn ((l, s), x) => (l+1, s+x)) ((0, 0), xs)
   1.415 -				in
   1.416 -					make_first len (sum+1) max  (* increment 'sum' by 1 *)
   1.417 -				end)
   1.418 +		(* int -> int -> int -> int list -> int list option *)
   1.419 +		fun next max len sum [] =
   1.420 +			NONE
   1.421 +		  | next max len sum [x] =
   1.422 +			(* we've reached the last list element, so there's no shift possible *)
   1.423 +			make_first max (len+1) (sum+x+1)  (* increment 'sum' by 1 *)
   1.424 +		  | next max len sum (x1::x2::xs) =
   1.425 +			if x1>0 andalso (x2<max orelse max<0) then
   1.426 +				(* we can shift *)
   1.427 +				SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
   1.428 +			else
   1.429 +				(* continue search *)
   1.430 +				next max (len+1) (sum+x1) (x2::xs)
   1.431  		(* only consider those types for which the size is not fixed *)
   1.432  		val mutables = filter (fn (T, _) => assoc (sizes, string_of_typ T) = NONE) xs
   1.433  		(* subtract 'minsize' from every size (will be added again at the end) *)
   1.434  		val diffs = map (fn (_, n) => n-minsize) mutables
   1.435  	in
   1.436 -		case next (maxsize-minsize) diffs of
   1.437 +		case next (maxsize-minsize) 0 0 diffs of
   1.438  		  SOME diffs' =>
   1.439  			(* merge with those types for which the size is fixed *)
   1.440  			SOME (snd (foldl_map (fn (ds, (T, _)) =>
   1.441  				case assoc (sizes, string_of_typ T) of
   1.442 -				  SOME n => (ds, (T, n))                      (* return the fixed size *)
   1.443 -				| NONE   => (tl ds, (T, minsize + (hd ds))))  (* consume the head of 'ds', add 'minsize' *)
   1.444 +				  SOME n => (ds, (T, n))                    (* return the fixed size *)
   1.445 +				| NONE   => (tl ds, (T, minsize + hd ds)))  (* consume the head of 'ds', add 'minsize' *)
   1.446  				(diffs', xs)))
   1.447  		| NONE =>
   1.448  			NONE
   1.449 @@ -879,18 +935,39 @@
   1.450  			val _      = writeln ("Ground types: "
   1.451  				^ (if null types then "none."
   1.452  				   else commas (map (Sign.string_of_typ (sign_of thy)) types)))
   1.453 +			(* we can only consider fragments of recursive IDTs, so we issue a  *)
   1.454 +			(* warning if the formula contains a recursive IDT                  *)
   1.455 +			(* TODO: no warning needed for /positive/ occurrences of IDTs       *)
   1.456 +			val _ = if Library.exists (fn
   1.457 +				  Type (s, _) =>
   1.458 +					(case DatatypePackage.datatype_info thy s of
   1.459 +					  SOME info =>  (* inductive datatype *)
   1.460 +						let
   1.461 +							val index           = #index info
   1.462 +							val descr           = #descr info
   1.463 +							val (_, _, constrs) = (the o assoc) (descr, index)
   1.464 +						in
   1.465 +							(* recursive datatype? *)
   1.466 +							Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs
   1.467 +						end
   1.468 +					| NONE => false)
   1.469 +				| _ => false) types then
   1.470 +					warning "Term contains a recursive datatype; countermodel(s) may be spurious!"
   1.471 +				else
   1.472 +					()
   1.473  			(* (Term.typ * int) list -> unit *)
   1.474  			fun find_model_loop universe =
   1.475  			let
   1.476  				val init_model             = (universe, [])
   1.477 -				val init_args              = {maxvars = maxvars, next_idx = 1, bounds = [], wellformed = True}
   1.478 +				val init_args              = {maxvars = maxvars, def_eq = false, next_idx = 1, bounds = [], wellformed = True}
   1.479  				val _                      = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
   1.480  				(* translate 't' and all axioms *)
   1.481  				val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
   1.482  					let
   1.483  						val (i, m', a') = interpret thy m a t'
   1.484  					in
   1.485 -						((m', a'), i)
   1.486 +						(* set 'def_eq' to 'true' *)
   1.487 +						((m', {maxvars = #maxvars a', def_eq = true, next_idx = #next_idx a', bounds = #bounds a', wellformed = #wellformed a'}), i)
   1.488  					end) ((init_model, init_args), t :: axioms)
   1.489  				(* make 't' either true or false, and make all axioms true, and *)
   1.490  				(* add the well-formedness side condition                       *)
   1.491 @@ -901,13 +978,19 @@
   1.492  				immediate_output " invoking SAT solver...";
   1.493  				(case SatSolver.invoke_solver satsolver fm of
   1.494  				  SatSolver.SATISFIABLE assignment =>
   1.495 -					writeln ("\n*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of SOME b => b | NONE => true))
   1.496 -				| _ =>  (* SatSolver.UNSATISFIABLE, SatSolver.UNKNOWN *)
   1.497 +					(writeln " model found!";
   1.498 +					writeln ("*** Model found: ***\n" ^ print_model thy model (fn i => case assignment i of SOME b => b | NONE => true)))
   1.499 +				| SatSolver.UNSATISFIABLE =>
   1.500 +					(immediate_output " no model exists.\n";
   1.501 +					case next_universe universe sizes minsize maxsize of
   1.502 +					  SOME universe' => find_model_loop universe'
   1.503 +					| NONE           => writeln "Search terminated, no larger universe within the given limits.")
   1.504 +				| SatSolver.UNKNOWN =>
   1.505  					(immediate_output " no model found.\n";
   1.506  					case next_universe universe sizes minsize maxsize of
   1.507  					  SOME universe' => find_model_loop universe'
   1.508 -					| NONE           => writeln "Search terminated, no larger universe within the given limits."))
   1.509 -				handle SatSolver.NOT_CONFIGURED =>
   1.510 +					| NONE           => writeln "Search terminated, no larger universe within the given limits.")
   1.511 +				) handle SatSolver.NOT_CONFIGURED =>
   1.512  					error ("SAT solver " ^ quote satsolver ^ " is not configured.")
   1.513  			end handle MAXVARS_EXCEEDED =>
   1.514  				writeln ("\nSearch terminated, number of Boolean variables (" ^ string_of_int maxvars ^ " allowed) exceeded.")
   1.515 @@ -921,17 +1004,17 @@
   1.516  			assert (maxsize>=minsize) ("\"maxsize\" (=" ^ string_of_int maxsize ^ ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ").");
   1.517  			assert (maxvars>=0) ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0");
   1.518  			assert (maxtime>=0) ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
   1.519 -			(* enter loop with/without time limit *)
   1.520 +			(* enter loop with or without time limit *)
   1.521  			writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": "
   1.522  				^ Sign.string_of_term (sign_of thy) t);
   1.523 -			if maxtime>0 then
   1.524 -				(TimeLimit.timeLimit (Time.fromSeconds (Int.toLarge maxtime))
   1.525 +			if maxtime>0 then (
   1.526 +				TimeLimit.timeLimit (Time.fromSeconds (Int.toLarge maxtime))
   1.527  					wrapper ()
   1.528  				handle TimeLimit.TimeOut =>
   1.529  					writeln ("\nSearch terminated, time limit ("
   1.530  						^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds")
   1.531 -						^ ") exceeded."))
   1.532 -			else
   1.533 +						^ ") exceeded.")
   1.534 +			) else
   1.535  				wrapper ()
   1.536  		end;
   1.537  
   1.538 @@ -1054,7 +1137,7 @@
   1.539  		(* int * int -> int *)
   1.540  		fun power (a,0) = 1
   1.541  		  | power (a,1) = a
   1.542 -		  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end
   1.543 +		  | power (a,b) = let val ab = power(a, b div 2) in ab * ab * power(a, b mod 2) end
   1.544  	in
   1.545  		case intr of
   1.546  		  Leaf xs => length xs
   1.547 @@ -1074,6 +1157,12 @@
   1.548  (* ------------------------------------------------------------------------- *)
   1.549  (* make_equality: returns an interpretation that denotes (extensional)       *)
   1.550  (*                equality of two interpretations                            *)
   1.551 +(* - two interpretations are 'equal' iff they are both defined and denote    *)
   1.552 +(*   the same value                                                          *)
   1.553 +(* - two interpretations are 'not_equal' iff they are both defined at least  *)
   1.554 +(*   partially, and a defined part denotes different values                  *)
   1.555 +(* - a completely undefined interpretation is neither 'equal' nor            *)
   1.556 +(*   'not_equal' to another interpretation                                   *)
   1.557  (* ------------------------------------------------------------------------- *)
   1.558  
   1.559  	(* We could in principle represent '=' on a type T by a particular        *)
   1.560 @@ -1092,7 +1181,7 @@
   1.561  			(case i1 of
   1.562  			  Leaf xs =>
   1.563  				(case i2 of
   1.564 -				  Leaf ys => PropLogic.dot_product (xs, ys)
   1.565 +				  Leaf ys => PropLogic.dot_product (xs, ys)  (* defined and equal *)
   1.566  				| Node _  => raise REFUTE ("make_equality", "second interpretation is higher"))
   1.567  			| Node xs =>
   1.568  				(case i2 of
   1.569 @@ -1112,17 +1201,92 @@
   1.570  				| Node ys => PropLogic.exists (map not_equal (xs ~~ ys))))
   1.571  	in
   1.572  		(* a value may be undefined; therefore 'not_equal' is not just the     *)
   1.573 -		(* negation of 'equal':                                                *)
   1.574 -		(* - two interpretations are 'equal' iff they are both defined and     *)
   1.575 -		(*   denote the same value                                             *)
   1.576 -		(* - two interpretations are 'not_equal' iff they are both defined at  *)
   1.577 -		(*   least partially, and a defined part denotes different values      *)
   1.578 -		(* - an undefined interpretation is neither 'equal' nor 'not_equal' to *)
   1.579 -		(*   another value                                                     *)
   1.580 +		(* negation of 'equal'                                                 *)
   1.581  		Leaf [equal (i1, i2), not_equal (i1, i2)]
   1.582  	end;
   1.583  
   1.584  (* ------------------------------------------------------------------------- *)
   1.585 +(* make_def_equality: returns an interpretation that denotes (extensional)   *)
   1.586 +(*                    equality of two interpretations                        *)
   1.587 +(* This function treats undefined/partially defined interpretations          *)
   1.588 +(* different from 'make_equality': two undefined interpretations are         *)
   1.589 +(* considered equal, while a defined interpretation is considered not equal  *)
   1.590 +(* to an undefined interpretation.                                           *)
   1.591 +(* ------------------------------------------------------------------------- *)
   1.592 +
   1.593 +	(* interpretation * interpretation -> interpretation *)
   1.594 +
   1.595 +	fun make_def_equality (i1, i2) =
   1.596 +	let
   1.597 +		(* interpretation * interpretation -> prop_formula *)
   1.598 +		fun equal (i1, i2) =
   1.599 +			(case i1 of
   1.600 +			  Leaf xs =>
   1.601 +				(case i2 of
   1.602 +				  Leaf ys => SOr (PropLogic.dot_product (xs, ys),  (* defined and equal, or both undefined *)
   1.603 +					SAnd (PropLogic.all (map SNot xs), PropLogic.all (map SNot ys)))
   1.604 +				| Node _  => raise REFUTE ("make_def_equality", "second interpretation is higher"))
   1.605 +			| Node xs =>
   1.606 +				(case i2 of
   1.607 +				  Leaf _  => raise REFUTE ("make_def_equality", "first interpretation is higher")
   1.608 +				| Node ys => PropLogic.all (map equal (xs ~~ ys))))
   1.609 +		(* interpretation *)
   1.610 +		val eq = equal (i1, i2)
   1.611 +	in
   1.612 +		Leaf [eq, SNot eq]
   1.613 +	end;
   1.614 +
   1.615 +(* ------------------------------------------------------------------------- *)
   1.616 +(* interpretation_apply: returns an interpretation that denotes the result   *)
   1.617 +(*                       of applying the function denoted by 'i2' to the     *)
   1.618 +(*                       argument denoted by 'i2'                            *)
   1.619 +(* ------------------------------------------------------------------------- *)
   1.620 +
   1.621 +	(* interpretation * interpretation -> interpretation *)
   1.622 +
   1.623 +	fun interpretation_apply (i1, i2) =
   1.624 +	let
   1.625 +		(* interpretation * interpretation -> interpretation *)
   1.626 +		fun interpretation_disjunction (tr1,tr2) =
   1.627 +			tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
   1.628 +		(* prop_formula * interpretation -> interpretation *)
   1.629 +		fun prop_formula_times_interpretation (fm,tr) =
   1.630 +			tree_map (map (fn x => SAnd (fm,x))) tr
   1.631 +		(* prop_formula list * interpretation list -> interpretation *)
   1.632 +		fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
   1.633 +			prop_formula_times_interpretation (fm,tr)
   1.634 +		  | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
   1.635 +			interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees))
   1.636 +		  | prop_formula_list_dot_product_interpretation_list (_,_) =
   1.637 +			raise REFUTE ("interpretation_apply", "empty list (in dot product)")
   1.638 +		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
   1.639 +		(* 'a -> 'a list list -> 'a list list *)
   1.640 +		fun cons_list x xss =
   1.641 +			map (fn xs => x::xs) xss
   1.642 +		(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
   1.643 +		(* 'a list list -> 'a list list *)
   1.644 +		fun pick_all [xs] =
   1.645 +			map (fn x => [x]) xs
   1.646 +		  | pick_all (xs::xss) =
   1.647 +			let val rec_pick = pick_all xss in
   1.648 +				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   1.649 +			end
   1.650 +		  | pick_all _ =
   1.651 +			raise REFUTE ("interpretation_apply", "empty list (in pick_all)")
   1.652 +		(* interpretation -> prop_formula list *)
   1.653 +		fun interpretation_to_prop_formula_list (Leaf xs) =
   1.654 +			xs
   1.655 +		  | interpretation_to_prop_formula_list (Node trees) =
   1.656 +			map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees))
   1.657 +	in
   1.658 +		case i1 of
   1.659 +		  Leaf _ =>
   1.660 +			raise REFUTE ("interpretation_apply", "first interpretation is a leaf")
   1.661 +		| Node xs =>
   1.662 +			prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list i2, xs)
   1.663 +	end;
   1.664 +
   1.665 +(* ------------------------------------------------------------------------- *)
   1.666  (* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions      *)
   1.667  (* ------------------------------------------------------------------------- *)
   1.668  
   1.669 @@ -1153,9 +1317,9 @@
   1.670  	fun product xs = foldl op* (1, xs);
   1.671  
   1.672  (* ------------------------------------------------------------------------- *)
   1.673 -(* size_of_dtyp: the size of (an initial fragment of) a data type is the sum *)
   1.674 -(*               (over its constructors) of the product (over their          *)
   1.675 -(*               arguments) of the size of the argument types                *)
   1.676 +(* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
   1.677 +(*               is the sum (over its constructors) of the product (over     *)
   1.678 +(*               their arguments) of the size of the argument types          *)
   1.679  (* ------------------------------------------------------------------------- *)
   1.680  
   1.681  	(* theory -> (Term.typ * int) list -> DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> (string * DatatypeAux.dtyp list) list -> int *)
   1.682 @@ -1165,7 +1329,7 @@
   1.683  			product (map (fn dtyp =>
   1.684  				let
   1.685  					val T         = typ_of_dtyp descr typ_assoc dtyp
   1.686 -					val (i, _, _) = interpret thy (typ_sizes, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.687 +					val (i, _, _) = interpret thy (typ_sizes, []) {maxvars=0, def_eq = false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.688  				in
   1.689  					size_of_type i
   1.690  				end) dtyps)) constructors);
   1.691 @@ -1182,32 +1346,29 @@
   1.692  
   1.693  	fun stlc_interpreter thy model args t =
   1.694  	let
   1.695 -		val (typs, terms)                           = model
   1.696 -		val {maxvars, next_idx, bounds, wellformed} = args
   1.697 +		val (typs, terms)                                   = model
   1.698 +		val {maxvars, def_eq, next_idx, bounds, wellformed} = args
   1.699  		(* Term.typ -> (interpretation * model * arguments) option *)
   1.700  		fun interpret_groundterm T =
   1.701  		let
   1.702  			(* unit -> (interpretation * model * arguments) option *)
   1.703  			fun interpret_groundtype () =
   1.704  			let
   1.705 -				val size = (if T = Term.propT then 2 else (the o assoc) (typs, T))                      (* the model MUST specify a size for ground types *)
   1.706 -				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 *)
   1.707 -				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())    (* check if 'maxvars' is large enough *)
   1.708 +				val size = (if T = Term.propT then 2 else (the o assoc) (typs, T))                    (* the model MUST specify a size for ground types *)
   1.709 +				val next = next_idx+size
   1.710 +				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
   1.711  				(* prop_formula list *)
   1.712 -				val fms  = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
   1.713 -					else (map BoolVar (next_idx upto (next_idx+size-1))))
   1.714 +				val fms  = map BoolVar (next_idx upto (next_idx+size-1))
   1.715  				(* interpretation *)
   1.716  				val intr = Leaf fms
   1.717  				(* prop_formula list -> prop_formula *)
   1.718  				fun one_of_two_false []      = True
   1.719  				  | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs)
   1.720 -				(* prop_formula list -> prop_formula *)
   1.721 -				fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
   1.722  				(* prop_formula *)
   1.723 -				val wf   = (if size=1 then True else if size=2 then True else exactly_one_true fms)
   1.724 +				val wf   = one_of_two_false fms
   1.725  			in
   1.726  				(* extend the model, increase 'next_idx', add well-formedness condition *)
   1.727 -				SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
   1.728 +				SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, def_eq = def_eq, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
   1.729  			end
   1.730  		in
   1.731  			case T of
   1.732 @@ -1216,7 +1377,7 @@
   1.733  					(* we create 'size_of_type (interpret (... T1))' different copies *)
   1.734  					(* of the interpretation for 'T2', which are then combined into a *)
   1.735  					(* single new interpretation                                      *)
   1.736 -					val (i1, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
   1.737 +					val (i1, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
   1.738  					(* make fresh copies, with different variable indices *)
   1.739  					(* 'idx': next variable index                         *)
   1.740  					(* 'n'  : number of copies                            *)
   1.741 @@ -1225,7 +1386,7 @@
   1.742  						(idx, [], True)
   1.743  					  | make_copies idx n =
   1.744  						let
   1.745 -							val (copy, _, new_args) = interpret thy (typs, []) {maxvars = maxvars, next_idx = idx, bounds = [], wellformed = True} (Free ("dummy", T2))
   1.746 +							val (copy, _, new_args) = interpret thy (typs, []) {maxvars = maxvars, def_eq = false, next_idx = idx, bounds = [], wellformed = True} (Free ("dummy", T2))
   1.747  							val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1)
   1.748  						in
   1.749  							(idx', copy :: copies, SAnd (#wellformed new_args, wf'))
   1.750 @@ -1235,7 +1396,7 @@
   1.751  					val intr = Node copies
   1.752  				in
   1.753  					(* extend the model, increase 'next_idx', add well-formedness condition *)
   1.754 -					SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
   1.755 +					SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, def_eq = def_eq, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
   1.756  				end
   1.757  			| Type _  => interpret_groundtype ()
   1.758  			| TFree _ => interpret_groundtype ()
   1.759 @@ -1259,17 +1420,17 @@
   1.760  			| Abs (x, T, body) =>
   1.761  				let
   1.762  					(* create all constants of type 'T' *)
   1.763 -					val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.764 +					val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
   1.765  					val constants = make_constants i
   1.766  					(* interpret the 'body' separately for each constant *)
   1.767  					val ((model', args'), bodies) = foldl_map
   1.768 -						(fn ((m,a), c) =>
   1.769 +						(fn ((m, a), c) =>
   1.770  							let
   1.771  								(* add 'c' to 'bounds' *)
   1.772 -								val (i', m', a') = interpret thy m {maxvars = #maxvars a, next_idx = #next_idx a, bounds = (c :: #bounds a), wellformed = #wellformed a} body
   1.773 +								val (i', m', a') = interpret thy m {maxvars = #maxvars a, def_eq = #def_eq a, next_idx = #next_idx a, bounds = (c :: #bounds a), wellformed = #wellformed a} body
   1.774  							in
   1.775  								(* keep the new model m' and 'next_idx' and 'wellformed', but use old 'bounds' *)
   1.776 -								((m', {maxvars = maxvars, next_idx = #next_idx a', bounds = bounds, wellformed = #wellformed a'}), i')
   1.777 +								((m', {maxvars = maxvars, def_eq = def_eq, next_idx = #next_idx a', bounds = bounds, wellformed = #wellformed a'}), i')
   1.778  							end)
   1.779  						((model, args), constants)
   1.780  				in
   1.781 @@ -1277,51 +1438,11 @@
   1.782  				end
   1.783  			| t1 $ t2          =>
   1.784  				let
   1.785 -					(* auxiliary functions *)
   1.786 -					(* interpretation * interpretation -> interpretation *)
   1.787 -					fun interpretation_disjunction (tr1,tr2) =
   1.788 -						tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
   1.789 -					(* prop_formula * interpretation -> interpretation *)
   1.790 -					fun prop_formula_times_interpretation (fm,tr) =
   1.791 -						tree_map (map (fn x => SAnd (fm,x))) tr
   1.792 -					(* prop_formula list * interpretation list -> interpretation *)
   1.793 -					fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
   1.794 -						prop_formula_times_interpretation (fm,tr)
   1.795 -					  | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
   1.796 -						interpretation_disjunction (prop_formula_times_interpretation (fm,tr), prop_formula_list_dot_product_interpretation_list (fms,trees))
   1.797 -					  | prop_formula_list_dot_product_interpretation_list (_,_) =
   1.798 -						raise REFUTE ("stlc_interpreter", "empty list (in dot product)")
   1.799 -					(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
   1.800 -					(* 'a -> 'a list list -> 'a list list *)
   1.801 -					fun cons_list x xss =
   1.802 -						map (fn xs => x::xs) xss
   1.803 -					(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
   1.804 -					(* 'a list list -> 'a list list *)
   1.805 -					fun pick_all [xs] =
   1.806 -						map (fn x => [x]) xs
   1.807 -					  | pick_all (xs::xss) =
   1.808 -						let val rec_pick = pick_all xss in
   1.809 -							foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   1.810 -						end
   1.811 -					  | pick_all _ =
   1.812 -						raise REFUTE ("stlc_interpreter", "empty list (in pick_all)")
   1.813 -					(* interpretation -> prop_formula list *)
   1.814 -					fun interpretation_to_prop_formula_list (Leaf xs) =
   1.815 -						xs
   1.816 -					  | interpretation_to_prop_formula_list (Node trees) =
   1.817 -						map PropLogic.all (pick_all (map interpretation_to_prop_formula_list trees))
   1.818 -					(* interpretation * interpretation -> interpretation *)
   1.819 -					fun interpretation_apply (tr1,tr2) =
   1.820 -						(case tr1 of
   1.821 -						  Leaf _ =>
   1.822 -							raise REFUTE ("stlc_interpreter", "first interpretation is a leaf")
   1.823 -						| Node xs =>
   1.824 -							prop_formula_list_dot_product_interpretation_list (interpretation_to_prop_formula_list tr2, xs))
   1.825  					(* interpret 't1' and 't2' separately *)
   1.826  					val (intr1, model1, args1) = interpret thy model args t1
   1.827  					val (intr2, model2, args2) = interpret thy model1 args1 t2
   1.828  				in
   1.829 -					SOME (interpretation_apply (intr1,intr2), model2, args2)
   1.830 +					SOME (interpretation_apply (intr1, intr2), model2, args2)
   1.831  				end)
   1.832  	end;
   1.833  
   1.834 @@ -1349,7 +1470,8 @@
   1.835  				val (i1, m1, a1) = interpret thy model args t1
   1.836  				val (i2, m2, a2) = interpret thy m1 a1 t2
   1.837  			in
   1.838 -				SOME (make_equality (i1, i2), m2, a2)
   1.839 +				(* we use either 'make_def_equality' or 'make_equality' *)
   1.840 +				SOME ((if #def_eq args then make_def_equality else make_equality) (i1, i2), m2, a2)
   1.841  			end
   1.842  		| Const ("==>", _) =>  (* simpler than translating 'Const ("==>", _) $ t1 $ t2' *)
   1.843  			SOME (Node [Node [TT, FF], Node [TT, TT]], model, args)
   1.844 @@ -1375,7 +1497,7 @@
   1.845  			SOME (FF, model, args)
   1.846  		| Const ("All", _) $ t1 =>
   1.847  		(* if "All" occurs without an argument (i.e. as argument to a higher-order *)
   1.848 -		(* function or  predicate), it is handled by the 'stlc_interpreter' (i.e.  *)
   1.849 +		(* function or predicate), it is handled by the 'stlc_interpreter' (i.e.   *)
   1.850  		(* by unfolding its definition)                                            *)
   1.851  			let
   1.852  				val (i, m, a) = interpret thy model args t1
   1.853 @@ -1393,7 +1515,7 @@
   1.854  			end
   1.855  		| Const ("Ex", _) $ t1 =>
   1.856  		(* if "Ex" occurs without an argument (i.e. as argument to a higher-order  *)
   1.857 -		(* function or  predicate), it is handled by the 'stlc_interpreter' (i.e.  *)
   1.858 +		(* function or predicate), it is handled by the 'stlc_interpreter' (i.e.   *)
   1.859  		(* by unfolding its definition)                                            *)
   1.860  			let
   1.861  				val (i, m, a) = interpret thy model args t1
   1.862 @@ -1420,12 +1542,49 @@
   1.863  			SOME (interpret thy model args (eta_expand t 1))
   1.864  		| Const ("op =", _) =>
   1.865  			SOME (interpret thy model args (eta_expand t 2))
   1.866 +		| Const ("op &", _) $ t1 $ t2 =>
   1.867 +			(* 3-valued logic *)
   1.868 +			let
   1.869 +				val (i1, m1, a1) = interpret thy model args t1
   1.870 +				val (i2, m2, a2) = interpret thy m1 a1 t2
   1.871 +				val fmTrue       = PropLogic.SAnd (toTrue i1, toTrue i2)
   1.872 +				val fmFalse      = PropLogic.SOr (toFalse i1, toFalse i2)
   1.873 +			in
   1.874 +				SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.875 +			end
   1.876 +		| Const ("op &", _) $ t1 =>
   1.877 +			SOME (interpret thy model args (eta_expand t 1))
   1.878  		| Const ("op &", _) =>
   1.879 -			SOME (Node [Node [TT, FF], Node [FF, FF]], model, args)
   1.880 +			SOME (interpret thy model args (eta_expand t 2))
   1.881 +			(* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)
   1.882 +		| Const ("op |", _) $ t1 $ t2 =>
   1.883 +			(* 3-valued logic *)
   1.884 +			let
   1.885 +				val (i1, m1, a1) = interpret thy model args t1
   1.886 +				val (i2, m2, a2) = interpret thy m1 a1 t2
   1.887 +				val fmTrue       = PropLogic.SOr (toTrue i1, toTrue i2)
   1.888 +				val fmFalse      = PropLogic.SAnd (toFalse i1, toFalse i2)
   1.889 +			in
   1.890 +				SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.891 +			end
   1.892 +		| Const ("op |", _) $ t1 =>
   1.893 +			SOME (interpret thy model args (eta_expand t 1))
   1.894  		| Const ("op |", _) =>
   1.895 -			SOME (Node [Node [TT, TT], Node [TT, FF]], model, args)
   1.896 +			SOME (interpret thy model args (eta_expand t 2))
   1.897 +			(* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
   1.898 +		| Const ("op -->", _) $ t1 $ t2 =>
   1.899 +			(* 3-valued logic *)
   1.900 +			let
   1.901 +				val (i1, m1, a1) = interpret thy model args t1
   1.902 +				val (i2, m2, a2) = interpret thy m1 a1 t2
   1.903 +				val fmTrue       = PropLogic.SOr (toFalse i1, toTrue i2)
   1.904 +				val fmFalse      = PropLogic.SAnd (toTrue i1, toFalse i2)
   1.905 +			in
   1.906 +				SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.907 +			end
   1.908  		| Const ("op -->", _) =>
   1.909 -			SOME (Node [Node [TT, FF], Node [TT, TT]], model, args)
   1.910 +			(* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *)
   1.911 +			SOME (interpret thy model args (eta_expand t 2))
   1.912  		| _ => NONE;
   1.913  
   1.914  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.915 @@ -1476,17 +1635,19 @@
   1.916  
   1.917  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.918  
   1.919 +	(* interprets variables and constants whose type is an IDT; constructors of  *)
   1.920 +	(* IDTs are properly interpreted by 'IDT_constructor_interpreter' however    *)
   1.921 +
   1.922  	fun IDT_interpreter thy model args t =
   1.923  	let
   1.924  		val (typs, terms) = model
   1.925  		(* Term.typ -> (interpretation * model * arguments) option *)
   1.926 -		fun interpret_variable (Type (s, Ts)) =
   1.927 +		fun interpret_term (Type (s, Ts)) =
   1.928  			(case DatatypePackage.datatype_info thy s of
   1.929  			  SOME info =>  (* inductive datatype *)
   1.930  				let
   1.931 -					val (typs, terms) = model
   1.932  					(* int option -- only recursive IDTs have an associated depth *)
   1.933 -					val depth         = assoc (typs, Type (s, Ts))
   1.934 +					val depth = assoc (typs, Type (s, Ts))
   1.935  				in
   1.936  					if depth = (SOME 0) then  (* termination condition to avoid infinite recursion *)
   1.937  						(* return a leaf of size 0 *)
   1.938 @@ -1509,28 +1670,25 @@
   1.939  							(* recursively compute the size of the datatype *)
   1.940  							val size     = size_of_dtyp thy typs' descr typ_assoc constrs
   1.941  							val next_idx = #next_idx args
   1.942 -							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 *)
   1.943 +							val next     = next_idx+size
   1.944  							val _        = (if next-1>(#maxvars args) andalso (#maxvars args)>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
   1.945  							(* prop_formula list *)
   1.946 -							val fms      = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
   1.947 -								else (map BoolVar (next_idx upto (next_idx+size-1))))
   1.948 +							val fms      = map BoolVar (next_idx upto (next_idx+size-1))
   1.949  							(* interpretation *)
   1.950  							val intr     = Leaf fms
   1.951  							(* prop_formula list -> prop_formula *)
   1.952  							fun one_of_two_false []      = True
   1.953  							  | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), one_of_two_false xs)
   1.954 -							(* prop_formula list -> prop_formula *)
   1.955 -							fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
   1.956  							(* prop_formula *)
   1.957 -							val wf       = (if size=1 then True else if size=2 then True else exactly_one_true fms)
   1.958 +							val wf       = one_of_two_false fms
   1.959  						in
   1.960  							(* extend the model, increase 'next_idx', add well-formedness condition *)
   1.961 -							SOME (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)})
   1.962 +							SOME (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, def_eq = #def_eq args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)})
   1.963  						end
   1.964  				end
   1.965  			| NONE =>  (* not an inductive datatype *)
   1.966  				NONE)
   1.967 -		  | interpret_variable _ =  (* a (free or schematic) type variable *)
   1.968 +		  | interpret_term _ =  (* a (free or schematic) type variable *)
   1.969  			NONE
   1.970  	in
   1.971  		case assoc (terms, t) of
   1.972 @@ -1539,120 +1697,352 @@
   1.973  			SOME (intr, model, args)
   1.974  		| NONE =>
   1.975  			(case t of
   1.976 -			  Free (_, T)  => interpret_variable T
   1.977 -			| Var (_, T)   => interpret_variable T
   1.978 -			| Const (s, T) =>
   1.979 -				(* TODO: case, recursion, size *)
   1.980 -				let
   1.981 -					(* unit -> (interpretation * model * arguments) option *)
   1.982 -					fun interpret_constructor () =
   1.983 -						(case body_type T of
   1.984 -						  Type (s', Ts') =>
   1.985 -							(case DatatypePackage.datatype_info thy s' of
   1.986 -							  SOME info =>  (* body type is an inductive datatype *)
   1.987 +			  Free (_, T)  => interpret_term T
   1.988 +			| Var (_, T)   => interpret_term T
   1.989 +			| Const (_, T) => interpret_term T
   1.990 +			| _            => NONE)
   1.991 +	end;
   1.992 +
   1.993 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.994 +
   1.995 +	fun IDT_constructor_interpreter thy model args t =
   1.996 +	let
   1.997 +		val (typs, terms) = model
   1.998 +	in
   1.999 +		case assoc (terms, t) of
  1.1000 +		  SOME intr =>
  1.1001 +			(* return an existing interpretation *)
  1.1002 +			SOME (intr, model, args)
  1.1003 +		| NONE =>
  1.1004 +			(case t of
  1.1005 +			  Const (s, T) =>
  1.1006 +				(case body_type T of
  1.1007 +				  Type (s', Ts') =>
  1.1008 +					(case DatatypePackage.datatype_info thy s' of
  1.1009 +					  SOME info =>  (* body type is an inductive datatype *)
  1.1010 +						let
  1.1011 +							val index               = #index info
  1.1012 +							val descr               = #descr info
  1.1013 +							val (_, dtyps, constrs) = (the o assoc) (descr, index)
  1.1014 +							val typ_assoc           = dtyps ~~ Ts'
  1.1015 +							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1.1016 +							val _ = (if Library.exists (fn d =>
  1.1017 +									case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
  1.1018 +								then
  1.1019 +									raise REFUTE ("IDT_constructor_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s', Ts')) ^ ") is not a variable")
  1.1020 +								else
  1.1021 +									())
  1.1022 +							(* split the constructors into those occuring before/after 'Const (s, T)' *)
  1.1023 +							val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
  1.1024 +								not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T,
  1.1025 +									map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs
  1.1026 +						in
  1.1027 +							case constrs2 of
  1.1028 +							  [] =>
  1.1029 +								(* 'Const (s, T)' is not a constructor of this datatype *)
  1.1030 +								NONE
  1.1031 +							| (_, ctypes)::cs =>
  1.1032  								let
  1.1033 -									val index               = #index info
  1.1034 -									val descr               = #descr info
  1.1035 -									val (_, dtyps, constrs) = (the o assoc) (descr, index)
  1.1036 -									val typ_assoc           = dtyps ~~ Ts'
  1.1037 -									(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1.1038 -									val _ = (if Library.exists (fn d =>
  1.1039 -											case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
  1.1040 -										then
  1.1041 -											raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s', Ts')) ^ ") is not a variable")
  1.1042 +									(* compute the total size of the datatype (with the current depth) *)
  1.1043 +									val (i, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type (s', Ts')))
  1.1044 +									val total     = size_of_type i
  1.1045 +									(* int option -- only recursive IDTs have an associated depth *)
  1.1046 +									val depth = assoc (typs, Type (s', Ts'))
  1.1047 +									val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s', Ts'), n-1)))
  1.1048 +									(* DatatypeAux.dtyp list -> interpretation *)
  1.1049 +									fun make_undef [] =
  1.1050 +										Leaf (replicate total False)
  1.1051 +									  | make_undef (d::ds) =
  1.1052 +										let
  1.1053 +											(* compute the current size of the type 'd' *)
  1.1054 +											val T           = typ_of_dtyp descr typ_assoc d
  1.1055 +											val (i, _, _)   = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1.1056 +											val size        = size_of_type i
  1.1057 +										in
  1.1058 +											Node (replicate size (make_undef ds))
  1.1059 +										end
  1.1060 +									(* returns the interpretation for a constructor at depth 1 *)
  1.1061 +									(* int * DatatypeAux.dtyp list -> int * interpretation *)
  1.1062 +									fun make_constr (offset, []) =
  1.1063 +										if offset<total then
  1.1064 +											(offset+1, Leaf ((replicate offset False) @ True :: (replicate (total-offset-1) False)))
  1.1065  										else
  1.1066 -											())
  1.1067 -									(* split the constructors into those occuring before/after 'Const (s, T)' *)
  1.1068 -									val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
  1.1069 -										not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T,
  1.1070 -											map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs
  1.1071 -								in
  1.1072 -									case constrs2 of
  1.1073 -									  [] =>
  1.1074 -										(* 'Const (s, T)' is not a constructor of this datatype *)
  1.1075 -										NONE
  1.1076 -									| c::cs =>
  1.1077 +											raise REFUTE ("IDT_constructor_interpreter", "offset >= total")
  1.1078 +									  | make_constr (offset, d::ds) =
  1.1079  										let
  1.1080 -											(* int option -- only recursive IDTs have an associated depth *)
  1.1081 -											val depth = assoc (typs, Type (s', Ts'))
  1.1082 -											val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s', Ts'), n-1)))
  1.1083 -											(* constructors before 'Const (s, T)' generate elements of the datatype *)
  1.1084 -											val offset  = size_of_dtyp thy typs' descr typ_assoc constrs1
  1.1085 -											(* 'Const (s, T)' and constructors after it generate elements of the datatype *)
  1.1086 -											val total   = offset + (size_of_dtyp thy typs' descr typ_assoc constrs2)
  1.1087 -											(* create an interpretation that corresponds to the constructor 'Const (s, T)' *)
  1.1088 -											(* by recursion over its argument types                                        *)
  1.1089 -											(* DatatypeAux.dtyp list -> interpretation *)
  1.1090 -											fun make_partial [] =
  1.1091 -												(* all entries of the leaf are 'False' *)
  1.1092 -												Leaf (replicate total False)
  1.1093 -											  | make_partial (d::ds) =
  1.1094 -												let
  1.1095 -													(* compute the "new" size of the type 'd' *)
  1.1096 -													val T         = typ_of_dtyp descr typ_assoc d
  1.1097 -													val (i, _, _) = interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1.1098 -												in
  1.1099 -													(* all entries of the whole subtree are 'False' *)
  1.1100 -													Node (replicate (size_of_type i) (make_partial ds))
  1.1101 -												end
  1.1102 -											(* int * DatatypeAux.dtyp list -> int * interpretation *)
  1.1103 -											fun make_constr (offset, []) =
  1.1104 -												if offset<total then
  1.1105 -													(offset+1, Leaf ((replicate offset False) @ True :: (replicate (total-offset-1) False)))
  1.1106 +											(* compute the current and the old size of the type 'd' *)
  1.1107 +											val T           = typ_of_dtyp descr typ_assoc d
  1.1108 +											val (i, _, _)   = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1.1109 +											val size        = size_of_type i
  1.1110 +											val (i', _, _)  = interpret thy (typs', []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1.1111 +											val size'       = size_of_type i'
  1.1112 +											(* sanity check *)
  1.1113 +											val _           = if size < size' then
  1.1114 +													raise REFUTE ("IDT_constructor_interpreter", "current size is less than old size")
  1.1115  												else
  1.1116 -													raise REFUTE ("IDT_interpreter", "internal error: offset >= total")
  1.1117 -											  | make_constr (offset, d::ds) =
  1.1118 -												let
  1.1119 -													(* compute the "new" and "old" size of the type 'd' *)
  1.1120 -													val T          = typ_of_dtyp descr typ_assoc d
  1.1121 -													val (i, _, _)  = interpret thy (typs, []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1.1122 -													val (i', _, _) = interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1.1123 -													val size       = size_of_type i
  1.1124 -													val size'      = size_of_type i'
  1.1125 -													val _ = if size<size' then
  1.1126 -															raise REFUTE ("IDT_interpreter", "internal error: new size < old size")
  1.1127 -														else
  1.1128 -															()
  1.1129 -													val (new_offset, intrs) = foldl_map make_constr (offset, replicate size' ds)
  1.1130 -												in
  1.1131 -													(* the first size' elements of the type actually yield a result *)
  1.1132 -													(* element, while the remaining size-size' elements don't       *)
  1.1133 -													(new_offset, Node (intrs @ (replicate (size-size') (make_partial ds))))
  1.1134 -												end
  1.1135 +													()
  1.1136 +											(* elements that exist at the previous depth are mapped to a defined *)
  1.1137 +											(* value, while new elements are mapped to "undefined" by the        *)
  1.1138 +											(* recursive constructor                                             *)
  1.1139 +											(* int * interpretation list *)
  1.1140 +											val (new_offset, intrs) = foldl_map make_constr (offset, replicate size' ds)
  1.1141 +											(* interpretation list *)
  1.1142 +											val undefs              = replicate (size - size') (make_undef ds)
  1.1143 +										in
  1.1144 +											(new_offset, Node (intrs @ undefs))
  1.1145 +										end
  1.1146 +									(* extends the interpretation for a constructor (both recursive *)
  1.1147 +									(* and non-recursive) obtained at depth n (n>=1) to depth n+1   *)
  1.1148 +									(* int * DatatypeAux.dtyp list * interpretation -> int * interpretation *)
  1.1149 +									fun extend_constr (offset, [], Leaf xs) =
  1.1150 +										let
  1.1151 +											(* returns the k-th unit vector of length n *)
  1.1152 +											(* int * int -> interpretation *)
  1.1153 +											fun unit_vector (k,n) =
  1.1154 +												Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1.1155 +											(* int *)
  1.1156 +											val k = find_index_eq True xs
  1.1157  										in
  1.1158 -											SOME ((snd o make_constr) (offset, snd c), model, args)
  1.1159 +											if k=(~1) then
  1.1160 +												(* if the element was mapped to "undefined" before, map it to   *)
  1.1161 +												(* the value given by 'offset' now (and extend the length of    *)
  1.1162 +												(* the leaf)                                                    *)
  1.1163 +												(offset+1, unit_vector (offset+1, total))
  1.1164 +											else
  1.1165 +												(* if the element was already mapped to a defined value, map it *)
  1.1166 +												(* to the same value again, just extend the length of the leaf, *)
  1.1167 +												(* do not increment offset                                      *)
  1.1168 +												(offset, unit_vector (k+1, total))
  1.1169 +										end
  1.1170 +									  | extend_constr (_, [], Node _) =
  1.1171 +										raise REFUTE ("IDT_constructor_interpreter", "interpretation for constructor (with no arguments left) is a node")
  1.1172 +									  | extend_constr (offset, d::ds, Node xs) =
  1.1173 +										let
  1.1174 +											(* compute the size of the type 'd' *)
  1.1175 +											val T          = typ_of_dtyp descr typ_assoc d
  1.1176 +											val (i, _, _)  = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1.1177 +											val size       = size_of_type i
  1.1178 +											(* sanity check *)
  1.1179 +											val _          = if size < length xs then
  1.1180 +													raise REFUTE ("IDT_constructor_interpreter", "new size of type is less than old size")
  1.1181 +												else
  1.1182 +													()
  1.1183 +											(* extend the existing interpretations *)
  1.1184 +											(* int * interpretation list *)
  1.1185 +											val (new_offset, intrs) = foldl_map (fn (off, i) => extend_constr (off, ds, i)) (offset, xs)
  1.1186 +											(* new elements of the type 'd' are mapped to "undefined" *)
  1.1187 +											val undefs = replicate (size - length xs) (make_undef ds)
  1.1188 +										in
  1.1189 +											(new_offset, Node (intrs @ undefs))
  1.1190 +										end
  1.1191 +									  | extend_constr (_, d::ds, Leaf _) =
  1.1192 +										raise REFUTE ("IDT_constructor_interpreter", "interpretation for constructor (with arguments left) is a leaf")
  1.1193 +									(* returns 'true' iff the constructor has a recursive argument *)
  1.1194 +									(* DatatypeAux.dtyp list -> bool *)
  1.1195 +									fun is_rec_constr ds =
  1.1196 +										Library.exists DatatypeAux.is_rec_type ds
  1.1197 +									(* constructors before 'Const (s, T)' generate elements of the datatype, *)
  1.1198 +									(* and if the constructor is recursive, then non-recursive constructors  *)
  1.1199 +									(* after it generate further elements                                    *)
  1.1200 +									val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 +
  1.1201 +										(if is_rec_constr ctypes then
  1.1202 +											size_of_dtyp thy typs' descr typ_assoc (filter (not o is_rec_constr o snd) cs)
  1.1203 +										else
  1.1204 +											0)
  1.1205 +								in
  1.1206 +									case depth of
  1.1207 +									  NONE =>  (* equivalent to a depth of 1 *)
  1.1208 +										SOME (snd (make_constr (offset, ctypes)), model, args)
  1.1209 +									| SOME 0 =>
  1.1210 +										raise REFUTE ("IDT_constructor_interpreter", "depth is 0")
  1.1211 +									| SOME 1 =>
  1.1212 +										SOME (snd (make_constr (offset, ctypes)), model, args)
  1.1213 +									| SOME n =>  (* n > 1 *)
  1.1214 +										let
  1.1215 +											(* interpret the constructor at depth-1 *)
  1.1216 +											val (iC, _, _) = interpret thy (typs', []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Const (s, T))
  1.1217 +											(* elements generated by the constructor at depth-1 must be added to 'offset' *)
  1.1218 +											(* interpretation -> int *)
  1.1219 +											fun number_of_defined_elements (Leaf xs) =
  1.1220 +												if find_index_eq True xs = (~1) then 0 else 1
  1.1221 +											  | number_of_defined_elements (Node xs) =
  1.1222 +												sum (map number_of_defined_elements xs)
  1.1223 +											(* int *)
  1.1224 +											val offset' = offset + number_of_defined_elements iC
  1.1225 +										in
  1.1226 +											SOME (snd (extend_constr (offset', ctypes, iC)), model, args)
  1.1227  										end
  1.1228  								end
  1.1229 -							| NONE =>  (* body type is not an inductive datatype *)
  1.1230 -								NONE)
  1.1231 -						| _ =>  (* body type is a (free or schematic) type variable *)
  1.1232 -							NONE)
  1.1233 -				in
  1.1234 -					case interpret_constructor () of
  1.1235 -					  SOME x => SOME x
  1.1236 -					| NONE   => interpret_variable T
  1.1237 -				end
  1.1238 -			| _ => NONE)
  1.1239 +						end
  1.1240 +					| NONE =>  (* body type is not an inductive datatype *)
  1.1241 +						NONE)
  1.1242 +				| _ =>  (* body type is a (free or schematic) type variable *)
  1.1243 +					NONE)
  1.1244 +			| _ =>  (* term is not a constant *)
  1.1245 +				NONE)
  1.1246  	end;
  1.1247  
  1.1248  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1249  
  1.1250 +	(* Difficult code ahead.  Make sure you understand the 'IDT_constructor_interpreter' *)
  1.1251 +	(* and the order in which it enumerates elements of an IDT before you try to         *)
  1.1252 +	(* understand this function.                                                         *)
  1.1253 +
  1.1254 +	fun IDT_recursion_interpreter thy model args t =
  1.1255 +		case strip_comb t of  (* careful: here we descend arbitrarily deep into 't', *)
  1.1256 +		                      (* possibly before any other interpreter for atomic    *)
  1.1257 +		                      (* terms has had a chance to look at 't'               *)
  1.1258 +		  (Const (s, T), params) =>
  1.1259 +			(* iterate over all datatypes in 'thy' *)
  1.1260 +			Symtab.foldl (fn (result, (_, info)) =>
  1.1261 +				case result of
  1.1262 +				  SOME _ =>
  1.1263 +					result  (* just keep 'result' *)
  1.1264 +				| NONE =>
  1.1265 +					if s mem (#rec_names info) then
  1.1266 +						(* okay, we do have a recursion operator of the datatype given by 'info' *)
  1.1267 +						let
  1.1268 +							val index               = #index info
  1.1269 +							val descr               = #descr info
  1.1270 +							val (_, dtyps, constrs) = (the o assoc) (descr, index)
  1.1271 +							(* the total number of constructors, including those of different    *)
  1.1272 +							(* (mutually recursive) datatypes within the same descriptor 'descr' *)
  1.1273 +							val constrs_count = sum (map (fn (_, (_, _, cs)) => length cs) descr)
  1.1274 +							val params_count  = length params
  1.1275 +						in
  1.1276 +							if constrs_count < params_count then
  1.1277 +								(* too many actual parameters; for now we'll use the *)
  1.1278 +								(* 'stlc_interpreter' to strip off one application   *)
  1.1279 +								NONE
  1.1280 +							else if constrs_count > params_count then
  1.1281 +								(* too few actual parameters; we use eta expansion            *)
  1.1282 +								(* Note that the resulting expansion of lambda abstractions   *)
  1.1283 +								(* by the 'stlc_interpreter' may be rather slow (depending on *)
  1.1284 +								(* the argument types and the size of the IDT, of course).    *)
  1.1285 +								SOME (interpret thy model args (eta_expand t (constrs_count - params_count)))
  1.1286 +							else  (* constrs_count = params_count *)
  1.1287 +								let
  1.1288 +									(* interpret each parameter separately *)
  1.1289 +									val ((model', args'), p_intrs) = foldl_map (fn ((m, a), p) =>
  1.1290 +										let
  1.1291 +											val (i, m', a') = interpret thy m a p
  1.1292 +										in
  1.1293 +											((m', a'), i)
  1.1294 +										end) ((model, args), params)
  1.1295 +									val (typs, terms) = model'
  1.1296 +									(* the type of a recursion operator: [T1, ..., Tn, IDT] ---> Tresult *)
  1.1297 +									val IDT       = nth_elem (constrs_count, binder_types T)
  1.1298 +									val typ_assoc = dtyps ~~ (snd o dest_Type) IDT
  1.1299 +									(* interpret each constructor of the datatype *)
  1.1300 +									(* TODO: we probably need to interpret every constructor in the descriptor, *)
  1.1301 +									(*       possibly for typs' instead of typs                                 *)
  1.1302 +									val c_intrs = map (#1 o interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True})
  1.1303 +										(map (fn (cname, cargs) => Const (cname, map (typ_of_dtyp descr typ_assoc) cargs ---> IDT)) constrs)
  1.1304 +									(* the recursion operator is a function that maps every element of *)
  1.1305 +									(* the inductive datatype to an element of the result type         *)
  1.1306 +									val (i, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", IDT))
  1.1307 +									val size      = size_of_type i
  1.1308 +									val INTRS     = Array.array (size, Leaf [])  (* the initial value 'Leaf []' does not matter; it will be overwritten *)
  1.1309 +									(* takes an interpretation, and if some leaf of this interpretation *)
  1.1310 +									(* is the 'elem'-th element of the datatype, the indices of the     *)
  1.1311 +									(* arguments leading to this leaf are returned                      *)
  1.1312 +									(* interpretation -> int -> int list option *)
  1.1313 +									fun get_args (Leaf xs) elem =
  1.1314 +										if find_index_eq True xs = elem then
  1.1315 +											SOME []
  1.1316 +										else
  1.1317 +											NONE
  1.1318 +									  | get_args (Node xs) elem =
  1.1319 +										let
  1.1320 +											(* interpretation * int -> int list option *)
  1.1321 +											fun search ([], _) =
  1.1322 +												NONE
  1.1323 +											  | search (x::xs, n) =
  1.1324 +												(case get_args x elem of
  1.1325 +												  SOME result => SOME (n::result)
  1.1326 +												| NONE        => search (xs, n+1))
  1.1327 +										in
  1.1328 +											search (xs, 0)
  1.1329 +										end
  1.1330 +									(* returns the index of the constructor and indices for its      *)
  1.1331 +									(* arguments that generate the 'elem'-th element of the datatype *)
  1.1332 +									(* int -> int * int list *)
  1.1333 +									fun get_cargs elem =
  1.1334 +										let
  1.1335 +											(* int * interpretation list -> int * int list *)
  1.1336 +											fun get_cargs_rec (_, []) =
  1.1337 +												raise REFUTE ("IDT_recursion_interpreter", "no matching constructor found for element " ^ string_of_int elem)
  1.1338 +											  | get_cargs_rec (n, x::xs) =
  1.1339 +												(case get_args x elem of
  1.1340 +												  SOME args => (n, args)
  1.1341 +												| NONE      => get_cargs_rec (n+1, xs))
  1.1342 +										in
  1.1343 +											get_cargs_rec (0, c_intrs)
  1.1344 +										end
  1.1345 +									(* int -> unit *)
  1.1346 +									fun compute_loop elem =
  1.1347 +										if elem=size then
  1.1348 +											()
  1.1349 +										else  (* elem < size *)
  1.1350 +											let
  1.1351 +												(* int * int list *)
  1.1352 +												val (c, args) = get_cargs elem
  1.1353 +												(* interpretation * int list -> interpretation *)
  1.1354 +												fun select_subtree (tr, []) =
  1.1355 +													tr  (* return the whole tree *)
  1.1356 +												  | select_subtree (Leaf _, _) =
  1.1357 +													raise REFUTE ("IDT_recursion_interpreter", "interpretation for parameter is a leaf; cannot select a subtree")
  1.1358 +												  | select_subtree (Node tr, x::xs) =
  1.1359 +													select_subtree (nth_elem (x, tr), xs)
  1.1360 +												(* select the correct subtree of the parameter corresponding to constructor 'c' *)
  1.1361 +												val p_intr = select_subtree (nth_elem (c, p_intrs), args)
  1.1362 +												(* find the indices of recursive arguments *)
  1.1363 +												val rec_args = map snd (filter (DatatypeAux.is_rec_type o fst) ((snd (nth_elem (c, constrs))) ~~ args))
  1.1364 +												(* apply 'p_intr' to recursively computed results *)
  1.1365 +												val rec_p_intr = foldl (fn (i, n) => interpretation_apply (i, Array.sub (INTRS, n))) (p_intr, rec_args)
  1.1366 +												(* update 'INTRS' *)
  1.1367 +												val _ = Array.update (INTRS, elem, rec_p_intr)
  1.1368 +											in
  1.1369 +												compute_loop (elem+1)
  1.1370 +											end
  1.1371 +									val _ = compute_loop 0
  1.1372 +									(* 'a Array.array -> 'a list *)
  1.1373 +									fun toList arr =
  1.1374 +										Array.foldr op:: [] arr
  1.1375 +								in
  1.1376 +									(* TODO writeln ("REC-OP: " ^ makestring (Node (toList INTRS))); *)
  1.1377 +									SOME (Node (toList INTRS), model', args')
  1.1378 +								end
  1.1379 +						end
  1.1380 +					else
  1.1381 +						NONE  (* not a recursion operator of this datatype *)
  1.1382 +				) (NONE, DatatypePackage.get_datatypes thy)
  1.1383 +		| _ =>  (* head of term is not a constant *)
  1.1384 +			NONE;
  1.1385 +
  1.1386 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1387 +
  1.1388  	(* only an optimization: 'card' could in principle be interpreted with    *)
  1.1389  	(* interpreters available already (using its definition), but the code    *)
  1.1390 -	(* below is much more efficient                                           *)
  1.1391 +	(* below is more efficient                                                *)
  1.1392  
  1.1393  	fun Finite_Set_card_interpreter thy model args t =
  1.1394  		case t of
  1.1395  		  Const ("Finite_Set.card", Type ("fun", [Type ("set", [T]), Type ("nat", [])])) =>
  1.1396  			let
  1.1397 -				val (i_nat, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
  1.1398 +				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
  1.1399  				val size_nat      = size_of_type i_nat
  1.1400 -				val (i_set, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T])))
  1.1401 +				val (i_set, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("set", [T])))
  1.1402  				val constants     = make_constants i_set
  1.1403  				(* interpretation -> int *)
  1.1404  				fun number_of_elements (Node xs) =
  1.1405  					foldl (fn (n, x) =>
  1.1406 -						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)
  1.1407 +						if x=TT then
  1.1408 +							n+1
  1.1409 +						else if x=FF then
  1.1410 +							n
  1.1411 +						else
  1.1412 +							raise REFUTE ("Finite_Set_card_interpreter", "interpretation for set type does not yield a Boolean")) (0, xs)
  1.1413  				  | number_of_elements (Leaf _) =
  1.1414  					raise REFUTE ("Finite_Set_card_interpreter", "interpretation for set type is a leaf")
  1.1415  				(* takes an interpretation for a set and returns an interpretation for a 'nat' *)
  1.1416 @@ -1672,6 +2062,106 @@
  1.1417  		| _ =>
  1.1418  			NONE;
  1.1419  
  1.1420 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1421 +
  1.1422 +	(* only an optimization: 'op <' could in principle be interpreted with    *)
  1.1423 +	(* interpreters available already (using its definition), but the code    *)
  1.1424 +	(* below is more efficient                                                *)
  1.1425 +
  1.1426 +	fun Nat_less_interpreter thy model args t =
  1.1427 +		case t of
  1.1428 +		  Const ("op <", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
  1.1429 +			let
  1.1430 +				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
  1.1431 +				val size_nat      = size_of_type i_nat
  1.1432 +				(* int -> interpretation *)
  1.1433 +				(* the 'n'-th nat is not less than the first 'n' nats, while it *)
  1.1434 +				(* is less than the remaining 'size_nat - n' nats               *)
  1.1435 +				fun less n = Node ((replicate n FF) @ (replicate (size_nat - n) TT))
  1.1436 +			in
  1.1437 +				SOME (Node (map less (1 upto size_nat)), model, args)
  1.1438 +			end
  1.1439 +		| _ =>
  1.1440 +			NONE;
  1.1441 +
  1.1442 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1443 +
  1.1444 +	(* only an optimization: 'op +' could in principle be interpreted with    *)
  1.1445 +	(* interpreters available already (using its definition), but the code    *)
  1.1446 +	(* below is more efficient                                                *)
  1.1447 +
  1.1448 +	fun Nat_plus_interpreter thy model args t =
  1.1449 +		case t of
  1.1450 +		  Const ("op +", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
  1.1451 +			let
  1.1452 +				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
  1.1453 +				val size_nat      = size_of_type i_nat
  1.1454 +				(* int -> int -> interpretation *)
  1.1455 +				fun plus m n = let
  1.1456 +						val element = (m+n)+1
  1.1457 +					in
  1.1458 +						if element > size_nat then
  1.1459 +							Leaf (replicate size_nat False)
  1.1460 +						else
  1.1461 +							Leaf ((replicate (element-1) False) @ True :: (replicate (size_nat - element) False))
  1.1462 +					end
  1.1463 +			in
  1.1464 +				SOME (Node (map (fn m => Node (map (plus m) (0 upto size_nat-1))) (0 upto size_nat-1)), model, args)
  1.1465 +			end
  1.1466 +		| _ =>
  1.1467 +			NONE;
  1.1468 +
  1.1469 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1470 +
  1.1471 +	(* only an optimization: 'op -' could in principle be interpreted with    *)
  1.1472 +	(* interpreters available already (using its definition), but the code    *)
  1.1473 +	(* below is more efficient                                                *)
  1.1474 +
  1.1475 +	fun Nat_minus_interpreter thy model args t =
  1.1476 +		case t of
  1.1477 +		  Const ("op -", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
  1.1478 +			let
  1.1479 +				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
  1.1480 +				val size_nat      = size_of_type i_nat
  1.1481 +				(* int -> int -> interpretation *)
  1.1482 +				fun minus m n = let
  1.1483 +						val element = Int.max (m-n, 0) + 1
  1.1484 +					in
  1.1485 +						Leaf ((replicate (element-1) False) @ True :: (replicate (size_nat - element) False))
  1.1486 +					end
  1.1487 +			in
  1.1488 +				SOME (Node (map (fn m => Node (map (minus m) (0 upto size_nat-1))) (0 upto size_nat-1)), model, args)
  1.1489 +			end
  1.1490 +		| _ =>
  1.1491 +			NONE;
  1.1492 +
  1.1493 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
  1.1494 +
  1.1495 +	(* only an optimization: 'op *' could in principle be interpreted with    *)
  1.1496 +	(* interpreters available already (using its definition), but the code    *)
  1.1497 +	(* below is more efficient                                                *)
  1.1498 +
  1.1499 +	fun Nat_mult_interpreter thy model args t =
  1.1500 +		case t of
  1.1501 +		  Const ("op *", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
  1.1502 +			let
  1.1503 +				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
  1.1504 +				val size_nat      = size_of_type i_nat
  1.1505 +				(* nat -> nat -> interpretation *)
  1.1506 +				fun mult m n = let
  1.1507 +						val element = (m*n)+1
  1.1508 +					in
  1.1509 +						if element > size_nat then
  1.1510 +							Leaf (replicate size_nat False)
  1.1511 +						else
  1.1512 +							Leaf ((replicate (element-1) False) @ True :: (replicate (size_nat - element) False))
  1.1513 +					end
  1.1514 +			in
  1.1515 +				SOME (Node (map (fn m => Node (map (mult m) (0 upto size_nat-1))) (0 upto size_nat-1)), model, args)
  1.1516 +			end
  1.1517 +		| _ =>
  1.1518 +			NONE;
  1.1519 +
  1.1520  
  1.1521  (* ------------------------------------------------------------------------- *)
  1.1522  (* PRINTERS                                                                  *)
  1.1523 @@ -1695,14 +2185,7 @@
  1.1524  		  | string_of_typ (TVar ((x,i), _)) = strip_leading_quote x ^ string_of_int i
  1.1525  		(* interpretation -> int *)
  1.1526  		fun index_from_interpretation (Leaf xs) =
  1.1527 -			let
  1.1528 -				val idx = find_index (PropLogic.eval assignment) xs
  1.1529 -			in
  1.1530 -				if idx<0 then
  1.1531 -					raise REFUTE ("stlc_printer", "illegal interpretation: no value assigned (SAT solver unsound?)")
  1.1532 -				else
  1.1533 -					idx
  1.1534 -			end
  1.1535 +			find_index (PropLogic.eval assignment) xs
  1.1536  		  | index_from_interpretation _ =
  1.1537  			raise REFUTE ("stlc_printer", "interpretation for ground type is not a leaf")
  1.1538  	in
  1.1539 @@ -1712,7 +2195,7 @@
  1.1540  			  Type ("fun", [T1, T2]) =>
  1.1541  				let
  1.1542  					(* create all constants of type 'T1' *)
  1.1543 -					val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
  1.1544 +					val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))
  1.1545  					val constants = make_constants i
  1.1546  					(* interpretation list *)
  1.1547  					val results = (case intr of
  1.1548 @@ -1735,12 +2218,22 @@
  1.1549  				end
  1.1550  			| Type ("prop", [])      =>
  1.1551  				(case index_from_interpretation intr of
  1.1552 -				  0 => SOME (HOLogic.mk_Trueprop HOLogic.true_const)
  1.1553 -				| 1 => SOME (HOLogic.mk_Trueprop HOLogic.false_const)
  1.1554 -				| _ => raise REFUTE ("stlc_interpreter", "illegal interpretation for a propositional value"))
  1.1555 -			| Type _  => SOME (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
  1.1556 -			| TFree _ => SOME (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
  1.1557 -			| TVar _  => SOME (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T)))
  1.1558 +				  (~1) => SOME (HOLogic.mk_Trueprop (Const ("arbitrary", HOLogic.boolT)))
  1.1559 +				| 0    => SOME (HOLogic.mk_Trueprop HOLogic.true_const)
  1.1560 +				| 1    => SOME (HOLogic.mk_Trueprop HOLogic.false_const)
  1.1561 +				| _    => raise REFUTE ("stlc_interpreter", "illegal interpretation for a propositional value"))
  1.1562 +			| Type _  => if index_from_interpretation intr = (~1) then
  1.1563 +					SOME (Const ("arbitrary", T))
  1.1564 +				else
  1.1565 +					SOME (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
  1.1566 +			| TFree _ => if index_from_interpretation intr = (~1) then
  1.1567 +					SOME (Const ("arbitrary", T))
  1.1568 +				else
  1.1569 +					SOME (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T))
  1.1570 +			| TVar _  => if index_from_interpretation intr = (~1) then
  1.1571 +					SOME (Const ("arbitrary", T))
  1.1572 +				else
  1.1573 +					SOME (Const (string_of_typ T ^ string_of_int (index_from_interpretation intr), T)))
  1.1574  		| NONE =>
  1.1575  			NONE
  1.1576  	end;
  1.1577 @@ -1759,7 +2252,7 @@
  1.1578  		  SOME (Type ("set", [T])) =>
  1.1579  			let
  1.1580  				(* create all constants of type 'T' *)
  1.1581 -				val (i, _, _) = interpret thy model {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1.1582 +				val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
  1.1583  				val constants = make_constants i
  1.1584  				(* interpretation list *)
  1.1585  				val results = (case intr of
  1.1586 @@ -1771,10 +2264,8 @@
  1.1587  					  Leaf [fmTrue, fmFalse] =>
  1.1588  						if PropLogic.eval assignment fmTrue then
  1.1589  							SOME (print thy model (Free ("dummy", T)) arg assignment)
  1.1590 -						else if PropLogic.eval assignment fmFalse then
  1.1591 +						else (*if PropLogic.eval assignment fmFalse then*)
  1.1592  							NONE
  1.1593 -						else
  1.1594 -							raise REFUTE ("set_printer", "illegal interpretation: no value assigned (SAT solver unsound?)")
  1.1595  					| _ =>
  1.1596  						raise REFUTE ("set_printer", "illegal interpretation for a Boolean value"))
  1.1597  					(constants ~~ results)
  1.1598 @@ -1821,46 +2312,58 @@
  1.1599  					val element = (case intr of
  1.1600  						  Leaf xs => find_index (PropLogic.eval assignment) xs
  1.1601  						| Node _  => raise REFUTE ("IDT_printer", "interpretation is not a leaf"))
  1.1602 -					val _ = (if element<0 then raise REFUTE ("IDT_printer", "invalid interpretation (no value assigned)") else ())
  1.1603 -					(* int option -- only recursive IDTs have an associated depth *)
  1.1604 -					val depth = assoc (typs, Type (s, Ts))
  1.1605 -					val typs' = (case depth of NONE => typs | SOME n => overwrite (typs, (Type (s, Ts), n-1)))
  1.1606 -					(* int -> DatatypeAux.dtyp list -> Term.term list *)
  1.1607 -					fun make_args n [] =
  1.1608 -						if n<>0 then
  1.1609 -							raise REFUTE ("IDT_printer", "error computing the element: remainder is not 0")
  1.1610 -						else
  1.1611 -							[]
  1.1612 -					  | make_args n (d::ds) =
  1.1613 -						let
  1.1614 -							val dT        = typ_of_dtyp descr typ_assoc d
  1.1615 -							val (i, _, _) = interpret thy (typs', []) {maxvars=0, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", dT))
  1.1616 -							val size      = size_of_type i
  1.1617 -							val consts    = make_constants i  (* we only need the (n mod size)-th element of *)
  1.1618 -								(* this list, so there might be a more efficient implementation that does not *)
  1.1619 -								(* generate all constants                                                     *)
  1.1620 -						in
  1.1621 -							(print thy (typs', []) (Free ("dummy", dT)) (nth_elem (n mod size, consts)) assignment)::(make_args (n div size) ds)
  1.1622 -						end
  1.1623 -					(* int -> (string * DatatypeAux.dtyp list) list -> Term.term *)
  1.1624 -					fun make_term _ [] =
  1.1625 -						raise REFUTE ("IDT_printer", "invalid interpretation (value too large - not enough constructors)")
  1.1626 -					  | make_term n (c::cs) =
  1.1627 -						let
  1.1628 -							val c_size = size_of_dtyp thy typs' descr typ_assoc [c]
  1.1629 -						in
  1.1630 -							if n<c_size then
  1.1631 -								let
  1.1632 -									val (cname, cargs) = c
  1.1633 -									val c_term = Const (cname, (map (typ_of_dtyp descr typ_assoc) cargs) ---> Type (s, Ts))
  1.1634 -								in
  1.1635 -									foldl op$ (c_term, rev (make_args n (rev cargs)))
  1.1636 -								end
  1.1637 -							else
  1.1638 -								make_term (n-c_size) cs
  1.1639 -						end
  1.1640  				in
  1.1641 -					SOME (make_term element constrs)
  1.1642 +					if element < 0 then
  1.1643 +						SOME (Const ("arbitrary", Type (s, Ts)))
  1.1644 +					else let
  1.1645 +						(* takes a datatype constructor, and if for some arguments this constructor *)
  1.1646 +						(* generates the datatype's element that is given by 'element', returns the *)
  1.1647 +						(* constructor (as a term) as well as the indices of the arguments          *)
  1.1648 +						(* string * DatatypeAux.dtyp list -> (Term.term * int list) option *)
  1.1649 +						fun get_constr_args (cname, cargs) =
  1.1650 +							let
  1.1651 +								val cTerm      = Const (cname, (map (typ_of_dtyp descr typ_assoc) cargs) ---> Type (s, Ts))
  1.1652 +								(*TODO val _          = writeln ("cTerm: " ^ makestring cTerm) *)
  1.1653 +								val (iC, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
  1.1654 +								(*TODO val _          = writeln ("iC: " ^ makestring iC) *)
  1.1655 +								(* interpretation -> int list option *)
  1.1656 +								fun get_args (Leaf xs) =
  1.1657 +									if find_index_eq True xs = element then
  1.1658 +										SOME []
  1.1659 +									else
  1.1660 +										NONE
  1.1661 +								  | get_args (Node xs) =
  1.1662 +									let
  1.1663 +										(* interpretation * int -> int list option *)
  1.1664 +										fun search ([], _) =
  1.1665 +											NONE
  1.1666 +										  | search (x::xs, n) =
  1.1667 +											(case get_args x of
  1.1668 +											  SOME result => SOME (n::result)
  1.1669 +											| NONE        => search (xs, n+1))
  1.1670 +									in
  1.1671 +										search (xs, 0)
  1.1672 +									end
  1.1673 +							in
  1.1674 +								apsome (fn args => (cTerm, cargs, args)) (get_args iC)
  1.1675 +							end
  1.1676 +						(* Term.term * DatatypeAux.dtyp list * int list *)
  1.1677 +						val (cTerm, cargs, args) = (case get_first get_constr_args constrs of
  1.1678 +							  SOME x => x
  1.1679 +							| NONE   => raise REFUTE ("IDT_printer", "no matching constructor found for element " ^ string_of_int element))
  1.1680 +						val argsTerms = map (fn (d, n) =>
  1.1681 +							let
  1.1682 +								val dT        = typ_of_dtyp descr typ_assoc d
  1.1683 +								val (i, _, _) = interpret thy (typs, []) {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", dT))
  1.1684 +								val consts    = make_constants i  (* we only need the n-th element of this *)
  1.1685 +									(* list, so there might be a more efficient implementation that does    *)
  1.1686 +									(* not generate all constants                                           *)
  1.1687 +							in
  1.1688 +								print thy (typs, []) (Free ("dummy", dT)) (nth_elem (n, consts)) assignment
  1.1689 +							end) (cargs ~~ args)
  1.1690 +					in
  1.1691 +						SOME (foldl op$ (cTerm, argsTerms))
  1.1692 +					end
  1.1693  				end
  1.1694  			| NONE =>  (* not an inductive datatype *)
  1.1695  				NONE)
  1.1696 @@ -1890,7 +2393,13 @@
  1.1697  		 add_interpreter "HOLogic"         HOLogic_interpreter,
  1.1698  		 add_interpreter "set"             set_interpreter,
  1.1699  		 add_interpreter "IDT"             IDT_interpreter,
  1.1700 +		 add_interpreter "IDT_constructor" IDT_constructor_interpreter,
  1.1701 +		 add_interpreter "IDT_recursion"   IDT_recursion_interpreter,
  1.1702  		 add_interpreter "Finite_Set.card" Finite_Set_card_interpreter,
  1.1703 +		 add_interpreter "Nat.op <"        Nat_less_interpreter,
  1.1704 +		 add_interpreter "Nat.op +"        Nat_plus_interpreter,
  1.1705 +		 add_interpreter "Nat.op -"        Nat_minus_interpreter,
  1.1706 +		 add_interpreter "Nat.op *"        Nat_mult_interpreter,
  1.1707  		 add_printer "stlc" stlc_printer,
  1.1708  		 add_printer "set"  set_printer,
  1.1709  		 add_printer "IDT"  IDT_printer];