# HG changeset patch # User blanchet # Date 1351679001 -3600 # Node ID 5b4b0e4e5205a382bb0ea2a63935d5cdfb673048 # Parent 9f655a6bffd8d63fced3323b17d43d6c604b61b2 moved Refute to "HOL/Library" to speed up building "Main" even more diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/Library/Refute.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Refute.thy Wed Oct 31 11:23:21 2012 +0100 @@ -0,0 +1,113 @@ +(* Title: HOL/Refute.thy + Author: Tjark Weber + Copyright 2003-2007 + +Basic setup and documentation for the 'refute' (and 'refute_params') command. +*) + +header {* Refute *} + +theory Refute +imports Hilbert_Choice List Sledgehammer +keywords "refute" :: diag and "refute_params" :: thy_decl +begin + +ML_file "refute.ML" +setup Refute.setup + +refute_params + [itself = 1, + minsize = 1, + maxsize = 8, + maxvars = 10000, + maxtime = 60, + satsolver = auto, + no_assms = false] + +text {* +\small +\begin{verbatim} +(* ------------------------------------------------------------------------- *) +(* REFUTE *) +(* *) +(* We use a SAT solver to search for a (finite) model that refutes a given *) +(* HOL formula. *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* NOTE *) +(* *) +(* I strongly recommend that you install a stand-alone SAT solver if you *) +(* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. If you *) +(* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME' *) +(* in 'etc/settings'. *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* USAGE *) +(* *) +(* See the file 'HOL/ex/Refute_Examples.thy' for examples. The supported *) +(* parameters are explained below. *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* CURRENT LIMITATIONS *) +(* *) +(* 'refute' currently accepts formulas of higher-order predicate logic (with *) +(* equality), including free/bound/schematic variables, lambda abstractions, *) +(* sets and set membership, "arbitrary", "The", "Eps", records and *) +(* inductively defined sets. Constants are unfolded automatically, and sort *) +(* axioms are added as well. Other, user-asserted axioms however are *) +(* ignored. Inductive datatypes and recursive functions are supported, but *) +(* may lead to spurious countermodels. *) +(* *) +(* The (space) complexity of the algorithm is non-elementary. *) +(* *) +(* Schematic type variables are not supported. *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* PARAMETERS *) +(* *) +(* The following global parameters are currently supported (and required, *) +(* except for "expect"): *) +(* *) +(* Name Type Description *) +(* *) +(* "minsize" int Only search for models with size at least *) +(* 'minsize'. *) +(* "maxsize" int If >0, only search for models with size at most *) +(* 'maxsize'. *) +(* "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. *) +(* This value is ignored under some ML compilers. *) +(* "satsolver" string Name of the 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"). *) +(* *) +(* The size of particular types can be specified in the form type=size *) +(* (where 'type' is a string, and 'size' is an int). Examples: *) +(* "'a"=1 *) +(* "List.list"=2 *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* FILES *) +(* *) +(* HOL/Tools/prop_logic.ML Propositional logic *) +(* HOL/Tools/sat_solver.ML SAT solvers *) +(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *) +(* Boolean assignment -> HOL model *) +(* HOL/Refute.thy This file: loads the ML files, basic setup, *) +(* documentation *) +(* HOL/SAT.thy Sets default parameters *) +(* HOL/ex/Refute_Examples.thy Examples *) +(* ------------------------------------------------------------------------- *) +\end{verbatim} +*} + +end diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/Library/refute.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/refute.ML Wed Oct 31 11:23:21 2012 +0100 @@ -0,0 +1,3229 @@ +(* 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 -> (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 * string) list + val actual_params : Proof.context -> (string * string) list -> 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 * string) list -> term list -> term -> string + (* tries to find a model that refutes a formula: *) + val refute_term : + Proof.context -> (string * string) list -> term list -> term -> string + val refute_goal : + Proof.context -> (string * string) list -> thm -> int -> string + + val setup : theory -> theory + +(* ------------------------------------------------------------------------- *) +(* 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; + +(* ('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 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 + (* (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 ctxt + (* 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 *) +(* ------------------------------------------------------------------------- *) + +val typ_of_dtyp = ATP_Util.typ_of_dtyp + +(* ------------------------------------------------------------------------- *) +(* close_form: universal closure over schematic variables in 't' *) +(* ------------------------------------------------------------------------- *) + +(* Term.term -> Term.term *) + +fun close_form t = + let + val vars = sort_wrt (fst o fst) (Term.add_vars t []) + in + fold (fn ((x, i), T) => fn t' => + Logic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t + end; + +val monomorphic_term = ATP_Util.monomorphic_term +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 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' *) +(* ------------------------------------------------------------------------- *) + +fun is_IDT_recursor thy (s, _) = + 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 *) +(* ------------------------------------------------------------------------- *) + +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" *) +(* ------------------------------------------------------------------------- *) + +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 (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 *) +(* ------------------------------------------------------------------------- *) + +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 + (* 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'. *) + +(* 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 ctxt t = + let + val thy = Proof_Context.theory_of ctxt + 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 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, monomorphic_term (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 ("prop", []) => axs + | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs) + | Type (@{type_name set}, [T1]) => 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 _ => (* 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 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; + +(* ------------------------------------------------------------------------- *) +(* 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 ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc) + | Type ("prop", []) => acc + | Type (@{type_name set}, [T1]) => collect_types T1 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.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 + Datatype.DtTFree _ => + collect_types dT acc + | Datatype.DtType (_, ds) => + collect_types dT (fold_rev collect_dtyp ds acc) + | Datatype.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.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 = + case AList.lookup (op =) sizes (string_of_typ T) of + SOME n => n + | NONE => minsize + in + map (fn T => (T, size_of_typ T)) xs + end; + +(* ------------------------------------------------------------------------- *) +(* next_universe: enumerates all universes (i.e. assignments of sizes to *) +(* types), where the minimal size of a type is given by *) +(* 'minsize', the maximal size is given by 'maxsize', and a *) +(* type may have a fixed size given in 'sizes' *) +(* ------------------------------------------------------------------------- *) + +(* (Term.typ * int) list -> (string * int) list -> int -> int -> + (Term.typ * int) list option *) + +fun next_universe xs sizes minsize maxsize = + let + (* creates the "first" list of length 'len', where the sum of all list *) + (* elements is 'sum', and the length of the list is 'len' *) + (* int -> int -> int -> int list option *) + fun make_first _ 0 sum = + if sum = 0 then + SOME [] + else + NONE + | make_first max len sum = + if sum <= max orelse max < 0 then + Option.map (fn xs' => sum :: xs') (make_first max (len-1) 0) + else + Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max)) + (* enumerates all int lists with a fixed length, where 0<=x<='max' for *) + (* all list elements x (unless 'max'<0) *) + (* int -> int -> int -> int list -> int list option *) + fun next _ _ _ [] = + 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 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" *) +(* ------------------------------------------------------------------------- *) + +(* interpretation -> prop_formula *) + +fun toTrue (Leaf [fm, _]) = fm + | toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value"); + +(* ------------------------------------------------------------------------- *) +(* toFalse: converts the interpretation of a Boolean value to a *) +(* propositional formula that is true iff the interpretation *) +(* denotes "false" *) +(* ------------------------------------------------------------------------- *) + +(* interpretation -> prop_formula *) + +fun toFalse (Leaf [_, fm]) = fm + | toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value"); + +(* ------------------------------------------------------------------------- *) +(* find_model: repeatedly calls 'interpret' with appropriate parameters, *) +(* applies a SAT solver, and (in case a model is found) displays *) +(* the model to the user by calling 'print_model' *) +(* {...} : 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 + (* string -> string *) + fun check_expect outcome_code = + if expect = "" orelse outcome_code = expect then outcome_code + else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") + (* unit -> string *) + 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 + (* Term.typ list *) + 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 Datatype.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 Datatype_Aux.is_rec_type ds) constrs + end + | NONE => false) + | _ => false) types + val _ = + if maybe_spurious then + warning ("Term contains a recursive datatype; " + ^ "countermodel(s) may be spurious!") + else + () + (* (Term.typ * int) list -> string *) + fun find_model_loop universe = + let + val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer) + val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime + orelse raise TimeLimit.TimeOut + 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 satsolver = "dpll" orelse satsolver = "enumerate" then + warning ("Using SAT solver " ^ quote satsolver ^ + "; for better performance, consider installing an \ + \external solver.") + else ()); + val solver = + SatSolver.invoke_solver satsolver + handle Option.Option => + error ("Unknown SAT solver: " ^ quote satsolver ^ + ". Available solvers: " ^ + commas (map (quote o fst) (!SatSolver.solvers)) ^ ".") + in + Output.urgent_message "Invoking SAT solver..."; + (case solver fm of + SatSolver.SATISFIABLE assignment => + (Output.urgent_message ("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") + | SatSolver.UNSATISFIABLE _ => + (Output.urgent_message "No model exists."; + case next_universe universe sizes minsize maxsize of + SOME universe' => find_model_loop universe' + | NONE => (Output.urgent_message + "Search terminated, no larger universe within the given limits."; + "none")) + | SatSolver.UNKNOWN => + (Output.urgent_message "No model found."; + case next_universe universe sizes minsize maxsize of + SOME universe' => find_model_loop universe' + | NONE => (Output.urgent_message + "Search terminated, no larger universe within the given limits."; + "unknown"))) handle SatSolver.NOT_CONFIGURED => + (error ("SAT solver " ^ quote satsolver ^ " is not configured."); + "unknown") + end + handle MAXVARS_EXCEEDED => + (Output.urgent_message ("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 *) + Output.urgent_message ("Trying to find a model that " + ^ (if negate then "refutes" else "satisfies") ^ ": " + ^ Syntax.string_of_term ctxt t); + if maxtime > 0 then ( + TimeLimit.timeLimit (Time.fromSeconds maxtime) + wrapper () + handle TimeLimit.TimeOut => + (Output.urgent_message ("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_wrt (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 all}, _) $ Abs (_, _, t)) = + strip_all_body t + | strip_all_body (Const (@{const_name Trueprop}, _) $ t) = + strip_all_body t + | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) = + strip_all_body t + | strip_all_body t = t + (* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *) + fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) = + (a, T) :: strip_all_vars t + | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) = + strip_all_vars t + | strip_all_vars (Const (@{const_name All}, _) $ 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 |> prop_of + in + if Logic.count_prems t = 0 then + (Output.urgent_message "No subgoal!"; "none") + else + let + val assms = map 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 *) + (* int -> interpretation list *) + fun unit_vectors n = + let + (* returns the k-th unit vector of length n *) + (* int * int -> interpretation *) + fun unit_vector (k, n) = + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) + (* int -> interpretation list *) + 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' *) + (* int -> 'a list -> 'a list list *) + fun pick_all 1 xs = map single xs + | pick_all n xs = + let val rec_pick = pick_all (n - 1) xs in + maps (fn x => map (cons x) rec_pick) xs + end + (* returns all constant interpretations that have the same tree *) + (* structure as the interpretation argument *) + (* interpretation -> interpretation list *) + 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 *) +(* ------------------------------------------------------------------------- *) + +(* interpretation *) + +val TT = Leaf [True, False]; + +val FF = Leaf [False, True]; + +(* ------------------------------------------------------------------------- *) +(* make_equality: returns an interpretation that denotes (extensional) *) +(* equality of two interpretations *) +(* - two interpretations are 'equal' iff they are both defined and denote *) +(* the same value *) +(* - two interpretations are 'not_equal' iff they are both defined at least *) +(* partially, and a defined part denotes different values *) +(* - a completely undefined interpretation is neither 'equal' nor *) +(* 'not_equal' to another interpretation *) +(* ------------------------------------------------------------------------- *) + +(* We could in principle represent '=' on a type T by a particular *) +(* interpretation. However, the size of that interpretation is quadratic *) +(* in the size of T. Therefore comparing the interpretations 'i1' and *) +(* 'i2' directly is more efficient than constructing the interpretation *) +(* for equality on T first, and "applying" this interpretation to 'i1' *) +(* and 'i2' in the usual way (cf. 'interpretation_apply') then. *) + +(* interpretation * interpretation -> interpretation *) + +fun make_equality (i1, i2) = + let + (* interpretation * interpretation -> prop_formula *) + fun equal (i1, i2) = + (case i1 of + Leaf xs => + (case i2 of + Leaf ys => 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)))) + (* interpretation * interpretation -> prop_formula *) + 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. *) +(* ------------------------------------------------------------------------- *) + +(* interpretation * interpretation -> interpretation *) + +fun make_def_equality (i1, i2) = + let + (* interpretation * interpretation -> prop_formula *) + fun equal (i1, i2) = + (case i1 of + Leaf xs => + (case i2 of + (* defined and equal, or both undefined *) + Leaf ys => SOr (Prop_Logic.dot_product (xs, ys), + SAnd (Prop_Logic.all (map SNot xs), Prop_Logic.all (map SNot ys))) + | Node _ => raise REFUTE ("make_def_equality", + "second interpretation is higher")) + | Node xs => + (case i2 of + Leaf _ => raise REFUTE ("make_def_equality", + "first interpretation is higher") + | Node ys => Prop_Logic.all (map equal (xs ~~ ys)))) + (* interpretation *) + val eq = equal (i1, i2) + in + Leaf [eq, SNot eq] + end; + +(* ------------------------------------------------------------------------- *) +(* interpretation_apply: returns an interpretation that denotes the result *) +(* of applying the function denoted by 'i1' to the *) +(* argument denoted by 'i2' *) +(* ------------------------------------------------------------------------- *) + +(* interpretation * interpretation -> interpretation *) + +fun interpretation_apply (i1, i2) = + let + (* interpretation * interpretation -> interpretation *) + fun interpretation_disjunction (tr1,tr2) = + tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) + (tree_pair (tr1,tr2)) + (* prop_formula * interpretation -> interpretation *) + fun prop_formula_times_interpretation (fm,tr) = + tree_map (map (fn x => SAnd (fm,x))) tr + (* prop_formula list * interpretation list -> interpretation *) + fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) = + prop_formula_times_interpretation (fm,tr) + | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) = + interpretation_disjunction (prop_formula_times_interpretation (fm,tr), + prop_formula_list_dot_product_interpretation_list (fms,trees)) + | prop_formula_list_dot_product_interpretation_list (_,_) = + raise REFUTE ("interpretation_apply", "empty list (in dot product)") + (* returns a list of lists, each one consisting of one element from each *) + (* element of 'xss' *) + (* 'a list list -> 'a list list *) + fun pick_all [xs] = map single xs + | pick_all (xs::xss) = + let val rec_pick = pick_all xss in + maps (fn x => map (cons x) rec_pick) xs + end + | pick_all _ = raise REFUTE ("interpretation_apply", "empty list (in pick_all)") + (* interpretation -> prop_formula list *) + fun interpretation_to_prop_formula_list (Leaf xs) = xs + | interpretation_to_prop_formula_list (Node trees) = + map Prop_Logic.all (pick_all + (map interpretation_to_prop_formula_list trees)) + in + case i1 of + Leaf _ => + raise REFUTE ("interpretation_apply", "first interpretation is a leaf") + | Node xs => + prop_formula_list_dot_product_interpretation_list + (interpretation_to_prop_formula_list i2, xs) + end; + +(* ------------------------------------------------------------------------- *) +(* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions *) +(* ------------------------------------------------------------------------- *) + +(* Term.term -> int -> Term.term *) + +fun eta_expand t i = + let + val Ts = Term.binder_types (Term.fastype_of t) + val t' = Term.incr_boundvars i t + in + fold_rev (fn T => fn term => Abs ("", T, term)) + (List.take (Ts, i)) + (Term.list_comb (t', map Bound (i-1 downto 0))) + end; + +(* ------------------------------------------------------------------------- *) +(* size_of_dtyp: the size of (an initial fragment of) an inductive data type *) +(* is the sum (over its constructors) of the product (over *) +(* their arguments) of the size of the argument types *) +(* ------------------------------------------------------------------------- *) + +fun size_of_dtyp ctxt typ_sizes descr typ_assoc constructors = + Integer.sum (map (fn (_, dtyps) => + Integer.prod (map (size_of_type ctxt (typ_sizes, []) o + (typ_of_dtyp descr typ_assoc)) dtyps)) + constructors); + + +(* ------------------------------------------------------------------------- *) +(* INTERPRETERS: Actual Interpreters *) +(* ------------------------------------------------------------------------- *) + +(* simply typed lambda calculus: Isabelle's basic term syntax, with type *) +(* variables, function types, and propT *) + +fun stlc_interpreter ctxt model args t = + let + val (typs, terms) = model + val {maxvars, def_eq, next_idx, bounds, wellformed} = args + (* Term.typ -> (interpretation * model * arguments) option *) + fun interpret_groundterm T = + let + (* unit -> (interpretation * model * arguments) option *) + fun interpret_groundtype () = + let + (* the model must specify a size for ground types *) + val size = + if T = Term.propT then 2 + else the (AList.lookup (op =) typs T) + val next = next_idx + size + (* check if 'maxvars' is large enough *) + val _ = (if next - 1 > maxvars andalso maxvars > 0 then + raise MAXVARS_EXCEEDED else ()) + (* prop_formula list *) + val fms = map BoolVar (next_idx upto (next_idx + size - 1)) + (* interpretation *) + val intr = Leaf fms + (* prop_formula list -> prop_formula *) + fun one_of_two_false [] = True + | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' => + SOr (SNot x, SNot x')) xs), one_of_two_false xs) + (* prop_formula *) + val wf = one_of_two_false fms + in + (* extend the model, increase 'next_idx', add well-formedness *) + (* condition *) + SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, + def_eq = def_eq, next_idx = next, bounds = bounds, + wellformed = SAnd (wellformed, wf)}) + end + in + case T of + Type ("fun", [T1, T2]) => + let + (* we create 'size_of_type ... T1' different copies of the *) + (* interpretation for 'T2', which are then combined into a single *) + (* new interpretation *) + (* make fresh copies, with different variable indices *) + (* 'idx': next variable index *) + (* 'n' : number of copies *) + (* int -> int -> (int * interpretation list * prop_formula *) + fun make_copies idx 0 = (idx, [], True) + | make_copies idx n = + let + val (copy, _, new_args) = interpret ctxt (typs, []) + {maxvars = maxvars, def_eq = false, next_idx = idx, + bounds = [], wellformed = True} (Free ("dummy", T2)) + val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1) + in + (idx', copy :: copies, SAnd (#wellformed new_args, wf')) + end + val (next, copies, wf) = make_copies next_idx + (size_of_type ctxt model T1) + (* combine copies into a single interpretation *) + val intr = Node copies + in + (* extend the model, increase 'next_idx', add well-formedness *) + (* condition *) + SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, + def_eq = def_eq, next_idx = next, bounds = bounds, + wellformed = SAnd (wellformed, wf)}) + end + | Type _ => interpret_groundtype () + | TFree _ => interpret_groundtype () + | TVar _ => interpret_groundtype () + end + in + case AList.lookup (op =) terms t of + SOME intr => + (* return an existing interpretation *) + SOME (intr, model, args) + | NONE => + (case t of + Const (_, T) => interpret_groundterm T + | Free (_, T) => interpret_groundterm T + | Var (_, T) => interpret_groundterm T + | Bound i => SOME (nth (#bounds args) i, model, args) + | Abs (_, T, body) => + let + (* create all constants of type 'T' *) + val constants = make_constants ctxt model T + (* interpret the 'body' separately for each constant *) + val (bodies, (model', args')) = fold_map + (fn c => fn (m, a) => + let + (* add 'c' to 'bounds' *) + val (i', m', a') = interpret ctxt m {maxvars = #maxvars a, + def_eq = #def_eq a, next_idx = #next_idx a, + bounds = (c :: #bounds a), wellformed = #wellformed a} body + in + (* keep the new model m' and 'next_idx' and 'wellformed', *) + (* but use old 'bounds' *) + (i', (m', {maxvars = maxvars, def_eq = def_eq, + next_idx = #next_idx a', bounds = bounds, + wellformed = #wellformed a'})) + end) + constants (model, args) + in + SOME (Node bodies, model', args') + end + | t1 $ t2 => + let + (* interpret 't1' and 't2' separately *) + val (intr1, model1, args1) = interpret ctxt model args t1 + val (intr2, model2, args2) = interpret ctxt model1 args1 t2 + in + SOME (interpretation_apply (intr1, intr2), model2, args2) + end) + end; + +fun Pure_interpreter ctxt model args t = + case t of + Const (@{const_name all}, _) $ t1 => + let + val (i, m, a) = interpret ctxt model args t1 + in + case i of + Node xs => + (* 3-valued logic *) + let + val fmTrue = Prop_Logic.all (map toTrue xs) + val fmFalse = Prop_Logic.exists (map toFalse xs) + in + SOME (Leaf [fmTrue, fmFalse], m, a) + end + | _ => + raise REFUTE ("Pure_interpreter", + "\"all\" is followed by a non-function") + end + | Const (@{const_name all}, _) => + SOME (interpret ctxt model args (eta_expand t 1)) + | Const (@{const_name "=="}, _) $ t1 $ t2 => + let + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 + in + (* we use either 'make_def_equality' or 'make_equality' *) + SOME ((if #def_eq args then make_def_equality else make_equality) + (i1, i2), m2, a2) + end + | Const (@{const_name "=="}, _) $ _ => + SOME (interpret ctxt model args (eta_expand t 1)) + | Const (@{const_name "=="}, _) => + SOME (interpret ctxt model args (eta_expand t 2)) + | Const (@{const_name "==>"}, _) $ t1 $ t2 => + (* 3-valued logic *) + let + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 + val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2) + val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2) + in + SOME (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const (@{const_name "==>"}, _) $ _ => + SOME (interpret ctxt model args (eta_expand t 1)) + | Const (@{const_name "==>"}, _) => + SOME (interpret ctxt model args (eta_expand t 2)) + | _ => NONE; + +fun HOLogic_interpreter ctxt model args t = +(* Providing interpretations directly is more efficient than unfolding the *) +(* logical constants. In HOL however, logical constants can themselves be *) +(* arguments. They are then translated using eta-expansion. *) + case t of + Const (@{const_name Trueprop}, _) => + SOME (Node [TT, FF], model, args) + | Const (@{const_name Not}, _) => + SOME (Node [FF, TT], model, args) + (* redundant, since 'True' is also an IDT constructor *) + | Const (@{const_name True}, _) => + SOME (TT, model, args) + (* redundant, since 'False' is also an IDT constructor *) + | Const (@{const_name False}, _) => + SOME (FF, model, args) + | Const (@{const_name All}, _) $ t1 => (* similar to "all" (Pure) *) + let + val (i, m, a) = interpret ctxt model args t1 + in + case i of + Node xs => + (* 3-valued logic *) + let + val fmTrue = Prop_Logic.all (map toTrue xs) + val fmFalse = Prop_Logic.exists (map toFalse xs) + in + SOME (Leaf [fmTrue, fmFalse], m, a) + end + | _ => + raise REFUTE ("HOLogic_interpreter", + "\"All\" is followed by a non-function") + end + | Const (@{const_name All}, _) => + SOME (interpret ctxt model args (eta_expand t 1)) + | Const (@{const_name Ex}, _) $ t1 => + let + val (i, m, a) = interpret ctxt model args t1 + in + case i of + Node xs => + (* 3-valued logic *) + let + val fmTrue = Prop_Logic.exists (map toTrue xs) + val fmFalse = Prop_Logic.all (map toFalse xs) + in + SOME (Leaf [fmTrue, fmFalse], m, a) + end + | _ => + raise REFUTE ("HOLogic_interpreter", + "\"Ex\" is followed by a non-function") + end + | Const (@{const_name Ex}, _) => + SOME (interpret ctxt model args (eta_expand t 1)) + | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *) + let + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 + in + SOME (make_equality (i1, i2), m2, a2) + end + | Const (@{const_name HOL.eq}, _) $ _ => + SOME (interpret ctxt model args (eta_expand t 1)) + | Const (@{const_name HOL.eq}, _) => + SOME (interpret ctxt model args (eta_expand t 2)) + | Const (@{const_name HOL.conj}, _) $ t1 $ t2 => + (* 3-valued logic *) + let + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 + val fmTrue = Prop_Logic.SAnd (toTrue i1, toTrue i2) + val fmFalse = Prop_Logic.SOr (toFalse i1, toFalse i2) + in + SOME (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const (@{const_name HOL.conj}, _) $ _ => + SOME (interpret ctxt model args (eta_expand t 1)) + | Const (@{const_name HOL.conj}, _) => + SOME (interpret ctxt model args (eta_expand t 2)) + (* this would make "undef" propagate, even for formulae like *) + (* "False & undef": *) + (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *) + | Const (@{const_name HOL.disj}, _) $ t1 $ t2 => + (* 3-valued logic *) + let + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 + val fmTrue = Prop_Logic.SOr (toTrue i1, toTrue i2) + val fmFalse = Prop_Logic.SAnd (toFalse i1, toFalse i2) + in + SOME (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const (@{const_name HOL.disj}, _) $ _ => + SOME (interpret ctxt model args (eta_expand t 1)) + | Const (@{const_name HOL.disj}, _) => + SOME (interpret ctxt model args (eta_expand t 2)) + (* this would make "undef" propagate, even for formulae like *) + (* "True | undef": *) + (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *) + | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *) + (* 3-valued logic *) + let + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 + val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2) + val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2) + in + SOME (Leaf [fmTrue, fmFalse], m2, a2) + end + | Const (@{const_name HOL.implies}, _) $ _ => + SOME (interpret ctxt model args (eta_expand t 1)) + | Const (@{const_name HOL.implies}, _) => + SOME (interpret ctxt model args (eta_expand t 2)) + (* this would make "undef" propagate, even for formulae like *) + (* "False --> undef": *) + (* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *) + | _ => NONE; + +(* interprets variables and constants whose type is an IDT (this is *) +(* relatively easy and merely requires us to compute the size of the IDT); *) +(* constructors of IDTs however are properly interpreted by *) +(* 'IDT_constructor_interpreter' *) + +fun IDT_interpreter ctxt model args t = + let + val thy = Proof_Context.theory_of ctxt + val (typs, terms) = model + (* Term.typ -> (interpretation * model * arguments) option *) + fun interpret_term (Type (s, Ts)) = + (case Datatype.get_info thy s of + SOME info => (* inductive datatype *) + let + (* int option -- only recursive IDTs have an associated depth *) + val depth = AList.lookup (op =) typs (Type (s, Ts)) + (* sanity check: depth must be at least 0 *) + val _ = + (case depth of SOME n => + if n < 0 then + raise REFUTE ("IDT_interpreter", "negative depth") + else () + | _ => ()) + in + (* termination condition to avoid infinite recursion *) + if depth = (SOME 0) then + (* return a leaf of size 0 *) + SOME (Leaf [], model, args) + else + let + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) + val typ_assoc = dtyps ~~ Ts + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = + if Library.exists (fn d => + case d of Datatype.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_interpreter", + "datatype argument (for type " + ^ Syntax.string_of_typ ctxt (Type (s, Ts)) + ^ ") is not a variable") + else () + (* if the model specifies a depth for the current type, *) + (* decrement it to avoid infinite recursion *) + val typs' = case depth of NONE => typs | SOME n => + AList.update (op =) (Type (s, Ts), n-1) typs + (* recursively compute the size of the datatype *) + val size = size_of_dtyp ctxt typs' descr typ_assoc constrs + val next_idx = #next_idx args + val next = next_idx+size + (* check if 'maxvars' is large enough *) + val _ = (if next-1 > #maxvars args andalso + #maxvars args > 0 then raise MAXVARS_EXCEEDED else ()) + (* prop_formula list *) + val fms = map BoolVar (next_idx upto (next_idx+size-1)) + (* interpretation *) + val intr = Leaf fms + (* prop_formula list -> prop_formula *) + fun one_of_two_false [] = True + | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' => + SOr (SNot x, SNot x')) xs), one_of_two_false xs) + (* prop_formula *) + val wf = one_of_two_false fms + in + (* extend the model, increase 'next_idx', add well-formedness *) + (* condition *) + SOME (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, + def_eq = #def_eq args, next_idx = next, bounds = #bounds args, + wellformed = SAnd (#wellformed args, wf)}) + end + end + | NONE => (* not an inductive datatype *) + NONE) + | interpret_term _ = (* a (free or schematic) type variable *) + NONE + in + case AList.lookup (op =) terms t of + SOME intr => + (* return an existing interpretation *) + SOME (intr, model, args) + | NONE => + (case t of + Free (_, T) => interpret_term T + | Var (_, T) => interpret_term T + | Const (_, T) => interpret_term T + | _ => NONE) + end; + +(* This function imposes an order on the elements of a datatype fragment *) +(* as follows: C_i x_1 ... x_n < C_j y_1 ... y_m iff i < j or *) +(* (x_1, ..., x_n) < (y_1, ..., y_m). With this order, a constructor is *) +(* a function C_i that maps some argument indices x_1, ..., x_n to the *) +(* datatype element given by index C_i x_1 ... x_n. The idea remains the *) +(* same for recursive datatypes, although the computation of indices gets *) +(* a little tricky. *) + +fun IDT_constructor_interpreter ctxt model args t = + let + val thy = Proof_Context.theory_of ctxt + (* returns a list of canonical representations for terms of the type 'T' *) + (* It would be nice if we could just use 'print' for this, but 'print' *) + (* for IDTs calls 'IDT_constructor_interpreter' again, and this could *) + (* lead to infinite recursion when we have (mutually) recursive IDTs. *) + (* (Term.typ * int) list -> Term.typ -> Term.term list *) + fun canonical_terms typs T = + (case T of + Type ("fun", [T1, T2]) => + (* 'T2' might contain a recursive IDT, so we cannot use 'print' (at *) + (* least not for 'T2' *) + let + (* returns a list of lists, each one consisting of n (possibly *) + (* identical) elements from 'xs' *) + (* int -> 'a list -> 'a list list *) + fun pick_all 1 xs = map single xs + | pick_all n xs = + let val rec_pick = pick_all (n-1) xs in + maps (fn x => map (cons x) rec_pick) xs + end + (* ["x1", ..., "xn"] *) + val terms1 = canonical_terms typs T1 + (* ["y1", ..., "ym"] *) + val terms2 = canonical_terms typs T2 + (* [[("x1", "y1"), ..., ("xn", "y1")], ..., *) + (* [("x1", "ym"), ..., ("xn", "ym")]] *) + val functions = map (curry (op ~~) terms1) + (pick_all (length terms1) terms2) + (* [["(x1, y1)", ..., "(xn, y1)"], ..., *) + (* ["(x1, ym)", ..., "(xn, ym)"]] *) + val pairss = map (map HOLogic.mk_prod) functions + (* Term.typ *) + val HOLogic_prodT = HOLogic.mk_prodT (T1, T2) + val HOLogic_setT = HOLogic.mk_setT HOLogic_prodT + (* Term.term *) + val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT) + val HOLogic_insert = + Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) + in + (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *) + map (fn ps => fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) ps + HOLogic_empty_set) pairss + end + | Type (s, Ts) => + (case Datatype.get_info thy s of + SOME info => + (case AList.lookup (op =) typs T of + SOME 0 => + (* termination condition to avoid infinite recursion *) + [] (* at depth 0, every IDT is empty *) + | _ => + let + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) + val typ_assoc = dtyps ~~ Ts + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = + if Library.exists (fn d => + case d of Datatype.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_constructor_interpreter", + "datatype argument (for type " + ^ Syntax.string_of_typ ctxt T + ^ ") is not a variable") + else () + (* decrement depth for the IDT 'T' *) + val typs' = + (case AList.lookup (op =) typs T of NONE => typs + | SOME n => AList.update (op =) (T, n-1) typs) + fun constructor_terms terms [] = terms + | constructor_terms terms (d::ds) = + let + val dT = typ_of_dtyp descr typ_assoc d + val d_terms = canonical_terms typs' dT + in + (* C_i x_1 ... x_n < C_i y_1 ... y_n if *) + (* (x_1, ..., x_n) < (y_1, ..., y_n) *) + constructor_terms + (map_product (curry op $) terms d_terms) ds + end + in + (* C_i ... < C_j ... if i < j *) + maps (fn (cname, ctyps) => + let + val cTerm = Const (cname, + map (typ_of_dtyp descr typ_assoc) ctyps ---> T) + in + constructor_terms [cTerm] ctyps + end) constrs + end) + | NONE => + (* not an inductive datatype; in this case the argument types in *) + (* 'Ts' may not be IDTs either, so 'print' should be safe *) + map (fn intr => print ctxt (typs, []) T intr (K false)) + (make_constants ctxt (typs, []) T)) + | _ => (* TFree ..., TVar ... *) + map (fn intr => print ctxt (typs, []) T intr (K false)) + (make_constants ctxt (typs, []) T)) + val (typs, terms) = model + in + case AList.lookup (op =) terms t of + SOME intr => + (* return an existing interpretation *) + SOME (intr, model, args) + | NONE => + (case t of + Const (s, T) => + (case body_type T of + Type (s', Ts') => + (case Datatype.get_info thy s' of + SOME info => (* body type is an inductive datatype *) + let + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) + val typ_assoc = dtyps ~~ Ts' + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = if Library.exists (fn d => + case d of Datatype.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_constructor_interpreter", + "datatype argument (for type " + ^ Syntax.string_of_typ ctxt (Type (s', Ts')) + ^ ") is not a variable") + else () + (* split the constructors into those occuring before/after *) + (* 'Const (s, T)' *) + val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) => + not (cname = s andalso Sign.typ_instance thy (T, + map (typ_of_dtyp descr typ_assoc) ctypes + ---> Type (s', Ts')))) constrs + in + case constrs2 of + [] => + (* 'Const (s, T)' is not a constructor of this datatype *) + NONE + | (_, ctypes)::_ => + let + (* int option -- only /recursive/ IDTs have an associated *) + (* depth *) + val depth = AList.lookup (op =) typs (Type (s', Ts')) + (* this should never happen: at depth 0, this IDT fragment *) + (* is definitely empty, and in this case we don't need to *) + (* interpret its constructors *) + val _ = (case depth of SOME 0 => + raise REFUTE ("IDT_constructor_interpreter", + "depth is 0") + | _ => ()) + val typs' = (case depth of NONE => typs | SOME n => + AList.update (op =) (Type (s', Ts'), n-1) typs) + (* elements of the datatype come before elements generated *) + (* by 'Const (s, T)' iff they are generated by a *) + (* constructor in constrs1 *) + val offset = size_of_dtyp ctxt typs' descr typ_assoc constrs1 + (* compute the total (current) size of the datatype *) + val total = offset + + size_of_dtyp ctxt typs' descr typ_assoc constrs2 + (* sanity check *) + val _ = if total <> size_of_type ctxt (typs, []) + (Type (s', Ts')) then + raise REFUTE ("IDT_constructor_interpreter", + "total is not equal to current size") + else () + (* returns an interpretation where everything is mapped to *) + (* an "undefined" element of the datatype *) + fun make_undef [] = Leaf (replicate total False) + | make_undef (d::ds) = + let + (* compute the current size of the type 'd' *) + val dT = typ_of_dtyp descr typ_assoc d + val size = size_of_type ctxt (typs, []) dT + in + Node (replicate size (make_undef ds)) + end + (* returns the interpretation for a constructor *) + fun make_constr [] offset = + if offset < total then + (Leaf (replicate offset False @ True :: + (replicate (total - offset - 1) False)), offset + 1) + else + raise REFUTE ("IDT_constructor_interpreter", + "offset >= total") + | make_constr (d::ds) offset = + let + (* Term.typ *) + val dT = typ_of_dtyp descr typ_assoc d + (* compute canonical term representations for all *) + (* elements of the type 'd' (with the reduced depth *) + (* for the IDT) *) + val terms' = canonical_terms typs' dT + (* sanity check *) + val _ = + if length terms' <> size_of_type ctxt (typs', []) dT + then + raise REFUTE ("IDT_constructor_interpreter", + "length of terms' is not equal to old size") + else () + (* compute canonical term representations for all *) + (* elements of the type 'd' (with the current depth *) + (* for the IDT) *) + val terms = canonical_terms typs dT + (* sanity check *) + val _ = + if length terms <> size_of_type ctxt (typs, []) dT + then + raise REFUTE ("IDT_constructor_interpreter", + "length of terms is not equal to current size") + else () + (* sanity check *) + val _ = + if length terms < length terms' then + raise REFUTE ("IDT_constructor_interpreter", + "current size is less than old size") + else () + (* sanity check: every element of terms' must also be *) + (* present in terms *) + val _ = + if forall (member (op =) terms) terms' then () + else + raise REFUTE ("IDT_constructor_interpreter", + "element has disappeared") + (* sanity check: the order on elements of terms' is *) + (* the same in terms, for those elements *) + val _ = + let + fun search (x::xs) (y::ys) = + if x = y then search xs ys else search (x::xs) ys + | search (_::_) [] = + raise REFUTE ("IDT_constructor_interpreter", + "element order not preserved") + | search [] _ = () + in search terms' terms end + (* int * interpretation list *) + val (intrs, new_offset) = + fold_map (fn t_elem => fn off => + (* if 't_elem' existed at the previous depth, *) + (* proceed recursively, otherwise map the entire *) + (* subtree to "undefined" *) + if member (op =) terms' t_elem then + make_constr ds off + else + (make_undef ds, off)) + terms offset + in + (Node intrs, new_offset) + end + in + SOME (fst (make_constr ctypes offset), model, args) + end + end + | NONE => (* body type is not an inductive datatype *) + NONE) + | _ => (* body type is a (free or schematic) type variable *) + NONE) + | _ => (* term is not a constant *) + NONE) + end; + +(* Difficult code ahead. Make sure you understand the *) +(* 'IDT_constructor_interpreter' and the order in which it enumerates *) +(* elements of an IDT before you try to understand this function. *) + +fun IDT_recursion_interpreter ctxt model args t = + let + val thy = Proof_Context.theory_of ctxt + in + (* careful: here we descend arbitrarily deep into 't', possibly before *) + (* any other interpreter for atomic terms has had a chance to look at *) + (* 't' *) + case strip_comb t of + (Const (s, T), params) => + (* iterate over all datatypes in 'thy' *) + Symtab.fold (fn (_, info) => fn result => + case result of + SOME _ => + result (* just keep 'result' *) + | NONE => + if member (op =) (#rec_names info) s then + (* we do have a recursion operator of one of the (mutually *) + (* recursive) datatypes given by 'info' *) + let + (* number of all constructors, including those of different *) + (* (mutually recursive) datatypes within the same descriptor *) + val mconstrs_count = + Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info)) + in + if mconstrs_count < length params then + (* too many actual parameters; for now we'll use the *) + (* 'stlc_interpreter' to strip off one application *) + NONE + else if mconstrs_count > length params then + (* too few actual parameters; we use eta expansion *) + (* Note that the resulting expansion of lambda abstractions *) + (* by the 'stlc_interpreter' may be rather slow (depending *) + (* on the argument types and the size of the IDT, of *) + (* course). *) + SOME (interpret ctxt model args (eta_expand t + (mconstrs_count - length params))) + else (* mconstrs_count = length params *) + let + (* interpret each parameter separately *) + val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) => + let + val (i, m', a') = interpret ctxt m a p + in + (i, (m', a')) + end) params (model, args) + val (typs, _) = model' + (* 'index' is /not/ necessarily the index of the IDT that *) + (* the recursion operator is associated with, but merely *) + (* the index of some mutually recursive IDT *) + val index = #index info + val descr = #descr info + val (_, dtyps, _) = the (AList.lookup (op =) descr index) + (* sanity check: we assume that the order of constructors *) + (* in 'descr' is the same as the order of *) + (* corresponding parameters, otherwise the *) + (* association code below won't match the *) + (* right constructors/parameters; we also *) + (* assume that the order of recursion *) + (* operators in '#rec_names info' is the *) + (* same as the order of corresponding *) + (* datatypes in 'descr' *) + val _ = if map fst descr <> (0 upto (length descr - 1)) then + raise REFUTE ("IDT_recursion_interpreter", + "order of constructors and corresponding parameters/" ^ + "recursion operators and corresponding datatypes " ^ + "different?") + else () + (* sanity check: every element in 'dtyps' must be a *) + (* 'DtTFree' *) + val _ = + if Library.exists (fn d => + case d of Datatype.DtTFree _ => false + | _ => true) dtyps + then + raise REFUTE ("IDT_recursion_interpreter", + "datatype argument is not a variable") + else () + (* the type of a recursion operator is *) + (* [T1, ..., Tn, IDT] ---> Tresult *) + val IDT = nth (binder_types T) mconstrs_count + (* by our assumption on the order of recursion operators *) + (* and datatypes, this is the index of the datatype *) + (* corresponding to the given recursion operator *) + val idt_index = find_index (fn s' => s' = s) (#rec_names info) + (* mutually recursive types must have the same type *) + (* parameters, unless the mutual recursion comes from *) + (* indirect recursion *) + fun rec_typ_assoc acc [] = acc + | rec_typ_assoc acc ((d, T)::xs) = + (case AList.lookup op= acc d of + NONE => + (case d of + Datatype.DtTFree _ => + (* add the association, proceed *) + rec_typ_assoc ((d, T)::acc) xs + | Datatype.DtType (s, ds) => + let + val (s', Ts) = dest_Type T + in + if s=s' then + rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) + else + raise REFUTE ("IDT_recursion_interpreter", + "DtType/Type mismatch") + end + | Datatype.DtRec i => + let + val (_, ds, _) = the (AList.lookup (op =) descr i) + val (_, Ts) = dest_Type T + in + rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) + end) + | SOME T' => + if T=T' then + (* ignore the association since it's already *) + (* present, proceed *) + rec_typ_assoc acc xs + else + raise REFUTE ("IDT_recursion_interpreter", + "different type associations for the same dtyp")) + val typ_assoc = filter + (fn (Datatype.DtTFree _, _) => true | (_, _) => false) + (rec_typ_assoc [] + (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT)) + (* sanity check: typ_assoc must associate types to the *) + (* elements of 'dtyps' (and only to those) *) + val _ = + if not (eq_set (op =) (dtyps, map fst typ_assoc)) + then + raise REFUTE ("IDT_recursion_interpreter", + "type association has extra/missing elements") + else () + (* interpret each constructor in the descriptor (including *) + (* those of mutually recursive datatypes) *) + (* (int * interpretation list) list *) + val mc_intrs = map (fn (idx, (_, _, cs)) => + let + val c_return_typ = typ_of_dtyp descr typ_assoc + (Datatype.DtRec idx) + in + (idx, map (fn (cname, cargs) => + (#1 o interpret ctxt (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], + wellformed=True}) (Const (cname, map (typ_of_dtyp + descr typ_assoc) cargs ---> c_return_typ))) cs) + end) descr + (* associate constructors with corresponding parameters *) + (* (int * (interpretation * interpretation) list) list *) + val (mc_p_intrs, p_intrs') = fold_map + (fn (idx, c_intrs) => fn p_intrs' => + let + val len = length c_intrs + in + ((idx, c_intrs ~~ List.take (p_intrs', len)), + List.drop (p_intrs', len)) + end) mc_intrs p_intrs + (* sanity check: no 'p_intr' may be left afterwards *) + val _ = + if p_intrs' <> [] then + raise REFUTE ("IDT_recursion_interpreter", + "more parameter than constructor interpretations") + else () + (* The recursion operator, applied to 'mconstrs_count' *) + (* arguments, is a function that maps every element of the *) + (* inductive datatype to an element of some result type. *) + (* Recursion operators for mutually recursive IDTs are *) + (* translated simultaneously. *) + (* Since the order on datatype elements is given by an *) + (* order on constructors (and then by the order on *) + (* argument tuples), we can simply copy corresponding *) + (* subtrees from 'p_intrs', in the order in which they are *) + (* given. *) + (* interpretation * interpretation -> interpretation list *) + fun ci_pi (Leaf xs, pi) = + (* if the constructor does not match the arguments to a *) + (* defined element of the IDT, the corresponding value *) + (* of the parameter must be ignored *) + if List.exists (equal True) xs then [pi] else [] + | ci_pi (Node xs, Node ys) = maps ci_pi (xs ~~ ys) + | ci_pi (Node _, Leaf _) = + raise REFUTE ("IDT_recursion_interpreter", + "constructor takes more arguments than the " ^ + "associated parameter") + (* (int * interpretation list) list *) + val rec_operators = map (fn (idx, c_p_intrs) => + (idx, maps ci_pi c_p_intrs)) mc_p_intrs + (* sanity check: every recursion operator must provide as *) + (* many values as the corresponding datatype *) + (* has elements *) + val _ = map (fn (idx, intrs) => + let + val T = typ_of_dtyp descr typ_assoc + (Datatype.DtRec idx) + in + if length intrs <> size_of_type ctxt (typs, []) T then + raise REFUTE ("IDT_recursion_interpreter", + "wrong number of interpretations for rec. operator") + else () + end) rec_operators + (* For non-recursive datatypes, we are pretty much done at *) + (* this point. For recursive datatypes however, we still *) + (* need to apply the interpretations in 'rec_operators' to *) + (* (recursively obtained) interpretations for recursive *) + (* constructor arguments. To do so more efficiently, we *) + (* copy 'rec_operators' into arrays first. Each Boolean *) + (* indicates whether the recursive arguments have been *) + (* considered already. *) + (* (int * (bool * interpretation) Array.array) list *) + val REC_OPERATORS = map (fn (idx, intrs) => + (idx, Array.fromList (map (pair false) intrs))) + rec_operators + (* takes an interpretation, and if some leaf of this *) + (* interpretation is the 'elem'-th element of the type, *) + (* the indices of the arguments leading to this leaf are *) + (* returned *) + (* interpretation -> int -> int list option *) + fun get_args (Leaf xs) elem = + if find_index (fn x => x = True) xs = elem then + SOME [] + else + NONE + | get_args (Node xs) elem = + let + (* interpretation list * int -> int list option *) + fun search ([], _) = + NONE + | search (x::xs, n) = + (case get_args x elem of + SOME result => SOME (n::result) + | NONE => search (xs, n+1)) + in + search (xs, 0) + end + (* returns the index of the constructor and indices for *) + (* its arguments that generate the 'elem'-th element of *) + (* the datatype given by 'idx' *) + (* int -> int -> int * int list *) + fun get_cargs idx elem = + let + (* int * interpretation list -> int * int list *) + fun get_cargs_rec (_, []) = + raise REFUTE ("IDT_recursion_interpreter", + "no matching constructor found for datatype element") + | get_cargs_rec (n, x::xs) = + (case get_args x elem of + SOME args => (n, args) + | NONE => get_cargs_rec (n+1, xs)) + in + get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx)) + end + (* computes one entry in 'REC_OPERATORS', and recursively *) + (* all entries needed for it, where 'idx' gives the *) + (* datatype and 'elem' the element of it *) + (* int -> int -> interpretation *) + fun compute_array_entry idx elem = + let + val arr = the (AList.lookup (op =) REC_OPERATORS idx) + val (flag, intr) = Array.sub (arr, elem) + in + if flag then + (* simply return the previously computed result *) + intr + else + (* we have to apply 'intr' to interpretations for all *) + (* recursive arguments *) + let + (* int * int list *) + val (c, args) = get_cargs idx elem + (* find the indices of the constructor's /recursive/ *) + (* arguments *) + val (_, _, constrs) = the (AList.lookup (op =) descr idx) + val (_, dtyps) = nth constrs c + val rec_dtyps_args = filter + (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args) + (* map those indices to interpretations *) + val rec_dtyps_intrs = map (fn (dtyp, arg) => + let + val dT = typ_of_dtyp descr typ_assoc dtyp + val consts = make_constants ctxt (typs, []) dT + val arg_i = nth consts arg + in + (dtyp, arg_i) + end) rec_dtyps_args + (* takes the dtyp and interpretation of an element, *) + (* and computes the interpretation for the *) + (* corresponding recursive argument *) + fun rec_intr (Datatype.DtRec i) (Leaf xs) = + (* recursive argument is "rec_i params elem" *) + compute_array_entry i (find_index (fn x => x = True) xs) + | rec_intr (Datatype.DtRec _) (Node _) = + raise REFUTE ("IDT_recursion_interpreter", + "interpretation for IDT is a node") + | rec_intr (Datatype.DtType ("fun", [_, dt2])) (Node xs) = + (* recursive argument is something like *) + (* "\x::dt1. rec_? params (elem x)" *) + Node (map (rec_intr dt2) xs) + | rec_intr (Datatype.DtType ("fun", [_, _])) (Leaf _) = + raise REFUTE ("IDT_recursion_interpreter", + "interpretation for function dtyp is a leaf") + | rec_intr _ _ = + (* admissibility ensures that every recursive type *) + (* is of the form 'Dt_1 -> ... -> Dt_k -> *) + (* (DtRec i)' *) + raise REFUTE ("IDT_recursion_interpreter", + "non-recursive codomain in recursive dtyp") + (* obtain interpretations for recursive arguments *) + (* interpretation list *) + val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs + (* apply 'intr' to all recursive arguments *) + val result = fold (fn arg_i => fn i => + interpretation_apply (i, arg_i)) arg_intrs intr + (* update 'REC_OPERATORS' *) + val _ = Array.update (arr, elem, (true, result)) + in + result + end + end + val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index)) + (* sanity check: the size of 'IDT' should be 'idt_size' *) + val _ = + if idt_size <> size_of_type ctxt (typs, []) IDT then + raise REFUTE ("IDT_recursion_interpreter", + "unexpected size of IDT (wrong type associated?)") + else () + (* interpretation *) + val rec_op = Node (map_range (compute_array_entry idt_index) idt_size) + in + SOME (rec_op, model', args') + end + end + else + NONE (* not a recursion operator of this datatype *) + ) (Datatype.get_all thy) NONE + | _ => (* head of term is not a constant *) + NONE + end; + +fun set_interpreter ctxt model args t = + let + val (typs, terms) = model + in + case AList.lookup (op =) terms t of + SOME intr => + (* return an existing interpretation *) + SOME (intr, model, args) + | NONE => + (case t of + Free (x, Type (@{type_name set}, [T])) => + let + val (intr, _, args') = + interpret ctxt (typs, []) args (Free (x, T --> HOLogic.boolT)) + in + SOME (intr, (typs, (t, intr)::terms), args') + end + | Var ((x, i), Type (@{type_name set}, [T])) => + let + val (intr, _, args') = + interpret ctxt (typs, []) args (Var ((x,i), T --> HOLogic.boolT)) + in + SOME (intr, (typs, (t, intr)::terms), args') + end + | Const (s, Type (@{type_name set}, [T])) => + let + val (intr, _, args') = + interpret ctxt (typs, []) args (Const (s, T --> HOLogic.boolT)) + in + SOME (intr, (typs, (t, intr)::terms), args') + end + (* 'Collect' == identity *) + | Const (@{const_name Collect}, _) $ t1 => + SOME (interpret ctxt model args t1) + | Const (@{const_name Collect}, _) => + SOME (interpret ctxt model args (eta_expand t 1)) + (* 'op :' == application *) + | Const (@{const_name Set.member}, _) $ t1 $ t2 => + SOME (interpret ctxt model args (t2 $ t1)) + | Const (@{const_name Set.member}, _) $ _ => + SOME (interpret ctxt model args (eta_expand t 1)) + | Const (@{const_name Set.member}, _) => + SOME (interpret ctxt model args (eta_expand t 2)) + | _ => NONE) + end; + +(* only an optimization: 'card' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) + +fun Finite_Set_card_interpreter ctxt model args t = + case t of + Const (@{const_name Finite_Set.card}, + Type ("fun", [Type (@{type_name set}, [T]), @{typ nat}])) => + let + (* interpretation -> int *) + fun number_of_elements (Node xs) = + fold (fn x => fn n => + if x = TT then + n + 1 + else if x = FF then + n + else + raise REFUTE ("Finite_Set_card_interpreter", + "interpretation for set type does not yield a Boolean")) + xs 0 + | number_of_elements (Leaf _) = + raise REFUTE ("Finite_Set_card_interpreter", + "interpretation for set type is a leaf") + val size_of_nat = size_of_type ctxt model (@{typ nat}) + (* takes an interpretation for a set and returns an interpretation *) + (* for a 'nat' denoting the set's cardinality *) + (* interpretation -> interpretation *) + fun card i = + let + val n = number_of_elements i + in + if n < size_of_nat then + Leaf ((replicate n False) @ True :: + (replicate (size_of_nat-n-1) False)) + else + Leaf (replicate size_of_nat False) + end + val set_constants = make_constants ctxt model (HOLogic.mk_setT T) + in + SOME (Node (map card set_constants), model, args) + end + | _ => NONE; + +(* only an optimization: 'finite' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) + +fun Finite_Set_finite_interpreter ctxt model args t = + case t of + Const (@{const_name Finite_Set.finite}, + Type ("fun", [_, @{typ bool}])) $ _ => + (* we only consider finite models anyway, hence EVERY set is *) + (* "finite" *) + SOME (TT, model, args) + | Const (@{const_name Finite_Set.finite}, + Type ("fun", [set_T, @{typ bool}])) => + let + val size_of_set = size_of_type ctxt model set_T + in + (* we only consider finite models anyway, hence EVERY set is *) + (* "finite" *) + SOME (Node (replicate size_of_set TT), model, args) + end + | _ => NONE; + +(* only an optimization: 'less' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) + +fun Nat_less_interpreter ctxt model args t = + case t of + Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat}, + Type ("fun", [@{typ nat}, @{typ bool}])])) => + let + val size_of_nat = size_of_type ctxt model (@{typ nat}) + (* the 'n'-th nat is not less than the first 'n' nats, while it *) + (* is less than the remaining 'size_of_nat - n' nats *) + (* int -> interpretation *) + fun less n = Node ((replicate n FF) @ (replicate (size_of_nat - n) TT)) + in + SOME (Node (map less (1 upto size_of_nat)), model, args) + end + | _ => NONE; + +(* only an optimization: 'plus' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) + +fun Nat_plus_interpreter ctxt model args t = + case t of + Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat}, + Type ("fun", [@{typ nat}, @{typ nat}])])) => + let + val size_of_nat = size_of_type ctxt model (@{typ nat}) + (* int -> int -> interpretation *) + fun plus m n = + let + val element = m + n + in + if element > size_of_nat - 1 then + Leaf (replicate size_of_nat False) + else + Leaf ((replicate element False) @ True :: + (replicate (size_of_nat - element - 1) False)) + end + in + SOME (Node (map_range (fn m => Node (map_range (plus m) size_of_nat)) size_of_nat), + model, args) + end + | _ => NONE; + +(* only an optimization: 'minus' could in principle be interpreted *) +(* with interpreters available already (using its definition), but the *) +(* code below is more efficient *) + +fun Nat_minus_interpreter ctxt model args t = + case t of + Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat}, + Type ("fun", [@{typ nat}, @{typ nat}])])) => + let + val size_of_nat = size_of_type ctxt model (@{typ nat}) + (* int -> int -> interpretation *) + fun minus m n = + let + val element = Int.max (m-n, 0) + in + Leaf ((replicate element False) @ True :: + (replicate (size_of_nat - element - 1) False)) + end + in + SOME (Node (map_range (fn m => Node (map_range (minus m) size_of_nat)) size_of_nat), + model, args) + end + | _ => NONE; + +(* only an optimization: 'times' could in principle be interpreted *) +(* with interpreters available already (using its definition), but the *) +(* code below is more efficient *) + +fun Nat_times_interpreter ctxt model args t = + case t of + Const (@{const_name Groups.times}, Type ("fun", [@{typ nat}, + Type ("fun", [@{typ nat}, @{typ nat}])])) => + let + val size_of_nat = size_of_type ctxt model (@{typ nat}) + (* nat -> nat -> interpretation *) + fun mult m n = + let + val element = m * n + in + if element > size_of_nat - 1 then + Leaf (replicate size_of_nat False) + else + Leaf ((replicate element False) @ True :: + (replicate (size_of_nat - element - 1) False)) + end + in + SOME (Node (map_range (fn m => Node (map_range (mult m) size_of_nat)) size_of_nat), + model, args) + end + | _ => NONE; + +(* only an optimization: 'append' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) + +fun List_append_interpreter ctxt model args t = + case t of + Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun", + [Type ("List.list", [_]), Type ("List.list", [_])])])) => + let + val size_elem = size_of_type ctxt model T + val size_list = size_of_type ctxt model (Type ("List.list", [T])) + (* maximal length of lists; 0 if we only consider the empty list *) + val list_length = + let + (* int -> int -> int -> int *) + fun list_length_acc len lists total = + if lists = total then + len + else if lists < total then + list_length_acc (len+1) (lists*size_elem) (total-lists) + else + raise REFUTE ("List_append_interpreter", + "size_list not equal to 1 + size_elem + ... + " ^ + "size_elem^len, for some len") + in + list_length_acc 0 1 size_list + end + val elements = 0 upto (size_list-1) + (* FIXME: there should be a nice formula, which computes the same as *) + (* the following, but without all this intermediate tree *) + (* length/offset stuff *) + (* associate each list with its length and offset in a complete tree *) + (* of width 'size_elem' and depth 'length_list' (with 'size_list' *) + (* nodes total) *) + (* (int * (int * int)) list *) + val (lenoff_lists, _) = fold_map (fn elem => fn (offsets, off) => + (* corresponds to a pre-order traversal of the tree *) + let + val len = length offsets + (* associate the given element with len/off *) + val assoc = (elem, (len, off)) + in + if len < list_length then + (* go to first child node *) + (assoc, (off :: offsets, off * size_elem)) + else if off mod size_elem < size_elem - 1 then + (* go to next sibling node *) + (assoc, (offsets, off + 1)) + else + (* go back up the stack until we find a level where we can go *) + (* to the next sibling node *) + let + val offsets' = snd (take_prefix + (fn off' => off' mod size_elem = size_elem - 1) offsets) + in + case offsets' of + [] => + (* we're at the last node in the tree; the next value *) + (* won't be used anyway *) + (assoc, ([], 0)) + | off'::offs' => + (* go to next sibling node *) + (assoc, (offs', off' + 1)) + end + end) elements ([], 0) + (* we also need the reverse association (from length/offset to *) + (* index) *) + val lenoff'_lists = map Library.swap lenoff_lists + (* returns the interpretation for "(list no. m) @ (list no. n)" *) + (* nat -> nat -> interpretation *) + fun append m n = + let + val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m) + val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n) + val len_elem = len_m + len_n + val off_elem = off_m * Integer.pow len_n size_elem + off_n + in + case AList.lookup op= lenoff'_lists (len_elem, off_elem) of + NONE => + (* undefined *) + Leaf (replicate size_list False) + | SOME element => + Leaf ((replicate element False) @ True :: + (replicate (size_list - element - 1) False)) + end + in + SOME (Node (map (fn m => Node (map (append m) elements)) elements), + model, args) + end + | _ => NONE; + +(* only an optimization: 'lfp' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) + +fun lfp_interpreter ctxt model args t = + case t of + Const (@{const_name lfp}, Type ("fun", [Type ("fun", + [Type (@{type_name set}, [T]), + Type (@{type_name set}, [_])]), + Type (@{type_name set}, [_])])) => + let + val size_elem = size_of_type ctxt model T + (* the universe (i.e. the set that contains every element) *) + val i_univ = Node (replicate size_elem TT) + (* all sets with elements from type 'T' *) + val i_sets = make_constants ctxt model (HOLogic.mk_setT T) + (* all functions that map sets to sets *) + val i_funs = make_constants ctxt model (Type ("fun", + [HOLogic.mk_setT T, HOLogic.mk_setT T])) + (* "lfp(f) == Inter({u. f(u) <= u})" *) + (* interpretation * interpretation -> bool *) + fun is_subset (Node subs, Node sups) = + forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups) + | is_subset (_, _) = + raise REFUTE ("lfp_interpreter", + "is_subset: interpretation for set is not a node") + (* interpretation * interpretation -> interpretation *) + fun intersection (Node xs, Node ys) = + Node (map (fn (x, y) => if x=TT andalso y=TT then TT else FF) + (xs ~~ ys)) + | intersection (_, _) = + raise REFUTE ("lfp_interpreter", + "intersection: interpretation for set is not a node") + (* interpretation -> interpretaion *) + fun lfp (Node resultsets) = + fold (fn (set, resultset) => fn acc => + if is_subset (resultset, set) then + intersection (acc, set) + else + acc) (i_sets ~~ resultsets) i_univ + | lfp _ = + raise REFUTE ("lfp_interpreter", + "lfp: interpretation for function is not a node") + in + SOME (Node (map lfp i_funs), model, args) + end + | _ => NONE; + +(* only an optimization: 'gfp' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) + +fun gfp_interpreter ctxt model args t = + case t of + Const (@{const_name gfp}, Type ("fun", [Type ("fun", + [Type (@{type_name set}, [T]), + Type (@{type_name set}, [_])]), + Type (@{type_name set}, [_])])) => + let + val size_elem = size_of_type ctxt model T + (* the universe (i.e. the set that contains every element) *) + val i_univ = Node (replicate size_elem TT) + (* all sets with elements from type 'T' *) + val i_sets = make_constants ctxt model (HOLogic.mk_setT T) + (* all functions that map sets to sets *) + val i_funs = make_constants ctxt model (Type ("fun", + [HOLogic.mk_setT T, HOLogic.mk_setT T])) + (* "gfp(f) == Union({u. u <= f(u)})" *) + (* interpretation * interpretation -> bool *) + fun is_subset (Node subs, Node sups) = + forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) + (subs ~~ sups) + | is_subset (_, _) = + raise REFUTE ("gfp_interpreter", + "is_subset: interpretation for set is not a node") + (* interpretation * interpretation -> interpretation *) + fun union (Node xs, Node ys) = + Node (map (fn (x,y) => if x=TT orelse y=TT then TT else FF) + (xs ~~ ys)) + | union (_, _) = + raise REFUTE ("gfp_interpreter", + "union: interpretation for set is not a node") + (* interpretation -> interpretaion *) + fun gfp (Node resultsets) = + fold (fn (set, resultset) => fn acc => + if is_subset (set, resultset) then + union (acc, set) + else + acc) (i_sets ~~ resultsets) i_univ + | gfp _ = + raise REFUTE ("gfp_interpreter", + "gfp: interpretation for function is not a node") + in + SOME (Node (map gfp i_funs), model, args) + end + | _ => NONE; + +(* only an optimization: 'fst' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) + +fun Product_Type_fst_interpreter ctxt model args t = + case t of + Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => + let + val constants_T = make_constants ctxt model T + val size_U = size_of_type ctxt model U + in + SOME (Node (maps (replicate size_U) constants_T), model, args) + end + | _ => NONE; + +(* only an optimization: 'snd' could in principle be interpreted with *) +(* interpreters available already (using its definition), but the code *) +(* below is more efficient *) + +fun Product_Type_snd_interpreter ctxt model args t = + case t of + Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => + let + val size_T = size_of_type ctxt model T + val constants_U = make_constants ctxt model U + in + SOME (Node (flat (replicate size_T constants_U)), model, args) + end + | _ => NONE; + + +(* ------------------------------------------------------------------------- *) +(* PRINTERS *) +(* ------------------------------------------------------------------------- *) + +fun stlc_printer ctxt model T intr assignment = + let + (* string -> string *) + val strip_leading_quote = perhaps (try (unprefix "'")) + (* Term.typ -> string *) + fun string_of_typ (Type (s, _)) = s + | string_of_typ (TFree (x, _)) = strip_leading_quote x + | string_of_typ (TVar ((x,i), _)) = + strip_leading_quote x ^ string_of_int i + (* interpretation -> int *) + fun index_from_interpretation (Leaf xs) = + find_index (Prop_Logic.eval assignment) xs + | index_from_interpretation _ = + raise REFUTE ("stlc_printer", + "interpretation for ground type is not a leaf") + in + case T of + Type ("fun", [T1, T2]) => + let + (* create all constants of type 'T1' *) + val constants = make_constants ctxt model T1 + (* interpretation list *) + val results = + (case intr of + Node xs => xs + | _ => raise REFUTE ("stlc_printer", + "interpretation for function type is a leaf")) + (* Term.term list *) + val pairs = map (fn (arg, result) => + HOLogic.mk_prod + (print ctxt model T1 arg assignment, + print ctxt model T2 result assignment)) + (constants ~~ results) + (* Term.typ *) + val HOLogic_prodT = HOLogic.mk_prodT (T1, T2) + val HOLogic_setT = HOLogic.mk_setT HOLogic_prodT + (* Term.term *) + val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT) + val HOLogic_insert = + Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) + in + SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set) + end + | Type ("prop", []) => + (case index_from_interpretation intr of + ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT))) + | 0 => SOME (HOLogic.mk_Trueprop @{term True}) + | 1 => SOME (HOLogic.mk_Trueprop @{term False}) + | _ => raise REFUTE ("stlc_interpreter", + "illegal interpretation for a propositional value")) + | Type _ => + if index_from_interpretation intr = (~1) then + SOME (Const (@{const_name undefined}, T)) + else + SOME (Const (string_of_typ T ^ + string_of_int (index_from_interpretation intr), T)) + | TFree _ => + if index_from_interpretation intr = (~1) then + SOME (Const (@{const_name undefined}, T)) + else + SOME (Const (string_of_typ T ^ + string_of_int (index_from_interpretation intr), T)) + | TVar _ => + if index_from_interpretation intr = (~1) then + SOME (Const (@{const_name undefined}, T)) + else + SOME (Const (string_of_typ T ^ + string_of_int (index_from_interpretation intr), T)) + end; + +fun set_printer ctxt model T intr assignment = + (case T of + Type (@{type_name set}, [T1]) => + let + (* create all constants of type 'T1' *) + val constants = make_constants ctxt model T1 + (* interpretation list *) + val results = (case intr of + Node xs => xs + | _ => raise REFUTE ("set_printer", + "interpretation for set type is a leaf")) + (* Term.term list *) + val elements = List.mapPartial (fn (arg, result) => + case result of + Leaf [fmTrue, (* fmFalse *) _] => + if Prop_Logic.eval assignment fmTrue then + SOME (print ctxt model T1 arg assignment) + else (* if Prop_Logic.eval assignment fmFalse then *) + NONE + | _ => + raise REFUTE ("set_printer", + "illegal interpretation for a Boolean value")) + (constants ~~ results) + (* Term.typ *) + val HOLogic_setT1 = HOLogic.mk_setT T1 + (* Term.term *) + val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT1) + val HOLogic_insert = + Const (@{const_name insert}, T1 --> HOLogic_setT1 --> HOLogic_setT1) + in + SOME (Library.foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) + (HOLogic_empty_set, elements)) + end + | _ => + NONE); + +fun IDT_printer ctxt model T intr assignment = + let + val thy = Proof_Context.theory_of ctxt + in + (case T of + Type (s, Ts) => + (case Datatype.get_info thy s of + SOME info => (* inductive datatype *) + let + val (typs, _) = model + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) + val typ_assoc = dtyps ~~ Ts + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = + if Library.exists (fn d => + case d of Datatype.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_printer", "datatype argument (for type " ^ + Syntax.string_of_typ ctxt (Type (s, Ts)) ^ ") is not a variable") + else () + (* the index of the element in the datatype *) + val element = + (case intr of + Leaf xs => find_index (Prop_Logic.eval assignment) xs + | Node _ => raise REFUTE ("IDT_printer", + "interpretation is not a leaf")) + in + if element < 0 then + SOME (Const (@{const_name undefined}, Type (s, Ts))) + else + let + (* takes a datatype constructor, and if for some arguments this *) + (* constructor generates the datatype's element that is given by *) + (* 'element', returns the constructor (as a term) as well as the *) + (* indices of the arguments *) + fun get_constr_args (cname, cargs) = + let + val cTerm = Const (cname, + map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts)) + val (iC, _, _) = interpret ctxt (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm + (* interpretation -> int list option *) + fun get_args (Leaf xs) = + if find_index (fn x => x = True) xs = element then + SOME [] + else + NONE + | get_args (Node xs) = + let + (* interpretation * int -> int list option *) + fun search ([], _) = + NONE + | search (x::xs, n) = + (case get_args x of + SOME result => SOME (n::result) + | NONE => search (xs, n+1)) + in + search (xs, 0) + end + in + Option.map (fn args => (cTerm, cargs, args)) (get_args iC) + end + val (cTerm, cargs, args) = + (* we could speed things up by computing the correct *) + (* constructor directly (rather than testing all *) + (* constructors), based on the order in which constructors *) + (* generate elements of datatypes; the current implementation *) + (* of 'IDT_printer' however is independent of the internals *) + (* of 'IDT_constructor_interpreter' *) + (case get_first get_constr_args constrs of + SOME x => x + | NONE => raise REFUTE ("IDT_printer", + "no matching constructor found for element " ^ + string_of_int element)) + val argsTerms = map (fn (d, n) => + let + val dT = typ_of_dtyp descr typ_assoc d + (* we only need the n-th element of this list, so there *) + (* might be a more efficient implementation that does not *) + (* generate all constants *) + val consts = make_constants ctxt (typs, []) dT + in + print ctxt (typs, []) dT (nth consts n) assignment + end) (cargs ~~ args) + in + SOME (list_comb (cTerm, argsTerms)) + end + end + | NONE => (* not an inductive datatype *) + NONE) + | _ => (* a (free or schematic) type variable *) + NONE) + end; + + +(* ------------------------------------------------------------------------- *) +(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *) +(* structure *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* Note: the interpreters and printers are used in reverse order; however, *) +(* an interpreter that can handle non-atomic terms ends up being *) +(* applied before the 'stlc_interpreter' breaks the term apart into *) +(* subterms that are then passed to other interpreters! *) +(* ------------------------------------------------------------------------- *) + +val setup = + add_interpreter "stlc" stlc_interpreter #> + add_interpreter "Pure" Pure_interpreter #> + add_interpreter "HOLogic" HOLogic_interpreter #> + add_interpreter "set" set_interpreter #> + add_interpreter "IDT" IDT_interpreter #> + add_interpreter "IDT_constructor" IDT_constructor_interpreter #> + add_interpreter "IDT_recursion" IDT_recursion_interpreter #> + add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #> + add_interpreter "Finite_Set.finite" Finite_Set_finite_interpreter #> + add_interpreter "Nat_Orderings.less" Nat_less_interpreter #> + add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #> + add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #> + add_interpreter "Nat_HOL.times" Nat_times_interpreter #> + add_interpreter "List.append" List_append_interpreter #> +(* UNSOUND + add_interpreter "lfp" lfp_interpreter #> + add_interpreter "gfp" gfp_interpreter #> +*) + add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #> + add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #> + add_printer "stlc" stlc_printer #> + add_printer "set" set_printer #> + add_printer "IDT" IDT_printer; + + + +(** outer syntax commands 'refute' and 'refute_params' **) + +(* argument parsing *) + +(*optional list of arguments of the form [name1=value1, name2=value2, ...]*) + +val scan_parm = Parse.name -- (Scan.optional (@{keyword "="} |-- Parse.name) "true") +val scan_parms = Scan.optional (@{keyword "["} |-- Parse.list scan_parm --| @{keyword "]"}) []; + + +(* 'refute' command *) + +val _ = + Outer_Syntax.improper_command @{command_spec "refute"} + "try to find a model that refutes a given subgoal" + (scan_parms -- Scan.optional Parse.nat 1 >> + (fn (parms, i) => + Toplevel.keep (fn state => + let + val ctxt = Toplevel.context_of state; + val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state); + in refute_goal ctxt parms st i; () end))); + + +(* 'refute_params' command *) + +val _ = + Outer_Syntax.command @{command_spec "refute_params"} + "show/store default parameters for the 'refute' command" + (scan_parms >> (fn parms => + Toplevel.theory (fn thy => + let + val thy' = fold set_default_param parms thy; + val output = + (case get_default_params (Proof_Context.init_global thy') of + [] => "none" + | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults)); + val _ = writeln ("Default parameters for 'refute':\n" ^ output); + in thy' end))); + +end; + diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/ROOT --- a/src/HOL/ROOT Wed Oct 31 11:23:21 2012 +0100 +++ b/src/HOL/ROOT Wed Oct 31 11:23:21 2012 +0100 @@ -49,6 +49,7 @@ (* Code_Prolog FIXME cf. 76965c356d2a *) Code_Real_Approx_By_Float Target_Numeral + Refute theories [condition = ISABELLE_FULL_TEST] Sum_of_Squares_Remote files "document/root.bib" "document/root.tex" @@ -422,6 +423,7 @@ Chinese Serbian "~~/src/HOL/Library/FinFun_Syntax" + "~~/src/HOL/Library/Refute" theories Iff_Oracle Coercion_Examples diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/Refute.thy --- a/src/HOL/Refute.thy Wed Oct 31 11:23:21 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,113 +0,0 @@ -(* Title: HOL/Refute.thy - Author: Tjark Weber - Copyright 2003-2007 - -Basic setup and documentation for the 'refute' (and 'refute_params') command. -*) - -header {* Refute *} - -theory Refute -imports Hilbert_Choice List Sledgehammer -keywords "refute" :: diag and "refute_params" :: thy_decl -begin - -ML_file "Tools/refute.ML" -setup Refute.setup - -refute_params - [itself = 1, - minsize = 1, - maxsize = 8, - maxvars = 10000, - maxtime = 60, - satsolver = auto, - no_assms = false] - -text {* -\small -\begin{verbatim} -(* ------------------------------------------------------------------------- *) -(* REFUTE *) -(* *) -(* We use a SAT solver to search for a (finite) model that refutes a given *) -(* HOL formula. *) -(* ------------------------------------------------------------------------- *) - -(* ------------------------------------------------------------------------- *) -(* NOTE *) -(* *) -(* I strongly recommend that you install a stand-alone SAT solver if you *) -(* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. If you *) -(* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME' *) -(* in 'etc/settings'. *) -(* ------------------------------------------------------------------------- *) - -(* ------------------------------------------------------------------------- *) -(* USAGE *) -(* *) -(* See the file 'HOL/ex/Refute_Examples.thy' for examples. The supported *) -(* parameters are explained below. *) -(* ------------------------------------------------------------------------- *) - -(* ------------------------------------------------------------------------- *) -(* CURRENT LIMITATIONS *) -(* *) -(* 'refute' currently accepts formulas of higher-order predicate logic (with *) -(* equality), including free/bound/schematic variables, lambda abstractions, *) -(* sets and set membership, "arbitrary", "The", "Eps", records and *) -(* inductively defined sets. Constants are unfolded automatically, and sort *) -(* axioms are added as well. Other, user-asserted axioms however are *) -(* ignored. Inductive datatypes and recursive functions are supported, but *) -(* may lead to spurious countermodels. *) -(* *) -(* The (space) complexity of the algorithm is non-elementary. *) -(* *) -(* Schematic type variables are not supported. *) -(* ------------------------------------------------------------------------- *) - -(* ------------------------------------------------------------------------- *) -(* PARAMETERS *) -(* *) -(* The following global parameters are currently supported (and required, *) -(* except for "expect"): *) -(* *) -(* Name Type Description *) -(* *) -(* "minsize" int Only search for models with size at least *) -(* 'minsize'. *) -(* "maxsize" int If >0, only search for models with size at most *) -(* 'maxsize'. *) -(* "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. *) -(* This value is ignored under some ML compilers. *) -(* "satsolver" string Name of the 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"). *) -(* *) -(* The size of particular types can be specified in the form type=size *) -(* (where 'type' is a string, and 'size' is an int). Examples: *) -(* "'a"=1 *) -(* "List.list"=2 *) -(* ------------------------------------------------------------------------- *) - -(* ------------------------------------------------------------------------- *) -(* FILES *) -(* *) -(* HOL/Tools/prop_logic.ML Propositional logic *) -(* HOL/Tools/sat_solver.ML SAT solvers *) -(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *) -(* Boolean assignment -> HOL model *) -(* HOL/Refute.thy This file: loads the ML files, basic setup, *) -(* documentation *) -(* HOL/SAT.thy Sets default parameters *) -(* HOL/ex/Refute_Examples.thy Examples *) -(* ------------------------------------------------------------------------- *) -\end{verbatim} -*} - -end diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/SAT.thy --- a/src/HOL/SAT.thy Wed Oct 31 11:23:21 2012 +0100 +++ b/src/HOL/SAT.thy Wed Oct 31 11:23:21 2012 +0100 @@ -8,7 +8,7 @@ header {* Reconstructing external resolution proofs for propositional logic *} theory SAT -imports Refute +imports Hilbert_Choice List Sledgehammer begin ML_file "Tools/sat_funcs.ML" diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/TPTP/ATP_Problem_Import.thy --- a/src/HOL/TPTP/ATP_Problem_Import.thy Wed Oct 31 11:23:21 2012 +0100 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Wed Oct 31 11:23:21 2012 +0100 @@ -5,7 +5,10 @@ header {* ATP Problem Importer *} theory ATP_Problem_Import -imports Complex_Main TPTP_Interpret +imports + Complex_Main + TPTP_Interpret + "~~/src/HOL/Library/Refute" begin ML_file "sledgehammer_tactics.ML" diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Wed Oct 31 11:23:21 2012 +0100 +++ b/src/HOL/TPTP/atp_problem_import.ML Wed Oct 31 11:23:21 2012 +0100 @@ -72,7 +72,7 @@ val thy = Proof_Context.theory_of ctxt val (defs, pseudo_defs) = defs |> map (ATP_Util.abs_extensionalize_term ctxt - #> aptrueprop (open_form I)) + #> aptrueprop (hol_open_form I)) |> List.partition (ATP_Util.is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop) o ATP_Util.unextensionalize_def) diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Oct 31 11:23:21 2012 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Oct 31 11:23:21 2012 +0100 @@ -1311,10 +1311,10 @@ |> map snd end -(* Ideally we would check against "Complex_Main", not "Refute", but any theory - will do as long as it contains all the "axioms" and "axiomatization" +(* Ideally we would check against "Complex_Main", not "Hilbert_Choice", but any + theory will do as long as it contains all the "axioms" and "axiomatization" commands. *) -fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute}) +fun is_built_in_theory thy = Theory.subthy (thy, @{theory Hilbert_Choice}) fun all_nondefs_of ctxt subst = ctxt |> Spec_Rules.get diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Oct 31 11:23:21 2012 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Oct 31 11:23:21 2012 +0100 @@ -351,8 +351,6 @@ commas (map (quote o Syntax.string_of_term ctxt) ts)) ^ " (" ^ quote loc ^ "): " ^ commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".") - | Refute.REFUTE (loc, details) => - error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".") fun pick_nits override_params mode i step state = let diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Oct 31 11:23:21 2012 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Oct 31 11:23:21 2012 +0100 @@ -252,14 +252,34 @@ val nat_T = @{typ nat} val int_T = @{typ int} -val simple_string_of_typ = Refute.string_of_typ -val is_real_constr = Refute.is_IDT_constructor +fun simple_string_of_typ (Type (s, _)) = s + | simple_string_of_typ (TFree (s, _)) = s + | simple_string_of_typ (TVar ((s, _), _)) = s + +fun is_real_constr 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 + val typ_of_dtyp = ATP_Util.typ_of_dtyp val varify_type = ATP_Util.varify_type val instantiate_type = ATP_Util.instantiate_type val varify_and_instantiate_type = ATP_Util.varify_and_instantiate_type -val is_of_class_const = Refute.is_const_of_class -val get_class_def = Refute.get_classdef + +fun is_of_class_const thy (s, _) = + member (op =) (map Logic.const_of_class (Sign.all_classes thy)) s + +fun get_class_def thy class = + let val axname = class ^ "_class_def" in + Option.map (pair axname) + (AList.lookup (op =) (Theory.all_axioms_of thy) axname) + end; + val monomorphic_term = ATP_Util.monomorphic_term val specialize_type = ATP_Util.specialize_type val eta_expand = ATP_Util.eta_expand diff -r 9f655a6bffd8 -r 5b4b0e4e5205 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed Oct 31 11:23:21 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3229 +0,0 @@ -(* 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 -> (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 * string) list - val actual_params : Proof.context -> (string * string) list -> 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 * string) list -> term list -> term -> string - (* tries to find a model that refutes a formula: *) - val refute_term : - Proof.context -> (string * string) list -> term list -> term -> string - val refute_goal : - Proof.context -> (string * string) list -> thm -> int -> string - - val setup : theory -> theory - -(* ------------------------------------------------------------------------- *) -(* 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; - -(* ('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 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 - (* (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 ctxt - (* 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 *) -(* ------------------------------------------------------------------------- *) - -val typ_of_dtyp = ATP_Util.typ_of_dtyp - -(* ------------------------------------------------------------------------- *) -(* close_form: universal closure over schematic variables in 't' *) -(* ------------------------------------------------------------------------- *) - -(* Term.term -> Term.term *) - -fun close_form t = - let - val vars = sort_wrt (fst o fst) (Term.add_vars t []) - in - fold (fn ((x, i), T) => fn t' => - Logic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t - end; - -val monomorphic_term = ATP_Util.monomorphic_term -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 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' *) -(* ------------------------------------------------------------------------- *) - -fun is_IDT_recursor thy (s, _) = - 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 *) -(* ------------------------------------------------------------------------- *) - -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" *) -(* ------------------------------------------------------------------------- *) - -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 (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 *) -(* ------------------------------------------------------------------------- *) - -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 - (* 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'. *) - -(* 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 ctxt t = - let - val thy = Proof_Context.theory_of ctxt - 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 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, monomorphic_term (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 ("prop", []) => axs - | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs) - | Type (@{type_name set}, [T1]) => 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 _ => (* 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 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; - -(* ------------------------------------------------------------------------- *) -(* 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 ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc) - | Type ("prop", []) => acc - | Type (@{type_name set}, [T1]) => collect_types T1 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.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 - Datatype.DtTFree _ => - collect_types dT acc - | Datatype.DtType (_, ds) => - collect_types dT (fold_rev collect_dtyp ds acc) - | Datatype.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.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 = - case AList.lookup (op =) sizes (string_of_typ T) of - SOME n => n - | NONE => minsize - in - map (fn T => (T, size_of_typ T)) xs - end; - -(* ------------------------------------------------------------------------- *) -(* next_universe: enumerates all universes (i.e. assignments of sizes to *) -(* types), where the minimal size of a type is given by *) -(* 'minsize', the maximal size is given by 'maxsize', and a *) -(* type may have a fixed size given in 'sizes' *) -(* ------------------------------------------------------------------------- *) - -(* (Term.typ * int) list -> (string * int) list -> int -> int -> - (Term.typ * int) list option *) - -fun next_universe xs sizes minsize maxsize = - let - (* creates the "first" list of length 'len', where the sum of all list *) - (* elements is 'sum', and the length of the list is 'len' *) - (* int -> int -> int -> int list option *) - fun make_first _ 0 sum = - if sum = 0 then - SOME [] - else - NONE - | make_first max len sum = - if sum <= max orelse max < 0 then - Option.map (fn xs' => sum :: xs') (make_first max (len-1) 0) - else - Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max)) - (* enumerates all int lists with a fixed length, where 0<=x<='max' for *) - (* all list elements x (unless 'max'<0) *) - (* int -> int -> int -> int list -> int list option *) - fun next _ _ _ [] = - 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 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" *) -(* ------------------------------------------------------------------------- *) - -(* interpretation -> prop_formula *) - -fun toTrue (Leaf [fm, _]) = fm - | toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value"); - -(* ------------------------------------------------------------------------- *) -(* toFalse: converts the interpretation of a Boolean value to a *) -(* propositional formula that is true iff the interpretation *) -(* denotes "false" *) -(* ------------------------------------------------------------------------- *) - -(* interpretation -> prop_formula *) - -fun toFalse (Leaf [_, fm]) = fm - | toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value"); - -(* ------------------------------------------------------------------------- *) -(* find_model: repeatedly calls 'interpret' with appropriate parameters, *) -(* applies a SAT solver, and (in case a model is found) displays *) -(* the model to the user by calling 'print_model' *) -(* {...} : 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 - (* string -> string *) - fun check_expect outcome_code = - if expect = "" orelse outcome_code = expect then outcome_code - else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") - (* unit -> string *) - 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 - (* Term.typ list *) - 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 Datatype.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 Datatype_Aux.is_rec_type ds) constrs - end - | NONE => false) - | _ => false) types - val _ = - if maybe_spurious then - warning ("Term contains a recursive datatype; " - ^ "countermodel(s) may be spurious!") - else - () - (* (Term.typ * int) list -> string *) - fun find_model_loop universe = - let - val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer) - val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime - orelse raise TimeLimit.TimeOut - 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 satsolver = "dpll" orelse satsolver = "enumerate" then - warning ("Using SAT solver " ^ quote satsolver ^ - "; for better performance, consider installing an \ - \external solver.") - else ()); - val solver = - SatSolver.invoke_solver satsolver - handle Option.Option => - error ("Unknown SAT solver: " ^ quote satsolver ^ - ". Available solvers: " ^ - commas (map (quote o fst) (!SatSolver.solvers)) ^ ".") - in - Output.urgent_message "Invoking SAT solver..."; - (case solver fm of - SatSolver.SATISFIABLE assignment => - (Output.urgent_message ("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") - | SatSolver.UNSATISFIABLE _ => - (Output.urgent_message "No model exists."; - case next_universe universe sizes minsize maxsize of - SOME universe' => find_model_loop universe' - | NONE => (Output.urgent_message - "Search terminated, no larger universe within the given limits."; - "none")) - | SatSolver.UNKNOWN => - (Output.urgent_message "No model found."; - case next_universe universe sizes minsize maxsize of - SOME universe' => find_model_loop universe' - | NONE => (Output.urgent_message - "Search terminated, no larger universe within the given limits."; - "unknown"))) handle SatSolver.NOT_CONFIGURED => - (error ("SAT solver " ^ quote satsolver ^ " is not configured."); - "unknown") - end - handle MAXVARS_EXCEEDED => - (Output.urgent_message ("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 *) - Output.urgent_message ("Trying to find a model that " - ^ (if negate then "refutes" else "satisfies") ^ ": " - ^ Syntax.string_of_term ctxt t); - if maxtime > 0 then ( - TimeLimit.timeLimit (Time.fromSeconds maxtime) - wrapper () - handle TimeLimit.TimeOut => - (Output.urgent_message ("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_wrt (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 all}, _) $ Abs (_, _, t)) = - strip_all_body t - | strip_all_body (Const (@{const_name Trueprop}, _) $ t) = - strip_all_body t - | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) = - strip_all_body t - | strip_all_body t = t - (* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *) - fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) = - (a, T) :: strip_all_vars t - | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) = - strip_all_vars t - | strip_all_vars (Const (@{const_name All}, _) $ 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 |> prop_of - in - if Logic.count_prems t = 0 then - (Output.urgent_message "No subgoal!"; "none") - else - let - val assms = map 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 *) - (* int -> interpretation list *) - fun unit_vectors n = - let - (* returns the k-th unit vector of length n *) - (* int * int -> interpretation *) - fun unit_vector (k, n) = - Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) - (* int -> interpretation list *) - 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' *) - (* int -> 'a list -> 'a list list *) - fun pick_all 1 xs = map single xs - | pick_all n xs = - let val rec_pick = pick_all (n - 1) xs in - maps (fn x => map (cons x) rec_pick) xs - end - (* returns all constant interpretations that have the same tree *) - (* structure as the interpretation argument *) - (* interpretation -> interpretation list *) - 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 *) -(* ------------------------------------------------------------------------- *) - -(* interpretation *) - -val TT = Leaf [True, False]; - -val FF = Leaf [False, True]; - -(* ------------------------------------------------------------------------- *) -(* make_equality: returns an interpretation that denotes (extensional) *) -(* equality of two interpretations *) -(* - two interpretations are 'equal' iff they are both defined and denote *) -(* the same value *) -(* - two interpretations are 'not_equal' iff they are both defined at least *) -(* partially, and a defined part denotes different values *) -(* - a completely undefined interpretation is neither 'equal' nor *) -(* 'not_equal' to another interpretation *) -(* ------------------------------------------------------------------------- *) - -(* We could in principle represent '=' on a type T by a particular *) -(* interpretation. However, the size of that interpretation is quadratic *) -(* in the size of T. Therefore comparing the interpretations 'i1' and *) -(* 'i2' directly is more efficient than constructing the interpretation *) -(* for equality on T first, and "applying" this interpretation to 'i1' *) -(* and 'i2' in the usual way (cf. 'interpretation_apply') then. *) - -(* interpretation * interpretation -> interpretation *) - -fun make_equality (i1, i2) = - let - (* interpretation * interpretation -> prop_formula *) - fun equal (i1, i2) = - (case i1 of - Leaf xs => - (case i2 of - Leaf ys => 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)))) - (* interpretation * interpretation -> prop_formula *) - 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. *) -(* ------------------------------------------------------------------------- *) - -(* interpretation * interpretation -> interpretation *) - -fun make_def_equality (i1, i2) = - let - (* interpretation * interpretation -> prop_formula *) - fun equal (i1, i2) = - (case i1 of - Leaf xs => - (case i2 of - (* defined and equal, or both undefined *) - Leaf ys => SOr (Prop_Logic.dot_product (xs, ys), - SAnd (Prop_Logic.all (map SNot xs), Prop_Logic.all (map SNot ys))) - | Node _ => raise REFUTE ("make_def_equality", - "second interpretation is higher")) - | Node xs => - (case i2 of - Leaf _ => raise REFUTE ("make_def_equality", - "first interpretation is higher") - | Node ys => Prop_Logic.all (map equal (xs ~~ ys)))) - (* interpretation *) - val eq = equal (i1, i2) - in - Leaf [eq, SNot eq] - end; - -(* ------------------------------------------------------------------------- *) -(* interpretation_apply: returns an interpretation that denotes the result *) -(* of applying the function denoted by 'i1' to the *) -(* argument denoted by 'i2' *) -(* ------------------------------------------------------------------------- *) - -(* interpretation * interpretation -> interpretation *) - -fun interpretation_apply (i1, i2) = - let - (* interpretation * interpretation -> interpretation *) - fun interpretation_disjunction (tr1,tr2) = - tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) - (tree_pair (tr1,tr2)) - (* prop_formula * interpretation -> interpretation *) - fun prop_formula_times_interpretation (fm,tr) = - tree_map (map (fn x => SAnd (fm,x))) tr - (* prop_formula list * interpretation list -> interpretation *) - fun prop_formula_list_dot_product_interpretation_list ([fm],[tr]) = - prop_formula_times_interpretation (fm,tr) - | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) = - interpretation_disjunction (prop_formula_times_interpretation (fm,tr), - prop_formula_list_dot_product_interpretation_list (fms,trees)) - | prop_formula_list_dot_product_interpretation_list (_,_) = - raise REFUTE ("interpretation_apply", "empty list (in dot product)") - (* returns a list of lists, each one consisting of one element from each *) - (* element of 'xss' *) - (* 'a list list -> 'a list list *) - fun pick_all [xs] = map single xs - | pick_all (xs::xss) = - let val rec_pick = pick_all xss in - maps (fn x => map (cons x) rec_pick) xs - end - | pick_all _ = raise REFUTE ("interpretation_apply", "empty list (in pick_all)") - (* interpretation -> prop_formula list *) - fun interpretation_to_prop_formula_list (Leaf xs) = xs - | interpretation_to_prop_formula_list (Node trees) = - map Prop_Logic.all (pick_all - (map interpretation_to_prop_formula_list trees)) - in - case i1 of - Leaf _ => - raise REFUTE ("interpretation_apply", "first interpretation is a leaf") - | Node xs => - prop_formula_list_dot_product_interpretation_list - (interpretation_to_prop_formula_list i2, xs) - end; - -(* ------------------------------------------------------------------------- *) -(* eta_expand: eta-expands a term 't' by adding 'i' lambda abstractions *) -(* ------------------------------------------------------------------------- *) - -(* Term.term -> int -> Term.term *) - -fun eta_expand t i = - let - val Ts = Term.binder_types (Term.fastype_of t) - val t' = Term.incr_boundvars i t - in - fold_rev (fn T => fn term => Abs ("", T, term)) - (List.take (Ts, i)) - (Term.list_comb (t', map Bound (i-1 downto 0))) - end; - -(* ------------------------------------------------------------------------- *) -(* size_of_dtyp: the size of (an initial fragment of) an inductive data type *) -(* is the sum (over its constructors) of the product (over *) -(* their arguments) of the size of the argument types *) -(* ------------------------------------------------------------------------- *) - -fun size_of_dtyp ctxt typ_sizes descr typ_assoc constructors = - Integer.sum (map (fn (_, dtyps) => - Integer.prod (map (size_of_type ctxt (typ_sizes, []) o - (typ_of_dtyp descr typ_assoc)) dtyps)) - constructors); - - -(* ------------------------------------------------------------------------- *) -(* INTERPRETERS: Actual Interpreters *) -(* ------------------------------------------------------------------------- *) - -(* simply typed lambda calculus: Isabelle's basic term syntax, with type *) -(* variables, function types, and propT *) - -fun stlc_interpreter ctxt model args t = - let - val (typs, terms) = model - val {maxvars, def_eq, next_idx, bounds, wellformed} = args - (* Term.typ -> (interpretation * model * arguments) option *) - fun interpret_groundterm T = - let - (* unit -> (interpretation * model * arguments) option *) - fun interpret_groundtype () = - let - (* the model must specify a size for ground types *) - val size = - if T = Term.propT then 2 - else the (AList.lookup (op =) typs T) - val next = next_idx + size - (* check if 'maxvars' is large enough *) - val _ = (if next - 1 > maxvars andalso maxvars > 0 then - raise MAXVARS_EXCEEDED else ()) - (* prop_formula list *) - val fms = map BoolVar (next_idx upto (next_idx + size - 1)) - (* interpretation *) - val intr = Leaf fms - (* prop_formula list -> prop_formula *) - fun one_of_two_false [] = True - | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' => - SOr (SNot x, SNot x')) xs), one_of_two_false xs) - (* prop_formula *) - val wf = one_of_two_false fms - in - (* extend the model, increase 'next_idx', add well-formedness *) - (* condition *) - SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, - def_eq = def_eq, next_idx = next, bounds = bounds, - wellformed = SAnd (wellformed, wf)}) - end - in - case T of - Type ("fun", [T1, T2]) => - let - (* we create 'size_of_type ... T1' different copies of the *) - (* interpretation for 'T2', which are then combined into a single *) - (* new interpretation *) - (* make fresh copies, with different variable indices *) - (* 'idx': next variable index *) - (* 'n' : number of copies *) - (* int -> int -> (int * interpretation list * prop_formula *) - fun make_copies idx 0 = (idx, [], True) - | make_copies idx n = - let - val (copy, _, new_args) = interpret ctxt (typs, []) - {maxvars = maxvars, def_eq = false, next_idx = idx, - bounds = [], wellformed = True} (Free ("dummy", T2)) - val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1) - in - (idx', copy :: copies, SAnd (#wellformed new_args, wf')) - end - val (next, copies, wf) = make_copies next_idx - (size_of_type ctxt model T1) - (* combine copies into a single interpretation *) - val intr = Node copies - in - (* extend the model, increase 'next_idx', add well-formedness *) - (* condition *) - SOME (intr, (typs, (t, intr)::terms), {maxvars = maxvars, - def_eq = def_eq, next_idx = next, bounds = bounds, - wellformed = SAnd (wellformed, wf)}) - end - | Type _ => interpret_groundtype () - | TFree _ => interpret_groundtype () - | TVar _ => interpret_groundtype () - end - in - case AList.lookup (op =) terms t of - SOME intr => - (* return an existing interpretation *) - SOME (intr, model, args) - | NONE => - (case t of - Const (_, T) => interpret_groundterm T - | Free (_, T) => interpret_groundterm T - | Var (_, T) => interpret_groundterm T - | Bound i => SOME (nth (#bounds args) i, model, args) - | Abs (_, T, body) => - let - (* create all constants of type 'T' *) - val constants = make_constants ctxt model T - (* interpret the 'body' separately for each constant *) - val (bodies, (model', args')) = fold_map - (fn c => fn (m, a) => - let - (* add 'c' to 'bounds' *) - val (i', m', a') = interpret ctxt m {maxvars = #maxvars a, - def_eq = #def_eq a, next_idx = #next_idx a, - bounds = (c :: #bounds a), wellformed = #wellformed a} body - in - (* keep the new model m' and 'next_idx' and 'wellformed', *) - (* but use old 'bounds' *) - (i', (m', {maxvars = maxvars, def_eq = def_eq, - next_idx = #next_idx a', bounds = bounds, - wellformed = #wellformed a'})) - end) - constants (model, args) - in - SOME (Node bodies, model', args') - end - | t1 $ t2 => - let - (* interpret 't1' and 't2' separately *) - val (intr1, model1, args1) = interpret ctxt model args t1 - val (intr2, model2, args2) = interpret ctxt model1 args1 t2 - in - SOME (interpretation_apply (intr1, intr2), model2, args2) - end) - end; - -fun Pure_interpreter ctxt model args t = - case t of - Const (@{const_name all}, _) $ t1 => - let - val (i, m, a) = interpret ctxt model args t1 - in - case i of - Node xs => - (* 3-valued logic *) - let - val fmTrue = Prop_Logic.all (map toTrue xs) - val fmFalse = Prop_Logic.exists (map toFalse xs) - in - SOME (Leaf [fmTrue, fmFalse], m, a) - end - | _ => - raise REFUTE ("Pure_interpreter", - "\"all\" is followed by a non-function") - end - | Const (@{const_name all}, _) => - SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name "=="}, _) $ t1 $ t2 => - let - val (i1, m1, a1) = interpret ctxt model args t1 - val (i2, m2, a2) = interpret ctxt m1 a1 t2 - in - (* we use either 'make_def_equality' or 'make_equality' *) - SOME ((if #def_eq args then make_def_equality else make_equality) - (i1, i2), m2, a2) - end - | Const (@{const_name "=="}, _) $ _ => - SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name "=="}, _) => - SOME (interpret ctxt model args (eta_expand t 2)) - | Const (@{const_name "==>"}, _) $ t1 $ t2 => - (* 3-valued logic *) - let - val (i1, m1, a1) = interpret ctxt model args t1 - val (i2, m2, a2) = interpret ctxt m1 a1 t2 - val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2) - val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2) - in - SOME (Leaf [fmTrue, fmFalse], m2, a2) - end - | Const (@{const_name "==>"}, _) $ _ => - SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name "==>"}, _) => - SOME (interpret ctxt model args (eta_expand t 2)) - | _ => NONE; - -fun HOLogic_interpreter ctxt model args t = -(* Providing interpretations directly is more efficient than unfolding the *) -(* logical constants. In HOL however, logical constants can themselves be *) -(* arguments. They are then translated using eta-expansion. *) - case t of - Const (@{const_name Trueprop}, _) => - SOME (Node [TT, FF], model, args) - | Const (@{const_name Not}, _) => - SOME (Node [FF, TT], model, args) - (* redundant, since 'True' is also an IDT constructor *) - | Const (@{const_name True}, _) => - SOME (TT, model, args) - (* redundant, since 'False' is also an IDT constructor *) - | Const (@{const_name False}, _) => - SOME (FF, model, args) - | Const (@{const_name All}, _) $ t1 => (* similar to "all" (Pure) *) - let - val (i, m, a) = interpret ctxt model args t1 - in - case i of - Node xs => - (* 3-valued logic *) - let - val fmTrue = Prop_Logic.all (map toTrue xs) - val fmFalse = Prop_Logic.exists (map toFalse xs) - in - SOME (Leaf [fmTrue, fmFalse], m, a) - end - | _ => - raise REFUTE ("HOLogic_interpreter", - "\"All\" is followed by a non-function") - end - | Const (@{const_name All}, _) => - SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name Ex}, _) $ t1 => - let - val (i, m, a) = interpret ctxt model args t1 - in - case i of - Node xs => - (* 3-valued logic *) - let - val fmTrue = Prop_Logic.exists (map toTrue xs) - val fmFalse = Prop_Logic.all (map toFalse xs) - in - SOME (Leaf [fmTrue, fmFalse], m, a) - end - | _ => - raise REFUTE ("HOLogic_interpreter", - "\"Ex\" is followed by a non-function") - end - | Const (@{const_name Ex}, _) => - SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *) - let - val (i1, m1, a1) = interpret ctxt model args t1 - val (i2, m2, a2) = interpret ctxt m1 a1 t2 - in - SOME (make_equality (i1, i2), m2, a2) - end - | Const (@{const_name HOL.eq}, _) $ _ => - SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name HOL.eq}, _) => - SOME (interpret ctxt model args (eta_expand t 2)) - | Const (@{const_name HOL.conj}, _) $ t1 $ t2 => - (* 3-valued logic *) - let - val (i1, m1, a1) = interpret ctxt model args t1 - val (i2, m2, a2) = interpret ctxt m1 a1 t2 - val fmTrue = Prop_Logic.SAnd (toTrue i1, toTrue i2) - val fmFalse = Prop_Logic.SOr (toFalse i1, toFalse i2) - in - SOME (Leaf [fmTrue, fmFalse], m2, a2) - end - | Const (@{const_name HOL.conj}, _) $ _ => - SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name HOL.conj}, _) => - SOME (interpret ctxt model args (eta_expand t 2)) - (* this would make "undef" propagate, even for formulae like *) - (* "False & undef": *) - (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *) - | Const (@{const_name HOL.disj}, _) $ t1 $ t2 => - (* 3-valued logic *) - let - val (i1, m1, a1) = interpret ctxt model args t1 - val (i2, m2, a2) = interpret ctxt m1 a1 t2 - val fmTrue = Prop_Logic.SOr (toTrue i1, toTrue i2) - val fmFalse = Prop_Logic.SAnd (toFalse i1, toFalse i2) - in - SOME (Leaf [fmTrue, fmFalse], m2, a2) - end - | Const (@{const_name HOL.disj}, _) $ _ => - SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name HOL.disj}, _) => - SOME (interpret ctxt model args (eta_expand t 2)) - (* this would make "undef" propagate, even for formulae like *) - (* "True | undef": *) - (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *) - | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *) - (* 3-valued logic *) - let - val (i1, m1, a1) = interpret ctxt model args t1 - val (i2, m2, a2) = interpret ctxt m1 a1 t2 - val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2) - val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2) - in - SOME (Leaf [fmTrue, fmFalse], m2, a2) - end - | Const (@{const_name HOL.implies}, _) $ _ => - SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name HOL.implies}, _) => - SOME (interpret ctxt model args (eta_expand t 2)) - (* this would make "undef" propagate, even for formulae like *) - (* "False --> undef": *) - (* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *) - | _ => NONE; - -(* interprets variables and constants whose type is an IDT (this is *) -(* relatively easy and merely requires us to compute the size of the IDT); *) -(* constructors of IDTs however are properly interpreted by *) -(* 'IDT_constructor_interpreter' *) - -fun IDT_interpreter ctxt model args t = - let - val thy = Proof_Context.theory_of ctxt - val (typs, terms) = model - (* Term.typ -> (interpretation * model * arguments) option *) - fun interpret_term (Type (s, Ts)) = - (case Datatype.get_info thy s of - SOME info => (* inductive datatype *) - let - (* int option -- only recursive IDTs have an associated depth *) - val depth = AList.lookup (op =) typs (Type (s, Ts)) - (* sanity check: depth must be at least 0 *) - val _ = - (case depth of SOME n => - if n < 0 then - raise REFUTE ("IDT_interpreter", "negative depth") - else () - | _ => ()) - in - (* termination condition to avoid infinite recursion *) - if depth = (SOME 0) then - (* return a leaf of size 0 *) - SOME (Leaf [], model, args) - else - let - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) - val typ_assoc = dtyps ~~ Ts - (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) - val _ = - if Library.exists (fn d => - case d of Datatype.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_interpreter", - "datatype argument (for type " - ^ Syntax.string_of_typ ctxt (Type (s, Ts)) - ^ ") is not a variable") - else () - (* if the model specifies a depth for the current type, *) - (* decrement it to avoid infinite recursion *) - val typs' = case depth of NONE => typs | SOME n => - AList.update (op =) (Type (s, Ts), n-1) typs - (* recursively compute the size of the datatype *) - val size = size_of_dtyp ctxt typs' descr typ_assoc constrs - val next_idx = #next_idx args - val next = next_idx+size - (* check if 'maxvars' is large enough *) - val _ = (if next-1 > #maxvars args andalso - #maxvars args > 0 then raise MAXVARS_EXCEEDED else ()) - (* prop_formula list *) - val fms = map BoolVar (next_idx upto (next_idx+size-1)) - (* interpretation *) - val intr = Leaf fms - (* prop_formula list -> prop_formula *) - fun one_of_two_false [] = True - | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' => - SOr (SNot x, SNot x')) xs), one_of_two_false xs) - (* prop_formula *) - val wf = one_of_two_false fms - in - (* extend the model, increase 'next_idx', add well-formedness *) - (* condition *) - SOME (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, - def_eq = #def_eq args, next_idx = next, bounds = #bounds args, - wellformed = SAnd (#wellformed args, wf)}) - end - end - | NONE => (* not an inductive datatype *) - NONE) - | interpret_term _ = (* a (free or schematic) type variable *) - NONE - in - case AList.lookup (op =) terms t of - SOME intr => - (* return an existing interpretation *) - SOME (intr, model, args) - | NONE => - (case t of - Free (_, T) => interpret_term T - | Var (_, T) => interpret_term T - | Const (_, T) => interpret_term T - | _ => NONE) - end; - -(* This function imposes an order on the elements of a datatype fragment *) -(* as follows: C_i x_1 ... x_n < C_j y_1 ... y_m iff i < j or *) -(* (x_1, ..., x_n) < (y_1, ..., y_m). With this order, a constructor is *) -(* a function C_i that maps some argument indices x_1, ..., x_n to the *) -(* datatype element given by index C_i x_1 ... x_n. The idea remains the *) -(* same for recursive datatypes, although the computation of indices gets *) -(* a little tricky. *) - -fun IDT_constructor_interpreter ctxt model args t = - let - val thy = Proof_Context.theory_of ctxt - (* returns a list of canonical representations for terms of the type 'T' *) - (* It would be nice if we could just use 'print' for this, but 'print' *) - (* for IDTs calls 'IDT_constructor_interpreter' again, and this could *) - (* lead to infinite recursion when we have (mutually) recursive IDTs. *) - (* (Term.typ * int) list -> Term.typ -> Term.term list *) - fun canonical_terms typs T = - (case T of - Type ("fun", [T1, T2]) => - (* 'T2' might contain a recursive IDT, so we cannot use 'print' (at *) - (* least not for 'T2' *) - let - (* returns a list of lists, each one consisting of n (possibly *) - (* identical) elements from 'xs' *) - (* int -> 'a list -> 'a list list *) - fun pick_all 1 xs = map single xs - | pick_all n xs = - let val rec_pick = pick_all (n-1) xs in - maps (fn x => map (cons x) rec_pick) xs - end - (* ["x1", ..., "xn"] *) - val terms1 = canonical_terms typs T1 - (* ["y1", ..., "ym"] *) - val terms2 = canonical_terms typs T2 - (* [[("x1", "y1"), ..., ("xn", "y1")], ..., *) - (* [("x1", "ym"), ..., ("xn", "ym")]] *) - val functions = map (curry (op ~~) terms1) - (pick_all (length terms1) terms2) - (* [["(x1, y1)", ..., "(xn, y1)"], ..., *) - (* ["(x1, ym)", ..., "(xn, ym)"]] *) - val pairss = map (map HOLogic.mk_prod) functions - (* Term.typ *) - val HOLogic_prodT = HOLogic.mk_prodT (T1, T2) - val HOLogic_setT = HOLogic.mk_setT HOLogic_prodT - (* Term.term *) - val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT) - val HOLogic_insert = - Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) - in - (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *) - map (fn ps => fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) ps - HOLogic_empty_set) pairss - end - | Type (s, Ts) => - (case Datatype.get_info thy s of - SOME info => - (case AList.lookup (op =) typs T of - SOME 0 => - (* termination condition to avoid infinite recursion *) - [] (* at depth 0, every IDT is empty *) - | _ => - let - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) - val typ_assoc = dtyps ~~ Ts - (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) - val _ = - if Library.exists (fn d => - case d of Datatype.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_constructor_interpreter", - "datatype argument (for type " - ^ Syntax.string_of_typ ctxt T - ^ ") is not a variable") - else () - (* decrement depth for the IDT 'T' *) - val typs' = - (case AList.lookup (op =) typs T of NONE => typs - | SOME n => AList.update (op =) (T, n-1) typs) - fun constructor_terms terms [] = terms - | constructor_terms terms (d::ds) = - let - val dT = typ_of_dtyp descr typ_assoc d - val d_terms = canonical_terms typs' dT - in - (* C_i x_1 ... x_n < C_i y_1 ... y_n if *) - (* (x_1, ..., x_n) < (y_1, ..., y_n) *) - constructor_terms - (map_product (curry op $) terms d_terms) ds - end - in - (* C_i ... < C_j ... if i < j *) - maps (fn (cname, ctyps) => - let - val cTerm = Const (cname, - map (typ_of_dtyp descr typ_assoc) ctyps ---> T) - in - constructor_terms [cTerm] ctyps - end) constrs - end) - | NONE => - (* not an inductive datatype; in this case the argument types in *) - (* 'Ts' may not be IDTs either, so 'print' should be safe *) - map (fn intr => print ctxt (typs, []) T intr (K false)) - (make_constants ctxt (typs, []) T)) - | _ => (* TFree ..., TVar ... *) - map (fn intr => print ctxt (typs, []) T intr (K false)) - (make_constants ctxt (typs, []) T)) - val (typs, terms) = model - in - case AList.lookup (op =) terms t of - SOME intr => - (* return an existing interpretation *) - SOME (intr, model, args) - | NONE => - (case t of - Const (s, T) => - (case body_type T of - Type (s', Ts') => - (case Datatype.get_info thy s' of - SOME info => (* body type is an inductive datatype *) - let - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) - val typ_assoc = dtyps ~~ Ts' - (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) - val _ = if Library.exists (fn d => - case d of Datatype.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_constructor_interpreter", - "datatype argument (for type " - ^ Syntax.string_of_typ ctxt (Type (s', Ts')) - ^ ") is not a variable") - else () - (* split the constructors into those occuring before/after *) - (* 'Const (s, T)' *) - val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) => - not (cname = s andalso Sign.typ_instance thy (T, - map (typ_of_dtyp descr typ_assoc) ctypes - ---> Type (s', Ts')))) constrs - in - case constrs2 of - [] => - (* 'Const (s, T)' is not a constructor of this datatype *) - NONE - | (_, ctypes)::_ => - let - (* int option -- only /recursive/ IDTs have an associated *) - (* depth *) - val depth = AList.lookup (op =) typs (Type (s', Ts')) - (* this should never happen: at depth 0, this IDT fragment *) - (* is definitely empty, and in this case we don't need to *) - (* interpret its constructors *) - val _ = (case depth of SOME 0 => - raise REFUTE ("IDT_constructor_interpreter", - "depth is 0") - | _ => ()) - val typs' = (case depth of NONE => typs | SOME n => - AList.update (op =) (Type (s', Ts'), n-1) typs) - (* elements of the datatype come before elements generated *) - (* by 'Const (s, T)' iff they are generated by a *) - (* constructor in constrs1 *) - val offset = size_of_dtyp ctxt typs' descr typ_assoc constrs1 - (* compute the total (current) size of the datatype *) - val total = offset + - size_of_dtyp ctxt typs' descr typ_assoc constrs2 - (* sanity check *) - val _ = if total <> size_of_type ctxt (typs, []) - (Type (s', Ts')) then - raise REFUTE ("IDT_constructor_interpreter", - "total is not equal to current size") - else () - (* returns an interpretation where everything is mapped to *) - (* an "undefined" element of the datatype *) - fun make_undef [] = Leaf (replicate total False) - | make_undef (d::ds) = - let - (* compute the current size of the type 'd' *) - val dT = typ_of_dtyp descr typ_assoc d - val size = size_of_type ctxt (typs, []) dT - in - Node (replicate size (make_undef ds)) - end - (* returns the interpretation for a constructor *) - fun make_constr [] offset = - if offset < total then - (Leaf (replicate offset False @ True :: - (replicate (total - offset - 1) False)), offset + 1) - else - raise REFUTE ("IDT_constructor_interpreter", - "offset >= total") - | make_constr (d::ds) offset = - let - (* Term.typ *) - val dT = typ_of_dtyp descr typ_assoc d - (* compute canonical term representations for all *) - (* elements of the type 'd' (with the reduced depth *) - (* for the IDT) *) - val terms' = canonical_terms typs' dT - (* sanity check *) - val _ = - if length terms' <> size_of_type ctxt (typs', []) dT - then - raise REFUTE ("IDT_constructor_interpreter", - "length of terms' is not equal to old size") - else () - (* compute canonical term representations for all *) - (* elements of the type 'd' (with the current depth *) - (* for the IDT) *) - val terms = canonical_terms typs dT - (* sanity check *) - val _ = - if length terms <> size_of_type ctxt (typs, []) dT - then - raise REFUTE ("IDT_constructor_interpreter", - "length of terms is not equal to current size") - else () - (* sanity check *) - val _ = - if length terms < length terms' then - raise REFUTE ("IDT_constructor_interpreter", - "current size is less than old size") - else () - (* sanity check: every element of terms' must also be *) - (* present in terms *) - val _ = - if forall (member (op =) terms) terms' then () - else - raise REFUTE ("IDT_constructor_interpreter", - "element has disappeared") - (* sanity check: the order on elements of terms' is *) - (* the same in terms, for those elements *) - val _ = - let - fun search (x::xs) (y::ys) = - if x = y then search xs ys else search (x::xs) ys - | search (_::_) [] = - raise REFUTE ("IDT_constructor_interpreter", - "element order not preserved") - | search [] _ = () - in search terms' terms end - (* int * interpretation list *) - val (intrs, new_offset) = - fold_map (fn t_elem => fn off => - (* if 't_elem' existed at the previous depth, *) - (* proceed recursively, otherwise map the entire *) - (* subtree to "undefined" *) - if member (op =) terms' t_elem then - make_constr ds off - else - (make_undef ds, off)) - terms offset - in - (Node intrs, new_offset) - end - in - SOME (fst (make_constr ctypes offset), model, args) - end - end - | NONE => (* body type is not an inductive datatype *) - NONE) - | _ => (* body type is a (free or schematic) type variable *) - NONE) - | _ => (* term is not a constant *) - NONE) - end; - -(* Difficult code ahead. Make sure you understand the *) -(* 'IDT_constructor_interpreter' and the order in which it enumerates *) -(* elements of an IDT before you try to understand this function. *) - -fun IDT_recursion_interpreter ctxt model args t = - let - val thy = Proof_Context.theory_of ctxt - in - (* careful: here we descend arbitrarily deep into 't', possibly before *) - (* any other interpreter for atomic terms has had a chance to look at *) - (* 't' *) - case strip_comb t of - (Const (s, T), params) => - (* iterate over all datatypes in 'thy' *) - Symtab.fold (fn (_, info) => fn result => - case result of - SOME _ => - result (* just keep 'result' *) - | NONE => - if member (op =) (#rec_names info) s then - (* we do have a recursion operator of one of the (mutually *) - (* recursive) datatypes given by 'info' *) - let - (* number of all constructors, including those of different *) - (* (mutually recursive) datatypes within the same descriptor *) - val mconstrs_count = - Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info)) - in - if mconstrs_count < length params then - (* too many actual parameters; for now we'll use the *) - (* 'stlc_interpreter' to strip off one application *) - NONE - else if mconstrs_count > length params then - (* too few actual parameters; we use eta expansion *) - (* Note that the resulting expansion of lambda abstractions *) - (* by the 'stlc_interpreter' may be rather slow (depending *) - (* on the argument types and the size of the IDT, of *) - (* course). *) - SOME (interpret ctxt model args (eta_expand t - (mconstrs_count - length params))) - else (* mconstrs_count = length params *) - let - (* interpret each parameter separately *) - val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) => - let - val (i, m', a') = interpret ctxt m a p - in - (i, (m', a')) - end) params (model, args) - val (typs, _) = model' - (* 'index' is /not/ necessarily the index of the IDT that *) - (* the recursion operator is associated with, but merely *) - (* the index of some mutually recursive IDT *) - val index = #index info - val descr = #descr info - val (_, dtyps, _) = the (AList.lookup (op =) descr index) - (* sanity check: we assume that the order of constructors *) - (* in 'descr' is the same as the order of *) - (* corresponding parameters, otherwise the *) - (* association code below won't match the *) - (* right constructors/parameters; we also *) - (* assume that the order of recursion *) - (* operators in '#rec_names info' is the *) - (* same as the order of corresponding *) - (* datatypes in 'descr' *) - val _ = if map fst descr <> (0 upto (length descr - 1)) then - raise REFUTE ("IDT_recursion_interpreter", - "order of constructors and corresponding parameters/" ^ - "recursion operators and corresponding datatypes " ^ - "different?") - else () - (* sanity check: every element in 'dtyps' must be a *) - (* 'DtTFree' *) - val _ = - if Library.exists (fn d => - case d of Datatype.DtTFree _ => false - | _ => true) dtyps - then - raise REFUTE ("IDT_recursion_interpreter", - "datatype argument is not a variable") - else () - (* the type of a recursion operator is *) - (* [T1, ..., Tn, IDT] ---> Tresult *) - val IDT = nth (binder_types T) mconstrs_count - (* by our assumption on the order of recursion operators *) - (* and datatypes, this is the index of the datatype *) - (* corresponding to the given recursion operator *) - val idt_index = find_index (fn s' => s' = s) (#rec_names info) - (* mutually recursive types must have the same type *) - (* parameters, unless the mutual recursion comes from *) - (* indirect recursion *) - fun rec_typ_assoc acc [] = acc - | rec_typ_assoc acc ((d, T)::xs) = - (case AList.lookup op= acc d of - NONE => - (case d of - Datatype.DtTFree _ => - (* add the association, proceed *) - rec_typ_assoc ((d, T)::acc) xs - | Datatype.DtType (s, ds) => - let - val (s', Ts) = dest_Type T - in - if s=s' then - rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) - else - raise REFUTE ("IDT_recursion_interpreter", - "DtType/Type mismatch") - end - | Datatype.DtRec i => - let - val (_, ds, _) = the (AList.lookup (op =) descr i) - val (_, Ts) = dest_Type T - in - rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) - end) - | SOME T' => - if T=T' then - (* ignore the association since it's already *) - (* present, proceed *) - rec_typ_assoc acc xs - else - raise REFUTE ("IDT_recursion_interpreter", - "different type associations for the same dtyp")) - val typ_assoc = filter - (fn (Datatype.DtTFree _, _) => true | (_, _) => false) - (rec_typ_assoc [] - (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT)) - (* sanity check: typ_assoc must associate types to the *) - (* elements of 'dtyps' (and only to those) *) - val _ = - if not (eq_set (op =) (dtyps, map fst typ_assoc)) - then - raise REFUTE ("IDT_recursion_interpreter", - "type association has extra/missing elements") - else () - (* interpret each constructor in the descriptor (including *) - (* those of mutually recursive datatypes) *) - (* (int * interpretation list) list *) - val mc_intrs = map (fn (idx, (_, _, cs)) => - let - val c_return_typ = typ_of_dtyp descr typ_assoc - (Datatype.DtRec idx) - in - (idx, map (fn (cname, cargs) => - (#1 o interpret ctxt (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], - wellformed=True}) (Const (cname, map (typ_of_dtyp - descr typ_assoc) cargs ---> c_return_typ))) cs) - end) descr - (* associate constructors with corresponding parameters *) - (* (int * (interpretation * interpretation) list) list *) - val (mc_p_intrs, p_intrs') = fold_map - (fn (idx, c_intrs) => fn p_intrs' => - let - val len = length c_intrs - in - ((idx, c_intrs ~~ List.take (p_intrs', len)), - List.drop (p_intrs', len)) - end) mc_intrs p_intrs - (* sanity check: no 'p_intr' may be left afterwards *) - val _ = - if p_intrs' <> [] then - raise REFUTE ("IDT_recursion_interpreter", - "more parameter than constructor interpretations") - else () - (* The recursion operator, applied to 'mconstrs_count' *) - (* arguments, is a function that maps every element of the *) - (* inductive datatype to an element of some result type. *) - (* Recursion operators for mutually recursive IDTs are *) - (* translated simultaneously. *) - (* Since the order on datatype elements is given by an *) - (* order on constructors (and then by the order on *) - (* argument tuples), we can simply copy corresponding *) - (* subtrees from 'p_intrs', in the order in which they are *) - (* given. *) - (* interpretation * interpretation -> interpretation list *) - fun ci_pi (Leaf xs, pi) = - (* if the constructor does not match the arguments to a *) - (* defined element of the IDT, the corresponding value *) - (* of the parameter must be ignored *) - if List.exists (equal True) xs then [pi] else [] - | ci_pi (Node xs, Node ys) = maps ci_pi (xs ~~ ys) - | ci_pi (Node _, Leaf _) = - raise REFUTE ("IDT_recursion_interpreter", - "constructor takes more arguments than the " ^ - "associated parameter") - (* (int * interpretation list) list *) - val rec_operators = map (fn (idx, c_p_intrs) => - (idx, maps ci_pi c_p_intrs)) mc_p_intrs - (* sanity check: every recursion operator must provide as *) - (* many values as the corresponding datatype *) - (* has elements *) - val _ = map (fn (idx, intrs) => - let - val T = typ_of_dtyp descr typ_assoc - (Datatype.DtRec idx) - in - if length intrs <> size_of_type ctxt (typs, []) T then - raise REFUTE ("IDT_recursion_interpreter", - "wrong number of interpretations for rec. operator") - else () - end) rec_operators - (* For non-recursive datatypes, we are pretty much done at *) - (* this point. For recursive datatypes however, we still *) - (* need to apply the interpretations in 'rec_operators' to *) - (* (recursively obtained) interpretations for recursive *) - (* constructor arguments. To do so more efficiently, we *) - (* copy 'rec_operators' into arrays first. Each Boolean *) - (* indicates whether the recursive arguments have been *) - (* considered already. *) - (* (int * (bool * interpretation) Array.array) list *) - val REC_OPERATORS = map (fn (idx, intrs) => - (idx, Array.fromList (map (pair false) intrs))) - rec_operators - (* takes an interpretation, and if some leaf of this *) - (* interpretation is the 'elem'-th element of the type, *) - (* the indices of the arguments leading to this leaf are *) - (* returned *) - (* interpretation -> int -> int list option *) - fun get_args (Leaf xs) elem = - if find_index (fn x => x = True) xs = elem then - SOME [] - else - NONE - | get_args (Node xs) elem = - let - (* interpretation list * int -> int list option *) - fun search ([], _) = - NONE - | search (x::xs, n) = - (case get_args x elem of - SOME result => SOME (n::result) - | NONE => search (xs, n+1)) - in - search (xs, 0) - end - (* returns the index of the constructor and indices for *) - (* its arguments that generate the 'elem'-th element of *) - (* the datatype given by 'idx' *) - (* int -> int -> int * int list *) - fun get_cargs idx elem = - let - (* int * interpretation list -> int * int list *) - fun get_cargs_rec (_, []) = - raise REFUTE ("IDT_recursion_interpreter", - "no matching constructor found for datatype element") - | get_cargs_rec (n, x::xs) = - (case get_args x elem of - SOME args => (n, args) - | NONE => get_cargs_rec (n+1, xs)) - in - get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx)) - end - (* computes one entry in 'REC_OPERATORS', and recursively *) - (* all entries needed for it, where 'idx' gives the *) - (* datatype and 'elem' the element of it *) - (* int -> int -> interpretation *) - fun compute_array_entry idx elem = - let - val arr = the (AList.lookup (op =) REC_OPERATORS idx) - val (flag, intr) = Array.sub (arr, elem) - in - if flag then - (* simply return the previously computed result *) - intr - else - (* we have to apply 'intr' to interpretations for all *) - (* recursive arguments *) - let - (* int * int list *) - val (c, args) = get_cargs idx elem - (* find the indices of the constructor's /recursive/ *) - (* arguments *) - val (_, _, constrs) = the (AList.lookup (op =) descr idx) - val (_, dtyps) = nth constrs c - val rec_dtyps_args = filter - (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args) - (* map those indices to interpretations *) - val rec_dtyps_intrs = map (fn (dtyp, arg) => - let - val dT = typ_of_dtyp descr typ_assoc dtyp - val consts = make_constants ctxt (typs, []) dT - val arg_i = nth consts arg - in - (dtyp, arg_i) - end) rec_dtyps_args - (* takes the dtyp and interpretation of an element, *) - (* and computes the interpretation for the *) - (* corresponding recursive argument *) - fun rec_intr (Datatype.DtRec i) (Leaf xs) = - (* recursive argument is "rec_i params elem" *) - compute_array_entry i (find_index (fn x => x = True) xs) - | rec_intr (Datatype.DtRec _) (Node _) = - raise REFUTE ("IDT_recursion_interpreter", - "interpretation for IDT is a node") - | rec_intr (Datatype.DtType ("fun", [_, dt2])) (Node xs) = - (* recursive argument is something like *) - (* "\x::dt1. rec_? params (elem x)" *) - Node (map (rec_intr dt2) xs) - | rec_intr (Datatype.DtType ("fun", [_, _])) (Leaf _) = - raise REFUTE ("IDT_recursion_interpreter", - "interpretation for function dtyp is a leaf") - | rec_intr _ _ = - (* admissibility ensures that every recursive type *) - (* is of the form 'Dt_1 -> ... -> Dt_k -> *) - (* (DtRec i)' *) - raise REFUTE ("IDT_recursion_interpreter", - "non-recursive codomain in recursive dtyp") - (* obtain interpretations for recursive arguments *) - (* interpretation list *) - val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs - (* apply 'intr' to all recursive arguments *) - val result = fold (fn arg_i => fn i => - interpretation_apply (i, arg_i)) arg_intrs intr - (* update 'REC_OPERATORS' *) - val _ = Array.update (arr, elem, (true, result)) - in - result - end - end - val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index)) - (* sanity check: the size of 'IDT' should be 'idt_size' *) - val _ = - if idt_size <> size_of_type ctxt (typs, []) IDT then - raise REFUTE ("IDT_recursion_interpreter", - "unexpected size of IDT (wrong type associated?)") - else () - (* interpretation *) - val rec_op = Node (map_range (compute_array_entry idt_index) idt_size) - in - SOME (rec_op, model', args') - end - end - else - NONE (* not a recursion operator of this datatype *) - ) (Datatype.get_all thy) NONE - | _ => (* head of term is not a constant *) - NONE - end; - -fun set_interpreter ctxt model args t = - let - val (typs, terms) = model - in - case AList.lookup (op =) terms t of - SOME intr => - (* return an existing interpretation *) - SOME (intr, model, args) - | NONE => - (case t of - Free (x, Type (@{type_name set}, [T])) => - let - val (intr, _, args') = - interpret ctxt (typs, []) args (Free (x, T --> HOLogic.boolT)) - in - SOME (intr, (typs, (t, intr)::terms), args') - end - | Var ((x, i), Type (@{type_name set}, [T])) => - let - val (intr, _, args') = - interpret ctxt (typs, []) args (Var ((x,i), T --> HOLogic.boolT)) - in - SOME (intr, (typs, (t, intr)::terms), args') - end - | Const (s, Type (@{type_name set}, [T])) => - let - val (intr, _, args') = - interpret ctxt (typs, []) args (Const (s, T --> HOLogic.boolT)) - in - SOME (intr, (typs, (t, intr)::terms), args') - end - (* 'Collect' == identity *) - | Const (@{const_name Collect}, _) $ t1 => - SOME (interpret ctxt model args t1) - | Const (@{const_name Collect}, _) => - SOME (interpret ctxt model args (eta_expand t 1)) - (* 'op :' == application *) - | Const (@{const_name Set.member}, _) $ t1 $ t2 => - SOME (interpret ctxt model args (t2 $ t1)) - | Const (@{const_name Set.member}, _) $ _ => - SOME (interpret ctxt model args (eta_expand t 1)) - | Const (@{const_name Set.member}, _) => - SOME (interpret ctxt model args (eta_expand t 2)) - | _ => NONE) - end; - -(* only an optimization: 'card' could in principle be interpreted with *) -(* interpreters available already (using its definition), but the code *) -(* below is more efficient *) - -fun Finite_Set_card_interpreter ctxt model args t = - case t of - Const (@{const_name Finite_Set.card}, - Type ("fun", [Type (@{type_name set}, [T]), @{typ nat}])) => - let - (* interpretation -> int *) - fun number_of_elements (Node xs) = - fold (fn x => fn n => - if x = TT then - n + 1 - else if x = FF then - n - else - raise REFUTE ("Finite_Set_card_interpreter", - "interpretation for set type does not yield a Boolean")) - xs 0 - | number_of_elements (Leaf _) = - raise REFUTE ("Finite_Set_card_interpreter", - "interpretation for set type is a leaf") - val size_of_nat = size_of_type ctxt model (@{typ nat}) - (* takes an interpretation for a set and returns an interpretation *) - (* for a 'nat' denoting the set's cardinality *) - (* interpretation -> interpretation *) - fun card i = - let - val n = number_of_elements i - in - if n < size_of_nat then - Leaf ((replicate n False) @ True :: - (replicate (size_of_nat-n-1) False)) - else - Leaf (replicate size_of_nat False) - end - val set_constants = make_constants ctxt model (HOLogic.mk_setT T) - in - SOME (Node (map card set_constants), model, args) - end - | _ => NONE; - -(* only an optimization: 'finite' could in principle be interpreted with *) -(* interpreters available already (using its definition), but the code *) -(* below is more efficient *) - -fun Finite_Set_finite_interpreter ctxt model args t = - case t of - Const (@{const_name Finite_Set.finite}, - Type ("fun", [_, @{typ bool}])) $ _ => - (* we only consider finite models anyway, hence EVERY set is *) - (* "finite" *) - SOME (TT, model, args) - | Const (@{const_name Finite_Set.finite}, - Type ("fun", [set_T, @{typ bool}])) => - let - val size_of_set = size_of_type ctxt model set_T - in - (* we only consider finite models anyway, hence EVERY set is *) - (* "finite" *) - SOME (Node (replicate size_of_set TT), model, args) - end - | _ => NONE; - -(* only an optimization: 'less' could in principle be interpreted with *) -(* interpreters available already (using its definition), but the code *) -(* below is more efficient *) - -fun Nat_less_interpreter ctxt model args t = - case t of - Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, @{typ bool}])])) => - let - val size_of_nat = size_of_type ctxt model (@{typ nat}) - (* the 'n'-th nat is not less than the first 'n' nats, while it *) - (* is less than the remaining 'size_of_nat - n' nats *) - (* int -> interpretation *) - fun less n = Node ((replicate n FF) @ (replicate (size_of_nat - n) TT)) - in - SOME (Node (map less (1 upto size_of_nat)), model, args) - end - | _ => NONE; - -(* only an optimization: 'plus' could in principle be interpreted with *) -(* interpreters available already (using its definition), but the code *) -(* below is more efficient *) - -fun Nat_plus_interpreter ctxt model args t = - case t of - Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, @{typ nat}])])) => - let - val size_of_nat = size_of_type ctxt model (@{typ nat}) - (* int -> int -> interpretation *) - fun plus m n = - let - val element = m + n - in - if element > size_of_nat - 1 then - Leaf (replicate size_of_nat False) - else - Leaf ((replicate element False) @ True :: - (replicate (size_of_nat - element - 1) False)) - end - in - SOME (Node (map_range (fn m => Node (map_range (plus m) size_of_nat)) size_of_nat), - model, args) - end - | _ => NONE; - -(* only an optimization: 'minus' could in principle be interpreted *) -(* with interpreters available already (using its definition), but the *) -(* code below is more efficient *) - -fun Nat_minus_interpreter ctxt model args t = - case t of - Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, @{typ nat}])])) => - let - val size_of_nat = size_of_type ctxt model (@{typ nat}) - (* int -> int -> interpretation *) - fun minus m n = - let - val element = Int.max (m-n, 0) - in - Leaf ((replicate element False) @ True :: - (replicate (size_of_nat - element - 1) False)) - end - in - SOME (Node (map_range (fn m => Node (map_range (minus m) size_of_nat)) size_of_nat), - model, args) - end - | _ => NONE; - -(* only an optimization: 'times' could in principle be interpreted *) -(* with interpreters available already (using its definition), but the *) -(* code below is more efficient *) - -fun Nat_times_interpreter ctxt model args t = - case t of - Const (@{const_name Groups.times}, Type ("fun", [@{typ nat}, - Type ("fun", [@{typ nat}, @{typ nat}])])) => - let - val size_of_nat = size_of_type ctxt model (@{typ nat}) - (* nat -> nat -> interpretation *) - fun mult m n = - let - val element = m * n - in - if element > size_of_nat - 1 then - Leaf (replicate size_of_nat False) - else - Leaf ((replicate element False) @ True :: - (replicate (size_of_nat - element - 1) False)) - end - in - SOME (Node (map_range (fn m => Node (map_range (mult m) size_of_nat)) size_of_nat), - model, args) - end - | _ => NONE; - -(* only an optimization: 'append' could in principle be interpreted with *) -(* interpreters available already (using its definition), but the code *) -(* below is more efficient *) - -fun List_append_interpreter ctxt model args t = - case t of - Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun", - [Type ("List.list", [_]), Type ("List.list", [_])])])) => - let - val size_elem = size_of_type ctxt model T - val size_list = size_of_type ctxt model (Type ("List.list", [T])) - (* maximal length of lists; 0 if we only consider the empty list *) - val list_length = - let - (* int -> int -> int -> int *) - fun list_length_acc len lists total = - if lists = total then - len - else if lists < total then - list_length_acc (len+1) (lists*size_elem) (total-lists) - else - raise REFUTE ("List_append_interpreter", - "size_list not equal to 1 + size_elem + ... + " ^ - "size_elem^len, for some len") - in - list_length_acc 0 1 size_list - end - val elements = 0 upto (size_list-1) - (* FIXME: there should be a nice formula, which computes the same as *) - (* the following, but without all this intermediate tree *) - (* length/offset stuff *) - (* associate each list with its length and offset in a complete tree *) - (* of width 'size_elem' and depth 'length_list' (with 'size_list' *) - (* nodes total) *) - (* (int * (int * int)) list *) - val (lenoff_lists, _) = fold_map (fn elem => fn (offsets, off) => - (* corresponds to a pre-order traversal of the tree *) - let - val len = length offsets - (* associate the given element with len/off *) - val assoc = (elem, (len, off)) - in - if len < list_length then - (* go to first child node *) - (assoc, (off :: offsets, off * size_elem)) - else if off mod size_elem < size_elem - 1 then - (* go to next sibling node *) - (assoc, (offsets, off + 1)) - else - (* go back up the stack until we find a level where we can go *) - (* to the next sibling node *) - let - val offsets' = snd (take_prefix - (fn off' => off' mod size_elem = size_elem - 1) offsets) - in - case offsets' of - [] => - (* we're at the last node in the tree; the next value *) - (* won't be used anyway *) - (assoc, ([], 0)) - | off'::offs' => - (* go to next sibling node *) - (assoc, (offs', off' + 1)) - end - end) elements ([], 0) - (* we also need the reverse association (from length/offset to *) - (* index) *) - val lenoff'_lists = map Library.swap lenoff_lists - (* returns the interpretation for "(list no. m) @ (list no. n)" *) - (* nat -> nat -> interpretation *) - fun append m n = - let - val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m) - val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n) - val len_elem = len_m + len_n - val off_elem = off_m * Integer.pow len_n size_elem + off_n - in - case AList.lookup op= lenoff'_lists (len_elem, off_elem) of - NONE => - (* undefined *) - Leaf (replicate size_list False) - | SOME element => - Leaf ((replicate element False) @ True :: - (replicate (size_list - element - 1) False)) - end - in - SOME (Node (map (fn m => Node (map (append m) elements)) elements), - model, args) - end - | _ => NONE; - -(* only an optimization: 'lfp' could in principle be interpreted with *) -(* interpreters available already (using its definition), but the code *) -(* below is more efficient *) - -fun lfp_interpreter ctxt model args t = - case t of - Const (@{const_name lfp}, Type ("fun", [Type ("fun", - [Type (@{type_name set}, [T]), - Type (@{type_name set}, [_])]), - Type (@{type_name set}, [_])])) => - let - val size_elem = size_of_type ctxt model T - (* the universe (i.e. the set that contains every element) *) - val i_univ = Node (replicate size_elem TT) - (* all sets with elements from type 'T' *) - val i_sets = make_constants ctxt model (HOLogic.mk_setT T) - (* all functions that map sets to sets *) - val i_funs = make_constants ctxt model (Type ("fun", - [HOLogic.mk_setT T, HOLogic.mk_setT T])) - (* "lfp(f) == Inter({u. f(u) <= u})" *) - (* interpretation * interpretation -> bool *) - fun is_subset (Node subs, Node sups) = - forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups) - | is_subset (_, _) = - raise REFUTE ("lfp_interpreter", - "is_subset: interpretation for set is not a node") - (* interpretation * interpretation -> interpretation *) - fun intersection (Node xs, Node ys) = - Node (map (fn (x, y) => if x=TT andalso y=TT then TT else FF) - (xs ~~ ys)) - | intersection (_, _) = - raise REFUTE ("lfp_interpreter", - "intersection: interpretation for set is not a node") - (* interpretation -> interpretaion *) - fun lfp (Node resultsets) = - fold (fn (set, resultset) => fn acc => - if is_subset (resultset, set) then - intersection (acc, set) - else - acc) (i_sets ~~ resultsets) i_univ - | lfp _ = - raise REFUTE ("lfp_interpreter", - "lfp: interpretation for function is not a node") - in - SOME (Node (map lfp i_funs), model, args) - end - | _ => NONE; - -(* only an optimization: 'gfp' could in principle be interpreted with *) -(* interpreters available already (using its definition), but the code *) -(* below is more efficient *) - -fun gfp_interpreter ctxt model args t = - case t of - Const (@{const_name gfp}, Type ("fun", [Type ("fun", - [Type (@{type_name set}, [T]), - Type (@{type_name set}, [_])]), - Type (@{type_name set}, [_])])) => - let - val size_elem = size_of_type ctxt model T - (* the universe (i.e. the set that contains every element) *) - val i_univ = Node (replicate size_elem TT) - (* all sets with elements from type 'T' *) - val i_sets = make_constants ctxt model (HOLogic.mk_setT T) - (* all functions that map sets to sets *) - val i_funs = make_constants ctxt model (Type ("fun", - [HOLogic.mk_setT T, HOLogic.mk_setT T])) - (* "gfp(f) == Union({u. u <= f(u)})" *) - (* interpretation * interpretation -> bool *) - fun is_subset (Node subs, Node sups) = - forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) - (subs ~~ sups) - | is_subset (_, _) = - raise REFUTE ("gfp_interpreter", - "is_subset: interpretation for set is not a node") - (* interpretation * interpretation -> interpretation *) - fun union (Node xs, Node ys) = - Node (map (fn (x,y) => if x=TT orelse y=TT then TT else FF) - (xs ~~ ys)) - | union (_, _) = - raise REFUTE ("gfp_interpreter", - "union: interpretation for set is not a node") - (* interpretation -> interpretaion *) - fun gfp (Node resultsets) = - fold (fn (set, resultset) => fn acc => - if is_subset (set, resultset) then - union (acc, set) - else - acc) (i_sets ~~ resultsets) i_univ - | gfp _ = - raise REFUTE ("gfp_interpreter", - "gfp: interpretation for function is not a node") - in - SOME (Node (map gfp i_funs), model, args) - end - | _ => NONE; - -(* only an optimization: 'fst' could in principle be interpreted with *) -(* interpreters available already (using its definition), but the code *) -(* below is more efficient *) - -fun Product_Type_fst_interpreter ctxt model args t = - case t of - Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => - let - val constants_T = make_constants ctxt model T - val size_U = size_of_type ctxt model U - in - SOME (Node (maps (replicate size_U) constants_T), model, args) - end - | _ => NONE; - -(* only an optimization: 'snd' could in principle be interpreted with *) -(* interpreters available already (using its definition), but the code *) -(* below is more efficient *) - -fun Product_Type_snd_interpreter ctxt model args t = - case t of - Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => - let - val size_T = size_of_type ctxt model T - val constants_U = make_constants ctxt model U - in - SOME (Node (flat (replicate size_T constants_U)), model, args) - end - | _ => NONE; - - -(* ------------------------------------------------------------------------- *) -(* PRINTERS *) -(* ------------------------------------------------------------------------- *) - -fun stlc_printer ctxt model T intr assignment = - let - (* string -> string *) - val strip_leading_quote = perhaps (try (unprefix "'")) - (* Term.typ -> string *) - fun string_of_typ (Type (s, _)) = s - | string_of_typ (TFree (x, _)) = strip_leading_quote x - | string_of_typ (TVar ((x,i), _)) = - strip_leading_quote x ^ string_of_int i - (* interpretation -> int *) - fun index_from_interpretation (Leaf xs) = - find_index (Prop_Logic.eval assignment) xs - | index_from_interpretation _ = - raise REFUTE ("stlc_printer", - "interpretation for ground type is not a leaf") - in - case T of - Type ("fun", [T1, T2]) => - let - (* create all constants of type 'T1' *) - val constants = make_constants ctxt model T1 - (* interpretation list *) - val results = - (case intr of - Node xs => xs - | _ => raise REFUTE ("stlc_printer", - "interpretation for function type is a leaf")) - (* Term.term list *) - val pairs = map (fn (arg, result) => - HOLogic.mk_prod - (print ctxt model T1 arg assignment, - print ctxt model T2 result assignment)) - (constants ~~ results) - (* Term.typ *) - val HOLogic_prodT = HOLogic.mk_prodT (T1, T2) - val HOLogic_setT = HOLogic.mk_setT HOLogic_prodT - (* Term.term *) - val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT) - val HOLogic_insert = - Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) - in - SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set) - end - | Type ("prop", []) => - (case index_from_interpretation intr of - ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT))) - | 0 => SOME (HOLogic.mk_Trueprop @{term True}) - | 1 => SOME (HOLogic.mk_Trueprop @{term False}) - | _ => raise REFUTE ("stlc_interpreter", - "illegal interpretation for a propositional value")) - | Type _ => - if index_from_interpretation intr = (~1) then - SOME (Const (@{const_name undefined}, T)) - else - SOME (Const (string_of_typ T ^ - string_of_int (index_from_interpretation intr), T)) - | TFree _ => - if index_from_interpretation intr = (~1) then - SOME (Const (@{const_name undefined}, T)) - else - SOME (Const (string_of_typ T ^ - string_of_int (index_from_interpretation intr), T)) - | TVar _ => - if index_from_interpretation intr = (~1) then - SOME (Const (@{const_name undefined}, T)) - else - SOME (Const (string_of_typ T ^ - string_of_int (index_from_interpretation intr), T)) - end; - -fun set_printer ctxt model T intr assignment = - (case T of - Type (@{type_name set}, [T1]) => - let - (* create all constants of type 'T1' *) - val constants = make_constants ctxt model T1 - (* interpretation list *) - val results = (case intr of - Node xs => xs - | _ => raise REFUTE ("set_printer", - "interpretation for set type is a leaf")) - (* Term.term list *) - val elements = List.mapPartial (fn (arg, result) => - case result of - Leaf [fmTrue, (* fmFalse *) _] => - if Prop_Logic.eval assignment fmTrue then - SOME (print ctxt model T1 arg assignment) - else (* if Prop_Logic.eval assignment fmFalse then *) - NONE - | _ => - raise REFUTE ("set_printer", - "illegal interpretation for a Boolean value")) - (constants ~~ results) - (* Term.typ *) - val HOLogic_setT1 = HOLogic.mk_setT T1 - (* Term.term *) - val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT1) - val HOLogic_insert = - Const (@{const_name insert}, T1 --> HOLogic_setT1 --> HOLogic_setT1) - in - SOME (Library.foldl (fn (acc, elem) => HOLogic_insert $ elem $ acc) - (HOLogic_empty_set, elements)) - end - | _ => - NONE); - -fun IDT_printer ctxt model T intr assignment = - let - val thy = Proof_Context.theory_of ctxt - in - (case T of - Type (s, Ts) => - (case Datatype.get_info thy s of - SOME info => (* inductive datatype *) - let - val (typs, _) = model - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) - val typ_assoc = dtyps ~~ Ts - (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) - val _ = - if Library.exists (fn d => - case d of Datatype.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_printer", "datatype argument (for type " ^ - Syntax.string_of_typ ctxt (Type (s, Ts)) ^ ") is not a variable") - else () - (* the index of the element in the datatype *) - val element = - (case intr of - Leaf xs => find_index (Prop_Logic.eval assignment) xs - | Node _ => raise REFUTE ("IDT_printer", - "interpretation is not a leaf")) - in - if element < 0 then - SOME (Const (@{const_name undefined}, Type (s, Ts))) - else - let - (* takes a datatype constructor, and if for some arguments this *) - (* constructor generates the datatype's element that is given by *) - (* 'element', returns the constructor (as a term) as well as the *) - (* indices of the arguments *) - fun get_constr_args (cname, cargs) = - let - val cTerm = Const (cname, - map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts)) - val (iC, _, _) = interpret ctxt (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm - (* interpretation -> int list option *) - fun get_args (Leaf xs) = - if find_index (fn x => x = True) xs = element then - SOME [] - else - NONE - | get_args (Node xs) = - let - (* interpretation * int -> int list option *) - fun search ([], _) = - NONE - | search (x::xs, n) = - (case get_args x of - SOME result => SOME (n::result) - | NONE => search (xs, n+1)) - in - search (xs, 0) - end - in - Option.map (fn args => (cTerm, cargs, args)) (get_args iC) - end - val (cTerm, cargs, args) = - (* we could speed things up by computing the correct *) - (* constructor directly (rather than testing all *) - (* constructors), based on the order in which constructors *) - (* generate elements of datatypes; the current implementation *) - (* of 'IDT_printer' however is independent of the internals *) - (* of 'IDT_constructor_interpreter' *) - (case get_first get_constr_args constrs of - SOME x => x - | NONE => raise REFUTE ("IDT_printer", - "no matching constructor found for element " ^ - string_of_int element)) - val argsTerms = map (fn (d, n) => - let - val dT = typ_of_dtyp descr typ_assoc d - (* we only need the n-th element of this list, so there *) - (* might be a more efficient implementation that does not *) - (* generate all constants *) - val consts = make_constants ctxt (typs, []) dT - in - print ctxt (typs, []) dT (nth consts n) assignment - end) (cargs ~~ args) - in - SOME (list_comb (cTerm, argsTerms)) - end - end - | NONE => (* not an inductive datatype *) - NONE) - | _ => (* a (free or schematic) type variable *) - NONE) - end; - - -(* ------------------------------------------------------------------------- *) -(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *) -(* structure *) -(* ------------------------------------------------------------------------- *) - -(* ------------------------------------------------------------------------- *) -(* Note: the interpreters and printers are used in reverse order; however, *) -(* an interpreter that can handle non-atomic terms ends up being *) -(* applied before the 'stlc_interpreter' breaks the term apart into *) -(* subterms that are then passed to other interpreters! *) -(* ------------------------------------------------------------------------- *) - -val setup = - add_interpreter "stlc" stlc_interpreter #> - add_interpreter "Pure" Pure_interpreter #> - add_interpreter "HOLogic" HOLogic_interpreter #> - add_interpreter "set" set_interpreter #> - add_interpreter "IDT" IDT_interpreter #> - add_interpreter "IDT_constructor" IDT_constructor_interpreter #> - add_interpreter "IDT_recursion" IDT_recursion_interpreter #> - add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #> - add_interpreter "Finite_Set.finite" Finite_Set_finite_interpreter #> - add_interpreter "Nat_Orderings.less" Nat_less_interpreter #> - add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #> - add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #> - add_interpreter "Nat_HOL.times" Nat_times_interpreter #> - add_interpreter "List.append" List_append_interpreter #> -(* UNSOUND - add_interpreter "lfp" lfp_interpreter #> - add_interpreter "gfp" gfp_interpreter #> -*) - add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #> - add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #> - add_printer "stlc" stlc_printer #> - add_printer "set" set_printer #> - add_printer "IDT" IDT_printer; - - - -(** outer syntax commands 'refute' and 'refute_params' **) - -(* argument parsing *) - -(*optional list of arguments of the form [name1=value1, name2=value2, ...]*) - -val scan_parm = Parse.name -- (Scan.optional (@{keyword "="} |-- Parse.name) "true") -val scan_parms = Scan.optional (@{keyword "["} |-- Parse.list scan_parm --| @{keyword "]"}) []; - - -(* 'refute' command *) - -val _ = - Outer_Syntax.improper_command @{command_spec "refute"} - "try to find a model that refutes a given subgoal" - (scan_parms -- Scan.optional Parse.nat 1 >> - (fn (parms, i) => - Toplevel.keep (fn state => - let - val ctxt = Toplevel.context_of state; - val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state); - in refute_goal ctxt parms st i; () end))); - - -(* 'refute_params' command *) - -val _ = - Outer_Syntax.command @{command_spec "refute_params"} - "show/store default parameters for the 'refute' command" - (scan_parms >> (fn parms => - Toplevel.theory (fn thy => - let - val thy' = fold set_default_param parms thy; - val output = - (case get_default_params (Proof_Context.init_global thy') of - [] => "none" - | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults)); - val _ = writeln ("Default parameters for 'refute':\n" ^ output); - in thy' end))); - -end; -