--- /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
--- /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<max orelse max<0) then
+ (* we can shift *)
+ SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
+ else
+ (* continue search *)
+ next max (len+1) (sum+x1) (x2::xs)
+ (* only consider those types for which the size is not fixed *)
+ val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs
+ (* subtract 'minsize' from every size (will be added again at the end) *)
+ val diffs = map (fn (_, n) => n-minsize) mutables
+ in
+ case next (maxsize-minsize) 0 0 diffs of
+ SOME diffs' =>
+ (* merge with those types for which the size is fixed *)
+ SOME (fst (fold_map (fn (T, _) => fn ds =>
+ case AList.lookup (op =) sizes (string_of_typ T) of
+ (* return the fixed size *)
+ SOME n => ((T, n), ds)
+ (* consume the head of 'ds', add 'minsize' *)
+ | NONE => ((T, minsize + hd ds), tl ds))
+ xs diffs'))
+ | NONE => NONE
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* toTrue: converts the interpretation of a Boolean value to a propositional *)
+(* formula that is true iff the interpretation denotes "true" *)
+(* ------------------------------------------------------------------------- *)
+
+(* 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 ("<eta_expand>", 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 *)
+ (* "\<lambda>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;
+
--- 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
--- 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
--- 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"
--- 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"
--- 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)
--- 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
--- 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
--- 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
--- 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<max orelse max<0) then
- (* we can shift *)
- SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
- else
- (* continue search *)
- next max (len+1) (sum+x1) (x2::xs)
- (* only consider those types for which the size is not fixed *)
- val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs
- (* subtract 'minsize' from every size (will be added again at the end) *)
- val diffs = map (fn (_, n) => n-minsize) mutables
- in
- case next (maxsize-minsize) 0 0 diffs of
- SOME diffs' =>
- (* merge with those types for which the size is fixed *)
- SOME (fst (fold_map (fn (T, _) => fn ds =>
- case AList.lookup (op =) sizes (string_of_typ T) of
- (* return the fixed size *)
- SOME n => ((T, n), ds)
- (* consume the head of 'ds', add 'minsize' *)
- | NONE => ((T, minsize + hd ds), tl ds))
- xs diffs'))
- | NONE => NONE
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* toTrue: converts the interpretation of a Boolean value to a propositional *)
-(* formula that is true iff the interpretation denotes "true" *)
-(* ------------------------------------------------------------------------- *)
-
-(* 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 ("<eta_expand>", 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 *)
- (* "\<lambda>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;
-