| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 13 kB |
|
SSL refute.ML Sprache: SML |
|||||||||
|
(* Title: HOL/Library/refute.ML
Author: Tjark Weber, TU Muenchen Finite model generation for HOL formulas, using a SAT solver. *) signature REFUTE = sig exception REFUTE of string * string (* ------------------------------------------------------------------------- *) (* Model/interpretation related code (translation HOL -> propositional logic *) (* ------------------------------------------------------------------------- *) type params type interpretation type model type arguments exception MAXVARS_EXCEEDED val add_interpreter : string -> (Proof.context -> model -> arguments -> term -> (interpretation * model * arguments) option) -> theory -> theory val add_printer : string -> (Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term option) -> theory -> theory val interpret : Proof.context -> model -> arguments -> term -> (interpretation * model * arguments) val print : Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term val print_model : Proof.context -> model -> (int -> bool) -> string (* ------------------------------------------------------------------------- *) (* Interface *) (* ------------------------------------------------------------------------- *) val set_default_param : (string * string) -> theory -> theory val get_default_param : Proof.context -> string -> string option val get_default_params : Proof.context -> (string * 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 (* ------------------------------------------------------------------------- *) (* Additional functions used by Nitpick (to be factored out) *) (* ------------------------------------------------------------------------- *) val get_classdef : theory -> string -> (string * term) option val norm_rhs : term -> term val get_def : theory -> string * typ -> (string * term) option val get_typedef : theory -> typ -> (string * term) option val is_IDT_constructor : theory -> string * typ -> bool val is_IDT_recursor : theory -> string * typ -> bool val is_const_of_class: theory -> string * typ -> bool val string_of_typ : typ -> string end; structure Refute : REFUTE = struct open Prop_Logic; (* We use 'REFUTE' only for internal error conditions that should *) (* never occur in the first place (i.e. errors caused by bugs in our *) (* code). Otherwise (e.g. to indicate invalid input data) we use *) (* 'error'. *) exception REFUTE of string * string; (* ("in function", "cause") *) (* should be raised by an interpreter when more variables would be *) (* required than allowed by 'maxvars' *) exception MAXVARS_EXCEEDED; (* ------------------------------------------------------------------------- *) (* TREES *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* tree: implements an arbitrarily (but finitely) branching tree as a list *) (* of (lists of ...) elements *) (* ------------------------------------------------------------------------- *) datatype 'a tree = Leaf of 'a | Node of ('a tree) list; fun tree_map f tr = case tr of Leaf x => Leaf (f x) | Node xs => Node (map (tree_map f) xs); fun tree_pair (t1, t2) = case t1 of Leaf x => (case t2 of Leaf y => Leaf (x,y) | Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)")) | Node xs => (case t2 of (* '~~' will raise an exception if the number of branches in *) (* both trees is different at the current node *) Node ys => Node (map tree_pair (xs ~~ ys)) | Leaf _ => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)")); (* ------------------------------------------------------------------------- *) (* params: parameters that control the translation into a propositional *) (* formula/model generation *) (* *) (* The following parameters are supported (and required (!), except for *) (* "sizes" and "expect"): *) (* *) (* Name Type Description *) (* *) (* "sizes" (string * int) list *) (* Size of ground types (e.g. 'a=2), or depth of IDTs. *) (* "minsize" int If >0, minimal size of each ground type/IDT depth. *) (* "maxsize" int If >0, maximal size of each ground type/IDT depth. *) (* "maxvars" int If >0, use at most 'maxvars' Boolean variables *) (* when transforming the term into a propositional *) (* formula. *) (* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) (* "satsolver" string SAT solver to be used. *) (* "no_assms" bool If "true", assumptions in structured proofs are *) (* not considered. *) (* "expect" string Expected result ("genuine", "potential", "none", or *) (* "unknown"). *) (* ------------------------------------------------------------------------- *) type params = { sizes : (string * int) list, minsize : int, maxsize : int, maxvars : int, maxtime : int, satsolver: string, no_assms : bool, expect : string }; (* ------------------------------------------------------------------------- *) (* interpretation: a term's interpretation is given by a variable of type *) (* 'interpretation' *) (* ------------------------------------------------------------------------- *) type interpretation = prop_formula list tree; (* ------------------------------------------------------------------------- *) (* model: a model specifies the size of types and the interpretation of *) (* terms *) (* ------------------------------------------------------------------------- *) type model = (typ * int) list * (term * interpretation) list; (* ------------------------------------------------------------------------- *) (* arguments: additional arguments required during interpretation of terms *) (* ------------------------------------------------------------------------- *) type arguments = { (* just passed unchanged from 'params': *) maxvars : int, (* whether to use 'make_equality' or 'make_def_equality': *) def_eq : bool, (* the following may change during the translation: *) next_idx : int, bounds : interpretation list, wellformed: prop_formula }; structure Data = Theory_Data ( type T = {interpreters: (string * (Proof.context -> model -> arguments -> term -> (interpretation * model * arguments) option)) list, printers: (string * (Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term option)) list, parameters: string Symtab.table}; val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; fun merge ({interpreters = in1, printers = pr1, parameters = pa1}, {interpreters = in2, printers = pr2, parameters = pa2}) : T = {interpreters = AList.merge (op =) (K true) (in1, in2), printers = AList.merge (op =) (K true) (pr1, pr2), parameters = Symtab.merge (op =) (pa1, pa2)}; ); val get_data = Data.get o Proof_Context.theory_of; (* ------------------------------------------------------------------------- *) (* interpret: interprets the term 't' using a suitable interpreter; returns *) (* the interpretation and a (possibly extended) model that keeps *) (* track of the interpretation of subterms *) (* ------------------------------------------------------------------------- *) fun interpret ctxt model args t = case get_first (fn (_, f) => f ctxt model args t) (#interpreters (get_data ctxt)) of NONE => raise REFUTE ("interpret", "no interpreter for term " ^ quote (Syntax.string_of_term ctxt t)) | SOME x => x; (* ------------------------------------------------------------------------- *) (* print: converts the interpretation 'intr', which must denote a term of *) (* type 'T', into a term using a suitable printer *) (* ------------------------------------------------------------------------- *) fun print ctxt model T intr assignment = case get_first (fn (_, f) => f ctxt model T intr assignment) (#printers (get_data ctxt)) of NONE => raise REFUTE ("print", "no printer for type " ^ quote (Syntax.string_of_typ ctxt T)) | SOME x => x; (* ------------------------------------------------------------------------- *) (* print_model: turns the model into a string, using a fixed interpretation *) (* (given by an assignment for Boolean variables) and suitable *) (* printers *) (* ------------------------------------------------------------------------- *) fun print_model ctxt model assignment = let val (typs, terms) = model val typs_msg = if null typs then "empty universe (no type variables in term)\n" else "Size of types: " ^ commas (map (fn (T, i) => Syntax.string_of_typ ctxt T ^ ": " ^ string_of_int i) typs) ^ "\n" val show_consts_msg = if not (Config.get ctxt show_consts) andalso Library.exists (is_Const o fst) terms then "enable \"show_consts\" to show the interpretation of constants\n" else "" val terms_msg = if null terms then "empty interpretation (no free variables in term)\n" else cat_lines (map_filter (fn (t, intr) => (* print constants only if 'show_consts' is true *) if Config.get ctxt show_consts orelse not (is_Const t) then SOME (Syntax.string_of_term ctxt t ^ ": " ^ Syntax.string_of_term ctxt (print ctxt model (Term.type_of t) intr assignment)) else NONE) terms) ^ "\n" in typs_msg ^ show_consts_msg ^ terms_msg end; (* ------------------------------------------------------------------------- *) (* PARAMETER MANAGEMENT *) (* ------------------------------------------------------------------------- *) fun add_interpreter name f = Data.map (fn {interpreters, printers, parameters} => case AList.lookup (op =) interpreters name of NONE => {interpreters = (name, f) :: interpreters, printers = printers, parameters = parameters} | SOME _ => error ("Interpreter " ^ name ^ " already declared")); fun add_printer name f = Data.map (fn {interpreters, printers, parameters} => case AList.lookup (op =) printers name of NONE => {interpreters = interpreters, printers = (name, f) :: printers, parameters = parameters} | SOME _ => error ("Printer " ^ name ^ " already declared")); (* ------------------------------------------------------------------------- *) (* set_default_param: stores the '(name, value)' pair in Data's *) (* parameter table *) (* ------------------------------------------------------------------------- *) fun set_default_param (name, value) = Data.map (fn {interpreters, printers, parameters} => {interpreters = interpreters, printers = printers, parameters = Symtab.update (name, value) parameters}); (* ------------------------------------------------------------------------- *) (* get_default_param: retrieves the value associated with 'name' from *) (* Data's parameter table *) (* ------------------------------------------------------------------------- *) val get_default_param = Symtab.lookup o #parameters o get_data; (* ------------------------------------------------------------------------- *) (* get_default_params: returns a list of all '(name, value)' pairs that are *) (* stored in Data's parameter table *) (* ------------------------------------------------------------------------- *) val get_default_params = Symtab.dest o #parameters o get_data; (* ------------------------------------------------------------------------- *) (* actual_params: takes a (possibly empty) list 'params' of parameters that *) (* override the default parameters currently specified, and *) (* returns a record that can be passed to 'find_model'. *) (* ------------------------------------------------------------------------- *) fun actual_params ctxt override = let fun read_bool (parms, name) = case AList.lookup (op =) parms name of SOME "true" => true | SOME "false" => false | SOME s => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be \"true\" or \"false\"") | NONE => error ("parameter " ^ quote name ^ " must be assigned a value") fun read_int (parms, name) = case AList.lookup (op =) parms name of SOME s => (case Int.fromString s of SOME i => i | NONE => error ("parameter " ^ quote name ^ " (value is " ^ quote s ^ ") must be an integer value")) | NONE => error ("parameter " ^ quote name ^ " must be assigned a value") fun read_string (parms, name) = case AList.lookup (op =) parms name of SOME s => s | NONE => error ("parameter " ^ quote name ^ " must be assigned a value") (* 'override' first, defaults last: *) val allparams = override @ get_default_params ctxt val minsize = read_int (allparams, "minsize") val maxsize = read_int (allparams, "maxsize") val maxvars = read_int (allparams, "maxvars") val maxtime = read_int (allparams, "maxtime") val satsolver = read_string (allparams, "satsolver") val no_assms = read_bool (allparams, "no_assms") val expect = the_default "" (AList.lookup (op =) allparams "expect") (* all remaining parameters of the form "string=int" are collected in *) (* 'sizes' *) (* TODO: it is currently not possible to specify a size for a type *) (* whose name is one of the other parameters (e.g. 'maxvars') *) (* (string * int) list *) val sizes = map_filter (fn (name, value) => Option.map (pair name) (Int.fromString value)) (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" andalso name<>"satsolver" andalso name<>"no_assms") allparams) in {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect} end; (* ------------------------------------------------------------------------- *) (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) (* ------------------------------------------------------------------------- *) fun typ_of_dtyp _ typ_assoc (Old_Datatype_Aux.DtTFree a) = the (AList.lookup (op =) typ_assoc (Old_Datatype_Aux.DtTFree a)) | typ_of_dtyp descr typ_assoc (Old_Datatype_Aux.DtType (s, Us)) = Type (s, map (typ_of_dtyp descr typ_assoc) Us) | typ_of_dtyp descr typ_assoc (Old_Datatype_Aux.DtRec i) = let val (s, ds, _) = the (AList.lookup (op =) descr i) in Type (s, map (typ_of_dtyp descr typ_assoc) ds) end val close_form = ATP_Util.close_form val specialize_type = ATP_Util.specialize_type (* ------------------------------------------------------------------------- *) (* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that *) (* denotes membership to an axiomatic type class *) (* ------------------------------------------------------------------------- *) fun is_const_of_class thy (s, _) = let val class_const_names = map Logic.const_of_class (Sign.all_classes thy) in (* I'm not quite sure if checking the name 's' is sufficient, *) (* or if we should also check the type 'T'. *) member (op =) class_const_names s end; (* ------------------------------------------------------------------------- *) (* is_IDT_constructor: returns 'true' iff 'Const (s, T)' is the constructor *) (* of an inductive datatype in 'thy' *) (* ------------------------------------------------------------------------- *) fun is_IDT_constructor thy (s, T) = (case body_type T of Type (s', _) => (case BNF_LFP_Compat.get_constrs thy s' of SOME constrs => List.exists (fn (cname, cty) => cname = s andalso Sign.typ_instance thy (T, cty)) constrs | NONE => false) | _ => false); (* ------------------------------------------------------------------------- *) (* is_IDT_recursor: returns 'true' iff 'Const (s, T)' is the recursion *) (* operator of an inductive datatype in 'thy' *) (* ------------------------------------------------------------------------- *) fun is_IDT_recursor thy (s, _) = let val rec_names = Symtab.fold (append o #rec_names o snd) (BNF_LFP_Compat.get_all thy []) [] in (* I'm not quite sure if checking the name 's' is sufficient, *) (* or if we should also check the type 'T'. *) member (op =) rec_names s end; (* ------------------------------------------------------------------------- *) (* norm_rhs: maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *) (* ------------------------------------------------------------------------- *) fun norm_rhs eqn = let fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) | lambda v t = raise TERM ("lambda", [v, t]) val (lhs, rhs) = Logic.dest_equals eqn val (_, args) = Term.strip_comb lhs in fold lambda (rev args) rhs end (* ------------------------------------------------------------------------- *) (* get_def: looks up the definition of a constant *) (* ------------------------------------------------------------------------- *) fun get_def thy (s, T) = let fun get_def_ax [] = NONE | get_def_ax ((axname, ax) :: axioms) = (let val (lhs, _) = Logic.dest_equals ax (* equations only *) val c = Term.head_of lhs val (s', T') = Term.dest_Const c in if s=s' then let val typeSubs = Sign.typ_match thy (T', T) Vartab.empty val ax' = Envir.subst_term_types typeSubs ax val rhs = norm_rhs ax' in SOME (axname, rhs) end else get_def_ax axioms end handle ERROR _ => get_def_ax axioms | TERM _ => get_def_ax axioms | Type.TYPE_MATCH => get_def_ax axioms) in get_def_ax (Theory.all_axioms_of thy) end; (* ------------------------------------------------------------------------- *) (* get_typedef: looks up the definition of a type, as created by "typedef" *) (* ------------------------------------------------------------------------- *) fun get_typedef thy T = let fun get_typedef_ax [] = NONE | get_typedef_ax ((axname, ax) :: axioms) = (let fun type_of_type_definition (Const (s', T')) = if s'= \<^const_name>\ SOME T' else NONE | type_of_type_definition (Free _) = NONE | type_of_type_definition (Var _) = NONE | type_of_type_definition (Bound _) = NONE | type_of_type_definition (Abs (_, _, body)) = type_of_type_definition body | type_of_type_definition (t1 $ t2) = (case type_of_type_definition t1 of SOME x => SOME x | NONE => type_of_type_definition t2) in case type_of_type_definition ax of SOME T' => let val T'' = domain_type (domain_type T') val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty in SOME (axname, Envir.subst_term_types typeSubs ax) end | NONE => get_typedef_ax axioms end handle ERROR _ => get_typedef_ax axioms | TERM _ => get_typedef_ax axioms | Type.TYPE_MATCH => get_typedef_ax axioms) in get_typedef_ax (Theory.all_axioms_of thy) end; (* ------------------------------------------------------------------------- *) (* get_classdef: looks up the defining axiom for an axiomatic type class, as *) (* created by the "axclass" command *) (* ------------------------------------------------------------------------- *) fun get_classdef thy class = let val axname = class ^ "_class_def" in Option.map (pair axname) (AList.lookup (op =) (Theory.all_axioms_of thy) axname) end; (* ------------------------------------------------------------------------- *) (* unfold_defs: unfolds all defined constants in a term 't', beta-eta *) (* normalizes the result term; certain constants are not *) (* unfolded (cf. 'collect_axioms' and the various interpreters *) (* below): if the interpretation respects a definition anyway, *) (* that definition does not need to be unfolded *) (* ------------------------------------------------------------------------- *) (* Note: we could intertwine unfolding of constants and beta-(eta-) *) (* normalization; this would save some unfolding for terms where *) (* constants are eliminated by beta-reduction (e.g. 'K c1 c2'). On *) (* the other hand, this would cause additional work for terms where *) (* constants are duplicated by beta-reduction (e.g. 'S c1 c2 c3'). *) fun unfold_defs thy t = let fun unfold_loop t = case t of (* Pure *) Const (\<^const_name>\<open>Pure.all\<close>, _) => t | Const (\<^const_name>\<open>Pure.eq\<close>, _) => t | Const (\<^const_name>\<open>Pure.imp\<close>, _) => t | Const (\<^const_name>\<open>Pure.type\<close>, _) => t (* axiomatic type classes *) (* HOL *) | Const (\<^const_name>\<open>Trueprop\<close>, _) => t | Const (\<^const_name>\<open>Not\<close>, _) => t | (* redundant, since 'True' is also an IDT constructor *) Const (\<^const_name>\<open>True\<close>, _) => t | (* redundant, since 'False' is also an IDT constructor *) Const (\<^const_name>\<open>False\<close>, _) => t | Const (\<^const_name>\<open>undefined\<close>, _) => t | Const (\<^const_name>\<open>The\<close>, _) => t | Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) => t | Const (\<^const_name>\<open>All\<close>, _) => t | Const (\<^const_name>\<open>Ex\<close>, _) => t | Const (\<^const_name>\<open>HOL.eq\<close>, _) => t | Const (\<^const_name>\<open>HOL.conj\<close>, _) => t | Const (\<^const_name>\<open>HOL.disj\<close>, _) => t | Const (\<^const_name>\<open>HOL.implies\<close>, _) => t (* sets *) | Const (\<^const_name>\<open>Collect\<close>, _) => t | Const (\<^const_name>\<open>Set.member\<close>, _) => t (* other optimizations *) | Const (\<^const_name>\<open>Finite_Set.card\<close>, _) => t | Const (\<^const_name>\<open>Finite_Set.finite\<close>, _) => t | Const (\<^const_name>\<open>Orderings.less\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>bool\<close>])])) => t | Const (\<^const_name>\<open>Groups.plus\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) => t | Const (\<^const_name>\<open>Groups.minus\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) => t | Const (\<^const_name>\<open>Groups.times\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) => t | Const (\<^const_name>\<open>append\<close>, _) => t | Const (\<^const_name>\<open>fst\<close>, _) => t | Const (\<^const_name>\<open>snd\<close>, _) => t (* simply-typed lambda calculus *) | Const (s, T) => (if is_IDT_constructor thy (s, T) orelse is_IDT_recursor thy (s, T) then t (* do not unfold IDT constructors/recursors *) (* unfold the constant if there is a defining equation *) else case get_def thy (s, T) of SOME ((*axname*) _, rhs) => (* Note: if the term to be unfolded (i.e. 'Const (s, T)') *) (* occurs on the right-hand side of the equation, i.e. in *) (* 'rhs', we must not use this equation to unfold, because *) (* that would loop. Here would be the right place to *) (* check this. However, getting this really right seems *) (* difficult because the user may state arbitrary axioms, *) (* which could interact with overloading to create loops. *) ((*tracing (" unfolding: " ^ axname);*) unfold_loop rhs) | NONE => t) | Free _ => t | Var _ => t | Bound _ => t | Abs (s, T, body) => Abs (s, T, unfold_loop body) | t1 $ t2 => (unfold_loop t1) $ (unfold_loop t2) val result = Envir.beta_eta_contract (unfold_loop t) in result end; (* ------------------------------------------------------------------------- *) (* collect_axioms: collects (monomorphic, universally quantified, unfolded *) (* versions of) all HOL axioms that are relevant w.r.t 't' *) (* ------------------------------------------------------------------------- *) (* Note: to make the collection of axioms more easily extensible, this *) (* function could be based on user-supplied "axiom collectors", *) (* similar to 'interpret'/interpreters or 'print'/printers *) (* Note: currently we use "inverse" functions to the definitional *) (* mechanisms provided by Isabelle/HOL, e.g. for "axclass", *) (* "typedef", "definition". A more general approach could consider *) (* *every* axiom of the theory and collect it if it has a constant/ *) (* type/typeclass in common with the term 't'. *) (* Which axioms are "relevant" for a particular term/type goes hand in *) (* hand with the interpretation of that term/type by its interpreter (see *) (* way below): if the interpretation respects an axiom anyway, the axiom *) (* does not need to be added as a constraint here. *) (* To avoid collecting the same axiom multiple times, we use an *) (* accumulator 'axs' which contains all axioms collected so far. *) local fun get_axiom thy xname = Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none); val the_eq_trivial = get_axiom \<^theory>\<open>HOL\<close> "the_eq_trivial"; val someI = get_axiom \<^theory>\<open>Hilbert_Choice\<close> "someI"; in fun collect_axioms ctxt t = let val thy = Proof_Context.theory_of ctxt val _ = tracing "Adding axioms..." fun collect_this_axiom (axname, ax) axs = let val ax' = unfold_defs thy ax in if member (op aconv) axs ax' then axs else (tracing axname; collect_term_axioms ax' (ax' :: axs)) end and collect_sort_axioms T axs = let val sort = (case T of TFree (_, sort) => sort | TVar (_, sort) => sort | _ => raise REFUTE ("collect_axioms", "type " ^ Syntax.string_of_typ ctxt T ^ " is not a variable")) (* obtain axioms for all superclasses *) val superclasses = sort @ maps (Sign.super_classes thy) sort (* merely an optimization, because 'collect_this_axiom' disallows *) (* duplicate axioms anyway: *) val superclasses = distinct (op =) superclasses val class_axioms = maps (fn class => map (fn ax => ("<" ^ class ^ ">", Thm.prop_of ax)) (#axioms (Axclass.get_info thy class) handle ERROR _ => [])) superclasses (* replace the (at most one) schematic type variable in each axiom *) (* by the actual type 'T' *) val monomorphic_class_axioms = map (fn (axname, ax) => (case Term.add_tvars ax [] of [] => (axname, ax) | [(idx, S)] => (axname, Envir.subst_term_types (Vartab.make [(idx, (S, T))]) ax) | _ => raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ Syntax.string_of_term ctxt ax ^ ") contains more than one type variable"))) class_axioms in fold collect_this_axiom monomorphic_class_axioms axs end and collect_type_axioms T axs = case T of (* simple types *) Type (\<^type_name>\<open>prop\<close>, []) => axs | Type (\<^type_name>\<open>fun\<close>, [T1, T2]) => collect_type_axioms T2 (collect_type_axio | Type (\<^type_name>\<open>set\<close>, [T1]) => collect_type_axioms T1 axs (* axiomatic type classes *) | Type (\<^type_name>\<open>itself\<close>, [T1]) => collect_type_axioms T1 axs | Type (s, Ts) => (case BNF_LFP_Compat.get_info thy [] s of SOME _ => (* inductive datatype *) (* only collect relevant type axioms for the argument types *) fold collect_type_axioms Ts axs | NONE => (case get_typedef thy T of SOME (axname, ax) => collect_this_axiom (axname, ax) axs | NONE => (* unspecified type, perhaps introduced with "typedecl" *) (* at least collect relevant type axioms for the argument types *) fold collect_type_axioms Ts axs)) (* axiomatic type classes *) | TFree _ => collect_sort_axioms T axs (* axiomatic type classes *) | TVar _ => collect_sort_axioms T axs and collect_term_axioms t axs = case t of (* Pure *) Const (\<^const_name>\<open>Pure.all\<close>, _) => axs | Const (\<^const_name>\<open>Pure.eq\<close>, _) => axs | Const (\<^const_name>\<open>Pure.imp\<close>, _) => axs (* axiomatic type classes *) | Const (\<^const_name>\<open>Pure.type\<close>, T) => collect_type_axioms T axs (* HOL *) | Const (\<^const_name>\<open>Trueprop\<close>, _) => axs | Const (\<^const_name>\<open>Not\<close>, _) => axs (* redundant, since 'True' is also an IDT constructor *) | Const (\<^const_name>\<open>True\<close>, _) => axs (* redundant, since 'False' is also an IDT constructor *) | Const (\<^const_name>\<open>False\<close>, _) => axs | Const (\<^const_name>\<open>undefined\<close>, T) => collect_type_axioms T axs | Const (\<^const_name>\<open>The\<close>, T) => let val ax = specialize_type thy (\<^const_name>\<open>The\<close>, T) (#2 the_eq_trivial) in collect_this_axiom (#1 the_eq_trivial, ax) axs end | Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, T) => let val ax = specialize_type thy (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, T) (#2 someI) in collect_this_axiom (#1 someI, ax) axs end | Const (\<^const_name>\<open>All\<close>, T) => collect_type_axioms T axs | Const (\<^const_name>\<open>Ex\<close>, T) => collect_type_axioms T axs | Const (\<^const_name>\<open>HOL.eq\<close>, T) => collect_type_axioms T axs | Const (\<^const_name>\<open>HOL.conj\<close>, _) => axs | Const (\<^const_name>\<open>HOL.disj\<close>, _) => axs | Const (\<^const_name>\<open>HOL.implies\<close>, _) => axs (* sets *) | Const (\<^const_name>\<open>Collect\<close>, T) => collect_type_axioms T axs | Const (\<^const_name>\<open>Set.member\<close>, T) => collect_type_axioms T axs (* other optimizations *) | Const (\<^const_name>\<open>Finite_Set.card\<close>, T) => collect_type_axioms T axs | Const (\<^const_name>\<open>Finite_Set.finite\<close>, T) => collect_type_axioms T axs | Const (\<^const_name>\<open>Orderings.less\<close>, T as Type ("fun", [\<^typ>\<open>nat\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>bool\<close>])])) => collect_type_axioms T axs | Const (\<^const_name>\<open>Groups.plus\<close>, T as Type ("fun", [\<^typ>\<open>nat\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) => collect_type_axioms T axs | Const (\<^const_name>\<open>Groups.minus\<close>, T as Type ("fun", [\<^typ>\<open>nat\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) => collect_type_axioms T axs | Const (\<^const_name>\<open>Groups.times\<close>, T as Type ("fun", [\<^typ>\<open>nat\<close>, Type ("fun", [\<^typ>\<open>nat\<close>, \<^typ>\<open>nat\<close>])])) => collect_type_axioms T axs | Const (\<^const_name>\<open>append\<close>, T) => collect_type_axioms T axs | Const (\<^const_name>\<open>fst\<close>, T) => collect_type_axioms T axs | Const (\<^const_name>\<open>snd\<close>, T) => collect_type_axioms T axs (* simply-typed lambda calculus *) | Const (s, T) => if is_const_of_class thy (s, T) then (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *) (* and the class definition *) let val class = Logic.class_of_const s val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class) val ax_in = SOME (specialize_type thy (s, T) of_class) (* type match may fail due to sort constraints *) handle Type.TYPE_MATCH => NONE val ax_1 = Option.map (fn ax => (Syntax.string_of_term ctxt ax, ax)) ax_in val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class) in collect_type_axioms T (fold collect_this_axiom (map_filter I [ax_1, ax_2]) axs) end else if is_IDT_constructor thy (s, T) orelse is_IDT_recursor thy (s, T) then (* only collect relevant type axioms *) collect_type_axioms T axs else (* other constants should have been unfolded, with some *) (* exceptions: e.g. Abs_xxx/Rep_xxx functions for *) (* typedefs, or type-class related constants *) (* only collect relevant type axioms *) collect_type_axioms T axs | Free (_, T) => collect_type_axioms T axs | Var (_, T) => collect_type_axioms T axs | Bound _ => axs | Abs (_, T, body) => collect_term_axioms body (collect_type_axioms T axs) | t1 $ t2 => collect_term_axioms t2 (collect_term_axioms t1 axs) val result = map close_form (collect_term_axioms t []) val _ = tracing " ...done." in result end; end; (* ------------------------------------------------------------------------- *) (* ground_types: collects all ground types in a term (including argument *) (* types of other types), suppressing duplicates. Does not *) (* return function types, set types, non-recursive IDTs, or *) (* 'propT'. For IDTs, also the argument types of constructors *) (* and all mutually recursive IDTs are considered. *) (* ------------------------------------------------------------------------- *) fun ground_types ctxt t = let val thy = Proof_Context.theory_of ctxt fun collect_types T acc = (case T of Type (\<^type_name>\<open>fun\<close>, [T1, T2]) => collect_types T1 (collect_types T2 acc) | Type (\<^type_name>\<open>prop\<close>, []) => acc | Type (\<^type_name>\<open>set\<close>, [T1]) => collect_types T1 acc | Type (s, Ts) => (case BNF_LFP_Compat.get_info thy [] s of SOME info => (* inductive datatype *) let val index = #index info val descr = #descr info val (_, typs, _) = the (AList.lookup (op =) descr index) val typ_assoc = typs ~~ Ts (* sanity check: every element in 'dtyps' must be a *) (* 'DtTFree' *) val _ = if Library.exists (fn d => case d of Old_Datatype_Aux.DtTFree _ => false | _ => true) typs then raise REFUTE ("ground_types", "datatype argument (for type " ^ Syntax.string_of_typ ctxt T ^ ") is not a variable") else () (* required for mutually recursive datatypes; those need to *) (* be added even if they are an instance of an otherwise non- *) (* recursive datatype *) fun collect_dtyp d acc = let val dT = typ_of_dtyp descr typ_assoc d in case d of Old_Datatype_Aux.DtTFree _ => collect_types dT acc | Old_Datatype_Aux.DtType (_, ds) => collect_types dT (fold_rev collect_dtyp ds acc) | Old_Datatype_Aux.DtRec i => if member (op =) acc dT then acc (* prevent infinite recursion *) else let val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i) (* if the current type is a recursive IDT (i.e. a depth *) (* is required), add it to 'acc' *) val acc_dT = if Library.exists (fn (_, ds) => Library.exists Old_Datatype_Aux.is_rec_type ds) dconstrs then insert (op =) dT acc else acc (* collect argument types *) val acc_dtyps = fold_rev collect_dtyp dtyps acc_dT (* collect constructor types *) val acc_dconstrs = fold_rev collect_dtyp (maps snd dconstrs) acc_dtyps in acc_dconstrs end end in (* argument types 'Ts' could be added here, but they are also *) (* added by 'collect_dtyp' automatically *) collect_dtyp (Old_Datatype_Aux.DtRec index) acc end | NONE => (* not an inductive datatype, e.g. defined via "typedef" or *) (* "typedecl" *) insert (op =) T (fold collect_types Ts acc)) | TFree _ => insert (op =) T acc | TVar _ => insert (op =) T acc) in fold_types collect_types t [] end; (* ------------------------------------------------------------------------- *) (* string_of_typ: (rather naive) conversion from types to strings, used to *) (* look up the size of a type in 'sizes'. Parameterized *) (* types with different parameters (e.g. "'a list" vs. "bool *) (* list") are identified. *) (* ------------------------------------------------------------------------- *) fun string_of_typ (Type (s, _)) = s | string_of_typ (TFree (s, _)) = s | string_of_typ (TVar ((s,_), _)) = s; (* ------------------------------------------------------------------------- *) (* first_universe: returns the "first" (i.e. smallest) universe by assigning *) (* 'minsize' to every type for which no size is specified in *) (* 'sizes' *) (* ------------------------------------------------------------------------- *) fun first_universe xs sizes minsize = let fun size_of_typ T = case AList.lookup (op =) sizes (string_of_typ T) of SOME n => n | NONE => minsize in map (fn T => (T, size_of_typ T)) xs end; (* ------------------------------------------------------------------------- *) (* next_universe: enumerates all universes (i.e. assignments of sizes to *) (* types), where the minimal size of a type is given by *) (* 'minsize', the maximal size is given by 'maxsize', and a *) (* type may have a fixed size given in 'sizes' *) (* ------------------------------------------------------------------------- *) fun next_universe xs sizes minsize maxsize = let (* creates the "first" list of length 'len', where the sum of all list *) (* elements is 'sum', and the length of the list is 'len' *) fun make_first _ 0 sum = if sum = 0 then SOME [] else NONE | make_first max len sum = if sum <= max orelse max < 0 then Option.map (fn xs' => sum :: xs') (make_first max (len-1) 0) else Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max)) (* enumerates all int lists with a fixed length, where 0<=x<='max' for *) (* all list elements x (unless 'max'<0) *) fun next _ _ _ [] = NONE | next max len sum [x] = (* we've reached the last list element, so there's no shift possible *) make_first max (len+1) (sum+x+1) (* increment 'sum' by 1 *) | next max len sum (x1::x2::xs) = if x1>0 andalso (x2<max orelse max<0) then (* we can shift *) SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs) else (* continue search *) next max (len+1) (sum+x1) (x2::xs) (* only consider those types for which the size is not fixed *) val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs (* subtract 'minsize' from every size (will be added again at the end) *) val diffs = map (fn (_, n) => n-minsize) mutables in case next (maxsize-minsize) 0 0 diffs of SOME diffs' => (* merge with those types for which the size is fixed *) SOME (fst (fold_map (fn (T, _) => fn ds => case AList.lookup (op =) sizes (string_of_typ T) of (* return the fixed size *) SOME n => ((T, n), ds) (* consume the head of 'ds', add 'minsize' *) | NONE => ((T, minsize + hd ds), tl ds)) xs diffs')) | NONE => NONE end; (* ------------------------------------------------------------------------- *) (* toTrue: converts the interpretation of a Boolean value to a propositional *) (* formula that is true iff the interpretation denotes "true" *) (* ------------------------------------------------------------------------- *) fun toTrue (Leaf [fm, _]) = fm | toTrue _ = raise REFUTE ("toTrue", "interpretation does not denote a Boolean value"); (* ------------------------------------------------------------------------- *) (* toFalse: converts the interpretation of a Boolean value to a *) (* propositional formula that is true iff the interpretation *) (* denotes "false" *) (* ------------------------------------------------------------------------- *) fun toFalse (Leaf [_, fm]) = fm | toFalse _ = raise REFUTE ("toFalse", "interpretation does not denote a Boolean value" (* ------------------------------------------------------------------------- *) (* find_model: repeatedly calls 'interpret' with appropriate parameters, *) (* applies a SAT solver, and (in case a model is found) displays *) (* the model to the user by calling 'print_model' *) (* {...} : parameters that control the translation/model generation *) (* assm_ts : assumptions to be considered unless "no_assms" is specified *) (* t : term to be translated into a propositional formula *) (* negate : if true, find a model that makes 't' false (rather than true) *) (* ------------------------------------------------------------------------- *) fun find_model ctxt {sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect} assm_ts t negate = let val thy = Proof_Context.theory_of ctxt fun check_expect outcome_code = if expect = "" orelse outcome_code = expect then outcome_code else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") fun wrapper () = let val time_start = Time.now () val t = if no_assms then t else if negate then Logic.list_implies (assm_ts, t) else Logic.mk_conjunction_list (t :: assm_ts) val u = unfold_defs thy t val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term ctxt u) val axioms = collect_axioms ctxt u val types = fold (union (op =) o ground_types ctxt) (u :: axioms) [] val _ = tracing ("Ground types: " ^ (if null types then "none." else commas (map (Syntax.string_of_typ ctxt) types))) (* we can only consider fragments of recursive IDTs, so we issue a *) (* warning if the formula contains a recursive IDT *) (* TODO: no warning needed for /positive/ occurrences of IDTs *) val maybe_spurious = Library.exists (fn Type (s, _) => (case BNF_LFP_Compat.get_info thy [] s of SOME info => (* inductive datatype *) let val index = #index info val descr = #descr info val (_, _, constrs) = the (AList.lookup (op =) descr index) in (* recursive datatype? *) Library.exists (fn (_, ds) => Library.exists Old_Datatype_Aux.is_rec_type ds) constrs end | NONE => false) | _ => false) types val _ = if maybe_spurious andalso Context_Position.is_visible ctxt then warning "Term contains a recursive datatype; countermodel(s) may be spurious!" else () fun find_model_loop universe = let val time_spent = Time.now () - time_start val _ = maxtime = 0 orelse time_spent < Timeout.scale_time (Time.fromSeconds maxtime) orelse raise Timeout.TIMEOUT time_spent val init_model = (universe, []) val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, bounds = [], wellformed = True} val _ = tracing ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") (* translate 'u' and all axioms *) val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) => let val (i, m', a') = interpret ctxt m a t' in (* set 'def_eq' to 'true' *) (i, (m', {maxvars = #maxvars a', def_eq = true, next_idx = #next_idx a', bounds = #bounds a', wellformed = #wellformed a'})) end) (u :: axioms) (init_model, init_args) (* make 'u' either true or false, and make all axioms true, and *) (* add the well-formedness side condition *) val fm_u = (if negate then toFalse else toTrue) (hd intrs) val fm_ax = Prop_Logic.all (map toTrue (tl intrs)) val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u] val _ = (if member (op =) ["cdclite"] satsolver andalso Context_Position.is_visible ctxt then warning ("Using SAT solver " ^ quote satsolver ^ "; for better performance, consider installing an \ \external solver.") else ()); val solver = SAT_Solver.invoke_solver satsolver handle Option.Option => error ("Unknown SAT solver: " ^ quote satsolver ^ ". Available solvers: " ^ commas (map (quote o fst) (SAT_Solver.get_solvers ())) ^ ".") in writeln "Invoking SAT solver..."; (case solver fm of SAT_Solver.SATISFIABLE assignment => (writeln ("Model found:\n" ^ print_model ctxt model (fn i => case assignment i of SOME b => b | NONE => true)); if maybe_spurious then "potential" else "genuine") | SAT_Solver.UNSATISFIABLE _ => (writeln "No model exists."; case next_universe universe sizes minsize maxsize of SOME universe' => find_model_loop universe' | NONE => (writeln "Search terminated, no larger universe within the given limits."; "none")) | SAT_Solver.UNKNOWN => (writeln "No model found."; case next_universe universe sizes minsize maxsize of SOME universe' => find_model_loop universe' | NONE => (writeln "Search terminated, no larger universe within the given limits."; "unknown"))) handle SAT_Solver.NOT_CONFIGURED => (error ("SAT solver " ^ quote satsolver ^ " is not configured."); "unknown") end handle MAXVARS_EXCEEDED => (writeln ("Search terminated, number of Boolean variables (" ^ string_of_int maxvars ^ " allowed) exceeded."); "unknown") val outcome_code = find_model_loop (first_universe types sizes minsize) in check_expect outcome_code end in (* some parameter sanity checks *) minsize>=1 orelse error ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1"); maxsize>=1 orelse error ("\"maxsize\" is " ^ string_of_int maxsize ^ ", must be at least 1"); maxsize>=minsize orelse error ("\"maxsize\" (=" ^ string_of_int maxsize ^ ") is less than \"minsize\" (=" ^ string_of_int minsize ^ ")."); maxvars>=0 orelse error ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0"); maxtime>=0 orelse error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0"); (* enter loop with or without time limit *) writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": " ^ Syntax.string_of_term ctxt t); Timeout.apply (Time.fromSeconds maxtime) wrapper () handle Timeout.TIMEOUT _ => (writeln ("Search terminated, time limit (" ^ string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded."); check_expect "unknown") end; (* ------------------------------------------------------------------------- *) (* INTERFACE, PART 2: FINDING A MODEL *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* satisfy_term: calls 'find_model' to find a model that satisfies 't' *) (* params : list of '(name, value)' pairs used to override default *) (* parameters *) (* ------------------------------------------------------------------------- *) fun satisfy_term ctxt params assm_ts t = find_model ctxt (actual_params ctxt params) assm_ts t false; (* ------------------------------------------------------------------------- *) (* refute_term: calls 'find_model' to find a model that refutes 't' *) (* params : list of '(name, value)' pairs used to override default *) (* parameters *) (* ------------------------------------------------------------------------- *) fun refute_term ctxt params assm_ts t = let (* disallow schematic type variables, since we cannot properly negate *) (* terms containing them (their logical meaning is that there EXISTS a *) (* type s.t. ...; to refute such a formula, we would have to show that *) (* for ALL types, not ...) *) val _ = null (Term.add_tvars t []) orelse error "Term to be refuted contains schematic type variables" (* existential closure over schematic variables *) val vars = sort_by (fst o fst) (Term.add_vars t []) (* Term.term *) val ex_closure = fold (fn ((x, i), T) => fn t' => HOLogic.exists_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t (* Note: If 't' is of type 'propT' (rather than 'boolT'), applying *) (* 'HOLogic.exists_const' is not type-correct. However, this is not *) (* really a problem as long as 'find_model' still interprets the *) (* resulting term correctly, without checking its type. *) (* replace outermost universally quantified variables by Free's: *) (* refuting a term with Free's is generally faster than refuting a *) (* term with (nested) quantifiers, because quantifiers are expanded, *) (* while the SAT solver searches for an interpretation for Free's. *) (* Also we get more information back that way, namely an *) (* interpretation which includes values for the (formerly) *) (* quantified variables. *) (* maps !!x1...xn. !xk...xm. t to t *) fun strip_all_body (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t)) = strip_all_body t | strip_all_body (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t) = strip_all_body t | strip_all_body (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = strip_all_body t | strip_all_body t = t (* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *) fun strip_all_vars (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t | strip_all_vars (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t) = strip_all_vars t | strip_all_vars (Const (\<^const_name>\<open>All\<close>, _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t | strip_all_vars _ = [] : (string * typ) list val strip_t = strip_all_body ex_closure val frees = Term.variant_bounds strip_t (strip_all_vars ex_closure) val subst_t = Term.subst_bounds (map Free (rev frees), strip_t) in find_model ctxt (actual_params ctxt params) assm_ts subst_t true end; (* ------------------------------------------------------------------------- *) (* refute_goal *) (* ------------------------------------------------------------------------- *) fun refute_goal ctxt params th i = let val t = th |> Thm.prop_of in if Logic.no_prems t then (writeln "No subgoal!"; "none") else let val assms = map Thm.term_of (Assumption.all_assms_of ctxt) val (t, frees) = Logic.goal_params t i in refute_term ctxt params assms (subst_bounds (frees, t)) end end (* ------------------------------------------------------------------------- *) (* INTERPRETERS: Auxiliary Functions *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* make_constants: returns all interpretations for type 'T' that consist of *) (* unit vectors with 'True'/'False' only (no Boolean *) (* variables) *) (* ------------------------------------------------------------------------- *) fun make_constants ctxt model T = let (* returns a list with all unit vectors of length n *) fun unit_vectors n = let (* returns the k-th unit vector of length n *) fun unit_vector (k, n) = Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False))) fun unit_vectors_loop k = if k>n then [] else unit_vector (k,n) :: unit_vectors_loop (k+1) in unit_vectors_loop 1 end (* returns a list of lists, each one consisting of n (possibly *) (* identical) elements from 'xs' *) fun pick_all 1 xs = map single xs | pick_all n xs = let val rec_pick = pick_all (n - 1) xs in maps (fn x => map (cons x) rec_pick) xs end (* returns all constant interpretations that have the same tree *) (* structure as the interpretation argument *) fun make_constants_intr (Leaf xs) = unit_vectors (length xs) | make_constants_intr (Node xs) = map Node (pick_all (length xs) (make_constants_intr (hd xs))) (* obtain the interpretation for a variable of type 'T' *) val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) in make_constants_intr i end; (* ------------------------------------------------------------------------- *) (* size_of_type: returns the number of elements in a type 'T' (i.e. 'length *) (* (make_constants T)', but implemented more efficiently) *) (* ------------------------------------------------------------------------- *) (* returns 0 for an empty ground type or a function type with empty *) (* codomain, but fails for a function type with empty domain -- *) (* admissibility of datatype constructor argument types (see "Inductive *) (* datatypes in HOL - lessons learned ...", S. Berghofer, M. Wenzel, *) (* TPHOLs 99) ensures that recursive, possibly empty, datatype fragments *) (* never occur as the domain of a function type that is the type of a *) (* constructor argument *) fun size_of_type ctxt model T = let (* returns the number of elements that have the same tree structure as a *) (* given interpretation *) fun size_of_intr (Leaf xs) = length xs | size_of_intr (Node xs) = Integer.pow (length xs) (size_of_intr (hd xs)) (* obtain the interpretation for a variable of type 'T' *) val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) in size_of_intr i end; (* ------------------------------------------------------------------------- *) (* TT/FF: interpretations that denote "true" or "false", respectively *) (* ------------------------------------------------------------------------- *) val TT = Leaf [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. *) fun make_equality (i1, i2) = let fun equal (i1, i2) = (case i1 of Leaf xs => (case i2 of Leaf ys => Prop_Logic.dot_product (xs, ys) (* defined and equal *) | Node _ => raise REFUTE ("make_equality", "second interpretation is higher")) | Node xs => (case i2 of Leaf _ => raise REFUTE ("make_equality", "first interpretation is higher") | Node ys => Prop_Logic.all (map equal (xs ~~ ys)))) fun not_equal (i1, i2) = (case i1 of Leaf xs => (case i2 of (* defined and not equal *) Leaf ys => Prop_Logic.all ((Prop_Logic.exists xs) :: (Prop_Logic.exists ys) :: (map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys))) | Node _ => raise REFUTE ("make_equality", "second interpretation is higher")) | Node xs => (case i2 of Leaf _ => raise REFUTE ("make_equality", "first interpretation is higher") | Node ys => Prop_Logic.exists (map not_equal (xs ~~ ys)))) in (* a value may be undefined; therefore 'not_equal' is not just the *) (* negation of 'equal' *) Leaf [equal (i1, i2), not_equal (i1, i2)] end; (* ------------------------------------------------------------------------- *) (* make_def_equality: returns an interpretation that denotes (extensional) *) (* equality of two interpretations *) (* This function treats undefined/partially defined interpretations *) (* different from 'make_equality': two undefined interpretations are *) (* considered equal, while a defined interpretation is considered not equal *) (* to an undefined interpretation. *) (* ------------------------------------------------------------------------- *) fun make_def_equality (i1, i2) = let fun equal (i1, i2) = (case i1 of Leaf xs => (case i2 of (* defined and equal, or both undefined *) Leaf ys => SOr (Prop_Logic.dot_product (xs, ys), SAnd (Prop_Logic.all (map SNot xs), Prop_Logic.all (map SNot ys))) | Node _ => raise REFUTE ("make_def_equality", --> -------------------- --> maximum size reached --> -------------------- ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.18Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Bot Zugriff |
|
2026-03-28