src/HOL/Library/refute.ML
changeset 49985 5b4b0e4e5205
parent 48902 44a6967240b7
child 50530 6266e44b3396
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/refute.ML	Wed Oct 31 11:23:21 2012 +0100
     1.3 @@ -0,0 +1,3229 @@
     1.4 +(*  Title:      HOL/Tools/refute.ML
     1.5 +    Author:     Tjark Weber, TU Muenchen
     1.6 +
     1.7 +Finite model generation for HOL formulas, using a SAT solver.
     1.8 +*)
     1.9 +
    1.10 +(* ------------------------------------------------------------------------- *)
    1.11 +(* Declares the 'REFUTE' signature as well as a structure 'Refute'.          *)
    1.12 +(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'.  *)
    1.13 +(* ------------------------------------------------------------------------- *)
    1.14 +
    1.15 +signature REFUTE =
    1.16 +sig
    1.17 +
    1.18 +  exception REFUTE of string * string
    1.19 +
    1.20 +(* ------------------------------------------------------------------------- *)
    1.21 +(* Model/interpretation related code (translation HOL -> propositional logic *)
    1.22 +(* ------------------------------------------------------------------------- *)
    1.23 +
    1.24 +  type params
    1.25 +  type interpretation
    1.26 +  type model
    1.27 +  type arguments
    1.28 +
    1.29 +  exception MAXVARS_EXCEEDED
    1.30 +
    1.31 +  val add_interpreter : string -> (Proof.context -> model -> arguments -> term ->
    1.32 +    (interpretation * model * arguments) option) -> theory -> theory
    1.33 +  val add_printer : string -> (Proof.context -> model -> typ ->
    1.34 +    interpretation -> (int -> bool) -> term option) -> theory -> theory
    1.35 +
    1.36 +  val interpret : Proof.context -> model -> arguments -> term ->
    1.37 +    (interpretation * model * arguments)
    1.38 +
    1.39 +  val print : Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term
    1.40 +  val print_model : Proof.context -> model -> (int -> bool) -> string
    1.41 +
    1.42 +(* ------------------------------------------------------------------------- *)
    1.43 +(* Interface                                                                 *)
    1.44 +(* ------------------------------------------------------------------------- *)
    1.45 +
    1.46 +  val set_default_param  : (string * string) -> theory -> theory
    1.47 +  val get_default_param  : Proof.context -> string -> string option
    1.48 +  val get_default_params : Proof.context -> (string * string) list
    1.49 +  val actual_params      : Proof.context -> (string * string) list -> params
    1.50 +
    1.51 +  val find_model :
    1.52 +    Proof.context -> params -> term list -> term -> bool -> string
    1.53 +
    1.54 +  (* tries to find a model for a formula: *)
    1.55 +  val satisfy_term :
    1.56 +    Proof.context -> (string * string) list -> term list -> term -> string
    1.57 +  (* tries to find a model that refutes a formula: *)
    1.58 +  val refute_term :
    1.59 +    Proof.context -> (string * string) list -> term list -> term -> string
    1.60 +  val refute_goal :
    1.61 +    Proof.context -> (string * string) list -> thm -> int -> string
    1.62 +
    1.63 +  val setup : theory -> theory
    1.64 +
    1.65 +(* ------------------------------------------------------------------------- *)
    1.66 +(* Additional functions used by Nitpick (to be factored out)                 *)
    1.67 +(* ------------------------------------------------------------------------- *)
    1.68 +
    1.69 +  val get_classdef : theory -> string -> (string * term) option
    1.70 +  val norm_rhs : term -> term
    1.71 +  val get_def : theory -> string * typ -> (string * term) option
    1.72 +  val get_typedef : theory -> typ -> (string * term) option
    1.73 +  val is_IDT_constructor : theory -> string * typ -> bool
    1.74 +  val is_IDT_recursor : theory -> string * typ -> bool
    1.75 +  val is_const_of_class: theory -> string * typ -> bool
    1.76 +  val string_of_typ : typ -> string
    1.77 +end;
    1.78 +
    1.79 +structure Refute : REFUTE =
    1.80 +struct
    1.81 +
    1.82 +open Prop_Logic;
    1.83 +
    1.84 +(* We use 'REFUTE' only for internal error conditions that should    *)
    1.85 +(* never occur in the first place (i.e. errors caused by bugs in our *)
    1.86 +(* code).  Otherwise (e.g. to indicate invalid input data) we use    *)
    1.87 +(* 'error'.                                                          *)
    1.88 +exception REFUTE of string * string;  (* ("in function", "cause") *)
    1.89 +
    1.90 +(* should be raised by an interpreter when more variables would be *)
    1.91 +(* required than allowed by 'maxvars'                              *)
    1.92 +exception MAXVARS_EXCEEDED;
    1.93 +
    1.94 +
    1.95 +(* ------------------------------------------------------------------------- *)
    1.96 +(* TREES                                                                     *)
    1.97 +(* ------------------------------------------------------------------------- *)
    1.98 +
    1.99 +(* ------------------------------------------------------------------------- *)
   1.100 +(* tree: implements an arbitrarily (but finitely) branching tree as a list   *)
   1.101 +(*       of (lists of ...) elements                                          *)
   1.102 +(* ------------------------------------------------------------------------- *)
   1.103 +
   1.104 +datatype 'a tree =
   1.105 +    Leaf of 'a
   1.106 +  | Node of ('a tree) list;
   1.107 +
   1.108 +(* ('a -> 'b) -> 'a tree -> 'b tree *)
   1.109 +
   1.110 +fun tree_map f tr =
   1.111 +  case tr of
   1.112 +    Leaf x  => Leaf (f x)
   1.113 +  | Node xs => Node (map (tree_map f) xs);
   1.114 +
   1.115 +(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
   1.116 +
   1.117 +fun tree_foldl f =
   1.118 +  let
   1.119 +    fun itl (e, Leaf x)  = f(e,x)
   1.120 +      | itl (e, Node xs) = Library.foldl (tree_foldl f) (e,xs)
   1.121 +  in
   1.122 +    itl
   1.123 +  end;
   1.124 +
   1.125 +(* 'a tree * 'b tree -> ('a * 'b) tree *)
   1.126 +
   1.127 +fun tree_pair (t1, t2) =
   1.128 +  case t1 of
   1.129 +    Leaf x =>
   1.130 +      (case t2 of
   1.131 +          Leaf y => Leaf (x,y)
   1.132 +        | Node _ => raise REFUTE ("tree_pair",
   1.133 +            "trees are of different height (second tree is higher)"))
   1.134 +  | Node xs =>
   1.135 +      (case t2 of
   1.136 +          (* '~~' will raise an exception if the number of branches in   *)
   1.137 +          (* both trees is different at the current node                 *)
   1.138 +          Node ys => Node (map tree_pair (xs ~~ ys))
   1.139 +        | Leaf _  => raise REFUTE ("tree_pair",
   1.140 +            "trees are of different height (first tree is higher)"));
   1.141 +
   1.142 +(* ------------------------------------------------------------------------- *)
   1.143 +(* params: parameters that control the translation into a propositional      *)
   1.144 +(*         formula/model generation                                          *)
   1.145 +(*                                                                           *)
   1.146 +(* The following parameters are supported (and required (!), except for      *)
   1.147 +(* "sizes" and "expect"):                                                    *)
   1.148 +(*                                                                           *)
   1.149 +(* Name          Type    Description                                         *)
   1.150 +(*                                                                           *)
   1.151 +(* "sizes"       (string * int) list                                         *)
   1.152 +(*                       Size of ground types (e.g. 'a=2), or depth of IDTs. *)
   1.153 +(* "minsize"     int     If >0, minimal size of each ground type/IDT depth.  *)
   1.154 +(* "maxsize"     int     If >0, maximal size of each ground type/IDT depth.  *)
   1.155 +(* "maxvars"     int     If >0, use at most 'maxvars' Boolean variables      *)
   1.156 +(*                       when transforming the term into a propositional     *)
   1.157 +(*                       formula.                                            *)
   1.158 +(* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
   1.159 +(* "satsolver"   string  SAT solver to be used.                              *)
   1.160 +(* "no_assms"    bool    If "true", assumptions in structured proofs are     *)
   1.161 +(*                       not considered.                                     *)
   1.162 +(* "expect"      string  Expected result ("genuine", "potential", "none", or *)
   1.163 +(*                       "unknown").                                         *)
   1.164 +(* ------------------------------------------------------------------------- *)
   1.165 +
   1.166 +type params =
   1.167 +  {
   1.168 +    sizes    : (string * int) list,
   1.169 +    minsize  : int,
   1.170 +    maxsize  : int,
   1.171 +    maxvars  : int,
   1.172 +    maxtime  : int,
   1.173 +    satsolver: string,
   1.174 +    no_assms : bool,
   1.175 +    expect   : string
   1.176 +  };
   1.177 +
   1.178 +(* ------------------------------------------------------------------------- *)
   1.179 +(* interpretation: a term's interpretation is given by a variable of type    *)
   1.180 +(*                 'interpretation'                                          *)
   1.181 +(* ------------------------------------------------------------------------- *)
   1.182 +
   1.183 +type interpretation =
   1.184 +  prop_formula list tree;
   1.185 +
   1.186 +(* ------------------------------------------------------------------------- *)
   1.187 +(* model: a model specifies the size of types and the interpretation of      *)
   1.188 +(*        terms                                                              *)
   1.189 +(* ------------------------------------------------------------------------- *)
   1.190 +
   1.191 +type model =
   1.192 +  (typ * int) list * (term * interpretation) list;
   1.193 +
   1.194 +(* ------------------------------------------------------------------------- *)
   1.195 +(* arguments: additional arguments required during interpretation of terms   *)
   1.196 +(* ------------------------------------------------------------------------- *)
   1.197 +
   1.198 +type arguments =
   1.199 +  {
   1.200 +    (* just passed unchanged from 'params': *)
   1.201 +    maxvars   : int,
   1.202 +    (* whether to use 'make_equality' or 'make_def_equality': *)
   1.203 +    def_eq    : bool,
   1.204 +    (* the following may change during the translation: *)
   1.205 +    next_idx  : int,
   1.206 +    bounds    : interpretation list,
   1.207 +    wellformed: prop_formula
   1.208 +  };
   1.209 +
   1.210 +structure Data = Theory_Data
   1.211 +(
   1.212 +  type T =
   1.213 +    {interpreters: (string * (Proof.context -> model -> arguments -> term ->
   1.214 +      (interpretation * model * arguments) option)) list,
   1.215 +     printers: (string * (Proof.context -> model -> typ -> interpretation ->
   1.216 +      (int -> bool) -> term option)) list,
   1.217 +     parameters: string Symtab.table};
   1.218 +  val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
   1.219 +  val extend = I;
   1.220 +  fun merge
   1.221 +    ({interpreters = in1, printers = pr1, parameters = pa1},
   1.222 +     {interpreters = in2, printers = pr2, parameters = pa2}) : T =
   1.223 +    {interpreters = AList.merge (op =) (K true) (in1, in2),
   1.224 +     printers = AList.merge (op =) (K true) (pr1, pr2),
   1.225 +     parameters = Symtab.merge (op =) (pa1, pa2)};
   1.226 +);
   1.227 +
   1.228 +val get_data = Data.get o Proof_Context.theory_of;
   1.229 +
   1.230 +
   1.231 +(* ------------------------------------------------------------------------- *)
   1.232 +(* interpret: interprets the term 't' using a suitable interpreter; returns  *)
   1.233 +(*            the interpretation and a (possibly extended) model that keeps  *)
   1.234 +(*            track of the interpretation of subterms                        *)
   1.235 +(* ------------------------------------------------------------------------- *)
   1.236 +
   1.237 +fun interpret ctxt model args t =
   1.238 +  case get_first (fn (_, f) => f ctxt model args t)
   1.239 +      (#interpreters (get_data ctxt)) of
   1.240 +    NONE => raise REFUTE ("interpret",
   1.241 +      "no interpreter for term " ^ quote (Syntax.string_of_term ctxt t))
   1.242 +  | SOME x => x;
   1.243 +
   1.244 +(* ------------------------------------------------------------------------- *)
   1.245 +(* print: converts the interpretation 'intr', which must denote a term of    *)
   1.246 +(*        type 'T', into a term using a suitable printer                     *)
   1.247 +(* ------------------------------------------------------------------------- *)
   1.248 +
   1.249 +fun print ctxt model T intr assignment =
   1.250 +  case get_first (fn (_, f) => f ctxt model T intr assignment)
   1.251 +      (#printers (get_data ctxt)) of
   1.252 +    NONE => raise REFUTE ("print",
   1.253 +      "no printer for type " ^ quote (Syntax.string_of_typ ctxt T))
   1.254 +  | SOME x => x;
   1.255 +
   1.256 +(* ------------------------------------------------------------------------- *)
   1.257 +(* print_model: turns the model into a string, using a fixed interpretation  *)
   1.258 +(*              (given by an assignment for Boolean variables) and suitable  *)
   1.259 +(*              printers                                                     *)
   1.260 +(* ------------------------------------------------------------------------- *)
   1.261 +
   1.262 +fun print_model ctxt model assignment =
   1.263 +  let
   1.264 +    val (typs, terms) = model
   1.265 +    val typs_msg =
   1.266 +      if null typs then
   1.267 +        "empty universe (no type variables in term)\n"
   1.268 +      else
   1.269 +        "Size of types: " ^ commas (map (fn (T, i) =>
   1.270 +          Syntax.string_of_typ ctxt T ^ ": " ^ string_of_int i) typs) ^ "\n"
   1.271 +    val show_consts_msg =
   1.272 +      if not (Config.get ctxt show_consts) andalso Library.exists (is_Const o fst) terms then
   1.273 +        "enable \"show_consts\" to show the interpretation of constants\n"
   1.274 +      else
   1.275 +        ""
   1.276 +    val terms_msg =
   1.277 +      if null terms then
   1.278 +        "empty interpretation (no free variables in term)\n"
   1.279 +      else
   1.280 +        cat_lines (map_filter (fn (t, intr) =>
   1.281 +          (* print constants only if 'show_consts' is true *)
   1.282 +          if Config.get ctxt show_consts orelse not (is_Const t) then
   1.283 +            SOME (Syntax.string_of_term ctxt t ^ ": " ^
   1.284 +              Syntax.string_of_term ctxt
   1.285 +                (print ctxt model (Term.type_of t) intr assignment))
   1.286 +          else
   1.287 +            NONE) terms) ^ "\n"
   1.288 +  in
   1.289 +    typs_msg ^ show_consts_msg ^ terms_msg
   1.290 +  end;
   1.291 +
   1.292 +
   1.293 +(* ------------------------------------------------------------------------- *)
   1.294 +(* PARAMETER MANAGEMENT                                                      *)
   1.295 +(* ------------------------------------------------------------------------- *)
   1.296 +
   1.297 +fun add_interpreter name f = Data.map (fn {interpreters, printers, parameters} =>
   1.298 +  case AList.lookup (op =) interpreters name of
   1.299 +    NONE => {interpreters = (name, f) :: interpreters,
   1.300 +      printers = printers, parameters = parameters}
   1.301 +  | SOME _ => error ("Interpreter " ^ name ^ " already declared"));
   1.302 +
   1.303 +fun add_printer name f = Data.map (fn {interpreters, printers, parameters} =>
   1.304 +  case AList.lookup (op =) printers name of
   1.305 +    NONE => {interpreters = interpreters,
   1.306 +      printers = (name, f) :: printers, parameters = parameters}
   1.307 +  | SOME _ => error ("Printer " ^ name ^ " already declared"));
   1.308 +
   1.309 +(* ------------------------------------------------------------------------- *)
   1.310 +(* set_default_param: stores the '(name, value)' pair in Data's              *)
   1.311 +(*                    parameter table                                        *)
   1.312 +(* ------------------------------------------------------------------------- *)
   1.313 +
   1.314 +fun set_default_param (name, value) = Data.map
   1.315 +  (fn {interpreters, printers, parameters} =>
   1.316 +    {interpreters = interpreters, printers = printers,
   1.317 +      parameters = Symtab.update (name, value) parameters});
   1.318 +
   1.319 +(* ------------------------------------------------------------------------- *)
   1.320 +(* get_default_param: retrieves the value associated with 'name' from        *)
   1.321 +(*                    Data's parameter table                                 *)
   1.322 +(* ------------------------------------------------------------------------- *)
   1.323 +
   1.324 +val get_default_param = Symtab.lookup o #parameters o get_data;
   1.325 +
   1.326 +(* ------------------------------------------------------------------------- *)
   1.327 +(* get_default_params: returns a list of all '(name, value)' pairs that are  *)
   1.328 +(*                     stored in Data's parameter table                      *)
   1.329 +(* ------------------------------------------------------------------------- *)
   1.330 +
   1.331 +val get_default_params = Symtab.dest o #parameters o get_data;
   1.332 +
   1.333 +(* ------------------------------------------------------------------------- *)
   1.334 +(* actual_params: takes a (possibly empty) list 'params' of parameters that  *)
   1.335 +(*      override the default parameters currently specified, and             *)
   1.336 +(*      returns a record that can be passed to 'find_model'.                 *)
   1.337 +(* ------------------------------------------------------------------------- *)
   1.338 +
   1.339 +fun actual_params ctxt override =
   1.340 +  let
   1.341 +    (* (string * string) list * string -> bool *)
   1.342 +    fun read_bool (parms, name) =
   1.343 +      case AList.lookup (op =) parms name of
   1.344 +        SOME "true" => true
   1.345 +      | SOME "false" => false
   1.346 +      | SOME s => error ("parameter " ^ quote name ^
   1.347 +          " (value is " ^ quote s ^ ") must be \"true\" or \"false\"")
   1.348 +      | NONE   => error ("parameter " ^ quote name ^
   1.349 +          " must be assigned a value")
   1.350 +    (* (string * string) list * string -> int *)
   1.351 +    fun read_int (parms, name) =
   1.352 +      case AList.lookup (op =) parms name of
   1.353 +        SOME s =>
   1.354 +          (case Int.fromString s of
   1.355 +            SOME i => i
   1.356 +          | NONE   => error ("parameter " ^ quote name ^
   1.357 +            " (value is " ^ quote s ^ ") must be an integer value"))
   1.358 +      | NONE => error ("parameter " ^ quote name ^
   1.359 +          " must be assigned a value")
   1.360 +    (* (string * string) list * string -> string *)
   1.361 +    fun read_string (parms, name) =
   1.362 +      case AList.lookup (op =) parms name of
   1.363 +        SOME s => s
   1.364 +      | NONE => error ("parameter " ^ quote name ^
   1.365 +        " must be assigned a value")
   1.366 +    (* 'override' first, defaults last: *)
   1.367 +    (* (string * string) list *)
   1.368 +    val allparams = override @ get_default_params ctxt
   1.369 +    (* int *)
   1.370 +    val minsize = read_int (allparams, "minsize")
   1.371 +    val maxsize = read_int (allparams, "maxsize")
   1.372 +    val maxvars = read_int (allparams, "maxvars")
   1.373 +    val maxtime = read_int (allparams, "maxtime")
   1.374 +    (* string *)
   1.375 +    val satsolver = read_string (allparams, "satsolver")
   1.376 +    val no_assms = read_bool (allparams, "no_assms")
   1.377 +    val expect = the_default "" (AList.lookup (op =) allparams "expect")
   1.378 +    (* all remaining parameters of the form "string=int" are collected in *)
   1.379 +    (* 'sizes'                                                            *)
   1.380 +    (* TODO: it is currently not possible to specify a size for a type    *)
   1.381 +    (*       whose name is one of the other parameters (e.g. 'maxvars')   *)
   1.382 +    (* (string * int) list *)
   1.383 +    val sizes = map_filter
   1.384 +      (fn (name, value) => Option.map (pair name) (Int.fromString value))
   1.385 +      (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
   1.386 +        andalso name<>"maxvars" andalso name<>"maxtime"
   1.387 +        andalso name<>"satsolver" andalso name<>"no_assms") allparams)
   1.388 +  in
   1.389 +    {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars,
   1.390 +      maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect}
   1.391 +  end;
   1.392 +
   1.393 +
   1.394 +(* ------------------------------------------------------------------------- *)
   1.395 +(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
   1.396 +(* ------------------------------------------------------------------------- *)
   1.397 +
   1.398 +val typ_of_dtyp = ATP_Util.typ_of_dtyp
   1.399 +
   1.400 +(* ------------------------------------------------------------------------- *)
   1.401 +(* close_form: universal closure over schematic variables in 't'             *)
   1.402 +(* ------------------------------------------------------------------------- *)
   1.403 +
   1.404 +(* Term.term -> Term.term *)
   1.405 +
   1.406 +fun close_form t =
   1.407 +  let
   1.408 +    val vars = sort_wrt (fst o fst) (Term.add_vars t [])
   1.409 +  in
   1.410 +    fold (fn ((x, i), T) => fn t' =>
   1.411 +      Logic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
   1.412 +  end;
   1.413 +
   1.414 +val monomorphic_term = ATP_Util.monomorphic_term
   1.415 +val specialize_type = ATP_Util.specialize_type
   1.416 +
   1.417 +(* ------------------------------------------------------------------------- *)
   1.418 +(* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that   *)
   1.419 +(*                    denotes membership to an axiomatic type class          *)
   1.420 +(* ------------------------------------------------------------------------- *)
   1.421 +
   1.422 +fun is_const_of_class thy (s, _) =
   1.423 +  let
   1.424 +    val class_const_names = map Logic.const_of_class (Sign.all_classes thy)
   1.425 +  in
   1.426 +    (* I'm not quite sure if checking the name 's' is sufficient, *)
   1.427 +    (* or if we should also check the type 'T'.                   *)
   1.428 +    member (op =) class_const_names s
   1.429 +  end;
   1.430 +
   1.431 +(* ------------------------------------------------------------------------- *)
   1.432 +(* is_IDT_constructor: returns 'true' iff 'Const (s, T)' is the constructor  *)
   1.433 +(*                     of an inductive datatype in 'thy'                     *)
   1.434 +(* ------------------------------------------------------------------------- *)
   1.435 +
   1.436 +fun is_IDT_constructor thy (s, T) =
   1.437 +  (case body_type T of
   1.438 +    Type (s', _) =>
   1.439 +      (case Datatype.get_constrs thy s' of
   1.440 +        SOME constrs =>
   1.441 +          List.exists (fn (cname, cty) =>
   1.442 +            cname = s andalso Sign.typ_instance thy (T, cty)) constrs
   1.443 +      | NONE => false)
   1.444 +  | _  => false);
   1.445 +
   1.446 +(* ------------------------------------------------------------------------- *)
   1.447 +(* is_IDT_recursor: returns 'true' iff 'Const (s, T)' is the recursion       *)
   1.448 +(*                  operator of an inductive datatype in 'thy'               *)
   1.449 +(* ------------------------------------------------------------------------- *)
   1.450 +
   1.451 +fun is_IDT_recursor thy (s, _) =
   1.452 +  let
   1.453 +    val rec_names = Symtab.fold (append o #rec_names o snd)
   1.454 +      (Datatype.get_all thy) []
   1.455 +  in
   1.456 +    (* I'm not quite sure if checking the name 's' is sufficient, *)
   1.457 +    (* or if we should also check the type 'T'.                   *)
   1.458 +    member (op =) rec_names s
   1.459 +  end;
   1.460 +
   1.461 +(* ------------------------------------------------------------------------- *)
   1.462 +(* norm_rhs: maps  f ?t1 ... ?tn == rhs  to  %t1...tn. rhs                   *)
   1.463 +(* ------------------------------------------------------------------------- *)
   1.464 +
   1.465 +fun norm_rhs eqn =
   1.466 +  let
   1.467 +    fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
   1.468 +      | lambda v t = raise TERM ("lambda", [v, t])
   1.469 +    val (lhs, rhs) = Logic.dest_equals eqn
   1.470 +    val (_, args) = Term.strip_comb lhs
   1.471 +  in
   1.472 +    fold lambda (rev args) rhs
   1.473 +  end
   1.474 +
   1.475 +(* ------------------------------------------------------------------------- *)
   1.476 +(* get_def: looks up the definition of a constant                            *)
   1.477 +(* ------------------------------------------------------------------------- *)
   1.478 +
   1.479 +fun get_def thy (s, T) =
   1.480 +  let
   1.481 +    (* (string * Term.term) list -> (string * Term.term) option *)
   1.482 +    fun get_def_ax [] = NONE
   1.483 +      | get_def_ax ((axname, ax) :: axioms) =
   1.484 +          (let
   1.485 +            val (lhs, _) = Logic.dest_equals ax  (* equations only *)
   1.486 +            val c        = Term.head_of lhs
   1.487 +            val (s', T') = Term.dest_Const c
   1.488 +          in
   1.489 +            if s=s' then
   1.490 +              let
   1.491 +                val typeSubs = Sign.typ_match thy (T', T) Vartab.empty
   1.492 +                val ax'      = monomorphic_term typeSubs ax
   1.493 +                val rhs      = norm_rhs ax'
   1.494 +              in
   1.495 +                SOME (axname, rhs)
   1.496 +              end
   1.497 +            else
   1.498 +              get_def_ax axioms
   1.499 +          end handle ERROR _         => get_def_ax axioms
   1.500 +                   | TERM _          => get_def_ax axioms
   1.501 +                   | Type.TYPE_MATCH => get_def_ax axioms)
   1.502 +  in
   1.503 +    get_def_ax (Theory.all_axioms_of thy)
   1.504 +  end;
   1.505 +
   1.506 +(* ------------------------------------------------------------------------- *)
   1.507 +(* get_typedef: looks up the definition of a type, as created by "typedef"   *)
   1.508 +(* ------------------------------------------------------------------------- *)
   1.509 +
   1.510 +fun get_typedef thy T =
   1.511 +  let
   1.512 +    (* (string * Term.term) list -> (string * Term.term) option *)
   1.513 +    fun get_typedef_ax [] = NONE
   1.514 +      | get_typedef_ax ((axname, ax) :: axioms) =
   1.515 +          (let
   1.516 +            (* Term.term -> Term.typ option *)
   1.517 +            fun type_of_type_definition (Const (s', T')) =
   1.518 +                  if s'= @{const_name type_definition} then
   1.519 +                    SOME T'
   1.520 +                  else
   1.521 +                    NONE
   1.522 +              | type_of_type_definition (Free _) = NONE
   1.523 +              | type_of_type_definition (Var _) = NONE
   1.524 +              | type_of_type_definition (Bound _) = NONE
   1.525 +              | type_of_type_definition (Abs (_, _, body)) =
   1.526 +                  type_of_type_definition body
   1.527 +              | type_of_type_definition (t1 $ t2) =
   1.528 +                  (case type_of_type_definition t1 of
   1.529 +                    SOME x => SOME x
   1.530 +                  | 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 (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 => get_typedef_ax axioms
   1.541 +          end handle ERROR _         => get_typedef_ax axioms
   1.542 +                   | TERM _          => get_typedef_ax axioms
   1.543 +                   | Type.TYPE_MATCH => get_typedef_ax axioms)
   1.544 +  in
   1.545 +    get_typedef_ax (Theory.all_axioms_of thy)
   1.546 +  end;
   1.547 +
   1.548 +(* ------------------------------------------------------------------------- *)
   1.549 +(* get_classdef: looks up the defining axiom for an axiomatic type class, as *)
   1.550 +(*               created by the "axclass" command                            *)
   1.551 +(* ------------------------------------------------------------------------- *)
   1.552 +
   1.553 +fun get_classdef thy class =
   1.554 +  let
   1.555 +    val axname = class ^ "_class_def"
   1.556 +  in
   1.557 +    Option.map (pair axname)
   1.558 +      (AList.lookup (op =) (Theory.all_axioms_of thy) axname)
   1.559 +  end;
   1.560 +
   1.561 +(* ------------------------------------------------------------------------- *)
   1.562 +(* unfold_defs: unfolds all defined constants in a term 't', beta-eta        *)
   1.563 +(*              normalizes the result term; certain constants are not        *)
   1.564 +(*              unfolded (cf. 'collect_axioms' and the various interpreters  *)
   1.565 +(*              below): if the interpretation respects a definition anyway,  *)
   1.566 +(*              that definition does not need to be unfolded                 *)
   1.567 +(* ------------------------------------------------------------------------- *)
   1.568 +
   1.569 +(* Note: we could intertwine unfolding of constants and beta-(eta-)       *)
   1.570 +(*       normalization; this would save some unfolding for terms where    *)
   1.571 +(*       constants are eliminated by beta-reduction (e.g. 'K c1 c2').  On *)
   1.572 +(*       the other hand, this would cause additional work for terms where *)
   1.573 +(*       constants are duplicated by beta-reduction (e.g. 'S c1 c2 c3').  *)
   1.574 +
   1.575 +fun unfold_defs thy t =
   1.576 +  let
   1.577 +    (* Term.term -> Term.term *)
   1.578 +    fun unfold_loop t =
   1.579 +      case t of
   1.580 +      (* Pure *)
   1.581 +        Const (@{const_name all}, _) => t
   1.582 +      | Const (@{const_name "=="}, _) => t
   1.583 +      | Const (@{const_name "==>"}, _) => t
   1.584 +      | Const (@{const_name TYPE}, _) => t  (* axiomatic type classes *)
   1.585 +      (* HOL *)
   1.586 +      | Const (@{const_name Trueprop}, _) => t
   1.587 +      | Const (@{const_name Not}, _) => t
   1.588 +      | (* redundant, since 'True' is also an IDT constructor *)
   1.589 +        Const (@{const_name True}, _) => t
   1.590 +      | (* redundant, since 'False' is also an IDT constructor *)
   1.591 +        Const (@{const_name False}, _) => t
   1.592 +      | Const (@{const_name undefined}, _) => t
   1.593 +      | Const (@{const_name The}, _) => t
   1.594 +      | Const (@{const_name Hilbert_Choice.Eps}, _) => t
   1.595 +      | Const (@{const_name All}, _) => t
   1.596 +      | Const (@{const_name Ex}, _) => t
   1.597 +      | Const (@{const_name HOL.eq}, _) => t
   1.598 +      | Const (@{const_name HOL.conj}, _) => t
   1.599 +      | Const (@{const_name HOL.disj}, _) => t
   1.600 +      | Const (@{const_name HOL.implies}, _) => t
   1.601 +      (* sets *)
   1.602 +      | Const (@{const_name Collect}, _) => t
   1.603 +      | Const (@{const_name Set.member}, _) => t
   1.604 +      (* other optimizations *)
   1.605 +      | Const (@{const_name Finite_Set.card}, _) => t
   1.606 +      | Const (@{const_name Finite_Set.finite}, _) => t
   1.607 +      | Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
   1.608 +          Type ("fun", [@{typ nat}, @{typ bool}])])) => t
   1.609 +      | Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
   1.610 +          Type ("fun", [@{typ nat}, @{typ nat}])])) => t
   1.611 +      | Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
   1.612 +          Type ("fun", [@{typ nat}, @{typ nat}])])) => t
   1.613 +      | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
   1.614 +          Type ("fun", [@{typ nat}, @{typ nat}])])) => t
   1.615 +      | Const (@{const_name List.append}, _) => t
   1.616 +(* UNSOUND
   1.617 +      | Const (@{const_name lfp}, _) => t
   1.618 +      | Const (@{const_name gfp}, _) => t
   1.619 +*)
   1.620 +      | Const (@{const_name fst}, _) => t
   1.621 +      | Const (@{const_name snd}, _) => t
   1.622 +      (* simply-typed lambda calculus *)
   1.623 +      | Const (s, T) =>
   1.624 +          (if is_IDT_constructor thy (s, T)
   1.625 +            orelse is_IDT_recursor thy (s, T) then
   1.626 +            t  (* do not unfold IDT constructors/recursors *)
   1.627 +          (* unfold the constant if there is a defining equation *)
   1.628 +          else
   1.629 +            case get_def thy (s, T) of
   1.630 +              SOME ((*axname*) _, rhs) =>
   1.631 +              (* Note: if the term to be unfolded (i.e. 'Const (s, T)')  *)
   1.632 +              (* occurs on the right-hand side of the equation, i.e. in  *)
   1.633 +              (* 'rhs', we must not use this equation to unfold, because *)
   1.634 +              (* that would loop.  Here would be the right place to      *)
   1.635 +              (* check this.  However, getting this really right seems   *)
   1.636 +              (* difficult because the user may state arbitrary axioms,  *)
   1.637 +              (* which could interact with overloading to create loops.  *)
   1.638 +              ((*tracing (" unfolding: " ^ axname);*)
   1.639 +               unfold_loop rhs)
   1.640 +            | NONE => t)
   1.641 +      | Free _ => t
   1.642 +      | Var _ => t
   1.643 +      | Bound _ => t
   1.644 +      | Abs (s, T, body) => Abs (s, T, unfold_loop body)
   1.645 +      | t1 $ t2 => (unfold_loop t1) $ (unfold_loop t2)
   1.646 +    val result = Envir.beta_eta_contract (unfold_loop t)
   1.647 +  in
   1.648 +    result
   1.649 +  end;
   1.650 +
   1.651 +(* ------------------------------------------------------------------------- *)
   1.652 +(* collect_axioms: collects (monomorphic, universally quantified, unfolded   *)
   1.653 +(*                 versions of) all HOL axioms that are relevant w.r.t 't'   *)
   1.654 +(* ------------------------------------------------------------------------- *)
   1.655 +
   1.656 +(* Note: to make the collection of axioms more easily extensible, this    *)
   1.657 +(*       function could be based on user-supplied "axiom collectors",     *)
   1.658 +(*       similar to 'interpret'/interpreters or 'print'/printers          *)
   1.659 +
   1.660 +(* Note: currently we use "inverse" functions to the definitional         *)
   1.661 +(*       mechanisms provided by Isabelle/HOL, e.g. for "axclass",         *)
   1.662 +(*       "typedef", "definition".  A more general approach could consider *)
   1.663 +(*       *every* axiom of the theory and collect it if it has a constant/ *)
   1.664 +(*       type/typeclass in common with the term 't'.                      *)
   1.665 +
   1.666 +(* Which axioms are "relevant" for a particular term/type goes hand in    *)
   1.667 +(* hand with the interpretation of that term/type by its interpreter (see *)
   1.668 +(* way below): if the interpretation respects an axiom anyway, the axiom  *)
   1.669 +(* does not need to be added as a constraint here.                        *)
   1.670 +
   1.671 +(* To avoid collecting the same axiom multiple times, we use an           *)
   1.672 +(* accumulator 'axs' which contains all axioms collected so far.          *)
   1.673 +
   1.674 +fun collect_axioms ctxt t =
   1.675 +  let
   1.676 +    val thy = Proof_Context.theory_of ctxt
   1.677 +    val _ = tracing "Adding axioms..."
   1.678 +    val axioms = Theory.all_axioms_of thy
   1.679 +    fun collect_this_axiom (axname, ax) axs =
   1.680 +      let
   1.681 +        val ax' = unfold_defs thy ax
   1.682 +      in
   1.683 +        if member (op aconv) axs ax' then axs
   1.684 +        else (tracing axname; collect_term_axioms ax' (ax' :: axs))
   1.685 +      end
   1.686 +    and collect_sort_axioms T axs =
   1.687 +      let
   1.688 +        val sort =
   1.689 +          (case T of
   1.690 +            TFree (_, sort) => sort
   1.691 +          | TVar (_, sort)  => sort
   1.692 +          | _ => raise REFUTE ("collect_axioms",
   1.693 +              "type " ^ Syntax.string_of_typ ctxt T ^ " is not a variable"))
   1.694 +        (* obtain axioms for all superclasses *)
   1.695 +        val superclasses = sort @ maps (Sign.super_classes thy) sort
   1.696 +        (* merely an optimization, because 'collect_this_axiom' disallows *)
   1.697 +        (* duplicate axioms anyway:                                       *)
   1.698 +        val superclasses = distinct (op =) superclasses
   1.699 +        val class_axioms = maps (fn class => map (fn ax =>
   1.700 +          ("<" ^ class ^ ">", Thm.prop_of ax))
   1.701 +          (#axioms (AxClass.get_info thy class) handle ERROR _ => []))
   1.702 +          superclasses
   1.703 +        (* replace the (at most one) schematic type variable in each axiom *)
   1.704 +        (* by the actual type 'T'                                          *)
   1.705 +        val monomorphic_class_axioms = map (fn (axname, ax) =>
   1.706 +          (case Term.add_tvars ax [] of
   1.707 +            [] => (axname, ax)
   1.708 +          | [(idx, S)] => (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
   1.709 +          | _ =>
   1.710 +            raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
   1.711 +              Syntax.string_of_term ctxt ax ^
   1.712 +              ") contains more than one type variable")))
   1.713 +          class_axioms
   1.714 +      in
   1.715 +        fold collect_this_axiom monomorphic_class_axioms axs
   1.716 +      end
   1.717 +    and collect_type_axioms T axs =
   1.718 +      case T of
   1.719 +      (* simple types *)
   1.720 +        Type ("prop", []) => axs
   1.721 +      | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
   1.722 +      | Type (@{type_name set}, [T1]) => collect_type_axioms T1 axs
   1.723 +      (* axiomatic type classes *)
   1.724 +      | Type ("itself", [T1]) => collect_type_axioms T1 axs
   1.725 +      | Type (s, Ts) =>
   1.726 +        (case Datatype.get_info thy s of
   1.727 +          SOME _ =>  (* inductive datatype *)
   1.728 +            (* only collect relevant type axioms for the argument types *)
   1.729 +            fold collect_type_axioms Ts axs
   1.730 +        | NONE =>
   1.731 +          (case get_typedef thy T of
   1.732 +            SOME (axname, ax) =>
   1.733 +              collect_this_axiom (axname, ax) axs
   1.734 +          | NONE =>
   1.735 +            (* unspecified type, perhaps introduced with "typedecl" *)
   1.736 +            (* at least collect relevant type axioms for the argument types *)
   1.737 +            fold collect_type_axioms Ts axs))
   1.738 +      (* axiomatic type classes *)
   1.739 +      | TFree _ => collect_sort_axioms T axs
   1.740 +      (* axiomatic type classes *)
   1.741 +      | TVar _ => collect_sort_axioms T axs
   1.742 +    and collect_term_axioms t axs =
   1.743 +      case t of
   1.744 +      (* Pure *)
   1.745 +        Const (@{const_name all}, _) => axs
   1.746 +      | Const (@{const_name "=="}, _) => axs
   1.747 +      | Const (@{const_name "==>"}, _) => axs
   1.748 +      (* axiomatic type classes *)
   1.749 +      | Const (@{const_name TYPE}, T) => collect_type_axioms T axs
   1.750 +      (* HOL *)
   1.751 +      | Const (@{const_name Trueprop}, _) => axs
   1.752 +      | Const (@{const_name Not}, _) => axs
   1.753 +      (* redundant, since 'True' is also an IDT constructor *)
   1.754 +      | Const (@{const_name True}, _) => axs
   1.755 +      (* redundant, since 'False' is also an IDT constructor *)
   1.756 +      | Const (@{const_name False}, _) => axs
   1.757 +      | Const (@{const_name undefined}, T) => collect_type_axioms T axs
   1.758 +      | Const (@{const_name The}, T) =>
   1.759 +          let
   1.760 +            val ax = specialize_type thy (@{const_name The}, T)
   1.761 +              (the (AList.lookup (op =) axioms "HOL.the_eq_trivial"))
   1.762 +          in
   1.763 +            collect_this_axiom ("HOL.the_eq_trivial", ax) axs
   1.764 +          end
   1.765 +      | Const (@{const_name Hilbert_Choice.Eps}, T) =>
   1.766 +          let
   1.767 +            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T)
   1.768 +              (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
   1.769 +          in
   1.770 +            collect_this_axiom ("Hilbert_Choice.someI", ax) axs
   1.771 +          end
   1.772 +      | Const (@{const_name All}, T) => collect_type_axioms T axs
   1.773 +      | Const (@{const_name Ex}, T) => collect_type_axioms T axs
   1.774 +      | Const (@{const_name HOL.eq}, T) => collect_type_axioms T axs
   1.775 +      | Const (@{const_name HOL.conj}, _) => axs
   1.776 +      | Const (@{const_name HOL.disj}, _) => axs
   1.777 +      | Const (@{const_name HOL.implies}, _) => axs
   1.778 +      (* sets *)
   1.779 +      | Const (@{const_name Collect}, T) => collect_type_axioms T axs
   1.780 +      | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
   1.781 +      (* other optimizations *)
   1.782 +      | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
   1.783 +      | Const (@{const_name Finite_Set.finite}, T) =>
   1.784 +        collect_type_axioms T axs
   1.785 +      | Const (@{const_name Orderings.less}, T as Type ("fun", [@{typ nat},
   1.786 +        Type ("fun", [@{typ nat}, @{typ bool}])])) =>
   1.787 +          collect_type_axioms T axs
   1.788 +      | Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat},
   1.789 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   1.790 +          collect_type_axioms T axs
   1.791 +      | Const (@{const_name Groups.minus}, T as Type ("fun", [@{typ nat},
   1.792 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   1.793 +          collect_type_axioms T axs
   1.794 +      | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
   1.795 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
   1.796 +          collect_type_axioms T axs
   1.797 +      | Const (@{const_name List.append}, T) => collect_type_axioms T axs
   1.798 +(* UNSOUND
   1.799 +      | Const (@{const_name lfp}, T) => collect_type_axioms T axs
   1.800 +      | Const (@{const_name gfp}, T) => collect_type_axioms T axs
   1.801 +*)
   1.802 +      | Const (@{const_name fst}, T) => collect_type_axioms T axs
   1.803 +      | Const (@{const_name snd}, T) => collect_type_axioms T axs
   1.804 +      (* simply-typed lambda calculus *)
   1.805 +      | Const (s, T) =>
   1.806 +          if is_const_of_class thy (s, T) then
   1.807 +            (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *)
   1.808 +            (* and the class definition                               *)
   1.809 +            let
   1.810 +              val class = Logic.class_of_const s
   1.811 +              val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class)
   1.812 +              val ax_in = SOME (specialize_type thy (s, T) of_class)
   1.813 +                (* type match may fail due to sort constraints *)
   1.814 +                handle Type.TYPE_MATCH => NONE
   1.815 +              val ax_1 = Option.map (fn ax => (Syntax.string_of_term ctxt ax, ax)) ax_in
   1.816 +              val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class)
   1.817 +            in
   1.818 +              collect_type_axioms T (fold collect_this_axiom (map_filter I [ax_1, ax_2]) axs)
   1.819 +            end
   1.820 +          else if is_IDT_constructor thy (s, T)
   1.821 +            orelse is_IDT_recursor thy (s, T)
   1.822 +          then
   1.823 +            (* only collect relevant type axioms *)
   1.824 +            collect_type_axioms T axs
   1.825 +          else
   1.826 +            (* other constants should have been unfolded, with some *)
   1.827 +            (* exceptions: e.g. Abs_xxx/Rep_xxx functions for       *)
   1.828 +            (* typedefs, or type-class related constants            *)
   1.829 +            (* only collect relevant type axioms *)
   1.830 +            collect_type_axioms T axs
   1.831 +      | Free (_, T) => collect_type_axioms T axs
   1.832 +      | Var (_, T) => collect_type_axioms T axs
   1.833 +      | Bound _ => axs
   1.834 +      | Abs (_, T, body) => collect_term_axioms body (collect_type_axioms T axs)
   1.835 +      | t1 $ t2 => collect_term_axioms t2 (collect_term_axioms t1 axs)
   1.836 +    val result = map close_form (collect_term_axioms t [])
   1.837 +    val _ = tracing " ...done."
   1.838 +  in
   1.839 +    result
   1.840 +  end;
   1.841 +
   1.842 +(* ------------------------------------------------------------------------- *)
   1.843 +(* ground_types: collects all ground types in a term (including argument     *)
   1.844 +(*               types of other types), suppressing duplicates.  Does not    *)
   1.845 +(*               return function types, set types, non-recursive IDTs, or    *)
   1.846 +(*               'propT'.  For IDTs, also the argument types of constructors *)
   1.847 +(*               and all mutually recursive IDTs are considered.             *)
   1.848 +(* ------------------------------------------------------------------------- *)
   1.849 +
   1.850 +fun ground_types ctxt t =
   1.851 +  let
   1.852 +    val thy = Proof_Context.theory_of ctxt
   1.853 +    fun collect_types T acc =
   1.854 +      (case T of
   1.855 +        Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
   1.856 +      | Type ("prop", []) => acc
   1.857 +      | Type (@{type_name set}, [T1]) => collect_types T1 acc
   1.858 +      | Type (s, Ts) =>
   1.859 +          (case Datatype.get_info thy s of
   1.860 +            SOME info =>  (* inductive datatype *)
   1.861 +              let
   1.862 +                val index = #index info
   1.863 +                val descr = #descr info
   1.864 +                val (_, typs, _) = the (AList.lookup (op =) descr index)
   1.865 +                val typ_assoc = typs ~~ Ts
   1.866 +                (* sanity check: every element in 'dtyps' must be a *)
   1.867 +                (* 'DtTFree'                                        *)
   1.868 +                val _ = if Library.exists (fn d =>
   1.869 +                  case d of Datatype.DtTFree _ => false | _ => true) typs then
   1.870 +                  raise REFUTE ("ground_types", "datatype argument (for type "
   1.871 +                    ^ Syntax.string_of_typ ctxt T ^ ") is not a variable")
   1.872 +                else ()
   1.873 +                (* required for mutually recursive datatypes; those need to   *)
   1.874 +                (* be added even if they are an instance of an otherwise non- *)
   1.875 +                (* recursive datatype                                         *)
   1.876 +                fun collect_dtyp d acc =
   1.877 +                  let
   1.878 +                    val dT = typ_of_dtyp descr typ_assoc d
   1.879 +                  in
   1.880 +                    case d of
   1.881 +                      Datatype.DtTFree _ =>
   1.882 +                      collect_types dT acc
   1.883 +                    | Datatype.DtType (_, ds) =>
   1.884 +                      collect_types dT (fold_rev collect_dtyp ds acc)
   1.885 +                    | Datatype.DtRec i =>
   1.886 +                      if member (op =) acc dT then
   1.887 +                        acc  (* prevent infinite recursion *)
   1.888 +                      else
   1.889 +                        let
   1.890 +                          val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i)
   1.891 +                          (* if the current type is a recursive IDT (i.e. a depth *)
   1.892 +                          (* is required), add it to 'acc'                        *)
   1.893 +                          val acc_dT = if Library.exists (fn (_, ds) =>
   1.894 +                            Library.exists Datatype_Aux.is_rec_type ds) dconstrs then
   1.895 +                              insert (op =) dT acc
   1.896 +                            else acc
   1.897 +                          (* collect argument types *)
   1.898 +                          val acc_dtyps = fold_rev collect_dtyp dtyps acc_dT
   1.899 +                          (* collect constructor types *)
   1.900 +                          val acc_dconstrs = fold_rev collect_dtyp (maps snd dconstrs) acc_dtyps
   1.901 +                        in
   1.902 +                          acc_dconstrs
   1.903 +                        end
   1.904 +                  end
   1.905 +              in
   1.906 +                (* argument types 'Ts' could be added here, but they are also *)
   1.907 +                (* added by 'collect_dtyp' automatically                      *)
   1.908 +                collect_dtyp (Datatype.DtRec index) acc
   1.909 +              end
   1.910 +          | NONE =>
   1.911 +            (* not an inductive datatype, e.g. defined via "typedef" or *)
   1.912 +            (* "typedecl"                                               *)
   1.913 +            insert (op =) T (fold collect_types Ts acc))
   1.914 +      | TFree _ => insert (op =) T acc
   1.915 +      | TVar _ => insert (op =) T acc)
   1.916 +  in
   1.917 +    fold_types collect_types t []
   1.918 +  end;
   1.919 +
   1.920 +(* ------------------------------------------------------------------------- *)
   1.921 +(* string_of_typ: (rather naive) conversion from types to strings, used to   *)
   1.922 +(*                look up the size of a type in 'sizes'.  Parameterized      *)
   1.923 +(*                types with different parameters (e.g. "'a list" vs. "bool  *)
   1.924 +(*                list") are identified.                                     *)
   1.925 +(* ------------------------------------------------------------------------- *)
   1.926 +
   1.927 +(* Term.typ -> string *)
   1.928 +
   1.929 +fun string_of_typ (Type (s, _))     = s
   1.930 +  | string_of_typ (TFree (s, _))    = s
   1.931 +  | string_of_typ (TVar ((s,_), _)) = s;
   1.932 +
   1.933 +(* ------------------------------------------------------------------------- *)
   1.934 +(* first_universe: returns the "first" (i.e. smallest) universe by assigning *)
   1.935 +(*                 'minsize' to every type for which no size is specified in *)
   1.936 +(*                 'sizes'                                                   *)
   1.937 +(* ------------------------------------------------------------------------- *)
   1.938 +
   1.939 +(* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *)
   1.940 +
   1.941 +fun first_universe xs sizes minsize =
   1.942 +  let
   1.943 +    fun size_of_typ T =
   1.944 +      case AList.lookup (op =) sizes (string_of_typ T) of
   1.945 +        SOME n => n
   1.946 +      | NONE => minsize
   1.947 +  in
   1.948 +    map (fn T => (T, size_of_typ T)) xs
   1.949 +  end;
   1.950 +
   1.951 +(* ------------------------------------------------------------------------- *)
   1.952 +(* next_universe: enumerates all universes (i.e. assignments of sizes to     *)
   1.953 +(*                types), where the minimal size of a type is given by       *)
   1.954 +(*                'minsize', the maximal size is given by 'maxsize', and a   *)
   1.955 +(*                type may have a fixed size given in 'sizes'                *)
   1.956 +(* ------------------------------------------------------------------------- *)
   1.957 +
   1.958 +(* (Term.typ * int) list -> (string * int) list -> int -> int ->
   1.959 +  (Term.typ * int) list option *)
   1.960 +
   1.961 +fun next_universe xs sizes minsize maxsize =
   1.962 +  let
   1.963 +    (* creates the "first" list of length 'len', where the sum of all list *)
   1.964 +    (* elements is 'sum', and the length of the list is 'len'              *)
   1.965 +    (* int -> int -> int -> int list option *)
   1.966 +    fun make_first _ 0 sum =
   1.967 +          if sum = 0 then
   1.968 +            SOME []
   1.969 +          else
   1.970 +            NONE
   1.971 +      | make_first max len sum =
   1.972 +          if sum <= max orelse max < 0 then
   1.973 +            Option.map (fn xs' => sum :: xs') (make_first max (len-1) 0)
   1.974 +          else
   1.975 +            Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max))
   1.976 +    (* enumerates all int lists with a fixed length, where 0<=x<='max' for *)
   1.977 +    (* all list elements x (unless 'max'<0)                                *)
   1.978 +    (* int -> int -> int -> int list -> int list option *)
   1.979 +    fun next _ _ _ [] =
   1.980 +          NONE
   1.981 +      | next max len sum [x] =
   1.982 +          (* we've reached the last list element, so there's no shift possible *)
   1.983 +          make_first max (len+1) (sum+x+1)  (* increment 'sum' by 1 *)
   1.984 +      | next max len sum (x1::x2::xs) =
   1.985 +          if x1>0 andalso (x2<max orelse max<0) then
   1.986 +            (* we can shift *)
   1.987 +            SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
   1.988 +          else
   1.989 +            (* continue search *)
   1.990 +            next max (len+1) (sum+x1) (x2::xs)
   1.991 +    (* only consider those types for which the size is not fixed *)
   1.992 +    val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs
   1.993 +    (* subtract 'minsize' from every size (will be added again at the end) *)
   1.994 +    val diffs = map (fn (_, n) => n-minsize) mutables
   1.995 +  in
   1.996 +    case next (maxsize-minsize) 0 0 diffs of
   1.997 +      SOME diffs' =>
   1.998 +        (* merge with those types for which the size is fixed *)
   1.999 +        SOME (fst (fold_map (fn (T, _) => fn ds =>
  1.1000 +          case AList.lookup (op =) sizes (string_of_typ T) of
  1.1001 +          (* return the fixed size *)
  1.1002 +            SOME n => ((T, n), ds)
  1.1003 +          (* consume the head of 'ds', add 'minsize' *)
  1.1004 +          | NONE   => ((T, minsize + hd ds), tl ds))
  1.1005 +          xs diffs'))
  1.1006 +    | NONE => NONE
  1.1007 +  end;
  1.1008 +
  1.1009 +(* ------------------------------------------------------------------------- *)
  1.1010 +(* toTrue: converts the interpretation of a Boolean value to a propositional *)
  1.1011 +(*         formula that is true iff the interpretation denotes "true"        *)
  1.1012 +(* ------------------------------------------------------------------------- *)
  1.1013 +
  1.1014 +(* interpretation -> prop_formula *)
  1.1015 +
  1.1016 +fun toTrue (Leaf [fm, _]) = fm
  1.1017 +  | toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value");
  1.1018 +
  1.1019 +(* ------------------------------------------------------------------------- *)
  1.1020 +(* toFalse: converts the interpretation of a Boolean value to a              *)
  1.1021 +(*          propositional formula that is true iff the interpretation        *)
  1.1022 +(*          denotes "false"                                                  *)
  1.1023 +(* ------------------------------------------------------------------------- *)
  1.1024 +
  1.1025 +(* interpretation -> prop_formula *)
  1.1026 +
  1.1027 +fun toFalse (Leaf [_, fm]) = fm
  1.1028 +  | toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");
  1.1029 +
  1.1030 +(* ------------------------------------------------------------------------- *)
  1.1031 +(* find_model: repeatedly calls 'interpret' with appropriate parameters,     *)
  1.1032 +(*             applies a SAT solver, and (in case a model is found) displays *)
  1.1033 +(*             the model to the user by calling 'print_model'                *)
  1.1034 +(* {...}     : parameters that control the translation/model generation      *)
  1.1035 +(* assm_ts   : assumptions to be considered unless "no_assms" is specified   *)
  1.1036 +(* t         : term to be translated into a propositional formula            *)
  1.1037 +(* negate    : if true, find a model that makes 't' false (rather than true) *)
  1.1038 +(* ------------------------------------------------------------------------- *)
  1.1039 +
  1.1040 +fun find_model ctxt
  1.1041 +    {sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect}
  1.1042 +    assm_ts t negate =
  1.1043 +  let
  1.1044 +    val thy = Proof_Context.theory_of ctxt
  1.1045 +    (* string -> string *)
  1.1046 +    fun check_expect outcome_code =
  1.1047 +      if expect = "" orelse outcome_code = expect then outcome_code
  1.1048 +      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
  1.1049 +    (* unit -> string *)
  1.1050 +    fun wrapper () =
  1.1051 +      let
  1.1052 +        val timer = Timer.startRealTimer ()
  1.1053 +        val t =
  1.1054 +          if no_assms then t
  1.1055 +          else if negate then Logic.list_implies (assm_ts, t)
  1.1056 +          else Logic.mk_conjunction_list (t :: assm_ts)
  1.1057 +        val u = unfold_defs thy t
  1.1058 +        val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term ctxt u)
  1.1059 +        val axioms = collect_axioms ctxt u
  1.1060 +        (* Term.typ list *)
  1.1061 +        val types = fold (union (op =) o ground_types ctxt) (u :: axioms) []
  1.1062 +        val _ = tracing ("Ground types: "
  1.1063 +          ^ (if null types then "none."
  1.1064 +             else commas (map (Syntax.string_of_typ ctxt) types)))
  1.1065 +        (* we can only consider fragments of recursive IDTs, so we issue a  *)
  1.1066 +        (* warning if the formula contains a recursive IDT                  *)
  1.1067 +        (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
  1.1068 +        val maybe_spurious = Library.exists (fn
  1.1069 +            Type (s, _) =>
  1.1070 +              (case Datatype.get_info thy s of
  1.1071 +                SOME info =>  (* inductive datatype *)
  1.1072 +                  let
  1.1073 +                    val index           = #index info
  1.1074 +                    val descr           = #descr info
  1.1075 +                    val (_, _, constrs) = the (AList.lookup (op =) descr index)
  1.1076 +                  in
  1.1077 +                    (* recursive datatype? *)
  1.1078 +                    Library.exists (fn (_, ds) =>
  1.1079 +                      Library.exists Datatype_Aux.is_rec_type ds) constrs
  1.1080 +                  end
  1.1081 +              | NONE => false)
  1.1082 +          | _ => false) types
  1.1083 +        val _ =
  1.1084 +          if maybe_spurious then
  1.1085 +            warning ("Term contains a recursive datatype; "
  1.1086 +              ^ "countermodel(s) may be spurious!")
  1.1087 +          else
  1.1088 +            ()
  1.1089 +        (* (Term.typ * int) list -> string *)
  1.1090 +        fun find_model_loop universe =
  1.1091 +          let
  1.1092 +            val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
  1.1093 +            val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
  1.1094 +                    orelse raise TimeLimit.TimeOut
  1.1095 +            val init_model = (universe, [])
  1.1096 +            val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
  1.1097 +              bounds = [], wellformed = True}
  1.1098 +            val _ = tracing ("Translating term (sizes: "
  1.1099 +              ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
  1.1100 +            (* translate 'u' and all axioms *)
  1.1101 +            val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) =>
  1.1102 +              let
  1.1103 +                val (i, m', a') = interpret ctxt m a t'
  1.1104 +              in
  1.1105 +                (* set 'def_eq' to 'true' *)
  1.1106 +                (i, (m', {maxvars = #maxvars a', def_eq = true,
  1.1107 +                  next_idx = #next_idx a', bounds = #bounds a',
  1.1108 +                  wellformed = #wellformed a'}))
  1.1109 +              end) (u :: axioms) (init_model, init_args)
  1.1110 +            (* make 'u' either true or false, and make all axioms true, and *)
  1.1111 +            (* add the well-formedness side condition                       *)
  1.1112 +            val fm_u = (if negate then toFalse else toTrue) (hd intrs)
  1.1113 +            val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
  1.1114 +            val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
  1.1115 +            val _ =
  1.1116 +              (if satsolver = "dpll" orelse satsolver = "enumerate" then
  1.1117 +                warning ("Using SAT solver " ^ quote satsolver ^
  1.1118 +                         "; for better performance, consider installing an \
  1.1119 +                         \external solver.")
  1.1120 +               else ());
  1.1121 +            val solver =
  1.1122 +              SatSolver.invoke_solver satsolver
  1.1123 +              handle Option.Option =>
  1.1124 +                     error ("Unknown SAT solver: " ^ quote satsolver ^
  1.1125 +                            ". Available solvers: " ^
  1.1126 +                            commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
  1.1127 +          in
  1.1128 +            Output.urgent_message "Invoking SAT solver...";
  1.1129 +            (case solver fm of
  1.1130 +              SatSolver.SATISFIABLE assignment =>
  1.1131 +                (Output.urgent_message ("Model found:\n" ^ print_model ctxt model
  1.1132 +                  (fn i => case assignment i of SOME b => b | NONE => true));
  1.1133 +                 if maybe_spurious then "potential" else "genuine")
  1.1134 +            | SatSolver.UNSATISFIABLE _ =>
  1.1135 +                (Output.urgent_message "No model exists.";
  1.1136 +                case next_universe universe sizes minsize maxsize of
  1.1137 +                  SOME universe' => find_model_loop universe'
  1.1138 +                | NONE => (Output.urgent_message
  1.1139 +                    "Search terminated, no larger universe within the given limits.";
  1.1140 +                    "none"))
  1.1141 +            | SatSolver.UNKNOWN =>
  1.1142 +                (Output.urgent_message "No model found.";
  1.1143 +                case next_universe universe sizes minsize maxsize of
  1.1144 +                  SOME universe' => find_model_loop universe'
  1.1145 +                | NONE => (Output.urgent_message
  1.1146 +                  "Search terminated, no larger universe within the given limits.";
  1.1147 +                  "unknown"))) handle SatSolver.NOT_CONFIGURED =>
  1.1148 +              (error ("SAT solver " ^ quote satsolver ^ " is not configured.");
  1.1149 +               "unknown")
  1.1150 +          end
  1.1151 +          handle MAXVARS_EXCEEDED =>
  1.1152 +            (Output.urgent_message ("Search terminated, number of Boolean variables ("
  1.1153 +              ^ string_of_int maxvars ^ " allowed) exceeded.");
  1.1154 +              "unknown")
  1.1155 +
  1.1156 +        val outcome_code = find_model_loop (first_universe types sizes minsize)
  1.1157 +      in
  1.1158 +        check_expect outcome_code
  1.1159 +      end
  1.1160 +  in
  1.1161 +    (* some parameter sanity checks *)
  1.1162 +    minsize>=1 orelse
  1.1163 +      error ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1");
  1.1164 +    maxsize>=1 orelse
  1.1165 +      error ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1");
  1.1166 +    maxsize>=minsize orelse
  1.1167 +      error ("\"maxsize\" (=" ^ string_of_int maxsize ^
  1.1168 +      ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ").");
  1.1169 +    maxvars>=0 orelse
  1.1170 +      error ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0");
  1.1171 +    maxtime>=0 orelse
  1.1172 +      error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
  1.1173 +    (* enter loop with or without time limit *)
  1.1174 +    Output.urgent_message ("Trying to find a model that "
  1.1175 +      ^ (if negate then "refutes" else "satisfies") ^ ": "
  1.1176 +      ^ Syntax.string_of_term ctxt t);
  1.1177 +    if maxtime > 0 then (
  1.1178 +      TimeLimit.timeLimit (Time.fromSeconds maxtime)
  1.1179 +        wrapper ()
  1.1180 +      handle TimeLimit.TimeOut =>
  1.1181 +        (Output.urgent_message ("Search terminated, time limit (" ^
  1.1182 +            string_of_int maxtime
  1.1183 +            ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
  1.1184 +         check_expect "unknown")
  1.1185 +    ) else wrapper ()
  1.1186 +  end;
  1.1187 +
  1.1188 +
  1.1189 +(* ------------------------------------------------------------------------- *)
  1.1190 +(* INTERFACE, PART 2: FINDING A MODEL                                        *)
  1.1191 +(* ------------------------------------------------------------------------- *)
  1.1192 +
  1.1193 +(* ------------------------------------------------------------------------- *)
  1.1194 +(* satisfy_term: calls 'find_model' to find a model that satisfies 't'       *)
  1.1195 +(* params      : list of '(name, value)' pairs used to override default      *)
  1.1196 +(*               parameters                                                  *)
  1.1197 +(* ------------------------------------------------------------------------- *)
  1.1198 +
  1.1199 +fun satisfy_term ctxt params assm_ts t =
  1.1200 +  find_model ctxt (actual_params ctxt params) assm_ts t false;
  1.1201 +
  1.1202 +(* ------------------------------------------------------------------------- *)
  1.1203 +(* refute_term: calls 'find_model' to find a model that refutes 't'          *)
  1.1204 +(* params     : list of '(name, value)' pairs used to override default       *)
  1.1205 +(*              parameters                                                   *)
  1.1206 +(* ------------------------------------------------------------------------- *)
  1.1207 +
  1.1208 +fun refute_term ctxt params assm_ts t =
  1.1209 +  let
  1.1210 +    (* disallow schematic type variables, since we cannot properly negate  *)
  1.1211 +    (* terms containing them (their logical meaning is that there EXISTS a *)
  1.1212 +    (* type s.t. ...; to refute such a formula, we would have to show that *)
  1.1213 +    (* for ALL types, not ...)                                             *)
  1.1214 +    val _ = null (Term.add_tvars t []) orelse
  1.1215 +      error "Term to be refuted contains schematic type variables"
  1.1216 +
  1.1217 +    (* existential closure over schematic variables *)
  1.1218 +    val vars = sort_wrt (fst o fst) (Term.add_vars t [])
  1.1219 +    (* Term.term *)
  1.1220 +    val ex_closure = fold (fn ((x, i), T) => fn t' =>
  1.1221 +      HOLogic.exists_const T $
  1.1222 +        Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
  1.1223 +    (* Note: If 't' is of type 'propT' (rather than 'boolT'), applying   *)
  1.1224 +    (* 'HOLogic.exists_const' is not type-correct.  However, this is not *)
  1.1225 +    (* really a problem as long as 'find_model' still interprets the     *)
  1.1226 +    (* resulting term correctly, without checking its type.              *)
  1.1227 +
  1.1228 +    (* replace outermost universally quantified variables by Free's:     *)
  1.1229 +    (* refuting a term with Free's is generally faster than refuting a   *)
  1.1230 +    (* term with (nested) quantifiers, because quantifiers are expanded, *)
  1.1231 +    (* while the SAT solver searches for an interpretation for Free's.   *)
  1.1232 +    (* Also we get more information back that way, namely an             *)
  1.1233 +    (* interpretation which includes values for the (formerly)           *)
  1.1234 +    (* quantified variables.                                             *)
  1.1235 +    (* maps  !!x1...xn. !xk...xm. t   to   t  *)
  1.1236 +    fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) =
  1.1237 +          strip_all_body t
  1.1238 +      | strip_all_body (Const (@{const_name Trueprop}, _) $ t) =
  1.1239 +          strip_all_body t
  1.1240 +      | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) =
  1.1241 +          strip_all_body t
  1.1242 +      | strip_all_body t = t
  1.1243 +    (* maps  !!x1...xn. !xk...xm. t   to   [x1, ..., xn, xk, ..., xm]  *)
  1.1244 +    fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) =
  1.1245 +          (a, T) :: strip_all_vars t
  1.1246 +      | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) =
  1.1247 +          strip_all_vars t
  1.1248 +      | strip_all_vars (Const (@{const_name All}, _) $ Abs (a, T, t)) =
  1.1249 +          (a, T) :: strip_all_vars t
  1.1250 +      | strip_all_vars _ = [] : (string * typ) list
  1.1251 +    val strip_t = strip_all_body ex_closure
  1.1252 +    val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure)
  1.1253 +    val subst_t = Term.subst_bounds (map Free frees, strip_t)
  1.1254 +  in
  1.1255 +    find_model ctxt (actual_params ctxt params) assm_ts subst_t true
  1.1256 +  end;
  1.1257 +
  1.1258 +(* ------------------------------------------------------------------------- *)
  1.1259 +(* refute_goal                                                               *)
  1.1260 +(* ------------------------------------------------------------------------- *)
  1.1261 +
  1.1262 +fun refute_goal ctxt params th i =
  1.1263 +  let
  1.1264 +    val t = th |> prop_of
  1.1265 +  in
  1.1266 +    if Logic.count_prems t = 0 then
  1.1267 +      (Output.urgent_message "No subgoal!"; "none")
  1.1268 +    else
  1.1269 +      let
  1.1270 +        val assms = map term_of (Assumption.all_assms_of ctxt)
  1.1271 +        val (t, frees) = Logic.goal_params t i
  1.1272 +      in
  1.1273 +        refute_term ctxt params assms (subst_bounds (frees, t))
  1.1274 +      end
  1.1275 +  end
  1.1276 +
  1.1277 +
  1.1278 +(* ------------------------------------------------------------------------- *)
  1.1279 +(* INTERPRETERS: Auxiliary Functions                                         *)
  1.1280 +(* ------------------------------------------------------------------------- *)
  1.1281 +
  1.1282 +(* ------------------------------------------------------------------------- *)
  1.1283 +(* make_constants: returns all interpretations for type 'T' that consist of  *)
  1.1284 +(*                 unit vectors with 'True'/'False' only (no Boolean         *)
  1.1285 +(*                 variables)                                                *)
  1.1286 +(* ------------------------------------------------------------------------- *)
  1.1287 +
  1.1288 +fun make_constants ctxt model T =
  1.1289 +  let
  1.1290 +    (* returns a list with all unit vectors of length n *)
  1.1291 +    (* int -> interpretation list *)
  1.1292 +    fun unit_vectors n =
  1.1293 +      let
  1.1294 +        (* returns the k-th unit vector of length n *)
  1.1295 +        (* int * int -> interpretation *)
  1.1296 +        fun unit_vector (k, n) =
  1.1297 +          Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
  1.1298 +        (* int -> interpretation list *)
  1.1299 +        fun unit_vectors_loop k =
  1.1300 +          if k>n then [] else unit_vector (k,n) :: unit_vectors_loop (k+1)
  1.1301 +      in
  1.1302 +        unit_vectors_loop 1
  1.1303 +      end
  1.1304 +    (* returns a list of lists, each one consisting of n (possibly *)
  1.1305 +    (* identical) elements from 'xs'                               *)
  1.1306 +    (* int -> 'a list -> 'a list list *)
  1.1307 +    fun pick_all 1 xs = map single xs
  1.1308 +      | pick_all n xs =
  1.1309 +          let val rec_pick = pick_all (n - 1) xs in
  1.1310 +            maps (fn x => map (cons x) rec_pick) xs
  1.1311 +          end
  1.1312 +    (* returns all constant interpretations that have the same tree *)
  1.1313 +    (* structure as the interpretation argument                     *)
  1.1314 +    (* interpretation -> interpretation list *)
  1.1315 +    fun make_constants_intr (Leaf xs) = unit_vectors (length xs)
  1.1316 +      | make_constants_intr (Node xs) = map Node (pick_all (length xs)
  1.1317 +          (make_constants_intr (hd xs)))
  1.1318 +    (* obtain the interpretation for a variable of type 'T' *)
  1.1319 +    val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1,
  1.1320 +      bounds=[], wellformed=True} (Free ("dummy", T))
  1.1321 +  in
  1.1322 +    make_constants_intr i
  1.1323 +  end;
  1.1324 +
  1.1325 +(* ------------------------------------------------------------------------- *)
  1.1326 +(* size_of_type: returns the number of elements in a type 'T' (i.e. 'length  *)
  1.1327 +(*               (make_constants T)', but implemented more efficiently)      *)
  1.1328 +(* ------------------------------------------------------------------------- *)
  1.1329 +
  1.1330 +(* returns 0 for an empty ground type or a function type with empty      *)
  1.1331 +(* codomain, but fails for a function type with empty domain --          *)
  1.1332 +(* admissibility of datatype constructor argument types (see "Inductive  *)
  1.1333 +(* datatypes in HOL - lessons learned ...", S. Berghofer, M. Wenzel,     *)
  1.1334 +(* TPHOLs 99) ensures that recursive, possibly empty, datatype fragments *)
  1.1335 +(* never occur as the domain of a function type that is the type of a    *)
  1.1336 +(* constructor argument                                                  *)
  1.1337 +
  1.1338 +fun size_of_type ctxt model T =
  1.1339 +  let
  1.1340 +    (* returns the number of elements that have the same tree structure as a *)
  1.1341 +    (* given interpretation                                                  *)
  1.1342 +    fun size_of_intr (Leaf xs) = length xs
  1.1343 +      | size_of_intr (Node xs) = Integer.pow (length xs) (size_of_intr (hd xs))
  1.1344 +    (* obtain the interpretation for a variable of type 'T' *)
  1.1345 +    val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1,
  1.1346 +      bounds=[], wellformed=True} (Free ("dummy", T))
  1.1347 +  in
  1.1348 +    size_of_intr i
  1.1349 +  end;
  1.1350 +
  1.1351 +(* ------------------------------------------------------------------------- *)
  1.1352 +(* TT/FF: interpretations that denote "true" or "false", respectively        *)
  1.1353 +(* ------------------------------------------------------------------------- *)
  1.1354 +
  1.1355 +(* interpretation *)
  1.1356 +
  1.1357 +val TT = Leaf [True, False];
  1.1358 +
  1.1359 +val FF = Leaf [False, True];
  1.1360 +
  1.1361 +(* ------------------------------------------------------------------------- *)
  1.1362 +(* make_equality: returns an interpretation that denotes (extensional)       *)
  1.1363 +(*                equality of two interpretations                            *)
  1.1364 +(* - two interpretations are 'equal' iff they are both defined and denote    *)
  1.1365 +(*   the same value                                                          *)
  1.1366 +(* - two interpretations are 'not_equal' iff they are both defined at least  *)
  1.1367 +(*   partially, and a defined part denotes different values                  *)
  1.1368 +(* - a completely undefined interpretation is neither 'equal' nor            *)
  1.1369 +(*   'not_equal' to another interpretation                                   *)
  1.1370 +(* ------------------------------------------------------------------------- *)
  1.1371 +
  1.1372 +(* We could in principle represent '=' on a type T by a particular        *)
  1.1373 +(* interpretation.  However, the size of that interpretation is quadratic *)
  1.1374 +(* in the size of T.  Therefore comparing the interpretations 'i1' and    *)
  1.1375 +(* 'i2' directly is more efficient than constructing the interpretation   *)
  1.1376 +(* for equality on T first, and "applying" this interpretation to 'i1'    *)
  1.1377 +(* and 'i2' in the usual way (cf. 'interpretation_apply') then.           *)
  1.1378 +
  1.1379 +(* interpretation * interpretation -> interpretation *)
  1.1380 +
  1.1381 +fun make_equality (i1, i2) =
  1.1382 +  let
  1.1383 +    (* interpretation * interpretation -> prop_formula *)
  1.1384 +    fun equal (i1, i2) =
  1.1385 +      (case i1 of
  1.1386 +        Leaf xs =>
  1.1387 +          (case i2 of
  1.1388 +            Leaf ys => Prop_Logic.dot_product (xs, ys)  (* defined and equal *)
  1.1389 +          | Node _  => raise REFUTE ("make_equality",
  1.1390 +            "second interpretation is higher"))
  1.1391 +      | Node xs =>
  1.1392 +          (case i2 of
  1.1393 +            Leaf _  => raise REFUTE ("make_equality",
  1.1394 +            "first interpretation is higher")
  1.1395 +          | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
  1.1396 +    (* interpretation * interpretation -> prop_formula *)
  1.1397 +    fun not_equal (i1, i2) =
  1.1398 +      (case i1 of
  1.1399 +        Leaf xs =>
  1.1400 +          (case i2 of
  1.1401 +            (* defined and not equal *)
  1.1402 +            Leaf ys => Prop_Logic.all ((Prop_Logic.exists xs)
  1.1403 +            :: (Prop_Logic.exists ys)
  1.1404 +            :: (map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys)))
  1.1405 +          | Node _  => raise REFUTE ("make_equality",
  1.1406 +            "second interpretation is higher"))
  1.1407 +      | Node xs =>
  1.1408 +          (case i2 of
  1.1409 +            Leaf _  => raise REFUTE ("make_equality",
  1.1410 +            "first interpretation is higher")
  1.1411 +          | Node ys => Prop_Logic.exists (map not_equal (xs ~~ ys))))
  1.1412 +  in
  1.1413 +    (* a value may be undefined; therefore 'not_equal' is not just the *)
  1.1414 +    (* negation of 'equal'                                             *)
  1.1415 +    Leaf [equal (i1, i2), not_equal (i1, i2)]
  1.1416 +  end;
  1.1417 +
  1.1418 +(* ------------------------------------------------------------------------- *)
  1.1419 +(* make_def_equality: returns an interpretation that denotes (extensional)   *)
  1.1420 +(*                    equality of two interpretations                        *)
  1.1421 +(* This function treats undefined/partially defined interpretations          *)
  1.1422 +(* different from 'make_equality': two undefined interpretations are         *)
  1.1423 +(* considered equal, while a defined interpretation is considered not equal  *)
  1.1424 +(* to an undefined interpretation.                                           *)
  1.1425 +(* ------------------------------------------------------------------------- *)
  1.1426 +
  1.1427 +(* interpretation * interpretation -> interpretation *)
  1.1428 +
  1.1429 +fun make_def_equality (i1, i2) =
  1.1430 +  let
  1.1431 +    (* interpretation * interpretation -> prop_formula *)
  1.1432 +    fun equal (i1, i2) =
  1.1433 +      (case i1 of
  1.1434 +        Leaf xs =>
  1.1435 +          (case i2 of
  1.1436 +            (* defined and equal, or both undefined *)
  1.1437 +            Leaf ys => SOr (Prop_Logic.dot_product (xs, ys),
  1.1438 +            SAnd (Prop_Logic.all (map SNot xs), Prop_Logic.all (map SNot ys)))
  1.1439 +          | Node _  => raise REFUTE ("make_def_equality",
  1.1440 +            "second interpretation is higher"))
  1.1441 +      | Node xs =>
  1.1442 +          (case i2 of
  1.1443 +            Leaf _  => raise REFUTE ("make_def_equality",
  1.1444 +            "first interpretation is higher")
  1.1445 +          | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
  1.1446 +    (* interpretation *)
  1.1447 +    val eq = equal (i1, i2)
  1.1448 +  in
  1.1449 +    Leaf [eq, SNot eq]
  1.1450 +  end;
  1.1451 +
  1.1452 +(* ------------------------------------------------------------------------- *)
  1.1453 +(* interpretation_apply: returns an interpretation that denotes the result   *)
  1.1454 +(*                       of applying the function denoted by 'i1' to the     *)
  1.1455 +(*                       argument denoted by 'i2'                            *)
  1.1456 +(* ------------------------------------------------------------------------- *)
  1.1457 +
  1.1458 +(* interpretation * interpretation -> interpretation *)
  1.1459 +
  1.1460 +fun interpretation_apply (i1, i2) =
  1.1461 +  let
  1.1462 +    (* interpretation * interpretation -> interpretation *)
  1.1463 +    fun interpretation_disjunction (tr1,tr2) =
  1.1464 +      tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys))
  1.1465 +        (tree_pair (tr1,tr2))
  1.1466 +    (* prop_formula * interpretation -> interpretation *)
  1.1467 +    fun prop_formula_times_interpretation (fm,tr) =
  1.1468 +      tree_map (map (fn x => SAnd (fm,x))) tr
  1.1469 +    (* prop_formula list * interpretation list -> interpretation *)
  1.1470 +    fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =
  1.1471 +          prop_formula_times_interpretation (fm,tr)
  1.1472 +      | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
  1.1473 +          interpretation_disjunction (prop_formula_times_interpretation (fm,tr),
  1.1474 +            prop_formula_list_dot_product_interpretation_list (fms,trees))
  1.1475 +      | prop_formula_list_dot_product_interpretation_list (_,_) =
  1.1476 +          raise REFUTE ("interpretation_apply", "empty list (in dot product)")
  1.1477 +    (* returns a list of lists, each one consisting of one element from each *)
  1.1478 +    (* element of 'xss'                                                      *)
  1.1479 +    (* 'a list list -> 'a list list *)
  1.1480 +    fun pick_all [xs] = map single xs
  1.1481 +      | pick_all (xs::xss) =
  1.1482 +          let val rec_pick = pick_all xss in
  1.1483 +            maps (fn x => map (cons x) rec_pick) xs
  1.1484 +          end
  1.1485 +      | pick_all _ = raise REFUTE ("interpretation_apply", "empty list (in pick_all)")
  1.1486 +    (* interpretation -> prop_formula list *)
  1.1487 +    fun interpretation_to_prop_formula_list (Leaf xs) = xs
  1.1488 +      | interpretation_to_prop_formula_list (Node trees) =
  1.1489 +          map Prop_Logic.all (pick_all
  1.1490 +            (map interpretation_to_prop_formula_list trees))
  1.1491 +  in
  1.1492 +    case i1 of
  1.1493 +      Leaf _ =>
  1.1494 +        raise REFUTE ("interpretation_apply", "first interpretation is a leaf")
  1.1495 +    | Node xs =>
  1.1496 +        prop_formula_list_dot_product_interpretation_list
  1.1497 +          (interpretation_to_prop_formula_list i2, xs)
  1.1498 +  end;
  1.1499 +
  1.1500 +(* ------------------------------------------------------------------------- *)
  1.1501 +(* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions      *)
  1.1502 +(* ------------------------------------------------------------------------- *)
  1.1503 +
  1.1504 +(* Term.term -> int -> Term.term *)
  1.1505 +
  1.1506 +fun eta_expand t i =
  1.1507 +  let
  1.1508 +    val Ts = Term.binder_types (Term.fastype_of t)
  1.1509 +    val t' = Term.incr_boundvars i t
  1.1510 +  in
  1.1511 +    fold_rev (fn T => fn term => Abs ("<eta_expand>", T, term))
  1.1512 +      (List.take (Ts, i))
  1.1513 +      (Term.list_comb (t', map Bound (i-1 downto 0)))
  1.1514 +  end;
  1.1515 +
  1.1516 +(* ------------------------------------------------------------------------- *)
  1.1517 +(* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
  1.1518 +(*               is the sum (over its constructors) of the product (over     *)
  1.1519 +(*               their arguments) of the size of the argument types          *)
  1.1520 +(* ------------------------------------------------------------------------- *)
  1.1521 +
  1.1522 +fun size_of_dtyp ctxt typ_sizes descr typ_assoc constructors =
  1.1523 +  Integer.sum (map (fn (_, dtyps) =>
  1.1524 +    Integer.prod (map (size_of_type ctxt (typ_sizes, []) o
  1.1525 +      (typ_of_dtyp descr typ_assoc)) dtyps))
  1.1526 +        constructors);
  1.1527 +
  1.1528 +
  1.1529 +(* ------------------------------------------------------------------------- *)
  1.1530 +(* INTERPRETERS: Actual Interpreters                                         *)
  1.1531 +(* ------------------------------------------------------------------------- *)
  1.1532 +
  1.1533 +(* simply typed lambda calculus: Isabelle's basic term syntax, with type *)
  1.1534 +(* variables, function types, and propT                                  *)
  1.1535 +
  1.1536 +fun stlc_interpreter ctxt model args t =
  1.1537 +  let
  1.1538 +    val (typs, terms) = model
  1.1539 +    val {maxvars, def_eq, next_idx, bounds, wellformed} = args
  1.1540 +    (* Term.typ -> (interpretation * model * arguments) option *)
  1.1541 +    fun interpret_groundterm T =
  1.1542 +      let
  1.1543 +        (* unit -> (interpretation * model * arguments) option *)
  1.1544 +        fun interpret_groundtype () =
  1.1545 +          let
  1.1546 +            (* the model must specify a size for ground types *)
  1.1547 +            val size =
  1.1548 +              if T = Term.propT then 2
  1.1549 +              else the (AList.lookup (op =) typs T)
  1.1550 +            val next = next_idx + size
  1.1551 +            (* check if 'maxvars' is large enough *)
  1.1552 +            val _ = (if next - 1 > maxvars andalso maxvars > 0 then
  1.1553 +              raise MAXVARS_EXCEEDED else ())
  1.1554 +            (* prop_formula list *)
  1.1555 +            val fms  = map BoolVar (next_idx upto (next_idx + size - 1))
  1.1556 +            (* interpretation *)
  1.1557 +            val intr = Leaf fms
  1.1558 +            (* prop_formula list -> prop_formula *)
  1.1559 +            fun one_of_two_false [] = True
  1.1560 +              | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
  1.1561 +                  SOr (SNot x, SNot x')) xs), one_of_two_false xs)
  1.1562 +            (* prop_formula *)
  1.1563 +            val wf = one_of_two_false fms
  1.1564 +          in
  1.1565 +            (* extend the model, increase 'next_idx', add well-formedness *)
  1.1566 +            (* condition                                                  *)
  1.1567 +            SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars,
  1.1568 +              def_eq = def_eq, next_idx = next, bounds = bounds,
  1.1569 +              wellformed = SAnd (wellformed, wf)})
  1.1570 +          end
  1.1571 +      in
  1.1572 +        case T of
  1.1573 +          Type ("fun", [T1, T2]) =>
  1.1574 +            let
  1.1575 +              (* we create 'size_of_type ... T1' different copies of the        *)
  1.1576 +              (* interpretation for 'T2', which are then combined into a single *)
  1.1577 +              (* new interpretation                                             *)
  1.1578 +              (* make fresh copies, with different variable indices *)
  1.1579 +              (* 'idx': next variable index                         *)
  1.1580 +              (* 'n'  : number of copies                            *)
  1.1581 +              (* int -> int -> (int * interpretation list * prop_formula *)
  1.1582 +              fun make_copies idx 0 = (idx, [], True)
  1.1583 +                | make_copies idx n =
  1.1584 +                    let
  1.1585 +                      val (copy, _, new_args) = interpret ctxt (typs, [])
  1.1586 +                        {maxvars = maxvars, def_eq = false, next_idx = idx,
  1.1587 +                        bounds = [], wellformed = True} (Free ("dummy", T2))
  1.1588 +                      val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1)
  1.1589 +                    in
  1.1590 +                      (idx', copy :: copies, SAnd (#wellformed new_args, wf'))
  1.1591 +                    end
  1.1592 +              val (next, copies, wf) = make_copies next_idx
  1.1593 +                (size_of_type ctxt model T1)
  1.1594 +              (* combine copies into a single interpretation *)
  1.1595 +              val intr = Node copies
  1.1596 +            in
  1.1597 +              (* extend the model, increase 'next_idx', add well-formedness *)
  1.1598 +              (* condition                                                  *)
  1.1599 +              SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars,
  1.1600 +                def_eq = def_eq, next_idx = next, bounds = bounds,
  1.1601 +                wellformed = SAnd (wellformed, wf)})
  1.1602 +            end
  1.1603 +        | Type _  => interpret_groundtype ()
  1.1604 +        | TFree _ => interpret_groundtype ()
  1.1605 +        | TVar  _ => interpret_groundtype ()
  1.1606 +      end
  1.1607 +  in
  1.1608 +    case AList.lookup (op =) terms t of
  1.1609 +      SOME intr =>
  1.1610 +        (* return an existing interpretation *)
  1.1611 +        SOME (intr, model, args)
  1.1612 +    | NONE =>
  1.1613 +        (case t of
  1.1614 +          Const (_, T) => interpret_groundterm T
  1.1615 +        | Free (_, T) => interpret_groundterm T
  1.1616 +        | Var (_, T) => interpret_groundterm T
  1.1617 +        | Bound i => SOME (nth (#bounds args) i, model, args)
  1.1618 +        | Abs (_, T, body) =>
  1.1619 +            let
  1.1620 +              (* create all constants of type 'T' *)
  1.1621 +              val constants = make_constants ctxt model T
  1.1622 +              (* interpret the 'body' separately for each constant *)
  1.1623 +              val (bodies, (model', args')) = fold_map
  1.1624 +                (fn c => fn (m, a) =>
  1.1625 +                  let
  1.1626 +                    (* add 'c' to 'bounds' *)
  1.1627 +                    val (i', m', a') = interpret ctxt m {maxvars = #maxvars a,
  1.1628 +                      def_eq = #def_eq a, next_idx = #next_idx a,
  1.1629 +                      bounds = (c :: #bounds a), wellformed = #wellformed a} body
  1.1630 +                  in
  1.1631 +                    (* keep the new model m' and 'next_idx' and 'wellformed', *)
  1.1632 +                    (* but use old 'bounds'                                   *)
  1.1633 +                    (i', (m', {maxvars = maxvars, def_eq = def_eq,
  1.1634 +                      next_idx = #next_idx a', bounds = bounds,
  1.1635 +                      wellformed = #wellformed a'}))
  1.1636 +                  end)
  1.1637 +                constants (model, args)
  1.1638 +            in
  1.1639 +              SOME (Node bodies, model', args')
  1.1640 +            end
  1.1641 +        | t1 $ t2 =>
  1.1642 +            let
  1.1643 +              (* interpret 't1' and 't2' separately *)
  1.1644 +              val (intr1, model1, args1) = interpret ctxt model args t1
  1.1645 +              val (intr2, model2, args2) = interpret ctxt model1 args1 t2
  1.1646 +            in
  1.1647 +              SOME (interpretation_apply (intr1, intr2), model2, args2)
  1.1648 +            end)
  1.1649 +  end;
  1.1650 +
  1.1651 +fun Pure_interpreter ctxt model args t =
  1.1652 +  case t of
  1.1653 +    Const (@{const_name all}, _) $ t1 =>
  1.1654 +      let
  1.1655 +        val (i, m, a) = interpret ctxt model args t1
  1.1656 +      in
  1.1657 +        case i of
  1.1658 +          Node xs =>
  1.1659 +            (* 3-valued logic *)
  1.1660 +            let
  1.1661 +              val fmTrue  = Prop_Logic.all (map toTrue xs)
  1.1662 +              val fmFalse = Prop_Logic.exists (map toFalse xs)
  1.1663 +            in
  1.1664 +              SOME (Leaf [fmTrue, fmFalse], m, a)
  1.1665 +            end
  1.1666 +        | _ =>
  1.1667 +          raise REFUTE ("Pure_interpreter",
  1.1668 +            "\"all\" is followed by a non-function")
  1.1669 +      end
  1.1670 +  | Const (@{const_name all}, _) =>
  1.1671 +      SOME (interpret ctxt model args (eta_expand t 1))
  1.1672 +  | Const (@{const_name "=="}, _) $ t1 $ t2 =>
  1.1673 +      let
  1.1674 +        val (i1, m1, a1) = interpret ctxt model args t1
  1.1675 +        val (i2, m2, a2) = interpret ctxt m1 a1 t2
  1.1676 +      in
  1.1677 +        (* we use either 'make_def_equality' or 'make_equality' *)
  1.1678 +        SOME ((if #def_eq args then make_def_equality else make_equality)
  1.1679 +          (i1, i2), m2, a2)
  1.1680 +      end
  1.1681 +  | Const (@{const_name "=="}, _) $ _ =>
  1.1682 +      SOME (interpret ctxt model args (eta_expand t 1))
  1.1683 +  | Const (@{const_name "=="}, _) =>
  1.1684 +      SOME (interpret ctxt model args (eta_expand t 2))
  1.1685 +  | Const (@{const_name "==>"}, _) $ t1 $ t2 =>
  1.1686 +      (* 3-valued logic *)
  1.1687 +      let
  1.1688 +        val (i1, m1, a1) = interpret ctxt model args t1
  1.1689 +        val (i2, m2, a2) = interpret ctxt m1 a1 t2
  1.1690 +        val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2)
  1.1691 +        val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2)
  1.1692 +      in
  1.1693 +        SOME (Leaf [fmTrue, fmFalse], m2, a2)
  1.1694 +      end
  1.1695 +  | Const (@{const_name "==>"}, _) $ _ =>
  1.1696 +      SOME (interpret ctxt model args (eta_expand t 1))
  1.1697 +  | Const (@{const_name "==>"}, _) =>
  1.1698 +      SOME (interpret ctxt model args (eta_expand t 2))
  1.1699 +  | _ => NONE;
  1.1700 +
  1.1701 +fun HOLogic_interpreter ctxt model args t =
  1.1702 +(* Providing interpretations directly is more efficient than unfolding the *)
  1.1703 +(* logical constants.  In HOL however, logical constants can themselves be *)
  1.1704 +(* arguments.  They are then translated using eta-expansion.               *)
  1.1705 +  case t of
  1.1706 +    Const (@{const_name Trueprop}, _) =>
  1.1707 +      SOME (Node [TT, FF], model, args)
  1.1708 +  | Const (@{const_name Not}, _) =>
  1.1709 +      SOME (Node [FF, TT], model, args)
  1.1710 +  (* redundant, since 'True' is also an IDT constructor *)
  1.1711 +  | Const (@{const_name True}, _) =>
  1.1712 +      SOME (TT, model, args)
  1.1713 +  (* redundant, since 'False' is also an IDT constructor *)
  1.1714 +  | Const (@{const_name False}, _) =>
  1.1715 +      SOME (FF, model, args)
  1.1716 +  | Const (@{const_name All}, _) $ t1 =>  (* similar to "all" (Pure) *)
  1.1717 +      let
  1.1718 +        val (i, m, a) = interpret ctxt model args t1
  1.1719 +      in
  1.1720 +        case i of
  1.1721 +          Node xs =>
  1.1722 +            (* 3-valued logic *)
  1.1723 +            let
  1.1724 +              val fmTrue = Prop_Logic.all (map toTrue xs)
  1.1725 +              val fmFalse = Prop_Logic.exists (map toFalse xs)
  1.1726 +            in
  1.1727 +              SOME (Leaf [fmTrue, fmFalse], m, a)
  1.1728 +            end
  1.1729 +        | _ =>
  1.1730 +          raise REFUTE ("HOLogic_interpreter",
  1.1731 +            "\"All\" is followed by a non-function")
  1.1732 +      end
  1.1733 +  | Const (@{const_name All}, _) =>
  1.1734 +      SOME (interpret ctxt model args (eta_expand t 1))
  1.1735 +  | Const (@{const_name Ex}, _) $ t1 =>
  1.1736 +      let
  1.1737 +        val (i, m, a) = interpret ctxt model args t1
  1.1738 +      in
  1.1739 +        case i of
  1.1740 +          Node xs =>
  1.1741 +            (* 3-valued logic *)
  1.1742 +            let
  1.1743 +              val fmTrue = Prop_Logic.exists (map toTrue xs)
  1.1744 +              val fmFalse = Prop_Logic.all (map toFalse xs)
  1.1745 +            in
  1.1746 +              SOME (Leaf [fmTrue, fmFalse], m, a)
  1.1747 +            end
  1.1748 +        | _ =>
  1.1749 +          raise REFUTE ("HOLogic_interpreter",
  1.1750 +            "\"Ex\" is followed by a non-function")
  1.1751 +      end
  1.1752 +  | Const (@{const_name Ex}, _) =>
  1.1753 +      SOME (interpret ctxt model args (eta_expand t 1))
  1.1754 +  | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)
  1.1755 +      let
  1.1756 +        val (i1, m1, a1) = interpret ctxt model args t1
  1.1757 +        val (i2, m2, a2) = interpret ctxt m1 a1 t2
  1.1758 +      in
  1.1759 +        SOME (make_equality (i1, i2), m2, a2)
  1.1760 +      end
  1.1761 +  | Const (@{const_name HOL.eq}, _) $ _ =>
  1.1762 +      SOME (interpret ctxt model args (eta_expand t 1))
  1.1763 +  | Const (@{const_name HOL.eq}, _) =>
  1.1764 +      SOME (interpret ctxt model args (eta_expand t 2))
  1.1765 +  | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
  1.1766 +      (* 3-valued logic *)
  1.1767 +      let
  1.1768 +        val (i1, m1, a1) = interpret ctxt model args t1
  1.1769 +        val (i2, m2, a2) = interpret ctxt m1 a1 t2
  1.1770 +        val fmTrue = Prop_Logic.SAnd (toTrue i1, toTrue i2)
  1.1771 +        val fmFalse = Prop_Logic.SOr (toFalse i1, toFalse i2)
  1.1772 +      in
  1.1773 +        SOME (Leaf [fmTrue, fmFalse], m2, a2)
  1.1774 +      end
  1.1775 +  | Const (@{const_name HOL.conj}, _) $ _ =>
  1.1776 +      SOME (interpret ctxt model args (eta_expand t 1))
  1.1777 +  | Const (@{const_name HOL.conj}, _) =>
  1.1778 +      SOME (interpret ctxt model args (eta_expand t 2))
  1.1779 +      (* this would make "undef" propagate, even for formulae like *)
  1.1780 +      (* "False & undef":                                          *)
  1.1781 +      (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)
  1.1782 +  | Const (@{const_name HOL.disj}, _) $ t1 $ t2 =>
  1.1783 +      (* 3-valued logic *)
  1.1784 +      let
  1.1785 +        val (i1, m1, a1) = interpret ctxt model args t1
  1.1786 +        val (i2, m2, a2) = interpret ctxt m1 a1 t2
  1.1787 +        val fmTrue = Prop_Logic.SOr (toTrue i1, toTrue i2)
  1.1788 +        val fmFalse = Prop_Logic.SAnd (toFalse i1, toFalse i2)
  1.1789 +      in
  1.1790 +        SOME (Leaf [fmTrue, fmFalse], m2, a2)
  1.1791 +      end
  1.1792 +  | Const (@{const_name HOL.disj}, _) $ _ =>
  1.1793 +      SOME (interpret ctxt model args (eta_expand t 1))
  1.1794 +  | Const (@{const_name HOL.disj}, _) =>
  1.1795 +      SOME (interpret ctxt model args (eta_expand t 2))
  1.1796 +      (* this would make "undef" propagate, even for formulae like *)
  1.1797 +      (* "True | undef":                                           *)
  1.1798 +      (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
  1.1799 +  | Const (@{const_name HOL.implies}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
  1.1800 +      (* 3-valued logic *)
  1.1801 +      let
  1.1802 +        val (i1, m1, a1) = interpret ctxt model args t1
  1.1803 +        val (i2, m2, a2) = interpret ctxt m1 a1 t2
  1.1804 +        val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2)
  1.1805 +        val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2)
  1.1806 +      in
  1.1807 +        SOME (Leaf [fmTrue, fmFalse], m2, a2)
  1.1808 +      end
  1.1809 +  | Const (@{const_name HOL.implies}, _) $ _ =>
  1.1810 +      SOME (interpret ctxt model args (eta_expand t 1))
  1.1811 +  | Const (@{const_name HOL.implies}, _) =>
  1.1812 +      SOME (interpret ctxt model args (eta_expand t 2))
  1.1813 +      (* this would make "undef" propagate, even for formulae like *)
  1.1814 +      (* "False --> undef":                                        *)
  1.1815 +      (* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *)
  1.1816 +  | _ => NONE;
  1.1817 +
  1.1818 +(* interprets variables and constants whose type is an IDT (this is        *)
  1.1819 +(* relatively easy and merely requires us to compute the size of the IDT); *)
  1.1820 +(* constructors of IDTs however are properly interpreted by                *)
  1.1821 +(* 'IDT_constructor_interpreter'                                           *)
  1.1822 +
  1.1823 +fun IDT_interpreter ctxt model args t =
  1.1824 +  let
  1.1825 +    val thy = Proof_Context.theory_of ctxt
  1.1826 +    val (typs, terms) = model
  1.1827 +    (* Term.typ -> (interpretation * model * arguments) option *)
  1.1828 +    fun interpret_term (Type (s, Ts)) =
  1.1829 +          (case Datatype.get_info thy s of
  1.1830 +            SOME info =>  (* inductive datatype *)
  1.1831 +              let
  1.1832 +                (* int option -- only recursive IDTs have an associated depth *)
  1.1833 +                val depth = AList.lookup (op =) typs (Type (s, Ts))
  1.1834 +                (* sanity check: depth must be at least 0 *)
  1.1835 +                val _ =
  1.1836 +                  (case depth of SOME n =>
  1.1837 +                    if n < 0 then
  1.1838 +                      raise REFUTE ("IDT_interpreter", "negative depth")
  1.1839 +                    else ()
  1.1840 +                  | _ => ())
  1.1841 +              in
  1.1842 +                (* termination condition to avoid infinite recursion *)
  1.1843 +                if depth = (SOME 0) then
  1.1844 +                  (* return a leaf of size 0 *)
  1.1845 +                  SOME (Leaf [], model, args)
  1.1846 +                else
  1.1847 +                  let
  1.1848 +                    val index               = #index info
  1.1849 +                    val descr               = #descr info
  1.1850 +                    val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
  1.1851 +                    val typ_assoc           = dtyps ~~ Ts
  1.1852 +                    (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1.1853 +                    val _ =
  1.1854 +                      if Library.exists (fn d =>
  1.1855 +                        case d of Datatype.DtTFree _ => false | _ => true) dtyps
  1.1856 +                      then
  1.1857 +                        raise REFUTE ("IDT_interpreter",
  1.1858 +                          "datatype argument (for type "
  1.1859 +                          ^ Syntax.string_of_typ ctxt (Type (s, Ts))
  1.1860 +                          ^ ") is not a variable")
  1.1861 +                      else ()
  1.1862 +                    (* if the model specifies a depth for the current type, *)
  1.1863 +                    (* decrement it to avoid infinite recursion             *)
  1.1864 +                    val typs' = case depth of NONE => typs | SOME n =>
  1.1865 +                      AList.update (op =) (Type (s, Ts), n-1) typs
  1.1866 +                    (* recursively compute the size of the datatype *)
  1.1867 +                    val size     = size_of_dtyp ctxt typs' descr typ_assoc constrs
  1.1868 +                    val next_idx = #next_idx args
  1.1869 +                    val next     = next_idx+size
  1.1870 +                    (* check if 'maxvars' is large enough *)
  1.1871 +                    val _        = (if next-1 > #maxvars args andalso
  1.1872 +                      #maxvars args > 0 then raise MAXVARS_EXCEEDED else ())
  1.1873 +                    (* prop_formula list *)
  1.1874 +                    val fms      = map BoolVar (next_idx upto (next_idx+size-1))
  1.1875 +                    (* interpretation *)
  1.1876 +                    val intr     = Leaf fms
  1.1877 +                    (* prop_formula list -> prop_formula *)
  1.1878 +                    fun one_of_two_false [] = True
  1.1879 +                      | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
  1.1880 +                          SOr (SNot x, SNot x')) xs), one_of_two_false xs)
  1.1881 +                    (* prop_formula *)
  1.1882 +                    val wf = one_of_two_false fms
  1.1883 +                  in
  1.1884 +                    (* extend the model, increase 'next_idx', add well-formedness *)
  1.1885 +                    (* condition                                                  *)
  1.1886 +                    SOME (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args,
  1.1887 +                      def_eq = #def_eq args, next_idx = next, bounds = #bounds args,
  1.1888 +                      wellformed = SAnd (#wellformed args, wf)})
  1.1889 +                  end
  1.1890 +              end
  1.1891 +          | NONE =>  (* not an inductive datatype *)
  1.1892 +              NONE)
  1.1893 +      | interpret_term _ =  (* a (free or schematic) type variable *)
  1.1894 +          NONE
  1.1895 +  in
  1.1896 +    case AList.lookup (op =) terms t of
  1.1897 +      SOME intr =>
  1.1898 +        (* return an existing interpretation *)
  1.1899 +        SOME (intr, model, args)
  1.1900 +    | NONE =>
  1.1901 +        (case t of
  1.1902 +          Free (_, T) => interpret_term T
  1.1903 +        | Var (_, T) => interpret_term T
  1.1904 +        | Const (_, T) => interpret_term T
  1.1905 +        | _ => NONE)
  1.1906 +  end;
  1.1907 +
  1.1908 +(* This function imposes an order on the elements of a datatype fragment  *)
  1.1909 +(* as follows: C_i x_1 ... x_n < C_j y_1 ... y_m iff i < j or             *)
  1.1910 +(* (x_1, ..., x_n) < (y_1, ..., y_m).  With this order, a constructor is  *)
  1.1911 +(* a function C_i that maps some argument indices x_1, ..., x_n to the    *)
  1.1912 +(* datatype element given by index C_i x_1 ... x_n.  The idea remains the *)
  1.1913 +(* same for recursive datatypes, although the computation of indices gets *)
  1.1914 +(* a little tricky.                                                       *)
  1.1915 +
  1.1916 +fun IDT_constructor_interpreter ctxt model args t =
  1.1917 +  let
  1.1918 +    val thy = Proof_Context.theory_of ctxt
  1.1919 +    (* returns a list of canonical representations for terms of the type 'T' *)
  1.1920 +    (* It would be nice if we could just use 'print' for this, but 'print'   *)
  1.1921 +    (* for IDTs calls 'IDT_constructor_interpreter' again, and this could    *)
  1.1922 +    (* lead to infinite recursion when we have (mutually) recursive IDTs.    *)
  1.1923 +    (* (Term.typ * int) list -> Term.typ -> Term.term list *)
  1.1924 +    fun canonical_terms typs T =
  1.1925 +          (case T of
  1.1926 +            Type ("fun", [T1, T2]) =>
  1.1927 +            (* 'T2' might contain a recursive IDT, so we cannot use 'print' (at *)
  1.1928 +            (* least not for 'T2'                                               *)
  1.1929 +            let
  1.1930 +              (* returns a list of lists, each one consisting of n (possibly *)
  1.1931 +              (* identical) elements from 'xs'                               *)
  1.1932 +              (* int -> 'a list -> 'a list list *)
  1.1933 +              fun pick_all 1 xs = map single xs
  1.1934 +                | pick_all n xs =
  1.1935 +                    let val rec_pick = pick_all (n-1) xs in
  1.1936 +                      maps (fn x => map (cons x) rec_pick) xs
  1.1937 +                    end
  1.1938 +              (* ["x1", ..., "xn"] *)
  1.1939 +              val terms1 = canonical_terms typs T1
  1.1940 +              (* ["y1", ..., "ym"] *)
  1.1941 +              val terms2 = canonical_terms typs T2
  1.1942 +              (* [[("x1", "y1"), ..., ("xn", "y1")], ..., *)
  1.1943 +              (*   [("x1", "ym"), ..., ("xn", "ym")]]     *)
  1.1944 +              val functions = map (curry (op ~~) terms1)
  1.1945 +                (pick_all (length terms1) terms2)
  1.1946 +              (* [["(x1, y1)", ..., "(xn, y1)"], ..., *)
  1.1947 +              (*   ["(x1, ym)", ..., "(xn, ym)"]]     *)
  1.1948 +              val pairss = map (map HOLogic.mk_prod) functions
  1.1949 +              (* Term.typ *)
  1.1950 +              val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
  1.1951 +              val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
  1.1952 +              (* Term.term *)
  1.1953 +              val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT)
  1.1954 +              val HOLogic_insert    =
  1.1955 +                Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
  1.1956 +            in
  1.1957 +              (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *)
  1.1958 +              map (fn ps => fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) ps
  1.1959 +                HOLogic_empty_set) pairss
  1.1960 +            end
  1.1961 +      | Type (s, Ts) =>
  1.1962 +          (case Datatype.get_info thy s of
  1.1963 +            SOME info =>
  1.1964 +              (case AList.lookup (op =) typs T of
  1.1965 +                SOME 0 =>
  1.1966 +                  (* termination condition to avoid infinite recursion *)
  1.1967 +                  []  (* at depth 0, every IDT is empty *)
  1.1968 +              | _ =>
  1.1969 +                let
  1.1970 +                  val index = #index info
  1.1971 +                  val descr = #descr info
  1.1972 +                  val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
  1.1973 +                  val typ_assoc = dtyps ~~ Ts
  1.1974 +                  (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1.1975 +                  val _ =
  1.1976 +                    if Library.exists (fn d =>
  1.1977 +                      case d of Datatype.DtTFree _ => false | _ => true) dtyps
  1.1978 +                    then
  1.1979 +                      raise REFUTE ("IDT_constructor_interpreter",
  1.1980 +                        "datatype argument (for type "
  1.1981 +                        ^ Syntax.string_of_typ ctxt T
  1.1982 +                        ^ ") is not a variable")
  1.1983 +                    else ()
  1.1984 +                  (* decrement depth for the IDT 'T' *)
  1.1985 +                  val typs' =
  1.1986 +                    (case AList.lookup (op =) typs T of NONE => typs
  1.1987 +                    | SOME n => AList.update (op =) (T, n-1) typs)
  1.1988 +                  fun constructor_terms terms [] = terms
  1.1989 +                    | constructor_terms terms (d::ds) =
  1.1990 +                        let
  1.1991 +                          val dT = typ_of_dtyp descr typ_assoc d
  1.1992 +                          val d_terms = canonical_terms typs' dT
  1.1993 +                        in
  1.1994 +                          (* C_i x_1 ... x_n < C_i y_1 ... y_n if *)
  1.1995 +                          (* (x_1, ..., x_n) < (y_1, ..., y_n)    *)
  1.1996 +                          constructor_terms
  1.1997 +                            (map_product (curry op $) terms d_terms) ds
  1.1998 +                        end
  1.1999 +                in
  1.2000 +                  (* C_i ... < C_j ... if i < j *)
  1.2001 +                  maps (fn (cname, ctyps) =>
  1.2002 +                    let
  1.2003 +                      val cTerm = Const (cname,
  1.2004 +                        map (typ_of_dtyp descr typ_assoc) ctyps ---> T)
  1.2005 +                    in
  1.2006 +                      constructor_terms [cTerm] ctyps
  1.2007 +                    end) constrs
  1.2008 +                end)
  1.2009 +          | NONE =>
  1.2010 +              (* not an inductive datatype; in this case the argument types in *)
  1.2011 +              (* 'Ts' may not be IDTs either, so 'print' should be safe        *)
  1.2012 +              map (fn intr => print ctxt (typs, []) T intr (K false))
  1.2013 +                (make_constants ctxt (typs, []) T))
  1.2014 +      | _ =>  (* TFree ..., TVar ... *)
  1.2015 +          map (fn intr => print ctxt (typs, []) T intr (K false))
  1.2016 +            (make_constants ctxt (typs, []) T))
  1.2017 +    val (typs, terms) = model
  1.2018 +  in
  1.2019 +    case AList.lookup (op =) terms t of
  1.2020 +      SOME intr =>
  1.2021 +        (* return an existing interpretation *)
  1.2022 +        SOME (intr, model, args)
  1.2023 +    | NONE =>
  1.2024 +        (case t of
  1.2025 +          Const (s, T) =>
  1.2026 +            (case body_type T of
  1.2027 +              Type (s', Ts') =>
  1.2028 +                (case Datatype.get_info thy s' of
  1.2029 +                  SOME info =>  (* body type is an inductive datatype *)
  1.2030 +                    let
  1.2031 +                      val index               = #index info
  1.2032 +                      val descr               = #descr info
  1.2033 +                      val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
  1.2034 +                      val typ_assoc           = dtyps ~~ Ts'
  1.2035 +                      (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1.2036 +                      val _ = if Library.exists (fn d =>
  1.2037 +                          case d of Datatype.DtTFree _ => false | _ => true) dtyps
  1.2038 +                        then
  1.2039 +                          raise REFUTE ("IDT_constructor_interpreter",
  1.2040 +                            "datatype argument (for type "
  1.2041 +                            ^ Syntax.string_of_typ ctxt (Type (s', Ts'))
  1.2042 +                            ^ ") is not a variable")
  1.2043 +                        else ()
  1.2044 +                      (* split the constructors into those occuring before/after *)
  1.2045 +                      (* 'Const (s, T)'                                          *)
  1.2046 +                      val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
  1.2047 +                        not (cname = s andalso Sign.typ_instance thy (T,
  1.2048 +                          map (typ_of_dtyp descr typ_assoc) ctypes
  1.2049 +                            ---> Type (s', Ts')))) constrs
  1.2050 +                    in
  1.2051 +                      case constrs2 of
  1.2052 +                        [] =>
  1.2053 +                          (* 'Const (s, T)' is not a constructor of this datatype *)
  1.2054 +                          NONE
  1.2055 +                      | (_, ctypes)::_ =>
  1.2056 +                          let
  1.2057 +                            (* int option -- only /recursive/ IDTs have an associated *)
  1.2058 +                            (*               depth                                    *)
  1.2059 +                            val depth = AList.lookup (op =) typs (Type (s', Ts'))
  1.2060 +                            (* this should never happen: at depth 0, this IDT fragment *)
  1.2061 +                            (* is definitely empty, and in this case we don't need to  *)
  1.2062 +                            (* interpret its constructors                              *)
  1.2063 +                            val _ = (case depth of SOME 0 =>
  1.2064 +                                raise REFUTE ("IDT_constructor_interpreter",
  1.2065 +                                  "depth is 0")
  1.2066 +                              | _ => ())
  1.2067 +                            val typs' = (case depth of NONE => typs | SOME n =>
  1.2068 +                              AList.update (op =) (Type (s', Ts'), n-1) typs)
  1.2069 +                            (* elements of the datatype come before elements generated *)
  1.2070 +                            (* by 'Const (s, T)' iff they are generated by a           *)
  1.2071 +                            (* constructor in constrs1                                 *)
  1.2072 +                            val offset = size_of_dtyp ctxt typs' descr typ_assoc constrs1
  1.2073 +                            (* compute the total (current) size of the datatype *)
  1.2074 +                            val total = offset +
  1.2075 +                              size_of_dtyp ctxt typs' descr typ_assoc constrs2
  1.2076 +                            (* sanity check *)
  1.2077 +                            val _ = if total <> size_of_type ctxt (typs, [])
  1.2078 +                              (Type (s', Ts')) then
  1.2079 +                                raise REFUTE ("IDT_constructor_interpreter",
  1.2080 +                                  "total is not equal to current size")
  1.2081 +                              else ()
  1.2082 +                            (* returns an interpretation where everything is mapped to *)
  1.2083 +                            (* an "undefined" element of the datatype                  *)
  1.2084 +                            fun make_undef [] = Leaf (replicate total False)
  1.2085 +                              | make_undef (d::ds) =
  1.2086 +                                  let
  1.2087 +                                    (* compute the current size of the type 'd' *)
  1.2088 +                                    val dT   = typ_of_dtyp descr typ_assoc d
  1.2089 +                                    val size = size_of_type ctxt (typs, []) dT
  1.2090 +                                  in
  1.2091 +                                    Node (replicate size (make_undef ds))
  1.2092 +                                  end
  1.2093 +                            (* returns the interpretation for a constructor *)
  1.2094 +                            fun make_constr [] offset =
  1.2095 +                                  if offset < total then
  1.2096 +                                    (Leaf (replicate offset False @ True ::
  1.2097 +                                      (replicate (total - offset - 1) False)), offset + 1)
  1.2098 +                                  else
  1.2099 +                                    raise REFUTE ("IDT_constructor_interpreter",
  1.2100 +                                      "offset >= total")
  1.2101 +                              | make_constr (d::ds) offset =
  1.2102 +                                  let
  1.2103 +                                    (* Term.typ *)
  1.2104 +                                    val dT = typ_of_dtyp descr typ_assoc d
  1.2105 +                                    (* compute canonical term representations for all   *)
  1.2106 +                                    (* elements of the type 'd' (with the reduced depth *)
  1.2107 +                                    (* for the IDT)                                     *)
  1.2108 +                                    val terms' = canonical_terms typs' dT
  1.2109 +                                    (* sanity check *)
  1.2110 +                                    val _ =
  1.2111 +                                      if length terms' <> size_of_type ctxt (typs', []) dT
  1.2112 +                                      then
  1.2113 +                                        raise REFUTE ("IDT_constructor_interpreter",
  1.2114 +                                          "length of terms' is not equal to old size")
  1.2115 +                                      else ()
  1.2116 +                                    (* compute canonical term representations for all   *)
  1.2117 +                                    (* elements of the type 'd' (with the current depth *)
  1.2118 +                                    (* for the IDT)                                     *)
  1.2119 +                                    val terms = canonical_terms typs dT
  1.2120 +                                    (* sanity check *)
  1.2121 +                                    val _ =
  1.2122 +                                      if length terms <> size_of_type ctxt (typs, []) dT
  1.2123 +                                      then
  1.2124 +                                        raise REFUTE ("IDT_constructor_interpreter",
  1.2125 +                                          "length of terms is not equal to current size")
  1.2126 +                                      else ()
  1.2127 +                                    (* sanity check *)
  1.2128 +                                    val _ =
  1.2129 +                                      if length terms < length terms' then
  1.2130 +                                        raise REFUTE ("IDT_constructor_interpreter",
  1.2131 +                                          "current size is less than old size")
  1.2132 +                                      else ()
  1.2133 +                                    (* sanity check: every element of terms' must also be *)
  1.2134 +                                    (*               present in terms                     *)
  1.2135 +                                    val _ =
  1.2136 +                                      if forall (member (op =) terms) terms' then ()
  1.2137 +                                      else
  1.2138 +                                        raise REFUTE ("IDT_constructor_interpreter",
  1.2139 +                                          "element has disappeared")
  1.2140 +                                    (* sanity check: the order on elements of terms' is    *)
  1.2141 +                                    (*               the same in terms, for those elements *)
  1.2142 +                                    val _ =
  1.2143 +                                      let
  1.2144 +                                        fun search (x::xs) (y::ys) =
  1.2145 +                                              if x = y then search xs ys else search (x::xs) ys
  1.2146 +                                          | search (_::_) [] =
  1.2147 +                                              raise REFUTE ("IDT_constructor_interpreter",
  1.2148 +                                                "element order not preserved")
  1.2149 +                                          | search [] _ = ()
  1.2150 +                                      in search terms' terms end
  1.2151 +                                    (* int * interpretation list *)
  1.2152 +                                    val (intrs, new_offset) =
  1.2153 +                                      fold_map (fn t_elem => fn off =>
  1.2154 +                                        (* if 't_elem' existed at the previous depth,    *)
  1.2155 +                                        (* proceed recursively, otherwise map the entire *)
  1.2156 +                                        (* subtree to "undefined"                        *)
  1.2157 +                                        if member (op =) terms' t_elem then
  1.2158 +                                          make_constr ds off
  1.2159 +                                        else
  1.2160 +                                          (make_undef ds, off))
  1.2161 +                                      terms offset
  1.2162 +                                  in
  1.2163 +                                    (Node intrs, new_offset)
  1.2164 +                                  end
  1.2165 +                          in
  1.2166 +                            SOME (fst (make_constr ctypes offset), model, args)
  1.2167 +                          end
  1.2168 +                    end
  1.2169 +                | NONE =>  (* body type is not an inductive datatype *)
  1.2170 +                    NONE)
  1.2171 +            | _ =>  (* body type is a (free or schematic) type variable *)
  1.2172 +              NONE)
  1.2173 +        | _ =>  (* term is not a constant *)
  1.2174 +          NONE)
  1.2175 +  end;
  1.2176 +
  1.2177 +(* Difficult code ahead.  Make sure you understand the                *)
  1.2178 +(* 'IDT_constructor_interpreter' and the order in which it enumerates *)
  1.2179 +(* elements of an IDT before you try to understand this function.     *)
  1.2180 +
  1.2181 +fun IDT_recursion_interpreter ctxt model args t =
  1.2182 +  let
  1.2183 +    val thy = Proof_Context.theory_of ctxt
  1.2184 +  in
  1.2185 +    (* careful: here we descend arbitrarily deep into 't', possibly before *)
  1.2186 +    (* any other interpreter for atomic terms has had a chance to look at  *)
  1.2187 +    (* 't'                                                                 *)
  1.2188 +    case strip_comb t of
  1.2189 +      (Const (s, T), params) =>
  1.2190 +        (* iterate over all datatypes in 'thy' *)
  1.2191 +        Symtab.fold (fn (_, info) => fn result =>
  1.2192 +          case result of
  1.2193 +            SOME _ =>
  1.2194 +              result  (* just keep 'result' *)
  1.2195 +          | NONE =>
  1.2196 +              if member (op =) (#rec_names info) s then
  1.2197 +                (* we do have a recursion operator of one of the (mutually *)
  1.2198 +                (* recursive) datatypes given by 'info'                    *)
  1.2199 +                let
  1.2200 +                  (* number of all constructors, including those of different  *)
  1.2201 +                  (* (mutually recursive) datatypes within the same descriptor *)
  1.2202 +                  val mconstrs_count =
  1.2203 +                    Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info))
  1.2204 +                in
  1.2205 +                  if mconstrs_count < length params then
  1.2206 +                    (* too many actual parameters; for now we'll use the *)
  1.2207 +                    (* 'stlc_interpreter' to strip off one application   *)
  1.2208 +                    NONE
  1.2209 +                  else if mconstrs_count > length params then
  1.2210 +                    (* too few actual parameters; we use eta expansion          *)
  1.2211 +                    (* Note that the resulting expansion of lambda abstractions *)
  1.2212 +                    (* by the 'stlc_interpreter' may be rather slow (depending  *)
  1.2213 +                    (* on the argument types and the size of the IDT, of        *)
  1.2214 +                    (* course).                                                 *)
  1.2215 +                    SOME (interpret ctxt model args (eta_expand t
  1.2216 +                      (mconstrs_count - length params)))
  1.2217 +                  else  (* mconstrs_count = length params *)
  1.2218 +                    let
  1.2219 +                      (* interpret each parameter separately *)
  1.2220 +                      val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) =>
  1.2221 +                        let
  1.2222 +                          val (i, m', a') = interpret ctxt m a p
  1.2223 +                        in
  1.2224 +                          (i, (m', a'))
  1.2225 +                        end) params (model, args)
  1.2226 +                      val (typs, _) = model'
  1.2227 +                      (* 'index' is /not/ necessarily the index of the IDT that *)
  1.2228 +                      (* the recursion operator is associated with, but merely  *)
  1.2229 +                      (* the index of some mutually recursive IDT               *)
  1.2230 +                      val index         = #index info
  1.2231 +                      val descr         = #descr info
  1.2232 +                      val (_, dtyps, _) = the (AList.lookup (op =) descr index)
  1.2233 +                      (* sanity check: we assume that the order of constructors *)
  1.2234 +                      (*               in 'descr' is the same as the order of   *)
  1.2235 +                      (*               corresponding parameters, otherwise the  *)
  1.2236 +                      (*               association code below won't match the   *)
  1.2237 +                      (*               right constructors/parameters; we also   *)
  1.2238 +                      (*               assume that the order of recursion       *)
  1.2239 +                      (*               operators in '#rec_names info' is the    *)
  1.2240 +                      (*               same as the order of corresponding       *)
  1.2241 +                      (*               datatypes in 'descr'                     *)
  1.2242 +                      val _ = if map fst descr <> (0 upto (length descr - 1)) then
  1.2243 +                          raise REFUTE ("IDT_recursion_interpreter",
  1.2244 +                            "order of constructors and corresponding parameters/" ^
  1.2245 +                              "recursion operators and corresponding datatypes " ^
  1.2246 +                              "different?")
  1.2247 +                        else ()
  1.2248 +                      (* sanity check: every element in 'dtyps' must be a *)
  1.2249 +                      (*               'DtTFree'                          *)
  1.2250 +                      val _ =
  1.2251 +                        if Library.exists (fn d =>
  1.2252 +                          case d of Datatype.DtTFree _ => false
  1.2253 +                                  | _ => true) dtyps
  1.2254 +                        then
  1.2255 +                          raise REFUTE ("IDT_recursion_interpreter",
  1.2256 +                            "datatype argument is not a variable")
  1.2257 +                        else ()
  1.2258 +                      (* the type of a recursion operator is *)
  1.2259 +                      (* [T1, ..., Tn, IDT] ---> Tresult     *)
  1.2260 +                      val IDT = nth (binder_types T) mconstrs_count
  1.2261 +                      (* by our assumption on the order of recursion operators *)
  1.2262 +                      (* and datatypes, this is the index of the datatype      *)
  1.2263 +                      (* corresponding to the given recursion operator         *)
  1.2264 +                      val idt_index = find_index (fn s' => s' = s) (#rec_names info)
  1.2265 +                      (* mutually recursive types must have the same type   *)
  1.2266 +                      (* parameters, unless the mutual recursion comes from *)
  1.2267 +                      (* indirect recursion                                 *)
  1.2268 +                      fun rec_typ_assoc acc [] = acc
  1.2269 +                        | rec_typ_assoc acc ((d, T)::xs) =
  1.2270 +                            (case AList.lookup op= acc d of
  1.2271 +                              NONE =>
  1.2272 +                                (case d of
  1.2273 +                                  Datatype.DtTFree _ =>
  1.2274 +                                  (* add the association, proceed *)
  1.2275 +                                  rec_typ_assoc ((d, T)::acc) xs
  1.2276 +                                | Datatype.DtType (s, ds) =>
  1.2277 +                                    let
  1.2278 +                                      val (s', Ts) = dest_Type T
  1.2279 +                                    in
  1.2280 +                                      if s=s' then
  1.2281 +                                        rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs)
  1.2282 +                                      else
  1.2283 +                                        raise REFUTE ("IDT_recursion_interpreter",
  1.2284 +                                          "DtType/Type mismatch")
  1.2285 +                                    end
  1.2286 +                                | Datatype.DtRec i =>
  1.2287 +                                    let
  1.2288 +                                      val (_, ds, _) = the (AList.lookup (op =) descr i)
  1.2289 +                                      val (_, Ts)    = dest_Type T
  1.2290 +                                    in
  1.2291 +                                      rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs)
  1.2292 +                                    end)
  1.2293 +                            | SOME T' =>
  1.2294 +                                if T=T' then
  1.2295 +                                  (* ignore the association since it's already *)
  1.2296 +                                  (* present, proceed                          *)
  1.2297 +                                  rec_typ_assoc acc xs
  1.2298 +                                else
  1.2299 +                                  raise REFUTE ("IDT_recursion_interpreter",
  1.2300 +                                    "different type associations for the same dtyp"))
  1.2301 +                      val typ_assoc = filter
  1.2302 +                        (fn (Datatype.DtTFree _, _) => true | (_, _) => false)
  1.2303 +                        (rec_typ_assoc []
  1.2304 +                          (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
  1.2305 +                      (* sanity check: typ_assoc must associate types to the   *)
  1.2306 +                      (*               elements of 'dtyps' (and only to those) *)
  1.2307 +                      val _ =
  1.2308 +                        if not (eq_set (op =) (dtyps, map fst typ_assoc))
  1.2309 +                        then
  1.2310 +                          raise REFUTE ("IDT_recursion_interpreter",
  1.2311 +                            "type association has extra/missing elements")
  1.2312 +                        else ()
  1.2313 +                      (* interpret each constructor in the descriptor (including *)
  1.2314 +                      (* those of mutually recursive datatypes)                  *)
  1.2315 +                      (* (int * interpretation list) list *)
  1.2316 +                      val mc_intrs = map (fn (idx, (_, _, cs)) =>
  1.2317 +                        let
  1.2318 +                          val c_return_typ = typ_of_dtyp descr typ_assoc
  1.2319 +                            (Datatype.DtRec idx)
  1.2320 +                        in
  1.2321 +                          (idx, map (fn (cname, cargs) =>
  1.2322 +                            (#1 o interpret ctxt (typs, []) {maxvars=0,
  1.2323 +                              def_eq=false, next_idx=1, bounds=[],
  1.2324 +                              wellformed=True}) (Const (cname, map (typ_of_dtyp
  1.2325 +                              descr typ_assoc) cargs ---> c_return_typ))) cs)
  1.2326 +                        end) descr
  1.2327 +                      (* associate constructors with corresponding parameters *)
  1.2328 +                      (* (int * (interpretation * interpretation) list) list *)
  1.2329 +                      val (mc_p_intrs, p_intrs') = fold_map
  1.2330 +                        (fn (idx, c_intrs) => fn p_intrs' =>
  1.2331 +                          let
  1.2332 +                            val len = length c_intrs
  1.2333 +                          in
  1.2334 +                            ((idx, c_intrs ~~ List.take (p_intrs', len)),
  1.2335 +                              List.drop (p_intrs', len))
  1.2336 +                          end) mc_intrs p_intrs
  1.2337 +                      (* sanity check: no 'p_intr' may be left afterwards *)
  1.2338 +                      val _ =
  1.2339 +                        if p_intrs' <> [] then
  1.2340 +                          raise REFUTE ("IDT_recursion_interpreter",
  1.2341 +                            "more parameter than constructor interpretations")
  1.2342 +                        else ()
  1.2343 +                      (* The recursion operator, applied to 'mconstrs_count'     *)
  1.2344 +                      (* arguments, is a function that maps every element of the *)
  1.2345 +                      (* inductive datatype to an element of some result type.   *)
  1.2346 +                      (* Recursion operators for mutually recursive IDTs are     *)
  1.2347 +                      (* translated simultaneously.                              *)
  1.2348 +                      (* Since the order on datatype elements is given by an     *)
  1.2349 +                      (* order on constructors (and then by the order on         *)
  1.2350 +                      (* argument tuples), we can simply copy corresponding      *)
  1.2351 +                      (* subtrees from 'p_intrs', in the order in which they are *)
  1.2352 +                      (* given.                                                  *)
  1.2353 +                      (* interpretation * interpretation -> interpretation list *)
  1.2354 +                      fun ci_pi (Leaf xs, pi) =
  1.2355 +                            (* if the constructor does not match the arguments to a *)
  1.2356 +                            (* defined element of the IDT, the corresponding value  *)
  1.2357 +                            (* of the parameter must be ignored                     *)
  1.2358 +                            if List.exists (equal True) xs then [pi] else []
  1.2359 +                        | ci_pi (Node xs, Node ys) = maps ci_pi (xs ~~ ys)
  1.2360 +                        | ci_pi (Node _, Leaf _) =
  1.2361 +                            raise REFUTE ("IDT_recursion_interpreter",
  1.2362 +                              "constructor takes more arguments than the " ^
  1.2363 +                                "associated parameter")
  1.2364 +                      (* (int * interpretation list) list *)
  1.2365 +                      val rec_operators = map (fn (idx, c_p_intrs) =>
  1.2366 +                        (idx, maps ci_pi c_p_intrs)) mc_p_intrs
  1.2367 +                      (* sanity check: every recursion operator must provide as  *)
  1.2368 +                      (*               many values as the corresponding datatype *)
  1.2369 +                      (*               has elements                              *)
  1.2370 +                      val _ = map (fn (idx, intrs) =>
  1.2371 +                        let
  1.2372 +                          val T = typ_of_dtyp descr typ_assoc
  1.2373 +                            (Datatype.DtRec idx)
  1.2374 +                        in
  1.2375 +                          if length intrs <> size_of_type ctxt (typs, []) T then
  1.2376 +                            raise REFUTE ("IDT_recursion_interpreter",
  1.2377 +                              "wrong number of interpretations for rec. operator")
  1.2378 +                          else ()
  1.2379 +                        end) rec_operators
  1.2380 +                      (* For non-recursive datatypes, we are pretty much done at *)
  1.2381 +                      (* this point.  For recursive datatypes however, we still  *)
  1.2382 +                      (* need to apply the interpretations in 'rec_operators' to *)
  1.2383 +                      (* (recursively obtained) interpretations for recursive    *)
  1.2384 +                      (* constructor arguments.  To do so more efficiently, we   *)
  1.2385 +                      (* copy 'rec_operators' into arrays first.  Each Boolean   *)
  1.2386 +                      (* indicates whether the recursive arguments have been     *)
  1.2387 +                      (* considered already.                                     *)
  1.2388 +                      (* (int * (bool * interpretation) Array.array) list *)
  1.2389 +                      val REC_OPERATORS = map (fn (idx, intrs) =>
  1.2390 +                        (idx, Array.fromList (map (pair false) intrs)))
  1.2391 +                        rec_operators
  1.2392 +                      (* takes an interpretation, and if some leaf of this     *)
  1.2393 +                      (* interpretation is the 'elem'-th element of the type,  *)
  1.2394 +                      (* the indices of the arguments leading to this leaf are *)
  1.2395 +                      (* returned                                              *)
  1.2396 +                      (* interpretation -> int -> int list option *)
  1.2397 +                      fun get_args (Leaf xs) elem =
  1.2398 +                            if find_index (fn x => x = True) xs = elem then
  1.2399 +                              SOME []
  1.2400 +                            else
  1.2401 +                              NONE
  1.2402 +                        | get_args (Node xs) elem =
  1.2403 +                            let
  1.2404 +                              (* interpretation list * int -> int list option *)
  1.2405 +                              fun search ([], _) =
  1.2406 +                                NONE
  1.2407 +                                | search (x::xs, n) =
  1.2408 +                                (case get_args x elem of
  1.2409 +                                  SOME result => SOME (n::result)
  1.2410 +                                | NONE        => search (xs, n+1))
  1.2411 +                            in
  1.2412 +                              search (xs, 0)
  1.2413 +                            end
  1.2414 +                      (* returns the index of the constructor and indices for *)
  1.2415 +                      (* its arguments that generate the 'elem'-th element of *)
  1.2416 +                      (* the datatype given by 'idx'                          *)
  1.2417 +                      (* int -> int -> int * int list *)
  1.2418 +                      fun get_cargs idx elem =
  1.2419 +                        let
  1.2420 +                          (* int * interpretation list -> int * int list *)
  1.2421 +                          fun get_cargs_rec (_, []) =
  1.2422 +                                raise REFUTE ("IDT_recursion_interpreter",
  1.2423 +                                  "no matching constructor found for datatype element")
  1.2424 +                            | get_cargs_rec (n, x::xs) =
  1.2425 +                                (case get_args x elem of
  1.2426 +                                  SOME args => (n, args)
  1.2427 +                                | NONE => get_cargs_rec (n+1, xs))
  1.2428 +                        in
  1.2429 +                          get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx))
  1.2430 +                        end
  1.2431 +                      (* computes one entry in 'REC_OPERATORS', and recursively *)
  1.2432 +                      (* all entries needed for it, where 'idx' gives the       *)
  1.2433 +                      (* datatype and 'elem' the element of it                  *)
  1.2434 +                      (* int -> int -> interpretation *)
  1.2435 +                      fun compute_array_entry idx elem =
  1.2436 +                        let
  1.2437 +                          val arr = the (AList.lookup (op =) REC_OPERATORS idx)
  1.2438 +                          val (flag, intr) = Array.sub (arr, elem)
  1.2439 +                        in
  1.2440 +                          if flag then
  1.2441 +                            (* simply return the previously computed result *)
  1.2442 +                            intr
  1.2443 +                          else
  1.2444 +                            (* we have to apply 'intr' to interpretations for all *)
  1.2445 +                            (* recursive arguments                                *)
  1.2446 +                            let
  1.2447 +                              (* int * int list *)
  1.2448 +                              val (c, args) = get_cargs idx elem
  1.2449 +                              (* find the indices of the constructor's /recursive/ *)
  1.2450 +                              (* arguments                                         *)
  1.2451 +                              val (_, _, constrs) = the (AList.lookup (op =) descr idx)
  1.2452 +                              val (_, dtyps) = nth constrs c
  1.2453 +                              val rec_dtyps_args = filter
  1.2454 +                                (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args)
  1.2455 +                              (* map those indices to interpretations *)
  1.2456 +                              val rec_dtyps_intrs = map (fn (dtyp, arg) =>
  1.2457 +                                let
  1.2458 +                                  val dT = typ_of_dtyp descr typ_assoc dtyp
  1.2459 +                                  val consts = make_constants ctxt (typs, []) dT
  1.2460 +                                  val arg_i = nth consts arg
  1.2461 +                                in
  1.2462 +                                  (dtyp, arg_i)
  1.2463 +                                end) rec_dtyps_args
  1.2464 +                              (* takes the dtyp and interpretation of an element, *)
  1.2465 +                              (* and computes the interpretation for the          *)
  1.2466 +                              (* corresponding recursive argument                 *)
  1.2467 +                              fun rec_intr (Datatype.DtRec i) (Leaf xs) =
  1.2468 +                                    (* recursive argument is "rec_i params elem" *)
  1.2469 +                                    compute_array_entry i (find_index (fn x => x = True) xs)
  1.2470 +                                | rec_intr (Datatype.DtRec _) (Node _) =
  1.2471 +                                    raise REFUTE ("IDT_recursion_interpreter",
  1.2472 +                                      "interpretation for IDT is a node")
  1.2473 +                                | rec_intr (Datatype.DtType ("fun", [_, dt2])) (Node xs) =
  1.2474 +                                    (* recursive argument is something like     *)
  1.2475 +                                    (* "\<lambda>x::dt1. rec_? params (elem x)" *)
  1.2476 +                                    Node (map (rec_intr dt2) xs)
  1.2477 +                                | rec_intr (Datatype.DtType ("fun", [_, _])) (Leaf _) =
  1.2478 +                                    raise REFUTE ("IDT_recursion_interpreter",
  1.2479 +                                      "interpretation for function dtyp is a leaf")
  1.2480 +                                | rec_intr _ _ =
  1.2481 +                                    (* admissibility ensures that every recursive type *)
  1.2482 +                                    (* is of the form 'Dt_1 -> ... -> Dt_k ->          *)
  1.2483 +                                    (* (DtRec i)'                                      *)
  1.2484 +                                    raise REFUTE ("IDT_recursion_interpreter",
  1.2485 +                                      "non-recursive codomain in recursive dtyp")
  1.2486 +                              (* obtain interpretations for recursive arguments *)
  1.2487 +                              (* interpretation list *)
  1.2488 +                              val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs
  1.2489 +                              (* apply 'intr' to all recursive arguments *)
  1.2490 +                              val result = fold (fn arg_i => fn i =>
  1.2491 +                                interpretation_apply (i, arg_i)) arg_intrs intr
  1.2492 +                              (* update 'REC_OPERATORS' *)
  1.2493 +                              val _ = Array.update (arr, elem, (true, result))
  1.2494 +                            in
  1.2495 +                              result
  1.2496 +                            end
  1.2497 +                        end
  1.2498 +                      val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index))
  1.2499 +                      (* sanity check: the size of 'IDT' should be 'idt_size' *)
  1.2500 +                      val _ =
  1.2501 +                          if idt_size <> size_of_type ctxt (typs, []) IDT then
  1.2502 +                            raise REFUTE ("IDT_recursion_interpreter",
  1.2503 +                              "unexpected size of IDT (wrong type associated?)")
  1.2504 +                          else ()
  1.2505 +                      (* interpretation *)
  1.2506 +                      val rec_op = Node (map_range (compute_array_entry idt_index) idt_size)
  1.2507 +                    in
  1.2508 +                      SOME (rec_op, model', args')
  1.2509 +                    end
  1.2510 +                end
  1.2511 +              else
  1.2512 +                NONE  (* not a recursion operator of this datatype *)
  1.2513 +          ) (Datatype.get_all thy) NONE
  1.2514 +    | _ =>  (* head of term is not a constant *)
  1.2515 +      NONE
  1.2516 +  end;
  1.2517 +
  1.2518 +fun set_interpreter ctxt model args t =
  1.2519 +  let
  1.2520 +    val (typs, terms) = model
  1.2521 +  in
  1.2522 +    case AList.lookup (op =) terms t of
  1.2523 +      SOME intr =>
  1.2524 +        (* return an existing interpretation *)
  1.2525 +        SOME (intr, model, args)
  1.2526 +    | NONE =>
  1.2527 +        (case t of
  1.2528 +          Free (x, Type (@{type_name set}, [T])) =>
  1.2529 +          let
  1.2530 +            val (intr, _, args') =
  1.2531 +              interpret ctxt (typs, []) args (Free (x, T --> HOLogic.boolT))
  1.2532 +          in
  1.2533 +            SOME (intr, (typs, (t, intr)::terms), args')
  1.2534 +          end
  1.2535 +        | Var ((x, i), Type (@{type_name set}, [T])) =>
  1.2536 +          let
  1.2537 +            val (intr, _, args') =
  1.2538 +              interpret ctxt (typs, []) args (Var ((x,i), T --> HOLogic.boolT))
  1.2539 +          in
  1.2540 +            SOME (intr, (typs, (t, intr)::terms), args')
  1.2541 +          end
  1.2542 +        | Const (s, Type (@{type_name set}, [T])) =>
  1.2543 +          let
  1.2544 +            val (intr, _, args') =
  1.2545 +              interpret ctxt (typs, []) args (Const (s, T --> HOLogic.boolT))
  1.2546 +          in
  1.2547 +            SOME (intr, (typs, (t, intr)::terms), args')
  1.2548 +          end
  1.2549 +        (* 'Collect' == identity *)
  1.2550 +        | Const (@{const_name Collect}, _) $ t1 =>
  1.2551 +            SOME (interpret ctxt model args t1)
  1.2552 +        | Const (@{const_name Collect}, _) =>
  1.2553 +            SOME (interpret ctxt model args (eta_expand t 1))
  1.2554 +        (* 'op :' == application *)
  1.2555 +        | Const (@{const_name Set.member}, _) $ t1 $ t2 =>
  1.2556 +            SOME (interpret ctxt model args (t2 $ t1))
  1.2557 +        | Const (@{const_name Set.member}, _) $ _ =>
  1.2558 +            SOME (interpret ctxt model args (eta_expand t 1))
  1.2559 +        | Const (@{const_name Set.member}, _) =>
  1.2560 +            SOME (interpret ctxt model args (eta_expand t 2))
  1.2561 +        | _ => NONE)
  1.2562 +  end;
  1.2563 +
  1.2564 +(* only an optimization: 'card' could in principle be interpreted with *)
  1.2565 +(* interpreters available already (using its definition), but the code *)
  1.2566 +(* below is more efficient                                             *)
  1.2567 +
  1.2568 +fun Finite_Set_card_interpreter ctxt model args t =
  1.2569 +  case t of
  1.2570 +    Const (@{const_name Finite_Set.card},
  1.2571 +        Type ("fun", [Type (@{type_name set}, [T]), @{typ nat}])) =>
  1.2572 +      let
  1.2573 +        (* interpretation -> int *)
  1.2574 +        fun number_of_elements (Node xs) =
  1.2575 +            fold (fn x => fn n =>
  1.2576 +              if x = TT then
  1.2577 +                n + 1
  1.2578 +              else if x = FF then
  1.2579 +                n
  1.2580 +              else
  1.2581 +                raise REFUTE ("Finite_Set_card_interpreter",
  1.2582 +                  "interpretation for set type does not yield a Boolean"))
  1.2583 +              xs 0
  1.2584 +          | number_of_elements (Leaf _) =
  1.2585 +              raise REFUTE ("Finite_Set_card_interpreter",
  1.2586 +                "interpretation for set type is a leaf")
  1.2587 +        val size_of_nat = size_of_type ctxt model (@{typ nat})
  1.2588 +        (* takes an interpretation for a set and returns an interpretation *)
  1.2589 +        (* for a 'nat' denoting the set's cardinality                      *)
  1.2590 +        (* interpretation -> interpretation *)
  1.2591 +        fun card i =
  1.2592 +          let
  1.2593 +            val n = number_of_elements i
  1.2594 +          in
  1.2595 +            if n < size_of_nat then
  1.2596 +              Leaf ((replicate n False) @ True ::
  1.2597 +                (replicate (size_of_nat-n-1) False))
  1.2598 +            else
  1.2599 +              Leaf (replicate size_of_nat False)
  1.2600 +          end
  1.2601 +        val set_constants = make_constants ctxt model (HOLogic.mk_setT T)
  1.2602 +      in
  1.2603 +        SOME (Node (map card set_constants), model, args)
  1.2604 +      end
  1.2605 +  | _ => NONE;
  1.2606 +
  1.2607 +(* only an optimization: 'finite' could in principle be interpreted with  *)
  1.2608 +(* interpreters available already (using its definition), but the code    *)
  1.2609 +(* below is more efficient                                                *)
  1.2610 +
  1.2611 +fun Finite_Set_finite_interpreter ctxt model args t =
  1.2612 +  case t of
  1.2613 +    Const (@{const_name Finite_Set.finite},
  1.2614 +           Type ("fun", [_, @{typ bool}])) $ _ =>
  1.2615 +        (* we only consider finite models anyway, hence EVERY set is *)
  1.2616 +        (* "finite"                                                  *)
  1.2617 +        SOME (TT, model, args)
  1.2618 +  | Const (@{const_name Finite_Set.finite},
  1.2619 +           Type ("fun", [set_T, @{typ bool}])) =>
  1.2620 +      let
  1.2621 +        val size_of_set = size_of_type ctxt model set_T
  1.2622 +      in
  1.2623 +        (* we only consider finite models anyway, hence EVERY set is *)
  1.2624 +        (* "finite"                                                  *)
  1.2625 +        SOME (Node (replicate size_of_set TT), model, args)
  1.2626 +      end
  1.2627 +  | _ => NONE;
  1.2628 +
  1.2629 +(* only an optimization: 'less' could in principle be interpreted with *)
  1.2630 +(* interpreters available already (using its definition), but the code     *)
  1.2631 +(* below is more efficient                                                 *)
  1.2632 +
  1.2633 +fun Nat_less_interpreter ctxt model args t =
  1.2634 +  case t of
  1.2635 +    Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
  1.2636 +        Type ("fun", [@{typ nat}, @{typ bool}])])) =>
  1.2637 +      let
  1.2638 +        val size_of_nat = size_of_type ctxt model (@{typ nat})
  1.2639 +        (* the 'n'-th nat is not less than the first 'n' nats, while it *)
  1.2640 +        (* is less than the remaining 'size_of_nat - n' nats            *)
  1.2641 +        (* int -> interpretation *)
  1.2642 +        fun less n = Node ((replicate n FF) @ (replicate (size_of_nat - n) TT))
  1.2643 +      in
  1.2644 +        SOME (Node (map less (1 upto size_of_nat)), model, args)
  1.2645 +      end
  1.2646 +  | _ => NONE;
  1.2647 +
  1.2648 +(* only an optimization: 'plus' could in principle be interpreted with *)
  1.2649 +(* interpreters available already (using its definition), but the code     *)
  1.2650 +(* below is more efficient                                                 *)
  1.2651 +
  1.2652 +fun Nat_plus_interpreter ctxt model args t =
  1.2653 +  case t of
  1.2654 +    Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
  1.2655 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
  1.2656 +      let
  1.2657 +        val size_of_nat = size_of_type ctxt model (@{typ nat})
  1.2658 +        (* int -> int -> interpretation *)
  1.2659 +        fun plus m n =
  1.2660 +          let
  1.2661 +            val element = m + n
  1.2662 +          in
  1.2663 +            if element > size_of_nat - 1 then
  1.2664 +              Leaf (replicate size_of_nat False)
  1.2665 +            else
  1.2666 +              Leaf ((replicate element False) @ True ::
  1.2667 +                (replicate (size_of_nat - element - 1) False))
  1.2668 +          end
  1.2669 +      in
  1.2670 +        SOME (Node (map_range (fn m => Node (map_range (plus m) size_of_nat)) size_of_nat),
  1.2671 +          model, args)
  1.2672 +      end
  1.2673 +  | _ => NONE;
  1.2674 +
  1.2675 +(* only an optimization: 'minus' could in principle be interpreted *)
  1.2676 +(* with interpreters available already (using its definition), but the *)
  1.2677 +(* code below is more efficient                                        *)
  1.2678 +
  1.2679 +fun Nat_minus_interpreter ctxt model args t =
  1.2680 +  case t of
  1.2681 +    Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
  1.2682 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
  1.2683 +      let
  1.2684 +        val size_of_nat = size_of_type ctxt model (@{typ nat})
  1.2685 +        (* int -> int -> interpretation *)
  1.2686 +        fun minus m n =
  1.2687 +          let
  1.2688 +            val element = Int.max (m-n, 0)
  1.2689 +          in
  1.2690 +            Leaf ((replicate element False) @ True ::
  1.2691 +              (replicate (size_of_nat - element - 1) False))
  1.2692 +          end
  1.2693 +      in
  1.2694 +        SOME (Node (map_range (fn m => Node (map_range (minus m) size_of_nat)) size_of_nat),
  1.2695 +          model, args)
  1.2696 +      end
  1.2697 +  | _ => NONE;
  1.2698 +
  1.2699 +(* only an optimization: 'times' could in principle be interpreted *)
  1.2700 +(* with interpreters available already (using its definition), but the *)
  1.2701 +(* code below is more efficient                                        *)
  1.2702 +
  1.2703 +fun Nat_times_interpreter ctxt model args t =
  1.2704 +  case t of
  1.2705 +    Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
  1.2706 +        Type ("fun", [@{typ nat}, @{typ nat}])])) =>
  1.2707 +      let
  1.2708 +        val size_of_nat = size_of_type ctxt model (@{typ nat})
  1.2709 +        (* nat -> nat -> interpretation *)
  1.2710 +        fun mult m n =
  1.2711 +          let
  1.2712 +            val element = m * n
  1.2713 +          in
  1.2714 +            if element > size_of_nat - 1 then
  1.2715 +              Leaf (replicate size_of_nat False)
  1.2716 +            else
  1.2717 +              Leaf ((replicate element False) @ True ::
  1.2718 +                (replicate (size_of_nat - element - 1) False))
  1.2719 +          end
  1.2720 +      in
  1.2721 +        SOME (Node (map_range (fn m => Node (map_range (mult m) size_of_nat)) size_of_nat),
  1.2722 +          model, args)
  1.2723 +      end
  1.2724 +  | _ => NONE;
  1.2725 +
  1.2726 +(* only an optimization: 'append' could in principle be interpreted with *)
  1.2727 +(* interpreters available already (using its definition), but the code   *)
  1.2728 +(* below is more efficient                                               *)
  1.2729 +
  1.2730 +fun List_append_interpreter ctxt model args t =
  1.2731 +  case t of
  1.2732 +    Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun",
  1.2733 +        [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
  1.2734 +      let
  1.2735 +        val size_elem = size_of_type ctxt model T
  1.2736 +        val size_list = size_of_type ctxt model (Type ("List.list", [T]))
  1.2737 +        (* maximal length of lists; 0 if we only consider the empty list *)
  1.2738 +        val list_length =
  1.2739 +          let
  1.2740 +            (* int -> int -> int -> int *)
  1.2741 +            fun list_length_acc len lists total =
  1.2742 +              if lists = total then
  1.2743 +                len
  1.2744 +              else if lists < total then
  1.2745 +                list_length_acc (len+1) (lists*size_elem) (total-lists)
  1.2746 +              else
  1.2747 +                raise REFUTE ("List_append_interpreter",
  1.2748 +                  "size_list not equal to 1 + size_elem + ... + " ^
  1.2749 +                    "size_elem^len, for some len")
  1.2750 +          in
  1.2751 +            list_length_acc 0 1 size_list
  1.2752 +          end
  1.2753 +        val elements = 0 upto (size_list-1)
  1.2754 +        (* FIXME: there should be a nice formula, which computes the same as *)
  1.2755 +        (*        the following, but without all this intermediate tree      *)
  1.2756 +        (*        length/offset stuff                                        *)
  1.2757 +        (* associate each list with its length and offset in a complete tree *)
  1.2758 +        (* of width 'size_elem' and depth 'length_list' (with 'size_list'    *)
  1.2759 +        (* nodes total)                                                      *)
  1.2760 +        (* (int * (int * int)) list *)
  1.2761 +        val (lenoff_lists, _) = fold_map (fn elem => fn (offsets, off) =>
  1.2762 +          (* corresponds to a pre-order traversal of the tree *)
  1.2763 +          let
  1.2764 +            val len = length offsets
  1.2765 +            (* associate the given element with len/off *)
  1.2766 +            val assoc = (elem, (len, off))
  1.2767 +          in
  1.2768 +            if len < list_length then
  1.2769 +              (* go to first child node *)
  1.2770 +              (assoc, (off :: offsets, off * size_elem))
  1.2771 +            else if off mod size_elem < size_elem - 1 then
  1.2772 +              (* go to next sibling node *)
  1.2773 +              (assoc, (offsets, off + 1))
  1.2774 +            else
  1.2775 +              (* go back up the stack until we find a level where we can go *)
  1.2776 +              (* to the next sibling node                                   *)
  1.2777 +              let
  1.2778 +                val offsets' = snd (take_prefix
  1.2779 +                  (fn off' => off' mod size_elem = size_elem - 1) offsets)
  1.2780 +              in
  1.2781 +                case offsets' of
  1.2782 +                  [] =>
  1.2783 +                    (* we're at the last node in the tree; the next value *)
  1.2784 +                    (* won't be used anyway                               *)
  1.2785 +                    (assoc, ([], 0))
  1.2786 +                | off'::offs' =>
  1.2787 +                    (* go to next sibling node *)
  1.2788 +                    (assoc, (offs', off' + 1))
  1.2789 +              end
  1.2790 +          end) elements ([], 0)
  1.2791 +        (* we also need the reverse association (from length/offset to *)
  1.2792 +        (* index)                                                      *)
  1.2793 +        val lenoff'_lists = map Library.swap lenoff_lists
  1.2794 +        (* returns the interpretation for "(list no. m) @ (list no. n)" *)
  1.2795 +        (* nat -> nat -> interpretation *)
  1.2796 +        fun append m n =
  1.2797 +          let
  1.2798 +            val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m)
  1.2799 +            val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n)
  1.2800 +            val len_elem = len_m + len_n
  1.2801 +            val off_elem = off_m * Integer.pow len_n size_elem + off_n
  1.2802 +          in
  1.2803 +            case AList.lookup op= lenoff'_lists (len_elem, off_elem) of
  1.2804 +              NONE =>
  1.2805 +                (* undefined *)
  1.2806 +                Leaf (replicate size_list False)
  1.2807 +            | SOME element =>
  1.2808 +                Leaf ((replicate element False) @ True ::
  1.2809 +                  (replicate (size_list - element - 1) False))
  1.2810 +          end
  1.2811 +      in
  1.2812 +        SOME (Node (map (fn m => Node (map (append m) elements)) elements),
  1.2813 +          model, args)
  1.2814 +      end
  1.2815 +  | _ => NONE;
  1.2816 +
  1.2817 +(* only an optimization: 'lfp' could in principle be interpreted with  *)
  1.2818 +(* interpreters available already (using its definition), but the code *)
  1.2819 +(* below is more efficient                                             *)
  1.2820 +
  1.2821 +fun lfp_interpreter ctxt model args t =
  1.2822 +  case t of
  1.2823 +    Const (@{const_name lfp}, Type ("fun", [Type ("fun",
  1.2824 +      [Type (@{type_name set}, [T]),
  1.2825 +       Type (@{type_name set}, [_])]),
  1.2826 +       Type (@{type_name set}, [_])])) =>
  1.2827 +      let
  1.2828 +        val size_elem = size_of_type ctxt model T
  1.2829 +        (* the universe (i.e. the set that contains every element) *)
  1.2830 +        val i_univ = Node (replicate size_elem TT)
  1.2831 +        (* all sets with elements from type 'T' *)
  1.2832 +        val i_sets = make_constants ctxt model (HOLogic.mk_setT T)
  1.2833 +        (* all functions that map sets to sets *)
  1.2834 +        val i_funs = make_constants ctxt model (Type ("fun",
  1.2835 +          [HOLogic.mk_setT T, HOLogic.mk_setT T]))
  1.2836 +        (* "lfp(f) == Inter({u. f(u) <= u})" *)
  1.2837 +        (* interpretation * interpretation -> bool *)
  1.2838 +        fun is_subset (Node subs, Node sups) =
  1.2839 +              forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups)
  1.2840 +          | is_subset (_, _) =
  1.2841 +              raise REFUTE ("lfp_interpreter",
  1.2842 +                "is_subset: interpretation for set is not a node")
  1.2843 +        (* interpretation * interpretation -> interpretation *)
  1.2844 +        fun intersection (Node xs, Node ys) =
  1.2845 +              Node (map (fn (x, y) => if x=TT andalso y=TT then TT else FF)
  1.2846 +                (xs ~~ ys))
  1.2847 +          | intersection (_, _) =
  1.2848 +              raise REFUTE ("lfp_interpreter",
  1.2849 +                "intersection: interpretation for set is not a node")
  1.2850 +        (* interpretation -> interpretaion *)
  1.2851 +        fun lfp (Node resultsets) =
  1.2852 +              fold (fn (set, resultset) => fn acc =>
  1.2853 +                if is_subset (resultset, set) then
  1.2854 +                  intersection (acc, set)
  1.2855 +                else
  1.2856 +                  acc) (i_sets ~~ resultsets) i_univ
  1.2857 +          | lfp _ =
  1.2858 +              raise REFUTE ("lfp_interpreter",
  1.2859 +                "lfp: interpretation for function is not a node")
  1.2860 +      in
  1.2861 +        SOME (Node (map lfp i_funs), model, args)
  1.2862 +      end
  1.2863 +  | _ => NONE;
  1.2864 +
  1.2865 +(* only an optimization: 'gfp' could in principle be interpreted with  *)
  1.2866 +(* interpreters available already (using its definition), but the code *)
  1.2867 +(* below is more efficient                                             *)
  1.2868 +
  1.2869 +fun gfp_interpreter ctxt model args t =
  1.2870 +  case t of
  1.2871 +    Const (@{const_name gfp}, Type ("fun", [Type ("fun",
  1.2872 +      [Type (@{type_name set}, [T]),
  1.2873 +       Type (@{type_name set}, [_])]),
  1.2874 +       Type (@{type_name set}, [_])])) =>
  1.2875 +      let
  1.2876 +        val size_elem = size_of_type ctxt model T
  1.2877 +        (* the universe (i.e. the set that contains every element) *)
  1.2878 +        val i_univ = Node (replicate size_elem TT)
  1.2879 +        (* all sets with elements from type 'T' *)
  1.2880 +        val i_sets = make_constants ctxt model (HOLogic.mk_setT T)
  1.2881 +        (* all functions that map sets to sets *)
  1.2882 +        val i_funs = make_constants ctxt model (Type ("fun",
  1.2883 +          [HOLogic.mk_setT T, HOLogic.mk_setT T]))
  1.2884 +        (* "gfp(f) == Union({u. u <= f(u)})" *)
  1.2885 +        (* interpretation * interpretation -> bool *)
  1.2886 +        fun is_subset (Node subs, Node sups) =
  1.2887 +              forall (fn (sub, sup) => (sub = FF) orelse (sup = TT))
  1.2888 +                (subs ~~ sups)
  1.2889 +          | is_subset (_, _) =
  1.2890 +              raise REFUTE ("gfp_interpreter",
  1.2891 +                "is_subset: interpretation for set is not a node")
  1.2892 +        (* interpretation * interpretation -> interpretation *)
  1.2893 +        fun union (Node xs, Node ys) =
  1.2894 +              Node (map (fn (x,y) => if x=TT orelse y=TT then TT else FF)
  1.2895 +                   (xs ~~ ys))
  1.2896 +          | union (_, _) =
  1.2897 +              raise REFUTE ("gfp_interpreter",
  1.2898 +                "union: interpretation for set is not a node")
  1.2899 +        (* interpretation -> interpretaion *)
  1.2900 +        fun gfp (Node resultsets) =
  1.2901 +              fold (fn (set, resultset) => fn acc =>
  1.2902 +                if is_subset (set, resultset) then
  1.2903 +                  union (acc, set)
  1.2904 +                else
  1.2905 +                  acc) (i_sets ~~ resultsets) i_univ
  1.2906 +          | gfp _ =
  1.2907 +              raise REFUTE ("gfp_interpreter",
  1.2908 +                "gfp: interpretation for function is not a node")
  1.2909 +      in
  1.2910 +        SOME (Node (map gfp i_funs), model, args)
  1.2911 +      end
  1.2912 +  | _ => NONE;
  1.2913 +
  1.2914 +(* only an optimization: 'fst' could in principle be interpreted with  *)
  1.2915 +(* interpreters available already (using its definition), but the code *)
  1.2916 +(* below is more efficient                                             *)
  1.2917 +
  1.2918 +fun Product_Type_fst_interpreter ctxt model args t =
  1.2919 +  case t of
  1.2920 +    Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
  1.2921 +      let
  1.2922 +        val constants_T = make_constants ctxt model T
  1.2923 +        val size_U = size_of_type ctxt model U
  1.2924 +      in
  1.2925 +        SOME (Node (maps (replicate size_U) constants_T), model, args)
  1.2926 +      end
  1.2927 +  | _ => NONE;
  1.2928 +
  1.2929 +(* only an optimization: 'snd' could in principle be interpreted with  *)
  1.2930 +(* interpreters available already (using its definition), but the code *)
  1.2931 +(* below is more efficient                                             *)
  1.2932 +
  1.2933 +fun Product_Type_snd_interpreter ctxt model args t =
  1.2934 +  case t of
  1.2935 +    Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
  1.2936 +      let
  1.2937 +        val size_T = size_of_type ctxt model T
  1.2938 +        val constants_U = make_constants ctxt model U
  1.2939 +      in
  1.2940 +        SOME (Node (flat (replicate size_T constants_U)), model, args)
  1.2941 +      end
  1.2942 +  | _ => NONE;
  1.2943 +
  1.2944 +
  1.2945 +(* ------------------------------------------------------------------------- *)
  1.2946 +(* PRINTERS                                                                  *)
  1.2947 +(* ------------------------------------------------------------------------- *)
  1.2948 +
  1.2949 +fun stlc_printer ctxt model T intr assignment =
  1.2950 +  let
  1.2951 +    (* string -> string *)
  1.2952 +    val strip_leading_quote = perhaps (try (unprefix "'"))
  1.2953 +    (* Term.typ -> string *)
  1.2954 +    fun string_of_typ (Type (s, _)) = s
  1.2955 +      | string_of_typ (TFree (x, _)) = strip_leading_quote x
  1.2956 +      | string_of_typ (TVar ((x,i), _)) =
  1.2957 +          strip_leading_quote x ^ string_of_int i
  1.2958 +    (* interpretation -> int *)
  1.2959 +    fun index_from_interpretation (Leaf xs) =
  1.2960 +          find_index (Prop_Logic.eval assignment) xs
  1.2961 +      | index_from_interpretation _ =
  1.2962 +          raise REFUTE ("stlc_printer",
  1.2963 +            "interpretation for ground type is not a leaf")
  1.2964 +  in
  1.2965 +    case T of
  1.2966 +      Type ("fun", [T1, T2]) =>
  1.2967 +        let
  1.2968 +          (* create all constants of type 'T1' *)
  1.2969 +          val constants = make_constants ctxt model T1
  1.2970 +          (* interpretation list *)
  1.2971 +          val results =
  1.2972 +            (case intr of
  1.2973 +              Node xs => xs
  1.2974 +            | _ => raise REFUTE ("stlc_printer",
  1.2975 +              "interpretation for function type is a leaf"))
  1.2976 +          (* Term.term list *)
  1.2977 +          val pairs = map (fn (arg, result) =>
  1.2978 +            HOLogic.mk_prod
  1.2979 +              (print ctxt model T1 arg assignment,
  1.2980 +               print ctxt model T2 result assignment))
  1.2981 +            (constants ~~ results)
  1.2982 +          (* Term.typ *)
  1.2983 +          val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
  1.2984 +          val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
  1.2985 +          (* Term.term *)
  1.2986 +          val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT)
  1.2987 +          val HOLogic_insert    =
  1.2988 +            Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
  1.2989 +        in
  1.2990 +          SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set)
  1.2991 +        end
  1.2992 +    | Type ("prop", []) =>
  1.2993 +        (case index_from_interpretation intr of
  1.2994 +          ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
  1.2995 +        | 0  => SOME (HOLogic.mk_Trueprop @{term True})
  1.2996 +        | 1  => SOME (HOLogic.mk_Trueprop @{term False})
  1.2997 +        | _  => raise REFUTE ("stlc_interpreter",
  1.2998 +          "illegal interpretation for a propositional value"))
  1.2999 +    | Type _  =>
  1.3000 +        if index_from_interpretation intr = (~1) then
  1.3001 +          SOME (Const (@{const_name undefined}, T))
  1.3002 +        else
  1.3003 +          SOME (Const (string_of_typ T ^
  1.3004 +            string_of_int (index_from_interpretation intr), T))
  1.3005 +    | TFree _ =>
  1.3006 +        if index_from_interpretation intr = (~1) then
  1.3007 +          SOME (Const (@{const_name undefined}, T))
  1.3008 +        else
  1.3009 +          SOME (Const (string_of_typ T ^
  1.3010 +            string_of_int (index_from_interpretation intr), T))
  1.3011 +    | TVar _  =>
  1.3012 +        if index_from_interpretation intr = (~1) then
  1.3013 +          SOME (Const (@{const_name undefined}, T))
  1.3014 +        else
  1.3015 +          SOME (Const (string_of_typ T ^
  1.3016 +            string_of_int (index_from_interpretation intr), T))
  1.3017 +  end;
  1.3018 +
  1.3019 +fun set_printer ctxt model T intr assignment =
  1.3020 +  (case T of
  1.3021 +    Type (@{type_name set}, [T1]) =>
  1.3022 +    let
  1.3023 +      (* create all constants of type 'T1' *)
  1.3024 +      val constants = make_constants ctxt model T1
  1.3025 +      (* interpretation list *)
  1.3026 +      val results = (case intr of
  1.3027 +          Node xs => xs
  1.3028 +        | _       => raise REFUTE ("set_printer",
  1.3029 +          "interpretation for set type is a leaf"))
  1.3030 +      (* Term.term list *)
  1.3031 +      val elements = List.mapPartial (fn (arg, result) =>
  1.3032 +        case result of
  1.3033 +          Leaf [fmTrue, (* fmFalse *) _] =>
  1.3034 +          if Prop_Logic.eval assignment fmTrue then
  1.3035 +            SOME (print ctxt model T1 arg assignment)
  1.3036 +          else (* if Prop_Logic.eval assignment fmFalse then *)
  1.3037 +            NONE
  1.3038 +        | _ =>
  1.3039 +          raise REFUTE ("set_printer",
  1.3040 +            "illegal interpretation for a Boolean value"))
  1.3041 +        (constants ~~ results)
  1.3042 +      (* Term.typ *)
  1.3043 +      val HOLogic_setT1     = HOLogic.mk_setT T1
  1.3044 +      (* Term.term *)
  1.3045 +      val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT1)
  1.3046 +      val HOLogic_insert    =
  1.3047 +        Const (@{const_name insert}, T1 --> HOLogic_setT1 --> HOLogic_setT1)
  1.3048 +    in
  1.3049 +      SOME (Library.foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc)
  1.3050 +        (HOLogic_empty_set, elements))
  1.3051 +    end
  1.3052 +  | _ =>
  1.3053 +    NONE);
  1.3054 +
  1.3055 +fun IDT_printer ctxt model T intr assignment =
  1.3056 +  let
  1.3057 +    val thy = Proof_Context.theory_of ctxt
  1.3058 +  in
  1.3059 +    (case T of
  1.3060 +      Type (s, Ts) =>
  1.3061 +        (case Datatype.get_info thy s of
  1.3062 +          SOME info =>  (* inductive datatype *)
  1.3063 +            let
  1.3064 +              val (typs, _)           = model
  1.3065 +              val index               = #index info
  1.3066 +              val descr               = #descr info
  1.3067 +              val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
  1.3068 +              val typ_assoc           = dtyps ~~ Ts
  1.3069 +              (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
  1.3070 +              val _ =
  1.3071 +                if Library.exists (fn d =>
  1.3072 +                  case d of Datatype.DtTFree _ => false | _ => true) dtyps
  1.3073 +                then
  1.3074 +                  raise REFUTE ("IDT_printer", "datatype argument (for type " ^
  1.3075 +                    Syntax.string_of_typ ctxt (Type (s, Ts)) ^ ") is not a variable")
  1.3076 +                else ()
  1.3077 +              (* the index of the element in the datatype *)
  1.3078 +              val element =
  1.3079 +                (case intr of
  1.3080 +                  Leaf xs => find_index (Prop_Logic.eval assignment) xs
  1.3081 +                | Node _  => raise REFUTE ("IDT_printer",
  1.3082 +                  "interpretation is not a leaf"))
  1.3083 +            in
  1.3084 +              if element < 0 then
  1.3085 +                SOME (Const (@{const_name undefined}, Type (s, Ts)))
  1.3086 +              else
  1.3087 +                let
  1.3088 +                  (* takes a datatype constructor, and if for some arguments this  *)
  1.3089 +                  (* constructor generates the datatype's element that is given by *)
  1.3090 +                  (* 'element', returns the constructor (as a term) as well as the *)
  1.3091 +                  (* indices of the arguments                                      *)
  1.3092 +                  fun get_constr_args (cname, cargs) =
  1.3093 +                    let
  1.3094 +                      val cTerm      = Const (cname,
  1.3095 +                        map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts))
  1.3096 +                      val (iC, _, _) = interpret ctxt (typs, []) {maxvars=0,
  1.3097 +                        def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
  1.3098 +                      (* interpretation -> int list option *)
  1.3099 +                      fun get_args (Leaf xs) =
  1.3100 +                            if find_index (fn x => x = True) xs = element then
  1.3101 +                              SOME []
  1.3102 +                            else
  1.3103 +                              NONE
  1.3104 +                        | get_args (Node xs) =
  1.3105 +                            let
  1.3106 +                              (* interpretation * int -> int list option *)
  1.3107 +                              fun search ([], _) =
  1.3108 +                                NONE
  1.3109 +                                | search (x::xs, n) =
  1.3110 +                                (case get_args x of
  1.3111 +                                  SOME result => SOME (n::result)
  1.3112 +                                | NONE        => search (xs, n+1))
  1.3113 +                            in
  1.3114 +                              search (xs, 0)
  1.3115 +                            end
  1.3116 +                    in
  1.3117 +                      Option.map (fn args => (cTerm, cargs, args)) (get_args iC)
  1.3118 +                    end
  1.3119 +                  val (cTerm, cargs, args) =
  1.3120 +                    (* we could speed things up by computing the correct          *)
  1.3121 +                    (* constructor directly (rather than testing all              *)
  1.3122 +                    (* constructors), based on the order in which constructors    *)
  1.3123 +                    (* generate elements of datatypes; the current implementation *)
  1.3124 +                    (* of 'IDT_printer' however is independent of the internals   *)
  1.3125 +                    (* of 'IDT_constructor_interpreter'                           *)
  1.3126 +                    (case get_first get_constr_args constrs of
  1.3127 +                      SOME x => x
  1.3128 +                    | NONE   => raise REFUTE ("IDT_printer",
  1.3129 +                      "no matching constructor found for element " ^
  1.3130 +                      string_of_int element))
  1.3131 +                  val argsTerms = map (fn (d, n) =>
  1.3132 +                    let
  1.3133 +                      val dT = typ_of_dtyp descr typ_assoc d
  1.3134 +                      (* we only need the n-th element of this list, so there   *)
  1.3135 +                      (* might be a more efficient implementation that does not *)
  1.3136 +                      (* generate all constants                                 *)
  1.3137 +                      val consts = make_constants ctxt (typs, []) dT
  1.3138 +                    in
  1.3139 +                      print ctxt (typs, []) dT (nth consts n) assignment
  1.3140 +                    end) (cargs ~~ args)
  1.3141 +                in
  1.3142 +                  SOME (list_comb (cTerm, argsTerms))
  1.3143 +                end
  1.3144 +            end
  1.3145 +        | NONE =>  (* not an inductive datatype *)
  1.3146 +            NONE)
  1.3147 +    | _ =>  (* a (free or schematic) type variable *)
  1.3148 +        NONE)
  1.3149 +  end;
  1.3150 +
  1.3151 +
  1.3152 +(* ------------------------------------------------------------------------- *)
  1.3153 +(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
  1.3154 +(* structure                                                                 *)
  1.3155 +(* ------------------------------------------------------------------------- *)
  1.3156 +
  1.3157 +(* ------------------------------------------------------------------------- *)
  1.3158 +(* Note: the interpreters and printers are used in reverse order; however,   *)
  1.3159 +(*       an interpreter that can handle non-atomic terms ends up being       *)
  1.3160 +(*       applied before the 'stlc_interpreter' breaks the term apart into    *)
  1.3161 +(*       subterms that are then passed to other interpreters!                *)
  1.3162 +(* ------------------------------------------------------------------------- *)
  1.3163 +
  1.3164 +val setup =
  1.3165 +   add_interpreter "stlc"    stlc_interpreter #>
  1.3166 +   add_interpreter "Pure"    Pure_interpreter #>
  1.3167 +   add_interpreter "HOLogic" HOLogic_interpreter #>
  1.3168 +   add_interpreter "set"     set_interpreter #>
  1.3169 +   add_interpreter "IDT"             IDT_interpreter #>
  1.3170 +   add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
  1.3171 +   add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>
  1.3172 +   add_interpreter "Finite_Set.card"    Finite_Set_card_interpreter #>
  1.3173 +   add_interpreter "Finite_Set.finite"  Finite_Set_finite_interpreter #>
  1.3174 +   add_interpreter "Nat_Orderings.less" Nat_less_interpreter #>
  1.3175 +   add_interpreter "Nat_HOL.plus"       Nat_plus_interpreter #>
  1.3176 +   add_interpreter "Nat_HOL.minus"      Nat_minus_interpreter #>
  1.3177 +   add_interpreter "Nat_HOL.times"      Nat_times_interpreter #>
  1.3178 +   add_interpreter "List.append" List_append_interpreter #>
  1.3179 +(* UNSOUND
  1.3180 +   add_interpreter "lfp" lfp_interpreter #>
  1.3181 +   add_interpreter "gfp" gfp_interpreter #>
  1.3182 +*)
  1.3183 +   add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #>
  1.3184 +   add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #>
  1.3185 +   add_printer "stlc" stlc_printer #>
  1.3186 +   add_printer "set" set_printer #>
  1.3187 +   add_printer "IDT"  IDT_printer;
  1.3188 +
  1.3189 +
  1.3190 +
  1.3191 +(** outer syntax commands 'refute' and 'refute_params' **)
  1.3192 +
  1.3193 +(* argument parsing *)
  1.3194 +
  1.3195 +(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
  1.3196 +
  1.3197 +val scan_parm = Parse.name -- (Scan.optional (@{keyword "="} |-- Parse.name) "true")
  1.3198 +val scan_parms = Scan.optional (@{keyword "["} |-- Parse.list scan_parm --| @{keyword "]"}) [];
  1.3199 +
  1.3200 +
  1.3201 +(* 'refute' command *)
  1.3202 +
  1.3203 +val _ =
  1.3204 +  Outer_Syntax.improper_command @{command_spec "refute"}
  1.3205 +    "try to find a model that refutes a given subgoal"
  1.3206 +    (scan_parms -- Scan.optional Parse.nat 1 >>
  1.3207 +      (fn (parms, i) =>
  1.3208 +        Toplevel.keep (fn state =>
  1.3209 +          let
  1.3210 +            val ctxt = Toplevel.context_of state;
  1.3211 +            val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
  1.3212 +          in refute_goal ctxt parms st i; () end)));
  1.3213 +
  1.3214 +
  1.3215 +(* 'refute_params' command *)
  1.3216 +
  1.3217 +val _ =
  1.3218 +  Outer_Syntax.command @{command_spec "refute_params"}
  1.3219 +    "show/store default parameters for the 'refute' command"
  1.3220 +    (scan_parms >> (fn parms =>
  1.3221 +      Toplevel.theory (fn thy =>
  1.3222 +        let
  1.3223 +          val thy' = fold set_default_param parms thy;
  1.3224 +          val output =
  1.3225 +            (case get_default_params (Proof_Context.init_global thy') of
  1.3226 +              [] => "none"
  1.3227 +            | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
  1.3228 +          val _ = writeln ("Default parameters for 'refute':\n" ^ output);
  1.3229 +        in thy' end)));
  1.3230 +
  1.3231 +end;
  1.3232 +