(*  Title:      HOL/Tools/refute.ML

     ID:         $Id$

     Author:     Tjark Weber

     Copyright   2003-2007

 Finite model generation for HOL formulas, using a SAT solver.

 *)

 (* ------------------------------------------------------------------------- *)

 (* Declares the 'REFUTE' signature as well as a structure 'Refute'.          *)

 (* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'.  *)

 (* ------------------------------------------------------------------------- *)

 signature REFUTE =

 sig

   exception REFUTE of string * string

 (* ------------------------------------------------------------------------- *)

 (* Model/interpretation related code (translation HOL -> propositional logic *)

 (* ------------------------------------------------------------------------- *)

   type params

   type interpretation

   type model

   type arguments

   exception MAXVARS_EXCEEDED

   val add_interpreter : string -> (theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option) -> theory -> theory

   val add_printer     : string -> (theory -> model -> Term.term ->

     interpretation -> (int -> bool) -> Term.term option) -> theory -> theory

   val interpret : theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments)

   val print       : theory -> model -> Term.term -> interpretation ->

     (int -> bool) -> Term.term

   val print_model : theory -> model -> (int -> bool) -> string

 (* ------------------------------------------------------------------------- *)

 (* Interface                                                                 *)

 (* ------------------------------------------------------------------------- *)

   val set_default_param  : (string * string) -> theory -> theory

   val get_default_param  : theory -> string -> string option

   val get_default_params : theory -> (string * string) list

   val actual_params      : theory -> (string * string) list -> params

   val find_model : theory -> params -> Term.term -> bool -> unit

   (* tries to find a model for a formula: *)

   val satisfy_term   : theory -> (string * string) list -> Term.term -> unit

   (* tries to find a model that refutes a formula: *)

   val refute_term    : theory -> (string * string) list -> Term.term -> unit

   val refute_subgoal :

     theory -> (string * string) list -> Thm.thm -> int -> unit

   val setup : theory -> theory

 end;  (* signature REFUTE *)

 structure Refute : REFUTE =

 struct

   open PropLogic;

   (* We use 'REFUTE' only for internal error conditions that should    *)

   (* never occur in the first place (i.e. errors caused by bugs in our *)

   (* code).  Otherwise (e.g. to indicate invalid input data) we use    *)

   (* 'error'.                                                          *)

   exception REFUTE of string * string;  (* ("in function", "cause") *)

   (* should be raised by an interpreter when more variables would be *)

   (* required than allowed by 'maxvars'                              *)

   exception MAXVARS_EXCEEDED;

 (* ------------------------------------------------------------------------- *)

 (* TREES                                                                     *)

 (* ------------------------------------------------------------------------- *)

 (* ------------------------------------------------------------------------- *)

 (* tree: implements an arbitrarily (but finitely) branching tree as a list   *)

 (*       of (lists of ...) elements                                          *)

 (* ------------------------------------------------------------------------- *)

   datatype 'a tree =

       Leaf of 'a

     | Node of ('a tree) list;

   (* ('a -> 'b) -> 'a tree -> 'b tree *)

   fun tree_map f tr =

     case tr of

       Leaf x  => Leaf (f x)

     | Node xs => Node (map (tree_map f) xs);

   (* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)

   fun tree_foldl f =

   let

     fun itl (e, Leaf x)  = f(e,x)

       | itl (e, Node xs) = Library.foldl (tree_foldl f) (e,xs)

   in

     itl

   end;

   (* 'a tree * 'b tree -> ('a * 'b) tree *)

   fun tree_pair (t1, t2) =

     case t1 of

       Leaf x =>

       (case t2 of

           Leaf y => Leaf (x,y)

         | Node _ => raise REFUTE ("tree_pair",

             "trees are of different height (second tree is higher)"))

     | Node xs =>

       (case t2 of

           (* '~~' will raise an exception if the number of branches in   *)

           (* both trees is different at the current node                 *)

           Node ys => Node (map tree_pair (xs ~~ ys))

         | Leaf _  => raise REFUTE ("tree_pair",

             "trees are of different height (first tree is higher)"));

 (* ------------------------------------------------------------------------- *)

 (* params: parameters that control the translation into a propositional      *)

 (*         formula/model generation                                          *)

 (*                                                                           *)

 (* The following parameters are supported (and required (!), except for      *)

 (* "sizes"):                                                                 *)

 (*                                                                           *)

 (* Name          Type    Description                                         *)

 (*                                                                           *)

 (* "sizes"       (string * int) list                                         *)

 (*                       Size of ground types (e.g. 'a=2), or depth of IDTs. *)

 (* "minsize"     int     If >0, minimal size of each ground type/IDT depth.  *)

 (* "maxsize"     int     If >0, maximal size of each ground type/IDT depth.  *)

 (* "maxvars"     int     If >0, use at most 'maxvars' Boolean variables      *)

 (*                       when transforming the term into a propositional     *)

 (*                       formula.                                            *)

 (* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)

 (* "satsolver"   string  SAT solver to be used.                              *)

 (* ------------------------------------------------------------------------- *)

   type params =

     {

       sizes    : (string * int) list,

       minsize  : int,

       maxsize  : int,

       maxvars  : int,

       maxtime  : int,

       satsolver: string

     };

 (* ------------------------------------------------------------------------- *)

 (* interpretation: a term's interpretation is given by a variable of type    *)

 (*                 'interpretation'                                          *)

 (* ------------------------------------------------------------------------- *)

   type interpretation =

     prop_formula list tree;

 (* ------------------------------------------------------------------------- *)

 (* model: a model specifies the size of types and the interpretation of      *)

 (*        terms                                                              *)

 (* ------------------------------------------------------------------------- *)

   type model =

     (Term.typ * int) list * (Term.term * interpretation) list;

 (* ------------------------------------------------------------------------- *)

 (* arguments: additional arguments required during interpretation of terms   *)

 (* ------------------------------------------------------------------------- *)

   type arguments =

     {

       (* just passed unchanged from 'params': *)

       maxvars   : int,

       (* whether to use 'make_equality' or 'make_def_equality': *)

       def_eq    : bool,

       (* the following may change during the translation: *)

       next_idx  : int,

       bounds    : interpretation list,

       wellformed: prop_formula

     };

   structure RefuteData = TheoryDataFun

   (

     type T =

       {interpreters: (string * (theory -> model -> arguments -> Term.term ->

         (interpretation * model * arguments) option)) list,

        printers: (string * (theory -> model -> Term.term -> interpretation ->

         (int -> bool) -> Term.term option)) list,

        parameters: string Symtab.table};

     val empty = {interpreters = [], printers = [], parameters = Symtab.empty};

     val copy = I;

     val extend = I;

     fun merge _

       ({interpreters = in1, printers = pr1, parameters = pa1},

        {interpreters = in2, printers = pr2, parameters = pa2}) =

       {interpreters = AList.merge (op =) (K true) (in1, in2),

        printers = AList.merge (op =) (K true) (pr1, pr2),

        parameters = Symtab.merge (op=) (pa1, pa2)};

   );

 (* ------------------------------------------------------------------------- *)

 (* interpret: interprets the term 't' using a suitable interpreter; returns  *)

 (*            the interpretation and a (possibly extended) model that keeps  *)

 (*            track of the interpretation of subterms                        *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) *)

   fun interpret thy model args t =

     case get_first (fn (_, f) => f thy model args t)

       (#interpreters (RefuteData.get thy)) of

       NONE   => raise REFUTE ("interpret",

         "no interpreter for term " ^ quote (Sign.string_of_term thy t))

     | SOME x => x;

 (* ------------------------------------------------------------------------- *)

 (* print: converts the constant denoted by the term 't' into a term using a  *)

 (*        suitable printer                                                   *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> model -> Term.term -> interpretation -> (int -> bool) ->

     Term.term *)

   fun print thy model t intr assignment =

     case get_first (fn (_, f) => f thy model t intr assignment)

       (#printers (RefuteData.get thy)) of

       NONE   => raise REFUTE ("print",

         "no printer for term " ^ quote (Sign.string_of_term thy t))

     | SOME x => x;

 (* ------------------------------------------------------------------------- *)

 (* print_model: turns the model into a string, using a fixed interpretation  *)

 (*              (given by an assignment for Boolean variables) and suitable  *)

 (*              printers                                                     *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> model -> (int -> bool) -> string *)

   fun print_model thy model assignment =

   let

     val (typs, terms) = model

     val typs_msg =

       if null typs then

         "empty universe (no type variables in term)\n"

       else

         "Size of types: " ^ commas (map (fn (T, i) =>

           Sign.string_of_typ thy T ^ ": " ^ string_of_int i) typs) ^ "\n"

     val show_consts_msg =

       if not (!show_consts) andalso Library.exists (is_Const o fst) terms then

         "set \"show_consts\" to show the interpretation of constants\n"

       else

         ""

     val terms_msg =

       if null terms then

         "empty interpretation (no free variables in term)\n"

       else

         space_implode "\n" (List.mapPartial (fn (t, intr) =>

           (* print constants only if 'show_consts' is true *)

           if (!show_consts) orelse not (is_Const t) then

             SOME (Sign.string_of_term thy t ^ ": " ^

               Sign.string_of_term thy (print thy model t intr assignment))

           else

             NONE) terms) ^ "\n"

   in

     typs_msg ^ show_consts_msg ^ terms_msg

   end;

 (* ------------------------------------------------------------------------- *)

 (* PARAMETER MANAGEMENT                                                      *)

 (* ------------------------------------------------------------------------- *)

   (* string -> (theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option) -> theory -> theory *)

   fun add_interpreter name f thy =

   let

     val {interpreters, printers, parameters} = RefuteData.get thy

   in

     case AList.lookup (op =) interpreters name of

       NONE   => RefuteData.put {interpreters = (name, f) :: interpreters,

       printers = printers, parameters = parameters} thy

     | SOME _ => error ("Interpreter " ^ name ^ " already declared")

   end;

   (* string -> (theory -> model -> Term.term -> interpretation ->

     (int -> bool) -> Term.term option) -> theory -> theory *)

   fun add_printer name f thy =

   let

     val {interpreters, printers, parameters} = RefuteData.get thy

   in

     case AList.lookup (op =) printers name of

       NONE   => RefuteData.put {interpreters = interpreters,

       printers = (name, f) :: printers, parameters = parameters} thy

     | SOME _ => error ("Printer " ^ name ^ " already declared")

   end;

 (* ------------------------------------------------------------------------- *)

 (* set_default_param: stores the '(name, value)' pair in RefuteData's        *)

 (*                    parameter table                                        *)

 (* ------------------------------------------------------------------------- *)

   (* (string * string) -> theory -> theory *)

   fun set_default_param (name, value) thy =

   let

     val {interpreters, printers, parameters} = RefuteData.get thy

   in

     RefuteData.put (case Symtab.lookup parameters name of

       NONE   =>

       {interpreters = interpreters, printers = printers,

         parameters = Symtab.extend (parameters, [(name, value)])}

     | SOME _ =>

       {interpreters = interpreters, printers = printers,

         parameters = Symtab.update (name, value) parameters}) thy

   end;

 (* ------------------------------------------------------------------------- *)

 (* get_default_param: retrieves the value associated with 'name' from        *)

 (*                    RefuteData's parameter table                           *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> string -> string option *)

   val get_default_param = Symtab.lookup o #parameters o RefuteData.get;

 (* ------------------------------------------------------------------------- *)

 (* get_default_params: returns a list of all '(name, value)' pairs that are  *)

 (*                     stored in RefuteData's parameter table                *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> (string * string) list *)

   val get_default_params = Symtab.dest o #parameters o RefuteData.get;

 (* ------------------------------------------------------------------------- *)

 (* actual_params: takes a (possibly empty) list 'params' of parameters that  *)

 (*      override the default parameters currently specified in 'thy', and    *)

 (*      returns a record that can be passed to 'find_model'.                 *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> (string * string) list -> params *)

   fun actual_params thy override =

   let

     (* (string * string) list * string -> int *)

     fun read_int (parms, name) =

       case AList.lookup (op =) parms name of

         SOME s => (case Int.fromString s of

           SOME i => i

         | NONE   => error ("parameter " ^ quote name ^

           " (value is " ^ quote s ^ ") must be an integer value"))

       | NONE   => error ("parameter " ^ quote name ^

           " must be assigned a value")

     (* (string * string) list * string -> string *)

     fun read_string (parms, name) =

       case AList.lookup (op =) parms name of

         SOME s => s

       | NONE   => error ("parameter " ^ quote name ^

         " must be assigned a value")

     (* 'override' first, defaults last: *)

     (* (string * string) list *)

     val allparams = override @ (get_default_params thy)

     (* int *)

     val minsize   = read_int (allparams, "minsize")

     val maxsize   = read_int (allparams, "maxsize")

     val maxvars   = read_int (allparams, "maxvars")

     val maxtime   = read_int (allparams, "maxtime")

     (* string *)

     val satsolver = read_string (allparams, "satsolver")

     (* all remaining parameters of the form "string=int" are collected in *)

     (* 'sizes'                                                            *)

     (* TODO: it is currently not possible to specify a size for a type    *)

     (*       whose name is one of the other parameters (e.g. 'maxvars')   *)

     (* (string * int) list *)

     val sizes     = List.mapPartial

       (fn (name, value) => Option.map (pair name) (Int.fromString value))

       (List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"

         andalso name<>"maxvars" andalso name<>"maxtime"

         andalso name<>"satsolver") allparams)

   in

     {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars,

       maxtime=maxtime, satsolver=satsolver}

   end;

 (* ------------------------------------------------------------------------- *)

 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)

 (* ------------------------------------------------------------------------- *)

   (* (''a * 'b) list -> ''a -> 'b *)

   fun lookup xs key =

     Option.valOf (AList.lookup (op =) xs key);

 (* ------------------------------------------------------------------------- *)

 (* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type        *)

 (*              ('Term.typ'), given type parameters for the data type's type *)

 (*              arguments                                                    *)

 (* ------------------------------------------------------------------------- *)

   (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list ->

     DatatypeAux.dtyp -> Term.typ *)

   fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =

     (* replace a 'DtTFree' variable by the associated type *)

     lookup typ_assoc (DatatypeAux.DtTFree a)

     | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =

     Type (s, map (typ_of_dtyp descr typ_assoc) ds)

     | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =

     let

       val (s, ds, _) = lookup descr i

     in

       Type (s, map (typ_of_dtyp descr typ_assoc) ds)

     end;

 (* ------------------------------------------------------------------------- *)

 (* close_form: universal closure over schematic variables in 't'             *)

 (* ------------------------------------------------------------------------- *)

   (* Term.term -> Term.term *)

   fun close_form t =

   let

     (* (Term.indexname * Term.typ) list *)

     val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))

   in

     Library.foldl (fn (t', ((x, i), T)) =>

       (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t')))

       (t, vars)

   end;

 (* ------------------------------------------------------------------------- *)

 (* monomorphic_term: applies a type substitution 'typeSubs' for all type     *)

 (*                   variables in a term 't'                                 *)

 (* ------------------------------------------------------------------------- *)

   (* Type.tyenv -> Term.term -> Term.term *)

   fun monomorphic_term typeSubs t =

     map_types (map_type_tvar

       (fn v =>

         case Type.lookup (typeSubs, v) of

           NONE =>

           (* schematic type variable not instantiated *)

           raise REFUTE ("monomorphic_term",

             "no substitution for type variable " ^ fst (fst v) ^

             " in term " ^ Display.raw_string_of_term t)

         | SOME typ =>

           typ)) t;

 (* ------------------------------------------------------------------------- *)

 (* specialize_type: given a constant 's' of type 'T', which is a subterm of  *)

 (*                  't', where 't' has a (possibly) more general type, the   *)

 (*                  schematic type variables in 't' are instantiated to      *)

 (*                  match the type 'T' (may raise Type.TYPE_MATCH)           *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> (string * Term.typ) -> Term.term -> Term.term *)

   fun specialize_type thy (s, T) t =

   let

     fun find_typeSubs (Const (s', T')) =

       if s=s' then

         SOME (Sign.typ_match thy (T', T) Vartab.empty)

           handle Type.TYPE_MATCH => NONE

       else

         NONE

       | find_typeSubs (Free _)           = NONE

       | find_typeSubs (Var _)            = NONE

       | find_typeSubs (Bound _)          = NONE

       | find_typeSubs (Abs (_, _, body)) = find_typeSubs body

       | find_typeSubs (t1 $ t2)          =

       (case find_typeSubs t1 of SOME x => SOME x

                               | NONE   => find_typeSubs t2)

   in

     case find_typeSubs t of

       SOME typeSubs =>

       monomorphic_term typeSubs t

     | NONE =>

       (* no match found - perhaps due to sort constraints *)

       raise Type.TYPE_MATCH

   end;

 (* ------------------------------------------------------------------------- *)

 (* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that   *)

 (*                    denotes membership to an axiomatic type class          *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> string * Term.typ -> bool *)

   fun is_const_of_class thy (s, T) =

   let

     val class_const_names = map Logic.const_of_class (Sign.all_classes thy)

   in

     (* I'm not quite sure if checking the name 's' is sufficient, *)

     (* or if we should also check the type 'T'.                   *)

     s mem_string class_const_names

   end;

 (* ------------------------------------------------------------------------- *)

 (* is_IDT_constructor: returns 'true' iff 'Const (s, T)' is the constructor  *)

 (*                     of an inductive datatype in 'thy'                     *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> string * Term.typ -> bool *)

   fun is_IDT_constructor thy (s, T) =

     (case body_type T of

       Type (s', _) =>

       (case DatatypePackage.get_datatype_constrs thy s' of

         SOME constrs =>

         List.exists (fn (cname, cty) =>

           cname = s andalso Sign.typ_instance thy (T, cty)) constrs

       | NONE =>

         false)

     | _  =>

       false);

 (* ------------------------------------------------------------------------- *)

 (* is_IDT_recursor: returns 'true' iff 'Const (s, T)' is the recursion       *)

 (*                  operator of an inductive datatype in 'thy'               *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> string * Term.typ -> bool *)

   fun is_IDT_recursor thy (s, T) =

   let

     val rec_names = Symtab.fold (append o #rec_names o snd)

       (DatatypePackage.get_datatypes thy) []

   in

     (* I'm not quite sure if checking the name 's' is sufficient, *)

     (* or if we should also check the type 'T'.                   *)

     s mem_string rec_names

   end;

 (* ------------------------------------------------------------------------- *)

 (* get_def: looks up the definition of a constant, as created by "constdefs" *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> string * Term.typ -> (string * Term.term) option *)

   fun get_def thy (s, T) =

   let

     (* maps  f ?t1 ... ?tn == rhs  to  %t1...tn. rhs *)

     fun norm_rhs eqn =

     let

       fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))

         | lambda v t                      = raise TERM ("lambda", [v, t])

       val (lhs, rhs) = Logic.dest_equals eqn

       val (_, args)  = Term.strip_comb lhs

     in

       fold lambda (rev args) rhs

     end

     (* (string * Term.term) list -> (string * Term.term) option *)

     fun get_def_ax [] = NONE

       | get_def_ax ((axname, ax) :: axioms) =

       (let

         val (lhs, _) = Logic.dest_equals ax  (* equations only *)

         val c        = Term.head_of lhs

         val (s', T') = Term.dest_Const c

       in

         if s=s' then

           let

             val typeSubs = Sign.typ_match thy (T', T) Vartab.empty

             val ax'      = monomorphic_term typeSubs ax

             val rhs      = norm_rhs ax'

           in

             SOME (axname, rhs)

           end

         else

           get_def_ax axioms

       end handle ERROR _         => get_def_ax axioms

                | TERM _          => get_def_ax axioms

                | Type.TYPE_MATCH => get_def_ax axioms)

   in

     get_def_ax (Theory.all_axioms_of thy)

   end;

 (* ------------------------------------------------------------------------- *)

 (* get_typedef: looks up the definition of a type, as created by "typedef"   *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> (string * Term.typ) -> (string * Term.term) option *)

   fun get_typedef thy T =

   let

     (* (string * Term.term) list -> (string * Term.term) option *)

     fun get_typedef_ax [] = NONE

       | get_typedef_ax ((axname, ax) :: axioms) =

       (let

         (* Term.term -> Term.typ option *)

         fun type_of_type_definition (Const (s', T')) =

           if s'="Typedef.type_definition" then

             SOME T'

           else

             NONE

           | type_of_type_definition (Free _)           = NONE

           | type_of_type_definition (Var _)            = NONE

           | type_of_type_definition (Bound _)          = NONE

           | type_of_type_definition (Abs (_, _, body)) =

           type_of_type_definition body

           | type_of_type_definition (t1 $ t2)          =

           (case type_of_type_definition t1 of

             SOME x => SOME x

           | NONE   => type_of_type_definition t2)

       in

         case type_of_type_definition ax of

           SOME T' =>

           let

             val T''      = (domain_type o domain_type) T'

             val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty

           in

             SOME (axname, monomorphic_term typeSubs ax)

           end

         | NONE =>

           get_typedef_ax axioms

       end handle ERROR _         => get_typedef_ax axioms

                | MATCH           => get_typedef_ax axioms

                | Type.TYPE_MATCH => get_typedef_ax axioms)

   in

     get_typedef_ax (Theory.all_axioms_of thy)

   end;

 (* ------------------------------------------------------------------------- *)

 (* get_classdef: looks up the defining axiom for an axiomatic type class, as *)

 (*               created by the "axclass" command                            *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> string -> (string * Term.term) option *)

   fun get_classdef thy class =

   let

     val axname = class ^ "_class_def"

   in

     Option.map (pair axname)

       (AList.lookup (op =) (Theory.all_axioms_of thy) axname)

   end;

 (* ------------------------------------------------------------------------- *)

 (* unfold_defs: unfolds all defined constants in a term 't', beta-eta        *)

 (*              normalizes the result term; certain constants are not        *)

 (*              unfolded (cf. 'collect_axioms' and the various interpreters  *)

 (*              below): if the interpretation respects a definition anyway,  *)

 (*              that definition does not need to be unfolded                 *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> Term.term -> Term.term *)

   (* Note: we could intertwine unfolding of constants and beta-(eta-)       *)

   (*       normalization; this would save some unfolding for terms where    *)

   (*       constants are eliminated by beta-reduction (e.g. 'K c1 c2').  On *)

   (*       the other hand, this would cause additional work for terms where *)

   (*       constants are duplicated by beta-reduction (e.g. 'S c1 c2 c3').  *)

   fun unfold_defs thy t =

   let

     (* Term.term -> Term.term *)

     fun unfold_loop t =

       case t of

       (* Pure *)

         Const ("all", _)                => t

       | Const ("==", _)                 => t

       | Const ("==>", _)                => t

       | Const ("TYPE", _)               => t  (* axiomatic type classes *)

       (* HOL *)

       | Const ("Trueprop", _)           => t

       | Const ("Not", _)                => t

       | (* redundant, since 'True' is also an IDT constructor *)

         Const ("True", _)               => t

       | (* redundant, since 'False' is also an IDT constructor *)

         Const ("False", _)              => t

       | Const ("arbitrary", _)          => t

       | Const ("The", _)                => t

       | Const ("Hilbert_Choice.Eps", _) => t

       | Const ("All", _)                => t

       | Const ("Ex", _)                 => t

       | Const ("op =", _)               => t

       | Const ("op &", _)               => t

       | Const ("op |", _)               => t

       | Const ("op -->", _)             => t

       (* sets *)

       | Const ("Collect", _)            => t

       | Const ("op :", _)               => t

       (* other optimizations *)

       | Const ("Finite_Set.card", _)    => t

       | Const ("Finite_Set.Finites", _) => t

       | Const ("Finite_Set.finite", _)  => t

       | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),

         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t

       | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),

         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t

       | Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),

         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t

       | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),

         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t

       | Const ("List.append", _)          => t

       | Const ("Lfp.lfp", _)            => t

       | Const ("Gfp.gfp", _)            => t

       | Const ("fst", _)                => t

       | Const ("snd", _)                => t

       (* simply-typed lambda calculus *)

       | Const (s, T) =>

         (if is_IDT_constructor thy (s, T)

           orelse is_IDT_recursor thy (s, T) then

           t  (* do not unfold IDT constructors/recursors *)

         (* unfold the constant if there is a defining equation *)

         else case get_def thy (s, T) of

           SOME (axname, rhs) =>

           (* Note: if the term to be unfolded (i.e. 'Const (s, T)')  *)

           (* occurs on the right-hand side of the equation, i.e. in  *)

           (* 'rhs', we must not use this equation to unfold, because *)

           (* that would loop.  Here would be the right place to      *)

           (* check this.  However, getting this really right seems   *)

           (* difficult because the user may state arbitrary axioms,  *)

           (* which could interact with overloading to create loops.  *)

           ((*Output.immediate_output (" unfolding: " ^ axname);*)unfold_loop rhs)

         | NONE => t)

       | Free _           => t

       | Var _            => t

       | Bound _          => t

       | Abs (s, T, body) => Abs (s, T, unfold_loop body)

       | t1 $ t2          => (unfold_loop t1) $ (unfold_loop t2)

     val result = Envir.beta_eta_contract (unfold_loop t)

   in

     result

   end;

 (* ------------------------------------------------------------------------- *)

 (* collect_axioms: collects (monomorphic, universally quantified, unfolded   *)

 (*                 versions of) all HOL axioms that are relevant w.r.t 't'   *)

 (* ------------------------------------------------------------------------- *)

   (* Note: to make the collection of axioms more easily extensible, this    *)

   (*       function could be based on user-supplied "axiom collectors",     *)

   (*       similar to 'interpret'/interpreters or 'print'/printers          *)

   (* Note: currently we use "inverse" functions to the definitional         *)

   (*       mechanisms provided by Isabelle/HOL, e.g. for "axclass",         *)

   (*       "typedef", "constdefs".  A more general approach could consider  *)

   (*       *every* axiom of the theory and collect it if it has a constant/ *)

   (*       type/typeclass in common with the term 't'.                      *)

   (* theory -> Term.term -> Term.term list *)

   (* Which axioms are "relevant" for a particular term/type goes hand in    *)

   (* hand with the interpretation of that term/type by its interpreter (see *)

   (* way below): if the interpretation respects an axiom anyway, the axiom  *)

   (* does not need to be added as a constraint here.                        *)

   (* To avoid collecting the same axiom multiple times, we use an           *)

   (* accumulator 'axs' which contains all axioms collected so far.          *)

   fun collect_axioms thy t =

   let

     val _ = Output.immediate_output "Adding axioms..."

     (* (string * Term.term) list *)

     val axioms = Theory.all_axioms_of thy

     (* string * Term.term -> Term.term list -> Term.term list *)

     fun collect_this_axiom (axname, ax) axs =

     let

       val ax' = unfold_defs thy ax

     in

       if member (op aconv) axs ax' then

         axs

       else (

         Output.immediate_output (" " ^ axname);

         collect_term_axioms (ax' :: axs, ax')

       )

     end

     (* Term.term list * Term.typ -> Term.term list *)

     and collect_sort_axioms (axs, T) =

     let

       (* string list *)

       val sort = (case T of

           TFree (_, sort) => sort

         | TVar (_, sort)  => sort

         | _               => raise REFUTE ("collect_axioms", "type " ^

           Sign.string_of_typ thy T ^ " is not a variable"))

       (* obtain axioms for all superclasses *)

       val superclasses = sort @ (maps (Sign.super_classes thy) sort)

       (* merely an optimization, because 'collect_this_axiom' disallows *)

       (* duplicate axioms anyway:                                       *)

       val superclasses = distinct (op =) superclasses

       val class_axioms = maps (fn class => map (fn ax =>

         ("<" ^ class ^ ">", Thm.prop_of ax))

         (#axioms (AxClass.get_definition thy class) handle ERROR _ => []))

         superclasses

       (* replace the (at most one) schematic type variable in each axiom *)

       (* by the actual type 'T'                                          *)

       val monomorphic_class_axioms = map (fn (axname, ax) =>

         (case Term.term_tvars ax of

           [] =>

           (axname, ax)

         | [(idx, S)] =>

           (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)

         | _ =>

           raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^

             Sign.string_of_term thy ax ^

             ") contains more than one type variable")))

         class_axioms

     in

       fold collect_this_axiom monomorphic_class_axioms axs

     end

     (* Term.term list * Term.typ -> Term.term list *)

     and collect_type_axioms (axs, T) =

       case T of

       (* simple types *)

         Type ("prop", [])      => axs

       | Type ("fun", [T1, T2]) => collect_type_axioms

         (collect_type_axioms (axs, T1), T2)

       | Type ("set", [T1])     => collect_type_axioms (axs, T1)

       (* axiomatic type classes *)

       | Type ("itself", [T1])  => collect_type_axioms (axs, T1)

       | Type (s, Ts)           =>

         (case DatatypePackage.get_datatype thy s of

           SOME info =>  (* inductive datatype *)

             (* only collect relevant type axioms for the argument types *)

             Library.foldl collect_type_axioms (axs, Ts)

         | NONE =>

           (case get_typedef thy T of

             SOME (axname, ax) =>

             collect_this_axiom (axname, ax) axs

           | NONE =>

             (* unspecified type, perhaps introduced with "typedecl" *)

             (* at least collect relevant type axioms for the argument types *)

             Library.foldl collect_type_axioms (axs, Ts)))

       (* axiomatic type classes *)

       | TFree _                => collect_sort_axioms (axs, T)

       (* axiomatic type classes *)

       | TVar _                 => collect_sort_axioms (axs, T)

     (* Term.term list * Term.term -> Term.term list *)

     and collect_term_axioms (axs, t) =

       case t of

       (* Pure *)

         Const ("all", _)                => axs

       | Const ("==", _)                 => axs

       | Const ("==>", _)                => axs

       (* axiomatic type classes *)

       | Const ("TYPE", T)               => collect_type_axioms (axs, T)

       (* HOL *)

       | Const ("Trueprop", _)           => axs

       | Const ("Not", _)                => axs

       (* redundant, since 'True' is also an IDT constructor *)

       | Const ("True", _)               => axs

       (* redundant, since 'False' is also an IDT constructor *)

       | Const ("False", _)              => axs

       | Const ("arbitrary", T)          => collect_type_axioms (axs, T)

       | Const ("The", T)                =>

         let

           val ax = specialize_type thy ("The", T)

             (lookup axioms "HOL.the_eq_trivial")

         in

           collect_this_axiom ("HOL.the_eq_trivial", ax) axs

         end

       | Const ("Hilbert_Choice.Eps", T) =>

         let

           val ax = specialize_type thy ("Hilbert_Choice.Eps", T)

             (lookup axioms "Hilbert_Choice.someI")

         in

           collect_this_axiom ("Hilbert_Choice.someI", ax) axs

         end

       | Const ("All", T)                => collect_type_axioms (axs, T)

       | Const ("Ex", T)                 => collect_type_axioms (axs, T)

       | Const ("op =", T)               => collect_type_axioms (axs, T)

       | Const ("op &", _)               => axs

       | Const ("op |", _)               => axs

       | Const ("op -->", _)             => axs

       (* sets *)

       | Const ("Collect", T)            => collect_type_axioms (axs, T)

       | Const ("op :", T)               => collect_type_axioms (axs, T)

       (* other optimizations *)

       | Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)

       | Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)

       | Const ("Finite_Set.finite", T)  => collect_type_axioms (axs, T)

       | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),

         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>

           collect_type_axioms (axs, T)

       | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),

         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>

           collect_type_axioms (axs, T)

       | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []),

         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>

           collect_type_axioms (axs, T)

       | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),

         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>

           collect_type_axioms (axs, T)

       | Const ("List.append", T)          => collect_type_axioms (axs, T)

       | Const ("Lfp.lfp", T)            => collect_type_axioms (axs, T)

       | Const ("Gfp.gfp", T)            => collect_type_axioms (axs, T)

       | Const ("fst", T)                => collect_type_axioms (axs, T)

       | Const ("snd", T)                => collect_type_axioms (axs, T)

       (* simply-typed lambda calculus *)

       | Const (s, T)                    =>

           if is_const_of_class thy (s, T) then

             (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *)

             (* and the class definition                               *)

             let

               val class   = Logic.class_of_const s

               val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)

               val ax_in   = SOME (specialize_type thy (s, T) inclass)

                 (* type match may fail due to sort constraints *)

                 handle Type.TYPE_MATCH => NONE

               val ax_1 = Option.map (fn ax => (Sign.string_of_term thy ax, ax))

                 ax_in

               val ax_2 = Option.map (apsnd (specialize_type thy (s, T)))

                 (get_classdef thy class)

             in

               collect_type_axioms (fold collect_this_axiom

                 (map_filter I [ax_1, ax_2]) axs, T)

             end

           else if is_IDT_constructor thy (s, T)

             orelse is_IDT_recursor thy (s, T) then

             (* only collect relevant type axioms *)

             collect_type_axioms (axs, T)

           else

             (* other constants should have been unfolded, with some *)

             (* exceptions: e.g. Abs_xxx/Rep_xxx functions for       *)

             (* typedefs, or type-class related constants            *)

             (* only collect relevant type axioms *)

             collect_type_axioms (axs, T)

       | Free (_, T)      => collect_type_axioms (axs, T)

       | Var (_, T)       => collect_type_axioms (axs, T)

       | Bound i          => axs

       | Abs (_, T, body) => collect_term_axioms

         (collect_type_axioms (axs, T), body)

       | t1 $ t2          => collect_term_axioms

         (collect_term_axioms (axs, t1), t2)

     (* Term.term list *)

     val result = map close_form (collect_term_axioms ([], t))

     val _ = writeln " ...done."

   in

     result

   end;

 (* ------------------------------------------------------------------------- *)

 (* ground_types: collects all ground types in a term (including argument     *)

 (*               types of other types), suppressing duplicates.  Does not    *)

 (*               return function types, set types, non-recursive IDTs, or    *)

 (*               'propT'.  For IDTs, also the argument types of constructors *)

 (*               are considered.                                             *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> Term.term -> Term.typ list *)

   fun ground_types thy t =

   let

     (* Term.typ * Term.typ list -> Term.typ list *)

     fun collect_types (T, acc) =

       if T mem acc then

         acc  (* prevent infinite recursion (for IDTs) *)

       else

         (case T of

           Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc))

         | Type ("prop", [])      => acc

         | Type ("set", [T1])     => collect_types (T1, acc)

         | Type (s, Ts)           =>

           (case DatatypePackage.get_datatype thy s of

             SOME info =>  (* inductive datatype *)

             let

               val index               = #index info

               val descr               = #descr info

               val (_, dtyps, constrs) = lookup descr index

               val typ_assoc           = dtyps ~~ Ts

               (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)

               val _ = (if Library.exists (fn d =>

                   case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps

                 then

                   raise REFUTE ("ground_types", "datatype argument (for type "

                     ^ Sign.string_of_typ thy (Type (s, Ts))

                     ^ ") is not a variable")

                 else

                   ())

               (* if the current type is a recursive IDT (i.e. a depth is *)

               (* required), add it to 'acc'                              *)

               val acc' = (if Library.exists (fn (_, ds) => Library.exists

                 DatatypeAux.is_rec_type ds) constrs then

                   insert (op =) T acc

                 else

                   acc)

               (* collect argument types *)

               val acc_args = foldr collect_types acc' Ts

               (* collect constructor types *)

               val acc_constrs = foldr collect_types acc_args (List.concat

                 (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds)

                   constrs))

             in

               acc_constrs

             end

           | NONE =>

             (* not an inductive datatype, e.g. defined via "typedef" or *)

             (* "typedecl"                                               *)

             insert (op =) T (foldr collect_types acc Ts))

         | TFree _                => insert (op =) T acc

         | TVar _                 => insert (op =) T acc)

   in

     it_term_types collect_types (t, [])

   end;

 (* ------------------------------------------------------------------------- *)

 (* string_of_typ: (rather naive) conversion from types to strings, used to   *)

 (*                look up the size of a type in 'sizes'.  Parameterized      *)

 (*                types with different parameters (e.g. "'a list" vs. "bool  *)

 (*                list") are identified.                                     *)

 (* ------------------------------------------------------------------------- *)

   (* Term.typ -> string *)

   fun string_of_typ (Type (s, _))     = s

     | string_of_typ (TFree (s, _))    = s

     | string_of_typ (TVar ((s,_), _)) = s;

 (* ------------------------------------------------------------------------- *)

 (* first_universe: returns the "first" (i.e. smallest) universe by assigning *)

 (*                 'minsize' to every type for which no size is specified in *)

 (*                 'sizes'                                                   *)

 (* ------------------------------------------------------------------------- *)

   (* Term.typ list -> (string * int) list -> int -> (Term.typ * int) list *)

   fun first_universe xs sizes minsize =

   let

     fun size_of_typ T =

       case AList.lookup (op =) sizes (string_of_typ T) of

         SOME n => n

       | NONE   => minsize

   in

     map (fn T => (T, size_of_typ T)) xs

   end;

 (* ------------------------------------------------------------------------- *)

 (* next_universe: enumerates all universes (i.e. assignments of sizes to     *)

 (*                types), where the minimal size of a type is given by       *)

 (*                'minsize', the maximal size is given by 'maxsize', and a   *)

 (*                type may have a fixed size given in 'sizes'                *)

 (* ------------------------------------------------------------------------- *)

   (* (Term.typ * int) list -> (string * int) list -> int -> int ->

     (Term.typ * int) list option *)

   fun next_universe xs sizes minsize maxsize =

   let

     (* creates the "first" list of length 'len', where the sum of all list *)

     (* elements is 'sum', and the length of the list is 'len'              *)

     (* int -> int -> int -> int list option *)

     fun make_first _ 0 sum =

       if sum=0 then

         SOME []

       else

         NONE

       | make_first max len sum =

       if sum<=max orelse max<0 then

         Option.map (fn xs' => sum :: xs') (make_first max (len-1) 0)

       else

         Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max))

     (* enumerates all int lists with a fixed length, where 0<=x<='max' for *)

     (* all list elements x (unless 'max'<0)                                *)

     (* int -> int -> int -> int list -> int list option *)

     fun next max len sum [] =

       NONE

       | next max len sum [x] =

       (* we've reached the last list element, so there's no shift possible *)

       make_first max (len+1) (sum+x+1)  (* increment 'sum' by 1 *)

       | next max len sum (x1::x2::xs) =

       if x1>0 andalso (x2<max orelse max<0) then

         (* we can shift *)

         SOME (valOf (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)

       else

         (* continue search *)

         next max (len+1) (sum+x1) (x2::xs)

     (* only consider those types for which the size is not fixed *)

     val mutables = List.filter

       (not o (AList.defined (op =) sizes) o string_of_typ o fst) xs

     (* subtract 'minsize' from every size (will be added again at the end) *)

     val diffs = map (fn (_, n) => n-minsize) mutables

   in

     case next (maxsize-minsize) 0 0 diffs of

       SOME diffs' =>

       (* merge with those types for which the size is fixed *)

       SOME (snd (foldl_map (fn (ds, (T, _)) =>

         case AList.lookup (op =) sizes (string_of_typ T) of

         (* return the fixed size *)

           SOME n => (ds, (T, n))

         (* consume the head of 'ds', add 'minsize' *)

         | NONE   => (tl ds, (T, minsize + hd ds)))

         (diffs', xs)))

     | NONE =>

       NONE

   end;

 (* ------------------------------------------------------------------------- *)

 (* toTrue: converts the interpretation of a Boolean value to a propositional *)

 (*         formula that is true iff the interpretation denotes "true"        *)

 (* ------------------------------------------------------------------------- *)

   (* interpretation -> prop_formula *)

   fun toTrue (Leaf [fm, _]) =

     fm

     | toTrue _              =

     raise REFUTE ("toTrue", "interpretation does not denote a Boolean value");

 (* ------------------------------------------------------------------------- *)

 (* toFalse: converts the interpretation of a Boolean value to a              *)

 (*          propositional formula that is true iff the interpretation        *)

 (*          denotes "false"                                                  *)

 (* ------------------------------------------------------------------------- *)

   (* interpretation -> prop_formula *)

   fun toFalse (Leaf [_, fm]) =

     fm

     | toFalse _              =

     raise REFUTE ("toFalse", "interpretation does not denote a Boolean value");

 (* ------------------------------------------------------------------------- *)

 (* find_model: repeatedly calls 'interpret' with appropriate parameters,     *)

 (*             applies a SAT solver, and (in case a model is found) displays *)

 (*             the model to the user by calling 'print_model'                *)

 (* thy       : the current theory                                            *)

 (* {...}     : parameters that control the translation/model generation      *)

 (* t         : term to be translated into a propositional formula            *)

 (* negate    : if true, find a model that makes 't' false (rather than true) *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> params -> Term.term -> bool -> unit *)

   fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver} t

     negate =

   let

     (* unit -> unit *)

     fun wrapper () =

     let

       val u      = unfold_defs thy t

       val _      = writeln ("Unfolded term: " ^ Sign.string_of_term thy u)

       val axioms = collect_axioms thy u

       (* Term.typ list *)

       val types = Library.foldl (fn (acc, t') =>

         acc union (ground_types thy t')) ([], u :: axioms)

       val _     = writeln ("Ground types: "

         ^ (if null types then "none."

            else commas (map (Sign.string_of_typ thy) types)))

       (* we can only consider fragments of recursive IDTs, so we issue a  *)

       (* warning if the formula contains a recursive IDT                  *)

       (* TODO: no warning needed for /positive/ occurrences of IDTs       *)

       val _ = if Library.exists (fn

           Type (s, _) =>

           (case DatatypePackage.get_datatype thy s of

             SOME info =>  (* inductive datatype *)

             let

               val index           = #index info

               val descr           = #descr info

               val (_, _, constrs) = lookup descr index

             in

               (* recursive datatype? *)

               Library.exists (fn (_, ds) =>

                 Library.exists DatatypeAux.is_rec_type ds) constrs

             end

           | NONE => false)

         | _ => false) types then

           warning ("Term contains a recursive datatype; "

             ^ "countermodel(s) may be spurious!")

         else

           ()

       (* (Term.typ * int) list -> unit *)

       fun find_model_loop universe =

       let

         val init_model = (universe, [])

         val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,

           bounds = [], wellformed = True}

         val _          = Output.immediate_output ("Translating term (sizes: "

           ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")

         (* translate 'u' and all axioms *)

         val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>

           let

             val (i, m', a') = interpret thy m a t'

           in

             (* set 'def_eq' to 'true' *)

             ((m', {maxvars = #maxvars a', def_eq = true,

               next_idx = #next_idx a', bounds = #bounds a',

               wellformed = #wellformed a'}), i)

           end) ((init_model, init_args), u :: axioms)

         (* make 'u' either true or false, and make all axioms true, and *)

         (* add the well-formedness side condition                       *)

         val fm_u  = (if negate then toFalse else toTrue) (hd intrs)

         val fm_ax = PropLogic.all (map toTrue (tl intrs))

         val fm    = PropLogic.all [#wellformed args, fm_ax, fm_u]

       in

         Output.immediate_output " invoking SAT solver...";

         (case SatSolver.invoke_solver satsolver fm of

           SatSolver.SATISFIABLE assignment =>

           (writeln " model found!";

           writeln ("*** Model found: ***\n" ^ print_model thy model

             (fn i => case assignment i of SOME b => b | NONE => true)))

         | SatSolver.UNSATISFIABLE _ =>

           (Output.immediate_output " no model exists.\n";

           case next_universe universe sizes minsize maxsize of

             SOME universe' => find_model_loop universe'

           | NONE           => writeln

             "Search terminated, no larger universe within the given limits.")

         | SatSolver.UNKNOWN =>

           (Output.immediate_output " no model found.\n";

           case next_universe universe sizes minsize maxsize of

             SOME universe' => find_model_loop universe'

           | NONE           => writeln

             "Search terminated, no larger universe within the given limits.")

         ) handle SatSolver.NOT_CONFIGURED =>

           error ("SAT solver " ^ quote satsolver ^ " is not configured.")

       end handle MAXVARS_EXCEEDED =>

         writeln ("\nSearch terminated, number of Boolean variables ("

           ^ string_of_int maxvars ^ " allowed) exceeded.")

       in

         find_model_loop (first_universe types sizes minsize)

       end

     in

       (* some parameter sanity checks *)

       minsize>=1 orelse

         error ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1");

       maxsize>=1 orelse

         error ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1");

       maxsize>=minsize orelse

         error ("\"maxsize\" (=" ^ string_of_int maxsize ^

         ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ").");

       maxvars>=0 orelse

         error ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0");

       maxtime>=0 orelse

         error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");

       (* enter loop with or without time limit *)

       writeln ("Trying to find a model that "

         ^ (if negate then "refutes" else "satisfies") ^ ": "

         ^ Sign.string_of_term thy t);

       if maxtime>0 then (

         interrupt_timeout (Time.fromSeconds (Int.toLarge maxtime))

           wrapper ()

         handle Interrupt =>

           writeln ("\nSearch terminated, time limit (" ^ string_of_int maxtime

             ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.")

       ) else

         wrapper ()

     end;

 (* ------------------------------------------------------------------------- *)

 (* INTERFACE, PART 2: FINDING A MODEL                                        *)

 (* ------------------------------------------------------------------------- *)

 (* ------------------------------------------------------------------------- *)

 (* satisfy_term: calls 'find_model' to find a model that satisfies 't'       *)

 (* params      : list of '(name, value)' pairs used to override default      *)

 (*               parameters                                                  *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> (string * string) list -> Term.term -> unit *)

   fun satisfy_term thy params t =

     find_model thy (actual_params thy params) t false;

 (* ------------------------------------------------------------------------- *)

 (* refute_term: calls 'find_model' to find a model that refutes 't'          *)

 (* params     : list of '(name, value)' pairs used to override default       *)

 (*              parameters                                                   *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> (string * string) list -> Term.term -> unit *)

   fun refute_term thy params t =

   let

     (* disallow schematic type variables, since we cannot properly negate  *)

     (* terms containing them (their logical meaning is that there EXISTS a *)

     (* type s.t. ...; to refute such a formula, we would have to show that *)

     (* for ALL types, not ...)                                             *)

     val _ = null (term_tvars t) orelse

       error "Term to be refuted contains schematic type variables"

     (* existential closure over schematic variables *)

     (* (Term.indexname * Term.typ) list *)

     val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))

     (* Term.term *)

     val ex_closure = Library.foldl (fn (t', ((x, i), T)) =>

       (HOLogic.exists_const T) $

         Abs (x, T, abstract_over (Var ((x, i), T), t')))

       (t, vars)

     (* Note: If 't' is of type 'propT' (rather than 'boolT'), applying   *)

     (* 'HOLogic.exists_const' is not type-correct.  However, this is not *)

     (* really a problem as long as 'find_model' still interprets the     *)

     (* resulting term correctly, without checking its type.              *)

     (* replace outermost universally quantified variables by Free's:     *)

     (* refuting a term with Free's is generally faster than refuting a   *)

     (* term with (nested) quantifiers, because quantifiers are expanded, *)

     (* while the SAT solver searches for an interpretation for Free's.   *)

     (* Also we get more information back that way, namely an             *)

     (* interpretation which includes values for the (formerly)           *)

     (* quantified variables.                                             *)

     (* maps  !!x1...xn. !xk...xm. t   to   t  *)

     fun strip_all_body (Const ("all", _) $ Abs (_, _, t)) = strip_all_body t

       | strip_all_body (Const ("Trueprop", _) $ t)        = strip_all_body t

       | strip_all_body (Const ("All", _) $ Abs (_, _, t)) = strip_all_body t

       | strip_all_body t                                  = t

     (* maps  !!x1...xn. !xk...xm. t   to   [x1, ..., xn, xk, ..., xm]  *)

     fun strip_all_vars (Const ("all", _) $ Abs (a, T, t)) =

       (a, T) :: strip_all_vars t

       | strip_all_vars (Const ("Trueprop", _) $ t)        =

       strip_all_vars t

       | strip_all_vars (Const ("All", _) $ Abs (a, T, t)) =

       (a, T) :: strip_all_vars t

       | strip_all_vars t                                  =

       [] : (string * typ) list

     val strip_t = strip_all_body ex_closure

     val frees   = Term.rename_wrt_term strip_t (strip_all_vars ex_closure)

     val subst_t = Term.subst_bounds (map Free frees, strip_t)

   in

     find_model thy (actual_params thy params) subst_t true

   end;

 (* ------------------------------------------------------------------------- *)

 (* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)

 (* params        : list of '(name, value)' pairs used to override default    *)

 (*                 parameters                                                *)

 (* subgoal       : 0-based index specifying the subgoal number               *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> (string * string) list -> Thm.thm -> int -> unit *)

   fun refute_subgoal thy params thm subgoal =

     refute_term thy params (List.nth (Thm.prems_of thm, subgoal));

 (* ------------------------------------------------------------------------- *)

 (* INTERPRETERS: Auxiliary Functions                                         *)

 (* ------------------------------------------------------------------------- *)

 (* ------------------------------------------------------------------------- *)

 (* make_constants: returns all interpretations that have the same tree       *)

 (*                 structure as 'intr', but consist of unit vectors with     *)

 (*                 'True'/'False' only (no Boolean variables)                *)

 (* ------------------------------------------------------------------------- *)

   (* interpretation -> interpretation list *)

   fun make_constants intr =

   let

     (* returns a list with all unit vectors of length n *)

     (* int -> interpretation list *)

     fun unit_vectors n =

     let

       (* returns the k-th unit vector of length n *)

       (* int * int -> interpretation *)

       fun unit_vector (k,n) =

         Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))

       (* int -> interpretation list -> interpretation list *)

       fun unit_vectors_acc k vs =

         if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)

     in

       unit_vectors_acc 1 []

     end

     (* returns a list of lists, each one consisting of n (possibly *)

     (* identical) elements from 'xs'                               *)

     (* int -> 'a list -> 'a list list *)

     fun pick_all 1 xs =

       map single xs

       | pick_all n xs =

       let val rec_pick = pick_all (n-1) xs in

         Library.foldl (fn (acc, x) => map (cons x) rec_pick @ acc) ([], xs)

       end

   in

     case intr of

       Leaf xs => unit_vectors (length xs)

     | Node xs => map (fn xs' => Node xs') (pick_all (length xs)

       (make_constants (hd xs)))

   end;

 (* ------------------------------------------------------------------------- *)

 (* size_of_type: returns the number of constants in a type (i.e. 'length     *)

 (*               (make_constants intr)', but implemented more efficiently)   *)

 (* ------------------------------------------------------------------------- *)

   (* interpretation -> int *)

   fun size_of_type intr =

   let

     (* power (a, b) computes a^b, for a>=0, b>=0 *)

     (* int * int -> int *)

     fun power (a, 0) = 1

       | power (a, 1) = a

       | power (a, b) = let val ab = power(a, b div 2) in

         ab * ab * power(a, b mod 2)

       end

   in

     case intr of

       Leaf xs => length xs

     | Node xs => power (size_of_type (hd xs), length xs)

   end;

 (* ------------------------------------------------------------------------- *)

 (* TT/FF: interpretations that denote "true" or "false", respectively        *)

 (* ------------------------------------------------------------------------- *)

   (* interpretation *)

   val TT = Leaf [True, False];

   val FF = Leaf [False, True];

 (* ------------------------------------------------------------------------- *)

 (* make_equality: returns an interpretation that denotes (extensional)       *)

 (*                equality of two interpretations                            *)

 (* - two interpretations are 'equal' iff they are both defined and denote    *)

 (*   the same value                                                          *)

 (* - two interpretations are 'not_equal' iff they are both defined at least  *)

 (*   partially, and a defined part denotes different values                  *)

 (* - a completely undefined interpretation is neither 'equal' nor            *)

 (*   'not_equal' to another interpretation                                   *)

 (* ------------------------------------------------------------------------- *)

   (* We could in principle represent '=' on a type T by a particular        *)

   (* interpretation.  However, the size of that interpretation is quadratic *)

   (* in the size of T.  Therefore comparing the interpretations 'i1' and    *)

   (* 'i2' directly is more efficient than constructing the interpretation   *)

   (* for equality on T first, and "applying" this interpretation to 'i1'    *)

   (* and 'i2' in the usual way (cf. 'interpretation_apply') then.           *)

   (* interpretation * interpretation -> interpretation *)

   fun make_equality (i1, i2) =

   let

     (* interpretation * interpretation -> prop_formula *)

     fun equal (i1, i2) =

       (case i1 of

         Leaf xs =>

         (case i2 of

           Leaf ys => PropLogic.dot_product (xs, ys)  (* defined and equal *)

         | Node _  => raise REFUTE ("make_equality",

           "second interpretation is higher"))

       | Node xs =>

         (case i2 of

           Leaf _  => raise REFUTE ("make_equality",

           "first interpretation is higher")

         | Node ys => PropLogic.all (map equal (xs ~~ ys))))

     (* interpretation * interpretation -> prop_formula *)

     fun not_equal (i1, i2) =

       (case i1 of

         Leaf xs =>

         (case i2 of

           (* defined and not equal *)

           Leaf ys => PropLogic.all ((PropLogic.exists xs)

           :: (PropLogic.exists ys)

           :: (map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys)))

         | Node _  => raise REFUTE ("make_equality",

           "second interpretation is higher"))

       | Node xs =>

         (case i2 of

           Leaf _  => raise REFUTE ("make_equality",

           "first interpretation is higher")

         | Node ys => PropLogic.exists (map not_equal (xs ~~ ys))))

   in

     (* a value may be undefined; therefore 'not_equal' is not just the *)

     (* negation of 'equal'                                             *)

     Leaf [equal (i1, i2), not_equal (i1, i2)]

   end;

 (* ------------------------------------------------------------------------- *)

 (* make_def_equality: returns an interpretation that denotes (extensional)   *)

 (*                    equality of two interpretations                        *)

 (* This function treats undefined/partially defined interpretations          *)

 (* different from 'make_equality': two undefined interpretations are         *)

 (* considered equal, while a defined interpretation is considered not equal  *)

 (* to an undefined interpretation.                                           *)

 (* ------------------------------------------------------------------------- *)

   (* interpretation * interpretation -> interpretation *)

   fun make_def_equality (i1, i2) =

   let

     (* interpretation * interpretation -> prop_formula *)

     fun equal (i1, i2) =

       (case i1 of

         Leaf xs =>

         (case i2 of

           (* defined and equal, or both undefined *)

           Leaf ys => SOr (PropLogic.dot_product (xs, ys),

           SAnd (PropLogic.all (map SNot xs), PropLogic.all (map SNot ys)))

         | Node _  => raise REFUTE ("make_def_equality",

           "second interpretation is higher"))

       | Node xs =>

         (case i2 of

           Leaf _  => raise REFUTE ("make_def_equality",

           "first interpretation is higher")

         | Node ys => PropLogic.all (map equal (xs ~~ ys))))

     (* interpretation *)

     val eq = equal (i1, i2)

   in

     Leaf [eq, SNot eq]

   end;

 (* ------------------------------------------------------------------------- *)

 (* interpretation_apply: returns an interpretation that denotes the result   *)

 (*                       of applying the function denoted by 'i1' to the     *)

 (*                       argument denoted by 'i2'                            *)

 (* ------------------------------------------------------------------------- *)

   (* interpretation * interpretation -> interpretation *)

   fun interpretation_apply (i1, i2) =

   let

     (* interpretation * interpretation -> interpretation *)

     fun interpretation_disjunction (tr1,tr2) =

       tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys))

         (tree_pair (tr1,tr2))

     (* prop_formula * interpretation -> interpretation *)

     fun prop_formula_times_interpretation (fm,tr) =

       tree_map (map (fn x => SAnd (fm,x))) tr

     (* prop_formula list * interpretation list -> interpretation *)

     fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) =

       prop_formula_times_interpretation (fm,tr)

       | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =

       interpretation_disjunction (prop_formula_times_interpretation (fm,tr),

         prop_formula_list_dot_product_interpretation_list (fms,trees))

       | prop_formula_list_dot_product_interpretation_list (_,_) =

       raise REFUTE ("interpretation_apply", "empty list (in dot product)")

     (* concatenates 'x' with every list in 'xss', returning a new list of *)

     (* lists                                                              *)

     (* 'a -> 'a list list -> 'a list list *)

     fun cons_list x xss =

       map (cons x) xss

     (* returns a list of lists, each one consisting of one element from each *)

     (* element of 'xss'                                                      *)

     (* 'a list list -> 'a list list *)

     fun pick_all [xs] =

       map single xs

       | pick_all (xs::xss) =

       let val rec_pick = pick_all xss in

         Library.foldl (fn (acc, x) => (cons_list x rec_pick) @ acc) ([], xs)

       end

       | pick_all _ =

       raise REFUTE ("interpretation_apply", "empty list (in pick_all)")

     (* interpretation -> prop_formula list *)

     fun interpretation_to_prop_formula_list (Leaf xs) =

       xs

       | interpretation_to_prop_formula_list (Node trees) =

       map PropLogic.all (pick_all

         (map interpretation_to_prop_formula_list trees))

   in

     case i1 of

       Leaf _ =>

       raise REFUTE ("interpretation_apply", "first interpretation is a leaf")

     | Node xs =>

       prop_formula_list_dot_product_interpretation_list

         (interpretation_to_prop_formula_list i2, xs)

   end;

 (* ------------------------------------------------------------------------- *)

 (* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions      *)

 (* ------------------------------------------------------------------------- *)

   (* Term.term -> int -> Term.term *)

   fun eta_expand t i =

   let

     val Ts = Term.binder_types (Term.fastype_of t)

     val t' = Term.incr_boundvars i t

   in

     foldr (fn (T, term) => Abs ("<eta_expand>", T, term))

       (Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i))

   end;

 (* ------------------------------------------------------------------------- *)

 (* sum: returns the sum of a list 'xs' of integers                           *)

 (* ------------------------------------------------------------------------- *)

   (* int list -> int *)

   fun sum xs = foldl op+ 0 xs;

 (* ------------------------------------------------------------------------- *)

 (* product: returns the product of a list 'xs' of integers                   *)

 (* ------------------------------------------------------------------------- *)

   (* int list -> int *)

   fun product xs = foldl op* 1 xs;

 (* ------------------------------------------------------------------------- *)

 (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)

 (*               is the sum (over its constructors) of the product (over     *)

 (*               their arguments) of the size of the argument types          *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> (Term.typ * int) list -> DatatypeAux.descr ->

     (DatatypeAux.dtyp * Term.typ) list ->

     (string * DatatypeAux.dtyp list) list -> int *)

   fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =

     sum (map (fn (_, dtyps) =>

       product (map (fn dtyp =>

         let

           val T         = typ_of_dtyp descr typ_assoc dtyp

           val (i, _, _) = interpret thy (typ_sizes, [])

             {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True}

             (Free ("dummy", T))

         in

           size_of_type i

         end) dtyps)) constructors);

 (* ------------------------------------------------------------------------- *)

 (* INTERPRETERS: Actual Interpreters                                         *)

 (* ------------------------------------------------------------------------- *)

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   (* simply typed lambda calculus: Isabelle's basic term syntax, with type *)

   (* variables, function types, and propT                                  *)

   fun stlc_interpreter thy model args t =

   let

     val (typs, terms)                                   = model

     val {maxvars, def_eq, next_idx, bounds, wellformed} = args

     (* Term.typ -> (interpretation * model * arguments) option *)

     fun interpret_groundterm T =

     let

       (* unit -> (interpretation * model * arguments) option *)

       fun interpret_groundtype () =

       let

         (* the model must specify a size for ground types *)

         val size = (if T = Term.propT then 2 else lookup typs T)

         val next = next_idx+size

         (* check if 'maxvars' is large enough *)

         val _    = (if next-1>maxvars andalso maxvars>0 then

           raise MAXVARS_EXCEEDED else ())

         (* prop_formula list *)

         val fms  = map BoolVar (next_idx upto (next_idx+size-1))

         (* interpretation *)

         val intr = Leaf fms

         (* prop_formula list -> prop_formula *)

         fun one_of_two_false []      = True

           | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' =>

           SOr (SNot x, SNot x')) xs), one_of_two_false xs)

         (* prop_formula *)

         val wf   = one_of_two_false fms

       in

         (* extend the model, increase 'next_idx', add well-formedness *)

         (* condition                                                  *)

         SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars,

           def_eq = def_eq, next_idx = next, bounds = bounds,

           wellformed = SAnd (wellformed, wf)})

       end

     in

       case T of

         Type ("fun", [T1, T2]) =>

         let

           (* we create 'size_of_type (interpret (... T1))' different copies *)

           (* of the interpretation for 'T2', which are then combined into a *)

           (* single new interpretation                                      *)

           val (i1, _, _) = interpret thy model {maxvars=0, def_eq=false,

             next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T1))

           (* make fresh copies, with different variable indices *)

           (* 'idx': next variable index                         *)

           (* 'n'  : number of copies                            *)

           (* int -> int -> (int * interpretation list * prop_formula *)

           fun make_copies idx 0 =

             (idx, [], True)

             | make_copies idx n =

             let

               val (copy, _, new_args) = interpret thy (typs, [])

                 {maxvars = maxvars, def_eq = false, next_idx = idx,

                 bounds = [], wellformed = True} (Free ("dummy", T2))

               val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1)

             in

               (idx', copy :: copies, SAnd (#wellformed new_args, wf'))

             end

           val (next, copies, wf) = make_copies next_idx (size_of_type i1)

           (* combine copies into a single interpretation *)

           val intr = Node copies

         in

           (* extend the model, increase 'next_idx', add well-formedness *)

           (* condition                                                  *)

           SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars,

             def_eq = def_eq, next_idx = next, bounds = bounds,

             wellformed = SAnd (wellformed, wf)})

         end

       | Type _  => interpret_groundtype ()

       | TFree _ => interpret_groundtype ()

       | TVar  _ => interpret_groundtype ()

     end

   in

     case AList.lookup (op =) terms t of

       SOME intr =>

       (* return an existing interpretation *)

       SOME (intr, model, args)

     | NONE =>

       (case t of

         Const (_, T)     =>

         interpret_groundterm T

       | Free (_, T)      =>

         interpret_groundterm T

       | Var (_, T)       =>

         interpret_groundterm T

       | Bound i          =>

         SOME (List.nth (#bounds args, i), model, args)

       | Abs (x, T, body) =>

         let

           (* create all constants of type 'T' *)

           val (i, _, _) = interpret thy model {maxvars=0, def_eq=false,

             next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))

           val constants = make_constants i

           (* interpret the 'body' separately for each constant *)

           val ((model', args'), bodies) = foldl_map

             (fn ((m, a), c) =>

               let

                 (* add 'c' to 'bounds' *)

                 val (i', m', a') = interpret thy m {maxvars = #maxvars a,

                   def_eq = #def_eq a, next_idx = #next_idx a,

                   bounds = (c :: #bounds a), wellformed = #wellformed a} body

               in

                 (* keep the new model m' and 'next_idx' and 'wellformed', *)

                 (* but use old 'bounds'                                   *)

                 ((m', {maxvars = maxvars, def_eq = def_eq,

                   next_idx = #next_idx a', bounds = bounds,

                   wellformed = #wellformed a'}), i')

               end)

             ((model, args), constants)

         in

           SOME (Node bodies, model', args')

         end

       | t1 $ t2          =>

         let

           (* interpret 't1' and 't2' separately *)

           val (intr1, model1, args1) = interpret thy model args t1

           val (intr2, model2, args2) = interpret thy model1 args1 t2

         in

           SOME (interpretation_apply (intr1, intr2), model2, args2)

         end)

   end;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   fun Pure_interpreter thy model args t =

     case t of

       Const ("all", _) $ t1 =>

       let

         val (i, m, a) = interpret thy model args t1

       in

         case i of

           Node xs =>

           (* 3-valued logic *)

           let

             val fmTrue  = PropLogic.all (map toTrue xs)

             val fmFalse = PropLogic.exists (map toFalse xs)

           in

             SOME (Leaf [fmTrue, fmFalse], m, a)

           end

         | _ =>

           raise REFUTE ("Pure_interpreter",

             "\"all\" is followed by a non-function")

       end

     | Const ("all", _) =>

       SOME (interpret thy model args (eta_expand t 1))

     | Const ("==", _) $ t1 $ t2 =>

       let

         val (i1, m1, a1) = interpret thy model args t1

         val (i2, m2, a2) = interpret thy m1 a1 t2

       in

         (* we use either 'make_def_equality' or 'make_equality' *)

         SOME ((if #def_eq args then make_def_equality else make_equality)

           (i1, i2), m2, a2)

       end

     | Const ("==", _) $ t1 =>

       SOME (interpret thy model args (eta_expand t 1))

     | Const ("==", _) =>

       SOME (interpret thy model args (eta_expand t 2))

     | Const ("==>", _) $ t1 $ t2 =>

       (* 3-valued logic *)

       let

         val (i1, m1, a1) = interpret thy model args t1

         val (i2, m2, a2) = interpret thy m1 a1 t2

         val fmTrue       = PropLogic.SOr (toFalse i1, toTrue i2)

         val fmFalse      = PropLogic.SAnd (toTrue i1, toFalse i2)

       in

         SOME (Leaf [fmTrue, fmFalse], m2, a2)

       end

     | Const ("==>", _) $ t1 =>

       SOME (interpret thy model args (eta_expand t 1))

     | Const ("==>", _) =>

       SOME (interpret thy model args (eta_expand t 2))

     | _ => NONE;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   fun HOLogic_interpreter thy model args t =

   (* Providing interpretations directly is more efficient than unfolding the *)

   (* logical constants.  In HOL however, logical constants can themselves be *)

   (* arguments.  They are then translated using eta-expansion.               *)

     case t of

       Const ("Trueprop", _) =>

       SOME (Node [TT, FF], model, args)

     | Const ("Not", _) =>

       SOME (Node [FF, TT], model, args)

     (* redundant, since 'True' is also an IDT constructor *)

     | Const ("True", _) =>

       SOME (TT, model, args)

     (* redundant, since 'False' is also an IDT constructor *)

     | Const ("False", _) =>

       SOME (FF, model, args)

     | Const ("All", _) $ t1 =>  (* similar to "all" (Pure) *)

       let

         val (i, m, a) = interpret thy model args t1

       in

         case i of

           Node xs =>

           (* 3-valued logic *)

           let

             val fmTrue  = PropLogic.all (map toTrue xs)

             val fmFalse = PropLogic.exists (map toFalse xs)

           in

             SOME (Leaf [fmTrue, fmFalse], m, a)

           end

         | _ =>

           raise REFUTE ("HOLogic_interpreter",

             "\"All\" is followed by a non-function")

       end

     | Const ("All", _) =>

       SOME (interpret thy model args (eta_expand t 1))

     | Const ("Ex", _) $ t1 =>

       let

         val (i, m, a) = interpret thy model args t1

       in

         case i of

           Node xs =>

           (* 3-valued logic *)

           let

             val fmTrue  = PropLogic.exists (map toTrue xs)

             val fmFalse = PropLogic.all (map toFalse xs)

           in

             SOME (Leaf [fmTrue, fmFalse], m, a)

           end

         | _ =>

           raise REFUTE ("HOLogic_interpreter",

             "\"Ex\" is followed by a non-function")

       end

     | Const ("Ex", _) =>

       SOME (interpret thy model args (eta_expand t 1))

     | Const ("op =", _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)

       let

         val (i1, m1, a1) = interpret thy model args t1

         val (i2, m2, a2) = interpret thy m1 a1 t2

       in

         SOME (make_equality (i1, i2), m2, a2)

       end

     | Const ("op =", _) $ t1 =>

       SOME (interpret thy model args (eta_expand t 1))

     | Const ("op =", _) =>

       SOME (interpret thy model args (eta_expand t 2))

     | Const ("op &", _) $ t1 $ t2 =>

       (* 3-valued logic *)

       let

         val (i1, m1, a1) = interpret thy model args t1

         val (i2, m2, a2) = interpret thy m1 a1 t2

         val fmTrue       = PropLogic.SAnd (toTrue i1, toTrue i2)

         val fmFalse      = PropLogic.SOr (toFalse i1, toFalse i2)

       in

         SOME (Leaf [fmTrue, fmFalse], m2, a2)

       end

     | Const ("op &", _) $ t1 =>

       SOME (interpret thy model args (eta_expand t 1))

     | Const ("op &", _) =>

       SOME (interpret thy model args (eta_expand t 2))

       (* this would make "undef" propagate, even for formulae like *)

       (* "False & undef":                                          *)

       (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)

     | Const ("op |", _) $ t1 $ t2 =>

       (* 3-valued logic *)

       let

         val (i1, m1, a1) = interpret thy model args t1

         val (i2, m2, a2) = interpret thy m1 a1 t2

         val fmTrue       = PropLogic.SOr (toTrue i1, toTrue i2)

         val fmFalse      = PropLogic.SAnd (toFalse i1, toFalse i2)

       in

         SOME (Leaf [fmTrue, fmFalse], m2, a2)

       end

     | Const ("op |", _) $ t1 =>

       SOME (interpret thy model args (eta_expand t 1))

     | Const ("op |", _) =>

       SOME (interpret thy model args (eta_expand t 2))

       (* this would make "undef" propagate, even for formulae like *)

       (* "True | undef":                                           *)

       (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)

     | Const ("op -->", _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)

       (* 3-valued logic *)

       let

         val (i1, m1, a1) = interpret thy model args t1

         val (i2, m2, a2) = interpret thy m1 a1 t2

         val fmTrue       = PropLogic.SOr (toFalse i1, toTrue i2)

         val fmFalse      = PropLogic.SAnd (toTrue i1, toFalse i2)

       in

         SOME (Leaf [fmTrue, fmFalse], m2, a2)

       end

     | Const ("op -->", _) $ t1 =>

       SOME (interpret thy model args (eta_expand t 1))

     | Const ("op -->", _) =>

       SOME (interpret thy model args (eta_expand t 2))

       (* this would make "undef" propagate, even for formulae like *)

       (* "False --> undef":                                        *)

       (* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *)

     | _ => NONE;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   fun set_interpreter thy model args t =

   (* "T set" is isomorphic to "T --> bool" *)

   let

     val (typs, terms) = model

   in

     case AList.lookup (op =) terms t of

       SOME intr =>

       (* return an existing interpretation *)

       SOME (intr, model, args)

     | NONE =>

       (case t of

         Free (x, Type ("set", [T])) =>

         let

           val (intr, _, args') =

             interpret thy (typs, []) args (Free (x, T --> HOLogic.boolT))

         in

           SOME (intr, (typs, (t, intr)::terms), args')

         end

       | Var ((x, i), Type ("set", [T])) =>

         let

           val (intr, _, args') =

             interpret thy (typs, []) args (Var ((x,i), T --> HOLogic.boolT))

         in

           SOME (intr, (typs, (t, intr)::terms), args')

         end

       | Const (s, Type ("set", [T])) =>

         let

           val (intr, _, args') =

             interpret thy (typs, []) args (Const (s, T --> HOLogic.boolT))

         in

           SOME (intr, (typs, (t, intr)::terms), args')

         end

       (* 'Collect' == identity *)

       | Const ("Collect", _) $ t1 =>

         SOME (interpret thy model args t1)

       | Const ("Collect", _) =>

         SOME (interpret thy model args (eta_expand t 1))

       (* 'op :' == application *)

       | Const ("op :", _) $ t1 $ t2 =>

         SOME (interpret thy model args (t2 $ t1))

       | Const ("op :", _) $ t1 =>

         SOME (interpret thy model args (eta_expand t 1))

       | Const ("op :", _) =>

         SOME (interpret thy model args (eta_expand t 2))

       | _ => NONE)

   end;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   (* interprets variables and constants whose type is an IDT; *)

   (* constructors of IDTs however are properly interpreted by *)

   (* 'IDT_constructor_interpreter'                            *)

   fun IDT_interpreter thy model args t =

   let

     val (typs, terms) = model

     (* Term.typ -> (interpretation * model * arguments) option *)

     fun interpret_term (Type (s, Ts)) =

       (case DatatypePackage.get_datatype thy s of

         SOME info =>  (* inductive datatype *)

         let

           (* int option -- only recursive IDTs have an associated depth *)

           val depth = AList.lookup (op =) typs (Type (s, Ts))

         in

           (* termination condition to avoid infinite recursion *)

           if depth = (SOME 0) then

             (* return a leaf of size 0 *)

             SOME (Leaf [], model, args)

           else

             let

               val index               = #index info

               val descr               = #descr info

               val (_, dtyps, constrs) = lookup descr index

               val typ_assoc           = dtyps ~~ Ts

               (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)

               val _ = (if Library.exists (fn d =>

                   case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps

                 then

                   raise REFUTE ("IDT_interpreter",

                     "datatype argument (for type "

                     ^ Sign.string_of_typ thy (Type (s, Ts))

                     ^ ") is not a variable")

                 else

                   ())

               (* if the model specifies a depth for the current type, *)

               (* decrement it to avoid infinite recursion             *)

               val typs'    = case depth of NONE => typs | SOME n =>

                 AList.update (op =) (Type (s, Ts), n-1) typs

               (* recursively compute the size of the datatype *)

               val size     = size_of_dtyp thy typs' descr typ_assoc constrs

               val next_idx = #next_idx args

               val next     = next_idx+size

               (* check if 'maxvars' is large enough *)

               val _        = (if next-1 > #maxvars args andalso

                 #maxvars args > 0 then raise MAXVARS_EXCEEDED else ())

               (* prop_formula list *)

               val fms      = map BoolVar (next_idx upto (next_idx+size-1))

               (* interpretation *)

               val intr     = Leaf fms

               (* prop_formula list -> prop_formula *)

               fun one_of_two_false []      = True

                 | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' =>

                 SOr (SNot x, SNot x')) xs), one_of_two_false xs)

               (* prop_formula *)

               val wf       = one_of_two_false fms

             in

               (* extend the model, increase 'next_idx', add well-formedness *)

               (* condition                                                  *)

               SOME (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args,

                 def_eq = #def_eq args, next_idx = next, bounds = #bounds args,

                 wellformed = SAnd (#wellformed args, wf)})

             end

         end

       | NONE =>  (* not an inductive datatype *)

         NONE)

       | interpret_term _ =  (* a (free or schematic) type variable *)

       NONE

   in

     case AList.lookup (op =) terms t of

       SOME intr =>

       (* return an existing interpretation *)

       SOME (intr, model, args)

     | NONE =>

       (case t of

         Free (_, T)  => interpret_term T

       | Var (_, T)   => interpret_term T

       | Const (_, T) => interpret_term T

       | _            => NONE)

   end;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   fun IDT_constructor_interpreter thy model args t =

   let

     val (typs, terms) = model

   in

     case AList.lookup (op =) terms t of

       SOME intr =>

       (* return an existing interpretation *)

       SOME (intr, model, args)

     | NONE =>

       (case t of

         Const (s, T) =>

         (case body_type T of

           Type (s', Ts') =>

           (case DatatypePackage.get_datatype thy s' of

             SOME info =>  (* body type is an inductive datatype *)

             let

               val index               = #index info

               val descr               = #descr info

               val (_, dtyps, constrs) = lookup descr index

               val typ_assoc           = dtyps ~~ Ts'

               (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)

               val _ = (if Library.exists (fn d =>

                   case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps

                 then

                   raise REFUTE ("IDT_constructor_interpreter",

                     "datatype argument (for type "

                     ^ Sign.string_of_typ thy (Type (s', Ts'))

                     ^ ") is not a variable")

                 else

                   ())

               (* split the constructors into those occuring before/after *)

               (* 'Const (s, T)'                                          *)

               val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>

                 not (cname = s andalso Sign.typ_instance thy (T,

                   map (typ_of_dtyp descr typ_assoc) ctypes

                     ---> Type (s', Ts')))) constrs

             in

               case constrs2 of

                 [] =>

                 (* 'Const (s, T)' is not a constructor of this datatype *)

                 NONE

               | (_, ctypes)::cs =>

                 let

                   (* compute the total size of the datatype (with the *)

                   (* current depth)                                   *)

                   val (i, _, _) = interpret thy (typs, []) {maxvars=0,

                     def_eq=false, next_idx=1, bounds=[], wellformed=True}

                     (Free ("dummy", Type (s', Ts')))

                   val total     = size_of_type i

                   (* int option -- only /recursive/ IDTs have an associated *)

                   (*               depth                                    *)

                   val depth = AList.lookup (op =) typs (Type (s', Ts'))

                   val typs' = (case depth of NONE => typs | SOME n =>

                     AList.update (op =) (Type (s', Ts'), n-1) typs)

                   (* returns an interpretation where everything is mapped to *)

                   (* "undefined"                                             *)

                   (* DatatypeAux.dtyp list -> interpretation *)

                   fun make_undef [] =

                     Leaf (replicate total False)

                     | make_undef (d::ds) =

                     let

                       (* compute the current size of the type 'd' *)

                       val T           = typ_of_dtyp descr typ_assoc d

                       val (i, _, _)   = interpret thy (typs, []) {maxvars=0,

                         def_eq=false, next_idx=1, bounds=[], wellformed=True}

                         (Free ("dummy", T))

                       val size        = size_of_type i

                     in

                       Node (replicate size (make_undef ds))

                     end

                   (* returns the interpretation for a constructor at depth 1 *)

                   (* int * DatatypeAux.dtyp list -> int * interpretation *)

                   fun make_constr (offset, []) =

                     if offset<total then

                       (offset+1, Leaf ((replicate offset False) @ True ::

                         (replicate (total-offset-1) False)))

                     else

                       raise REFUTE ("IDT_constructor_interpreter",

                         "offset >= total")

                     | make_constr (offset, d::ds) =

                     let

                       (* compute the current and the old size of the type 'd' *)

                       val T           = typ_of_dtyp descr typ_assoc d

                       val (i, _, _)   = interpret thy (typs, []) {maxvars=0,

                         def_eq=false, next_idx=1, bounds=[], wellformed=True}

                         (Free ("dummy", T))

                       val size        = size_of_type i

                       val (i', _, _)  = interpret thy (typs', []) {maxvars=0,

                         def_eq=false, next_idx=1, bounds=[], wellformed=True}

                         (Free ("dummy", T))

                       val size'       = size_of_type i'

                       (* sanity check *)

                       val _           = if size < size' then

                           raise REFUTE ("IDT_constructor_interpreter",

                             "current size is less than old size")

                         else ()

                       (* int * interpretation list *)

                       val (new_offset, intrs) = foldl_map make_constr

                         (offset, replicate size' ds)

                       (* interpretation list *)

                       val undefs = replicate (size - size') (make_undef ds)

                     in

                       (* elements that exist at the previous depth are      *)

                       (* mapped to a defined value, while new elements are  *)

                       (* mapped to "undefined" by the recursive constructor *)

                       (new_offset, Node (intrs @ undefs))

                     end

                   (* extends the interpretation for a constructor (both      *)

                   (* recursive and non-recursive) obtained at depth n (n>=1) *)

                   (* to depth n+1                                            *)

                   (* int * DatatypeAux.dtyp list * interpretation

                     -> int * interpretation *)

                   fun extend_constr (offset, [], Leaf xs) =

                     let

                       (* returns the k-th unit vector of length n *)

                       (* int * int -> interpretation *)

                       fun unit_vector (k, n) =

                         Leaf ((replicate (k-1) False) @ True ::

                           (replicate (n-k) False))

                       (* int *)

                       val k = find_index_eq True xs

                     in

                       if k=(~1) then

                         (* if the element was mapped to "undefined" before, *)

                         (* map it to the value given by 'offset' now (and   *)

                         (* extend the length of the leaf)                   *)

                         (offset+1, unit_vector (offset+1, total))

                       else

                         (* if the element was already mapped to a defined  *)

                         (* value, map it to the same value again, just     *)

                         (* extend the length of the leaf, do not increment *)

                         (* the 'offset'                                    *)

                         (offset, unit_vector (k+1, total))

                     end

                     | extend_constr (_, [], Node _) =

                     raise REFUTE ("IDT_constructor_interpreter",

                       "interpretation for constructor (with no arguments left)"

                       ^ " is a node")

                     | extend_constr (offset, d::ds, Node xs) =

                     let

                       (* compute the size of the type 'd' *)

                       val T          = typ_of_dtyp descr typ_assoc d

                       val (i, _, _)  = interpret thy (typs, []) {maxvars=0,

                         def_eq=false, next_idx=1, bounds=[], wellformed=True}

                         (Free ("dummy", T))

                       val size       = size_of_type i

                       (* sanity check *)

                       val _          = if size < length xs then

                           raise REFUTE ("IDT_constructor_interpreter",

                             "new size of type is less than old size")

                         else ()

                       (* extend the existing interpretations *)

                       (* int * interpretation list *)

                       val (new_offset, intrs) = foldl_map (fn (off, i) =>

                         extend_constr (off, ds, i)) (offset, xs)

                       (* new elements of the type 'd' are mapped to *)

                       (* "undefined"                                *)

                       val undefs = replicate (size - length xs) (make_undef ds)

                     in

                       (new_offset, Node (intrs @ undefs))

                     end

                     | extend_constr (_, d::ds, Leaf _) =

                     raise REFUTE ("IDT_constructor_interpreter",

                       "interpretation for constructor (with arguments left)"

                       ^ " is a leaf")

                   (* returns 'true' iff the constructor has a recursive *)

                   (* argument                                           *)

                   (* DatatypeAux.dtyp list -> bool *)

                   fun is_rec_constr ds =

                     Library.exists DatatypeAux.is_rec_type ds

                   (* constructors before 'Const (s, T)' generate elements of *)

                   (* the datatype                                            *)

                   val offset = size_of_dtyp thy typs' descr typ_assoc constrs1

                 in

                   case depth of

                     NONE =>  (* equivalent to a depth of 1 *)

                     SOME (snd (make_constr (offset, ctypes)), model, args)

                   | SOME 0 =>

                     raise REFUTE ("IDT_constructor_interpreter", "depth is 0")

                   | SOME 1 =>

                     SOME (snd (make_constr (offset, ctypes)), model, args)

                   | SOME n =>  (* n > 1 *)

                     let

                       (* interpret the constructor at depth-1 *)

                       val (iC, _, _) = interpret thy (typs', []) {maxvars=0,

                         def_eq=false, next_idx=1, bounds=[], wellformed=True}

                         (Const (s, T))

                       (* elements generated by the constructor at depth-1 *)

                       (* must be added to 'offset'                        *)

                       (* interpretation -> int *)

                       fun number_of_defined_elements (Leaf xs) =

                         if find_index_eq True xs = (~1) then 0 else 1

                         | number_of_defined_elements (Node xs) =

                         sum (map number_of_defined_elements xs)

                       (* int *)

                       val offset' = offset + number_of_defined_elements iC

                     in

                       SOME (snd (extend_constr (offset', ctypes, iC)), model,

                         args)

                     end

                 end

             end

           | NONE =>  (* body type is not an inductive datatype *)

             NONE)

         | _ =>  (* body type is a (free or schematic) type variable *)

           NONE)

       | _ =>  (* term is not a constant *)

         NONE)

   end;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   (* Difficult code ahead.  Make sure you understand the                *)

   (* 'IDT_constructor_interpreter' and the order in which it enumerates *)

   (* elements of an IDT before you try to understand this function.     *)

   fun IDT_recursion_interpreter thy model args t =

     (* careful: here we descend arbitrarily deep into 't', possibly before *)

     (* any other interpreter for atomic terms has had a chance to look at  *)

     (* 't'                                                                 *)

     case strip_comb t of

       (Const (s, T), params) =>

       (* iterate over all datatypes in 'thy' *)

       Symtab.fold (fn (_, info) => fn result =>

         case result of

           SOME _ =>

           result  (* just keep 'result' *)

         | NONE =>

           if member (op =) (#rec_names info) s then

             (* we do have a recursion operator of the datatype given by *)

             (* 'info', or of a mutually recursive datatype              *)

             let

               val index              = #index info

               val descr              = #descr info

               val (dtname, dtyps, _) = lookup descr index

               (* number of all constructors, including those of different  *)

               (* (mutually recursive) datatypes within the same descriptor *)

               (* 'descr'                                                   *)

               val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs)

                 descr)

               val params_count   = length params

               (* the type of a recursion operator: *)

               (* [T1, ..., Tn, IDT] ---> Tresult   *)

               val IDT = List.nth (binder_types T, mconstrs_count)

             in

               if (fst o dest_Type) IDT <> dtname then

                 (* recursion operator of a mutually recursive datatype *)

                 NONE

               else if mconstrs_count < params_count then

                 (* too many actual parameters; for now we'll use the *)

                 (* 'stlc_interpreter' to strip off one application   *)

                 NONE

               else if mconstrs_count > params_count then

                 (* too few actual parameters; we use eta expansion          *)

                 (* Note that the resulting expansion of lambda abstractions *)

                 (* by the 'stlc_interpreter' may be rather slow (depending  *)

                 (* on the argument types and the size of the IDT, of        *)

                 (* course).                                                 *)

                 SOME (interpret thy model args (eta_expand t

                   (mconstrs_count - params_count)))

               else  (* mconstrs_count = params_count *)

                 let

                   (* interpret each parameter separately *)

                   val ((model', args'), p_intrs) = foldl_map (fn ((m, a), p) =>

                     let

                       val (i, m', a') = interpret thy m a p

                     in

                       ((m', a'), i)

                     end) ((model, args), params)

                   val (typs, _) = model'

                   val typ_assoc = dtyps ~~ (snd o dest_Type) IDT

                   (* interpret each constructor in the descriptor (including *)

                   (* those of mutually recursive datatypes)                  *)

                   (* (int * interpretation list) list *)

                   val mc_intrs = map (fn (idx, (_, _, cs)) =>

                     let

                       val c_return_typ = typ_of_dtyp descr typ_assoc

                         (DatatypeAux.DtRec idx)

                     in

                       (idx, map (fn (cname, cargs) =>

                         (#1 o interpret thy (typs, []) {maxvars=0,

                           def_eq=false, next_idx=1, bounds=[],

                           wellformed=True}) (Const (cname, map (typ_of_dtyp

                           descr typ_assoc) cargs ---> c_return_typ))) cs)

                     end) descr

                   (* the recursion operator is a function that maps every   *)

                   (* element of the inductive datatype (and of mutually     *)

                   (* recursive types) to an element of some result type; an *)

                   (* array entry of NONE means that the actual result has   *)

                   (* not been computed yet                                  *)

                   (* (int * interpretation option Array.array) list *)

                   val INTRS = map (fn (idx, _) =>

                     let

                       val T         = typ_of_dtyp descr typ_assoc

                         (DatatypeAux.DtRec idx)

                       val (i, _, _) = interpret thy (typs, []) {maxvars=0,

                         def_eq=false, next_idx=1, bounds=[], wellformed=True}

                         (Free ("dummy", T))

                       val size      = size_of_type i

                     in

                       (idx, Array.array (size, NONE))

                     end) descr

                   (* takes an interpretation, and if some leaf of this     *)

                   (* interpretation is the 'elem'-th element of the type,  *)

                   (* the indices of the arguments leading to this leaf are *)

                   (* returned                                              *)

                   (* interpretation -> int -> int list option *)

                   fun get_args (Leaf xs) elem =

                     if find_index_eq True xs = elem then

                       SOME []

                     else

                       NONE

                     | get_args (Node xs) elem =

                     let

                       (* interpretation * int -> int list option *)

                       fun search ([], _) =

                         NONE

                         | search (x::xs, n) =

                         (case get_args x elem of

                           SOME result => SOME (n::result)

                         | NONE        => search (xs, n+1))

                     in

                       search (xs, 0)

                     end

                   (* returns the index of the constructor and indices for *)

                   (* its arguments that generate the 'elem'-th element of *)

                   (* the datatype given by 'idx'                          *)

                   (* int -> int -> int * int list *)

                   fun get_cargs idx elem =

                     let

                       (* int * interpretation list -> int * int list *)

                       fun get_cargs_rec (_, []) =

                         raise REFUTE ("IDT_recursion_interpreter",

                           "no matching constructor found for element "

                           ^ string_of_int elem ^ " in datatype "

                           ^ Sign.string_of_typ thy IDT ^ " (datatype index "

                           ^ string_of_int idx ^ ")")

                         | get_cargs_rec (n, x::xs) =

                         (case get_args x elem of

                           SOME args => (n, args)

                         | NONE      => get_cargs_rec (n+1, xs))

                     in

                       get_cargs_rec (0, lookup mc_intrs idx)

                     end

                   (* returns the number of constructors in datatypes that *)

                   (* occur in the descriptor 'descr' before the datatype  *)

                   (* given by 'idx'                                       *)

                   fun get_coffset idx =

                     let

                       fun get_coffset_acc _ [] =

                         raise REFUTE ("IDT_recursion_interpreter", "index "

                           ^ string_of_int idx ^ " not found in descriptor")

                         | get_coffset_acc sum ((i, (_, _, cs))::descr') =

                         if i=idx then

                           sum

                         else

                           get_coffset_acc (sum + length cs) descr'

                     in

                       get_coffset_acc 0 descr

                     end

                   (* computes one entry in INTRS, and recursively all      *)

                   (* entries needed for it, where 'idx' gives the datatype *)

                   (* and 'elem' the element of it                          *)

                   (* int -> int -> interpretation *)

                   fun compute_array_entry idx elem =

                     case Array.sub (lookup INTRS idx, elem) of

                       SOME result =>

                       (* simply return the previously computed result *)

                       result

                     | NONE =>

                       let

                         (* int * int list *)

                         val (c, args) = get_cargs idx elem

                         (* interpretation * int list -> interpretation *)

                         fun select_subtree (tr, []) =

                           tr  (* return the whole tree *)

                           | select_subtree (Leaf _, _) =

                           raise REFUTE ("IDT_recursion_interpreter",

                             "interpretation for parameter is a leaf; "

                             ^ "cannot select a subtree")

                           | select_subtree (Node tr, x::xs) =

                           select_subtree (List.nth (tr, x), xs)

                         (* select the correct subtree of the parameter *)

                         (* corresponding to constructor 'c'            *)

                         val p_intr = select_subtree (List.nth

                           (p_intrs, get_coffset idx + c), args)

                         (* find the indices of the constructor's recursive *)

                         (* arguments                                       *)

                         val (_, _, constrs) = lookup descr idx

                         val constr_args     = (snd o List.nth) (constrs, c)

                         val rec_args        = List.filter

                           (DatatypeAux.is_rec_type o fst) (constr_args ~~ args)

                         val rec_args'       = map (fn (dtyp, elem) =>

                           (DatatypeAux.dest_DtRec dtyp, elem)) rec_args

                         (* apply 'p_intr' to recursively computed results *)

                         val result = foldl (fn ((idx, elem), intr) =>

                           interpretation_apply (intr,

                           compute_array_entry idx elem)) p_intr rec_args'

                         (* update 'INTRS' *)

                         val _ = Array.update (lookup INTRS idx, elem,

                           SOME result)

                       in

                         result

                       end

                   (* compute all entries in INTRS for the current datatype *)

                   (* (given by 'index')                                    *)

                   (* TODO: we can use Array.modifyi instead once PolyML's *)

                   (*       Array signature conforms to the ML standard    *)

                   (* (int * 'a -> 'a) -> 'a array -> unit *)

                   fun modifyi f arr =

                     let

                       val size = Array.length arr

                       fun modifyi_loop i =

                         if i < size then (

                           Array.update (arr, i, f (i, Array.sub (arr, i)));

                           modifyi_loop (i+1)

                         ) else

                           ()

                     in

                       modifyi_loop 0

                     end

                   val _ = modifyi (fn (i, _) =>

                     SOME (compute_array_entry index i)) (lookup INTRS index)

                   (* 'a Array.array -> 'a list *)

                   fun toList arr =

                     Array.foldr op:: [] arr

                 in

                   (* return the part of 'INTRS' that corresponds to the *)

                   (* current datatype                                   *)

                   SOME ((Node o map Option.valOf o toList o lookup INTRS)

                     index, model', args')

                 end

             end

           else

             NONE  (* not a recursion operator of this datatype *)

         ) (DatatypePackage.get_datatypes thy) NONE

     | _ =>  (* head of term is not a constant *)

       NONE;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   (* only an optimization: 'card' could in principle be interpreted with *)

   (* interpreters available already (using its definition), but the code *)

   (* below is more efficient                                             *)

   fun Finite_Set_card_interpreter thy model args t =

     case t of

       Const ("Finite_Set.card",

         Type ("fun", [Type ("set", [T]), Type ("nat", [])])) =>

       let

         val (i_nat, _, _) = interpret thy model

           {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True}

           (Free ("dummy", Type ("nat", [])))

         val size_nat      = size_of_type i_nat

         val (i_set, _, _) = interpret thy model

           {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True}

           (Free ("dummy", Type ("set", [T])))

         val constants     = make_constants i_set

         (* interpretation -> int *)

         fun number_of_elements (Node xs) =

           Library.foldl (fn (n, x) =>

             if x=TT then

               n+1

             else if x=FF then

               n

             else

               raise REFUTE ("Finite_Set_card_interpreter",

                 "interpretation for set type does not yield a Boolean"))

             (0, xs)

           | number_of_elements (Leaf _) =

           raise REFUTE ("Finite_Set_card_interpreter",

             "interpretation for set type is a leaf")

         (* takes an interpretation for a set and returns an interpretation *)

         (* for a 'nat'                                                     *)

         (* interpretation -> interpretation *)

         fun card i =

           let

             val n = number_of_elements i

           in

             if n<size_nat then

               Leaf ((replicate n False) @ True ::

                 (replicate (size_nat-n-1) False))

             else

               Leaf (replicate size_nat False)

           end

       in

         SOME (Node (map card constants), model, args)

       end

     | _ =>

       NONE;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   (* only an optimization: 'Finites' could in principle be interpreted with *)

   (* interpreters available already (using its definition), but the code    *)

   (* below is more efficient                                                *)

   fun Finite_Set_Finites_interpreter thy model args t =

     case t of

       Const ("Finite_Set.Finites", Type ("set", [Type ("set", [T])])) =>

       let

         val (i_set, _, _) = interpret thy model

           {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True}

           (Free ("dummy", Type ("set", [T])))

         val size_set      = size_of_type i_set

       in

         (* we only consider finite models anyway, hence EVERY set is in *)

         (* "Finites"                                                    *)

         SOME (Node (replicate size_set TT), model, args)

       end

     | _ =>

       NONE;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   (* only an optimization: 'finite' could in principle be interpreted with  *)

   (* interpreters available already (using its definition), but the code    *)

   (* below is more efficient                                                *)

   fun Finite_Set_finite_interpreter thy model args t =

     case t of

       Const ("Finite_Set.finite",

         Type ("fun", [Type ("set", [T]), Type ("bool", [])])) $ _ =>

         (* we only consider finite models anyway, hence EVERY set is *)

         (* "finite"                                                  *)

         SOME (TT, model, args)

     | Const ("Finite_Set.finite",

         Type ("fun", [Type ("set", [T]), Type ("bool", [])])) =>

       let

         val (i_set, _, _) = interpret thy model

           {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True}

           (Free ("dummy", Type ("set", [T])))

         val size_set      = size_of_type i_set

       in

         (* we only consider finite models anyway, hence EVERY set is *)

         (* "finite"                                                  *)

         SOME (Node (replicate size_set TT), model, args)

       end

     | _ =>

       NONE;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   (* only an optimization: 'Orderings.less' could in principle be            *)

   (* interpreted with interpreters available already (using its definition), *)

   (* but the code below is more efficient                                    *)

   fun Nat_less_interpreter thy model args t =

     case t of

       Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),

         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>

       let

         val (i_nat, _, _) = interpret thy model

           {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True}

           (Free ("dummy", Type ("nat", [])))

         val size_nat      = size_of_type i_nat

         (* int -> interpretation *)

         (* the 'n'-th nat is not less than the first 'n' nats, while it *)

         (* is less than the remaining 'size_nat - n' nats               *)

         fun less n = Node ((replicate n FF) @ (replicate (size_nat - n) TT))

       in

         SOME (Node (map less (1 upto size_nat)), model, args)

       end

     | _ =>

       NONE;

   (* theory -> model -> arguments -> Term.term ->

     (interpretation * model * arguments) option *)

   (* only an optimization: 'HOL.plus' could in principle be interpreted with *)

   (* interpreters available already (using its definition), but the code     *)

   (* below is more efficient                                                 *)

   fun Nat_plus_interpreter thy model args t =

     case t of

       Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),

         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>

       let

         val (i_nat, _, _) = interpret thy model

           {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True}

           (Free ("dummy", Type ("nat", [])))

         val size_nat      = size_of_type i_nat

         (* int -> int -> interpretation *)

         fun plus m n =

           let

             val element = (m+n)+1

           in

             if element > size_nat then

               Leaf (replicate size_nat False)

             else

               Leaf ((replicate (element-1) False) @ True ::