fixed eta-expansion: introduce a couple of abstractions at once

merged

made sml/nj happy

removing file refute_isar.ML that was missed in 4006f5c3f421

added nitpick to mutabelle script

reactivating nitpick in Mutabelle

more appropriate closures for static evaluation

more uniform naming

merged

merged

updated generated files

simplified evaluation function names

turned simp_trace_depth_limit into a configuration option

add notsqsubseteq syntax

show: display goal refinement rule as "state", to avoid odd Output.urgent_message and make its association with the goal more explicit;

make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts)

merged

adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition

added enum_term_of to correct present nested functions

adding postprocessing for sets in term construction of quickcheck

merged

fixed trigger inference: testing if a theorem already has a trigger was too strict; fixed monomorphization with respect to triggers (which might occur schematically)

fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)

the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils

facilitate debugging

merged

clean up fudge factors a little bit

added weights to SMT problems

move facts supplied with "add:" to the front, so that they get a better weight (SMT)

beautify MacLaurin proofs; make better use of DERIV_intros

workaround for bug in weight handling -- sometimes numerals got replaced by Vars and this confused the weight extractor

avoid ML structure aliases (especially single-letter abbreviations);

eliminated dead code;

more correct ML snippets that are unchecked; tuned comments;

merged

Added two theorems about the concept of range. Tidied up the comments.

honor "overlord" option for SMT solvers as well and don't pass "ext" to them

make Sledgehammer's relevance filter include the "ext" rule when appropriate

tuning

tuning

added support for "type_sys" option to Mirabelle

honor "metisFT" in Mirabelle

make "full_types" take precedence over "type_sys"

crank up Metis's timeout for SMT solvers, since users love Metis

generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction

make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences

consider "finite" overloaded in "precise_overloaded_args" mode

added timeout max for remote server invocation

fix translation of higher-order equality ("fequal") if "precise_overloaded_args" is "true"

fix Vampire parsing problem

improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags

example tuning

remove at most one double negation -- any other double negations are part of some higher-order reasoning and should be left alone, cf. "HO_Reas.thy"

weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed

added example to exercise higher-order reasoning with Sledgehammer and Metis

added Sledgehammer support for higher-order propositional reasoning

add Metis support for higher-order propositional reasoning

implemented partially-typed "tags" type encoding

implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations

implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound

tuning: unused var

added "type_sys" option to Sledgehammer

merged

updated SMT certificates

fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)

adapted the Z3 proof parser to recent changes in Z3's proof format; keep the proof steps in an ordered list instead of in an Inttab (simplifies proof reconstruction code)

also show function definitions for higher-order free variables in Z3 models

always add pair rules and function update rules automatically (Boogie provides pairs and function update as built-in concepts and does not generate background axioms for them)

re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure); abolished SMT interface concept in favor of solver classes (now also the translation configuration is stored in the context); proof reconstruction is now expected to return a theorem stating False (and hence needs to discharge all hypothetical definitions); built-in functions carry additionally their arity and their most general type; slightly generalized the definition of fun_app

re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level); added simple trigger inference mechanism; added syntactic checks for triggers and quantifier weights; factored out the normalization of special quantifiers (used to be in the eta-normalization part); normalization now unfolds abs/min/max (not SMT-LIB-specific); rules for pairs and function update are not anymore added automatically to the problem; more aggressive rewriting of natural number operations into integer operations (minimizes the number of remaining nat-int coercions); normalizations are now managed in a class-based manner (similar to built-in symbols)

added option to enable trigger inference; better documentation of triggers and SMT available options

moved SMT classes and dictionary functions to SMT_Utils

tuned

rewrite Z3 model equations one-by-one (the previous approach led to loss of information)

added option to modify the random seed of SMT solvers

adding an Isar version of the MacLaurin theorem from some students' work in 2005

Admin/contributed_components tries to formalize compatibility with external components (for use e.g. by testing tools), guessing from the content of TUM contrib_devel directory

separated dictionary weakning into separate type

eliminated dest_all_all_ctx

private term variant of Variable.focus

adding an executable THE operator on finite types

tuned headers

added signature; more honest header

add HOLCF library theories with cpo/predomain instances for HOL types

xsymbol notation for powerdomain types

new powerdomain lemmas

made smlnj happy

merged

moved most fundamental lemmas upwards

setting finite_type_size to 1 in mutabelle_extra

adding check_all instances for a few more finite types in smallcheck

removing unneccassary sort constraints

made smlnj happy

merged

tuned names

dictionary constants must permit explicit weakening of classes; tuned names

tracing of term to be evaluated

merged

use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand

integral over setprod

cleanup bijectivity btw. product spaces and pairs

compile

lower fudge factor

reword error message

implicitly call the minimizer for SMT solvers that don't return an unsat core

renamings

moved function to later module

clarified terminology

split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems

if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck

adding a smarter enumeration scheme for finite functions

merged

work around problems with eta-expansion of equations

bot comes before top, inf before sup etc.

tuned

nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules

NEWS

adding more efficient implementations for quantifiers in Enum

improving the mutabelle script

primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`; tuned

primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`

hide popular names R and B

built-in numbers are also built-in terms

be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)

merged

more concise case names; proved extensionality

name filter operation just filter (c.f. List.filter and list comprehension syntax)

tuned whitespace