constants are unfolded, universal quantifiers are stripped, some minor changes
authorwebertj
Thu Jan 04 00:12:30 2007 +0100 (2007-01-04)
changeset 21985acfb13e8819e
parent 21984 7b9c2f6b45f5
child 21986 76d3d258cfa3
constants are unfolded, universal quantifiers are stripped, some minor changes
src/HOL/Tools/refute.ML
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Jan 03 22:59:30 2007 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Jan 04 00:12:30 2007 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Tools/refute.ML
     1.5      ID:         $Id$
     1.6      Author:     Tjark Weber
     1.7 -    Copyright   2003-2005
     1.8 +    Copyright   2003-2007
     1.9  
    1.10  Finite model generation for HOL formulas, using a SAT solver.
    1.11  *)
    1.12 @@ -382,25 +382,337 @@
    1.13  
    1.14  	fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
    1.15  		(* replace a 'DtTFree' variable by the associated type *)
    1.16 -		(the o AList.lookup (op =) typ_assoc) (DatatypeAux.DtTFree a)
    1.17 +		(Option.valOf o AList.lookup (op =) typ_assoc) (DatatypeAux.DtTFree a)
    1.18  	  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
    1.19  		Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.20  	  | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
    1.21  		let
    1.22 -			val (s, ds, _) = (the o AList.lookup (op =) descr) i
    1.23 +			val (s, ds, _) = (Option.valOf o AList.lookup (op =) descr) i
    1.24  		in
    1.25  			Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.26  		end;
    1.27  
    1.28  (* ------------------------------------------------------------------------- *)
    1.29 -(* collect_axioms: collects (monomorphic, universally quantified versions    *)
    1.30 -(*                 of) all HOL axioms that are relevant w.r.t 't'            *)
    1.31 +(* close_form: universal closure over schematic variables in 't'             *)
    1.32 +(* ------------------------------------------------------------------------- *)
    1.33 +
    1.34 +	(* Term.term -> Term.term *)
    1.35 +
    1.36 +	fun close_form t =
    1.37 +	let
    1.38 +		(* (Term.indexname * Term.typ) list *)
    1.39 +		val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
    1.40 +	in
    1.41 +		Library.foldl
    1.42 +			(fn (t', ((x, i), T)) => (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
    1.43 +			(t, vars)
    1.44 +	end;
    1.45 +
    1.46 +(* ------------------------------------------------------------------------- *)
    1.47 +(* monomorphic_term: applies a type substitution 'typeSubs' for all type     *)
    1.48 +(*                   variables in a term 't'                                 *)
    1.49 +(* ------------------------------------------------------------------------- *)
    1.50 +
    1.51 +	(* Type.tyenv -> Term.term -> Term.term *)
    1.52 +
    1.53 +	fun monomorphic_term typeSubs t =
    1.54 +		map_types (map_type_tvar
    1.55 +			(fn v =>
    1.56 +				case Type.lookup (typeSubs, v) of
    1.57 +				  NONE =>
    1.58 +					(* schematic type variable not instantiated *)
    1.59 +					raise REFUTE ("monomorphic_term",
    1.60 +						"no substitution for type variable " ^ fst (fst v) ^
    1.61 +						" in term " ^ Display.raw_string_of_term t)
    1.62 +				| SOME typ =>
    1.63 +					typ)) t;
    1.64 +
    1.65 +(* ------------------------------------------------------------------------- *)
    1.66 +(* specialize_type: given a constant 's' of type 'T', which is a subterm of  *)
    1.67 +(*                  't', where 't' has a (possibly) more general type, the   *)
    1.68 +(*                  schematic type variables in 't' are instantiated to      *)
    1.69 +(*                  match the type 'T' (may raise Type.TYPE_MATCH)           *)
    1.70 +(* ------------------------------------------------------------------------- *)
    1.71 +
    1.72 +	(* theory -> (string * Term.typ) -> Term.term -> Term.term *)
    1.73 +
    1.74 +	fun specialize_type thy (s, T) t =
    1.75 +	let
    1.76 +		fun find_typeSubs (Const (s', T')) =
    1.77 +			if s=s' then
    1.78 +				SOME (Sign.typ_match thy (T', T) Vartab.empty)
    1.79 +					handle Type.TYPE_MATCH => NONE
    1.80 +			else
    1.81 +				NONE
    1.82 +		  | find_typeSubs (Free _)           = NONE
    1.83 +		  | find_typeSubs (Var _)            = NONE
    1.84 +		  | find_typeSubs (Bound _)          = NONE
    1.85 +		  | find_typeSubs (Abs (_, _, body)) = find_typeSubs body
    1.86 +		  | find_typeSubs (t1 $ t2)          =
    1.87 +			(case find_typeSubs t1 of SOME x => SOME x
    1.88 +			                        | NONE   => find_typeSubs t2)
    1.89 +	in
    1.90 +		case find_typeSubs t of
    1.91 +		  SOME typeSubs =>
    1.92 +			monomorphic_term typeSubs t
    1.93 +		| NONE =>
    1.94 +			(* no match found - perhaps due to sort constraints *)
    1.95 +			raise Type.TYPE_MATCH
    1.96 +	end;
    1.97 +
    1.98 +(* ------------------------------------------------------------------------- *)
    1.99 +(* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that   *)
   1.100 +(*                    denotes membership to an axiomatic type class          *)
   1.101 +(* ------------------------------------------------------------------------- *)
   1.102 +
   1.103 +	(* theory -> string * Term.typ -> bool *)
   1.104 +
   1.105 +	fun is_const_of_class thy (s, T) =
   1.106 +	let
   1.107 +		val class_const_names = map Logic.const_of_class (Sign.all_classes thy)
   1.108 +	in
   1.109 +		(* I'm not quite sure if checking the name 's' is sufficient, *)
   1.110 +		(* or if we should also check the type 'T'.                   *)
   1.111 +		s mem_string class_const_names
   1.112 +	end;
   1.113 +
   1.114 +(* ------------------------------------------------------------------------- *)
   1.115 +(* is_IDT_constructor: returns 'true' iff 'Const (s, T)' is the constructor  *)
   1.116 +(*                     of an inductive datatype in 'thy'                     *)
   1.117 +(* ------------------------------------------------------------------------- *)
   1.118 +
   1.119 +	(* theory -> string * Term.typ -> bool *)
   1.120 +
   1.121 +	fun is_IDT_constructor thy (s, T) =
   1.122 +		(case body_type T of
   1.123 +		  Type (s', _) =>
   1.124 +			(case DatatypePackage.get_datatype_constrs thy s' of
   1.125 +			  SOME constrs =>
   1.126 +				List.exists (fn (cname, cty) =>
   1.127 +					cname = s andalso Sign.typ_instance thy (T, cty)) constrs
   1.128 +			| NONE =>
   1.129 +				false)
   1.130 +		| _  =>
   1.131 +			false);
   1.132 +
   1.133 +(* ------------------------------------------------------------------------- *)
   1.134 +(* is_IDT_recursor: returns 'true' iff 'Const (s, T)' is the recursion       *)
   1.135 +(*                  operator of an inductive datatype in 'thy'               *)
   1.136 +(* ------------------------------------------------------------------------- *)
   1.137 +
   1.138 +	(* theory -> string * Term.typ -> bool *)
   1.139 +
   1.140 +	fun is_IDT_recursor thy (s, T) =
   1.141 +	let
   1.142 +		val rec_names = Symtab.fold (append o #rec_names o snd)
   1.143 +			(DatatypePackage.get_datatypes thy) []
   1.144 +	in
   1.145 +		(* I'm not quite sure if checking the name 's' is sufficient, *)
   1.146 +		(* or if we should also check the type 'T'.                   *)
   1.147 +		s mem_string rec_names
   1.148 +	end;
   1.149 +
   1.150 +(* ------------------------------------------------------------------------- *)
   1.151 +(* get_def: looks up the definition of a constant, as created by "constdefs" *)
   1.152 +(* ------------------------------------------------------------------------- *)
   1.153 +
   1.154 +	(* theory -> string * Term.typ -> (string * Term.term) option *)
   1.155 +
   1.156 +	fun get_def thy (s, T) =
   1.157 +	let
   1.158 +		(* maps  f ?t1 ... ?tn == rhs  to  %t1...tn. rhs *)
   1.159 +		fun norm_rhs eqn =
   1.160 +		let
   1.161 +			fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
   1.162 +			  | lambda v t                      = raise TERM ("lambda", [v, t])
   1.163 +			val (lhs, rhs) = Logic.dest_equals eqn
   1.164 +			val (_, args)  = Term.strip_comb lhs
   1.165 +		in
   1.166 +			fold lambda (rev args) rhs
   1.167 +		end
   1.168 +		(* (string * Term.term) list -> (string * Term.term) option *)
   1.169 +		fun get_def_ax [] = NONE
   1.170 +		  | get_def_ax ((axname, ax) :: axioms) =
   1.171 +			(let
   1.172 +				val (lhs, _) = Logic.dest_equals ax  (* equations only *)
   1.173 +				val c        = Term.head_of lhs
   1.174 +				val (s', T') = Term.dest_Const c
   1.175 +			in
   1.176 +				if s=s' then
   1.177 +					let
   1.178 +						val typeSubs = Sign.typ_match thy (T', T) Vartab.empty
   1.179 +						val ax'      = monomorphic_term typeSubs ax
   1.180 +						val rhs      = norm_rhs ax'
   1.181 +					in
   1.182 +						SOME (axname, rhs)
   1.183 +					end
   1.184 +				else
   1.185 +					get_def_ax axioms
   1.186 +			end handle ERROR _         => get_def_ax axioms
   1.187 +			         | TERM _          => get_def_ax axioms
   1.188 +			         | Type.TYPE_MATCH => get_def_ax axioms)
   1.189 +	in
   1.190 +		get_def_ax (Theory.all_axioms_of thy)
   1.191 +	end;
   1.192 +
   1.193 +(* ------------------------------------------------------------------------- *)
   1.194 +(* get_typedef: looks up the definition of a type, as created by "typedef"   *)
   1.195 +(* ------------------------------------------------------------------------- *)
   1.196 +
   1.197 +	(* theory -> (string * Term.typ) -> (string * Term.term) option *)
   1.198 +
   1.199 +	fun get_typedef thy T =
   1.200 +	let
   1.201 +		(* (string * Term.term) list -> (string * Term.term) option *)
   1.202 +		fun get_typedef_ax [] = NONE
   1.203 +		  | get_typedef_ax ((axname, ax) :: axioms) =
   1.204 +			(let
   1.205 +				(* Term.term -> Term.typ option *)
   1.206 +				fun type_of_type_definition (Const (s', T')) =
   1.207 +					if s'="Typedef.type_definition" then
   1.208 +						SOME T'
   1.209 +					else
   1.210 +						NONE
   1.211 +				  | type_of_type_definition (Free _)           = NONE
   1.212 +				  | type_of_type_definition (Var _)            = NONE
   1.213 +				  | type_of_type_definition (Bound _)          = NONE
   1.214 +				  | type_of_type_definition (Abs (_, _, body)) =
   1.215 +					type_of_type_definition body
   1.216 +				  | type_of_type_definition (t1 $ t2)          =
   1.217 +					(case type_of_type_definition t1 of
   1.218 +					  SOME x => SOME x
   1.219 +					| NONE   => type_of_type_definition t2)
   1.220 +			in
   1.221 +				case type_of_type_definition ax of
   1.222 +				  SOME T' =>
   1.223 +					let
   1.224 +						val T''      = (domain_type o domain_type) T'
   1.225 +						val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty
   1.226 +					in
   1.227 +						SOME (axname, monomorphic_term typeSubs ax)
   1.228 +					end
   1.229 +				| NONE =>
   1.230 +					get_typedef_ax axioms
   1.231 +			end handle ERROR _         => get_typedef_ax axioms
   1.232 +			         | MATCH           => get_typedef_ax axioms
   1.233 +			         | Type.TYPE_MATCH => get_typedef_ax axioms)
   1.234 +	in
   1.235 +		get_typedef_ax (Theory.all_axioms_of thy)
   1.236 +	end;
   1.237 +
   1.238 +(* ------------------------------------------------------------------------- *)
   1.239 +(* get_classdef: looks up the defining axiom for an axiomatic type class, as *)
   1.240 +(*               created by the "axclass" command                            *)
   1.241 +(* ------------------------------------------------------------------------- *)
   1.242 +
   1.243 +	(* theory -> string -> (string * Term.term) option *)
   1.244 +
   1.245 +	fun get_classdef thy class =
   1.246 +	let
   1.247 +		val axname = class ^ "_class_def"
   1.248 +	in
   1.249 +		Option.map (pair axname)
   1.250 +			(AList.lookup (op =) (Theory.all_axioms_of thy) axname)
   1.251 +	end;
   1.252 +
   1.253 +(* ------------------------------------------------------------------------- *)
   1.254 +(* unfold_defs: unfolds all defined constants in a term 't', beta-eta        *)
   1.255 +(*              normalizes the result term; certain constants are not        *)
   1.256 +(*              unfolded (cf. 'collect_axioms' and the various interpreters  *)
   1.257 +(*              below): if the interpretation respects a definition anyway,  *)
   1.258 +(*              that definition does not need to be unfolded                 *)
   1.259 +(* ------------------------------------------------------------------------- *)
   1.260 +
   1.261 +	(* theory -> Term.term -> Term.term *)
   1.262 +
   1.263 +	(* Note: we could intertwine unfolding of constants and beta-(eta-)       *)
   1.264 +	(*       normalization; this would save some unfolding for terms where    *)
   1.265 +	(*       constants are eliminated by beta-reduction (e.g. 'K c1 c2').  On *)
   1.266 +	(*       the other hand, this would cause additional work for terms where *)
   1.267 +	(*       constants are duplicated by beta-reduction (e.g. 'S c1 c2 c3').  *)
   1.268 +
   1.269 +	fun unfold_defs thy t =
   1.270 +	let
   1.271 +		(* Term.term -> Term.term *)
   1.272 +		fun unfold_loop t =
   1.273 +			case t of
   1.274 +			(* Pure *)
   1.275 +			  Const ("all", _)                => t
   1.276 +			| Const ("==", _)                 => t
   1.277 +			| Const ("==>", _)                => t
   1.278 +			| Const ("TYPE", _)               => t  (* axiomatic type classes *)
   1.279 +			(* HOL *)
   1.280 +			| Const ("Trueprop", _)           => t
   1.281 +			| Const ("Not", _)                => t
   1.282 +			| (* redundant, since 'True' is also an IDT constructor *)
   1.283 +			  Const ("True", _)               => t
   1.284 +			| (* redundant, since 'False' is also an IDT constructor *)
   1.285 +			  Const ("False", _)              => t
   1.286 +			| Const ("arbitrary", _)          => t
   1.287 +			| Const ("The", _)                => t
   1.288 +			| Const ("Hilbert_Choice.Eps", _) => t
   1.289 +			| Const ("All", _)                => t
   1.290 +			| Const ("Ex", _)                 => t
   1.291 +			| Const ("op =", _)               => t
   1.292 +			| Const ("op &", _)               => t
   1.293 +			| Const ("op |", _)               => t
   1.294 +			| Const ("op -->", _)             => t
   1.295 +			(* sets *)
   1.296 +			| Const ("Collect", _)            => t
   1.297 +			| Const ("op :", _)               => t
   1.298 +			(* other optimizations *)
   1.299 +			| Const ("Finite_Set.card", _)    => t
   1.300 +			| Const ("Finite_Set.Finites", _) => t
   1.301 +			| Const ("Orderings.less", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
   1.302 +			| Const ("HOL.plus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   1.303 +			| Const ("HOL.minus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   1.304 +			| Const ("HOL.times", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   1.305 +			| Const ("List.op @", _)          => t
   1.306 +			| Const ("Lfp.lfp", _)            => t
   1.307 +			| Const ("Gfp.gfp", _)            => t
   1.308 +			| Const ("fst", _)                => t
   1.309 +			| Const ("snd", _)                => t
   1.310 +			(* simply-typed lambda calculus *)
   1.311 +			| Const (s, T) =>
   1.312 +				(if is_IDT_constructor thy (s, T) orelse is_IDT_recursor thy (s, T) then
   1.313 +					t  (* do not unfold IDT constructors/recursors *)
   1.314 +				(* unfold the constant if there is a defining equation *)
   1.315 +				else case get_def thy (s, T) of
   1.316 +				  SOME (axname, rhs) =>
   1.317 +					(* Note: if the term to be unfolded (i.e. 'Const (s, T)')  *)
   1.318 +					(* occurs on the right-hand side of the equation, i.e. in  *)
   1.319 +					(* 'rhs', we must not use this equation to unfold, because *)
   1.320 +					(* that would loop.  Here would be the right place to      *)
   1.321 +					(* check this.  However, getting this really right seems   *)
   1.322 +					(* difficult because the user may state arbitrary axioms,  *)
   1.323 +					(* which could interact with overloading to create loops.  *)
   1.324 +					((*immediate_output (" unfolding: " ^ axname);*)unfold_loop rhs)
   1.325 +				| NONE => t)
   1.326 +			| Free _           => t
   1.327 +			| Var _            => t
   1.328 +			| Bound _          => t
   1.329 +			| Abs (s, T, body) => Abs (s, T, unfold_loop body)
   1.330 +			| t1 $ t2          => (unfold_loop t1) $ (unfold_loop t2)
   1.331 +		val result = Envir.beta_eta_contract (unfold_loop t)
   1.332 +	in
   1.333 +		result
   1.334 +	end;
   1.335 +
   1.336 +(* ------------------------------------------------------------------------- *)
   1.337 +(* collect_axioms: collects (monomorphic, universally quantified, unfolded   *)
   1.338 +(*                 versions of) all HOL axioms that are relevant w.r.t 't'   *)
   1.339  (* ------------------------------------------------------------------------- *)
   1.340  
   1.341  	(* Note: to make the collection of axioms more easily extensible, this    *)
   1.342  	(*       function could be based on user-supplied "axiom collectors",     *)
   1.343  	(*       similar to 'interpret'/interpreters or 'print'/printers          *)
   1.344  
   1.345 +	(* Note: currently we use "inverse" functions to the definitional         *)
   1.346 +	(*       mechanisms provided by Isabelle/HOL, e.g. for "axclass",         *)
   1.347 +	(*       "typedef", "constdefs".  A more general approach could consider  *)
   1.348 +	(*       *every* axiom of the theory and collect it if it has a constant/ *)
   1.349 +	(*       type/typeclass in common with the term 't'.                      *)
   1.350 +
   1.351  	(* theory -> Term.term -> Term.term list *)
   1.352  
   1.353  	(* Which axioms are "relevant" for a particular term/type goes hand in    *)
   1.354 @@ -408,109 +720,60 @@
   1.355  	(* way below): if the interpretation respects an axiom anyway, the axiom  *)
   1.356  	(* does not need to be added as a constraint here.                        *)
   1.357  
   1.358 -	(* When an axiom is added as relevant, further axioms may need to be      *)
   1.359 -	(* added as well (e.g. when a constant is defined in terms of other       *)
   1.360 -	(* constants).  To avoid infinite recursion (which should not happen for  *)
   1.361 -	(* constants anyway, but it could happen for "typedef"-related axioms,    *)
   1.362 -	(* since they contain the type again), we use an accumulator 'axs' and    *)
   1.363 -	(* add a relevant axiom only if it is not in 'axs' yet.                   *)
   1.364 +	(* To avoid collecting the same axiom multiple times, we use an           *)
   1.365 +	(* accumulator 'axs' which contains all axioms collected so far.          *)
   1.366  
   1.367  	fun collect_axioms thy t =
   1.368  	let
   1.369  		val _ = immediate_output "Adding axioms..."
   1.370  		(* (string * Term.term) list *)
   1.371 -		val axioms = Theory.all_axioms_of thy;
   1.372 -		(* string list *)
   1.373 -		val rec_names = Symtab.fold (append o #rec_names o snd)
   1.374 -          (DatatypePackage.get_datatypes thy) [];
   1.375 -		(* string list *)
   1.376 -		val const_of_class_names = map Logic.const_of_class (Sign.all_classes thy)
   1.377 -		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
   1.378 -		(* 't' has a (possibly) more general type, the schematic type          *)
   1.379 -		(* variables in 't' are instantiated to match the type 'T' (may raise  *)
   1.380 -		(* Type.TYPE_MATCH)                                                    *)
   1.381 -		(* (string * Term.typ) * Term.term -> Term.term *)
   1.382 -		fun specialize_type ((s, T), t) =
   1.383 +		val axioms = Theory.all_axioms_of thy
   1.384 +		(* string * Term.term -> Term.term list -> Term.term list *)
   1.385 +		fun collect_this_axiom (axname, ax) axs =
   1.386  		let
   1.387 -			fun find_typeSubs (Const (s', T')) =
   1.388 -				(if s=s' then
   1.389 -					SOME (Sign.typ_match thy (T', T) Vartab.empty) handle Type.TYPE_MATCH => NONE
   1.390 -				else
   1.391 -					NONE)
   1.392 -			  | find_typeSubs (Free _)           = NONE
   1.393 -			  | find_typeSubs (Var _)            = NONE
   1.394 -			  | find_typeSubs (Bound _)          = NONE
   1.395 -			  | find_typeSubs (Abs (_, _, body)) = find_typeSubs body
   1.396 -			  | find_typeSubs (t1 $ t2)          = (case find_typeSubs t1 of SOME x => SOME x | NONE => find_typeSubs t2)
   1.397 -			val typeSubs = (case find_typeSubs t of
   1.398 -				  SOME x => x
   1.399 -				| NONE   => raise Type.TYPE_MATCH (* no match found - perhaps due to sort constraints *))
   1.400 +			val ax' = unfold_defs thy ax
   1.401  		in
   1.402 -			map_types
   1.403 -				(map_type_tvar
   1.404 -					(fn v =>
   1.405 -						case Type.lookup (typeSubs, v) of
   1.406 -						  NONE =>
   1.407 -							(* schematic type variable not instantiated *)
   1.408 -							raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")")
   1.409 -						| SOME typ =>
   1.410 -							typ))
   1.411 -					t
   1.412 +			if member (op aconv) axs ax' then
   1.413 +				axs
   1.414 +			else (
   1.415 +				immediate_output (" " ^ axname);
   1.416 +				collect_term_axioms (ax' :: axs, ax')
   1.417 +			)
   1.418  		end
   1.419 -		(* applies a type substitution 'typeSubs' for all type variables in a  *)
   1.420 -		(* term 't'                                                            *)
   1.421 -		(* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *)
   1.422 -		fun monomorphic_term typeSubs t =
   1.423 -			map_types (map_type_tvar
   1.424 -				(fn v =>
   1.425 -					case Type.lookup (typeSubs, v) of
   1.426 -					  NONE =>
   1.427 -						(* schematic type variable not instantiated *)
   1.428 -						error ""
   1.429 -					| SOME typ =>
   1.430 -						typ)) t
   1.431  		(* Term.term list * Term.typ -> Term.term list *)
   1.432 -		fun collect_sort_axioms (axs, T) =
   1.433 -			let
   1.434 -				(* collect the axioms for a single 'class' (but not for its superclasses) *)
   1.435 -				(* Term.term list * string -> Term.term list *)
   1.436 -				fun collect_class_axioms (axs, class) =
   1.437 -					let
   1.438 -						(* obtain the axioms generated by the "axclass" command *)
   1.439 -						(* (string * Term.term) list *)
   1.440 -						val class_axioms             = List.filter (fn (s, _) => String.isPrefix (Logic.const_of_class class ^ ".axioms_") s) axioms
   1.441 -						(* replace the one schematic type variable in each axiom by the actual type 'T' *)
   1.442 -						(* (string * Term.term) list *)
   1.443 -						val monomorphic_class_axioms = map (fn (axname, ax) =>
   1.444 -							let
   1.445 -								val (idx, S) = (case term_tvars ax of
   1.446 -									  [is] => is
   1.447 -									| _    => raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ Sign.string_of_term (sign_of thy) ax ^ ") does not contain exactly one type variable"))
   1.448 -							in
   1.449 -								(axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
   1.450 -							end) class_axioms
   1.451 -						(* Term.term list * (string * Term.term) list -> Term.term list *)
   1.452 -						fun collect_axiom (axs, (axname, ax)) =
   1.453 -							if member (op aconv) axs ax then
   1.454 -								axs
   1.455 -							else (
   1.456 -								immediate_output (" " ^ axname);
   1.457 -								collect_term_axioms (ax :: axs, ax)
   1.458 -							)
   1.459 -					in
   1.460 -						Library.foldl collect_axiom (axs, monomorphic_class_axioms)
   1.461 -					end
   1.462 -				(* string list *)
   1.463 -				val sort = (case T of
   1.464 -					  TFree (_, sort) => sort
   1.465 -					| TVar (_, sort)  => sort
   1.466 -					| _               => raise REFUTE ("collect_axioms", "type " ^ Sign.string_of_typ (sign_of thy) T ^ " is not a variable"))
   1.467 -				(* obtain all superclasses of classes in 'sort' *)
   1.468 -				(* string list *)
   1.469 -				val superclasses = distinct (op =) (sort @ maps (Sign.super_classes thy) sort)
   1.470 -			in
   1.471 -				Library.foldl collect_class_axioms (axs, superclasses)
   1.472 -			end
   1.473 +		and collect_sort_axioms (axs, T) =
   1.474 +		let
   1.475 +			(* string list *)
   1.476 +			val sort = (case T of
   1.477 +				  TFree (_, sort) => sort
   1.478 +				| TVar (_, sort)  => sort
   1.479 +				| _               => raise REFUTE ("collect_axioms", "type " ^
   1.480 +					Sign.string_of_typ thy T ^ " is not a variable"))
   1.481 +			(* obtain axioms for all superclasses *)
   1.482 +			val superclasses = sort @ (maps (Sign.super_classes thy) sort)
   1.483 +			(* merely an optimization, because 'collect_this_axiom' disallows *)
   1.484 +			(* duplicate axioms anyway:                                       *)
   1.485 +			val superclasses = distinct (op =) superclasses
   1.486 +			val class_axioms = maps (fn class => map (fn ax =>
   1.487 +				("<" ^ class ^ ">", Thm.prop_of ax))
   1.488 +				(#axioms (AxClass.get_definition thy class) handle ERROR _ => []))
   1.489 +				superclasses
   1.490 +			(* replace the (at most one) schematic type variable in each axiom *)
   1.491 +			(* by the actual type 'T'                                          *)
   1.492 +			val monomorphic_class_axioms = map (fn (axname, ax) =>
   1.493 +				(case Term.term_tvars ax of
   1.494 +				  [] =>
   1.495 +					(axname, ax)
   1.496 +				| [(idx, S)] =>
   1.497 +					(axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
   1.498 +				| _ =>
   1.499 +					raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
   1.500 +						Sign.string_of_term thy ax ^
   1.501 +						") contains more than one type variable")))
   1.502 +				class_axioms
   1.503 +		in
   1.504 +			fold collect_this_axiom monomorphic_class_axioms axs
   1.505 +		end
   1.506  		(* Term.term list * Term.typ -> Term.term list *)
   1.507  		and collect_type_axioms (axs, T) =
   1.508  			case T of
   1.509 @@ -520,58 +783,18 @@
   1.510  			| Type ("set", [T1])     => collect_type_axioms (axs, T1)
   1.511  			| Type ("itself", [T1])  => collect_type_axioms (axs, T1)  (* axiomatic type classes *)
   1.512  			| Type (s, Ts)           =>
   1.513 -				let
   1.514 -					(* look up the definition of a type, as created by "typedef" *)
   1.515 -					(* (string * Term.term) list -> (string * Term.term) option *)
   1.516 -					fun get_typedefn [] =
   1.517 -						NONE
   1.518 -					  | get_typedefn ((axname,ax)::axms) =
   1.519 -						(let
   1.520 -							(* Term.term -> Term.typ option *)
   1.521 -							fun type_of_type_definition (Const (s', T')) =
   1.522 -								if s'="Typedef.type_definition" then
   1.523 -									SOME T'
   1.524 -								else
   1.525 -									NONE
   1.526 -							  | type_of_type_definition (Free _)           = NONE
   1.527 -							  | type_of_type_definition (Var _)            = NONE
   1.528 -							  | type_of_type_definition (Bound _)          = NONE
   1.529 -							  | type_of_type_definition (Abs (_, _, body)) = type_of_type_definition body
   1.530 -							  | type_of_type_definition (t1 $ t2)          = (case type_of_type_definition t1 of SOME x => SOME x | NONE => type_of_type_definition t2)
   1.531 -						in
   1.532 -							case type_of_type_definition ax of
   1.533 -							  SOME T' =>
   1.534 -								let
   1.535 -									val T''      = (domain_type o domain_type) T'
   1.536 -									val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty
   1.537 -								in
   1.538 -									SOME (axname, monomorphic_term typeSubs ax)
   1.539 -								end
   1.540 -							| NONE =>
   1.541 -								get_typedefn axms
   1.542 -						end
   1.543 -						handle ERROR _         => get_typedefn axms
   1.544 -						     | MATCH           => get_typedefn axms
   1.545 -						     | Type.TYPE_MATCH => get_typedefn axms)
   1.546 -				in
   1.547 -					case DatatypePackage.get_datatype thy s of
   1.548 -					  SOME info =>  (* inductive datatype *)
   1.549 -							(* only collect relevant type axioms for the argument types *)
   1.550 -							Library.foldl collect_type_axioms (axs, Ts)
   1.551 +				(case DatatypePackage.get_datatype thy s of
   1.552 +				  SOME info =>  (* inductive datatype *)
   1.553 +						(* only collect relevant type axioms for the argument types *)
   1.554 +						Library.foldl collect_type_axioms (axs, Ts)
   1.555 +				| NONE =>
   1.556 +					(case get_typedef thy T of
   1.557 +					  SOME (axname, ax) =>
   1.558 +						collect_this_axiom (axname, ax) axs
   1.559  					| NONE =>
   1.560 -						(case get_typedefn axioms of
   1.561 -						  SOME (axname, ax) => 
   1.562 -							if member (op aconv) axs ax then
   1.563 -								(* only collect relevant type axioms for the argument types *)
   1.564 -								Library.foldl collect_type_axioms (axs, Ts)
   1.565 -							else
   1.566 -								(immediate_output (" " ^ axname);
   1.567 -								collect_term_axioms (ax :: axs, ax))
   1.568 -						| NONE =>
   1.569 -							(* unspecified type, perhaps introduced with 'typedecl' *)
   1.570 -							(* at least collect relevant type axioms for the argument types *)
   1.571 -							Library.foldl collect_type_axioms (axs, Ts))
   1.572 -				end
   1.573 +						(* unspecified type, perhaps introduced with "typedecl" *)
   1.574 +						(* at least collect relevant type axioms for the argument types *)
   1.575 +						Library.foldl collect_type_axioms (axs, Ts)))
   1.576  			| TFree _                => collect_sort_axioms (axs, T)  (* axiomatic type classes *)
   1.577  			| TVar _                 => collect_sort_axioms (axs, T)  (* axiomatic type classes *)
   1.578  		(* Term.term list * Term.term -> Term.term list *)
   1.579 @@ -590,27 +813,18 @@
   1.580  			| Const ("arbitrary", T)          => collect_type_axioms (axs, T)
   1.581  			| Const ("The", T)                =>
   1.582  				let
   1.583 -					val ax = specialize_type (("The", T), (the o AList.lookup (op =) axioms) "HOL.the_eq_trivial")
   1.584 +					val ax = specialize_type thy ("The", T) ((Option.valOf o AList.lookup (op =) axioms) "HOL.the_eq_trivial")
   1.585  				in
   1.586 -					if member (op aconv) axs ax then
   1.587 -						collect_type_axioms (axs, T)
   1.588 -					else
   1.589 -						(immediate_output " HOL.the_eq_trivial";
   1.590 -						collect_term_axioms (ax :: axs, ax))
   1.591 +					collect_this_axiom ("HOL.the_eq_trivial", ax) axs
   1.592  				end
   1.593  			| Const ("Hilbert_Choice.Eps", T) =>
   1.594  				let
   1.595 -					val ax = specialize_type (("Hilbert_Choice.Eps", T),
   1.596 -                      (the o AList.lookup (op =) axioms) "Hilbert_Choice.someI")
   1.597 +					val ax = specialize_type thy ("Hilbert_Choice.Eps", T) ((Option.valOf o AList.lookup (op =) axioms) "Hilbert_Choice.someI")
   1.598  				in
   1.599 -					if member (op aconv) axs ax then
   1.600 -						collect_type_axioms (axs, T)
   1.601 -					else
   1.602 -						(immediate_output " Hilbert_Choice.someI";
   1.603 -						collect_term_axioms (ax :: axs, ax))
   1.604 +					collect_this_axiom ("Hilbert_Choice.someI", ax) axs
   1.605  				end
   1.606 -			| Const ("All", _) $ t1           => collect_term_axioms (axs, t1)
   1.607 -			| Const ("Ex", _) $ t1            => collect_term_axioms (axs, t1)
   1.608 +			| Const ("All", T)                => collect_type_axioms (axs, T)
   1.609 +			| Const ("Ex", T)                 => collect_type_axioms (axs, T)
   1.610  			| Const ("op =", T)               => collect_type_axioms (axs, T)
   1.611  			| Const ("op &", _)               => axs
   1.612  			| Const ("op |", _)               => axs
   1.613 @@ -632,116 +846,36 @@
   1.614  			| Const ("snd", T)                => collect_type_axioms (axs, T)
   1.615  			(* simply-typed lambda calculus *)
   1.616  			| Const (s, T)                    =>
   1.617 -				let
   1.618 -					(* look up the definition of a constant, as created by "constdefs" *)
   1.619 -					(* string -> Term.typ -> (string * Term.term) list -> (string * Term.term) option *)
   1.620 -					fun get_defn [] =
   1.621 -						NONE
   1.622 -					  | get_defn ((axname, ax)::axms) =
   1.623 -						(let
   1.624 -							val (lhs, _) = Logic.dest_equals ax  (* equations only *)
   1.625 -							val c        = head_of lhs
   1.626 -							val (s', T') = dest_Const c
   1.627 -						in
   1.628 -							if s=s' then
   1.629 -								let
   1.630 -									val typeSubs = Sign.typ_match thy (T', T) Vartab.empty
   1.631 -								in
   1.632 -									SOME (axname, monomorphic_term typeSubs ax)
   1.633 -								end
   1.634 -							else
   1.635 -								get_defn axms
   1.636 -						end
   1.637 -						handle ERROR _         => get_defn axms
   1.638 -						     | TERM _          => get_defn axms
   1.639 -						     | Type.TYPE_MATCH => get_defn axms)
   1.640 -					(* axiomatic type classes *)
   1.641 -					(* unit -> bool *)
   1.642 -					fun is_const_of_class () =
   1.643 -						(* I'm not quite sure if checking the name 's' is sufficient, *)
   1.644 -						(* or if we should also check the type 'T'                    *)
   1.645 -						s mem const_of_class_names
   1.646 -					(* inductive data types *)
   1.647 -					(* unit -> bool *)
   1.648 -					fun is_IDT_constructor () =
   1.649 -						(case body_type T of
   1.650 -						  Type (s', _) =>
   1.651 -							(case DatatypePackage.get_datatype_constrs thy s' of
   1.652 -							  SOME constrs =>
   1.653 -								Library.exists (fn (cname, cty) =>
   1.654 -								cname = s andalso Sign.typ_instance thy (T, cty))
   1.655 -									constrs
   1.656 -							| NONE =>
   1.657 -								false)
   1.658 -						| _  =>
   1.659 -							false)
   1.660 -					(* unit -> bool *)
   1.661 -					fun is_IDT_recursor () =
   1.662 -						(* I'm not quite sure if checking the name 's' is sufficient, *)
   1.663 -						(* or if we should also check the type 'T'                    *)
   1.664 -						member (op =) rec_names s
   1.665 -				in
   1.666 -					if is_const_of_class () then
   1.667 -						(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" and *)
   1.668 -						(* the introduction rule "class.intro" as axioms              *)
   1.669 +					if is_const_of_class thy (s, T) then
   1.670 +						(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *)
   1.671 +						(* and the class definition                               *)
   1.672  						let
   1.673  							val class   = Logic.class_of_const s
   1.674  							val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
   1.675 -							(* Term.term option *)
   1.676 -							val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
   1.677 -							val intro_ax   = (Option.map (fn t => specialize_type ((s, T), t))
   1.678 -								(AList.lookup (op =) axioms (class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
   1.679 -							val axs'       = (case ofclass_ax of NONE => axs | SOME ax => if member (op aconv) axs ax then
   1.680 -									(* collect relevant type axioms *)
   1.681 -									collect_type_axioms (axs, T)
   1.682 -								else
   1.683 -									(immediate_output (" " ^ Sign.string_of_term (sign_of thy) ax);
   1.684 -									collect_term_axioms (ax :: axs, ax)))
   1.685 -							val axs''      = (case intro_ax of NONE => axs' | SOME ax => if member (op aconv) axs' ax then
   1.686 -									(* collect relevant type axioms *)
   1.687 -									collect_type_axioms (axs', T)
   1.688 -								else
   1.689 -									(immediate_output (" " ^ s ^ ".intro");
   1.690 -									collect_term_axioms (ax :: axs', ax)))
   1.691 +							val ax_in   = SOME (specialize_type thy (s, T) inclass)
   1.692 +								(* type match may fail due to sort constraints *)
   1.693 +								handle Type.TYPE_MATCH => NONE
   1.694 +							val ax_1 = Option.map (fn ax => (Sign.string_of_term thy ax, ax)) ax_in
   1.695 +							val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class)
   1.696  						in
   1.697 -							axs''
   1.698 +							collect_type_axioms (fold collect_this_axiom
   1.699 +								(map_filter I [ax_1, ax_2]) axs, T)
   1.700  						end
   1.701 -					else if is_IDT_constructor () then
   1.702 -						(* only collect relevant type axioms *)
   1.703 -						collect_type_axioms (axs, T)
   1.704 -					else if is_IDT_recursor () then
   1.705 +					else if is_IDT_constructor thy (s, T)
   1.706 +						orelse is_IDT_recursor thy (s, T) then
   1.707  						(* only collect relevant type axioms *)
   1.708  						collect_type_axioms (axs, T)
   1.709 -					else (
   1.710 -						case get_defn axioms of
   1.711 -						  SOME (axname, ax) => 
   1.712 -							if member (op aconv) axs ax then
   1.713 -								(* collect relevant type axioms *)
   1.714 -								collect_type_axioms (axs, T)
   1.715 -							else
   1.716 -								(immediate_output (" " ^ axname);
   1.717 -								collect_term_axioms (ax :: axs, ax))
   1.718 -						| NONE =>
   1.719 -							(* collect relevant type axioms *)
   1.720 -							collect_type_axioms (axs, T)
   1.721 -					)
   1.722 -				end
   1.723 -			| Free (_, T)                     => collect_type_axioms (axs, T)
   1.724 -			| Var (_, T)                      => collect_type_axioms (axs, T)
   1.725 -			| Bound i                         => axs
   1.726 -			| Abs (_, T, body)                => collect_term_axioms (collect_type_axioms (axs, T), body)
   1.727 -			| t1 $ t2                         => collect_term_axioms (collect_term_axioms (axs, t1), t2)
   1.728 -		(* universal closure over schematic variables *)
   1.729 -		(* Term.term -> Term.term *)
   1.730 -		fun close_form t =
   1.731 -		let
   1.732 -			(* (Term.indexname * Term.typ) list *)
   1.733 -			val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   1.734 -		in
   1.735 -			Library.foldl
   1.736 -				(fn (t', ((x, i), T)) => (Term.all T) $ Abs (x, T, abstract_over (Var((x, i), T), t')))
   1.737 -				(t, vars)
   1.738 -		end
   1.739 +					else
   1.740 +						(* other constants should have been unfolded, with some *)
   1.741 +						(* exceptions: e.g. Abs_xxx/Rep_xxx functions for       *)
   1.742 +						(* typedefs, or type-class related constants            *)
   1.743 +						(* only collect relevant type axioms *)
   1.744 +						collect_type_axioms (axs, T)
   1.745 +			| Free (_, T)      => collect_type_axioms (axs, T)
   1.746 +			| Var (_, T)       => collect_type_axioms (axs, T)
   1.747 +			| Bound i          => axs
   1.748 +			| Abs (_, T, body) => collect_term_axioms (collect_type_axioms (axs, T), body)
   1.749 +			| t1 $ t2          => collect_term_axioms (collect_term_axioms (axs, t1), t2)
   1.750  		(* Term.term list *)
   1.751  		val result = map close_form (collect_term_axioms ([], t))
   1.752  		val _ = writeln " ...done."
   1.753 @@ -776,7 +910,7 @@
   1.754  						let
   1.755  							val index               = #index info
   1.756  							val descr               = #descr info
   1.757 -							val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
   1.758 +							val (_, dtyps, constrs) = (Option.valOf o AList.lookup (op =) descr) index
   1.759  							val typ_assoc           = dtyps ~~ Ts
   1.760  							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.761  							val _ = (if Library.exists (fn d =>
   1.762 @@ -930,11 +1064,12 @@
   1.763  		(* unit -> unit *)
   1.764  		fun wrapper () =
   1.765  		let
   1.766 -			(* Term.term list *)
   1.767 -			val axioms = collect_axioms thy t
   1.768 +			val u      = unfold_defs thy t
   1.769 +			val _      = writeln ("Unfolded term: " ^ Sign.string_of_term (sign_of thy) u)
   1.770 +			val axioms = collect_axioms thy u
   1.771  			(* Term.typ list *)
   1.772 -			val types  = Library.foldl (fn (acc, t') => acc union (ground_types thy t')) ([], t :: axioms)
   1.773 -			val _      = writeln ("Ground types: "
   1.774 +			val types = Library.foldl (fn (acc, t') => acc union (ground_types thy t')) ([], u :: axioms)
   1.775 +			val _     = writeln ("Ground types: "
   1.776  				^ (if null types then "none."
   1.777  				   else commas (map (Sign.string_of_typ (sign_of thy)) types)))
   1.778  			(* we can only consider fragments of recursive IDTs, so we issue a  *)
   1.779 @@ -947,7 +1082,7 @@
   1.780  						let
   1.781  							val index           = #index info
   1.782  							val descr           = #descr info
   1.783 -							val (_, _, constrs) = (the o AList.lookup (op =) descr) index
   1.784 +							val (_, _, constrs) = (Option.valOf o AList.lookup (op =) descr) index
   1.785  						in
   1.786  							(* recursive datatype? *)
   1.787  							Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs
   1.788 @@ -963,19 +1098,19 @@
   1.789  				val init_model             = (universe, [])
   1.790  				val init_args              = {maxvars = maxvars, def_eq = false, next_idx = 1, bounds = [], wellformed = True}
   1.791  				val _                      = immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
   1.792 -				(* translate 't' and all axioms *)
   1.793 +				(* translate 'u' and all axioms *)
   1.794  				val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
   1.795  					let
   1.796  						val (i, m', a') = interpret thy m a t'
   1.797  					in
   1.798  						(* set 'def_eq' to 'true' *)
   1.799  						((m', {maxvars = #maxvars a', def_eq = true, next_idx = #next_idx a', bounds = #bounds a', wellformed = #wellformed a'}), i)
   1.800 -					end) ((init_model, init_args), t :: axioms)
   1.801 -				(* make 't' either true or false, and make all axioms true, and *)
   1.802 +					end) ((init_model, init_args), u :: axioms)
   1.803 +				(* make 'u' either true or false, and make all axioms true, and *)
   1.804  				(* add the well-formedness side condition                       *)
   1.805 -				val fm_t  = (if negate then toFalse else toTrue) (hd intrs)
   1.806 +				val fm_u  = (if negate then toFalse else toTrue) (hd intrs)
   1.807  				val fm_ax = PropLogic.all (map toTrue (tl intrs))
   1.808 -				val fm    = PropLogic.all [#wellformed args, fm_ax, fm_t]
   1.809 +				val fm    = PropLogic.all [#wellformed args, fm_ax, fm_u]
   1.810  			in
   1.811  				immediate_output " invoking SAT solver...";
   1.812  				(case SatSolver.invoke_solver satsolver fm of
   1.813 @@ -1317,10 +1452,11 @@
   1.814  
   1.815  	fun eta_expand t i =
   1.816  	let
   1.817 -		val Ts = binder_types (fastype_of t)
   1.818 +		val Ts = Term.binder_types (Term.fastype_of t)
   1.819 +		val t' = Term.incr_boundvars i t
   1.820  	in
   1.821 -		foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
   1.822 -			(list_comb (t, map Bound (i-1 downto 0))) (Library.take (i, Ts))
   1.823 +		foldr (fn (T, term) => Abs ("<eta_expand>", T, term))
   1.824 +			(Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i))
   1.825  	end;
   1.826  
   1.827  (* ------------------------------------------------------------------------- *)
   1.828 @@ -1377,7 +1513,7 @@
   1.829  			(* unit -> (interpretation * model * arguments) option *)
   1.830  			fun interpret_groundtype () =
   1.831  			let
   1.832 -				val size = (if T = Term.propT then 2 else (the o AList.lookup (op =) typs) T)                    (* the model MUST specify a size for ground types *)
   1.833 +				val size = (if T = Term.propT then 2 else (Option.valOf o AList.lookup (op =) typs) T)                    (* the model MUST specify a size for ground types *)
   1.834  				val next = next_idx+size
   1.835  				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
   1.836  				(* prop_formula list *)
   1.837 @@ -1473,12 +1609,13 @@
   1.838  
   1.839  	fun Pure_interpreter thy model args t =
   1.840  		case t of
   1.841 -		  Const ("all", _) $ t1 =>  (* in the meta-logic, 'all' MUST be followed by an argument term *)
   1.842 +		  Const ("all", _) $ t1 =>
   1.843  			let
   1.844  				val (i, m, a) = interpret thy model args t1
   1.845  			in
   1.846  				case i of
   1.847  				  Node xs =>
   1.848 +					(* 3-valued logic *)
   1.849  					let
   1.850  						val fmTrue  = PropLogic.all (map toTrue xs)
   1.851  						val fmFalse = PropLogic.exists (map toFalse xs)
   1.852 @@ -1488,6 +1625,8 @@
   1.853  				| _ =>
   1.854  					raise REFUTE ("Pure_interpreter", "\"all\" is not followed by a function")
   1.855  			end
   1.856 +		| Const ("all", _) =>
   1.857 +			SOME (interpret thy model args (eta_expand t 1))
   1.858  		| Const ("==", _) $ t1 $ t2 =>
   1.859  			let
   1.860  				val (i1, m1, a1) = interpret thy model args t1
   1.861 @@ -1496,8 +1635,24 @@
   1.862  				(* we use either 'make_def_equality' or 'make_equality' *)
   1.863  				SOME ((if #def_eq args then make_def_equality else make_equality) (i1, i2), m2, a2)
   1.864  			end
   1.865 -		| Const ("==>", _) =>  (* simpler than translating 'Const ("==>", _) $ t1 $ t2' *)
   1.866 -			SOME (Node [Node [TT, FF], Node [TT, TT]], model, args)
   1.867 +		| Const ("==", _) $ t1 =>
   1.868 +			SOME (interpret thy model args (eta_expand t 1))
   1.869 +		| Const ("==", _) =>
   1.870 +			SOME (interpret thy model args (eta_expand t 2))
   1.871 +		| Const ("==>", _) $ t1 $ t2 =>
   1.872 +			(* 3-valued logic *)
   1.873 +			let
   1.874 +				val (i1, m1, a1) = interpret thy model args t1
   1.875 +				val (i2, m2, a2) = interpret thy m1 a1 t2
   1.876 +				val fmTrue       = PropLogic.SOr (toFalse i1, toTrue i2)
   1.877 +				val fmFalse      = PropLogic.SAnd (toTrue i1, toFalse i2)
   1.878 +			in
   1.879 +				SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.880 +			end
   1.881 +		| Const ("==>", _) $ t1 =>
   1.882 +			SOME (interpret thy model args (eta_expand t 1))
   1.883 +		| Const ("==>", _) =>
   1.884 +			SOME (interpret thy model args (eta_expand t 2))
   1.885  		| _ => NONE;
   1.886  
   1.887  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.888 @@ -1506,8 +1661,7 @@
   1.889  	(* ------------------------------------------------------------------------- *)
   1.890  	(* Providing interpretations directly is more efficient than unfolding the   *)
   1.891  	(* logical constants.  In HOL however, logical constants can themselves be   *)
   1.892 -	(* arguments.  "All" and "Ex" are then translated just like any other        *)
   1.893 -	(* constant, with the relevant axiom being added by 'collect_axioms'.        *)
   1.894 +	(* arguments.  They are then translated using eta-expansion.                 *)
   1.895  	(* ------------------------------------------------------------------------- *)
   1.896  		case t of
   1.897  		  Const ("Trueprop", _) =>
   1.898 @@ -1518,15 +1672,13 @@
   1.899  			SOME (TT, model, args)
   1.900  		| Const ("False", _) =>  (* redundant, since 'False' is also an IDT constructor *)
   1.901  			SOME (FF, model, args)
   1.902 -		| Const ("All", _) $ t1 =>
   1.903 -		(* if "All" occurs without an argument (i.e. as argument to a higher-order *)
   1.904 -		(* function or predicate), it is handled by the 'stlc_interpreter' (i.e.   *)
   1.905 -		(* by unfolding its definition)                                            *)
   1.906 +		| Const ("All", _) $ t1 =>  (* similar to "all" (Pure) *)
   1.907  			let
   1.908  				val (i, m, a) = interpret thy model args t1
   1.909  			in
   1.910  				case i of
   1.911  				  Node xs =>
   1.912 +					(* 3-valued logic *)
   1.913  					let
   1.914  						val fmTrue  = PropLogic.all (map toTrue xs)
   1.915  						val fmFalse = PropLogic.exists (map toFalse xs)
   1.916 @@ -1536,15 +1688,15 @@
   1.917  				| _ =>
   1.918  					raise REFUTE ("HOLogic_interpreter", "\"All\" is followed by a non-function")
   1.919  			end
   1.920 +		| Const ("All", _) =>
   1.921 +			SOME (interpret thy model args (eta_expand t 1))
   1.922  		| Const ("Ex", _) $ t1 =>
   1.923 -		(* if "Ex" occurs without an argument (i.e. as argument to a higher-order  *)
   1.924 -		(* function or predicate), it is handled by the 'stlc_interpreter' (i.e.   *)
   1.925 -		(* by unfolding its definition)                                            *)
   1.926  			let
   1.927  				val (i, m, a) = interpret thy model args t1
   1.928  			in
   1.929  				case i of
   1.930  				  Node xs =>
   1.931 +					(* 3-valued logic *)
   1.932  					let
   1.933  						val fmTrue  = PropLogic.exists (map toTrue xs)
   1.934  						val fmFalse = PropLogic.all (map toFalse xs)
   1.935 @@ -1554,7 +1706,9 @@
   1.936  				| _ =>
   1.937  					raise REFUTE ("HOLogic_interpreter", "\"Ex\" is followed by a non-function")
   1.938  			end
   1.939 -		| Const ("op =", _) $ t1 $ t2 =>
   1.940 +		| Const ("Ex", _) =>
   1.941 +			SOME (interpret thy model args (eta_expand t 1))
   1.942 +		| Const ("op =", _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)
   1.943  			let
   1.944  				val (i1, m1, a1) = interpret thy model args t1
   1.945  				val (i2, m2, a2) = interpret thy m1 a1 t2
   1.946 @@ -1579,6 +1733,8 @@
   1.947  			SOME (interpret thy model args (eta_expand t 1))
   1.948  		| Const ("op &", _) =>
   1.949  			SOME (interpret thy model args (eta_expand t 2))
   1.950 +			(* this would make "undef" propagate, even for formulae like *)
   1.951 +			(* "False & undef":                                          *)
   1.952  			(* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)
   1.953  		| Const ("op |", _) $ t1 $ t2 =>
   1.954  			(* 3-valued logic *)
   1.955 @@ -1594,8 +1750,10 @@
   1.956  			SOME (interpret thy model args (eta_expand t 1))
   1.957  		| Const ("op |", _) =>
   1.958  			SOME (interpret thy model args (eta_expand t 2))
   1.959 +			(* this would make "undef" propagate, even for formulae like *)
   1.960 +			(* "True | undef":                                           *)
   1.961  			(* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
   1.962 -		| Const ("op -->", _) $ t1 $ t2 =>
   1.963 +		| Const ("op -->", _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
   1.964  			(* 3-valued logic *)
   1.965  			let
   1.966  				val (i1, m1, a1) = interpret thy model args t1
   1.967 @@ -1605,9 +1763,13 @@
   1.968  			in
   1.969  				SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.970  			end
   1.971 +		| Const ("op -->", _) $ t1 =>
   1.972 +			SOME (interpret thy model args (eta_expand t 1))
   1.973  		| Const ("op -->", _) =>
   1.974 +			SOME (interpret thy model args (eta_expand t 2))
   1.975 +			(* this would make "undef" propagate, even for formulae like *)
   1.976 +			(* "False --> undef":                                        *)
   1.977  			(* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *)
   1.978 -			SOME (interpret thy model args (eta_expand t 2))
   1.979  		| _ => NONE;
   1.980  
   1.981  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
   1.982 @@ -1679,7 +1841,7 @@
   1.983  						let
   1.984  							val index               = #index info
   1.985  							val descr               = #descr info
   1.986 -							val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
   1.987 +							val (_, dtyps, constrs) = (Option.valOf o AList.lookup (op =) descr) index
   1.988  							val typ_assoc           = dtyps ~~ Ts
   1.989  							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.990  							val _ = (if Library.exists (fn d =>
   1.991 @@ -1747,7 +1909,7 @@
   1.992  						let
   1.993  							val index               = #index info
   1.994  							val descr               = #descr info
   1.995 -							val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
   1.996 +							val (_, dtyps, constrs) = (Option.valOf o AList.lookup (op =) descr) index
   1.997  							val typ_assoc           = dtyps ~~ Ts'
   1.998  							(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.999  							val _ = (if Library.exists (fn d =>
  1.1000 @@ -1925,8 +2087,8 @@
  1.1001  						let
  1.1002  							val index              = #index info
  1.1003  							val descr              = #descr info
  1.1004 -							val (dtname, dtyps, _) = (the o AList.lookup (op =) descr) index
  1.1005 -							(* number of all constructors, including those of different           *)
  1.1006 +							val (dtname, dtyps, _) = (Option.valOf o AList.lookup (op =) descr) index
  1.1007 +							(* number of all constructors, including those of ({({(a0, True)}, False), ({(a0, False)}, False)}, True)different           *)
  1.1008  							(* (mutually recursive) datatypes within the same descriptor 'descr'  *)
  1.1009  							val mconstrs_count     = sum (map (fn (_, (_, _, cs)) => length cs) descr)
  1.1010  							val params_count       = length params
  1.1011 @@ -2016,7 +2178,7 @@
  1.1012  												  SOME args => (n, args)
  1.1013  												| NONE      => get_cargs_rec (n+1, xs))
  1.1014  										in
  1.1015 -											get_cargs_rec (0, (the o AList.lookup (op =) mc_intrs) idx)
  1.1016 +											get_cargs_rec (0, (Option.valOf o AList.lookup (op =) mc_intrs) idx)
  1.1017  										end
  1.1018  									(* returns the number of constructors in datatypes that occur in *)
  1.1019  									(* the descriptor 'descr' before the datatype given by 'idx'     *)
  1.1020 @@ -2036,7 +2198,7 @@
  1.1021  									(* where 'idx' gives the datatype and 'elem' the element of it             *)
  1.1022  									(* int -> int -> interpretation *)
  1.1023  									fun compute_array_entry idx elem =
  1.1024 -										case Array.sub ((the o AList.lookup (op =) INTRS) idx, elem) of
  1.1025 +										case Array.sub ((Option.valOf o AList.lookup (op =) INTRS) idx, elem) of
  1.1026  										  SOME result =>
  1.1027  											(* simply return the previously computed result *)
  1.1028  											result
  1.1029 @@ -2054,7 +2216,7 @@
  1.1030  												(* select the correct subtree of the parameter corresponding to constructor 'c' *)
  1.1031  												val p_intr = select_subtree (List.nth (p_intrs, get_coffset idx + c), args)
  1.1032  												(* find the indices of the constructor's recursive arguments *)
  1.1033 -												val (_, _, constrs) = (the o AList.lookup (op =) descr) idx
  1.1034 +												val (_, _, constrs) = (Option.valOf o AList.lookup (op =) descr) idx
  1.1035  												val constr_args     = (snd o List.nth) (constrs, c)
  1.1036  												val rec_args        = List.filter (DatatypeAux.is_rec_type o fst) (constr_args ~~ args)
  1.1037  												val rec_args'       = map (fn (dtyp, elem) => (DatatypeAux.dest_DtRec dtyp, elem)) rec_args
  1.1038 @@ -2062,7 +2224,7 @@
  1.1039  												val result = foldl (fn ((idx, elem), intr) =>
  1.1040  													interpretation_apply (intr, compute_array_entry idx elem)) p_intr rec_args'
  1.1041  												(* update 'INTRS' *)
  1.1042 -												val _ = Array.update ((the o AList.lookup (op =) INTRS) idx, elem, SOME result)
  1.1043 +												val _ = Array.update ((Option.valOf o AList.lookup (op =) INTRS) idx, elem, SOME result)
  1.1044  											in
  1.1045  												result
  1.1046  											end
  1.1047 @@ -2081,13 +2243,13 @@
  1.1048  										in
  1.1049  											modifyi_loop 0
  1.1050  										end
  1.1051 -									val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((the o AList.lookup (op =) INTRS) index)
  1.1052 +									val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((Option.valOf o AList.lookup (op =) INTRS) index)
  1.1053  									(* 'a Array.array -> 'a list *)
  1.1054  									fun toList arr =
  1.1055  										Array.foldr op:: [] arr
  1.1056  								in
  1.1057  									(* return the part of 'INTRS' that corresponds to the current datatype *)
  1.1058 -									SOME ((Node o map the o toList o the o AList.lookup (op =) INTRS) index, model', args')
  1.1059 +									SOME ((Node o map Option.valOf o toList o Option.valOf o AList.lookup (op =) INTRS) index, model', args')
  1.1060  								end
  1.1061  						end
  1.1062  					else
  1.1063 @@ -2576,7 +2738,7 @@
  1.1064  					val (typs, _)           = model
  1.1065  					val index               = #index info
  1.1066  					val descr               = #descr info
  1.1067 -					val (_, dtyps, constrs) = (the o AList.lookup (op =) descr) index
  1.1068 +					val (_, dtyps, constrs) = (Option.valOf o AList.lookup (op =) descr) index
  1.1069  					val typ_assoc           = dtyps ~~ Ts
  1.1070  					(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1.1071  					val _ = (if Library.exists (fn d =>
     2.1 --- a/src/HOL/ex/Refute_Examples.thy	Wed Jan 03 22:59:30 2007 +0100
     2.2 +++ b/src/HOL/ex/Refute_Examples.thy	Thu Jan 04 00:12:30 2007 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      HOL/ex/Refute_Examples.thy
     2.5      ID:         $Id$
     2.6      Author:     Tjark Weber
     2.7 -    Copyright   2003-2005
     2.8 +    Copyright   2003-2007
     2.9  *)
    2.10  
    2.11  (* See 'HOL/Refute.thy' for help. *)
    2.12 @@ -24,6 +24,8 @@
    2.13    refute [satsolver="dpll"] 2  -- {* ... and specify a subgoal at the same time *}
    2.14  oops
    2.15  
    2.16 +(******************************************************************************)
    2.17 +
    2.18  section {* Examples and Test Cases *}
    2.19  
    2.20  subsection {* Propositional logic *}
    2.21 @@ -65,6 +67,8 @@
    2.22    refute
    2.23  oops
    2.24  
    2.25 +(******************************************************************************)
    2.26 +
    2.27  subsection {* Predicate logic *}
    2.28  
    2.29  lemma "P x y z"
    2.30 @@ -79,6 +83,8 @@
    2.31    refute
    2.32  oops
    2.33  
    2.34 +(******************************************************************************)
    2.35 +
    2.36  subsection {* Equality *}
    2.37  
    2.38  lemma "P = True"
    2.39 @@ -111,6 +117,8 @@
    2.40    refute
    2.41  oops
    2.42  
    2.43 +(******************************************************************************)
    2.44 +
    2.45  subsection {* First-Order Logic *}
    2.46  
    2.47  lemma "\<exists>x. P x"
    2.48 @@ -203,6 +211,8 @@
    2.49    refute
    2.50  oops
    2.51  
    2.52 +(******************************************************************************)
    2.53 +
    2.54  subsection {* Higher-Order Logic *}
    2.55  
    2.56  lemma "\<exists>P. P"
    2.57 @@ -227,15 +237,15 @@
    2.58    refute
    2.59  oops
    2.60  
    2.61 -lemma "P All"
    2.62 +lemma "x \<noteq> All"
    2.63    refute
    2.64  oops
    2.65  
    2.66 -lemma "P Ex"
    2.67 +lemma "x \<noteq> Ex"
    2.68    refute
    2.69  oops
    2.70  
    2.71 -lemma "P Ex1"
    2.72 +lemma "x \<noteq> Ex1"
    2.73    refute
    2.74  oops
    2.75  
    2.76 @@ -302,6 +312,8 @@
    2.77    apply (fast intro: ext)
    2.78  done
    2.79  
    2.80 +(******************************************************************************)
    2.81 +
    2.82  subsection {* Meta-logic *}
    2.83  
    2.84  lemma "!!x. P x"
    2.85 @@ -320,6 +332,20 @@
    2.86    refute
    2.87  oops
    2.88  
    2.89 +lemma "(x == all) \<Longrightarrow> False"
    2.90 +  refute
    2.91 +oops
    2.92 +
    2.93 +lemma "(x == (op ==)) \<Longrightarrow> False"
    2.94 +  refute
    2.95 +oops
    2.96 +
    2.97 +lemma "(x == (op \<Longrightarrow>)) \<Longrightarrow> False"
    2.98 +  refute
    2.99 +oops
   2.100 +
   2.101 +(******************************************************************************)
   2.102 +
   2.103  subsection {* Schematic variables *}
   2.104  
   2.105  lemma "?P"
   2.106 @@ -332,6 +358,8 @@
   2.107    apply auto
   2.108  done
   2.109  
   2.110 +(******************************************************************************)
   2.111 +
   2.112  subsection {* Abstractions *}
   2.113  
   2.114  lemma "(\<lambda>x. x) = (\<lambda>x. y)"
   2.115 @@ -347,6 +375,8 @@
   2.116    apply simp
   2.117  done
   2.118  
   2.119 +(******************************************************************************)
   2.120 +
   2.121  subsection {* Sets *}
   2.122  
   2.123  lemma "P (A::'a set)"
   2.124 @@ -390,6 +420,8 @@
   2.125    refute
   2.126  oops
   2.127  
   2.128 +(******************************************************************************)
   2.129 +
   2.130  subsection {* arbitrary *}
   2.131  
   2.132  lemma "arbitrary"
   2.133 @@ -408,6 +440,8 @@
   2.134    refute
   2.135  oops
   2.136  
   2.137 +(******************************************************************************)
   2.138 +
   2.139  subsection {* The *}
   2.140  
   2.141  lemma "The P"
   2.142 @@ -430,6 +464,8 @@
   2.143    refute
   2.144  oops
   2.145  
   2.146 +(******************************************************************************)
   2.147 +
   2.148  subsection {* Eps *}
   2.149  
   2.150  lemma "Eps P"
   2.151 @@ -968,11 +1004,11 @@
   2.152    refute
   2.153  oops
   2.154  
   2.155 -lemma "a @ [] = b @ []"
   2.156 +lemma "xs @ [] = ys @ []"
   2.157    refute
   2.158  oops
   2.159  
   2.160 -lemma "a @ b = b @ a"
   2.161 +lemma "xs @ ys = ys @ xs"
   2.162    refute
   2.163  oops
   2.164  
   2.165 @@ -1000,7 +1036,7 @@
   2.166    refute
   2.167  oops
   2.168  
   2.169 -text {* The axiom of this type class does not contain any type variables, but is internally converted into one that does: *}
   2.170 +text {* The axiom of this type class does not contain any type variables: *}
   2.171  
   2.172  axclass classB
   2.173    classB_ax: "P | ~ P"