(*  Title:      HOL/Tools/refute.ML

    Author:     Tjark Weber, TU Muenchen

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 ->

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

  val add_printer     : string -> (theory -> model -> typ ->

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

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

    (interpretation * model * arguments)

  val print       : theory -> model -> typ -> interpretation -> (int -> bool) -> 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 list -> term -> bool -> unit

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

  val satisfy_term :

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

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

  val refute_term :

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

  val refute_goal :

    Proof.context -> (string * string) list -> thm -> int -> unit

  val setup : theory -> theory

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

(* Additional functions used by Nitpick (to be factored out)                 *)

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

  val close_form : term -> term

  val get_classdef : theory -> string -> (string * term) option

  val norm_rhs : term -> term

  val get_def : theory -> string * typ -> (string * term) option

  val get_typedef : theory -> typ -> (string * term) option

  val is_IDT_constructor : theory -> string * typ -> bool

  val is_IDT_recursor : theory -> string * typ -> bool

  val is_const_of_class: theory -> string * typ -> bool

  val string_of_typ : typ -> string

  val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ

end;

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" and "expect"):                                                    *)

(*                                                                           *)

(* 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.                              *)

(* "no_assms"    bool    If "true", assumptions in structured proofs are     *)

(*                       not considered.                                     *)

(* "expect"      string  Expected result ("genuine", "potential", "none", or *)

(*                       "unknown").                                         *)

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

type params =

  {

    sizes    : (string * int) list,

    minsize  : int,

    maxsize  : int,

    maxvars  : int,

    maxtime  : int,

    satsolver: string,

    no_assms : bool,

    expect   : 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 =

  (typ * int) list * (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 = Theory_Data

(

  type T =

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

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

     printers: (string * (theory -> model -> typ -> interpretation ->

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

     parameters: string Symtab.table};

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

  val extend = I;

  fun merge

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

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

    {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 (Syntax.string_of_term_global thy t))

  | SOME x => x;

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

(* print: converts the interpretation 'intr', which must denote a term of    *)

(*        type 'T', into a term using a suitable printer                     *)

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

(* theory -> model -> Term.typ -> 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 type " ^ quote (Syntax.string_of_typ_global 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) =>

          Syntax.string_of_typ_global 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

        cat_lines (map_filter (fn (t, intr) =>

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

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

            SOME (Syntax.string_of_term_global thy t ^ ": " ^

              Syntax.string_of_term_global thy

                (print thy model (Term.type_of 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.typ -> 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) = RefuteData.map 

  (fn {interpreters, printers, parameters} =>

    {interpreters = interpreters, printers = printers,

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

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

(* 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 -> bool *)

    fun read_bool (parms, name) =

      case AList.lookup (op =) parms name of

        SOME "true" => true

      | SOME "false" => false

      | SOME s => error ("parameter " ^ quote name ^

          " (value is " ^ quote s ^ ") must be \"true\" or \"false\"")

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

          " must be assigned a value")

    (* (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")

    val no_assms = read_bool (allparams, "no_assms")

    val expect = the_default "" (AList.lookup (op =) allparams "expect")

    (* 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 = map_filter

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

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

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

        andalso name<>"satsolver" andalso name<>"no_assms") allparams)

  in

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

      maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect}

  end;

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

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

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

fun typ_of_dtyp descr typ_assoc (Datatype_Aux.DtTFree a) =

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

      the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))

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

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

  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =

      let

        val (s, ds, _) = the (AList.lookup (op =) 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 (OldTerm.term_vars t))

  in

    fold (fn ((x, i), T) => fn t' =>

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

  end;

val monomorphic_term = Sledgehammer_Util.monomorphic_term

val specialize_type = Sledgehammer_Util.specialize_type

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

(* 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'.                   *)

    member (op =) class_const_names s

  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 Datatype.get_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)

      (Datatype.get_all thy) []

  in

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

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

    member (op =) rec_names s

  end;

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

(* norm_rhs: 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

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

(* get_def: looks up the definition of a constant                            *)

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

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

fun get_def thy (s, T) =

  let

    (* (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 -> 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'= @{const_name 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

                   | TERM _          => 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 (@{const_name all}, _) => t

      | Const (@{const_name "=="}, _) => t

      | Const (@{const_name "==>"}, _) => t

      | Const (@{const_name TYPE}, _) => t  (* axiomatic type classes *)

      (* HOL *)

      | Const (@{const_name Trueprop}, _) => t

      | Const (@{const_name Not}, _) => t

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

        Const (@{const_name True}, _) => t

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

        Const (@{const_name False}, _) => t

      | Const (@{const_name undefined}, _) => t

      | Const (@{const_name The}, _) => t

      | Const (@{const_name Hilbert_Choice.Eps}, _) => t

      | Const (@{const_name All}, _) => t

      | Const (@{const_name Ex}, _) => t

      | Const (@{const_name HOL.eq}, _) => t

      | Const (@{const_name HOL.conj}, _) => t

      | Const (@{const_name HOL.disj}, _) => t

      | Const (@{const_name HOL.implies}, _) => t

      (* sets *)

      | Const (@{const_name Collect}, _) => t

      | Const (@{const_name Set.member}, _) => t

      (* other optimizations *)

      | Const (@{const_name Finite_Set.card}, _) => t

      | Const (@{const_name Finite_Set.finite}, _) => t

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

          Type ("fun", [@{typ nat}, @{typ bool}])])) => t

      | Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},

          Type ("fun", [@{typ nat}, @{typ nat}])])) => t

      | Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},

          Type ("fun", [@{typ nat}, @{typ nat}])])) => t

      | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},

          Type ("fun", [@{typ nat}, @{typ nat}])])) => t

      | Const (@{const_name List.append}, _) => t

(* UNSOUND

      | Const (@{const_name lfp}, _) => t

      | Const (@{const_name gfp}, _) => t

*)

      | Const (@{const_name fst}, _) => t

      | Const (@{const_name 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.  *)

              ((*tracing (" 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", "definition".  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 _ = tracing "Adding axioms..."

    val axioms = Theory.all_axioms_of thy

    fun collect_this_axiom (axname, ax) axs =

      let

        val ax' = unfold_defs thy ax

      in

        if member (op aconv) axs ax' then axs

        else (tracing axname; collect_term_axioms ax' (ax' :: axs))

      end

    and collect_sort_axioms T axs =

      let

        val sort =

          (case T of

            TFree (_, sort) => sort

          | TVar (_, sort)  => sort

          | _ => raise REFUTE ("collect_axioms",

              "type " ^ Syntax.string_of_typ_global 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_info 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.add_tvars ax [] of

            [] => (axname, ax)

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

          | _ =>

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

              Syntax.string_of_term_global thy ax ^

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

          class_axioms

      in

        fold collect_this_axiom monomorphic_class_axioms axs

      end

    and collect_type_axioms T axs =

      case T of

      (* simple types *)

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

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

      (* axiomatic type classes *)

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

      | Type (s, Ts) =>

        (case Datatype.get_info thy s of

          SOME info =>  (* inductive datatype *)

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

            fold collect_type_axioms Ts axs

        | 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 *)

            fold collect_type_axioms Ts axs))

      (* axiomatic type classes *)

      | TFree _ => collect_sort_axioms T axs

      (* axiomatic type classes *)

      | TVar _ => collect_sort_axioms T axs

    and collect_term_axioms t axs =

      case t of

      (* Pure *)

        Const (@{const_name all}, _) => axs

      | Const (@{const_name "=="}, _) => axs

      | Const (@{const_name "==>"}, _) => axs

      (* axiomatic type classes *)

      | Const (@{const_name TYPE}, T) => collect_type_axioms T axs

      (* HOL *)

      | Const (@{const_name Trueprop}, _) => axs

      | Const (@{const_name Not}, _) => axs

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

      | Const (@{const_name True}, _) => axs

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

      | Const (@{const_name False}, _) => axs

      | Const (@{const_name undefined}, T) => collect_type_axioms T axs

      | Const (@{const_name The}, T) =>

          let

            val ax = specialize_type thy (@{const_name The}, T)

              (the (AList.lookup (op =) axioms "HOL.the_eq_trivial"))

          in

            collect_this_axiom ("HOL.the_eq_trivial", ax) axs

          end

      | Const (@{const_name Hilbert_Choice.Eps}, T) =>

          let

            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T)

              (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))

          in

            collect_this_axiom ("Hilbert_Choice.someI", ax) axs

          end

      | Const (@{const_name All}, T) => collect_type_axioms T axs

      | Const (@{const_name Ex}, T) => collect_type_axioms T axs

      | Const (@{const_name HOL.eq}, T) => collect_type_axioms T axs

      | Const (@{const_name HOL.conj}, _) => axs

      | Const (@{const_name HOL.disj}, _) => axs

      | Const (@{const_name HOL.implies}, _) => axs

      (* sets *)

      | Const (@{const_name Collect}, T) => collect_type_axioms T axs

      | Const (@{const_name Set.member}, T) => collect_type_axioms T axs

      (* other optimizations *)

      | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs

      | Const (@{const_name Finite_Set.finite}, T) =>

        collect_type_axioms T axs

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

        Type ("fun", [@{typ nat}, @{typ bool}])])) =>

          collect_type_axioms T axs

      | Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat},

        Type ("fun", [@{typ nat}, @{typ nat}])])) =>

          collect_type_axioms T axs

      | Const (@{const_name Groups.minus}, T as Type ("fun", [@{typ nat},

        Type ("fun", [@{typ nat}, @{typ nat}])])) =>

          collect_type_axioms T axs

      | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},

        Type ("fun", [@{typ nat}, @{typ nat}])])) =>

          collect_type_axioms T axs

      | Const (@{const_name List.append}, T) => collect_type_axioms T axs

(* UNSOUND

      | Const (@{const_name lfp}, T) => collect_type_axioms T axs

      | Const (@{const_name gfp}, T) => collect_type_axioms T axs

*)

      | Const (@{const_name fst}, T) => collect_type_axioms T axs

      | Const (@{const_name snd}, T) => collect_type_axioms T axs

      (* 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 of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class)

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

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

                handle Type.TYPE_MATCH => NONE

              val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax)) ax_in

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

            in

              collect_type_axioms T (fold collect_this_axiom (map_filter I [ax_1, ax_2]) axs)

            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 T axs

          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 T axs

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

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

      | Bound _ => axs

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

      | t1 $ t2 => collect_term_axioms t2 (collect_term_axioms t1 axs)

    val result = map close_form (collect_term_axioms t [])

    val _ = tracing " ...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 *)

(*               and all mutually recursive IDTs are considered.             *)

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

fun ground_types thy t =

  let

    fun collect_types T acc =

      (case T of

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

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

      | Type (s, Ts) =>

          (case Datatype.get_info thy s of

            SOME info =>  (* inductive datatype *)

              let

                val index = #index info

                val descr = #descr info

                val (_, typs, _) = the (AList.lookup (op =) descr index)

                val typ_assoc = typs ~~ Ts

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

                (* 'DtTFree'                                        *)

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

                  case d of Datatype_Aux.DtTFree _ => false | _ => true) typs then

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

                    ^ Syntax.string_of_typ_global thy T ^ ") is not a variable")

                else ()

                (* required for mutually recursive datatypes; those need to   *)

                (* be added even if they are an instance of an otherwise non- *)

                (* recursive datatype                                         *)

                fun collect_dtyp d acc =

                  let

                    val dT = typ_of_dtyp descr typ_assoc d

                  in

                    case d of

                      Datatype_Aux.DtTFree _ =>

                      collect_types dT acc

                    | Datatype_Aux.DtType (_, ds) =>

                      collect_types dT (fold_rev collect_dtyp ds acc)

                    | Datatype_Aux.DtRec i =>

                      if member (op =) acc dT then

                        acc  (* prevent infinite recursion *)

                      else

                        let

                          val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i)

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

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

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

                            Library.exists Datatype_Aux.is_rec_type ds) dconstrs then

                              insert (op =) dT acc

                            else acc

                          (* collect argument types *)

                          val acc_dtyps = fold_rev collect_dtyp dtyps acc_dT

                          (* collect constructor types *)

                          val acc_dconstrs = fold_rev collect_dtyp (maps snd dconstrs) acc_dtyps

                        in

                          acc_dconstrs

                        end

                  end

              in

                (* argument types 'Ts' could be added here, but they are also *)

                (* added by 'collect_dtyp' automatically                      *)

                collect_dtyp (Datatype_Aux.DtRec index) acc

              end

          | NONE =>

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

            (* "typedecl"                                               *)

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

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

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

  in

    fold_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 =