products/sources/formale Sprachen/Isabelle/HOL/Library image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: refute.ML   Sprache: SML

Original von: Isabelle©

(*  Title:      HOL/Library/refute.ML
    Author:     Tjark Weber, TU Muenchen

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


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 -> (Proof.context -> model -> arguments -> term ->
    (interpretation * model * arguments) option) -> theory -> theory
  val add_printer : string -> (Proof.context -> model -> typ ->
    interpretation -> (int -> bool) -> term option) -> theory -> theory

  val interpret : Proof.context -> model -> arguments -> term ->
    (interpretation * model * arguments)

  val print : Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term
  val print_model : Proof.context -> model -> (int -> bool) -> string

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

  val set_default_param  : (string * string) -> theory -> theory
  val get_default_param  : Proof.context -> string -> string option
  val get_default_params : Proof.context -> (string * stringlist
  val actual_params      : Proof.context -> (string * stringlist -> params

  val find_model :
    Proof.context -> params -> term list -> term -> bool -> string

  (* tries to find a model for a formula: *)
  val satisfy_term :
    Proof.context -> (string * stringlist -> term list -> term -> string
  (* tries to find a model that refutes a formula: *)
  val refute_term :
    Proof.context -> (string * stringlist -> term list -> term -> string
  val refute_goal :
    Proof.context -> (string * stringlist -> thm -> int -> string

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

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

structure Refute : REFUTE =
struct

open Prop_Logic;

(* 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;

fun tree_map f tr =
  case tr of
    Leaf x  => Leaf (f x)
  | Node xs => Node (map (tree_map f) xs);

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 Data = Theory_Data
(
  type T =
    {interpreters: (string * (Proof.context -> model -> arguments -> term ->
      (interpretation * model * arguments) option)) list,
     printers: (string * (Proof.context -> 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)};
);

val get_data = Data.get o Proof_Context.theory_of;


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

fun interpret ctxt model args t =
  case get_first (fn (_, f) => f ctxt model args t)
      (#interpreters (get_data ctxt)) of
    NONE => raise REFUTE ("interpret",
      "no interpreter for term " ^ quote (Syntax.string_of_term ctxt t))
  | SOME x => x;

(* ------------------------------------------------------------------------- *)
(* print: converts the interpretation 'intr', which must denote a term of    *)
(*        type 'T', into a term using a suitable printer                     *)
(* ------------------------------------------------------------------------- *)

fun print ctxt model T intr assignment =
  case get_first (fn (_, f) => f ctxt model T intr assignment)
      (#printers (get_data ctxt)) of
    NONE => raise REFUTE ("print",
      "no printer for type " ^ quote (Syntax.string_of_typ ctxt 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                                                     *)
(* ------------------------------------------------------------------------- *)

fun print_model ctxt 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 ctxt T ^ ": " ^ string_of_int i) typs) ^ "\n"
    val show_consts_msg =
      if not (Config.get ctxt show_consts) andalso Library.exists (is_Const o fst) terms then
        "enable \"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 Config.get ctxt show_consts orelse not (is_Const t) then
            SOME (Syntax.string_of_term ctxt t ^ ": " ^
              Syntax.string_of_term ctxt
                (print ctxt model (Term.type_of t) intr assignment))
          else
            NONE) terms) ^ "\n"
  in
    typs_msg ^ show_consts_msg ^ terms_msg
  end;


(* ------------------------------------------------------------------------- *)
(* PARAMETER MANAGEMENT                                                      *)
(* ------------------------------------------------------------------------- *)

fun add_interpreter name f = Data.map (fn {interpreters, printers, parameters} =>
  case AList.lookup (op =) interpreters name of
    NONE => {interpreters = (name, f) :: interpreters,
      printers = printers, parameters = parameters}
  | SOME _ => error ("Interpreter " ^ name ^ " already declared"));

fun add_printer name f = Data.map (fn {interpreters, printers, parameters} =>
  case AList.lookup (op =) printers name of
    NONE => {interpreters = interpreters,
      printers = (name, f) :: printers, parameters = parameters}
  | SOME _ => error ("Printer " ^ name ^ " already declared"));

(* ------------------------------------------------------------------------- *)
(* set_default_param: stores the '(name, value)' pair in Data's              *)
(*                    parameter table                                        *)
(* ------------------------------------------------------------------------- *)

fun set_default_param (name, value) = Data.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        *)
(*                    Data's parameter table                                 *)
(* ------------------------------------------------------------------------- *)

val get_default_param = Symtab.lookup o #parameters o get_data;

(* ------------------------------------------------------------------------- *)
(* get_default_params: returns a list of all '(name, value)' pairs that are  *)
(*                     stored in Data's parameter table                      *)
(* ------------------------------------------------------------------------- *)

val get_default_params = Symtab.dest o #parameters o get_data;

(* ------------------------------------------------------------------------- *)
(* actual_params: takes a (possibly empty) list 'params' of parameters that  *)
(*      override the default parameters currently specified, and             *)
(*      returns a record that can be passed to 'find_model'.                 *)
(* ------------------------------------------------------------------------- *)

fun actual_params ctxt override =
  let
    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")
    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")
    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: *)
    val allparams = override @ get_default_params ctxt
    val minsize = read_int (allparams, "minsize")
    val maxsize = read_int (allparams, "maxsize")
    val maxvars = read_int (allparams, "maxvars")
    val maxtime = read_int (allparams, "maxtime")
    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 _ typ_assoc (Old_Datatype_Aux.DtTFree a) =
    the (AList.lookup (op =) typ_assoc (Old_Datatype_Aux.DtTFree a))
  | typ_of_dtyp descr typ_assoc (Old_Datatype_Aux.DtType (s, Us)) =
    Type (s, map (typ_of_dtyp descr typ_assoc) Us)
  | typ_of_dtyp descr typ_assoc (Old_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

val close_form = ATP_Util.close_form
val specialize_type = ATP_Util.specialize_type

(* ------------------------------------------------------------------------- *)
(* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that   *)
(*                    denotes membership to an axiomatic type class          *)
(* ------------------------------------------------------------------------- *)

fun is_const_of_class thy (s, _) =
  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'                     *)
(* ------------------------------------------------------------------------- *)

fun is_IDT_constructor thy (s, T) =
  (case body_type T of
    Type (s', _) =>
      (case BNF_LFP_Compat.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'               *)
(* ------------------------------------------------------------------------- *)

fun is_IDT_recursor thy (s, _) =
  let
    val rec_names = Symtab.fold (append o #rec_names o snd) (BNF_LFP_Compat.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                            *)
(* ------------------------------------------------------------------------- *)

fun get_def thy (s, T) =
  let
    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' = Envir.subst_term_types 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"   *)
(* ------------------------------------------------------------------------- *)

fun get_typedef thy T =
  let
    fun get_typedef_ax [] = NONE
      | get_typedef_ax ((axname, ax) :: axioms) =
          (let
            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 (domain_type T')
                  val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty
                in
                  SOME (axname, Envir.subst_term_types 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                            *)
(* ------------------------------------------------------------------------- *)

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

(* 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
    fun unfold_loop t =
      case t of
      (* Pure *)
        Const (\<^const_name>\<open>Pure.all\<close>, _) => t
      | Const (\<^const_name>\<open>Pure.eq\<close>, _) => t
      | Const (\<^const_name>\<open>Pure.imp\<close>, _) => t
      | Const (\<^const_name>\<open>Pure.type\<close>, _) => t  (* axiomatic type classes *)
      (* HOL *)
      | Const (\<^const_name>\<open>Trueprop\<close>, _) => t
      | Const (\<^const_name>\<open>Not\<close>, _) => t
      | (* redundant, since 'True' is also an IDT constructor *)
        Const (\<^const_name>\<open>True\<close>, _) => t
      | (* redundant, since 'False' is also an IDT constructor *)
        Const (\<^const_name>\<open>False\<close>, _) => t
      | Const (\<^const_name>\<open>undefined\<close>, _) => t
      | Const (\<^const_name>\<open>The\<close>, _) => t
      | Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) => t
      | Const (\<^const_name>\<open>All\<close>, _) => t
      | Const (\<^const_name>\<open>Ex\<close>, _) => t
      | Const (\<^const_name>\<open>HOL.eq\<close>, _) => t
      | Const (\<^const_name>\<open>HOL.conj\<close>, _) => t
      | Const (\<^const_name>\<open>HOL.disj\<close>, _) => t
      | Const (\<^const_name>\<open>HOL.implies\<close>, _) => t
      (* sets *)
      | Const (\<^const_name>\<open>Collect\<close>, _) => t
      | Const (\<^const_name>\<open>Set.member\<close>, _) => t
      (* other optimizations *)
      | Const (\<^const_name>\<open>Finite_Set.card\<close>, _) => t
      | Const (\<^const_name>\<open>Finite_Set.finite\<close>, _) => t
      | Const (\<^const_name>\<open>Orderings.less\<close>, Type ("fun", [\<^typ>\<open>nat\<close>,
          Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>bool\<close>])])) => t
      | Const (\<^const_name>\<open>Groups.plus\<close>, Type ("fun", [\<^typ>\<open>nat\<close>,
          Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) => t
      | Const (\<^const_name>\<open>Groups.minus\<close>, Type ("fun", [\<^typ>\<open>nat\<close>,
          Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) => t
      | Const (\<^const_name>\<open>Groups.times\<close>, Type ("fun", [\<^typ>\<open>nat\<close>,
          Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) => t
      | Const (\<^const_name>\<open>append\<close>, _) => t
      | Const (\<^const_name>\<open>fst\<close>, _) => t
      | Const (\<^const_name>\<open>snd\<close>, _) => 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'.                      *)

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

local

fun get_axiom thy xname =
  Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none);

val the_eq_trivial = get_axiom \<^theory>\<open>HOL\<close> "the_eq_trivial";
val someI = get_axiom \<^theory>\<open>Hilbert_Choice\<close> "someI";

in

fun collect_axioms ctxt t =
  let
    val thy = Proof_Context.theory_of ctxt
    val _ = tracing "Adding axioms..."
    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 ctxt 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, Envir.subst_term_types (Vartab.make [(idx, (S, T))]) ax)
          | _ =>
            raise REFUTE ("collect_axioms""class axiom " ^ axname ^ " (" ^
              Syntax.string_of_term ctxt 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 (\<^type_name>\<open>prop\<close>, []) => axs
      | Type (\<^type_name>\<open>fun\<close>, [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
      | Type (\<^type_name>\<open>set\<close>, [T1]) => collect_type_axioms T1 axs
      (* axiomatic type classes *)
      | Type (\<^type_name>\<open>itself\<close>, [T1]) => collect_type_axioms T1 axs
      | Type (s, Ts) =>
        (case BNF_LFP_Compat.get_info thy [] s of
          SOME _ =>  (* 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>\<open>Pure.all\<close>, _) => axs
      | Const (\<^const_name>\<open>Pure.eq\<close>, _) => axs
      | Const (\<^const_name>\<open>Pure.imp\<close>, _) => axs
      (* axiomatic type classes *)
      | Const (\<^const_name>\<open>Pure.type\<close>, T) => collect_type_axioms T axs
      (* HOL *)
      | Const (\<^const_name>\<open>Trueprop\<close>, _) => axs
      | Const (\<^const_name>\<open>Not\<close>, _) => axs
      (* redundant, since 'True' is also an IDT constructor *)
      | Const (\<^const_name>\<open>True\<close>, _) => axs
      (* redundant, since 'False' is also an IDT constructor *)
      | Const (\<^const_name>\<open>False\<close>, _) => axs
      | Const (\<^const_name>\<open>undefined\<close>, T) => collect_type_axioms T axs
      | Const (\<^const_name>\<open>The\<close>, T) =>
          let
            val ax = specialize_type thy (\<^const_name>\<open>The\<close>, T) (#2 the_eq_trivial)
          in
            collect_this_axiom (#1 the_eq_trivial, ax) axs
          end
      | Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, T) =>
          let
            val ax = specialize_type thy (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, T) (#2 someI)
          in
            collect_this_axiom (#1 someI, ax) axs
          end
      | Const (\<^const_name>\<open>All\<close>, T) => collect_type_axioms T axs
      | Const (\<^const_name>\<open>Ex\<close>, T) => collect_type_axioms T axs
      | Const (\<^const_name>\<open>HOL.eq\<close>, T) => collect_type_axioms T axs
      | Const (\<^const_name>\<open>HOL.conj\<close>, _) => axs
      | Const (\<^const_name>\<open>HOL.disj\<close>, _) => axs
      | Const (\<^const_name>\<open>HOL.implies\<close>, _) => axs
      (* sets *)
      | Const (\<^const_name>\<open>Collect\<close>, T) => collect_type_axioms T axs
      | Const (\<^const_name>\<open>Set.member\<close>, T) => collect_type_axioms T axs
      (* other optimizations *)
      | Const (\<^const_name>\<open>Finite_Set.card\<close>, T) => collect_type_axioms T axs
      | Const (\<^const_name>\<open>Finite_Set.finite\<close>, T) =>
        collect_type_axioms T axs
      | Const (\<^const_name>\<open>Orderings.less\<close>, T as Type ("fun", [\<^typ>\<open>nat\<close>,
        Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>bool\<close>])])) =>
          collect_type_axioms T axs
      | Const (\<^const_name>\<open>Groups.plus\<close>, T as Type ("fun", [\<^typ>\<open>nat\<close>,
        Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) =>
          collect_type_axioms T axs
      | Const (\<^const_name>\<open>Groups.minus\<close>, T as Type ("fun", [\<^typ>\<open>nat\<close>,
        Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) =>
          collect_type_axioms T axs
      | Const (\<^const_name>\<open>Groups.times\<close>, T as Type ("fun", [\<^typ>\<open>nat\<close>,
        Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) =>
          collect_type_axioms T axs
      | Const (\<^const_name>\<open>append\<close>, T) => collect_type_axioms T axs
      | Const (\<^const_name>\<open>fst\<close>, T) => collect_type_axioms T axs
      | Const (\<^const_name>\<open>snd\<close>, 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 ctxt 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;

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 ctxt t =
  let
    val thy = Proof_Context.theory_of ctxt
    fun collect_types T acc =
      (case T of
        Type (\<^type_name>\<open>fun\<close>, [T1, T2]) => collect_types T1 (collect_types T2 acc)
      | Type (\<^type_name>\<open>prop\<close>, []) => acc
      | Type (\<^type_name>\<open>set\<close>, [T1]) => collect_types T1 acc
      | Type (s, Ts) =>
          (case BNF_LFP_Compat.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 Old_Datatype_Aux.DtTFree _ => false | _ => true) typs then
                  raise REFUTE ("ground_types""datatype argument (for type "
                    ^ Syntax.string_of_typ ctxt 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
                      Old_Datatype_Aux.DtTFree _ =>
                      collect_types dT acc
                    | Old_Datatype_Aux.DtType (_, ds) =>
                      collect_types dT (fold_rev collect_dtyp ds acc)
                    | Old_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 Old_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 (Old_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.                                     *)
(* ------------------------------------------------------------------------- *)

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

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

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'              *)
    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)                                *)
    fun next _ _ _ [] =
          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 (the (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 = filter_out (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 (fst (fold_map (fn (T, _) => fn ds =>
          case AList.lookup (op =) sizes (string_of_typ T) of
          (* return the fixed size *)
            SOME n => ((T, n), ds)
          (* consume the head of 'ds', add 'minsize' *)
          | NONE   => ((T, minsize + hd ds), tl ds))
          xs diffs'))
    | NONE => NONE
  end;

(* ------------------------------------------------------------------------- *)
(* toTrue: converts the interpretation of a Boolean value to a propositional *)
(*         formula that is true iff the interpretation denotes "true"        *)
(* ------------------------------------------------------------------------- *)

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

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'                *)
(* {...}     : parameters that control the translation/model generation      *)
(* assm_ts   : assumptions to be considered unless "no_assms" is specified   *)
(* t         : term to be translated into a propositional formula            *)
(* negate    : if true, find a model that makes 't' false (rather than true) *)
(* ------------------------------------------------------------------------- *)

fun find_model ctxt
    {sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect}
    assm_ts t negate =
  let
    val thy = Proof_Context.theory_of ctxt
    fun check_expect outcome_code =
      if expect = "" orelse outcome_code = expect then outcome_code
      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    fun wrapper () =
      let
        val timer = Timer.startRealTimer ()
        val t =
          if no_assms then t
          else if negate then Logic.list_implies (assm_ts, t)
          else Logic.mk_conjunction_list (t :: assm_ts)
        val u = unfold_defs thy t
        val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term ctxt u)
        val axioms = collect_axioms ctxt u
        val types = fold (union (op =) o ground_types ctxt) (u :: axioms) []
        val _ = tracing ("Ground types: "
          ^ (if null types then "none."
             else commas (map (Syntax.string_of_typ ctxt) 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 maybe_spurious = Library.exists (fn
            Type (s, _) =>
              (case BNF_LFP_Compat.get_info thy [] s of
                SOME info =>  (* inductive datatype *)
                  let
                    val index           = #index info
                    val descr           = #descr info
                    val (_, _, constrs) = the (AList.lookup (op =) descr index)
                  in
                    (* recursive datatype? *)
                    Library.exists (fn (_, ds) =>
                      Library.exists Old_Datatype_Aux.is_rec_type ds) constrs
                  end
              | NONE => false)
          | _ => false) types
        val _ =
          if maybe_spurious andalso Context_Position.is_visible ctxt then
            warning "Term contains a recursive datatype; countermodel(s) may be spurious!"
          else ()
        fun find_model_loop universe =
          let
            val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
            val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
                    orelse raise Timeout.TIMEOUT (Time.fromMilliseconds msecs_spent)
            val init_model = (universe, [])
            val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
              bounds = [], wellformed = True}
            val _ = tracing ("Translating term (sizes: "
              ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
            (* translate 'u' and all axioms *)
            val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) =>
              let
                val (i, m', a') = interpret ctxt m a t'
              in
                (* set 'def_eq' to 'true' *)
                (i, (m', {maxvars = #maxvars a', def_eq = true,
                  next_idx = #next_idx a', bounds = #bounds a',
                  wellformed = #wellformed a'}))
              end) (u :: axioms) (init_model, init_args)
            (* 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 = Prop_Logic.all (map toTrue (tl intrs))
            val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
            val _ =
              (if member (op =) ["cdclite"] satsolver andalso Context_Position.is_visible ctxt then
                warning ("Using SAT solver " ^ quote satsolver ^
                         "; for better performance, consider installing an \
                         \external solver.")
               else ());
            val solver =
              SAT_Solver.invoke_solver satsolver
              handle Option.Option =>
                     error ("Unknown SAT solver: " ^ quote satsolver ^
                            ". Available solvers: " ^
                            commas (map (quote o fst) (SAT_Solver.get_solvers ())) ^ ".")
          in
            writeln "Invoking SAT solver...";
            (case solver fm of
              SAT_Solver.SATISFIABLE assignment =>
                (writeln ("Model found:\n" ^ print_model ctxt model
                  (fn i => case assignment i of SOME b => b | NONE => true));
                 if maybe_spurious then "potential" else "genuine")
            | SAT_Solver.UNSATISFIABLE _ =>
                (writeln "No model exists.";
                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.";
                    "none"))
            | SAT_Solver.UNKNOWN =>
                (writeln "No model found.";
                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.";
                  "unknown"))) handle SAT_Solver.NOT_CONFIGURED =>
              (error ("SAT solver " ^ quote satsolver ^ " is not configured.");
               "unknown")
          end
          handle MAXVARS_EXCEEDED =>
            (writeln ("Search terminated, number of Boolean variables ("
              ^ string_of_int maxvars ^ " allowed) exceeded.");
              "unknown")

        val outcome_code = find_model_loop (first_universe types sizes minsize)
      in
        check_expect outcome_code
      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") ^ ": "
      ^ Syntax.string_of_term ctxt t);
    if maxtime > 0 then (
      Timeout.apply (Time.fromSeconds maxtime)
        wrapper ()
      handle Timeout.TIMEOUT _ =>
        (writeln ("Search terminated, time limit (" ^
            string_of_int maxtime
            ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
         check_expect "unknown")
    ) 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                                                  *)
(* ------------------------------------------------------------------------- *)

fun satisfy_term ctxt params assm_ts t =
  find_model ctxt (actual_params ctxt params) assm_ts 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                                                   *)
(* ------------------------------------------------------------------------- *)

fun refute_term ctxt params assm_ts 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.add_tvars t []) orelse
      error "Term to be refuted contains schematic type variables"

    (* existential closure over schematic variables *)
    val vars = sort_by (fst o fst) (Term.add_vars t [])
    (* Term.term *)
    val ex_closure = fold (fn ((x, i), T) => fn t' =>
      HOLogic.exists_const T $
        Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
    (* 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 (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t)) =
          strip_all_body t
      | strip_all_body (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t) =
          strip_all_body t
      | strip_all_body (Const (\<^const_name>\<open>All\<close>, _) $ 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 (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (a, T, t)) =
          (a, T) :: strip_all_vars t
      | strip_all_vars (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t) =
          strip_all_vars t
      | strip_all_vars (Const (\<^const_name>\<open>All\<close>, _) $ Abs (a, T, t)) =
          (a, T) :: strip_all_vars t
      | strip_all_vars _ = [] : (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 ctxt (actual_params ctxt params) assm_ts subst_t true
  end;

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

fun refute_goal ctxt params th i =
  let
    val t = th |> Thm.prop_of
  in
    if Logic.count_prems t = 0 then
      (writeln "No subgoal!""none")
    else
      let
        val assms = map Thm.term_of (Assumption.all_assms_of ctxt)
        val (t, frees) = Logic.goal_params t i
      in
        refute_term ctxt params assms (subst_bounds (frees, t))
      end
  end


(* ------------------------------------------------------------------------- *)
(* INTERPRETERS: Auxiliary Functions                                         *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* make_constants: returns all interpretations for type 'T' that consist of  *)
(*                 unit vectors with 'True'/'False' only (no Boolean         *)
(*                 variables)                                                *)
(* ------------------------------------------------------------------------- *)

fun make_constants ctxt model T =
  let
    (* returns a list with all unit vectors of length n *)
    fun unit_vectors n =
      let
        (* returns the k-th unit vector of length n *)
        fun unit_vector (k, n) =
          Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
        fun unit_vectors_loop k =
          if k>n then [] else unit_vector (k,n) :: unit_vectors_loop (k+1)
      in
        unit_vectors_loop 1
      end
    (* returns a list of lists, each one consisting of n (possibly *)
    (* identical) elements from 'xs'                               *)
    fun pick_all 1 xs = map single xs
      | pick_all n xs =
          let val rec_pick = pick_all (n - 1) xs in
            maps (fn x => map (cons x) rec_pick) xs
          end
    (* returns all constant interpretations that have the same tree *)
    (* structure as the interpretation argument                     *)
    fun make_constants_intr (Leaf xs) = unit_vectors (length xs)
      | make_constants_intr (Node xs) = map Node (pick_all (length xs)
          (make_constants_intr (hd xs)))
    (* obtain the interpretation for a variable of type 'T' *)
    val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1,
      bounds=[], wellformed=True} (Free ("dummy", T))
  in
    make_constants_intr i
  end;

(* ------------------------------------------------------------------------- *)
(* size_of_type: returns the number of elements in a type 'T' (i.e. 'length  *)
(*               (make_constants T)', but implemented more efficiently)      *)
(* ------------------------------------------------------------------------- *)

(* returns 0 for an empty ground type or a function type with empty      *)
(* codomain, but fails for a function type with empty domain --          *)
(* admissibility of datatype constructor argument types (see "Inductive  *)
(* datatypes in HOL - lessons learned ...", S. Berghofer, M. Wenzel,     *)
(* TPHOLs 99) ensures that recursive, possibly empty, datatype fragments *)
(* never occur as the domain of a function type that is the type of a    *)
(* constructor argument                                                  *)

fun size_of_type ctxt model T =
  let
    (* returns the number of elements that have the same tree structure as a *)
    (* given interpretation                                                  *)
    fun size_of_intr (Leaf xs) = length xs
      | size_of_intr (Node xs) = Integer.pow (length xs) (size_of_intr (hd xs))
    (* obtain the interpretation for a variable of type 'T' *)
    val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1,
      bounds=[], wellformed=True} (Free ("dummy", T))
  in
    size_of_intr i
  end;

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

val TT = Leaf [TrueFalse];

val FF = Leaf [FalseTrue];

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

fun make_equality (i1, i2) =
  let
    fun equal (i1, i2) =
      (case i1 of
        Leaf xs =>
          (case i2 of
            Leaf ys => Prop_Logic.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 => Prop_Logic.all (map equal (xs ~~ ys))))
    fun not_equal (i1, i2) =
      (case i1 of
        Leaf xs =>
          (case i2 of
            (* defined and not equal *)
            Leaf ys => Prop_Logic.all ((Prop_Logic.exists xs)
            :: (Prop_Logic.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 => Prop_Logic.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.                                           *)
(* ------------------------------------------------------------------------- *)

fun make_def_equality (i1, i2) =
  let
    fun equal (i1, i2) =
      (case i1 of
        Leaf xs =>
          (case i2 of
            (* defined and equal, or both undefined *)
            Leaf ys => SOr (Prop_Logic.dot_product (xs, ys),
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff